Ignore:
Timestamp:
Oct 6, 2011, 6:45:54 PM (10 years ago)
Author:
campbell
Message:

Merge trunk to invariants branch, sorting out the handling of temporaries
in Clight/toCminor.

Location:
Deliverables/D3.3/id-lookup-branch
Files:
2 edited

Legend:

Unmodified
Added
Removed

  • Deliverables/D3.3/id-lookup-branch

  • Deliverables/D3.3/id-lookup-branch/ERTL/liveness.ma

    r1197 r1311  
    11include "ASM/Util.ma".
    22include "ERTL/ERTL.ma".
    3 
    4 definition list_set_union ≝
    5   λA: Type[0].
    6   λeq_a: A → A → bool.
    7   λl: list A.
    8   λr: list A.
    9     nub_by A eq_a (l @ r).
    10 
    11 definition list_set_add ≝
    12   λA: Type[0].
    13   λeq_a: A → A → bool.
    14   λa: A.
    15   λs: list A.
    16     nub_by A eq_a (a :: s).
    17 
    18 definition list_set_diff ≝
    19   λA: Type[0].
    20   λeq_a: A → A → bool.
    21   λl: list A.
    22   λr: list A.
    23     filter A (λx. member A eq_a x r) l.
    24 
    25 definition list_set_equal ≝
    26   λA: Type[0].
    27   λeq_a: A → A → bool.
    28   λl: list A.
    29   λr: list A.
    30     foldr ? ? andb true (map ? ? (λx. member A eq_a x r) l).
    31 
    32 definition list_set_member ≝ member.
    33 
    34 definition list_set_fold ≝ foldr.
     3include "utilities/adt/set_adt.ma".
    354
    365definition statement_successors ≝
    … …  
    387  λs: ertl_statement globals.
    398  match s with
    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 ⇒ [ ]
    54   ].
    55 
    56 definition register_lattice ≝ (list register) × (list Register).
     9  [ sequential seq l ⇒
     10    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
     18definition register_lattice ≝ (set register) × (set Register).
    5719definition lattice_property ≝ register_lattice.
    58 definition lattice_bottom: register_lattice ≝ 〈[ ], [ ]〉.
     20definition lattice_bottom: register_lattice ≝ 〈set_empty register, set_empty Register〉.
    5921definition lattice_psingleton: register → register_lattice ≝
    6022  λr.
    61     〈[ r ], [ ]〉.
     23    〈set_singleton … r, set_empty …〉.
    6224definition lattice_hsingleton: Register → register_lattice ≝
    6325  λr.
    64     〈[ ], [ r ]〉.
     26    〈set_empty …, set_singleton … r〉.
    6527
    6628definition lattice_join: register_lattice → register_lattice → register_lattice ≝
    … …  
    6931  let 〈lp, lh〉 ≝ left in
    7032  let 〈rp, rh〉 ≝ right in
    71     〈list_set_union ? (eq_identifier ?) lp rp, list_set_union ? eq_Register lh rh〉.
     33    〈set_union … lp rp, set_union … lh rh〉.
    7234
    7335definition lattice_diff: register_lattice → register_lattice → register_lattice ≝
    … …  
    7638  let 〈lp, lh〉 ≝ left in
    7739  let 〈rp, rh〉 ≝ right in
    78     〈list_set_diff ? (eq_identifier ?) lp rp, list_set_diff ? eq_Register lh rh〉.
     40    〈set_diff … lp rp, set_diff … lh rh〉.
    7941
    8042definition lattice_equal: register_lattice → register_lattice → bool ≝
    … …  
    8345  let 〈lp, lh〉 ≝ left in
    8446  let 〈rp, rh〉 ≝ right in
    85     andb (list_set_equal ? (eq_identifier ?) lp rp) (list_set_equal ? eq_Register lh rh).
     47    andb (set_equal … (eq_identifier …) lp rp) (set_equal … eq_Register lh rh).
    8648
    8749definition lattice_is_maximal: register_lattice → bool ≝ λl. false.
    … …  
    10264definition property ≝
    10365  mk_lattice_property_sig
    104     ((list register) × (list Register))
     66    ((set register) × (set Register))
    10567    lattice_property
    10668    lattice_bottom
    … …  
    11678  λs: ertl_statement globals.
    11779  match s with
    118   [ joint_st_sequential seq l ⇒
    119     match seq with
    120     [ joint_instr_op2 op2 r _ ⇒
     80  [ sequential seq l ⇒
     81    match seq with
     82    [ OP2 op2 r1 r2 _ ⇒
    12183      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
     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
     88      ]
     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
    13598    (* 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 ⇒
     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 ⇒
    143106      (* first register relevant only *)
    144107      let r1 ≝ \fst pair_reg in
    … …  
    147110      | hardware h ⇒ lattice_hsingleton h
    148111      ]
    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
    158   ].
    159 
    160 definition list_set_of_list ≝
    161   λrl.
    162     foldr ? ? (list_set_add Register eq_Register) rl [ ].
    163 
    164 definition list_set_of_list2 ≝
    165   let f ≝ λset. λr. list_set_add Register eq_Register r set in
    166     foldl ? ? f [ ].
    167 
    168 definition ret_regs ≝ list_set_of_list RegisterRets.
     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
     121definition ret_regs ≝ set_from_list … RegisterRets.
    169122
    170123definition used ≝
    … …  
    172125  λs: ertl_statement globals.
    173126  match s with
    174   [ joint_st_sequential seq l ⇒
    175     match seq with
    176     [ joint_instr_op2 op2 acc_a r ⇒
     127  [ sequential seq l ⇒
     128    match seq with
     129    [ OP2 op2 acc_a r1 r2 ⇒
    177130      match op2 with
    178131      [ 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
     132        lattice_join (lattice_join (lattice_psingleton r1) (lattice_psingleton r2)) (lattice_hsingleton RegisterCarry)
     133      | _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
     134      ]
     135    | CLEAR_CARRY ⇒ lattice_bottom
     136    | SET_CARRY ⇒ lattice_bottom
    184137    (* 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)
     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)
    191145    (* Reads the hardware registers that are used to pass parameters. *)
    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 ⇒
     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 ⇒
    196150      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 ⇒
     151    | COST_LABEL clabel ⇒ lattice_bottom
     152    | PUSH r ⇒ lattice_psingleton r
     153    | MOVE pair_reg ⇒
    200154      (* only second reg in pair relevant *)
    201155      let r2 ≝ \snd pair_reg in
    … …  
    204158      | hardware h ⇒ lattice_hsingleton h
    205159      ]
    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 ⇒
     160  | extension ext ⇒
    210161    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     ]
     162    [ ertl_st_ext_new_frame ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
     163    | ertl_st_ext_del_frame ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
     164    | ertl_st_ext_frame_size r ⇒ lattice_bottom]]
     165  | RETURN ⇒ 〈set_empty …, set_union … (set_from_list … RegisterCalleeSaved) ret_regs〉
     166  | GOTO l ⇒ lattice_bottom
    215167  ].
    216168
    … …  
    221173  let 〈pliveafter, hliveafter〉 ≝ l in
    222174  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 ⇒
     175  [ sequential seq l ⇒
     176    match seq with
     177    [ OP2 op2 r1 r2 r3 ⇒
     178      if set_member … (eq_identifier …) r1 pliveafter ∨
     179         set_member … eq_Register RegisterCarry hliveafter then
     180        None ?
     181      else
     182        Some ? l
     183    | CLEAR_CARRY ⇒ None ?
     184    | SET_CARRY ⇒ None ?
     185    | OPACCS opaccs dr1 dr2 sr1 sr2 ⇒
     186      if set_member … (eq_identifier …) dr1 pliveafter ∨
     187         set_member … (eq_identifier …) dr2 pliveafter ∨
     188         set_member … eq_Register RegisterCarry hliveafter then
     189        None ?
     190      else
     191        Some ? l
     192    | OP1 op1 r1 r2 ⇒
     193      if set_member … (eq_identifier …) r1 pliveafter ∨
     194         set_member … eq_Register RegisterCarry hliveafter then
     195        None ?
     196      else
     197        Some ? l
     198    | POP r ⇒ None ?
     199    | INT r _ ⇒
     200      if set_member … (eq_identifier …) r pliveafter ∨
     201         set_member … eq_Register RegisterCarry hliveafter then
     202        None ?
     203      else
     204        Some ? l
     205    | ADDRESS _ _ r1 r2 ⇒
     206      if set_member … (eq_identifier …) r1 pliveafter ∨
     207         set_member … (eq_identifier …) r2 pliveafter ∨
     208         set_member … eq_Register RegisterCarry hliveafter then
     209        None ?
     210      else
     211        Some ? l
     212    | LOAD acc_a dpl dph ⇒
     213      if set_member ? (eq_identifier …) acc_a pliveafter ∨
     214         set_member … eq_Register RegisterCarry hliveafter then
     215        None ?
     216      else
     217        Some ? l
     218    | CALL_ID _ nparams _ ⇒ None ?
     219    | COMMENT c ⇒ None ?
     220    | COND r lbl_true ⇒ None ?
     221    | STORE acc_a dpl dph ⇒ None ?
     222    | COST_LABEL clabel ⇒ None ?
     223    | PUSH r ⇒ None ?
     224    | MOVE pair_reg ⇒
    273225      let r1 ≝ \fst pair_reg in
    274226      let r2 ≝ \snd pair_reg in
    275227      match r1 with
    276228      [ pseudo p1 ⇒
    277         if list_set_member register (eq_identifier ?) p1 pliveafter ∨
    278            list_set_member Register eq_Register RegisterCarry hliveafter then
     229        if set_member … (eq_identifier …) p1 pliveafter ∨
     230           set_member … eq_Register RegisterCarry hliveafter then
    279231          None ?
    280232        else
    281233          Some ? l
    282234      | hardware h1 ⇒
    283         if list_set_member Register eq_Register h1 hliveafter then
     235        if set_member … eq_Register h1 hliveafter then
    284236          None ?
    285237        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     ]
     238          Some ? l]
     239    | extension ext ⇒
     240      match ext with
     241      [ ertl_st_ext_new_frame ⇒ None ?
     242      | ertl_st_ext_del_frame ⇒ None ?
     243      | ertl_st_ext_frame_size r ⇒
     244        if set_member ? (eq_identifier RegisterTag) r pliveafter ∨
     245           set_member ? eq_Register RegisterCarry hliveafter then
     246          None ?
     247        else
     248          Some ? l]]
     249  | GOTO l ⇒ None ?
     250  | RETURN ⇒ None ?
    302251  ].
    303252
    … …  
    319268definition livebefore ≝
    320269  λglobals: list ident.
    321   λint_fun.
     270  λint_fun: ertl_internal_function globals.
    322271  λlabel.
    323272  λliveafter: valuation.
    324   match lookup ? ? (ertl_if_graph globals int_fun) label with
     273  match lookup … (joint_if_code … int_fun) label with
    325274  [ None      ⇒ ?
    326275  | Some stmt ⇒ statement_semantics globals stmt (liveafter label)
    … …  
    330279
    331280definition liveafter ≝
    332   λglobals.
    333   λint_fun.
    334   λlivebefore.
     281  λglobals: list ident.
     282  λint_fun: ertl_internal_function globals.
     283  λlivebefore: label → ?.
    335284  λlabel.
    336285  λliveafter: valuation.
    337   match lookup … (ertl_if_graph globals int_fun) label with
     286  match lookup … (joint_if_code … int_fun) label with
    338287  [ None      ⇒ ?
    339   | Some stmt ⇒ list_set_fold … (λsuccessor. λaccu: register_lattice.
     288  | Some stmt ⇒ set_fold ? ? (λsuccessor. λaccu: register_lattice.
    340289      lattice_join (livebefore successor liveafter) accu)
    341       lattice_bottom (statement_successors globals stmt)
     290      (statement_successors globals stmt) lattice_bottom
    342291  ].
    343292  cases not_implemented (* XXX *)
Note: See TracChangeset for help on using the changeset viewer.