source: src/ERTL/liveness.ma @ 1730

Last change on this file since 1730 was 1730, checked in by sacerdot, 8 years ago

Minor changes while studying the proof.

File size: 10.6 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  [ sequential seq l ⇒
10    match seq with
11    [ COND acc_a_reg lbl_true ⇒
12        set_insert … lbl_true (set_singleton … l)
13    | _ ⇒ set_singleton … l ]
14  | GOTO l ⇒ set_singleton … l
15  | 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  [ sequential seq l ⇒
81    match seq with
82    [ 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    | CLEAR_CARRY ⇒ lattice_hsingleton RegisterCarry
90    | SET_CARRY ⇒ lattice_hsingleton RegisterCarry
91    | OPACCS opaccs dr1 dr2 sr1 sr2 ⇒
92       lattice_join (lattice_psingleton dr1) (lattice_psingleton dr2)
93    | OP1 op1 r1 r2 ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
94    | POP r ⇒ lattice_psingleton r
95    | INT r _ ⇒ lattice_psingleton r
96    | ADDRESS _ _ r1 r2 ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
97    | LOAD r _ _ ⇒ lattice_psingleton r
98    (* Potentially destroys all caller-save hardware registers. *)
99    | CALL_ID id _ _ ⇒ 〈set_empty …, set_from_list … RegisterCallerSaved〉
100    | COMMENT c ⇒ lattice_bottom
101    | COND r lbl_true ⇒ lattice_bottom
102    | STORE acc_a dpl dph ⇒ lattice_bottom
103    | COST_LABEL clabel ⇒ lattice_bottom
104    | PUSH r ⇒ lattice_bottom
105    | MOVE pair_reg ⇒
106      (* first register relevant only *)
107      let r1 ≝ \fst pair_reg in
108      match r1 with
109      [ pseudo p ⇒ lattice_psingleton p
110      | hardware h ⇒ lattice_hsingleton h
111      ]
112    | extension ext ⇒
113      match ext with
114      [ ertl_st_ext_new_frame ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
115      | ertl_st_ext_del_frame ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
116      | ertl_st_ext_frame_size r ⇒ lattice_psingleton r]]
117  | RETURN ⇒ lattice_bottom
118  | GOTO l ⇒ lattice_bottom
119  ].
120
121definition ret_regs ≝ set_from_list … RegisterRets.
122
123definition used ≝
124  λglobals: list ident.
125  λs: ertl_statement globals.
126  match s with
127  [ sequential seq l ⇒
128    match seq with
129    [ OP2 op2 acc_a r1 r2 ⇒
130      match op2 with
131      [ Addc ⇒
132        lattice_join (lattice_join (lattice_psingleton r1) (lattice_psingleton r2)) (lattice_hsingleton RegisterCarry)
133      | _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
134      ]
135    | CLEAR_CARRY ⇒ lattice_bottom
136    | SET_CARRY ⇒ lattice_bottom
137    (* acc_a and acc_b *)
138    | OPACCS opaccs dr1 dr2 sr1 sr2 ⇒
139       lattice_join (lattice_psingleton sr1) (lattice_psingleton sr2)
140    | OP1 op1 r1 r2 ⇒ lattice_psingleton r2
141    | POP r ⇒ lattice_bottom
142    | INT r _ ⇒ lattice_bottom
143    | ADDRESS _ _ r1 r2 ⇒ lattice_bottom
144    | LOAD acc_a dpl dph ⇒ lattice_join (lattice_psingleton dpl) (lattice_psingleton dph)
145    (* Reads the hardware registers that are used to pass parameters. *)
146    | CALL_ID _ nparams _ ⇒ 〈set_empty …, set_from_list … (prefix ? nparams RegisterParams)〉
147    | COMMENT c ⇒ lattice_bottom
148    | COND r lbl_true ⇒ lattice_psingleton r
149    | STORE acc_a dpl dph ⇒
150      lattice_join (lattice_join (lattice_psingleton acc_a) (lattice_psingleton dpl)) (lattice_psingleton dph)
151    | COST_LABEL clabel ⇒ lattice_bottom
152    | PUSH r ⇒ lattice_psingleton r
153    | MOVE pair_reg ⇒
154      let r2 ≝ \snd pair_reg in
155      match r2 with
156      [ pseudo p ⇒ lattice_psingleton p
157      | hardware h ⇒ lattice_hsingleton h
158      ]
159  | extension ext ⇒
160    match ext with
161    [ ertl_st_ext_new_frame ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
162    | ertl_st_ext_del_frame ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
163    | ertl_st_ext_frame_size r ⇒ lattice_bottom]]
164  | RETURN ⇒ 〈set_empty …, set_union … (set_from_list … RegisterCalleeSaved) ret_regs〉
165  | GOTO l ⇒ lattice_bottom
166  ].
167
168definition eliminable ≝
169  λglobals: list ident.
170  λl: register_lattice.
171  λs: ertl_statement globals.
172  let 〈pliveafter, hliveafter〉 ≝ l in
173  match s with
174  [ sequential seq l ⇒
175    match seq with
176    [ OP2 op2 r1 r2 r3 ⇒
177      if set_member … (eq_identifier …) r1 pliveafter ∨
178         set_member … eq_Register RegisterCarry hliveafter then
179        None ?
180      else
181        Some ? l
182    | CLEAR_CARRY ⇒ None ?
183    | SET_CARRY ⇒ None ?
184    | OPACCS opaccs dr1 dr2 sr1 sr2 ⇒
185      if set_member … (eq_identifier …) dr1 pliveafter ∨
186         set_member … (eq_identifier …) dr2 pliveafter ∨
187         set_member … eq_Register RegisterCarry hliveafter then
188        None ?
189      else
190        Some ? l
191    | OP1 op1 r1 r2 ⇒
192      if set_member … (eq_identifier …) r1 pliveafter ∨
193         set_member … eq_Register RegisterCarry hliveafter then
194        None ?
195      else
196        Some ? l
197    | POP r ⇒ None ?
198    | INT r _ ⇒
199      if set_member … (eq_identifier …) r pliveafter ∨
200         set_member … eq_Register RegisterCarry hliveafter then
201        None ?
202      else
203        Some ? l
204    | ADDRESS _ _ r1 r2 ⇒
205      if set_member … (eq_identifier …) r1 pliveafter ∨
206         set_member … (eq_identifier …) r2 pliveafter ∨
207         set_member … eq_Register RegisterCarry hliveafter then
208        None ?
209      else
210        Some ? l
211    | LOAD acc_a dpl dph ⇒
212      if set_member ? (eq_identifier …) acc_a pliveafter ∨
213         set_member … eq_Register RegisterCarry hliveafter then
214        None ?
215      else
216        Some ? l
217    | CALL_ID _ nparams _ ⇒ None ?
218    | COMMENT c ⇒ None ?
219    | COND r lbl_true ⇒ None ?
220    | STORE acc_a dpl dph ⇒ None ?
221    | COST_LABEL clabel ⇒ None ?
222    | PUSH r ⇒ None ?
223    | MOVE pair_reg ⇒
224      let r1 ≝ \fst pair_reg in
225      let r2 ≝ \snd pair_reg in
226      match r1 with
227      [ pseudo p1 ⇒
228        if set_member … (eq_identifier …) p1 pliveafter ∨
229           set_member … eq_Register RegisterCarry hliveafter then
230          None ?
231        else
232          Some ? l
233      | hardware h1 ⇒
234        if set_member … eq_Register h1 hliveafter then
235          None ?
236        else
237          Some ? l]
238    | extension ext ⇒
239      match ext with
240      [ ertl_st_ext_new_frame ⇒ None ?
241      | ertl_st_ext_del_frame ⇒ None ?
242      | ertl_st_ext_frame_size r ⇒
243        if set_member ? (eq_identifier RegisterTag) r pliveafter ∨
244           set_member ? eq_Register RegisterCarry hliveafter then
245          None ?
246        else
247          Some ? l]]
248  | GOTO l ⇒ None ?
249  | RETURN ⇒ None ?
250  ].
251
252definition statement_semantics: ∀globals: list ident. ertl_statement globals → register_lattice → register_lattice ≝
253  λglobals.
254  λstmt.
255  λliveafter.
256  match eliminable globals liveafter stmt with
257  [ None ⇒ lattice_join (lattice_diff liveafter (defined globals stmt)) (used globals stmt)
258  | Some l ⇒ liveafter
259  ].
260
261definition valuation ≝ label → register_lattice.
262definition rhs ≝ valuation → lattice_property.
263definition equations ≝ label → rhs.
264
265definition livebefore ≝
266  λglobals: list ident.
267  λint_fun: ertl_internal_function globals.
268  λlabel.
269  λliveafter: valuation.
270  match lookup … (joint_if_code … int_fun) label with
271  [ None      ⇒ ?
272  | Some stmt ⇒ statement_semantics globals stmt (liveafter label)
273  ].
274  cases not_implemented (* XXX *)
275qed.
276
277definition liveafter ≝
278  λglobals: list ident.
279  λint_fun: ertl_internal_function globals.
280  λlabel.
281  λliveafter: valuation.
282  match lookup … (joint_if_code … int_fun) label with
283  [ None      ⇒ ?
284  | Some stmt ⇒ set_fold ? ? (λsuccessor. λaccu: register_lattice.
285      lattice_join (livebefore globals int_fun successor liveafter) accu)
286      (statement_successors globals stmt) lattice_bottom
287  ].
288  cases not_implemented (* XXX *)
289qed.
290
291record fixpoint: Type[0] ≝
292{
293  (* XXX: this never fails to compute a fixed point as in any program we will
294          only ever use a finite number of pseudoregisters, therefore no chain
295          conditions, etc. are necessary for this to terminate with a correct
296          solution. *)
297  fix_lfp    :1> equations → valuation;
298  fix_correct:
299    ∀globals: list ident.
300    ∀int_fun.
301    ∀f. (* CSC: was let f ≝ liveafter globals int_fun in *)
302      ∀v: label.
303        lattice_equal (f v (fix_lfp f)) (fix_lfp f v) (*CSC: TOO STRONG: WE ONLY NEED CORRECTNESS NOT COMPLETENESS *)
304}.
305
306axiom the_fixpoint: fixpoint.
307
308definition analyse ≝
309  λglobals.
310  λint_fun.
311    the_fixpoint (liveafter globals int_fun).
Note: See TracBrowser for help on using the repository browser.