43158
|
1 |
(* Author: Tobias Nipkow *)
|
|
2 |
|
|
3 |
header "Live Variable Analysis"
|
|
4 |
|
|
5 |
theory Live imports Vars Big_Step
|
|
6 |
begin
|
|
7 |
|
|
8 |
subsection "Liveness Analysis"
|
|
9 |
|
45212
|
10 |
fun L :: "com \<Rightarrow> vname set \<Rightarrow> vname set" where
|
51425
|
11 |
"L SKIP X = X" |
|
51396
|
12 |
"L (x ::= a) X = (X - {x}) \<union> vars a" |
|
51425
|
13 |
"L (c\<^isub>1; c\<^isub>2) X = L c\<^isub>1 (L c\<^isub>2 X)" |
|
43158
|
14 |
"L (IF b THEN c\<^isub>1 ELSE c\<^isub>2) X = vars b \<union> L c\<^isub>1 X \<union> L c\<^isub>2 X" |
|
51425
|
15 |
"L (WHILE b DO c) X = vars b \<union> X \<union> L c X"
|
43158
|
16 |
|
|
17 |
value "show (L (''y'' ::= V ''z''; ''x'' ::= Plus (V ''y'') (V ''z'')) {''x''})"
|
|
18 |
|
|
19 |
value "show (L (WHILE Less (V ''x'') (V ''x'') DO ''y'' ::= V ''z'') {''x''})"
|
|
20 |
|
45212
|
21 |
fun "kill" :: "com \<Rightarrow> vname set" where
|
43158
|
22 |
"kill SKIP = {}" |
|
|
23 |
"kill (x ::= a) = {x}" |
|
|
24 |
"kill (c\<^isub>1; c\<^isub>2) = kill c\<^isub>1 \<union> kill c\<^isub>2" |
|
|
25 |
"kill (IF b THEN c\<^isub>1 ELSE c\<^isub>2) = kill c\<^isub>1 \<inter> kill c\<^isub>2" |
|
|
26 |
"kill (WHILE b DO c) = {}"
|
|
27 |
|
45212
|
28 |
fun gen :: "com \<Rightarrow> vname set" where
|
43158
|
29 |
"gen SKIP = {}" |
|
|
30 |
"gen (x ::= a) = vars a" |
|
|
31 |
"gen (c\<^isub>1; c\<^isub>2) = gen c\<^isub>1 \<union> (gen c\<^isub>2 - kill c\<^isub>1)" |
|
|
32 |
"gen (IF b THEN c\<^isub>1 ELSE c\<^isub>2) = vars b \<union> gen c\<^isub>1 \<union> gen c\<^isub>2" |
|
|
33 |
"gen (WHILE b DO c) = vars b \<union> gen c"
|
|
34 |
|
51433
|
35 |
lemma L_gen_kill: "L c X = gen c \<union> (X - kill c)"
|
43158
|
36 |
by(induct c arbitrary:X) auto
|
|
37 |
|
45771
|
38 |
lemma L_While_pfp: "L c (L (WHILE b DO c) X) \<subseteq> L (WHILE b DO c) X"
|
43158
|
39 |
by(auto simp add:L_gen_kill)
|
|
40 |
|
45771
|
41 |
lemma L_While_lpfp:
|
45784
|
42 |
"vars b \<union> X \<union> L c P \<subseteq> P \<Longrightarrow> L (WHILE b DO c) X \<subseteq> P"
|
45771
|
43 |
by(simp add: L_gen_kill)
|
|
44 |
|
43158
|
45 |
|
|
46 |
subsection "Soundness"
|
|
47 |
|
|
48 |
theorem L_sound:
|
|
49 |
"(c,s) \<Rightarrow> s' \<Longrightarrow> s = t on L c X \<Longrightarrow>
|
|
50 |
\<exists> t'. (c,t) \<Rightarrow> t' & s' = t' on X"
|
45015
|
51 |
proof (induction arbitrary: X t rule: big_step_induct)
|
43158
|
52 |
case Skip then show ?case by auto
|
|
53 |
next
|
|
54 |
case Assign then show ?case
|
|
55 |
by (auto simp: ball_Un)
|
|
56 |
next
|
47818
|
57 |
case (Seq c1 s1 s2 c2 s3 X t1)
|
|
58 |
from Seq.IH(1) Seq.prems obtain t2 where
|
43158
|
59 |
t12: "(c1, t1) \<Rightarrow> t2" and s2t2: "s2 = t2 on L c2 X"
|
|
60 |
by simp blast
|
47818
|
61 |
from Seq.IH(2)[OF s2t2] obtain t3 where
|
43158
|
62 |
t23: "(c2, t2) \<Rightarrow> t3" and s3t3: "s3 = t3 on X"
|
|
63 |
by auto
|
|
64 |
show ?case using t12 t23 s3t3 by auto
|
|
65 |
next
|
|
66 |
case (IfTrue b s c1 s' c2)
|
|
67 |
hence "s = t on vars b" "s = t on L c1 X" by auto
|
|
68 |
from bval_eq_if_eq_on_vars[OF this(1)] IfTrue(1) have "bval b t" by simp
|
50009
|
69 |
from IfTrue.IH[OF `s = t on L c1 X`] obtain t' where
|
43158
|
70 |
"(c1, t) \<Rightarrow> t'" "s' = t' on X" by auto
|
|
71 |
thus ?case using `bval b t` by auto
|
|
72 |
next
|
|
73 |
case (IfFalse b s c2 s' c1)
|
|
74 |
hence "s = t on vars b" "s = t on L c2 X" by auto
|
|
75 |
from bval_eq_if_eq_on_vars[OF this(1)] IfFalse(1) have "~bval b t" by simp
|
50009
|
76 |
from IfFalse.IH[OF `s = t on L c2 X`] obtain t' where
|
43158
|
77 |
"(c2, t) \<Rightarrow> t'" "s' = t' on X" by auto
|
|
78 |
thus ?case using `~bval b t` by auto
|
|
79 |
next
|
|
80 |
case (WhileFalse b s c)
|
|
81 |
hence "~ bval b t" by (auto simp: ball_Un) (metis bval_eq_if_eq_on_vars)
|
45770
|
82 |
thus ?case using WhileFalse.prems by auto
|
43158
|
83 |
next
|
|
84 |
case (WhileTrue b s1 c s2 s3 X t1)
|
|
85 |
let ?w = "WHILE b DO c"
|
45770
|
86 |
from `bval b s1` WhileTrue.prems have "bval b t1"
|
43158
|
87 |
by (auto simp: ball_Un) (metis bval_eq_if_eq_on_vars)
|
45771
|
88 |
have "s1 = t1 on L c (L ?w X)" using L_While_pfp WhileTrue.prems
|
43158
|
89 |
by (blast)
|
45015
|
90 |
from WhileTrue.IH(1)[OF this] obtain t2 where
|
43158
|
91 |
"(c, t1) \<Rightarrow> t2" "s2 = t2 on L ?w X" by auto
|
45015
|
92 |
from WhileTrue.IH(2)[OF this(2)] obtain t3 where "(?w,t2) \<Rightarrow> t3" "s3 = t3 on X"
|
43158
|
93 |
by auto
|
|
94 |
with `bval b t1` `(c, t1) \<Rightarrow> t2` show ?case by auto
|
|
95 |
qed
|
|
96 |
|
|
97 |
|
|
98 |
subsection "Program Optimization"
|
|
99 |
|
|
100 |
text{* Burying assignments to dead variables: *}
|
45212
|
101 |
fun bury :: "com \<Rightarrow> vname set \<Rightarrow> com" where
|
43158
|
102 |
"bury SKIP X = SKIP" |
|
50009
|
103 |
"bury (x ::= a) X = (if x \<in> X then x ::= a else SKIP)" |
|
43158
|
104 |
"bury (c\<^isub>1; c\<^isub>2) X = (bury c\<^isub>1 (L c\<^isub>2 X); bury c\<^isub>2 X)" |
|
|
105 |
"bury (IF b THEN c\<^isub>1 ELSE c\<^isub>2) X = IF b THEN bury c\<^isub>1 X ELSE bury c\<^isub>2 X" |
|
|
106 |
"bury (WHILE b DO c) X = WHILE b DO bury c (vars b \<union> X \<union> L c X)"
|
|
107 |
|
|
108 |
text{* We could prove the analogous lemma to @{thm[source]L_sound}, and the
|
|
109 |
proof would be very similar. However, we phrase it as a semantics
|
|
110 |
preservation property: *}
|
|
111 |
|
|
112 |
theorem bury_sound:
|
|
113 |
"(c,s) \<Rightarrow> s' \<Longrightarrow> s = t on L c X \<Longrightarrow>
|
|
114 |
\<exists> t'. (bury c X,t) \<Rightarrow> t' & s' = t' on X"
|
45015
|
115 |
proof (induction arbitrary: X t rule: big_step_induct)
|
43158
|
116 |
case Skip then show ?case by auto
|
|
117 |
next
|
|
118 |
case Assign then show ?case
|
|
119 |
by (auto simp: ball_Un)
|
|
120 |
next
|
47818
|
121 |
case (Seq c1 s1 s2 c2 s3 X t1)
|
|
122 |
from Seq.IH(1) Seq.prems obtain t2 where
|
43158
|
123 |
t12: "(bury c1 (L c2 X), t1) \<Rightarrow> t2" and s2t2: "s2 = t2 on L c2 X"
|
|
124 |
by simp blast
|
47818
|
125 |
from Seq.IH(2)[OF s2t2] obtain t3 where
|
43158
|
126 |
t23: "(bury c2 X, t2) \<Rightarrow> t3" and s3t3: "s3 = t3 on X"
|
|
127 |
by auto
|
|
128 |
show ?case using t12 t23 s3t3 by auto
|
|
129 |
next
|
|
130 |
case (IfTrue b s c1 s' c2)
|
|
131 |
hence "s = t on vars b" "s = t on L c1 X" by auto
|
|
132 |
from bval_eq_if_eq_on_vars[OF this(1)] IfTrue(1) have "bval b t" by simp
|
50009
|
133 |
from IfTrue.IH[OF `s = t on L c1 X`] obtain t' where
|
43158
|
134 |
"(bury c1 X, t) \<Rightarrow> t'" "s' =t' on X" by auto
|
|
135 |
thus ?case using `bval b t` by auto
|
|
136 |
next
|
|
137 |
case (IfFalse b s c2 s' c1)
|
|
138 |
hence "s = t on vars b" "s = t on L c2 X" by auto
|
|
139 |
from bval_eq_if_eq_on_vars[OF this(1)] IfFalse(1) have "~bval b t" by simp
|
50009
|
140 |
from IfFalse.IH[OF `s = t on L c2 X`] obtain t' where
|
43158
|
141 |
"(bury c2 X, t) \<Rightarrow> t'" "s' = t' on X" by auto
|
|
142 |
thus ?case using `~bval b t` by auto
|
|
143 |
next
|
|
144 |
case (WhileFalse b s c)
|
|
145 |
hence "~ bval b t" by (auto simp: ball_Un) (metis bval_eq_if_eq_on_vars)
|
45770
|
146 |
thus ?case using WhileFalse.prems by auto
|
43158
|
147 |
next
|
|
148 |
case (WhileTrue b s1 c s2 s3 X t1)
|
|
149 |
let ?w = "WHILE b DO c"
|
45770
|
150 |
from `bval b s1` WhileTrue.prems have "bval b t1"
|
43158
|
151 |
by (auto simp: ball_Un) (metis bval_eq_if_eq_on_vars)
|
|
152 |
have "s1 = t1 on L c (L ?w X)"
|
45771
|
153 |
using L_While_pfp WhileTrue.prems by blast
|
45015
|
154 |
from WhileTrue.IH(1)[OF this] obtain t2 where
|
43158
|
155 |
"(bury c (L ?w X), t1) \<Rightarrow> t2" "s2 = t2 on L ?w X" by auto
|
45015
|
156 |
from WhileTrue.IH(2)[OF this(2)] obtain t3
|
43158
|
157 |
where "(bury ?w X,t2) \<Rightarrow> t3" "s3 = t3 on X"
|
|
158 |
by auto
|
|
159 |
with `bval b t1` `(bury c (L ?w X), t1) \<Rightarrow> t2` show ?case by auto
|
|
160 |
qed
|
|
161 |
|
|
162 |
corollary final_bury_sound: "(c,s) \<Rightarrow> s' \<Longrightarrow> (bury c UNIV,s) \<Rightarrow> s'"
|
|
163 |
using bury_sound[of c s s' UNIV]
|
|
164 |
by (auto simp: fun_eq_iff[symmetric])
|
|
165 |
|
|
166 |
text{* Now the opposite direction. *}
|
|
167 |
|
|
168 |
lemma SKIP_bury[simp]:
|
|
169 |
"SKIP = bury c X \<longleftrightarrow> c = SKIP | (EX x a. c = x::=a & x \<notin> X)"
|
|
170 |
by (cases c) auto
|
|
171 |
|
|
172 |
lemma Assign_bury[simp]: "x::=a = bury c X \<longleftrightarrow> c = x::=a & x : X"
|
|
173 |
by (cases c) auto
|
|
174 |
|
47818
|
175 |
lemma Seq_bury[simp]: "bc\<^isub>1;bc\<^isub>2 = bury c X \<longleftrightarrow>
|
43158
|
176 |
(EX c\<^isub>1 c\<^isub>2. c = c\<^isub>1;c\<^isub>2 & bc\<^isub>2 = bury c\<^isub>2 X & bc\<^isub>1 = bury c\<^isub>1 (L c\<^isub>2 X))"
|
|
177 |
by (cases c) auto
|
|
178 |
|
|
179 |
lemma If_bury[simp]: "IF b THEN bc1 ELSE bc2 = bury c X \<longleftrightarrow>
|
|
180 |
(EX c1 c2. c = IF b THEN c1 ELSE c2 &
|
|
181 |
bc1 = bury c1 X & bc2 = bury c2 X)"
|
|
182 |
by (cases c) auto
|
|
183 |
|
|
184 |
lemma While_bury[simp]: "WHILE b DO bc' = bury c X \<longleftrightarrow>
|
|
185 |
(EX c'. c = WHILE b DO c' & bc' = bury c' (vars b \<union> X \<union> L c X))"
|
|
186 |
by (cases c) auto
|
|
187 |
|
|
188 |
theorem bury_sound2:
|
|
189 |
"(bury c X,s) \<Rightarrow> s' \<Longrightarrow> s = t on L c X \<Longrightarrow>
|
|
190 |
\<exists> t'. (c,t) \<Rightarrow> t' & s' = t' on X"
|
45015
|
191 |
proof (induction "bury c X" s s' arbitrary: c X t rule: big_step_induct)
|
43158
|
192 |
case Skip then show ?case by auto
|
|
193 |
next
|
|
194 |
case Assign then show ?case
|
|
195 |
by (auto simp: ball_Un)
|
|
196 |
next
|
47818
|
197 |
case (Seq bc1 s1 s2 bc2 s3 c X t1)
|
43158
|
198 |
then obtain c1 c2 where c: "c = c1;c2"
|
|
199 |
and bc2: "bc2 = bury c2 X" and bc1: "bc1 = bury c1 (L c2 X)" by auto
|
47818
|
200 |
note IH = Seq.hyps(2,4)
|
|
201 |
from IH(1)[OF bc1, of t1] Seq.prems c obtain t2 where
|
43158
|
202 |
t12: "(c1, t1) \<Rightarrow> t2" and s2t2: "s2 = t2 on L c2 X" by auto
|
45015
|
203 |
from IH(2)[OF bc2 s2t2] obtain t3 where
|
43158
|
204 |
t23: "(c2, t2) \<Rightarrow> t3" and s3t3: "s3 = t3 on X"
|
|
205 |
by auto
|
|
206 |
show ?case using c t12 t23 s3t3 by auto
|
|
207 |
next
|
|
208 |
case (IfTrue b s bc1 s' bc2)
|
|
209 |
then obtain c1 c2 where c: "c = IF b THEN c1 ELSE c2"
|
|
210 |
and bc1: "bc1 = bury c1 X" and bc2: "bc2 = bury c2 X" by auto
|
|
211 |
have "s = t on vars b" "s = t on L c1 X" using IfTrue.prems c by auto
|
|
212 |
from bval_eq_if_eq_on_vars[OF this(1)] IfTrue(1) have "bval b t" by simp
|
45015
|
213 |
note IH = IfTrue.hyps(3)
|
|
214 |
from IH[OF bc1 `s = t on L c1 X`] obtain t' where
|
43158
|
215 |
"(c1, t) \<Rightarrow> t'" "s' =t' on X" by auto
|
|
216 |
thus ?case using c `bval b t` by auto
|
|
217 |
next
|
|
218 |
case (IfFalse b s bc2 s' bc1)
|
|
219 |
then obtain c1 c2 where c: "c = IF b THEN c1 ELSE c2"
|
|
220 |
and bc1: "bc1 = bury c1 X" and bc2: "bc2 = bury c2 X" by auto
|
|
221 |
have "s = t on vars b" "s = t on L c2 X" using IfFalse.prems c by auto
|
|
222 |
from bval_eq_if_eq_on_vars[OF this(1)] IfFalse(1) have "~bval b t" by simp
|
45015
|
223 |
note IH = IfFalse.hyps(3)
|
|
224 |
from IH[OF bc2 `s = t on L c2 X`] obtain t' where
|
43158
|
225 |
"(c2, t) \<Rightarrow> t'" "s' =t' on X" by auto
|
|
226 |
thus ?case using c `~bval b t` by auto
|
|
227 |
next
|
|
228 |
case (WhileFalse b s c)
|
|
229 |
hence "~ bval b t" by (auto simp: ball_Un dest: bval_eq_if_eq_on_vars)
|
|
230 |
thus ?case using WhileFalse by auto
|
|
231 |
next
|
|
232 |
case (WhileTrue b s1 bc' s2 s3 c X t1)
|
|
233 |
then obtain c' where c: "c = WHILE b DO c'"
|
|
234 |
and bc': "bc' = bury c' (vars b \<union> X \<union> L c' X)" by auto
|
|
235 |
let ?w = "WHILE b DO c'"
|
|
236 |
from `bval b s1` WhileTrue.prems c have "bval b t1"
|
|
237 |
by (auto simp: ball_Un) (metis bval_eq_if_eq_on_vars)
|
45015
|
238 |
note IH = WhileTrue.hyps(3,5)
|
43158
|
239 |
have "s1 = t1 on L c' (L ?w X)"
|
45771
|
240 |
using L_While_pfp WhileTrue.prems c by blast
|
45015
|
241 |
with IH(1)[OF bc', of t1] obtain t2 where
|
43158
|
242 |
"(c', t1) \<Rightarrow> t2" "s2 = t2 on L ?w X" by auto
|
45015
|
243 |
from IH(2)[OF WhileTrue.hyps(6), of t2] c this(2) obtain t3
|
43158
|
244 |
where "(?w,t2) \<Rightarrow> t3" "s3 = t3 on X"
|
|
245 |
by auto
|
|
246 |
with `bval b t1` `(c', t1) \<Rightarrow> t2` c show ?case by auto
|
|
247 |
qed
|
|
248 |
|
|
249 |
corollary final_bury_sound2: "(bury c UNIV,s) \<Rightarrow> s' \<Longrightarrow> (c,s) \<Rightarrow> s'"
|
|
250 |
using bury_sound2[of c UNIV]
|
|
251 |
by (auto simp: fun_eq_iff[symmetric])
|
|
252 |
|
51433
|
253 |
corollary bury_sim: "bury c UNIV \<sim> c"
|
43158
|
254 |
by(metis final_bury_sound final_bury_sound2)
|
|
255 |
|
|
256 |
end
|