source: src/ERTL/liveness.ma @ 1271

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

finished, kind of

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