Changeset 1185


Ignore:
Timestamp:
Sep 5, 2011, 5:02:53 PM (8 years ago)
Author:
mulligan
Message:

ported liveness analysis to new code

Location:
src/ERTL
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/build.ma

    r1144 r1185  
    1616        let exceptions ≝
    1717          match stmt with
    18           [ ertl_st_move _ sr _    ⇒ lattice_psingleton sr
    19           | ertl_st_set_hdw _ sr _ ⇒ lattice_psingleton sr
    20           | ertl_st_get_hdw _ sr _ ⇒ lattice_hsingleton sr
    21           | _                      ⇒ ?
     18          [ joint_st_sequential seq l ⇒
     19            match seq with
     20            [ joint_instr_move pair_reg ⇒
     21              let reg_r ≝ \snd pair_reg in
     22              match reg_r with
     23              [ hardware hw ⇒ lattice_hsingleton hw
     24              | pseudo   ps ⇒ lattice_psingleton ps
     25              ]
     26            | _                         ⇒ ?
     27            ]
     28          | _ ⇒ ?
    2229          ]
    2330        in
     
    2532        let graph ≝
    2633          match stmt with
    27           [ ertl_st_move r1 r2 _    ⇒ ig_mkppp graph r1 r2
    28           | ertl_st_get_hdw r hwr _ ⇒ ig_mkpph graph r hwr
    29           | ertl_st_set_hdw hwr r _ ⇒ ig_mkpph graph r hwr
    30           | _                       ⇒ graph
     34          [ joint_st_sequential seq l ⇒
     35            match seq with
     36            [ joint_instr_move pair_reg ⇒
     37              let reg_l ≝ \fst pair_reg in
     38              let reg_r ≝ \snd pair_reg in
     39              match reg_l with
     40              [ pseudo ps1 ⇒
     41                match reg_r with
     42                [ pseudo ps2  ⇒ ig_mkppp graph ps1 ps2
     43                | hardware hw ⇒ ig_mkpph graph ps1 hw
     44                ]
     45              | hardware hw1 ⇒
     46                match reg_r with
     47                [ pseudo ps    ⇒ ig_mkpph graph ps hw1
     48                | hardware hw2 ⇒ graph
     49                ]
     50            | _ ⇒ graph
     51            ]
     52          | _ ⇒ graph
    3153          ]
    3254        in graph
  • src/ERTL/liveness.ma

    r1144 r1185  
    3535
    3636definition statement_successors ≝
    37   λs: ertl_statement.
     37  λglobals: list ident.
     38  λs: ertl_statement globals.
    3839  match s with
    39   [ ertl_st_return ⇒ [ ]
    40   | ertl_st_skip l ⇒ [ l ]
    41   | ertl_st_comment c l ⇒ [ l ]
    42   | ertl_st_cost c l ⇒ [ l ]
    43   | ertl_st_set_hdw _ _ l ⇒ [ l ]
    44   | ertl_st_get_hdw _ _ l ⇒ [ l ]
    45   | ertl_st_hdw_to_hdw _ _ l ⇒ [ l ]
    46   | ertl_st_new_frame l ⇒ [ l ]
    47   | ertl_st_del_frame l ⇒ [ l ]
    48   | ertl_st_frame_size _ l ⇒ [ l ]
    49   | ertl_st_push _ l ⇒ [ l ]
    50   | ertl_st_pop _ l ⇒ [ l ]
    51   | ertl_st_addr _ _ _ l ⇒ [ l ]
    52   | ertl_st_int _ _ l ⇒ [ l ]
    53   | ertl_st_move _ _ l ⇒ [ l ]
    54   | ertl_st_opaccs _ _ _ _ _ l ⇒ [ l ]
    55   | ertl_st_op1 _ _ _ l ⇒ [ l ]
    56   | ertl_st_op2 _ _ _ _ l ⇒ [ l ]
    57   | ertl_st_clear_carry l ⇒ [ l ]
    58   | ertl_st_set_carry l ⇒ [ l ]
    59   | ertl_st_load _ _ _ l ⇒ [ l ]
    60   | ertl_st_store _ _ _ l ⇒ [ l ]
    61   | ertl_st_call_id _ _ l ⇒ [ l ]
    62   | ertl_st_cond _ l1 l2 ⇒
    63       list_set_add ? (eq_identifier ?) l1 [ l2 ]
     40  [ joint_st_sequential seq l ⇒
     41    match seq with
     42    [ joint_instr_cond acc_a_reg lbl_true ⇒
     43        list_set_add ? (eq_identifier ?) lbl_true [ l ]
     44    | _ ⇒ [ l ]
     45    ]
     46  | joint_st_extension ext ⇒
     47    match ext with
     48    [ ertl_st_ext_new_frame l ⇒ [ l ]
     49    | ertl_st_ext_del_frame l ⇒ [ l ]
     50    | ertl_st_ext_frame_size r l ⇒ [ l ]
     51    ]
     52  | joint_st_goto l ⇒ [ l ]
     53  | joint_st_return ⇒ [ ]
    6454  ].
    6555
     
    122112    lattice_is_maximal.
    123113
    124 definition defined: ertl_statement → register_lattice ≝
    125   λs.
     114definition defined ≝
     115  λglobals: list ident.
     116  λs: ertl_statement globals.
    126117  match s with
    127   [ ertl_st_skip _ ⇒ lattice_bottom
    128   | ertl_st_comment _ _ ⇒ lattice_bottom
    129   | ertl_st_cost _ _ ⇒ lattice_bottom
    130   | ertl_st_push _ _⇒ lattice_bottom
    131   | ertl_st_store _ _ _ _ ⇒ lattice_bottom
    132   | ertl_st_cond _ _ _ ⇒ lattice_bottom
    133   | ertl_st_return ⇒ lattice_bottom
    134   | ertl_st_clear_carry _ ⇒ lattice_hsingleton RegisterCarry
    135   | ertl_st_set_carry _ ⇒ lattice_hsingleton RegisterCarry
    136   | ertl_st_op2 op2 r _ _ _ ⇒
    137     match op2 with
    138     [ Add ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r)
    139     | Addc ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r)
    140     | Sub ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r)
    141     | _ ⇒ lattice_psingleton r
    142     ]
    143   | ertl_st_op1 op1 r _ _ ⇒ lattice_psingleton r
    144   | ertl_st_get_hdw r _ _ ⇒ lattice_psingleton r
    145   | ertl_st_frame_size r _ ⇒ lattice_psingleton r
    146   | ertl_st_pop r _ ⇒ lattice_psingleton r
    147   | ertl_st_int r _ _ ⇒ lattice_psingleton r
    148   | ertl_st_addr r1 r2 _ _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    149   | ertl_st_move r _ _ ⇒ lattice_psingleton r
    150   (* XXX: change from o'caml *)
    151   | ertl_st_opaccs _ r1 r2 _ _ _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    152   | ertl_st_load r _ _ _ ⇒ lattice_psingleton r
    153   | ertl_st_set_hdw r _ _ ⇒ lattice_hsingleton r
    154   | ertl_st_hdw_to_hdw r _ _ ⇒ lattice_hsingleton r
    155   (* Potentially destroys all caller-save hardware registers. *)
    156   | ertl_st_call_id _ _ _ ⇒ 〈[ ], RegisterCallerSaved〉
    157   | ertl_st_new_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
    158   | ertl_st_del_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
     118  [ joint_st_sequential seq l ⇒
     119    match seq with
     120    [ joint_instr_op2 op2 r _ ⇒
     121      match op2 with
     122      [ Add ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r)
     123      | Addc ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r)
     124      | Sub ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r)
     125      | _ ⇒ lattice_psingleton r
     126      ]
     127    | joint_instr_clear_carry ⇒ lattice_hsingleton RegisterCarry
     128    | joint_instr_set_carry ⇒ lattice_hsingleton RegisterCarry
     129    | joint_instr_opaccs opaccs r1 r2 ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
     130    | joint_instr_op1 op1 r ⇒ lattice_psingleton r
     131    | joint_instr_pop r ⇒ lattice_psingleton r
     132    | joint_instr_int r _ ⇒ lattice_psingleton r
     133    | joint_instr_address _ _ r1 r2 ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
     134    | joint_instr_load r _ _ ⇒ lattice_psingleton r
     135    (* Potentially destroys all caller-save hardware registers. *)
     136    | joint_instr_call_id _ _ ⇒ 〈[ ], RegisterCallerSaved〉
     137    | joint_instr_comment c ⇒ lattice_bottom
     138    | joint_instr_cond r lbl_true ⇒ lattice_bottom
     139    | joint_instr_store acc_a dpl dph ⇒ lattice_bottom
     140    | joint_instr_cost_label clabel ⇒ lattice_bottom
     141    | joint_instr_push r ⇒ lattice_bottom
     142    | joint_instr_move pair_reg ⇒
     143      (* first register relevant only *)
     144      let r1 ≝ \fst pair_reg in
     145      match r1 with
     146      [ pseudo p ⇒ lattice_psingleton p
     147      | hardware h ⇒ lattice_hsingleton h
     148      ]
     149    ]
     150  | joint_st_return ⇒ lattice_bottom
     151  | joint_st_extension ext ⇒
     152    match ext with
     153    [ ertl_st_ext_new_frame l ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
     154    | ertl_st_ext_del_frame l ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
     155    | ertl_st_ext_frame_size r l ⇒ lattice_psingleton r
     156    ]
     157  | joint_st_goto l ⇒ lattice_bottom
    159158  ].
    160159
     
    169168definition ret_regs ≝ list_set_of_list RegisterRets.
    170169
    171 definition used: ertl_statement → register_lattice ≝
    172   λstmt.
    173   match stmt with
    174   [ ertl_st_skip _ ⇒ lattice_bottom
    175   | ertl_st_cost _ _ ⇒ lattice_bottom
    176   | ertl_st_comment _ _ ⇒ lattice_bottom
    177   | ertl_st_frame_size _ _ ⇒ lattice_bottom
    178   | ertl_st_pop _ _ ⇒ lattice_bottom
    179   | ertl_st_addr _ _ _ _ ⇒ lattice_bottom
    180   | ertl_st_int _ _ _ ⇒ lattice_bottom
    181   | ertl_st_clear_carry _ ⇒ lattice_bottom
    182   | ertl_st_set_carry _ ⇒ lattice_bottom
     170definition used ≝
     171  λglobals: list ident.
     172  λs: ertl_statement globals.
     173  match s with
     174  [ joint_st_sequential seq l ⇒
     175    match seq with
     176    [ joint_instr_op2 op2 acc_a r ⇒
     177      match op2 with
     178      [ Addc ⇒
     179        lattice_join (lattice_join (lattice_psingleton acc_a) (lattice_psingleton r)) (lattice_hsingleton RegisterCarry)
     180      | _ ⇒ lattice_join (lattice_psingleton acc_a) (lattice_psingleton r)
     181      ]
     182    | joint_instr_clear_carry ⇒ lattice_bottom
     183    | joint_instr_set_carry ⇒ lattice_bottom
     184    (* acc_a and acc_b *)
     185    | joint_instr_opaccs opaccs r1 r2 ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
     186    | joint_instr_op1 op1 r ⇒ lattice_psingleton r
     187    | joint_instr_pop r ⇒ lattice_bottom
     188    | joint_instr_int r _ ⇒ lattice_bottom
     189    | joint_instr_address _ _ r1 r2 ⇒ lattice_bottom
     190    | joint_instr_load acc_a dpl dph ⇒ lattice_join (lattice_psingleton dpl) (lattice_psingleton dph)
    183191    (* Reads the hardware registers that are used to pass parameters. *)
    184   | ertl_st_call_id _ nparams _ ⇒
    185     〈[ ], list_set_of_list (prefix ? nparams RegisterParameters)〉
    186   | ertl_st_get_hdw _ r _ ⇒ lattice_hsingleton r
    187   | ertl_st_hdw_to_hdw _ r _ ⇒ lattice_hsingleton r
    188   | ertl_st_set_hdw _ r _ ⇒ lattice_psingleton r
    189   | ertl_st_push r _ ⇒ lattice_psingleton r
    190   | ertl_st_move _ r _ ⇒ lattice_psingleton r
    191   | ertl_st_op1 _ _ r _ ⇒ lattice_psingleton r
    192   | ertl_st_cond r _ _ ⇒ lattice_psingleton r
    193   | ertl_st_op2 op2 _ r1 r2 _ ⇒
    194     match op2 with
    195     [ Addc ⇒
    196       lattice_join (lattice_join (lattice_psingleton r1) (lattice_psingleton r2)) (lattice_hsingleton RegisterCarry)
    197     | _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    198     ]
    199   | ertl_st_opaccs _ d1 d2 s1 s2 _ ⇒ lattice_join (lattice_psingleton s1) (lattice_psingleton s2)
    200   | ertl_st_load _ r1 r2 _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    201   | ertl_st_store r1 r2 r3 _ ⇒
    202     lattice_join (lattice_join (lattice_psingleton r1) (lattice_psingleton r2)) (lattice_psingleton r3)
    203   | ertl_st_new_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
    204   | ertl_st_del_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
    205   | ertl_st_return ⇒ 〈[ ], list_set_union ? eq_Register RegisterCalleeSaved ret_regs〉
    206   ].
    207 
    208 definition eliminable: register_lattice → ertl_statement → option label ≝
    209   λl.
    210   λstmt.
     192    | joint_instr_call_id _ nparams ⇒ 〈[ ], list_set_of_list (prefix ? nparams RegisterParams)〉
     193    | joint_instr_comment c ⇒ lattice_bottom
     194    | joint_instr_cond r lbl_true ⇒ lattice_psingleton r
     195    | joint_instr_store acc_a dpl dph ⇒
     196      lattice_join (lattice_join (lattice_psingleton acc_a) (lattice_psingleton dpl)) (lattice_psingleton dph)
     197    | joint_instr_cost_label clabel ⇒ lattice_bottom
     198    | joint_instr_push r ⇒ lattice_psingleton r
     199    | joint_instr_move pair_reg ⇒
     200      (* only second reg in pair relevant *)
     201      let r2 ≝ \snd pair_reg in
     202      match r2 with
     203      [ pseudo p ⇒ lattice_psingleton p
     204      | hardware h ⇒ lattice_hsingleton h
     205      ]
     206    ]
     207  | joint_st_return ⇒ 〈[ ], list_set_union ? eq_Register RegisterCalleeSaved ret_regs〉
     208  | joint_st_goto l ⇒ lattice_bottom
     209  | joint_st_extension ext ⇒
     210    match ext with
     211    [ ertl_st_ext_new_frame l ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
     212    | ertl_st_ext_del_frame l ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
     213    | ertl_st_ext_frame_size r l ⇒ lattice_bottom
     214    ]
     215  ].
     216
     217definition eliminable ≝
     218  λglobals: list ident.
     219  λl: register_lattice.
     220  λs: ertl_statement globals.
    211221  let 〈pliveafter, hliveafter〉 ≝ l in
    212   match stmt with
    213   [ ertl_st_skip _ ⇒ None ?
    214   | ertl_st_comment _ _ ⇒ None ?
    215   | ertl_st_cost _ _ ⇒ None ?
    216   | ertl_st_new_frame _ ⇒ None ?
    217   | ertl_st_del_frame _ ⇒ None ?
    218   | ertl_st_pop _ _ ⇒ None ?
    219   | ertl_st_push _ _ ⇒ None ?
    220   | ertl_st_clear_carry _  ⇒ None ?
    221   | ertl_st_set_carry _  ⇒ None ?
    222   | ertl_st_store _ _ _ _ ⇒ None ?
    223   | ertl_st_call_id _ _ _ ⇒ None ?
    224   | ertl_st_cond _ _ _ ⇒ None ?
    225   | ertl_st_return ⇒ None ?
    226   | ertl_st_get_hdw r _ l ⇒
    227     if list_set_member register (eq_identifier ?) r pliveafter ∨
    228        list_set_member Register eq_Register RegisterCarry hliveafter then
    229       None ?
    230     else
    231       Some ? l
    232   | ertl_st_frame_size r l ⇒
    233     if list_set_member register (eq_identifier ?) r pliveafter ∨
    234        list_set_member Register eq_Register RegisterCarry hliveafter then
    235       None ?
    236     else
    237       Some ? l
    238   | ertl_st_int r _ l ⇒
    239     if list_set_member register (eq_identifier ?) r pliveafter ∨
    240        list_set_member Register eq_Register RegisterCarry hliveafter then
    241       None ?
    242     else
    243       Some ? l
    244   | ertl_st_addr r1 r2 _ l ⇒
    245     if list_set_member register (eq_identifier ?) r1 pliveafter ∨
    246        list_set_member register (eq_identifier ?) r2 pliveafter ∨
    247        list_set_member Register eq_Register RegisterCarry hliveafter then
    248       None ?
    249     else
    250       Some ? l
    251   | ertl_st_move r _ l ⇒
    252     if list_set_member register (eq_identifier ?) r pliveafter ∨
    253        list_set_member Register eq_Register RegisterCarry hliveafter then
    254       None ?
    255     else
    256       Some ? l
    257   | ertl_st_opaccs _ d1 d2 _ _ l ⇒
    258     if list_set_member register (eq_identifier ?) d1 pliveafter ∨
    259        list_set_member register (eq_identifier ?) d2 pliveafter ∨
    260        list_set_member Register eq_Register RegisterCarry hliveafter then
    261       None ?
    262     else
    263       Some ? l
    264   | ertl_st_op1 _ r _ l ⇒
    265     if list_set_member register (eq_identifier ?) r pliveafter ∨
    266        list_set_member Register eq_Register RegisterCarry hliveafter then
    267       None ?
    268     else
    269       Some ? l
    270   | ertl_st_op2 _ r _ _ l ⇒
    271     if list_set_member register (eq_identifier ?) r pliveafter ∨
    272        list_set_member Register eq_Register RegisterCarry hliveafter then
    273       None ?
    274     else
    275       Some ? l
    276   | ertl_st_load r _ _ l ⇒
    277     if list_set_member register (eq_identifier ?) r pliveafter ∨
    278        list_set_member Register eq_Register RegisterCarry hliveafter then
    279       None ?
    280     else
    281       Some ? l
    282   | ertl_st_set_hdw r _ l ⇒
    283     if list_set_member Register eq_Register r hliveafter then
    284       None ?
    285     else
    286       Some ? l
    287   | ertl_st_hdw_to_hdw r _ l ⇒
    288     if list_set_member Register eq_Register r hliveafter then
    289       None ?
    290     else
    291       Some ? l
    292   ].
    293 
    294 definition statement_semantics: ertl_statement → register_lattice → register_lattice ≝
     222  match s with
     223  [ joint_st_sequential seq l ⇒
     224    match seq with
     225    [ joint_instr_op2 op2 acc_a r ⇒
     226      if list_set_member register (eq_identifier ?) acc_a pliveafter ∨
     227         list_set_member Register eq_Register RegisterCarry hliveafter then
     228        None ?
     229      else
     230        Some ? l
     231    | joint_instr_clear_carry ⇒ None ?
     232    | joint_instr_set_carry ⇒ None ?
     233    | joint_instr_opaccs opaccs r1 r2 ⇒
     234      if list_set_member register (eq_identifier ?) r1 pliveafter ∨
     235         list_set_member register (eq_identifier ?) r2 pliveafter ∨
     236         list_set_member Register eq_Register RegisterCarry hliveafter then
     237        None ?
     238      else
     239        Some ? l
     240    | joint_instr_op1 op1 r ⇒
     241      if list_set_member register (eq_identifier ?) r pliveafter ∨
     242         list_set_member Register eq_Register RegisterCarry hliveafter then
     243        None ?
     244      else
     245        Some ? l
     246    | joint_instr_pop r ⇒ None ?
     247    | joint_instr_int r _ ⇒
     248      if list_set_member register (eq_identifier ?) r pliveafter ∨
     249         list_set_member Register eq_Register RegisterCarry hliveafter then
     250        None ?
     251      else
     252        Some ? l
     253    | joint_instr_address _ _ r1 r2 ⇒
     254      if list_set_member register (eq_identifier ?) r1 pliveafter ∨
     255         list_set_member register (eq_identifier ?) r2 pliveafter ∨
     256         list_set_member Register eq_Register RegisterCarry hliveafter then
     257        None ?
     258      else
     259        Some ? l
     260    | joint_instr_load acc_a dpl dph ⇒
     261      if list_set_member register (eq_identifier ?) acc_a pliveafter ∨
     262         list_set_member Register eq_Register RegisterCarry hliveafter then
     263        None ?
     264      else
     265        Some ? l
     266    | joint_instr_call_id _ nparams ⇒ None ?
     267    | joint_instr_comment c ⇒ None ?
     268    | joint_instr_cond r lbl_true ⇒ None ?
     269    | joint_instr_store acc_a dpl dph ⇒ None ?
     270    | joint_instr_cost_label clabel ⇒ None ?
     271    | joint_instr_push r ⇒ None ?
     272    | joint_instr_move pair_reg ⇒
     273      let r1 ≝ \fst pair_reg in
     274      let r2 ≝ \snd pair_reg in
     275      match r1 with
     276      [ pseudo p1 ⇒
     277        if list_set_member register (eq_identifier ?) p1 pliveafter ∨
     278           list_set_member Register eq_Register RegisterCarry hliveafter then
     279          None ?
     280        else
     281          Some ? l
     282      | hardware h1 ⇒
     283        if list_set_member Register eq_Register h1 hliveafter then
     284          None ?
     285        else
     286          Some ? l
     287      ]
     288    ]
     289  | joint_st_goto l ⇒ None ?
     290  | joint_st_return ⇒ None ?
     291  | joint_st_extension ext ⇒
     292    match ext with
     293    [ ertl_st_ext_new_frame l ⇒ None ?
     294    | ertl_st_ext_del_frame l ⇒ None ?
     295    | ertl_st_ext_frame_size r l ⇒
     296      if list_set_member register (eq_identifier ?) r pliveafter ∨
     297        list_set_member Register eq_Register RegisterCarry hliveafter then
     298        None ?
     299      else
     300        Some ? l
     301    ]
     302  ].
     303
     304definition statement_semantics: ∀globals: list ident. ertl_statement globals → register_lattice → register_lattice ≝
     305  λglobals.
    295306  λstmt.
    296307  λliveafter.
    297   match eliminable liveafter stmt with
    298   [ None ⇒ lattice_join (lattice_diff liveafter (defined stmt)) (used stmt)
     308  match eliminable globals liveafter stmt with
     309  [ None ⇒ lattice_join (lattice_diff liveafter (defined globals stmt)) (used globals stmt)
    299310  | Some l ⇒ liveafter
    300311  ].
     
    307318
    308319definition livebefore ≝
     320  λglobals: list ident.
    309321  λint_fun.
    310322  λlabel.
    311323  λliveafter: valuation.
    312   match lookup ? ? (ertl_if_graph int_fun) label with
     324  match lookup ? ? (ertl_if_graph globals int_fun) label with
    313325  [ None      ⇒ ?
    314   | Some stmt ⇒ statement_semantics stmt (liveafter label)
     326  | Some stmt ⇒ statement_semantics globals stmt (liveafter label)
    315327  ].
    316328  cases not_implemented (* XXX *)
     
    318330
    319331definition liveafter ≝
     332  λglobals.
    320333  λint_fun.
    321334  λlivebefore.
    322335  λlabel.
    323336  λliveafter: valuation.
    324   match lookup ? ? (ertl_if_graph int_fun) label with
     337  match lookup … (ertl_if_graph globals int_fun) label with
    325338  [ None      ⇒ ?
    326   | Some stmt ⇒ list_set_fold ? ? (λsuccessor. λaccu.
     339  | Some stmt ⇒ list_set_fold … (λsuccessor. λaccu: register_lattice.
    327340      lattice_join (livebefore successor liveafter) accu)
    328       lattice_bottom (statement_successors stmt)
     341      lattice_bottom (statement_successors globals stmt)
    329342  ].
    330343  cases not_implemented (* XXX *)
    331344qed.
    332345
    333 definition analyse: ertl_internal_function → valuation ≝
     346definition analyse ≝
     347  λglobals.
    334348  λint_fun.
    335     fix_lfp (liveafter int_fun (livebefore int_fun)).
     349    fix_lfp (liveafter globals int_fun (livebefore globals int_fun)).
Note: See TracChangeset for help on using the changeset viewer.