source: src/compiler.ma @ 2946

Last change on this file since 2946 was 2946, checked in by tranquil, 7 years ago

main novelties:

  • there is an in-built stack_usage nat in joint states, at the base of the new division of RTL's semantics (with separate stacks, with separate stacks but with an artificial overflow error, with a unique stack)
  • a premain is added semantically to the global env, so initial cost label and main call and return are observed
  • proper initialization is now in LINToASM (to be sure, endianess should be checked ;-)

The update breaks proofs of back end atm. compiler.ma should be okay, but I have not had time to complete its compilation.

File size: 5.4 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".
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
[2875]31 | lin_pass: pass
32 | assembly_pass: pass
33 | object_code_pass: pass.
[2828]34
[2841]35definition with_stack_model : Type[0] → Type[0] ≝
36 λA:Type[0].A × (ident → option ℕ).
37
[2828]38definition syntax_of_pass : pass → Type[0] ≝
39 λpass.
40  match pass with
41  [ clight_pass ⇒ clight_program
42  | clight_switch_removed_pass ⇒ clight_program
43  | clight_label_pass ⇒ clight_program
44  | clight_simplified_pass ⇒ clight_program
45  | cminor_pass ⇒ Cminor_program
46  | rtlabs_pass ⇒ RTLabs_program
[2841]47  | rtl_separate_pass ⇒ with_stack_model rtl_program
48  | rtl_uniq_pass ⇒ with_stack_model rtl_program
49  | ertl_pass ⇒ with_stack_model ertl_program
50  | ertlptr_pass ⇒ with_stack_model ertlptr_program
51  | ltl_pass ⇒ with_stack_model ltl_program
[2875]52  | lin_pass ⇒ with_stack_model lin_program
[2899]53  | assembly_pass ⇒
54     pseudo_assembly_program × (Word → Word) × (Word → bool)
[2875]55  | object_code_pass ⇒ labelled_object_code ].
[2828]56
57definition observe_pass ≝ ∀pass. syntax_of_pass pass → unit.
58
59(* The compiler front-end *)
60definition front_end :
61 observe_pass → clight_program → res (costlabel × clight_program × RTLabs_program) ≝
62λobserve,p.
63  let i ≝ observe clight_pass p in
[2475]64  let p ≝ program_switch_removal p in
[2828]65  let i ≝ observe clight_switch_removed_pass p in
[2319]66  let 〈p',init_cost〉 ≝ clight_label p in
[2828]67  let i ≝ observe clight_label_pass p' in
[2001]68  let p ≝ simplify_program p' in
[2828]69  let i ≝ observe clight_simplified_pass p in
[1991]70  ! p ← clight_to_cminor p;
[2828]71  let i ≝ observe cminor_pass p in
[2936]72  let p ≝ cminor_to_rtlabs p in
[2828]73  let i ≝ observe rtlabs_pass p in
[2724]74  if check_cost_program p then
75    if check_program_cost_injectivity p then
76      (return 〈init_cost,p',p〉)
77    else
78      (Error ? (msg RepeatedCostLabel))
79  else
80    (Error ? (msg BadCostLabelling)).
[1995]81
[2828]82(* The compiler back-end *)
[2841]83include "ERTLptr/uses.ma".  (* Included by the untrusted code *)
[2700]84axiom compute_fixpoint : fixpoint_computer.
85axiom colour_graph : coloured_graph_computer.
[2505]86
[2841]87include "common/AssocList.ma".
88
89(* Inefficient, replace with Trie lookup *)
90definition lookup_stack_cost ≝
91 λP,p,id.
92  assoc_list_lookup ?? id (eq_identifier …) (stack_cost P p).
93
[2774]94definition back_end :
[2946]95 observe_pass → costlabel → RTLabs_program →
[2774]96  res (pseudo_assembly_program × stack_cost_model × nat) ≝
[2946]97λobserve,init_cost,p.
98  let p ≝ rtlabs_to_rtl init_cost p in
[2841]99  let st ≝ lookup_stack_cost … p in
100  let i ≝ observe rtl_separate_pass 〈p,st〉 in
101  let i ≝ observe rtl_uniq_pass 〈p,st〉 in
[1995]102  let p ≝ rtl_to_ertl p in
[2841]103  let st ≝ lookup_stack_cost … p in 
104  let i ≝ observe ertl_pass 〈p,st〉 in
[2697]105  let p ≝ ertl_to_ertlptr p in
[2841]106  let st ≝ lookup_stack_cost … p in 
107  let i ≝ observe ertlptr_pass 〈p,st〉 in
108  let 〈p,stack_cost,max_stack〉 ≝ ertlptr_to_ltl compute_fixpoint colour_graph p in
109  (* The two stack models are the same *)
110  let st ≝ lookup_stack_cost … p in
111  let i ≝ observe ltl_pass 〈p,st〉 in
112  let st ≝ lookup_stack_cost … p in
[1995]113  let p ≝ ltl_to_lin p in
[2841]114  let st ≝ lookup_stack_cost … p in
115  let i ≝ observe lin_pass 〈p,st〉 in
[2875]116   ! p ← opt_to_res ? (msg AssemblyTooLarge) (lin_to_asm p) ;
[2794]117   return 〈p,stack_cost,max_stack〉.
[1995]118
[2828]119(* The assembler *)
[2702]120include "ASM/Policy.ma".
[2794]121
[2875]122definition assembler :
123 observe_pass → pseudo_assembly_program → res labelled_object_code ≝
124λobserve,p.
[2762]125  ! sigma_pol ← opt_to_res ? (msg Jump_expansion_failed) (jump_expansion' p);
[2702]126  let sigma ≝ λppc. \fst sigma_pol ppc in
127  let pol ≝ λppc. \snd sigma_pol ppc in
[2899]128  let i ≝ observe assembly_pass 〈p,sigma,pol〉 in
[2875]129  let p ≝ assembly p sigma pol in
130  let i ≝ observe object_code_pass p in
131  OK ? p.
[1995]132
[2828]133(* Cost lifting *)
[2505]134include "ASM/ASMCosts.ma".
135
[2753]136definition lift_cost_map_back_to_front :
[2907]137  ∀clight, oc.
138    let abstat ≝ OC_abstract_status oc in
[2753]139  as_cost_map abstat → clight_cost_map clight ≝
[2907]140  λclight,oc,k,asm_cost_map.
[2753]141  lift_sigma_map_id … 0 (* labels not present in out code get 0 *)
[2762]142    (strong_decidable_in_codomain …) k asm_cost_map.
[2753]143
[2828]144(* Cost model computation *)
145include "ASM/ASMCostsSplit.ma".
[2753]146
[2774]147record compiler_output : Type[0] ≝
148 { c_labelled_object_code: labelled_object_code
149 ; c_stack_cost: stack_cost_model
150 ; c_max_stack: nat
151 ; c_labelled_clight: clight_program
152 ; c_clight_cost_map: clight_cost_map c_labelled_clight
153 }.
154
[2828]155definition compile : observe_pass → clight_program → res compiler_output ≝
156λobserve,p.
157  ! 〈init_cost,p',p〉 ← front_end observe p;
[2946]158  ! 〈p,stack_cost,max_stack〉 ← back_end observe init_cost p;
[2875]159  ! p ← assembler observe p;
[2762]160  let k ≝ ASM_cost_map p in
161  let k' ≝
[2907]162   lift_cost_map_back_to_front p' p k in
163  return mk_compiler_output p stack_cost max_stack p' k'.
Note: See TracBrowser for help on using the repository browser.