source: src/ERTL/liveness.ma @ 2689

Last change on this file since 2689 was 2689, checked in by tranquil, 7 years ago
  • fixed passes up to linearisation
File size: 8.8 KB
Line 
1
2include "ASM/Util.ma".
3include "ERTL/ERTL.ma".
4include "utilities/adt/set_adt.ma".
5include "utilities/fixpoints.ma".
6
7definition register_lattice : property_lattice ≝
8mk_property_lattice
9 ((set register) × (set Register))
10 〈set_empty …, set_empty …〉
11 (λleft.
12  λright.
13  set_equal … (eq_identifier ?) (\fst left) (\fst right) ∧
14  set_equal … eq_Register (\snd left) (\snd right))
15 (λleft.
16  λright.
17  set_subset … (eq_identifier ?) (\fst left) (\fst right) ∧
18  set_subset … eq_Register (\snd left) (\snd right))
19 (λ_.false).
20
21definition rl_bottom ≝ l_bottom register_lattice.
22definition rl_psingleton: register → register_lattice ≝
23  λr.
24    〈set_singleton … r, set_empty …〉.
25definition rl_hsingleton: Register → register_lattice ≝
26  λr.
27    〈set_empty …, set_singleton … r〉.
28
29definition rl_join: register_lattice → register_lattice → register_lattice ≝
30  λleft.
31  λright.
32  let 〈lp, lh〉 ≝ left in
33  let 〈rp, rh〉 ≝ right in
34    〈set_union … lp rp, set_union … lh rh〉.
35
36definition rl_diff: register_lattice → register_lattice → register_lattice ≝
37  λleft.
38  λright.
39  let 〈lp, lh〉 ≝ left in
40  let 〈rp, rh〉 ≝ right in
41    〈set_diff … lp rp, set_diff … lh rh〉.
42
43definition defined ≝
44  λglobals: list ident.
45  λs: joint_statement ERTL globals.
46  match s with
47  [ sequential seq l ⇒
48    match seq with
49    [ step_seq s ⇒
50      match s with
51      [ OP2 op2 r1 r2 _ ⇒
52        match op2 with
53        [ Add ⇒ rl_join (rl_hsingleton RegisterCarry) (rl_psingleton r1)
54        | Addc ⇒ rl_join (rl_hsingleton RegisterCarry) (rl_psingleton r1)
55        | Sub ⇒ rl_join (rl_hsingleton RegisterCarry)  (rl_psingleton r1)
56        | _ ⇒ rl_psingleton r1
57        ]
58      | CLEAR_CARRY ⇒ rl_hsingleton RegisterCarry
59      | SET_CARRY ⇒ rl_hsingleton RegisterCarry
60      | OPACCS opaccs dr1 dr2 sr1 sr2 ⇒
61        rl_join (rl_join (rl_psingleton dr1)
62                                    (rl_psingleton dr2))
63                      (rl_hsingleton RegisterCarry)
64      | OP1 op1 r1 r2 ⇒ rl_join (rl_psingleton r1) (rl_psingleton r2)
65      | POP r ⇒ rl_psingleton r
66      | ADDRESS _ _ r1 r2 ⇒ rl_join (rl_psingleton r1) (rl_psingleton r2)
67      | LOAD r _ _ ⇒ rl_psingleton r
68      | COMMENT c ⇒ rl_bottom
69      | STORE acc_a dpl dph ⇒ rl_bottom
70      | PUSH r ⇒ rl_bottom
71      | MOVE pair_reg ⇒
72        (* first register relevant only *)
73        match \fst pair_reg with
74        [ PSD p ⇒ rl_psingleton p
75        | HDW h ⇒ rl_hsingleton h
76        ]
77      | extension_seq ext ⇒
78        match ext with
79        [ ertl_new_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
80        | ertl_del_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
81        | ertl_frame_size r ⇒ rl_psingleton r
82        ]
83      (* Potentially destroys all caller-save hardware registers. *)
84      ]
85    | CALL _ _ _ ⇒ 〈set_empty …, set_from_list … RegisterCallerSaved〉
86    | COND r lbl_true ⇒ rl_bottom
87    | COST_LABEL clabel ⇒ rl_bottom
88    ]
89  | final _ ⇒ rl_bottom
90  | FCOND abs _ _ _ ⇒ Ⓧabs
91  ].
92
93definition ret_regs ≝ set_from_list … RegisterRets.
94
95definition rl_arg : psd_argument → register_lattice ≝
96  λarg.match arg with
97  [ Imm _ ⇒ rl_bottom
98  | Reg r ⇒ rl_psingleton r
99  ].
100
101definition used ≝
102  λglobals: list ident.
103  λs: joint_statement ERTL globals.
104  match s with
105  [ sequential seq l ⇒
106    match seq with
107    [ step_seq s ⇒
108      match s with
109      [ OP2 op2 acc_a r1 r2 ⇒
110        rl_join (rl_join (rl_arg r1) (rl_arg r2))
111          (match op2 with
112            [ Addc ⇒ rl_hsingleton RegisterCarry
113            | Sub ⇒ rl_hsingleton RegisterCarry
114            | _ ⇒ rl_bottom
115            ])
116      (* acc_a and acc_b *)
117      | OPACCS opaccs dr1 dr2 sr1 sr2 ⇒
118        rl_join (rl_arg sr1) (rl_arg sr2)
119      | OP1 op1 r1 r2 ⇒ rl_psingleton r2
120      | LOAD acc_a dpl dph ⇒ rl_join (rl_arg dpl) (rl_arg dph)
121      | STORE acc_a dpl dph ⇒
122        rl_join (rl_join (rl_arg acc_a) (rl_arg dpl)) (rl_arg dph)
123      | PUSH r ⇒ rl_arg r
124      | MOVE pair_reg ⇒
125        let r2 ≝ \snd pair_reg in
126        match r2 with
127        [ Reg p ⇒
128          match p with
129          [ PSD r ⇒ rl_psingleton r
130          | HDW r ⇒ rl_hsingleton r
131          ]
132        | Imm _ ⇒ rl_bottom
133        ]
134      | extension_seq ext ⇒
135        match ext with
136        [ ertl_new_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
137        | ertl_del_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
138        | ertl_frame_size r ⇒ rl_bottom
139        ]
140      (* Reads the hardware registers that are used to pass parameters. *)
141      | _ ⇒ rl_bottom
142      ]
143    | COST_LABEL clabel ⇒ rl_bottom
144    | CALL _ nparams _ ⇒ 〈set_empty …, set_from_list … (prefix ? nparams RegisterParams)〉
145    | COND r lbl_true ⇒ rl_psingleton r
146    ]
147  | final fin ⇒
148    match fin with
149    [ RETURN ⇒ 〈set_empty …, set_union … (set_from_list … RegisterCalleeSaved) ret_regs〉
150    | GOTO l ⇒ rl_bottom
151    | TAILCALL abs _ _ ⇒ match abs in False with [ ]
152    ]
153  | FCOND abs _ _ _ ⇒ Ⓧabs
154  ].
155
156definition eliminable ≝
157  λglobals: list ident.
158  λl: register_lattice.
159  λs: joint_statement ERTL globals.
160  let pliveafter ≝ \fst l in
161  let hliveafter ≝ \snd l in
162  match s with
163  [ sequential seq l ⇒
164    match seq with
165    [ step_seq s ⇒
166      match s with
167      [ OP2 op2 r1 r2 r3 ⇒
168        if match op2 with
169          [ Add ⇒ set_member … eq_Register RegisterCarry hliveafter
170          | Addc ⇒ set_member … eq_Register RegisterCarry hliveafter
171          | Sub ⇒ set_member … eq_Register RegisterCarry hliveafter
172          | _ ⇒ false
173          ] ∨ set_member … (eq_identifier …) r1 pliveafter
174        then
175          None ?
176        else
177          Some ? l
178      | OPACCS opaccs dr1 dr2 sr1 sr2 ⇒
179        if set_member … (eq_identifier …) dr1 pliveafter ∨
180           set_member … (eq_identifier …) dr2 pliveafter ∨
181           set_member … eq_Register RegisterCarry hliveafter then
182          None ?
183        else
184          Some ? l
185      | OP1 op1 r1 r2 ⇒
186        if set_member … (eq_identifier …) r1 pliveafter then
187          None ?
188        else
189          Some ? l
190      | ADDRESS _ _ r1 r2 ⇒
191        if set_member … (eq_identifier …) r1 pliveafter ∨
192           set_member … (eq_identifier …) r2 pliveafter then
193          None ?
194        else
195          Some ? l
196      | LOAD acc_a dpl dph ⇒
197        if set_member ? (eq_identifier …) acc_a pliveafter then
198          None ?
199        else
200          Some ? l
201      | MOVE pair_reg ⇒
202        if match \fst pair_reg with
203          [ PSD p1 ⇒
204            set_member … (eq_identifier …) p1 pliveafter
205          | HDW h1 ⇒
206            set_member … eq_Register h1 hliveafter
207          ] then
208            None ?
209          else
210            Some ? l
211      | extension_seq ext ⇒
212        match ext with
213        [ ertl_new_frame ⇒ None ?
214        | ertl_del_frame ⇒ None ?
215        | ertl_frame_size r ⇒
216          if set_member ? (eq_identifier RegisterTag) r pliveafter then
217            None ?
218          else
219            Some ? l
220        ]
221      | _ ⇒ None ?
222      ]
223    | _ ⇒ None ?
224    ]
225  | _ ⇒ None ?
226  ].
227
228definition statement_semantics: ∀globals: list ident.
229  joint_statement ERTL globals → register_lattice → register_lattice ≝
230  λglobals.
231  λstmt.
232  λliveafter.
233  match eliminable globals liveafter stmt with
234  [ None ⇒ rl_join (rl_diff liveafter (defined globals stmt)) (used globals stmt)
235  | Some l ⇒ liveafter
236  ].
237
238definition livebefore ≝
239  λglobals: list ident.
240  λint_fun: joint_internal_function ERTL globals.
241  λlabel.
242  λliveafter: valuation register_lattice.
243  match lookup ?? (joint_if_code … int_fun) label with
244  [ None      ⇒ rl_bottom
245  | Some stmt ⇒ statement_semantics globals stmt (liveafter label)
246  ].
247
248definition liveafter ≝
249   λglobals: list ident.
250  λint_fun: joint_internal_function ERTL globals.
251  λlabel.
252  λliveafter: valuation register_lattice.
253 match lookup ?? (joint_if_code … int_fun) label with
254  [ None      ⇒ rl_bottom
255  | Some stmt ⇒
256    \fold[rl_join,rl_bottom]_{successor ∈ stmt_labels … stmt}
257      (livebefore globals int_fun successor liveafter)
258  ].
259
260definition analyse_liveness ≝
261  λglobals.
262  λint_fun.
263    the_fixpoint ? (liveafter globals int_fun).
264
265definition vertex ≝ register + Register.
266
267definition plives : register → register_lattice → bool ≝
268  λvertex.λprop.set_member ? (eq_identifier RegisterTag) vertex (\fst prop).
269definition hlives : Register → register_lattice → bool ≝
270  λvertex.λprop.set_member ? eq_Register vertex (\snd prop).
271
272definition lives : vertex → register_lattice → bool ≝
273  λvertex.
274  match vertex with
275  [ inl v ⇒ plives v
276  | inr v ⇒ hlives v
277  ].
Note: See TracBrowser for help on using the repository browser.