source: extracted/genMem.ml @ 2797

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

Extracted again after James's cleanup and the implementation of the
new testing function to be used in the untrusted code.

File size: 9.7 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 Lists
44
45open Identifiers
46
47open Integers
48
49open AST
50
51open Division
52
[2717]53open Exp
54
[2601]55open Arithmetic
56
[2773]57open Setoids
58
59open Monad
60
61open Option
62
[2601]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
[2773]83(** val update : Z.z -> 'a1 -> (Z.z -> 'a1) -> Z.z -> 'a1 **)
84let update x v f y =
[2601]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 **)
[2797]102let rec block_contents_rect_Type4 h_mk_block_contents x_6399 =
103  let { low = low0; high = high0; contents = contents0 } = x_6399 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 **)
[2797]108let rec block_contents_rect_Type5 h_mk_block_contents x_6401 =
109  let { low = low0; high = high0; contents = contents0 } = x_6401 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 **)
[2797]114let rec block_contents_rect_Type3 h_mk_block_contents x_6403 =
115  let { low = low0; high = high0; contents = contents0 } = x_6403 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 **)
[2797]120let rec block_contents_rect_Type2 h_mk_block_contents x_6405 =
121  let { low = low0; high = high0; contents = contents0 } = x_6405 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 **)
[2797]126let rec block_contents_rect_Type1 h_mk_block_contents x_6407 =
127  let { low = low0; high = high0; contents = contents0 } = x_6407 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 **)
[2797]132let rec block_contents_rect_Type0 h_mk_block_contents x_6409 =
133  let { low = low0; high = high0; contents = contents0 } = x_6409 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
[2773]185type mem = { blocks : (Pointers.block -> block_contents); nextblock : Z.z }
[2601]186
187(** val mem_rect_Type4 :
[2773]188    ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem -> 'a1 **)
[2797]189let rec mem_rect_Type4 h_mk_mem x_6425 =
190  let { blocks = blocks0; nextblock = nextblock0 } = x_6425 in
[2601]191  h_mk_mem blocks0 nextblock0 __
192
193(** val mem_rect_Type5 :
[2773]194    ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem -> 'a1 **)
[2797]195let rec mem_rect_Type5 h_mk_mem x_6427 =
196  let { blocks = blocks0; nextblock = nextblock0 } = x_6427 in
[2601]197  h_mk_mem blocks0 nextblock0 __
198
199(** val mem_rect_Type3 :
[2773]200    ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem -> 'a1 **)
[2797]201let rec mem_rect_Type3 h_mk_mem x_6429 =
202  let { blocks = blocks0; nextblock = nextblock0 } = x_6429 in
[2601]203  h_mk_mem blocks0 nextblock0 __
204
205(** val mem_rect_Type2 :
[2773]206    ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem -> 'a1 **)
[2797]207let rec mem_rect_Type2 h_mk_mem x_6431 =
208  let { blocks = blocks0; nextblock = nextblock0 } = x_6431 in
[2601]209  h_mk_mem blocks0 nextblock0 __
210
211(** val mem_rect_Type1 :
[2773]212    ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem -> 'a1 **)
[2797]213let rec mem_rect_Type1 h_mk_mem x_6433 =
214  let { blocks = blocks0; nextblock = nextblock0 } = x_6433 in
[2601]215  h_mk_mem blocks0 nextblock0 __
216
217(** val mem_rect_Type0 :
[2773]218    ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem -> 'a1 **)
[2797]219let rec mem_rect_Type0 h_mk_mem x_6435 =
220  let { blocks = blocks0; nextblock = nextblock0 } = x_6435 in
[2601]221  h_mk_mem blocks0 nextblock0 __
222
[2773]223(** val blocks : mem -> Pointers.block -> block_contents **)
[2601]224let rec blocks xxx =
225  xxx.blocks
226
[2773]227(** val nextblock : mem -> Z.z **)
[2601]228let rec nextblock xxx =
229  xxx.nextblock
230
231(** val mem_inv_rect_Type4 :
[2773]232    mem -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
[2601]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 :
[2773]238    mem -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
[2601]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 :
[2773]244    mem -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
[2601]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 :
[2773]250    mem -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
[2601]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 :
[2773]256    mem -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
[2601]257    'a1 **)
258let mem_inv_rect_Type0 hterm h1 =
259  let hcut = mem_rect_Type0 h1 hterm in hcut __
260
[2773]261(** val mem_discr : mem -> mem -> __ **)
[2601]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
[2773]267(** val mem_jmdiscr : mem -> mem -> __ **)
[2601]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
[2773]281(** val empty : mem **)
[2601]282let empty =
283  { blocks = (fun x -> empty_block Z.OZ Z.OZ); nextblock = (Z.Pos
284    Positive.One) }
285
[2773]286(** val alloc : mem -> Z.z -> Z.z -> (mem, Pointers.block) Types.prod **)
[2649]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
[2773]292(** val free : mem -> Pointers.block -> mem **)
[2601]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
[2773]298(** val free_list : mem -> Pointers.block List.list -> mem **)
[2601]299let free_list m l =
300  List.foldr (fun b m0 -> free m0 b) m l
301
[2773]302(** val low_bound : mem -> Pointers.block -> Z.z **)
[2601]303let low_bound m b =
304  (m.blocks b).low
305
[2773]306(** val high_bound : mem -> Pointers.block -> Z.z **)
[2601]307let high_bound m b =
308  (m.blocks b).high
309
[2773]310(** val block_region : mem -> Pointers.block -> AST.region **)
311let block_region m b =
[2649]312  Pointers.block_region b
[2601]313
314(** val do_if_in_bounds :
[2773]315    mem -> Pointers.pointer -> (Pointers.block -> block_contents -> Z.z ->
[2601]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 :
[2773]332    mem -> Pointers.pointer -> ByteValues.beval Types.option **)
[2601]333let beloadv m ptr =
334  do_if_in_bounds m ptr (fun b content off -> content.contents off)
335
336(** val bestorev :
[2773]337    mem -> Pointers.pointer -> ByteValues.beval -> mem Types.option **)
[2601]338let bestorev m ptr v =
339  do_if_in_bounds m ptr (fun b content off ->
[2773]340    let contents0 = update off v content.contents in
[2601]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.