extracted/pointers.ml

   1 open Preamble
   2
   3 open Division
   4
   5 open Exp
   6
   7 open Arithmetic
   8
   9 open Setoids
  10
  11 open Monad
  12
  13 open Option
  14
  15 open Extranat
  16
  17 open Vector
  18
  19 open Div_and_mod
  20
  21 open Jmeq
  22
  23 open Russell
  24
  25 open List
  26
  27 open Util
  28
  29 open FoldStuff
  30
  31 open BitVector
  32
  33 open Types
  34
  35 open Bool
  36
  37 open Relations
  38
  39 open Nat
  40
  41 open Hints_declaration
  42
  43 open Core_notation
  44
  45 open Pts
  46
  47 open Logic
  48
  49 open Positive
  50
  51 open Z
  52
  53 open BitVectorZ
  54
  55 open Proper
  56
  57 open PositiveMap
  58
  59 open Deqsets
  60
  61 open ErrorMessages
  62
  63 open PreIdentifiers
  64
  65 open Errors
  66
  67 open Extralib
  68
  69 open Lists
  70
  71 open Identifiers
  72
  73 open Integers
  74
  75 open AST
  76
  77 type block =
  78   Z.z
  79   (* singleton inductive, whose constructor was mk_block *)
  80
  81 (** val block_rect_Type4 : (Z.z -> 'a1) -> block -> 'a1 **)
  82 let rec block_rect_Type4 h_mk_block x_5028 =
  83   let block_id = x_5028 in h_mk_block block_id
  84
  85 (** val block_rect_Type5 : (Z.z -> 'a1) -> block -> 'a1 **)
  86 let rec block_rect_Type5 h_mk_block x_5030 =
  87   let block_id = x_5030 in h_mk_block block_id
  88
  89 (** val block_rect_Type3 : (Z.z -> 'a1) -> block -> 'a1 **)
  90 let rec block_rect_Type3 h_mk_block x_5032 =
  91   let block_id = x_5032 in h_mk_block block_id
  92
  93 (** val block_rect_Type2 : (Z.z -> 'a1) -> block -> 'a1 **)
  94 let rec block_rect_Type2 h_mk_block x_5034 =
  95   let block_id = x_5034 in h_mk_block block_id
  96
  97 (** val block_rect_Type1 : (Z.z -> 'a1) -> block -> 'a1 **)
  98 let rec block_rect_Type1 h_mk_block x_5036 =
  99   let block_id = x_5036 in h_mk_block block_id
 100
 101 (** val block_rect_Type0 : (Z.z -> 'a1) -> block -> 'a1 **)
 102 let rec block_rect_Type0 h_mk_block x_5038 =
 103   let block_id = x_5038 in h_mk_block block_id
 104
 105 (** val block_id : block -> Z.z **)
 106 let rec block_id xxx =
 107   let yyy = xxx in yyy
 108
 109 (** val block_inv_rect_Type4 : block -> (Z.z -> __ -> 'a1) -> 'a1 **)
 110 let block_inv_rect_Type4 hterm h1 =
 111   let hcut = block_rect_Type4 h1 hterm in hcut __
 112
 113 (** val block_inv_rect_Type3 : block -> (Z.z -> __ -> 'a1) -> 'a1 **)
 114 let block_inv_rect_Type3 hterm h1 =
 115   let hcut = block_rect_Type3 h1 hterm in hcut __
 116
 117 (** val block_inv_rect_Type2 : block -> (Z.z -> __ -> 'a1) -> 'a1 **)
 118 let block_inv_rect_Type2 hterm h1 =
 119   let hcut = block_rect_Type2 h1 hterm in hcut __
 120
 121 (** val block_inv_rect_Type1 : block -> (Z.z -> __ -> 'a1) -> 'a1 **)
 122 let block_inv_rect_Type1 hterm h1 =
 123   let hcut = block_rect_Type1 h1 hterm in hcut __
 124
 125 (** val block_inv_rect_Type0 : block -> (Z.z -> __ -> 'a1) -> 'a1 **)
 126 let block_inv_rect_Type0 hterm h1 =
 127   let hcut = block_rect_Type0 h1 hterm in hcut __
 128
 129 (** val block_discr : block -> block -> __ **)
 130 let block_discr x y =
 131   Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
 132
 133 (** val block_jmdiscr : block -> block -> __ **)
 134 let block_jmdiscr x y =
 135   Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
 136
 137 (** val block_region : block -> AST.region **)
 138 let block_region b =
 139   match Z.zleb (block_id b) Z.OZ with
 140   | Bool.True -> AST.Code
 141   | Bool.False -> AST.XData
 142
 143 (** val dummy_block_code : block **)
 144 let dummy_block_code =
 145   Z.OZ
 146
 147 (** val eq_block : block -> block -> Bool.bool **)
 148 let eq_block b1 b2 =
 149   Z.eqZb (block_id b1) (block_id b2)
 150
 151 (** val block_eq : Deqsets.deqSet **)
 152 let block_eq =
 153   Obj.magic eq_block
 154
 155 (** val offset_size : Nat.nat **)
 156 let offset_size =
 157   Nat.times (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 158     Nat.O)))))))) AST.size_pointer
 159
 160 type offset =
 161   BitVector.bitVector
 162   (* singleton inductive, whose constructor was mk_offset *)
 163
 164 (** val offset_rect_Type4 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
 165 let rec offset_rect_Type4 h_mk_offset x_5054 =
 166   let offv = x_5054 in h_mk_offset offv
 167
 168 (** val offset_rect_Type5 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
 169 let rec offset_rect_Type5 h_mk_offset x_5056 =
 170   let offv = x_5056 in h_mk_offset offv
 171
 172 (** val offset_rect_Type3 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
 173 let rec offset_rect_Type3 h_mk_offset x_5058 =
 174   let offv = x_5058 in h_mk_offset offv
 175
 176 (** val offset_rect_Type2 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
 177 let rec offset_rect_Type2 h_mk_offset x_5060 =
 178   let offv = x_5060 in h_mk_offset offv
 179
 180 (** val offset_rect_Type1 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
 181 let rec offset_rect_Type1 h_mk_offset x_5062 =
 182   let offv = x_5062 in h_mk_offset offv
 183
 184 (** val offset_rect_Type0 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
 185 let rec offset_rect_Type0 h_mk_offset x_5064 =
 186   let offv = x_5064 in h_mk_offset offv
 187
 188 (** val offv : offset -> BitVector.bitVector **)
 189 let rec offv xxx =
 190   let yyy = xxx in yyy
 191
 192 (** val offset_inv_rect_Type4 :
 193     offset -> (BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
 194 let offset_inv_rect_Type4 hterm h1 =
 195   let hcut = offset_rect_Type4 h1 hterm in hcut __
 196
 197 (** val offset_inv_rect_Type3 :
 198     offset -> (BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
 199 let offset_inv_rect_Type3 hterm h1 =
 200   let hcut = offset_rect_Type3 h1 hterm in hcut __
 201
 202 (** val offset_inv_rect_Type2 :
 203     offset -> (BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
 204 let offset_inv_rect_Type2 hterm h1 =
 205   let hcut = offset_rect_Type2 h1 hterm in hcut __
 206
 207 (** val offset_inv_rect_Type1 :
 208     offset -> (BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
 209 let offset_inv_rect_Type1 hterm h1 =
 210   let hcut = offset_rect_Type1 h1 hterm in hcut __
 211
 212 (** val offset_inv_rect_Type0 :
 213     offset -> (BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
 214 let offset_inv_rect_Type0 hterm h1 =
 215   let hcut = offset_rect_Type0 h1 hterm in hcut __
 216
 217 (** val offset_discr : offset -> offset -> __ **)
 218 let offset_discr x y =
 219   Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
 220
 221 (** val offset_jmdiscr : offset -> offset -> __ **)
 222 let offset_jmdiscr x y =
 223   Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
 224
 225 (** val eq_offset : offset -> offset -> Bool.bool **)
 226 let eq_offset x y =
 227   BitVector.eq_bv offset_size (offv x) (offv y)
 228
 229 (** val offset_of_Z : Z.z -> offset **)
 230 let offset_of_Z z =
 231   BitVectorZ.bitvector_of_Z offset_size z
 232
 233 (** val shift_offset : Nat.nat -> offset -> BitVector.bitVector -> offset **)
 234 let shift_offset n o i =
 235   Arithmetic.addition_n offset_size (offv o)
 236     (Arithmetic.sign_ext n offset_size i)
 237
 238 (** val shift_offset_n :
 239     Nat.nat -> offset -> Nat.nat -> AST.signedness -> BitVector.bitVector ->
 240     offset **)
 241 let shift_offset_n n o i sg j =
 242   Arithmetic.addition_n offset_size (offv o)
 243     (Arithmetic.short_multiplication offset_size
 244       (Arithmetic.bitvector_of_nat offset_size i)
 245       (match sg with
 246        | AST.Signed -> Arithmetic.sign_ext n offset_size j
 247        | AST.Unsigned -> Arithmetic.zero_ext n offset_size j))
 248
 249 (** val neg_shift_offset :
 250     Nat.nat -> offset -> BitVector.bitVector -> offset **)
 251 let neg_shift_offset n o i =
 252   Arithmetic.subtraction offset_size (offv o)
 253     (Arithmetic.sign_ext n offset_size i)
 254
 255 (** val neg_shift_offset_n :
 256     Nat.nat -> offset -> Nat.nat -> AST.signedness -> BitVector.bitVector ->
 257     offset **)
 258 let neg_shift_offset_n n o i sg j =
 259   Arithmetic.subtraction offset_size (offv o)
 260     (Arithmetic.short_multiplication offset_size
 261       (Arithmetic.bitvector_of_nat offset_size i)
 262       (match sg with
 263        | AST.Signed -> Arithmetic.sign_ext n offset_size j
 264        | AST.Unsigned -> Arithmetic.zero_ext n offset_size j))
 265
 266 (** val sub_offset : Nat.nat -> offset -> offset -> BitVector.bitVector **)
 267 let sub_offset n x y =
 268   Arithmetic.sign_ext offset_size n
 269     (Arithmetic.subtraction offset_size (offv x) (offv y))
 270
 271 (** val zero_offset : offset **)
 272 let zero_offset =
 273   BitVector.zero offset_size
 274
 275 (** val lt_offset : offset -> offset -> Bool.bool **)
 276 let lt_offset x y =
 277   Arithmetic.lt_u offset_size (offv x) (offv y)
 278
 279 type pointer = { pblock : block; poff : offset }
 280
 281 (** val pointer_rect_Type4 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
 282 let rec pointer_rect_Type4 h_mk_pointer x_5080 =
 283   let { pblock = pblock0; poff = poff0 } = x_5080 in
 284   h_mk_pointer pblock0 poff0
 285
 286 (** val pointer_rect_Type5 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
 287 let rec pointer_rect_Type5 h_mk_pointer x_5082 =
 288   let { pblock = pblock0; poff = poff0 } = x_5082 in
 289   h_mk_pointer pblock0 poff0
 290
 291 (** val pointer_rect_Type3 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
 292 let rec pointer_rect_Type3 h_mk_pointer x_5084 =
 293   let { pblock = pblock0; poff = poff0 } = x_5084 in
 294   h_mk_pointer pblock0 poff0
 295
 296 (** val pointer_rect_Type2 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
 297 let rec pointer_rect_Type2 h_mk_pointer x_5086 =
 298   let { pblock = pblock0; poff = poff0 } = x_5086 in
 299   h_mk_pointer pblock0 poff0
 300
 301 (** val pointer_rect_Type1 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
 302 let rec pointer_rect_Type1 h_mk_pointer x_5088 =
 303   let { pblock = pblock0; poff = poff0 } = x_5088 in
 304   h_mk_pointer pblock0 poff0
 305
 306 (** val pointer_rect_Type0 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
 307 let rec pointer_rect_Type0 h_mk_pointer x_5090 =
 308   let { pblock = pblock0; poff = poff0 } = x_5090 in
 309   h_mk_pointer pblock0 poff0
 310
 311 (** val pblock : pointer -> block **)
 312 let rec pblock xxx =
 313   xxx.pblock
 314
 315 (** val poff : pointer -> offset **)
 316 let rec poff xxx =
 317   xxx.poff
 318
 319 (** val pointer_inv_rect_Type4 :
 320     pointer -> (block -> offset -> __ -> 'a1) -> 'a1 **)
 321 let pointer_inv_rect_Type4 hterm h1 =
 322   let hcut = pointer_rect_Type4 h1 hterm in hcut __
 323
 324 (** val pointer_inv_rect_Type3 :
 325     pointer -> (block -> offset -> __ -> 'a1) -> 'a1 **)
 326 let pointer_inv_rect_Type3 hterm h1 =
 327   let hcut = pointer_rect_Type3 h1 hterm in hcut __
 328
 329 (** val pointer_inv_rect_Type2 :
 330     pointer -> (block -> offset -> __ -> 'a1) -> 'a1 **)
 331 let pointer_inv_rect_Type2 hterm h1 =
 332   let hcut = pointer_rect_Type2 h1 hterm in hcut __
 333
 334 (** val pointer_inv_rect_Type1 :
 335     pointer -> (block -> offset -> __ -> 'a1) -> 'a1 **)
 336 let pointer_inv_rect_Type1 hterm h1 =
 337   let hcut = pointer_rect_Type1 h1 hterm in hcut __
 338
 339 (** val pointer_inv_rect_Type0 :
 340     pointer -> (block -> offset -> __ -> 'a1) -> 'a1 **)
 341 let pointer_inv_rect_Type0 hterm h1 =
 342   let hcut = pointer_rect_Type0 h1 hterm in hcut __
 343
 344 (** val pointer_discr : pointer -> pointer -> __ **)
 345 let pointer_discr x y =
 346   Logic.eq_rect_Type2 x
 347     (let { pblock = a0; poff = a1 } = x in Obj.magic (fun _ dH -> dH __ __))
 348     y
 349
 350 (** val pointer_jmdiscr : pointer -> pointer -> __ **)
 351 let pointer_jmdiscr x y =
 352   Logic.eq_rect_Type2 x
 353     (let { pblock = a0; poff = a1 } = x in Obj.magic (fun _ dH -> dH __ __))
 354     y
 355
 356 (** val ptype : pointer -> AST.region **)
 357 let ptype p =
 358   block_region p.pblock
 359
 360 (** val shift_pointer :
 361     Nat.nat -> pointer -> BitVector.bitVector -> pointer **)
 362 let shift_pointer n p i =
 363   { pblock = p.pblock; poff = (shift_offset n p.poff i) }
 364
 365 (** val shift_pointer_n :
 366     Nat.nat -> pointer -> Nat.nat -> AST.signedness -> BitVector.bitVector ->
 367     pointer **)
 368 let shift_pointer_n n p i sg j =
 369   { pblock = p.pblock; poff = (shift_offset_n n p.poff i sg j) }
 370
 371 (** val neg_shift_pointer :
 372     Nat.nat -> pointer -> BitVector.bitVector -> pointer **)
 373 let neg_shift_pointer n p i =
 374   { pblock = p.pblock; poff = (neg_shift_offset n p.poff i) }
 375
 376 (** val neg_shift_pointer_n :
 377     Nat.nat -> pointer -> Nat.nat -> AST.signedness -> BitVector.bitVector ->
 378     pointer **)
 379 let neg_shift_pointer_n n p i sg j =
 380   { pblock = p.pblock; poff = (neg_shift_offset_n n p.poff i sg j) }
 381
 382 (** val eq_pointer : pointer -> pointer -> Bool.bool **)
 383 let eq_pointer p1 p2 =
 384   Bool.andb (eq_block p1.pblock p2.pblock) (eq_offset p1.poff p2.poff)
 385