1 | include "Clight/label.ma". |
---|
2 | include "Clight/SimplifyCasts.ma". |
---|
3 | include "Clight/switchRemoval.ma". |
---|
4 | include "Clight/toCminor.ma". |
---|
5 | include "Cminor/toRTLabs.ma". |
---|
6 | include "RTLabs/CostCheck.ma". |
---|
7 | include "RTLabs/CostInj.ma". |
---|
8 | |
---|
9 | definition 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 | |
---|
24 | include "RTLabs/RTLabsToRTL.ma". |
---|
25 | include "RTL/RTLToERTL.ma". |
---|
26 | include "ERTL/ERTLToERTLptr.ma". |
---|
27 | include "ERTLptr/ERTLptrToLTL.ma". |
---|
28 | include "LTL/LTLToLIN.ma". |
---|
29 | include "LIN/LINToASM.ma". |
---|
30 | |
---|
31 | axiom compute_fixpoint : fixpoint_computer. |
---|
32 | axiom colour_graph : coloured_graph_computer. |
---|
33 | |
---|
34 | definition 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 |
---|
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 | lin_to_asm p. |
---|
42 | |
---|
43 | include "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 | |
---|
52 | definition assembler : pseudo_assembly_program → res labelled_object_code ≝ |
---|
53 | λp. |
---|
54 | let 〈preamble, list_instr〉 ≝ p in |
---|
55 | ! list_instr_ok ← opt_to_res ? (msg AssemblyTooLarge) ?(*(program_ok_opt ? list_instr)*); |
---|
56 | let p' ≝ 〈preamble, list_instr〉 in |
---|
57 | ! sigma_pol ← opt_to_res ? (msg Jump_expansion_failed) (jump_expansion' p'); |
---|
58 | let sigma ≝ λppc. \fst sigma_pol ppc in |
---|
59 | let pol ≝ λppc. \snd sigma_pol ppc in |
---|
60 | OK ? (assembly p sigma pol). |
---|
61 | (* % [1: @list_instr_ok | cases daemon] *) cases daemon |
---|
62 | qed. |
---|
63 | |
---|
64 | include "ASM/ASMCosts.ma". |
---|
65 | |
---|
66 | (*CSC: move the next definitions, e.g. in BitVectorTrie *) |
---|
67 | definition in_codomain: ∀A:Type[0].∀n:nat. BitVectorTrie A n → A → Prop ≝ |
---|
68 | λA,n,m,a. ∃k:BitVector n. lookup_opt … k m = Some … a. |
---|
69 | |
---|
70 | definition strong_decidable: Prop → Type[0] ≝ |
---|
71 | λP:Prop. P + ¬ P. |
---|
72 | |
---|
73 | lemma strong_decidable_in_codomain: |
---|
74 | ∀A:DeqSet.∀n:nat.∀m: BitVectorTrie A n.∀a:A. |
---|
75 | strong_decidable (in_codomain A n m a). |
---|
76 | #A #n #m elim m |
---|
77 | [ normalize #a' #a inversion (a' == a) #H |
---|
78 | [ %1 %{(VEmpty …)} >(\P H) % |
---|
79 | | %2 % * #_ #EQ destruct lapply (\Pf H) /2/ ] |
---|
80 | | -n #n #L #R #Hl #Hr #a |
---|
81 | cases (Hl a) -Hl [#K %1 cases K #k #H %{(false:::k)} <H % ] #Hl |
---|
82 | cases (Hr a) -Hr [#K %1 cases K #k #H %{(true:::k)} <H % ] #Hr |
---|
83 | %2 % * #k cases (BitVector_Sn … k) ** #tl #EQ >EQ whd in ⊢ (??%? → ?); |
---|
84 | normalize nodelta whd in match (tail ???); #abs [ cases Hr | cases Hl ] /3/ |
---|
85 | | #n #A %2 % * #x normalize #abs destruct ] |
---|
86 | qed. |
---|
87 | |
---|
88 | (* can now move this defn to ASM/ASMCosts.ma *) |
---|
89 | definition lift_cost_map_back_to_front : |
---|
90 | ∀clight, code_memory, lbls. |
---|
91 | let abstat ≝ ASM_abstract_status code_memory lbls in |
---|
92 | (* (∀l. (as_cost_labelled abstat l) + ¬(as_cost_labelled abstat l)) → *) |
---|
93 | as_cost_map abstat → clight_cost_map clight ≝ |
---|
94 | λclight,code_memory,lbls,(*dec,*)k,asm_cost_map. |
---|
95 | lift_sigma_map_id … 0 (* labels not present in out code get 0 *) |
---|
96 | (strong_decidable_in_codomain …) (* (* dec *) now eliminated as a hypothesis *) |
---|
97 | k asm_cost_map. |
---|
98 | |
---|
99 | include "ASM/ASMCostsSplit.ma". |
---|
100 | |
---|
101 | definition compile : clight_program → |
---|
102 | res (labelled_object_code × (𝚺labelled:clight_program. clight_cost_map labelled)) ≝ |
---|
103 | λp. |
---|
104 | ! 〈init_cost,p',p〉 ← front_end p; |
---|
105 | let p ≝ back_end p in |
---|
106 | ! p ← assembler p; |
---|
107 | let k ≝ ASM_cost_map p ? in |
---|
108 | let k' ≝ lift_cost_map_back_to_front |
---|
109 | p' |
---|
110 | (load_code_memory (\fst p)) |
---|
111 | (\fst (\snd p)) |
---|
112 | k |
---|
113 | in |
---|
114 | return 〈p, ❬p', k'❭〉. |
---|
115 | cases daemon |
---|
116 | qed. |
---|