source: extracted/genMem.ml @ 2731

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

Exported again.

File size: 9.8 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 Extralib
30
31open Proper
32
33open PositiveMap
34
35open Deqsets
36
[2649]37open ErrorMessages
38
[2601]39open PreIdentifiers
40
41open Errors
42
43open Setoids
44
45open Monad
46
47open Option
48
49open Lists
50
51open Identifiers
52
53open Integers
54
55open AST
56
57open Division
58
[2717]59open Exp
60
[2601]61open Arithmetic
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 update1 : Z.z -> 'a1 -> (Z.z -> 'a1) -> Z.z -> 'a1 **)
84let update1 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 **)
[2730]102let rec block_contents_rect_Type4 h_mk_block_contents x_1100 =
103  let { low = low0; high = high0; contents = contents0 } = x_1100 in
[2601]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 **)
[2730]108let rec block_contents_rect_Type5 h_mk_block_contents x_1102 =
109  let { low = low0; high = high0; contents = contents0 } = x_1102 in
[2601]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 **)
[2730]114let rec block_contents_rect_Type3 h_mk_block_contents x_1104 =
115  let { low = low0; high = high0; contents = contents0 } = x_1104 in
[2601]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 **)
[2730]120let rec block_contents_rect_Type2 h_mk_block_contents x_1106 =
121  let { low = low0; high = high0; contents = contents0 } = x_1106 in
[2601]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 **)
[2730]126let rec block_contents_rect_Type1 h_mk_block_contents x_1108 =
127  let { low = low0; high = high0; contents = contents0 } = x_1108 in
[2601]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 **)
[2730]132let rec block_contents_rect_Type0 h_mk_block_contents x_1110 =
133  let { low = low0; high = high0; contents = contents0 } = x_1110 in
[2601]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 mem1 = { blocks : (Pointers.block -> block_contents); nextblock : Z.z }
186
187(** val mem_rect_Type4 :
188    ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem1 -> 'a1 **)
[2730]189let rec mem_rect_Type4 h_mk_mem x_1126 =
190  let { blocks = blocks0; nextblock = nextblock0 } = x_1126 in
[2601]191  h_mk_mem blocks0 nextblock0 __
192
193(** val mem_rect_Type5 :
194    ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem1 -> 'a1 **)
[2730]195let rec mem_rect_Type5 h_mk_mem x_1128 =
196  let { blocks = blocks0; nextblock = nextblock0 } = x_1128 in
[2601]197  h_mk_mem blocks0 nextblock0 __
198
199(** val mem_rect_Type3 :
200    ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem1 -> 'a1 **)
[2730]201let rec mem_rect_Type3 h_mk_mem x_1130 =
202  let { blocks = blocks0; nextblock = nextblock0 } = x_1130 in
[2601]203  h_mk_mem blocks0 nextblock0 __
204
205(** val mem_rect_Type2 :
206    ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem1 -> 'a1 **)
[2730]207let rec mem_rect_Type2 h_mk_mem x_1132 =
208  let { blocks = blocks0; nextblock = nextblock0 } = x_1132 in
[2601]209  h_mk_mem blocks0 nextblock0 __
210
211(** val mem_rect_Type1 :
212    ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem1 -> 'a1 **)
[2730]213let rec mem_rect_Type1 h_mk_mem x_1134 =
214  let { blocks = blocks0; nextblock = nextblock0 } = x_1134 in
[2601]215  h_mk_mem blocks0 nextblock0 __
216
217(** val mem_rect_Type0 :
218    ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem1 -> 'a1 **)
[2730]219let rec mem_rect_Type0 h_mk_mem x_1136 =
220  let { blocks = blocks0; nextblock = nextblock0 } = x_1136 in
[2601]221  h_mk_mem blocks0 nextblock0 __
222
223(** val blocks : mem1 -> Pointers.block -> block_contents **)
224let rec blocks xxx =
225  xxx.blocks
226
227(** val nextblock : mem1 -> Z.z **)
228let rec nextblock xxx =
229  xxx.nextblock
230
231(** val mem_inv_rect_Type4 :
232    mem1 -> ((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    mem1 -> ((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    mem1 -> ((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    mem1 -> ((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    mem1 -> ((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 : mem1 -> mem1 -> __ **)
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 : mem1 -> mem1 -> __ **)
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 : mem1 **)
282let empty =
283  { blocks = (fun x -> empty_block Z.OZ Z.OZ); nextblock = (Z.Pos
284    Positive.One) }
285
[2649]286(** val alloc : mem1 -> Z.z -> Z.z -> (mem1, Pointers.block) Types.prod **)
287let rec alloc m lo hi =
288  let b = m.nextblock in
[2601]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 : mem1 -> Pointers.block -> mem1 **)
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 : mem1 -> Pointers.block List.list -> mem1 **)
299let free_list m l =
300  List.foldr (fun b m0 -> free m0 b) m l
301
302(** val low_bound : mem1 -> Pointers.block -> Z.z **)
303let low_bound m b =
304  (m.blocks b).low
305
306(** val high_bound : mem1 -> Pointers.block -> Z.z **)
307let high_bound m b =
308  (m.blocks b).high
309
310(** val block_region0 : mem1 -> Pointers.block -> AST.region **)
311let block_region0 m b =
[2649]312  Pointers.block_region b
[2601]313
314(** val do_if_in_bounds :
315    mem1 -> 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
[2649]319  (match Z.zltb (Pointers.block_id b) m.nextblock with
[2601]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    mem1 -> 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    mem1 -> Pointers.pointer -> ByteValues.beval -> mem1 Types.option **)
338let bestorev m ptr v =
339  do_if_in_bounds m ptr (fun b content off ->
340    let contents0 = update1 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.