source: src/ERTL/liveness.ma @ 1136

Last change on this file since 1136 was 1124, checked in by mulligan, 8 years ago

finished off liveness analysis by axiomatising properties

File size: 11.8 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  λs: ertl_statement.
38  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_h _ _ l ⇒ [ l ]
52  | ertl_st_addr_l _ _ l ⇒ [ l ]
53  | ertl_st_int _ _ l ⇒ [ l ]
54  | ertl_st_move _ _ l ⇒ [ l ]
55  | ertl_st_opaccs_a _ _ _ _ l ⇒ [ l ]
56  | ertl_st_opaccs_b _ _ _ _ l ⇒ [ l ]
57  | ertl_st_op1 _ _ _ l ⇒ [ l ]
58  | ertl_st_op2 _ _ _ _ l ⇒ [ l ]
59  | ertl_st_clear_carry l ⇒ [ l ]
60  | ertl_st_set_carry l ⇒ [ l ]
61  | ertl_st_load _ _ _ l ⇒ [ l ]
62  | ertl_st_store _ _ _ l ⇒ [ l ]
63  | ertl_st_call_id _ _ l ⇒ [ l ]
64  | ertl_st_cond _ l1 l2 ⇒
65      list_set_add ? (eq_identifier ?) l1 [ l2 ]
66  ].
67
68definition register_lattice ≝ (list register) × (list Register).
69definition lattice_property ≝ register_lattice.
70definition lattice_bottom: register_lattice ≝ 〈[ ], [ ]〉.
71definition lattice_psingleton: register → register_lattice ≝
72  λr.
73    〈[ r ], [ ]〉.
74definition lattice_hsingleton: Register → register_lattice ≝
75  λr.
76    〈[ ], [ r ]〉.
77
78definition lattice_join: register_lattice → register_lattice → register_lattice ≝
79  λleft.
80  λright.
81  let 〈lp, lh〉 ≝ left in
82  let 〈rp, rh〉 ≝ right in
83    〈list_set_union ? (eq_identifier ?) lp rp, list_set_union ? eq_Register lh rh〉.
84
85definition lattice_diff: register_lattice → register_lattice → register_lattice ≝
86  λleft.
87  λright.
88  let 〈lp, lh〉 ≝ left in
89  let 〈rp, rh〉 ≝ right in
90    〈list_set_diff ? (eq_identifier ?) lp rp, list_set_diff ? eq_Register lh rh〉.
91
92definition lattice_equal: register_lattice → register_lattice → bool ≝
93  λleft.
94  λright.
95  let 〈lp, lh〉 ≝ left in
96  let 〈rp, rh〉 ≝ right in
97    andb (list_set_equal ? (eq_identifier ?) lp rp) (list_set_equal ? eq_Register lh rh).
98
99definition lattice_is_maximal: register_lattice → bool ≝ λl. false.
100
101record lattice_property_sig: Type[1] ≝
102{
103  lp_type      : Type[0];
104  lp_property  : Type[0];
105  lp_bottom    : lp_type;
106  lp_psingleton: register → lp_type;
107  lp_hsingleton: Register → lp_type;
108  lp_join      : lp_type → lp_type → lp_type;
109  lp_diff      : lp_type → lp_type → lp_type;
110  lp_equal     : lp_type → lp_type → bool;
111  lp_is_maximal: lp_type → bool
112}.
113
114definition property ≝
115  mk_lattice_property_sig
116    ((list register) × (list Register))
117    lattice_property
118    lattice_bottom
119    lattice_psingleton
120    lattice_hsingleton
121    lattice_join
122    lattice_diff
123    lattice_equal
124    lattice_is_maximal.
125
126definition defined: ertl_statement → register_lattice ≝
127  λs.
128  match s with
129  [ ertl_st_skip _ ⇒ lattice_bottom
130  | ertl_st_comment _ _ ⇒ lattice_bottom
131  | ertl_st_cost _ _ ⇒ lattice_bottom
132  | ertl_st_push _ _⇒ lattice_bottom
133  | ertl_st_store _ _ _ _ ⇒ lattice_bottom
134  | ertl_st_cond _ _ _ ⇒ lattice_bottom
135  | ertl_st_return ⇒ lattice_bottom
136  | ertl_st_clear_carry _ ⇒ lattice_hsingleton RegisterCarry
137  | ertl_st_set_carry _ ⇒ lattice_hsingleton RegisterCarry
138  | ertl_st_op2 op2 r _ _ _ ⇒
139    match op2 with
140    [ Add ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r)
141    | Addc ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r)
142    | Sub ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r)
143    | _ ⇒ lattice_psingleton r
144    ]
145  | ertl_st_op1 op1 r _ _ ⇒ lattice_psingleton r
146  | ertl_st_get_hdw r _ _ ⇒ lattice_psingleton r
147  | ertl_st_frame_size r _ ⇒ lattice_psingleton r
148  | ertl_st_pop r _ ⇒ lattice_psingleton r
149  | ertl_st_int r _ _ ⇒ lattice_psingleton r
150  | ertl_st_addr_h r _ _ ⇒ lattice_psingleton r
151  | ertl_st_addr_l r _ _ ⇒ lattice_psingleton r
152  | ertl_st_move r _ _ ⇒ lattice_psingleton r
153  | ertl_st_opaccs_a _ r _ _ _ ⇒ lattice_psingleton r
154  | ertl_st_opaccs_b _ r _ _ _ ⇒ lattice_psingleton r
155  | ertl_st_load r _ _ _ ⇒ lattice_psingleton r
156  | ertl_st_set_hdw r _ _ ⇒ lattice_hsingleton r
157  | ertl_st_hdw_to_hdw r _ _ ⇒ lattice_hsingleton r
158  (* Potentially destroys all caller-save hardware registers. *)
159  | ertl_st_call_id _ _ _ ⇒ 〈[ ], RegisterCallerSaved〉
160  | ertl_st_new_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
161  | ertl_st_del_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
162  ].
163
164definition list_set_of_list ≝
165  λrl.
166    foldr ? ? (list_set_add Register eq_Register) rl [ ].
167
168definition list_set_of_list2 ≝
169  let f ≝ λset. λr. list_set_add Register eq_Register r set in
170    foldl ? ? f [ ].
171
172definition ret_regs ≝ list_set_of_list RegisterRets.
173
174definition used: ertl_statement → register_lattice ≝
175  λstmt.
176  match stmt with
177  [ ertl_st_skip _ ⇒ lattice_bottom
178  | ertl_st_cost _ _ ⇒ lattice_bottom
179  | ertl_st_comment _ _ ⇒ lattice_bottom
180  | ertl_st_frame_size _ _ ⇒ lattice_bottom
181  | ertl_st_pop _ _ ⇒ lattice_bottom
182  | ertl_st_addr_h _ _ _ ⇒ lattice_bottom
183  | ertl_st_addr_l _ _ _ ⇒ lattice_bottom
184  | ertl_st_int _ _ _ ⇒ lattice_bottom
185  | ertl_st_clear_carry _ ⇒ lattice_bottom
186  | ertl_st_set_carry _ ⇒ lattice_bottom
187    (* Reads the hardware registers that are used to pass parameters. *)
188  | ertl_st_call_id _ nparams _ ⇒
189    〈[ ], list_set_of_list (prefix ? (nat_of_bitvector ? nparams) RegisterParameters)〉
190  | ertl_st_get_hdw _ r _ ⇒ lattice_hsingleton r
191  | ertl_st_hdw_to_hdw _ r _ ⇒ lattice_hsingleton r
192  | ertl_st_set_hdw _ r _ ⇒ lattice_psingleton r
193  | ertl_st_push r _ ⇒ lattice_psingleton r
194  | ertl_st_move _ r _ ⇒ lattice_psingleton r
195  | ertl_st_op1 _ _ r _ ⇒ lattice_psingleton r
196  | ertl_st_cond r _ _ ⇒ lattice_psingleton r
197  | ertl_st_op2 op2 _ r1 r2 _ ⇒
198    match op2 with
199    [ Addc ⇒
200      lattice_join (lattice_join (lattice_psingleton r1) (lattice_psingleton r2)) (lattice_hsingleton RegisterCarry)
201    | _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
202    ]
203  | ertl_st_opaccs_a _ _ r1 r2 _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
204  | ertl_st_opaccs_b _ _ r1 r2 _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
205  | ertl_st_load _ r1 r2 _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
206  | ertl_st_store r1 r2 r3 _ ⇒
207    lattice_join (lattice_join (lattice_psingleton r1) (lattice_psingleton r2)) (lattice_psingleton r3)
208  | ertl_st_new_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
209  | ertl_st_del_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
210  | ertl_st_return ⇒ 〈[ ], list_set_union ? eq_Register RegisterCalleeSaved ret_regs〉
211  ].
212
213definition eliminable: register_lattice → ertl_statement → option label ≝
214  λl.
215  λstmt.
216  let 〈pliveafter, hliveafter〉 ≝ l in
217  match stmt with
218  [ ertl_st_skip _ ⇒ None ?
219  | ertl_st_comment _ _ ⇒ None ?
220  | ertl_st_cost _ _ ⇒ None ?
221  | ertl_st_new_frame _ ⇒ None ?
222  | ertl_st_del_frame _ ⇒ None ?
223  | ertl_st_pop _ _ ⇒ None ?
224  | ertl_st_push _ _ ⇒ None ?
225  | ertl_st_clear_carry _  ⇒ None ?
226  | ertl_st_set_carry _  ⇒ None ?
227  | ertl_st_store _ _ _ _ ⇒ None ?
228  | ertl_st_call_id _ _ _ ⇒ None ?
229  | ertl_st_cond _ _ _ ⇒ None ?
230  | ertl_st_return ⇒ None ?
231  | ertl_st_get_hdw r _ l ⇒
232    if list_set_member register (eq_identifier ?) r pliveafter ∨
233       list_set_member Register eq_Register RegisterCarry hliveafter then
234      None ?
235    else
236      Some ? l
237  | ertl_st_frame_size r l ⇒
238    if list_set_member register (eq_identifier ?) r pliveafter ∨
239       list_set_member Register eq_Register RegisterCarry hliveafter then
240      None ?
241    else
242      Some ? l
243  | ertl_st_int r _ l ⇒
244    if list_set_member register (eq_identifier ?) r pliveafter ∨
245       list_set_member Register eq_Register RegisterCarry hliveafter then
246      None ?
247    else
248      Some ? l
249  | ertl_st_addr_h r _ l ⇒
250    if list_set_member register (eq_identifier ?) r pliveafter ∨
251       list_set_member Register eq_Register RegisterCarry hliveafter then
252      None ?
253    else
254      Some ? l
255  | ertl_st_addr_l r _ l ⇒
256    if list_set_member register (eq_identifier ?) r pliveafter ∨
257       list_set_member Register eq_Register RegisterCarry hliveafter then
258      None ?
259    else
260      Some ? l
261  | ertl_st_move r _ l ⇒
262    if list_set_member register (eq_identifier ?) r pliveafter ∨
263       list_set_member Register eq_Register RegisterCarry hliveafter then
264      None ?
265    else
266      Some ? l
267  | ertl_st_opaccs_a _ r _ _ l ⇒
268    if list_set_member register (eq_identifier ?) r pliveafter ∨
269       list_set_member Register eq_Register RegisterCarry hliveafter then
270      None ?
271    else
272      Some ? l
273  | ertl_st_opaccs_b _ r _ _ l ⇒
274    if list_set_member register (eq_identifier ?) r pliveafter ∨
275       list_set_member Register eq_Register RegisterCarry hliveafter then
276      None ?
277    else
278      Some ? l
279  | ertl_st_op1 _ r _ l ⇒
280    if list_set_member register (eq_identifier ?) r pliveafter ∨
281       list_set_member Register eq_Register RegisterCarry hliveafter then
282      None ?
283    else
284      Some ? l
285  | ertl_st_op2 _ r _ _ l ⇒
286    if list_set_member register (eq_identifier ?) r pliveafter ∨
287       list_set_member Register eq_Register RegisterCarry hliveafter then
288      None ?
289    else
290      Some ? l
291  | ertl_st_load r _ _ l ⇒
292    if list_set_member register (eq_identifier ?) r pliveafter ∨
293       list_set_member Register eq_Register RegisterCarry hliveafter then
294      None ?
295    else
296      Some ? l
297  | ertl_st_set_hdw r _ l ⇒
298    if list_set_member Register eq_Register r hliveafter then
299      None ?
300    else
301      Some ? l
302  | ertl_st_hdw_to_hdw r _ l ⇒
303    if list_set_member Register eq_Register r hliveafter then
304      None ?
305    else
306      Some ? l
307  ].
308
309definition statement_semantics: ertl_statement → register_lattice → register_lattice ≝
310  λstmt.
311  λliveafter.
312  match eliminable liveafter stmt with
313  [ None ⇒ lattice_join (lattice_diff liveafter (defined stmt)) (used stmt)
314  | Some l ⇒ liveafter
315  ].
316
317definition valuation ≝ label → register_lattice.
318definition rhs ≝ valuation → lattice_property.
319definition equations ≝ label → rhs.
320
321axiom fix_lfp: equations → valuation.
322
323definition livebefore ≝
324  λint_fun.
325  λlabel.
326  λliveafter: valuation.
327  match lookup ? ? (ertl_if_graph int_fun) label with
328  [ None      ⇒ ?
329  | Some stmt ⇒ statement_semantics stmt (liveafter label)
330  ].
331  cases not_implemented (* XXX *)
332qed.
333
334definition liveafter ≝
335  λint_fun.
336  λlivebefore.
337  λlabel.
338  λliveafter: valuation.
339  match lookup ? ? (ertl_if_graph int_fun) label with
340  [ None      ⇒ ?
341  | Some stmt ⇒ list_set_fold ? ? (λsuccessor. λaccu.
342      lattice_join (livebefore successor liveafter) accu)
343      lattice_bottom (statement_successors stmt)
344  ].
345  cases not_implemented (* XXX *)
346qed.
347
348definition analyse: ertl_internal_function → valuation ≝
349  λint_fun.
350    fix_lfp (liveafter int_fun (livebefore int_fun)).
Note: See TracBrowser for help on using the repository browser.