source: src/ERTL/liveness_paolo.ma @ 2208

Last change on this file since 2208 was 2208, checked in by tranquil, 8 years ago
  • moving some code around
  • changed immediates to hold beval in general, not only bytes
  • fixed RTLabsToRTL after redefinitions in front end
File size: 8.9 KB
Line 
1include "ASM/Util.ma".
2include "ERTL/ERTL_paolo.ma".
3include "utilities/adt/set_adt.ma".
4include "utilities/fixpoints.ma".
5
6definition register_lattice : property_lattice ≝
7mk_property_lattice
8 ((set register) × (set Register))
9 〈set_empty …, set_empty …〉
10 (λleft.
11  λright.
12  set_equal … (eq_identifier ?) (\fst left) (\fst right) ∧
13  set_equal … eq_Register (\snd left) (\snd right))
14 (λleft.
15  λright.
16  set_subset … (eq_identifier ?) (\fst left) (\fst right) ∧
17  set_subset … eq_Register (\snd left) (\snd right))
18 (λ_.false).
19
20definition rl_bottom ≝ l_bottom register_lattice.
21definition rl_psingleton: register → register_lattice ≝
22  λr.
23    〈set_singleton … r, set_empty …〉.
24definition rl_hsingleton: Register → register_lattice ≝
25  λr.
26    〈set_empty …, set_singleton … r〉.
27
28definition rl_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 rl_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 defined ≝
43  λglobals: list ident.
44  λs: joint_statement ertl_params globals.
45  match s with
46  [ sequential seq l ⇒
47    match seq with
48    [ step_seq s ⇒
49      match s with
50      [ OP2 op2 r1 r2 _ ⇒
51        match op2 with
52        [ Add ⇒ rl_join (rl_hsingleton RegisterCarry) (rl_psingleton r1)
53        | Addc ⇒ rl_join (rl_hsingleton RegisterCarry) (rl_psingleton r1)
54        | Sub ⇒ rl_join (rl_hsingleton RegisterCarry)  (rl_psingleton r1)
55        | _ ⇒ rl_psingleton r1
56        ]
57      | CLEAR_CARRY ⇒ rl_hsingleton RegisterCarry
58      | SET_CARRY ⇒ rl_hsingleton RegisterCarry
59      | OPACCS opaccs dr1 dr2 sr1 sr2 ⇒
60        rl_join (rl_join (rl_psingleton dr1)
61                                    (rl_psingleton dr2))
62                      (rl_hsingleton RegisterCarry)
63      | OP1 op1 r1 r2 ⇒ rl_join (rl_psingleton r1) (rl_psingleton r2)
64      | POP r ⇒ rl_psingleton r
65      | ADDRESS _ _ r1 r2 ⇒ rl_join (rl_psingleton r1) (rl_psingleton r2)
66      | LOAD r _ _ ⇒ rl_psingleton r
67      | COMMENT c ⇒ rl_bottom
68      | STORE acc_a dpl dph ⇒ rl_bottom
69      | COST_LABEL clabel ⇒ 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      | CALL_ID id _ _ ⇒ 〈set_empty …, set_from_list … RegisterCallerSaved〉
85      | extension_call abs ⇒ match abs in void with [ ]
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_params 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_ID _ nparams _ ⇒ 〈set_empty …, set_from_list … (prefix ? nparams RegisterParams)〉
141      | extension_call abs ⇒ match abs in void with [ ]
142      | _ ⇒ rl_bottom
143      ]
144    | COND r lbl_true ⇒ rl_psingleton r
145    ]
146  | final fin ⇒
147    match fin with
148    [ RETURN ⇒ 〈set_empty …, set_union … (set_from_list … RegisterCalleeSaved) ret_regs〉
149    | GOTO l ⇒ rl_bottom
150    | tailcall abs ⇒ match abs in void with [ ]
151    ]
152  ].
153
154definition eliminable ≝
155  λglobals: list ident.
156  λl: register_lattice.
157  λs: joint_statement ertl_params globals.
158  let pliveafter ≝ \fst l in
159  let hliveafter ≝ \snd l in
160  match s with
161  [ sequential seq l ⇒
162    match seq with
163    [ step_seq s ⇒
164      match s with
165      [ OP2 op2 r1 r2 r3 ⇒
166        if match op2 with
167          [ Add ⇒ set_member … eq_Register RegisterCarry hliveafter
168          | Addc ⇒ set_member … eq_Register RegisterCarry hliveafter
169          | Sub ⇒ set_member … eq_Register RegisterCarry hliveafter
170          | _ ⇒ false
171          ] ∨ set_member … (eq_identifier …) r1 pliveafter
172        then
173          None ?
174        else
175          Some ? l
176      | OPACCS opaccs dr1 dr2 sr1 sr2 ⇒
177        if set_member … (eq_identifier …) dr1 pliveafter ∨
178           set_member … (eq_identifier …) dr2 pliveafter ∨
179           set_member … eq_Register RegisterCarry hliveafter then
180          None ?
181        else
182          Some ? l
183      | OP1 op1 r1 r2 ⇒
184        if set_member … (eq_identifier …) r1 pliveafter then
185          None ?
186        else
187          Some ? l
188      | ADDRESS _ _ r1 r2 ⇒
189        if set_member … (eq_identifier …) r1 pliveafter ∨
190           set_member … (eq_identifier …) r2 pliveafter then
191          None ?
192        else
193          Some ? l
194      | LOAD acc_a dpl dph ⇒
195        if set_member ? (eq_identifier …) acc_a pliveafter then
196          None ?
197        else
198          Some ? l
199      | MOVE pair_reg ⇒
200        if match \fst pair_reg with
201          [ PSD p1 ⇒
202            set_member … (eq_identifier …) p1 pliveafter
203          | HDW h1 ⇒
204            set_member … eq_Register h1 hliveafter
205          ] then
206            None ?
207          else
208            Some ? l
209      | extension_seq ext ⇒
210        match ext with
211        [ ertl_new_frame ⇒ None ?
212        | ertl_del_frame ⇒ None ?
213        | ertl_frame_size r ⇒
214          if set_member ? (eq_identifier RegisterTag) r pliveafter then
215            None ?
216          else
217            Some ? l
218        ]
219      | _ ⇒ None ?
220      ]
221    | COND _ _ ⇒ None ?
222    ]
223  | _ ⇒ None ?
224  ].
225
226definition statement_semantics: ∀globals: list ident.
227  joint_statement ertl_params globals → register_lattice → register_lattice ≝
228  λglobals.
229  λstmt.
230  λliveafter.
231  match eliminable globals liveafter stmt with
232  [ None ⇒ rl_join (rl_diff liveafter (defined globals stmt)) (used globals stmt)
233  | Some l ⇒ liveafter
234  ].
235
236definition livebefore ≝
237  λglobals: list ident.
238  λint_fun: joint_internal_function globals ertl_params.
239  λlabel.
240  λliveafter: valuation register_lattice.
241  match lookup ?? (joint_if_code … int_fun) label with
242  [ None      ⇒ rl_bottom
243  | Some stmt ⇒ statement_semantics globals stmt (liveafter label)
244  ].
245
246definition liveafter ≝
247   λglobals: list ident.
248  λint_fun: joint_internal_function globals ertl_params.
249  λlabel.
250  λliveafter: valuation register_lattice.
251 match lookup ?? (joint_if_code … int_fun) label with
252  [ None      ⇒ rl_bottom
253  | Some stmt ⇒
254    \fold[rl_join,rl_bottom]_{successor ∈ stmt_labels … stmt}
255      (livebefore globals int_fun successor liveafter)
256  ].
257
258definition analyse_liveness ≝
259  λglobals.
260  λint_fun.
261    the_fixpoint ? (liveafter globals int_fun).
262
263definition vertex ≝ register + Register.
264
265definition plives : register → register_lattice → bool ≝
266  λvertex.λprop.set_member ? (eq_identifier RegisterTag) vertex (\fst prop).
267definition hlives : Register → register_lattice → bool ≝
268  λvertex.λprop.set_member ? eq_Register vertex (\snd prop).
269
270definition lives : vertex → register_lattice → bool ≝
271  λvertex.
272  match vertex with
273  [ inl v ⇒ plives v
274  | inr v ⇒ hlives v
275  ].
Note: See TracBrowser for help on using the repository browser.