author  wenzelm 
Fri, 23 Sep 2011 21:51:49 +0200  
changeset 45068  3cc2ac688fd9 
parent 45054  73accf69135d 
child 53024  e0968e1f6fe9 
permissions  rwrr 
8011  1 
(* Title: HOL/MicroJava/BV/BVSpecTypeSafe.thy 
12516  2 
Author: Cornelia Pusch, Gerwin Klein 
8011  3 
Copyright 1999 Technische Universitaet Muenchen 
4 
*) 

5 

12911  6 
header {* \isaheader{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 

17 
section {* Preliminaries *} 

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 

44 
section {* Exception Handling *} 

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 

11085  585 
section {* Single Instructions *} 
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" 

892 
by (auto simp add: conf_def) blast 

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)" 
12516  950 
by (simp add: approx_loc_def list_all2_def set_replicate_conv_if) 
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" 

1055 
by clarsimp blast 

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'" 

1077 
by (clarsimp simp add: wt_instr_def eff_def norm_eff_def) blast 

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 