extracted/genMem.ml

   1 open Preamble
   2
   3 open Div_and_mod
   4
   5 open Jmeq
   6
   7 open Russell
   8
   9 open Util
  10
  11 open Bool
  12
  13 open Relations
  14
  15 open Nat
  16
  17 open List
  18
  19 open Hints_declaration
  20
  21 open Core_notation
  22
  23 open Pts
  24
  25 open Logic
  26
  27 open Types
  28
  29 open Extralib
  30
  31 open Proper
  32
  33 open PositiveMap
  34
  35 open Deqsets
  36
  37 open ErrorMessages
  38
  39 open PreIdentifiers
  40
  41 open Errors
  42
  43 open Lists
  44
  45 open Identifiers
  46
  47 open Integers
  48
  49 open AST
  50
  51 open Division
  52
  53 open Exp
  54
  55 open Arithmetic
  56
  57 open Setoids
  58
  59 open Monad
  60
  61 open Option
  62
  63 open Extranat
  64
  65 open Vector
  66
  67 open FoldStuff
  68
  69 open BitVector
  70
  71 open Positive
  72
  73 open Z
  74
  75 open BitVectorZ
  76
  77 open Pointers
  78
  79 open Hide
  80
  81 open ByteValues
  82
  83 (** val update : Z.z -> 'a1 -> (Z.z -> 'a1) -> Z.z -> 'a1 **)
  84 let 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 **)
  91 let update_block x v f y =
  92   match Pointers.eq_block y x with
  93   | Bool.True -> v
  94   | Bool.False -> f y
  95
  96 type contentmap = Z.z -> ByteValues.beval
  97
  98 type 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 **)
 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
 105
 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
 111
 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
 117
 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
 123
 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
 129
 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
 135
 136 (** val low : block_contents -> Z.z **)
 137 let rec low xxx =
 138   xxx.low
 139
 140 (** val high : block_contents -> Z.z **)
 141 let rec high xxx =
 142   xxx.high
 143
 144 (** val contents : block_contents -> contentmap **)
 145 let rec contents xxx =
 146   xxx.contents
 147
 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 __
 152
 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 __
 157
 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 __
 162
 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 __
 167
 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 __
 172
 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
 178
 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
 184
 185 type 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 **)
 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 __
 192
 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 __
 198
 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 __
 204
 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 __
 210
 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 __
 216
 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 __
 222
 223 (** val blocks : mem -> Pointers.block -> block_contents **)
 224 let rec blocks xxx =
 225   xxx.blocks
 226
 227 (** val nextblock : mem -> Z.z **)
 228 let rec nextblock xxx =
 229   xxx.nextblock
 230
 231 (** val mem_inv_rect_Type4 :
 232     mem -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
 233     'a1 **)
 234 let 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 **)
 240 let 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 **)
 246 let 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 **)
 252 let 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 **)
 258 let mem_inv_rect_Type0 hterm h1 =
 259   let hcut = mem_rect_Type0 h1 hterm in hcut __
 260
 261 (** val mem_discr : mem -> mem -> __ **)
 262 let 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 -> __ **)
 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
 272
 273 (** val oneZ : Z.z **)
 274 let oneZ =
 275   Z.Pos Positive.One
 276
 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) }
 280
 281 (** val empty : mem **)
 282 let 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 **)
 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 }
 291
 292 (** val free : mem -> Pointers.block -> mem **)
 293 let 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 **)
 299 let 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 **)
 303 let low_bound m b =
 304   (m.blocks b).low
 305
 306 (** val high_bound : mem -> Pointers.block -> Z.z **)
 307 let high_bound m b =
 308   (m.blocks b).high
 309
 310 (** val block_region : mem -> Pointers.block -> AST.region **)
 311 let 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 **)
 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
 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 **)
 333 let 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 **)
 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 =
 342       contents0 }
 343     in
 344     let blocks0 = update_block b content0 m.blocks in
 345     { blocks = blocks0; nextblock = m.nextblock })
 346