Changeset 1098 for Deliverables/D3.3/idlookupbranch/ERTL/liveness.ma
 Timestamp:
 Aug 3, 2011, 2:48:11 PM (9 years ago)
 Location:
 Deliverables/D3.3/idlookupbranch
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.3/idlookupbranch

Deliverables/D3.3/idlookupbranch/ERTL/liveness.ma
r1091 r1098 30 30 λr: list A. 31 31 foldr ? ? andb true (map ? ? (λx. member A eq_a x r) l). 32 33 definition list_set_member ≝ 34 λA: Type[0]. 35 λeq_a: A → A → bool. 36 λa: A. 37 λl: list A. 38 member A eq_a a l. 32 39 33 40 definition statement_successors ≝ … … 106 113  ertl_st_cond _ _ _ ⇒ lattice_bottom 107 114  ertl_st_return _ ⇒ lattice_bottom 108  ertl_st_clear_carry _ ⇒ 〈[ ], [ RegisterCarry ]〉 109  ertl_st_set_carry _ ⇒ 〈[ ], [ RegisterCarry ]〉 110  _ ⇒ ? 111 ]. 112 113 let defined (stmt : statement) : L.t = 115  ertl_st_clear_carry _ ⇒ lattice_hsingleton RegisterCarry 116  ertl_st_set_carry _ ⇒ lattice_hsingleton RegisterCarry 117  ertl_st_op2 op2 r _ _ _ ⇒ 118 match op2 with 119 [ Add ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r) 120  Addc ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r) 121  Sub ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r) 122  _ ⇒ lattice_psingleton r 123 ] 124  ertl_st_op1 op1 r _ _ ⇒ lattice_psingleton r 125  ertl_st_get_hdw r _ _ ⇒ lattice_psingleton r 126  ertl_st_frame_size r _ ⇒ lattice_psingleton r 127  ertl_st_pop r _ ⇒ lattice_psingleton r 128  ertl_st_int r _ _ ⇒ lattice_psingleton r 129  ertl_st_addr_h r _ _ ⇒ lattice_psingleton r 130  ertl_st_addr_l r _ _ ⇒ lattice_psingleton r 131  ertl_st_move r _ _ ⇒ lattice_psingleton r 132  ertl_st_opaccs_a _ r _ _ _ ⇒ lattice_psingleton r 133  ertl_st_opaccs_b _ r _ _ _ ⇒ lattice_psingleton r 134  ertl_st_load r _ _ _ ⇒ lattice_psingleton r 135  ertl_st_set_hdw r _ _ ⇒ lattice_hsingleton r 136  ertl_st_hdw_to_hdw r _ _ ⇒ lattice_hsingleton r 137 (* Potentially destroys all callersave hardware registers. *) 138  ertl_st_call_id _ _ _ ⇒ 〈[ ], RegisterCallerSaved〉 139  ertl_st_new_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH) 140  ertl_st_del_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH) 141 ]. 142 143 definition list_set_of_list ≝ 144 λrl. 145 foldr ? ? (list_set_add Register eq_Register) rl [ ]. 146 147 definition list_set_of_list2 ≝ 148 let f ≝ λset. λr. list_set_add Register eq_Register r set in 149 foldl ? ? f [ ]. 150 151 definition ret_regs ≝ list_set_of_list RegisterRets. 152 153 definition used: ertl_statement → register_lattice ≝ 154 λstmt. 114 155 match stmt with 115  St_clear_carry _ 116  St_set_carry _ > 117 Register.Set.empty, I8051.RegisterSet.singleton I8051.carry 118  St_op2 (I8051.Add, r, _, _, _) 119  St_op2 (I8051.Addc, r, _, _, _) 120  St_op2 (I8051.Sub, r, _, _, _) > 121 L.join (L.hsingleton I8051.carry) (L.psingleton r) 122  St_op1 (I8051.Inc, r, _, _) 123  St_get_hdw (r, _, _) 124  St_framesize (r, _) 125  St_pop (r, _) 126  St_int (r, _, _) 127  St_addrH (r, _, _) 128  St_addrL (r, _, _) 129  St_move (r, _, _) 130  St_opaccsA (_, r, _, _, _) 131  St_opaccsB (_, r, _, _, _) 132  St_op1 (_, r, _, _) 133  St_op2 (_, r, _, _, _) 134  St_load (r, _, _, _) > 135 L.psingleton r 136  St_set_hdw (r, _, _) 137  St_hdw_to_hdw (r, _, _) > 138 L.hsingleton r 139  St_call_id _ > 140 (* Potentially destroys all callersave hardware registers. *) 141 Register.Set.empty, I8051.caller_saved 142  St_newframe _ 143  St_delframe _ > 144 L.join (L.hsingleton I8051.spl) (L.hsingleton I8051.sph) 156 [ ertl_st_skip _ ⇒ lattice_bottom 157  ertl_st_cost _ _ ⇒ lattice_bottom 158  ertl_st_comment _ _ ⇒ lattice_bottom 159  ertl_st_frame_size _ _ ⇒ lattice_bottom 160  ertl_st_pop _ _ ⇒ lattice_bottom 161  ertl_st_addr_h _ _ _ ⇒ lattice_bottom 162  ertl_st_addr_l _ _ _ ⇒ lattice_bottom 163  ertl_st_int _ _ _ ⇒ lattice_bottom 164  ertl_st_clear_carry _ ⇒ lattice_bottom 165  ertl_st_set_carry _ ⇒ lattice_bottom 166 (* Reads the hardware registers that are used to pass parameters. *) 167  ertl_st_call_id _ nparams _ ⇒ 168 〈[ ], list_set_of_list (prefix ? (nat_of_bitvector ? nparams) RegisterParameters)〉 169  ertl_st_get_hdw _ r _ ⇒ lattice_hsingleton r 170  ertl_st_hdw_to_hdw _ r _ ⇒ lattice_hsingleton r 171  ertl_st_set_hdw _ r _ ⇒ lattice_psingleton r 172  ertl_st_push r _ ⇒ lattice_psingleton r 173  ertl_st_move _ r _ ⇒ lattice_psingleton r 174  ertl_st_op1 _ _ r _ ⇒ lattice_psingleton r 175  ertl_st_cond r _ _ ⇒ lattice_psingleton r 176  ertl_st_op2 op2 _ r1 r2 _ ⇒ 177 match op2 with 178 [ Addc ⇒ 179 lattice_join (lattice_join (lattice_psingleton r1) (lattice_psingleton r2)) (lattice_hsingleton RegisterCarry) 180  _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2) 181 ] 182  ertl_st_opaccs_a _ _ r1 r2 _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2) 183  ertl_st_opaccs_b _ _ r1 r2 _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2) 184  ertl_st_load _ r1 r2 _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2) 185  ertl_st_store r1 r2 r3 _ ⇒ 186 lattice_join (lattice_join (lattice_psingleton r1) (lattice_psingleton r2)) (lattice_psingleton r3) 187  ertl_st_new_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH) 188  ertl_st_del_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH) 189  ertl_st_return _ ⇒ 〈[ ], list_set_union ? eq_Register RegisterCalleeSaved ret_regs〉 190 ]. 191 192 definition eliminable: register_lattice → ertl_statement → option label ≝ 193 λl. 194 λstmt. 195 let 〈pliveafter, hliveafter〉 ≝ l in 196 match stmt with 197 [ ertl_st_skip _ ⇒ None ? 198  ertl_st_comment _ _ ⇒ None ? 199  ertl_st_cost _ _ ⇒ None ? 200  ertl_st_new_frame _ ⇒ None ? 201  ertl_st_del_frame _ ⇒ None ? 202  ertl_st_pop _ _ ⇒ None ? 203  ertl_st_push _ _ ⇒ None ? 204  ertl_st_clear_carry _ ⇒ None ? 205  ertl_st_set_carry _ ⇒ None ? 206  ertl_st_store _ _ _ _ ⇒ None ? 207  ertl_st_call_id _ _ _ ⇒ None ? 208  ertl_st_cond _ _ _ ⇒ None ? 209  ertl_st_return _ ⇒ None ? 210  ertl_st_get_hdw r _ l ⇒ 211 if list_set_member register (eq_identifier ?) r pliveafter ∨ 212 list_set_member Register eq_Register RegisterCarry hliveafter then 213 None ? 214 else 215 Some ? l 216  ertl_st_frame_size r l ⇒ 217 if list_set_member register (eq_identifier ?) r pliveafter ∨ 218 list_set_member Register eq_Register RegisterCarry hliveafter then 219 None ? 220 else 221 Some ? l 222  ertl_st_int r _ l ⇒ 223 if list_set_member register (eq_identifier ?) r pliveafter ∨ 224 list_set_member Register eq_Register RegisterCarry hliveafter then 225 None ? 226 else 227 Some ? l 228  ertl_st_addr_h r _ l ⇒ 229 if list_set_member register (eq_identifier ?) r pliveafter ∨ 230 list_set_member Register eq_Register RegisterCarry hliveafter then 231 None ? 232 else 233 Some ? l 234  ertl_st_addr_l r _ l ⇒ 235 if list_set_member register (eq_identifier ?) r pliveafter ∨ 236 list_set_member Register eq_Register RegisterCarry hliveafter then 237 None ? 238 else 239 Some ? l 240  ertl_st_move r _ l ⇒ 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  ertl_st_opaccs_a _ r _ _ l ⇒ 247 if list_set_member register (eq_identifier ?) r pliveafter ∨ 248 list_set_member Register eq_Register RegisterCarry hliveafter then 249 None ? 250 else 251 Some ? l 252  ertl_st_opaccs_b _ r _ _ l ⇒ 253 if list_set_member register (eq_identifier ?) r pliveafter ∨ 254 list_set_member Register eq_Register RegisterCarry hliveafter then 255 None ? 256 else 257 Some ? l 258  ertl_st_op1 _ r _ l ⇒ 259 if list_set_member register (eq_identifier ?) r pliveafter ∨ 260 list_set_member Register eq_Register RegisterCarry hliveafter then 261 None ? 262 else 263 Some ? l 264  ertl_st_op2 _ 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_load 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_set_hdw r _ l ⇒ 277 if list_set_member Register eq_Register r hliveafter then 278 None ? 279 else 280 Some ? l 281  ertl_st_hdw_to_hdw r _ l ⇒ 282 if list_set_member Register eq_Register r hliveafter then 283 None ? 284 else 285 Some ? l 286 ]. 287 288 definition statement_semantics: ertl_statement → register_lattice → register_lattice ≝ 289 λstmt. 290 λliveafter. 291 match eliminable liveafter stmt with 292 [ None ⇒ lattice_join (lattice_diff liveafter (defined stmt)) (used stmt) 293  Some l ⇒ liveafter 294 ]. 295 296 definition valuation ≝ label → register_lattice. 297 298 definition analyse: ertl_internal_function → valuation ≝ 299 λint_fun. 300 let livebefore ≝ λlabel. λliveafter: valuation. 301 match lookup ? ? (ertl_if_graph int_fun) label with 302 [ None ⇒ ? 303  Some stmt ⇒ statement_semantics stmt (liveafter label) 304 ] 305 in ?.
Note: See TracChangeset
for help on using the changeset viewer.