source: src/compiler.ma @ 2782

Last change on this file since 2782 was 2774, checked in by sacerdot, 7 years ago
  1. the compiler now outputs both the stack cost model and the max stack available
  2. hypothesis on initial status not failing removed from correctness.ma by using the low level definition
File size: 3.3 KB
Line 
1include "Clight/label.ma".
2include "Clight/SimplifyCasts.ma".
3include "Clight/switchRemoval.ma".
4include "Clight/toCminor.ma".
5include "Cminor/toRTLabs.ma".
6include "RTLabs/CostCheck.ma".
7include "RTLabs/CostInj.ma".
8
9definition front_end : clight_program → res (costlabel × clight_program × RTLabs_program) ≝
10λp.
11  let p ≝ program_switch_removal p in
12  let 〈p',init_cost〉 ≝ clight_label p in
13  let p ≝ simplify_program p' in
14  ! p ← clight_to_cminor p;
15  let p ≝ cminor_to_rtlabs init_cost p in
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)).
23
24include "RTLabs/RTLabsToRTL.ma".
25include "RTL/RTLToERTL.ma".
26include "ERTL/ERTLToERTLptr.ma".
27include "ERTLptr/ERTLptrToLTL.ma".
28include "LTL/LTLToLIN.ma".
29include "LIN/LINToASM.ma".
30
31axiom compute_fixpoint : fixpoint_computer.
32axiom colour_graph : coloured_graph_computer.
33
34definition back_end :
35 RTLabs_program →
36  res (pseudo_assembly_program × stack_cost_model × nat) ≝
37λp.
38  let p ≝ rtlabs_to_rtl p in
39  let p ≝ rtl_to_ertl p in
40  let p ≝ ertl_to_ertlptr p in
41  let 〈p,stack_cost,max_stack〉 ≝ ertlptr_to_ltl compute_fixpoint colour_graph p in (* TODO: abstract over colouring *)
42  let p ≝ ltl_to_lin p in
43  let p ≝ lin_to_asm p in
44   match p with
45   [ None ⇒ Error … (msg AssemblyTooLarge)
46   | Some p ⇒ OK … 〈p,stack_cost,max_stack〉 ].
47
48include "ASM/Policy.ma".
49(* Equivalent to the inclusion of ASM/Policy.ma, waiting for that slow
50   file to compile
51  include "ASM/PolicyStep.ma".
52  axiom jump_expansion': ∀program:preamble × (Σl:list labelled_instruction.lt (S (|l|)) 2^16 ∧ is_well_labelled_p l).
53 option (Σsigma_policy:(Word → Word) × (Word → bool).
54   let 〈sigma,policy〉≝ sigma_policy in
55   sigma_policy_specification 〈\fst program,\snd program〉 sigma policy). *)
56   
57definition assembler : pseudo_assembly_program → res labelled_object_code ≝
58λp.
59  ! sigma_pol ← opt_to_res ? (msg Jump_expansion_failed) (jump_expansion' p);
60  let sigma ≝ λppc. \fst sigma_pol ppc in
61  let pol ≝ λppc. \snd sigma_pol ppc in
62  OK ? (assembly p sigma pol).
63
64include "ASM/ASMCosts.ma".
65
66(*CSC: move the next definitions, e.g. in BitVectorTrie; JHM: done! *)
67
68definition lift_cost_map_back_to_front :
69  ∀clight, code_memory, lbls.
70    let abstat ≝ ASM_abstract_status code_memory lbls in
71  as_cost_map abstat → clight_cost_map clight ≝
72  λclight,code_memory,lbls,k,asm_cost_map.
73  lift_sigma_map_id … 0 (* labels not present in out code get 0 *)
74    (strong_decidable_in_codomain …) k asm_cost_map.
75
76include "ASM/ASMCostsSplit.ma".
77
78record compiler_output : Type[0] ≝
79 { c_labelled_object_code: labelled_object_code
80 ; c_stack_cost: stack_cost_model
81 ; c_max_stack: nat
82 ; c_labelled_clight: clight_program
83 ; c_clight_cost_map: clight_cost_map c_labelled_clight
84 }.
85
86definition compile : clight_program → res compiler_output ≝
87λp.
88  ! 〈init_cost,p',p〉 ← front_end p;
89  ! 〈p,stack_cost,max_stack〉 ← back_end p;
90  ! p ← assembler p;
91  let k ≝ ASM_cost_map p in
92  let k' ≝
93   lift_cost_map_back_to_front p' (load_code_memory (oc p)) (costlabels p) k in
94  return mk_compiler_output p stack_cost max_stack p' k'.
Note: See TracBrowser for help on using the repository browser.