source: extracted/values.ml @ 2601

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

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

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