source: extracted/frontEndMem.ml @ 2716

Last change on this file since 2716 was 2649, checked in by sacerdot, 7 years ago

...

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