source: Deliverables/D3.3/id-lookup-branch/ERTL/liveness.ma @ 1109

Last change on this file since 1109 was 1109, checked in by campbell, 8 years ago

Update branch.

File size: 11.0 KB
Line 
1include "utilities/Fix.ma".
2include "ASM/Util.ma".
3include "ERTL/ERTL.ma".
4
5definition list_set_union ≝
6  λA: Type[0].
7  λeq_a: A → A → bool.
8  λl: list A.
9  λr: list A.
10    nub_by A eq_a (l @ r).
11
12definition list_set_add ≝
13  λA: Type[0].
14  λeq_a: A → A → bool.
15  λa: A.
16  λs: list A.
17    nub_by A eq_a (a :: s).
18
19definition list_set_diff ≝
20  λA: Type[0].
21  λeq_a: A → A → bool.
22  λl: list A.
23  λr: list A.
24    filter A (λx. member A eq_a x r) l.
25
26definition list_set_equal ≝
27  λA: Type[0].
28  λeq_a: A → A → bool.
29  λl: list A.
30  λr: list A.
31    foldr ? ? andb true (map ? ? (λx. member A eq_a x r) l).
32
33definition list_set_member ≝ member.
34
35definition list_set_fold ≝ foldr.
36
37definition statement_successors ≝
38  λs: ertl_statement.
39  match s with
40  [ ertl_st_return _ ⇒ [ ]
41  | ertl_st_skip l ⇒ [ l ]
42  | ertl_st_comment c l ⇒ [ l ]
43  | ertl_st_cost c l ⇒ [ l ]
44  | ertl_st_set_hdw _ _ l ⇒ [ l ]
45  | ertl_st_get_hdw _ _ l ⇒ [ l ]
46  | ertl_st_hdw_to_hdw _ _ l ⇒ [ l ]
47  | ertl_st_new_frame l ⇒ [ l ]
48  | ertl_st_del_frame l ⇒ [ l ]
49  | ertl_st_frame_size _ l ⇒ [ l ]
50  | ertl_st_push _ l ⇒ [ l ]
51  | ertl_st_pop _ l ⇒ [ l ]
52  | ertl_st_addr_h _ _ l ⇒ [ l ]
53  | ertl_st_addr_l _ _ l ⇒ [ l ]
54  | ertl_st_int _ _ l ⇒ [ l ]
55  | ertl_st_move _ _ l ⇒ [ l ]
56  | ertl_st_opaccs_a _ _ _ _ l ⇒ [ l ]
57  | ertl_st_opaccs_b _ _ _ _ l ⇒ [ l ]
58  | ertl_st_op1 _ _ _ l ⇒ [ l ]
59  | ertl_st_op2 _ _ _ _ l ⇒ [ l ]
60  | ertl_st_clear_carry l ⇒ [ l ]
61  | ertl_st_set_carry l ⇒ [ l ]
62  | ertl_st_load _ _ _ l ⇒ [ l ]
63  | ertl_st_store _ _ _ l ⇒ [ l ]
64  | ertl_st_call_id _ _ l ⇒ [ l ]
65  | ertl_st_cond _ l1 l2 ⇒
66      list_set_add ? (eq_identifier ?) l1 [ l2 ]
67  ].
68
69definition register_lattice ≝ (list register) × (list Register).
70definition lattice_property ≝ register_lattice.
71definition lattice_bottom: register_lattice ≝ 〈[ ], [ ]〉.
72definition lattice_psingleton: register → register_lattice ≝
73  λr.
74    〈[ r ], [ ]〉.
75definition lattice_hsingleton: Register → register_lattice ≝
76  λr.
77    〈[ ], [ r ]〉.
78
79definition lattice_join: register_lattice → register_lattice → register_lattice ≝
80  λleft.
81  λright.
82  let 〈lp, lh〉 ≝ left in
83  let 〈rp, rh〉 ≝ right in
84    〈list_set_union ? (eq_identifier ?) lp rp, list_set_union ? eq_Register lh rh〉.
85
86definition lattice_diff: register_lattice → register_lattice → register_lattice ≝
87  λleft.
88  λright.
89  let 〈lp, lh〉 ≝ left in
90  let 〈rp, rh〉 ≝ right in
91    〈list_set_diff ? (eq_identifier ?) lp rp, list_set_diff ? eq_Register lh rh〉.
92
93definition lattice_equal: register_lattice → register_lattice → bool ≝
94  λleft.
95  λright.
96  let 〈lp, lh〉 ≝ left in
97  let 〈rp, rh〉 ≝ right in
98    andb (list_set_equal ? (eq_identifier ?) lp rp) (list_set_equal ? eq_Register lh rh).
99
100definition lattice_is_maximal: register_lattice → bool ≝ λl. false.
101
102definition defined: ertl_statement → register_lattice ≝
103  λs.
104  match s with
105  [ ertl_st_skip _ ⇒ lattice_bottom
106  | ertl_st_comment _ _ ⇒ lattice_bottom
107  | ertl_st_cost _ _ ⇒ lattice_bottom
108  | ertl_st_push _ _⇒ lattice_bottom
109  | ertl_st_store _ _ _ _ ⇒ lattice_bottom
110  | ertl_st_cond _ _ _ ⇒ lattice_bottom
111  | ertl_st_return _ ⇒ lattice_bottom
112  | ertl_st_clear_carry _ ⇒ lattice_hsingleton RegisterCarry
113  | ertl_st_set_carry _ ⇒ lattice_hsingleton RegisterCarry
114  | ertl_st_op2 op2 r _ _ _ ⇒
115    match op2 with
116    [ Add ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r)
117    | Addc ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r)
118    | Sub ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r)
119    | _ ⇒ lattice_psingleton r
120    ]
121  | ertl_st_op1 op1 r _ _ ⇒ lattice_psingleton r
122  | ertl_st_get_hdw r _ _ ⇒ lattice_psingleton r
123  | ertl_st_frame_size r _ ⇒ lattice_psingleton r
124  | ertl_st_pop r _ ⇒ lattice_psingleton r
125  | ertl_st_int r _ _ ⇒ lattice_psingleton r
126  | ertl_st_addr_h r _ _ ⇒ lattice_psingleton r
127  | ertl_st_addr_l r _ _ ⇒ lattice_psingleton r
128  | ertl_st_move r _ _ ⇒ lattice_psingleton r
129  | ertl_st_opaccs_a _ r _ _ _ ⇒ lattice_psingleton r
130  | ertl_st_opaccs_b _ r _ _ _ ⇒ lattice_psingleton r
131  | ertl_st_load r _ _ _ ⇒ lattice_psingleton r
132  | ertl_st_set_hdw r _ _ ⇒ lattice_hsingleton r
133  | ertl_st_hdw_to_hdw r _ _ ⇒ lattice_hsingleton r
134  (* Potentially destroys all caller-save hardware registers. *)
135  | ertl_st_call_id _ _ _ ⇒ 〈[ ], RegisterCallerSaved〉
136  | ertl_st_new_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
137  | ertl_st_del_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
138  ].
139
140definition list_set_of_list ≝
141  λrl.
142    foldr ? ? (list_set_add Register eq_Register) rl [ ].
143
144definition list_set_of_list2 ≝
145  let f ≝ λset. λr. list_set_add Register eq_Register r set in
146    foldl ? ? f [ ].
147
148definition ret_regs ≝ list_set_of_list RegisterRets.
149
150definition used: ertl_statement → register_lattice ≝
151  λstmt.
152  match stmt with
153  [ ertl_st_skip _ ⇒ lattice_bottom
154  | ertl_st_cost _ _ ⇒ lattice_bottom
155  | ertl_st_comment _ _ ⇒ lattice_bottom
156  | ertl_st_frame_size _ _ ⇒ lattice_bottom
157  | ertl_st_pop _ _ ⇒ lattice_bottom
158  | ertl_st_addr_h _ _ _ ⇒ lattice_bottom
159  | ertl_st_addr_l _ _ _ ⇒ lattice_bottom
160  | ertl_st_int _ _ _ ⇒ lattice_bottom
161  | ertl_st_clear_carry _ ⇒ lattice_bottom
162  | ertl_st_set_carry _ ⇒ lattice_bottom
163    (* Reads the hardware registers that are used to pass parameters. *)
164  | ertl_st_call_id _ nparams _ ⇒
165    〈[ ], list_set_of_list (prefix ? (nat_of_bitvector ? nparams) RegisterParameters)〉
166  | ertl_st_get_hdw _ r _ ⇒ lattice_hsingleton r
167  | ertl_st_hdw_to_hdw _ r _ ⇒ lattice_hsingleton r
168  | ertl_st_set_hdw _ r _ ⇒ lattice_psingleton r
169  | ertl_st_push r _ ⇒ lattice_psingleton r
170  | ertl_st_move _ r _ ⇒ lattice_psingleton r
171  | ertl_st_op1 _ _ r _ ⇒ lattice_psingleton r
172  | ertl_st_cond r _ _ ⇒ lattice_psingleton r
173  | ertl_st_op2 op2 _ r1 r2 _ ⇒
174    match op2 with
175    [ Addc ⇒
176      lattice_join (lattice_join (lattice_psingleton r1) (lattice_psingleton r2)) (lattice_hsingleton RegisterCarry)
177    | _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
178    ]
179  | ertl_st_opaccs_a _ _ r1 r2 _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
180  | ertl_st_opaccs_b _ _ r1 r2 _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
181  | ertl_st_load _ r1 r2 _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
182  | ertl_st_store r1 r2 r3 _ ⇒
183    lattice_join (lattice_join (lattice_psingleton r1) (lattice_psingleton r2)) (lattice_psingleton r3)
184  | ertl_st_new_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
185  | ertl_st_del_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
186  | ertl_st_return _ ⇒ 〈[ ], list_set_union ? eq_Register RegisterCalleeSaved ret_regs〉
187  ].
188
189definition eliminable: register_lattice → ertl_statement → option label ≝
190  λl.
191  λstmt.
192  let 〈pliveafter, hliveafter〉 ≝ l in
193  match stmt with
194  [ ertl_st_skip _ ⇒ None ?
195  | ertl_st_comment _ _ ⇒ None ?
196  | ertl_st_cost _ _ ⇒ None ?
197  | ertl_st_new_frame _ ⇒ None ?
198  | ertl_st_del_frame _ ⇒ None ?
199  | ertl_st_pop _ _ ⇒ None ?
200  | ertl_st_push _ _ ⇒ None ?
201  | ertl_st_clear_carry _  ⇒ None ?
202  | ertl_st_set_carry _  ⇒ None ?
203  | ertl_st_store _ _ _ _ ⇒ None ?
204  | ertl_st_call_id _ _ _ ⇒ None ?
205  | ertl_st_cond _ _ _ ⇒ None ?
206  | ertl_st_return _ ⇒ None ?
207  | ertl_st_get_hdw r _ l ⇒
208    if list_set_member register (eq_identifier ?) r pliveafter ∨
209       list_set_member Register eq_Register RegisterCarry hliveafter then
210      None ?
211    else
212      Some ? l
213  | ertl_st_frame_size r l ⇒
214    if list_set_member register (eq_identifier ?) r pliveafter ∨
215       list_set_member Register eq_Register RegisterCarry hliveafter then
216      None ?
217    else
218      Some ? l
219  | ertl_st_int r _ l ⇒
220    if list_set_member register (eq_identifier ?) r pliveafter ∨
221       list_set_member Register eq_Register RegisterCarry hliveafter then
222      None ?
223    else
224      Some ? l
225  | ertl_st_addr_h r _ l ⇒
226    if list_set_member register (eq_identifier ?) r pliveafter ∨
227       list_set_member Register eq_Register RegisterCarry hliveafter then
228      None ?
229    else
230      Some ? l
231  | ertl_st_addr_l 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_move 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_opaccs_a _ 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_opaccs_b _ 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_op1 _ 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_op2 _ 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_load 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_set_hdw r _ l ⇒
274    if list_set_member Register eq_Register r hliveafter then
275      None ?
276    else
277      Some ? l
278  | ertl_st_hdw_to_hdw r _ l ⇒
279    if list_set_member Register eq_Register r hliveafter then
280      None ?
281    else
282      Some ? l
283  ].
284
285definition statement_semantics: ertl_statement → register_lattice → register_lattice ≝
286  λstmt.
287  λliveafter.
288  match eliminable liveafter stmt with
289  [ None ⇒ lattice_join (lattice_diff liveafter (defined stmt)) (used stmt)
290  | Some l ⇒ liveafter
291  ].
292
293definition valuation ≝ label → register_lattice.
294
295definition analyse: ertl_internal_function → valuation ≝
296  λint_fun.
297  let livebefore ≝ λlabel. λliveafter: valuation.
298    match lookup ? ? (ertl_if_graph int_fun) label with
299    [ None      ⇒ ?
300    | Some stmt ⇒ statement_semantics stmt (liveafter label)
301    ]
302  in
303  let liveafter ≝ λlabel. λliveafter: valuation.
304    match lookup ? ? (ertl_if_graph int_fun) label with
305    [ None      ⇒ ?
306    | Some stmt ⇒ list_set_fold ? ? (λsuccessor. λaccu.
307        lattice_join (livebefore successor liveafter) accu)
308        lattice_bottom (statement_successors stmt)
309    ]
310  in ?.
Note: See TracBrowser for help on using the repository browser.