extracted/memoryInjections.ml

   1 open Preamble
   2
   3 open SmallstepExec
   4
   5 open Cexec
   6
   7 open Sets
   8
   9 open Listb
  10
  11 open IO
  12
  13 open IOMonad
  14
  15 open Star
  16
  17 open ClassifyOp
  18
  19 open Events
  20
  21 open Smallstep
  22
  23 open Extra_bool
  24
  25 open Values
  26
  27 open FrontEndVal
  28
  29 open Hide
  30
  31 open ByteValues
  32
  33 open Division
  34
  35 open Z
  36
  37 open BitVectorZ
  38
  39 open Pointers
  40
  41 open GenMem
  42
  43 open FrontEndMem
  44
  45 open Globalenvs
  46
  47 open Csem
  48
  49 open CostLabel
  50
  51 open Coqlib
  52
  53 open Proper
  54
  55 open PositiveMap
  56
  57 open Deqsets
  58
  59 open ErrorMessages
  60
  61 open PreIdentifiers
  62
  63 open Errors
  64
  65 open Extralib
  66
  67 open Lists
  68
  69 open Positive
  70
  71 open Identifiers
  72
  73 open Exp
  74
  75 open Arithmetic
  76
  77 open Vector
  78
  79 open Div_and_mod
  80
  81 open Util
  82
  83 open FoldStuff
  84
  85 open BitVector
  86
  87 open Jmeq
  88
  89 open Russell
  90
  91 open List
  92
  93 open Setoids
  94
  95 open Monad
  96
  97 open Option
  98
  99 open Extranat
 100
 101 open Bool
 102
 103 open Relations
 104
 105 open Nat
 106
 107 open Integers
 108
 109 open Hints_declaration
 110
 111 open Core_notation
 112
 113 open Pts
 114
 115 open Logic
 116
 117 open Types
 118
 119 open AST
 120
 121 open Csyntax
 122
 123 open TypeComparison
 124
 125 open Frontend_misc
 126
 127 open MemProperties
 128
 129 (** val zoo : Pointers.offset -> Z.z **)
 130 let zoo x =
 131   BitVectorZ.z_of_unsigned_bitvector Pointers.offset_size (Pointers.offv x)
 132
 133 (** val boo : Z.z -> Pointers.offset **)
 134 let boo x =
 135   BitVectorZ.bitvector_of_Z Pointers.offset_size x
 136
 137 (** val block_decidable_eq :
 138     Pointers.block -> Pointers.block -> (__, __) Types.sum **)
 139 let block_decidable_eq clearme =
 140   let a = clearme in
 141   (fun clearme0 ->
 142   let b = clearme0 in
 143   (match Z.decidable_eq_Z_Type a b with
 144    | Types.Inl _ -> Types.Inl __
 145    | Types.Inr _ -> Types.Inr __))
 146
 147 type embedding =
 148   Pointers.block -> (Pointers.block, Pointers.offset) Types.prod Types.option
 149
 150 (** val offset_plus :
 151     Pointers.offset -> Pointers.offset -> Pointers.offset **)
 152 let offset_plus o1 o2 =
 153   Arithmetic.addition_n Pointers.offset_size (Pointers.offv o1)
 154     (Pointers.offv o2)
 155
 156 (** val pointer_translation :
 157     Pointers.pointer -> embedding -> Pointers.pointer Types.option **)
 158 let pointer_translation p e =
 159   let { Pointers.pblock = pblock; Pointers.poff = poff } = p in
 160   (match e pblock with
 161    | Types.None -> Types.None
 162    | Types.Some loc ->
 163      let { Types.fst = dest_block; Types.snd = dest_off } = loc in
 164      let ptr = { Pointers.pblock = dest_block; Pointers.poff =
 165        (offset_plus poff dest_off) }
 166      in
 167      Types.Some ptr)
 168
 169 (** val memory_inj_rect_Type4 :
 170     embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ ->
 171     __ -> __ -> 'a1) -> 'a1 **)
 172 let rec memory_inj_rect_Type4 e m1 m2 h_mk_memory_inj =
 173   h_mk_memory_inj __ __ __ __ __ __ __
 174
 175 (** val memory_inj_rect_Type5 :
 176     embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ ->
 177     __ -> __ -> 'a1) -> 'a1 **)
 178 let rec memory_inj_rect_Type5 e m1 m2 h_mk_memory_inj =
 179   h_mk_memory_inj __ __ __ __ __ __ __
 180
 181 (** val memory_inj_rect_Type3 :
 182     embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ ->
 183     __ -> __ -> 'a1) -> 'a1 **)
 184 let rec memory_inj_rect_Type3 e m1 m2 h_mk_memory_inj =
 185   h_mk_memory_inj __ __ __ __ __ __ __
 186
 187 (** val memory_inj_rect_Type2 :
 188     embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ ->
 189     __ -> __ -> 'a1) -> 'a1 **)
 190 let rec memory_inj_rect_Type2 e m1 m2 h_mk_memory_inj =
 191   h_mk_memory_inj __ __ __ __ __ __ __
 192
 193 (** val memory_inj_rect_Type1 :
 194     embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ ->
 195     __ -> __ -> 'a1) -> 'a1 **)
 196 let rec memory_inj_rect_Type1 e m1 m2 h_mk_memory_inj =
 197   h_mk_memory_inj __ __ __ __ __ __ __
 198
 199 (** val memory_inj_rect_Type0 :
 200     embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ ->
 201     __ -> __ -> 'a1) -> 'a1 **)
 202 let rec memory_inj_rect_Type0 e m1 m2 h_mk_memory_inj =
 203   h_mk_memory_inj __ __ __ __ __ __ __
 204
 205 (** val memory_inj_inv_rect_Type4 :
 206     embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ ->
 207     __ -> __ -> __ -> 'a1) -> 'a1 **)
 208 let memory_inj_inv_rect_Type4 x1 x2 x3 h1 =
 209   let hcut = memory_inj_rect_Type4 x1 x2 x3 h1 in hcut __
 210
 211 (** val memory_inj_inv_rect_Type3 :
 212     embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ ->
 213     __ -> __ -> __ -> 'a1) -> 'a1 **)
 214 let memory_inj_inv_rect_Type3 x1 x2 x3 h1 =
 215   let hcut = memory_inj_rect_Type3 x1 x2 x3 h1 in hcut __
 216
 217 (** val memory_inj_inv_rect_Type2 :
 218     embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ ->
 219     __ -> __ -> __ -> 'a1) -> 'a1 **)
 220 let memory_inj_inv_rect_Type2 x1 x2 x3 h1 =
 221   let hcut = memory_inj_rect_Type2 x1 x2 x3 h1 in hcut __
 222
 223 (** val memory_inj_inv_rect_Type1 :
 224     embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ ->
 225     __ -> __ -> __ -> 'a1) -> 'a1 **)
 226 let memory_inj_inv_rect_Type1 x1 x2 x3 h1 =
 227   let hcut = memory_inj_rect_Type1 x1 x2 x3 h1 in hcut __
 228
 229 (** val memory_inj_inv_rect_Type0 :
 230     embedding -> GenMem.mem -> GenMem.mem -> (__ -> __ -> __ -> __ -> __ ->
 231     __ -> __ -> __ -> 'a1) -> 'a1 **)
 232 let memory_inj_inv_rect_Type0 x1 x2 x3 h1 =
 233   let hcut = memory_inj_rect_Type0 x1 x2 x3 h1 in hcut __
 234
 235 (** val memory_inj_jmdiscr : embedding -> GenMem.mem -> GenMem.mem -> __ **)
 236 let memory_inj_jmdiscr a1 a2 a3 =
 237   Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __)) __
 238
 239 (** val typesize' : Csyntax.type0 -> Nat.nat **)
 240 let typesize' ty =
 241   AST.typesize (Csyntax.typ_of_type ty)
 242