source: src/ERTL/liveness.ma @ 3145

Last change on this file since 3145 was 3037, checked in by tranquil, 7 years ago
  • ADDRESS joint instruction now has also an offset
  • corrected call to pointer (needed to clear the accumulator)
  • now we make sure globals contain also function names

LINToASM will be fixed in an upcoming commit

File size: 8.7 KB
Line 
1include "ASM/Util.ma".
2include "ERTL/ERTL.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 ERTL 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         [ 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      (* Potentially destroys all caller-save hardware registers. *)
81      ]
82    | CALL _ _ _ ⇒ 〈set_empty …, set_from_list … RegisterCallerSaved〉
83    | COND r lbl_true ⇒ rl_bottom
84    | COST_LABEL clabel ⇒ rl_bottom
85    ]
86  | final _ ⇒ rl_bottom
87  | FCOND abs _ _ _ ⇒ Ⓧabs
88  ].
89
90definition ret_regs ≝ set_from_list … RegisterRets.
91
92definition rl_arg : psd_argument → register_lattice ≝
93  λarg.match arg with
94  [ Imm _ ⇒ rl_bottom
95  | Reg r ⇒ rl_psingleton r
96  ].
97
98definition used ≝
99  λglobals: list ident.
100  λs: joint_statement ERTL globals.
101  match s with
102  [ sequential seq l ⇒
103    match seq with
104    [ step_seq s ⇒
105      match s with
106      [ OP2 op2 acc_a r1 r2 ⇒
107        rl_join (rl_join (rl_arg r1) (rl_arg r2))
108          (match op2 with
109            [ Addc ⇒ rl_hsingleton RegisterCarry
110            | Sub ⇒ rl_hsingleton RegisterCarry
111            | _ ⇒ rl_bottom
112            ])
113      (* acc_a and acc_b *)
114      | OPACCS opaccs dr1 dr2 sr1 sr2 ⇒
115        rl_join (rl_arg sr1) (rl_arg sr2)
116      | OP1 op1 r1 r2 ⇒ rl_psingleton r2
117      | LOAD acc_a dpl dph ⇒ rl_join (rl_arg dpl) (rl_arg dph)
118      | STORE acc_a dpl dph ⇒
119        rl_join (rl_join (rl_arg acc_a) (rl_arg dpl)) (rl_arg dph)
120      | PUSH r ⇒ rl_arg r
121      | MOVE pair_reg ⇒
122        let r2 ≝ \snd pair_reg in
123        match r2 with
124        [ Reg p ⇒
125          match p with
126          [ PSD r ⇒ rl_psingleton r
127          | HDW r ⇒ rl_hsingleton r
128          ]
129        | Imm _ ⇒ rl_bottom
130        ]
131      | extension_seq ext ⇒
132        match ext with
133         [ ertl_new_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
134         | ertl_del_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
135         | ertl_frame_size r ⇒ rl_bottom ]
136      (* Reads the hardware registers that are used to pass parameters. *)
137      | _ ⇒ rl_bottom
138      ]
139    | COST_LABEL clabel ⇒ rl_bottom
140    | CALL f nparams _ ⇒
141      rl_join (match f with
142      [ inl _ ⇒ rl_bottom
143      | inr pr ⇒ rl_join (rl_arg (\fst pr)) (rl_arg (\snd pr))
144      ]) 〈set_empty …, set_from_list … (prefix ? nparams RegisterParams)〉
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 False with [ ]
152    ]
153  | FCOND abs _ _ _ ⇒ Ⓧabs
154  ].
155
156definition eliminable_step ≝
157λglobals: list ident.
158λl: register_lattice.
159λs: joint_step ERTL globals.
160let pliveafter ≝ \fst l in
161let hliveafter ≝ \snd l in
162match s with
163[ step_seq s ⇒
164  match s with
165  [ OP2 op2 r1 r2 r3 ⇒
166    ¬(match op2 with
167      [ Add ⇒ set_member … eq_Register RegisterCarry hliveafter
168      | Addc ⇒ set_member … eq_Register RegisterCarry hliveafter
169      | Sub ⇒ set_member … eq_Register RegisterCarry hliveafter
170      | _ ⇒ false
171      ] ∨ set_member … (eq_identifier …) r1 pliveafter)
172  | OPACCS opaccs dr1 dr2 sr1 sr2 ⇒
173    ¬(set_member … (eq_identifier …) dr1 pliveafter ∨
174      set_member … (eq_identifier …) dr2 pliveafter ∨
175      set_member … eq_Register RegisterCarry hliveafter)
176  | OP1 op1 r1 r2 ⇒
177    ¬set_member … (eq_identifier …) r1 pliveafter
178  | ADDRESS _ _ _ r1 r2 ⇒
179    ¬(set_member … (eq_identifier …) r1 pliveafter ∨
180      set_member … (eq_identifier …) r2 pliveafter)
181  | LOAD acc_a dpl dph ⇒
182    ¬set_member ? (eq_identifier …) acc_a pliveafter
183  | MOVE pair_reg ⇒
184    ¬match \fst pair_reg with
185      [ PSD p1 ⇒
186        set_member … (eq_identifier …) p1 pliveafter
187      | HDW h1 ⇒
188        set_member … eq_Register h1 hliveafter
189      ]
190  | extension_seq ext ⇒
191    match ext with
192     [ ertl_new_frame ⇒ false
193     | ertl_del_frame ⇒ false
194     | ertl_frame_size r ⇒
195       ¬set_member ? (eq_identifier RegisterTag) r pliveafter
196     ]
197  | _ ⇒ false
198  ]
199| _ ⇒ false
200].
201
202definition eliminable ≝
203  λglobals: list ident.
204  λl: register_lattice.
205  λs: joint_statement ERTL globals.
206  let pliveafter ≝ \fst l in
207  let hliveafter ≝ \snd l in
208  match s with
209  [ sequential seq _ ⇒ eliminable_step … l seq
210  | _ ⇒ false
211  ].
212
213definition statement_semantics: ∀globals: list ident.
214  joint_statement ERTL globals → register_lattice → register_lattice ≝
215  λglobals.
216  λstmt.
217  λliveafter.
218  if eliminable globals liveafter stmt then
219    liveafter
220  else
221    rl_join (rl_diff liveafter (defined globals stmt)) (used globals stmt).
222
223definition livebefore:
224  ∀globals: list ident.
225   joint_internal_function ERTL globals →
226     valuation register_lattice → valuation register_lattice
227
228  λglobals: list ident.
229  λint_fun: joint_internal_function ERTL globals.
230  λliveafter: valuation register_lattice.
231  λlabel.
232  match lookup ?? (joint_if_code … int_fun) label with
233  [ None      ⇒ rl_bottom
234  | Some stmt ⇒ statement_semantics globals stmt (liveafter label)
235  ].
236
237definition liveafter ≝
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 ⇒
245    \fold[rl_join,rl_bottom]_{successor ∈ stmt_labels … stmt}
246      (livebefore globals int_fun liveafter successor)
247  ].
248
249definition analyse_liveness ≝
250  λthe_fixpoint: fixpoint_computer. λglobals,int_fun.
251   the_fixpoint ? (liveafter globals int_fun).
252
253definition vertex ≝ register + Register.
254
255definition plives : register → register_lattice → bool ≝
256  λvertex.λprop.set_member ? (eq_identifier RegisterTag) vertex (\fst prop).
257definition hlives : Register → register_lattice → bool ≝
258  λvertex.λprop.set_member ? eq_Register vertex (\snd prop).
259
260definition lives : vertex → register_lattice → bool ≝
261  λvertex.
262  match vertex with
263  [ inl v ⇒ plives v
264  | inr v ⇒ hlives v
265  ].
Note: See TracBrowser for help on using the repository browser.