Changeset 3263 for src/ERTL/liveness.ma


Ignore:
Timestamp:
May 10, 2013, 1:40:31 PM (7 years ago)
Author:
tranquil
Message:

moved callee saved saving and restoring to ERTL -> LTL pass (untrusted
colourer and interference graph creator still need to be updated)
joint now has the stack size split in three (referenced locals, params
and spilled)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/liveness.ma

    r3255 r3263  
    9696definition used ≝
    9797  λglobals: list ident.
     98  λcallee_saved_store : list register.
    9899  λs: joint_statement ERTL globals.
    99100  match s with
     
    143144  | final fin ⇒
    144145    match fin with
    145     [ RETURN ⇒ 〈set_empty …, set_union … (set_from_list … RegisterCalleeSaved) ret_regs〉
     146    [ RETURN ⇒ 〈set_from_list … callee_saved_store,
     147                set_union … (set_from_list … RegisterCalleeSaved) ret_regs〉
    146148    | GOTO l ⇒ rl_bottom
    147149    | TAILCALL abs _ _ ⇒ match abs in False with [ ]
     
    205207  ].
    206208
    207 definition statement_semantics: ∀globals: list ident.
     209definition statement_semantics: ∀globals: list ident.list register →
    208210  joint_statement ERTL globals → register_lattice → register_lattice ≝
    209   λglobals.
     211  λglobals,callee_saved_store.
    210212  λstmt.
    211213  λliveafter.
     
    213215    liveafter
    214216  else
    215     rl_join (rl_diff liveafter (defined globals stmt)) (used globals stmt).
     217    rl_join (rl_diff liveafter (defined globals stmt))
     218      (used globals callee_saved_store stmt).
    216219
    217220definition livebefore:
    218221  ∀globals: list ident.
    219222   joint_internal_function ERTL globals →
     223   list register →
    220224     valuation register_lattice → valuation register_lattice
    221225
    222226  λglobals: list ident.
    223227  λint_fun: joint_internal_function ERTL globals.
     228  λcallee_saved_store.
    224229  λliveafter: valuation register_lattice.
    225230  λlabel.
    226231  match lookup ?? (joint_if_code … int_fun) label with
    227232  [ None      ⇒ rl_bottom
    228   | Some stmt ⇒ statement_semantics globals stmt (liveafter label)
     233  | Some stmt ⇒ statement_semantics globals callee_saved_store stmt (liveafter label)
    229234  ].
    230235
     
    232237   λglobals: list ident.
    233238  λint_fun: joint_internal_function ERTL globals.
     239  λcallee_saved_store.
    234240  λlabel.
    235241  λliveafter: valuation register_lattice.
     
    238244  | Some stmt ⇒
    239245    \fold[rl_join,rl_bottom]_{successor ∈ stmt_labels … stmt}
    240       (livebefore globals int_fun liveafter successor)
     246      (livebefore globals int_fun callee_saved_store liveafter successor)
    241247  ].
    242248
    243249definition analyse_liveness ≝
    244   λthe_fixpoint: fixpoint_computer. λglobals,int_fun.
    245    the_fixpoint ? (liveafter globals int_fun).
     250  λthe_fixpoint: fixpoint_computer. λglobals,int_fun,callee_saved_store.
     251   the_fixpoint ? (liveafter globals int_fun callee_saved_store).
    246252
    247253definition vertex ≝ register + Register.
Note: See TracChangeset for help on using the changeset viewer.