19 open Hints_declaration
83 | Vint of AST.intsize * AST.bvint
85 | Vptr of Pointers.pointer
87 (** val val_rect_Type4 :
88 'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
89 'a1) -> val0 -> 'a1 **)
90 let rec val_rect_Type4 h_Vundef h_Vint h_Vnull h_Vptr = function
92 | Vint (sz, x_5112) -> h_Vint sz x_5112
94 | Vptr x_5113 -> h_Vptr x_5113
96 (** val val_rect_Type5 :
97 'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
98 'a1) -> val0 -> 'a1 **)
99 let rec val_rect_Type5 h_Vundef h_Vint h_Vnull h_Vptr = function
101 | Vint (sz, x_5119) -> h_Vint sz x_5119
103 | Vptr x_5120 -> h_Vptr x_5120
105 (** val val_rect_Type3 :
106 'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
107 'a1) -> val0 -> 'a1 **)
108 let rec val_rect_Type3 h_Vundef h_Vint h_Vnull h_Vptr = function
110 | Vint (sz, x_5126) -> h_Vint sz x_5126
112 | Vptr x_5127 -> h_Vptr x_5127
114 (** val val_rect_Type2 :
115 'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
116 'a1) -> val0 -> 'a1 **)
117 let rec val_rect_Type2 h_Vundef h_Vint h_Vnull h_Vptr = function
119 | Vint (sz, x_5133) -> h_Vint sz x_5133
121 | Vptr x_5134 -> h_Vptr x_5134
123 (** val val_rect_Type1 :
124 'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
125 'a1) -> val0 -> 'a1 **)
126 let rec val_rect_Type1 h_Vundef h_Vint h_Vnull h_Vptr = function
128 | Vint (sz, x_5140) -> h_Vint sz x_5140
130 | Vptr x_5141 -> h_Vptr x_5141
132 (** val val_rect_Type0 :
133 'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
134 'a1) -> val0 -> 'a1 **)
135 let rec val_rect_Type0 h_Vundef h_Vint h_Vnull h_Vptr = function
137 | Vint (sz, x_5147) -> h_Vint sz x_5147
139 | Vptr x_5148 -> h_Vptr x_5148
141 (** val val_inv_rect_Type4 :
142 val0 -> (__ -> 'a1) -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (__ ->
143 'a1) -> (Pointers.pointer -> __ -> 'a1) -> 'a1 **)
144 let val_inv_rect_Type4 hterm h1 h2 h3 h4 =
145 let hcut = val_rect_Type4 h1 h2 h3 h4 hterm in hcut __
147 (** val val_inv_rect_Type3 :
148 val0 -> (__ -> 'a1) -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (__ ->
149 'a1) -> (Pointers.pointer -> __ -> 'a1) -> 'a1 **)
150 let val_inv_rect_Type3 hterm h1 h2 h3 h4 =
151 let hcut = val_rect_Type3 h1 h2 h3 h4 hterm in hcut __
153 (** val val_inv_rect_Type2 :
154 val0 -> (__ -> 'a1) -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (__ ->
155 'a1) -> (Pointers.pointer -> __ -> 'a1) -> 'a1 **)
156 let val_inv_rect_Type2 hterm h1 h2 h3 h4 =
157 let hcut = val_rect_Type2 h1 h2 h3 h4 hterm in hcut __
159 (** val val_inv_rect_Type1 :
160 val0 -> (__ -> 'a1) -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (__ ->
161 'a1) -> (Pointers.pointer -> __ -> 'a1) -> 'a1 **)
162 let val_inv_rect_Type1 hterm h1 h2 h3 h4 =
163 let hcut = val_rect_Type1 h1 h2 h3 h4 hterm in hcut __
165 (** val val_inv_rect_Type0 :
166 val0 -> (__ -> 'a1) -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (__ ->
167 'a1) -> (Pointers.pointer -> __ -> 'a1) -> 'a1 **)
168 let val_inv_rect_Type0 hterm h1 h2 h3 h4 =
169 let hcut = val_rect_Type0 h1 h2 h3 h4 hterm in hcut __
171 (** val val_discr : val0 -> val0 -> __ **)
173 Logic.eq_rect_Type2 x
175 | Vundef -> Obj.magic (fun _ dH -> dH)
176 | Vint (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
177 | Vnull -> Obj.magic (fun _ dH -> dH)
178 | Vptr a0 -> Obj.magic (fun _ dH -> dH __)) y
180 (** val val_jmdiscr : val0 -> val0 -> __ **)
181 let val_jmdiscr x y =
182 Logic.eq_rect_Type2 x
184 | Vundef -> Obj.magic (fun _ dH -> dH)
185 | Vint (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
186 | Vnull -> Obj.magic (fun _ dH -> dH)
187 | Vptr a0 -> Obj.magic (fun _ dH -> dH __)) y
189 (** val vzero : AST.intsize -> val0 **)
191 Vint (sz, (BitVector.zero (AST.bitsize_of_intsize sz)))
193 (** val vone : AST.intsize -> val0 **)
195 Vint (sz, (AST.repr sz (Nat.S Nat.O)))
197 (** val mone : AST.intsize -> BitVector.bitVector **)
199 BitVectorZ.bitvector_of_Z (AST.bitsize_of_intsize sz) (Z.Neg Positive.One)
201 (** val vmone : AST.intsize -> val0 **)
205 (** val vtrue : val0 **)
209 (** val vfalse : val0 **)
213 (** val of_bool : Bool.bool -> val0 **)
214 let of_bool = function
216 | Bool.False -> vfalse
218 (** val eval_bool_of_val : val0 -> Bool.bool Errors.res **)
219 let eval_bool_of_val = function
220 | Vundef -> Errors.Error (Errors.msg ErrorMessages.ValueNotABoolean)
224 (BitVector.eq_bv (AST.bitsize_of_intsize x) i
225 (BitVector.zero (AST.bitsize_of_intsize x))))
226 | Vnull -> Errors.OK Bool.False
227 | Vptr x -> Errors.OK Bool.True
229 (** val neg : val0 -> val0 **)
234 (Arithmetic.two_complement_negation (AST.bitsize_of_intsize sz) n))
238 (** val notint : val0 -> val0 **)
239 let notint = function
243 (BitVector.exclusive_disjunction_bv (AST.bitsize_of_intsize sz) n
248 (** val notbool : val0 -> val0 **)
249 let notbool = function
253 (BitVector.eq_bv (AST.bitsize_of_intsize sz) n
254 (BitVector.zero (AST.bitsize_of_intsize sz)))
258 (** val zero_ext : AST.intsize -> val0 -> val0 **)
259 let zero_ext rsz = function
263 (Arithmetic.zero_ext (AST.bitsize_of_intsize sz)
264 (AST.bitsize_of_intsize rsz) n))
268 (** val sign_ext : AST.intsize -> val0 -> val0 **)
269 let sign_ext rsz = function
273 (Arithmetic.sign_ext (AST.bitsize_of_intsize sz)
274 (AST.bitsize_of_intsize rsz) i))
278 (** val add : val0 -> val0 -> val0 **)
286 AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Vint (sz2,
287 (Arithmetic.addition_n (AST.bitsize_of_intsize sz2) n10 n2))) Vundef
290 Vptr (Pointers.shift_pointer (AST.bitsize_of_intsize sz1) ptr n1))
296 Vptr (Pointers.shift_pointer (AST.bitsize_of_intsize x) ptr n2)
300 (** val sub : val0 -> val0 -> val0 **)
308 AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Vint (sz2,
309 (Arithmetic.subtraction (AST.bitsize_of_intsize sz2) n10 n2)))
316 | Vint (x, x0) -> Vundef
317 | Vnull -> vzero AST.I32
323 Vptr (Pointers.neg_shift_pointer (AST.bitsize_of_intsize sz2) ptr1 n2)
326 (match Pointers.eq_block ptr1.Pointers.pblock ptr2.Pointers.pblock with
329 (Pointers.sub_offset (AST.bitsize_of_intsize AST.I32)
330 ptr1.Pointers.poff ptr2.Pointers.poff))
331 | Bool.False -> Vundef))
333 (** val mul : val0 -> val0 -> val0 **)
341 AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Vint (sz2,
342 (Vector.vsplit (AST.bitsize_of_intsize sz2)
343 (AST.bitsize_of_intsize sz2)
344 (Arithmetic.multiplication (AST.bitsize_of_intsize sz2) n10 n2)).Types.snd))
351 (** val v_and : val0 -> val0 -> val0 **)
359 AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Vint (sz2,
360 (BitVector.conjunction_bv (AST.bitsize_of_intsize sz2) n10 n2)))
367 (** val or0 : val0 -> val0 -> val0 **)
375 AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Vint (sz2,
376 (BitVector.inclusive_disjunction_bv (AST.bitsize_of_intsize sz2) n10
383 (** val xor : val0 -> val0 -> val0 **)
391 AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Vint (sz2,
392 (BitVector.exclusive_disjunction_bv (AST.bitsize_of_intsize sz2) n10
399 (** val cmp_match : Integers.comparison -> val0 **)
400 let cmp_match = function
401 | Integers.Ceq -> vtrue
402 | Integers.Cne -> vfalse
403 | Integers.Clt -> Vundef
404 | Integers.Cle -> Vundef
405 | Integers.Cgt -> Vundef
406 | Integers.Cge -> Vundef
408 (** val cmp_mismatch : Integers.comparison -> val0 **)
409 let cmp_mismatch = function
410 | Integers.Ceq -> vfalse
411 | Integers.Cne -> vtrue
412 | Integers.Clt -> Vundef
413 | Integers.Cle -> Vundef
414 | Integers.Cgt -> Vundef
415 | Integers.Cge -> Vundef
418 Integers.comparison -> Pointers.offset -> Pointers.offset -> Bool.bool **)
419 let cmp_offset c x y =
421 | Integers.Ceq -> Pointers.eq_offset x y
422 | Integers.Cne -> Bool.notb (Pointers.eq_offset x y)
423 | Integers.Clt -> Pointers.lt_offset x y
424 | Integers.Cle -> Bool.notb (Pointers.lt_offset y x)
425 | Integers.Cgt -> Pointers.lt_offset y x
426 | Integers.Cge -> Bool.notb (Pointers.lt_offset x y)
429 Nat.nat -> Integers.comparison -> BitVector.bitVector ->
430 BitVector.bitVector -> Bool.bool **)
431 let cmp_int n c x y =
433 | Integers.Ceq -> BitVector.eq_bv n x y
434 | Integers.Cne -> Bool.notb (BitVector.eq_bv n x y)
435 | Integers.Clt -> Arithmetic.lt_s n x y
436 | Integers.Cle -> Bool.notb (Arithmetic.lt_s n y x)
437 | Integers.Cgt -> Arithmetic.lt_s n y x
438 | Integers.Cge -> Bool.notb (Arithmetic.lt_s n x y)
441 Nat.nat -> Integers.comparison -> BitVector.bitVector ->
442 BitVector.bitVector -> Bool.bool **)
443 let cmpu_int n c x y =
445 | Integers.Ceq -> BitVector.eq_bv n x y
446 | Integers.Cne -> Bool.notb (BitVector.eq_bv n x y)
447 | Integers.Clt -> Arithmetic.lt_u n x y
448 | Integers.Cle -> Bool.notb (Arithmetic.lt_u n y x)
449 | Integers.Cgt -> Arithmetic.lt_u n y x
450 | Integers.Cge -> Bool.notb (Arithmetic.lt_u n x y)
452 (** val cmp : Integers.comparison -> val0 -> val0 -> val0 **)
460 AST.intsize_eq_elim sz1 sz2 n1 (fun n10 ->
461 of_bool (cmp_int (AST.bitsize_of_intsize sz2) c n10 n2)) Vundef
467 | Vint (x, x0) -> Vundef
468 | Vnull -> cmp_match c
469 | Vptr x -> cmp_mismatch c)
473 | Vint (x, x0) -> Vundef
474 | Vnull -> cmp_mismatch c
476 (match Pointers.eq_block ptr1.Pointers.pblock ptr2.Pointers.pblock with
478 of_bool (cmp_offset c ptr1.Pointers.poff ptr2.Pointers.poff)
479 | Bool.False -> cmp_mismatch c))
481 (** val cmpu : Integers.comparison -> val0 -> val0 -> val0 **)
489 AST.intsize_eq_elim sz1 sz2 n1 (fun n10 ->
490 of_bool (cmpu_int (AST.bitsize_of_intsize sz2) c n10 n2)) Vundef
496 | Vint (x, x0) -> Vundef
497 | Vnull -> cmp_match c
498 | Vptr x -> cmp_mismatch c)
502 | Vint (x, x0) -> Vundef
503 | Vnull -> cmp_mismatch c
505 (match Pointers.eq_block ptr1.Pointers.pblock ptr2.Pointers.pblock with
507 of_bool (cmp_offset c ptr1.Pointers.poff ptr2.Pointers.poff)
508 | Bool.False -> cmp_mismatch c))
510 (** val load_result : AST.typ -> val0 -> val0 **)
511 let rec load_result chunk v = match v with
515 | AST.ASTint (sz', sg) ->
516 (match AST.eq_intsize sz sz' with
518 | Bool.False -> Vundef)
519 | AST.ASTptr -> Vundef)
522 | AST.ASTint (x, x0) -> Vundef
523 | AST.ASTptr -> Vnull)
526 | AST.ASTint (x, x0) -> Vundef
527 | AST.ASTptr -> Vptr ptr)