source: extracted/values.ml @ 3043

Last change on this file since 3043 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
Line 
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
31open ErrorMessages
32
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
63open Exp
64
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
92| Vint (sz, x_5112) -> h_Vint sz x_5112
93| Vnull -> h_Vnull
94| Vptr x_5113 -> h_Vptr x_5113
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
101| Vint (sz, x_5119) -> h_Vint sz x_5119
102| Vnull -> h_Vnull
103| Vptr x_5120 -> h_Vptr x_5120
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
110| Vint (sz, x_5126) -> h_Vint sz x_5126
111| Vnull -> h_Vnull
112| Vptr x_5127 -> h_Vptr x_5127
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
119| Vint (sz, x_5133) -> h_Vint sz x_5133
120| Vnull -> h_Vnull
121| Vptr x_5134 -> h_Vptr x_5134
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
128| Vint (sz, x_5140) -> h_Vint sz x_5140
129| Vnull -> h_Vnull
130| Vptr x_5141 -> h_Vptr x_5141
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
137| Vint (sz, x_5147) -> h_Vint sz x_5147
138| Vnull -> h_Vnull
139| Vptr x_5148 -> h_Vptr x_5148
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 =
195  Vint (sz, (AST.repr sz (Nat.S Nat.O)))
196
197(** val mone : AST.intsize -> BitVector.bitVector **)
198let mone sz =
199  BitVectorZ.bitvector_of_Z (AST.bitsize_of_intsize sz) (Z.Neg Positive.One)
200
201(** val vmone : AST.intsize -> val0 **)
202let vmone sz =
203  Vint (sz, (mone sz))
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
220| Vundef -> Errors.Error (Errors.msg ErrorMessages.ValueNotABoolean)
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
229(** val neg : val0 -> val0 **)
230let neg = function
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
244      (mone sz)))
245| Vnull -> Vundef
246| Vptr x -> Vundef
247
248(** val notbool : val0 -> val0 **)
249let notbool = function
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
258(** val zero_ext : AST.intsize -> val0 -> val0 **)
259let zero_ext rsz = function
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
268(** val sign_ext : AST.intsize -> val0 -> val0 **)
269let sign_ext rsz = function
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
278(** val add : val0 -> val0 -> val0 **)
279let add v1 v2 =
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
333(** val mul : val0 -> val0 -> val0 **)
334let mul v1 v2 =
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
367(** val or0 : val0 -> val0 -> val0 **)
368let or0 v1 v2 =
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
383(** val xor : val0 -> val0 -> val0 **)
384let xor v1 v2 =
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
452(** val cmp : Integers.comparison -> val0 -> val0 -> val0 **)
453let cmp c v1 v2 =
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
481(** val cmpu : Integers.comparison -> val0 -> val0 -> val0 **)
482let cmpu c v1 v2 =
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.