source: src/ERTLptr/liveness.ma @ 3007

Last change on this file since 3007 was 2949, checked in by sacerdot, 7 years ago

Some advance/repairing in ERTLptrToLTLProof. In particular, we know take in
account that the fixpoint computation only returns a pre-fixpoint.

File size: 9.2 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 _ nparams _ ⇒ 〈set_empty …, set_from_list … (prefix ? nparams RegisterParams)〉
151    | COND r lbl_true ⇒ rl_psingleton r
152    ]
153  | final fin ⇒
154    match fin with
155    [ RETURN ⇒ 〈set_empty …, set_union … (set_from_list … RegisterCalleeSaved) ret_regs〉
156    | GOTO l ⇒ rl_bottom
157    | TAILCALL abs _ _ ⇒ match abs in False with [ ]
158    ]
159  | FCOND abs _ _ _ ⇒ Ⓧabs
160  ].
161
162definition eliminable_step ≝
163λglobals: list ident.
164λl: register_lattice.
165λs: joint_step ERTLptr globals.
166let pliveafter ≝ \fst l in
167let hliveafter ≝ \snd l in
168match s with
169[ step_seq s ⇒
170  match s with
171  [ OP2 op2 r1 r2 r3 ⇒
172    ¬(match op2 with
173      [ Add ⇒ set_member … eq_Register RegisterCarry hliveafter
174      | Addc ⇒ set_member … eq_Register RegisterCarry hliveafter
175      | Sub ⇒ set_member … eq_Register RegisterCarry hliveafter
176      | _ ⇒ false
177      ] ∨ set_member … (eq_identifier …) r1 pliveafter)
178  | OPACCS opaccs dr1 dr2 sr1 sr2 ⇒
179    ¬(set_member … (eq_identifier …) dr1 pliveafter ∨
180      set_member … (eq_identifier …) dr2 pliveafter ∨
181      set_member … eq_Register RegisterCarry hliveafter)
182  | OP1 op1 r1 r2 ⇒
183    ¬set_member … (eq_identifier …) r1 pliveafter
184  | ADDRESS _ _ r1 r2 ⇒
185    ¬(set_member … (eq_identifier …) r1 pliveafter ∨
186      set_member … (eq_identifier …) r2 pliveafter)
187  | LOAD acc_a dpl dph ⇒
188    ¬set_member ? (eq_identifier …) acc_a pliveafter
189  | MOVE pair_reg ⇒
190    ¬match \fst pair_reg with
191      [ PSD p1 ⇒
192        set_member … (eq_identifier …) p1 pliveafter
193      | HDW h1 ⇒
194        set_member … eq_Register h1 hliveafter
195      ]
196  | extension_seq ext ⇒
197    match ext with
198    [ ertlptr_ertl ext' ⇒
199       match ext' with
200       [ ertl_new_frame ⇒ false
201       | ertl_del_frame ⇒ false
202       | ertl_frame_size r ⇒
203         ¬set_member ? (eq_identifier RegisterTag) r pliveafter
204       ]
205    | LOW_ADDRESS r1 l' ⇒
206       ¬set_member ? (eq_identifier RegisterTag) r1 pliveafter
207    | HIGH_ADDRESS r1 l' ⇒
208       ¬set_member ? (eq_identifier RegisterTag) r1 pliveafter
209    ]       
210  | _ ⇒ false
211  ]
212| _ ⇒ false
213].
214
215definition eliminable ≝
216  λglobals: list ident.
217  λl: register_lattice.
218  λs: joint_statement ERTLptr globals.
219  let pliveafter ≝ \fst l in
220  let hliveafter ≝ \snd l in
221  match s with
222  [ sequential seq _ ⇒ eliminable_step … l seq
223  | _ ⇒ false
224  ].
225
226definition statement_semantics: ∀globals: list ident.
227  joint_statement ERTLptr globals → register_lattice → register_lattice ≝
228  λglobals.
229  λstmt.
230  λliveafter.
231  if eliminable globals liveafter stmt then
232    liveafter
233  else
234    rl_join (rl_diff liveafter (defined globals stmt)) (used globals stmt).
235
236definition livebefore:
237  ∀globals: list ident.
238   joint_internal_function ERTLptr globals →
239     valuation register_lattice → valuation register_lattice
240
241  λglobals: list ident.
242  λint_fun: joint_internal_function ERTLptr globals.
243  λliveafter: valuation register_lattice.
244  λlabel.
245  match lookup ?? (joint_if_code … int_fun) label with
246  [ None      ⇒ rl_bottom
247  | Some stmt ⇒ statement_semantics globals stmt (liveafter label)
248  ].
249
250definition liveafter ≝
251   λglobals: list ident.
252  λint_fun: joint_internal_function ERTLptr globals.
253  λlabel.
254  λliveafter: valuation register_lattice.
255 match lookup ?? (joint_if_code … int_fun) label with
256  [ None      ⇒ rl_bottom
257  | Some stmt ⇒
258    \fold[rl_join,rl_bottom]_{successor ∈ stmt_labels … stmt}
259      (livebefore globals int_fun liveafter successor)
260  ].
261
262definition analyse_liveness ≝
263  λthe_fixpoint: fixpoint_computer. λglobals,int_fun.
264   the_fixpoint ? (liveafter globals int_fun).
265
266definition vertex ≝ register + Register.
267
268definition plives : register → register_lattice → bool ≝
269  λvertex.λprop.set_member ? (eq_identifier RegisterTag) vertex (\fst prop).
270definition hlives : Register → register_lattice → bool ≝
271  λvertex.λprop.set_member ? eq_Register vertex (\snd prop).
272
273definition lives : vertex → register_lattice → bool ≝
274  λvertex.
275  match vertex with
276  [ inl v ⇒ plives v
277  | inr v ⇒ hlives v
278  ].
Note: See TracBrowser for help on using the repository browser.