source: src/compiler.ma @ 2861

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

The compiler now computes also the stack cost for every intermediate
back-end language. The extracted compiler now executes all back-end
passes up to the assembly lanuguage (excluded ATM).

File size: 5.1 KB
Line 
1(* Front-end related includes *)
2include "Clight/label.ma".
3include "Clight/SimplifyCasts.ma".
4include "Clight/switchRemoval.ma".
5include "Clight/toCminor.ma".
6include "Cminor/toRTLabs.ma".
7include "RTLabs/CostCheck.ma".
8include "RTLabs/CostInj.ma".
9
10(* Back-end related includes *)
11include "RTLabs/RTLabsToRTL.ma".
12include "RTL/RTLToERTL.ma".
13include "ERTL/ERTLToERTLptr.ma".
14include "ERTLptr/ERTLptrToLTL.ma".
15include "LTL/LTLToLIN.ma".
16include "LIN/LINToASM.ma".
17
18(* List of all passes whose outputs can be observed *)
19inductive pass : Type[0] ≝
20   clight_pass: pass
21 | clight_switch_removed_pass: pass
22 | clight_label_pass: pass
23 | clight_simplified_pass: pass
24 | cminor_pass: pass
25 | rtlabs_pass: pass
26 | rtl_separate_pass: pass
27 | rtl_uniq_pass: pass
28 | ertl_pass: pass
29 | ertlptr_pass: pass
30 | ltl_pass: pass
31 | lin_pass: pass.
32
33definition with_stack_model : Type[0] → Type[0] ≝
34 λA:Type[0].A × (ident → option ℕ).
35
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
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  | ertlptr_pass ⇒ with_stack_model ertlptr_program
49  | ltl_pass ⇒ with_stack_model ltl_program
50  | lin_pass ⇒ with_stack_model lin_program ].
51
52definition observe_pass ≝ ∀pass. syntax_of_pass pass → unit.
53
54(* The compiler front-end *)
55definition front_end :
56 observe_pass → clight_program → res (costlabel × clight_program × RTLabs_program) ≝
57λobserve,p.
58  let i ≝ observe clight_pass p in
59  let p ≝ program_switch_removal p in
60  let i ≝ observe clight_switch_removed_pass p in
61  let 〈p',init_cost〉 ≝ clight_label p in
62  let i ≝ observe clight_label_pass p' in
63  let p ≝ simplify_program p' in
64  let i ≝ observe clight_simplified_pass p in
65  ! p ← clight_to_cminor p;
66  let i ≝ observe cminor_pass p in
67  let p ≝ cminor_to_rtlabs init_cost p in
68  let i ≝ observe rtlabs_pass p in
69  if check_cost_program p then
70    if check_program_cost_injectivity p then
71      (return 〈init_cost,p',p〉)
72    else
73      (Error ? (msg RepeatedCostLabel))
74  else
75    (Error ? (msg BadCostLabelling)).
76
77(* The compiler back-end *)
78include "ERTLptr/uses.ma".  (* Included by the untrusted code *)
79axiom compute_fixpoint : fixpoint_computer.
80axiom colour_graph : coloured_graph_computer.
81
82include "common/AssocList.ma".
83
84(* Inefficient, replace with Trie lookup *)
85definition lookup_stack_cost ≝
86 λP,p,id.
87  assoc_list_lookup ?? id (eq_identifier …) (stack_cost P p).
88
89definition back_end :
90 observe_pass → RTLabs_program →
91  res (pseudo_assembly_program × stack_cost_model × nat) ≝
92λobserve,p.
93  let p ≝ rtlabs_to_rtl p in
94  let st ≝ lookup_stack_cost … p in
95  let i ≝ observe rtl_separate_pass 〈p,st〉 in
96  let i ≝ observe rtl_uniq_pass 〈p,st〉 in
97  let p ≝ rtl_to_ertl p in
98  let st ≝ lookup_stack_cost … p in 
99  let i ≝ observe ertl_pass 〈p,st〉 in
100  let p ≝ ertl_to_ertlptr p in
101  let st ≝ lookup_stack_cost … p in 
102  let i ≝ observe ertlptr_pass 〈p,st〉 in
103  let 〈p,stack_cost,max_stack〉 ≝ ertlptr_to_ltl compute_fixpoint colour_graph p in
104  (* The two stack models are the same *)
105  let st ≝ lookup_stack_cost … p in
106  let i ≝ observe ltl_pass 〈p,st〉 in
107  let st ≝ lookup_stack_cost … p in
108  let p ≝ ltl_to_lin p in
109  let st ≝ lookup_stack_cost … p in
110  let i ≝ observe lin_pass 〈p,st〉 in
111   ! p ← opt_to_res ? (msg AssemblyTooLarge) (lin_to_asm p) ;
112   return 〈p,stack_cost,max_stack〉.
113
114(* The assembler *)
115include "ASM/Policy.ma".
116
117definition assembler : pseudo_assembly_program → res labelled_object_code ≝
118λp.
119  ! sigma_pol ← opt_to_res ? (msg Jump_expansion_failed) (jump_expansion' p);
120  let sigma ≝ λppc. \fst sigma_pol ppc in
121  let pol ≝ λppc. \snd sigma_pol ppc in
122  OK ? (assembly p sigma pol).
123
124(* Cost lifting *)
125include "ASM/ASMCosts.ma".
126
127definition lift_cost_map_back_to_front :
128  ∀clight, code_memory, lbls.
129    let abstat ≝ ASM_abstract_status code_memory lbls in
130  as_cost_map abstat → clight_cost_map clight ≝
131  λclight,code_memory,lbls,k,asm_cost_map.
132  lift_sigma_map_id … 0 (* labels not present in out code get 0 *)
133    (strong_decidable_in_codomain …) k asm_cost_map.
134
135(* Cost model computation *)
136include "ASM/ASMCostsSplit.ma".
137
138record compiler_output : Type[0] ≝
139 { c_labelled_object_code: labelled_object_code
140 ; c_stack_cost: stack_cost_model
141 ; c_max_stack: nat
142 ; c_labelled_clight: clight_program
143 ; c_clight_cost_map: clight_cost_map c_labelled_clight
144 }.
145
146definition compile : observe_pass → clight_program → res compiler_output ≝
147λobserve,p.
148  ! 〈init_cost,p',p〉 ← front_end observe p;
149  ! 〈p,stack_cost,max_stack〉 ← back_end observe p;
150  ! p ← assembler p;
151  let k ≝ ASM_cost_map p in
152  let k' ≝
153   lift_cost_map_back_to_front p' (load_code_memory (oc p)) (costlabels p) k in
154  return mk_compiler_output p stack_cost max_stack p' k'.
Note: See TracBrowser for help on using the repository browser.