extracted/frontEndMem.ml

   1 open Preamble
   2
   3 open Hide
   4
   5 open ByteValues
   6
   7 open Proper
   8
   9 open PositiveMap
  10
  11 open Deqsets
  12
  13 open ErrorMessages
  14
  15 open PreIdentifiers
  16
  17 open Errors
  18
  19 open Lists
  20
  21 open Identifiers
  22
  23 open Integers
  24
  25 open AST
  26
  27 open Division
  28
  29 open Exp
  30
  31 open Arithmetic
  32
  33 open Setoids
  34
  35 open Monad
  36
  37 open Option
  38
  39 open Extranat
  40
  41 open Vector
  42
  43 open FoldStuff
  44
  45 open BitVector
  46
  47 open Positive
  48
  49 open Z
  50
  51 open BitVectorZ
  52
  53 open Pointers
  54
  55 open Div_and_mod
  56
  57 open Jmeq
  58
  59 open Russell
  60
  61 open Util
  62
  63 open Bool
  64
  65 open Relations
  66
  67 open Nat
  68
  69 open List
  70
  71 open Hints_declaration
  72
  73 open Core_notation
  74
  75 open Pts
  76
  77 open Logic
  78
  79 open Types
  80
  81 open Extralib
  82
  83 open GenMem
  84
  85 open Coqlib
  86
  87 open Values
  88
  89 open FrontEndVal
  90
  91 (** val loadn :
  92     GenMem.mem -> Pointers.pointer -> Nat.nat -> ByteValues.beval List.list
  93     Types.option **)
  94 let rec loadn m ptr = function
  95 | Nat.O -> Types.Some List.Nil
  96 | Nat.S n' ->
  97   (match GenMem.beloadv m ptr with
  98    | Types.None -> Types.None
  99    | Types.Some v ->
 100      (match loadn m
 101               (Pointers.shift_pointer (Nat.S (Nat.S Nat.O)) ptr
 102                 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S Nat.O)) (Nat.S
 103                   Nat.O))) n' with
 104       | Types.None -> Types.None
 105       | Types.Some vs -> Types.Some (List.Cons (v, vs))))
 106
 107 (** val load :
 108     AST.typ -> GenMem.mem -> Pointers.pointer -> Values.val0 Types.option **)
 109 let load t m ptr =
 110   match loadn m ptr (AST.typesize t) with
 111   | Types.None -> Types.None
 112   | Types.Some vs -> Types.Some (FrontEndVal.be_to_fe_value t vs)
 113
 114 (** val loadv :
 115     AST.typ -> GenMem.mem -> Values.val0 -> Values.val0 Types.option **)
 116 let rec loadv t m = function
 117 | Values.Vundef -> Types.None
 118 | Values.Vint (x, x0) -> Types.None
 119 | Values.Vnull -> Types.None
 120 | Values.Vptr ptr -> load t m ptr
 121
 122 (** val storen :
 123     GenMem.mem -> Pointers.pointer -> ByteValues.beval List.list ->
 124     GenMem.mem Types.option **)
 125 let rec storen m ptr = function
 126 | List.Nil -> Types.Some m
 127 | List.Cons (v, tl) ->
 128   (match GenMem.bestorev m ptr v with
 129    | Types.None -> Types.None
 130    | Types.Some m' ->
 131      storen m'
 132        (Pointers.shift_pointer (Nat.S (Nat.S Nat.O)) ptr
 133          (Arithmetic.bitvector_of_nat (Nat.S (Nat.S Nat.O)) (Nat.S Nat.O)))
 134        tl)
 135
 136 (** val store :
 137     AST.typ -> GenMem.mem -> Pointers.pointer -> Values.val0 -> GenMem.mem
 138     Types.option **)
 139 let store t m ptr v =
 140   storen m ptr (FrontEndVal.fe_to_be_values t v)
 141
 142 (** val storev :
 143     AST.typ -> GenMem.mem -> Values.val0 -> Values.val0 -> GenMem.mem
 144     Types.option **)
 145 let storev t m addr v =
 146   match addr with
 147   | Values.Vundef -> Types.None
 148   | Values.Vint (x, x0) -> Types.None
 149   | Values.Vnull -> Types.None
 150   | Values.Vptr ptr -> store t m ptr v
 151
 152 (** val valid_pointer : GenMem.mem -> Pointers.pointer -> Bool.bool **)
 153 let valid_pointer m ptr =
 154   let off =
 155     BitVectorZ.z_of_unsigned_bitvector Pointers.offset_size
 156       (Pointers.offv ptr.Pointers.poff)
 157   in
 158   Bool.andb
 159     (Bool.andb
 160       (Z.zltb (Pointers.block_id ptr.Pointers.pblock) m.GenMem.nextblock)
 161       (Z.zleb (GenMem.low_bound m ptr.Pointers.pblock) off))
 162     (Z.zltb off (GenMem.high_bound m ptr.Pointers.pblock))
 163