source: src/ERTL/liveness_paolo.ma @ 2174

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