source: extracted/genMem.ml @ 2649

Last change on this file since 2649 was 2649, checked in by sacerdot, 8 years ago

...

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