47613

1 
(* Author: Tobias Nipkow *)


2 


3 
theory Abs_Int2


4 
imports Abs_Int1


5 
begin


6 


7 
instantiation prod :: (preord,preord) preord


8 
begin


9 


10 
definition "le_prod p1 p2 = (fst p1 \<sqsubseteq> fst p2 \<and> snd p1 \<sqsubseteq> snd p2)"


11 


12 
instance


13 
proof


14 
case goal1 show ?case by(simp add: le_prod_def)


15 
next


16 
case goal2 thus ?case unfolding le_prod_def by(metis le_trans)


17 
qed


18 


19 
end


20 


21 


22 
subsection "Backward Analysis of Expressions"


23 

49396

24 
class lattice = semilattice + bot +

47613

25 
fixes meet :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 65)


26 
assumes meet_le1 [simp]: "x \<sqinter> y \<sqsubseteq> x"


27 
and meet_le2 [simp]: "x \<sqinter> y \<sqsubseteq> y"


28 
and meet_greatest: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z"


29 
begin


30 


31 
lemma mono_meet: "x \<sqsubseteq> x' \<Longrightarrow> y \<sqsubseteq> y' \<Longrightarrow> x \<sqinter> y \<sqsubseteq> x' \<sqinter> y'"


32 
by (metis meet_greatest meet_le1 meet_le2 le_trans)


33 


34 
end


35 


36 
locale Val_abs1_gamma =

49396

37 
Gamma where \<gamma> = \<gamma> for \<gamma> :: "'av::lattice \<Rightarrow> val set" +

47613

38 
assumes inter_gamma_subset_gamma_meet:


39 
"\<gamma> a1 \<inter> \<gamma> a2 \<subseteq> \<gamma>(a1 \<sqinter> a2)"

49396

40 
and gamma_bot[simp]: "\<gamma> \<bottom> = {}"

47613

41 
begin


42 


43 
lemma in_gamma_meet: "x : \<gamma> a1 \<Longrightarrow> x : \<gamma> a2 \<Longrightarrow> x : \<gamma>(a1 \<sqinter> a2)"


44 
by (metis IntI inter_gamma_subset_gamma_meet set_mp)


45 


46 
lemma gamma_meet[simp]: "\<gamma>(a1 \<sqinter> a2) = \<gamma> a1 \<inter> \<gamma> a2"


47 
by (metis equalityI inter_gamma_subset_gamma_meet le_inf_iff mono_gamma meet_le1 meet_le2)


48 


49 
end


50 


51 


52 
locale Val_abs1 =


53 
Val_abs1_gamma where \<gamma> = \<gamma>

49396

54 
for \<gamma> :: "'av::lattice \<Rightarrow> val set" +

47613

55 
fixes test_num' :: "val \<Rightarrow> 'av \<Rightarrow> bool"


56 
and filter_plus' :: "'av \<Rightarrow> 'av \<Rightarrow> 'av \<Rightarrow> 'av * 'av"


57 
and filter_less' :: "bool \<Rightarrow> 'av \<Rightarrow> 'av \<Rightarrow> 'av * 'av"

51036

58 
assumes test_num': "test_num' n a = (n : \<gamma> a)"

47613

59 
and filter_plus': "filter_plus' a a1 a2 = (b1,b2) \<Longrightarrow>

51036

60 
n1 : \<gamma> a1 \<Longrightarrow> n2 : \<gamma> a2 \<Longrightarrow> n1+n2 : \<gamma> a \<Longrightarrow> n1 : \<gamma> b1 \<and> n2 : \<gamma> b2"


61 
and filter_less': "filter_less' (n1<n2) a1 a2 = (b1,b2) \<Longrightarrow>


62 
n1 : \<gamma> a1 \<Longrightarrow> n2 : \<gamma> a2 \<Longrightarrow> n1 : \<gamma> b1 \<and> n2 : \<gamma> b2"

47613

63 


64 


