Changeset 1463 for src/ERTL/liveness.ma
 Timestamp:
 Oct 25, 2011, 5:33:53 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTL/liveness.ma
r1425 r1463 152 152  PUSH r ⇒ lattice_psingleton r 153 153  MOVE pair_reg ⇒ 154 (* only second reg in pair relevant *) 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 *) 155 168 let r2 ≝ \snd pair_reg in 156 169 match r2 with … … 264 277 definition equations ≝ label → rhs. 265 278 266 record fixpoint: Type[0] ≝267 {268 fix_lfp :1> equations → valuation;269 fix_correct: ∀f: equations.270 ∀v: label.271 lattice_equal (f v (fix_lfp f)) (fix_lfp f v)272 }.273 274 axiom the_fixpoint: fixpoint.275 276 279 definition livebefore ≝ 277 280 λglobals: list ident. … … 301 304 qed. 302 305 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 303 323 definition analyse ≝ 304 324 λglobals.
Note: See TracChangeset
for help on using the changeset viewer.