Changeset 1995
 Timestamp:
 May 24, 2012, 7:18:35 PM (7 years ago)
 Location:
 src
 Files:

 6 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTL/liveness.ma
r1730 r1995 298 298 fix_correct: 299 299 ∀globals: list ident. 300 ∀int_fun. 300 (* ∀int_fun.*) 301 301 ∀f. (* CSC: was let f ≝ liveafter globals int_fun in *) 302 302 ∀v: label. 
src/LIN/LINToASM.ma
r1522 r1995 106 106 [ Cmpl ⇒ Instruction (CPL ? ACC_A) 107 107  Inc ⇒ Instruction (INC ? ACC_A) 108  Rl ⇒ Instruction (RL ? ACC_A) 108 109 ] 109 110  OP2 op2 _ _ reg ⇒ … … 337 338 338 339 (* dpm: fresh prefix stuff needs unifying with brian *) 339 definition translate: lin_program → pseudo_assembly_program ≝340 definition lin_to_asm : lin_program → pseudo_assembly_program ≝ 340 341 λp. 341 342 let prog_lbls ≝ program_labels … p in 
src/RTL/RTLToERTL.ma
r1601 r1995 4 4 include "ERTL/ERTL.ma". 5 5 include "joint/TranslateUtils.ma". 6 7 include alias "basics/lists/list.ma". 6 8 7 9 definition save_hdws ≝ … … 412 414 definition translate_funct ≝ λglobals,def. (move_first_cost_label_up_internal … (translate_funct_internal globals def)). 413 415 414 definition translate: rtl_program → ertl_program ≝416 definition rtl_to_ertl : rtl_program → ertl_program ≝ 415 417 λp. 416 418 let p ≝ tailcall_simplify p in (* tailcall simplification here *) 
src/RTLabs/RTLabsToRTL.ma
r1601 r1995 212 212 qed. 213 213 214 (* Type safety in RTLabs has broken this for the moment... 214 215 let rec translate_cst 215 216 (globals: list ident) (cst: constant) (destrs: list register) … … 1251 1252 definition rtlabs_to_rtl: RTLabs_program → rtl_program ≝ 1252 1253 λp. transform_program … p (transf_fundef … (translate_internal (prog_var_names …))). 1254 1255 *) 1256 axiom rtlabs_to_rtl: RTLabs_program → rtl_program. 1257 
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 
src/joint/TranslateUtils.ma
r1599 r1995 22 22 [ % 23 23  #m whd in ⊢ (? → ??(??(???%))?); @pair_elim 24 #def' #regs #EQ >EQ normalize // ]24 #def' #regs #EQ >EQ cases (fresh_reg ???) normalize // ] 25 25 qed. 26 26
Note: See TracChangeset
for help on using the changeset viewer.