65 
locale Abs_Int1 =

49396

66 
Val_abs1 where \<gamma> = \<gamma> for \<gamma> :: "'av::lattice \<Rightarrow> val set"

47613

67 
begin


68 


69 
lemma in_gamma_join_UpI:

49396

70 
"S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> s : \<gamma>\<^isub>o S1 \<or> s : \<gamma>\<^isub>o S2 \<Longrightarrow> s : \<gamma>\<^isub>o(S1 \<squnion> S2)"


71 
by (metis (hide_lams, no_types) semilatticeL_class.join_ge1 semilatticeL_class.join_ge2 mono_gamma_o subsetD)

47613

72 


73 
fun aval'' :: "aexp \<Rightarrow> 'av st option \<Rightarrow> 'av" where


74 
"aval'' e None = \<bottom>" 


75 
"aval'' e (Some sa) = aval' e sa"


76 

49396

77 
lemma aval''_sound: "s : \<gamma>\<^isub>o S \<Longrightarrow> S \<in> L X \<Longrightarrow> vars a \<subseteq> X \<Longrightarrow> aval a s : \<gamma>(aval'' a S)"


78 
by(simp add: L_option_def L_st_def aval'_sound split: option.splits)

47613

79 


80 
subsubsection "Backward analysis"


81 


82 
fun afilter :: "aexp \<Rightarrow> 'av \<Rightarrow> 'av st option \<Rightarrow> 'av st option" where

51036

83 
"afilter (N n) a S = (if test_num' n a then S else None)" 

47613

84 
"afilter (V x) a S = (case S of None \<Rightarrow> None  Some S \<Rightarrow>


85 
let a' = fun S x \<sqinter> a in


86 
if a' \<sqsubseteq> \<bottom> then None else Some(update S x a'))" 


87 
"afilter (Plus e1 e2) a S =

51036

88 
(let (a1,a2) = filter_plus' a (aval'' e1 S) (aval'' e2 S)


89 
in afilter e1 a1 (afilter e2 a2 S))"

47613

90 


91 
text{* The test for @{const bot} in the @{const V}case is important: @{const


92 
bot} indicates that a variable has no possible values, i.e.\ that the current


93 
program point is unreachable. But then the abstract state should collapse to


94 
@{const None}. Put differently, we maintain the invariant that in an abstract


95 
state of the form @{term"Some s"}, all variables are mapped to non@{const


96 
bot} values. Otherwise the (pointwise) join of two abstract states, one of


97 
which contains @{const bot} values, may produce too large a result, thus


98 
making the analysis less precise. *}


99 


100 


101 
fun bfilter :: "bexp \<Rightarrow> bool \<Rightarrow> 'av st option \<Rightarrow> 'av st option" where


102 
"bfilter (Bc v) res S = (if v=res then S else None)" 


103 
"bfilter (Not b) res S = bfilter b (\<not> res) S" 


104 
"bfilter (And b1 b2) res S =


105 
(if res then bfilter b1 True (bfilter b2 True S)


106 
else bfilter b1 False S \<squnion> bfilter b2 False S)" 


107 
"bfilter (Less e1 e2) res S =

51037

108 
(let (a1,a2) = filter_less' res (aval'' e1 S) (aval'' e2 S)


109 
in afilter e1 a1 (afilter e2 a2 S))"

47613

110 

49396

111 
lemma afilter_in_L: "S \<in> L X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow> afilter e a S \<in> L X"

47613

112 
by(induction e arbitrary: a S)

49396

113 
(auto simp: Let_def update_def L_st_def

47613

114 
split: option.splits prod.split)


115 

49396

116 
lemma afilter_sound: "S \<in> L X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow>

47613

117 
s : \<gamma>\<^isub>o S \<Longrightarrow> aval e s : \<gamma> a \<Longrightarrow> s : \<gamma>\<^isub>o (afilter e a S)"


118 
proof(induction e arbitrary: a S)


