(* Front-end related includes *) include "Clight/label.ma". include "Clight/SimplifyCasts.ma". include "Clight/switchRemoval.ma". include "Clight/toCminor.ma". include "Cminor/toRTLabs.ma". include "RTLabs/CostCheck.ma". include "RTLabs/CostInj.ma". (* Back-end related includes *) include "RTLabs/RTLabsToRTL.ma". include "RTL/RTLToERTL.ma". include "ERTL/ERTLToERTLptr.ma". include "ERTLptr/ERTLptrToLTL.ma". include "LTL/LTLToLIN.ma". include "LIN/LINToASM.ma". (* List of all passes whose outputs can be observed *) inductive pass : Type[0] ≝ clight_pass: pass | clight_switch_removed_pass: pass | clight_label_pass: pass | clight_simplified_pass: pass | cminor_pass: pass | rtlabs_pass: pass | rtl_separate_pass: pass | rtl_uniq_pass: pass | ertl_pass: pass | ertlptr_pass: pass | ltl_pass: pass | lin_pass: pass | assembly_pass: pass | object_code_pass: pass. definition with_stack_model : Type[0] → Type[0] ≝ λA:Type[0].A × (ident → option ℕ). definition syntax_of_pass : pass → Type[0] ≝ λpass. match pass with [ clight_pass ⇒ clight_program | clight_switch_removed_pass ⇒ clight_program | clight_label_pass ⇒ clight_program | clight_simplified_pass ⇒ clight_program | cminor_pass ⇒ Cminor_program | rtlabs_pass ⇒ RTLabs_program | rtl_separate_pass ⇒ with_stack_model rtl_program | rtl_uniq_pass ⇒ with_stack_model rtl_program | ertl_pass ⇒ with_stack_model ertl_program | ertlptr_pass ⇒ with_stack_model ertlptr_program | ltl_pass ⇒ with_stack_model ltl_program | lin_pass ⇒ with_stack_model lin_program | assembly_pass ⇒ pseudo_assembly_program × (Word → Word) × (Word → bool) | object_code_pass ⇒ labelled_object_code ]. definition observe_pass ≝ ∀pass. syntax_of_pass pass → unit. (* The compiler front-end *) definition front_end : observe_pass → clight_program → res (costlabel × clight_program × RTLabs_program) ≝ λobserve,p. let i ≝ observe clight_pass p in let p ≝ program_switch_removal p in let i ≝ observe clight_switch_removed_pass p in let 〈p',init_cost〉 ≝ clight_label p in let i ≝ observe clight_label_pass p' in let p ≝ simplify_program p' in let i ≝ observe clight_simplified_pass p in ! p ← clight_to_cminor p; let i ≝ observe cminor_pass p in let p ≝ cminor_to_rtlabs p in let i ≝ observe rtlabs_pass p in if check_cost_program p then if check_program_cost_injectivity p then (return 〈init_cost,p',p〉) else (Error ? (msg RepeatedCostLabel)) else (Error ? (msg BadCostLabelling)). (* The compiler back-end *) include "ERTLptr/uses.ma". (* Included by the untrusted code *) axiom compute_fixpoint : fixpoint_computer. axiom colour_graph : coloured_graph_computer. include "common/AssocList.ma". (* Inefficient, replace with Trie lookup *) definition lookup_stack_cost ≝ λP,p,id. assoc_list_lookup ?? id (eq_identifier …) (stack_cost P p). definition back_end : observe_pass → costlabel → RTLabs_program → res (pseudo_assembly_program × stack_cost_model × nat) ≝ λobserve,init_cost,p. let p ≝ rtlabs_to_rtl init_cost p in let st ≝ lookup_stack_cost … p in let i ≝ observe rtl_separate_pass 〈p,st〉 in let i ≝ observe rtl_uniq_pass 〈p,st〉 in let p ≝ rtl_to_ertl p in let st ≝ lookup_stack_cost … p in let i ≝ observe ertl_pass 〈p,st〉 in let p ≝ ertl_to_ertlptr p in let st ≝ lookup_stack_cost … p in let i ≝ observe ertlptr_pass 〈p,st〉 in let 〈p,stack_cost,max_stack〉 ≝ ertlptr_to_ltl compute_fixpoint colour_graph p in (* The two stack models are the same *) let st ≝ lookup_stack_cost … p in let i ≝ observe ltl_pass 〈p,st〉 in let st ≝ lookup_stack_cost … p in let p ≝ ltl_to_lin p in let st ≝ lookup_stack_cost … p in let i ≝ observe lin_pass 〈p,st〉 in ! p ← opt_to_res ? (msg AssemblyTooLarge) (lin_to_asm p) ; return 〈p,stack_cost,max_stack〉. (* The assembler *) include "ASM/Policy.ma". definition assembler : observe_pass → pseudo_assembly_program → res labelled_object_code ≝ λobserve,p. ! 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 let i ≝ observe assembly_pass 〈p,sigma,pol〉 in let p ≝ assembly p sigma pol in let i ≝ observe object_code_pass p in OK ? p. (* Cost lifting *) include "ASM/ASMCosts.ma". definition lift_cost_map_back_to_front : ∀clight, oc. let abstat ≝ OC_abstract_status oc in as_cost_map abstat → clight_cost_map clight ≝ λclight,oc,k,asm_cost_map. lift_sigma_map_id … 0 (* labels not present in out code get 0 *) (strong_decidable_in_codomain …) k asm_cost_map. (* Cost model computation *) include "ASM/ASMCostsSplit.ma". record compiler_output : Type[0] ≝ { c_labelled_object_code: labelled_object_code ; c_stack_cost: stack_cost_model ; c_max_stack: nat ; c_labelled_clight: clight_program ; c_clight_cost_map: clight_cost_map c_labelled_clight }. definition compile : observe_pass → clight_program → res compiler_output ≝ λobserve,p. ! 〈init_cost,p',p〉 ← front_end observe p; ! 〈p,stack_cost,max_stack〉 ← back_end observe init_cost p; ! p ← assembler observe p; let k ≝ ASM_cost_map p in let k' ≝ lift_cost_map_back_to_front p' p k in return mk_compiler_output p stack_cost max_stack p' k'.