source: src/compiler.ma @ 2752

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

Fixed TODO regarding length of list_instr
Added ASM/CodeMemory.ma to incorporate miscellany on program size, memory etc.
Added final(?) error message

File size: 4.1 KB
RevLine 
[1991]1include "Clight/label.ma".
[2019]2include "Clight/SimplifyCasts.ma".
[2475]3include "Clight/switchRemoval.ma".
[1991]4include "Clight/toCminor.ma".
5include "Cminor/toRTLabs.ma".
[2724]6include "RTLabs/CostCheck.ma".
7include "RTLabs/CostInj.ma".
[1991]8
[2319]9definition front_end : clight_program → res (costlabel × clight_program × RTLabs_program) ≝
[1991]10λp.
[2475]11  let p ≝ program_switch_removal p in
[2319]12  let 〈p',init_cost〉 ≝ clight_label p in
[2001]13  let p ≝ simplify_program p' in
[1991]14  ! p ← clight_to_cminor p;
[2319]15  let p ≝ cminor_to_rtlabs init_cost p in
[2724]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)).
[1995]23
[2494]24include "RTLabs/RTLabsToRTL.ma".
[1995]25include "RTL/RTLToERTL.ma".
[2697]26include "ERTL/ERTLToERTLptr.ma".
27include "ERTLptr/ERTLptrToLTL.ma".
[2705]28include "LTL/LTLToLIN.ma".
[1995]29include "LIN/LINToASM.ma".
30
[2700]31axiom compute_fixpoint : fixpoint_computer.
32axiom colour_graph : coloured_graph_computer.
[2505]33
[1995]34definition back_end : RTLabs_program → pseudo_assembly_program ≝
35λp.
36  let p ≝ rtlabs_to_rtl p in
37  let p ≝ rtl_to_ertl p in
[2697]38  let p ≝ ertl_to_ertlptr p in
[2700]39  let p ≝ ertlptr_to_ltl compute_fixpoint colour_graph p in (* TODO: abstract over colouring *)
[1995]40  let p ≝ ltl_to_lin p in
41          lin_to_asm p.
42
[2752]43(* JHM: object_code and program_size_ok defns added *)
44include "ASM/CodeMemory.ma".
[1995]45
[2702]46include "ASM/Policy.ma".
47(* Equivalent to the inclusion of ASM/Policy.ma, waiting for that slow
48   file to compile
49  include "ASM/PolicyStep.ma".
50  axiom jump_expansion': ∀program:preamble × (Σl:list labelled_instruction.lt (S (|l|)) 2^16 ∧ is_well_labelled_p l).
[2700]51 option (Σsigma_policy:(Word → Word) × (Word → bool).
52   let 〈sigma,policy〉≝ sigma_policy in
[2702]53   sigma_policy_specification 〈\fst program,\snd program〉 sigma policy). *)
[2752]54   
[1995]55definition assembler : pseudo_assembly_program → res (object_code × costlabel_map) ≝
56λp.
57  let 〈preamble, list_instr〉 ≝ p in
[2752]58  ! list_instr_ok ← opt_to_res ? (msg AssemblyTooLarge) (program_ok_opt ? list_instr);
[1995]59  let p' ≝ 〈preamble, list_instr〉 in
60  ! sigma_pol ← opt_to_res ? (msg Jump_expansion_failed) (jump_expansion' p');
[2702]61  let sigma ≝ λppc. \fst sigma_pol ppc in
62  let pol ≝ λppc. \snd sigma_pol ppc in
[1995]63  OK ? (assembly p sigma pol).
[2752]64  % [1: @list_instr_ok | cases daemon]
[2497]65qed.
[1995]66
[2505]67include "ASM/ASMCosts.ma".
68
[2001]69definition lift_cost_map_back_to_front :
[2399]70  ∀clight, code_memory, lbls.
[2505]71    let abstat ≝ ASM_abstract_status code_memory lbls in
72   (∀l. (as_cost_labelled abstat l) + ¬(as_cost_labelled abstat l)) →
73  as_cost_map abstat → clight_cost_map clight ≝
74  λclight,code_memory,lbls,dec,k,asm_cost_map.
75  lift_sigma_map_id … 0 (* labels not present in out code get 0 *)
[2508]76    dec k asm_cost_map.
[2001]77
[2505]78include "ASM/ASMCostsSplit.ma".
79
[2745]80(*CSC: move the next definitions, e.g. in BitVectorTrie *)
81definition in_codomain: ∀A:Type[0].∀n:nat. BitVectorTrie A n → A → Prop ≝
82 λA,n,m,a. ∃k:BitVector n. lookup_opt … k m = Some … a.
83
84definition strong_decidable: Prop → Type[0] ≝
85 λP:Prop. P + ¬ P.
86
87lemma strong_decidable_in_codomain:
88 ∀A:DeqSet.∀n:nat.∀m: BitVectorTrie A n.∀a:A.
89  strong_decidable (in_codomain A n m a).
90 #A #n #m elim m
91 [ normalize #a' #a inversion (a' == a) #H
92   [ %1 %{(VEmpty …)} >(\P H) %
93   | %2 % * #_ #EQ destruct lapply (\Pf H) /2/ ]
94 | -n #n #L #R #Hl #Hr #a
95   cases (Hl a) -Hl [#K %1 cases K #k #H %{(false:::k)} <H % ] #Hl
96   cases (Hr a) -Hr [#K %1 cases K #k #H %{(true:::k)}  <H % ] #Hr
97   %2 % * #k cases (BitVector_Sn … k) ** #tl #EQ >EQ whd in ⊢ (??%? → ?);
98   normalize nodelta whd in match (tail ???); #abs [ cases Hr | cases Hl ] /3/
99 | #n #A %2 % * #x normalize #abs destruct ]
100qed.
101
[2001]102definition compile : clight_program →
[2508]103  res (object_code × costlabel_map × (𝚺labelled:clight_program. clight_cost_map labelled)) ≝
[1995]104λp.
[2320]105  ! 〈init_cost,p',p〉 ← front_end p;
[1995]106  let p ≝ back_end p in
[2001]107    ! p ← assembler p;
108  let k ≝ ASM_cost_map p ? in
109  let k' ≝ lift_cost_map_back_to_front
[2399]110    p'
[2001]111    (load_code_memory (\fst p))
112    (\snd p)
113    ? k
114    in
[2399]115  return 〈p, ❬p', k'❭〉.
[2745]116 [ @strong_decidable_in_codomain
117 | cases daemon ]
[2709]118qed.
Note: See TracBrowser for help on using the repository browser.