Changeset 1124


Ignore:
Timestamp:
Aug 29, 2011, 2:42:43 PM (8 years ago)
Author:
mulligan
Message:

finished off liveness analysis by axiomatising properties

Location:
src/ERTL
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL.ma

    r1110 r1124  
    33include "LTL/LTL.ma".
    44
    5 (*
    65definition translate_internal ≝
    76  λf.
     
    1413      ?
    1514      ?.
    16 *)
    1715
    1816definition translate_funct ≝
  • src/ERTL/liveness.ma

    r1107 r1124  
    1 include "utilities/Fix.ma".
    21include "ASM/Util.ma".
    32include "ERTL/ERTL.ma".
     
    3837  λs: ertl_statement.
    3938  match s with
    40   [ ertl_st_return _ ⇒ [ ]
     39  [ ertl_st_return ⇒ [ ]
    4140  | ertl_st_skip l ⇒ [ l ]
    4241  | ertl_st_comment c l ⇒ [ l ]
     
    10099definition lattice_is_maximal: register_lattice → bool ≝ λl. false.
    101100
     101record lattice_property_sig: Type[1] ≝
     102{
     103  lp_type      : Type[0];
     104  lp_property  : Type[0];
     105  lp_bottom    : lp_type;
     106  lp_psingleton: register → lp_type;
     107  lp_hsingleton: Register → lp_type;
     108  lp_join      : lp_type → lp_type → lp_type;
     109  lp_diff      : lp_type → lp_type → lp_type;
     110  lp_equal     : lp_type → lp_type → bool;
     111  lp_is_maximal: lp_type → bool
     112}.
     113
     114definition property ≝
     115  mk_lattice_property_sig
     116    ((list register) × (list Register))
     117    lattice_property
     118    lattice_bottom
     119    lattice_psingleton
     120    lattice_hsingleton
     121    lattice_join
     122    lattice_diff
     123    lattice_equal
     124    lattice_is_maximal.
     125
    102126definition defined: ertl_statement → register_lattice ≝
    103127  λs.
     
    109133  | ertl_st_store _ _ _ _ ⇒ lattice_bottom
    110134  | ertl_st_cond _ _ _ ⇒ lattice_bottom
    111   | ertl_st_return _ ⇒ lattice_bottom
     135  | ertl_st_return ⇒ lattice_bottom
    112136  | ertl_st_clear_carry _ ⇒ lattice_hsingleton RegisterCarry
    113137  | ertl_st_set_carry _ ⇒ lattice_hsingleton RegisterCarry
     
    184208  | ertl_st_new_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
    185209  | ertl_st_del_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
    186   | ertl_st_return _ ⇒ 〈[ ], list_set_union ? eq_Register RegisterCalleeSaved ret_regs〉
     210  | ertl_st_return ⇒ 〈[ ], list_set_union ? eq_Register RegisterCalleeSaved ret_regs〉
    187211  ].
    188212
     
    204228  | ertl_st_call_id _ _ _ ⇒ None ?
    205229  | ertl_st_cond _ _ _ ⇒ None ?
    206   | ertl_st_return _ ⇒ None ?
     230  | ertl_st_return ⇒ None ?
    207231  | ertl_st_get_hdw r _ l ⇒
    208232    if list_set_member register (eq_identifier ?) r pliveafter ∨
     
    292316
    293317definition valuation ≝ label → register_lattice.
     318definition rhs ≝ valuation → lattice_property.
     319definition equations ≝ label → rhs.
     320
     321axiom fix_lfp: equations → valuation.
     322
     323definition livebefore ≝
     324  λint_fun.
     325  λlabel.
     326  λliveafter: valuation.
     327  match lookup ? ? (ertl_if_graph int_fun) label with
     328  [ None      ⇒ ?
     329  | Some stmt ⇒ statement_semantics stmt (liveafter label)
     330  ].
     331  cases not_implemented (* XXX *)
     332qed.
     333
     334definition liveafter ≝
     335  λint_fun.
     336  λlivebefore.
     337  λlabel.
     338  λliveafter: valuation.
     339  match lookup ? ? (ertl_if_graph int_fun) label with
     340  [ None      ⇒ ?
     341  | Some stmt ⇒ list_set_fold ? ? (λsuccessor. λaccu.
     342      lattice_join (livebefore successor liveafter) accu)
     343      lattice_bottom (statement_successors stmt)
     344  ].
     345  cases not_implemented (* XXX *)
     346qed.
    294347
    295348definition analyse: ertl_internal_function → valuation ≝
    296349  λint_fun.
    297   let livebefore ≝ λlabel. λliveafter: valuation.
    298     match lookup ? ? (ertl_if_graph int_fun) label with
    299     [ None      ⇒ ?
    300     | Some stmt ⇒ statement_semantics stmt (liveafter label)
    301     ]
    302   in
    303   let liveafter ≝ λlabel. λliveafter: valuation.
    304     match lookup ? ? (ertl_if_graph int_fun) label with
    305     [ None      ⇒ ?
    306     | Some stmt ⇒ list_set_fold ? ? (λsuccessor. λaccu.
    307         lattice_join (livebefore successor liveafter) accu)
    308         lattice_bottom (statement_successors stmt)
    309     ]
    310   in ?.
     350    fix_lfp (liveafter int_fun (livebefore int_fun)).
Note: See TracChangeset for help on using the changeset viewer.