source: src/compiler.ma @ 2771

Last change on this file since 2771 was 2767, checked in by mckinna, 7 years ago

WARNING: BIG commit, which pushes code_size_opt check into LIN/LINToASM.ma
following CSC's comment on my previous partial commit
plus rolls all the miscellaneous code motion into the rest of the repo.

suggest REBUILD compiler.ma/correctness.ma from scratch.

File size: 2.9 KB
Line 
1include "Clight/label.ma".
2include "Clight/SimplifyCasts.ma".
3include "Clight/switchRemoval.ma".
4include "Clight/toCminor.ma".
5include "Cminor/toRTLabs.ma".
6include "RTLabs/CostCheck.ma".
7include "RTLabs/CostInj.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  if check_cost_program p then
17    if check_program_cost_injectivity p then
18      (return 〈init_cost,p',p〉)
19    else
20      (Error ? (msg RepeatedCostLabel))
21  else
22    (Error ? (msg BadCostLabelling)).
23
24include "RTLabs/RTLabsToRTL.ma".
25include "RTL/RTLToERTL.ma".
26include "ERTL/ERTLToERTLptr.ma".
27include "ERTLptr/ERTLptrToLTL.ma".
28include "LTL/LTLToLIN.ma".
29include "LIN/LINToASM.ma".
30
31axiom compute_fixpoint : fixpoint_computer.
32axiom colour_graph : coloured_graph_computer.
33
34definition back_end : RTLabs_program → res pseudo_assembly_program ≝
35λp.
36  let p ≝ rtlabs_to_rtl p in
37  let p ≝ rtl_to_ertl p in
38  let p ≝ ertl_to_ertlptr p in
39  let p ≝ ertlptr_to_ltl compute_fixpoint colour_graph p in (* TODO: abstract over colouring *)
40  let p ≝ ltl_to_lin p in
41          opt_to_res ? (msg AssemblyTooLarge) (lin_to_asm p).
42
43include "ASM/Policy.ma".
44(* Equivalent to the inclusion of ASM/Policy.ma, waiting for that slow
45   file to compile
46  include "ASM/PolicyStep.ma".
47  axiom jump_expansion': ∀program:preamble × (Σl:list labelled_instruction.lt (S (|l|)) 2^16 ∧ is_well_labelled_p l).
48 option (Σsigma_policy:(Word → Word) × (Word → bool).
49   let 〈sigma,policy〉≝ sigma_policy in
50   sigma_policy_specification 〈\fst program,\snd program〉 sigma policy). *)
51   
52definition assembler : pseudo_assembly_program → res labelled_object_code ≝
53λp.
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).
58
59include "ASM/ASMCosts.ma".
60
61(*CSC: move the next definitions, e.g. in BitVectorTrie; JHM: done! *)
62
63definition lift_cost_map_back_to_front :
64  ∀clight, code_memory, lbls.
65    let abstat ≝ ASM_abstract_status code_memory lbls in
66  as_cost_map abstat → clight_cost_map clight ≝
67  λclight,code_memory,lbls,k,asm_cost_map.
68  lift_sigma_map_id … 0 (* labels not present in out code get 0 *)
69    (strong_decidable_in_codomain …) k asm_cost_map.
70
71include "ASM/ASMCostsSplit.ma".
72
73definition compile : clight_program →
74  res (labelled_object_code × (𝚺labelled:clight_program. clight_cost_map labelled)) ≝
75λp.
76  ! 〈init_cost,p',p〉 ← front_end p;
77  ! p ← back_end p;
78  ! p ← assembler p;
79  let k ≝ ASM_cost_map p in
80  let k' ≝
81   lift_cost_map_back_to_front p' (load_code_memory (oc p)) (costlabels p) k in
82  return 〈p, ❬p', k'❭〉.
Note: See TracBrowser for help on using the repository browser.