Changeset 1250 for src/ERTL/liveness.ma


Ignore:
Timestamp:
Sep 22, 2011, 12:02:35 PM (9 years ago)
Author:
sacerdot
Message:
  1. Sigma types projections moved to utilities/extralib.ma
  2. Extended statement turned into extended instructions, decreasing the amount of code in the translations
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/liveness.ma

    r1249 r1250  
    1111    [ joint_instr_cond acc_a_reg lbl_true ⇒
    1212        set_insert … lbl_true (set_singleton … l)
    13     | _ ⇒ set_singleton … l
    14     ]
    15   | joint_st_extension ext ⇒
    16     match ext with
    17     [ ertl_st_ext_new_frame l ⇒ set_singleton … l
    18     | ertl_st_ext_del_frame l ⇒ set_singleton … l
    19     | ertl_st_ext_frame_size r l ⇒ set_singleton … l
    20     ]
     13    | _ ⇒ set_singleton … l ]
    2114  | joint_st_goto l ⇒ set_singleton … l
    22   | joint_st_return ⇒ set_empty
     15  | joint_st_return ⇒ set_empty ?
    2316  ].
    2417
     
    116109      | hardware h ⇒ lattice_hsingleton h
    117110      ]
    118     ]
     111    | joint_instr_extension ext ⇒
     112      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]]
    119116  | joint_st_return ⇒ lattice_bottom
    120   | joint_st_extension ext ⇒
    121     match ext with
    122     [ ertl_st_ext_new_frame l ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
    123     | ertl_st_ext_del_frame l ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
    124     | ertl_st_ext_frame_size r l ⇒ lattice_psingleton r
    125     ]
    126117  | joint_st_goto l ⇒ lattice_bottom
    127118  ].
     
    165156      | hardware h ⇒ lattice_hsingleton h
    166157      ]
    167     ]
    168   | joint_st_return ⇒ 〈set_empty …, set_union … (set_from_list … RegisterCalleeSaved) ret_regs〉
    169   | joint_st_goto l ⇒ lattice_bottom
    170   | joint_st_extension ext ⇒
     158  | joint_instr_extension ext ⇒
    171159    match ext with
    172160    [ ertl_st_ext_new_frame l ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
    173161    | ertl_st_ext_del_frame l ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
    174     | ertl_st_ext_frame_size r l ⇒ lattice_bottom
    175     ]
     162    | ertl_st_ext_frame_size r l ⇒ lattice_bottom]]
     163  | joint_st_return ⇒ 〈set_empty …, set_union … (set_from_list … RegisterCalleeSaved) ret_regs〉
     164  | joint_st_goto l ⇒ lattice_bottom
    176165  ].
    177166
     
    245234          None ?
    246235        else
    247           Some ? l
    248       ]
    249     ]
     236          Some ? l]
     237    | joint_instr_extension ext ⇒
     238      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 ⇒
     242        if set_member ? (eq_identifier RegisterTag) r pliveafter ∨
     243           set_member ? eq_Register RegisterCarry hliveafter then
     244          None ?
     245        else
     246          Some ? l]]
    250247  | joint_st_goto l ⇒ None ?
    251248  | joint_st_return ⇒ None ?
    252   | joint_st_extension ext ⇒
    253     match ext with
    254     [ ertl_st_ext_new_frame l ⇒ None ?
    255     | ertl_st_ext_del_frame l ⇒ None ?
    256     | ertl_st_ext_frame_size r l ⇒
    257       if set_member ? (eq_identifier RegisterTag) r pliveafter ∨
    258          set_member ? eq_Register RegisterCarry hliveafter then
    259         None ?
    260       else
    261         Some ? l
    262     ]
    263249  ].
    264250
Note: See TracChangeset for help on using the changeset viewer.