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