1 | |
---|
2 | include "Clight/label.ma". |
---|
3 | include "Clight/SimplifyCasts.ma". |
---|
4 | include "Clight/switchRemoval.ma". |
---|
5 | include "Clight/toCminor.ma". |
---|
6 | include "Cminor/initialisation.ma". |
---|
7 | include "Cminor/toRTLabs.ma". |
---|
8 | |
---|
9 | definition front_end : clight_program → res (costlabel × clight_program × RTLabs_program) ≝ |
---|
10 | λp. |
---|
11 | let p ≝ program_switch_removal p in |
---|
12 | let 〈p',init_cost〉 ≝ clight_label p in |
---|
13 | let p ≝ simplify_program p' in |
---|
14 | ! p ← clight_to_cminor p; |
---|
15 | let p ≝ cminor_to_rtlabs init_cost p in |
---|
16 | return 〈init_cost,p',p〉. |
---|
17 | |
---|
18 | (* Recent changes have temporarily stopped the back-end from checking, so |
---|
19 | axiomatise it for a little while. |
---|
20 | include "RTLabs/RTLabsToRTL.ma". |
---|
21 | include "RTL/RTLToERTL.ma". |
---|
22 | include "ERTL/ERTLToLTL.ma". |
---|
23 | include "LTL/LTLToLIN.ma". |
---|
24 | include "LIN/LINToASM.ma". |
---|
25 | |
---|
26 | (* these are already defined in utilities/fixpoint.ma and ERTL/Interference.ma |
---|
27 | axiom the_fixpoint : fixpoint. |
---|
28 | axiom build : ∀valuation. coloured_graph valuation. |
---|
29 | *) |
---|
30 | definition back_end : RTLabs_program → pseudo_assembly_program ≝ |
---|
31 | λp. |
---|
32 | let p ≝ rtlabs_to_rtl p in |
---|
33 | let p ≝ rtl_to_ertl p in |
---|
34 | let p ≝ ertl_to_ltl p in (* TODO: abstract over colouring *) |
---|
35 | let p ≝ ltl_to_lin p in |
---|
36 | lin_to_asm p. |
---|
37 | *) |
---|
38 | include "ASM/ASM.ma". |
---|
39 | axiom back_end : RTLabs_program → pseudo_assembly_program. |
---|
40 | |
---|
41 | include "ASM/Assembly.ma". |
---|
42 | |
---|
43 | include "ASM/Policy.ma". |
---|
44 | |
---|
45 | axiom Jump_expansion_failed : String. |
---|
46 | |
---|
47 | include "ASM/ASMCostsSplit.ma". |
---|
48 | |
---|
49 | axiom assembler : pseudo_assembly_program → res (object_code × costlabel_map). (* |
---|
50 | definition assembler : pseudo_assembly_program → res (object_code × costlabel_map) ≝ |
---|
51 | λp. |
---|
52 | let 〈preamble, list_instr〉 ≝ p in |
---|
53 | (* TODO: fail if p is too large. *) |
---|
54 | let p' ≝ 〈preamble, list_instr〉 in |
---|
55 | ! sigma_pol ← opt_to_res ? (msg Jump_expansion_failed) (jump_expansion' p'); |
---|
56 | let sigma ≝ λppc. \fst (sigma_pol ppc) in |
---|
57 | let pol ≝ λppc. \snd (sigma_pol ppc) in |
---|
58 | OK ? (assembly p sigma pol). |
---|
59 | cases daemon |
---|
60 | qed.*) |
---|
61 | |
---|
62 | include "RTLabs/semantics.ma". |
---|
63 | |
---|
64 | include "joint/Traces.ma". |
---|
65 | |
---|
66 | include "ASM/Fetch.ma". (* For load_code_memory only *) |
---|
67 | |
---|
68 | definition lift_cost_map_back_to_front : |
---|
69 | ∀clight, code_memory, lbls. |
---|
70 | (∀l. (∃pc.as_label_of_pc (ASM_abstract_status code_memory lbls) pc = Some … l) + |
---|
71 | ¬(∃pc.as_label_of_pc (ASM_abstract_status code_memory lbls) pc = Some … l)) → |
---|
72 | as_cost_map (ASM_abstract_status code_memory lbls) → |
---|
73 | (Σl : costlabel.in_clight_program clight l) → ℕ ≝ λclight,code_memory,lbls,dec,k,l_sig. |
---|
74 | match dec l_sig with |
---|
75 | [ inl prf ⇒ k «l_sig, prf» |
---|
76 | | inr _ ⇒ 0 (* labels not present in out code get 0 *) |
---|
77 | ]. |
---|
78 | |
---|
79 | definition compile : clight_program → |
---|
80 | res (object_code × costlabel_map × (𝚺labelled:clight_program. ((Σl.in_clight_program labelled l) → ℕ))) ≝ |
---|
81 | λp. |
---|
82 | ! 〈init_cost,p',p〉 ← front_end p; |
---|
83 | let p ≝ back_end p in |
---|
84 | ! p ← assembler p; |
---|
85 | let k ≝ ASM_cost_map p ? in |
---|
86 | let k' ≝ lift_cost_map_back_to_front |
---|
87 | p' |
---|
88 | (load_code_memory (\fst p)) |
---|
89 | (\snd p) |
---|
90 | ? k |
---|
91 | in |
---|
92 | return 〈p, ❬p', k'❭〉. |
---|
93 | cases daemon |
---|
94 | qed. |
---|
95 | |
---|