source: src/ERTL/liveness.ma @ 1684

Last change on this file since 1684 was 1463, checked in by mulligan, 9 years ago

added erasure for lin

File size: 11.1 KB
RevLine 
[1088]1include "ASM/Util.ma".
2include "ERTL/ERTL.ma".
[1223]3include "utilities/adt/set_adt.ma".
[1088]4
5definition statement_successors ≝
[1185]6  λglobals: list ident.
7  λs: ertl_statement globals.
[1088]8  match s with
[1282]9  [ sequential seq l ⇒
[1185]10    match seq with
[1282]11    [ COND acc_a_reg lbl_true ⇒
[1223]12        set_insert … lbl_true (set_singleton … l)
[1250]13    | _ ⇒ set_singleton … l ]
[1282]14  | GOTO l ⇒ set_singleton … l
15  | RETURN ⇒ set_empty ?
[1088]16  ].
17
[1223]18definition register_lattice ≝ (set register) × (set Register).
[1088]19definition lattice_property ≝ register_lattice.
[1223]20definition lattice_bottom: register_lattice ≝ 〈set_empty register, set_empty Register〉.
[1088]21definition lattice_psingleton: register → register_lattice ≝
22  λr.
[1223]23    〈set_singleton … r, set_empty …〉.
[1088]24definition lattice_hsingleton: Register → register_lattice ≝
25  λr.
[1223]26    〈set_empty …, set_singleton … r〉.
[1088]27
28definition lattice_join: register_lattice → register_lattice → register_lattice ≝
29  λleft.
30  λright.
31  let 〈lp, lh〉 ≝ left in
32  let 〈rp, rh〉 ≝ right in
[1223]33    〈set_union … lp rp, set_union … lh rh〉.
[1088]34
35definition lattice_diff: register_lattice → register_lattice → register_lattice ≝
36  λleft.
37  λright.
38  let 〈lp, lh〉 ≝ left in
39  let 〈rp, rh〉 ≝ right in
[1223]40    〈set_diff … lp rp, set_diff … lh rh〉.
[1088]41
42definition lattice_equal: register_lattice → register_lattice → bool ≝
43  λleft.
44  λright.
45  let 〈lp, lh〉 ≝ left in
46  let 〈rp, rh〉 ≝ right in
[1223]47    andb (set_equal … (eq_identifier …) lp rp) (set_equal … eq_Register lh rh).
[1088]48
49definition lattice_is_maximal: register_lattice → bool ≝ λl. false.
50
[1124]51record 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
64definition property ≝
65  mk_lattice_property_sig
[1223]66    ((set register) × (set Register))
[1124]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
[1185]76definition defined ≝
77  λglobals: list ident.
78  λs: ertl_statement globals.
[1088]79  match s with
[1282]80  [ sequential seq l ⇒
[1185]81    match seq with
[1282]82    [ OP2 op2 r1 r2 _ ⇒
[1185]83      match op2 with
[1260]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
[1185]88      ]
[1282]89    | CLEAR_CARRY ⇒ lattice_hsingleton RegisterCarry
90    | SET_CARRY ⇒ lattice_hsingleton RegisterCarry
91    | OPACCS opaccs dr1 dr2 sr1 sr2 ⇒
[1275]92       lattice_join (lattice_psingleton dr1) (lattice_psingleton dr2)
[1282]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
[1185]98    (* Potentially destroys all caller-save hardware registers. *)
[1282]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 ⇒
[1185]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      ]
[1282]112    | extension ext ⇒
[1250]113      match ext with
[1260]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]]
[1282]117  | RETURN ⇒ lattice_bottom
118  | GOTO l ⇒ lattice_bottom
[1088]119  ].
120
[1223]121definition ret_regs ≝ set_from_list … RegisterRets.
[1094]122
[1185]123definition used ≝
124  λglobals: list ident.
125  λs: ertl_statement globals.
126  match s with
[1282]127  [ sequential seq l ⇒
[1185]128    match seq with
[1282]129    [ OP2 op2 acc_a r1 r2 ⇒
[1185]130      match op2 with
131      [ Addc ⇒
[1260]132        lattice_join (lattice_join (lattice_psingleton r1) (lattice_psingleton r2)) (lattice_hsingleton RegisterCarry)
133      | _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
[1185]134      ]
[1282]135    | CLEAR_CARRY ⇒ lattice_bottom
136    | SET_CARRY ⇒ lattice_bottom
[1185]137    (* acc_a and acc_b *)
[1282]138    | OPACCS opaccs dr1 dr2 sr1 sr2 ⇒
[1275]139       lattice_join (lattice_psingleton sr1) (lattice_psingleton sr2)
[1282]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)
[1094]145    (* Reads the hardware registers that are used to pass parameters. *)
[1282]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 ⇒
[1185]150      lattice_join (lattice_join (lattice_psingleton acc_a) (lattice_psingleton dpl)) (lattice_psingleton dph)
[1282]151    | COST_LABEL clabel ⇒ lattice_bottom
152    | PUSH r ⇒ lattice_psingleton r
153    | MOVE pair_reg ⇒
[1463]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 *)
[1185]168      let r2 ≝ \snd pair_reg in
169      match r2 with
170      [ pseudo p ⇒ lattice_psingleton p
171      | hardware h ⇒ lattice_hsingleton h
172      ]
[1282]173  | extension ext ⇒
[1185]174    match ext with
[1260]175    [ ertl_st_ext_new_frame ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
176    | ertl_st_ext_del_frame ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
177    | ertl_st_ext_frame_size r ⇒ lattice_bottom]]
[1282]178  | RETURN ⇒ 〈set_empty …, set_union … (set_from_list … RegisterCalleeSaved) ret_regs〉
179  | GOTO l ⇒ lattice_bottom
[1094]180  ].
181
[1185]182definition eliminable ≝
183  λglobals: list ident.
184  λl: register_lattice.
185  λs: ertl_statement globals.
[1094]186  let 〈pliveafter, hliveafter〉 ≝ l in
[1185]187  match s with
[1282]188  [ sequential seq l ⇒
[1185]189    match seq with
[1282]190    [ OP2 op2 r1 r2 r3 ⇒
[1260]191      if set_member … (eq_identifier …) r1 pliveafter ∨
[1223]192         set_member … eq_Register RegisterCarry hliveafter then
[1185]193        None ?
194      else
195        Some ? l
[1282]196    | CLEAR_CARRY ⇒ None ?
197    | SET_CARRY ⇒ None ?
198    | OPACCS opaccs dr1 dr2 sr1 sr2 ⇒
[1275]199      if set_member … (eq_identifier …) dr1 pliveafter ∨
200         set_member … (eq_identifier …) dr2 pliveafter ∨
[1223]201         set_member … eq_Register RegisterCarry hliveafter then
[1185]202        None ?
203      else
204        Some ? l
[1282]205    | OP1 op1 r1 r2 ⇒
[1260]206      if set_member … (eq_identifier …) r1 pliveafter ∨
[1223]207         set_member … eq_Register RegisterCarry hliveafter then
[1185]208        None ?
209      else
210        Some ? l
[1282]211    | POP r ⇒ None ?
212    | INT r _ ⇒
[1223]213      if set_member … (eq_identifier …) r pliveafter ∨
214         set_member … eq_Register RegisterCarry hliveafter then
[1185]215        None ?
216      else
217        Some ? l
[1282]218    | ADDRESS _ _ r1 r2 ⇒
[1223]219      if set_member … (eq_identifier …) r1 pliveafter ∨
220         set_member … (eq_identifier …) r2 pliveafter ∨
221         set_member … eq_Register RegisterCarry hliveafter then
[1185]222        None ?
223      else
224        Some ? l
[1282]225    | LOAD acc_a dpl dph ⇒
[1223]226      if set_member ? (eq_identifier …) acc_a pliveafter ∨
227         set_member … eq_Register RegisterCarry hliveafter then
[1185]228        None ?
229      else
230        Some ? l
[1282]231    | CALL_ID _ nparams _ ⇒ None ?
232    | COMMENT c ⇒ None ?
233    | COND r lbl_true ⇒ None ?
234    | STORE acc_a dpl dph ⇒ None ?
235    | COST_LABEL clabel ⇒ None ?
236    | PUSH r ⇒ None ?
237    | MOVE pair_reg ⇒
[1185]238      let r1 ≝ \fst pair_reg in
239      let r2 ≝ \snd pair_reg in
240      match r1 with
241      [ pseudo p1 ⇒
[1223]242        if set_member … (eq_identifier …) p1 pliveafter ∨
243           set_member … eq_Register RegisterCarry hliveafter then
[1185]244          None ?
245        else
246          Some ? l
247      | hardware h1 ⇒
[1223]248        if set_member … eq_Register h1 hliveafter then
[1185]249          None ?
250        else
[1250]251          Some ? l]
[1282]252    | extension ext ⇒
[1250]253      match ext with
[1260]254      [ ertl_st_ext_new_frame ⇒ None ?
255      | ertl_st_ext_del_frame ⇒ None ?
256      | ertl_st_ext_frame_size r ⇒
[1250]257        if set_member ? (eq_identifier RegisterTag) r pliveafter ∨
258           set_member ? eq_Register RegisterCarry hliveafter then
259          None ?
260        else
261          Some ? l]]
[1282]262  | GOTO l ⇒ None ?
263  | RETURN ⇒ None ?
[1094]264  ].
265
[1185]266definition statement_semantics: ∀globals: list ident. ertl_statement globals → register_lattice → register_lattice ≝
267  λglobals.
[1094]268  λstmt.
269  λliveafter.
[1185]270  match eliminable globals liveafter stmt with
271  [ None ⇒ lattice_join (lattice_diff liveafter (defined globals stmt)) (used globals stmt)
[1094]272  | Some l ⇒ liveafter
273  ].
274
275definition valuation ≝ label → register_lattice.
[1124]276definition rhs ≝ valuation → lattice_property.
277definition equations ≝ label → rhs.
[1094]278
[1124]279definition livebefore ≝
[1185]280  λglobals: list ident.
[1223]281  λint_fun: ertl_internal_function globals.
[1124]282  λlabel.
283  λliveafter: valuation.
[1249]284  match lookup … (joint_if_code … int_fun) label with
[1124]285  [ None      ⇒ ?
[1185]286  | Some stmt ⇒ statement_semantics globals stmt (liveafter label)
[1124]287  ].
288  cases not_implemented (* XXX *)
289qed.
290
291definition liveafter ≝
[1223]292  λglobals: list ident.
293  λint_fun: ertl_internal_function globals.
294  λlivebefore: label → ?.
[1124]295  λlabel.
296  λliveafter: valuation.
[1249]297  match lookup … (joint_if_code … int_fun) label with
[1124]298  [ None      ⇒ ?
[1223]299  | Some stmt ⇒ set_fold ? ? (λsuccessor. λaccu: register_lattice.
[1124]300      lattice_join (livebefore successor liveafter) accu)
[1223]301      (statement_successors globals stmt) lattice_bottom
[1124]302  ].
303  cases not_implemented (* XXX *)
304qed.
305
[1463]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
[1185]323definition analyse ≝
324  λglobals.
[1094]325  λint_fun.
[1425]326    the_fixpoint (liveafter globals int_fun (livebefore globals int_fun)).
Note: See TracBrowser for help on using the repository browser.