source: src/compiler.ma @ 2113

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

Split out special induction principle for Clight from soundness file.
Put cast simplification into compiler.ma.

File size: 2.7 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 (clight_program × RTLabs_program) ≝
10λp.
11  let p' ≝ clight_label p in
12  let p ≝ simplify_program p' in
13  let p ≝ program_switch_removal p in
14  ! p ← clight_to_cminor p;
15  ! p ← cminor_to_rtlabs p;
16  return 〈p',p〉.
17
18include "RTLabs/RTLabsToRTL.ma".
19include "RTL/RTLToERTL.ma".
20include "ERTL/ERTLToLTL.ma".
21include "LTL/LTLToLIN.ma".
22include "LIN/LINToASM.ma".
23
24axiom the_fixpoint : fixpoint.
25axiom build : ∀valuation. coloured_graph valuation.
26
27definition back_end : RTLabs_program → pseudo_assembly_program ≝
28λp.
29  let p ≝ rtlabs_to_rtl p in
30  let p ≝ rtl_to_ertl p in
31  let p ≝ ertl_to_ltl p in  (* TODO: abstract over colouring *)
32  let p ≝ ltl_to_lin p in
33          lin_to_asm p.
34
35include "ASM/Assembly.ma".
36
37include "ASM/Policy.ma".
38
39axiom Jump_expansion_failed : String.
40
41include "ASM/ASMCostsSplit.ma".
42
43definition assembler : pseudo_assembly_program → res (object_code × costlabel_map) ≝
44λp.
45  let 〈preamble, list_instr〉 ≝ p in
46  (* TODO: fail if p is too large. *)
47  let p' ≝ 〈preamble, list_instr〉 in
48  ! sigma_pol ← opt_to_res ? (msg Jump_expansion_failed) (jump_expansion' p');
49  let sigma ≝ λppc. \fst (sigma_pol ppc) in
50  let pol ≝ λppc. \snd (sigma_pol ppc) in
51  OK ? (assembly p sigma pol).
52cases daemon
53qed.
54
55include "RTLabs/semantics.ma".
56
57axiom RTLabs_abstract_status : genv → abstract_status.
58
59include "joint/semantics.ma".
60axiom joint_abstract_status :
61  ∀globals.∀p:params globals.genv globals p → abstract_status.
62
63include "common/StructuredTraces.ma".
64
65definition in_clight_program : costlabel → Prop ≝ λ_.True.
66
67definition lift_cost_map_back_to_front :
68  ∀code_memory, lbls.
69   (∀l. (∃pc.as_label_of_pc (ASM_abstract_status code_memory lbls) pc = Some … l) +
70       ¬(∃pc.as_label_of_pc (ASM_abstract_status code_memory lbls) pc = Some … l)) →
71  as_cost_map (ASM_abstract_status code_memory lbls) →
72  (Σl : costlabel.in_clight_program l) → ℕ ≝ λcode_memory,lbls,dec,k,l_sig.
73   match dec l_sig with
74   [ inl prf ⇒ k «l_sig, prf»
75   | inr _ ⇒ 0 (* labels not present in out code get 0 *)
76   ].
77
78definition compile : clight_program →
79  res (object_code × costlabel_map × clight_program × ((Σl.in_clight_program l) → ℕ)) ≝
80λp.
81  ! 〈p',p〉 ← front_end p;
82  let p ≝ back_end p in
83    ! p ← assembler p;
84  let k ≝ ASM_cost_map p ? in
85  let k' ≝ lift_cost_map_back_to_front
86    (load_code_memory (\fst p))
87    (\snd p)
88    ? k
89    in
90  return 〈p, p', k'〉.
91  cases daemon
92  qed.
93
Note: See TracBrowser for help on using the repository browser.