Changeset 1098 for Deliverables/D3.3/id-lookup-branch/ERTL
- Timestamp:
- Aug 3, 2011, 2:48:11 PM (10 years ago)
- Location:
- Deliverables/D3.3/id-lookup-branch
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D3.3/id-lookup-branch
-
Deliverables/D3.3/id-lookup-branch/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 caller-save 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 caller-save 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.