Changeset 1185 for src/ERTL/liveness.ma
 Timestamp:
 Sep 5, 2011, 5:02:53 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTL/liveness.ma
r1144 r1185 35 35 36 36 definition statement_successors ≝ 37 λs: ertl_statement. 37 λglobals: list ident. 38 λs: ertl_statement globals. 38 39 match s with 39 [ ertl_st_return ⇒ [ ] 40  ertl_st_skip l ⇒ [ l ] 41  ertl_st_comment c l ⇒ [ l ] 42  ertl_st_cost c l ⇒ [ l ] 43  ertl_st_set_hdw _ _ l ⇒ [ l ] 44  ertl_st_get_hdw _ _ l ⇒ [ l ] 45  ertl_st_hdw_to_hdw _ _ l ⇒ [ l ] 46  ertl_st_new_frame l ⇒ [ l ] 47  ertl_st_del_frame l ⇒ [ l ] 48  ertl_st_frame_size _ l ⇒ [ l ] 49  ertl_st_push _ l ⇒ [ l ] 50  ertl_st_pop _ l ⇒ [ l ] 51  ertl_st_addr _ _ _ l ⇒ [ l ] 52  ertl_st_int _ _ l ⇒ [ l ] 53  ertl_st_move _ _ l ⇒ [ l ] 54  ertl_st_opaccs _ _ _ _ _ l ⇒ [ l ] 55  ertl_st_op1 _ _ _ l ⇒ [ l ] 56  ertl_st_op2 _ _ _ _ l ⇒ [ l ] 57  ertl_st_clear_carry l ⇒ [ l ] 58  ertl_st_set_carry l ⇒ [ l ] 59  ertl_st_load _ _ _ l ⇒ [ l ] 60  ertl_st_store _ _ _ l ⇒ [ l ] 61  ertl_st_call_id _ _ l ⇒ [ l ] 62  ertl_st_cond _ l1 l2 ⇒ 63 list_set_add ? (eq_identifier ?) l1 [ l2 ] 40 [ joint_st_sequential seq l ⇒ 41 match seq with 42 [ joint_instr_cond acc_a_reg lbl_true ⇒ 43 list_set_add ? (eq_identifier ?) lbl_true [ l ] 44  _ ⇒ [ l ] 45 ] 46  joint_st_extension ext ⇒ 47 match ext with 48 [ ertl_st_ext_new_frame l ⇒ [ l ] 49  ertl_st_ext_del_frame l ⇒ [ l ] 50  ertl_st_ext_frame_size r l ⇒ [ l ] 51 ] 52  joint_st_goto l ⇒ [ l ] 53  joint_st_return ⇒ [ ] 64 54 ]. 65 55 … … 122 112 lattice_is_maximal. 123 113 124 definition defined: ertl_statement → register_lattice ≝ 125 λs. 114 definition defined ≝ 115 λglobals: list ident. 116 λs: ertl_statement globals. 126 117 match s with 127 [ ertl_st_skip _ ⇒ lattice_bottom 128  ertl_st_comment _ _ ⇒ lattice_bottom 129  ertl_st_cost _ _ ⇒ lattice_bottom 130  ertl_st_push _ _⇒ lattice_bottom 131  ertl_st_store _ _ _ _ ⇒ lattice_bottom 132  ertl_st_cond _ _ _ ⇒ lattice_bottom 133  ertl_st_return ⇒ lattice_bottom 134  ertl_st_clear_carry _ ⇒ lattice_hsingleton RegisterCarry 135  ertl_st_set_carry _ ⇒ lattice_hsingleton RegisterCarry 136  ertl_st_op2 op2 r _ _ _ ⇒ 137 match op2 with 138 [ Add ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r) 139  Addc ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r) 140  Sub ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r) 141  _ ⇒ lattice_psingleton r 142 ] 143  ertl_st_op1 op1 r _ _ ⇒ lattice_psingleton r 144  ertl_st_get_hdw r _ _ ⇒ lattice_psingleton r 145  ertl_st_frame_size r _ ⇒ lattice_psingleton r 146  ertl_st_pop r _ ⇒ lattice_psingleton r 147  ertl_st_int r _ _ ⇒ lattice_psingleton r 148  ertl_st_addr r1 r2 _ _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2) 149  ertl_st_move r _ _ ⇒ lattice_psingleton r 150 (* XXX: change from o'caml *) 151  ertl_st_opaccs _ r1 r2 _ _ _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2) 152  ertl_st_load r _ _ _ ⇒ lattice_psingleton r 153  ertl_st_set_hdw r _ _ ⇒ lattice_hsingleton r 154  ertl_st_hdw_to_hdw r _ _ ⇒ lattice_hsingleton r 155 (* Potentially destroys all callersave hardware registers. *) 156  ertl_st_call_id _ _ _ ⇒ 〈[ ], RegisterCallerSaved〉 157  ertl_st_new_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH) 158  ertl_st_del_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH) 118 [ joint_st_sequential seq l ⇒ 119 match seq with 120 [ joint_instr_op2 op2 r _ ⇒ 121 match op2 with 122 [ Add ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r) 123  Addc ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r) 124  Sub ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r) 125  _ ⇒ lattice_psingleton r 126 ] 127  joint_instr_clear_carry ⇒ lattice_hsingleton RegisterCarry 128  joint_instr_set_carry ⇒ lattice_hsingleton RegisterCarry 129  joint_instr_opaccs opaccs r1 r2 ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2) 130  joint_instr_op1 op1 r ⇒ lattice_psingleton r 131  joint_instr_pop r ⇒ lattice_psingleton r 132  joint_instr_int r _ ⇒ lattice_psingleton r 133  joint_instr_address _ _ r1 r2 ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2) 134  joint_instr_load r _ _ ⇒ lattice_psingleton r 135 (* Potentially destroys all callersave hardware registers. *) 136  joint_instr_call_id _ _ ⇒ 〈[ ], RegisterCallerSaved〉 137  joint_instr_comment c ⇒ lattice_bottom 138  joint_instr_cond r lbl_true ⇒ lattice_bottom 139  joint_instr_store acc_a dpl dph ⇒ lattice_bottom 140  joint_instr_cost_label clabel ⇒ lattice_bottom 141  joint_instr_push r ⇒ lattice_bottom 142  joint_instr_move pair_reg ⇒ 143 (* first register relevant only *) 144 let r1 ≝ \fst pair_reg in 145 match r1 with 146 [ pseudo p ⇒ lattice_psingleton p 147  hardware h ⇒ lattice_hsingleton h 148 ] 149 ] 150  joint_st_return ⇒ lattice_bottom 151  joint_st_extension ext ⇒ 152 match ext with 153 [ ertl_st_ext_new_frame l ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH) 154  ertl_st_ext_del_frame l ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH) 155  ertl_st_ext_frame_size r l ⇒ lattice_psingleton r 156 ] 157  joint_st_goto l ⇒ lattice_bottom 159 158 ]. 160 159 … … 169 168 definition ret_regs ≝ list_set_of_list RegisterRets. 170 169 171 definition used: ertl_statement → register_lattice ≝ 172 λstmt. 173 match stmt with 174 [ ertl_st_skip _ ⇒ lattice_bottom 175  ertl_st_cost _ _ ⇒ lattice_bottom 176  ertl_st_comment _ _ ⇒ lattice_bottom 177  ertl_st_frame_size _ _ ⇒ lattice_bottom 178  ertl_st_pop _ _ ⇒ lattice_bottom 179  ertl_st_addr _ _ _ _ ⇒ lattice_bottom 180  ertl_st_int _ _ _ ⇒ lattice_bottom 181  ertl_st_clear_carry _ ⇒ lattice_bottom 182  ertl_st_set_carry _ ⇒ lattice_bottom 170 definition used ≝ 171 λglobals: list ident. 172 λs: ertl_statement globals. 173 match s with 174 [ joint_st_sequential seq l ⇒ 175 match seq with 176 [ joint_instr_op2 op2 acc_a r ⇒ 177 match op2 with 178 [ Addc ⇒ 179 lattice_join (lattice_join (lattice_psingleton acc_a) (lattice_psingleton r)) (lattice_hsingleton RegisterCarry) 180  _ ⇒ lattice_join (lattice_psingleton acc_a) (lattice_psingleton r) 181 ] 182  joint_instr_clear_carry ⇒ lattice_bottom 183  joint_instr_set_carry ⇒ lattice_bottom 184 (* acc_a and acc_b *) 185  joint_instr_opaccs opaccs r1 r2 ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2) 186  joint_instr_op1 op1 r ⇒ lattice_psingleton r 187  joint_instr_pop r ⇒ lattice_bottom 188  joint_instr_int r _ ⇒ lattice_bottom 189  joint_instr_address _ _ r1 r2 ⇒ lattice_bottom 190  joint_instr_load acc_a dpl dph ⇒ lattice_join (lattice_psingleton dpl) (lattice_psingleton dph) 183 191 (* Reads the hardware registers that are used to pass parameters. *) 184  ertl_st_call_id _ nparams _ ⇒ 185 〈[ ], list_set_of_list (prefix ? nparams RegisterParameters)〉 186  ertl_st_get_hdw _ r _ ⇒ lattice_hsingleton r 187  ertl_st_hdw_to_hdw _ r _ ⇒ lattice_hsingleton r 188  ertl_st_set_hdw _ r _ ⇒ lattice_psingleton r 189  ertl_st_push r _ ⇒ lattice_psingleton r 190  ertl_st_move _ r _ ⇒ lattice_psingleton r 191  ertl_st_op1 _ _ r _ ⇒ lattice_psingleton r 192  ertl_st_cond r _ _ ⇒ lattice_psingleton r 193  ertl_st_op2 op2 _ r1 r2 _ ⇒ 194 match op2 with 195 [ Addc ⇒ 196 lattice_join (lattice_join (lattice_psingleton r1) (lattice_psingleton r2)) (lattice_hsingleton RegisterCarry) 197  _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2) 198 ] 199  ertl_st_opaccs _ d1 d2 s1 s2 _ ⇒ lattice_join (lattice_psingleton s1) (lattice_psingleton s2) 200  ertl_st_load _ r1 r2 _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2) 201  ertl_st_store r1 r2 r3 _ ⇒ 202 lattice_join (lattice_join (lattice_psingleton r1) (lattice_psingleton r2)) (lattice_psingleton r3) 203  ertl_st_new_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH) 204  ertl_st_del_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH) 205  ertl_st_return ⇒ 〈[ ], list_set_union ? eq_Register RegisterCalleeSaved ret_regs〉 206 ]. 207 208 definition eliminable: register_lattice → ertl_statement → option label ≝ 209 λl. 210 λstmt. 192  joint_instr_call_id _ nparams ⇒ 〈[ ], list_set_of_list (prefix ? nparams RegisterParams)〉 193  joint_instr_comment c ⇒ lattice_bottom 194  joint_instr_cond r lbl_true ⇒ lattice_psingleton r 195  joint_instr_store acc_a dpl dph ⇒ 196 lattice_join (lattice_join (lattice_psingleton acc_a) (lattice_psingleton dpl)) (lattice_psingleton dph) 197  joint_instr_cost_label clabel ⇒ lattice_bottom 198  joint_instr_push r ⇒ lattice_psingleton r 199  joint_instr_move pair_reg ⇒ 200 (* only second reg in pair relevant *) 201 let r2 ≝ \snd pair_reg in 202 match r2 with 203 [ pseudo p ⇒ lattice_psingleton p 204  hardware h ⇒ lattice_hsingleton h 205 ] 206 ] 207  joint_st_return ⇒ 〈[ ], list_set_union ? eq_Register RegisterCalleeSaved ret_regs〉 208  joint_st_goto l ⇒ lattice_bottom 209  joint_st_extension ext ⇒ 210 match ext with 211 [ ertl_st_ext_new_frame l ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH) 212  ertl_st_ext_del_frame l ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH) 213  ertl_st_ext_frame_size r l ⇒ lattice_bottom 214 ] 215 ]. 216 217 definition eliminable ≝ 218 λglobals: list ident. 219 λl: register_lattice. 220 λs: ertl_statement globals. 211 221 let 〈pliveafter, hliveafter〉 ≝ l in 212 match stmt with 213 [ ertl_st_skip _ ⇒ None ? 214  ertl_st_comment _ _ ⇒ None ? 215  ertl_st_cost _ _ ⇒ None ? 216  ertl_st_new_frame _ ⇒ None ? 217  ertl_st_del_frame _ ⇒ None ? 218  ertl_st_pop _ _ ⇒ None ? 219  ertl_st_push _ _ ⇒ None ? 220  ertl_st_clear_carry _ ⇒ None ? 221  ertl_st_set_carry _ ⇒ None ? 222  ertl_st_store _ _ _ _ ⇒ None ? 223  ertl_st_call_id _ _ _ ⇒ None ? 224  ertl_st_cond _ _ _ ⇒ None ? 225  ertl_st_return ⇒ None ? 226  ertl_st_get_hdw r _ l ⇒ 227 if list_set_member register (eq_identifier ?) r pliveafter ∨ 228 list_set_member Register eq_Register RegisterCarry hliveafter then 229 None ? 230 else 231 Some ? l 232  ertl_st_frame_size r l ⇒ 233 if list_set_member register (eq_identifier ?) r pliveafter ∨ 234 list_set_member Register eq_Register RegisterCarry hliveafter then 235 None ? 236 else 237 Some ? l 238  ertl_st_int r _ l ⇒ 239 if list_set_member register (eq_identifier ?) r pliveafter ∨ 240 list_set_member Register eq_Register RegisterCarry hliveafter then 241 None ? 242 else 243 Some ? l 244  ertl_st_addr r1 r2 _ l ⇒ 245 if list_set_member register (eq_identifier ?) r1 pliveafter ∨ 246 list_set_member register (eq_identifier ?) r2 pliveafter ∨ 247 list_set_member Register eq_Register RegisterCarry hliveafter then 248 None ? 249 else 250 Some ? l 251  ertl_st_move r _ l ⇒ 252 if list_set_member register (eq_identifier ?) r pliveafter ∨ 253 list_set_member Register eq_Register RegisterCarry hliveafter then 254 None ? 255 else 256 Some ? l 257  ertl_st_opaccs _ d1 d2 _ _ l ⇒ 258 if list_set_member register (eq_identifier ?) d1 pliveafter ∨ 259 list_set_member register (eq_identifier ?) d2 pliveafter ∨ 260 list_set_member Register eq_Register RegisterCarry hliveafter then 261 None ? 262 else 263 Some ? l 264  ertl_st_op1 _ r _ l ⇒ 265 if list_set_member register (eq_identifier ?) r pliveafter ∨ 266 list_set_member Register eq_Register RegisterCarry hliveafter then 267 None ? 268 else 269 Some ? l 270  ertl_st_op2 _ r _ _ l ⇒ 271 if list_set_member register (eq_identifier ?) r pliveafter ∨ 272 list_set_member Register eq_Register RegisterCarry hliveafter then 273 None ? 274 else 275 Some ? l 276  ertl_st_load r _ _ l ⇒ 277 if list_set_member register (eq_identifier ?) r pliveafter ∨ 278 list_set_member Register eq_Register RegisterCarry hliveafter then 279 None ? 280 else 281 Some ? l 282  ertl_st_set_hdw r _ l ⇒ 283 if list_set_member Register eq_Register r hliveafter then 284 None ? 285 else 286 Some ? l 287  ertl_st_hdw_to_hdw r _ l ⇒ 288 if list_set_member Register eq_Register r hliveafter then 289 None ? 290 else 291 Some ? l 292 ]. 293 294 definition statement_semantics: ertl_statement → register_lattice → register_lattice ≝ 222 match s with 223 [ joint_st_sequential seq l ⇒ 224 match seq with 225 [ joint_instr_op2 op2 acc_a r ⇒ 226 if list_set_member register (eq_identifier ?) acc_a pliveafter ∨ 227 list_set_member Register eq_Register RegisterCarry hliveafter then 228 None ? 229 else 230 Some ? l 231  joint_instr_clear_carry ⇒ None ? 232  joint_instr_set_carry ⇒ None ? 233  joint_instr_opaccs opaccs r1 r2 ⇒ 234 if list_set_member register (eq_identifier ?) r1 pliveafter ∨ 235 list_set_member register (eq_identifier ?) r2 pliveafter ∨ 236 list_set_member Register eq_Register RegisterCarry hliveafter then 237 None ? 238 else 239 Some ? l 240  joint_instr_op1 op1 r ⇒ 241 if list_set_member register (eq_identifier ?) r pliveafter ∨ 242 list_set_member Register eq_Register RegisterCarry hliveafter then 243 None ? 244 else 245 Some ? l 246  joint_instr_pop r ⇒ None ? 247  joint_instr_int r _ ⇒ 248 if list_set_member register (eq_identifier ?) r pliveafter ∨ 249 list_set_member Register eq_Register RegisterCarry hliveafter then 250 None ? 251 else 252 Some ? l 253  joint_instr_address _ _ r1 r2 ⇒ 254 if list_set_member register (eq_identifier ?) r1 pliveafter ∨ 255 list_set_member register (eq_identifier ?) r2 pliveafter ∨ 256 list_set_member Register eq_Register RegisterCarry hliveafter then 257 None ? 258 else 259 Some ? l 260  joint_instr_load acc_a dpl dph ⇒ 261 if list_set_member register (eq_identifier ?) acc_a pliveafter ∨ 262 list_set_member Register eq_Register RegisterCarry hliveafter then 263 None ? 264 else 265 Some ? l 266  joint_instr_call_id _ nparams ⇒ None ? 267  joint_instr_comment c ⇒ None ? 268  joint_instr_cond r lbl_true ⇒ None ? 269  joint_instr_store acc_a dpl dph ⇒ None ? 270  joint_instr_cost_label clabel ⇒ None ? 271  joint_instr_push r ⇒ None ? 272  joint_instr_move pair_reg ⇒ 273 let r1 ≝ \fst pair_reg in 274 let r2 ≝ \snd pair_reg in 275 match r1 with 276 [ pseudo p1 ⇒ 277 if list_set_member register (eq_identifier ?) p1 pliveafter ∨ 278 list_set_member Register eq_Register RegisterCarry hliveafter then 279 None ? 280 else 281 Some ? l 282  hardware h1 ⇒ 283 if list_set_member Register eq_Register h1 hliveafter then 284 None ? 285 else 286 Some ? l 287 ] 288 ] 289  joint_st_goto l ⇒ None ? 290  joint_st_return ⇒ None ? 291  joint_st_extension ext ⇒ 292 match ext with 293 [ ertl_st_ext_new_frame l ⇒ None ? 294  ertl_st_ext_del_frame l ⇒ None ? 295  ertl_st_ext_frame_size r l ⇒ 296 if list_set_member register (eq_identifier ?) r pliveafter ∨ 297 list_set_member Register eq_Register RegisterCarry hliveafter then 298 None ? 299 else 300 Some ? l 301 ] 302 ]. 303 304 definition statement_semantics: ∀globals: list ident. ertl_statement globals → register_lattice → register_lattice ≝ 305 λglobals. 295 306 λstmt. 296 307 λliveafter. 297 match eliminable liveafter stmt with298 [ None ⇒ lattice_join (lattice_diff liveafter (defined stmt)) (usedstmt)308 match eliminable globals liveafter stmt with 309 [ None ⇒ lattice_join (lattice_diff liveafter (defined globals stmt)) (used globals stmt) 299 310  Some l ⇒ liveafter 300 311 ]. … … 307 318 308 319 definition livebefore ≝ 320 λglobals: list ident. 309 321 λint_fun. 310 322 λlabel. 311 323 λliveafter: valuation. 312 match lookup ? ? (ertl_if_graph int_fun) label with324 match lookup ? ? (ertl_if_graph globals int_fun) label with 313 325 [ None ⇒ ? 314  Some stmt ⇒ statement_semantics stmt (liveafter label)326  Some stmt ⇒ statement_semantics globals stmt (liveafter label) 315 327 ]. 316 328 cases not_implemented (* XXX *) … … 318 330 319 331 definition liveafter ≝ 332 λglobals. 320 333 λint_fun. 321 334 λlivebefore. 322 335 λlabel. 323 336 λliveafter: valuation. 324 match lookup ? ? (ertl_if_graphint_fun) label with337 match lookup … (ertl_if_graph globals int_fun) label with 325 338 [ None ⇒ ? 326  Some stmt ⇒ list_set_fold ? ? (λsuccessor. λaccu.339  Some stmt ⇒ list_set_fold … (λsuccessor. λaccu: register_lattice. 327 340 lattice_join (livebefore successor liveafter) accu) 328 lattice_bottom (statement_successors stmt)341 lattice_bottom (statement_successors globals stmt) 329 342 ]. 330 343 cases not_implemented (* XXX *) 331 344 qed. 332 345 333 definition analyse: ertl_internal_function → valuation ≝ 346 definition analyse ≝ 347 λglobals. 334 348 λint_fun. 335 fix_lfp (liveafter int_fun (livebeforeint_fun)).349 fix_lfp (liveafter globals int_fun (livebefore globals int_fun)).
Note: See TracChangeset
for help on using the changeset viewer.