source: src/ERTLptr/liveness.ma @ 3008

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

corrected bug where the address of pointer calls was not defined as used

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