|
1 (* Title: HOL/MicroJava/BV/Effect.thy |
|
2 ID: $Id$ |
|
3 Author: Gerwin Klein |
|
4 Copyright 2000 Technische Universitaet Muenchen |
|
5 *) |
|
6 |
|
7 header {* Effect of Instructions on the State Type *} |
|
8 |
|
9 theory Effect = JVMType + JVMExec: |
|
10 |
|
11 types |
|
12 succ_type = "(p_count \<times> state_type option) list" |
|
13 |
|
14 text {* Program counter of successor instructions: *} |
|
15 consts |
|
16 succs :: "instr => p_count => p_count list" |
|
17 primrec |
|
18 "succs (Load idx) pc = [pc+1]" |
|
19 "succs (Store idx) pc = [pc+1]" |
|
20 "succs (LitPush v) pc = [pc+1]" |
|
21 "succs (Getfield F C) pc = [pc+1]" |
|
22 "succs (Putfield F C) pc = [pc+1]" |
|
23 "succs (New C) pc = [pc+1]" |
|
24 "succs (Checkcast C) pc = [pc+1]" |
|
25 "succs Pop pc = [pc+1]" |
|
26 "succs Dup pc = [pc+1]" |
|
27 "succs Dup_x1 pc = [pc+1]" |
|
28 "succs Dup_x2 pc = [pc+1]" |
|
29 "succs Swap pc = [pc+1]" |
|
30 "succs IAdd pc = [pc+1]" |
|
31 "succs (Ifcmpeq b) pc = [pc+1, nat (int pc + b)]" |
|
32 "succs (Goto b) pc = [nat (int pc + b)]" |
|
33 "succs Return pc = [pc]" |
|
34 "succs (Invoke C mn fpTs) pc = [pc+1]" |
|
35 "succs Throw pc = [pc]" |
|
36 |
|
37 text "Effect of instruction on the state type:" |
|
38 consts |
|
39 eff' :: "instr \<times> jvm_prog \<times> state_type => state_type" |
|
40 |
|
41 recdef eff' "{}" |
|
42 "eff' (Load idx, G, (ST, LT)) = (ok_val (LT ! idx) # ST, LT)" |
|
43 "eff' (Store idx, G, (ts#ST, LT)) = (ST, LT[idx:= OK ts])" |
|
44 "eff' (LitPush v, G, (ST, LT)) = (the (typeof (\<lambda>v. None) v) # ST, LT)" |
|
45 "eff' (Getfield F C, G, (oT#ST, LT)) = (snd (the (field (G,C) F)) # ST, LT)" |
|
46 "eff' (Putfield F C, G, (vT#oT#ST, LT)) = (ST,LT)" |
|
47 "eff' (New C, G, (ST,LT)) = (Class C # ST, LT)" |
|
48 "eff' (Checkcast C, G, (RefT rt#ST,LT)) = (Class C # ST,LT)" |
|
49 "eff' (Pop, G, (ts#ST,LT)) = (ST,LT)" |
|
50 "eff' (Dup, G, (ts#ST,LT)) = (ts#ts#ST,LT)" |
|
51 "eff' (Dup_x1, G, (ts1#ts2#ST,LT)) = (ts1#ts2#ts1#ST,LT)" |
|
52 "eff' (Dup_x2, G, (ts1#ts2#ts3#ST,LT)) = (ts1#ts2#ts3#ts1#ST,LT)" |
|
53 "eff' (Swap, G, (ts1#ts2#ST,LT)) = (ts2#ts1#ST,LT)" |
|
54 "eff' (IAdd, G, (PrimT Integer#PrimT Integer#ST,LT)) |
|
55 = (PrimT Integer#ST,LT)" |
|
56 "eff' (Ifcmpeq b, G, (ts1#ts2#ST,LT)) = (ST,LT)" |
|
57 "eff' (Goto b, G, s) = s" |
|
58 -- "Return has no successor instruction in the same method" |
|
59 "eff' (Return, G, s) = s" |
|
60 -- "Throw always terminates abruptly" |
|
61 "eff' (Throw, G, s) = s" |
|
62 "eff' (Invoke C mn fpTs, G, (ST,LT)) = (let ST' = drop (length fpTs) ST |
|
63 in (fst (snd (the (method (G,C) (mn,fpTs))))#(tl ST'),LT))" |
|
64 |
|
65 |
|
66 consts |
|
67 match_any :: "jvm_prog \<Rightarrow> p_count \<Rightarrow> exception_table \<Rightarrow> cname list" |
|
68 primrec |
|
69 "match_any G pc [] = []" |
|
70 "match_any G pc (e#es) = (let (start_pc, end_pc, handler_pc, catch_type) = e; |
|
71 es' = match_any G pc es |
|
72 in |
|
73 if start_pc <= pc \<and> pc < end_pc then catch_type#es' else es')" |
|
74 |
|
75 |
|
76 consts |
|
77 xcpt_names :: "instr \<times> jvm_prog \<times> p_count \<times> exception_table => cname list" |
|
78 recdef xcpt_names "{}" |
|
79 "xcpt_names (Getfield F C, G, pc, et) = [Xcpt NullPointer]" |
|
80 "xcpt_names (Putfield F C, G, pc, et) = [Xcpt NullPointer]" |
|
81 "xcpt_names (New C, G, pc, et) = [Xcpt OutOfMemory]" |
|
82 "xcpt_names (Checkcast C, G, pc, et) = [Xcpt ClassCast]" |
|
83 "xcpt_names (Throw, G, pc, et) = match_any G pc et" |
|
84 "xcpt_names (Invoke C m p, G, pc, et) = match_any G pc et" |
|
85 "xcpt_names (i, G, pc, et) = []" |
|
86 |
|
87 |
|
88 constdefs |
|
89 xcpt_eff :: "instr \<Rightarrow> jvm_prog \<Rightarrow> p_count \<Rightarrow> state_type option \<Rightarrow> exception_table \<Rightarrow> succ_type" |
|
90 "xcpt_eff i G pc s et == |
|
91 map (\<lambda>C. (the (match_exception_table G C pc et), case s of None \<Rightarrow> None | Some s' \<Rightarrow> Some ([Class C], snd s'))) |
|
92 (xcpt_names (i,G,pc,et))" |
|
93 |
|
94 norm_eff :: "instr \<Rightarrow> jvm_prog \<Rightarrow> state_type option \<Rightarrow> state_type option" |
|
95 "norm_eff i G == option_map (\<lambda>s. eff' (i,G,s))" |
|
96 |
|
97 eff :: "instr => jvm_prog => p_count => exception_table => state_type option => succ_type" |
|
98 "eff i G pc et s == (map (\<lambda>pc'. (pc',norm_eff i G s)) (succs i pc)) @ (xcpt_eff i G pc s et)" |
|
99 |
|
100 |
|
101 text "Conditions under which eff is applicable:" |
|
102 consts |
|
103 app' :: "instr \<times> jvm_prog \<times> nat \<times> ty \<times> state_type => bool" |
|
104 |
|
105 recdef app' "{}" |
|
106 "app' (Load idx, G, maxs, rT, s) = (idx < length (snd s) \<and> |
|
107 (snd s) ! idx \<noteq> Err \<and> |
|
108 length (fst s) < maxs)" |
|
109 "app' (Store idx, G, maxs, rT, (ts#ST, LT)) = (idx < length LT)" |
|
110 "app' (LitPush v, G, maxs, rT, s) = (length (fst s) < maxs \<and> typeof (\<lambda>t. None) v \<noteq> None)" |
|
111 "app' (Getfield F C, G, maxs, rT, (oT#ST, LT)) = (is_class G C \<and> |
|
112 field (G,C) F \<noteq> None \<and> |
|
113 fst (the (field (G,C) F)) = C \<and> |
|
114 G \<turnstile> oT \<preceq> (Class C))" |
|
115 "app' (Putfield F C, G, maxs, rT, (vT#oT#ST, LT)) = (is_class G C \<and> |
|
116 field (G,C) F \<noteq> None \<and> |
|
117 fst (the (field (G,C) F)) = C \<and> |
|
118 G \<turnstile> oT \<preceq> (Class C) \<and> |
|
119 G \<turnstile> vT \<preceq> (snd (the (field (G,C) F))))" |
|
120 "app' (New C, G, maxs, rT, s) = (is_class G C \<and> length (fst s) < maxs)" |
|
121 "app' (Checkcast C, G, maxs, rT, (RefT rt#ST,LT)) = (is_class G C)" |
|
122 "app' (Pop, G, maxs, rT, (ts#ST,LT)) = True" |
|
123 "app' (Dup, G, maxs, rT, (ts#ST,LT)) = (1+length ST < maxs)" |
|
124 "app' (Dup_x1, G, maxs, rT, (ts1#ts2#ST,LT)) = (2+length ST < maxs)" |
|
125 "app' (Dup_x2, G, maxs, rT, (ts1#ts2#ts3#ST,LT)) = (3+length ST < maxs)" |
|
126 "app' (Swap, G, maxs, rT, (ts1#ts2#ST,LT)) = True" |
|
127 "app' (IAdd, G, maxs, rT, (PrimT Integer#PrimT Integer#ST,LT)) |
|
128 = True" |
|
129 "app' (Ifcmpeq b, G, maxs, rT, (ts#ts'#ST,LT)) = ((\<exists>p. ts = PrimT p \<and> ts' = PrimT p) \<or> |
|
130 (\<exists>r r'. ts = RefT r \<and> ts' = RefT r'))" |
|
131 "app' (Goto b, G, maxs, rT, s) = True" |
|
132 "app' (Return, G, maxs, rT, (T#ST,LT)) = (G \<turnstile> T \<preceq> rT)" |
|
133 "app' (Throw, G, maxs, rT, (T#ST,LT)) = (\<exists>r. T = RefT r)" |
|
134 "app' (Invoke C mn fpTs, G, maxs, rT, s) = |
|
135 (length fpTs < length (fst s) \<and> |
|
136 (let apTs = rev (take (length fpTs) (fst s)); |
|
137 X = hd (drop (length fpTs) (fst s)) |
|
138 in |
|
139 G \<turnstile> X \<preceq> Class C \<and> is_class G C \<and> method (G,C) (mn,fpTs) \<noteq> None \<and> |
|
140 (\<forall>(aT,fT)\<in>set(zip apTs fpTs). G \<turnstile> aT \<preceq> fT)))" |
|
141 |
|
142 "app' (i,G,maxs,rT,s) = False" |
|
143 |
|
144 |
|
145 |
|
146 constdefs |
|
147 xcpt_app :: "instr \<Rightarrow> jvm_prog \<Rightarrow> nat \<Rightarrow> exception_table \<Rightarrow> bool" |
|
148 "xcpt_app i G pc et \<equiv> \<forall>C\<in>set(xcpt_names (i,G,pc,et)). is_class G C" |
|
149 |
|
150 app :: "instr => jvm_prog => nat => ty => nat => exception_table => state_type option => bool" |
|
151 "app i G maxs rT pc et s == case s of None => True | Some t => app' (i,G,maxs,rT,t) \<and> xcpt_app i G pc et" |
|
152 |
|
153 |
|
154 lemma 1: "2 < length a ==> (\<exists>l l' l'' ls. a = l#l'#l''#ls)" |
|
155 proof (cases a) |
|
156 fix x xs assume "a = x#xs" "2 < length a" |
|
157 thus ?thesis by - (cases xs, simp, cases "tl xs", auto) |
|
158 qed auto |
|
159 |
|
160 lemma 2: "\<not>(2 < length a) ==> a = [] \<or> (\<exists> l. a = [l]) \<or> (\<exists> l l'. a = [l,l'])" |
|
161 proof -; |
|
162 assume "\<not>(2 < length a)" |
|
163 hence "length a < (Suc (Suc (Suc 0)))" by simp |
|
164 hence * : "length a = 0 \<or> length a = Suc 0 \<or> length a = Suc (Suc 0)" |
|
165 by (auto simp add: less_Suc_eq) |
|
166 |
|
167 { |
|
168 fix x |
|
169 assume "length x = Suc 0" |
|
170 hence "\<exists> l. x = [l]" by - (cases x, auto) |
|
171 } note 0 = this |
|
172 |
|
173 have "length a = Suc (Suc 0) ==> \<exists>l l'. a = [l,l']" by (cases a, auto dest: 0) |
|
174 with * show ?thesis by (auto dest: 0) |
|
175 qed |
|
176 |
|
177 lemmas [simp] = app_def xcpt_app_def |
|
178 |
|
179 text {* |
|
180 \medskip |
|
181 simp rules for @{term app} |
|
182 *} |
|
183 lemma appNone[simp]: "app i G maxs rT pc et None = True" by simp |
|
184 |
|
185 |
|
186 lemma appLoad[simp]: |
|
187 "(app (Load idx) G maxs rT pc et (Some s)) = (\<exists>ST LT. s = (ST,LT) \<and> idx < length LT \<and> LT!idx \<noteq> Err \<and> length ST < maxs)" |
|
188 by (cases s, simp) |
|
189 |
|
190 lemma appStore[simp]: |
|
191 "(app (Store idx) G maxs rT pc et (Some s)) = (\<exists>ts ST LT. s = (ts#ST,LT) \<and> idx < length LT)" |
|
192 by (cases s, cases "2 < length (fst s)", auto dest: 1 2) |
|
193 |
|
194 lemma appLitPush[simp]: |
|
195 "(app (LitPush v) G maxs rT pc et (Some s)) = (\<exists>ST LT. s = (ST,LT) \<and> length ST < maxs \<and> typeof (\<lambda>v. None) v \<noteq> None)" |
|
196 by (cases s, simp) |
|
197 |
|
198 lemma appGetField[simp]: |
|
199 "(app (Getfield F C) G maxs rT pc et (Some s)) = |
|
200 (\<exists> oT vT ST LT. s = (oT#ST, LT) \<and> is_class G C \<and> |
|
201 field (G,C) F = Some (C,vT) \<and> G \<turnstile> oT \<preceq> (Class C) \<and> is_class G (Xcpt NullPointer))" |
|
202 by (cases s, cases "2 <length (fst s)", auto dest!: 1 2) |
|
203 |
|
204 lemma appPutField[simp]: |
|
205 "(app (Putfield F C) G maxs rT pc et (Some s)) = |
|
206 (\<exists> vT vT' oT ST LT. s = (vT#oT#ST, LT) \<and> is_class G C \<and> |
|
207 field (G,C) F = Some (C, vT') \<and> G \<turnstile> oT \<preceq> (Class C) \<and> G \<turnstile> vT \<preceq> vT' \<and> is_class G (Xcpt NullPointer))" |
|
208 by (cases s, cases "2 <length (fst s)", auto dest!: 1 2) |
|
209 |
|
210 lemma appNew[simp]: |
|
211 "(app (New C) G maxs rT pc et (Some s)) = |
|
212 (\<exists>ST LT. s=(ST,LT) \<and> is_class G C \<and> length ST < maxs \<and> is_class G (Xcpt OutOfMemory))" |
|
213 by (cases s, simp) |
|
214 |
|
215 lemma appCheckcast[simp]: |
|
216 "(app (Checkcast C) G maxs rT pc et (Some s)) = |
|
217 (\<exists>rT ST LT. s = (RefT rT#ST,LT) \<and> is_class G C \<and> is_class G (Xcpt ClassCast))" |
|
218 by (cases s, cases "fst s", simp add: app_def) (cases "hd (fst s)", auto) |
|
219 |
|
220 lemma appPop[simp]: |
|
221 "(app Pop G maxs rT pc et (Some s)) = (\<exists>ts ST LT. s = (ts#ST,LT))" |
|
222 by (cases s, cases "2 <length (fst s)", auto dest: 1 2) |
|
223 |
|
224 |
|
225 lemma appDup[simp]: |
|
226 "(app Dup G maxs rT pc et (Some s)) = (\<exists>ts ST LT. s = (ts#ST,LT) \<and> 1+length ST < maxs)" |
|
227 by (cases s, cases "2 <length (fst s)", auto dest: 1 2) |
|
228 |
|
229 |
|
230 lemma appDup_x1[simp]: |
|
231 "(app Dup_x1 G maxs rT pc et (Some s)) = (\<exists>ts1 ts2 ST LT. s = (ts1#ts2#ST,LT) \<and> 2+length ST < maxs)" |
|
232 by (cases s, cases "2 <length (fst s)", auto dest: 1 2) |
|
233 |
|
234 |
|
235 lemma appDup_x2[simp]: |
|
236 "(app Dup_x2 G maxs rT pc et (Some s)) = (\<exists>ts1 ts2 ts3 ST LT. s = (ts1#ts2#ts3#ST,LT) \<and> 3+length ST < maxs)" |
|
237 by (cases s, cases "2 <length (fst s)", auto dest: 1 2) |
|
238 |
|
239 |
|
240 lemma appSwap[simp]: |
|
241 "app Swap G maxs rT pc et (Some s) = (\<exists>ts1 ts2 ST LT. s = (ts1#ts2#ST,LT))" |
|
242 by (cases s, cases "2 <length (fst s)", auto dest: 1 2) |
|
243 |
|
244 |
|
245 lemma appIAdd[simp]: |
|
246 "app IAdd G maxs rT pc et (Some s) = (\<exists> ST LT. s = (PrimT Integer#PrimT Integer#ST,LT))" |
|
247 (is "?app s = ?P s") |
|
248 proof (cases (open) s) |
|
249 case Pair |
|
250 have "?app (a,b) = ?P (a,b)" |
|
251 proof (cases "a") |
|
252 fix t ts assume a: "a = t#ts" |
|
253 show ?thesis |
|
254 proof (cases t) |
|
255 fix p assume p: "t = PrimT p" |
|
256 show ?thesis |
|
257 proof (cases p) |
|
258 assume ip: "p = Integer" |
|
259 show ?thesis |
|
260 proof (cases ts) |
|
261 fix t' ts' assume t': "ts = t' # ts'" |
|
262 show ?thesis |
|
263 proof (cases t') |
|
264 fix p' assume "t' = PrimT p'" |
|
265 with t' ip p a |
|
266 show ?thesis by - (cases p', auto) |
|
267 qed (auto simp add: a p ip t') |
|
268 qed (auto simp add: a p ip) |
|
269 qed (auto simp add: a p) |
|
270 qed (auto simp add: a) |
|
271 qed auto |
|
272 with Pair show ?thesis by simp |
|
273 qed |
|
274 |
|
275 |
|
276 lemma appIfcmpeq[simp]: |
|
277 "app (Ifcmpeq b) G maxs rT pc et (Some s) = (\<exists>ts1 ts2 ST LT. s = (ts1#ts2#ST,LT) \<and> |
|
278 ((\<exists> p. ts1 = PrimT p \<and> ts2 = PrimT p) \<or> (\<exists>r r'. ts1 = RefT r \<and> ts2 = RefT r')))" |
|
279 by (cases s, cases "2 <length (fst s)", auto dest: 1 2) |
|
280 |
|
281 |
|
282 lemma appReturn[simp]: |
|
283 "app Return G maxs rT pc et (Some s) = (\<exists>T ST LT. s = (T#ST,LT) \<and> (G \<turnstile> T \<preceq> rT))" |
|
284 by (cases s, cases "2 <length (fst s)", auto dest: 1 2) |
|
285 |
|
286 lemma appGoto[simp]: |
|
287 "app (Goto branch) G maxs rT pc et (Some s) = True" |
|
288 by simp |
|
289 |
|
290 lemma appThrow[simp]: |
|
291 "app Throw G maxs rT pc et (Some s) = |
|
292 (\<exists>T ST LT r. s=(T#ST,LT) \<and> T = RefT r \<and> (\<forall>C \<in> set (match_any G pc et). is_class G C))" |
|
293 by (cases s, cases "2 < length (fst s)", auto dest: 1 2) |
|
294 |
|
295 lemma appInvoke[simp]: |
|
296 "app (Invoke C mn fpTs) G maxs rT pc et (Some s) = (\<exists>apTs X ST LT mD' rT' b'. |
|
297 s = ((rev apTs) @ (X # ST), LT) \<and> length apTs = length fpTs \<and> is_class G C \<and> |
|
298 G \<turnstile> X \<preceq> Class C \<and> (\<forall>(aT,fT)\<in>set(zip apTs fpTs). G \<turnstile> aT \<preceq> fT) \<and> |
|
299 method (G,C) (mn,fpTs) = Some (mD', rT', b') \<and> |
|
300 (\<forall>C \<in> set (match_any G pc et). is_class G C))" (is "?app s = ?P s") |
|
301 proof (cases (open) s) |
|
302 case Pair |
|
303 have "?app (a,b) ==> ?P (a,b)" |
|
304 proof - |
|
305 assume app: "?app (a,b)" |
|
306 hence "a = (rev (rev (take (length fpTs) a))) @ (drop (length fpTs) a) \<and> |
|
307 length fpTs < length a" (is "?a \<and> ?l") |
|
308 by (auto simp add: app_def) |
|
309 hence "?a \<and> 0 < length (drop (length fpTs) a)" (is "?a \<and> ?l") |
|
310 by auto |
|
311 hence "?a \<and> ?l \<and> length (rev (take (length fpTs) a)) = length fpTs" |
|
312 by (auto simp add: min_def) |
|
313 hence "\<exists>apTs ST. a = rev apTs @ ST \<and> length apTs = length fpTs \<and> 0 < length ST" |
|
314 by blast |
|
315 hence "\<exists>apTs ST. a = rev apTs @ ST \<and> length apTs = length fpTs \<and> ST \<noteq> []" |
|
316 by blast |
|
317 hence "\<exists>apTs ST. a = rev apTs @ ST \<and> length apTs = length fpTs \<and> |
|
318 (\<exists>X ST'. ST = X#ST')" |
|
319 by (simp add: neq_Nil_conv) |
|
320 hence "\<exists>apTs X ST. a = rev apTs @ X # ST \<and> length apTs = length fpTs" |
|
321 by blast |
|
322 with app |
|
323 show ?thesis by (unfold app_def, clarsimp) blast |
|
324 qed |
|
325 with Pair |
|
326 have "?app s ==> ?P s" by simp |
|
327 moreover |
|
328 have "?P s \<Longrightarrow> ?app s" by (unfold app_def) clarsimp |
|
329 ultimately |
|
330 show ?thesis by blast |
|
331 qed |
|
332 |
|
333 lemma effNone: |
|
334 "(pc', s') \<in> set (eff i G pc et None) \<Longrightarrow> s' = None" |
|
335 by (auto simp add: eff_def xcpt_eff_def norm_eff_def) |
|
336 |
|
337 lemmas [simp del] = app_def xcpt_app_def |
|
338 |
|
339 end |