source: src/ERTL/liveness.ma @ 1185

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

ported liveness analysis to new code

File size: 11.7 KB
Line 
1include "ASM/Util.ma".
2include "ERTL/ERTL.ma".
3
4definition 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
11definition 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
18definition 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
25definition 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
32definition list_set_member ≝ member.
33
34definition list_set_fold ≝ foldr.
35
36definition statement_successors ≝
37  λglobals: list ident.
38  λs: ertl_statement globals.
39  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
56definition register_lattice ≝ (list register) × (list Register).
57definition lattice_property ≝ register_lattice.
58definition lattice_bottom: register_lattice ≝ 〈[ ], [ ]〉.
59definition lattice_psingleton: register → register_lattice ≝
60  λr.
61    〈[ r ], [ ]〉.
62definition lattice_hsingleton: Register → register_lattice ≝
63  λr.
64    〈[ ], [ r ]〉.
65
66definition lattice_join: register_lattice → register_lattice → register_lattice ≝
67  λleft.
68  λright.
69  let 〈lp, lh〉 ≝ left in
70  let 〈rp, rh〉 ≝ right in
71    〈list_set_union ? (eq_identifier ?) lp rp, list_set_union ? eq_Register lh rh〉.
72
73definition lattice_diff: register_lattice → register_lattice → register_lattice ≝
74  λleft.
75  λright.
76  let 〈lp, lh〉 ≝ left in
77  let 〈rp, rh〉 ≝ right in
78    〈list_set_diff ? (eq_identifier ?) lp rp, list_set_diff ? eq_Register lh rh〉.
79
80definition lattice_equal: register_lattice → register_lattice → bool ≝
81  λleft.
82  λright.
83  let 〈lp, lh〉 ≝ left in
84  let 〈rp, rh〉 ≝ right in
85    andb (list_set_equal ? (eq_identifier ?) lp rp) (list_set_equal ? eq_Register lh rh).
86
87definition lattice_is_maximal: register_lattice → bool ≝ λl. false.
88
89record lattice_property_sig: Type[1] ≝
90{
91  lp_type      : Type[0];
92  lp_property  : Type[0];
93  lp_bottom    : lp_type;
94  lp_psingleton: register → lp_type;
95  lp_hsingleton: Register → lp_type;
96  lp_join      : lp_type → lp_type → lp_type;
97  lp_diff      : lp_type → lp_type → lp_type;
98  lp_equal     : lp_type → lp_type → bool;
99  lp_is_maximal: lp_type → bool
100}.
101
102definition property ≝
103  mk_lattice_property_sig
104    ((list register) × (list Register))
105    lattice_property
106    lattice_bottom
107    lattice_psingleton
108    lattice_hsingleton
109    lattice_join
110    lattice_diff
111    lattice_equal
112    lattice_is_maximal.
113
114definition defined ≝
115  λglobals: list ident.
116  λs: ertl_statement globals.
117  match s with
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
158  ].
159
160definition list_set_of_list ≝
161  λrl.
162    foldr ? ? (list_set_add Register eq_Register) rl [ ].
163
164definition list_set_of_list2 ≝
165  let f ≝ λset. λr. list_set_add Register eq_Register r set in
166    foldl ? ? f [ ].
167
168definition ret_regs ≝ list_set_of_list RegisterRets.
169
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)
191    (* 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 ⇒
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.
221  let 〈pliveafter, hliveafter〉 ≝ l in
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.
306  λstmt.
307  λliveafter.
308  match eliminable globals liveafter stmt with
309  [ None ⇒ lattice_join (lattice_diff liveafter (defined globals stmt)) (used globals stmt)
310  | Some l ⇒ liveafter
311  ].
312
313definition valuation ≝ label → register_lattice.
314definition rhs ≝ valuation → lattice_property.
315definition equations ≝ label → rhs.
316
317axiom fix_lfp: equations → valuation.
318
319definition livebefore ≝
320  λglobals: list ident.
321  λint_fun.
322  λlabel.
323  λliveafter: valuation.
324  match lookup ? ? (ertl_if_graph globals int_fun) label with
325  [ None      ⇒ ?
326  | Some stmt ⇒ statement_semantics globals stmt (liveafter label)
327  ].
328  cases not_implemented (* XXX *)
329qed.
330
331definition liveafter ≝
332  λglobals.
333  λint_fun.
334  λlivebefore.
335  λlabel.
336  λliveafter: valuation.
337  match lookup … (ertl_if_graph globals int_fun) label with
338  [ None      ⇒ ?
339  | Some stmt ⇒ list_set_fold … (λsuccessor. λaccu: register_lattice.
340      lattice_join (livebefore successor liveafter) accu)
341      lattice_bottom (statement_successors globals stmt)
342  ].
343  cases not_implemented (* XXX *)
344qed.
345
346definition analyse ≝
347  λglobals.
348  λint_fun.
349    fix_lfp (liveafter globals int_fun (livebefore globals int_fun)).
Note: See TracBrowser for help on using the repository browser.