source: src/compiler.ma @ 2807

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

Minor tweaks/tidying up

File size: 2.7 KB
RevLine 
[1991]1include "Clight/label.ma".
[2019]2include "Clight/SimplifyCasts.ma".
[2475]3include "Clight/switchRemoval.ma".
[1991]4include "Clight/toCminor.ma".
5include "Cminor/toRTLabs.ma".
[2724]6include "RTLabs/CostCheck.ma".
7include "RTLabs/CostInj.ma".
[1991]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
[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]24include "RTLabs/RTLabsToRTL.ma".
[1995]25include "RTL/RTLToERTL.ma".
[2697]26include "ERTL/ERTLToERTLptr.ma".
27include "ERTLptr/ERTLptrToLTL.ma".
[2794]28include "LTL/LTLToLIN.ma".
[1995]29include "LIN/LINToASM.ma".
30
[2700]31axiom compute_fixpoint : fixpoint_computer.
32axiom colour_graph : coloured_graph_computer.
[2505]33
[2774]34definition 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]46include "ASM/Policy.ma".
[2794]47
[2754]48definition 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]55include "ASM/ASMCosts.ma".
56
[2753]57definition 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
65include "ASM/ASMCostsSplit.ma".
66
[2774]67record 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
75definition 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'.
Note: See TracBrowser for help on using the repository browser.