source: src/ERTLptr/liveness.ma @ 2883

Last change on this file since 2883 was 2883, checked in by piccolo, 7 years ago

partial commit

File size: 9.6 KB
Line 
1include "ASM/Util.ma".
2include "ERTLptr/ERTLptr.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 pairwise : ∀A,B : Type[0]. ∀f : A → A → A. ∀g: B → B → B.
29A × B → A × B → A × B≝
30λA,B,f,g,c1,c2.〈f (\fst c1) (\fst c2) , g (\snd c1) (\snd c2)〉.
31
32definition rl_join: register_lattice → register_lattice → register_lattice ≝
33pairwise ?? (set_union …) (set_union …).
34
35definition rl_diff: register_lattice → register_lattice → register_lattice ≝
36pairwise ?? (set_diff …) (set_diff …).
37
38definition defined ≝
39  λglobals: list ident.
40  λs: joint_statement ERTLptr globals.
41  match s with
42  [ sequential seq l ⇒
43    match seq with
44    [ step_seq s ⇒
45      match s with
46      [ OP2 op2 r1 r2 _ ⇒
47        match op2 with
48        [ Add ⇒ rl_join (rl_hsingleton RegisterCarry) (rl_psingleton r1)
49        | Addc ⇒ rl_join (rl_hsingleton RegisterCarry) (rl_psingleton r1)
50        | Sub ⇒ rl_join (rl_hsingleton RegisterCarry)  (rl_psingleton r1)
51        | _ ⇒ rl_psingleton r1
52        ]
53      | CLEAR_CARRY ⇒ rl_hsingleton RegisterCarry
54      | SET_CARRY ⇒ rl_hsingleton RegisterCarry
55      | OPACCS opaccs dr1 dr2 sr1 sr2 ⇒
56        rl_join (rl_join (rl_psingleton dr1)
57                                    (rl_psingleton dr2))
58                      (rl_hsingleton RegisterCarry)
59      | OP1 op1 r1 r2 ⇒ rl_psingleton r1
60      | POP r ⇒ rl_psingleton r
61      | ADDRESS _ _ r1 r2 ⇒ rl_join (rl_psingleton r1) (rl_psingleton r2)
62      | LOAD r _ _ ⇒ rl_psingleton r
63      | COMMENT c ⇒ rl_bottom
64      | STORE acc_a dpl dph ⇒ rl_bottom
65      | PUSH r ⇒ rl_bottom
66      | MOVE pair_reg ⇒
67        (* first register relevant only *)
68        match \fst pair_reg with
69        [ PSD p ⇒ rl_psingleton p
70        | HDW h ⇒ rl_hsingleton h
71        ]
72      | extension_seq ext ⇒
73        match ext with
74        [ ertlptr_ertl ext' ⇒
75           match ext' with
76           [ ertl_new_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
77           | ertl_del_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
78           | ertl_frame_size r ⇒ rl_psingleton r
79           ]
80        | LOW_ADDRESS r1 l ⇒ rl_psingleton r1
81        | HIGH_ADDRESS r1 l ⇒ rl_psingleton r1
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 ERTLptr 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        [ ertlptr_ertl ext' ⇒
137           match ext' with
138           [ ertl_new_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
139           | ertl_del_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
140           | ertl_frame_size r ⇒ rl_bottom ]
141        | LOW_ADDRESS r1 l ⇒ rl_bottom
142        | HIGH_ADDRESS r1 l ⇒ rl_bottom
143        ]       
144      (* Reads the hardware registers that are used to pass parameters. *)
145      | _ ⇒ rl_bottom
146      ]
147    | COST_LABEL clabel ⇒ rl_bottom
148    | CALL _ nparams _ ⇒ 〈set_empty …, set_from_list … (prefix ? nparams RegisterParams)〉
149    | COND r lbl_true ⇒ rl_psingleton r
150    ]
151  | final fin ⇒
152    match fin with
153    [ RETURN ⇒ 〈set_empty …, set_union … (set_from_list … RegisterCalleeSaved) ret_regs〉
154    | GOTO l ⇒ rl_bottom
155    | TAILCALL abs _ _ ⇒ match abs in False with [ ]
156    ]
157  | FCOND abs _ _ _ ⇒ Ⓧabs
158  ].
159
160definition eliminable ≝
161  λglobals: list ident.
162  λl: register_lattice.
163  λs: joint_statement ERTLptr globals.
164  let pliveafter ≝ \fst l in
165  let hliveafter ≝ \snd l in
166  match s with
167  [ sequential seq l ⇒
168    match seq with
169    [ step_seq s ⇒
170      match s with
171      [ OP2 op2 r1 r2 r3 ⇒
172        if match op2 with
173          [ Add ⇒ set_member … eq_Register RegisterCarry hliveafter
174          | Addc ⇒ set_member … eq_Register RegisterCarry hliveafter
175          | Sub ⇒ set_member … eq_Register RegisterCarry hliveafter
176          | _ ⇒ false
177          ] ∨ set_member … (eq_identifier …) r1 pliveafter
178        then
179          None ?
180        else
181          Some ? l
182      | OPACCS opaccs dr1 dr2 sr1 sr2 ⇒
183        if set_member … (eq_identifier …) dr1 pliveafter ∨
184           set_member … (eq_identifier …) dr2 pliveafter ∨
185           set_member … eq_Register RegisterCarry hliveafter then
186          None ?
187        else
188          Some ? l
189      | OP1 op1 r1 r2 ⇒
190        if set_member … (eq_identifier …) r1 pliveafter then
191          None ?
192        else
193          Some ? l
194      | ADDRESS _ _ r1 r2 ⇒
195        if set_member … (eq_identifier …) r1 pliveafter ∨
196           set_member … (eq_identifier …) r2 pliveafter then
197          None ?
198        else
199          Some ? l
200      | LOAD acc_a dpl dph ⇒
201        if set_member ? (eq_identifier …) acc_a pliveafter then
202          None ?
203        else
204          Some ? l
205      | MOVE pair_reg ⇒
206        if match \fst pair_reg with
207          [ PSD p1 ⇒
208            set_member … (eq_identifier …) p1 pliveafter
209          | HDW h1 ⇒
210            set_member … eq_Register h1 hliveafter
211          ] then
212            None ?
213          else
214            Some ? l
215      | extension_seq ext ⇒
216        match ext with
217        [ ertlptr_ertl ext' ⇒
218           match ext' with
219           [ ertl_new_frame ⇒ None ?
220           | ertl_del_frame ⇒ None ?
221           | ertl_frame_size r ⇒
222             if set_member ? (eq_identifier RegisterTag) r pliveafter then
223               None ?
224             else
225               Some ? l]
226        | LOW_ADDRESS r1 l' ⇒
227           if set_member ? (eq_identifier RegisterTag) r1 pliveafter then
228             None ?
229           else
230             Some ? l
231        | HIGH_ADDRESS r1 l' ⇒
232           if set_member ? (eq_identifier RegisterTag) r1 pliveafter then
233             None ?
234           else
235             Some ? l
236        ]       
237      | _ ⇒ None ?
238      ]
239    | _ ⇒ None ?
240    ]
241  | _ ⇒ None ?
242  ].
243
244definition statement_semantics: ∀globals: list ident.
245  joint_statement ERTLptr globals → register_lattice → register_lattice ≝
246  λglobals.
247  λstmt.
248  λliveafter.
249  match eliminable globals liveafter stmt with
250  [ None ⇒ rl_join (rl_diff liveafter (defined globals stmt)) (used globals stmt)
251  | Some l ⇒ liveafter
252  ].
253
254definition livebefore ≝
255  λglobals: list ident.
256  λint_fun: joint_internal_function ERTLptr globals.
257  λlabel.
258  λliveafter: valuation register_lattice.
259  match lookup ?? (joint_if_code … int_fun) label with
260  [ None      ⇒ rl_bottom
261  | Some stmt ⇒ statement_semantics globals stmt (liveafter label)
262  ].
263
264definition liveafter ≝
265   λglobals: list ident.
266  λint_fun: joint_internal_function ERTLptr globals.
267  λlabel.
268  λliveafter: valuation register_lattice.
269 match lookup ?? (joint_if_code … int_fun) label with
270  [ None      ⇒ rl_bottom
271  | Some stmt ⇒
272    \fold[rl_join,rl_bottom]_{successor ∈ stmt_labels … stmt}
273      (livebefore globals int_fun successor liveafter)
274  ].
275
276definition analyse_liveness ≝
277  λthe_fixpoint: fixpoint_computer. λglobals,int_fun.
278   the_fixpoint ? (liveafter globals int_fun).
279
280definition vertex ≝ register + Register.
281
282definition plives : register → register_lattice → bool ≝
283  λvertex.λprop.set_member ? (eq_identifier RegisterTag) vertex (\fst prop).
284definition hlives : Register → register_lattice → bool ≝
285  λvertex.λprop.set_member ? eq_Register vertex (\snd prop).
286
287definition lives : vertex → register_lattice → bool ≝
288  λvertex.
289  match vertex with
290  [ inl v ⇒ plives v
291  | inr v ⇒ hlives v
292  ].
Note: See TracBrowser for help on using the repository browser.