Ignore:
Timestamp:
Feb 22, 2013, 11:39:03 AM (8 years ago)
Author:
sacerdot
Message:
  1. Stuff moved to correct places.
  2. ERTLptr pass added
File:
1 moved

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/liveness.ma

    r2690 r2693  
    1 
    21include "ASM/Util.ma".
    3 include "ERTL/ERTL.ma".
     2include "ERTLptr/ERTLptr.ma".
    43include "utilities/adt/set_adt.ma".
    54include "utilities/fixpoints.ma".
     
    4342definition defined ≝
    4443  λglobals: list ident.
    45   λs: joint_statement ERTL globals.
     44  λs: joint_statement ERTLptr globals.
    4645  match s with
    4746  [ sequential seq l ⇒
     
    6261                                    (rl_psingleton dr2))
    6362                      (rl_hsingleton RegisterCarry)
    64       | OP1 op1 r1 r2 ⇒ rl_join (rl_psingleton r1) (rl_psingleton r2)
     63      | OP1 op1 r1 r2 ⇒ rl_psingleton r1
    6564      | POP r ⇒ rl_psingleton r
    6665      | ADDRESS _ _ r1 r2 ⇒ rl_join (rl_psingleton r1) (rl_psingleton r2)
     
    7776      | extension_seq ext ⇒
    7877        match ext with
    79         [ ertl_new_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
    80         | ertl_del_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
    81         | ertl_frame_size r ⇒ rl_psingleton r
     78        [ ertlptr_ertl ext' ⇒
     79           match ext' with
     80           [ ertl_new_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
     81           | ertl_del_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
     82           | ertl_frame_size r ⇒ rl_psingleton r
     83           ]
     84        | LOW_ADDRESS r1 l ⇒ rl_psingleton r1
     85        | HIGH_ADDRESS r1 l ⇒ rl_psingleton r1
    8286        ]
    8387      (* Potentially destroys all caller-save hardware registers. *)
     
    101105definition used ≝
    102106  λglobals: list ident.
    103   λs: joint_statement ERTL globals.
     107  λs: joint_statement ERTLptr globals.
    104108  match s with
    105109  [ sequential seq l ⇒
     
    134138      | extension_seq ext ⇒
    135139        match ext with
    136         [ ertl_new_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
    137         | ertl_del_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
    138         | ertl_frame_size r ⇒ rl_bottom
    139         ]
     140        [ ertlptr_ertl ext' ⇒
     141           match ext' with
     142           [ ertl_new_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
     143           | ertl_del_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
     144           | ertl_frame_size r ⇒ rl_bottom ]
     145        | LOW_ADDRESS r1 l ⇒ rl_bottom
     146        | HIGH_ADDRESS r1 l ⇒ rl_bottom
     147        ]       
    140148      (* Reads the hardware registers that are used to pass parameters. *)
    141149      | _ ⇒ rl_bottom
     
    157165  λglobals: list ident.
    158166  λl: register_lattice.
    159   λs: joint_statement ERTL globals.
     167  λs: joint_statement ERTLptr globals.
    160168  let pliveafter ≝ \fst l in
    161169  let hliveafter ≝ \snd l in
     
    211219      | extension_seq ext ⇒
    212220        match ext with
    213         [ ertl_new_frame ⇒ None ?
    214         | ertl_del_frame ⇒ None ?
    215         | ertl_frame_size r ⇒
    216           if set_member ? (eq_identifier RegisterTag) r pliveafter then
    217             None ?
    218           else
    219             Some ? l
    220         ]
     221        [ ertlptr_ertl ext' ⇒
     222           match ext' with
     223           [ ertl_new_frame ⇒ None ?
     224           | ertl_del_frame ⇒ None ?
     225           | ertl_frame_size r ⇒
     226             if set_member ? (eq_identifier RegisterTag) r pliveafter then
     227               None ?
     228             else
     229               Some ? l]
     230        | LOW_ADDRESS r1 l' ⇒
     231           if set_member ? (eq_identifier RegisterTag) r1 pliveafter then
     232             None ?
     233           else
     234             Some ? l
     235        | HIGH_ADDRESS r1 l' ⇒
     236           if set_member ? (eq_identifier RegisterTag) r1 pliveafter then
     237             None ?
     238           else
     239             Some ? l
     240        ]       
    221241      | _ ⇒ None ?
    222242      ]
     
    227247
    228248definition statement_semantics: ∀globals: list ident.
    229   joint_statement ERTL globals → register_lattice → register_lattice ≝
     249  joint_statement ERTLptr globals → register_lattice → register_lattice ≝
    230250  λglobals.
    231251  λstmt.
     
    238258definition livebefore ≝
    239259  λglobals: list ident.
    240   λint_fun: joint_internal_function ERTL globals.
     260  λint_fun: joint_internal_function ERTLptr globals.
    241261  λlabel.
    242262  λliveafter: valuation register_lattice.
     
    248268definition liveafter ≝
    249269   λglobals: list ident.
    250   λint_fun: joint_internal_function ERTL globals.
     270  λint_fun: joint_internal_function ERTLptr globals.
    251271  λlabel.
    252272  λliveafter: valuation register_lattice.
Note: See TracChangeset for help on using the changeset viewer.