source: extracted/frontEndVal.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: 4.4 KB
Line 
1open Preamble
2
3open Proper
4
5open PositiveMap
6
7open Deqsets
8
9open Extralib
10
11open Lists
12
13open Identifiers
14
15open Floats
16
17open Integers
18
19open AST
20
21open Division
22
23open Arithmetic
24
25open Extranat
26
27open Vector
28
29open FoldStuff
30
31open BitVector
32
33open Z
34
35open BitVectorZ
36
37open Pointers
38
39open Option
40
41open Setoids
42
43open Monad
44
45open Positive
46
47open Char
48
49open String
50
51open PreIdentifiers
52
53open Errors
54
55open Div_and_mod
56
57open Jmeq
58
59open Russell
60
61open Util
62
63open Bool
64
65open Relations
66
67open Nat
68
69open List
70
71open Hints_declaration
72
73open Core_notation
74
75open Pts
76
77open Logic
78
79open Types
80
81open Coqlib
82
83open Values
84
85open Hide
86
87open ByteValues
88
89(** val make_parts : ByteValues.part List.list **)
90let make_parts =
91  List.map ByteValues.part_from_sig (Lists.range_strong AST.size_pointer)
92
93(** val make_be_null : ByteValues.beval List.list **)
94let make_be_null =
95  List.map (fun p -> ByteValues.BVnull p) make_parts
96
97(** val bytes_of_bitvector :
98    Nat.nat -> BitVector.bitVector -> BitVector.byte List.list **)
99let rec bytes_of_bitvector n v =
100  (match n with
101   | Nat.O -> (fun x -> List.Nil)
102   | Nat.S m ->
103     (fun v0 ->
104       let { Types.fst = h; Types.snd = t } =
105         Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
106           (Nat.S Nat.O))))))))
107           (Nat.times m (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
108             (Nat.S Nat.O))))))))) v0
109       in
110       List.Cons (h, (bytes_of_bitvector m t)))) v
111
112(** val fe_to_be_values :
113    AST.typ -> Values.val0 -> ByteValues.beval List.list **)
114let fe_to_be_values t = function
115| Values.Vundef -> List.make_list ByteValues.BVundef (AST.typesize t)
116| Values.Vint (sz, i) ->
117  List.map (fun b -> ByteValues.BVByte b)
118    (bytes_of_bitvector (AST.size_intsize sz) i)
119| Values.Vnull -> make_be_null
120| Values.Vptr ptr -> ByteValues.bevals_of_pointer ptr
121
122(** val check_be_null :
123    Nat.nat -> ByteValues.beval List.list -> Bool.bool **)
124let rec check_be_null n = function
125| List.Nil -> Nat.eqb AST.size_pointer n
126| List.Cons (hd0, tl) ->
127  (match hd0 with
128   | ByteValues.BVundef -> Bool.False
129   | ByteValues.BVnonzero -> Bool.False
130   | ByteValues.BVXor (x, x0, x1) -> Bool.False
131   | ByteValues.BVByte x -> Bool.False
132   | ByteValues.BVnull pt ->
133     Bool.andb (Nat.eqb (ByteValues.part_no pt) n)
134       (check_be_null (Nat.S n) tl)
135   | ByteValues.BVptr (x, x0) -> Bool.False
136   | ByteValues.BVpc (x, x0) -> Bool.False)
137
138(** val build_integer :
139    Nat.nat -> ByteValues.beval List.list -> BitVector.bitVector Types.option **)
140let rec build_integer n l =
141  match n with
142  | Nat.O ->
143    (match l with
144     | List.Nil -> Types.Some Vector.VEmpty
145     | List.Cons (x, x0) -> Types.None)
146  | Nat.S m ->
147    (match l with
148     | List.Nil -> Types.None
149     | List.Cons (h, t) ->
150       (match h with
151        | ByteValues.BVundef -> Types.None
152        | ByteValues.BVnonzero -> Types.None
153        | ByteValues.BVXor (x, x0, x1) -> Types.None
154        | ByteValues.BVByte b ->
155          Types.option_map (fun tl ->
156            Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
157              (Nat.S Nat.O))))))))
158              (Nat.times m (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
159                (Nat.S Nat.O))))))))) b tl) (build_integer m t)
160        | ByteValues.BVnull x -> Types.None
161        | ByteValues.BVptr (x, x0) -> Types.None
162        | ByteValues.BVpc (x, x0) -> Types.None))
163
164(** val build_integer_val :
165    AST.typ -> ByteValues.beval List.list -> Values.val0 **)
166let build_integer_val t l =
167  match t with
168  | AST.ASTint (sz, sg) ->
169    Types.option_map_def (fun x -> Values.Vint (sz, x)) Values.Vundef
170      (build_integer (AST.size_intsize sz) l)
171  | AST.ASTptr -> Values.Vundef
172
173(** val be_to_fe_value :
174    AST.typ -> ByteValues.beval List.list -> Values.val0 **)
175let be_to_fe_value ty l = match l with
176| List.Nil -> Values.Vundef
177| List.Cons (h, t) ->
178  (match h with
179   | ByteValues.BVundef -> Values.Vundef
180   | ByteValues.BVnonzero -> Values.Vundef
181   | ByteValues.BVXor (x, x0, x1) -> Values.Vundef
182   | ByteValues.BVByte b -> build_integer_val ty l
183   | ByteValues.BVnull pt ->
184     (match Bool.andb (Nat.eqb (ByteValues.part_no pt) Nat.O)
185              (check_be_null (Nat.S Nat.O) t) with
186      | Bool.True -> Values.Vnull
187      | Bool.False -> Values.Vundef)
188   | ByteValues.BVptr (x, x0) ->
189     (match ByteValues.pointer_of_bevals l with
190      | Errors.OK ptr -> Values.Vptr ptr
191      | Errors.Error x1 -> Values.Vundef)
192   | ByteValues.BVpc (x, x0) -> Values.Vundef)
193
Note: See TracBrowser for help on using the repository browser.