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

43158

11 
"L SKIP X = X" 


12 
"L (x ::= a) X = X{x} \<union> vars a" 


13 
"L (c\<^isub>1; c\<^isub>2) X = (L c\<^isub>1 \<circ> L c\<^isub>2) X" 


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" 


15 
"L (WHILE b DO c) X = vars b \<union> X \<union> L c X"


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 


35 
lemma L_gen_kill: "L c X = (X  kill c) \<union> gen c"


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


57 
case (Semi c1 s1 s2 c2 s3 X t1)

45015

58 
from Semi.IH(1) Semi.prems obtain t2 where

43158

59 
t12: "(c1, t1) \<Rightarrow> t2" and s2t2: "s2 = t2 on L c2 X"


60 
by simp blast

45015

61 
from Semi.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


69 
from IfTrue(3)[OF `s = t on L c1 X`] obtain t' where


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


76 
from IfFalse(3)[OF `s = t on L c2 X`] obtain t' where


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" 


103 
"bury (x ::= a) X = (if x:X then x::= a else SKIP)" 


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


121 
case (Semi c1 s1 s2 c2 s3 X t1)

45015

122 
from Semi.IH(1) Semi.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

45015

125 
from Semi.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


133 
from IfTrue(3)[OF `s = t on L c1 X`] obtain t' where


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


140 
from IfFalse(3)[OF `s = t on L c2 X`] obtain t' where


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 


175 
lemma Semi_bury[simp]: "bc\<^isub>1;bc\<^isub>2 = bury c X \<longleftrightarrow>


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


197 
case (Semi bc1 s1 s2 bc2 s3 c X t1)


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

45015

200 
note IH = Semi.hyps(2,4)


201 
from IH(1)[OF bc1, of t1] Semi.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 


253 
corollary bury_iff: "(bury c UNIV,s) \<Rightarrow> s' \<longleftrightarrow> (c,s) \<Rightarrow> s'"


254 
by(metis final_bury_sound final_bury_sound2)


255 


256 
end
