source: extracted/compiler.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.7 KB
Line 
1open Preamble
2
3open CostLabel
4
5open Proper
6
7open PositiveMap
8
9open Deqsets
10
11open PreIdentifiers
12
13open Errors
14
15open Extralib
16
17open Setoids
18
19open Monad
20
21open Option
22
23open Lists
24
25open Positive
26
27open Identifiers
28
29open Coqlib
30
31open Floats
32
33open Arithmetic
34
35open Char
36
37open String
38
39open Vector
40
41open Div_and_mod
42
43open Jmeq
44
45open Russell
46
47open List
48
49open Util
50
51open FoldStuff
52
53open BitVector
54
55open Extranat
56
57open Bool
58
59open Relations
60
61open Nat
62
63open Integers
64
65open Hints_declaration
66
67open Core_notation
68
69open Pts
70
71open Logic
72
73open Types
74
75open AST
76
77open Csyntax
78
79open Label
80
81open Sets
82
83open Listb
84
85open Star
86
87open Frontend_misc
88
89open CexecInd
90
91open CexecSound
92
93open Casts
94
95open ClassifyOp
96
97open Smallstep
98
99open Extra_bool
100
101open FrontEndVal
102
103open Hide
104
105open ByteValues
106
107open GenMem
108
109open FrontEndMem
110
111open Globalenvs
112
113open Csem
114
115open SmallstepExec
116
117open Division
118
119open Z
120
121open BitVectorZ
122
123open Pointers
124
125open Values
126
127open Events
128
129open IOMonad
130
131open IO
132
133open Cexec
134
135open TypeComparison
136
137open SimplifyCasts
138
139open MemProperties
140
141open MemoryInjections
142
143open Fresh
144
145open SwitchRemoval
146
147open FrontEndOps
148
149open Cminor_syntax
150
151open ToCminor
152
153open Initialisation
154
155open BitVectorTrie
156
157open Graphs
158
159open Order
160
161open Registers
162
163open RTLabs_syntax
164
165open ToRTLabs
166
167(** val front_end :
168    Csyntax.clight_program -> ((CostLabel.costlabel, Csyntax.clight_program)
169    Types.prod, RTLabs_syntax.rTLabs_program) Types.prod Errors.res **)
170let front_end p =
171  let p0 = SwitchRemoval.program_switch_removal p in
172  let { Types.fst = p'; Types.snd = init_cost } = Label.clight_label p0 in
173  let p3 = SimplifyCasts.simplify_program p' in
174  Obj.magic
175    (Monad.m_bind0 (Monad.max_def Errors.res0)
176      (Obj.magic (ToCminor.clight_to_cminor p3)) (fun p4 ->
177      let p5 = ToRTLabs.cminor_to_rtlabs init_cost p4 in
178      Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = { Types.fst =
179        init_cost; Types.snd = p' }; Types.snd = p5 }))
180
181open LabelledObjects
182
183open ASM
184
185(** val back_end :
186    RTLabs_syntax.rTLabs_program -> ASM.pseudo_assembly_program **)
187let back_end =
188  failwith "AXIOM TO BE REALIZED"
189
190type object_code = BitVector.byte List.list
191
192type costlabel_map = CostLabel.costlabel BitVectorTrie.bitVectorTrie
193
194(** val assembler :
195    ASM.pseudo_assembly_program -> (object_code, costlabel_map) Types.prod
196    Errors.res **)
197let assembler =
198  failwith "AXIOM TO BE REALIZED"
199
200open StructuredTraces
201
202open AbstractStatus
203
204open Status
205
206open StatusProofs
207
208open Interpret
209
210open Fetch
211
212open ASMCosts
213
214(** val lift_cost_map_back_to_front :
215    Csyntax.clight_program -> BitVector.byte BitVectorTrie.bitVectorTrie ->
216    CostLabel.costlabel BitVectorTrie.bitVectorTrie -> (CostLabel.costlabel
217    -> (__, __) Types.sum) -> StructuredTraces.as_cost_map ->
218    Label.clight_cost_map **)
219let lift_cost_map_back_to_front clight code_memory lbls dec k asm_cost_map =
220  StructuredTraces.lift_sigma_map_id Nat.O dec k asm_cost_map
221
222open UtilBranch
223
224open ASMCostsSplit
225
226(** val compile :
227    Csyntax.clight_program -> ((object_code, costlabel_map) Types.prod,
228    (Csyntax.clight_program, Label.clight_cost_map) Types.dPair) Types.prod
229    Errors.res **)
230let compile p =
231  Obj.magic
232    (Monad.m_bind3 (Monad.max_def Errors.res0) (Obj.magic (front_end p))
233      (fun init_cost p' p0 ->
234      let p3 = back_end p0 in
235      Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (assembler p3))
236        (fun p4 ->
237        let k = ASMCostsSplit.aSM_cost_map p4 in
238        let k' =
239          lift_cost_map_back_to_front p'
240            (Fetch.load_code_memory p4.Types.fst) p4.Types.snd (assert false
241            (* absurd case *)) k
242        in
243        Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = p4;
244          Types.snd = { Types.dpi1 = p'; Types.dpi2 = k' } })))
245
Note: See TracBrowser for help on using the repository browser.