[1991] | 1 | include "Clight/label.ma". |
---|
[2019] | 2 | include "Clight/SimplifyCasts.ma". |
---|
[2475] | 3 | include "Clight/switchRemoval.ma". |
---|
[1991] | 4 | include "Clight/toCminor.ma". |
---|
| 5 | include "Cminor/initialisation.ma". |
---|
| 6 | include "Cminor/toRTLabs.ma". |
---|
[2724] | 7 | include "RTLabs/CostCheck.ma". |
---|
| 8 | include "RTLabs/CostInj.ma". |
---|
[1991] | 9 | |
---|
[2319] | 10 | definition front_end : clight_program → res (costlabel × clight_program × RTLabs_program) ≝ |
---|
[1991] | 11 | λp. |
---|
[2475] | 12 | let p ≝ program_switch_removal p in |
---|
[2319] | 13 | let 〈p',init_cost〉 ≝ clight_label p in |
---|
[2001] | 14 | let p ≝ simplify_program p' in |
---|
[1991] | 15 | ! p ← clight_to_cminor p; |
---|
[2319] | 16 | let p ≝ cminor_to_rtlabs init_cost p in |
---|
[2724] | 17 | if check_cost_program p then |
---|
| 18 | if check_program_cost_injectivity p then |
---|
| 19 | (return 〈init_cost,p',p〉) |
---|
| 20 | else |
---|
| 21 | (Error ? (msg RepeatedCostLabel)) |
---|
| 22 | else |
---|
| 23 | (Error ? (msg BadCostLabelling)). |
---|
[1995] | 24 | |
---|
[2494] | 25 | include "RTLabs/RTLabsToRTL.ma". |
---|
[1995] | 26 | include "RTL/RTLToERTL.ma". |
---|
[2697] | 27 | include "ERTL/ERTLToERTLptr.ma". |
---|
| 28 | include "ERTLptr/ERTLptrToLTL.ma". |
---|
[2705] | 29 | include "LTL/LTLToLIN.ma". |
---|
[1995] | 30 | include "LIN/LINToASM.ma". |
---|
| 31 | |
---|
[2700] | 32 | axiom compute_fixpoint : fixpoint_computer. |
---|
| 33 | axiom colour_graph : coloured_graph_computer. |
---|
[2505] | 34 | |
---|
[1995] | 35 | definition back_end : RTLabs_program → pseudo_assembly_program ≝ |
---|
| 36 | λp. |
---|
| 37 | let p ≝ rtlabs_to_rtl p in |
---|
| 38 | let p ≝ rtl_to_ertl p in |
---|
[2697] | 39 | let p ≝ ertl_to_ertlptr p in |
---|
[2700] | 40 | let p ≝ ertlptr_to_ltl compute_fixpoint colour_graph p in (* TODO: abstract over colouring *) |
---|
[1995] | 41 | let p ≝ ltl_to_lin p in |
---|
| 42 | lin_to_asm p. |
---|
| 43 | |
---|
[2709] | 44 | (* JHM: minimum needed for assembler to typecheck *) |
---|
| 45 | (* JHM: moved from ASMCostsSplit.ma *) |
---|
| 46 | (* JHM: should move elsewhere in ASM/ *) |
---|
[2512] | 47 | definition object_code ≝ list Byte. |
---|
| 48 | definition costlabel_map ≝ BitVectorTrie costlabel 16. |
---|
[1995] | 49 | |
---|
[2702] | 50 | include "ASM/Policy.ma". |
---|
| 51 | (* Equivalent to the inclusion of ASM/Policy.ma, waiting for that slow |
---|
| 52 | file to compile |
---|
| 53 | include "ASM/PolicyStep.ma". |
---|
| 54 | axiom jump_expansion': ∀program:preamble × (Σl:list labelled_instruction.lt (S (|l|)) 2^16 ∧ is_well_labelled_p l). |
---|
[2700] | 55 | option (Σsigma_policy:(Word → Word) × (Word → bool). |
---|
| 56 | let 〈sigma,policy〉≝ sigma_policy in |
---|
[2702] | 57 | sigma_policy_specification 〈\fst program,\snd program〉 sigma policy). *) |
---|
[2505] | 58 | |
---|
[1995] | 59 | definition assembler : pseudo_assembly_program → res (object_code × costlabel_map) ≝ |
---|
| 60 | λp. |
---|
| 61 | let 〈preamble, list_instr〉 ≝ p in |
---|
| 62 | (* TODO: fail if p is too large. *) |
---|
| 63 | let p' ≝ 〈preamble, list_instr〉 in |
---|
| 64 | ! sigma_pol ← opt_to_res ? (msg Jump_expansion_failed) (jump_expansion' p'); |
---|
[2702] | 65 | let sigma ≝ λppc. \fst sigma_pol ppc in |
---|
| 66 | let pol ≝ λppc. \snd sigma_pol ppc in |
---|
[1995] | 67 | OK ? (assembly p sigma pol). |
---|
| 68 | cases daemon |
---|
[2497] | 69 | qed. |
---|
[1995] | 70 | |
---|
[2505] | 71 | include "ASM/ASMCosts.ma". |
---|
| 72 | |
---|
[2001] | 73 | definition lift_cost_map_back_to_front : |
---|
[2399] | 74 | ∀clight, code_memory, lbls. |
---|
[2505] | 75 | let abstat ≝ ASM_abstract_status code_memory lbls in |
---|
| 76 | (∀l. (as_cost_labelled abstat l) + ¬(as_cost_labelled abstat l)) → |
---|
| 77 | as_cost_map abstat → clight_cost_map clight ≝ |
---|
| 78 | λclight,code_memory,lbls,dec,k,asm_cost_map. |
---|
| 79 | lift_sigma_map_id … 0 (* labels not present in out code get 0 *) |
---|
[2508] | 80 | dec k asm_cost_map. |
---|
[2001] | 81 | |
---|
[2505] | 82 | include "ASM/ASMCostsSplit.ma". |
---|
| 83 | |
---|
[2001] | 84 | definition compile : clight_program → |
---|
[2508] | 85 | res (object_code × costlabel_map × (𝚺labelled:clight_program. clight_cost_map labelled)) ≝ |
---|
[1995] | 86 | λp. |
---|
[2320] | 87 | ! 〈init_cost,p',p〉 ← front_end p; |
---|
[1995] | 88 | let p ≝ back_end p in |
---|
[2001] | 89 | ! p ← assembler p; |
---|
| 90 | let k ≝ ASM_cost_map p ? in |
---|
| 91 | let k' ≝ lift_cost_map_back_to_front |
---|
[2399] | 92 | p' |
---|
[2001] | 93 | (load_code_memory (\fst p)) |
---|
| 94 | (\snd p) |
---|
| 95 | ? k |
---|
| 96 | in |
---|
[2399] | 97 | return 〈p, ❬p', k'❭〉. |
---|
[2001] | 98 | cases daemon |
---|
[2709] | 99 | qed. |
---|