source: src/compiler.ma @ 2505

Last change on this file since 2505 was 2505, checked in by mckinna, 7 years ago

Cleaned up compiler.ma; some refactoring/additional code needed in Clight/label, and a tweak to translate_cst in RTLabsToRTL to restore its checked status.

File size: 2.8 KB
RevLine 
[1991]1
2include "Clight/label.ma".
[2019]3include "Clight/SimplifyCasts.ma".
[2475]4include "Clight/switchRemoval.ma".
[1991]5include "Clight/toCminor.ma".
6include "Cminor/initialisation.ma".
7include "Cminor/toRTLabs.ma".
8
[2319]9definition 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
16  return 〈init_cost,p',p〉.
[1995]17
[2494]18include "RTLabs/RTLabsToRTL.ma".
[1995]19include "RTL/RTLToERTL.ma".
20include "ERTL/ERTLToLTL.ma".
21include "LTL/LTLToLIN.ma".
22include "LIN/LINToASM.ma".
23
[2286]24(* these are already defined in utilities/fixpoint.ma and ERTL/Interference.ma
[1995]25axiom the_fixpoint : fixpoint.
26axiom build : ∀valuation. coloured_graph valuation.
[2286]27*)
[2505]28
[1995]29definition back_end : RTLabs_program → pseudo_assembly_program ≝
30λp.
31  let p ≝ rtlabs_to_rtl p in
32  let p ≝ rtl_to_ertl p in
33  let p ≝ ertl_to_ltl p in  (* TODO: abstract over colouring *)
34  let p ≝ ltl_to_lin p in
35          lin_to_asm p.
36
[2505]37include "ASM/Fetch.ma". (* minimum needed for axiom to typecheck *)
[1995]38
[2497]39axiom assembler : pseudo_assembly_program → res (object_code × costlabel_map).
[1995]40
[2505]41(* include "ASM/Policy.ma".
42
[1995]43axiom Jump_expansion_failed : String.
44
45definition assembler : pseudo_assembly_program → res (object_code × costlabel_map) ≝
46λp.
47  let 〈preamble, list_instr〉 ≝ p in
48  (* TODO: fail if p is too large. *)
49  let p' ≝ 〈preamble, list_instr〉 in
50  ! sigma_pol ← opt_to_res ? (msg Jump_expansion_failed) (jump_expansion' p');
51  let sigma ≝ λppc. \fst (sigma_pol ppc) in
52  let pol ≝ λppc. \snd (sigma_pol ppc) in
53  OK ? (assembly p sigma pol).
54cases daemon
[2497]55qed.
56*)
[1995]57
[2001]58
[2505]59include "ASM/ASMCosts.ma".
60
[2001]61definition lift_cost_map_back_to_front :
[2399]62  ∀clight, code_memory, lbls.
[2505]63    let abstat ≝ ASM_abstract_status code_memory lbls in
64   (∀l. (as_cost_labelled abstat l) + ¬(as_cost_labelled abstat l)) →
65  as_cost_map abstat → clight_cost_map clight ≝
66  λclight,code_memory,lbls,dec,k,asm_cost_map.
67  lift_sigma_map_id … 0 (* labels not present in out code get 0 *)
68    dec k asm_cost_map
69  (*
70   match dec asm_cost_map with
[2001]71   [ inl prf ⇒ k «l_sig, prf»
72   | inr _ ⇒ 0 (* labels not present in out code get 0 *)
[2505]73   ]*).
[2001]74
[2505]75include "ASM/ASMCostsSplit.ma".
76
[2001]77definition compile : clight_program →
[2505]78  res (object_code × costlabel_map × (𝚺labelled:clight_program. clight_cost_map labelled)) (*(Σl.in_clight_program labelled l) → ℕ*) ≝
[1995]79λp.
[2320]80  ! 〈init_cost,p',p〉 ← front_end p;
[1995]81  let p ≝ back_end p in
[2001]82    ! p ← assembler p;
83  let k ≝ ASM_cost_map p ? in
84  let k' ≝ lift_cost_map_back_to_front
[2399]85    p'
[2001]86    (load_code_memory (\fst p))
87    (\snd p)
88    ? k
89    in
[2399]90  return 〈p, ❬p', k'❭〉.
[2001]91  cases daemon
92  qed.
Note: See TracBrowser for help on using the repository browser.