source: extracted/values.ml @ 3069

Last change on this file since 3069 was 3043, checked in by sacerdot, 7 years ago

New major extraction that should have solved all remaining issues.
As tests/PROBLEMI shows, we still have some bugs with:

a) initialization of global data (regression)
b) function pointers call

File size: 13.8 KB
RevLine 
[2601]1open Preamble
2
3open Div_and_mod
4
5open Jmeq
6
7open Russell
8
9open Util
10
11open Bool
12
13open Relations
14
15open Nat
16
17open List
18
19open Hints_declaration
20
21open Core_notation
22
23open Pts
24
25open Logic
26
27open Types
28
29open Coqlib
30
[2649]31open ErrorMessages
32
[2601]33open Option
34
35open Setoids
36
37open Monad
38
39open Positive
40
41open PreIdentifiers
42
43open Errors
44
45open Proper
46
47open PositiveMap
48
49open Deqsets
50
51open Extralib
52
53open Lists
54
55open Identifiers
56
57open Integers
58
59open AST
60
61open Division
62
[2717]63open Exp
64
[2601]65open Arithmetic
66
67open Extranat
68
69open Vector
70
71open FoldStuff
72
73open BitVector
74
75open Z
76
77open BitVectorZ
78
79open Pointers
80
81type val0 =
82| Vundef
83| Vint of AST.intsize * AST.bvint
84| Vnull
85| Vptr of Pointers.pointer
86
87(** val val_rect_Type4 :
88    'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
89    'a1) -> val0 -> 'a1 **)
90let rec val_rect_Type4 h_Vundef h_Vint h_Vnull h_Vptr = function
91| Vundef -> h_Vundef
[3043]92| Vint (sz, x_5112) -> h_Vint sz x_5112
[2601]93| Vnull -> h_Vnull
[3043]94| Vptr x_5113 -> h_Vptr x_5113
[2601]95
96(** val val_rect_Type5 :
97    'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
98    'a1) -> val0 -> 'a1 **)
99let rec val_rect_Type5 h_Vundef h_Vint h_Vnull h_Vptr = function
100| Vundef -> h_Vundef
[3043]101| Vint (sz, x_5119) -> h_Vint sz x_5119
[2601]102| Vnull -> h_Vnull
[3043]103| Vptr x_5120 -> h_Vptr x_5120
[2601]104
105(** val val_rect_Type3 :
106    'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
107    'a1) -> val0 -> 'a1 **)
108let rec val_rect_Type3 h_Vundef h_Vint h_Vnull h_Vptr = function
109| Vundef -> h_Vundef
[3043]110| Vint (sz, x_5126) -> h_Vint sz x_5126
[2601]111| Vnull -> h_Vnull
[3043]112| Vptr x_5127 -> h_Vptr x_5127
[2601]113
114(** val val_rect_Type2 :
115    'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
116    'a1) -> val0 -> 'a1 **)
117let rec val_rect_Type2 h_Vundef h_Vint h_Vnull h_Vptr = function
118| Vundef -> h_Vundef
[3043]119| Vint (sz, x_5133) -> h_Vint sz x_5133
[2601]120| Vnull -> h_Vnull
[3043]121| Vptr x_5134 -> h_Vptr x_5134
[2601]122
123(** val val_rect_Type1 :
124    'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
125    'a1) -> val0 -> 'a1 **)
126let rec val_rect_Type1 h_Vundef h_Vint h_Vnull h_Vptr = function
127| Vundef -> h_Vundef
[3043]128| Vint (sz, x_5140) -> h_Vint sz x_5140
[2601]129| Vnull -> h_Vnull
[3043]130| Vptr x_5141 -> h_Vptr x_5141
[2601]131
132(** val val_rect_Type0 :
133    'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
134    'a1) -> val0 -> 'a1 **)
135let rec val_rect_Type0 h_Vundef h_Vint h_Vnull h_Vptr = function
136| Vundef -> h_Vundef
[3043]137| Vint (sz, x_5147) -> h_Vint sz x_5147
[2601]138| Vnull -> h_Vnull
[3043]139| Vptr x_5148 -> h_Vptr x_5148
[2601]140
141(** val val_inv_rect_Type4 :
142    val0 -> (__ -> 'a1) -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (__ ->
143    'a1) -> (Pointers.pointer -> __ -> 'a1) -> 'a1 **)
144let val_inv_rect_Type4 hterm h1 h2 h3 h4 =
145  let hcut = val_rect_Type4 h1 h2 h3 h4 hterm in hcut __
146
147(** val val_inv_rect_Type3 :
148    val0 -> (__ -> 'a1) -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (__ ->
149    'a1) -> (Pointers.pointer -> __ -> 'a1) -> 'a1 **)
150let val_inv_rect_Type3 hterm h1 h2 h3 h4 =
151  let hcut = val_rect_Type3 h1 h2 h3 h4 hterm in hcut __
152
153(** val val_inv_rect_Type2 :
154    val0 -> (__ -> 'a1) -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (__ ->
155    'a1) -> (Pointers.pointer -> __ -> 'a1) -> 'a1 **)
156let val_inv_rect_Type2 hterm h1 h2 h3 h4 =
157  let hcut = val_rect_Type2 h1 h2 h3 h4 hterm in hcut __
158
159(** val val_inv_rect_Type1 :
160    val0 -> (__ -> 'a1) -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (__ ->
161    'a1) -> (Pointers.pointer -> __ -> 'a1) -> 'a1 **)
162let val_inv_rect_Type1 hterm h1 h2 h3 h4 =
163  let hcut = val_rect_Type1 h1 h2 h3 h4 hterm in hcut __
164
165(** val val_inv_rect_Type0 :
166    val0 -> (__ -> 'a1) -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (__ ->
167    'a1) -> (Pointers.pointer -> __ -> 'a1) -> 'a1 **)
168let val_inv_rect_Type0 hterm h1 h2 h3 h4 =
169  let hcut = val_rect_Type0 h1 h2 h3 h4 hterm in hcut __
170
171(** val val_discr : val0 -> val0 -> __ **)
172let val_discr x y =
173  Logic.eq_rect_Type2 x
174    (match x with
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
179
180(** val val_jmdiscr : val0 -> val0 -> __ **)
181let val_jmdiscr x y =
182  Logic.eq_rect_Type2 x
183    (match x with
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
188
189(** val vzero : AST.intsize -> val0 **)
190let vzero sz =
191  Vint (sz, (BitVector.zero (AST.bitsize_of_intsize sz)))
192
193(** val vone : AST.intsize -> val0 **)
194let vone sz =
[2773]195  Vint (sz, (AST.repr sz (Nat.S Nat.O)))
[2601]196
[2773]197(** val mone : AST.intsize -> BitVector.bitVector **)
198let mone sz =
[2601]199  BitVectorZ.bitvector_of_Z (AST.bitsize_of_intsize sz) (Z.Neg Positive.One)
200
201(** val vmone : AST.intsize -> val0 **)
202let vmone sz =
[2773]203  Vint (sz, (mone sz))
[2601]204
205(** val vtrue : val0 **)
206let vtrue =
207  vone AST.I32
208
209(** val vfalse : val0 **)
210let vfalse =
211  vzero AST.I32
212
213(** val of_bool : Bool.bool -> val0 **)
214let of_bool = function
215| Bool.True -> vtrue
216| Bool.False -> vfalse
217
218(** val eval_bool_of_val : val0 -> Bool.bool Errors.res **)
219let eval_bool_of_val = function
[2649]220| Vundef -> Errors.Error (Errors.msg ErrorMessages.ValueNotABoolean)
[2601]221| Vint (x, i) ->
222  Errors.OK
223    (Bool.notb
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
228
[2773]229(** val neg : val0 -> val0 **)
230let neg = function
[2601]231| Vundef -> Vundef
232| Vint (sz, n) ->
233  Vint (sz,
234    (Arithmetic.two_complement_negation (AST.bitsize_of_intsize sz) n))
235| Vnull -> Vundef
236| Vptr x -> Vundef
237
238(** val notint : val0 -> val0 **)
239let notint = function
240| Vundef -> Vundef
241| Vint (sz, n) ->
242  Vint (sz,
243    (BitVector.exclusive_disjunction_bv (AST.bitsize_of_intsize sz) n
[2773]244      (mone sz)))
[2601]245| Vnull -> Vundef
246| Vptr x -> Vundef
247
[2773]248(** val notbool : val0 -> val0 **)
249let notbool = function
[2601]250| Vundef -> Vundef
251| Vint (sz, n) ->
252  of_bool
253    (BitVector.eq_bv (AST.bitsize_of_intsize sz) n
254      (BitVector.zero (AST.bitsize_of_intsize sz)))
255| Vnull -> vtrue
256| Vptr x -> vfalse
257
[2773]258(** val zero_ext : AST.intsize -> val0 -> val0 **)
259let zero_ext rsz = function
[2601]260| Vundef -> Vundef
261| Vint (sz, n) ->
262  Vint (rsz,
263    (Arithmetic.zero_ext (AST.bitsize_of_intsize sz)
264      (AST.bitsize_of_intsize rsz) n))
265| Vnull -> Vundef
266| Vptr x -> Vundef
267
[2773]268(** val sign_ext : AST.intsize -> val0 -> val0 **)
269let sign_ext rsz = function
[2601]270| Vundef -> Vundef
271| Vint (sz, i) ->
272  Vint (rsz,
273    (Arithmetic.sign_ext (AST.bitsize_of_intsize sz)
274      (AST.bitsize_of_intsize rsz) i))
275| Vnull -> Vundef
276| Vptr x -> Vundef
277
[2773]278(** val add : val0 -> val0 -> val0 **)
279let add v1 v2 =
[2601]280  match v1 with
281  | Vundef -> Vundef
282  | Vint (sz1, n1) ->
283    (match v2 with
284     | Vundef -> Vundef
285     | Vint (sz2, n2) ->
286       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Vint (sz2,
287         (Arithmetic.addition_n (AST.bitsize_of_intsize sz2) n10 n2))) Vundef
288     | Vnull -> Vundef
289     | Vptr ptr ->
290       Vptr (Pointers.shift_pointer (AST.bitsize_of_intsize sz1) ptr n1))
291  | Vnull -> Vundef
292  | Vptr ptr ->
293    (match v2 with
294     | Vundef -> Vundef
295     | Vint (x, n2) ->
296       Vptr (Pointers.shift_pointer (AST.bitsize_of_intsize x) ptr n2)
297     | Vnull -> Vundef
298     | Vptr x -> Vundef)
299
300(** val sub : val0 -> val0 -> val0 **)
301let sub v1 v2 =
302  match v1 with
303  | Vundef -> Vundef
304  | Vint (sz1, n1) ->
305    (match v2 with
306     | Vundef -> Vundef
307     | Vint (sz2, n2) ->
308       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Vint (sz2,
309         (Arithmetic.subtraction (AST.bitsize_of_intsize sz2) n10 n2)))
310         Vundef
311     | Vnull -> Vundef
312     | Vptr x -> Vundef)
313  | Vnull ->
314    (match v2 with
315     | Vundef -> Vundef
316     | Vint (x, x0) -> Vundef
317     | Vnull -> vzero AST.I32
318     | Vptr x -> Vundef)
319  | Vptr ptr1 ->
320    (match v2 with
321     | Vundef -> Vundef
322     | Vint (sz2, n2) ->
323       Vptr (Pointers.neg_shift_pointer (AST.bitsize_of_intsize sz2) ptr1 n2)
324     | Vnull -> Vundef
325     | Vptr ptr2 ->
326       (match Pointers.eq_block ptr1.Pointers.pblock ptr2.Pointers.pblock with
327        | Bool.True ->
328          Vint (AST.I32,
329            (Pointers.sub_offset (AST.bitsize_of_intsize AST.I32)
330              ptr1.Pointers.poff ptr2.Pointers.poff))
331        | Bool.False -> Vundef))
332
[2773]333(** val mul : val0 -> val0 -> val0 **)
334let mul v1 v2 =
[2601]335  match v1 with
336  | Vundef -> Vundef
337  | Vint (sz1, n1) ->
338    (match v2 with
339     | Vundef -> Vundef
340     | Vint (sz2, n2) ->
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))
345         Vundef
346     | Vnull -> Vundef
347     | Vptr x -> Vundef)
348  | Vnull -> Vundef
349  | Vptr x -> Vundef
350
351(** val v_and : val0 -> val0 -> val0 **)
352let v_and v1 v2 =
353  match v1 with
354  | Vundef -> Vundef
355  | Vint (sz1, n1) ->
356    (match v2 with
357     | Vundef -> Vundef
358     | Vint (sz2, n2) ->
359       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Vint (sz2,
360         (BitVector.conjunction_bv (AST.bitsize_of_intsize sz2) n10 n2)))
361         Vundef
362     | Vnull -> Vundef
363     | Vptr x -> Vundef)
364  | Vnull -> Vundef
365  | Vptr x -> Vundef
366
[2773]367(** val or0 : val0 -> val0 -> val0 **)
368let or0 v1 v2 =
[2601]369  match v1 with
370  | Vundef -> Vundef
371  | Vint (sz1, n1) ->
372    (match v2 with
373     | Vundef -> Vundef
374     | Vint (sz2, n2) ->
375       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Vint (sz2,
376         (BitVector.inclusive_disjunction_bv (AST.bitsize_of_intsize sz2) n10
377           n2))) Vundef
378     | Vnull -> Vundef
379     | Vptr x -> Vundef)
380  | Vnull -> Vundef
381  | Vptr x -> Vundef
382
[2773]383(** val xor : val0 -> val0 -> val0 **)
384let xor v1 v2 =
[2601]385  match v1 with
386  | Vundef -> Vundef
387  | Vint (sz1, n1) ->
388    (match v2 with
389     | Vundef -> Vundef
390     | Vint (sz2, n2) ->
391       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Vint (sz2,
392         (BitVector.exclusive_disjunction_bv (AST.bitsize_of_intsize sz2) n10
393           n2))) Vundef
394     | Vnull -> Vundef
395     | Vptr x -> Vundef)
396  | Vnull -> Vundef
397  | Vptr x -> Vundef
398
399(** val cmp_match : Integers.comparison -> val0 **)
400let 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
407
408(** val cmp_mismatch : Integers.comparison -> val0 **)
409let 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
416
417(** val cmp_offset :
418    Integers.comparison -> Pointers.offset -> Pointers.offset -> Bool.bool **)
419let cmp_offset c x y =
420  match c with
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)
427
428(** val cmp_int :
429    Nat.nat -> Integers.comparison -> BitVector.bitVector ->
430    BitVector.bitVector -> Bool.bool **)
431let cmp_int n c x y =
432  match c with
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)
439
440(** val cmpu_int :
441    Nat.nat -> Integers.comparison -> BitVector.bitVector ->
442    BitVector.bitVector -> Bool.bool **)
443let cmpu_int n c x y =
444  match c with
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)
451
[2773]452(** val cmp : Integers.comparison -> val0 -> val0 -> val0 **)
453let cmp c v1 v2 =
[2601]454  match v1 with
455  | Vundef -> Vundef
456  | Vint (sz1, n1) ->
457    (match v2 with
458     | Vundef -> Vundef
459     | Vint (sz2, n2) ->
460       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 ->
461         of_bool (cmp_int (AST.bitsize_of_intsize sz2) c n10 n2)) Vundef
462     | Vnull -> Vundef
463     | Vptr x -> Vundef)
464  | Vnull ->
465    (match v2 with
466     | Vundef -> Vundef
467     | Vint (x, x0) -> Vundef
468     | Vnull -> cmp_match c
469     | Vptr x -> cmp_mismatch c)
470  | Vptr ptr1 ->
471    (match v2 with
472     | Vundef -> Vundef
473     | Vint (x, x0) -> Vundef
474     | Vnull -> cmp_mismatch c
475     | Vptr ptr2 ->
476       (match Pointers.eq_block ptr1.Pointers.pblock ptr2.Pointers.pblock with
477        | Bool.True ->
478          of_bool (cmp_offset c ptr1.Pointers.poff ptr2.Pointers.poff)
479        | Bool.False -> cmp_mismatch c))
480
[2773]481(** val cmpu : Integers.comparison -> val0 -> val0 -> val0 **)
482let cmpu c v1 v2 =
[2601]483  match v1 with
484  | Vundef -> Vundef
485  | Vint (sz1, n1) ->
486    (match v2 with
487     | Vundef -> Vundef
488     | Vint (sz2, n2) ->
489       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 ->
490         of_bool (cmpu_int (AST.bitsize_of_intsize sz2) c n10 n2)) Vundef
491     | Vnull -> Vundef
492     | Vptr x -> Vundef)
493  | Vnull ->
494    (match v2 with
495     | Vundef -> Vundef
496     | Vint (x, x0) -> Vundef
497     | Vnull -> cmp_match c
498     | Vptr x -> cmp_mismatch c)
499  | Vptr ptr1 ->
500    (match v2 with
501     | Vundef -> Vundef
502     | Vint (x, x0) -> Vundef
503     | Vnull -> cmp_mismatch c
504     | Vptr ptr2 ->
505       (match Pointers.eq_block ptr1.Pointers.pblock ptr2.Pointers.pblock with
506        | Bool.True ->
507          of_bool (cmp_offset c ptr1.Pointers.poff ptr2.Pointers.poff)
508        | Bool.False -> cmp_mismatch c))
509
510(** val load_result : AST.typ -> val0 -> val0 **)
511let rec load_result chunk v = match v with
512| Vundef -> Vundef
513| Vint (sz, n) ->
514  (match chunk with
515   | AST.ASTint (sz', sg) ->
516     (match AST.eq_intsize sz sz' with
517      | Bool.True -> v
518      | Bool.False -> Vundef)
519   | AST.ASTptr -> Vundef)
520| Vnull ->
521  (match chunk with
522   | AST.ASTint (x, x0) -> Vundef
523   | AST.ASTptr -> Vnull)
524| Vptr ptr ->
525  (match chunk with
526   | AST.ASTint (x, x0) -> Vundef
527   | AST.ASTptr -> Vptr ptr)
528
Note: See TracBrowser for help on using the repository browser.