source: src/ERTL/liveness.ma @ 1151

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

added build.ma file. matita bug found

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