source: src/compiler.ma @ 3097

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

The cost and stack* variables are now initialized with the cost of
the pre-main and the size of globals.

File size: 5.5 KB
RevLine 
[2828]1(* Front-end related includes *)
[1991]2include "Clight/label.ma".
[2019]3include "Clight/SimplifyCasts.ma".
[2475]4include "Clight/switchRemoval.ma".
[1991]5include "Clight/toCminor.ma".
6include "Cminor/toRTLabs.ma".
[2724]7include "RTLabs/CostCheck.ma".
8include "RTLabs/CostInj.ma".
[1991]9
[2828]10(* Back-end related includes *)
11include "RTLabs/RTLabsToRTL.ma".
12include "RTL/RTLToERTL.ma".
[3014]13include "ERTL/ERTLToLTL.ma".
[2828]14include "LTL/LTLToLIN.ma".
15include "LIN/LINToASM.ma".
16
17(* List of all passes whose outputs can be observed *)
18inductive pass : Type[0] ≝
19   clight_pass: pass
20 | clight_switch_removed_pass: pass
21 | clight_label_pass: pass
22 | clight_simplified_pass: pass
23 | cminor_pass: pass
24 | rtlabs_pass: pass
25 | rtl_separate_pass: pass
26 | rtl_uniq_pass: pass
27 | ertl_pass: pass
28 | ltl_pass: pass
[2875]29 | lin_pass: pass
30 | assembly_pass: pass
31 | object_code_pass: pass.
[2828]32
[2841]33definition with_stack_model : Type[0] → Type[0] ≝
34 λA:Type[0].A × (ident → option ℕ).
35
[2828]36definition syntax_of_pass : pass → Type[0] ≝
37 λpass.
38  match pass with
39  [ clight_pass ⇒ clight_program
40  | clight_switch_removed_pass ⇒ clight_program
41  | clight_label_pass ⇒ clight_program
42  | clight_simplified_pass ⇒ clight_program
43  | cminor_pass ⇒ Cminor_program
44  | rtlabs_pass ⇒ RTLabs_program
[2841]45  | rtl_separate_pass ⇒ with_stack_model rtl_program
46  | rtl_uniq_pass ⇒ with_stack_model rtl_program
47  | ertl_pass ⇒ with_stack_model ertl_program
48  | ltl_pass ⇒ with_stack_model ltl_program
[2875]49  | lin_pass ⇒ with_stack_model lin_program
[2899]50  | assembly_pass ⇒
51     pseudo_assembly_program × (Word → Word) × (Word → bool)
[2875]52  | object_code_pass ⇒ labelled_object_code ].
[2828]53
54definition observe_pass ≝ ∀pass. syntax_of_pass pass → unit.
55
56(* The compiler front-end *)
57definition front_end :
58 observe_pass → clight_program → res (costlabel × clight_program × RTLabs_program) ≝
59λobserve,p.
60  let i ≝ observe clight_pass p in
[2475]61  let p ≝ program_switch_removal p in
[2828]62  let i ≝ observe clight_switch_removed_pass p in
[2319]63  let 〈p',init_cost〉 ≝ clight_label p in
[2828]64  let i ≝ observe clight_label_pass p' in
[2001]65  let p ≝ simplify_program p' in
[2828]66  let i ≝ observe clight_simplified_pass p in
[1991]67  ! p ← clight_to_cminor p;
[2828]68  let i ≝ observe cminor_pass p in
[2936]69  let p ≝ cminor_to_rtlabs p in
[2828]70  let i ≝ observe rtlabs_pass p in
[3022]71  ! WCL ← check_cost_program_prf p;
72  ! INJ ← check_program_cost_injectivity_prf p;
73  return 〈init_cost,p',p〉.
[1995]74
[2828]75(* The compiler back-end *)
[3018]76include "ERTL/uses.ma".  (* Included by the untrusted code *)
[2700]77axiom compute_fixpoint : fixpoint_computer.
78axiom colour_graph : coloured_graph_computer.
[2505]79
[2841]80include "common/AssocList.ma".
81
82(* Inefficient, replace with Trie lookup *)
83definition lookup_stack_cost ≝
84 λP,p,id.
85  assoc_list_lookup ?? id (eq_identifier …) (stack_cost P p).
86
[2774]87definition back_end :
[2946]88 observe_pass → costlabel → RTLabs_program →
[3083]89  res (pseudo_assembly_program × costlabel × stack_cost_model × nat) ≝
[2946]90λobserve,init_cost,p.
91  let p ≝ rtlabs_to_rtl init_cost p in
[2841]92  let st ≝ lookup_stack_cost … p in
93  let i ≝ observe rtl_separate_pass 〈p,st〉 in
94  let i ≝ observe rtl_uniq_pass 〈p,st〉 in
[1995]95  let p ≝ rtl_to_ertl p in
[2841]96  let st ≝ lookup_stack_cost … p in 
97  let i ≝ observe ertl_pass 〈p,st〉 in
[3014]98  let 〈p,stack_cost,max_stack〉 ≝ ertl_to_ltl compute_fixpoint colour_graph p in
[2841]99  (* The two stack models are the same *)
100  let st ≝ lookup_stack_cost … p in
101  let i ≝ observe ltl_pass 〈p,st〉 in
102  let st ≝ lookup_stack_cost … p in
[1995]103  let p ≝ ltl_to_lin p in
[2841]104  let st ≝ lookup_stack_cost … p in
105  let i ≝ observe lin_pass 〈p,st〉 in
[2875]106   ! p ← opt_to_res ? (msg AssemblyTooLarge) (lin_to_asm p) ;
[3083]107   return 〈〈p,init_cost〉,stack_cost,max_stack〉.
[1995]108
[2828]109(* The assembler *)
[2702]110include "ASM/Policy.ma".
[2794]111
[2875]112definition assembler :
113 observe_pass → pseudo_assembly_program → res labelled_object_code ≝
114λobserve,p.
[2762]115  ! sigma_pol ← opt_to_res ? (msg Jump_expansion_failed) (jump_expansion' p);
[2702]116  let sigma ≝ λppc. \fst sigma_pol ppc in
117  let pol ≝ λppc. \snd sigma_pol ppc in
[2899]118  let i ≝ observe assembly_pass 〈p,sigma,pol〉 in
[2875]119  let p ≝ assembly p sigma pol in
120  let i ≝ observe object_code_pass p in
121  OK ? p.
[1995]122
[2828]123(* Cost lifting *)
[2505]124include "ASM/ASMCosts.ma".
125
[3021]126definition lift_out_of_sigma :
127  ∀A,B : Type[0].∀P_out : A → Prop.B →
128    (∀a.P_out a + ¬ P_out a) →
129  ((Σa.P_out a) → B) → A → B ≝ λA,B,P_out,dflt,dec,m,a_sig.
130   match dec a_sig with
131   [ inl prf ⇒ m «a_sig, prf»
132   | inr _ ⇒ dflt (* labels not present in out code get 0 *)
133   ].
134
[2753]135definition lift_cost_map_back_to_front :
[3021]136  ∀oc.
[2907]137    let abstat ≝ OC_abstract_status oc in
[3021]138  as_cost_map abstat → clight_cost_map ≝
139  λoc,asm_cost_map.
140  lift_out_of_sigma … 0 (* labels not present in out code get 0 *)
141    (strong_decidable_in_codomain …) asm_cost_map.
[2753]142
[2828]143(* Cost model computation *)
144include "ASM/ASMCostsSplit.ma".
[2753]145
[2774]146record compiler_output : Type[0] ≝
147 { c_labelled_object_code: labelled_object_code
148 ; c_stack_cost: stack_cost_model
149 ; c_max_stack: nat
[3083]150 ; c_init_costlabel: costlabel
[2774]151 ; c_labelled_clight: clight_program
[3021]152 ; c_clight_cost_map: clight_cost_map
[2774]153 }.
154
[2828]155definition compile : observe_pass → clight_program → res compiler_output ≝
156λobserve,p.
157  ! 〈init_cost,p',p〉 ← front_end observe p;
[3083]158  ! 〈p_init_costlabel,stack_cost,max_stack〉 ← back_end observe init_cost p;
159  let 〈p,init_costlabel〉 ≝ p_init_costlabel in
[2875]160  ! p ← assembler observe p;
[2762]161  let k ≝ ASM_cost_map p in
162  let k' ≝
[3021]163   lift_cost_map_back_to_front p k in
[3083]164  return mk_compiler_output p stack_cost max_stack init_costlabel p' k'.
Note: See TracBrowser for help on using the repository browser.