Changeset 2887


Ignore:
Timestamp:
Mar 15, 2013, 7:22:17 PM (4 years ago)
Author:
tranquil
Message:

Corrected bug where eliminable statements where not eliminated. Changed eliminable output from option label to bool.

Location:
src/ERTLptr
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/ERTLptrToLTL.ma

    r2883 r2887  
    350350  let carry_lives_after ≝ hlives RegisterCarry (after lbl) in
    351351  let move ≝ move globals localss carry_lives_after in
     352  if eliminable_step … (after lbl) s then ([ ] : step_block LTL globals) else
    352353  match s with
    353354  [ step_seq s' ⇒
  • src/ERTLptr/liveness.ma

    r2883 r2887  
    158158  ].
    159159
     160definition eliminable_step ≝
     161λglobals: list ident.
     162λl: register_lattice.
     163λs: joint_step ERTLptr globals.
     164let pliveafter ≝ \fst l in
     165let hliveafter ≝ \snd l in
     166match s with
     167[ step_seq s ⇒
     168  match s with
     169  [ OP2 op2 r1 r2 r3 ⇒
     170    ¬(match op2 with
     171      [ Add ⇒ set_member … eq_Register RegisterCarry hliveafter
     172      | Addc ⇒ set_member … eq_Register RegisterCarry hliveafter
     173      | Sub ⇒ set_member … eq_Register RegisterCarry hliveafter
     174      | _ ⇒ false
     175      ] ∨ set_member … (eq_identifier …) r1 pliveafter)
     176  | OPACCS opaccs dr1 dr2 sr1 sr2 ⇒
     177    ¬(set_member … (eq_identifier …) dr1 pliveafter ∨
     178      set_member … (eq_identifier …) dr2 pliveafter ∨
     179      set_member … eq_Register RegisterCarry hliveafter)
     180  | OP1 op1 r1 r2 ⇒
     181    ¬set_member … (eq_identifier …) r1 pliveafter
     182  | ADDRESS _ _ r1 r2 ⇒
     183    ¬(set_member … (eq_identifier …) r1 pliveafter ∨
     184      set_member … (eq_identifier …) r2 pliveafter)
     185  | LOAD acc_a dpl dph ⇒
     186    ¬set_member ? (eq_identifier …) acc_a pliveafter
     187  | MOVE pair_reg ⇒
     188    ¬match \fst pair_reg with
     189      [ PSD p1 ⇒
     190        set_member … (eq_identifier …) p1 pliveafter
     191      | HDW h1 ⇒
     192        set_member … eq_Register h1 hliveafter
     193      ]
     194  | extension_seq ext ⇒
     195    match ext with
     196    [ ertlptr_ertl ext' ⇒
     197       match ext' with
     198       [ ertl_new_frame ⇒ false
     199       | ertl_del_frame ⇒ false
     200       | ertl_frame_size r ⇒
     201         ¬set_member ? (eq_identifier RegisterTag) r pliveafter
     202       ]
     203    | LOW_ADDRESS r1 l' ⇒
     204       ¬set_member ? (eq_identifier RegisterTag) r1 pliveafter
     205    | HIGH_ADDRESS r1 l' ⇒
     206       ¬set_member ? (eq_identifier RegisterTag) r1 pliveafter
     207    ]       
     208  | _ ⇒ false
     209  ]
     210| _ ⇒ false
     211].
     212
    160213definition eliminable ≝
    161214  λglobals: list ident.
     
    165218  let hliveafter ≝ \snd l in
    166219  match s with
    167   [ sequential seq l ⇒
    168     match seq with
    169     [ step_seq s ⇒
    170       match s with
    171       [ OP2 op2 r1 r2 r3 ⇒
    172         if match op2 with
    173           [ Add ⇒ set_member … eq_Register RegisterCarry hliveafter
    174           | Addc ⇒ set_member … eq_Register RegisterCarry hliveafter
    175           | Sub ⇒ set_member … eq_Register RegisterCarry hliveafter
    176           | _ ⇒ false
    177           ] ∨ set_member … (eq_identifier …) r1 pliveafter
    178         then
    179           None ?
    180         else
    181           Some ? l
    182       | OPACCS opaccs dr1 dr2 sr1 sr2 ⇒
    183         if set_member … (eq_identifier …) dr1 pliveafter ∨
    184            set_member … (eq_identifier …) dr2 pliveafter ∨
    185            set_member … eq_Register RegisterCarry hliveafter then
    186           None ?
    187         else
    188           Some ? l
    189       | OP1 op1 r1 r2 ⇒
    190         if set_member … (eq_identifier …) r1 pliveafter then
    191           None ?
    192         else
    193           Some ? l
    194       | ADDRESS _ _ r1 r2 ⇒
    195         if set_member … (eq_identifier …) r1 pliveafter ∨
    196            set_member … (eq_identifier …) r2 pliveafter then
    197           None ?
    198         else
    199           Some ? l
    200       | LOAD acc_a dpl dph ⇒
    201         if set_member ? (eq_identifier …) acc_a pliveafter then
    202           None ?
    203         else
    204           Some ? l
    205       | MOVE pair_reg ⇒
    206         if match \fst pair_reg with
    207           [ PSD p1 ⇒
    208             set_member … (eq_identifier …) p1 pliveafter
    209           | HDW h1 ⇒
    210             set_member … eq_Register h1 hliveafter
    211           ] then
    212             None ?
    213           else
    214             Some ? l
    215       | extension_seq ext ⇒
    216         match ext with
    217         [ ertlptr_ertl ext' ⇒
    218            match ext' with
    219            [ ertl_new_frame ⇒ None ?
    220            | ertl_del_frame ⇒ None ?
    221            | ertl_frame_size r ⇒
    222              if set_member ? (eq_identifier RegisterTag) r pliveafter then
    223                None ?
    224              else
    225                Some ? l]
    226         | LOW_ADDRESS r1 l' ⇒
    227            if set_member ? (eq_identifier RegisterTag) r1 pliveafter then
    228              None ?
    229            else
    230              Some ? l
    231         | HIGH_ADDRESS r1 l' ⇒
    232            if set_member ? (eq_identifier RegisterTag) r1 pliveafter then
    233              None ?
    234            else
    235              Some ? l
    236         ]       
    237       | _ ⇒ None ?
    238       ]
    239     | _ ⇒ None ?
    240     ]
    241   | _ ⇒ None ?
     220  [ sequential seq _ ⇒ eliminable_step … l seq
     221  | _ ⇒ false
    242222  ].
    243223
     
    247227  λstmt.
    248228  λliveafter.
    249   match eliminable globals liveafter stmt with
    250   [ None ⇒ rl_join (rl_diff liveafter (defined globals stmt)) (used globals stmt)
    251   | Some l ⇒ liveafter
    252   ].
     229  if eliminable globals liveafter stmt then
     230    liveafter
     231  else
     232    rl_join (rl_diff liveafter (defined globals stmt)) (used globals stmt).
    253233
    254234definition livebefore ≝
Note: See TracChangeset for help on using the changeset viewer.