source: extracted/compiler.ml @ 2743

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

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

File size: 5.7 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
165open Deqsets_extra
166
167open CostMisc
168
169open Listb_extra
170
171open CostSpec
172
173open CostCheck
174
175open Executions
176
177open StructuredTraces
178
179open RTLabs_semantics
180
181open RTLabs_abstract
182
183open RTLabs_traces
184
185open CostInj
186
187(** val front_end :
188    Csyntax.clight_program -> ((CostLabel.costlabel, Csyntax.clight_program)
189    Types.prod, RTLabs_syntax.rTLabs_program) Types.prod Errors.res **)
190let front_end p =
191  let p0 = SwitchRemoval.program_switch_removal p in
192  let { Types.fst = p'; Types.snd = init_cost } = Label.clight_label p0 in
193  let p3 = SimplifyCasts.simplify_program p' in
194  Obj.magic
195    (Monad.m_bind0 (Monad.max_def Errors.res0)
196      (Obj.magic (ToCminor.clight_to_cminor p3)) (fun p4 ->
197      let p5 = ToRTLabs.cminor_to_rtlabs init_cost p4 in
198      (match CostCheck.check_cost_program p5 with
199       | Bool.True ->
200         (match CostInj.check_program_cost_injectivity p5 with
201          | Bool.True ->
202            Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
203              { Types.fst = init_cost; Types.snd = p' }; Types.snd = p5 }
204          | Bool.False ->
205            Obj.magic (Errors.Error
206              (Errors.msg ErrorMessages.RepeatedCostLabel)))
207       | Bool.False ->
208         Obj.magic (Errors.Error (Errors.msg ErrorMessages.BadCostLabelling)))))
209
210open State
211
212open Bind_new
213
214open BindLists
215
216open Blocks
217
218open TranslateUtils
219
220open AssocList
221
222open String
223
224open LabelledObjects
225
226open I8051
227
228open BackEndOps
229
230open Joint
231
232open RTL
233
234open RTLabsToRTL
235
236open ERTL
237
238open RegisterSet
239
240open RTLToERTL
241
242open ERTLptr
243
244open ERTLToERTLptr
245
246open Fixpoints
247
248open Set_adt
249
250open Liveness
251
252open Interference
253
254open Joint_LTL_LIN
255
256open LTL
257
258open ERTLptrToLTL
259
260open LIN
261
262open Linearise
263
264open LTLToLIN
265
266open ASM
267
268open BitVectorTrieSet
269
270open LINToASM
271
272(** val compute_fixpoint : Fixpoints.fixpoint_computer **)
273let compute_fixpoint = Compute_fixpoints.compute_fixpoint
274
275(** val colour_graph : Interference.coloured_graph_computer **)
276let colour_graph = Compute_colouring.colour_graph
277
278(** val back_end :
279    RTLabs_syntax.rTLabs_program -> ASM.pseudo_assembly_program **)
280let back_end p =
281  let p0 = RTLabsToRTL.rtlabs_to_rtl p in
282  let p3 = RTLToERTL.rtl_to_ertl p0 in
283  let p4 = ERTLToERTLptr.ertl_to_ertlptr p3 in
284  let p5 = ERTLptrToLTL.ertlptr_to_ltl compute_fixpoint colour_graph p4 in
285  let p6 = LTLToLIN.ltl_to_lin p5 in LINToASM.lin_to_asm p6
286
287type object_code = BitVector.byte List.list
288
289type costlabel_map1 = CostLabel.costlabel BitVectorTrie.bitVectorTrie
290
291open Assembly
292
293open Status
294
295open Fetch
296
297open PolicyFront
298
299open PolicyStep
300
301open Policy
302
303(** val assembler :
304    ASM.pseudo_assembly_program -> (object_code, costlabel_map1) Types.prod
305    Errors.res **)
306let assembler p =
307  let { Types.fst = preamble0; Types.snd = list_instr } = p in
308  let p' = { Types.fst = preamble0; Types.snd = list_instr } in
309  Obj.magic
310    (Monad.m_bind0 (Monad.max_def Errors.res0)
311      (Obj.magic
312        (Errors.opt_to_res (Errors.msg ErrorMessages.Jump_expansion_failed)
313          (Policy.jump_expansion' (Types.coerc_pair_sigma p'))))
314      (fun sigma_pol ->
315      let sigma0 = fun ppc -> (Types.pi1 sigma_pol).Types.fst ppc in
316      let pol = fun ppc -> (Types.pi1 sigma_pol).Types.snd ppc in
317      Obj.magic (Errors.OK (Types.pi1 (Assembly.assembly p sigma0 pol)))))
318
319open AbstractStatus
320
321open StatusProofs
322
323open Interpret
324
325open ASMCosts
326
327(** val lift_cost_map_back_to_front :
328    Csyntax.clight_program -> BitVector.byte BitVectorTrie.bitVectorTrie ->
329    CostLabel.costlabel BitVectorTrie.bitVectorTrie -> (CostLabel.costlabel
330    -> (__, __) Types.sum) -> StructuredTraces.as_cost_map ->
331    Label.clight_cost_map **)
332let lift_cost_map_back_to_front clight code_memory lbls dec k asm_cost_map =
333  StructuredTraces.lift_sigma_map_id Nat.O dec k asm_cost_map
334
335open UtilBranch
336
337open ASMCostsSplit
338
339(** val compile :
340    Csyntax.clight_program -> ((object_code, costlabel_map1) Types.prod,
341    (Csyntax.clight_program, Label.clight_cost_map) Types.dPair) Types.prod
342    Errors.res **)
343let compile p =
344  Obj.magic
345    (Monad.m_bind3 (Monad.max_def Errors.res0) (Obj.magic (front_end p))
346      (fun init_cost p' p0 ->
347      let p3 = back_end p0 in
348      Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (assembler p3))
349        (fun p4 ->
350        let k = ASMCostsSplit.aSM_cost_map p4 in
351        let k' =
352          lift_cost_map_back_to_front p'
353            (Fetch.load_code_memory p4.Types.fst) p4.Types.snd (assert false
354            (* absurd case *)) k
355        in
356        Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = p4;
357          Types.snd = { Types.dpi1 = p'; Types.dpi2 = k' } })))
358
Note: See TracBrowser for help on using the repository browser.