author | kleing |
Sun, 16 Dec 2001 00:17:44 +0100 | |
changeset 12516 | d09d0f160888 |
parent 12389 | 23bd419144eb |
child 12545 | 7319d384d0d3 |
permissions | -rw-r--r-- |
8011 | 1 |
(* Title: HOL/MicroJava/BV/BVSpecTypeSafe.thy |
2 |
ID: $Id$ |
|
12516 | 3 |
Author: Cornelia Pusch, Gerwin Klein |
8011 | 4 |
Copyright 1999 Technische Universitaet Muenchen |
5 |
*) |
|
6 |
||
10056 | 7 |
header "BV Type Safety Proof" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
8 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
9 |
theory BVSpecTypeSafe = Correct: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
10 |
|
12516 | 11 |
text {* |
12 |
This theory contains proof that the specification of the bytecode |
|
13 |
verifier only admits type safe programs. |
|
14 |
*} |
|
15 |
||
16 |
section {* Preliminaries *} |
|
17 |
||
18 |
text {* |
|
19 |
Simp and intro setup for the type safety proof: |
|
20 |
*} |
|
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
21 |
lemmas defs1 = sup_state_conv correct_state_def correct_frame_def |
12516 | 22 |
wt_instr_def eff_def norm_eff_def |
10056 | 23 |
|
11252 | 24 |
lemmas widen_rules[intro] = approx_val_widen approx_loc_widen approx_stk_widen |
25 |
||
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
26 |
lemmas [simp del] = split_paired_All |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
27 |
|
12516 | 28 |
|
29 |
text {* |
|
30 |
If we have a welltyped program and a conforming state, we |
|
31 |
can directly infer that the current instruction is well typed: |
|
32 |
*} |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
33 |
lemma wt_jvm_prog_impl_wt_instr_cor: |
12516 | 34 |
"[| wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
35 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] |
12516 | 36 |
==> wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
37 |
apply (unfold correct_state_def Let_def correct_frame_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
38 |
apply simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
39 |
apply (blast intro: wt_jvm_prog_impl_wt_instr) |
9819 | 40 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
41 |
|
12516 | 42 |
|
43 |
section {* Exception Handling *} |
|
44 |
||
45 |
text {* |
|
46 |
Exceptions don't touch anything except the stack: |
|
47 |
*} |
|
48 |
lemma exec_instr_xcpt: |
|
49 |
"(fst (exec_instr i G hp stk vars Cl sig pc frs) = Some xcp) |
|
50 |
= (\<exists>stk'. exec_instr i G hp stk vars Cl sig pc frs = |
|
51 |
(Some xcp, hp, (stk', vars, Cl, sig, pc)#frs))" |
|
52 |
by (cases i, auto simp add: split_beta split: split_if_asm) |
|
53 |
||
54 |
||
55 |
text {* |
|
56 |
Relates @{text match_any} from the Bytecode Verifier with |
|
57 |
@{text match_exception_table} from the operational semantics: |
|
58 |
*} |
|
59 |
lemma in_match_any: |
|
60 |
"match_exception_table G xcpt pc et = Some pc' ==> |
|
61 |
\<exists>C. C \<in> set (match_any G pc et) \<and> G \<turnstile> xcpt \<preceq>C C \<and> |
|
62 |
match_exception_table G C pc et = Some pc'" |
|
63 |
(is "PROP ?P et" is "?match et ==> ?match_any et") |
|
64 |
proof (induct et) |
|
65 |
show "PROP ?P []" |
|
66 |
by simp |
|
67 |
||
68 |
fix e es |
|
69 |
assume IH: "PROP ?P es" |
|
70 |
assume match: "?match (e#es)" |
|
71 |
||
72 |
obtain start_pc end_pc handler_pc catch_type where |
|
73 |
e [simp]: "e = (start_pc, end_pc, handler_pc, catch_type)" |
|
74 |
by (cases e) |
|
75 |
||
76 |
from IH match |
|
77 |
show "?match_any (e#es)" |
|
78 |
proof (cases "match_exception_entry G xcpt pc e") |
|
79 |
case False |
|
80 |
with match |
|
81 |
have "match_exception_table G xcpt pc es = Some pc'" by simp |
|
82 |
with IH |
|
83 |
obtain C where |
|
84 |
set: "C \<in> set (match_any G pc es)" and |
|
85 |
C: "G \<turnstile> xcpt \<preceq>C C" and |
|
86 |
m: "match_exception_table G C pc es = Some pc'" by blast |
|
87 |
||
88 |
from set |
|
89 |
have "C \<in> set (match_any G pc (e#es))" by simp |
|
90 |
moreover |
|
91 |
from False C |
|
92 |
have "\<not> match_exception_entry G C pc e" |
|
93 |
by - (erule contrapos_nn, |
|
94 |
auto simp add: match_exception_entry_def elim: rtrancl_trans) |
|
95 |
with m |
|
96 |
have "match_exception_table G C pc (e#es) = Some pc'" by simp |
|
97 |
moreover note C |
|
98 |
ultimately |
|
99 |
show ?thesis by blast |
|
100 |
next |
|
101 |
case True with match |
|
102 |
have "match_exception_entry G catch_type pc e" |
|
103 |
by (simp add: match_exception_entry_def) |
|
104 |
moreover |
|
105 |
from True match |
|
106 |
obtain |
|
107 |
"start_pc \<le> pc" |
|
108 |
"pc < end_pc" |
|
109 |
"G \<turnstile> xcpt \<preceq>C catch_type" |
|
110 |
"handler_pc = pc'" |
|
111 |
by (simp add: match_exception_entry_def) |
|
112 |
ultimately |
|
113 |
show ?thesis by auto |
|
114 |
qed |
|
115 |
qed |
|
116 |
||
117 |
text {* |
|
118 |
We can prove separately that the recursive search for exception |
|
119 |
handlers (@{text find_handler}) in the frame stack results in |
|
120 |
a conforming state (if there was no matching exception handler |
|
121 |
in the current frame). We require that the exception is a valid |
|
122 |
heap address, and that the state before the exception occured |
|
123 |
conforms. |
|
124 |
*} |
|
125 |
lemma uncaught_xcpt_correct: |
|
126 |
"!!f. [| wt_jvm_prog G phi; xcp = Addr adr; hp adr = Some T; |
|
127 |
G,phi \<turnstile>JVM (None, hp, f#frs)\<surd> |] |
|
128 |
==> G,phi \<turnstile>JVM (find_handler G (Some xcp) hp frs)\<surd>" |
|
129 |
(is "!!f. [| ?wt; ?adr; ?hp; ?correct (None, hp, f#frs) |] ==> ?correct (?find frs)") |
|
130 |
proof (induct frs) |
|
131 |
-- "the base case is trivial, as it should be" |
|
132 |
show "?correct (?find [])" by (simp add: correct_state_def) |
|
133 |
||
134 |
-- "we will need both forms @{text wt_jvm_prog} and @{text wf_prog} later" |
|
135 |
assume wt: ?wt |
|
136 |
then obtain mb where wf: "wf_prog mb G" by (simp add: wt_jvm_prog_def) |
|
137 |
||
138 |
-- "these two don't change in the induction:" |
|
139 |
assume adr: ?adr |
|
140 |
assume hp: ?hp |
|
141 |
||
142 |
-- "the assumption for the cons case:" |
|
143 |
fix f f' frs' |
|
144 |
assume cr: "?correct (None, hp, f#f'#frs')" |
|
145 |
||
146 |
-- "the induction hypothesis as produced by Isabelle, immediatly simplified |
|
147 |
with the fixed assumptions above" |
|
148 |
assume "\<And>f. [| ?wt; ?adr; ?hp; ?correct (None, hp, f#frs') |] ==> ?correct (?find frs')" |
|
149 |
with wt adr hp |
|
150 |
have IH: "\<And>f. ?correct (None, hp, f#frs') ==> ?correct (?find frs')" by blast |
|
151 |
||
152 |
from cr |
|
153 |
have cr': "?correct (None, hp, f'#frs')" by (auto simp add: correct_state_def) |
|
154 |
||
155 |
obtain stk loc C sig pc where f' [simp]: "f' = (stk,loc,C,sig,pc)" |
|
156 |
by (cases f') |
|
157 |
||
158 |
from cr |
|
159 |
obtain rT maxs maxl ins et where |
|
160 |
meth: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)" |
|
161 |
by (simp add: correct_state_def, blast) |
|
162 |
||
163 |
hence [simp]: "ex_table_of (snd (snd (the (method (G, C) sig)))) = et" |
|
164 |
by simp |
|
165 |
||
166 |
show "?correct (?find (f'#frs'))" |
|
167 |
proof (cases "match_exception_table G (cname_of hp xcp) pc et") |
|
168 |
case None |
|
169 |
with cr' IH |
|
170 |
show ?thesis by simp |
|
171 |
next |
|
172 |
fix handler_pc |
|
173 |
assume match: "match_exception_table G (cname_of hp xcp) pc et = Some handler_pc" |
|
174 |
(is "?match (cname_of hp xcp) = _") |
|
175 |
||
176 |
from wt meth cr' [simplified] |
|
177 |
have wti: "wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc" |
|
178 |
by (rule wt_jvm_prog_impl_wt_instr_cor) |
|
179 |
||
180 |
from cr meth |
|
181 |
obtain C' mn pts ST LT where |
|
182 |
ins: "ins!pc = Invoke C' mn pts" (is "_ = ?i") and |
|
183 |
phi: "phi C sig ! pc = Some (ST, LT)" |
|
184 |
by (simp add: correct_state_def) blast |
|
185 |
||
186 |
from match |
|
187 |
obtain D where |
|
188 |
in_any: "D \<in> set (match_any G pc et)" and |
|
189 |
D: "G \<turnstile> cname_of hp xcp \<preceq>C D" and |
|
190 |
match': "?match D = Some handler_pc" |
|
191 |
by (blast dest: in_match_any) |
|
192 |
||
193 |
from ins wti phi have |
|
194 |
"\<forall>D\<in>set (match_any G pc et). the (?match D) < length ins \<and> |
|
195 |
G \<turnstile> Some ([Class D], LT) <=' phi C sig!the (?match D)" |
|
196 |
by (simp add: wt_instr_def eff_def xcpt_eff_def) |
|
197 |
with in_any match' obtain |
|
198 |
pc: "handler_pc < length ins" |
|
199 |
"G \<turnstile> Some ([Class D], LT) <=' phi C sig ! handler_pc" |
|
200 |
by auto |
|
201 |
then obtain ST' LT' where |
|
202 |
phi': "phi C sig ! handler_pc = Some (ST',LT')" and |
|
203 |
less: "G \<turnstile> ([Class D], LT) <=s (ST',LT')" |
|
204 |
by auto |
|
205 |
||
206 |
from cr' phi meth f' |
|
207 |
have "correct_frame G hp (ST, LT) maxl ins f'" |
|
208 |
by (unfold correct_state_def) auto |
|
209 |
then obtain |
|
210 |
len: "length loc = 1+length (snd sig)+maxl" and |
|
211 |
loc: "approx_loc G hp loc LT" |
|
212 |
by (unfold correct_frame_def) auto |
|
213 |
||
214 |
let ?f = "([xcp], loc, C, sig, handler_pc)" |
|
215 |
have "correct_frame G hp (ST', LT') maxl ins ?f" |
|
216 |
proof - |
|
217 |
from wf less loc |
|
218 |
have "approx_loc G hp loc LT'" by (simp add: sup_state_conv) blast |
|
219 |
moreover |
|
220 |
from D adr hp |
|
221 |
have "G,hp \<turnstile> xcp ::\<preceq> Class D" by (simp add: conf_def obj_ty_def) |
|
222 |
with wf less loc |
|
223 |
have "approx_stk G hp [xcp] ST'" |
|
224 |
by (auto simp add: sup_state_conv approx_stk_def approx_val_def |
|
225 |
elim: conf_widen split: Err.split) |
|
226 |
moreover |
|
227 |
note len pc |
|
228 |
ultimately |
|
229 |
show ?thesis by (simp add: correct_frame_def) |
|
230 |
qed |
|
231 |
||
232 |
with cr' match phi' meth |
|
233 |
show ?thesis by (unfold correct_state_def) auto |
|
234 |
qed |
|
235 |
qed |
|
236 |
||
237 |
||
238 |
text {* |
|
239 |
The requirement of lemma @{text uncaught_xcpt_correct} (that |
|
240 |
the exception is a valid reference on the heap) is always met |
|
241 |
for welltyped instructions and conformant states: |
|
242 |
*} |
|
243 |
lemma exec_instr_xcpt_hp: |
|
244 |
"[| fst (exec_instr (ins!pc) G hp stk vars Cl sig pc frs) = Some xcp; |
|
245 |
wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; |
|
246 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] |
|
247 |
==> \<exists>adr T. xcp = Addr adr \<and> hp adr = Some T" |
|
248 |
(is "[| ?xcpt; ?wt; ?correct |] ==> ?thesis") |
|
249 |
proof - |
|
250 |
note [simp] = system_xcpt_allocated split_beta raise_system_xcpt_def |
|
251 |
note [split] = split_if_asm option.split_asm |
|
252 |
||
253 |
assume wt: ?wt ?correct |
|
254 |
||
255 |
assume xcpt: ?xcpt |
|
256 |
thus ?thesis |
|
257 |
proof (cases "ins!pc") |
|
258 |
case New with xcpt |
|
259 |
show ?thesis by (auto dest: new_Addr_OutOfMemory) |
|
260 |
next |
|
261 |
case Throw with xcpt wt |
|
262 |
show ?thesis |
|
263 |
by (auto simp add: wt_instr_def correct_state_def correct_frame_def |
|
264 |
dest: non_npD) |
|
265 |
qed auto |
|
266 |
qed |
|
267 |
||
268 |
||
269 |
text {* |
|
270 |
Finally we can state that, whenever an exception occurs, the |
|
271 |
resulting next state always conforms: |
|
272 |
*} |
|
273 |
lemma xcpt_correct: |
|
274 |
"[| wt_jvm_prog G phi; |
|
275 |
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); |
|
276 |
wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; |
|
277 |
fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = Some xcp; |
|
278 |
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); |
|
279 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] |
|
280 |
==> G,phi \<turnstile>JVM state'\<surd>" |
|
281 |
proof - |
|
282 |
assume wtp: "wt_jvm_prog G phi" |
|
283 |
assume meth: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)" |
|
284 |
assume wt: "wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc" |
|
285 |
assume xp: "fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = Some xcp" |
|
286 |
assume s': "Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs)" |
|
287 |
assume correct: "G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>" |
|
288 |
||
289 |
from wtp obtain wfmb where wf: "wf_prog wfmb G" by (simp add: wt_jvm_prog_def) |
|
290 |
||
291 |
note xp' = meth s' xp |
|
292 |
||
293 |
note wtp |
|
294 |
moreover |
|
295 |
from xp wt correct |
|
296 |
obtain adr T where |
|
297 |
adr: "xcp = Addr adr" "hp adr = Some T" |
|
298 |
by (blast dest: exec_instr_xcpt_hp) |
|
299 |
moreover |
|
300 |
note correct |
|
301 |
ultimately |
|
302 |
have "G,phi \<turnstile>JVM find_handler G (Some xcp) hp frs \<surd>" by (rule uncaught_xcpt_correct) |
|
303 |
with xp' |
|
304 |
have "match_exception_table G (cname_of hp xcp) pc et = None \<Longrightarrow> ?thesis" |
|
305 |
(is "?m (cname_of hp xcp) = _ \<Longrightarrow> _" is "?match = _ \<Longrightarrow> _") |
|
306 |
by (clarsimp simp add: exec_instr_xcpt split_beta) |
|
307 |
moreover |
|
308 |
{ fix handler |
|
309 |
assume some_handler: "?match = Some handler" |
|
310 |
||
311 |
from correct meth |
|
312 |
obtain ST LT where |
|
313 |
hp_ok: "G \<turnstile>h hp \<surd>" and |
|
314 |
class: "is_class G C" and |
|
315 |
phi_pc: "phi C sig ! pc = Some (ST, LT)" and |
|
316 |
frame: "correct_frame G hp (ST, LT) maxl ins (stk, loc, C, sig, pc)" and |
|
317 |
frames: "correct_frames G hp phi rT sig frs" |
|
318 |
by (unfold correct_state_def) auto |
|
319 |
||
320 |
from frame obtain |
|
321 |
stk: "approx_stk G hp stk ST" and |
|
322 |
loc: "approx_loc G hp loc LT" and |
|
323 |
pc: "pc < length ins" and |
|
324 |
len: "length loc = 1+length (snd sig)+maxl" |
|
325 |
by (unfold correct_frame_def) auto |
|
326 |
||
327 |
from wt obtain |
|
328 |
eff: "\<forall>(pc', s')\<in>set (xcpt_eff (ins!pc) G pc (phi C sig!pc) et). |
|
329 |
pc' < length ins \<and> G \<turnstile> s' <=' phi C sig!pc'" |
|
330 |
by (simp add: wt_instr_def eff_def) |
|
331 |
||
332 |
from some_handler xp' |
|
333 |
have state': |
|
334 |
"state' = (None, hp, ([xcp], loc, C, sig, handler)#frs)" |
|
335 |
by (cases "ins!pc", auto simp add: raise_system_xcpt_def split_beta |
|
336 |
split: split_if_asm) (* takes long! *) |
|
337 |
||
338 |
let ?f' = "([xcp], loc, C, sig, handler)" |
|
339 |
from eff |
|
340 |
obtain ST' LT' where |
|
341 |
phi_pc': "phi C sig ! handler = Some (ST', LT')" and |
|
342 |
frame': "correct_frame G hp (ST',LT') maxl ins ?f'" |
|
343 |
proof (cases "ins!pc") |
|
344 |
case Return -- "can't generate exceptions:" |
|
345 |
with xp' have False by (simp add: split_beta split: split_if_asm) |
|
346 |
thus ?thesis .. |
|
347 |
next |
|
348 |
case New |
|
349 |
with some_handler xp' |
|
350 |
have xcp: "xcp = Addr (XcptRef OutOfMemory)" |
|
351 |
by (simp add: raise_system_xcpt_def split_beta new_Addr_OutOfMemory) |
|
352 |
hence "cname_of hp xcp = Xcpt OutOfMemory" |
|
353 |
by (simp add: system_xcpt_allocated) |
|
354 |
with New some_handler phi_pc eff |
|
355 |
obtain ST' LT' where |
|
356 |
phi': "phi C sig ! handler = Some (ST', LT')" and |
|
357 |
less: "G \<turnstile> ([Class (Xcpt OutOfMemory)], LT) <=s (ST', LT')" and |
|
358 |
pc': "handler < length ins" |
|
359 |
by (simp add: xcpt_eff_def) blast |
|
360 |
note phi' |
|
361 |
moreover |
|
362 |
{ from xcp |
|
363 |
have "G,hp \<turnstile> xcp ::\<preceq> Class (Xcpt OutOfMemory)" |
|
364 |
by (simp add: conf_def obj_ty_def system_xcpt_allocated) |
|
365 |
moreover |
|
366 |
from wf less loc |
|
367 |
have "approx_loc G hp loc LT'" |
|
368 |
by (simp add: sup_state_conv) blast |
|
369 |
moreover |
|
370 |
note wf less pc' len |
|
371 |
ultimately |
|
372 |
have "correct_frame G hp (ST',LT') maxl ins ?f'" |
|
373 |
by (unfold correct_frame_def) (auto simp add: sup_state_conv |
|
374 |
approx_stk_def approx_val_def split: err.split elim: conf_widen) |
|
375 |
} |
|
376 |
ultimately |
|
377 |
show ?thesis by (rule that) |
|
378 |
next |
|
379 |
case Getfield |
|
380 |
with some_handler xp' |
|
381 |
have xcp: "xcp = Addr (XcptRef NullPointer)" |
|
382 |
by (simp add: raise_system_xcpt_def split_beta split: split_if_asm) |
|
383 |
hence "cname_of hp xcp = Xcpt NullPointer" |
|
384 |
by (simp add: system_xcpt_allocated) |
|
385 |
with Getfield some_handler phi_pc eff |
|
386 |
obtain ST' LT' where |
|
387 |
phi': "phi C sig ! handler = Some (ST', LT')" and |
|
388 |
less: "G \<turnstile> ([Class (Xcpt NullPointer)], LT) <=s (ST', LT')" and |
|
389 |
pc': "handler < length ins" |
|
390 |
by (simp add: xcpt_eff_def) blast |
|
391 |
note phi' |
|
392 |
moreover |
|
393 |
{ from xcp |
|
394 |
have "G,hp \<turnstile> xcp ::\<preceq> Class (Xcpt NullPointer)" |
|
395 |
by (simp add: conf_def obj_ty_def system_xcpt_allocated) |
|
396 |
moreover |
|
397 |
from wf less loc |
|
398 |
have "approx_loc G hp loc LT'" |
|
399 |
by (simp add: sup_state_conv) blast |
|
400 |
moreover |
|
401 |
note wf less pc' len |
|
402 |
ultimately |
|
403 |
have "correct_frame G hp (ST',LT') maxl ins ?f'" |
|
404 |
by (unfold correct_frame_def) (auto simp add: sup_state_conv |
|
405 |
approx_stk_def approx_val_def split: err.split elim: conf_widen) |
|
406 |
} |
|
407 |
ultimately |
|
408 |
show ?thesis by (rule that) |
|
409 |
next |
|
410 |
case Putfield |
|
411 |
with some_handler xp' |
|
412 |
have xcp: "xcp = Addr (XcptRef NullPointer)" |
|
413 |
by (simp add: raise_system_xcpt_def split_beta split: split_if_asm) |
|
414 |
hence "cname_of hp xcp = Xcpt NullPointer" |
|
415 |
by (simp add: system_xcpt_allocated) |
|
416 |
with Putfield some_handler phi_pc eff |
|
417 |
obtain ST' LT' where |
|
418 |
phi': "phi C sig ! handler = Some (ST', LT')" and |
|
419 |
less: "G \<turnstile> ([Class (Xcpt NullPointer)], LT) <=s (ST', LT')" and |
|
420 |
pc': "handler < length ins" |
|
421 |
by (simp add: xcpt_eff_def) blast |
|
422 |
note phi' |
|
423 |
moreover |
|
424 |
{ from xcp |
|
425 |
have "G,hp \<turnstile> xcp ::\<preceq> Class (Xcpt NullPointer)" |
|
426 |
by (simp add: conf_def obj_ty_def system_xcpt_allocated) |
|
427 |
moreover |
|
428 |
from wf less loc |
|
429 |
have "approx_loc G hp loc LT'" |
|
430 |
by (simp add: sup_state_conv) blast |
|
431 |
moreover |
|
432 |
note wf less pc' len |
|
433 |
ultimately |
|
434 |
have "correct_frame G hp (ST',LT') maxl ins ?f'" |
|
435 |
by (unfold correct_frame_def) (auto simp add: sup_state_conv |
|
436 |
approx_stk_def approx_val_def split: err.split elim: conf_widen) |
|
437 |
} |
|
438 |
ultimately |
|
439 |
show ?thesis by (rule that) |
|
440 |
next |
|
441 |
case Checkcast |
|
442 |
with some_handler xp' |
|
443 |
have xcp: "xcp = Addr (XcptRef ClassCast)" |
|
444 |
by (simp add: raise_system_xcpt_def split_beta split: split_if_asm) |
|
445 |
hence "cname_of hp xcp = Xcpt ClassCast" |
|
446 |
by (simp add: system_xcpt_allocated) |
|
447 |
with Checkcast some_handler phi_pc eff |
|
448 |
obtain ST' LT' where |
|
449 |
phi': "phi C sig ! handler = Some (ST', LT')" and |
|
450 |
less: "G \<turnstile> ([Class (Xcpt ClassCast)], LT) <=s (ST', LT')" and |
|
451 |
pc': "handler < length ins" |
|
452 |
by (simp add: xcpt_eff_def) blast |
|
453 |
note phi' |
|
454 |
moreover |
|
455 |
{ from xcp |
|
456 |
have "G,hp \<turnstile> xcp ::\<preceq> Class (Xcpt ClassCast)" |
|
457 |
by (simp add: conf_def obj_ty_def system_xcpt_allocated) |
|
458 |
moreover |
|
459 |
from wf less loc |
|
460 |
have "approx_loc G hp loc LT'" |
|
461 |
by (simp add: sup_state_conv) blast |
|
462 |
moreover |
|
463 |
note wf less pc' len |
|
464 |
ultimately |
|
465 |
have "correct_frame G hp (ST',LT') maxl ins ?f'" |
|
466 |
by (unfold correct_frame_def) (auto simp add: sup_state_conv |
|
467 |
approx_stk_def approx_val_def split: err.split elim: conf_widen) |
|
468 |
} |
|
469 |
ultimately |
|
470 |
show ?thesis by (rule that) |
|
471 |
next |
|
472 |
case Invoke |
|
473 |
with phi_pc eff |
|
474 |
have |
|
475 |
"\<forall>D\<in>set (match_any G pc et). |
|
476 |
the (?m D) < length ins \<and> G \<turnstile> Some ([Class D], LT) <=' phi C sig!the (?m D)" |
|
477 |
by (simp add: xcpt_eff_def) |
|
478 |
moreover |
|
479 |
from some_handler |
|
480 |
obtain D where |
|
481 |
"D \<in> set (match_any G pc et)" and |
|
482 |
D: "G \<turnstile> cname_of hp xcp \<preceq>C D" and |
|
483 |
"?m D = Some handler" |
|
484 |
by (blast dest: in_match_any) |
|
485 |
ultimately |
|
486 |
obtain |
|
487 |
pc': "handler < length ins" and |
|
488 |
"G \<turnstile> Some ([Class D], LT) <=' phi C sig ! handler" |
|
489 |
by auto |
|
490 |
then |
|
491 |
obtain ST' LT' where |
|
492 |
phi': "phi C sig ! handler = Some (ST', LT')" and |
|
493 |
less: "G \<turnstile> ([Class D], LT) <=s (ST', LT')" |
|
494 |
by auto |
|
495 |
from xp wt correct |
|
496 |
obtain addr T where |
|
497 |
xcp: "xcp = Addr addr" "hp addr = Some T" |
|
498 |
by (blast dest: exec_instr_xcpt_hp) |
|
499 |
note phi' |
|
500 |
moreover |
|
501 |
{ from xcp D |
|
502 |
have "G,hp \<turnstile> xcp ::\<preceq> Class D" |
|
503 |
by (simp add: conf_def obj_ty_def) |
|
504 |
moreover |
|
505 |
from wf less loc |
|
506 |
have "approx_loc G hp loc LT'" |
|
507 |
by (simp add: sup_state_conv) blast |
|
508 |
moreover |
|
509 |
note wf less pc' len |
|
510 |
ultimately |
|
511 |
have "correct_frame G hp (ST',LT') maxl ins ?f'" |
|
512 |
by (unfold correct_frame_def) (auto simp add: sup_state_conv |
|
513 |
approx_stk_def approx_val_def split: err.split elim: conf_widen) |
|
514 |
} |
|
515 |
ultimately |
|
516 |
show ?thesis by (rule that) |
|
517 |
next |
|
518 |
case Throw |
|
519 |
with phi_pc eff |
|
520 |
have |
|
521 |
"\<forall>D\<in>set (match_any G pc et). |
|
522 |
the (?m D) < length ins \<and> G \<turnstile> Some ([Class D], LT) <=' phi C sig!the (?m D)" |
|
523 |
by (simp add: xcpt_eff_def) |
|
524 |
moreover |
|
525 |
from some_handler |
|
526 |
obtain D where |
|
527 |
"D \<in> set (match_any G pc et)" and |
|
528 |
D: "G \<turnstile> cname_of hp xcp \<preceq>C D" and |
|
529 |
"?m D = Some handler" |
|
530 |
by (blast dest: in_match_any) |
|
531 |
ultimately |
|
532 |
obtain |
|
533 |
pc': "handler < length ins" and |
|
534 |
"G \<turnstile> Some ([Class D], LT) <=' phi C sig ! handler" |
|
535 |
by auto |
|
536 |
then |
|
537 |
obtain ST' LT' where |
|
538 |
phi': "phi C sig ! handler = Some (ST', LT')" and |
|
539 |
less: "G \<turnstile> ([Class D], LT) <=s (ST', LT')" |
|
540 |
by auto |
|
541 |
from xp wt correct |
|
542 |
obtain addr T where |
|
543 |
xcp: "xcp = Addr addr" "hp addr = Some T" |
|
544 |
by (blast dest: exec_instr_xcpt_hp) |
|
545 |
note phi' |
|
546 |
moreover |
|
547 |
{ from xcp D |
|
548 |
have "G,hp \<turnstile> xcp ::\<preceq> Class D" |
|
549 |
by (simp add: conf_def obj_ty_def) |
|
550 |
moreover |
|
551 |
from wf less loc |
|
552 |
have "approx_loc G hp loc LT'" |
|
553 |
by (simp add: sup_state_conv) blast |
|
554 |
moreover |
|
555 |
note wf less pc' len |
|
556 |
ultimately |
|
557 |
have "correct_frame G hp (ST',LT') maxl ins ?f'" |
|
558 |
by (unfold correct_frame_def) (auto simp add: sup_state_conv |
|
559 |
approx_stk_def approx_val_def split: err.split elim: conf_widen) |
|
560 |
} |
|
561 |
ultimately |
|
562 |
show ?thesis by (rule that) |
|
563 |
qed (insert xp', auto) -- "the other instructions don't generate exceptions" |
|
564 |
||
565 |
from state' meth hp_ok class frames phi_pc' frame' |
|
566 |
have ?thesis by (unfold correct_state_def) simp |
|
567 |
} |
|
568 |
ultimately |
|
569 |
show ?thesis by (cases "?match") blast+ |
|
570 |
qed |
|
571 |
||
572 |
||
573 |
||
11085 | 574 |
section {* Single Instructions *} |
575 |
||
12516 | 576 |
text {* |
577 |
In this section we look at each single (welltyped) instruction, and |
|
578 |
prove that the state after execution of the instruction still conforms. |
|
579 |
Since we have already handled exceptions above, we can now assume, that |
|
580 |
on exception occurs for this (single step) execution. |
|
581 |
*} |
|
582 |
||
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
583 |
lemmas [iff] = not_Err_eq |
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
584 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
585 |
lemma Load_correct: |
10042 | 586 |
"[| wf_prog wt G; |
12516 | 587 |
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); |
10056 | 588 |
ins!pc = Load idx; |
12516 | 589 |
wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; |
10056 | 590 |
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); |
12516 | 591 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
592 |
==> G,phi \<turnstile>JVM state'\<surd>" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
593 |
apply (clarsimp simp add: defs1 map_eq_Cons) |
11252 | 594 |
apply (blast intro: approx_loc_imp_approx_val_sup) |
9819 | 595 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
596 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
597 |
lemma Store_correct: |
10042 | 598 |
"[| wf_prog wt G; |
12516 | 599 |
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
600 |
ins!pc = Store idx; |
12516 | 601 |
wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
602 |
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
603 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] |
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
604 |
==> G,phi \<turnstile>JVM state'\<surd>" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
605 |
apply (clarsimp simp add: defs1 map_eq_Cons) |
11252 | 606 |
apply (blast intro: approx_loc_subst) |
9819 | 607 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
608 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
609 |
|
10897
697fab84709e
removed instructions Aconst_null+Bipush, introduced LitPush
kleing
parents:
10812
diff
changeset
|
610 |
lemma LitPush_correct: |
10042 | 611 |
"[| wf_prog wt G; |
12516 | 612 |
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); |
10897
697fab84709e
removed instructions Aconst_null+Bipush, introduced LitPush
kleing
parents:
10812
diff
changeset
|
613 |
ins!pc = LitPush v; |
12516 | 614 |
wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; |
10056 | 615 |
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
616 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] |
11252 | 617 |
==> G,phi \<turnstile>JVM state'\<surd>" |
618 |
apply (clarsimp simp add: defs1 sup_PTS_eq map_eq_Cons) |
|
619 |
apply (blast dest: conf_litval intro: conf_widen) |
|
9819 | 620 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
621 |
|
10897
697fab84709e
removed instructions Aconst_null+Bipush, introduced LitPush
kleing
parents:
10812
diff
changeset
|
622 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
623 |
lemma Cast_conf2: |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
624 |
"[| wf_prog ok G; G,h\<turnstile>v::\<preceq>RefT rt; cast_ok G C h v; |
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
625 |
G\<turnstile>Class C\<preceq>T; is_class G C|] |
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
626 |
==> G,h\<turnstile>v::\<preceq>T" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
627 |
apply (unfold cast_ok_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
628 |
apply (frule widen_Class) |
11252 | 629 |
apply (elim exE disjE) |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
630 |
apply (simp add: null) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
631 |
apply (clarsimp simp add: conf_def obj_ty_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
632 |
apply (cases v) |
10897
697fab84709e
removed instructions Aconst_null+Bipush, introduced LitPush
kleing
parents:
10812
diff
changeset
|
633 |
apply (auto intro: rtrancl_trans) |
9819 | 634 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
635 |
|
12516 | 636 |
lemmas defs1 = defs1 raise_system_xcpt_def |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
637 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
638 |
lemma Checkcast_correct: |
12516 | 639 |
"[| wt_jvm_prog G phi; |
640 |
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); |
|
10056 | 641 |
ins!pc = Checkcast D; |
12516 | 642 |
wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; |
10056 | 643 |
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
12516 | 644 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>; |
645 |
fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None |] |
|
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
646 |
==> G,phi \<turnstile>JVM state'\<surd>" |
12516 | 647 |
apply (clarsimp simp add: defs1 wt_jvm_prog_def map_eq_Cons split: split_if_asm) |
11252 | 648 |
apply (blast intro: Cast_conf2) |
9819 | 649 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
650 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
651 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
652 |
lemma Getfield_correct: |
12516 | 653 |
"[| wt_jvm_prog G phi; |
654 |
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
655 |
ins!pc = Getfield F D; |
12516 | 656 |
wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
657 |
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
12516 | 658 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>; |
659 |
fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None |] |
|
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
660 |
==> G,phi \<turnstile>JVM state'\<surd>" |
12516 | 661 |
apply (clarsimp simp add: defs1 map_eq_Cons wt_jvm_prog_def |
662 |
split: option.split split_if_asm) |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
663 |
apply (frule conf_widen) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
664 |
apply assumption+ |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
665 |
apply (drule conf_RefTD) |
11252 | 666 |
apply (clarsimp simp add: defs1) |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
667 |
apply (rule conjI) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
668 |
apply (drule widen_cfs_fields) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
669 |
apply assumption+ |
12516 | 670 |
apply (erule conf_widen) |
671 |
prefer 2 |
|
672 |
apply assumption |
|
673 |
apply (simp add: hconf_def oconf_def lconf_def) |
|
674 |
apply (elim allE) |
|
675 |
apply (erule impE, assumption) |
|
676 |
apply simp |
|
677 |
apply (elim allE) |
|
678 |
apply (erule impE, assumption) |
|
679 |
apply clarsimp |
|
11252 | 680 |
apply blast |
9819 | 681 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
682 |
|
12516 | 683 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
684 |
lemma Putfield_correct: |
10042 | 685 |
"[| wf_prog wt G; |
12516 | 686 |
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
687 |
ins!pc = Putfield F D; |
12516 | 688 |
wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
689 |
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
12516 | 690 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>; |
691 |
fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None |] |
|
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
692 |
==> G,phi \<turnstile>JVM state'\<surd>" |
12516 | 693 |
apply (clarsimp simp add: defs1 split_beta split: option.split List.split split_if_asm) |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
694 |
apply (frule conf_widen) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
695 |
prefer 2 |
11252 | 696 |
apply assumption |
697 |
apply assumption |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
698 |
apply (drule conf_RefTD) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
699 |
apply clarsimp |
10056 | 700 |
apply (blast |
701 |
intro: |
|
11252 | 702 |
hext_upd_obj approx_stk_sup_heap |
703 |
approx_loc_sup_heap |
|
704 |
hconf_field_update |
|
705 |
correct_frames_field_update conf_widen |
|
10056 | 706 |
dest: |
707 |
widen_cfs_fields) |
|
9819 | 708 |
done |
12516 | 709 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
710 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
711 |
lemma New_correct: |
10042 | 712 |
"[| wf_prog wt G; |
12516 | 713 |
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); |
10920 | 714 |
ins!pc = New X; |
12516 | 715 |
wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
716 |
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
12516 | 717 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>; |
718 |
fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None |] |
|
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
719 |
==> G,phi \<turnstile>JVM state'\<surd>" |
10920 | 720 |
proof - |
721 |
assume wf: "wf_prog wt G" |
|
12516 | 722 |
assume meth: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)" |
10920 | 723 |
assume ins: "ins!pc = New X" |
12516 | 724 |
assume wt: "wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc" |
10920 | 725 |
assume exec: "Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs)" |
726 |
assume conf: "G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>" |
|
12516 | 727 |
assume no_x: "fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None" |
10920 | 728 |
|
729 |
from ins conf meth |
|
730 |
obtain ST LT where |
|
731 |
heap_ok: "G\<turnstile>h hp\<surd>" and |
|
732 |
phi_pc: "phi C sig!pc = Some (ST,LT)" and |
|
733 |
is_class_C: "is_class G C" and |
|
734 |
frame: "correct_frame G hp (ST,LT) maxl ins (stk, loc, C, sig, pc)" and |
|
735 |
frames: "correct_frames G hp phi rT sig frs" |
|
736 |
by (auto simp add: correct_state_def iff del: not_None_eq) |
|
11252 | 737 |
|
10920 | 738 |
from phi_pc ins wt |
739 |
obtain ST' LT' where |
|
740 |
is_class_X: "is_class G X" and |
|
12516 | 741 |
maxs: "length ST < maxs" and |
10920 | 742 |
suc_pc: "Suc pc < length ins" and |
743 |
phi_suc: "phi C sig ! Suc pc = Some (ST', LT')" and |
|
744 |
less: "G \<turnstile> (Class X # ST, LT) <=s (ST', LT')" |
|
12516 | 745 |
by (unfold wt_instr_def eff_def norm_eff_def) auto |
10920 | 746 |
|
747 |
obtain oref xp' where |
|
12516 | 748 |
new_Addr: "new_Addr hp = (oref,xp')" |
749 |
by (cases "new_Addr hp") |
|
750 |
with ins no_x |
|
751 |
obtain hp: "hp oref = None" and "xp' = None" |
|
752 |
by (auto dest: new_AddrD simp add: raise_system_xcpt_def) |
|
753 |
||
754 |
with exec ins meth new_Addr |
|
755 |
have state': |
|
756 |
"state' = Norm (hp(oref\<mapsto>(X, init_vars (fields (G, X)))), |
|
757 |
(Addr oref # stk, loc, C, sig, Suc pc) # frs)" |
|
758 |
(is "state' = Norm (?hp', ?f # frs)") |
|
759 |
by simp |
|
10920 | 760 |
moreover |
12516 | 761 |
from wf hp heap_ok is_class_X |
762 |
have hp': "G \<turnstile>h ?hp' \<surd>" |
|
763 |
by - (rule hconf_newref, auto simp add: oconf_def dest: fields_is_type) |
|
10920 | 764 |
moreover |
12516 | 765 |
from hp |
766 |
have sup: "hp \<le>| ?hp'" by (rule hext_new) |
|
767 |
from hp frame less suc_pc wf |
|
768 |
have "correct_frame G ?hp' (ST', LT') maxl ins ?f" |
|
769 |
apply (unfold correct_frame_def sup_state_conv) |
|
770 |
apply (clarsimp simp add: map_eq_Cons conf_def fun_upd_apply approx_val_def) |
|
771 |
apply (blast intro: approx_stk_sup_heap approx_loc_sup_heap sup) |
|
772 |
done |
|
773 |
moreover |
|
774 |
from hp frames wf heap_ok is_class_X |
|
775 |
have "correct_frames G ?hp' phi rT sig frs" |
|
776 |
by - (rule correct_frames_newref, |
|
777 |
auto simp add: oconf_def dest: fields_is_type) |
|
10920 | 778 |
ultimately |
12516 | 779 |
show ?thesis |
780 |
by (simp add: is_class_C meth phi_suc correct_state_def del: not_None_eq) |
|
10920 | 781 |
qed |
11085 | 782 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
783 |
lemmas [simp del] = split_paired_Ex |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
784 |
|
12516 | 785 |
|
10626
46bcddfe9e7b
update for changes in Correct.thy and class/is_class defs
kleing
parents:
10612
diff
changeset
|
786 |
lemma Invoke_correct: |
46bcddfe9e7b
update for changes in Correct.thy and class/is_class defs
kleing
parents:
10612
diff
changeset
|
787 |
"[| wt_jvm_prog G phi; |
12516 | 788 |
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
789 |
ins ! pc = Invoke C' mn pTs; |
12516 | 790 |
wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
791 |
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
12516 | 792 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>; |
793 |
fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None |] |
|
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
794 |
==> G,phi \<turnstile>JVM state'\<surd>" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
795 |
proof - |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
796 |
assume wtprog: "wt_jvm_prog G phi" |
12516 | 797 |
assume method: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
798 |
assume ins: "ins ! pc = Invoke C' mn pTs" |
12516 | 799 |
assume wti: "wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
800 |
assume state': "Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs)" |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
801 |
assume approx: "G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>" |
12516 | 802 |
assume no_xcp: "fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
803 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
804 |
from wtprog |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
805 |
obtain wfmb where |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
806 |
wfprog: "wf_prog wfmb G" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
807 |
by (simp add: wt_jvm_prog_def) |
10626
46bcddfe9e7b
update for changes in Correct.thy and class/is_class defs
kleing
parents:
10612
diff
changeset
|
808 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
809 |
from ins method approx |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
810 |
obtain s where |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
811 |
heap_ok: "G\<turnstile>h hp\<surd>" and |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
812 |
phi_pc: "phi C sig!pc = Some s" and |
10626
46bcddfe9e7b
update for changes in Correct.thy and class/is_class defs
kleing
parents:
10612
diff
changeset
|
813 |
is_class_C: "is_class G C" and |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
814 |
frame: "correct_frame G hp s maxl ins (stk, loc, C, sig, pc)" and |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
815 |
frames: "correct_frames G hp phi rT sig frs" |
10626
46bcddfe9e7b
update for changes in Correct.thy and class/is_class defs
kleing
parents:
10612
diff
changeset
|
816 |
by (clarsimp simp add: correct_state_def iff del: not_None_eq) |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
817 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
818 |
from ins wti phi_pc |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
819 |
obtain apTs X ST LT D' rT body where |
10626
46bcddfe9e7b
update for changes in Correct.thy and class/is_class defs
kleing
parents:
10612
diff
changeset
|
820 |
is_class: "is_class G C'" and |
11252 | 821 |
s: "s = (rev apTs @ X # ST, LT)" and |
822 |
l: "length apTs = length pTs" and |
|
823 |
X: "G\<turnstile> X \<preceq> Class C'" and |
|
824 |
w: "\<forall>x\<in>set (zip apTs pTs). x \<in> widen G" and |
|
825 |
mC':"method (G, C') (mn, pTs) = Some (D', rT, body)" and |
|
826 |
pc: "Suc pc < length ins" and |
|
12516 | 827 |
eff: "G \<turnstile> norm_eff (Invoke C' mn pTs) G (Some s) <=' phi C sig!Suc pc" |
828 |
by (simp add: wt_instr_def eff_def del: not_None_eq) |
|
829 |
(elim exE conjE, rule that) |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
830 |
|
12516 | 831 |
from eff |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
832 |
obtain ST' LT' where |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
833 |
s': "phi C sig ! Suc pc = Some (ST', LT')" |
12516 | 834 |
by (simp add: norm_eff_def split_paired_Ex) blast |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
835 |
|
12516 | 836 |
from X |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
837 |
obtain T where |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
838 |
X_Ref: "X = RefT T" |
12516 | 839 |
by - (drule widen_RefT2, erule exE, rule that) |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
840 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
841 |
from s ins frame |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
842 |
obtain |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
843 |
a_stk: "approx_stk G hp stk (rev apTs @ X # ST)" and |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
844 |
a_loc: "approx_loc G hp loc LT" and |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
845 |
suc_l: "length loc = Suc (length (snd sig) + maxl)" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
846 |
by (simp add: correct_frame_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
847 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
848 |
from a_stk |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
849 |
obtain opTs stk' oX where |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
850 |
opTs: "approx_stk G hp opTs (rev apTs)" and |
10496 | 851 |
oX: "approx_val G hp oX (OK X)" and |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
852 |
a_stk': "approx_stk G hp stk' ST" and |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
853 |
stk': "stk = opTs @ oX # stk'" and |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
854 |
l_o: "length opTs = length apTs" |
12516 | 855 |
"length stk' = length ST" |
856 |
by - (drule approx_stk_append, auto) |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
857 |
|
12516 | 858 |
from oX X_Ref |
859 |
have oX_conf: "G,hp \<turnstile> oX ::\<preceq> RefT T" |
|
860 |
by (simp add: approx_val_def) |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
861 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
862 |
from stk' l_o l |
11252 | 863 |
have oX_pos: "last (take (Suc (length pTs)) stk) = oX" by simp |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
864 |
|
12516 | 865 |
with state' method ins no_xcp oX_conf |
866 |
obtain ref where oX_Addr: "oX = Addr ref" |
|
867 |
by (auto simp add: raise_system_xcpt_def dest: conf_RefTD) |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
868 |
|
12516 | 869 |
with oX_conf X_Ref |
870 |
obtain obj D where |
|
871 |
loc: "hp ref = Some obj" and |
|
872 |
obj_ty: "obj_ty obj = Class D" and |
|
873 |
D: "G \<turnstile> Class D \<preceq> X" |
|
874 |
by (auto simp add: conf_def) blast |
|
875 |
||
876 |
with X_Ref obtain X' where X': "X = Class X'" |
|
877 |
by (blast dest: widen_Class) |
|
878 |
||
879 |
with X have X'_subcls: "G \<turnstile> X' \<preceq>C C'" by simp |
|
10612
779af7c58743
improved superclass entry for classes and definition status of is_class, class
oheimb
parents:
10592
diff
changeset
|
880 |
|
12516 | 881 |
with mC' wfprog |
882 |
obtain D0 rT0 maxs0 maxl0 ins0 et0 where |
|
883 |
mX: "method (G, X') (mn, pTs) = Some (D0, rT0, maxs0, maxl0, ins0, et0)" "G\<turnstile>rT0\<preceq>rT" |
|
884 |
by (auto dest: subtype_widen_methd intro: that) |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
885 |
|
12516 | 886 |
from X' D have D_subcls: "G \<turnstile> D \<preceq>C X'" by simp |
887 |
||
888 |
with wfprog mX |
|
889 |
obtain D'' rT' mxs' mxl' ins' et' where |
|
890 |
mD: "method (G, D) (mn, pTs) = Some (D'', rT', mxs', mxl', ins', et')" |
|
891 |
"G \<turnstile> rT' \<preceq> rT0" |
|
892 |
by (auto dest: subtype_widen_methd intro: that) |
|
893 |
||
894 |
from mX mD have rT': "G \<turnstile> rT' \<preceq> rT" by - (rule widen_trans) |
|
895 |
||
896 |
from is_class X'_subcls D_subcls |
|
897 |
have is_class_D: "is_class G D" by (auto dest: subcls_is_class2) |
|
898 |
||
899 |
with mD wfprog |
|
900 |
obtain mD'': |
|
901 |
"method (G, D'') (mn, pTs) = Some (D'', rT', mxs', mxl', ins', et')" |
|
902 |
"is_class G D''" |
|
903 |
by (auto dest: method_in_md) |
|
904 |
||
905 |
from loc obj_ty have "fst (the (hp ref)) = D" by (simp add: obj_ty_def) |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
906 |
|
12516 | 907 |
with oX_Addr oX_pos state' method ins stk' l_o l loc obj_ty mD no_xcp |
908 |
have state'_val: |
|
909 |
"state' = |
|
910 |
Norm (hp, ([], Addr ref # rev opTs @ replicate mxl' arbitrary, |
|
911 |
D'', (mn, pTs), 0) # (opTs @ Addr ref # stk', loc, C, sig, pc) # frs)" |
|
912 |
(is "state' = Norm (hp, ?f # ?f' # frs)") |
|
913 |
by (simp add: raise_system_xcpt_def) |
|
914 |
||
915 |
from wtprog mD'' |
|
916 |
have start: "wt_start G D'' pTs mxl' (phi D'' (mn, pTs)) \<and> ins' \<noteq> []" |
|
917 |
by (auto dest: wt_jvm_prog_impl_wt_start) |
|
918 |
||
919 |
then obtain LT0 where |
|
920 |
LT0: "phi D'' (mn, pTs) ! 0 = Some ([], LT0)" |
|
921 |
by (clarsimp simp add: wt_start_def sup_state_conv) |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
922 |
|
12516 | 923 |
have c_f: "correct_frame G hp ([], LT0) mxl' ins' ?f" |
924 |
proof - |
|
925 |
from start LT0 |
|
926 |
have sup_loc: |
|
927 |
"G \<turnstile> (OK (Class D'') # map OK pTs @ replicate mxl' Err) <=l LT0" |
|
928 |
(is "G \<turnstile> ?LT <=l LT0") |
|
929 |
by (simp add: wt_start_def sup_state_conv) |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
930 |
|
12516 | 931 |
have r: "approx_loc G hp (replicate mxl' arbitrary) (replicate mxl' Err)" |
932 |
by (simp add: approx_loc_def list_all2_def set_replicate_conv_if) |
|
933 |
||
934 |
from wfprog mD is_class_D |
|
935 |
have "G \<turnstile> Class D \<preceq> Class D''" |
|
936 |
by (auto dest: method_wf_mdecl) |
|
937 |
with obj_ty loc |
|
938 |
have a: "approx_val G hp (Addr ref) (OK (Class D''))" |
|
939 |
by (simp add: approx_val_def conf_def) |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
940 |
|
12516 | 941 |
from opTs w l l_o wfprog |
942 |
have "approx_stk G hp opTs (rev pTs)" |
|
943 |
by (auto elim!: approx_stk_all_widen simp add: zip_rev) |
|
944 |
hence "approx_stk G hp (rev opTs) pTs" by (subst approx_stk_rev) |
|
945 |
||
946 |
with r a l_o l |
|
947 |
have "approx_loc G hp (Addr ref # rev opTs @ replicate mxl' arbitrary) ?LT" |
|
948 |
(is "approx_loc G hp ?lt ?LT") |
|
949 |
by (auto simp add: approx_loc_append approx_stk_def) |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
950 |
|
12516 | 951 |
from this sup_loc wfprog |
952 |
have "approx_loc G hp ?lt LT0" by (rule approx_loc_widen) |
|
953 |
with start l_o l |
|
954 |
show ?thesis by (simp add: correct_frame_def) |
|
955 |
qed |
|
956 |
||
957 |
from state'_val heap_ok mD'' ins method phi_pc s X' l mX |
|
958 |
frames s' LT0 c_f is_class_C stk' oX_Addr frame |
|
959 |
show ?thesis by (simp add: correct_state_def) (intro exI conjI, blast) |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
960 |
qed |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
961 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
962 |
lemmas [simp del] = map_append |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
963 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
964 |
lemma Return_correct: |
10626
46bcddfe9e7b
update for changes in Correct.thy and class/is_class defs
kleing
parents:
10612
diff
changeset
|
965 |
"[| wt_jvm_prog G phi; |
12516 | 966 |
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
967 |
ins ! pc = Return; |
12516 | 968 |
wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
969 |
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
12516 | 970 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
971 |
==> G,phi \<turnstile>JVM state'\<surd>" |
12516 | 972 |
proof - |
973 |
assume wt_prog: "wt_jvm_prog G phi" |
|
974 |
assume meth: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)" |
|
975 |
assume ins: "ins ! pc = Return" |
|
976 |
assume wt: "wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc" |
|
977 |
assume s': "Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs)" |
|
978 |
assume correct: "G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>" |
|
979 |
||
980 |
from wt_prog |
|
981 |
obtain wfmb where wf: "wf_prog wfmb G" by (simp add: wt_jvm_prog_def) |
|
982 |
||
983 |
from meth ins s' |
|
984 |
have "frs = [] \<Longrightarrow> ?thesis" by (simp add: correct_state_def) |
|
985 |
moreover |
|
986 |
{ fix f frs' |
|
987 |
assume frs': "frs = f#frs'" |
|
988 |
moreover |
|
989 |
obtain stk' loc' C' sig' pc' where |
|
990 |
f: "f = (stk',loc',C',sig',pc')" by (cases f) |
|
991 |
moreover |
|
992 |
obtain mn pt where |
|
993 |
sig: "sig = (mn,pt)" by (cases sig) |
|
994 |
moreover |
|
995 |
note meth ins s' |
|
996 |
ultimately |
|
997 |
have state': |
|
998 |
"state' = (None,hp,(hd stk#(drop (1+length pt) stk'),loc',C',sig',pc'+1)#frs')" |
|
999 |
(is "state' = (None,hp,?f'#frs')") |
|
1000 |
by simp |
|
1001 |
||
1002 |
from correct meth |
|
1003 |
obtain ST LT where |
|
1004 |
hp_ok: "G \<turnstile>h hp \<surd>" and |
|
1005 |
phi_pc: "phi C sig ! pc = Some (ST, LT)" and |
|
1006 |
frame: "correct_frame G hp (ST, LT) maxl ins (stk,loc,C,sig,pc)" and |
|
1007 |
frames: "correct_frames G hp phi rT sig frs" |
|
1008 |
by (simp add: correct_state_def, clarify, blast) |
|
1009 |
||
1010 |
from phi_pc ins wt |
|
1011 |
obtain T ST' where "ST = T # ST'" "G \<turnstile> T \<preceq> rT" |
|
1012 |
by (simp add: wt_instr_def) blast |
|
1013 |
with wf frame |
|
1014 |
have hd_stk: "G,hp \<turnstile> (hd stk) ::\<preceq> rT" |
|
1015 |
by (auto simp add: correct_frame_def elim: conf_widen) |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1016 |
|
12516 | 1017 |
from f frs' frames sig |
1018 |
obtain apTs ST0' ST' LT' D D' D'' rT' rT'' maxs' maxl' ins' et' body where |
|
1019 |
phi': "phi C' sig' ! pc' = Some (ST',LT')" and |
|
1020 |
class': "is_class G C'" and |
|
1021 |
meth': "method (G,C') sig' = Some (C',rT',maxs',maxl',ins',et')" and |
|
1022 |
ins': "ins' ! pc' = Invoke D' mn pt" and |
|
1023 |
frame': "correct_frame G hp (ST', LT') maxl' ins' f" and |
|
1024 |
frames':"correct_frames G hp phi rT' sig' frs'" and |
|
1025 |
rT'': "G \<turnstile> rT \<preceq> rT''" and |
|
1026 |
meth'': "method (G, D) sig = Some (D'', rT'', body)" and |
|
1027 |
ST0': "ST' = rev apTs @ Class D # ST0'" and |
|
1028 |
len': "length apTs = length pt" |
|
1029 |
by clarsimp blast |
|
1030 |
||
1031 |
from f frame' |
|
1032 |
obtain |
|
1033 |
stk': "approx_stk G hp stk' ST'" and |
|
1034 |
loc': "approx_loc G hp loc' LT'" and |
|
1035 |
pc': "pc' < length ins'" and |
|
1036 |
lloc':"length loc' = Suc (length (snd sig') + maxl')" |
|
1037 |
by (simp add: correct_frame_def) |
|
1038 |
||
1039 |
from wt_prog class' meth' pc' |
|
1040 |
have "wt_instr (ins'!pc') G rT' (phi C' sig') maxs' (length ins') et' pc'" |
|
1041 |
by (rule wt_jvm_prog_impl_wt_instr) |
|
1042 |
with ins' phi' sig |
|
1043 |
obtain apTs ST0 X ST'' LT'' body' rT0 mD where |
|
1044 |
phi_suc: "phi C' sig' ! Suc pc' = Some (ST'', LT'')" and |
|
1045 |
ST0: "ST' = rev apTs @ X # ST0" and |
|
1046 |
len: "length apTs = length pt" and |
|
1047 |
less: "G \<turnstile> (rT0 # ST0, LT') <=s (ST'', LT'')" and |
|
1048 |
methD': "method (G, D') sig = Some (mD, rT0, body')" and |
|
1049 |
lessD': "G \<turnstile> X \<preceq> Class D'" and |
|
1050 |
suc_pc': "Suc pc' < length ins'" |
|
1051 |
by (clarsimp simp add: wt_instr_def eff_def norm_eff_def) blast |
|
1052 |
||
1053 |
from len len' ST0 ST0' |
|
1054 |
have "X = Class D" by simp |
|
1055 |
with lessD' |
|
1056 |
have "G \<turnstile> D \<preceq>C D'" by simp |
|
1057 |
moreover |
|
1058 |
note wf meth'' methD' |
|
1059 |
ultimately |
|
1060 |
have "G \<turnstile> rT'' \<preceq> rT0" by (auto dest: subcls_widen_methd) |
|
1061 |
with wf hd_stk rT'' |
|
1062 |
have hd_stk': "G,hp \<turnstile> (hd stk) ::\<preceq> rT0" by (auto elim: conf_widen widen_trans) |
|
1063 |
||
1064 |
have frame'': |
|
1065 |
"correct_frame G hp (ST'',LT'') maxl' ins' ?f'" |
|
1066 |
proof - |
|
1067 |
from wf hd_stk' len stk' less ST0 |
|
1068 |
have "approx_stk G hp (hd stk # drop (1+length pt) stk') ST''" |
|
1069 |
by (auto simp add: map_eq_Cons sup_state_conv |
|
1070 |
dest!: approx_stk_append elim: conf_widen) |
|
1071 |
moreover |
|
1072 |
from wf loc' less |
|
1073 |
have "approx_loc G hp loc' LT''" by (simp add: sup_state_conv) blast |
|
1074 |
moreover |
|
1075 |
note suc_pc' lloc' |
|
1076 |
ultimately |
|
1077 |
show ?thesis by (simp add: correct_frame_def) |
|
1078 |
qed |
|
1079 |
||
1080 |
with state' frs' f meth hp_ok hd_stk phi_suc frames' meth' phi' class' |
|
1081 |
have ?thesis by (simp add: correct_state_def) |
|
1082 |
} |
|
1083 |
ultimately |
|
1084 |
show ?thesis by (cases frs) blast+ |
|
1085 |
qed |
|
1086 |
||
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1087 |
lemmas [simp] = map_append |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1088 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1089 |
lemma Goto_correct: |
10042 | 1090 |
"[| wf_prog wt G; |
12516 | 1091 |
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1092 |
ins ! pc = Goto branch; |
12516 | 1093 |
wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1094 |
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
1095 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] |
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
1096 |
==> G,phi \<turnstile>JVM state'\<surd>" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1097 |
apply (clarsimp simp add: defs1) |
11252 | 1098 |
apply fast |
9819 | 1099 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1100 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1101 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1102 |
lemma Ifcmpeq_correct: |
10042 | 1103 |
"[| wf_prog wt G; |
12516 | 1104 |
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1105 |
ins ! pc = Ifcmpeq branch; |
12516 | 1106 |
wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1107 |
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
1108 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] |
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
1109 |
==> G,phi \<turnstile>JVM state'\<surd>" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1110 |
apply (clarsimp simp add: defs1) |
11252 | 1111 |
apply fast |
9819 | 1112 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1113 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1114 |
lemma Pop_correct: |
10042 | 1115 |
"[| wf_prog wt G; |
12516 | 1116 |
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1117 |
ins ! pc = Pop; |
12516 | 1118 |
wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1119 |
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
1120 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] |
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
1121 |
==> G,phi \<turnstile>JVM state'\<surd>" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1122 |
apply (clarsimp simp add: defs1) |
11252 | 1123 |
apply fast |
9819 | 1124 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1125 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1126 |
lemma Dup_correct: |
10042 | 1127 |
"[| wf_prog wt G; |
12516 | 1128 |
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1129 |
ins ! pc = Dup; |
12516 | 1130 |
wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1131 |
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
1132 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] |
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
1133 |
==> G,phi \<turnstile>JVM state'\<surd>" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1134 |
apply (clarsimp simp add: defs1 map_eq_Cons) |
11252 | 1135 |
apply (blast intro: conf_widen) |
9819 | 1136 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1137 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1138 |
lemma Dup_x1_correct: |
10042 | 1139 |
"[| wf_prog wt G; |
12516 | 1140 |
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1141 |
ins ! pc = Dup_x1; |
12516 | 1142 |
wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1143 |
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
1144 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] |
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
1145 |
==> G,phi \<turnstile>JVM state'\<surd>" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1146 |
apply (clarsimp simp add: defs1 map_eq_Cons) |
11252 | 1147 |
apply (blast intro: conf_widen) |
9819 | 1148 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1149 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1150 |
lemma Dup_x2_correct: |
10042 | 1151 |
"[| wf_prog wt G; |
12516 | 1152 |
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1153 |
ins ! pc = Dup_x2; |
12516 | 1154 |
wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1155 |
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
1156 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] |
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
1157 |
==> G,phi \<turnstile>JVM state'\<surd>" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1158 |
apply (clarsimp simp add: defs1 map_eq_Cons) |
11252 | 1159 |
apply (blast intro: conf_widen) |
9819 | 1160 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1161 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1162 |
lemma Swap_correct: |
10042 | 1163 |
"[| wf_prog wt G; |
12516 | 1164 |
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1165 |
ins ! pc = Swap; |
12516 | 1166 |
wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1167 |
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
1168 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] |
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
1169 |
==> G,phi \<turnstile>JVM state'\<surd>" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1170 |
apply (clarsimp simp add: defs1 map_eq_Cons) |
11252 | 1171 |
apply (blast intro: conf_widen) |
9819 | 1172 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1173 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1174 |
lemma IAdd_correct: |
10042 | 1175 |
"[| wf_prog wt G; |
12516 | 1176 |
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1177 |
ins ! pc = IAdd; |
12516 | 1178 |
wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1179 |
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
1180 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] |
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
1181 |
==> G,phi \<turnstile>JVM state'\<surd>" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1182 |
apply (clarsimp simp add: defs1 map_eq_Cons approx_val_def conf_def) |
11252 | 1183 |
apply blast |
9819 | 1184 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1185 |
|
12516 | 1186 |
lemma Throw_correct: |
1187 |
"[| wf_prog wt G; |
|
1188 |
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); |
|
1189 |
ins ! pc = Throw; |
|
1190 |
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
|
1191 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>; |
|
1192 |
fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None |] |
|
1193 |
==> G,phi \<turnstile>JVM state'\<surd>" |
|
1194 |
by simp |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1195 |
|
12516 | 1196 |
|
1197 |
text {* |
|
1198 |
The next theorem collects the results of the sections above, |
|
1199 |
i.e.~exception handling and the execution step for each |
|
1200 |
instruction. It states type safety for single step execution: |
|
1201 |
in welltyped programs, a conforming state is transformed |
|
1202 |
into another conforming state when one instruction is executed. |
|
1203 |
*} |
|
1204 |
theorem instr_correct: |
|
10626
46bcddfe9e7b
update for changes in Correct.thy and class/is_class defs
kleing
parents:
10612
diff
changeset
|
1205 |
"[| wt_jvm_prog G phi; |
12516 | 1206 |
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1207 |
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
1208 |
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] |
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
1209 |
==> G,phi \<turnstile>JVM state'\<surd>" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1210 |
apply (frule wt_jvm_prog_impl_wt_instr_cor) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1211 |
apply assumption+ |
12516 | 1212 |
apply (cases "fst (exec_instr (ins!pc) G hp stk loc C sig pc frs)") |
1213 |
defer |
|
1214 |
apply (erule xcpt_correct, assumption+) |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1215 |
apply (cases "ins!pc") |
10897
697fab84709e
removed instructions Aconst_null+Bipush, introduced LitPush
kleing
parents:
10812
diff
changeset
|
1216 |
prefer 8 |
10626
46bcddfe9e7b
update for changes in Correct.thy and class/is_class defs
kleing
parents:
10612
diff
changeset
|
1217 |
apply (rule Invoke_correct, assumption+) |
10897
697fab84709e
removed instructions Aconst_null+Bipush, introduced LitPush
kleing
parents:
10812
diff
changeset
|
1218 |
prefer 8 |
10626
46bcddfe9e7b
update for changes in Correct.thy and class/is_class defs
kleing
parents:
10612
diff
changeset
|
1219 |
apply (rule Return_correct, assumption+) |
12516 | 1220 |
prefer 5 |
1221 |
apply (rule Getfield_correct, assumption+) |
|
1222 |
prefer 6 |
|
1223 |
apply (rule Checkcast_correct, assumption+) |
|
10612
779af7c58743
improved superclass entry for classes and definition status of is_class, class
oheimb
parents:
10592
diff
changeset
|
1224 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1225 |
apply (unfold wt_jvm_prog_def) |
10626
46bcddfe9e7b
update for changes in Correct.thy and class/is_class defs
kleing
parents:
10612
diff
changeset
|
1226 |
apply (rule Load_correct, assumption+) |
46bcddfe9e7b
update for changes in Correct.thy and class/is_class defs
kleing
parents:
10612
diff
changeset
|
1227 |
apply (rule Store_correct, assumption+) |
10897
697fab84709e
removed instructions Aconst_null+Bipush, introduced LitPush
kleing
parents:
10812
diff
changeset
|
1228 |
apply (rule LitPush_correct, assumption+) |
10626
46bcddfe9e7b
update for changes in Correct.thy and class/is_class defs
kleing
parents:
10612
diff
changeset
|
1229 |
apply (rule New_correct, assumption+) |
46bcddfe9e7b
update for changes in Correct.thy and class/is_class defs
kleing
parents:
10612
diff
changeset
|
1230 |
apply (rule Putfield_correct, assumption+) |
46bcddfe9e7b
update for changes in Correct.thy and class/is_class defs
kleing
parents:
10612
diff
changeset
|
1231 |
apply (rule Pop_correct, assumption+) |
46bcddfe9e7b
update for changes in Correct.thy and class/is_class defs
kleing
parents:
10612
diff
changeset
|
1232 |
apply (rule Dup_correct, assumption+) |
46bcddfe9e7b
update for changes in Correct.thy and class/is_class defs
kleing
parents:
10612
diff
changeset
|
1233 |
apply (rule Dup_x1_correct, assumption+) |
46bcddfe9e7b
update for changes in Correct.thy and class/is_class defs
kleing
parents:
10612
diff
changeset
|
1234 |
apply (rule Dup_x2_correct, assumption+) |
46bcddfe9e7b
update for changes in Correct.thy and class/is_class defs
kleing
parents:
10612
diff
changeset
|
1235 |
apply (rule Swap_correct, assumption+) |
46bcddfe9e7b
update for changes in Correct.thy and class/is_class defs
kleing
parents:
10612
diff
changeset
|
1236 |
apply (rule IAdd_correct, assumption+) |
46bcddfe9e7b
update for changes in Correct.thy and class/is_class defs
kleing
parents:
10612
diff
changeset
|
1237 |
apply (rule Goto_correct, assumption+) |
46bcddfe9e7b
update for changes in Correct.thy and class/is_class defs
kleing
parents:
10612
diff
changeset
|
1238 |
apply (rule Ifcmpeq_correct, assumption+) |
12516 | 1239 |
apply (rule Throw_correct, assumption+) |
9819 | 1240 |
done |
10626
46bcddfe9e7b
update for changes in Correct.thy and class/is_class defs
kleing
parents:
10612
diff
changeset
|
1241 |
|
11085 | 1242 |
section {* Main *} |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1243 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1244 |
lemma correct_state_impl_Some_method: |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
1245 |
"G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
1246 |
==> \<exists>meth. method (G,C) sig = Some(C,meth)" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1247 |
by (auto simp add: correct_state_def Let_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1248 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1249 |
|
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
1250 |
lemma BV_correct_1 [rule_format]: |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
1251 |
"!!state. [| wt_jvm_prog G phi; G,phi \<turnstile>JVM state\<surd>|] |
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
1252 |
==> exec (G,state) = Some state' --> G,phi \<turnstile>JVM state'\<surd>" |
9819 | 1253 |
apply (simp only: split_tupled_all) |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1254 |
apply (rename_tac xp hp frs) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1255 |
apply (case_tac xp) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1256 |
apply (case_tac frs) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1257 |
apply simp |
9819 | 1258 |
apply (simp only: split_tupled_all) |
1259 |
apply hypsubst |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1260 |
apply (frule correct_state_impl_Some_method) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1261 |
apply (force intro: instr_correct) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1262 |
apply (case_tac frs) |
9819 | 1263 |
apply simp_all |
1264 |
done |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1265 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1266 |
|
12516 | 1267 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1268 |
lemma L0: |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
1269 |
"[| xp=None; frs\<noteq>[] |] ==> (\<exists>state'. exec (G,xp,hp,frs) = Some state')" |
12516 | 1270 |
by (clarsimp simp add: neq_Nil_conv split_beta) |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1271 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1272 |
lemma L1: |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
1273 |
"[|wt_jvm_prog G phi; G,phi \<turnstile>JVM (xp,hp,frs)\<surd>; xp=None; frs\<noteq>[]|] |
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
1274 |
==> \<exists>state'. exec(G,xp,hp,frs) = Some state' \<and> G,phi \<turnstile>JVM state'\<surd>" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1275 |
apply (drule L0) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1276 |
apply assumption |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1277 |
apply (fast intro: BV_correct_1) |
9819 | 1278 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1279 |
|
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
1280 |
theorem BV_correct [rule_format]: |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
1281 |
"[| wt_jvm_prog G phi; G \<turnstile> s -jvm-> t |] ==> G,phi \<turnstile>JVM s\<surd> --> G,phi \<turnstile>JVM t\<surd>" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1282 |
apply (unfold exec_all_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1283 |
apply (erule rtrancl_induct) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1284 |
apply simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1285 |
apply (auto intro: BV_correct_1) |
9819 | 1286 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1287 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1288 |
theorem BV_correct_initial: |
10056 | 1289 |
"[| wt_jvm_prog G phi; |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10763
diff
changeset
|
1290 |
G \<turnstile> s0 -jvm-> (None,hp,(stk,loc,C,sig,pc)#frs); G,phi \<turnstile>JVM s0 \<surd>|] |
12516 | 1291 |
==> approx_stk G hp stk (fst (the (phi C sig ! pc))) \<and> |
1292 |
approx_loc G hp loc (snd (the (phi C sig ! pc)))" |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1293 |
apply (drule BV_correct) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1294 |
apply assumption+ |
10056 | 1295 |
apply (simp add: correct_state_def correct_frame_def split_def |
1296 |
split: option.splits) |
|
9819 | 1297 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1298 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
8011
diff
changeset
|
1299 |
end |