source: src/compiler.ma @ 2492

Last change on this file since 2492 was 2492, checked in by campbell, 8 years ago

Reduce axiomatisation in compiler.ma.

File size: 3.0 KB
Line 
1
2include "Clight/label.ma".
3include "Clight/SimplifyCasts.ma".
4include "Clight/switchRemoval.ma".
5include "Clight/toCminor.ma".
6include "Cminor/initialisation.ma".
7include "Cminor/toRTLabs.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  return 〈init_cost,p',p〉.
17
18(* Recent changes have temporarily stopped the back-end from checking, so
19   axiomatise it for a little while.
20include "RTLabs/RTLabsToRTL.ma". *) include "RTL/RTL.ma". axiom rtlabs_to_rtl: RTLabs_program → rtl_program.
21include "RTL/RTLToERTL.ma".
22include "ERTL/ERTLToLTL.ma".
23include "LTL/LTLToLIN.ma".
24include "LIN/LINToASM.ma".
25
26(* these are already defined in utilities/fixpoint.ma and ERTL/Interference.ma
27axiom the_fixpoint : fixpoint.
28axiom build : ∀valuation. coloured_graph valuation.
29*)
30definition back_end : RTLabs_program → pseudo_assembly_program ≝
31λp.
32  let p ≝ rtlabs_to_rtl p in
33  let p ≝ rtl_to_ertl p in
34  let p ≝ ertl_to_ltl p in  (* TODO: abstract over colouring *)
35  let p ≝ ltl_to_lin p in
36          lin_to_asm p.
37
38include "ASM/Assembly.ma".
39
40include "ASM/Policy.ma".
41
42axiom Jump_expansion_failed : String.
43
44include "ASM/ASMCostsSplit.ma".
45
46axiom assembler : pseudo_assembly_program → res (object_code × costlabel_map). (*
47definition assembler : pseudo_assembly_program → res (object_code × costlabel_map) ≝
48λp.
49  let 〈preamble, list_instr〉 ≝ p in
50  (* TODO: fail if p is too large. *)
51  let p' ≝ 〈preamble, list_instr〉 in
52  ! sigma_pol ← opt_to_res ? (msg Jump_expansion_failed) (jump_expansion' p');
53  let sigma ≝ λppc. \fst (sigma_pol ppc) in
54  let pol ≝ λppc. \snd (sigma_pol ppc) in
55  OK ? (assembly p sigma pol).
56cases daemon
57qed.*)
58
59include "RTLabs/semantics.ma".
60
61include "joint/Traces.ma".
62
63include "ASM/Fetch.ma". (* For load_code_memory only *)
64
65definition lift_cost_map_back_to_front :
66  ∀clight, code_memory, lbls.
67   (∀l. (∃pc.as_label_of_pc (ASM_abstract_status code_memory lbls) pc = Some … l) +
68       ¬(∃pc.as_label_of_pc (ASM_abstract_status code_memory lbls) pc = Some … l)) →
69  as_cost_map (ASM_abstract_status code_memory lbls) →
70  (Σl : costlabel.in_clight_program clight l) → ℕ ≝ λclight,code_memory,lbls,dec,k,l_sig.
71   match dec l_sig with
72   [ inl prf ⇒ k «l_sig, prf»
73   | inr _ ⇒ 0 (* labels not present in out code get 0 *)
74   ].
75
76definition compile : clight_program →
77  res (object_code × costlabel_map × (𝚺labelled:clight_program. ((Σl.in_clight_program labelled l) → ℕ))) ≝
78λp.
79  ! 〈init_cost,p',p〉 ← front_end p;
80  let p ≝ back_end p in
81    ! p ← assembler p;
82  let k ≝ ASM_cost_map p ? in
83  let k' ≝ lift_cost_map_back_to_front
84    p'
85    (load_code_memory (\fst p))
86    (\snd p)
87    ? k
88    in
89  return 〈p, ❬p', k'❭〉.
90  cases daemon
91  qed.
92
Note: See TracBrowser for help on using the repository browser.