Changeset 1463 for src/ERTL


Ignore:
Timestamp:
Oct 25, 2011, 5:33:53 PM (8 years ago)
Author:
mulligan
Message:

added erasure for lin

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/liveness.ma

    r1425 r1463  
    152152    | PUSH r ⇒ lattice_psingleton r
    153153    | 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 *)
     167qed.r relevant *)
    155168      let r2 ≝ \snd pair_reg in
    156169      match r2 with
     
    264277definition equations ≝ label → rhs.
    265278
    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 
    276279definition livebefore ≝
    277280  λglobals: list ident.
     
    301304qed.
    302305
     306record 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
     321axiom the_fixpoint: fixpoint.
     322
    303323definition analyse ≝
    304324  λglobals.
Note: See TracChangeset for help on using the changeset viewer.