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