source: extracted/compiler.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: 5.2 KB
Line 
1open Preamble
2
3open BitVectorTrie
4
5open CostLabel
6
7open Coqlib
8
9open Proper
10
11open PositiveMap
12
13open Deqsets
14
15open ErrorMessages
16
17open PreIdentifiers
18
19open Errors
20
21open Extralib
22
23open Setoids
24
25open Monad
26
27open Option
28
29open Lists
30
31open Positive
32
33open Identifiers
34
35open Exp
36
37open Arithmetic
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 Graphs
156
157open Order
158
159open Registers
160
161open RTLabs_syntax
162
163open ToRTLabs
164
165(** val front_end :
166    Csyntax.clight_program -> ((CostLabel.costlabel, Csyntax.clight_program)
167    Types.prod, RTLabs_syntax.rTLabs_program) Types.prod Errors.res **)
168let front_end p =
169  let p0 = SwitchRemoval.program_switch_removal p in
170  let { Types.fst = p'; Types.snd = init_cost } = Label.clight_label p0 in
171  let p3 = SimplifyCasts.simplify_program p' in
172  Obj.magic
173    (Monad.m_bind0 (Monad.max_def Errors.res0)
174      (Obj.magic (ToCminor.clight_to_cminor p3)) (fun p4 ->
175      let p5 = ToRTLabs.cminor_to_rtlabs init_cost p4 in
176      Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = { Types.fst =
177        init_cost; Types.snd = p' }; Types.snd = p5 }))
178
179open Deqsets
180
181open State
182
183open Bind_new
184
185open BindLists
186
187open Blocks
188
189open TranslateUtils
190
191open AssocList
192
193open String
194
195open LabelledObjects
196
197open I8051
198
199open BackEndOps
200
201open Joint
202
203open RTL
204
205open RTLabsToRTL
206
207open ERTL
208
209open RegisterSet
210
211open RTLToERTL
212
213open ERTLptr
214
215open ERTLToERTLptr
216
217open Fixpoints
218
219open Set_adt
220
221open Liveness
222
223open Interference
224
225open Joint_LTL_LIN
226
227open LTL
228
229open ERTLptrToLTL
230
231open LIN
232
233open Linearise
234
235open LTLToLIN
236
237open ASM
238
239open BitVectorTrieSet
240
241open LINToASM
242
243(** val compute_fixpoint : Fixpoints.fixpoint_computer **)
244let compute_fixpoint _ =
245  failwith "AXIOM TO BE REALIZED"
246
247(** val colour_graph : Interference.coloured_graph_computer **)
248let colour_graph _ =
249  failwith "AXIOM TO BE REALIZED"
250
251(** val back_end :
252    RTLabs_syntax.rTLabs_program -> ASM.pseudo_assembly_program **)
253let back_end p =
254  let p0 = RTLabsToRTL.rtlabs_to_rtl p in
255  let p3 = RTLToERTL.rtl_to_ertl p0 in
256  let p4 = ERTLToERTLptr.ertl_to_ertlptr p3 in
257  let p5 = ERTLptrToLTL.ertlptr_to_ltl compute_fixpoint colour_graph p4 in
258  let p6 = LTLToLIN.ltl_to_lin p5 in LINToASM.lin_to_asm p6
259
260type object_code = BitVector.byte List.list
261
262type costlabel_map1 = CostLabel.costlabel BitVectorTrie.bitVectorTrie
263
264open Assembly
265
266open Status
267
268open Fetch
269
270open PolicyFront
271
272open PolicyStep
273
274open Policy
275
276(** val assembler :
277    ASM.pseudo_assembly_program -> (object_code, costlabel_map1) Types.prod
278    Errors.res **)
279let assembler p =
280  let { Types.fst = preamble0; Types.snd = list_instr } = p in
281  let p' = { Types.fst = preamble0; Types.snd = list_instr } in
282  Obj.magic
283    (Monad.m_bind0 (Monad.max_def Errors.res0)
284      (Obj.magic
285        (Errors.opt_to_res (Errors.msg ErrorMessages.Jump_expansion_failed)
286          (Policy.jump_expansion' (Types.coerc_pair_sigma p'))))
287      (fun sigma_pol ->
288      let sigma0 = fun ppc -> (Types.pi1 sigma_pol).Types.fst ppc in
289      let pol = fun ppc -> (Types.pi1 sigma_pol).Types.snd ppc in
290      Obj.magic (Errors.OK (Types.pi1 (Assembly.assembly p sigma0 pol)))))
291
292open StructuredTraces
293
294open AbstractStatus
295
296open StatusProofs
297
298open Interpret
299
300open ASMCosts
301
302(** val lift_cost_map_back_to_front :
303    Csyntax.clight_program -> BitVector.byte BitVectorTrie.bitVectorTrie ->
304    CostLabel.costlabel BitVectorTrie.bitVectorTrie -> (CostLabel.costlabel
305    -> (__, __) Types.sum) -> StructuredTraces.as_cost_map ->
306    Label.clight_cost_map **)
307let lift_cost_map_back_to_front clight code_memory lbls dec k asm_cost_map =
308  StructuredTraces.lift_sigma_map_id Nat.O dec k asm_cost_map
309
310open UtilBranch
311
312open ASMCostsSplit
313
314(** val compile :
315    Csyntax.clight_program -> ((object_code, costlabel_map1) Types.prod,
316    (Csyntax.clight_program, Label.clight_cost_map) Types.dPair) Types.prod
317    Errors.res **)
318let compile p =
319  Obj.magic
320    (Monad.m_bind3 (Monad.max_def Errors.res0) (Obj.magic (front_end p))
321      (fun init_cost p' p0 ->
322      let p3 = back_end p0 in
323      Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (assembler p3))
324        (fun p4 ->
325        let k = ASMCostsSplit.aSM_cost_map p4 in
326        let k' =
327          lift_cost_map_back_to_front p'
328            (Fetch.load_code_memory p4.Types.fst) p4.Types.snd (assert false
329            (* absurd case *)) k
330        in
331        Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = p4;
332          Types.snd = { Types.dpi1 = p'; Types.dpi2 = k' } })))
333
Note: See TracBrowser for help on using the repository browser.