Changeset 1995


Ignore:
Timestamp:
May 24, 2012, 7:18:35 PM (5 years ago)
Author:
campbell
Message:

Overall compiler definition; bits and pieces to
make everything happy(ish).

Location:
src
Files:
6 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/liveness.ma

    r1730 r1995  
    298298  fix_correct:
    299299    ∀globals: list ident.
    300     ∀int_fun.
     300(*    ∀int_fun.*)
    301301    ∀f. (* CSC: was let f ≝ liveafter globals int_fun in *)
    302302      ∀v: label.
  • src/LIN/LINToASM.ma

    r1522 r1995  
    106106        [ Cmpl ⇒ Instruction (CPL ? ACC_A)
    107107        | Inc ⇒ Instruction (INC ? ACC_A)
     108        | Rl ⇒ Instruction (RL ? ACC_A)
    108109        ]
    109110      | OP2 op2 _ _ reg ⇒
     
    337338
    338339(* dpm: fresh prefix stuff needs unifying with brian *)
    339 definition translate : lin_program → pseudo_assembly_program ≝
     340definition lin_to_asm : lin_program → pseudo_assembly_program ≝
    340341  λp.
    341342  let prog_lbls ≝ program_labels … p in
  • src/RTL/RTLToERTL.ma

    r1601 r1995  
    44include "ERTL/ERTL.ma".
    55include "joint/TranslateUtils.ma".
     6
     7include alias "basics/lists/list.ma".
    68
    79definition save_hdws ≝
     
    412414definition translate_funct ≝ λglobals,def. (move_first_cost_label_up_internal … (translate_funct_internal globals def)).
    413415
    414 definition translate : rtl_program → ertl_program ≝
     416definition rtl_to_ertl : rtl_program → ertl_program ≝
    415417 λp.
    416418  let p ≝ tailcall_simplify p in (* tailcall simplification here *)
  • src/RTLabs/RTLabsToRTL.ma

    r1601 r1995  
    212212qed.
    213213
     214(* Type safety in RTLabs has broken this for the moment...
    214215let rec translate_cst
    215216  (globals: list ident) (cst: constant) (destrs: list register)
     
    12511252definition rtlabs_to_rtl: RTLabs_program → rtl_program ≝
    12521253 λp. transform_program … p (transf_fundef … (translate_internal (prog_var_names …))).
     1254
     1255*)
     1256axiom rtlabs_to_rtl: RTLabs_program → rtl_program.
     1257
  • src/compiler.ma

    r1991 r1995  
    1313  let p ≝ program_switch_removal p in
    1414  ! p ← clight_to_cminor p;
    15   cminor_to_rtlabs p.
     15        cminor_to_rtlabs p.
     16
     17include "RTLabs/RTLabsToRTL.ma".
     18include "RTL/RTLToERTL.ma".
     19include "ERTL/ERTLToLTL.ma".
     20include "LTL/LTLToLIN.ma".
     21include "LIN/LINToASM.ma".
     22
     23axiom the_fixpoint : fixpoint.
     24axiom build : ∀valuation. coloured_graph valuation.
     25
     26definition 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
     34include "ASM/Assembly.ma".
     35
     36definition object_code ≝ list Byte.
     37definition costlabel_map ≝ BitVectorTrie costlabel 16.
     38
     39include "ASM/Policy.ma".
     40
     41axiom Jump_expansion_failed : String.
     42
     43definition 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).
     52cases daemon
     53qed.
     54
     55definition 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  
    2222  [ %
    2323  | #m whd in ⊢ (? → ??(??(???%))?); @pair_elim
    24     #def' #regs #EQ >EQ normalize // ]
     24    #def' #regs #EQ >EQ cases (fresh_reg ???) normalize // ]
    2525qed.
    2626
Note: See TracChangeset for help on using the changeset viewer.