open Preamble

open Div_and_mod

open Jmeq

open Russell

open Util

open Bool

open Relations

open Nat

open List

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open Extralib

open Proper

open PositiveMap

open Deqsets

open ErrorMessages

open PreIdentifiers

open Errors

open Lists

open Identifiers

open Integers

open AST

open Division

open Exp

open Arithmetic

open Setoids

open Monad

open Option

open Extranat

open Vector

open FoldStuff

open BitVector

open Positive

open Z

open BitVectorZ

open Pointers

open Hide

open ByteValues

(** val update : Z.z -> 'a1 -> (Z.z -> 'a1) -> Z.z -> 'a1 **)
let update x v f y =
  match Z.eqZb y x with
  | Bool.True -> v
  | Bool.False -> f y

(** val update_block :
    Pointers.block -> 'a1 -> (Pointers.block -> 'a1) -> Pointers.block -> 'a1 **)
let update_block x v f y =
  match Pointers.eq_block y x with
  | Bool.True -> v
  | Bool.False -> f y

type contentmap = Z.z -> ByteValues.beval

type block_contents = { low : Z.z; high : Z.z; contents : contentmap }

(** val block_contents_rect_Type4 :
    (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1 **)
let rec block_contents_rect_Type4 h_mk_block_contents x_6568 =
  let { low = low0; high = high0; contents = contents0 } = x_6568 in
  h_mk_block_contents low0 high0 contents0

(** val block_contents_rect_Type5 :
    (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1 **)
let rec block_contents_rect_Type5 h_mk_block_contents x_6570 =
  let { low = low0; high = high0; contents = contents0 } = x_6570 in
  h_mk_block_contents low0 high0 contents0

(** val block_contents_rect_Type3 :
    (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1 **)
let rec block_contents_rect_Type3 h_mk_block_contents x_6572 =
  let { low = low0; high = high0; contents = contents0 } = x_6572 in
  h_mk_block_contents low0 high0 contents0

(** val block_contents_rect_Type2 :
    (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1 **)
let rec block_contents_rect_Type2 h_mk_block_contents x_6574 =
  let { low = low0; high = high0; contents = contents0 } = x_6574 in
  h_mk_block_contents low0 high0 contents0

(** val block_contents_rect_Type1 :
    (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1 **)
let rec block_contents_rect_Type1 h_mk_block_contents x_6576 =
  let { low = low0; high = high0; contents = contents0 } = x_6576 in
  h_mk_block_contents low0 high0 contents0

(** val block_contents_rect_Type0 :
    (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1 **)
let rec block_contents_rect_Type0 h_mk_block_contents x_6578 =
  let { low = low0; high = high0; contents = contents0 } = x_6578 in
  h_mk_block_contents low0 high0 contents0

(** val low : block_contents -> Z.z **)
let rec low xxx =
  xxx.low

(** val high : block_contents -> Z.z **)
let rec high xxx =
  xxx.high

(** val contents : block_contents -> contentmap **)
let rec contents xxx =
  xxx.contents

(** val block_contents_inv_rect_Type4 :
    block_contents -> (Z.z -> Z.z -> contentmap -> __ -> 'a1) -> 'a1 **)
let block_contents_inv_rect_Type4 hterm h1 =
  let hcut = block_contents_rect_Type4 h1 hterm in hcut __

(** val block_contents_inv_rect_Type3 :
    block_contents -> (Z.z -> Z.z -> contentmap -> __ -> 'a1) -> 'a1 **)
let block_contents_inv_rect_Type3 hterm h1 =
  let hcut = block_contents_rect_Type3 h1 hterm in hcut __

(** val block_contents_inv_rect_Type2 :
    block_contents -> (Z.z -> Z.z -> contentmap -> __ -> 'a1) -> 'a1 **)
let block_contents_inv_rect_Type2 hterm h1 =
  let hcut = block_contents_rect_Type2 h1 hterm in hcut __

(** val block_contents_inv_rect_Type1 :
    block_contents -> (Z.z -> Z.z -> contentmap -> __ -> 'a1) -> 'a1 **)
let block_contents_inv_rect_Type1 hterm h1 =
  let hcut = block_contents_rect_Type1 h1 hterm in hcut __

(** val block_contents_inv_rect_Type0 :
    block_contents -> (Z.z -> Z.z -> contentmap -> __ -> 'a1) -> 'a1 **)
let block_contents_inv_rect_Type0 hterm h1 =
  let hcut = block_contents_rect_Type0 h1 hterm in hcut __

(** val block_contents_discr : block_contents -> block_contents -> __ **)
let block_contents_discr x y =
  Logic.eq_rect_Type2 x
    (let { low = a0; high = a1; contents = a2 } = x in
    Obj.magic (fun _ dH -> dH __ __ __)) y

(** val block_contents_jmdiscr : block_contents -> block_contents -> __ **)
let block_contents_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (let { low = a0; high = a1; contents = a2 } = x in
    Obj.magic (fun _ dH -> dH __ __ __)) y

type mem = { blocks : (Pointers.block -> block_contents); nextblock : Z.z }

(** val mem_rect_Type4 :
    ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem -> 'a1 **)
let rec mem_rect_Type4 h_mk_mem x_6594 =
  let { blocks = blocks0; nextblock = nextblock0 } = x_6594 in
  h_mk_mem blocks0 nextblock0 __

(** val mem_rect_Type5 :
    ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem -> 'a1 **)
let rec mem_rect_Type5 h_mk_mem x_6596 =
  let { blocks = blocks0; nextblock = nextblock0 } = x_6596 in
  h_mk_mem blocks0 nextblock0 __

(** val mem_rect_Type3 :
    ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem -> 'a1 **)
let rec mem_rect_Type3 h_mk_mem x_6598 =
  let { blocks = blocks0; nextblock = nextblock0 } = x_6598 in
  h_mk_mem blocks0 nextblock0 __

(** val mem_rect_Type2 :
    ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem -> 'a1 **)
let rec mem_rect_Type2 h_mk_mem x_6600 =
  let { blocks = blocks0; nextblock = nextblock0 } = x_6600 in
  h_mk_mem blocks0 nextblock0 __

(** val mem_rect_Type1 :
    ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem -> 'a1 **)
let rec mem_rect_Type1 h_mk_mem x_6602 =
  let { blocks = blocks0; nextblock = nextblock0 } = x_6602 in
  h_mk_mem blocks0 nextblock0 __

(** val mem_rect_Type0 :
    ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem -> 'a1 **)
let rec mem_rect_Type0 h_mk_mem x_6604 =
  let { blocks = blocks0; nextblock = nextblock0 } = x_6604 in
  h_mk_mem blocks0 nextblock0 __

(** val blocks : mem -> Pointers.block -> block_contents **)
let rec blocks xxx =
  xxx.blocks

(** val nextblock : mem -> Z.z **)
let rec nextblock xxx =
  xxx.nextblock

(** val mem_inv_rect_Type4 :
    mem -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
    'a1 **)
let mem_inv_rect_Type4 hterm h1 =
  let hcut = mem_rect_Type4 h1 hterm in hcut __

(** val mem_inv_rect_Type3 :
    mem -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
    'a1 **)
let mem_inv_rect_Type3 hterm h1 =
  let hcut = mem_rect_Type3 h1 hterm in hcut __

(** val mem_inv_rect_Type2 :
    mem -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
    'a1 **)
let mem_inv_rect_Type2 hterm h1 =
  let hcut = mem_rect_Type2 h1 hterm in hcut __

(** val mem_inv_rect_Type1 :
    mem -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
    'a1 **)
let mem_inv_rect_Type1 hterm h1 =
  let hcut = mem_rect_Type1 h1 hterm in hcut __

(** val mem_inv_rect_Type0 :
    mem -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
    'a1 **)
let mem_inv_rect_Type0 hterm h1 =
  let hcut = mem_rect_Type0 h1 hterm in hcut __

(** val mem_discr : mem -> mem -> __ **)
let mem_discr x y =
  Logic.eq_rect_Type2 x
    (let { blocks = a0; nextblock = a1 } = x in
    Obj.magic (fun _ dH -> dH __ __ __)) y

(** val mem_jmdiscr : mem -> mem -> __ **)
let mem_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (let { blocks = a0; nextblock = a1 } = x in
    Obj.magic (fun _ dH -> dH __ __ __)) y

(** val oneZ : Z.z **)
let oneZ =
  Z.Pos Positive.One

(** val empty_block : Z.z -> Z.z -> block_contents **)
let empty_block lo hi =
  { low = lo; high = hi; contents = (fun y -> ByteValues.BVundef) }

(** val empty : mem **)
let empty =
  { blocks = (fun x -> empty_block Z.OZ Z.OZ); nextblock = (Z.Pos
    Positive.One) }

(** val alloc : mem -> Z.z -> Z.z -> (mem, Pointers.block) Types.prod **)
let rec alloc m lo hi =
  let b = m.nextblock in
  { Types.fst = { blocks = (update_block b (empty_block lo hi) m.blocks);
  nextblock = (Z.zsucc m.nextblock) }; Types.snd = b }

(** val free : mem -> Pointers.block -> mem **)
let free m b =
  { blocks =
    (update_block b (empty_block (Z.Pos Positive.One) Z.OZ) m.blocks);
    nextblock = m.nextblock }

(** val free_list : mem -> Pointers.block List.list -> mem **)
let free_list m l =
  List.foldr (fun b m0 -> free m0 b) m l

(** val low_bound : mem -> Pointers.block -> Z.z **)
let low_bound m b =
  (m.blocks b).low

(** val high_bound : mem -> Pointers.block -> Z.z **)
let high_bound m b =
  (m.blocks b).high

(** val block_region : mem -> Pointers.block -> AST.region **)
let block_region m b =
  Pointers.block_region b

(** val do_if_in_bounds :
    mem -> Pointers.pointer -> (Pointers.block -> block_contents -> Z.z ->
    'a1) -> 'a1 Types.option **)
let do_if_in_bounds m ptr f =
  let b = ptr.Pointers.pblock in
  (match Z.zltb (Pointers.block_id b) m.nextblock with
   | Bool.True ->
     let content = m.blocks b in
     let off =
       BitVectorZ.z_of_unsigned_bitvector Pointers.offset_size
         (Pointers.offv ptr.Pointers.poff)
     in
     (match Bool.andb (Z.zleb content.low off) (Z.zltb off content.high) with
      | Bool.True -> Types.Some (f b content off)
      | Bool.False -> Types.None)
   | Bool.False -> Types.None)

(** val beloadv :
    mem -> Pointers.pointer -> ByteValues.beval Types.option **)
let beloadv m ptr =
  do_if_in_bounds m ptr (fun b content off -> content.contents off)

(** val bestorev :
    mem -> Pointers.pointer -> ByteValues.beval -> mem Types.option **)
let bestorev m ptr v =
  do_if_in_bounds m ptr (fun b content off ->
    let contents0 = update off v content.contents in
    let content0 = { low = content.low; high = content.high; contents =
      contents0 }
    in
    let blocks0 = update_block b content0 m.blocks in
    { blocks = blocks0; nextblock = m.nextblock })