69 open Hints_declaration
87 (** val make_parts : ByteValues.part List.list **)
89 List.map ByteValues.part_from_sig (Lists.range_strong AST.size_pointer)
91 (** val make_be_null : ByteValues.beval List.list **)
93 List.map (fun p -> ByteValues.BVnull p) make_parts
95 (** val bytes_of_bitvector :
96 Nat.nat -> BitVector.bitVector -> BitVector.byte List.list **)
97 let rec bytes_of_bitvector n v =
99 | Nat.O -> (fun x -> List.Nil)
102 let { Types.fst = h; Types.snd = t } =
103 Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
105 (Nat.times m (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
106 (Nat.S Nat.O))))))))) v0
108 List.Cons (h, (bytes_of_bitvector m t)))) v
110 (** val fe_to_be_values :
111 AST.typ -> Values.val0 -> ByteValues.beval List.list **)
112 let fe_to_be_values t = function
113 | Values.Vundef -> List.make_list ByteValues.BVundef (AST.typesize t)
114 | Values.Vint (sz, i) ->
115 List.map (fun b -> ByteValues.BVByte b)
116 (bytes_of_bitvector (AST.size_intsize sz) i)
117 | Values.Vnull -> make_be_null
118 | Values.Vptr ptr -> ByteValues.bevals_of_pointer ptr
120 (** val check_be_null :
121 Nat.nat -> ByteValues.beval List.list -> Bool.bool **)
122 let rec check_be_null n = function
123 | List.Nil -> Nat.eqb AST.size_pointer n
124 | List.Cons (hd, tl) ->
126 | ByteValues.BVundef -> Bool.False
127 | ByteValues.BVnonzero -> Bool.False
128 | ByteValues.BVXor (x, x0, x1) -> Bool.False
129 | ByteValues.BVByte x -> Bool.False
130 | ByteValues.BVnull pt ->
131 Bool.andb (Nat.eqb (ByteValues.part_no pt) n)
132 (check_be_null (Nat.S n) tl)
133 | ByteValues.BVptr (x, x0) -> Bool.False
134 | ByteValues.BVpc (x, x0) -> Bool.False)
136 (** val build_integer :
137 Nat.nat -> ByteValues.beval List.list -> BitVector.bitVector Types.option **)
138 let rec build_integer n l =
142 | List.Nil -> Types.Some Vector.VEmpty
143 | List.Cons (x, x0) -> Types.None)
146 | List.Nil -> Types.None
147 | List.Cons (h, t) ->
149 | ByteValues.BVundef -> Types.None
150 | ByteValues.BVnonzero -> Types.None
151 | ByteValues.BVXor (x, x0, x1) -> Types.None
152 | ByteValues.BVByte b ->
153 Types.option_map (fun tl ->
154 Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
156 (Nat.times m (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
157 (Nat.S Nat.O))))))))) b tl) (build_integer m t)
158 | ByteValues.BVnull x -> Types.None
159 | ByteValues.BVptr (x, x0) -> Types.None
160 | ByteValues.BVpc (x, x0) -> Types.None))
162 (** val build_integer_val :
163 AST.typ -> ByteValues.beval List.list -> Values.val0 **)
164 let build_integer_val t l =
166 | AST.ASTint (sz, sg) ->
167 Types.option_map_def (fun x -> Values.Vint (sz, x)) Values.Vundef
168 (build_integer (AST.size_intsize sz) l)
169 | AST.ASTptr -> Values.Vundef
171 (** val be_to_fe_value :
172 AST.typ -> ByteValues.beval List.list -> Values.val0 **)
173 let be_to_fe_value ty l = match l with
174 | List.Nil -> Values.Vundef
175 | List.Cons (h, t) ->
177 | ByteValues.BVundef -> Values.Vundef
178 | ByteValues.BVnonzero -> Values.Vundef
179 | ByteValues.BVXor (x, x0, x1) -> Values.Vundef
180 | ByteValues.BVByte b -> build_integer_val ty l
181 | ByteValues.BVnull pt ->
182 (match Bool.andb (Nat.eqb (ByteValues.part_no pt) Nat.O)
183 (check_be_null (Nat.S Nat.O) t) with
184 | Bool.True -> Values.Vnull
185 | Bool.False -> Values.Vundef)
186 | ByteValues.BVptr (x, x0) ->
187 (match ByteValues.pointer_of_bevals l with
188 | Errors.OK ptr -> Values.Vptr ptr
189 | Errors.Error x1 -> Values.Vundef)
190 | ByteValues.BVpc (x, x0) -> Values.Vundef)