Changeset 1995 for src/compiler.ma
- Timestamp:
- May 24, 2012, 7:18:35 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/compiler.ma
r1991 r1995 13 13 let p ≝ program_switch_removal p in 14 14 ! p ← clight_to_cminor p; 15 cminor_to_rtlabs p. 15 cminor_to_rtlabs p. 16 17 include "RTLabs/RTLabsToRTL.ma". 18 include "RTL/RTLToERTL.ma". 19 include "ERTL/ERTLToLTL.ma". 20 include "LTL/LTLToLIN.ma". 21 include "LIN/LINToASM.ma". 22 23 axiom the_fixpoint : fixpoint. 24 axiom build : ∀valuation. coloured_graph valuation. 25 26 definition back_end : RTLabs_program → pseudo_assembly_program ≝ 27 λp. 28 let p ≝ rtlabs_to_rtl p in 29 let p ≝ rtl_to_ertl p in 30 let p ≝ ertl_to_ltl p in (* TODO: abstract over colouring *) 31 let p ≝ ltl_to_lin p in 32 lin_to_asm p. 33 34 include "ASM/Assembly.ma". 35 36 definition object_code ≝ list Byte. 37 definition costlabel_map ≝ BitVectorTrie costlabel 16. 38 39 include "ASM/Policy.ma". 40 41 axiom Jump_expansion_failed : String. 42 43 definition assembler : pseudo_assembly_program → res (object_code × costlabel_map) ≝ 44 λp. 45 let 〈preamble, list_instr〉 ≝ p in 46 (* TODO: fail if p is too large. *) 47 let p' ≝ 〈preamble, list_instr〉 in 48 ! sigma_pol ← opt_to_res ? (msg Jump_expansion_failed) (jump_expansion' p'); 49 let sigma ≝ λppc. \fst (sigma_pol ppc) in 50 let pol ≝ λppc. \snd (sigma_pol ppc) in 51 OK ? (assembly p sigma pol). 52 cases daemon 53 qed. 54 55 definition compile : clight_program → res (object_code × costlabel_map) ≝ 56 λp. 57 ! p ← front_end p; 58 let p ≝ back_end p in 59 assembler p. 60 61 62
Note: See TracChangeset
for help on using the changeset viewer.