source: extracted/genMem.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: 9.9 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 Extralib
30
31open Proper
32
33open PositiveMap
34
35open Deqsets
36
37open PreIdentifiers
38
39open Errors
40
41open Setoids
42
43open Monad
44
45open Option
46
47open Lists
48
49open Identifiers
50
51open Coqlib
52
53open Floats
54
55open Integers
56
57open AST
58
59open Division
60
61open Arithmetic
62
63open Char
64
65open String
66
67open Extranat
68
69open Vector
70
71open FoldStuff
72
73open BitVector
74
75open Positive
76
77open Z
78
79open BitVectorZ
80
81open Pointers
82
83open Hide
84
85open ByteValues
86
87(** val update1 : Z.z -> 'a1 -> (Z.z -> 'a1) -> Z.z -> 'a1 **)
88let update1 x v f y =
89  match Z.eqZb y x with
90  | Bool.True -> v
91  | Bool.False -> f y
92
93(** val update_block :
94    Pointers.block -> 'a1 -> (Pointers.block -> 'a1) -> Pointers.block -> 'a1 **)
95let update_block x v f y =
96  match Pointers.eq_block y x with
97  | Bool.True -> v
98  | Bool.False -> f y
99
100type contentmap = Z.z -> ByteValues.beval
101
102type block_contents = { low : Z.z; high : Z.z; contents : contentmap }
103
104(** val block_contents_rect_Type4 :
105    (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1 **)
106let rec block_contents_rect_Type4 h_mk_block_contents x_5450 =
107  let { low = low0; high = high0; contents = contents0 } = x_5450 in
108  h_mk_block_contents low0 high0 contents0
109
110(** val block_contents_rect_Type5 :
111    (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1 **)
112let rec block_contents_rect_Type5 h_mk_block_contents x_5452 =
113  let { low = low0; high = high0; contents = contents0 } = x_5452 in
114  h_mk_block_contents low0 high0 contents0
115
116(** val block_contents_rect_Type3 :
117    (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1 **)
118let rec block_contents_rect_Type3 h_mk_block_contents x_5454 =
119  let { low = low0; high = high0; contents = contents0 } = x_5454 in
120  h_mk_block_contents low0 high0 contents0
121
122(** val block_contents_rect_Type2 :
123    (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1 **)
124let rec block_contents_rect_Type2 h_mk_block_contents x_5456 =
125  let { low = low0; high = high0; contents = contents0 } = x_5456 in
126  h_mk_block_contents low0 high0 contents0
127
128(** val block_contents_rect_Type1 :
129    (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1 **)
130let rec block_contents_rect_Type1 h_mk_block_contents x_5458 =
131  let { low = low0; high = high0; contents = contents0 } = x_5458 in
132  h_mk_block_contents low0 high0 contents0
133
134(** val block_contents_rect_Type0 :
135    (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1 **)
136let rec block_contents_rect_Type0 h_mk_block_contents x_5460 =
137  let { low = low0; high = high0; contents = contents0 } = x_5460 in
138  h_mk_block_contents low0 high0 contents0
139
140(** val low : block_contents -> Z.z **)
141let rec low xxx =
142  xxx.low
143
144(** val high : block_contents -> Z.z **)
145let rec high xxx =
146  xxx.high
147
148(** val contents : block_contents -> contentmap **)
149let rec contents xxx =
150  xxx.contents
151
152(** val block_contents_inv_rect_Type4 :
153    block_contents -> (Z.z -> Z.z -> contentmap -> __ -> 'a1) -> 'a1 **)
154let block_contents_inv_rect_Type4 hterm h1 =
155  let hcut = block_contents_rect_Type4 h1 hterm in hcut __
156
157(** val block_contents_inv_rect_Type3 :
158    block_contents -> (Z.z -> Z.z -> contentmap -> __ -> 'a1) -> 'a1 **)
159let block_contents_inv_rect_Type3 hterm h1 =
160  let hcut = block_contents_rect_Type3 h1 hterm in hcut __
161
162(** val block_contents_inv_rect_Type2 :
163    block_contents -> (Z.z -> Z.z -> contentmap -> __ -> 'a1) -> 'a1 **)
164let block_contents_inv_rect_Type2 hterm h1 =
165  let hcut = block_contents_rect_Type2 h1 hterm in hcut __
166
167(** val block_contents_inv_rect_Type1 :
168    block_contents -> (Z.z -> Z.z -> contentmap -> __ -> 'a1) -> 'a1 **)
169let block_contents_inv_rect_Type1 hterm h1 =
170  let hcut = block_contents_rect_Type1 h1 hterm in hcut __
171
172(** val block_contents_inv_rect_Type0 :
173    block_contents -> (Z.z -> Z.z -> contentmap -> __ -> 'a1) -> 'a1 **)
174let block_contents_inv_rect_Type0 hterm h1 =
175  let hcut = block_contents_rect_Type0 h1 hterm in hcut __
176
177(** val block_contents_discr : block_contents -> block_contents -> __ **)
178let block_contents_discr x y =
179  Logic.eq_rect_Type2 x
180    (let { low = a0; high = a1; contents = a2 } = x in
181    Obj.magic (fun _ dH -> dH __ __ __)) y
182
183(** val block_contents_jmdiscr : block_contents -> block_contents -> __ **)
184let block_contents_jmdiscr x y =
185  Logic.eq_rect_Type2 x
186    (let { low = a0; high = a1; contents = a2 } = x in
187    Obj.magic (fun _ dH -> dH __ __ __)) y
188
189type mem1 = { blocks : (Pointers.block -> block_contents); nextblock : Z.z }
190
191(** val mem_rect_Type4 :
192    ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem1 -> 'a1 **)
193let rec mem_rect_Type4 h_mk_mem x_5476 =
194  let { blocks = blocks0; nextblock = nextblock0 } = x_5476 in
195  h_mk_mem blocks0 nextblock0 __
196
197(** val mem_rect_Type5 :
198    ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem1 -> 'a1 **)
199let rec mem_rect_Type5 h_mk_mem x_5478 =
200  let { blocks = blocks0; nextblock = nextblock0 } = x_5478 in
201  h_mk_mem blocks0 nextblock0 __
202
203(** val mem_rect_Type3 :
204    ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem1 -> 'a1 **)
205let rec mem_rect_Type3 h_mk_mem x_5480 =
206  let { blocks = blocks0; nextblock = nextblock0 } = x_5480 in
207  h_mk_mem blocks0 nextblock0 __
208
209(** val mem_rect_Type2 :
210    ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem1 -> 'a1 **)
211let rec mem_rect_Type2 h_mk_mem x_5482 =
212  let { blocks = blocks0; nextblock = nextblock0 } = x_5482 in
213  h_mk_mem blocks0 nextblock0 __
214
215(** val mem_rect_Type1 :
216    ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem1 -> 'a1 **)
217let rec mem_rect_Type1 h_mk_mem x_5484 =
218  let { blocks = blocks0; nextblock = nextblock0 } = x_5484 in
219  h_mk_mem blocks0 nextblock0 __
220
221(** val mem_rect_Type0 :
222    ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem1 -> 'a1 **)
223let rec mem_rect_Type0 h_mk_mem x_5486 =
224  let { blocks = blocks0; nextblock = nextblock0 } = x_5486 in
225  h_mk_mem blocks0 nextblock0 __
226
227(** val blocks : mem1 -> Pointers.block -> block_contents **)
228let rec blocks xxx =
229  xxx.blocks
230
231(** val nextblock : mem1 -> Z.z **)
232let rec nextblock xxx =
233  xxx.nextblock
234
235(** val mem_inv_rect_Type4 :
236    mem1 -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
237    'a1 **)
238let mem_inv_rect_Type4 hterm h1 =
239  let hcut = mem_rect_Type4 h1 hterm in hcut __
240
241(** val mem_inv_rect_Type3 :
242    mem1 -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
243    'a1 **)
244let mem_inv_rect_Type3 hterm h1 =
245  let hcut = mem_rect_Type3 h1 hterm in hcut __
246
247(** val mem_inv_rect_Type2 :
248    mem1 -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
249    'a1 **)
250let mem_inv_rect_Type2 hterm h1 =
251  let hcut = mem_rect_Type2 h1 hterm in hcut __
252
253(** val mem_inv_rect_Type1 :
254    mem1 -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
255    'a1 **)
256let mem_inv_rect_Type1 hterm h1 =
257  let hcut = mem_rect_Type1 h1 hterm in hcut __
258
259(** val mem_inv_rect_Type0 :
260    mem1 -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
261    'a1 **)
262let mem_inv_rect_Type0 hterm h1 =
263  let hcut = mem_rect_Type0 h1 hterm in hcut __
264
265(** val mem_discr : mem1 -> mem1 -> __ **)
266let mem_discr x y =
267  Logic.eq_rect_Type2 x
268    (let { blocks = a0; nextblock = a1 } = x in
269    Obj.magic (fun _ dH -> dH __ __ __)) y
270
271(** val mem_jmdiscr : mem1 -> mem1 -> __ **)
272let mem_jmdiscr x y =
273  Logic.eq_rect_Type2 x
274    (let { blocks = a0; nextblock = a1 } = x in
275    Obj.magic (fun _ dH -> dH __ __ __)) y
276
277(** val oneZ : Z.z **)
278let oneZ =
279  Z.Pos Positive.One
280
281(** val empty_block : Z.z -> Z.z -> block_contents **)
282let empty_block lo hi =
283  { low = lo; high = hi; contents = (fun y -> ByteValues.BVundef) }
284
285(** val empty : mem1 **)
286let empty =
287  { blocks = (fun x -> empty_block Z.OZ Z.OZ); nextblock = (Z.Pos
288    Positive.One) }
289
290(** val alloc :
291    mem1 -> Z.z -> Z.z -> AST.region -> (mem1, Pointers.block Types.sig0)
292    Types.prod **)
293let rec alloc m lo hi r =
294  let b = { Pointers.block_region = r; Pointers.block_id = m.nextblock } in
295  { Types.fst = { blocks = (update_block b (empty_block lo hi) m.blocks);
296  nextblock = (Z.zsucc m.nextblock) }; Types.snd = b }
297
298(** val free : mem1 -> Pointers.block -> mem1 **)
299let free m b =
300  { blocks =
301    (update_block b (empty_block (Z.Pos Positive.One) Z.OZ) m.blocks);
302    nextblock = m.nextblock }
303
304(** val free_list : mem1 -> Pointers.block List.list -> mem1 **)
305let free_list m l =
306  List.foldr (fun b m0 -> free m0 b) m l
307
308(** val low_bound : mem1 -> Pointers.block -> Z.z **)
309let low_bound m b =
310  (m.blocks b).low
311
312(** val high_bound : mem1 -> Pointers.block -> Z.z **)
313let high_bound m b =
314  (m.blocks b).high
315
316(** val block_region0 : mem1 -> Pointers.block -> AST.region **)
317let block_region0 m b =
318  b.Pointers.block_region
319
320(** val do_if_in_bounds :
321    mem1 -> Pointers.pointer -> (Pointers.block -> block_contents -> Z.z ->
322    'a1) -> 'a1 Types.option **)
323let do_if_in_bounds m ptr f =
324  let b = ptr.Pointers.pblock in
325  (match Z.zltb b.Pointers.block_id m.nextblock with
326   | Bool.True ->
327     let content = m.blocks b in
328     let off =
329       BitVectorZ.z_of_unsigned_bitvector Pointers.offset_size
330         (Pointers.offv ptr.Pointers.poff)
331     in
332     (match Bool.andb (Z.zleb content.low off) (Z.zltb off content.high) with
333      | Bool.True -> Types.Some (f b content off)
334      | Bool.False -> Types.None)
335   | Bool.False -> Types.None)
336
337(** val beloadv :
338    mem1 -> Pointers.pointer -> ByteValues.beval Types.option **)
339let beloadv m ptr =
340  do_if_in_bounds m ptr (fun b content off -> content.contents off)
341
342(** val bestorev :
343    mem1 -> Pointers.pointer -> ByteValues.beval -> mem1 Types.option **)
344let bestorev m ptr v =
345  do_if_in_bounds m ptr (fun b content off ->
346    let contents0 = update1 off v content.contents in
347    let content0 = { low = content.low; high = content.high; contents =
348      contents0 }
349    in
350    let blocks0 = update_block b content0 m.blocks in
351    { blocks = blocks0; nextblock = m.nextblock })
352
Note: See TracBrowser for help on using the repository browser.