source: extracted/frontEndMem.ml @ 2601

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

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

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