source: src/ERTL/liveness.ma @ 2443

Last change on this file since 2443 was 2286, checked in by tranquil, 8 years ago

Big update!

  • merge of all _paolo variants
  • reorganised some depends (in particular, Register and thus back-end laguages no longer have fake ASM dependency)
  • split I8051.ma spawning new BackEndOps?.ma

compiler.ma broken at the moment, but not by these changes as far as I can tell

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