source: src/ERTLptr/liveness.ma @ 2887

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

Corrected bug where eliminable statements where not eliminated. Changed eliminable output from option label to bool.

File size: 9.0 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_step ≝
161λglobals: list ident.
162λl: register_lattice.
163λs: joint_step ERTLptr globals.
164let pliveafter ≝ \fst l in
165let hliveafter ≝ \snd l in
166match s with
167[ step_seq s ⇒
168  match s with
169  [ OP2 op2 r1 r2 r3 ⇒
170    ¬(match op2 with
171      [ Add ⇒ set_member … eq_Register RegisterCarry hliveafter
172      | Addc ⇒ set_member … eq_Register RegisterCarry hliveafter
173      | Sub ⇒ set_member … eq_Register RegisterCarry hliveafter
174      | _ ⇒ false
175      ] ∨ set_member … (eq_identifier …) r1 pliveafter)
176  | OPACCS opaccs dr1 dr2 sr1 sr2 ⇒
177    ¬(set_member … (eq_identifier …) dr1 pliveafter ∨
178      set_member … (eq_identifier …) dr2 pliveafter ∨
179      set_member … eq_Register RegisterCarry hliveafter)
180  | OP1 op1 r1 r2 ⇒
181    ¬set_member … (eq_identifier …) r1 pliveafter
182  | ADDRESS _ _ r1 r2 ⇒
183    ¬(set_member … (eq_identifier …) r1 pliveafter ∨
184      set_member … (eq_identifier …) r2 pliveafter)
185  | LOAD acc_a dpl dph ⇒
186    ¬set_member ? (eq_identifier …) acc_a pliveafter
187  | MOVE pair_reg ⇒
188    ¬match \fst pair_reg with
189      [ PSD p1 ⇒
190        set_member … (eq_identifier …) p1 pliveafter
191      | HDW h1 ⇒
192        set_member … eq_Register h1 hliveafter
193      ]
194  | extension_seq ext ⇒
195    match ext with
196    [ ertlptr_ertl ext' ⇒
197       match ext' with
198       [ ertl_new_frame ⇒ false
199       | ertl_del_frame ⇒ false
200       | ertl_frame_size r ⇒
201         ¬set_member ? (eq_identifier RegisterTag) r pliveafter
202       ]
203    | LOW_ADDRESS r1 l' ⇒
204       ¬set_member ? (eq_identifier RegisterTag) r1 pliveafter
205    | HIGH_ADDRESS r1 l' ⇒
206       ¬set_member ? (eq_identifier RegisterTag) r1 pliveafter
207    ]       
208  | _ ⇒ false
209  ]
210| _ ⇒ false
211].
212
213definition eliminable ≝
214  λglobals: list ident.
215  λl: register_lattice.
216  λs: joint_statement ERTLptr globals.
217  let pliveafter ≝ \fst l in
218  let hliveafter ≝ \snd l in
219  match s with
220  [ sequential seq _ ⇒ eliminable_step … l seq
221  | _ ⇒ false
222  ].
223
224definition statement_semantics: ∀globals: list ident.
225  joint_statement ERTLptr globals → register_lattice → register_lattice ≝
226  λglobals.
227  λstmt.
228  λliveafter.
229  if eliminable globals liveafter stmt then
230    liveafter
231  else
232    rl_join (rl_diff liveafter (defined globals stmt)) (used globals stmt).
233
234definition livebefore ≝
235  λglobals: list ident.
236  λint_fun: joint_internal_function ERTLptr globals.
237  λlabel.
238  λliveafter: valuation register_lattice.
239  match lookup ?? (joint_if_code … int_fun) label with
240  [ None      ⇒ rl_bottom
241  | Some stmt ⇒ statement_semantics globals stmt (liveafter label)
242  ].
243
244definition liveafter ≝
245   λglobals: list ident.
246  λint_fun: joint_internal_function ERTLptr globals.
247  λlabel.
248  λliveafter: valuation register_lattice.
249 match lookup ?? (joint_if_code … int_fun) label with
250  [ None      ⇒ rl_bottom
251  | Some stmt ⇒
252    \fold[rl_join,rl_bottom]_{successor ∈ stmt_labels … stmt}
253      (livebefore globals int_fun successor liveafter)
254  ].
255
256definition analyse_liveness ≝
257  λthe_fixpoint: fixpoint_computer. λglobals,int_fun.
258   the_fixpoint ? (liveafter globals int_fun).
259
260definition vertex ≝ register + Register.
261
262definition plives : register → register_lattice → bool ≝
263  λvertex.λprop.set_member ? (eq_identifier RegisterTag) vertex (\fst prop).
264definition hlives : Register → register_lattice → bool ≝
265  λvertex.λprop.set_member ? eq_Register vertex (\snd prop).
266
267definition lives : vertex → register_lattice → bool ≝
268  λvertex.
269  match vertex with
270  [ inl v ⇒ plives v
271  | inr v ⇒ hlives v
272  ].
Note: See TracBrowser for help on using the repository browser.