19 open Hints_declaration
83 (** val update : Z.z -> 'a1 -> (Z.z -> 'a1) -> Z.z -> 'a1 **)
89 (** val update_block :
90 Pointers.block -> 'a1 -> (Pointers.block -> 'a1) -> Pointers.block -> 'a1 **)
91 let update_block x v f y =
92 match Pointers.eq_block y x with
96 type contentmap = Z.z -> ByteValues.beval
98 type block_contents = { low : Z.z; high : Z.z; contents : contentmap }
100 (** val block_contents_rect_Type4 :
101 (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1 **)
102 let 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
106 (** val block_contents_rect_Type5 :
107 (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1 **)
108 let 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
112 (** val block_contents_rect_Type3 :
113 (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1 **)
114 let 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
118 (** val block_contents_rect_Type2 :
119 (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1 **)
120 let 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
124 (** val block_contents_rect_Type1 :
125 (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1 **)
126 let 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
130 (** val block_contents_rect_Type0 :
131 (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1 **)
132 let 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
136 (** val low : block_contents -> Z.z **)
140 (** val high : block_contents -> Z.z **)
144 (** val contents : block_contents -> contentmap **)
145 let rec contents xxx =
148 (** val block_contents_inv_rect_Type4 :
149 block_contents -> (Z.z -> Z.z -> contentmap -> __ -> 'a1) -> 'a1 **)
150 let block_contents_inv_rect_Type4 hterm h1 =
151 let hcut = block_contents_rect_Type4 h1 hterm in hcut __
153 (** val block_contents_inv_rect_Type3 :
154 block_contents -> (Z.z -> Z.z -> contentmap -> __ -> 'a1) -> 'a1 **)
155 let block_contents_inv_rect_Type3 hterm h1 =
156 let hcut = block_contents_rect_Type3 h1 hterm in hcut __
158 (** val block_contents_inv_rect_Type2 :
159 block_contents -> (Z.z -> Z.z -> contentmap -> __ -> 'a1) -> 'a1 **)
160 let block_contents_inv_rect_Type2 hterm h1 =
161 let hcut = block_contents_rect_Type2 h1 hterm in hcut __
163 (** val block_contents_inv_rect_Type1 :
164 block_contents -> (Z.z -> Z.z -> contentmap -> __ -> 'a1) -> 'a1 **)
165 let block_contents_inv_rect_Type1 hterm h1 =
166 let hcut = block_contents_rect_Type1 h1 hterm in hcut __
168 (** val block_contents_inv_rect_Type0 :
169 block_contents -> (Z.z -> Z.z -> contentmap -> __ -> 'a1) -> 'a1 **)
170 let block_contents_inv_rect_Type0 hterm h1 =
171 let hcut = block_contents_rect_Type0 h1 hterm in hcut __
173 (** val block_contents_discr : block_contents -> block_contents -> __ **)
174 let 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
179 (** val block_contents_jmdiscr : block_contents -> block_contents -> __ **)
180 let 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
185 type mem = { blocks : (Pointers.block -> block_contents); nextblock : Z.z }
187 (** val mem_rect_Type4 :
188 ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem -> 'a1 **)
189 let rec mem_rect_Type4 h_mk_mem x_6594 =
190 let { blocks = blocks0; nextblock = nextblock0 } = x_6594 in
191 h_mk_mem blocks0 nextblock0 __
193 (** val mem_rect_Type5 :
194 ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem -> 'a1 **)
195 let rec mem_rect_Type5 h_mk_mem x_6596 =
196 let { blocks = blocks0; nextblock = nextblock0 } = x_6596 in
197 h_mk_mem blocks0 nextblock0 __
199 (** val mem_rect_Type3 :
200 ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem -> 'a1 **)
201 let rec mem_rect_Type3 h_mk_mem x_6598 =
202 let { blocks = blocks0; nextblock = nextblock0 } = x_6598 in
203 h_mk_mem blocks0 nextblock0 __
205 (** val mem_rect_Type2 :
206 ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem -> 'a1 **)
207 let rec mem_rect_Type2 h_mk_mem x_6600 =
208 let { blocks = blocks0; nextblock = nextblock0 } = x_6600 in
209 h_mk_mem blocks0 nextblock0 __
211 (** val mem_rect_Type1 :
212 ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem -> 'a1 **)
213 let rec mem_rect_Type1 h_mk_mem x_6602 =
214 let { blocks = blocks0; nextblock = nextblock0 } = x_6602 in
215 h_mk_mem blocks0 nextblock0 __
217 (** val mem_rect_Type0 :
218 ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem -> 'a1 **)
219 let rec mem_rect_Type0 h_mk_mem x_6604 =
220 let { blocks = blocks0; nextblock = nextblock0 } = x_6604 in
221 h_mk_mem blocks0 nextblock0 __
223 (** val blocks : mem -> Pointers.block -> block_contents **)
227 (** val nextblock : mem -> Z.z **)
228 let rec nextblock xxx =
231 (** val mem_inv_rect_Type4 :
232 mem -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
234 let mem_inv_rect_Type4 hterm h1 =
235 let hcut = mem_rect_Type4 h1 hterm in hcut __
237 (** val mem_inv_rect_Type3 :
238 mem -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
240 let mem_inv_rect_Type3 hterm h1 =
241 let hcut = mem_rect_Type3 h1 hterm in hcut __
243 (** val mem_inv_rect_Type2 :
244 mem -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
246 let mem_inv_rect_Type2 hterm h1 =
247 let hcut = mem_rect_Type2 h1 hterm in hcut __
249 (** val mem_inv_rect_Type1 :
250 mem -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
252 let mem_inv_rect_Type1 hterm h1 =
253 let hcut = mem_rect_Type1 h1 hterm in hcut __
255 (** val mem_inv_rect_Type0 :
256 mem -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
258 let mem_inv_rect_Type0 hterm h1 =
259 let hcut = mem_rect_Type0 h1 hterm in hcut __
261 (** val mem_discr : mem -> mem -> __ **)
263 Logic.eq_rect_Type2 x
264 (let { blocks = a0; nextblock = a1 } = x in
265 Obj.magic (fun _ dH -> dH __ __ __)) y
267 (** val mem_jmdiscr : mem -> mem -> __ **)
268 let 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
273 (** val oneZ : Z.z **)
277 (** val empty_block : Z.z -> Z.z -> block_contents **)
278 let empty_block lo hi =
279 { low = lo; high = hi; contents = (fun y -> ByteValues.BVundef) }
281 (** val empty : mem **)
283 { blocks = (fun x -> empty_block Z.OZ Z.OZ); nextblock = (Z.Pos
286 (** val alloc : mem -> Z.z -> Z.z -> (mem, Pointers.block) Types.prod **)
287 let 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 }
292 (** val free : mem -> Pointers.block -> mem **)
295 (update_block b (empty_block (Z.Pos Positive.One) Z.OZ) m.blocks);
296 nextblock = m.nextblock }
298 (** val free_list : mem -> Pointers.block List.list -> mem **)
300 List.foldr (fun b m0 -> free m0 b) m l
302 (** val low_bound : mem -> Pointers.block -> Z.z **)
306 (** val high_bound : mem -> Pointers.block -> Z.z **)
310 (** val block_region : mem -> Pointers.block -> AST.region **)
311 let block_region m b =
312 Pointers.block_region b
314 (** val do_if_in_bounds :
315 mem -> Pointers.pointer -> (Pointers.block -> block_contents -> Z.z ->
316 'a1) -> 'a1 Types.option **)
317 let 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
321 let content = m.blocks b in
323 BitVectorZ.z_of_unsigned_bitvector Pointers.offset_size
324 (Pointers.offv ptr.Pointers.poff)
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)
332 mem -> Pointers.pointer -> ByteValues.beval Types.option **)
334 do_if_in_bounds m ptr (fun b content off -> content.contents off)
337 mem -> Pointers.pointer -> ByteValues.beval -> mem Types.option **)
338 let 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 =
344 let blocks0 = update_block b content0 m.blocks in
345 { blocks = blocks0; nextblock = m.nextblock })