source: extracted/frontEndMem.ml @ 2717

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

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

File size: 3.0 KB
Line 
1open Preamble
2
3open Hide
4
5open ByteValues
6
7open Proper
8
9open PositiveMap
10
11open Deqsets
12
13open ErrorMessages
14
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 Exp
36
37open Arithmetic
38
39open Extranat
40
41open Vector
42
43open FoldStuff
44
45open BitVector
46
47open Positive
48
49open Z
50
51open BitVectorZ
52
53open Pointers
54
55open Div_and_mod
56
57open Jmeq
58
59open Russell
60
61open Util
62
63open Bool
64
65open Relations
66
67open Nat
68
69open List
70
71open Hints_declaration
72
73open Core_notation
74
75open Pts
76
77open Logic
78
79open Types
80
81open Extralib
82
83open GenMem
84
85open Coqlib
86
87open Values
88
89open FrontEndVal
90
91(** val loadn :
92    GenMem.mem1 -> Pointers.pointer -> Nat.nat -> ByteValues.beval List.list
93    Types.option **)
94let 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.mem1 -> Pointers.pointer -> Values.val0 Types.option **)
109let 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.mem1 -> Values.val0 -> Values.val0 Types.option **)
116let 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.mem1 -> Pointers.pointer -> ByteValues.beval List.list ->
124    GenMem.mem1 Types.option **)
125let 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.mem1 -> Pointers.pointer -> Values.val0 -> GenMem.mem1
138    Types.option **)
139let store t m ptr v =
140  storen m ptr (FrontEndVal.fe_to_be_values t v)
141
142(** val storev :
143    AST.typ -> GenMem.mem1 -> Values.val0 -> Values.val0 -> GenMem.mem1
144    Types.option **)
145let 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.mem1 -> Pointers.pointer -> Bool.bool **)
153let 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
Note: See TracBrowser for help on using the repository browser.