source: extracted/compiler.ml @ 2827

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

Everything extracted again.

File size: 12.8 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.RepeatedCostLabel0)))
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 String
221
222open LabelledObjects
223
224open I8051
225
226open BackEndOps
227
228open Joint
229
230open RTL
231
232open RTLabsToRTL
233
234open ERTL
235
236open RegisterSet
237
238open RTLToERTL
239
240open ERTLptr
241
242open ERTLToERTLptr
243
244open Fixpoints
245
246open Set_adt
247
248open Liveness
249
250open Interference
251
252open Joint_LTL_LIN
253
254open LTL
255
256open ERTLptrToLTL
257
258open LIN
259
260open Linearise
261
262open LTLToLIN
263
264open ASM
265
266open BitVectorTrieSet
267
268open LINToASM
269
270(** val compute_fixpoint : Fixpoints.fixpoint_computer **)
271let compute_fixpoint = Compute_fixpoints.compute_fixpoint
272
273(** val colour_graph : Interference.coloured_graph_computer **)
274let colour_graph = Compute_colouring.colour_graph
275
276(** val back_end :
277    RTLabs_syntax.rTLabs_program -> ((ASM.pseudo_assembly_program,
278    Joint.stack_cost_model) Types.prod, Nat.nat) Types.prod Errors.res **)
279let back_end p =
280  let p0 = RTLabsToRTL.rtlabs_to_rtl p in
281  let p1 = RTLToERTL.rtl_to_ertl p0 in
282  let p2 = ERTLToERTLptr.ertl_to_ertlptr p1 in
283  let { Types.fst = eta29084; Types.snd = max_stack } =
284    ERTLptrToLTL.ertlptr_to_ltl compute_fixpoint colour_graph p2
285  in
286  let { Types.fst = p3; Types.snd = stack_cost } = eta29084 in
287  let p4 = LTLToLIN.ltl_to_lin p3 in
288  Obj.magic
289    (Monad.m_bind0 (Monad.max_def Errors.res0)
290      (Obj.magic
291        (Errors.opt_to_res (Errors.msg ErrorMessages.AssemblyTooLarge)
292          (LINToASM.lin_to_asm p4))) (fun p5 ->
293      Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = { Types.fst =
294        p5; Types.snd = stack_cost }; Types.snd = max_stack }))
295
296open Assembly
297
298open Status
299
300open Fetch
301
302open PolicyFront
303
304open PolicyStep
305
306open Policy
307
308(** val assembler :
309    ASM.pseudo_assembly_program -> ASM.labelled_object_code Errors.res **)
310let assembler p =
311  Obj.magic
312    (Monad.m_bind0 (Monad.max_def Errors.res0)
313      (Obj.magic
314        (Errors.opt_to_res (Errors.msg ErrorMessages.Jump_expansion_failed)
315          (Policy.jump_expansion' p))) (fun sigma_pol ->
316      let sigma = fun ppc -> (Types.pi1 sigma_pol).Types.fst ppc in
317      let pol = fun ppc -> (Types.pi1 sigma_pol).Types.snd ppc in
318      Obj.magic (Errors.OK (Types.pi1 (Assembly.assembly p sigma pol)))))
319
320open AbstractStatus
321
322open StatusProofs
323
324open Interpret
325
326open ASMCosts
327
328(** val lift_cost_map_back_to_front :
329    Csyntax.clight_program -> BitVector.byte BitVectorTrie.bitVectorTrie ->
330    CostLabel.costlabel BitVectorTrie.bitVectorTrie ->
331    StructuredTraces.as_cost_map -> Label.clight_cost_map **)
332let lift_cost_map_back_to_front clight code_memory lbls k asm_cost_map =
333  StructuredTraces.lift_sigma_map_id Nat.O
334    (BitVectorTrie.strong_decidable_in_codomain
335      (Identifiers.deq_identifier PreIdentifiers.CostTag) (Nat.S (Nat.S
336      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
337      (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))) (Obj.magic lbls))
338    (Obj.magic k) (Obj.magic asm_cost_map)
339
340open UtilBranch
341
342open ASMCostsSplit
343
344type compiler_output = { c_labelled_object_code : ASM.labelled_object_code;
345                         c_stack_cost : Joint.stack_cost_model;
346                         c_max_stack : Nat.nat;
347                         c_labelled_clight : Csyntax.clight_program;
348                         c_clight_cost_map : Label.clight_cost_map }
349
350(** val compiler_output_rect_Type4 :
351    (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
352    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
353    compiler_output -> 'a1 **)
354let rec compiler_output_rect_Type4 h_mk_compiler_output x_25025 =
355  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
356    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
357    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_25025
358  in
359  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
360    c_labelled_clight0 c_clight_cost_map0
361
362(** val compiler_output_rect_Type5 :
363    (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
364    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
365    compiler_output -> 'a1 **)
366let rec compiler_output_rect_Type5 h_mk_compiler_output x_25027 =
367  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
368    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
369    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_25027
370  in
371  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
372    c_labelled_clight0 c_clight_cost_map0
373
374(** val compiler_output_rect_Type3 :
375    (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
376    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
377    compiler_output -> 'a1 **)
378let rec compiler_output_rect_Type3 h_mk_compiler_output x_25029 =
379  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
380    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
381    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_25029
382  in
383  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
384    c_labelled_clight0 c_clight_cost_map0
385
386(** val compiler_output_rect_Type2 :
387    (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
388    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
389    compiler_output -> 'a1 **)
390let rec compiler_output_rect_Type2 h_mk_compiler_output x_25031 =
391  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
392    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
393    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_25031
394  in
395  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
396    c_labelled_clight0 c_clight_cost_map0
397
398(** val compiler_output_rect_Type1 :
399    (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
400    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
401    compiler_output -> 'a1 **)
402let rec compiler_output_rect_Type1 h_mk_compiler_output x_25033 =
403  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
404    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
405    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_25033
406  in
407  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
408    c_labelled_clight0 c_clight_cost_map0
409
410(** val compiler_output_rect_Type0 :
411    (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
412    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
413    compiler_output -> 'a1 **)
414let rec compiler_output_rect_Type0 h_mk_compiler_output x_25035 =
415  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
416    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
417    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_25035
418  in
419  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
420    c_labelled_clight0 c_clight_cost_map0
421
422(** val c_labelled_object_code :
423    compiler_output -> ASM.labelled_object_code **)
424let rec c_labelled_object_code xxx =
425  xxx.c_labelled_object_code
426
427(** val c_stack_cost : compiler_output -> Joint.stack_cost_model **)
428let rec c_stack_cost xxx =
429  xxx.c_stack_cost
430
431(** val c_max_stack : compiler_output -> Nat.nat **)
432let rec c_max_stack xxx =
433  xxx.c_max_stack
434
435(** val c_labelled_clight : compiler_output -> Csyntax.clight_program **)
436let rec c_labelled_clight xxx =
437  xxx.c_labelled_clight
438
439(** val c_clight_cost_map : compiler_output -> Label.clight_cost_map **)
440let rec c_clight_cost_map xxx =
441  xxx.c_clight_cost_map
442
443(** val compiler_output_inv_rect_Type4 :
444    compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
445    Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1)
446    -> 'a1 **)
447let compiler_output_inv_rect_Type4 hterm h1 =
448  let hcut = compiler_output_rect_Type4 h1 hterm in hcut __
449
450(** val compiler_output_inv_rect_Type3 :
451    compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
452    Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1)
453    -> 'a1 **)
454let compiler_output_inv_rect_Type3 hterm h1 =
455  let hcut = compiler_output_rect_Type3 h1 hterm in hcut __
456
457(** val compiler_output_inv_rect_Type2 :
458    compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
459    Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1)
460    -> 'a1 **)
461let compiler_output_inv_rect_Type2 hterm h1 =
462  let hcut = compiler_output_rect_Type2 h1 hterm in hcut __
463
464(** val compiler_output_inv_rect_Type1 :
465    compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
466    Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1)
467    -> 'a1 **)
468let compiler_output_inv_rect_Type1 hterm h1 =
469  let hcut = compiler_output_rect_Type1 h1 hterm in hcut __
470
471(** val compiler_output_inv_rect_Type0 :
472    compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
473    Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1)
474    -> 'a1 **)
475let compiler_output_inv_rect_Type0 hterm h1 =
476  let hcut = compiler_output_rect_Type0 h1 hterm in hcut __
477
478(** val compiler_output_discr : compiler_output -> compiler_output -> __ **)
479let compiler_output_discr x y =
480  Logic.eq_rect_Type2 x
481    (let { c_labelled_object_code = a0; c_stack_cost = a1; c_max_stack = a2;
482       c_labelled_clight = a3; c_clight_cost_map = a4 } = x
483     in
484    Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
485
486(** val compiler_output_jmdiscr :
487    compiler_output -> compiler_output -> __ **)
488let compiler_output_jmdiscr x y =
489  Logic.eq_rect_Type2 x
490    (let { c_labelled_object_code = a0; c_stack_cost = a1; c_max_stack = a2;
491       c_labelled_clight = a3; c_clight_cost_map = a4 } = x
492     in
493    Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
494
495(** val compile : Csyntax.clight_program -> compiler_output Errors.res **)
496let compile p =
497  Obj.magic
498    (Monad.m_bind3 (Monad.max_def Errors.res0) (Obj.magic (front_end p))
499      (fun init_cost p' p0 ->
500      Monad.m_bind3 (Monad.max_def Errors.res0) (Obj.magic (back_end p0))
501        (fun p1 stack_cost max_stack ->
502        Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (assembler p1))
503          (fun p2 ->
504          let k = ASMCostsSplit.aSM_cost_map p2 in
505          let k' =
506            lift_cost_map_back_to_front p' (Fetch.load_code_memory p2.ASM.oc)
507              p2.ASM.costlabels k
508          in
509          Monad.m_return0 (Monad.max_def Errors.res0)
510            { c_labelled_object_code = p2; c_stack_cost = stack_cost;
511            c_max_stack = max_stack; c_labelled_clight = p';
512            c_clight_cost_map = k' }))))
513
Note: See TracBrowser for help on using the repository browser.