source: src/ERTL/liveness.ma @ 2563

Last change on this file since 2563 was 2490, checked in by tranquil, 7 years ago

switched back to Byte immediate (instead of beval ones)
propagated pending changes to all passes

File size: 8.7 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      | COST_LABEL clabel ⇒ rl_bottom
71      | PUSH r ⇒ rl_bottom
72      | MOVE pair_reg ⇒
73        (* first register relevant only *)
74        match \fst pair_reg with
75        [ PSD p ⇒ rl_psingleton p
76        | HDW h ⇒ rl_hsingleton h
77        ]
78      | extension_seq ext ⇒
79        match ext with
80        [ ertl_new_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
81        | ertl_del_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
82        | ertl_frame_size r ⇒ rl_psingleton r
83        ]
84      (* Potentially destroys all caller-save hardware registers. *)
85      | CALL _ _ _ ⇒ 〈set_empty …, set_from_list … RegisterCallerSaved〉
86      ]
87    | COND r lbl_true ⇒ rl_bottom
88    ]
89  | final _ ⇒ rl_bottom
90  ].
91
92definition ret_regs ≝ set_from_list … RegisterRets.
93
94definition rl_arg : psd_argument → register_lattice ≝
95  λarg.match arg with
96  [ Imm _ ⇒ rl_bottom
97  | Reg r ⇒ rl_psingleton r
98  ].
99
100definition used ≝
101  λglobals: list ident.
102  λs: joint_statement ERTL globals.
103  match s with
104  [ sequential seq l ⇒
105    match seq with
106    [ step_seq s ⇒
107      match s with
108      [ OP2 op2 acc_a r1 r2 ⇒
109        rl_join (rl_join (rl_arg r1) (rl_arg r2))
110          (match op2 with
111            [ Addc ⇒ rl_hsingleton RegisterCarry
112            | Sub ⇒ rl_hsingleton RegisterCarry
113            | _ ⇒ rl_bottom
114            ])
115      (* acc_a and acc_b *)
116      | OPACCS opaccs dr1 dr2 sr1 sr2 ⇒
117        rl_join (rl_arg sr1) (rl_arg sr2)
118      | OP1 op1 r1 r2 ⇒ rl_psingleton r2
119      | LOAD acc_a dpl dph ⇒ rl_join (rl_arg dpl) (rl_arg dph)
120      | STORE acc_a dpl dph ⇒
121        rl_join (rl_join (rl_arg acc_a) (rl_arg dpl)) (rl_arg dph)
122      | PUSH r ⇒ rl_arg r
123      | MOVE pair_reg ⇒
124        let r2 ≝ \snd pair_reg in
125        match r2 with
126        [ Reg p ⇒
127          match p with
128          [ PSD r ⇒ rl_psingleton r
129          | HDW r ⇒ rl_hsingleton r
130          ]
131        | Imm _ ⇒ rl_bottom
132        ]
133      | extension_seq ext ⇒
134        match ext with
135        [ ertl_new_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
136        | ertl_del_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
137        | ertl_frame_size r ⇒ rl_bottom
138        ]
139      (* Reads the hardware registers that are used to pass parameters. *)
140      | CALL _ nparams _ ⇒ 〈set_empty …, set_from_list … (prefix ? nparams RegisterParams)〉
141      | _ ⇒ rl_bottom
142      ]
143    | COND r lbl_true ⇒ rl_psingleton r
144    ]
145  | final fin ⇒
146    match fin with
147    [ RETURN ⇒ 〈set_empty …, set_union … (set_from_list … RegisterCalleeSaved) ret_regs〉
148    | GOTO l ⇒ rl_bottom
149    | TAILCALL abs _ _ ⇒ match abs in False with [ ]
150    ]
151  ].
152
153definition eliminable ≝
154  λglobals: list ident.
155  λl: register_lattice.
156  λs: joint_statement ERTL globals.
157  let pliveafter ≝ \fst l in
158  let hliveafter ≝ \snd l in
159  match s with
160  [ sequential seq l ⇒
161    match seq with
162    [ step_seq s ⇒
163      match s with
164      [ OP2 op2 r1 r2 r3 ⇒
165        if match op2 with
166          [ Add ⇒ set_member … eq_Register RegisterCarry hliveafter
167          | Addc ⇒ set_member … eq_Register RegisterCarry hliveafter
168          | Sub ⇒ set_member … eq_Register RegisterCarry hliveafter
169          | _ ⇒ false
170          ] ∨ set_member … (eq_identifier …) r1 pliveafter
171        then
172          None ?
173        else
174          Some ? l
175      | OPACCS opaccs dr1 dr2 sr1 sr2 ⇒
176        if set_member … (eq_identifier …) dr1 pliveafter ∨
177           set_member … (eq_identifier …) dr2 pliveafter ∨
178           set_member … eq_Register RegisterCarry hliveafter then
179          None ?
180        else
181          Some ? l
182      | OP1 op1 r1 r2 ⇒
183        if set_member … (eq_identifier …) r1 pliveafter then
184          None ?
185        else
186          Some ? l
187      | ADDRESS _ _ r1 r2 ⇒
188        if set_member … (eq_identifier …) r1 pliveafter ∨
189           set_member … (eq_identifier …) r2 pliveafter then
190          None ?
191        else
192          Some ? l
193      | LOAD acc_a dpl dph ⇒
194        if set_member ? (eq_identifier …) acc_a pliveafter then
195          None ?
196        else
197          Some ? l
198      | MOVE pair_reg ⇒
199        if match \fst pair_reg with
200          [ PSD p1 ⇒
201            set_member … (eq_identifier …) p1 pliveafter
202          | HDW h1 ⇒
203            set_member … eq_Register h1 hliveafter
204          ] then
205            None ?
206          else
207            Some ? l
208      | extension_seq ext ⇒
209        match ext with
210        [ ertl_new_frame ⇒ None ?
211        | ertl_del_frame ⇒ None ?
212        | ertl_frame_size r ⇒
213          if set_member ? (eq_identifier RegisterTag) r pliveafter then
214            None ?
215          else
216            Some ? l
217        ]
218      | _ ⇒ None ?
219      ]
220    | COND _ _ ⇒ None ?
221    ]
222  | _ ⇒ None ?
223  ].
224
225definition statement_semantics: ∀globals: list ident.
226  joint_statement ERTL globals → register_lattice → register_lattice ≝
227  λglobals.
228  λstmt.
229  λliveafter.
230  match eliminable globals liveafter stmt with
231  [ None ⇒ rl_join (rl_diff liveafter (defined globals stmt)) (used globals stmt)
232  | Some l ⇒ liveafter
233  ].
234
235definition livebefore ≝
236  λglobals: list ident.
237  λint_fun: joint_internal_function ERTL globals.
238  λlabel.
239  λliveafter: valuation register_lattice.
240  match lookup ?? (joint_if_code … int_fun) label with
241  [ None      ⇒ rl_bottom
242  | Some stmt ⇒ statement_semantics globals stmt (liveafter label)
243  ].
244
245definition liveafter ≝
246   λglobals: list ident.
247  λint_fun: joint_internal_function ERTL globals.
248  λlabel.
249  λliveafter: valuation register_lattice.
250 match lookup ?? (joint_if_code … int_fun) label with
251  [ None      ⇒ rl_bottom
252  | Some stmt ⇒
253    \fold[rl_join,rl_bottom]_{successor ∈ stmt_labels … stmt}
254      (livebefore globals int_fun successor liveafter)
255  ].
256
257definition analyse_liveness ≝
258  λglobals.
259  λint_fun.
260    the_fixpoint ? (liveafter globals int_fun).
261
262definition vertex ≝ register + Register.
263
264definition plives : register → register_lattice → bool ≝
265  λvertex.λprop.set_member ? (eq_identifier RegisterTag) vertex (\fst prop).
266definition hlives : Register → register_lattice → bool ≝
267  λvertex.λprop.set_member ? eq_Register vertex (\snd prop).
268
269definition lives : vertex → register_lattice → bool ≝
270  λvertex.
271  match vertex with
272  [ inl v ⇒ plives v
273  | inr v ⇒ hlives v
274  ].
Note: See TracBrowser for help on using the repository browser.