source: src/compiler.ma @ 2709

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

LINToAsm repaired

File size: 3.1 KB
Line 
1include "Clight/label.ma".
2include "Clight/SimplifyCasts.ma".
3include "Clight/switchRemoval.ma".
4include "Clight/toCminor.ma".
5include "Cminor/initialisation.ma".
6include "Cminor/toRTLabs.ma".
7
8definition front_end : clight_program → res (costlabel × clight_program × RTLabs_program) ≝
9λp.
10  let p ≝ program_switch_removal p in
11  let 〈p',init_cost〉 ≝ clight_label p in
12  let p ≝ simplify_program p' in
13  ! p ← clight_to_cminor p;
14  let p ≝ cminor_to_rtlabs init_cost p in
15  return 〈init_cost,p',p〉.
16
17include "RTLabs/RTLabsToRTL.ma".
18include "RTL/RTLToERTL.ma".
19include "ERTL/ERTLToERTLptr.ma".
20include "ERTLptr/ERTLptrToLTL.ma".
21include "LTL/LTLToLIN.ma".
22include "LIN/LINToASM.ma".
23
24axiom compute_fixpoint : fixpoint_computer.
25axiom colour_graph : coloured_graph_computer.
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_ertlptr p in
32  let p ≝ ertlptr_to_ltl compute_fixpoint colour_graph p in (* TODO: abstract over colouring *)
33  let p ≝ ltl_to_lin p in
34          lin_to_asm p.
35
36(* JHM: minimum needed for assembler to typecheck *)
37(* JHM: moved from ASMCostsSplit.ma               *)
38(* JHM: should move elsewhere in ASM/             *)
39definition object_code ≝ list Byte.
40definition costlabel_map ≝ BitVectorTrie costlabel 16.
41
42include "ASM/Policy.ma".
43(* Equivalent to the inclusion of ASM/Policy.ma, waiting for that slow
44   file to compile
45  include "ASM/PolicyStep.ma".
46  axiom jump_expansion': ∀program:preamble × (Σl:list labelled_instruction.lt (S (|l|)) 2^16 ∧ is_well_labelled_p l).
47 option (Σsigma_policy:(Word → Word) × (Word → bool).
48   let 〈sigma,policy〉≝ sigma_policy in
49   sigma_policy_specification 〈\fst program,\snd program〉 sigma policy). *)
50
51definition assembler : pseudo_assembly_program → res (object_code × costlabel_map) ≝
52λp.
53  let 〈preamble, list_instr〉 ≝ p in
54  (* TODO: fail if p is too large. *)
55  let p' ≝ 〈preamble, list_instr〉 in
56  ! sigma_pol ← opt_to_res ? (msg Jump_expansion_failed) (jump_expansion' p');
57  let sigma ≝ λppc. \fst sigma_pol ppc in
58  let pol ≝ λppc. \snd sigma_pol ppc in
59  OK ? (assembly p sigma pol).
60cases daemon
61qed.
62
63include "ASM/ASMCosts.ma".
64
65definition lift_cost_map_back_to_front :
66  ∀clight, code_memory, lbls.
67    let abstat ≝ ASM_abstract_status code_memory lbls in
68   (∀l. (as_cost_labelled abstat l) + ¬(as_cost_labelled abstat l)) →
69  as_cost_map abstat → clight_cost_map clight ≝
70  λclight,code_memory,lbls,dec,k,asm_cost_map.
71  lift_sigma_map_id … 0 (* labels not present in out code get 0 *)
72    dec k asm_cost_map.
73
74include "ASM/ASMCostsSplit.ma".
75
76definition compile : clight_program →
77  res (object_code × costlabel_map × (𝚺labelled:clight_program. clight_cost_map labelled)) ≝
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
91qed.
Note: See TracBrowser for help on using the repository browser.