[1088] | 1 | include "ASM/Util.ma". |
---|
| 2 | include "ERTL/ERTL.ma". |
---|
[1223] | 3 | include "utilities/adt/set_adt.ma". |
---|
[1088] | 4 | |
---|
| 5 | definition statement_successors ≝ |
---|
[1185] | 6 | λglobals: list ident. |
---|
| 7 | λs: ertl_statement globals. |
---|
[1088] | 8 | match s with |
---|
[1282] | 9 | [ sequential seq l ⇒ |
---|
[1185] | 10 | match seq with |
---|
[1282] | 11 | [ COND acc_a_reg lbl_true ⇒ |
---|
[1223] | 12 | set_insert … lbl_true (set_singleton … l) |
---|
[1250] | 13 | | _ ⇒ set_singleton … l ] |
---|
[1282] | 14 | | GOTO l ⇒ set_singleton … l |
---|
| 15 | | RETURN ⇒ set_empty ? |
---|
[1088] | 16 | ]. |
---|
| 17 | |
---|
[1223] | 18 | definition register_lattice ≝ (set register) × (set Register). |
---|
[1088] | 19 | definition lattice_property ≝ register_lattice. |
---|
[1223] | 20 | definition lattice_bottom: register_lattice ≝ 〈set_empty register, set_empty Register〉. |
---|
[1088] | 21 | definition lattice_psingleton: register → register_lattice ≝ |
---|
| 22 | λr. |
---|
[1223] | 23 | 〈set_singleton … r, set_empty …〉. |
---|
[1088] | 24 | definition lattice_hsingleton: Register → register_lattice ≝ |
---|
| 25 | λr. |
---|
[1223] | 26 | 〈set_empty …, set_singleton … r〉. |
---|
[1088] | 27 | |
---|
| 28 | definition lattice_join: register_lattice → register_lattice → register_lattice ≝ |
---|
| 29 | λleft. |
---|
| 30 | λright. |
---|
| 31 | let 〈lp, lh〉 ≝ left in |
---|
| 32 | let 〈rp, rh〉 ≝ right in |
---|
[1223] | 33 | 〈set_union … lp rp, set_union … lh rh〉. |
---|
[1088] | 34 | |
---|
| 35 | definition lattice_diff: register_lattice → register_lattice → register_lattice ≝ |
---|
| 36 | λleft. |
---|
| 37 | λright. |
---|
| 38 | let 〈lp, lh〉 ≝ left in |
---|
| 39 | let 〈rp, rh〉 ≝ right in |
---|
[1223] | 40 | 〈set_diff … lp rp, set_diff … lh rh〉. |
---|
[1088] | 41 | |
---|
| 42 | definition lattice_equal: register_lattice → register_lattice → bool ≝ |
---|
| 43 | λleft. |
---|
| 44 | λright. |
---|
| 45 | let 〈lp, lh〉 ≝ left in |
---|
| 46 | let 〈rp, rh〉 ≝ right in |
---|
[1223] | 47 | andb (set_equal … (eq_identifier …) lp rp) (set_equal … eq_Register lh rh). |
---|
[1088] | 48 | |
---|
| 49 | definition lattice_is_maximal: register_lattice → bool ≝ λl. false. |
---|
| 50 | |
---|
[1124] | 51 | record lattice_property_sig: Type[1] ≝ |
---|
| 52 | { |
---|
| 53 | lp_type : Type[0]; |
---|
| 54 | lp_property : Type[0]; |
---|
| 55 | lp_bottom : lp_type; |
---|
| 56 | lp_psingleton: register → lp_type; |
---|
| 57 | lp_hsingleton: Register → lp_type; |
---|
| 58 | lp_join : lp_type → lp_type → lp_type; |
---|
| 59 | lp_diff : lp_type → lp_type → lp_type; |
---|
| 60 | lp_equal : lp_type → lp_type → bool; |
---|
| 61 | lp_is_maximal: lp_type → bool |
---|
| 62 | }. |
---|
| 63 | |
---|
| 64 | definition property ≝ |
---|
| 65 | mk_lattice_property_sig |
---|
[1223] | 66 | ((set register) × (set Register)) |
---|
[1124] | 67 | lattice_property |
---|
| 68 | lattice_bottom |
---|
| 69 | lattice_psingleton |
---|
| 70 | lattice_hsingleton |
---|
| 71 | lattice_join |
---|
| 72 | lattice_diff |
---|
| 73 | lattice_equal |
---|
| 74 | lattice_is_maximal. |
---|
| 75 | |
---|
[1185] | 76 | definition defined ≝ |
---|
| 77 | λglobals: list ident. |
---|
| 78 | λs: ertl_statement globals. |
---|
[1088] | 79 | match s with |
---|
[1282] | 80 | [ sequential seq l ⇒ |
---|
[1185] | 81 | match seq with |
---|
[1282] | 82 | [ OP2 op2 r1 r2 _ ⇒ |
---|
[1185] | 83 | match op2 with |
---|
[1260] | 84 | [ Add ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r1) |
---|
| 85 | | Addc ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r1) |
---|
| 86 | | Sub ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r1) |
---|
| 87 | | _ ⇒ lattice_psingleton r1 |
---|
[1185] | 88 | ] |
---|
[1282] | 89 | | CLEAR_CARRY ⇒ lattice_hsingleton RegisterCarry |
---|
| 90 | | SET_CARRY ⇒ lattice_hsingleton RegisterCarry |
---|
| 91 | | OPACCS opaccs dr1 dr2 sr1 sr2 ⇒ |
---|
[1275] | 92 | lattice_join (lattice_psingleton dr1) (lattice_psingleton dr2) |
---|
[1282] | 93 | | OP1 op1 r1 r2 ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2) |
---|
| 94 | | POP r ⇒ lattice_psingleton r |
---|
| 95 | | INT r _ ⇒ lattice_psingleton r |
---|
| 96 | | ADDRESS _ _ r1 r2 ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2) |
---|
| 97 | | LOAD r _ _ ⇒ lattice_psingleton r |
---|
[1185] | 98 | (* Potentially destroys all caller-save hardware registers. *) |
---|
[1282] | 99 | | CALL_ID id _ _ ⇒ 〈set_empty …, set_from_list … RegisterCallerSaved〉 |
---|
| 100 | | COMMENT c ⇒ lattice_bottom |
---|
| 101 | | COND r lbl_true ⇒ lattice_bottom |
---|
| 102 | | STORE acc_a dpl dph ⇒ lattice_bottom |
---|
| 103 | | COST_LABEL clabel ⇒ lattice_bottom |
---|
| 104 | | PUSH r ⇒ lattice_bottom |
---|
| 105 | | MOVE pair_reg ⇒ |
---|
[1185] | 106 | (* first register relevant only *) |
---|
| 107 | let r1 ≝ \fst pair_reg in |
---|
| 108 | match r1 with |
---|
| 109 | [ pseudo p ⇒ lattice_psingleton p |
---|
| 110 | | hardware h ⇒ lattice_hsingleton h |
---|
| 111 | ] |
---|
[1282] | 112 | | extension ext ⇒ |
---|
[1250] | 113 | match ext with |
---|
[1260] | 114 | [ ertl_st_ext_new_frame ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH) |
---|
| 115 | | ertl_st_ext_del_frame ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH) |
---|
| 116 | | ertl_st_ext_frame_size r ⇒ lattice_psingleton r]] |
---|
[1282] | 117 | | RETURN ⇒ lattice_bottom |
---|
| 118 | | GOTO l ⇒ lattice_bottom |
---|
[1088] | 119 | ]. |
---|
| 120 | |
---|
[1223] | 121 | definition ret_regs ≝ set_from_list … RegisterRets. |
---|
[1094] | 122 | |
---|
[1185] | 123 | definition used ≝ |
---|
| 124 | λglobals: list ident. |
---|
| 125 | λs: ertl_statement globals. |
---|
| 126 | match s with |
---|
[1282] | 127 | [ sequential seq l ⇒ |
---|
[1185] | 128 | match seq with |
---|
[1282] | 129 | [ OP2 op2 acc_a r1 r2 ⇒ |
---|
[1185] | 130 | match op2 with |
---|
| 131 | [ Addc ⇒ |
---|
[1260] | 132 | lattice_join (lattice_join (lattice_psingleton r1) (lattice_psingleton r2)) (lattice_hsingleton RegisterCarry) |
---|
| 133 | | _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2) |
---|
[1185] | 134 | ] |
---|
[1282] | 135 | | CLEAR_CARRY ⇒ lattice_bottom |
---|
| 136 | | SET_CARRY ⇒ lattice_bottom |
---|
[1185] | 137 | (* acc_a and acc_b *) |
---|
[1282] | 138 | | OPACCS opaccs dr1 dr2 sr1 sr2 ⇒ |
---|
[1275] | 139 | lattice_join (lattice_psingleton sr1) (lattice_psingleton sr2) |
---|
[1282] | 140 | | OP1 op1 r1 r2 ⇒ lattice_psingleton r2 |
---|
| 141 | | POP r ⇒ lattice_bottom |
---|
| 142 | | INT r _ ⇒ lattice_bottom |
---|
| 143 | | ADDRESS _ _ r1 r2 ⇒ lattice_bottom |
---|
| 144 | | LOAD acc_a dpl dph ⇒ lattice_join (lattice_psingleton dpl) (lattice_psingleton dph) |
---|
[1094] | 145 | (* Reads the hardware registers that are used to pass parameters. *) |
---|
[1282] | 146 | | CALL_ID _ nparams _ ⇒ 〈set_empty …, set_from_list … (prefix ? nparams RegisterParams)〉 |
---|
| 147 | | COMMENT c ⇒ lattice_bottom |
---|
| 148 | | COND r lbl_true ⇒ lattice_psingleton r |
---|
| 149 | | STORE acc_a dpl dph ⇒ |
---|
[1185] | 150 | lattice_join (lattice_join (lattice_psingleton acc_a) (lattice_psingleton dpl)) (lattice_psingleton dph) |
---|
[1282] | 151 | | COST_LABEL clabel ⇒ lattice_bottom |
---|
| 152 | | PUSH r ⇒ lattice_psingleton r |
---|
| 153 | | MOVE pair_reg ⇒ |
---|
[1463] | 154 | (* only second reg in paidefinition liveafter ≝ |
---|
| 155 | λglobals: list ident. |
---|
| 156 | λint_fun: ertl_internal_function globals. |
---|
| 157 | λlivebefore: label → ?. |
---|
| 158 | λlabel. |
---|
| 159 | λliveafter: valuation. |
---|
| 160 | match lookup … (joint_if_code … int_fun) label with |
---|
| 161 | [ None ⇒ ? |
---|
| 162 | | Some stmt ⇒ set_fold ? ? (λsuccessor. λaccu: register_lattice. |
---|
| 163 | lattice_join (livebefore successor liveafter) accu) |
---|
| 164 | (statement_successors globals stmt) lattice_bottom |
---|
| 165 | ]. |
---|
| 166 | cases not_implemented (* XXX *) |
---|
| 167 | qed.r relevant *) |
---|
[1185] | 168 | let r2 ≝ \snd pair_reg in |
---|
| 169 | match r2 with |
---|
| 170 | [ pseudo p ⇒ lattice_psingleton p |
---|
| 171 | | hardware h ⇒ lattice_hsingleton h |
---|
| 172 | ] |
---|
[1282] | 173 | | extension ext ⇒ |
---|
[1185] | 174 | match ext with |
---|
[1260] | 175 | [ ertl_st_ext_new_frame ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH) |
---|
| 176 | | ertl_st_ext_del_frame ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH) |
---|
| 177 | | ertl_st_ext_frame_size r ⇒ lattice_bottom]] |
---|
[1282] | 178 | | RETURN ⇒ 〈set_empty …, set_union … (set_from_list … RegisterCalleeSaved) ret_regs〉 |
---|
| 179 | | GOTO l ⇒ lattice_bottom |
---|
[1094] | 180 | ]. |
---|
| 181 | |
---|
[1185] | 182 | definition eliminable ≝ |
---|
| 183 | λglobals: list ident. |
---|
| 184 | λl: register_lattice. |
---|
| 185 | λs: ertl_statement globals. |
---|
[1094] | 186 | let 〈pliveafter, hliveafter〉 ≝ l in |
---|
[1185] | 187 | match s with |
---|
[1282] | 188 | [ sequential seq l ⇒ |
---|
[1185] | 189 | match seq with |
---|
[1282] | 190 | [ OP2 op2 r1 r2 r3 ⇒ |
---|
[1260] | 191 | if set_member … (eq_identifier …) r1 pliveafter ∨ |
---|
[1223] | 192 | set_member … eq_Register RegisterCarry hliveafter then |
---|
[1185] | 193 | None ? |
---|
| 194 | else |
---|
| 195 | Some ? l |
---|
[1282] | 196 | | CLEAR_CARRY ⇒ None ? |
---|
| 197 | | SET_CARRY ⇒ None ? |
---|
| 198 | | OPACCS opaccs dr1 dr2 sr1 sr2 ⇒ |
---|
[1275] | 199 | if set_member … (eq_identifier …) dr1 pliveafter ∨ |
---|
| 200 | set_member … (eq_identifier …) dr2 pliveafter ∨ |
---|
[1223] | 201 | set_member … eq_Register RegisterCarry hliveafter then |
---|
[1185] | 202 | None ? |
---|
| 203 | else |
---|
| 204 | Some ? l |
---|
[1282] | 205 | | OP1 op1 r1 r2 ⇒ |
---|
[1260] | 206 | if set_member … (eq_identifier …) r1 pliveafter ∨ |
---|
[1223] | 207 | set_member … eq_Register RegisterCarry hliveafter then |
---|
[1185] | 208 | None ? |
---|
| 209 | else |
---|
| 210 | Some ? l |
---|
[1282] | 211 | | POP r ⇒ None ? |
---|
| 212 | | INT r _ ⇒ |
---|
[1223] | 213 | if set_member … (eq_identifier …) r pliveafter ∨ |
---|
| 214 | set_member … eq_Register RegisterCarry hliveafter then |
---|
[1185] | 215 | None ? |
---|
| 216 | else |
---|
| 217 | Some ? l |
---|
[1282] | 218 | | ADDRESS _ _ r1 r2 ⇒ |
---|
[1223] | 219 | if set_member … (eq_identifier …) r1 pliveafter ∨ |
---|
| 220 | set_member … (eq_identifier …) r2 pliveafter ∨ |
---|
| 221 | set_member … eq_Register RegisterCarry hliveafter then |
---|
[1185] | 222 | None ? |
---|
| 223 | else |
---|
| 224 | Some ? l |
---|
[1282] | 225 | | LOAD acc_a dpl dph ⇒ |
---|
[1223] | 226 | if set_member ? (eq_identifier …) acc_a pliveafter ∨ |
---|
| 227 | set_member … eq_Register RegisterCarry hliveafter then |
---|
[1185] | 228 | None ? |
---|
| 229 | else |
---|
| 230 | Some ? l |
---|
[1282] | 231 | | CALL_ID _ nparams _ ⇒ None ? |
---|
| 232 | | COMMENT c ⇒ None ? |
---|
| 233 | | COND r lbl_true ⇒ None ? |
---|
| 234 | | STORE acc_a dpl dph ⇒ None ? |
---|
| 235 | | COST_LABEL clabel ⇒ None ? |
---|
| 236 | | PUSH r ⇒ None ? |
---|
| 237 | | MOVE pair_reg ⇒ |
---|
[1185] | 238 | let r1 ≝ \fst pair_reg in |
---|
| 239 | let r2 ≝ \snd pair_reg in |
---|
| 240 | match r1 with |
---|
| 241 | [ pseudo p1 ⇒ |
---|
[1223] | 242 | if set_member … (eq_identifier …) p1 pliveafter ∨ |
---|
| 243 | set_member … eq_Register RegisterCarry hliveafter then |
---|
[1185] | 244 | None ? |
---|
| 245 | else |
---|
| 246 | Some ? l |
---|
| 247 | | hardware h1 ⇒ |
---|
[1223] | 248 | if set_member … eq_Register h1 hliveafter then |
---|
[1185] | 249 | None ? |
---|
| 250 | else |
---|
[1250] | 251 | Some ? l] |
---|
[1282] | 252 | | extension ext ⇒ |
---|
[1250] | 253 | match ext with |
---|
[1260] | 254 | [ ertl_st_ext_new_frame ⇒ None ? |
---|
| 255 | | ertl_st_ext_del_frame ⇒ None ? |
---|
| 256 | | ertl_st_ext_frame_size r ⇒ |
---|
[1250] | 257 | if set_member ? (eq_identifier RegisterTag) r pliveafter ∨ |
---|
| 258 | set_member ? eq_Register RegisterCarry hliveafter then |
---|
| 259 | None ? |
---|
| 260 | else |
---|
| 261 | Some ? l]] |
---|
[1282] | 262 | | GOTO l ⇒ None ? |
---|
| 263 | | RETURN ⇒ None ? |
---|
[1094] | 264 | ]. |
---|
| 265 | |
---|
[1185] | 266 | definition statement_semantics: ∀globals: list ident. ertl_statement globals → register_lattice → register_lattice ≝ |
---|
| 267 | λglobals. |
---|
[1094] | 268 | λstmt. |
---|
| 269 | λliveafter. |
---|
[1185] | 270 | match eliminable globals liveafter stmt with |
---|
| 271 | [ None ⇒ lattice_join (lattice_diff liveafter (defined globals stmt)) (used globals stmt) |
---|
[1094] | 272 | | Some l ⇒ liveafter |
---|
| 273 | ]. |
---|
| 274 | |
---|
| 275 | definition valuation ≝ label → register_lattice. |
---|
[1124] | 276 | definition rhs ≝ valuation → lattice_property. |
---|
| 277 | definition equations ≝ label → rhs. |
---|
[1094] | 278 | |
---|
[1124] | 279 | definition livebefore ≝ |
---|
[1185] | 280 | λglobals: list ident. |
---|
[1223] | 281 | λint_fun: ertl_internal_function globals. |
---|
[1124] | 282 | λlabel. |
---|
| 283 | λliveafter: valuation. |
---|
[1249] | 284 | match lookup … (joint_if_code … int_fun) label with |
---|
[1124] | 285 | [ None ⇒ ? |
---|
[1185] | 286 | | Some stmt ⇒ statement_semantics globals stmt (liveafter label) |
---|
[1124] | 287 | ]. |
---|
| 288 | cases not_implemented (* XXX *) |
---|
| 289 | qed. |
---|
| 290 | |
---|
| 291 | definition liveafter ≝ |
---|
[1223] | 292 | λglobals: list ident. |
---|
| 293 | λint_fun: ertl_internal_function globals. |
---|
| 294 | λlivebefore: label → ?. |
---|
[1124] | 295 | λlabel. |
---|
| 296 | λliveafter: valuation. |
---|
[1249] | 297 | match lookup … (joint_if_code … int_fun) label with |
---|
[1124] | 298 | [ None ⇒ ? |
---|
[1223] | 299 | | Some stmt ⇒ set_fold ? ? (λsuccessor. λaccu: register_lattice. |
---|
[1124] | 300 | lattice_join (livebefore successor liveafter) accu) |
---|
[1223] | 301 | (statement_successors globals stmt) lattice_bottom |
---|
[1124] | 302 | ]. |
---|
| 303 | cases not_implemented (* XXX *) |
---|
| 304 | qed. |
---|
| 305 | |
---|
[1463] | 306 | record fixpoint: Type[0] ≝ |
---|
| 307 | { |
---|
| 308 | (* XXX: this never fails to compute a fixed point as in any program we will |
---|
| 309 | only ever use a finite number of pseudoregisters, therefore no chain |
---|
| 310 | conditions, etc. are necessary for this to terminate with a correct |
---|
| 311 | solution. *) |
---|
| 312 | fix_lfp :1> equations → valuation; |
---|
| 313 | fix_correct: |
---|
| 314 | ∀globals: list ident. |
---|
| 315 | ∀int_fun. |
---|
| 316 | let f ≝ liveafter globals int_fun (livebefore globals int_fun) in |
---|
| 317 | ∀v: label. |
---|
| 318 | lattice_equal (f v (fix_lfp f)) (fix_lfp f v) |
---|
| 319 | }. |
---|
| 320 | |
---|
| 321 | axiom the_fixpoint: fixpoint. |
---|
| 322 | |
---|
[1185] | 323 | definition analyse ≝ |
---|
| 324 | λglobals. |
---|
[1094] | 325 | λint_fun. |
---|
[1425] | 326 | the_fixpoint (liveafter globals int_fun (livebefore globals int_fun)). |
---|