source: extracted/values.ml @ 2716

Last change on this file since 2716 was 2649, checked in by sacerdot, 7 years ago

...

File size: 13.9 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
63open Arithmetic
64
65open Extranat
66
67open Vector
68
69open FoldStuff
70
71open BitVector
72
73open Z
74
75open BitVectorZ
76
77open Pointers
78
79type val0 =
80| Vundef
81| Vint of AST.intsize * AST.bvint
82| Vnull
83| Vptr of Pointers.pointer
84
85(** val val_rect_Type4 :
86    'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
87    'a1) -> val0 -> 'a1 **)
88let rec val_rect_Type4 h_Vundef h_Vint h_Vnull h_Vptr = function
89| Vundef -> h_Vundef
[2649]90| Vint (sz, x_2472) -> h_Vint sz x_2472
[2601]91| Vnull -> h_Vnull
[2649]92| Vptr x_2473 -> h_Vptr x_2473
[2601]93
94(** val val_rect_Type5 :
95    'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
96    'a1) -> val0 -> 'a1 **)
97let rec val_rect_Type5 h_Vundef h_Vint h_Vnull h_Vptr = function
98| Vundef -> h_Vundef
[2649]99| Vint (sz, x_2479) -> h_Vint sz x_2479
[2601]100| Vnull -> h_Vnull
[2649]101| Vptr x_2480 -> h_Vptr x_2480
[2601]102
103(** val val_rect_Type3 :
104    'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
105    'a1) -> val0 -> 'a1 **)
106let rec val_rect_Type3 h_Vundef h_Vint h_Vnull h_Vptr = function
107| Vundef -> h_Vundef
[2649]108| Vint (sz, x_2486) -> h_Vint sz x_2486
[2601]109| Vnull -> h_Vnull
[2649]110| Vptr x_2487 -> h_Vptr x_2487
[2601]111
112(** val val_rect_Type2 :
113    'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
114    'a1) -> val0 -> 'a1 **)
115let rec val_rect_Type2 h_Vundef h_Vint h_Vnull h_Vptr = function
116| Vundef -> h_Vundef
[2649]117| Vint (sz, x_2493) -> h_Vint sz x_2493
[2601]118| Vnull -> h_Vnull
[2649]119| Vptr x_2494 -> h_Vptr x_2494
[2601]120
121(** val val_rect_Type1 :
122    'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
123    'a1) -> val0 -> 'a1 **)
124let rec val_rect_Type1 h_Vundef h_Vint h_Vnull h_Vptr = function
125| Vundef -> h_Vundef
[2649]126| Vint (sz, x_2500) -> h_Vint sz x_2500
[2601]127| Vnull -> h_Vnull
[2649]128| Vptr x_2501 -> h_Vptr x_2501
[2601]129
130(** val val_rect_Type0 :
131    'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
132    'a1) -> val0 -> 'a1 **)
133let rec val_rect_Type0 h_Vundef h_Vint h_Vnull h_Vptr = function
134| Vundef -> h_Vundef
[2649]135| Vint (sz, x_2507) -> h_Vint sz x_2507
[2601]136| Vnull -> h_Vnull
[2649]137| Vptr x_2508 -> h_Vptr x_2508
[2601]138
139(** val val_inv_rect_Type4 :
140    val0 -> (__ -> 'a1) -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (__ ->
141    'a1) -> (Pointers.pointer -> __ -> 'a1) -> 'a1 **)
142let val_inv_rect_Type4 hterm h1 h2 h3 h4 =
143  let hcut = val_rect_Type4 h1 h2 h3 h4 hterm in hcut __
144
145(** val val_inv_rect_Type3 :
146    val0 -> (__ -> 'a1) -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (__ ->
147    'a1) -> (Pointers.pointer -> __ -> 'a1) -> 'a1 **)
148let val_inv_rect_Type3 hterm h1 h2 h3 h4 =
149  let hcut = val_rect_Type3 h1 h2 h3 h4 hterm in hcut __
150
151(** val val_inv_rect_Type2 :
152    val0 -> (__ -> 'a1) -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (__ ->
153    'a1) -> (Pointers.pointer -> __ -> 'a1) -> 'a1 **)
154let val_inv_rect_Type2 hterm h1 h2 h3 h4 =
155  let hcut = val_rect_Type2 h1 h2 h3 h4 hterm in hcut __
156
157(** val val_inv_rect_Type1 :
158    val0 -> (__ -> 'a1) -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (__ ->
159    'a1) -> (Pointers.pointer -> __ -> 'a1) -> 'a1 **)
160let val_inv_rect_Type1 hterm h1 h2 h3 h4 =
161  let hcut = val_rect_Type1 h1 h2 h3 h4 hterm in hcut __
162
163(** val val_inv_rect_Type0 :
164    val0 -> (__ -> 'a1) -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (__ ->
165    'a1) -> (Pointers.pointer -> __ -> 'a1) -> 'a1 **)
166let val_inv_rect_Type0 hterm h1 h2 h3 h4 =
167  let hcut = val_rect_Type0 h1 h2 h3 h4 hterm in hcut __
168
169(** val val_discr : val0 -> val0 -> __ **)
170let val_discr x y =
171  Logic.eq_rect_Type2 x
172    (match x with
173     | Vundef -> Obj.magic (fun _ dH -> dH)
174     | Vint (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
175     | Vnull -> Obj.magic (fun _ dH -> dH)
176     | Vptr a0 -> Obj.magic (fun _ dH -> dH __)) y
177
178(** val val_jmdiscr : val0 -> val0 -> __ **)
179let val_jmdiscr x y =
180  Logic.eq_rect_Type2 x
181    (match x with
182     | Vundef -> Obj.magic (fun _ dH -> dH)
183     | Vint (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
184     | Vnull -> Obj.magic (fun _ dH -> dH)
185     | Vptr a0 -> Obj.magic (fun _ dH -> dH __)) y
186
187(** val vzero : AST.intsize -> val0 **)
188let vzero sz =
189  Vint (sz, (BitVector.zero (AST.bitsize_of_intsize sz)))
190
191(** val vone : AST.intsize -> val0 **)
192let vone sz =
193  Vint (sz, (AST.repr0 sz (Nat.S Nat.O)))
194
195(** val mone0 : AST.intsize -> BitVector.bitVector **)
196let mone0 sz =
197  BitVectorZ.bitvector_of_Z (AST.bitsize_of_intsize sz) (Z.Neg Positive.One)
198
199(** val vmone : AST.intsize -> val0 **)
200let vmone sz =
201  Vint (sz, (mone0 sz))
202
203(** val vtrue : val0 **)
204let vtrue =
205  vone AST.I32
206
207(** val vfalse : val0 **)
208let vfalse =
209  vzero AST.I32
210
211(** val of_bool : Bool.bool -> val0 **)
212let of_bool = function
213| Bool.True -> vtrue
214| Bool.False -> vfalse
215
216(** val eval_bool_of_val : val0 -> Bool.bool Errors.res **)
217let eval_bool_of_val = function
[2649]218| Vundef -> Errors.Error (Errors.msg ErrorMessages.ValueNotABoolean)
[2601]219| Vint (x, i) ->
220  Errors.OK
221    (Bool.notb
222      (BitVector.eq_bv (AST.bitsize_of_intsize x) i
223        (BitVector.zero (AST.bitsize_of_intsize x))))
224| Vnull -> Errors.OK Bool.False
225| Vptr x -> Errors.OK Bool.True
226
227(** val neg0 : val0 -> val0 **)
228let neg0 = function
229| Vundef -> Vundef
230| Vint (sz, n) ->
231  Vint (sz,
232    (Arithmetic.two_complement_negation (AST.bitsize_of_intsize sz) n))
233| Vnull -> Vundef
234| Vptr x -> Vundef
235
236(** val notint : val0 -> val0 **)
237let notint = function
238| Vundef -> Vundef
239| Vint (sz, n) ->
240  Vint (sz,
241    (BitVector.exclusive_disjunction_bv (AST.bitsize_of_intsize sz) n
242      (mone0 sz)))
243| Vnull -> Vundef
244| Vptr x -> Vundef
245
246(** val notbool0 : val0 -> val0 **)
247let notbool0 = function
248| Vundef -> Vundef
249| Vint (sz, n) ->
250  of_bool
251    (BitVector.eq_bv (AST.bitsize_of_intsize sz) n
252      (BitVector.zero (AST.bitsize_of_intsize sz)))
253| Vnull -> vtrue
254| Vptr x -> vfalse
255
256(** val zero_ext1 : AST.intsize -> val0 -> val0 **)
257let zero_ext1 rsz = function
258| Vundef -> Vundef
259| Vint (sz, n) ->
260  Vint (rsz,
261    (Arithmetic.zero_ext (AST.bitsize_of_intsize sz)
262      (AST.bitsize_of_intsize rsz) n))
263| Vnull -> Vundef
264| Vptr x -> Vundef
265
266(** val sign_ext1 : AST.intsize -> val0 -> val0 **)
267let sign_ext1 rsz = function
268| Vundef -> Vundef
269| Vint (sz, i) ->
270  Vint (rsz,
271    (Arithmetic.sign_ext (AST.bitsize_of_intsize sz)
272      (AST.bitsize_of_intsize rsz) i))
273| Vnull -> Vundef
274| Vptr x -> Vundef
275
276(** val add0 : val0 -> val0 -> val0 **)
277let add0 v1 v2 =
278  match v1 with
279  | Vundef -> Vundef
280  | Vint (sz1, n1) ->
281    (match v2 with
282     | Vundef -> Vundef
283     | Vint (sz2, n2) ->
284       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Vint (sz2,
285         (Arithmetic.addition_n (AST.bitsize_of_intsize sz2) n10 n2))) Vundef
286     | Vnull -> Vundef
287     | Vptr ptr ->
288       Vptr (Pointers.shift_pointer (AST.bitsize_of_intsize sz1) ptr n1))
289  | Vnull -> Vundef
290  | Vptr ptr ->
291    (match v2 with
292     | Vundef -> Vundef
293     | Vint (x, n2) ->
294       Vptr (Pointers.shift_pointer (AST.bitsize_of_intsize x) ptr n2)
295     | Vnull -> Vundef
296     | Vptr x -> Vundef)
297
298(** val sub : val0 -> val0 -> val0 **)
299let sub v1 v2 =
300  match v1 with
301  | Vundef -> Vundef
302  | Vint (sz1, n1) ->
303    (match v2 with
304     | Vundef -> Vundef
305     | Vint (sz2, n2) ->
306       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Vint (sz2,
307         (Arithmetic.subtraction (AST.bitsize_of_intsize sz2) n10 n2)))
308         Vundef
309     | Vnull -> Vundef
310     | Vptr x -> Vundef)
311  | Vnull ->
312    (match v2 with
313     | Vundef -> Vundef
314     | Vint (x, x0) -> Vundef
315     | Vnull -> vzero AST.I32
316     | Vptr x -> Vundef)
317  | Vptr ptr1 ->
318    (match v2 with
319     | Vundef -> Vundef
320     | Vint (sz2, n2) ->
321       Vptr (Pointers.neg_shift_pointer (AST.bitsize_of_intsize sz2) ptr1 n2)
322     | Vnull -> Vundef
323     | Vptr ptr2 ->
324       (match Pointers.eq_block ptr1.Pointers.pblock ptr2.Pointers.pblock with
325        | Bool.True ->
326          Vint (AST.I32,
327            (Pointers.sub_offset (AST.bitsize_of_intsize AST.I32)
328              ptr1.Pointers.poff ptr2.Pointers.poff))
329        | Bool.False -> Vundef))
330
331(** val mul0 : val0 -> val0 -> val0 **)
332let mul0 v1 v2 =
333  match v1 with
334  | Vundef -> Vundef
335  | Vint (sz1, n1) ->
336    (match v2 with
337     | Vundef -> Vundef
338     | Vint (sz2, n2) ->
339       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Vint (sz2,
340         (Vector.vsplit (AST.bitsize_of_intsize sz2)
341           (AST.bitsize_of_intsize sz2)
342           (Arithmetic.multiplication (AST.bitsize_of_intsize sz2) n10 n2)).Types.snd))
343         Vundef
344     | Vnull -> Vundef
345     | Vptr x -> Vundef)
346  | Vnull -> Vundef
347  | Vptr x -> Vundef
348
349(** val v_and : val0 -> val0 -> val0 **)
350let v_and v1 v2 =
351  match v1 with
352  | Vundef -> Vundef
353  | Vint (sz1, n1) ->
354    (match v2 with
355     | Vundef -> Vundef
356     | Vint (sz2, n2) ->
357       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Vint (sz2,
358         (BitVector.conjunction_bv (AST.bitsize_of_intsize sz2) n10 n2)))
359         Vundef
360     | Vnull -> Vundef
361     | Vptr x -> Vundef)
362  | Vnull -> Vundef
363  | Vptr x -> Vundef
364
365(** val or1 : val0 -> val0 -> val0 **)
366let or1 v1 v2 =
367  match v1 with
368  | Vundef -> Vundef
369  | Vint (sz1, n1) ->
370    (match v2 with
371     | Vundef -> Vundef
372     | Vint (sz2, n2) ->
373       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Vint (sz2,
374         (BitVector.inclusive_disjunction_bv (AST.bitsize_of_intsize sz2) n10
375           n2))) Vundef
376     | Vnull -> Vundef
377     | Vptr x -> Vundef)
378  | Vnull -> Vundef
379  | Vptr x -> Vundef
380
381(** val xor0 : val0 -> val0 -> val0 **)
382let xor0 v1 v2 =
383  match v1 with
384  | Vundef -> Vundef
385  | Vint (sz1, n1) ->
386    (match v2 with
387     | Vundef -> Vundef
388     | Vint (sz2, n2) ->
389       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Vint (sz2,
390         (BitVector.exclusive_disjunction_bv (AST.bitsize_of_intsize sz2) n10
391           n2))) Vundef
392     | Vnull -> Vundef
393     | Vptr x -> Vundef)
394  | Vnull -> Vundef
395  | Vptr x -> Vundef
396
397(** val cmp_match : Integers.comparison -> val0 **)
398let cmp_match = function
399| Integers.Ceq -> vtrue
400| Integers.Cne -> vfalse
401| Integers.Clt -> Vundef
402| Integers.Cle -> Vundef
403| Integers.Cgt -> Vundef
404| Integers.Cge -> Vundef
405
406(** val cmp_mismatch : Integers.comparison -> val0 **)
407let cmp_mismatch = function
408| Integers.Ceq -> vfalse
409| Integers.Cne -> vtrue
410| Integers.Clt -> Vundef
411| Integers.Cle -> Vundef
412| Integers.Cgt -> Vundef
413| Integers.Cge -> Vundef
414
415(** val cmp_offset :
416    Integers.comparison -> Pointers.offset -> Pointers.offset -> Bool.bool **)
417let cmp_offset c x y =
418  match c with
419  | Integers.Ceq -> Pointers.eq_offset x y
420  | Integers.Cne -> Bool.notb (Pointers.eq_offset x y)
421  | Integers.Clt -> Pointers.lt_offset x y
422  | Integers.Cle -> Bool.notb (Pointers.lt_offset y x)
423  | Integers.Cgt -> Pointers.lt_offset y x
424  | Integers.Cge -> Bool.notb (Pointers.lt_offset x y)
425
426(** val cmp_int :
427    Nat.nat -> Integers.comparison -> BitVector.bitVector ->
428    BitVector.bitVector -> Bool.bool **)
429let cmp_int n c x y =
430  match c with
431  | Integers.Ceq -> BitVector.eq_bv n x y
432  | Integers.Cne -> Bool.notb (BitVector.eq_bv n x y)
433  | Integers.Clt -> Arithmetic.lt_s n x y
434  | Integers.Cle -> Bool.notb (Arithmetic.lt_s n y x)
435  | Integers.Cgt -> Arithmetic.lt_s n y x
436  | Integers.Cge -> Bool.notb (Arithmetic.lt_s n x y)
437
438(** val cmpu_int :
439    Nat.nat -> Integers.comparison -> BitVector.bitVector ->
440    BitVector.bitVector -> Bool.bool **)
441let cmpu_int n c x y =
442  match c with
443  | Integers.Ceq -> BitVector.eq_bv n x y
444  | Integers.Cne -> Bool.notb (BitVector.eq_bv n x y)
445  | Integers.Clt -> Arithmetic.lt_u n x y
446  | Integers.Cle -> Bool.notb (Arithmetic.lt_u n y x)
447  | Integers.Cgt -> Arithmetic.lt_u n y x
448  | Integers.Cge -> Bool.notb (Arithmetic.lt_u n x y)
449
450(** val cmp0 : Integers.comparison -> val0 -> val0 -> val0 **)
451let cmp0 c v1 v2 =
452  match v1 with
453  | Vundef -> Vundef
454  | Vint (sz1, n1) ->
455    (match v2 with
456     | Vundef -> Vundef
457     | Vint (sz2, n2) ->
458       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 ->
459         of_bool (cmp_int (AST.bitsize_of_intsize sz2) c n10 n2)) Vundef
460     | Vnull -> Vundef
461     | Vptr x -> Vundef)
462  | Vnull ->
463    (match v2 with
464     | Vundef -> Vundef
465     | Vint (x, x0) -> Vundef
466     | Vnull -> cmp_match c
467     | Vptr x -> cmp_mismatch c)
468  | Vptr ptr1 ->
469    (match v2 with
470     | Vundef -> Vundef
471     | Vint (x, x0) -> Vundef
472     | Vnull -> cmp_mismatch c
473     | Vptr ptr2 ->
474       (match Pointers.eq_block ptr1.Pointers.pblock ptr2.Pointers.pblock with
475        | Bool.True ->
476          of_bool (cmp_offset c ptr1.Pointers.poff ptr2.Pointers.poff)
477        | Bool.False -> cmp_mismatch c))
478
479(** val cmpu0 : Integers.comparison -> val0 -> val0 -> val0 **)
480let cmpu0 c v1 v2 =
481  match v1 with
482  | Vundef -> Vundef
483  | Vint (sz1, n1) ->
484    (match v2 with
485     | Vundef -> Vundef
486     | Vint (sz2, n2) ->
487       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 ->
488         of_bool (cmpu_int (AST.bitsize_of_intsize sz2) c n10 n2)) Vundef
489     | Vnull -> Vundef
490     | Vptr x -> Vundef)
491  | Vnull ->
492    (match v2 with
493     | Vundef -> Vundef
494     | Vint (x, x0) -> Vundef
495     | Vnull -> cmp_match c
496     | Vptr x -> cmp_mismatch c)
497  | Vptr ptr1 ->
498    (match v2 with
499     | Vundef -> Vundef
500     | Vint (x, x0) -> Vundef
501     | Vnull -> cmp_mismatch c
502     | Vptr ptr2 ->
503       (match Pointers.eq_block ptr1.Pointers.pblock ptr2.Pointers.pblock with
504        | Bool.True ->
505          of_bool (cmp_offset c ptr1.Pointers.poff ptr2.Pointers.poff)
506        | Bool.False -> cmp_mismatch c))
507
508(** val load_result : AST.typ -> val0 -> val0 **)
509let rec load_result chunk v = match v with
510| Vundef -> Vundef
511| Vint (sz, n) ->
512  (match chunk with
513   | AST.ASTint (sz', sg) ->
514     (match AST.eq_intsize sz sz' with
515      | Bool.True -> v
516      | Bool.False -> Vundef)
517   | AST.ASTptr -> Vundef)
518| Vnull ->
519  (match chunk with
520   | AST.ASTint (x, x0) -> Vundef
521   | AST.ASTptr -> Vnull)
522| Vptr ptr ->
523  (match chunk with
524   | AST.ASTint (x, x0) -> Vundef
525   | AST.ASTptr -> Vptr ptr)
526
Note: See TracBrowser for help on using the repository browser.