source: src/compiler.ma @ 2724

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

Add RTLabs cost labelling checks to compiler.ma.

File size: 3.3 KB
RevLine 
[1991]1include "Clight/label.ma".
[2019]2include "Clight/SimplifyCasts.ma".
[2475]3include "Clight/switchRemoval.ma".
[1991]4include "Clight/toCminor.ma".
5include "Cminor/initialisation.ma".
6include "Cminor/toRTLabs.ma".
[2724]7include "RTLabs/CostCheck.ma".
8include "RTLabs/CostInj.ma".
[1991]9
[2319]10definition front_end : clight_program → res (costlabel × clight_program × RTLabs_program) ≝
[1991]11λp.
[2475]12  let p ≝ program_switch_removal p in
[2319]13  let 〈p',init_cost〉 ≝ clight_label p in
[2001]14  let p ≝ simplify_program p' in
[1991]15  ! p ← clight_to_cminor p;
[2319]16  let p ≝ cminor_to_rtlabs init_cost p in
[2724]17  if check_cost_program p then
18    if check_program_cost_injectivity p then
19      (return 〈init_cost,p',p〉)
20    else
21      (Error ? (msg RepeatedCostLabel))
22  else
23    (Error ? (msg BadCostLabelling)).
[1995]24
[2494]25include "RTLabs/RTLabsToRTL.ma".
[1995]26include "RTL/RTLToERTL.ma".
[2697]27include "ERTL/ERTLToERTLptr.ma".
28include "ERTLptr/ERTLptrToLTL.ma".
[2705]29include "LTL/LTLToLIN.ma".
[1995]30include "LIN/LINToASM.ma".
31
[2700]32axiom compute_fixpoint : fixpoint_computer.
33axiom colour_graph : coloured_graph_computer.
[2505]34
[1995]35definition back_end : RTLabs_program → pseudo_assembly_program ≝
36λp.
37  let p ≝ rtlabs_to_rtl p in
38  let p ≝ rtl_to_ertl p in
[2697]39  let p ≝ ertl_to_ertlptr p in
[2700]40  let p ≝ ertlptr_to_ltl compute_fixpoint colour_graph p in (* TODO: abstract over colouring *)
[1995]41  let p ≝ ltl_to_lin p in
42          lin_to_asm p.
43
[2709]44(* JHM: minimum needed for assembler to typecheck *)
45(* JHM: moved from ASMCostsSplit.ma               *)
46(* JHM: should move elsewhere in ASM/             *)
[2512]47definition object_code ≝ list Byte.
48definition costlabel_map ≝ BitVectorTrie costlabel 16.
[1995]49
[2702]50include "ASM/Policy.ma".
51(* Equivalent to the inclusion of ASM/Policy.ma, waiting for that slow
52   file to compile
53  include "ASM/PolicyStep.ma".
54  axiom jump_expansion': ∀program:preamble × (Σl:list labelled_instruction.lt (S (|l|)) 2^16 ∧ is_well_labelled_p l).
[2700]55 option (Σsigma_policy:(Word → Word) × (Word → bool).
56   let 〈sigma,policy〉≝ sigma_policy in
[2702]57   sigma_policy_specification 〈\fst program,\snd program〉 sigma policy). *)
[2505]58
[1995]59definition assembler : pseudo_assembly_program → res (object_code × costlabel_map) ≝
60λp.
61  let 〈preamble, list_instr〉 ≝ p in
62  (* TODO: fail if p is too large. *)
63  let p' ≝ 〈preamble, list_instr〉 in
64  ! sigma_pol ← opt_to_res ? (msg Jump_expansion_failed) (jump_expansion' p');
[2702]65  let sigma ≝ λppc. \fst sigma_pol ppc in
66  let pol ≝ λppc. \snd sigma_pol ppc in
[1995]67  OK ? (assembly p sigma pol).
68cases daemon
[2497]69qed.
[1995]70
[2505]71include "ASM/ASMCosts.ma".
72
[2001]73definition lift_cost_map_back_to_front :
[2399]74  ∀clight, code_memory, lbls.
[2505]75    let abstat ≝ ASM_abstract_status code_memory lbls in
76   (∀l. (as_cost_labelled abstat l) + ¬(as_cost_labelled abstat l)) →
77  as_cost_map abstat → clight_cost_map clight ≝
78  λclight,code_memory,lbls,dec,k,asm_cost_map.
79  lift_sigma_map_id … 0 (* labels not present in out code get 0 *)
[2508]80    dec k asm_cost_map.
[2001]81
[2505]82include "ASM/ASMCostsSplit.ma".
83
[2001]84definition compile : clight_program →
[2508]85  res (object_code × costlabel_map × (𝚺labelled:clight_program. clight_cost_map labelled)) ≝
[1995]86λp.
[2320]87  ! 〈init_cost,p',p〉 ← front_end p;
[1995]88  let p ≝ back_end p in
[2001]89    ! p ← assembler p;
90  let k ≝ ASM_cost_map p ? in
91  let k' ≝ lift_cost_map_back_to_front
[2399]92    p'
[2001]93    (load_code_memory (\fst p))
94    (\snd p)
95    ? k
96    in
[2399]97  return 〈p, ❬p', k'❭〉.
[2001]98  cases daemon
[2709]99qed.
Note: See TracBrowser for help on using the repository browser.