[1991] | 1 | |
---|
| 2 | include "Clight/label.ma". |
---|
[2019] | 3 | include "Clight/SimplifyCasts.ma". |
---|
[1991] | 4 | include "Clight/switchRemoval.ma". |
---|
| 5 | include "Clight/toCminor.ma". |
---|
| 6 | include "Cminor/initialisation.ma". |
---|
| 7 | include "Cminor/toRTLabs.ma". |
---|
| 8 | |
---|
[2001] | 9 | definition front_end : clight_program → res (clight_program × RTLabs_program) ≝ |
---|
[1991] | 10 | λp. |
---|
[2001] | 11 | let p' ≝ clight_label p in |
---|
| 12 | let p ≝ simplify_program p' in |
---|
[1991] | 13 | let p ≝ program_switch_removal p in |
---|
| 14 | ! p ← clight_to_cminor p; |
---|
[2001] | 15 | ! p ← cminor_to_rtlabs p; |
---|
| 16 | return 〈p',p〉. |
---|
[1995] | 17 | |
---|
| 18 | include "RTLabs/RTLabsToRTL.ma". |
---|
| 19 | include "RTL/RTLToERTL.ma". |
---|
| 20 | include "ERTL/ERTLToLTL.ma". |
---|
| 21 | include "LTL/LTLToLIN.ma". |
---|
| 22 | include "LIN/LINToASM.ma". |
---|
| 23 | |
---|
| 24 | axiom the_fixpoint : fixpoint. |
---|
| 25 | axiom build : ∀valuation. coloured_graph valuation. |
---|
| 26 | |
---|
| 27 | definition 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_ltl p in (* TODO: abstract over colouring *) |
---|
| 32 | let p ≝ ltl_to_lin p in |
---|
| 33 | lin_to_asm p. |
---|
| 34 | |
---|
| 35 | include "ASM/Assembly.ma". |
---|
| 36 | |
---|
| 37 | include "ASM/Policy.ma". |
---|
| 38 | |
---|
| 39 | axiom Jump_expansion_failed : String. |
---|
| 40 | |
---|
[2001] | 41 | include "ASM/ASMCostsSplit.ma". |
---|
| 42 | |
---|
[2205] | 43 | axiom assembler : pseudo_assembly_program → res (object_code × costlabel_map). (* |
---|
[1995] | 44 | definition assembler : pseudo_assembly_program → res (object_code × costlabel_map) ≝ |
---|
| 45 | λp. |
---|
| 46 | let 〈preamble, list_instr〉 ≝ p in |
---|
| 47 | (* TODO: fail if p is too large. *) |
---|
| 48 | let p' ≝ 〈preamble, list_instr〉 in |
---|
| 49 | ! sigma_pol ← opt_to_res ? (msg Jump_expansion_failed) (jump_expansion' p'); |
---|
| 50 | let sigma ≝ λppc. \fst (sigma_pol ppc) in |
---|
| 51 | let pol ≝ λppc. \snd (sigma_pol ppc) in |
---|
| 52 | OK ? (assembly p sigma pol). |
---|
| 53 | cases daemon |
---|
[2205] | 54 | qed.*) |
---|
[1995] | 55 | |
---|
[2001] | 56 | include "RTLabs/semantics.ma". |
---|
| 57 | |
---|
| 58 | axiom RTLabs_abstract_status : genv → abstract_status. |
---|
| 59 | |
---|
| 60 | include "joint/semantics.ma". |
---|
| 61 | axiom joint_abstract_status : |
---|
| 62 | ∀globals.∀p:params globals.genv globals p → abstract_status. |
---|
| 63 | |
---|
| 64 | include "common/StructuredTraces.ma". |
---|
[2116] | 65 | include "ASM/Fetch.ma". (* For load_code_memory only *) |
---|
[2001] | 66 | |
---|
| 67 | definition in_clight_program : costlabel → Prop ≝ λ_.True. |
---|
| 68 | |
---|
| 69 | definition lift_cost_map_back_to_front : |
---|
| 70 | ∀code_memory, lbls. |
---|
| 71 | (∀l. (∃pc.as_label_of_pc (ASM_abstract_status code_memory lbls) pc = Some … l) + |
---|
| 72 | ¬(∃pc.as_label_of_pc (ASM_abstract_status code_memory lbls) pc = Some … l)) → |
---|
| 73 | as_cost_map (ASM_abstract_status code_memory lbls) → |
---|
| 74 | (Σl : costlabel.in_clight_program l) → ℕ ≝ λcode_memory,lbls,dec,k,l_sig. |
---|
| 75 | match dec l_sig with |
---|
| 76 | [ inl prf ⇒ k «l_sig, prf» |
---|
| 77 | | inr _ ⇒ 0 (* labels not present in out code get 0 *) |
---|
| 78 | ]. |
---|
| 79 | |
---|
| 80 | definition compile : clight_program → |
---|
| 81 | res (object_code × costlabel_map × clight_program × ((Σl.in_clight_program l) → ℕ)) ≝ |
---|
[1995] | 82 | λp. |
---|
[2001] | 83 | ! 〈p',p〉 ← front_end p; |
---|
[1995] | 84 | let p ≝ back_end p in |
---|
[2001] | 85 | ! p ← assembler p; |
---|
| 86 | let k ≝ ASM_cost_map p ? in |
---|
| 87 | let k' ≝ lift_cost_map_back_to_front |
---|
| 88 | (load_code_memory (\fst p)) |
---|
| 89 | (\snd p) |
---|
| 90 | ? k |
---|
| 91 | in |
---|
| 92 | return 〈p, p', k'〉. |
---|
| 93 | cases daemon |
---|
| 94 | qed. |
---|
[1995] | 95 | |
---|