119 
case N thus ?case by simp (metis test_num')


120 
next


121 
case (V x)

49497

122 
obtain S' where "S = Some S'" and "s : \<gamma>\<^isub>s S'" using `s : \<gamma>\<^isub>o S`

47613

123 
by(auto simp: in_gamma_option_iff)


124 
moreover hence "s x : \<gamma> (fun S' x)"

49396

125 
using V(1,2) by(simp add: \<gamma>_st_def L_st_def)

47613

126 
moreover have "s x : \<gamma> a" using V by simp


127 
ultimately show ?case using V(3)


128 
by(simp add: Let_def \<gamma>_st_def)

49396

129 
(metis mono_gamma emptyE in_gamma_meet gamma_bot subset_empty)

47613

130 
next


131 
case (Plus e1 e2) thus ?case


132 
using filter_plus'[OF _ aval''_sound[OF Plus.prems(3)] aval''_sound[OF Plus.prems(3)]]

49396

133 
by (auto simp: afilter_in_L split: prod.split)

47613

134 
qed


135 

49396

136 
lemma bfilter_in_L: "S \<in> L X \<Longrightarrow> vars b \<subseteq> X \<Longrightarrow> bfilter b bv S \<in> L X"


137 
by(induction b arbitrary: bv S)(auto simp: afilter_in_L split: prod.split)

47613

138 

49396

139 
lemma bfilter_sound: "S \<in> L X \<Longrightarrow> vars b \<subseteq> X \<Longrightarrow>

47613

140 
s : \<gamma>\<^isub>o S \<Longrightarrow> bv = bval b s \<Longrightarrow> s : \<gamma>\<^isub>o(bfilter b bv S)"


141 
proof(induction b arbitrary: S bv)


142 
case Bc thus ?case by simp


143 
next


144 
case (Not b) thus ?case by simp


145 
next


146 
case (And b1 b2) thus ?case

49396

147 
by simp (metis And(1) And(2) bfilter_in_L in_gamma_join_UpI)

47613

148 
next


149 
case (Less e1 e2) thus ?case


150 
by(auto split: prod.split)

49396

151 
(metis (lifting) afilter_in_L afilter_sound aval''_sound filter_less')

47613

152 
qed


153 


154 


155 
fun step' :: "'av st option \<Rightarrow> 'av st option acom \<Rightarrow> 'av st option acom"


156 
where


157 
"step' S (SKIP {P}) = (SKIP {S})" 


158 
"step' S (x ::= e {P}) =


159 
x ::= e {case S of None \<Rightarrow> None  Some S \<Rightarrow> Some(update S x (aval' e S))}" 


160 
"step' S (C1; C2) = step' S C1; step' (post C1) C2" 

49344

161 
"step' S (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) =


162 
(let P1' = bfilter b True S; C1' = step' P1 C1; P2' = bfilter b False S; C2' = step' P2 C2


163 
in IF b THEN {P1'} C1' ELSE {P2'} C2' {post C1 \<squnion> post C2})" 


164 
"step' S ({I} WHILE b DO {p} C {Q}) =

47613

165 
{S \<squnion> post C}

49095

166 
WHILE b DO {bfilter b True I} step' p C


167 
{bfilter b False I}"

47613

168 


169 
definition AI :: "com \<Rightarrow> 'av st option acom option" where

51036

170 
"AI c = pfp (step' \<top>\<^bsub>vars c\<^esub>) (bot c)"

47613

171 


172 
lemma strip_step'[simp]: "strip(step' S c) = strip c"


173 
by(induct c arbitrary: S) (simp_all add: Let_def)


174 


175 


176 
subsubsection "Soundness"


177 


178 
lemma in_gamma_update:

49497

179 
"\<lbrakk> s : \<gamma>\<^isub>s S; i : \<gamma> a \<rbrakk> \<Longrightarrow> s(x := i) : \<gamma>\<^isub>s(update S x a)"

47613

180 
by(simp add: \<gamma>_st_def)


181 

50986

182 
lemma step_step': "C \<in> L X \<Longrightarrow> S \<in> L X \<Longrightarrow> step (\<gamma>\<^isub>o S) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c (step' S C)"


183 
proof(induction C arbitrary: S)


184 
case SKIP thus ?case by auto

47613

185 
next


186 
case Assign thus ?case

50986

187 
by (fastforce simp: L_st_def intro: aval'_sound in_gamma_update split: option.splits)

47613

188 
next

50986

189 
case Seq thus ?case by auto

47613

190 
next

50986

191 
case (If b _ C1 _ C2)


192 
hence 0: "post C1 \<sqsubseteq> post C1 \<squnion> post C2 \<and> post C2 \<sqsubseteq> post C1 \<squnion> post C2"


193 
by(simp, metis post_in_L join_ge1 join_ge2)


194 
have "vars b \<subseteq> X" using If.prems by simp


195 
note vars = `S \<in> L X` `vars b \<subseteq> X`


196 
show ?case using If 0


197 
by (auto simp: mono_gamma_o bfilter_sound[OF vars] bfilter_in_L[OF vars])

47613

198 
next

50986

199 
case (While I b)


200 
hence vars: "I \<in> L X" "vars b \<subseteq> X" by simp_all


201 
thus ?case using While


202 
by (auto simp: mono_gamma_o bfilter_sound[OF vars] bfilter_in_L[OF vars])

47613

203 
qed


204 

50986

205 
lemma step'_in_L[simp]: "\<lbrakk> C \<in> L X; S \<in> L X \<rbrakk> \<Longrightarrow> step' S C \<in> L X"

47613

206 
proof(induction C arbitrary: S)

49396

207 
case Assign thus ?case by(simp add: L_option_def L_st_def update_def split: option.splits)


208 
qed (auto simp add: bfilter_in_L)

47613

209 

50986

210 
lemma AI_sound: "AI c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C"

47613

211 
proof(simp add: CS_def AI_def)

51036

212 
assume 1: "pfp (step' (top(vars c))) (bot c) = Some C"

49396

213 
have "C \<in> L(vars c)"

49464

214 
by(rule pfp_inv[where P = "%C. C \<in> L(vars c)", OF 1 _ bot_in_L])

49396

215 
(erule step'_in_L[OF _ top_in_L])

51036

216 
have pfp': "step' (top(vars c)) C \<sqsubseteq> C" by(rule pfp_pfp[OF 1])


217 
have 2: "step (\<gamma>\<^isub>o(top(vars c))) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C"

50986

218 
proof(rule order_trans)

51036

219 
show "step (\<gamma>\<^isub>o (top(vars c))) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c (step' (top(vars c)) C)"

50986

220 
by(rule step_step'[OF `C \<in> L(vars c)` top_in_L])

51036

221 
show "\<gamma>\<^isub>c (step' (top(vars c)) C) \<le> \<gamma>\<^isub>c C"

50986

222 
by(rule mono_gamma_c[OF pfp'])

47613

223 
qed

50986

224 
have 3: "strip (\<gamma>\<^isub>c C) = c" by(simp add: strip_pfp[OF _ 1])

51036

225 
have "lfp c (step (\<gamma>\<^isub>o(top(vars c)))) \<le> \<gamma>\<^isub>c C"


226 
by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o(top(vars c)))", OF 3 2])

50986

227 
thus "lfp c (step UNIV) \<le> \<gamma>\<^isub>c C" by simp

47613

228 
qed


229 


230 
end


231 


232 


233 
subsubsection "Monotonicity"


234 


235 
locale Abs_Int1_mono = Abs_Int1 +


236 
assumes mono_plus': "a1 \<sqsubseteq> b1 \<Longrightarrow> a2 \<sqsubseteq> b2 \<Longrightarrow> plus' a1 a2 \<sqsubseteq> plus' b1 b2"


237 
and mono_filter_plus': "a1 \<sqsubseteq> b1 \<Longrightarrow> a2 \<sqsubseteq> b2 \<Longrightarrow> r \<sqsubseteq> r' \<Longrightarrow>


238 
filter_plus' r a1 a2 \<sqsubseteq> filter_plus' r' b1 b2"


239 
and mono_filter_less': "a1 \<sqsubseteq> b1 \<Longrightarrow> a2 \<sqsubseteq> b2 \<Longrightarrow>


240 
filter_less' bv a1 a2 \<sqsubseteq> filter_less' bv b1 b2"


241 
begin


242 


243 
lemma mono_aval':

49396

244 
"S1 \<sqsubseteq> S2 \<Longrightarrow> S1 \<in> L X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow> aval' e S1 \<sqsubseteq> aval' e S2"


245 
by(induction e) (auto simp: le_st_def mono_plus' L_st_def)

47613

246 


247 
lemma mono_aval'':

49396

248 
"S1 \<sqsubseteq> S2 \<Longrightarrow> S1 \<in> L X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow> aval'' e S1 \<sqsubseteq> aval'' e S2"

47613

249 
apply(cases S1)


250 
apply simp


251 
apply(cases S2)


252 
apply simp


253 
by (simp add: mono_aval')


254 

49396

255 
lemma mono_afilter: "S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow>

47613

256 
r1 \<sqsubseteq> r2 \<Longrightarrow> S1 \<sqsubseteq> S2 \<Longrightarrow> afilter e r1 S1 \<sqsubseteq> afilter e r2 S2"


257 
apply(induction e arbitrary: r1 r2 S1 S2)


258 
apply(auto simp: test_num' Let_def mono_meet split: option.splits prod.splits)


259 
apply (metis mono_gamma subsetD)

49396

260 
apply(drule (2) mono_fun_L)

47613

261 
apply (metis mono_meet le_trans)

49396

262 
apply(metis mono_aval'' mono_filter_plus'[simplified le_prod_def] fst_conv snd_conv afilter_in_L)

47613

263 
done


264 

49396

265 
lemma mono_bfilter: "S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> vars b \<subseteq> X \<Longrightarrow>

47613

266 
S1 \<sqsubseteq> S2 \<Longrightarrow> bfilter b bv S1 \<sqsubseteq> bfilter b bv S2"


267 
apply(induction b arbitrary: bv S1 S2)


268 
apply(simp)


269 
apply(simp)


270 
apply simp

49396

271 
apply(metis join_least le_trans[OF _ join_ge1] le_trans[OF _ join_ge2] bfilter_in_L)

47613

272 
apply (simp split: prod.splits)

49396

273 
apply(metis mono_aval'' mono_afilter mono_filter_less'[simplified le_prod_def] fst_conv snd_conv afilter_in_L)

47613

274 
done


275 

49396

276 
theorem mono_step': "S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> C1 \<in> L X \<Longrightarrow> C2 \<in> L X \<Longrightarrow>

47613

277 
S1 \<sqsubseteq> S2 \<Longrightarrow> C1 \<sqsubseteq> C2 \<Longrightarrow> step' S1 C1 \<sqsubseteq> step' S2 C2"


278 
apply(induction C1 C2 arbitrary: S1 S2 rule: le_acom.induct)


279 
apply (auto simp: Let_def mono_bfilter mono_aval' mono_post

49396

280 
le_join_disj le_join_disj[OF post_in_L post_in_L] bfilter_in_L

47613

281 
split: option.split)


282 
done


283 

51036

284 
lemma mono_step'_top: "C1 \<in> L X \<Longrightarrow> C2 \<in> L X \<Longrightarrow>


285 
C1 \<sqsubseteq> C2 \<Longrightarrow> step' (top X) C1 \<sqsubseteq> step' (top X) C2"

49396

286 
by (metis top_in_L mono_step' preord_class.le_refl)

47613

287 


288 
end


289 


290 
end
