source: extracted/memoryInjections.ml @ 2601

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