source: src/ERTL/liveness.ma @ 3371

Last change on this file since 3371 was 3371, checked in by piccolo, 6 years ago

Modified RTLsemantics and ERTLsemantics. Now the pop frame will set
to undef the carry bit and all RegisterCallerSaved? exept those used to
pass the return value of a function.

Added an overflow check in ERTL_semantics

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