Changeset 1260 for src/ERTL/liveness.ma


Ignore:
Timestamp:
Sep 23, 2011, 3:04:20 PM (8 years ago)
Author:
mulligan
Message:

commit for csc

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/liveness.ma

    r1250 r1260  
    8080  [ joint_st_sequential seq l ⇒
    8181    match seq with
    82     [ joint_instr_op2 op2 r _ ⇒
     82    [ joint_instr_op2 op2 r1 r2 _ ⇒
    8383      match op2 with
    84       [ Add ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r)
    85       | Addc ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r)
    86       | Sub ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r)
    87       | _ ⇒ lattice_psingleton r
     84      [ Add ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r1)
     85      | Addc ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r1)
     86      | Sub ⇒ lattice_join (lattice_hsingleton RegisterCarry)  (lattice_psingleton r1)
     87      | _ ⇒ lattice_psingleton r1
    8888      ]
    8989    | joint_instr_clear_carry ⇒ lattice_hsingleton RegisterCarry
    9090    | joint_instr_set_carry ⇒ lattice_hsingleton RegisterCarry
    9191    | joint_instr_opaccs opaccs r1 r2 ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    92     | joint_instr_op1 op1 r ⇒ lattice_psingleton r
     92    | joint_instr_op1 op1 r1 r2 ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    9393    | joint_instr_pop r ⇒ lattice_psingleton r
    9494    | joint_instr_int r _ ⇒ lattice_psingleton r
     
    111111    | joint_instr_extension ext ⇒
    112112      match ext with
    113       [ ertl_st_ext_new_frame l ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
    114       | ertl_st_ext_del_frame l ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
    115       | ertl_st_ext_frame_size r l ⇒ lattice_psingleton r]]
     113      [ ertl_st_ext_new_frame ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
     114      | ertl_st_ext_del_frame ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
     115      | ertl_st_ext_frame_size r ⇒ lattice_psingleton r]]
    116116  | joint_st_return ⇒ lattice_bottom
    117117  | joint_st_goto l ⇒ lattice_bottom
     
    126126  [ joint_st_sequential seq l ⇒
    127127    match seq with
    128     [ joint_instr_op2 op2 acc_a r
     128    [ joint_instr_op2 op2 acc_a r1 r2
    129129      match op2 with
    130130      [ Addc ⇒
    131         lattice_join (lattice_join (lattice_psingleton acc_a) (lattice_psingleton r)) (lattice_hsingleton RegisterCarry)
    132       | _ ⇒ lattice_join (lattice_psingleton acc_a) (lattice_psingleton r)
     131        lattice_join (lattice_join (lattice_psingleton r1) (lattice_psingleton r2)) (lattice_hsingleton RegisterCarry)
     132      | _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    133133      ]
    134134    | joint_instr_clear_carry ⇒ lattice_bottom
     
    136136    (* acc_a and acc_b *)
    137137    | joint_instr_opaccs opaccs r1 r2 ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    138     | joint_instr_op1 op1 r ⇒ lattice_psingleton r
     138    | joint_instr_op1 op1 r1 r2 ⇒ lattice_psingleton r2
    139139    | joint_instr_pop r ⇒ lattice_bottom
    140140    | joint_instr_int r _ ⇒ lattice_bottom
     
    158158  | joint_instr_extension ext ⇒
    159159    match ext with
    160     [ ertl_st_ext_new_frame l ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
    161     | ertl_st_ext_del_frame l ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
    162     | ertl_st_ext_frame_size r l ⇒ lattice_bottom]]
     160    [ ertl_st_ext_new_frame ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
     161    | ertl_st_ext_del_frame ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
     162    | ertl_st_ext_frame_size r ⇒ lattice_bottom]]
    163163  | joint_st_return ⇒ 〈set_empty …, set_union … (set_from_list … RegisterCalleeSaved) ret_regs〉
    164164  | joint_st_goto l ⇒ lattice_bottom
     
    173173  [ joint_st_sequential seq l ⇒
    174174    match seq with
    175     [ joint_instr_op2 op2 acc_a r
    176       if set_member … (eq_identifier …) acc_a pliveafter ∨
     175    [ joint_instr_op2 op2 r1 r2 r3
     176      if set_member … (eq_identifier …) r1 pliveafter ∨
    177177         set_member … eq_Register RegisterCarry hliveafter then
    178178        None ?
     
    188188      else
    189189        Some ? l
    190     | joint_instr_op1 op1 r
    191       if set_member … (eq_identifier …) r pliveafter ∨
     190    | joint_instr_op1 op1 r1 r2
     191      if set_member … (eq_identifier …) r1 pliveafter ∨
    192192         set_member … eq_Register RegisterCarry hliveafter then
    193193        None ?
     
    237237    | joint_instr_extension ext ⇒
    238238      match ext with
    239       [ ertl_st_ext_new_frame l ⇒ None ?
    240       | ertl_st_ext_del_frame l ⇒ None ?
    241       | ertl_st_ext_frame_size r l
     239      [ ertl_st_ext_new_frame ⇒ None ?
     240      | ertl_st_ext_del_frame ⇒ None ?
     241      | ertl_st_ext_frame_size r
    242242        if set_member ? (eq_identifier RegisterTag) r pliveafter ∨
    243243           set_member ? eq_Register RegisterCarry hliveafter then
Note: See TracChangeset for help on using the changeset viewer.