source: src/compiler.ma @ 2697

Last change on this file since 2697 was 2697, checked in by sacerdot, 7 years ago

Compiler fixed to include the ERTLptrToLTL pass.

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