source: src/ERTLptr/liveness.ma @ 2845

Last change on this file since 2845 was 2700, checked in by sacerdot, 8 years ago
  1. exponential function dropped in favour of standard library
  2. fixpoint computation and graph colouring abstracted in the back-end, axiomatized in the compiler
  3. minor speedups in Policy.ma
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 rl_join: register_lattice → register_lattice → register_lattice ≝
29  λleft.
30  λright.
31  let 〈lp, lh〉 ≝ left in
32  let 〈rp, rh〉 ≝ right in
33    〈set_union … lp rp, set_union … lh rh〉.
34
35definition rl_diff: register_lattice → register_lattice → register_lattice ≝
36  λleft.
37  λright.
38  let 〈lp, lh〉 ≝ left in
39  let 〈rp, rh〉 ≝ right in
40    〈set_diff … lp rp, set_diff … lh rh〉.
41
42definition defined ≝
43  λglobals: list ident.
44  λs: joint_statement ERTLptr globals.
45  match s with
46  [ sequential seq l ⇒
47    match seq with
48    [ step_seq s ⇒
49      match s with
50      [ OP2 op2 r1 r2 _ ⇒
51        match op2 with
52        [ Add ⇒ rl_join (rl_hsingleton RegisterCarry) (rl_psingleton r1)
53        | Addc ⇒ rl_join (rl_hsingleton RegisterCarry) (rl_psingleton r1)
54        | Sub ⇒ rl_join (rl_hsingleton RegisterCarry)  (rl_psingleton r1)
55        | _ ⇒ rl_psingleton r1
56        ]
57      | CLEAR_CARRY ⇒ rl_hsingleton RegisterCarry
58      | SET_CARRY ⇒ rl_hsingleton RegisterCarry
59      | OPACCS opaccs dr1 dr2 sr1 sr2 ⇒
60        rl_join (rl_join (rl_psingleton dr1)
61                                    (rl_psingleton dr2))
62                      (rl_hsingleton RegisterCarry)
63      | OP1 op1 r1 r2 ⇒ rl_psingleton r1
64      | POP r ⇒ rl_psingleton r
65      | ADDRESS _ _ r1 r2 ⇒ rl_join (rl_psingleton r1) (rl_psingleton r2)
66      | LOAD r _ _ ⇒ rl_psingleton r
67      | COMMENT c ⇒ rl_bottom
68      | STORE acc_a dpl dph ⇒ rl_bottom
69      | PUSH r ⇒ rl_bottom
70      | MOVE pair_reg ⇒
71        (* first register relevant only *)
72        match \fst pair_reg with
73        [ PSD p ⇒ rl_psingleton p
74        | HDW h ⇒ rl_hsingleton h
75        ]
76      | extension_seq ext ⇒
77        match ext with
78        [ ertlptr_ertl 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        | LOW_ADDRESS r1 l ⇒ rl_psingleton r1
85        | HIGH_ADDRESS r1 l ⇒ rl_psingleton r1
86        ]
87      (* Potentially destroys all caller-save hardware registers. *)
88      ]
89    | CALL _ _ _ ⇒ 〈set_empty …, set_from_list … RegisterCallerSaved〉
90    | COND r lbl_true ⇒ rl_bottom
91    | COST_LABEL clabel ⇒ rl_bottom
92    ]
93  | final _ ⇒ rl_bottom
94  | FCOND abs _ _ _ ⇒ Ⓧabs
95  ].
96
97definition ret_regs ≝ set_from_list … RegisterRets.
98
99definition rl_arg : psd_argument → register_lattice ≝
100  λarg.match arg with
101  [ Imm _ ⇒ rl_bottom
102  | Reg r ⇒ rl_psingleton r
103  ].
104
105definition used ≝
106  λglobals: list ident.
107  λs: joint_statement ERTLptr globals.
108  match s with
109  [ sequential seq l ⇒
110    match seq with
111    [ step_seq s ⇒
112      match s with
113      [ OP2 op2 acc_a r1 r2 ⇒
114        rl_join (rl_join (rl_arg r1) (rl_arg r2))
115          (match op2 with
116            [ Addc ⇒ rl_hsingleton RegisterCarry
117            | Sub ⇒ rl_hsingleton RegisterCarry
118            | _ ⇒ rl_bottom
119            ])
120      (* acc_a and acc_b *)
121      | OPACCS opaccs dr1 dr2 sr1 sr2 ⇒
122        rl_join (rl_arg sr1) (rl_arg sr2)
123      | OP1 op1 r1 r2 ⇒ rl_psingleton r2
124      | LOAD acc_a dpl dph ⇒ rl_join (rl_arg dpl) (rl_arg dph)
125      | STORE acc_a dpl dph ⇒
126        rl_join (rl_join (rl_arg acc_a) (rl_arg dpl)) (rl_arg dph)
127      | PUSH r ⇒ rl_arg r
128      | MOVE pair_reg ⇒
129        let r2 ≝ \snd pair_reg in
130        match r2 with
131        [ Reg p ⇒
132          match p with
133          [ PSD r ⇒ rl_psingleton r
134          | HDW r ⇒ rl_hsingleton r
135          ]
136        | Imm _ ⇒ rl_bottom
137        ]
138      | extension_seq ext ⇒
139        match ext with
140        [ ertlptr_ertl ext' ⇒
141           match ext' with
142           [ ertl_new_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
143           | ertl_del_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
144           | ertl_frame_size r ⇒ rl_bottom ]
145        | LOW_ADDRESS r1 l ⇒ rl_bottom
146        | HIGH_ADDRESS r1 l ⇒ rl_bottom
147        ]       
148      (* Reads the hardware registers that are used to pass parameters. *)
149      | _ ⇒ rl_bottom
150      ]
151    | COST_LABEL clabel ⇒ rl_bottom
152    | CALL _ nparams _ ⇒ 〈set_empty …, set_from_list … (prefix ? nparams RegisterParams)〉
153    | COND r lbl_true ⇒ rl_psingleton r
154    ]
155  | final fin ⇒
156    match fin with
157    [ RETURN ⇒ 〈set_empty …, set_union … (set_from_list … RegisterCalleeSaved) ret_regs〉
158    | GOTO l ⇒ rl_bottom
159    | TAILCALL abs _ _ ⇒ match abs in False with [ ]
160    ]
161  | FCOND abs _ _ _ ⇒ Ⓧabs
162  ].
163
164definition eliminable ≝
165  λglobals: list ident.
166  λl: register_lattice.
167  λs: joint_statement ERTLptr globals.
168  let pliveafter ≝ \fst l in
169  let hliveafter ≝ \snd l in
170  match s with
171  [ sequential seq l ⇒
172    match seq with
173    [ step_seq s ⇒
174      match s with
175      [ OP2 op2 r1 r2 r3 ⇒
176        if 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        then
183          None ?
184        else
185          Some ? l
186      | OPACCS opaccs dr1 dr2 sr1 sr2 ⇒
187        if set_member … (eq_identifier …) dr1 pliveafter ∨
188           set_member … (eq_identifier …) dr2 pliveafter ∨
189           set_member … eq_Register RegisterCarry hliveafter then
190          None ?
191        else
192          Some ? l
193      | OP1 op1 r1 r2 ⇒
194        if set_member … (eq_identifier …) r1 pliveafter then
195          None ?
196        else
197          Some ? l
198      | ADDRESS _ _ r1 r2 ⇒
199        if set_member … (eq_identifier …) r1 pliveafter ∨
200           set_member … (eq_identifier …) r2 pliveafter then
201          None ?
202        else
203          Some ? l
204      | LOAD acc_a dpl dph ⇒
205        if set_member ? (eq_identifier …) acc_a pliveafter then
206          None ?
207        else
208          Some ? l
209      | MOVE pair_reg ⇒
210        if match \fst pair_reg with
211          [ PSD p1 ⇒
212            set_member … (eq_identifier …) p1 pliveafter
213          | HDW h1 ⇒
214            set_member … eq_Register h1 hliveafter
215          ] then
216            None ?
217          else
218            Some ? l
219      | extension_seq ext ⇒
220        match ext with
221        [ ertlptr_ertl ext' ⇒
222           match ext' with
223           [ ertl_new_frame ⇒ None ?
224           | ertl_del_frame ⇒ None ?
225           | ertl_frame_size r ⇒
226             if set_member ? (eq_identifier RegisterTag) r pliveafter then
227               None ?
228             else
229               Some ? l]
230        | LOW_ADDRESS r1 l' ⇒
231           if set_member ? (eq_identifier RegisterTag) r1 pliveafter then
232             None ?
233           else
234             Some ? l
235        | HIGH_ADDRESS r1 l' ⇒
236           if set_member ? (eq_identifier RegisterTag) r1 pliveafter then
237             None ?
238           else
239             Some ? l
240        ]       
241      | _ ⇒ None ?
242      ]
243    | _ ⇒ None ?
244    ]
245  | _ ⇒ None ?
246  ].
247
248definition statement_semantics: ∀globals: list ident.
249  joint_statement ERTLptr globals → register_lattice → register_lattice ≝
250  λglobals.
251  λstmt.
252  λliveafter.
253  match eliminable globals liveafter stmt with
254  [ None ⇒ rl_join (rl_diff liveafter (defined globals stmt)) (used globals stmt)
255  | Some l ⇒ liveafter
256  ].
257
258definition livebefore ≝
259  λglobals: list ident.
260  λint_fun: joint_internal_function ERTLptr globals.
261  λlabel.
262  λliveafter: valuation register_lattice.
263  match lookup ?? (joint_if_code … int_fun) label with
264  [ None      ⇒ rl_bottom
265  | Some stmt ⇒ statement_semantics globals stmt (liveafter label)
266  ].
267
268definition liveafter ≝
269   λglobals: list ident.
270  λint_fun: joint_internal_function ERTLptr globals.
271  λlabel.
272  λliveafter: valuation register_lattice.
273 match lookup ?? (joint_if_code … int_fun) label with
274  [ None      ⇒ rl_bottom
275  | Some stmt ⇒
276    \fold[rl_join,rl_bottom]_{successor ∈ stmt_labels … stmt}
277      (livebefore globals int_fun successor liveafter)
278  ].
279
280definition analyse_liveness ≝
281  λthe_fixpoint: fixpoint_computer. λglobals,int_fun.
282   the_fixpoint ? (liveafter globals int_fun).
283
284definition vertex ≝ register + Register.
285
286definition plives : register → register_lattice → bool ≝
287  λvertex.λprop.set_member ? (eq_identifier RegisterTag) vertex (\fst prop).
288definition hlives : Register → register_lattice → bool ≝
289  λvertex.λprop.set_member ? eq_Register vertex (\snd prop).
290
291definition lives : vertex → register_lattice → bool ≝
292  λvertex.
293  match vertex with
294  [ inl v ⇒ plives v
295  | inr v ⇒ hlives v
296  ].
Note: See TracBrowser for help on using the repository browser.