| 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 | (* |
|---|
| 19 | include "RTLabs/RTLabsToRTL.ma". |
|---|
| 20 | include "RTL/RTLToERTL.ma". |
|---|
| 21 | include "ERTL/ERTLToLTL.ma". |
|---|
| 22 | include "LTL/LTLToLIN.ma". |
|---|
| 23 | include "LIN/LINToASM.ma". |
|---|
| 24 | |
|---|
| 25 | (* these are already defined in utilities/fixpoint.ma and ERTL/Interference.ma |
|---|
| 26 | axiom the_fixpoint : fixpoint. |
|---|
| 27 | axiom build : ∀valuation. coloured_graph valuation. |
|---|
| 28 | *) |
|---|
| 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 | (* JHM: minimum needed for assembler axiom to typecheck *) |
|---|
| 42 | (* JHM: moved from ASMCostsSplit.ma *) |
|---|
| 43 | (* JHM: should move elsewhere in ASM/ *) |
|---|
| 44 | definition object_code ≝ list Byte. |
|---|
| 45 | definition costlabel_map ≝ BitVectorTrie costlabel 16. |
|---|
| 46 | |
|---|
| 47 | axiom assembler : pseudo_assembly_program → res (object_code × costlabel_map). |
|---|
| 48 | |
|---|
| 49 | (* include "ASM/Policy.ma". |
|---|
| 50 | |
|---|
| 51 | axiom Jump_expansion_failed : String. |
|---|
| 52 | |
|---|
| 53 | definition assembler : pseudo_assembly_program → res (object_code × costlabel_map) ≝ |
|---|
| 54 | λp. |
|---|
| 55 | let 〈preamble, list_instr〉 ≝ p in |
|---|
| 56 | (* TODO: fail if p is too large. *) |
|---|
| 57 | let p' ≝ 〈preamble, list_instr〉 in |
|---|
| 58 | ! sigma_pol ← opt_to_res ? (msg Jump_expansion_failed) (jump_expansion' p'); |
|---|
| 59 | let sigma ≝ λppc. \fst (sigma_pol ppc) in |
|---|
| 60 | let pol ≝ λppc. \snd (sigma_pol ppc) in |
|---|
| 61 | OK ? (assembly p sigma pol). |
|---|
| 62 | cases daemon |
|---|
| 63 | qed. |
|---|
| 64 | *) |
|---|
| 65 | |
|---|
| 66 | include "ASM/ASMCosts.ma". |
|---|
| 67 | |
|---|
| 68 | definition lift_cost_map_back_to_front : |
|---|
| 69 | ∀clight, code_memory, lbls. |
|---|
| 70 | let abstat ≝ ASM_abstract_status code_memory lbls in |
|---|
| 71 | (∀l. (as_cost_labelled abstat l) + ¬(as_cost_labelled abstat l)) → |
|---|
| 72 | as_cost_map abstat → clight_cost_map clight ≝ |
|---|
| 73 | λclight,code_memory,lbls,dec,k,asm_cost_map. |
|---|
| 74 | lift_sigma_map_id … 0 (* labels not present in out code get 0 *) |
|---|
| 75 | dec k asm_cost_map. |
|---|
| 76 | |
|---|
| 77 | include "ASM/ASMCostsSplit.ma". |
|---|
| 78 | |
|---|
| 79 | definition compile : clight_program → |
|---|
| 80 | res (object_code × costlabel_map × (𝚺labelled:clight_program. clight_cost_map labelled)) ≝ |
|---|
| 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. |
|---|
