[1088] | 1 | include "ASM/Util.ma". |
---|
| 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 | |
---|
[1107] | 32 | definition list_set_member ≝ member. |
---|
[1094] | 33 | |
---|
[1107] | 34 | definition list_set_fold ≝ foldr. |
---|
| 35 | |
---|
[1088] | 36 | definition statement_successors ≝ |
---|
| 37 | λs: ertl_statement. |
---|
| 38 | match s with |
---|
[1124] | 39 | [ ertl_st_return ⇒ [ ] |
---|
[1088] | 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 ] |
---|
[1144] | 51 | | ertl_st_addr _ _ _ l ⇒ [ l ] |
---|
[1088] | 52 | | ertl_st_int _ _ l ⇒ [ l ] |
---|
| 53 | | ertl_st_move _ _ l ⇒ [ l ] |
---|
[1144] | 54 | | ertl_st_opaccs _ _ _ _ _ l ⇒ [ l ] |
---|
[1088] | 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 ] |
---|
| 64 | ]. |
---|
| 65 | |
---|
| 66 | definition register_lattice ≝ (list register) × (list Register). |
---|
| 67 | definition lattice_property ≝ register_lattice. |
---|
| 68 | definition lattice_bottom: register_lattice ≝ 〈[ ], [ ]〉. |
---|
| 69 | definition lattice_psingleton: register → register_lattice ≝ |
---|
| 70 | λr. |
---|
| 71 | 〈[ r ], [ ]〉. |
---|
| 72 | definition lattice_hsingleton: Register → register_lattice ≝ |
---|
| 73 | λr. |
---|
| 74 | 〈[ ], [ r ]〉. |
---|
| 75 | |
---|
| 76 | definition lattice_join: register_lattice → register_lattice → register_lattice ≝ |
---|
| 77 | λleft. |
---|
| 78 | λright. |
---|
| 79 | let 〈lp, lh〉 ≝ left in |
---|
| 80 | let 〈rp, rh〉 ≝ right in |
---|
| 81 | 〈list_set_union ? (eq_identifier ?) lp rp, list_set_union ? eq_Register lh rh〉. |
---|
| 82 | |
---|
| 83 | definition lattice_diff: register_lattice → register_lattice → register_lattice ≝ |
---|
| 84 | λleft. |
---|
| 85 | λright. |
---|
| 86 | let 〈lp, lh〉 ≝ left in |
---|
| 87 | let 〈rp, rh〉 ≝ right in |
---|
| 88 | 〈list_set_diff ? (eq_identifier ?) lp rp, list_set_diff ? eq_Register lh rh〉. |
---|
| 89 | |
---|
| 90 | definition lattice_equal: register_lattice → register_lattice → bool ≝ |
---|
| 91 | λleft. |
---|
| 92 | λright. |
---|
| 93 | let 〈lp, lh〉 ≝ left in |
---|
| 94 | let 〈rp, rh〉 ≝ right in |
---|
| 95 | andb (list_set_equal ? (eq_identifier ?) lp rp) (list_set_equal ? eq_Register lh rh). |
---|
| 96 | |
---|
| 97 | definition lattice_is_maximal: register_lattice → bool ≝ λl. false. |
---|
| 98 | |
---|
[1124] | 99 | record lattice_property_sig: Type[1] ≝ |
---|
| 100 | { |
---|
| 101 | lp_type : Type[0]; |
---|
| 102 | lp_property : Type[0]; |
---|
| 103 | lp_bottom : lp_type; |
---|
| 104 | lp_psingleton: register → lp_type; |
---|
| 105 | lp_hsingleton: Register → lp_type; |
---|
| 106 | lp_join : lp_type → lp_type → lp_type; |
---|
| 107 | lp_diff : lp_type → lp_type → lp_type; |
---|
| 108 | lp_equal : lp_type → lp_type → bool; |
---|
| 109 | lp_is_maximal: lp_type → bool |
---|
| 110 | }. |
---|
| 111 | |
---|
| 112 | definition property ≝ |
---|
| 113 | mk_lattice_property_sig |
---|
| 114 | ((list register) × (list Register)) |
---|
| 115 | lattice_property |
---|
| 116 | lattice_bottom |
---|
| 117 | lattice_psingleton |
---|
| 118 | lattice_hsingleton |
---|
| 119 | lattice_join |
---|
| 120 | lattice_diff |
---|
| 121 | lattice_equal |
---|
| 122 | lattice_is_maximal. |
---|
| 123 | |
---|
[1088] | 124 | definition defined: ertl_statement → register_lattice ≝ |
---|
| 125 | λs. |
---|
| 126 | 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 |
---|
[1124] | 133 | | ertl_st_return ⇒ lattice_bottom |
---|
[1094] | 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 |
---|
[1144] | 148 | | ertl_st_addr r1 r2 _ _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2) |
---|
[1094] | 149 | | ertl_st_move r _ _ ⇒ lattice_psingleton r |
---|
[1144] | 150 | (* XXX: change from o'caml *) |
---|
| 151 | | ertl_st_opaccs _ r1 r2 _ _ _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2) |
---|
[1094] | 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 caller-save 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) |
---|
[1088] | 159 | ]. |
---|
| 160 | |
---|
[1094] | 161 | definition list_set_of_list ≝ |
---|
| 162 | λrl. |
---|
| 163 | foldr ? ? (list_set_add Register eq_Register) rl [ ]. |
---|
| 164 | |
---|
| 165 | definition list_set_of_list2 ≝ |
---|
| 166 | let f ≝ λset. λr. list_set_add Register eq_Register r set in |
---|
| 167 | foldl ? ? f [ ]. |
---|
| 168 | |
---|
| 169 | definition ret_regs ≝ list_set_of_list RegisterRets. |
---|
| 170 | |
---|
| 171 | definition used: ertl_statement → register_lattice ≝ |
---|
| 172 | λstmt. |
---|
[1088] | 173 | match stmt with |
---|
[1094] | 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 |
---|
[1144] | 179 | | ertl_st_addr _ _ _ _ ⇒ lattice_bottom |
---|
[1094] | 180 | | ertl_st_int _ _ _ ⇒ lattice_bottom |
---|
| 181 | | ertl_st_clear_carry _ ⇒ lattice_bottom |
---|
| 182 | | ertl_st_set_carry _ ⇒ lattice_bottom |
---|
| 183 | (* Reads the hardware registers that are used to pass parameters. *) |
---|
| 184 | | ertl_st_call_id _ nparams _ ⇒ |
---|
[1144] | 185 | 〈[ ], list_set_of_list (prefix ? nparams RegisterParameters)〉 |
---|
[1094] | 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 | ] |
---|
[1144] | 199 | | ertl_st_opaccs _ d1 d2 s1 s2 _ ⇒ lattice_join (lattice_psingleton s1) (lattice_psingleton s2) |
---|
[1094] | 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) |
---|
[1124] | 205 | | ertl_st_return ⇒ 〈[ ], list_set_union ? eq_Register RegisterCalleeSaved ret_regs〉 |
---|
[1094] | 206 | ]. |
---|
| 207 | |
---|
| 208 | definition eliminable: register_lattice → ertl_statement → option label ≝ |
---|
| 209 | λl. |
---|
| 210 | λstmt. |
---|
| 211 | 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 ? |
---|
[1124] | 225 | | ertl_st_return ⇒ None ? |
---|
[1094] | 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 |
---|
[1144] | 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 ∨ |
---|
[1094] | 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 |
---|
[1144] | 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 ∨ |
---|
[1094] | 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 ≝ |
---|
| 295 | λstmt. |
---|
| 296 | λliveafter. |
---|
| 297 | match eliminable liveafter stmt with |
---|
| 298 | [ None ⇒ lattice_join (lattice_diff liveafter (defined stmt)) (used stmt) |
---|
| 299 | | Some l ⇒ liveafter |
---|
| 300 | ]. |
---|
| 301 | |
---|
| 302 | definition valuation ≝ label → register_lattice. |
---|
[1124] | 303 | definition rhs ≝ valuation → lattice_property. |
---|
| 304 | definition equations ≝ label → rhs. |
---|
[1094] | 305 | |
---|
[1124] | 306 | axiom fix_lfp: equations → valuation. |
---|
| 307 | |
---|
| 308 | definition livebefore ≝ |
---|
| 309 | λint_fun. |
---|
| 310 | λlabel. |
---|
| 311 | λliveafter: valuation. |
---|
| 312 | match lookup ? ? (ertl_if_graph int_fun) label with |
---|
| 313 | [ None ⇒ ? |
---|
| 314 | | Some stmt ⇒ statement_semantics stmt (liveafter label) |
---|
| 315 | ]. |
---|
| 316 | cases not_implemented (* XXX *) |
---|
| 317 | qed. |
---|
| 318 | |
---|
| 319 | definition liveafter ≝ |
---|
| 320 | λint_fun. |
---|
| 321 | λlivebefore. |
---|
| 322 | λlabel. |
---|
| 323 | λliveafter: valuation. |
---|
| 324 | match lookup ? ? (ertl_if_graph int_fun) label with |
---|
| 325 | [ None ⇒ ? |
---|
| 326 | | Some stmt ⇒ list_set_fold ? ? (λsuccessor. λaccu. |
---|
| 327 | lattice_join (livebefore successor liveafter) accu) |
---|
| 328 | lattice_bottom (statement_successors stmt) |
---|
| 329 | ]. |
---|
| 330 | cases not_implemented (* XXX *) |
---|
| 331 | qed. |
---|
| 332 | |
---|
[1094] | 333 | definition analyse: ertl_internal_function → valuation ≝ |
---|
| 334 | λint_fun. |
---|
[1124] | 335 | fix_lfp (liveafter int_fun (livebefore int_fun)). |
---|