Changeset 1107


Ignore:
Timestamp:
Aug 24, 2011, 2:43:58 PM (8 years ago)
Author:
mulligan
Message:

got rtl-ertl pass working again

Location:
src
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL.ma

    r1084 r1107  
    3232  | ertl_st_load: register → register → register → label → ertl_statement
    3333  | ertl_st_store: register → register → register → label → ertl_statement
    34   | ertl_st_call_id: label → Byte → label → ertl_statement
     34  | ertl_st_call_id: ident → Byte → label → ertl_statement
    3535  | ertl_st_cond: register → label → label → ertl_statement
    36   | ertl_st_return: label → ertl_statement.
     36  | ertl_st_return: ertl_statement.
    3737
    3838definition ertl_statement_graph ≝ graph ertl_statement.
  • src/ERTL/liveness.ma

    r1094 r1107  
    1 
     1include "utilities/Fix.ma".
    22include "ASM/Util.ma".
    33include "ERTL/ERTL.ma".
     
    3131    foldr ? ? andb true (map ? ? (λx. member A eq_a x r) l).
    3232
    33 definition list_set_member ≝
    34   λA: Type[0].
    35   λeq_a: A → A → bool.
    36   λa: A.
    37   λl: list A.
    38     member A eq_a a l.
     33definition list_set_member ≝ member.
     34
     35definition list_set_fold ≝ foldr.
    3936
    4037definition statement_successors ≝
     
    303300    | Some stmt ⇒ statement_semantics stmt (liveafter label)
    304301    ]
     302  in
     303  let liveafter ≝ λlabel. λliveafter: valuation.
     304    match lookup ? ? (ertl_if_graph int_fun) label with
     305    [ None      ⇒ ?
     306    | Some stmt ⇒ list_set_fold ? ? (λsuccessor. λaccu.
     307        lattice_join (livebefore successor liveafter) accu)
     308        lattice_bottom (statement_successors stmt)
     309    ]
    305310  in ?.
  • src/RTL/RTLtoERTL.ma

    r1081 r1107  
    190190 
    191191definition save_hdws_internal ≝
    192   λdestr_srcr: register × hardware_register.
     192  λdestr_srcr: register × Register.
    193193  λstart_lbl: label.
    194194    let 〈destr, srcr〉 ≝ destr_srcr in
     
    200200   
    201201definition restore_hdws_internal ≝
    202   λdestr_srcr: hardware_register × register.
     202  λdestr_srcr: Register × register.
    203203  λstart_lbl: label.
    204204    let 〈destr, srcr〉 ≝ destr_srcr in
Note: See TracChangeset for help on using the changeset viewer.