source: extracted/compiler.ml @ 2773

Last change on this file since 2773 was 2773, checked in by sacerdot, 7 years ago
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File size: 5.7 KB
Line 
1open Preamble
2
3open CostLabel
4
5open Coqlib
6
7open Proper
8
9open PositiveMap
10
11open Deqsets
12
13open ErrorMessages
14
15open PreIdentifiers
16
17open Errors
18
19open Extralib
20
21open Lists
22
23open Positive
24
25open Identifiers
26
27open Exp
28
29open Arithmetic
30
31open Vector
32
33open Div_and_mod
34
35open Util
36
37open FoldStuff
38
39open BitVector
40
41open Jmeq
42
43open Russell
44
45open List
46
47open Setoids
48
49open Monad
50
51open Option
52
53open Extranat
54
55open Bool
56
57open Relations
58
59open Nat
60
61open Integers
62
63open Hints_declaration
64
65open Core_notation
66
67open Pts
68
69open Logic
70
71open Types
72
73open AST
74
75open Csyntax
76
77open Label
78
79open Sets
80
81open Listb
82
83open Star
84
85open Frontend_misc
86
87open CexecInd
88
89open CexecSound
90
91open Casts
92
93open ClassifyOp
94
95open Smallstep
96
97open Extra_bool
98
99open FrontEndVal
100
101open Hide
102
103open ByteValues
104
105open GenMem
106
107open FrontEndMem
108
109open Globalenvs
110
111open Csem
112
113open SmallstepExec
114
115open Division
116
117open Z
118
119open BitVectorZ
120
121open Pointers
122
123open Values
124
125open Events
126
127open IOMonad
128
129open IO
130
131open Cexec
132
133open TypeComparison
134
135open SimplifyCasts
136
137open MemProperties
138
139open MemoryInjections
140
141open Fresh
142
143open SwitchRemoval
144
145open FrontEndOps
146
147open Cminor_syntax
148
149open ToCminor
150
151open Initialisation
152
153open BitVectorTrie
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 p1 = SimplifyCasts.simplify_program p' in
194  Obj.magic
195    (Monad.m_bind0 (Monad.max_def Errors.res0)
196      (Obj.magic (ToCminor.clight_to_cminor p1)) (fun p2 ->
197      let p3 = ToRTLabs.cminor_to_rtlabs init_cost p2 in
198      (match CostCheck.check_cost_program p3 with
199       | Bool.True ->
200         (match CostInj.check_program_cost_injectivity p3 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 = p3 }
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 Errors.res **)
280let back_end p =
281  let p0 = RTLabsToRTL.rtlabs_to_rtl p in
282  let p1 = RTLToERTL.rtl_to_ertl p0 in
283  let p2 = ERTLToERTLptr.ertl_to_ertlptr p1 in
284  let p3 = ERTLptrToLTL.ertlptr_to_ltl compute_fixpoint colour_graph p2 in
285  let p4 = LTLToLIN.ltl_to_lin p3 in
286  Errors.opt_to_res (Errors.msg ErrorMessages.AssemblyTooLarge)
287    (LINToASM.lin_to_asm p4)
288
289open Assembly
290
291open Status
292
293open Fetch
294
295open PolicyFront
296
297open PolicyStep
298
299open Policy
300
301(** val assembler :
302    ASM.pseudo_assembly_program -> ASM.labelled_object_code Errors.res **)
303let assembler p =
304  Obj.magic
305    (Monad.m_bind0 (Monad.max_def Errors.res0)
306      (Obj.magic
307        (Errors.opt_to_res (Errors.msg ErrorMessages.Jump_expansion_failed)
308          (Policy.jump_expansion' p))) (fun sigma_pol ->
309      let sigma = fun ppc -> (Types.pi1 sigma_pol).Types.fst ppc in
310      let pol = fun ppc -> (Types.pi1 sigma_pol).Types.snd ppc in
311      Obj.magic (Errors.OK (Types.pi1 (Assembly.assembly p sigma pol)))))
312
313open AbstractStatus
314
315open StatusProofs
316
317open Interpret
318
319open ASMCosts
320
321(** val lift_cost_map_back_to_front :
322    Csyntax.clight_program -> BitVector.byte BitVectorTrie.bitVectorTrie ->
323    CostLabel.costlabel BitVectorTrie.bitVectorTrie ->
324    StructuredTraces.as_cost_map -> Label.clight_cost_map **)
325let lift_cost_map_back_to_front clight code_memory lbls k asm_cost_map =
326  StructuredTraces.lift_sigma_map_id Nat.O
327    (BitVectorTrie.strong_decidable_in_codomain
328      (Identifiers.deq_identifier PreIdentifiers.CostTag) (Nat.S (Nat.S
329      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
330      (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))) (Obj.magic lbls))
331    (Obj.magic k) (Obj.magic asm_cost_map)
332
333open UtilBranch
334
335open ASMCostsSplit
336
337(** val compile :
338    Csyntax.clight_program -> (ASM.labelled_object_code,
339    (Csyntax.clight_program, Label.clight_cost_map) Types.dPair) Types.prod
340    Errors.res **)
341let compile p =
342  Obj.magic
343    (Monad.m_bind3 (Monad.max_def Errors.res0) (Obj.magic (front_end p))
344      (fun init_cost p' p0 ->
345      Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (back_end p0))
346        (fun p1 ->
347        Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (assembler p1))
348          (fun p2 ->
349          let k = ASMCostsSplit.aSM_cost_map p2 in
350          let k' =
351            lift_cost_map_back_to_front p' (Fetch.load_code_memory p2.ASM.oc)
352              p2.ASM.costlabels k
353          in
354          Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = p2;
355            Types.snd = { Types.dpi1 = p'; Types.dpi2 = k' } }))))
356
Note: See TracBrowser for help on using the repository browser.