include "Clight/label.ma". include "Clight/SimplifyCasts.ma". include "Clight/switchRemoval.ma". include "Clight/toCminor.ma". include "Cminor/initialisation.ma". include "Cminor/toRTLabs.ma". definition front_end : clight_program → res (costlabel × clight_program × RTLabs_program) ≝ λp. let p ≝ program_switch_removal p in let 〈p',init_cost〉 ≝ clight_label p in let p ≝ simplify_program p' in ! p ← clight_to_cminor p; let p ≝ cminor_to_rtlabs init_cost p in return 〈init_cost,p',p〉. include "RTLabs/RTLabsToRTL.ma". include "RTL/RTLToERTL.ma". include "ERTL/ERTLToLTL.ma". (* include "LTL/LTLToLIN.ma". include "LIN/LINToASM.ma". *) include "ASM/ASM.ma". include "LIN/LIN.ma". axiom ltl_to_lin: ltl_program → lin_program. axiom lin_to_asm: lin_program → pseudo_assembly_program. (* these are already defined in utilities/fixpoint.ma and ERTL/Interference.ma axiom the_fixpoint : fixpoint. axiom build : ∀valuation. coloured_graph valuation. *) definition back_end : RTLabs_program → pseudo_assembly_program ≝ λp. let p ≝ rtlabs_to_rtl p in let p ≝ rtl_to_ertl p in let p ≝ ertl_to_ltl p in (* TODO: abstract over colouring *) let p ≝ ltl_to_lin p in lin_to_asm p. (* JHM: minimum needed for assembler axiom to typecheck *) (* JHM: moved from ASMCostsSplit.ma *) (* JHM: should move elsewhere in ASM/ *) definition object_code ≝ list Byte. definition costlabel_map ≝ BitVectorTrie costlabel 16. axiom assembler : pseudo_assembly_program → res (object_code × costlabel_map). (* include "ASM/Policy.ma". definition assembler : pseudo_assembly_program → res (object_code × costlabel_map) ≝ λp. let 〈preamble, list_instr〉 ≝ p in (* TODO: fail if p is too large. *) let p' ≝ 〈preamble, list_instr〉 in ! sigma_pol ← opt_to_res ? (msg Jump_expansion_failed) (jump_expansion' p'); let sigma ≝ λppc. \fst (sigma_pol ppc) in let pol ≝ λppc. \snd (sigma_pol ppc) in OK ? (assembly p sigma pol). cases daemon qed. *) include "ASM/ASMCosts.ma". definition lift_cost_map_back_to_front : ∀clight, code_memory, lbls. let abstat ≝ ASM_abstract_status code_memory lbls in (∀l. (as_cost_labelled abstat l) + ¬(as_cost_labelled abstat l)) → as_cost_map abstat → clight_cost_map clight ≝ λclight,code_memory,lbls,dec,k,asm_cost_map. lift_sigma_map_id … 0 (* labels not present in out code get 0 *) dec k asm_cost_map. include "ASM/ASMCostsSplit.ma". definition compile : clight_program → res (object_code × costlabel_map × (𝚺labelled:clight_program. clight_cost_map labelled)) ≝ λp. ! 〈init_cost,p',p〉 ← front_end p; let p ≝ back_end p in ! p ← assembler p; let k ≝ ASM_cost_map p ? in let k' ≝ lift_cost_map_back_to_front p' (load_code_memory (\fst p)) (\snd p) ? k in return 〈p, ❬p', k'❭〉. cases daemon qed.