Ignore:
Timestamp:
Aug 30, 2011, 6:55:12 PM (8 years ago)
Author:
campbell
Message:

Merge trunk into branch.

Location:
Deliverables/D3.3/id-lookup-branch
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/id-lookup-branch

  • Deliverables/D3.3/id-lookup-branch/ERTL/liveness.ma

    r1109 r1153  
    1 include "utilities/Fix.ma".
    21include "ASM/Util.ma".
    32include "ERTL/ERTL.ma".
     
    3837  λs: ertl_statement.
    3938  match s with
    40   [ ertl_st_return _ ⇒ [ ]
     39  [ ertl_st_return ⇒ [ ]
    4140  | ertl_st_skip l ⇒ [ l ]
    4241  | ertl_st_comment c l ⇒ [ l ]
     
    5049  | ertl_st_push _ l ⇒ [ l ]
    5150  | ertl_st_pop _ l ⇒ [ l ]
    52   | ertl_st_addr_h _ _ l ⇒ [ l ]
    53   | ertl_st_addr_l _ _ l ⇒ [ l ]
     51  | ertl_st_addr _ _ _ l ⇒ [ l ]
    5452  | ertl_st_int _ _ l ⇒ [ l ]
    5553  | ertl_st_move _ _ l ⇒ [ l ]
    56   | ertl_st_opaccs_a _ _ _ _ l ⇒ [ l ]
    57   | ertl_st_opaccs_b _ _ _ _ l ⇒ [ l ]
     54  | ertl_st_opaccs _ _ _ _ _ l ⇒ [ l ]
    5855  | ertl_st_op1 _ _ _ l ⇒ [ l ]
    5956  | ertl_st_op2 _ _ _ _ l ⇒ [ l ]
     
    10097definition lattice_is_maximal: register_lattice → bool ≝ λl. false.
    10198
     99record lattice_property_sig: Type[1] ≝
     100{
     101  lp_type      : Type[0];
     102  lp_property  : Type[0];
     103  lp_bottom    : lp_type;
     104  lp_psingleton: register → lp_type;
     105  lp_hsingleton: Register → lp_type;
     106  lp_join      : lp_type → lp_type → lp_type;
     107  lp_diff      : lp_type → lp_type → lp_type;
     108  lp_equal     : lp_type → lp_type → bool;
     109  lp_is_maximal: lp_type → bool
     110}.
     111
     112definition property ≝
     113  mk_lattice_property_sig
     114    ((list register) × (list Register))
     115    lattice_property
     116    lattice_bottom
     117    lattice_psingleton
     118    lattice_hsingleton
     119    lattice_join
     120    lattice_diff
     121    lattice_equal
     122    lattice_is_maximal.
     123
    102124definition defined: ertl_statement → register_lattice ≝
    103125  λs.
     
    109131  | ertl_st_store _ _ _ _ ⇒ lattice_bottom
    110132  | ertl_st_cond _ _ _ ⇒ lattice_bottom
    111   | ertl_st_return _ ⇒ lattice_bottom
     133  | ertl_st_return ⇒ lattice_bottom
    112134  | ertl_st_clear_carry _ ⇒ lattice_hsingleton RegisterCarry
    113135  | ertl_st_set_carry _ ⇒ lattice_hsingleton RegisterCarry
     
    124146  | ertl_st_pop r _ ⇒ lattice_psingleton r
    125147  | ertl_st_int r _ _ ⇒ lattice_psingleton r
    126   | ertl_st_addr_h r _ _ ⇒ lattice_psingleton r
    127   | ertl_st_addr_l r _ _ ⇒ lattice_psingleton r
     148  | ertl_st_addr r1 r2 _ _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    128149  | ertl_st_move r _ _ ⇒ lattice_psingleton r
    129   | ertl_st_opaccs_a _ r _ _ _ ⇒ lattice_psingleton r
    130   | ertl_st_opaccs_b _ r _ _ _ ⇒ lattice_psingleton r
     150  (* XXX: change from o'caml *)
     151  | ertl_st_opaccs _ r1 r2 _ _ _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    131152  | ertl_st_load r _ _ _ ⇒ lattice_psingleton r
    132153  | ertl_st_set_hdw r _ _ ⇒ lattice_hsingleton r
     
    156177  | ertl_st_frame_size _ _ ⇒ lattice_bottom
    157178  | ertl_st_pop _ _ ⇒ lattice_bottom
    158   | ertl_st_addr_h _ _ _ ⇒ lattice_bottom
    159   | ertl_st_addr_l _ _ _ ⇒ lattice_bottom
     179  | ertl_st_addr _ _ _ _ ⇒ lattice_bottom
    160180  | ertl_st_int _ _ _ ⇒ lattice_bottom
    161181  | ertl_st_clear_carry _ ⇒ lattice_bottom
     
    163183    (* Reads the hardware registers that are used to pass parameters. *)
    164184  | ertl_st_call_id _ nparams _ ⇒
    165     〈[ ], list_set_of_list (prefix ? (nat_of_bitvector ? nparams) RegisterParameters)〉
     185    〈[ ], list_set_of_list (prefix ? nparams RegisterParameters)〉
    166186  | ertl_st_get_hdw _ r _ ⇒ lattice_hsingleton r
    167187  | ertl_st_hdw_to_hdw _ r _ ⇒ lattice_hsingleton r
     
    177197    | _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    178198    ]
    179   | ertl_st_opaccs_a _ _ r1 r2 _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    180   | ertl_st_opaccs_b _ _ r1 r2 _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
     199  | ertl_st_opaccs _ d1 d2 s1 s2 _ ⇒ lattice_join (lattice_psingleton s1) (lattice_psingleton s2)
    181200  | ertl_st_load _ r1 r2 _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    182201  | ertl_st_store r1 r2 r3 _ ⇒
     
    184203  | ertl_st_new_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
    185204  | ertl_st_del_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
    186   | ertl_st_return _ ⇒ 〈[ ], list_set_union ? eq_Register RegisterCalleeSaved ret_regs〉
     205  | ertl_st_return ⇒ 〈[ ], list_set_union ? eq_Register RegisterCalleeSaved ret_regs〉
    187206  ].
    188207
     
    204223  | ertl_st_call_id _ _ _ ⇒ None ?
    205224  | ertl_st_cond _ _ _ ⇒ None ?
    206   | ertl_st_return _ ⇒ None ?
     225  | ertl_st_return ⇒ None ?
    207226  | ertl_st_get_hdw r _ l ⇒
    208227    if list_set_member register (eq_identifier ?) r pliveafter ∨
     
    223242    else
    224243      Some ? l
    225   | ertl_st_addr_h r _ l ⇒
    226     if list_set_member register (eq_identifier ?) r pliveafter ∨
    227        list_set_member Register eq_Register RegisterCarry hliveafter then
    228       None ?
    229     else
    230       Some ? l
    231   | ertl_st_addr_l r _ l ⇒
    232     if list_set_member register (eq_identifier ?) r pliveafter ∨
     244  | ertl_st_addr r1 r2 _ l ⇒
     245    if list_set_member register (eq_identifier ?) r1 pliveafter ∨
     246       list_set_member register (eq_identifier ?) r2 pliveafter ∨
    233247       list_set_member Register eq_Register RegisterCarry hliveafter then
    234248      None ?
     
    241255    else
    242256      Some ? l
    243   | ertl_st_opaccs_a _ r _ _ l ⇒
    244     if list_set_member register (eq_identifier ?) r pliveafter ∨
    245        list_set_member Register eq_Register RegisterCarry hliveafter then
    246       None ?
    247     else
    248       Some ? l
    249   | ertl_st_opaccs_b _ r _ _ l ⇒
    250     if list_set_member register (eq_identifier ?) r pliveafter ∨
     257  | ertl_st_opaccs _ d1 d2 _ _ l ⇒
     258    if list_set_member register (eq_identifier ?) d1 pliveafter ∨
     259       list_set_member register (eq_identifier ?) d2 pliveafter ∨
    251260       list_set_member Register eq_Register RegisterCarry hliveafter then
    252261      None ?
     
    292301
    293302definition valuation ≝ label → register_lattice.
     303definition rhs ≝ valuation → lattice_property.
     304definition equations ≝ label → rhs.
     305
     306axiom fix_lfp: equations → valuation.
     307
     308definition livebefore ≝
     309  λint_fun.
     310  λlabel.
     311  λliveafter: valuation.
     312  match lookup ? ? (ertl_if_graph int_fun) label with
     313  [ None      ⇒ ?
     314  | Some stmt ⇒ statement_semantics stmt (liveafter label)
     315  ].
     316  cases not_implemented (* XXX *)
     317qed.
     318
     319definition liveafter ≝
     320  λint_fun.
     321  λlivebefore.
     322  λlabel.
     323  λliveafter: valuation.
     324  match lookup ? ? (ertl_if_graph int_fun) label with
     325  [ None      ⇒ ?
     326  | Some stmt ⇒ list_set_fold ? ? (λsuccessor. λaccu.
     327      lattice_join (livebefore successor liveafter) accu)
     328      lattice_bottom (statement_successors stmt)
     329  ].
     330  cases not_implemented (* XXX *)
     331qed.
    294332
    295333definition analyse: ertl_internal_function → valuation ≝
    296334  λint_fun.
    297   let livebefore ≝ λlabel. λliveafter: valuation.
    298     match lookup ? ? (ertl_if_graph int_fun) label with
    299     [ None      ⇒ ?
    300     | Some stmt ⇒ statement_semantics stmt (liveafter label)
    301     ]
    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     ]
    310   in ?.
     335    fix_lfp (liveafter int_fun (livebefore int_fun)).
Note: See TracChangeset for help on using the changeset viewer.