Changeset 2286 for src/ERTL/liveness.ma


Ignore:
Timestamp:
Aug 2, 2012, 3:18:11 PM (9 years ago)
Author:
tranquil
Message:

Big update!

  • merge of all _paolo variants
  • reorganised some depends (in particular, Register and thus back-end laguages no longer have fake ASM dependency)
  • split I8051.ma spawning new BackEndOps?.ma

compiler.ma broken at the moment, but not by these changes as far as I can tell

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/liveness.ma

    r1995 r2286  
     1
    12include "ASM/Util.ma".
    23include "ERTL/ERTL.ma".
    34include "utilities/adt/set_adt.ma".
    4 
    5 definition statement_successors ≝
    6   λglobals: list ident.
    7   λs: ertl_statement globals.
     5include "utilities/fixpoints.ma".
     6
     7definition register_lattice : property_lattice ≝
     8mk_property_lattice
     9 ((set register) × (set Register))
     10 〈set_empty …, set_empty …〉
     11 (λleft.
     12  λright.
     13  set_equal … (eq_identifier ?) (\fst left) (\fst right) ∧
     14  set_equal … eq_Register (\snd left) (\snd right))
     15 (λleft.
     16  λright.
     17  set_subset … (eq_identifier ?) (\fst left) (\fst right) ∧
     18  set_subset … eq_Register (\snd left) (\snd right))
     19 (λ_.false).
     20
     21definition rl_bottom ≝ l_bottom register_lattice.
     22definition rl_psingleton: register → register_lattice ≝
     23  λr.
     24    〈set_singleton … r, set_empty …〉.
     25definition rl_hsingleton: Register → register_lattice ≝
     26  λr.
     27    〈set_empty …, set_singleton … r〉.
     28
     29definition rl_join: register_lattice → register_lattice → register_lattice ≝
     30  λleft.
     31  λright.
     32  let 〈lp, lh〉 ≝ left in
     33  let 〈rp, rh〉 ≝ right in
     34    〈set_union … lp rp, set_union … lh rh〉.
     35
     36definition rl_diff: register_lattice → register_lattice → register_lattice ≝
     37  λleft.
     38  λright.
     39  let 〈lp, lh〉 ≝ left in
     40  let 〈rp, rh〉 ≝ right in
     41    〈set_diff … lp rp, set_diff … lh rh〉.
     42
     43definition defined ≝
     44  λglobals: list ident.
     45  λs: joint_statement ERTL globals.
    846  match s with
    947  [ sequential seq l ⇒
    1048    match seq with
    11     [ COND acc_a_reg lbl_true ⇒
    12         set_insert … lbl_true (set_singleton … l)
    13     | _ ⇒ set_singleton … l ]
    14   | GOTO l ⇒ set_singleton … l
    15   | RETURN ⇒ set_empty ?
    16   ].
    17 
    18 definition register_lattice ≝ (set register) × (set Register).
    19 definition lattice_property ≝ register_lattice.
    20 definition lattice_bottom: register_lattice ≝ 〈set_empty register, set_empty Register〉.
    21 definition lattice_psingleton: register → register_lattice ≝
    22   λr.
    23     〈set_singleton … r, set_empty …〉.
    24 definition lattice_hsingleton: Register → register_lattice ≝
    25   λr.
    26     〈set_empty …, set_singleton … r〉.
    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
    33     〈set_union … lp rp, set_union … lh rh〉.
    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
    40     〈set_diff … lp rp, set_diff … lh rh〉.
    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
    47     andb (set_equal … (eq_identifier …) lp rp) (set_equal … eq_Register lh rh).
    48 
    49 definition lattice_is_maximal: register_lattice → bool ≝ λl. false.
    50 
    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
    66     ((set register) × (set Register))
    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 
    76 definition defined ≝
    77   λglobals: list ident.
    78   λs: ertl_statement globals.
     49    [ step_seq s ⇒
     50      match s with
     51      [ OP2 op2 r1 r2 _ ⇒
     52        match op2 with
     53        [ Add ⇒ rl_join (rl_hsingleton RegisterCarry) (rl_psingleton r1)
     54        | Addc ⇒ rl_join (rl_hsingleton RegisterCarry) (rl_psingleton r1)
     55        | Sub ⇒ rl_join (rl_hsingleton RegisterCarry)  (rl_psingleton r1)
     56        | _ ⇒ rl_psingleton r1
     57        ]
     58      | CLEAR_CARRY ⇒ rl_hsingleton RegisterCarry
     59      | SET_CARRY ⇒ rl_hsingleton RegisterCarry
     60      | OPACCS opaccs dr1 dr2 sr1 sr2 ⇒
     61        rl_join (rl_join (rl_psingleton dr1)
     62                                    (rl_psingleton dr2))
     63                      (rl_hsingleton RegisterCarry)
     64      | OP1 op1 r1 r2 ⇒ rl_join (rl_psingleton r1) (rl_psingleton r2)
     65      | POP r ⇒ rl_psingleton r
     66      | ADDRESS _ _ r1 r2 ⇒ rl_join (rl_psingleton r1) (rl_psingleton r2)
     67      | LOAD r _ _ ⇒ rl_psingleton r
     68      | COMMENT c ⇒ rl_bottom
     69      | STORE acc_a dpl dph ⇒ rl_bottom
     70      | COST_LABEL clabel ⇒ rl_bottom
     71      | PUSH r ⇒ rl_bottom
     72      | MOVE pair_reg ⇒
     73        (* first register relevant only *)
     74        match \fst pair_reg with
     75        [ PSD p ⇒ rl_psingleton p
     76        | HDW h ⇒ rl_hsingleton h
     77        ]
     78      | extension_seq ext ⇒
     79        match ext with
     80        [ ertl_new_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
     81        | ertl_del_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
     82        | ertl_frame_size r ⇒ rl_psingleton r
     83        ]
     84      (* Potentially destroys all caller-save hardware registers. *)
     85      | CALL_ID id _ _ ⇒ 〈set_empty …, set_from_list … RegisterCallerSaved〉
     86      | extension_call abs ⇒ match abs in void with [ ]
     87      ]
     88    | COND r lbl_true ⇒ rl_bottom
     89    ]
     90  | final _ ⇒ rl_bottom
     91  ].
     92
     93definition ret_regs ≝ set_from_list … RegisterRets.
     94
     95definition rl_arg : psd_argument → register_lattice ≝
     96  λarg.match arg with
     97  [ Imm _ ⇒ rl_bottom
     98  | Reg r ⇒ rl_psingleton r
     99  ].
     100
     101definition used ≝
     102  λglobals: list ident.
     103  λs: joint_statement ERTL globals.
    79104  match s with
    80105  [ sequential seq l ⇒
    81106    match seq with
    82     [ OP2 op2 r1 r2 _ ⇒
    83       match op2 with
    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
     107    [ step_seq s ⇒
     108      match s with
     109      [ OP2 op2 acc_a r1 r2 ⇒
     110        rl_join (rl_join (rl_arg r1) (rl_arg r2))
     111          (match op2 with
     112            [ Addc ⇒ rl_hsingleton RegisterCarry
     113            | Sub ⇒ rl_hsingleton RegisterCarry
     114            | _ ⇒ rl_bottom
     115            ])
     116      (* acc_a and acc_b *)
     117      | OPACCS opaccs dr1 dr2 sr1 sr2 ⇒
     118        rl_join (rl_arg sr1) (rl_arg sr2)
     119      | OP1 op1 r1 r2 ⇒ rl_psingleton r2
     120      | LOAD acc_a dpl dph ⇒ rl_join (rl_arg dpl) (rl_arg dph)
     121      | STORE acc_a dpl dph ⇒
     122        rl_join (rl_join (rl_arg acc_a) (rl_arg dpl)) (rl_arg dph)
     123      | PUSH r ⇒ rl_arg r
     124      | MOVE pair_reg ⇒
     125        let r2 ≝ \snd pair_reg in
     126        match r2 with
     127        [ Reg p ⇒
     128          match p with
     129          [ PSD r ⇒ rl_psingleton r
     130          | HDW r ⇒ rl_hsingleton r
     131          ]
     132        | Imm _ ⇒ rl_bottom
     133        ]
     134      | extension_seq ext ⇒
     135        match ext with
     136        [ ertl_new_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
     137        | ertl_del_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
     138        | ertl_frame_size r ⇒ rl_bottom
     139        ]
     140      (* Reads the hardware registers that are used to pass parameters. *)
     141      | CALL_ID _ nparams _ ⇒ 〈set_empty …, set_from_list … (prefix ? nparams RegisterParams)〉
     142      | extension_call abs ⇒ match abs in void with [ ]
     143      | _ ⇒ rl_bottom
    88144      ]
    89     | CLEAR_CARRY ⇒ lattice_hsingleton RegisterCarry
    90     | SET_CARRY ⇒ lattice_hsingleton RegisterCarry
    91     | OPACCS opaccs dr1 dr2 sr1 sr2 ⇒
    92        lattice_join (lattice_psingleton dr1) (lattice_psingleton dr2)
    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
    98     (* Potentially destroys all caller-save hardware registers. *)
    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 ⇒
    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       ]
    112     | extension ext ⇒
    113       match ext with
    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]]
    117   | RETURN ⇒ lattice_bottom
    118   | GOTO l ⇒ lattice_bottom
    119   ].
    120 
    121 definition ret_regs ≝ set_from_list … RegisterRets.
    122 
    123 definition used ≝
    124   λglobals: list ident.
    125   λs: ertl_statement globals.
     145    | COND r lbl_true ⇒ rl_psingleton r
     146    ]
     147  | final fin ⇒
     148    match fin with
     149    [ RETURN ⇒ 〈set_empty …, set_union … (set_from_list … RegisterCalleeSaved) ret_regs〉
     150    | GOTO l ⇒ rl_bottom
     151    | tailcall abs ⇒ match abs in void with [ ]
     152    ]
     153  ].
     154
     155definition eliminable ≝
     156  λglobals: list ident.
     157  λl: register_lattice.
     158  λs: joint_statement ERTL globals.
     159  let pliveafter ≝ \fst l in
     160  let hliveafter ≝ \snd l in
    126161  match s with
    127162  [ sequential seq l ⇒
    128163    match seq with
    129     [ OP2 op2 acc_a r1 r2 ⇒
    130       match op2 with
    131       [ Addc ⇒
    132         lattice_join (lattice_join (lattice_psingleton r1) (lattice_psingleton r2)) (lattice_hsingleton RegisterCarry)
    133       | _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
     164    [ step_seq s ⇒
     165      match s with
     166      [ OP2 op2 r1 r2 r3 ⇒
     167        if match op2 with
     168          [ Add ⇒ set_member … eq_Register RegisterCarry hliveafter
     169          | Addc ⇒ set_member … eq_Register RegisterCarry hliveafter
     170          | Sub ⇒ set_member … eq_Register RegisterCarry hliveafter
     171          | _ ⇒ false
     172          ] ∨ set_member … (eq_identifier …) r1 pliveafter
     173        then
     174          None ?
     175        else
     176          Some ? l
     177      | OPACCS opaccs dr1 dr2 sr1 sr2 ⇒
     178        if set_member … (eq_identifier …) dr1 pliveafter ∨
     179           set_member … (eq_identifier …) dr2 pliveafter ∨
     180           set_member … eq_Register RegisterCarry hliveafter then
     181          None ?
     182        else
     183          Some ? l
     184      | OP1 op1 r1 r2 ⇒
     185        if set_member … (eq_identifier …) r1 pliveafter then
     186          None ?
     187        else
     188          Some ? l
     189      | ADDRESS _ _ r1 r2 ⇒
     190        if set_member … (eq_identifier …) r1 pliveafter ∨
     191           set_member … (eq_identifier …) r2 pliveafter then
     192          None ?
     193        else
     194          Some ? l
     195      | LOAD acc_a dpl dph ⇒
     196        if set_member ? (eq_identifier …) acc_a pliveafter then
     197          None ?
     198        else
     199          Some ? l
     200      | MOVE pair_reg ⇒
     201        if match \fst pair_reg with
     202          [ PSD p1 ⇒
     203            set_member … (eq_identifier …) p1 pliveafter
     204          | HDW h1 ⇒
     205            set_member … eq_Register h1 hliveafter
     206          ] then
     207            None ?
     208          else
     209            Some ? l
     210      | extension_seq ext ⇒
     211        match ext with
     212        [ ertl_new_frame ⇒ None ?
     213        | ertl_del_frame ⇒ None ?
     214        | ertl_frame_size r ⇒
     215          if set_member ? (eq_identifier RegisterTag) r pliveafter then
     216            None ?
     217          else
     218            Some ? l
     219        ]
     220      | _ ⇒ None ?
    134221      ]
    135     | CLEAR_CARRY ⇒ lattice_bottom
    136     | SET_CARRY ⇒ lattice_bottom
    137     (* acc_a and acc_b *)
    138     | OPACCS opaccs dr1 dr2 sr1 sr2 ⇒
    139        lattice_join (lattice_psingleton sr1) (lattice_psingleton sr2)
    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)
    145     (* Reads the hardware registers that are used to pass parameters. *)
    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 ⇒
    150       lattice_join (lattice_join (lattice_psingleton acc_a) (lattice_psingleton dpl)) (lattice_psingleton dph)
    151     | COST_LABEL clabel ⇒ lattice_bottom
    152     | PUSH r ⇒ lattice_psingleton r
    153     | MOVE pair_reg ⇒
    154       let r2 ≝ \snd pair_reg in
    155       match r2 with
    156       [ pseudo p ⇒ lattice_psingleton p
    157       | hardware h ⇒ lattice_hsingleton h
    158       ]
    159   | extension ext ⇒
    160     match ext with
    161     [ ertl_st_ext_new_frame ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
    162     | ertl_st_ext_del_frame ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
    163     | ertl_st_ext_frame_size r ⇒ lattice_bottom]]
    164   | RETURN ⇒ 〈set_empty …, set_union … (set_from_list … RegisterCalleeSaved) ret_regs〉
    165   | GOTO l ⇒ lattice_bottom
    166   ].
    167 
    168 definition eliminable ≝
    169   λglobals: list ident.
    170   λl: register_lattice.
    171   λs: ertl_statement globals.
    172   let 〈pliveafter, hliveafter〉 ≝ l in
    173   match s with
    174   [ sequential seq l ⇒
    175     match seq with
    176     [ OP2 op2 r1 r2 r3 ⇒
    177       if set_member … (eq_identifier …) r1 pliveafter ∨
    178          set_member … eq_Register RegisterCarry hliveafter then
    179         None ?
    180       else
    181         Some ? l
    182     | CLEAR_CARRY ⇒ None ?
    183     | SET_CARRY ⇒ None ?
    184     | OPACCS opaccs dr1 dr2 sr1 sr2 ⇒
    185       if set_member … (eq_identifier …) dr1 pliveafter ∨
    186          set_member … (eq_identifier …) dr2 pliveafter ∨
    187          set_member … eq_Register RegisterCarry hliveafter then
    188         None ?
    189       else
    190         Some ? l
    191     | OP1 op1 r1 r2 ⇒
    192       if set_member … (eq_identifier …) r1 pliveafter ∨
    193          set_member … eq_Register RegisterCarry hliveafter then
    194         None ?
    195       else
    196         Some ? l
    197     | POP r ⇒ None ?
    198     | INT r _ ⇒
    199       if set_member … (eq_identifier …) r pliveafter ∨
    200          set_member … eq_Register RegisterCarry hliveafter then
    201         None ?
    202       else
    203         Some ? l
    204     | ADDRESS _ _ r1 r2 ⇒
    205       if set_member … (eq_identifier …) r1 pliveafter ∨
    206          set_member … (eq_identifier …) r2 pliveafter ∨
    207          set_member … eq_Register RegisterCarry hliveafter then
    208         None ?
    209       else
    210         Some ? l
    211     | LOAD acc_a dpl dph ⇒
    212       if set_member ? (eq_identifier …) acc_a pliveafter ∨
    213          set_member … eq_Register RegisterCarry hliveafter then
    214         None ?
    215       else
    216         Some ? l
    217     | CALL_ID _ nparams _ ⇒ None ?
    218     | COMMENT c ⇒ None ?
    219     | COND r lbl_true ⇒ None ?
    220     | STORE acc_a dpl dph ⇒ None ?
    221     | COST_LABEL clabel ⇒ None ?
    222     | PUSH r ⇒ None ?
    223     | MOVE pair_reg ⇒
    224       let r1 ≝ \fst pair_reg in
    225       let r2 ≝ \snd pair_reg in
    226       match r1 with
    227       [ pseudo p1 ⇒
    228         if set_member … (eq_identifier …) p1 pliveafter ∨
    229            set_member … eq_Register RegisterCarry hliveafter then
    230           None ?
    231         else
    232           Some ? l
    233       | hardware h1 ⇒
    234         if set_member … eq_Register h1 hliveafter then
    235           None ?
    236         else
    237           Some ? l]
    238     | extension ext ⇒
    239       match ext with
    240       [ ertl_st_ext_new_frame ⇒ None ?
    241       | ertl_st_ext_del_frame ⇒ None ?
    242       | ertl_st_ext_frame_size r ⇒
    243         if set_member ? (eq_identifier RegisterTag) r pliveafter ∨
    244            set_member ? eq_Register RegisterCarry hliveafter then
    245           None ?
    246         else
    247           Some ? l]]
    248   | GOTO l ⇒ None ?
    249   | RETURN ⇒ None ?
    250   ].
    251 
    252 definition statement_semantics: ∀globals: list ident. ertl_statement globals → register_lattice → register_lattice ≝
     222    | COND _ _ ⇒ None ?
     223    ]
     224  | _ ⇒ None ?
     225  ].
     226
     227definition statement_semantics: ∀globals: list ident.
     228  joint_statement ERTL globals → register_lattice → register_lattice ≝
    253229  λglobals.
    254230  λstmt.
    255231  λliveafter.
    256232  match eliminable globals liveafter stmt with
    257   [ None ⇒ lattice_join (lattice_diff liveafter (defined globals stmt)) (used globals stmt)
     233  [ None ⇒ rl_join (rl_diff liveafter (defined globals stmt)) (used globals stmt)
    258234  | Some l ⇒ liveafter
    259235  ].
    260236
    261 definition valuation ≝ label → register_lattice.
    262 definition rhs ≝ valuation → lattice_property.
    263 definition equations ≝ label → rhs.
    264 
    265237definition livebefore ≝
    266238  λglobals: list ident.
    267   λint_fun: ertl_internal_function globals.
     239  λint_fun: joint_internal_function ERTL globals.
    268240  λlabel.
    269   λliveafter: valuation.
    270   match lookup (joint_if_code … int_fun) label with
    271   [ None      ⇒ ?
     241  λliveafter: valuation register_lattice.
     242  match lookup ?? (joint_if_code … int_fun) label with
     243  [ None      ⇒ rl_bottom
    272244  | Some stmt ⇒ statement_semantics globals stmt (liveafter label)
    273245  ].
    274   cases not_implemented (* XXX *)
    275 qed.
    276246
    277247definition liveafter ≝
    278   λglobals: list ident.
    279   λint_fun: ertl_internal_function globals.
     248   λglobals: list ident.
     249  λint_fun: joint_internal_function ERTL globals.
    280250  λlabel.
    281   λliveafter: valuation.
    282   match lookup … (joint_if_code … int_fun) label with
    283   [ None      ⇒ ?
    284   | Some stmt ⇒ set_fold ? ? (λsuccessor. λaccu: register_lattice.
    285       lattice_join (livebefore globals int_fun successor liveafter) accu)
    286       (statement_successors globals stmt) lattice_bottom
    287   ].
    288   cases not_implemented (* XXX *)
    289 qed.
    290 
    291 record fixpoint: Type[0] ≝
    292 {
    293   (* XXX: this never fails to compute a fixed point as in any program we will
    294           only ever use a finite number of pseudoregisters, therefore no chain
    295           conditions, etc. are necessary for this to terminate with a correct
    296           solution. *)
    297   fix_lfp    :1> equations → valuation;
    298   fix_correct:
    299     ∀globals: list ident.
    300 (*    ∀int_fun.*)
    301     ∀f. (* CSC: was let f ≝ liveafter globals int_fun in *)
    302       ∀v: label.
    303         lattice_equal (f v (fix_lfp f)) (fix_lfp f v) (*CSC: TOO STRONG: WE ONLY NEED CORRECTNESS NOT COMPLETENESS *)
    304 }.
    305 
    306 axiom the_fixpoint: fixpoint.
    307 
    308 definition analyse ≝
     251  λliveafter: valuation register_lattice.
     252 match lookup ?? (joint_if_code … int_fun) label with
     253  [ None      ⇒ rl_bottom
     254  | Some stmt ⇒
     255    \fold[rl_join,rl_bottom]_{successor ∈ stmt_labels … stmt}
     256      (livebefore globals int_fun successor liveafter)
     257  ].
     258
     259definition analyse_liveness ≝
    309260  λglobals.
    310261  λint_fun.
    311     the_fixpoint (liveafter globals int_fun).
     262    the_fixpoint ? (liveafter globals int_fun).
     263
     264definition vertex ≝ register + Register.
     265
     266definition plives : register → register_lattice → bool ≝
     267  λvertex.λprop.set_member ? (eq_identifier RegisterTag) vertex (\fst prop).
     268definition hlives : Register → register_lattice → bool ≝
     269  λvertex.λprop.set_member ? eq_Register vertex (\snd prop).
     270
     271definition lives : vertex → register_lattice → bool ≝
     272  λvertex.
     273  match vertex with
     274  [ inl v ⇒ plives v
     275  | inr v ⇒ hlives v
     276  ].
Note: See TracChangeset for help on using the changeset viewer.