source: src/compiler.ma @ 2835

Last change on this file since 2835 was 2835, checked in by sacerdot, 8 years ago

Included Uses.ma which is required by the untrusted code.
The inclusion in the .ma file forces compilation and code extraction.

File size: 4.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".
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 syntax_of_pass : pass → Type[0] ≝
34 λpass.
35  match pass with
36  [ clight_pass ⇒ clight_program
37  | clight_switch_removed_pass ⇒ clight_program
38  | clight_label_pass ⇒ clight_program
39  | clight_simplified_pass ⇒ clight_program
40  | cminor_pass ⇒ Cminor_program
41  | rtlabs_pass ⇒ RTLabs_program
42  | rtl_separate_pass ⇒ rtl_program
43  | rtl_uniq_pass ⇒ rtl_program
44  | ertl_pass ⇒ ertl_program
45  | ertlptr_pass ⇒ ertlptr_program
46  | ltl_pass ⇒ ltl_program
47  | lin_pass ⇒ lin_program ].
48
49definition observe_pass ≝ ∀pass. syntax_of_pass pass → unit.
50
51(* The compiler front-end *)
52definition front_end :
53 observe_pass → clight_program → res (costlabel × clight_program × RTLabs_program) ≝
54λobserve,p.
55  let i ≝ observe clight_pass p in
[2475]56  let p ≝ program_switch_removal p in
[2828]57  let i ≝ observe clight_switch_removed_pass p in
[2319]58  let 〈p',init_cost〉 ≝ clight_label p in
[2828]59  let i ≝ observe clight_label_pass p' in
[2001]60  let p ≝ simplify_program p' in
[2828]61  let i ≝ observe clight_simplified_pass p in
[1991]62  ! p ← clight_to_cminor p;
[2828]63  let i ≝ observe cminor_pass p in
[2319]64  let p ≝ cminor_to_rtlabs init_cost p in
[2828]65  let i ≝ observe rtlabs_pass p in
[2724]66  if check_cost_program p then
67    if check_program_cost_injectivity p then
68      (return 〈init_cost,p',p〉)
69    else
70      (Error ? (msg RepeatedCostLabel))
71  else
72    (Error ? (msg BadCostLabelling)).
[1995]73
[2828]74(* The compiler back-end *)
[2835]75include "ERTLptr/Uses.ma".  (* Included by the untrusted code *)
[2700]76axiom compute_fixpoint : fixpoint_computer.
77axiom colour_graph : coloured_graph_computer.
[2505]78
[2774]79definition back_end :
[2828]80 observe_pass → RTLabs_program →
[2774]81  res (pseudo_assembly_program × stack_cost_model × nat) ≝
[2828]82λobserve,p.
[1995]83  let p ≝ rtlabs_to_rtl p in
[2828]84  let i ≝ observe rtl_separate_pass p in
85  let i ≝ observe rtl_uniq_pass p in
[1995]86  let p ≝ rtl_to_ertl p in
[2828]87  let i ≝ observe ertl_pass p in
[2697]88  let p ≝ ertl_to_ertlptr p in
[2828]89  let i ≝ observe ertlptr_pass p in
[2774]90  let 〈p,stack_cost,max_stack〉 ≝ ertlptr_to_ltl compute_fixpoint colour_graph p in (* TODO: abstract over colouring *)
[2828]91  let i ≝ observe ltl_pass p in
[1995]92  let p ≝ ltl_to_lin p in
[2828]93  let i ≝ observe lin_pass p in
[2794]94   ! p ← opt_to_res ? (msg AssemblyTooLarge) (lin_to_asm p) ;
95   return 〈p,stack_cost,max_stack〉.
[1995]96
[2828]97(* The assembler *)
[2702]98include "ASM/Policy.ma".
[2794]99
[2754]100definition assembler : pseudo_assembly_program → res labelled_object_code ≝
[1995]101λp.
[2762]102  ! sigma_pol ← opt_to_res ? (msg Jump_expansion_failed) (jump_expansion' p);
[2702]103  let sigma ≝ λppc. \fst sigma_pol ppc in
104  let pol ≝ λppc. \snd sigma_pol ppc in
[1995]105  OK ? (assembly p sigma pol).
106
[2828]107(* Cost lifting *)
[2505]108include "ASM/ASMCosts.ma".
109
[2753]110definition lift_cost_map_back_to_front :
111  ∀clight, code_memory, lbls.
112    let abstat ≝ ASM_abstract_status code_memory lbls in
113  as_cost_map abstat → clight_cost_map clight ≝
[2762]114  λclight,code_memory,lbls,k,asm_cost_map.
[2753]115  lift_sigma_map_id … 0 (* labels not present in out code get 0 *)
[2762]116    (strong_decidable_in_codomain …) k asm_cost_map.
[2753]117
[2828]118(* Cost model computation *)
119include "ASM/ASMCostsSplit.ma".
[2753]120
[2774]121record compiler_output : Type[0] ≝
122 { c_labelled_object_code: labelled_object_code
123 ; c_stack_cost: stack_cost_model
124 ; c_max_stack: nat
125 ; c_labelled_clight: clight_program
126 ; c_clight_cost_map: clight_cost_map c_labelled_clight
127 }.
128
[2828]129definition compile : observe_pass → clight_program → res compiler_output ≝
130λobserve,p.
131  ! 〈init_cost,p',p〉 ← front_end observe p;
132  ! 〈p,stack_cost,max_stack〉 ← back_end observe p;
[2767]133  ! p ← assembler p;
[2762]134  let k ≝ ASM_cost_map p in
135  let k' ≝
136   lift_cost_map_back_to_front p' (load_code_memory (oc p)) (costlabels p) k in
[2835]137  return mk_compiler_output p stack_cost max_stack p' k'.
Note: See TracBrowser for help on using the repository browser.