source: src/ERTL/liveness.ma @ 1229

Last change on this file since 1229 was 1223, checked in by mulligan, 9 years ago

changes

File size: 11.0 KB
Line 
1include "ASM/Util.ma".
2include "ERTL/ERTL.ma".
3include "utilities/adt/set_adt.ma".
4
5definition statement_successors ≝
6  λglobals: list ident.
7  λs: ertl_statement globals.
8  match s with
9  [ joint_st_sequential seq l ⇒
10    match seq with
11    [ joint_instr_cond acc_a_reg lbl_true ⇒
12        set_insert … lbl_true (set_singleton … l)
13    | _ ⇒ set_singleton … l
14    ]
15  | joint_st_extension ext ⇒
16    match ext with
17    [ ertl_st_ext_new_frame l ⇒ set_singleton … l
18    | ertl_st_ext_del_frame l ⇒ set_singleton … l
19    | ertl_st_ext_frame_size r l ⇒ set_singleton … l
20    ]
21  | joint_st_goto l ⇒ set_singleton … l
22  | joint_st_return ⇒ set_empty …
23  ].
24
25definition register_lattice ≝ (set register) × (set Register).
26definition lattice_property ≝ register_lattice.
27definition lattice_bottom: register_lattice ≝ 〈set_empty register, set_empty Register〉.
28definition lattice_psingleton: register → register_lattice ≝
29  λr.
30    〈set_singleton … r, set_empty …〉.
31definition lattice_hsingleton: Register → register_lattice ≝
32  λr.
33    〈set_empty …, set_singleton … r〉.
34
35definition lattice_join: register_lattice → register_lattice → register_lattice ≝
36  λleft.
37  λright.
38  let 〈lp, lh〉 ≝ left in
39  let 〈rp, rh〉 ≝ right in
40    〈set_union … lp rp, set_union … lh rh〉.
41
42definition lattice_diff: register_lattice → register_lattice → register_lattice ≝
43  λleft.
44  λright.
45  let 〈lp, lh〉 ≝ left in
46  let 〈rp, rh〉 ≝ right in
47    〈set_diff … lp rp, set_diff … lh rh〉.
48
49definition lattice_equal: register_lattice → register_lattice → bool ≝
50  λleft.
51  λright.
52  let 〈lp, lh〉 ≝ left in
53  let 〈rp, rh〉 ≝ right in
54    andb (set_equal … (eq_identifier …) lp rp) (set_equal … eq_Register lh rh).
55
56definition lattice_is_maximal: register_lattice → bool ≝ λl. false.
57
58record lattice_property_sig: Type[1] ≝
59{
60  lp_type      : Type[0];
61  lp_property  : Type[0];
62  lp_bottom    : lp_type;
63  lp_psingleton: register → lp_type;
64  lp_hsingleton: Register → lp_type;
65  lp_join      : lp_type → lp_type → lp_type;
66  lp_diff      : lp_type → lp_type → lp_type;
67  lp_equal     : lp_type → lp_type → bool;
68  lp_is_maximal: lp_type → bool
69}.
70
71definition property ≝
72  mk_lattice_property_sig
73    ((set register) × (set Register))
74    lattice_property
75    lattice_bottom
76    lattice_psingleton
77    lattice_hsingleton
78    lattice_join
79    lattice_diff
80    lattice_equal
81    lattice_is_maximal.
82
83definition defined ≝
84  λglobals: list ident.
85  λs: ertl_statement globals.
86  match s with
87  [ joint_st_sequential seq l ⇒
88    match seq with
89    [ joint_instr_op2 op2 r _ ⇒
90      match op2 with
91      [ Add ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r)
92      | Addc ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r)
93      | Sub ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r)
94      | _ ⇒ lattice_psingleton r
95      ]
96    | joint_instr_clear_carry ⇒ lattice_hsingleton RegisterCarry
97    | joint_instr_set_carry ⇒ lattice_hsingleton RegisterCarry
98    | joint_instr_opaccs opaccs r1 r2 ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
99    | joint_instr_op1 op1 r ⇒ lattice_psingleton r
100    | joint_instr_pop r ⇒ lattice_psingleton r
101    | joint_instr_int r _ ⇒ lattice_psingleton r
102    | joint_instr_address _ _ r1 r2 ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
103    | joint_instr_load r _ _ ⇒ lattice_psingleton r
104    (* Potentially destroys all caller-save hardware registers. *)
105    | joint_instr_call_id _ _ ⇒ 〈set_empty …, set_from_list … RegisterCallerSaved〉
106    | joint_instr_comment c ⇒ lattice_bottom
107    | joint_instr_cond r lbl_true ⇒ lattice_bottom
108    | joint_instr_store acc_a dpl dph ⇒ lattice_bottom
109    | joint_instr_cost_label clabel ⇒ lattice_bottom
110    | joint_instr_push r ⇒ lattice_bottom
111    | joint_instr_move pair_reg ⇒
112      (* first register relevant only *)
113      let r1 ≝ \fst pair_reg in
114      match r1 with
115      [ pseudo p ⇒ lattice_psingleton p
116      | hardware h ⇒ lattice_hsingleton h
117      ]
118    ]
119  | joint_st_return ⇒ lattice_bottom
120  | joint_st_extension ext ⇒
121    match ext with
122    [ ertl_st_ext_new_frame l ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
123    | ertl_st_ext_del_frame l ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
124    | ertl_st_ext_frame_size r l ⇒ lattice_psingleton r
125    ]
126  | joint_st_goto l ⇒ lattice_bottom
127  ].
128
129definition ret_regs ≝ set_from_list … RegisterRets.
130
131definition used ≝
132  λglobals: list ident.
133  λs: ertl_statement globals.
134  match s with
135  [ joint_st_sequential seq l ⇒
136    match seq with
137    [ joint_instr_op2 op2 acc_a r ⇒
138      match op2 with
139      [ Addc ⇒
140        lattice_join (lattice_join (lattice_psingleton acc_a) (lattice_psingleton r)) (lattice_hsingleton RegisterCarry)
141      | _ ⇒ lattice_join (lattice_psingleton acc_a) (lattice_psingleton r)
142      ]
143    | joint_instr_clear_carry ⇒ lattice_bottom
144    | joint_instr_set_carry ⇒ lattice_bottom
145    (* acc_a and acc_b *)
146    | joint_instr_opaccs opaccs r1 r2 ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
147    | joint_instr_op1 op1 r ⇒ lattice_psingleton r
148    | joint_instr_pop r ⇒ lattice_bottom
149    | joint_instr_int r _ ⇒ lattice_bottom
150    | joint_instr_address _ _ r1 r2 ⇒ lattice_bottom
151    | joint_instr_load acc_a dpl dph ⇒ lattice_join (lattice_psingleton dpl) (lattice_psingleton dph)
152    (* Reads the hardware registers that are used to pass parameters. *)
153    | joint_instr_call_id _ nparams ⇒ 〈set_empty …, set_from_list … (prefix ? nparams RegisterParams)〉
154    | joint_instr_comment c ⇒ lattice_bottom
155    | joint_instr_cond r lbl_true ⇒ lattice_psingleton r
156    | joint_instr_store acc_a dpl dph ⇒
157      lattice_join (lattice_join (lattice_psingleton acc_a) (lattice_psingleton dpl)) (lattice_psingleton dph)
158    | joint_instr_cost_label clabel ⇒ lattice_bottom
159    | joint_instr_push r ⇒ lattice_psingleton r
160    | joint_instr_move pair_reg ⇒
161      (* only second reg in pair relevant *)
162      let r2 ≝ \snd pair_reg in
163      match r2 with
164      [ pseudo p ⇒ lattice_psingleton p
165      | hardware h ⇒ lattice_hsingleton h
166      ]
167    ]
168  | joint_st_return ⇒ 〈set_empty …, set_union … (set_from_list … RegisterCalleeSaved) ret_regs〉
169  | joint_st_goto l ⇒ lattice_bottom
170  | joint_st_extension ext ⇒
171    match ext with
172    [ ertl_st_ext_new_frame l ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
173    | ertl_st_ext_del_frame l ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
174    | ertl_st_ext_frame_size r l ⇒ lattice_bottom
175    ]
176  ].
177
178definition eliminable ≝
179  λglobals: list ident.
180  λl: register_lattice.
181  λs: ertl_statement globals.
182  let 〈pliveafter, hliveafter〉 ≝ l in
183  match s with
184  [ joint_st_sequential seq l ⇒
185    match seq with
186    [ joint_instr_op2 op2 acc_a r ⇒
187      if set_member … (eq_identifier …) acc_a pliveafter ∨
188         set_member … eq_Register RegisterCarry hliveafter then
189        None ?
190      else
191        Some ? l
192    | joint_instr_clear_carry ⇒ None ?
193    | joint_instr_set_carry ⇒ None ?
194    | joint_instr_opaccs opaccs r1 r2 ⇒
195      if set_member … (eq_identifier …) r1 pliveafter ∨
196         set_member … (eq_identifier …) r2 pliveafter ∨
197         set_member … eq_Register RegisterCarry hliveafter then
198        None ?
199      else
200        Some ? l
201    | joint_instr_op1 op1 r ⇒
202      if set_member … (eq_identifier …) r pliveafter ∨
203         set_member … eq_Register RegisterCarry hliveafter then
204        None ?
205      else
206        Some ? l
207    | joint_instr_pop r ⇒ None ?
208    | joint_instr_int r _ ⇒
209      if set_member … (eq_identifier …) r pliveafter ∨
210         set_member … eq_Register RegisterCarry hliveafter then
211        None ?
212      else
213        Some ? l
214    | joint_instr_address _ _ r1 r2 ⇒
215      if set_member … (eq_identifier …) r1 pliveafter ∨
216         set_member … (eq_identifier …) r2 pliveafter ∨
217         set_member … eq_Register RegisterCarry hliveafter then
218        None ?
219      else
220        Some ? l
221    | joint_instr_load acc_a dpl dph ⇒
222      if set_member ? (eq_identifier …) acc_a pliveafter ∨
223         set_member … eq_Register RegisterCarry hliveafter then
224        None ?
225      else
226        Some ? l
227    | joint_instr_call_id _ nparams ⇒ None ?
228    | joint_instr_comment c ⇒ None ?
229    | joint_instr_cond r lbl_true ⇒ None ?
230    | joint_instr_store acc_a dpl dph ⇒ None ?
231    | joint_instr_cost_label clabel ⇒ None ?
232    | joint_instr_push r ⇒ None ?
233    | joint_instr_move pair_reg ⇒
234      let r1 ≝ \fst pair_reg in
235      let r2 ≝ \snd pair_reg in
236      match r1 with
237      [ pseudo p1 ⇒
238        if set_member … (eq_identifier …) p1 pliveafter ∨
239           set_member … eq_Register RegisterCarry hliveafter then
240          None ?
241        else
242          Some ? l
243      | hardware h1 ⇒
244        if set_member … eq_Register h1 hliveafter then
245          None ?
246        else
247          Some ? l
248      ]
249    ]
250  | joint_st_goto l ⇒ None ?
251  | joint_st_return ⇒ None ?
252  | joint_st_extension ext ⇒
253    match ext with
254    [ ertl_st_ext_new_frame l ⇒ None ?
255    | ertl_st_ext_del_frame l ⇒ None ?
256    | ertl_st_ext_frame_size r l ⇒
257      if set_member ? (eq_identifier RegisterTag) r pliveafter ∨
258         set_member ? eq_Register RegisterCarry hliveafter then
259        None ?
260      else
261        Some ? l
262    ]
263  ].
264
265definition statement_semantics: ∀globals: list ident. ertl_statement globals → register_lattice → register_lattice ≝
266  λglobals.
267  λstmt.
268  λliveafter.
269  match eliminable globals liveafter stmt with
270  [ None ⇒ lattice_join (lattice_diff liveafter (defined globals stmt)) (used globals stmt)
271  | Some l ⇒ liveafter
272  ].
273
274definition valuation ≝ label → register_lattice.
275definition rhs ≝ valuation → lattice_property.
276definition equations ≝ label → rhs.
277
278axiom fix_lfp: equations → valuation.
279
280definition livebefore ≝
281  λglobals: list ident.
282  λint_fun: ertl_internal_function globals.
283  λlabel.
284  λliveafter: valuation.
285  match lookup ? ? (joint_if_graph … int_fun) label with
286  [ None      ⇒ ?
287  | Some stmt ⇒ statement_semantics globals stmt (liveafter label)
288  ].
289  cases not_implemented (* XXX *)
290qed.
291
292definition liveafter ≝
293  λglobals: list ident.
294  λint_fun: ertl_internal_function globals.
295  λlivebefore: label → ?.
296  λlabel.
297  λliveafter: valuation.
298  match lookup … (joint_if_graph … int_fun) label with
299  [ None      ⇒ ?
300  | Some stmt ⇒ set_fold ? ? (λsuccessor. λaccu: register_lattice.
301      lattice_join (livebefore successor liveafter) accu)
302      (statement_successors globals stmt) lattice_bottom
303  ].
304  cases not_implemented (* XXX *)
305qed.
306
307definition analyse ≝
308  λglobals.
309  λint_fun.
310    fix_lfp (liveafter globals int_fun (livebefore globals int_fun)).
Note: See TracBrowser for help on using the repository browser.