Changeset 1282 for src/ERTL/liveness.ma
 Timestamp:
 Sep 28, 2011, 11:50:32 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTL/liveness.ma
r1275 r1282 7 7 λs: ertl_statement globals. 8 8 match s with 9 [ joint_st_sequential seq l ⇒10 match seq with 11 [ joint_instr_condacc_a_reg lbl_true ⇒9 [ sequential seq l ⇒ 10 match seq with 11 [ COND acc_a_reg lbl_true ⇒ 12 12 set_insert … lbl_true (set_singleton … l) 13 13  _ ⇒ set_singleton … l ] 14  joint_st_gotol ⇒ set_singleton … l15  joint_st_return⇒ set_empty ?14  GOTO l ⇒ set_singleton … l 15  RETURN ⇒ set_empty ? 16 16 ]. 17 17 … … 78 78 λs: ertl_statement globals. 79 79 match s with 80 [ joint_st_sequential seq l ⇒81 match seq with 82 [ joint_instr_op2 op2 r1 r2 _ ⇒80 [ sequential seq l ⇒ 81 match seq with 82 [ OP2 op2 r1 r2 _ ⇒ 83 83 match op2 with 84 84 [ Add ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r1) … … 87 87  _ ⇒ lattice_psingleton r1 88 88 ] 89  joint_instr_clear_carry⇒ lattice_hsingleton RegisterCarry90  joint_instr_set_carry⇒ lattice_hsingleton RegisterCarry91  joint_instr_opaccsopaccs dr1 dr2 sr1 sr2 ⇒89  CLEAR_CARRY ⇒ lattice_hsingleton RegisterCarry 90  SET_CARRY ⇒ lattice_hsingleton RegisterCarry 91  OPACCS opaccs dr1 dr2 sr1 sr2 ⇒ 92 92 lattice_join (lattice_psingleton dr1) (lattice_psingleton dr2) 93  joint_instr_op1 op1 r1 r2 ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)94  joint_instr_popr ⇒ lattice_psingleton r95  joint_instr_intr _ ⇒ lattice_psingleton r96  joint_instr_address_ _ r1 r2 ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)97  joint_instr_loadr _ _ ⇒ lattice_psingleton r93  OP1 op1 r1 r2 ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2) 94  POP r ⇒ lattice_psingleton r 95  INT r _ ⇒ lattice_psingleton r 96  ADDRESS _ _ r1 r2 ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2) 97  LOAD r _ _ ⇒ lattice_psingleton r 98 98 (* Potentially destroys all callersave hardware registers. *) 99  joint_instr_call_idid _ _ ⇒ 〈set_empty …, set_from_list … RegisterCallerSaved〉100  joint_instr_commentc ⇒ lattice_bottom101  joint_instr_condr lbl_true ⇒ lattice_bottom102  joint_instr_storeacc_a dpl dph ⇒ lattice_bottom103  joint_instr_cost_labelclabel ⇒ lattice_bottom104  joint_instr_pushr ⇒ lattice_bottom105  joint_instr_movepair_reg ⇒99  CALL_ID id _ _ ⇒ 〈set_empty …, set_from_list … RegisterCallerSaved〉 100  COMMENT c ⇒ lattice_bottom 101  COND r lbl_true ⇒ lattice_bottom 102  STORE acc_a dpl dph ⇒ lattice_bottom 103  COST_LABEL clabel ⇒ lattice_bottom 104  PUSH r ⇒ lattice_bottom 105  MOVE pair_reg ⇒ 106 106 (* first register relevant only *) 107 107 let r1 ≝ \fst pair_reg in … … 110 110  hardware h ⇒ lattice_hsingleton h 111 111 ] 112  joint_instr_extension ext ⇒112  extension ext ⇒ 113 113 match ext with 114 114 [ ertl_st_ext_new_frame ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH) 115 115  ertl_st_ext_del_frame ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH) 116 116  ertl_st_ext_frame_size r ⇒ lattice_psingleton r]] 117  joint_st_return⇒ lattice_bottom118  joint_st_gotol ⇒ lattice_bottom117  RETURN ⇒ lattice_bottom 118  GOTO l ⇒ lattice_bottom 119 119 ]. 120 120 … … 125 125 λs: ertl_statement globals. 126 126 match s with 127 [ joint_st_sequential seq l ⇒128 match seq with 129 [ joint_instr_op2 op2 acc_a r1 r2 ⇒127 [ sequential seq l ⇒ 128 match seq with 129 [ OP2 op2 acc_a r1 r2 ⇒ 130 130 match op2 with 131 131 [ Addc ⇒ … … 133 133  _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2) 134 134 ] 135  joint_instr_clear_carry⇒ lattice_bottom136  joint_instr_set_carry⇒ lattice_bottom135  CLEAR_CARRY ⇒ lattice_bottom 136  SET_CARRY ⇒ lattice_bottom 137 137 (* acc_a and acc_b *) 138  joint_instr_opaccsopaccs dr1 dr2 sr1 sr2 ⇒138  OPACCS opaccs dr1 dr2 sr1 sr2 ⇒ 139 139 lattice_join (lattice_psingleton sr1) (lattice_psingleton sr2) 140  joint_instr_op1 op1 r1 r2 ⇒ lattice_psingleton r2141  joint_instr_popr ⇒ lattice_bottom142  joint_instr_intr _ ⇒ lattice_bottom143  joint_instr_address_ _ r1 r2 ⇒ lattice_bottom144  joint_instr_loadacc_a dpl dph ⇒ lattice_join (lattice_psingleton dpl) (lattice_psingleton dph)140  OP1 op1 r1 r2 ⇒ lattice_psingleton r2 141  POP r ⇒ lattice_bottom 142  INT r _ ⇒ lattice_bottom 143  ADDRESS _ _ r1 r2 ⇒ lattice_bottom 144  LOAD acc_a dpl dph ⇒ lattice_join (lattice_psingleton dpl) (lattice_psingleton dph) 145 145 (* Reads the hardware registers that are used to pass parameters. *) 146  joint_instr_call_id_ nparams _ ⇒ 〈set_empty …, set_from_list … (prefix ? nparams RegisterParams)〉147  joint_instr_commentc ⇒ lattice_bottom148  joint_instr_condr lbl_true ⇒ lattice_psingleton r149  joint_instr_storeacc_a dpl dph ⇒146  CALL_ID _ nparams _ ⇒ 〈set_empty …, set_from_list … (prefix ? nparams RegisterParams)〉 147  COMMENT c ⇒ lattice_bottom 148  COND r lbl_true ⇒ lattice_psingleton r 149  STORE acc_a dpl dph ⇒ 150 150 lattice_join (lattice_join (lattice_psingleton acc_a) (lattice_psingleton dpl)) (lattice_psingleton dph) 151  joint_instr_cost_labelclabel ⇒ lattice_bottom152  joint_instr_pushr ⇒ lattice_psingleton r153  joint_instr_movepair_reg ⇒151  COST_LABEL clabel ⇒ lattice_bottom 152  PUSH r ⇒ lattice_psingleton r 153  MOVE pair_reg ⇒ 154 154 (* only second reg in pair relevant *) 155 155 let r2 ≝ \snd pair_reg in … … 158 158  hardware h ⇒ lattice_hsingleton h 159 159 ] 160  joint_instr_extension ext ⇒160  extension ext ⇒ 161 161 match ext with 162 162 [ ertl_st_ext_new_frame ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH) 163 163  ertl_st_ext_del_frame ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH) 164 164  ertl_st_ext_frame_size r ⇒ lattice_bottom]] 165  joint_st_return⇒ 〈set_empty …, set_union … (set_from_list … RegisterCalleeSaved) ret_regs〉166  joint_st_gotol ⇒ lattice_bottom165  RETURN ⇒ 〈set_empty …, set_union … (set_from_list … RegisterCalleeSaved) ret_regs〉 166  GOTO l ⇒ lattice_bottom 167 167 ]. 168 168 … … 173 173 let 〈pliveafter, hliveafter〉 ≝ l in 174 174 match s with 175 [ joint_st_sequential seq l ⇒176 match seq with 177 [ joint_instr_op2 op2 r1 r2 r3 ⇒175 [ sequential seq l ⇒ 176 match seq with 177 [ OP2 op2 r1 r2 r3 ⇒ 178 178 if set_member … (eq_identifier …) r1 pliveafter ∨ 179 179 set_member … eq_Register RegisterCarry hliveafter then … … 181 181 else 182 182 Some ? l 183  joint_instr_clear_carry⇒ None ?184  joint_instr_set_carry⇒ None ?185  joint_instr_opaccsopaccs dr1 dr2 sr1 sr2 ⇒183  CLEAR_CARRY ⇒ None ? 184  SET_CARRY ⇒ None ? 185  OPACCS opaccs dr1 dr2 sr1 sr2 ⇒ 186 186 if set_member … (eq_identifier …) dr1 pliveafter ∨ 187 187 set_member … (eq_identifier …) dr2 pliveafter ∨ … … 190 190 else 191 191 Some ? l 192  joint_instr_op1 op1 r1 r2 ⇒192  OP1 op1 r1 r2 ⇒ 193 193 if set_member … (eq_identifier …) r1 pliveafter ∨ 194 194 set_member … eq_Register RegisterCarry hliveafter then … … 196 196 else 197 197 Some ? l 198  joint_instr_popr ⇒ None ?199  joint_instr_intr _ ⇒198  POP r ⇒ None ? 199  INT r _ ⇒ 200 200 if set_member … (eq_identifier …) r pliveafter ∨ 201 201 set_member … eq_Register RegisterCarry hliveafter then … … 203 203 else 204 204 Some ? l 205  joint_instr_address_ _ r1 r2 ⇒205  ADDRESS _ _ r1 r2 ⇒ 206 206 if set_member … (eq_identifier …) r1 pliveafter ∨ 207 207 set_member … (eq_identifier …) r2 pliveafter ∨ … … 210 210 else 211 211 Some ? l 212  joint_instr_loadacc_a dpl dph ⇒212  LOAD acc_a dpl dph ⇒ 213 213 if set_member ? (eq_identifier …) acc_a pliveafter ∨ 214 214 set_member … eq_Register RegisterCarry hliveafter then … … 216 216 else 217 217 Some ? l 218  joint_instr_call_id_ nparams _ ⇒ None ?219  joint_instr_commentc ⇒ None ?220  joint_instr_condr lbl_true ⇒ None ?221  joint_instr_storeacc_a dpl dph ⇒ None ?222  joint_instr_cost_labelclabel ⇒ None ?223  joint_instr_pushr ⇒ None ?224  joint_instr_movepair_reg ⇒218  CALL_ID _ nparams _ ⇒ None ? 219  COMMENT c ⇒ None ? 220  COND r lbl_true ⇒ None ? 221  STORE acc_a dpl dph ⇒ None ? 222  COST_LABEL clabel ⇒ None ? 223  PUSH r ⇒ None ? 224  MOVE pair_reg ⇒ 225 225 let r1 ≝ \fst pair_reg in 226 226 let r2 ≝ \snd pair_reg in … … 237 237 else 238 238 Some ? l] 239  joint_instr_extension ext ⇒239  extension ext ⇒ 240 240 match ext with 241 241 [ ertl_st_ext_new_frame ⇒ None ? … … 247 247 else 248 248 Some ? l]] 249  joint_st_gotol ⇒ None ?250  joint_st_return⇒ None ?249  GOTO l ⇒ None ? 250  RETURN ⇒ None ? 251 251 ]. 252 252
Note: See TracChangeset
for help on using the changeset viewer.