Changeset 1223 for src/ERTL/liveness.ma
- Timestamp:
- Sep 16, 2011, 5:15:35 PM (10 years ago)
- File:
-
- 1 edited
-
src/ERTL/liveness.ma (modified) (17 diffs)
Legend:
- Unmodified
- Added
- Removed
-
src/ERTL/liveness.ma
r1185 r1223 1 1 include "ASM/Util.ma". 2 2 include "ERTL/ERTL.ma". 3 4 definition list_set_union ≝ 5 λA: Type[0]. 6 λeq_a: A → A → bool. 7 λl: list A. 8 λr: list A. 9 nub_by A eq_a (l @ r). 10 11 definition list_set_add ≝ 12 λA: Type[0]. 13 λeq_a: A → A → bool. 14 λa: A. 15 λs: list A. 16 nub_by A eq_a (a :: s). 17 18 definition list_set_diff ≝ 19 λA: Type[0]. 20 λeq_a: A → A → bool. 21 λl: list A. 22 λr: list A. 23 filter A (λx. member A eq_a x r) l. 24 25 definition list_set_equal ≝ 26 λA: Type[0]. 27 λeq_a: A → A → bool. 28 λl: list A. 29 λr: list A. 30 foldr ? ? andb true (map ? ? (λx. member A eq_a x r) l). 31 32 definition list_set_member ≝ member. 33 34 definition list_set_fold ≝ foldr. 3 include "utilities/adt/set_adt.ma". 35 4 36 5 definition statement_successors ≝ … … 41 10 match seq with 42 11 [ joint_instr_cond acc_a_reg lbl_true ⇒ 43 list_set_add ? (eq_identifier ?) lbl_true [ l ]44 | _ ⇒ [ l ]12 set_insert … lbl_true (set_singleton … l) 13 | _ ⇒ set_singleton … l 45 14 ] 46 15 | joint_st_extension ext ⇒ 47 16 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 ⇒ [ ]54 ]. 55 56 definition register_lattice ≝ ( list register) × (list Register).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 ] 21 | joint_st_goto l ⇒ set_singleton … l 22 | joint_st_return ⇒ set_empty … 23 ]. 24 25 definition register_lattice ≝ (set register) × (set Register). 57 26 definition lattice_property ≝ register_lattice. 58 definition lattice_bottom: register_lattice ≝ 〈 [ ], [ ]〉.27 definition lattice_bottom: register_lattice ≝ 〈set_empty register, set_empty Register〉. 59 28 definition lattice_psingleton: register → register_lattice ≝ 60 29 λr. 61 〈 [ r ], [ ]〉.30 〈set_singleton … r, set_empty …〉. 62 31 definition lattice_hsingleton: Register → register_lattice ≝ 63 32 λr. 64 〈 [ ], [ r ]〉.33 〈set_empty …, set_singleton … r〉. 65 34 66 35 definition lattice_join: register_lattice → register_lattice → register_lattice ≝ … … 69 38 let 〈lp, lh〉 ≝ left in 70 39 let 〈rp, rh〉 ≝ right in 71 〈 list_set_union ? (eq_identifier ?) lp rp, list_set_union ? eq_Registerlh rh〉.40 〈set_union … lp rp, set_union … lh rh〉. 72 41 73 42 definition lattice_diff: register_lattice → register_lattice → register_lattice ≝ … … 76 45 let 〈lp, lh〉 ≝ left in 77 46 let 〈rp, rh〉 ≝ right in 78 〈 list_set_diff ? (eq_identifier ?) lp rp, list_set_diff ? eq_Registerlh rh〉.47 〈set_diff … lp rp, set_diff … lh rh〉. 79 48 80 49 definition lattice_equal: register_lattice → register_lattice → bool ≝ … … 83 52 let 〈lp, lh〉 ≝ left in 84 53 let 〈rp, rh〉 ≝ right in 85 andb ( list_set_equal ? (eq_identifier ?) lp rp) (list_set_equal ?eq_Register lh rh).54 andb (set_equal … (eq_identifier …) lp rp) (set_equal … eq_Register lh rh). 86 55 87 56 definition lattice_is_maximal: register_lattice → bool ≝ λl. false. … … 102 71 definition property ≝ 103 72 mk_lattice_property_sig 104 (( list register) × (list Register))73 ((set register) × (set Register)) 105 74 lattice_property 106 75 lattice_bottom … … 134 103 | joint_instr_load r _ _ ⇒ lattice_psingleton r 135 104 (* Potentially destroys all caller-save hardware registers. *) 136 | joint_instr_call_id _ _ ⇒ 〈 [ ],RegisterCallerSaved〉105 | joint_instr_call_id _ _ ⇒ 〈set_empty …, set_from_list … RegisterCallerSaved〉 137 106 | joint_instr_comment c ⇒ lattice_bottom 138 107 | joint_instr_cond r lbl_true ⇒ lattice_bottom … … 158 127 ]. 159 128 160 definition list_set_of_list ≝ 161 λrl. 162 foldr ? ? (list_set_add Register eq_Register) rl [ ]. 163 164 definition list_set_of_list2 ≝ 165 let f ≝ λset. λr. list_set_add Register eq_Register r set in 166 foldl ? ? f [ ]. 167 168 definition ret_regs ≝ list_set_of_list RegisterRets. 129 definition ret_regs ≝ set_from_list … RegisterRets. 169 130 170 131 definition used ≝ … … 190 151 | joint_instr_load acc_a dpl dph ⇒ lattice_join (lattice_psingleton dpl) (lattice_psingleton dph) 191 152 (* Reads the hardware registers that are used to pass parameters. *) 192 | joint_instr_call_id _ nparams ⇒ 〈 [ ], list_set_of_list(prefix ? nparams RegisterParams)〉153 | joint_instr_call_id _ nparams ⇒ 〈set_empty …, set_from_list … (prefix ? nparams RegisterParams)〉 193 154 | joint_instr_comment c ⇒ lattice_bottom 194 155 | joint_instr_cond r lbl_true ⇒ lattice_psingleton r … … 205 166 ] 206 167 ] 207 | joint_st_return ⇒ 〈 [ ], list_set_union ? eq_Register RegisterCalleeSavedret_regs〉168 | joint_st_return ⇒ 〈set_empty …, set_union … (set_from_list … RegisterCalleeSaved) ret_regs〉 208 169 | joint_st_goto l ⇒ lattice_bottom 209 170 | joint_st_extension ext ⇒ … … 224 185 match seq with 225 186 [ joint_instr_op2 op2 acc_a r ⇒ 226 if list_set_member register (eq_identifier ?) acc_a pliveafter ∨227 list_set_member Registereq_Register RegisterCarry hliveafter then187 if set_member … (eq_identifier …) acc_a pliveafter ∨ 188 set_member … eq_Register RegisterCarry hliveafter then 228 189 None ? 229 190 else … … 232 193 | joint_instr_set_carry ⇒ None ? 233 194 | 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 Registereq_Register RegisterCarry hliveafter then195 if set_member … (eq_identifier …) r1 pliveafter ∨ 196 set_member … (eq_identifier …) r2 pliveafter ∨ 197 set_member … eq_Register RegisterCarry hliveafter then 237 198 None ? 238 199 else 239 200 Some ? l 240 201 | joint_instr_op1 op1 r ⇒ 241 if list_set_member register (eq_identifier ?) r pliveafter ∨242 list_set_member Registereq_Register RegisterCarry hliveafter then202 if set_member … (eq_identifier …) r pliveafter ∨ 203 set_member … eq_Register RegisterCarry hliveafter then 243 204 None ? 244 205 else … … 246 207 | joint_instr_pop r ⇒ None ? 247 208 | joint_instr_int r _ ⇒ 248 if list_set_member register (eq_identifier ?) r pliveafter ∨249 list_set_member Registereq_Register RegisterCarry hliveafter then209 if set_member … (eq_identifier …) r pliveafter ∨ 210 set_member … eq_Register RegisterCarry hliveafter then 250 211 None ? 251 212 else 252 213 Some ? l 253 214 | 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 Registereq_Register RegisterCarry hliveafter then215 if set_member … (eq_identifier …) r1 pliveafter ∨ 216 set_member … (eq_identifier …) r2 pliveafter ∨ 217 set_member … eq_Register RegisterCarry hliveafter then 257 218 None ? 258 219 else 259 220 Some ? l 260 221 | joint_instr_load acc_a dpl dph ⇒ 261 if list_set_member register (eq_identifier ?) acc_a pliveafter ∨262 list_set_member Registereq_Register RegisterCarry hliveafter then222 if set_member ? (eq_identifier …) acc_a pliveafter ∨ 223 set_member … eq_Register RegisterCarry hliveafter then 263 224 None ? 264 225 else … … 275 236 match r1 with 276 237 [ pseudo p1 ⇒ 277 if list_set_member register (eq_identifier ?) p1 pliveafter ∨278 list_set_member Registereq_Register RegisterCarry hliveafter then238 if set_member … (eq_identifier …) p1 pliveafter ∨ 239 set_member … eq_Register RegisterCarry hliveafter then 279 240 None ? 280 241 else 281 242 Some ? l 282 243 | hardware h1 ⇒ 283 if list_set_member Registereq_Register h1 hliveafter then244 if set_member … eq_Register h1 hliveafter then 284 245 None ? 285 246 else … … 294 255 | ertl_st_ext_del_frame l ⇒ None ? 295 256 | ertl_st_ext_frame_size r l ⇒ 296 if list_set_member register (eq_identifier ?) r pliveafter ∨297 list_set_member Registereq_Register RegisterCarry hliveafter then257 if set_member ? (eq_identifier RegisterTag) r pliveafter ∨ 258 set_member ? eq_Register RegisterCarry hliveafter then 298 259 None ? 299 260 else … … 319 280 definition livebefore ≝ 320 281 λglobals: list ident. 321 λint_fun .282 λint_fun: ertl_internal_function globals. 322 283 λlabel. 323 284 λliveafter: valuation. 324 match lookup ? ? ( ertl_if_graph globalsint_fun) label with285 match lookup ? ? (joint_if_graph … int_fun) label with 325 286 [ None ⇒ ? 326 287 | Some stmt ⇒ statement_semantics globals stmt (liveafter label) … … 330 291 331 292 definition liveafter ≝ 332 λglobals .333 λint_fun .334 λlivebefore .293 λglobals: list ident. 294 λint_fun: ertl_internal_function globals. 295 λlivebefore: label → ?. 335 296 λlabel. 336 297 λliveafter: valuation. 337 match lookup … ( ertl_if_graph globalsint_fun) label with298 match lookup … (joint_if_graph … int_fun) label with 338 299 [ None ⇒ ? 339 | Some stmt ⇒ list_set_fold …(λsuccessor. λaccu: register_lattice.300 | Some stmt ⇒ set_fold ? ? (λsuccessor. λaccu: register_lattice. 340 301 lattice_join (livebefore successor liveafter) accu) 341 lattice_bottom (statement_successors globals stmt)302 (statement_successors globals stmt) lattice_bottom 342 303 ]. 343 304 cases not_implemented (* XXX *)
Note: See TracChangeset
for help on using the changeset viewer.
