source: driver/extracted/genMem.ml @ 3106

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