1 | (* Front-end related includes *) |
---|
2 | include "Clight/label.ma". |
---|
3 | include "Clight/SimplifyCasts.ma". |
---|
4 | include "Clight/switchRemoval.ma". |
---|
5 | include "Clight/toCminor.ma". |
---|
6 | include "Cminor/toRTLabs.ma". |
---|
7 | include "RTLabs/CostCheck.ma". |
---|
8 | include "RTLabs/CostInj.ma". |
---|
9 | |
---|
10 | (* Back-end related includes *) |
---|
11 | include "RTLabs/RTLabsToRTL.ma". |
---|
12 | include "RTL/RTLToERTL.ma". |
---|
13 | include "ERTL/ERTLToLTL.ma". |
---|
14 | include "LTL/LTLToLIN.ma". |
---|
15 | include "LIN/LINToASM.ma". |
---|
16 | |
---|
17 | (* List of all passes whose outputs can be observed *) |
---|
18 | inductive pass : Type[0] ≝ |
---|
19 | clight_pass: pass |
---|
20 | | clight_switch_removed_pass: pass |
---|
21 | | clight_label_pass: pass |
---|
22 | | clight_simplified_pass: pass |
---|
23 | | cminor_pass: pass |
---|
24 | | rtlabs_pass: pass |
---|
25 | | rtl_separate_pass: pass |
---|
26 | | rtl_uniq_pass: pass |
---|
27 | | ertl_pass: pass |
---|
28 | | ltl_pass: pass |
---|
29 | | lin_pass: pass |
---|
30 | | assembly_pass: pass |
---|
31 | | object_code_pass: pass. |
---|
32 | |
---|
33 | definition with_stack_model : Type[0] → Type[0] ≝ |
---|
34 | λA:Type[0].A × (ident → option ℕ). |
---|
35 | |
---|
36 | definition syntax_of_pass : pass → Type[0] ≝ |
---|
37 | λpass. |
---|
38 | match pass with |
---|
39 | [ clight_pass ⇒ clight_program |
---|
40 | | clight_switch_removed_pass ⇒ clight_program |
---|
41 | | clight_label_pass ⇒ clight_program |
---|
42 | | clight_simplified_pass ⇒ clight_program |
---|
43 | | cminor_pass ⇒ Cminor_program |
---|
44 | | rtlabs_pass ⇒ RTLabs_program |
---|
45 | | rtl_separate_pass ⇒ with_stack_model rtl_program |
---|
46 | | rtl_uniq_pass ⇒ with_stack_model rtl_program |
---|
47 | | ertl_pass ⇒ with_stack_model ertl_program |
---|
48 | | ltl_pass ⇒ with_stack_model ltl_program |
---|
49 | | lin_pass ⇒ with_stack_model lin_program |
---|
50 | | assembly_pass ⇒ |
---|
51 | pseudo_assembly_program × (Word → Word) × (Word → bool) |
---|
52 | | object_code_pass ⇒ labelled_object_code ]. |
---|
53 | |
---|
54 | definition observe_pass ≝ ∀pass. syntax_of_pass pass → unit. |
---|
55 | |
---|
56 | (* The compiler front-end *) |
---|
57 | definition front_end : |
---|
58 | observe_pass → clight_program → res (costlabel × clight_program × RTLabs_program) ≝ |
---|
59 | λobserve,p. |
---|
60 | let i ≝ observe clight_pass p in |
---|
61 | let p ≝ program_switch_removal p in |
---|
62 | let i ≝ observe clight_switch_removed_pass p in |
---|
63 | let 〈p',init_cost〉 ≝ clight_label p in |
---|
64 | let i ≝ observe clight_label_pass p' in |
---|
65 | let p ≝ simplify_program p' in |
---|
66 | let i ≝ observe clight_simplified_pass p in |
---|
67 | ! p ← clight_to_cminor p; |
---|
68 | let i ≝ observe cminor_pass p in |
---|
69 | let p ≝ cminor_to_rtlabs p in |
---|
70 | let i ≝ observe rtlabs_pass p in |
---|
71 | ! WCL ← check_cost_program_prf p; |
---|
72 | ! INJ ← check_program_cost_injectivity_prf p; |
---|
73 | return 〈init_cost,p',p〉. |
---|
74 | |
---|
75 | (* The compiler back-end *) |
---|
76 | include "ERTL/uses.ma". (* Included by the untrusted code *) |
---|
77 | axiom compute_fixpoint : fixpoint_computer. |
---|
78 | axiom colour_graph : coloured_graph_computer. |
---|
79 | |
---|
80 | include "common/AssocList.ma". |
---|
81 | |
---|
82 | (* Inefficient, replace with Trie lookup *) |
---|
83 | definition lookup_stack_cost ≝ |
---|
84 | λP,p,id. |
---|
85 | assoc_list_lookup ?? id (eq_identifier …) (stack_cost P p). |
---|
86 | |
---|
87 | definition back_end : |
---|
88 | observe_pass → costlabel → RTLabs_program → |
---|
89 | res (pseudo_assembly_program × costlabel × stack_cost_model × nat) ≝ |
---|
90 | λobserve,init_cost,p. |
---|
91 | let p ≝ rtlabs_to_rtl init_cost p in |
---|
92 | let st ≝ lookup_stack_cost … p in |
---|
93 | let i ≝ observe rtl_separate_pass 〈p,st〉 in |
---|
94 | let i ≝ observe rtl_uniq_pass 〈p,st〉 in |
---|
95 | let p ≝ rtl_to_ertl p in |
---|
96 | let st ≝ lookup_stack_cost … p in |
---|
97 | let i ≝ observe ertl_pass 〈p,st〉 in |
---|
98 | let 〈p,stack_cost,max_stack〉 ≝ ertl_to_ltl compute_fixpoint colour_graph p in |
---|
99 | (* The two stack models are the same *) |
---|
100 | let st ≝ lookup_stack_cost … p in |
---|
101 | let i ≝ observe ltl_pass 〈p,st〉 in |
---|
102 | let st ≝ lookup_stack_cost … p in |
---|
103 | let p ≝ ltl_to_lin p in |
---|
104 | let st ≝ lookup_stack_cost … p in |
---|
105 | let i ≝ observe lin_pass 〈p,st〉 in |
---|
106 | ! p ← opt_to_res ? (msg AssemblyTooLarge) (lin_to_asm p) ; |
---|
107 | return 〈〈p,init_cost〉,stack_cost,max_stack〉. |
---|
108 | |
---|
109 | (* The assembler *) |
---|
110 | include "ASM/Policy.ma". |
---|
111 | |
---|
112 | definition assembler : |
---|
113 | observe_pass → pseudo_assembly_program → res labelled_object_code ≝ |
---|
114 | λobserve,p. |
---|
115 | ! sigma_pol ← opt_to_res ? (msg Jump_expansion_failed) (jump_expansion' p); |
---|
116 | let sigma ≝ λppc. \fst sigma_pol ppc in |
---|
117 | let pol ≝ λppc. \snd sigma_pol ppc in |
---|
118 | let i ≝ observe assembly_pass 〈p,sigma,pol〉 in |
---|
119 | let p ≝ assembly p sigma pol in |
---|
120 | let i ≝ observe object_code_pass p in |
---|
121 | OK ? p. |
---|
122 | |
---|
123 | (* Cost lifting *) |
---|
124 | include "ASM/ASMCosts.ma". |
---|
125 | |
---|
126 | definition lift_out_of_sigma : |
---|
127 | ∀A,B : Type[0].∀P_out : A → Prop.B → |
---|
128 | (∀a.P_out a + ¬ P_out a) → |
---|
129 | ((Σa.P_out a) → B) → A → B ≝ λA,B,P_out,dflt,dec,m,a_sig. |
---|
130 | match dec a_sig with |
---|
131 | [ inl prf ⇒ m «a_sig, prf» |
---|
132 | | inr _ ⇒ dflt (* labels not present in out code get 0 *) |
---|
133 | ]. |
---|
134 | |
---|
135 | definition lift_cost_map_back_to_front : |
---|
136 | ∀oc. |
---|
137 | let abstat ≝ OC_abstract_status oc in |
---|
138 | as_cost_map abstat → clight_cost_map ≝ |
---|
139 | λoc,asm_cost_map. |
---|
140 | lift_out_of_sigma … 0 (* labels not present in out code get 0 *) |
---|
141 | (strong_decidable_in_codomain …) asm_cost_map. |
---|
142 | |
---|
143 | (* Cost model computation *) |
---|
144 | include "ASM/ASMCostsSplit.ma". |
---|
145 | |
---|
146 | record compiler_output : Type[0] ≝ |
---|
147 | { c_labelled_object_code: labelled_object_code |
---|
148 | ; c_stack_cost: stack_cost_model |
---|
149 | ; c_max_stack: nat |
---|
150 | ; c_init_costlabel: costlabel |
---|
151 | ; c_labelled_clight: clight_program |
---|
152 | ; c_clight_cost_map: clight_cost_map |
---|
153 | }. |
---|
154 | |
---|
155 | definition compile : observe_pass → clight_program → res compiler_output ≝ |
---|
156 | λobserve,p. |
---|
157 | ! 〈init_cost,p',p〉 ← front_end observe p; |
---|
158 | ! 〈p_init_costlabel,stack_cost,max_stack〉 ← back_end observe init_cost p; |
---|
159 | let 〈p,init_costlabel〉 ≝ p_init_costlabel in |
---|
160 | ! p ← assembler observe p; |
---|
161 | let k ≝ ASM_cost_map p in |
---|
162 | let k' ≝ |
---|
163 | lift_cost_map_back_to_front p k in |
---|
164 | return mk_compiler_output p stack_cost max_stack init_costlabel p' k'. |
---|