[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/toRTLabs.ma". |
---|
[2724] | 6 | include "RTLabs/CostCheck.ma". |
---|
| 7 | include "RTLabs/CostInj.ma". |
---|
[1991] | 8 | |
---|
[2319] | 9 | definition front_end : clight_program → res (costlabel × clight_program × RTLabs_program) ≝ |
---|
[1991] | 10 | λp. |
---|
[2475] | 11 | let p ≝ program_switch_removal p in |
---|
[2319] | 12 | let 〈p',init_cost〉 ≝ clight_label p in |
---|
[2001] | 13 | let p ≝ simplify_program p' in |
---|
[1991] | 14 | ! p ← clight_to_cminor p; |
---|
[2319] | 15 | let p ≝ cminor_to_rtlabs init_cost p in |
---|
[2724] | 16 | if check_cost_program p then |
---|
| 17 | if check_program_cost_injectivity p then |
---|
| 18 | (return 〈init_cost,p',p〉) |
---|
| 19 | else |
---|
| 20 | (Error ? (msg RepeatedCostLabel)) |
---|
| 21 | else |
---|
| 22 | (Error ? (msg BadCostLabelling)). |
---|
[1995] | 23 | |
---|
[2494] | 24 | include "RTLabs/RTLabsToRTL.ma". |
---|
[1995] | 25 | include "RTL/RTLToERTL.ma". |
---|
[2697] | 26 | include "ERTL/ERTLToERTLptr.ma". |
---|
| 27 | include "ERTLptr/ERTLptrToLTL.ma". |
---|
[2794] | 28 | include "LTL/LTLToLIN.ma". |
---|
[1995] | 29 | include "LIN/LINToASM.ma". |
---|
| 30 | |
---|
[2700] | 31 | axiom compute_fixpoint : fixpoint_computer. |
---|
| 32 | axiom colour_graph : coloured_graph_computer. |
---|
[2505] | 33 | |
---|
[2774] | 34 | definition back_end : |
---|
| 35 | RTLabs_program → |
---|
| 36 | res (pseudo_assembly_program × stack_cost_model × nat) ≝ |
---|
[1995] | 37 | λp. |
---|
| 38 | let p ≝ rtlabs_to_rtl p in |
---|
| 39 | let p ≝ rtl_to_ertl p in |
---|
[2697] | 40 | let p ≝ ertl_to_ertlptr p in |
---|
[2774] | 41 | let 〈p,stack_cost,max_stack〉 ≝ ertlptr_to_ltl compute_fixpoint colour_graph p in (* TODO: abstract over colouring *) |
---|
[1995] | 42 | let p ≝ ltl_to_lin p in |
---|
[2794] | 43 | ! p ← opt_to_res ? (msg AssemblyTooLarge) (lin_to_asm p) ; |
---|
| 44 | return 〈p,stack_cost,max_stack〉. |
---|
[1995] | 45 | |
---|
[2702] | 46 | include "ASM/Policy.ma". |
---|
[2794] | 47 | |
---|
[2754] | 48 | definition assembler : pseudo_assembly_program → res labelled_object_code ≝ |
---|
[1995] | 49 | λp. |
---|
[2762] | 50 | ! sigma_pol ← opt_to_res ? (msg Jump_expansion_failed) (jump_expansion' p); |
---|
[2702] | 51 | let sigma ≝ λppc. \fst sigma_pol ppc in |
---|
| 52 | let pol ≝ λppc. \snd sigma_pol ppc in |
---|
[1995] | 53 | OK ? (assembly p sigma pol). |
---|
| 54 | |
---|
[2505] | 55 | include "ASM/ASMCosts.ma". |
---|
| 56 | |
---|
[2753] | 57 | definition lift_cost_map_back_to_front : |
---|
| 58 | ∀clight, code_memory, lbls. |
---|
| 59 | let abstat ≝ ASM_abstract_status code_memory lbls in |
---|
| 60 | as_cost_map abstat → clight_cost_map clight ≝ |
---|
[2762] | 61 | λclight,code_memory,lbls,k,asm_cost_map. |
---|
[2753] | 62 | lift_sigma_map_id … 0 (* labels not present in out code get 0 *) |
---|
[2762] | 63 | (strong_decidable_in_codomain …) k asm_cost_map. |
---|
[2753] | 64 | |
---|
| 65 | include "ASM/ASMCostsSplit.ma". |
---|
| 66 | |
---|
[2774] | 67 | record compiler_output : Type[0] ≝ |
---|
| 68 | { c_labelled_object_code: labelled_object_code |
---|
| 69 | ; c_stack_cost: stack_cost_model |
---|
| 70 | ; c_max_stack: nat |
---|
| 71 | ; c_labelled_clight: clight_program |
---|
| 72 | ; c_clight_cost_map: clight_cost_map c_labelled_clight |
---|
| 73 | }. |
---|
| 74 | |
---|
| 75 | definition compile : clight_program → res compiler_output ≝ |
---|
[1995] | 76 | λp. |
---|
[2320] | 77 | ! 〈init_cost,p',p〉 ← front_end p; |
---|
[2774] | 78 | ! 〈p,stack_cost,max_stack〉 ← back_end p; |
---|
[2767] | 79 | ! p ← assembler p; |
---|
[2762] | 80 | let k ≝ ASM_cost_map p in |
---|
| 81 | let k' ≝ |
---|
| 82 | lift_cost_map_back_to_front p' (load_code_memory (oc p)) (costlabels p) k in |
---|
[2774] | 83 | return mk_compiler_output p stack_cost max_stack p' k'. |
---|