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