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