source: src/compiler.ma @ 2562

Last change on this file since 2562 was 2512, checked in by mckinna, 8 years ago

Simplified dependencies on ASM, to allow rollback to when AssmeblyProof?.ma checked.
But still a problem with disambiguation in ASM/AssemblyProofSplit.ma, starting from case 12: (* JC *) (l.1148). What's gone wrong?

File size: 2.8 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
18include "RTLabs/RTLabsToRTL.ma".
19include "RTL/RTLToERTL.ma".
20include "ERTL/ERTLToLTL.ma".
21include "LTL/LTLToLIN.ma".
22include "LIN/LINToASM.ma".
23
24(* these are already defined in utilities/fixpoint.ma and ERTL/Interference.ma
25axiom the_fixpoint : fixpoint.
26axiom build : ∀valuation. coloured_graph valuation.
27*)
28
29definition back_end : RTLabs_program → pseudo_assembly_program ≝
30λp.
31  let p ≝ rtlabs_to_rtl p in
32  let p ≝ rtl_to_ertl p in
33  let p ≝ ertl_to_ltl p in  (* TODO: abstract over colouring *)
34  let p ≝ ltl_to_lin p in
35          lin_to_asm p.
36
37(* JHM: minimum needed for assembler axiom to typecheck *)
38(* JHM: moved from ASMCostsSplit.ma                     *)
39(* JHM: should move elsewhere in ASM/                   *)
40definition object_code ≝ list Byte.
41definition costlabel_map ≝ BitVectorTrie costlabel 16.
42
43axiom assembler : pseudo_assembly_program → res (object_code × costlabel_map).
44
45(* include "ASM/Policy.ma".
46
47axiom Jump_expansion_failed : String.
48
49definition assembler : pseudo_assembly_program → res (object_code × costlabel_map) ≝
50λp.
51  let 〈preamble, list_instr〉 ≝ p in
52  (* TODO: fail if p is too large. *)
53  let p' ≝ 〈preamble, list_instr〉 in
54  ! sigma_pol ← opt_to_res ? (msg Jump_expansion_failed) (jump_expansion' p');
55  let sigma ≝ λppc. \fst (sigma_pol ppc) in
56  let pol ≝ λppc. \snd (sigma_pol ppc) in
57  OK ? (assembly p sigma pol).
58cases daemon
59qed.
60*)
61
62include "ASM/ASMCosts.ma".
63
64definition lift_cost_map_back_to_front :
65  ∀clight, code_memory, lbls.
66    let abstat ≝ ASM_abstract_status code_memory lbls in
67   (∀l. (as_cost_labelled abstat l) + ¬(as_cost_labelled abstat l)) →
68  as_cost_map abstat → clight_cost_map clight ≝
69  λclight,code_memory,lbls,dec,k,asm_cost_map.
70  lift_sigma_map_id … 0 (* labels not present in out code get 0 *)
71    dec k asm_cost_map.
72
73include "ASM/ASMCostsSplit.ma".
74
75definition compile : clight_program →
76  res (object_code × costlabel_map × (𝚺labelled:clight_program. clight_cost_map labelled)) ≝
77λp.
78  ! 〈init_cost,p',p〉 ← front_end p;
79  let p ≝ back_end p in
80    ! p ← assembler p;
81  let k ≝ ASM_cost_map p ? in
82  let k' ≝ lift_cost_map_back_to_front
83    p'
84    (load_code_memory (\fst p))
85    (\snd p)
86    ? k
87    in
88  return 〈p, ❬p', k'❭〉.
89  cases daemon
90  qed.
Note: See TracBrowser for help on using the repository browser.