|
1 (* Author: Tobias Nipkow *) |
|
2 |
|
3 theory Abs_Int_den1 |
|
4 imports Abs_Int_den0_const |
|
5 begin |
|
6 |
|
7 subsection "Backward Analysis of Expressions" |
|
8 |
|
9 class L_top_bot = SL_top + |
|
10 fixes meet :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 65) |
|
11 and Bot :: "'a" |
|
12 assumes meet_le1 [simp]: "x \<sqinter> y \<sqsubseteq> x" |
|
13 and meet_le2 [simp]: "x \<sqinter> y \<sqsubseteq> y" |
|
14 and meet_greatest: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z" |
|
15 assumes bot[simp]: "Bot \<sqsubseteq> x" |
|
16 |
|
17 locale Rep1 = Rep rep for rep :: "'a::L_top_bot \<Rightarrow> 'b set" + |
|
18 assumes inter_rep_subset_rep_meet: "rep a1 \<inter> rep a2 \<subseteq> rep(a1 \<sqinter> a2)" |
|
19 and rep_Bot: "rep Bot = {}" |
|
20 begin |
|
21 |
|
22 lemma in_rep_meet: "x <: a1 \<Longrightarrow> x <: a2 \<Longrightarrow> x <: a1 \<sqinter> a2" |
|
23 by (metis IntI inter_rep_subset_rep_meet set_mp) |
|
24 |
|
25 lemma rep_meet[simp]: "rep(a1 \<sqinter> a2) = rep a1 \<inter> rep a2" |
|
26 by (metis equalityI inter_rep_subset_rep_meet le_inf_iff le_rep meet_le1 meet_le2) |
|
27 |
|
28 end |
|
29 |
|
30 |
|
31 locale Val_abs1 = Val_abs rep num' plus' + Rep1 rep |
|
32 for rep :: "'a::L_top_bot \<Rightarrow> int set" and num' plus' + |
|
33 fixes filter_plus' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a * 'a" |
|
34 and filter_less' :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a * 'a" |
|
35 assumes filter_plus': "filter_plus' a a1 a2 = (a1',a2') \<Longrightarrow> |
|
36 n1 <: a1 \<Longrightarrow> n2 <: a2 \<Longrightarrow> n1+n2 <: a \<Longrightarrow> n1 <: a1' \<and> n2 <: a2'" |
|
37 and filter_less': "filter_less' (n1<n2) a1 a2 = (a1',a2') \<Longrightarrow> |
|
38 n1 <: a1 \<Longrightarrow> n2 <: a2 \<Longrightarrow> n1 <: a1' \<and> n2 <: a2'" |
|
39 |
|
40 datatype 'a up = bot | Up 'a |
|
41 |
|
42 instantiation up :: (SL_top)SL_top |
|
43 begin |
|
44 |
|
45 fun le_up where |
|
46 "Up x \<sqsubseteq> Up y = (x \<sqsubseteq> y)" | |
|
47 "bot \<sqsubseteq> y = True" | |
|
48 "Up _ \<sqsubseteq> bot = False" |
|
49 |
|
50 lemma [simp]: "(x \<sqsubseteq> bot) = (x = bot)" |
|
51 by (cases x) simp_all |
|
52 |
|
53 lemma [simp]: "(Up x \<sqsubseteq> u) = (EX y. u = Up y & x \<sqsubseteq> y)" |
|
54 by (cases u) auto |
|
55 |
|
56 fun join_up where |
|
57 "Up x \<squnion> Up y = Up(x \<squnion> y)" | |
|
58 "bot \<squnion> y = y" | |
|
59 "x \<squnion> bot = x" |
|
60 |
|
61 lemma [simp]: "x \<squnion> bot = x" |
|
62 by (cases x) simp_all |
|
63 |
|
64 |
|
65 definition "Top = Up Top" |
|
66 |
|
67 instance proof |
|
68 case goal1 show ?case by(cases x, simp_all) |
|
69 next |
|
70 case goal2 thus ?case |
|
71 by(cases z, simp, cases y, simp, cases x, auto intro: le_trans) |
|
72 next |
|
73 case goal3 thus ?case by(cases x, simp, cases y, simp_all) |
|
74 next |
|
75 case goal4 thus ?case by(cases y, simp, cases x, simp_all) |
|
76 next |
|
77 case goal5 thus ?case by(cases z, simp, cases y, simp, cases x, simp_all) |
|
78 next |
|
79 case goal6 thus ?case by(cases x, simp_all add: Top_up_def) |
|
80 qed |
|
81 |
|
82 end |
|
83 |
|
84 |
|
85 locale Abs_Int1 = Val_abs1 + |
|
86 fixes pfp :: "('a astate up \<Rightarrow> 'a astate up) \<Rightarrow> 'a astate up \<Rightarrow> 'a astate up" |
|
87 assumes pfp: "f(pfp f x0) \<sqsubseteq> pfp f x0" |
|
88 assumes above: "x0 \<sqsubseteq> pfp f x0" |
|
89 begin |
|
90 |
|
91 (* FIXME avoid duplicating this defn *) |
|
92 abbreviation astate_in_rep (infix "<:" 50) where |
|
93 "s <: S == ALL x. s x <: lookup S x" |
|
94 |
|
95 abbreviation in_rep_up :: "state \<Rightarrow> 'a astate up \<Rightarrow> bool" (infix "<::" 50) where |
|
96 "s <:: S == EX S0. S = Up S0 \<and> s <: S0" |
|
97 |
|
98 lemma in_rep_up_trans: "(s::state) <:: S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <:: T" |
|
99 apply auto |
|
100 by (metis in_mono le_astate_def le_rep lookup_def top) |
|
101 |
|
102 lemma in_rep_join_UpI: "s <:: S1 | s <:: S2 \<Longrightarrow> s <:: S1 \<squnion> S2" |
|
103 by (metis in_rep_up_trans SL_top_class.join_ge1 SL_top_class.join_ge2) |
|
104 |
|
105 fun aval' :: "aexp \<Rightarrow> 'a astate up \<Rightarrow> 'a" ("aval\<^isup>#") where |
|
106 "aval' _ bot = Bot" | |
|
107 "aval' (N n) _ = num' n" | |
|
108 "aval' (V x) (Up S) = lookup S x" | |
|
109 "aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)" |
|
110 |
|
111 lemma aval'_sound: "s <:: S \<Longrightarrow> aval a s <: aval' a S" |
|
112 by (induct a) (auto simp: rep_num' rep_plus') |
|
113 |
|
114 fun afilter :: "aexp \<Rightarrow> 'a \<Rightarrow> 'a astate up \<Rightarrow> 'a astate up" where |
|
115 "afilter (N n) a S = (if n <: a then S else bot)" | |
|
116 "afilter (V x) a S = (case S of bot \<Rightarrow> bot | Up S \<Rightarrow> |
|
117 let a' = lookup S x \<sqinter> a in |
|
118 if a' \<sqsubseteq> Bot then bot else Up(update S x a'))" | |
|
119 "afilter (Plus e1 e2) a S = |
|
120 (let (a1,a2) = filter_plus' a (aval' e1 S) (aval' e2 S) |
|
121 in afilter e1 a1 (afilter e2 a2 S))" |
|
122 |
|
123 text{* The test for @{const Bot} in the @{const V}-case is important: @{const |
|
124 Bot} indicates that a variable has no possible values, i.e.\ that the current |
|
125 program point is unreachable. But then the abstract state should collapse to |
|
126 @{const bot}. Put differently, we maintain the invariant that in an abstract |
|
127 state all variables are mapped to non-@{const Bot} values. Otherwise the |
|
128 (pointwise) join of two abstract states, one of which contains @{const Bot} |
|
129 values, may produce too large a result, thus making the analysis less |
|
130 precise. *} |
|
131 |
|
132 |
|
133 fun bfilter :: "bexp \<Rightarrow> bool \<Rightarrow> 'a astate up \<Rightarrow> 'a astate up" where |
|
134 "bfilter (B bv) res S = (if bv=res then S else bot)" | |
|
135 "bfilter (Not b) res S = bfilter b (\<not> res) S" | |
|
136 "bfilter (And b1 b2) res S = |
|
137 (if res then bfilter b1 True (bfilter b2 True S) |
|
138 else bfilter b1 False S \<squnion> bfilter b2 False S)" | |
|
139 "bfilter (Less e1 e2) res S = |
|
140 (let (res1,res2) = filter_less' res (aval' e1 S) (aval' e2 S) |
|
141 in afilter e1 res1 (afilter e2 res2 S))" |
|
142 |
|
143 lemma afilter_sound: "s <:: S \<Longrightarrow> aval e s <: a \<Longrightarrow> s <:: afilter e a S" |
|
144 proof(induction e arbitrary: a S) |
|
145 case N thus ?case by simp |
|
146 next |
|
147 case (V x) |
|
148 obtain S' where "S = Up S'" and "s <: S'" using `s <:: S` by auto |
|
149 moreover hence "s x <: lookup S' x" by(simp) |
|
150 moreover have "s x <: a" using V by simp |
|
151 ultimately show ?case using V(1) |
|
152 by(simp add: lookup_update Let_def) |
|
153 (metis le_rep emptyE in_rep_meet rep_Bot subset_empty) |
|
154 next |
|
155 case (Plus e1 e2) thus ?case |
|
156 using filter_plus'[OF _ aval'_sound[OF Plus(3)] aval'_sound[OF Plus(3)]] |
|
157 by (auto split: prod.split) |
|
158 qed |
|
159 |
|
160 lemma bfilter_sound: "s <:: S \<Longrightarrow> bv = bval b s \<Longrightarrow> s <:: bfilter b bv S" |
|
161 proof(induction b arbitrary: S bv) |
|
162 case B thus ?case by simp |
|
163 next |
|
164 case (Not b) thus ?case by simp |
|
165 next |
|
166 case (And b1 b2) thus ?case by (auto simp: in_rep_join_UpI) |
|
167 next |
|
168 case (Less e1 e2) thus ?case |
|
169 by (auto split: prod.split) |
|
170 (metis afilter_sound filter_less' aval'_sound Less) |
|
171 qed |
|
172 |
|
173 fun AI :: "com \<Rightarrow> 'a astate up \<Rightarrow> 'a astate up" where |
|
174 "AI SKIP S = S" | |
|
175 "AI (x ::= a) S = |
|
176 (case S of bot \<Rightarrow> bot | Up S \<Rightarrow> Up(update S x (aval' a (Up S))))" | |
|
177 "AI (c1;c2) S = AI c2 (AI c1 S)" | |
|
178 "AI (IF b THEN c1 ELSE c2) S = |
|
179 AI c1 (bfilter b True S) \<squnion> AI c2 (bfilter b False S)" | |
|
180 "AI (WHILE b DO c) S = |
|
181 bfilter b False (pfp (\<lambda>S. AI c (bfilter b True S)) S)" |
|
182 |
|
183 lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <:: S \<Longrightarrow> t <:: AI c S" |
|
184 proof(induction c arbitrary: s t S) |
|
185 case SKIP thus ?case by fastforce |
|
186 next |
|
187 case Assign thus ?case |
|
188 by (auto simp: lookup_update aval'_sound) |
|
189 next |
|
190 case Semi thus ?case by fastforce |
|
191 next |
|
192 case If thus ?case by (auto simp: in_rep_join_UpI bfilter_sound) |
|
193 next |
|
194 case (While b c) |
|
195 let ?P = "pfp (\<lambda>S. AI c (bfilter b True S)) S" |
|
196 { fix s t |
|
197 have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> s <:: ?P \<Longrightarrow> |
|
198 t <:: bfilter b False ?P" |
|
199 proof(induction "WHILE b DO c" s t rule: big_step_induct) |
|
200 case WhileFalse thus ?case by(metis bfilter_sound) |
|
201 next |
|
202 case WhileTrue show ?case |
|
203 by(rule WhileTrue, rule in_rep_up_trans[OF _ pfp], |
|
204 rule While.IH[OF WhileTrue(2)], |
|
205 rule bfilter_sound[OF WhileTrue.prems], simp add: WhileTrue(1)) |
|
206 qed |
|
207 } |
|
208 with in_rep_up_trans[OF `s <:: S` above] While(2,3) AI.simps(5) |
|
209 show ?case by simp |
|
210 qed |
|
211 |
|
212 end |
|
213 |
|
214 end |