Up to index of Isabelle/HOL/jsr
theory BVSpecTypeSafe = Correct:(* Title: HOL/MicroJava/BV/BVSpecTypeSafe.thy
ID: $Id: BVSpecTypeSafe.html,v 1.1 2002/11/28 14:17:20 kleing Exp $
Author: Cornelia Pusch, Gerwin Klein
Copyright 1999 Technische Universitaet Muenchen
*)
header {* \isaheader{BV Type Safety Proof}\label{sec:BVSpecTypeSafe} *}
theory BVSpecTypeSafe = Correct:
text {*
This theory contains proof that the specification of the bytecode
verifier only admits type safe programs.
*}
section {* Preliminaries *}
text {*
Simp and intro setup for the type safety proof:
*}
lemmas defs1 = correct_state_def correct_frame_def wt_instr_def
eff_def norm_eff_def eff_bool_def
lemmas correctE = correct_stateE2 correct_frameE
declare eff_defs [simp del]
lemmas [simp del] = split_paired_All
text {*
If we have a welltyped program and a conforming state, we
can directly infer that the current instruction is well typed:
*}
lemma wt_jvm_prog_impl_wt_instr_cor:
"\<lbrakk> wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd> \<rbrakk>
\<Longrightarrow> wt_instr (ins!pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et pc"
apply (elim correct_stateE correct_frameE)
apply simp
apply (blast intro: wt_jvm_prog_impl_wt_instr)
done
section {* Exception Handling *}
text {*
Exceptions don't touch anything except the stack:
*}
lemma exec_instr_xcpt:
"(fst (exec_instr i G hp ihp stk vars Cl sig pc z frs) = Some xcp)
= (\<exists>stk'. exec_instr i G hp ihp stk vars Cl sig pc z frs =
(Some xcp, hp, ihp, (stk', vars, Cl, sig, pc, z)#frs))"
by (cases i, auto simp add: split_beta split: split_if_asm)
text {*
Relates @{text match_any} from the Bytecode Verifier with
@{text match_exception_table} from the operational semantics:
*}
lemma in_match_any:
"match_exception_table G xcpt pc et = Some pc' \<Longrightarrow>
\<exists>C. C \<in> set (match_any G pc et) \<and> G \<turnstile> xcpt \<preceq>C C \<and>
match_exception_table G C pc et = Some pc'"
(is "PROP ?P et" is "?match et \<Longrightarrow> ?match_any et")
proof (induct et)
show "PROP ?P []" by simp
fix e es
assume IH: "PROP ?P es"
assume match: "?match (e#es)"
obtain start_pc end_pc handler_pc catch_type where
[simp]: "e = (start_pc, end_pc, handler_pc, catch_type)" by (cases e)
from IH match
show "?match_any (e#es)"
proof (cases "match_exception_entry G xcpt pc e")
case False
with match
have "match_exception_table G xcpt pc es = Some pc'" by simp
with IH
obtain C where
set: "C \<in> set (match_any G pc es)" and
C: "G \<turnstile> xcpt \<preceq>C C" and
m: "match_exception_table G C pc es = Some pc'" by blast
from set
have "C \<in> set (match_any G pc (e#es))" by simp
moreover
from False C
have "¬ match_exception_entry G C pc e"
by - (erule contrapos_nn,
auto simp add: match_exception_entry_def elim: rtrancl_trans)
with m
have "match_exception_table G C pc (e#es) = Some pc'" by simp
moreover note C
ultimately
show ?thesis by blast
next
case True with match
have "match_exception_entry G catch_type pc e"
by (simp add: match_exception_entry_def)
moreover
from True match
obtain
"start_pc \<le> pc"
"pc < end_pc"
"G \<turnstile> xcpt \<preceq>C catch_type"
"handler_pc = pc'"
by (simp add: match_exception_entry_def)
ultimately
show ?thesis by auto
qed
qed
lemma match_et_imp_match:
"match_exception_table G X pc et = Some handler
\<Longrightarrow> match G X pc et = [X]"
apply (simp add: match_some_entry)
apply (induct et)
apply (auto split: split_if_asm)
done
lemma imageE2:
"x \<in> A \<Longrightarrow> y = f x \<Longrightarrow> y \<in> f ` A"
by simp
text {*
We can prove separately that the recursive search for exception
handlers (@{text find_handler}) in the frame stack results in
a conforming state (if there was no matching exception handler
in the current frame). We require that the exception is a valid,
initialized heap address, and that the state before the exception
occured conforms.
*}
lemma uncaught_xcpt_correct:
"\<And>f. \<lbrakk> wt_jvm_prog G phi; xcp = Addr adr; hp adr = Some T; is_init hp ihp xcp;
G,phi \<turnstile>JVM (None, hp, ihp, f#frs)\<surd> \<rbrakk>
\<Longrightarrow> G,phi \<turnstile>JVM (find_handler G (Some xcp) hp ihp frs)\<surd>"
(is "\<And>f. \<lbrakk> ?wt; ?adr; ?hp; ?init; ?correct (None, hp, ihp, f#frs) \<rbrakk> \<Longrightarrow> ?correct (?find frs)")
proof (induct frs)
-- "the base case is trivial, as it should be"
show "?correct (?find [])" by (simp add: correct_state_def)
-- "we will need both forms @{text wt_jvm_prog} and @{text wf_prog} later"
assume wt: ?wt
then obtain mb where wf: "wf_prog mb G" by (simp add: wt_jvm_prog_def)
-- "these do not change in the induction:"
assume adr: ?adr
assume hp: ?hp
assume init: ?init
-- "the assumption for the cons case:"
fix f f' frs' assume cr: "?correct (None, hp, ihp, f#f'#frs')"
-- "the induction hypothesis as produced by Isabelle, immediatly simplified
with the fixed assumptions above"
assume "\<And>f. \<lbrakk> ?wt; ?adr; ?hp; ?init; ?correct (None, hp, ihp, f#frs') \<rbrakk> \<Longrightarrow> ?correct (?find frs')"
with wt adr hp init
have IH: "\<And>f. ?correct (None, hp, ihp, f#frs') \<Longrightarrow> ?correct (?find frs')" by blast
obtain stk loc C sig pc r where f' [simp]: "f' = (stk,loc,C,sig,pc,r)"
by (cases f')
from cr have cr': "?correct (None, hp, ihp, f'#frs')"
by (unfold correct_state_def, clarsimp) blast
then obtain rT maxs maxl ins et where
meth: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
by (fastsimp elim!: correct_stateE)
hence [simp]: "ex_table_of (snd (snd (the (method (G, C) sig)))) = et" by simp
show "?correct (?find (f'#frs'))"
proof (cases "match_exception_table G (cname_of hp xcp) pc et")
case None
with cr' IH
show ?thesis by simp
next
fix handler_pc
assume match: "match_exception_table G (cname_of hp xcp) pc et = Some handler_pc"
(is "?match (cname_of hp xcp) = _")
from wt meth cr' [simplified]
have wti: "wt_instr (ins!pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et pc"
by (rule wt_jvm_prog_impl_wt_instr_cor)
from cr meth
obtain C' mn pts ST LT z where
ins: "ins ! pc = Invoke C' mn pts \<or> ins ! pc = Invoke_special C' mn pts" and
phi: "((ST, LT),z) \<in> phi C sig ! pc" and
frm: "correct_frame G hp ihp (ST,LT) maxl ins (stk, loc, C, sig, pc, r)" and
frms: "correct_frames G hp ihp phi rT sig z r frs'"
by (simp add: correct_state_def) fast
from match
obtain D where
in_any: "D \<in> set (match_any G pc et)" and
D: "G \<turnstile> cname_of hp xcp \<preceq>C D" and
match': "?match D = Some handler_pc"
by (blast dest: in_match_any)
from ins have "xcpt_names (ins ! pc, G, pc, et) = match_any G pc et" by auto
with wti phi have
"\<forall>D\<in>set (match_any G pc et). the (?match D) < length ins \<and>
(([Init (Class D)], LT),z) \<in> phi C sig!the (?match D)"
apply -
apply (unfold wt_instr_def xcpt_eff_def eff_def)
apply clarsimp
apply (drule bspec)
apply (rule UnI2)
apply (rule imageI)
apply assumption
apply clarsimp
apply (erule subsetD)
apply (erule imageE2)
apply simp
done
with in_any match' obtain
pc: "handler_pc < length ins"
"(([Init (Class D)], LT),z) \<in> phi C sig ! handler_pc"
by auto
from frm obtain
len: "length loc = 1+length (snd sig)+maxl" and
loc: "approx_loc G hp ihp loc LT" and
csi: "consistent_init stk loc (ST, LT) ihp" and
cor: "(fst sig = init \<longrightarrow>
corresponds stk loc (ST, LT) ihp (fst r) (PartInit C) \<and>
(\<exists>l. fst r = Addr l \<and> hp l \<noteq> None \<and> (ihp l = PartInit C \<or> (\<exists>C'. ihp l = Init (Class C')))))"
by (fastsimp elim!: correct_frameE)
let ?f = "([xcp], loc, C, sig, handler_pc, r)"
have "correct_frame G hp ihp ([Init (Class D)], LT) maxl ins ?f"
proof -
from D adr hp
have "G,hp \<turnstile> xcp ::\<preceq> Class D" by (simp add: conf_def obj_ty_def)
with init
have "approx_val G hp ihp xcp (OK (Init (Class D)))"
by (simp add: approx_val_def iconf_def)
with len pc csi cor loc
show ?thesis
by (simp add: correct_frame_def consistent_init_xcp)
(blast intro: corresponds_xcp)
qed
with cr' match meth pc frms
show ?thesis by (unfold correct_state_def) auto
qed
qed
text {*
The requirement of lemma @{text uncaught_xcpt_correct} (that
the exception is a valid, initialized reference on the heap) is always met
for welltyped instructions and conformant states:
*}
lemma exec_instr_xcpt_hp:
assumes xcpt: "fst (exec_instr (ins!pc) G hp ihp stk vars Cl sig pc r frs) = Some xcp"
assumes wt: "wt_instr (ins!pc) G Cl rT (phi C sig) maxs (fst sig=init) (length ins) et pc"
assumes correct: "G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd>"
shows "\<exists>adr T. xcp = Addr adr \<and> hp adr = Some T \<and> is_init hp ihp xcp"
proof -
note [simp] = split_beta raise_system_xcpt_def
note [split] = split_if_asm option.split_asm
from correct have pre: "preallocated hp ihp" ..
with xcpt show ?thesis
proof (cases "ins!pc")
case New with xcpt pre
show ?thesis by (auto dest: new_Addr_OutOfMemory dest!: preallocatedD)
next
case Throw
from correct obtain ST LT z where
"((ST, LT), z) \<in> phi C sig ! pc"
"approx_stk G hp ihp stk ST"
by (blast elim: correct_stateE correct_frameE)
with Throw wt xcpt pre show ?thesis
apply (unfold wt_instr_def)
apply clarsimp
apply (drule bspec, assumption)
apply (clarsimp simp add: approx_val_def iconf_def)
apply (blast dest: non_npD)+
done
next
case Invoke_special with xcpt pre
show ?thesis by (auto dest: new_Addr_OutOfMemory dest!: preallocatedD)
qed (auto dest!: preallocatedD)
qed
lemma cname_of_xcp [intro]:
"\<lbrakk>preallocated hp ihp; xcp = Addr (XcptRef x)\<rbrakk> \<Longrightarrow> cname_of hp xcp = Xcpt x"
by (auto elim: preallocatedE [of hp ihp x])
lemma prealloc_is_init [simp]:
"preallocated hp ihp \<Longrightarrow> is_init hp ihp (Addr (XcptRef x))"
by (drule preallocatedD) blast
thm wt_jvm_progD [intro?]
lemma wt_jvm_progE [intro?]:
"wt_jvm_prog G phi \<Longrightarrow> (\<And>wt. wf_prog wt G \<Longrightarrow> P) \<Longrightarrow> P"
by (simp add: wt_jvm_prog_def)
text {*
Finally we can state that the next state always conforms when an exception occured:
*}
lemma xcpt_correct:
assumes wtp: "wt_jvm_prog G phi"
assumes meth: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
assumes wt: "wt_instr (ins!pc) G C rT (phi C sig) maxs (fst sig=init) (length ins) et pc"
assumes xp: "fst (exec_instr (ins!pc) G hp ihp stk loc C sig pc r frs) = Some xcp"
assumes s': "Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)"
assumes correct: "G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd>"
shows "G,phi \<turnstile>JVM state'\<surd>"
proof -
from wtp obtain wfmb where wf: "wf_prog wfmb G" ..
note xp' = meth s' xp
note wtp
moreover
from xp wt correct
obtain adr T where
adr: "xcp = Addr adr" "hp adr = Some T" "is_init hp ihp xcp"
by (blast dest: exec_instr_xcpt_hp)
moreover
note correct
ultimately
have "G,phi \<turnstile>JVM find_handler G (Some xcp) hp ihp frs \<surd>" by (rule uncaught_xcpt_correct)
with xp'
have "match_exception_table G (cname_of hp xcp) pc et = None \<Longrightarrow> ?thesis"
(is "?m (cname_of hp xcp) = _ \<Longrightarrow> _" is "?match = _ \<Longrightarrow> _")
by (clarsimp simp add: exec_instr_xcpt split_beta)
moreover
{ fix handler assume some_handler: "?match = Some handler"
from correct meth obtain ST LT z where
hp_ok: "G \<turnstile>h hp \<surd>" and
h_ini: "h_init G hp ihp" and
prehp: "preallocated hp ihp" and
class: "is_class G C" and
phi_pc: "((ST,LT),z) \<in> phi C sig ! pc" and
frame: "correct_frame G hp ihp (ST, LT) maxl ins (stk, loc, C, sig, pc, r)" and
frames: "correct_frames G hp ihp phi rT sig z r frs"
..
from frame obtain
stk: "approx_stk G hp ihp stk ST" and
loc: "approx_loc G hp ihp loc LT" and
pc: "pc < length ins" and
len: "length loc = length (snd sig)+maxl+1" and
cin: "consistent_init stk loc (ST, LT) ihp" and
cor: "fst sig = init \<longrightarrow>
corresponds stk loc (ST, LT) ihp (fst r) (PartInit C) \<and>
(\<exists>l. fst r = Addr l \<and> hp l \<noteq> None \<and> (ihp l = PartInit C \<or> (\<exists>C'. ihp l = Init (Class C'))))"
..
from wt obtain
eff: "\<forall>(pc', s')\<in>set (xcpt_eff (ins!pc) G pc (phi C sig!pc) et).
pc' < length ins \<and> s' \<subseteq> phi C sig!pc'"
by (simp add: wt_instr_def eff_def)
from some_handler xp'
have state':
"state' = (None, hp, ihp, ([xcp], loc, C, sig, handler, r)#frs)"
by (cases "ins!pc", auto simp add: raise_system_xcpt_def split_beta
split: split_if_asm) -- "takes long!"
let ?f' = "([xcp], loc, C, sig, handler, r)"
from eff
obtain ST' where
phi_pc': "((ST', LT),z) \<in> phi C sig ! handler" and
frame': "correct_frame G hp ihp (ST',LT) maxl ins ?f'"
proof (cases "ins!pc")
case Return -- "can't generate exceptions:"
with xp' have False by (simp add: split_beta split: split_if_asm)
thus ?thesis ..
next
let ?C = "Init (Class (Xcpt OutOfMemory))"
case New
with some_handler xp'
have xcp: "xcp = Addr (XcptRef OutOfMemory)"
by (simp add: raise_system_xcpt_def split_beta new_Addr_OutOfMemory)
with prehp have "cname_of hp xcp = Xcpt OutOfMemory" ..
with New some_handler phi_pc eff
have
phi': "(([?C], LT),z) \<in> phi C sig ! handler" and
pc': "handler < length ins"
by (auto simp add: xcpt_eff_def match_et_imp_match)
note phi'
moreover
{ from xcp prehp
have "G,hp \<turnstile> xcp ::\<preceq> Class (Xcpt OutOfMemory)"
by (auto simp add: conf_def obj_ty_def dest!: preallocatedD)
with xcp prehp
have "approx_val G hp ihp xcp (OK ?C)"
by (simp add: iconf_def approx_val_def)
with wf pc' len loc cor cin
have "correct_frame G hp ihp ([?C],LT) maxl ins ?f'"
by (simp add: consistent_init_xcp correct_frame_def)
(blast intro: corresponds_xcp)
}
ultimately
show ?thesis by (rule that)
next
let ?C = "Init (Class (Xcpt NullPointer))"
case Getfield
with some_handler xp'
have xcp: "xcp = Addr (XcptRef NullPointer)"
by (simp add: raise_system_xcpt_def split_beta split: split_if_asm)
with prehp have "cname_of hp xcp = Xcpt NullPointer" ..
with Getfield some_handler phi_pc eff
have
phi': "(([?C],LT),z) \<in> phi C sig ! handler" and
pc': "handler < length ins"
by (auto simp add: xcpt_eff_def match_et_imp_match)
note phi'
moreover
{ from xcp prehp
have "approx_val G hp ihp xcp (OK ?C)"
by (auto simp add: iconf_def conf_def obj_ty_def approx_val_def dest!: preallocatedD)
with wf pc' len loc cor cin
have "correct_frame G hp ihp ([?C],LT) maxl ins ?f'"
by (simp add: consistent_init_xcp correct_frame_def)
(blast intro: corresponds_xcp)
}
ultimately
show ?thesis by (rule that)
next
let ?C = "Init (Class (Xcpt NullPointer))"
case Putfield
with some_handler xp'
have xcp: "xcp = Addr (XcptRef NullPointer)"
by (simp add: raise_system_xcpt_def split_beta split: split_if_asm)
with prehp have "cname_of hp xcp = Xcpt NullPointer" ..
with Putfield some_handler phi_pc eff
have
phi': "(([?C],LT),z) \<in> phi C sig ! handler" and
pc': "handler < length ins"
by (auto simp add: xcpt_eff_def match_et_imp_match)
note phi'
moreover
{ from xcp prehp
have "approx_val G hp ihp xcp (OK ?C)"
by (auto simp add: iconf_def conf_def obj_ty_def approx_val_def dest!: preallocatedD)
with wf pc' len loc cor cin
have "correct_frame G hp ihp ([?C],LT) maxl ins ?f'"
by (simp add: consistent_init_xcp correct_frame_def)
(blast intro: corresponds_xcp)
}
ultimately
show ?thesis by (rule that)
next
let ?X = ClassCast
let ?C = "Init (Class (Xcpt ?X))"
case Checkcast
with some_handler xp'
have xcp: "xcp = Addr (XcptRef ?X)"
by (simp add: raise_system_xcpt_def split_beta split: split_if_asm)
with prehp have "cname_of hp xcp = Xcpt ?X" ..
with Checkcast some_handler phi_pc eff
have
phi': "(([?C],LT),z) \<in> phi C sig ! handler" and
pc': "handler < length ins"
by (auto simp add: xcpt_eff_def match_et_imp_match)
note phi'
moreover
{ from xcp prehp
have "approx_val G hp ihp xcp (OK ?C)"
by (auto simp add: iconf_def conf_def obj_ty_def approx_val_def dest!: preallocatedD)
with wf pc' len loc cor cin
have "correct_frame G hp ihp ([?C],LT) maxl ins ?f'"
by (simp add: consistent_init_xcp correct_frame_def)
(blast intro: corresponds_xcp)
}
ultimately
show ?thesis by (rule that)
next
case Invoke
with phi_pc eff
have
"\<forall>D\<in>set (match_any G pc et).
the (?m D) < length ins \<and> (([Init (Class D)], LT),z) \<in> phi C sig!the (?m D)"
by (clarsimp simp add: xcpt_eff_def) (fastsimp elim: imageE2)
moreover
from some_handler
obtain D where
"D \<in> set (match_any G pc et)" and
D: "G \<turnstile> cname_of hp xcp \<preceq>C D" and
"?m D = Some handler"
by (blast dest: in_match_any)
ultimately
have
pc': "handler < length ins" and
phi': "(([Init (Class D)], LT), z) \<in> phi C sig ! handler"
by auto
from xp wt correct
obtain addr T where
xcp: "xcp = Addr addr" "hp addr = Some T" "is_init hp ihp xcp"
by (blast dest: exec_instr_xcpt_hp)
note phi'
moreover
{ from xcp D
have "approx_val G hp ihp xcp (OK (Init (Class D)))"
by (auto simp add: iconf_def conf_def obj_ty_def approx_val_def dest!: preallocatedD)
with wf pc' len loc cor cin
have "correct_frame G hp ihp ([Init (Class D)],LT) maxl ins ?f'"
by (simp add: consistent_init_xcp correct_frame_def)
(blast intro: corresponds_xcp)
}
ultimately
show ?thesis by (rule that)
next
case Invoke_special
with phi_pc eff
have
"\<forall>D\<in>set (match_any G pc et).
the (?m D) < length ins \<and> (([Init (Class D)], LT),z) \<in> phi C sig!the (?m D)"
by (clarsimp simp add: xcpt_eff_def) (fastsimp elim: imageE2)
moreover
from some_handler
obtain D where
"D \<in> set (match_any G pc et)" and
D: "G \<turnstile> cname_of hp xcp \<preceq>C D" and
"?m D = Some handler"
by (blast dest: in_match_any)
ultimately
have
pc': "handler < length ins" and
phi': "(([Init (Class D)], LT), z) \<in> phi C sig ! handler"
by auto
from xp wt correct
obtain addr T where
xcp: "xcp = Addr addr" "hp addr = Some T" "is_init hp ihp xcp"
by (blast dest: exec_instr_xcpt_hp)
note phi'
moreover
{ from xcp D
have "approx_val G hp ihp xcp (OK (Init (Class D)))"
by (auto simp add: iconf_def conf_def obj_ty_def approx_val_def dest!: preallocatedD)
with wf pc' len loc cor cin
have "correct_frame G hp ihp ([Init (Class D)],LT) maxl ins ?f'"
by (simp add: consistent_init_xcp correct_frame_def)
(blast intro: corresponds_xcp)
}
ultimately
show ?thesis by (rule that)
next
case Throw
with phi_pc eff
have
"\<forall>D\<in>set (match_any G pc et).
the (?m D) < length ins \<and> (([Init (Class D)], LT),z) \<in> phi C sig!the (?m D)"
by (clarsimp simp add: xcpt_eff_def) (fastsimp elim: imageE2)
moreover
from some_handler
obtain D where
"D \<in> set (match_any G pc et)" and
D: "G \<turnstile> cname_of hp xcp \<preceq>C D" and
"?m D = Some handler"
by (blast dest: in_match_any)
ultimately
have
pc': "handler < length ins" and
phi': "(([Init (Class D)], LT), z) \<in> phi C sig ! handler"
by auto
from xp wt correct
obtain addr T where
xcp: "xcp = Addr addr" "hp addr = Some T" "is_init hp ihp xcp"
by (blast dest: exec_instr_xcpt_hp)
note phi'
moreover
{ from xcp D
have "approx_val G hp ihp xcp (OK (Init (Class D)))"
by (auto simp add: iconf_def conf_def obj_ty_def approx_val_def dest!: preallocatedD)
with wf pc' len loc cor cin
have "correct_frame G hp ihp ([Init (Class D)],LT) maxl ins ?f'"
by (simp add: consistent_init_xcp correct_frame_def)
(blast intro: corresponds_xcp)
}
ultimately
show ?thesis by (rule that)
qed (insert xp', auto) -- "the other instructions do not generate exceptions"
from state' meth hp_ok class frames phi_pc' frame' h_ini prehp
have ?thesis by simp (rule correct_stateI)
}
ultimately
show ?thesis by (cases "?match") blast+
qed
section {* Single Instructions *}
text {*
In this section we look at each single (welltyped) instruction, and
prove that the state after execution of the instruction still conforms.
Since we have already handled exceptions above, we can now assume, that
on exception occurs for this (single step) execution.
*}
lemmas [iff] = not_Err_eq
lemma Load_correct:
"\<lbrakk> wf_prog wt G;
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
ins!pc = Load idx;
wt_instr (ins!pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et pc;
Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs);
G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd> \<rbrakk>
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
apply (elim correctE, assumption)
apply (clarsimp simp add: defs1 map_eq_Cons)
apply (drule bspec, assumption)
apply clarsimp
apply (rule exI)+
apply (rule conjI)
apply (erule subsetD)
apply (erule imageE2)
apply simp
apply (rule conjI, rule refl)+
apply (rule refl)
apply clarsimp
apply (clarsimp simp add: approx_loc_def list_all2_conv_all_nth)
apply (erule allE, erule impE, assumption)
apply simp
apply (rule conjI)
apply (erule consistent_init_loc_nth)
apply simp
apply simp
apply clarsimp
apply (frule corresponds_loc_nth)
apply simp
apply assumption
apply (clarsimp simp add: corresponds_def corr_stk_def corr_loc_cons)
done
lemma Store_correct:
"\<lbrakk> wf_prog wt G;
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
ins!pc = Store idx;
wt_instr (ins!pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et pc;
Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs);
G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd> \<rbrakk>
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
apply (elim correctE, assumption)
apply (clarsimp simp add: defs1 map_eq_Cons)
apply (drule bspec, assumption)
apply clarsimp
apply (rule exI)+
apply (rule conjI)
apply (erule subsetD)
apply (erule imageE2)
apply simp
apply (rule conjI, rule refl)+
apply (rule refl)
apply clarsimp
apply (blast intro: approx_loc_imp_approx_loc_subst
consistent_init_store
corresponds_var_upd)
done
lemma LitPush_correct:
"\<lbrakk> wf_prog wt G;
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
ins!pc = LitPush v;
wt_instr (ins!pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et pc;
Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs);
G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd> \<rbrakk>
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
apply (elim correctE, assumption)
apply (clarsimp simp add: defs1 approx_val_def iconf_def init_le_Init
map_eq_Cons)
apply (drule bspec, assumption)
apply clarsimp
apply (rule exI)+
apply (rule conjI)
apply (erule subsetD)
apply (erule imageE2)
apply simp
apply (rule conjI, rule refl)+
apply (rule refl)
apply clarsimp
apply (simp add: approx_val_def iconf_def)
apply (rule conjI)
apply (fastsimp intro: conf_litval)
apply (rule conjI)
apply (clarsimp simp add: is_init_def split: val.split)
apply (rule conjI)
apply (erule consistent_init_Init_stk)
apply (rule impI, erule impE, assumption, elim conjE exE)
apply (simp add: corresponds_stk_cons)
done
lemma Cast_conf2:
"\<lbrakk> wf_prog ok G; G,h\<turnstile>v::\<preceq>RefT rt; cast_ok G C h v;
G\<turnstile>Class C\<preceq>T; is_class G C\<rbrakk>
\<Longrightarrow> G,h\<turnstile>v::\<preceq>T"
apply (unfold cast_ok_def)
apply (frule widen_Class)
apply (elim exE disjE)
apply (simp add: null)
apply (clarsimp simp add: conf_def obj_ty_def)
apply (cases v)
apply (auto intro: rtrancl_trans)
done
lemmas defs2 = defs1 raise_system_xcpt_def
lemma Checkcast_correct:
"\<lbrakk> wt_jvm_prog G phi;
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
ins!pc = Checkcast D;
wt_instr (ins!pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et pc;
Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs);
G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd>;
fst (exec_instr (ins!pc) G hp ihp stk loc C sig pc r frs) = None \<rbrakk>
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
apply (elim correctE, assumption)
apply (clarsimp simp add: defs2 map_eq_Cons approx_val_def wt_jvm_prog_def
split: split_if_asm)
apply (drule bspec, assumption)
apply clarsimp
apply (rule exI)+
apply (rule conjI)
apply (erule subsetD)
apply (erule imageE2)
apply simp
apply (rule conjI, rule refl)+
apply (rule refl)
apply clarsimp
apply (rule conjI)
apply (clarsimp simp add: approx_val_def iconf_def init_le_Init)
apply (blast intro: Cast_conf2)
apply (rule conjI)
apply (drule consistent_init_pop)
apply (erule consistent_init_Init_stk)
apply (clarsimp simp add: init_le_Init corresponds_stk_cons)
done
lemma Getfield_correct:
"\<lbrakk> wt_jvm_prog G phi;
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
ins!pc = Getfield F D;
wt_instr (ins!pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et pc;
Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs);
G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd>;
fst (exec_instr (ins!pc) G hp ihp stk loc C sig pc r frs) = None \<rbrakk>
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
apply (elim correctE, assumption)
apply (clarsimp simp add: defs2 map_eq_Cons wt_jvm_prog_def approx_val_def
iconf_def init_le_Init2)
apply (drule bspec, assumption)
apply (clarsimp simp add: defs2 map_eq_Cons wt_jvm_prog_def approx_val_def
iconf_def init_le_Init2
split: option.split split_if_asm)
apply (frule non_np_objD, rule conf_widen, assumption+)
apply clarsimp
apply (rule exI)+
apply (rule conjI)
apply (erule subsetD)
apply (erule imageE2)
apply simp
apply (rule conjI, rule refl)+
apply (rule refl)
apply (clarsimp simp add: defs2 approx_val_def)
apply (rule conjI)
apply (clarsimp simp add: iconf_def init_le_Init)
apply (rule conjI)
apply (drule widen_cfs_fields, assumption+)
apply (simp add: hconf_def oconf_def lconf_def)
apply (erule allE, erule allE, erule impE, assumption)
apply (simp (no_asm_use))
apply (erule allE, erule allE, erule impE, assumption)
apply clarsimp
apply (clarsimp simp: is_init_def split: val.split)
apply (simp add: h_init_def o_init_def l_init_def)
apply (erule allE, erule allE, erule impE, assumption)
apply (drule hconfD, assumption)
apply (drule widen_cfs_fields, assumption+)
apply (drule oconf_objD, assumption)
apply clarsimp
apply (erule allE, erule impE) back apply blast
apply (clarsimp simp add: is_init_def)
apply (clarsimp simp add: init_le_Init corresponds_stk_cons)
apply (blast intro: consistent_init_Init_stk
consistent_init_pop)
done
lemma Putfield_correct:
"\<lbrakk> wf_prog wt G;
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
ins!pc = Putfield F D;
wt_instr (ins!pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et pc;
Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs) ;
G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd>;
fst (exec_instr (ins!pc) G hp ihp stk loc C sig pc r frs) = None \<rbrakk>
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
proof -
assume wf: "wf_prog wt G"
assume meth: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
assume ins: "ins!pc = Putfield F D"
assume wt: "wt_instr (ins!pc) G C rT (phi C sig) maxs
(fst sig = init) (length ins) et pc"
assume exec: "Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)"
assume conf: "G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd>"
assume no_x: "fst (exec_instr (ins!pc) G hp ihp stk loc C sig pc r frs) = None"
from ins conf meth
obtain ST LT z where
heap_ok: "G\<turnstile>h hp\<surd>" and
pre_alloc: "preallocated hp ihp" and
init_ok: "h_init G hp ihp" and
phi_pc: "((ST,LT),z) \<in> phi C sig!pc" and
is_class_C: "is_class G C" and
frame: "correct_frame G hp ihp (ST,LT) maxl ins (stk,loc,C,sig,pc,r)" and
frames: "correct_frames G hp ihp phi rT sig z r frs"
by (fastsimp elim: correct_stateE)
from phi_pc ins wt
obtain vT oT vT' tST ST' LT' where
ST: "ST = (Init vT) # (Init oT) # tST" and
suc_pc: "Suc pc < length ins" and
phi_suc: "((tST, LT),z) \<in> phi C sig ! Suc pc" and
class_D: "is_class G D" and
field: "field (G, D) F = Some (D, vT')" and
v_less: "G \<turnstile> Init vT \<preceq>i Init vT'" and
o_less: "G \<turnstile> Init oT \<preceq>i Init (Class D)"
apply (unfold wt_instr_def eff_defs)
apply clarsimp
apply (drule bspec, assumption)
apply clarsimp
apply (drule subsetD)
apply (rule imageI, assumption)
apply (clarsimp simp add: init_le_Init2)
apply blast
done
from ST frame
obtain vt ot stk' where
stk : "stk = vt#ot#stk'" and
app_v: "approx_val G hp ihp vt (OK (Init vT))" and
app_o: "approx_val G hp ihp ot (OK (Init oT))" and
app_s: "approx_stk G hp ihp stk' tST" and
app_l: "approx_loc G hp ihp loc LT" and
consi: "consistent_init (vt#ot#stk') loc ((Init vT)#(Init oT)#tST,LT) ihp" and
corr: "fst sig = init \<longrightarrow>
corresponds (vt#ot#stk') loc (Init vT#Init oT#tST,LT) ihp (fst r) (PartInit C) \<and>
(\<exists>l. fst r = Addr l \<and> hp l \<noteq> None \<and>
(ihp l = PartInit C \<or> (\<exists>C'. ihp l = Init (Class C'))))" and
len_l: "length loc = Suc (length (snd sig) + maxl)"
by - (erule correct_frameE, simp, blast)
from app_v app_o obtain
"G,hp \<turnstile> vt ::\<preceq> vT" and
conf_o: "G,hp \<turnstile> ot ::\<preceq> oT" and
is_init_vo: "is_init hp ihp vt" "is_init hp ihp ot"
by (simp add: approx_val_def iconf_def)
with wf v_less have conf_v: "G,hp \<turnstile> vt ::\<preceq> vT'"
by (auto intro: conf_widen)
{ assume "ot = Null"
with exec ins meth stk obtain x where
"fst (exec_instr (ins!pc) G hp ihp stk loc C sig pc r frs) = Some x"
by (simp add: split_beta raise_system_xcpt_def)
with no_x have ?thesis by simp
}
moreover
{ assume "ot \<noteq> Null"
with o_less conf_o
obtain x C' fs oT' where
ot_addr: "ot = Addr x" and
hp_Some: "hp x = Some (C',fs)" and
"G \<turnstile> (Class C') \<preceq> oT"
by (fastsimp dest: widen_RefT2 conf_RefTD)
with o_less
have C': "G \<turnstile> C' \<preceq>C D"
by (auto dest: widen_trans)
with wf field
have fields: "map_of (fields (G, C')) (F, D) = Some vT'"
by - (rule widen_cfs_fields)
let ?hp' = "hp(x\<mapsto>(C', fs((F, D)\<mapsto>vt)))"
and ?f' = "(stk', loc, C, sig, Suc pc, r)"
from exec ins meth stk ot_addr hp_Some
have state': "state' = Norm (?hp', ihp, ?f'#frs)"
by (simp add: raise_system_xcpt_def)
from hp_Some have hext: "hp \<le>| ?hp'" by (rule sup_heap_update_value)
with fields hp_Some conf_v heap_ok
have hp'_ok: "G \<turnstile>h ?hp' \<surd>" by (blast intro: hconf_imp_hconf_field_update )
from app_v have "is_init hp ihp vt" by (simp add: approx_val_def iconf_def)
with init_ok hp_Some have hp'_init: "h_init G ?hp' ihp"
by (rule h_init_field_update)
from fields hp_Some heap_ok pre_alloc have pre_alloc': "preallocated ?hp' ihp"
by (rule preallocated_field_update)
from corr have corr':
"fst sig = init \<longrightarrow>
corresponds stk' loc (tST, LT) ihp (fst r) (PartInit C) \<and>
(\<exists>l. fst r = Addr l \<and> ?hp' l \<noteq> None \<and>
(ihp l = PartInit C \<or> (\<exists>C'. ihp l = Init (Class C'))))"
by (clarsimp simp add: corresponds_stk_cons simp del: fun_upd_apply) simp
from consi stk have "consistent_init stk' loc (tST, LT) ihp"
by (blast intro: consistent_init_pop)
with wf app_l app_s len_l suc_pc hext corr'
have f'_correct:
"correct_frame G ?hp' ihp (tST, LT) maxl ins (stk',loc,C,sig,Suc pc,r)"
by (simp add: correct_frame_def)
(blast intro: approx_stk_imp_approx_stk_sup_heap
approx_loc_imp_approx_loc_sup_heap)
from wf frames hp_Some fields conf_v
have "correct_frames G ?hp' ihp phi rT sig z r frs"
by - (rule correct_frames_imp_correct_frames_field_update)
with state' ins meth is_class_C phi_suc hp'_ok hp'_init f'_correct pre_alloc'
have ?thesis by simp (rule correct_stateI)
}
ultimately
show ?thesis by blast
qed
lemma New_correct:
"\<lbrakk> wf_prog wt G;
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
ins!pc = New X;
wt_instr (ins!pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et pc;
Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs) ;
G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd>;
fst (exec_instr (ins!pc) G hp ihp stk loc C sig pc r frs) = None \<rbrakk>
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
proof -
assume wf: "wf_prog wt G"
assume meth: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
assume ins: "ins!pc = New X"
assume wt: "wt_instr (ins!pc) G C rT (phi C sig) maxs
(fst sig = init) (length ins) et pc"
assume exec: "Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)"
assume conf: "G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd>"
assume no_x: "fst (exec_instr (ins!pc) G hp ihp stk loc C sig pc r frs) = None"
from conf meth
obtain ST LT z where
heap_ok: "G\<turnstile>h hp\<surd>" and
init_ok: "h_init G hp ihp" and
phi_pc: "((ST,LT),z) \<in> phi C sig!pc" and
prealloc: "preallocated hp ihp" and
is_class_C: "is_class G C" and
frame: "correct_frame G hp ihp (ST,LT) maxl ins (stk,loc,C,sig,pc,r)" and
frames: "correct_frames G hp ihp phi rT sig z r frs"
..
from phi_pc ins wt
obtain
is_class_X: "is_class G X" and
maxs: "length ST < maxs" and
suc_pc: "Suc pc < length ins" and
phi_suc: "((UnInit X pc#ST, replace (OK (UnInit X pc)) Err LT), z) \<in> phi C sig ! Suc pc" (is "((?ST',?LT'),_) \<in> _") and
new_type: "UnInit X pc \<notin> set ST"
apply (unfold wt_instr_def eff_def eff_bool_def norm_eff_def)
apply clarsimp
apply (drule bspec, assumption)
apply clarsimp
apply (drule subsetD, rule imageI, assumption)
apply clarsimp
done
obtain oref xp' where
new_Addr: "new_Addr hp = (oref,xp')"
by (cases "new_Addr hp")
with ins no_x
obtain hp: "hp oref = None" and "xp' = None"
by (auto dest: new_AddrD simp add: raise_system_xcpt_def)
with exec ins meth new_Addr
have state':
"state' = Norm (hp(oref\<mapsto>blank G X), ihp(oref := UnInit X pc),
(Addr oref # stk, loc, C, sig, Suc pc, r) # frs)"
(is "state' = Norm (?hp', ?ihp', ?f # frs)")
by simp
moreover
from wf hp heap_ok is_class_X
have hp': "G \<turnstile>h ?hp' \<surd>"
by - (rule hconf_imp_hconf_newref,
auto simp add: oconf_def blank_def dest: fields_is_type)
moreover
from hp heap_ok init_ok
have "h_init G ?hp' ?ihp'" by (rule h_init_newref)
moreover
from hp have sup: "hp \<le>| ?hp'" by (rule sup_heap_newref)
from frame obtain
cons: "consistent_init stk loc (ST, LT) ihp" and
a_loc: "approx_loc G hp ihp loc LT" and
a_stk: "approx_stk G hp ihp stk ST" and
corr: "fst sig = init \<longrightarrow>
corresponds stk loc (ST, LT) ihp (fst r) (PartInit C) \<and>
(\<exists>l. fst r = Addr l \<and> hp l \<noteq> None \<and>
(ihp l = PartInit C \<or> (\<exists>C'. ihp l = Init (Class C'))))"
..
from a_loc
have a_loc': "approx_loc G hp ihp loc ?LT'" by (rule approx_loc_replace_Err)
from corr a_loc a_stk new_type hp
have corr':
"fst sig = init \<longrightarrow>
corresponds (Addr oref#stk) loc (?ST', ?LT') ?ihp' (fst r) (PartInit C) \<and>
(\<exists>l. fst r = Addr l \<and> ?hp' l \<noteq> None \<and>
(?ihp' l = PartInit C \<or> (\<exists>C'. ?ihp' l = Init (Class C'))))"
apply (clarsimp simp add: corresponds_stk_cons simp del: fun_upd_apply)
apply (drule corresponds_new_val2, assumption+)
apply (auto intro: corresponds_replace_Err)
done
from new_type have "OK (UnInit X pc) \<notin> set (map OK ST) \<union> set ?LT'"
by (auto simp add: replace_removes_elem)
with cons a_stk a_loc' hp
have "consistent_init (Addr oref # stk) loc (?ST',?LT') ?ihp'"
by (blast intro: consistent_init_newref consistent_init_replace_Err)
with hp frame suc_pc wf corr' a_loc'
have "correct_frame G ?hp' ?ihp' (?ST', ?LT') maxl ins ?f"
apply (unfold correct_frame_def)
apply (clarsimp simp add: map_eq_Cons conf_def blank_def
corresponds_stk_cons)
apply (insert sup, unfold blank_def)
apply (blast intro: approx_stk_newref
approx_stk_imp_approx_stk_sup_heap
approx_loc_imp_approx_loc_sup_heap
approx_loc_newref
approx_val_newref
sup)
done
moreover
from hp frames wf heap_ok is_class_X
have "correct_frames G ?hp' ?ihp' phi rT sig z r frs"
by (unfold blank_def)
(rule correct_frames_imp_correct_frames_newref,
auto simp add: oconf_def dest: fields_is_type)
moreover
from hp prealloc have "preallocated ?hp' ?ihp'" by (rule preallocated_newref)
ultimately
show ?thesis by simp (rule correct_stateI)
qed
text {* \bf Method Invocation *}
lemmas [simp del] = split_paired_Ex
lemma zip_map [rule_format]:
"\<forall>a. length a = length b \<longrightarrow>
zip (map f a) (map g b) = map (\<lambda>(x,y). (f x, g y)) (zip a b)"
apply (induct b)
apply simp
apply clarsimp
apply (case_tac aa)
apply simp+
done
lemma Invoke_correct:
"\<lbrakk> wt_jvm_prog G phi;
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
ins ! pc = Invoke C' mn pTs;
wt_instr (ins!pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et pc;
Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs) ;
G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd>;
fst (exec_instr (ins!pc) G hp ihp stk loc C sig pc r frs) = None \<rbrakk>
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
proof -
assume wtprog: "wt_jvm_prog G phi"
assume method: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
assume ins: "ins ! pc = Invoke C' mn pTs"
assume wti: "wt_instr (ins!pc) G C rT (phi C sig) maxs
(fst sig = init) (length ins) et pc"
assume state': "Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)"
assume approx: "G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd>"
assume no_xcp: "fst (exec_instr (ins!pc) G hp ihp stk loc C sig pc r frs) = None"
from wtprog obtain wfmb where
wfprog: "wf_prog wfmb G" by (simp add: wt_jvm_prog_def)
from approx method obtain s z where
heap_ok: "G\<turnstile>h hp\<surd>" and
init_ok: "h_init G hp ihp" and
phi_pc: "(s,z) \<in> phi C sig!pc" and
prealloc:"preallocated hp ihp" and
is_class_C: "is_class G C" and
frame: "correct_frame G hp ihp s maxl ins (stk, loc, C, sig, pc, r)" and
frames: "correct_frames G hp ihp phi rT sig z r frs"
..
from ins wti phi_pc obtain apTs X ST LT D' rT body where
is_class: "is_class G C'" and
s: "s = (rev apTs @ X # ST, LT)" and
l: "length apTs = length pTs" and
w: "\<forall>(x,y)\<in>set (zip apTs pTs). G \<turnstile> x \<preceq>i (Init y)" and
mC': "method (G, C') (mn, pTs) = Some (D', rT, body)" and
pc: "Suc pc < length ins" and
eff: "norm_eff (Invoke C' mn pTs) G pc (Suc pc) (phi C sig!pc) \<subseteq> phi C sig!Suc pc" and
X: "G \<turnstile> X \<preceq>i Init (Class C')" and
ni: "mn \<noteq> init"
apply (clarsimp simp add: wt_instr_def eff_def)
apply (drule bspec, assumption)
apply clarsimp
apply blast
done
from s ins frame obtain
a_stk: "approx_stk G hp ihp stk (rev apTs @ X # ST)" and
a_loc: "approx_loc G hp ihp loc LT" and
init: "consistent_init stk loc s ihp" and
suc_l: "length loc = Suc (length (snd sig) + maxl)"
by (simp add: correct_frame_def)
from a_stk obtain opTs stk' oX where
opTs: "approx_stk G hp ihp opTs (rev apTs)" and
oX: "approx_val G hp ihp oX (OK X)" and
a_stk': "approx_stk G hp ihp stk' ST" and
stk': "stk = opTs @ oX # stk'" and
l_o: "length opTs = length apTs"
"length stk' = length ST"
by (auto dest!: approx_stk_append_lemma)
from oX have X_oX: "G,hp,ihp \<turnstile> oX ::\<preceq>i X" by (simp add: approx_val_def)
with wfprog X have oX_conf: "G,hp \<turnstile> oX ::\<preceq> (Class C')"
by (auto simp add: approx_val_def iconf_def init_le_Init2 dest: conf_widen)
from stk' l_o l have oX_pos: "stk ! length pTs = oX" by (simp add: nth_append)
with state' method ins no_xcp oX_conf obtain ref where oX_Addr: "oX = Addr ref"
by (auto simp add: raise_system_xcpt_def dest: conf_RefTD)
with oX_conf obtain D fs where
hp_Some: "hp ref = Some (D,fs)" and
D_le_C': "G \<turnstile> D \<preceq>C C'"
by (fastsimp dest: conf_RefTD)
from D_le_C' wfprog mC'
obtain D'' rT' mxl' mxs' ins' et' where
mD: "method (G, D) (mn, pTs) = Some (D'', rT', mxs', mxl', ins', et')"
"G \<turnstile> rT' \<preceq> rT"
by (auto dest!: subtype_widen_methd) blast
let ?loc' = "oX # rev opTs @ replicate mxl' arbitrary"
let ?f = "([], ?loc', D'', (mn, pTs), 0, arbitrary)"
let ?f' = "(stk, loc, C, sig, pc, r)"
from oX_Addr oX_pos hp_Some state' method ins stk' l_o l mD
have state'_val: "state' = Norm (hp, ihp, ?f# ?f' # frs)"
by (simp add: raise_system_xcpt_def)
from is_class D_le_C' have is_class_D: "is_class G D"
by (auto dest: subcls_is_class2)
with mD wfprog obtain mD'':
"method (G, D'') (mn, pTs) = Some (D'', rT', mxs', mxl', ins', et')"
"is_class G D''"
by (auto dest: method_in_md)
from wtprog mD''
have start: "wt_start G D'' mn pTs mxl' (phi D'' (mn, pTs)) \<and> ins' \<noteq> []"
by (auto dest: wt_jvm_prog_impl_wt_start)
let ?T = "OK (Init (Class D''))"
let ?LT0 = "?T # map OK (map Init pTs) @ replicate mxl' Err"
from ni start have sup_loc:
"(([],?LT0),D''=Object) \<in> phi D'' (mn,pTs) ! 0"
by (simp add: wt_start_def)
have c_f: "correct_frame G hp ihp ([], ?LT0) mxl' ins' ?f"
proof -
have r:
"approx_loc G hp ihp (replicate mxl' arbitrary) (replicate mxl' Err)"
by (simp add: approx_loc_def approx_val_Err list_all2_def
set_replicate_conv_if)
from wfprog mD is_class_D have "G \<turnstile> Class D \<preceq> Class D''"
by (auto dest: method_wf_mdecl)
with hp_Some oX_Addr oX X have a: "approx_val G hp ihp oX ?T"
by (auto simp add: is_init_def init_le_Init2
approx_val_def iconf_def conf_def)
from w l
have "\<forall>(x,y)\<in>set (zip (map (\<lambda>x. x) apTs) (map Init pTs)). G \<turnstile> x \<preceq>i y"
by (simp only: zip_map) auto
hence "\<forall>(x,y)\<in>set (zip apTs (map Init pTs)). G \<turnstile> x \<preceq>i y" by simp
with l
have "\<forall>(x,y)\<in>set (zip (rev apTs) (rev (map Init pTs))). G \<turnstile> x \<preceq>i y"
by (auto simp add: zip_rev)
with wfprog l l_o opTs
have "approx_loc G hp ihp opTs (map OK (rev (map Init pTs)))"
by (auto intro: assConv_approx_stk_imp_approx_loc)
hence "approx_stk G hp ihp opTs (rev (map Init pTs))"
by (simp add: approx_stk_def)
hence "approx_stk G hp ihp (rev opTs) (map Init pTs)"
by (simp add: approx_stk_rev)
hence "approx_loc G hp ihp (rev opTs) (map OK (map Init pTs))"
by (simp add: approx_stk_def)
with r a l_o l
have loc: "approx_loc G hp ihp ?loc' ?LT0"
by (auto simp add: approx_loc_append approx_stk_def)
from l l_o have "length pTs = length opTs" by auto
hence "consistent_init [] ?loc' ([],?LT0) ihp"
by (blast intro: consistent_init_start)
with start loc l_o l ni show ?thesis by (simp add: correct_frame_def)
qed
from X X_oX oX_Addr hp_Some obtain X' where X': "X = Init (Class X')"
by (auto simp add: init_le_Init2 iconf_def conf_def dest!: widen_Class)
with X mC' wf obtain mD'' rT'' b'' where
"method (G, X') (mn, pTs) = Some (mD'', rT'', b'')"
"G \<turnstile> rT'' \<preceq> rT"
by simp (drule subtype_widen_methd, assumption+, blast)
with X' state'_val heap_ok mD'' ins method phi_pc s l
frames c_f frame is_class_C ni init_ok prealloc sup_loc
show "G,phi \<turnstile>JVM state'\<surd>"
apply simp
apply (rule correct_stateI, assumption+)
apply clarsimp
apply (intro exI conjI impI)
apply assumption+
apply (rule refl)
apply assumption+
done
qed
lemma Invoke_special_correct:
"\<lbrakk> wt_jvm_prog G phi;
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
ins ! pc = Invoke_special C' mn pTs;
wt_instr (ins!pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et pc;
Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs) ;
G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd>;
fst (exec_instr (ins!pc) G hp ihp stk loc C sig pc r frs) = None \<rbrakk>
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
proof -
assume wtprog: "wt_jvm_prog G phi"
assume method: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
assume ins: "ins ! pc = Invoke_special C' mn pTs"
assume wti: "wt_instr (ins!pc) G C rT (phi C sig) maxs
(fst sig = init) (length ins) et pc"
assume state': "Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)"
assume approx: "G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd>"
assume no_x: "fst (exec_instr (ins!pc) G hp ihp stk loc C sig pc r frs) = None"
from wtprog obtain wfmb where wfprog: "wf_prog wfmb G"
by (simp add: wt_jvm_prog_def)
from approx method obtain s z where
heap_ok: "G\<turnstile>h hp\<surd>" and
init_ok: "h_init G hp ihp" and
prealloc:"preallocated hp ihp" and
phi_pc: "(s,z) \<in> phi C sig!pc" and
is_class_C: "is_class G C" and
frame: "correct_frame G hp ihp s maxl ins (stk, loc, C, sig, pc, r)" and
frames: "correct_frames G hp ihp phi rT sig z r frs"
..
from ins wti phi_pc obtain apTs X ST LT rT' maxs' mxl' ins' et' where
s: "s = (rev apTs @ X # ST, LT)" and
l: "length apTs = length pTs" and
is_class: "is_class G C'" and
w: "\<forall>(x,y)\<in>set (zip apTs pTs). G \<turnstile> x \<preceq>i (Init y)" and
mC': "method (G, C') (mn, pTs) = Some (C', rT', maxs', mxl', ins', et')" and
pc: "Suc pc < length ins" and
eff: "norm_eff (Invoke_special C' mn pTs) G pc (Suc pc) (phi C sig!pc) \<subseteq>
phi C sig!Suc pc" and
X: "(\<exists>pc. X = UnInit C' pc) \<or> (X = PartInit C \<and> G \<turnstile> C \<prec>C1 C' \<and> ¬z)" and
is_init: "mn = init"
apply (clarsimp simp add: wt_instr_def split_paired_Ex eff_def)
apply (drule bspec, assumption)
apply clarsimp
apply blast
done
from s ins frame obtain
a_stk: "approx_stk G hp ihp stk (rev apTs @ X # ST)" and
a_loc: "approx_loc G hp ihp loc LT" and
init: "consistent_init stk loc (rev apTs @ X # ST, LT) ihp" and
corr: "fst sig = init \<longrightarrow> corresponds stk loc s ihp (fst r) (PartInit C) \<and>
(\<exists>l. fst r = Addr l \<and> hp l \<noteq> None \<and>
(ihp l = PartInit C \<or> (\<exists>C'. ihp l = Init (Class C'))))" and
suc_l: "length loc = Suc (length (snd sig) + maxl)"
by (simp add: correct_frame_def)
from a_stk obtain opTs stk' oX where
opTs: "approx_stk G hp ihp opTs (rev apTs)" and
oX: "approx_val G hp ihp oX (OK X)" and
a_stk': "approx_stk G hp ihp stk' ST" and
stk': "stk = opTs @ oX # stk'" and
l_o: "length opTs = length apTs"
"length stk' = length ST"
by (fastsimp dest!: approx_stk_append_lemma)
from stk' l_o l have oX_pos: "stk ! length pTs = oX" by (simp add: nth_append)
from state' method ins no_x oX_pos have "oX \<noteq> Null"
by (simp add: raise_system_xcpt_def split: split_if_asm)
moreover
from wfprog X oX have oX_conf: "G,hp \<turnstile> oX ::\<preceq> (Class C')"
by (auto simp add: approx_val_def iconf_def)
(blast dest: conf_widen)
ultimately
obtain ref obj D fs where
oX_Addr: "oX = Addr ref" and
hp_Some: "hp ref = Some (D,fs)" and
D_le_C': "G \<turnstile> D \<preceq>C C'"
by (fastsimp dest: conf_RefTD)
let ?new = "new_Addr hp"
let ?ref' = "fst ?new"
let ?xp' = "snd ?new"
let ?hp' = "hp(?ref'\<mapsto>blank G D)"
let ?loc' = "Addr ?ref' # rev opTs @ replicate mxl' arbitrary"
let ?ihp' = "if C' = Object then
ihp(?ref':= Init (Class D))
else
ihp(?ref' := PartInit C')"
let ?r' = "if C' = Object then
(Addr ?ref', Addr ?ref')
else
(Addr ?ref', Null)"
let ?f = "([], ?loc', C', (mn, pTs), 0, ?r')"
let ?f' = "(stk, loc, C, sig, pc, r)"
from state' method ins no_x have norm: "?xp' = None"
by (simp add: split_beta split: split_if_asm)
with oX_Addr oX_pos hp_Some state' method ins stk' l_o l mC'
have state'_val: "state' = Norm (?hp', ?ihp', ?f# ?f' # frs)"
by (simp add: raise_system_xcpt_def split_beta)
obtain ref' xp' where
new_Addr: "new_Addr hp = (ref',xp')"
by (cases "new_Addr hp") auto
with norm have new_ref': "hp ref' = None" by (auto dest: new_AddrD)
from is_class D_le_C' have is_class_D: "is_class G D"
by (auto dest: subcls_is_class2)
from wtprog is_class mC'
have start: "wt_start G C' mn pTs mxl' (phi C' (mn, pTs)) \<and> ins' \<noteq> []"
by (auto dest: wt_jvm_prog_impl_wt_start)
let ?T = "OK (if C' \<noteq> Object then PartInit C' else Init (Class C'))"
let ?LT0 = "?T # map OK (map Init pTs) @ replicate mxl' Err"
from start is_init
have LT0: "(([], ?LT0),C'=Object) \<in> phi C' (mn, pTs) ! 0"
by (clarsimp simp add: wt_start_def)
have c_f: "correct_frame G ?hp' ?ihp' ([], ?LT0) mxl' ins' ?f"
proof -
have r:
"approx_loc G ?hp' ?ihp' (replicate mxl' arbitrary) (replicate mxl' Err)"
by (simp add: approx_loc_def approx_val_Err list_all2_def
set_replicate_conv_if)
from new_Addr obtain fs where "?hp' ref' = Some (D,fs)" by (simp add: blank_def)
hence "G,?hp' \<turnstile> Addr ref' ::\<preceq> Class C'"
by (auto simp add: new_Addr D_le_C' intro: conf_obj_AddrI)
hence a: "approx_val G ?hp' ?ihp' (Addr ?ref') ?T"
by (auto simp add: approx_val_def iconf_def new_Addr
blank_def is_init_def)
from w l
have "\<forall>(x,y)\<in>set (zip (map (\<lambda>x. x) apTs) (map Init pTs)). G \<turnstile> x \<preceq>i y"
by (simp only: zip_map) auto
hence "\<forall>(x,y)\<in>set (zip apTs (map Init pTs)). G \<turnstile> x \<preceq>i y" by simp
with l
have "\<forall>(x,y)\<in>set (zip (rev apTs) (rev (map Init pTs))). G \<turnstile> x \<preceq>i y"
by (auto simp add: zip_rev)
with wfprog l l_o opTs
have "approx_loc G hp ihp opTs (map OK (rev (map Init pTs)))"
by (auto intro: assConv_approx_stk_imp_approx_loc)
hence "approx_stk G hp ihp opTs (rev (map Init pTs))"
by (simp add: approx_stk_def)
hence "approx_stk G hp ihp (rev opTs) (map Init pTs)"
by (simp add: approx_stk_rev)
hence "approx_loc G hp ihp (rev opTs) (map OK (map Init pTs))"
by (simp add: approx_stk_def)
with new_Addr new_ref'
have "approx_loc G hp ?ihp' (rev opTs) (map OK (map Init pTs))"
by (auto dest: approx_loc_newref)
moreover
from new_Addr new_ref' have "hp \<le>| ?hp'" by simp
ultimately
have "approx_loc G ?hp' ?ihp' (rev opTs) (map OK (map Init pTs))"
by (rule approx_loc_imp_approx_loc_sup_heap)
with r a l_o l
have loc: "approx_loc G ?hp' ?ihp' ?loc' ?LT0"
by (auto simp add: approx_loc_append)
from new_Addr new_ref' l_o l have corr':
"corresponds [] ?loc' ([], ?LT) ?ihp' (Addr ref') (PartInit C')"
apply (simp add: corresponds_def corr_stk_def corr_loc_cons
split del: split_if)
apply (rule conjI)
apply (simp add: corr_val_def)
apply (rule corr_loc_start)
apply clarsimp
apply (erule disjE)
apply (erule imageE, erule imageE)
apply simp
apply force
apply (drule in_set_replicateD)
apply assumption
apply simp
apply blast
done
from l_o l
have "length (rev opTs @ replicate mxl' arbitrary) =
length (map OK (map Init pTs) @ replicate mxl' Err)" by simp
moreover
have "\<forall>x\<in>set (map OK (map Init pTs) @ replicate mxl' Err).
x = Err \<or> (\<exists>t. x = OK (Init t))"
by (auto dest: in_set_replicateD)
ultimately
have "consistent_init [] ?loc' ([], ?LT0) ?ihp'"
apply (unfold consistent_init_def)
apply (unfold corresponds_def)
apply (simp (no_asm) add: corr_stk_def corr_loc_empty corr_loc_cons
split del: split_if)
apply safe
apply (rule exI)
apply (rule conjI)
apply (simp (no_asm))
apply (rule corr_loc_start)
apply assumption+
apply blast
apply (rule exI)
apply (rule conjI)
defer
apply (blast intro: corr_loc_start)
apply (rule impI)
apply (simp add: new_Addr split del: split_if)
apply (rule conjI)
apply (rule refl)
apply (simp add: corr_val_def new_Addr split: split_if_asm)
done
with start loc l_o l corr' new_Addr new_ref'
show ?thesis by (simp add: correct_frame_def split: split_if_asm)
qed
from a_stk a_loc init suc_l pc new_Addr new_ref' s corr
have c_f': "correct_frame G ?hp' ?ihp' (rev apTs @ X # ST, LT) maxl ins ?f'"
apply (unfold correct_frame_def)
apply simp
apply (rule conjI)
apply (rule impI)
apply (rule conjI)
apply (drule approx_stk_newref, assumption)
apply (rule approx_stk_imp_approx_stk_sup_heap, assumption)
apply simp
apply (rule conjI)
apply (drule approx_loc_newref, assumption)
apply (rule approx_loc_imp_approx_loc_sup_heap, assumption)
apply simp
apply (rule conjI)
apply (rule consistent_init_new_val, assumption+)
apply (rule impI, erule impE, assumption, elim exE conjE)
apply (rule conjI)
apply (rule corresponds_new_val2, assumption+)
apply simp
apply (rule exI, rule conjI)
apply (rule impI)
apply assumption
apply simp
apply (rule impI)
apply (rule conjI)
apply (drule approx_stk_newref, assumption)
apply (rule approx_stk_imp_approx_stk_sup_heap, assumption)
apply simp
apply (rule conjI)
apply (drule approx_loc_newref, assumption)
apply (rule approx_loc_imp_approx_loc_sup_heap, assumption)
apply simp
apply (rule conjI)
apply (rule consistent_init_new_val, assumption+)
apply (rule impI, erule impE, assumption, elim exE conjE)
apply (rule conjI)
apply (rule corresponds_new_val2, assumption+)
apply simp
apply (rule exI, rule conjI)
apply (rule impI)
apply (rule conjI)
apply assumption
apply simp
apply simp
done
from new_Addr new_ref' heap_ok is_class_D wfprog
have hp'_ok: "G \<turnstile>h ?hp' \<surd>"
by (auto intro: hconf_imp_hconf_newref oconf_blank)
with new_Addr new_ref'
have ihp'_ok: "h_init G ?hp' ?ihp'"
by (auto intro!: h_init_newref)
from hp_Some new_ref' have neq_ref: "ref \<noteq> ref'" by auto
with new_Addr oX_Addr X oX hp_Some
have ctor_ok:
"constructor_ok G ?hp' ?ihp' (Addr ref) C' (C'=Object) ?r'"
apply (unfold constructor_ok_def)
apply (simp add: approx_val_def iconf_def)
apply (erule disjE)
apply (clarsimp simp add: blank_def)
apply (elim exE conjE)
apply (simp add: blank_def)
done
from new_Addr new_ref' frames
have c_frs: "correct_frames G ?hp' ?ihp' phi rT sig z r frs"
by (auto simp add: blank_def
intro: correct_frames_imp_correct_frames_newref)
from new_Addr new_ref' prealloc have prealloc': "preallocated ?hp' ?ihp'"
by (auto intro: preallocated_newref)
from state'_val heap_ok mC' ins method phi_pc s l ctor_ok c_f' c_frs
frames LT0 c_f is_class_C is_class new_Addr new_ref' hp'_ok ihp'_ok
prealloc'
show "G,phi \<turnstile>JVM state'\<surd>"
apply (unfold correct_state_def)
apply (simp split del: split_if)
apply (intro exI conjI impI)
apply assumption+
apply (rule refl)
apply assumption+
apply (simp add: oX_pos oX_Addr hp_Some neq_ref)
apply assumption+
done
qed
lemmas [simp del] = map_append
lemma Return_correct_not_init:
"\<lbrakk> fst sig \<noteq> init;
wt_jvm_prog G phi;
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
ins ! pc = Return;
wt_instr (ins!pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et pc;
Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs) ;
G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd> \<rbrakk>
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
proof -
assume wtjvm: "wt_jvm_prog G phi"
assume mthd: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
assume ins: "ins!pc = Return"
assume wt: "wt_instr (ins!pc) G C rT (phi C sig) maxs
(fst sig = init) (length ins) et pc"
assume state: "Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)"
assume approx:"G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd>"
from approx mthd
obtain s z where
heap_ok: "G \<turnstile>h hp\<surd>" and
init_ok: "h_init G hp ihp" and
prealloc:"preallocated hp ihp" and
classC: "is_class G C" and
some: "(s,z) \<in> phi C sig ! pc" and
frame: "correct_frame G hp ihp s maxl ins (stk, loc, C, sig, pc, r)" and
frames: "correct_frames G hp ihp phi rT sig z r frs"
..
obtain mn pTs where sig: "sig = (mn,pTs)" by (cases sig)
moreover assume "fst sig \<noteq> init"
ultimately have not_init: "mn \<noteq> init" by simp
from ins some sig wt
obtain T ST LT where
s: "s = (T # ST, LT)" and
T: "G \<turnstile> T \<preceq>i Init rT"
apply (clarsimp simp add: wt_instr_def eff_def eff_bool_def norm_eff_def)
apply (drule bspec, assumption)
apply clarsimp
apply blast
done
from frame s
obtain rval stk' loc where
stk: "stk = rval # stk'" and
val: "approx_val G hp ihp rval (OK T)" and
approx_stk: "approx_stk G hp ihp stk' ST" and
approx_val: "approx_loc G hp ihp loc LT" and
consistent: "consistent_init stk loc (T # ST, LT) ihp" and
len: "length loc = Suc (length (snd sig) + maxl)" and
pc: "pc < length ins"
by (simp add: correct_frame_def) blast
from stk mthd ins state
have "frs = [] \<Longrightarrow> ?thesis" by (simp add: correct_state_def)
moreover
{ fix f frs' assume frs: "frs = f#frs'"
obtain stk0 loc0 C0 sig0 pc0 r0 where
f: "f = (stk0, loc0, C0, sig0, pc0, r0)" by (cases f)
let ?r' = "(stk0 ! length pTs, snd r0)"
let ?stk' = "drop (Suc (length pTs)) stk0"
let ?f' = "(rval#?stk',loc0,C0,sig0,Suc pc0,r0)"
from stk mthd ins sig f frs not_init state
have state': "state' = Norm (hp, ihp, ?f' # frs')" by (simp add: split_beta)
from f frs frames sig
obtain ST0 LT0 T0 z0 rT0 maxs0 maxl0 ins0 et0 C' apTs D D' rT' body' where
class_C0: "is_class G C0" and
methd_C0: "method (G, C0) sig0 = Some (C0, rT0, maxs0, maxl0, ins0, et0)" and
ins0: "ins0 ! pc0 = Invoke C' mn pTs \<or>
ins0 ! pc0 = Invoke_special C' mn pTs" and
phi_pc0: "((rev apTs @ T0 # ST0, LT0), z0) \<in> phi C0 sig0 ! pc0" and
apTs: "length apTs = length pTs" and
methd_C': "method (G, C') sig = Some (D', rT', body')" "G \<turnstile> rT \<preceq> rT'" and
c_fr: "correct_frame G hp ihp (rev apTs @ T0 # ST0, LT0) maxl0 ins0
(stk0, loc0, C0, sig0, pc0, r0)" and
c_frs: "correct_frames G hp ihp phi rT0 sig0 z0 r0 frs'"
apply simp (* fixme: this script sucks *)
apply (elim conjE exE)
apply (rule that)
apply assumption+
apply simp
apply assumption+
apply simp
apply (rule conjI, rule refl)+
apply (rule refl)
apply assumption+
apply simp
apply assumption
done
from c_fr obtain
a_stk0: "approx_stk G hp ihp stk0 (rev apTs @ T0 # ST0)" and
a_loc0: "approx_loc G hp ihp loc0 LT0" and
cons0: "consistent_init stk0 loc0 (rev apTs @ T0 # ST0, LT0) ihp" and
corr0: "fst sig0 = init \<longrightarrow>
corresponds stk0 loc0 (rev apTs @ T0 # ST0, LT0) ihp (fst r0) (PartInit C0) \<and>
(\<exists>l. fst r0 = Addr l \<and> hp l \<noteq> None \<and>
(ihp l = PartInit C0 \<or> (\<exists>C'. ihp l = Init (Class C'))))" and
pc0: "pc0 < length ins0" and
lenloc0:"length loc0 = Suc (length (snd sig0) + maxl0)"
by (unfold correct_frame_def) simp
from pc0 wtjvm methd_C0 have wt0:
"wt_instr (ins0!pc0) G C0 rT0 (phi C0 sig0) maxs0
(fst sig0 = init) (length ins0) et0 pc0"
by - (rule wt_jvm_prog_impl_wt_instr)
from ins0 apTs phi_pc0 not_init sig methd_C' wt0
obtain
Suc_pc0: "Suc pc0 < length ins0" and
phi_Suc_pc0: "((Init rT' # ST0, LT0),z0) \<in> phi C0 sig0 ! Suc pc0" and
T0: "G \<turnstile> T0 \<preceq>i Init (Class C')"
apply (simp add: wt_instr_def)
apply (erule disjE)
apply (clarsimp simp add: eff_def eff_bool_def norm_eff_def)
apply (drule bspec, assumption)
apply clarsimp
apply (drule subsetD, rule imageI, assumption)
apply clarsimp
apply simp
done
from wtjvm obtain mb where wf: "wf_prog mb G" by (simp add: wt_jvm_prog_def)
from a_stk0 obtain apts v stk0' where
stk0': "stk0 = apts @ v # stk0'" and
len: "length apts = length apTs" and
v: "approx_val G hp ihp v (OK T0)" and
a_stk0': "approx_stk G hp ihp stk0' ST0"
by - (drule approx_stk_append_lemma, auto)
from stk0' len v a_stk0' wf apTs val T wf methd_C'
have a_stk':
"approx_stk G hp ihp (rval # drop (Suc (length pTs)) stk0) (Init rT'#ST0)"
apply simp
apply (rule approx_val_widen, assumption+)
apply (clarsimp simp add: init_le_Init2)
apply (erule widen_trans)
apply assumption
done
from stk0' len apTs cons0
have cons':
"consistent_init (rval # drop (Suc (length pTs)) stk0) loc0
(Init rT'#ST0, LT0) ihp"
apply simp
apply (drule consistent_init_append)
apply simp
apply (drule consistent_init_pop)
apply (rule consistent_init_Init_stk)
apply assumption
done
from stk0' len apTs corr0
have corr':
"fst sig0 = init \<longrightarrow>
corresponds (rval # drop (Suc (length pTs)) stk0) loc0
(Init rT'#ST0, LT0) ihp (fst r0) (PartInit C0) \<and>
(\<exists>l. fst r0 = Addr l \<and> hp l \<noteq> None \<and>
(ihp l = PartInit C0 \<or> (\<exists>C'. ihp l = Init (Class C'))))"
apply clarsimp
apply (drule corresponds_append)
apply simp
apply (simp add: corresponds_stk_cons)
done
with cons' lenloc0 a_loc0 Suc_pc0 a_stk' wf
have frame':
"correct_frame G hp ihp (Init rT' # ST0,LT0) maxl0 ins0 ?f'"
by (simp add: correct_frame_def)
from state' heap_ok init_ok frame' c_frs class_C0 methd_C0 phi_Suc_pc0 prealloc
have ?thesis by (simp add: correct_state_def) blast
}
ultimately
show "G,phi \<turnstile>JVM state'\<surd>" by (cases frs, blast+)
qed
lemma Return_correct_init:
"\<lbrakk> fst sig = init;
wt_jvm_prog G phi;
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
ins ! pc = Return;
wt_instr (ins!pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et pc;
Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs);
G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd> \<rbrakk>
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
proof -
assume wtjvm: "wt_jvm_prog G phi"
assume mthd: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
assume ins: "ins!pc = Return"
assume wt: "wt_instr (ins!pc) G C rT (phi C sig) maxs
(fst sig = init) (length ins) et pc"
assume state: "Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)"
assume approx:"G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd>"
from approx mthd
obtain s z where
heap_ok: "G \<turnstile>h hp\<surd>" and
init_ok: "h_init G hp ihp" and
prealloc:"preallocated hp ihp" and
classC: "is_class G C" and
some: "(s,z)\<in> phi C sig ! pc" and
frame: "correct_frame G hp ihp s maxl ins (stk, loc, C, sig, pc, r)" and
frames: "correct_frames G hp ihp phi rT sig z r frs"
..
obtain mn pTs where sig: "sig = (mn,pTs)" by (cases sig)
moreover assume sig_in: "fst sig = init"
ultimately have is_init: "mn = init" by simp
from ins some sig is_init wt
obtain T ST LT where
s: "s = (T # ST, LT)" and
T: "G \<turnstile> T \<preceq>i Init rT" and
z: "z"
apply (clarsimp simp add: wt_instr_def eff_def eff_bool_def norm_eff_def)
apply (drule bspec, assumption)
apply clarsimp
apply blast
done
from frame s sig_in
obtain rval stk' loc where
stk: "stk = rval # stk'" and
val: "approx_val G hp ihp rval (OK T)" and
approx_stk: "approx_stk G hp ihp stk' ST" and
approx_val: "approx_loc G hp ihp loc LT" and
consistent: "consistent_init stk loc (T # ST, LT) ihp" and
corr: "corresponds stk loc (T # ST, LT) ihp (fst r) (PartInit C)" and
len: "length loc = Suc (length (snd sig) + maxl)"
by (simp add: correct_frame_def) blast
from stk mthd ins state
have "frs = [] \<Longrightarrow> ?thesis" by (simp add: correct_state_def)
moreover
{ fix f frs' assume frs: "frs = f#frs'"
obtain stk0 loc0 C0 sig0 pc0 r0 where
f: "f = (stk0, loc0, C0, sig0, pc0, r0)" by (cases f)
from f frs frames sig is_init
obtain ST0 LT0 T0 z0 rT0 maxs0 maxl0 ins0 et0 C' apTs D D' rT' body' where
class_C0: "is_class G C0" and
methd_C0: "method (G, C0) sig0 = Some (C0, rT0, maxs0, maxl0, ins0, et0)" and
ins0: "ins0 ! pc0 = Invoke C' mn pTs \<or>
ins0 ! pc0 = Invoke_special C' mn pTs" and
phi_pc0: "((rev apTs @ T0 # ST0, LT0), z0) \<in> phi C0 sig0 ! pc0" and
apTs: "length apTs = length pTs" and
methd_C': "method (G, C') sig = Some (D', rT', body')" "G \<turnstile> rT \<preceq> rT'" and
ctor_ok: "constructor_ok G hp ihp (stk0 ! length apTs) C' z r" and
c_fr: "correct_frame G hp ihp (rev apTs @ T0 # ST0, LT0) maxl0 ins0
(stk0, loc0, C0, sig0, pc0, r0)" and
c_frs: "correct_frames G hp ihp phi rT0 sig0 z0 r0 frs'"
apply simp
apply (elim conjE exE)
apply (rule that)
apply assumption+
apply simp
apply simp
apply assumption+
apply simp
apply (rule conjI,rule refl)+
apply (rule refl)
apply assumption+
apply simp
apply assumption
done
from c_fr
obtain
a_stk0: "approx_stk G hp ihp stk0 (rev apTs @ T0 # ST0)" and
a_loc0: "approx_loc G hp ihp loc0 LT0" and
cons0: "consistent_init stk0 loc0 (rev apTs @ T0 # ST0, LT0) ihp" and
corr0: "fst sig0 = init \<longrightarrow>
corresponds stk0 loc0 (rev apTs @ T0 # ST0, LT0) ihp (fst r0) (PartInit C0) \<and>
(\<exists>l. fst r0 = Addr l \<and> hp l \<noteq> None \<and>
(ihp l = PartInit C0 \<or> (\<exists>C'. ihp l = Init (Class C'))))" and
pc0: "pc0 < length ins0" and
lenloc0:"length loc0 = Suc (length (snd sig0) + maxl0)"
by (unfold correct_frame_def) simp
from pc0 wtjvm methd_C0 have wt0:
"wt_instr (ins0!pc0) G C0 rT0 (phi C0 sig0) maxs0
(fst sig0 = init) (length ins0) et0 pc0"
by - (rule wt_jvm_prog_impl_wt_instr)
let ?z' = "if \<exists>D. T0 = PartInit D then True else z0"
let ?ST' = "Init rT' # replace T0 (Init (theClass T0)) ST0"
let ?LT' = "replace (OK T0) (OK (Init (theClass T0))) LT0"
from ins0 apTs phi_pc0 is_init sig methd_C' wt0
obtain
Suc_pc0: "Suc pc0 < length ins0" and
phi_Suc_pc0: "((?ST',?LT'),?z') \<in> phi C0 sig0 ! Suc pc0" and
T0: "(\<exists>pc. T0 = UnInit C' pc) \<or>
(T0 = PartInit C0 \<and> G \<turnstile> C0 \<prec>C1 C' \<and> ¬z0)"
apply (simp add: wt_instr_def)
apply (erule disjE)
apply simp
apply (clarsimp simp add: eff_def eff_bool_def norm_eff_def)
apply (drule bspec, assumption)
apply clarsimp
apply (drule subsetD, rule imageI, assumption)
apply (rotate_tac -8)
apply (clarsimp simp add: nth_append)
done
from a_stk0 obtain apts oX stk0' where
stk0': "stk0 = apts @ oX # stk0'" "length apts = length apTs" and
a_val: "approx_val G hp ihp oX (OK T0)" and
a_stk: "approx_stk G hp ihp stk0' ST0"
by (force dest!: approx_stk_append_lemma)
with apTs have oX_pos: "stk0!length pTs = oX" by (simp add: nth_append)
let ?c = "snd r"
let ?r' = "if r0 = (oX,Null) then (oX, ?c) else r0"
let ?stk' = "rval#(replace oX ?c stk0')"
let ?loc' = "replace oX ?c loc0"
let ?f' = "(?stk',?loc',C0,sig0,Suc pc0,?r')"
from stk apTs stk0' mthd ins sig f frs is_init state oX_pos
have state': "state' = Norm (hp, ihp, ?f' # frs')" by (simp add: split_beta)
from wtjvm obtain mb where "wf_prog mb G" by (simp add: wt_jvm_prog_def)
from ctor_ok z apTs oX_pos a_val T0
obtain C'' D pc' a c fs1 fs3 where
a: "oX = Addr a" and
ihp_a: "ihp a = UnInit C'' pc' \<or> ihp a = PartInit D" and
hp_a: "hp a = Some (C'', fs1)" and
c: "snd r = Addr c" and
ihp_c: "ihp c = Init (Class C'')" and
hp_c: "hp c = Some (C'', fs3)"
by (simp add: constructor_ok_def, clarify) auto
from a_val a hp_a T0
have "G \<turnstile> C'' \<preceq>C C'\<and> (T0 = PartInit C0 \<longrightarrow> G \<turnstile> C'' \<preceq>C C0)"
apply -
apply (erule disjE)
apply (clarsimp simp add: approx_val_def iconf_def)
apply (clarsimp simp add: approx_val_def iconf_def)
apply (simp add: conf_def)
apply (rule rtrancl_trans, assumption)
apply blast
done
with c hp_c ihp_c heap_ok T0
have a_val':
"approx_val G hp ihp (snd r) (OK (Init (theClass T0)))"
apply (simp add: approx_val_def iconf_def is_init_def)
apply (erule disjE)
apply clarsimp
apply (rule conf_obj_AddrI, assumption+)
apply clarsimp
apply (rule conf_obj_AddrI, assumption+)
done
from stk0' cons0 T0
have corr:
"corresponds stk0' loc0 (ST0,LT0) ihp oX T0"
apply simp
apply (erule disjE)
apply (elim exE)
apply (drule consistent_init_append)
apply simp
apply (drule consistent_init_corresponds_stk_cons)
apply blast
apply (simp add: corresponds_stk_cons)
apply (drule consistent_init_append)
apply simp
apply (drule consistent_init_corresponds_stk_cons)
apply blast
apply (simp add: corresponds_stk_cons)
done
from a_val a_val' a_loc0 T0 corr
have a_loc':
"approx_loc G hp ihp ?loc' ?LT'"
by (auto elim: approx_loc_replace simp add: corresponds_def)
from wf T methd_C' a_val a_val' a_stk corr T0 val
have a_stk':
"approx_stk G hp ihp ?stk' ?ST'"
apply -
apply clarsimp
apply (rule conjI)
apply (clarsimp simp add: approx_val_def iconf_def init_le_Init2)
apply (rule conf_widen, assumption+)
apply (erule widen_trans, assumption)
apply (unfold approx_stk_def)
apply (erule disjE)
apply (elim exE conjE)
apply (drule approx_loc_replace)
apply assumption back
apply assumption
apply blast
apply (simp add: corresponds_def corr_stk_def)
apply (simp add: replace_map_OK)
apply (elim exE conjE)
apply (drule approx_loc_replace)
apply assumption back
apply assumption
apply blast
apply (simp add: corresponds_def corr_stk_def)
apply (simp add: replace_map_OK)
done
from stk0' apTs cons0
have "consistent_init stk0' loc0 (ST0,LT0) ihp"
apply simp
apply (drule consistent_init_append, simp)
apply (erule consistent_init_pop)
done
with a_stk a_loc0 a_val
have cons': "consistent_init ?stk' ?loc' (?ST', ?LT') ihp"
apply -
apply (rule consistent_init_Init_stk)
apply (erule consisten_init_replace)
apply assumption+
apply (rule refl)
done
from stk0' len apTs corr0
have
"fst sig0 = init \<longrightarrow>
corresponds (rval # stk0') loc0 (Init rT'#ST0, LT0) ihp (fst r0) (PartInit C0)"
apply clarsimp
apply (drule corresponds_append)
apply simp
apply (simp add: corresponds_stk_cons)
done
with a_stk a_loc0 a_val
have corr':
"fst sig0 = init \<longrightarrow>
corresponds ?stk' ?loc' (?ST', ?LT') ihp (fst r0) (PartInit C0)"
apply -
apply clarify
apply (simp add: corresponds_stk_cons)
apply (erule corresponds_replace)
apply assumption+
apply simp
apply blast
done
have fst_r': "fst ?r' = fst r0" by simp
from lenloc0 a_loc' Suc_pc0 a_stk' cons' fst_r' corr' corr0
have c_fr': "correct_frame G hp ihp (?ST', ?LT') maxl0 ins0 ?f'"
apply (unfold correct_frame_def)
apply clarify
apply (clarsimp simp add: map_eq_Cons split del: split_if)
done
from c_frs
have frs'1:
"fst sig0 \<noteq> init \<Longrightarrow> correct_frames G hp ihp phi rT0 sig0 ?z' ?r' frs'"
apply -
apply (cases frs')
apply simp
apply (clarsimp split del: split_if)
apply (intro exI conjI)
apply assumption+
apply (rule refl)
apply assumption+
done
moreover
have frs'2: "frs' = [] \<Longrightarrow> correct_frames G hp ihp phi rT0 sig0 ?z' ?r' frs'"
by simp
moreover
{ fix f'' frs''
assume cons: "frs' = f'' # frs''"
assume sig0_in: "fst sig0 = init"
{ assume eq: "oX = fst r0"
with corr0 sig0_in
have "corresponds stk0 loc0 (rev apTs @ T0 # ST0, LT0) ihp oX (PartInit C0)"
by simp
with stk0'
have "corresponds (oX#stk0') loc0 (T0#ST0, LT0) ihp oX (PartInit C0)"
apply simp
apply (rule corresponds_append)
apply assumption
apply simp
done
with a ihp_a eq corr0 sig0_in T0
have "ihp a = PartInit C0"
by (clarsimp simp add: corresponds_stk_cons corr_val_def)
with a T0 a_val
have z0: "T0 = PartInit C0 \<and> ¬z0"
by (auto simp add: approx_val_def iconf_def)
from c_frs sig0_in z0 cons
have "snd r0 = Null"
apply -
apply (drule correct_frames_ctor_ok)
apply clarsimp
apply (simp add: constructor_ok_def split_beta)
done
moreover
have "r0 = (fst r0, snd r0)" by simp
ultimately
have eq_r0: "r0 = (oX, Null)" by (simp add: eq)
with apTs oX_pos ctor_ok c_frs z cons
have "correct_frames G hp ihp phi rT0 sig0 True (oX, ?c) frs'"
apply (clarsimp split del: split_if)
apply (intro exI conjI)
apply assumption+
apply (rule refl)
apply assumption+
apply (rule impI, erule impE, assumption)
apply (rule constructor_ok_pass_val)
apply assumption
apply simp
apply simp
apply assumption+
done
with oX_pos apTs z0 eq_r0
have "correct_frames G hp ihp phi rT0 sig0 ?z' ?r' frs'" by simp
}
moreover
{ assume neq: "oX \<noteq> fst r0"
with T0 stk0' corr0 sig0_in
have "\<exists>pc'. T0 = UnInit C' pc'"
apply simp
apply (erule disjE)
apply simp
apply clarify
apply (drule corresponds_append)
apply simp
apply (simp add: corresponds_stk_cons)
done
with c_frs apTs oX_pos neq
have "correct_frames G hp ihp phi rT0 sig0 ?z' ?r' frs'" by clarsimp
}
ultimately
have "correct_frames G hp ihp phi rT0 sig0 ?z' ?r' frs'" by blast
}
ultimately
have "correct_frames G hp ihp phi rT0 sig0 ?z' ?r' frs'"
by (cases frs', blast+)
with state' heap_ok init_ok c_frs class_C0 methd_C0 phi_Suc_pc0 c_fr' prealloc
have ?thesis by (unfold correct_state_def) fastsimp
}
ultimately
show "G,phi \<turnstile>JVM state'\<surd>" by (cases frs, blast+)
qed
lemma Return_correct:
"\<lbrakk> wt_jvm_prog G phi;
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
ins ! pc = Return;
wt_instr (ins!pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et pc;
Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs) ;
G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd> \<rbrakk>
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
apply (cases "fst sig = init")
apply (rule Return_correct_init)
apply assumption+
apply (rule Return_correct_not_init)
apply simp
apply assumption+
done
lemmas [simp] = map_append
lemma Goto_correct:
"\<lbrakk> wf_prog wt G;
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
ins ! pc = Goto branch;
wt_instr (ins!pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et pc;
Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs) ;
G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd> \<rbrakk>
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
apply (elim correctE, assumption)
apply (clarsimp simp add: defs2)
apply (rule exI)+
apply (rule conjI)
apply (erule subsetD)
apply (erule imageE2)
apply simp
apply (rule conjI, rule refl)+
apply (rule refl)
apply clarsimp
done
lemma Ifcmpeq_correct:
"\<lbrakk> wf_prog wt G;
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
ins ! pc = Ifcmpeq branch;
wt_instr (ins!pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et pc;
Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs) ;
G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd> \<rbrakk>
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
apply (elim correctE, assumption)
apply (clarsimp simp add: defs2)
apply (drule bspec, assumption)
apply clarsimp
apply (rule conjI, rule impI)
apply (rule exI)+
apply (rule conjI)
apply (erule subsetD)
apply (erule imageE2)
apply simp
apply (rule conjI, rule refl)+
apply (rule refl)
apply clarsimp
apply (rule conjI)
apply (drule consistent_init_pop)+
apply assumption
apply (rule impI, erule impE, assumption, erule conjE)
apply (drule corresponds_pop)+
apply assumption
apply (rule impI)
apply (rule exI)+
apply (rule conjI)
apply (erule subsetD)
apply (erule imageE2)
apply simp
apply (rule conjI, rule refl)+
apply (rule refl)
apply clarsimp
apply (rule conjI)
apply (drule consistent_init_pop)+
apply assumption
apply (rule impI, erule impE, assumption, erule conjE)
apply (drule corresponds_pop)+
apply assumption
done
lemma Pop_correct:
"\<lbrakk> wf_prog wt G;
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
ins ! pc = Pop;
wt_instr (ins!pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et pc;
Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs) ;
G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd> \<rbrakk>
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
apply (elim correctE, assumption)
apply (clarsimp simp add: defs2)
apply (drule bspec, assumption)
apply clarsimp
apply (rule exI)+
apply (rule conjI)
apply (erule subsetD)
apply (erule imageE2)
apply simp
apply (rule conjI, rule refl)+
apply (rule refl)
apply clarsimp
apply (fast dest: consistent_init_pop corresponds_pop)
done
lemma Dup_correct:
"\<lbrakk> wf_prog wt G;
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
ins ! pc = Dup;
wt_instr (ins!pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et pc;
Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs) ;
G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd> \<rbrakk>
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
apply (elim correctE, assumption)
apply (clarsimp simp add: defs2 map_eq_Cons)
apply (drule bspec, assumption)
apply clarsimp
apply (rule exI)+
apply (rule conjI)
apply (erule subsetD)
apply (erule imageE2)
apply simp
apply (rule conjI, rule refl)+
apply (rule refl)
apply clarsimp
apply (rule conjI)
apply (erule consistent_init_Dup)
apply (rule impI, erule impE, assumption, erule conjE)
apply (erule corresponds_Dup)
done
lemma Dup_x1_correct:
"\<lbrakk> wf_prog wt G;
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
ins ! pc = Dup_x1;
wt_instr (ins!pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et pc;
Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs) ;
G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd> \<rbrakk>
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
apply (elim correctE, assumption)
apply (clarsimp simp add: defs2 map_eq_Cons)
apply (drule bspec, assumption)
apply clarsimp
apply (rule exI)+
apply (rule conjI)
apply (erule subsetD)
apply (erule imageE2)
apply simp
apply (rule conjI, rule refl)+
apply (rule refl)
apply clarsimp
apply (rule conjI)
apply (erule consistent_init_Dup_x1)
apply (rule impI, erule impE, assumption, erule conjE)
apply (erule corresponds_Dup_x1)
done
lemma Dup_x2_correct:
"\<lbrakk> wf_prog wt G;
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
ins ! pc = Dup_x2;
wt_instr (ins!pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et pc;
Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs) ;
G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd> \<rbrakk>
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
apply (elim correctE, assumption)
apply (clarsimp simp add: defs2 map_eq_Cons)
apply (drule bspec, assumption)
apply clarsimp
apply (rule exI)+
apply (rule conjI)
apply (erule subsetD)
apply (erule imageE2)
apply simp
apply (rule conjI, rule refl)+
apply (rule refl)
apply clarsimp
apply (rule conjI)
apply (erule consistent_init_Dup_x2)
apply (rule impI, erule impE, assumption, erule conjE)
apply (erule corresponds_Dup_x2)
done
lemma Swap_correct:
"\<lbrakk> wf_prog wt G;
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
ins ! pc = Swap;
wt_instr (ins!pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et pc;
Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs) ;
G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd> \<rbrakk>
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
apply (elim correctE, assumption)
apply (clarsimp simp add: defs2 map_eq_Cons)
apply (drule bspec, assumption)
apply clarsimp
apply (rule exI)+
apply (rule conjI)
apply (erule subsetD)
apply (erule imageE2)
apply simp
apply (rule conjI, rule refl)+
apply (rule refl)
apply clarsimp
apply (rule conjI)
apply (erule consistent_init_Swap)
apply (rule impI, erule impE, assumption, erule conjE)
apply (erule corresponds_Swap)
done
lemma IAdd_correct:
"\<lbrakk> wf_prog wt G;
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
ins ! pc = IAdd;
wt_instr (ins!pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et pc;
Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs) ;
G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd> \<rbrakk>
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
apply (elim correctE, assumption)
apply (clarsimp simp add: defs2 map_eq_Cons)
apply (drule bspec, assumption)
apply clarsimp
apply (rule exI)+
apply (rule conjI)
apply (erule subsetD)
apply (erule imageE2)
apply simp
apply (rule conjI, rule refl)+
apply (rule refl)
apply (clarsimp simp add: approx_val_def iconf_def init_le_Init conf_def)
apply (simp add: is_init_def)
apply (drule consistent_init_pop)+
apply (simp add: corresponds_stk_cons)
apply (blast intro: consistent_init_Init_stk)
done
lemma Throw_correct:
"\<lbrakk> wf_prog wt G;
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
ins ! pc = Throw;
Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs) ;
G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd>;
fst (exec_instr (ins!pc) G hp ihp stk loc C sig pc r frs) = None \<rbrakk>
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
by simp
lemma Jsr_correct:
"\<lbrakk>wf_prog wt G;
method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
G,phi \<turnstile>JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) \<surd>;
wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et pc;
fst (exec_instr (ins ! pc) G hp ihp stk loc C sig pc r frs) = None; ins ! pc = Jsr b\<rbrakk>
\<Longrightarrow> G,phi \<turnstile>JVM state' \<surd>"
apply (elim correctE, assumption)
apply (clarsimp simp add: defs2 map_eq_Cons)
apply (drule bspec, assumption)
apply clarsimp
apply (rule exI)+
apply (rule conjI)
apply (erule subsetD)
apply (erule imageE2)
apply simp
apply (rule conjI, rule refl)+
apply (rule refl)
apply clarsimp
apply (rule conjI)
apply (simp add: approx_val_def iconf_def is_init_def)
apply (rule conjI)
apply (erule consistent_init_Init_stk)
apply (rule impI, erule impE, assumption, erule conjE)
apply (simp add: corresponds_def corr_stk_def corr_loc_cons)
done
lemma phi_finite:
assumes wt: "wt_jvm_prog G phi"
assumes meth: "method (G, C) sig = Some (C, rT, maxs, maxl, ins, et)"
assumes corr: "G,phi \<turnstile>JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) \<surd>"
shows "finite (phi C sig!pc)"
proof -
from corr meth
have len: "pc < length ins" and "is_class G C"
by (unfold correct_state_def correct_frame_def) auto
with wt meth
have "wt_method G C (fst sig) (snd sig) rT maxs maxl ins et (phi C sig)"
by (auto dest: method_wf_mdecl simp add: wt_jvm_prog_def wf_mdecl_def)
with len obtain maxr where
"set (phi C sig) \<subseteq> Pow (address_types G maxs maxr (length ins))"
"pc < length (phi C sig)"
by (clarsimp simp add: wt_method_def check_types_def states_def)
hence "phi C sig ! pc \<in> Pow (address_types G maxs maxr (length ins))"
by (auto intro!: nth_in)
thus ?thesis by (auto elim: finite_subset intro: finite_address_types)
qed
lemma Ret_correct:
"\<lbrakk>wt_jvm_prog G phi;
method (G, C) sig = Some (C, rT, maxs, maxl, ins, et); Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
G,phi \<turnstile>JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) \<surd>;
wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et pc;
fst (exec_instr (ins ! pc) G hp ihp stk loc C sig pc r frs) = None; ins ! pc = Ret idx\<rbrakk>
\<Longrightarrow> G,phi \<turnstile>JVM state' \<surd>"
apply (frule phi_finite, assumption+)
apply (elim correctE, assumption)
apply (clarsimp simp add: defs2 map_eq_Cons)
apply (simp add: set_SOME_lists finite_imageI)
apply (drule bspec, assumption)
apply clarsimp
apply (drule bspec)
apply (rule UnI1)
apply (rule imageI)
apply (rule imageI)
apply assumption
apply (clarsimp simp add: theRA_def)
apply (subgoal_tac "loc!idx = RetAddr ra")
apply (simp add: split_def)
apply (rule exI)+
apply (rule conjI)
apply (erule subsetD)
apply simp
apply (rule conjI, assumption)
apply simp
apply simp
apply (clarsimp simp add: approx_loc_def list_all2_conv_all_nth)
apply (erule allE, erule impE, assumption)
apply (clarsimp simp add: approx_val_def iconf_def conf_def)
apply (cases "loc!idx")
apply auto
done
text {*
The next theorem collects the results of the sections above,
i.e.~exception handling and the execution step for each
instruction. It states type safety for single step execution:
in welltyped programs, a conforming state is transformed
into another conforming state when one instruction is executed.
*}
theorem instr_correct:
"\<lbrakk> wt_jvm_prog G phi;
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs);
G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd> \<rbrakk>
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
apply (frule wt_jvm_prog_impl_wt_instr_cor)
apply assumption+
apply (cases "fst (exec_instr (ins!pc) G hp ihp stk loc C sig pc r frs)")
defer
apply (erule xcpt_correct, assumption+)
apply (cases "ins!pc")
prefer 21
apply (rule Ret_correct, assumption+)
prefer 8
apply (rule Invoke_correct, assumption+)
prefer 8
apply (rule Invoke_special_correct, assumption+)
prefer 8
apply (rule Return_correct, assumption+)
prefer 5
apply (rule Getfield_correct, assumption+)
prefer 6
apply (rule Checkcast_correct, assumption+)
apply (unfold wt_jvm_prog_def)
apply (rule Load_correct, assumption+)
apply (rule Store_correct, assumption+)
apply (rule LitPush_correct, assumption+)
apply (rule New_correct, assumption+)
apply (rule Putfield_correct, assumption+)
apply (rule Pop_correct, assumption+)
apply (rule Dup_correct, assumption+)
apply (rule Dup_x1_correct, assumption+)
apply (rule Dup_x2_correct, assumption+)
apply (rule Swap_correct, assumption+)
apply (rule IAdd_correct, assumption+)
apply (rule Goto_correct, assumption+)
apply (rule Ifcmpeq_correct, assumption+)
apply (rule Throw_correct, assumption+)
apply (rule Jsr_correct, assumption+)
done
section {* Main *}
lemma correct_state_impl_Some_method:
"G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd>
\<Longrightarrow> \<exists>meth. method (G,C) sig = Some(C,meth)"
by (auto simp add: correct_state_def Let_def)
lemma BV_correct_1 [rule_format]:
"\<And>state. \<lbrakk> wt_jvm_prog G phi; G,phi \<turnstile>JVM state\<surd>\<rbrakk>
\<Longrightarrow> exec (G,state) = Some state' \<longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
apply (simp only: split_tupled_all)
apply (rename_tac xp hp ihp frs)
apply (case_tac xp)
apply (case_tac frs)
apply simp
apply (simp only: split_tupled_all)
apply hypsubst
apply (frule correct_state_impl_Some_method)
apply (force intro: instr_correct)
apply (case_tac frs)
apply simp_all
done
lemma L0:
"\<lbrakk> xp=None; frs\<noteq>[] \<rbrakk> \<Longrightarrow> (\<exists>state'. exec (G,xp,hp,ihp,frs) = Some state')"
by (clarsimp simp add: neq_Nil_conv split_beta)
lemma L1:
"\<lbrakk>wt_jvm_prog G phi; G,phi \<turnstile>JVM (xp,hp,ihp,frs)\<surd>; xp=None; frs\<noteq>[]\<rbrakk>
\<Longrightarrow> \<exists>state'. exec(G,xp,hp,ihp,frs) = Some state' \<and> G,phi \<turnstile>JVM state'\<surd>"
apply (drule L0)
apply assumption
apply (fast intro: BV_correct_1)
done
theorem BV_correct [rule_format]:
"\<lbrakk> wt_jvm_prog G phi; G \<turnstile> s -jvm\<rightarrow> t \<rbrakk> \<Longrightarrow> G,phi \<turnstile>JVM s\<surd> \<longrightarrow> G,phi \<turnstile>JVM t\<surd>"
apply (unfold exec_all_def)
apply (erule rtrancl_induct)
apply simp
apply (auto intro: BV_correct_1)
done
theorem BV_correct_implies_approx:
"\<lbrakk> wt_jvm_prog G phi;
G \<turnstile> s0 -jvm\<rightarrow> (None,hp,ihp,(stk,loc,C,sig,pc,r)#frs); G,phi \<turnstile>JVM s0 \<surd>\<rbrakk>
\<Longrightarrow> \<exists>ST LT z. ((ST,LT),z) \<in> (phi C sig) ! pc \<and>
approx_stk G hp ihp stk ST \<and>
approx_loc G hp ihp loc LT"
apply (drule BV_correct)
apply assumption+
apply (clarsimp simp add: correct_state_def correct_frame_def split_def
split: option.splits)
apply blast
apply blast
done
lemma hconf_start:
fixes G :: jvm_prog ("\<Gamma>")
assumes wf: "wf_prog wf_mb \<Gamma>"
shows "\<Gamma> \<turnstile>h (start_heap \<Gamma>) \<surd>"
apply (unfold hconf_def start_heap_def)
apply (auto simp add: blank_def oconf_def split: split_if_asm)
apply (simp add: fields_is_type [OF _ wf is_class_xcpt [OF wf]])+
done
lemma hinit_start:
fixes G :: jvm_prog ("\<Gamma>")
assumes wf: "wf_prog wf_mb \<Gamma>"
shows "h_init \<Gamma> (start_heap \<Gamma>) start_iheap"
apply (unfold h_init_def start_heap_def start_iheap_def)
apply (auto simp add: blank_def o_init_def l_init_def
is_init_def split: split_if_asm)
apply (auto simp add: init_vars_def map_of_map)
done
lemma consistent_init_start:
"consistent_init [] (Null#replicate n arbitrary) ([], OK (Init (Class C))#replicate n Err) hp"
apply (induct n)
apply (auto simp add: consistent_init_def corresponds_def corr_stk_def corr_loc_def)
done
lemma BV_correct_initial:
fixes G :: jvm_prog ("\<Gamma>") and Phi :: prog_type ("\<Phi>")
shows
"wt_jvm_prog \<Gamma> \<Phi> \<Longrightarrow> is_class \<Gamma> C \<Longrightarrow> method (\<Gamma>,C) (m,[]) = Some (C, b) \<Longrightarrow> m \<noteq> init
\<Longrightarrow> \<Gamma>,\<Phi> \<turnstile>JVM start_state G C m \<surd>"
apply (cases b)
apply (unfold start_state_def)
apply (unfold correct_state_def)
apply (auto simp add: preallocated_start)
apply (simp add: wt_jvm_prog_def hconf_start)
apply (simp add: wt_jvm_prog_def hinit_start)
apply (drule wt_jvm_prog_impl_wt_start, assumption+)
apply (clarsimp simp add: wt_start_def)
apply (auto simp add: correct_frame_def)
apply (simp add: approx_stk_def)
apply (rule exI, rule conjI)
apply (rule exI, assumption)
apply clarsimp
apply (simp add: consistent_init_start)
apply (auto simp add: approx_val_def iconf_def is_init_def dest!: widen_RefT)
done
theorem typesafe:
fixes G :: jvm_prog ("\<Gamma>") and Phi :: prog_type ("\<Phi>")
assumes welltyped: "wt_jvm_prog \<Gamma> \<Phi>" and
main: "is_class \<Gamma> C" "method (\<Gamma>,C) (m,[]) = Some (C, b)" "m \<noteq> init"
shows
"G \<turnstile> start_state \<Gamma> C m -jvm\<rightarrow> s \<Longrightarrow> \<Gamma>,\<Phi> \<turnstile>JVM s \<surd>"
proof -
from welltyped main
have "\<Gamma>,\<Phi> \<turnstile>JVM start_state \<Gamma> C m \<surd>" by (rule BV_correct_initial)
moreover
assume "G \<turnstile> start_state \<Gamma> C m -jvm\<rightarrow> s"
ultimately
show "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>" using welltyped by - (rule BV_correct)
qed
end
lemmas defs1:
correct_state G phi ==
%(xp, hp, ihp, frs).
case xp of
None =>
case frs of [] => True
| f # fs =>
G |-h hp [ok] &
h_init G hp ihp &
preallocated hp ihp &
(let (stk, loc, C, sig, pc, r) = f
in EX rT maxs maxl ins et s z.
is_class G C &
method (G, C) sig = Some (C, rT, maxs, maxl, ins, et) &
(s, z) : phi C sig ! pc &
correct_frame G hp ihp s maxl ins f &
correct_frames G hp ihp phi rT sig z r fs)
| Some x => frs = []
correct_frame G hp i ==
%(ST, LT) maxl ins (stk, loc, C, sig, pc, r).
approx_stk G hp i stk ST &
approx_loc G hp i loc LT &
consistent_init stk loc (ST, LT) i &
(fst sig = init -->
corresponds stk loc (ST, LT) i (fst r) (PartInit C) &
(EX l. fst r = Addr l &
hp l ~= None &
(i l = PartInit C | (EX C'. i l = Init (Class C'))))) &
pc < length ins & length loc = length (snd sig) + maxl + 1
wt_instr i G C rT phi mxs ini max_pc et pc == app i G C pc mxs max_pc rT ini et (phi ! pc) & (ALL (pc', s'):set (eff i G pc et (phi ! pc)). pc' < max_pc & s' <= phi ! pc')
eff i G pc et at == map (%pc'. (pc', norm_eff i G pc pc' at)) (succs i pc at) @ xcpt_eff i G pc at et
norm_eff i G pc pc' at ==
eff_bool i G pc `
(if EX idx. i = Ret idx then {s. s : at & pc' = theRA (theIdx i) s} else at)
eff_bool i G pc ==
%((ST, LT), z).
(eff' (i, G, pc, ST, LT),
if EX C p D. i = Invoke_special C init p & ST ! length p = PartInit D
then True else z)
lemmas correctE:
[| G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok];
method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
!!ST LT z.
[| G |-h hp [ok]; h_init G hp ihp; preallocated hp ihp; is_class G C;
((ST, LT), z) : phi C sig ! pc;
correct_frame G hp ihp (ST, LT) maxl ins (stk, loc, C, sig, pc, r);
correct_frames G hp ihp phi rT sig z r frs |]
==> P |]
==> P
[| correct_frame G hp ihp (ST, LT) maxl ins (stk, loc, C, sig, pc, r);
[| approx_stk G hp ihp stk ST; approx_loc G hp ihp loc LT;
consistent_init stk loc (ST, LT) ihp;
fst sig = init -->
corresponds stk loc (ST, LT) ihp (fst r) (PartInit C) &
(EX l. fst r = Addr l &
hp l ~= None &
(ihp l = PartInit C | (EX C'. ihp l = Init (Class C'))));
pc < length ins; length loc = length (snd sig) + maxl + 1 |]
==> P |]
==> P
lemmas
(ALL x. P x) = (ALL a b. P (a, b))
lemma wt_jvm_prog_impl_wt_instr_cor:
[| wt_jvm_prog G phi; method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok] |]
==> wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et
pc
lemma exec_instr_xcpt:
(fst (exec_instr i G hp ihp stk vars Cl sig pc z frs) = Some xcp) =
(EX stk'.
exec_instr i G hp ihp stk vars Cl sig pc z frs =
(Some xcp, hp, ihp, (stk', vars, Cl, sig, pc, z) # frs))
lemma in_match_any:
match_exception_table G xcpt pc et = Some pc'
==> EX C. C : set (match_any G pc et) &
G |- xcpt <=C C & match_exception_table G C pc et = Some pc'
lemma match_et_imp_match:
match_exception_table G X pc et = Some handler ==> match G X pc et = [X]
lemma imageE2:
[| x : A; y = f x |] ==> y : f ` A
lemma uncaught_xcpt_correct:
[| wt_jvm_prog G phi; xcp = Addr adr; hp adr = Some T; is_init hp ihp xcp;
G,phi |-JVM Norm (hp, ihp, f # frs) [ok] |]
==> G,phi |-JVM find_handler G (Some xcp) hp ihp frs [ok]
lemma
[| fst (exec_instr (ins ! pc) G hp ihp stk vars Cl sig pc r frs) = Some xcp;
wt_instr (ins ! pc) G Cl rT (phi C sig) maxs (fst sig = init) (length ins) et
pc;
G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok] |]
==> EX adr T. xcp = Addr adr & hp adr = Some T & is_init hp ihp xcp
lemma cname_of_xcp:
[| preallocated hp ihp; xcp = Addr (XcptRef x) |] ==> cname_of hp xcp = Xcpt x
lemma prealloc_is_init:
preallocated hp ihp ==> is_init hp ihp (Addr (XcptRef x))
lemma wt_jvm_progE:
[| wt_jvm_prog G phi; !!wt. wf_prog wt G ==> P |] ==> P
lemma
[| wt_jvm_prog G phi; method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et
pc;
fst (exec_instr (ins ! pc) G hp ihp stk loc C sig pc r frs) = Some xcp;
Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok] |]
==> G,phi |-JVM state' [ok]
lemmas
(x ~= Err) = (EX a. x = OK a)
lemma Load_correct:
[| wf_prog wt G; method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
ins ! pc = Load idx;
wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et
pc;
Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok] |]
==> G,phi |-JVM state' [ok]
lemma Store_correct:
[| wf_prog wt G; method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
ins ! pc = Store idx;
wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et
pc;
Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok] |]
==> G,phi |-JVM state' [ok]
lemma LitPush_correct:
[| wf_prog wt G; method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
ins ! pc = LitPush v;
wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et
pc;
Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok] |]
==> G,phi |-JVM state' [ok]
lemma Cast_conf2:
[| wf_prog ok G; G,h |- v ::<= RefT rt; cast_ok G C h v; G |- Class C <= T;
is_class G C |]
==> G,h |- v ::<= T
lemmas defs2:
correct_state G phi ==
%(xp, hp, ihp, frs).
case xp of
None =>
case frs of [] => True
| f # fs =>
G |-h hp [ok] &
h_init G hp ihp &
preallocated hp ihp &
(let (stk, loc, C, sig, pc, r) = f
in EX rT maxs maxl ins et s z.
is_class G C &
method (G, C) sig = Some (C, rT, maxs, maxl, ins, et) &
(s, z) : phi C sig ! pc &
correct_frame G hp ihp s maxl ins f &
correct_frames G hp ihp phi rT sig z r fs)
| Some x => frs = []
correct_frame G hp i ==
%(ST, LT) maxl ins (stk, loc, C, sig, pc, r).
approx_stk G hp i stk ST &
approx_loc G hp i loc LT &
consistent_init stk loc (ST, LT) i &
(fst sig = init -->
corresponds stk loc (ST, LT) i (fst r) (PartInit C) &
(EX l. fst r = Addr l &
hp l ~= None &
(i l = PartInit C | (EX C'. i l = Init (Class C'))))) &
pc < length ins & length loc = length (snd sig) + maxl + 1
wt_instr i G C rT phi mxs ini max_pc et pc == app i G C pc mxs max_pc rT ini et (phi ! pc) & (ALL (pc', s'):set (eff i G pc et (phi ! pc)). pc' < max_pc & s' <= phi ! pc')
eff i G pc et at == map (%pc'. (pc', norm_eff i G pc pc' at)) (succs i pc at) @ xcpt_eff i G pc at et
norm_eff i G pc pc' at ==
eff_bool i G pc `
(if EX idx. i = Ret idx then {s. s : at & pc' = theRA (theIdx i) s} else at)
eff_bool i G pc ==
%((ST, LT), z).
(eff' (i, G, pc, ST, LT),
if EX C p D. i = Invoke_special C init p & ST ! length p = PartInit D
then True else z)
raise_system_xcpt b x == if b then Some (Addr (XcptRef x)) else None
lemma Checkcast_correct:
[| wt_jvm_prog G phi; method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
ins ! pc = Checkcast D;
wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et
pc;
Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok];
fst (exec_instr (ins ! pc) G hp ihp stk loc C sig pc r frs) = None |]
==> G,phi |-JVM state' [ok]
lemma Getfield_correct:
[| wt_jvm_prog G phi; method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
ins ! pc = Getfield F D;
wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et
pc;
Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok];
fst (exec_instr (ins ! pc) G hp ihp stk loc C sig pc r frs) = None |]
==> G,phi |-JVM state' [ok]
lemma Putfield_correct:
[| wf_prog wt G; method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
ins ! pc = Putfield F D;
wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et
pc;
Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok];
fst (exec_instr (ins ! pc) G hp ihp stk loc C sig pc r frs) = None |]
==> G,phi |-JVM state' [ok]
lemma New_correct:
[| wf_prog wt G; method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
ins ! pc = New X;
wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et
pc;
Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok];
fst (exec_instr (ins ! pc) G hp ihp stk loc C sig pc r frs) = None |]
==> G,phi |-JVM state' [ok]
lemmas
(EX x. P x) = (EX a b. P (a, b))
lemma zip_map:
length a = length b ==> zip (map f a) (map g b) = map (%(x, y). (f x, g y)) (zip a b)
lemma Invoke_correct:
[| wt_jvm_prog G phi; method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
ins ! pc = Invoke C' mn pTs;
wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et
pc;
Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok];
fst (exec_instr (ins ! pc) G hp ihp stk loc C sig pc r frs) = None |]
==> G,phi |-JVM state' [ok]
lemma Invoke_special_correct:
[| wt_jvm_prog G phi; method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
ins ! pc = Invoke_special C' mn pTs;
wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et
pc;
Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok];
fst (exec_instr (ins ! pc) G hp ihp stk loc C sig pc r frs) = None |]
==> G,phi |-JVM state' [ok]
lemmas
map f (xs @ ys) = map f xs @ map f ys
lemma Return_correct_not_init:
[| fst sig ~= init; wt_jvm_prog G phi;
method (G, C) sig = Some (C, rT, maxs, maxl, ins, et); ins ! pc = Return;
wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et
pc;
Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok] |]
==> G,phi |-JVM state' [ok]
lemma Return_correct_init:
[| fst sig = init; wt_jvm_prog G phi;
method (G, C) sig = Some (C, rT, maxs, maxl, ins, et); ins ! pc = Return;
wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et
pc;
Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok] |]
==> G,phi |-JVM state' [ok]
lemma Return_correct:
[| wt_jvm_prog G phi; method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
ins ! pc = Return;
wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et
pc;
Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok] |]
==> G,phi |-JVM state' [ok]
lemmas
map f (xs @ ys) = map f xs @ map f ys
lemma Goto_correct:
[| wf_prog wt G; method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
ins ! pc = Goto branch;
wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et
pc;
Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok] |]
==> G,phi |-JVM state' [ok]
lemma Ifcmpeq_correct:
[| wf_prog wt G; method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
ins ! pc = Ifcmpeq branch;
wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et
pc;
Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok] |]
==> G,phi |-JVM state' [ok]
lemma Pop_correct:
[| wf_prog wt G; method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
ins ! pc = Pop;
wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et
pc;
Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok] |]
==> G,phi |-JVM state' [ok]
lemma Dup_correct:
[| wf_prog wt G; method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
ins ! pc = Dup;
wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et
pc;
Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok] |]
==> G,phi |-JVM state' [ok]
lemma Dup_x1_correct:
[| wf_prog wt G; method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
ins ! pc = Dup_x1;
wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et
pc;
Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok] |]
==> G,phi |-JVM state' [ok]
lemma Dup_x2_correct:
[| wf_prog wt G; method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
ins ! pc = Dup_x2;
wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et
pc;
Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok] |]
==> G,phi |-JVM state' [ok]
lemma Swap_correct:
[| wf_prog wt G; method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
ins ! pc = Swap;
wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et
pc;
Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok] |]
==> G,phi |-JVM state' [ok]
lemma IAdd_correct:
[| wf_prog wt G; method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
ins ! pc = IAdd;
wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et
pc;
Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok] |]
==> G,phi |-JVM state' [ok]
lemma Throw_correct:
[| wf_prog wt G; method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
ins ! pc = Throw;
Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok];
fst (exec_instr (ins ! pc) G hp ihp stk loc C sig pc r frs) = None |]
==> G,phi |-JVM state' [ok]
lemma Jsr_correct:
[| wf_prog wt G; method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok];
wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et
pc;
fst (exec_instr (ins ! pc) G hp ihp stk loc C sig pc r frs) = None;
ins ! pc = Jsr b |]
==> G,phi |-JVM state' [ok]
lemma
[| wt_jvm_prog G phi; method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok] |]
==> finite (phi C sig ! pc)
lemma Ret_correct:
[| wt_jvm_prog G phi; method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok];
wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et
pc;
fst (exec_instr (ins ! pc) G hp ihp stk loc C sig pc r frs) = None;
ins ! pc = Ret idx |]
==> G,phi |-JVM state' [ok]
theorem instr_correct:
[| wt_jvm_prog G phi; method (G, C) sig = Some (C, rT, maxs, maxl, ins, et);
Some state' = exec (G, Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs));
G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok] |]
==> G,phi |-JVM state' [ok]
lemma correct_state_impl_Some_method:
G,phi |-JVM Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs) [ok] ==> EX meth. method (G, C) sig = Some (C, meth)
lemma BV_correct_1:
[| wt_jvm_prog G phi; G,phi |-JVM state [ok]; exec (G, state) = Some state' |] ==> G,phi |-JVM state' [ok]
lemma L0:
[| xp = None; frs ~= [] |] ==> EX state'. exec (G, xp, hp, ihp, frs) = Some state'
lemma L1:
[| wt_jvm_prog G phi; G,phi |-JVM (xp, hp, ihp, frs) [ok]; xp = None;
frs ~= [] |]
==> EX state'.
exec (G, xp, hp, ihp, frs) = Some state' & G,phi |-JVM state' [ok]
theorem BV_correct:
[| wt_jvm_prog G phi; G |- s -jvm-> t; G,phi |-JVM s [ok] |] ==> G,phi |-JVM t [ok]
theorem BV_correct_implies_approx:
[| wt_jvm_prog G phi;
G |- s0 -jvm-> Norm (hp, ihp, (stk, loc, C, sig, pc, r) # frs);
G,phi |-JVM s0 [ok] |]
==> EX ST LT z.
((ST, LT), z) : phi C sig ! pc &
approx_stk G hp ihp stk ST & approx_loc G hp ihp loc LT
lemma
wf_prog wf_mb G ==> G |-h start_heap G [ok]
lemma
wf_prog wf_mb G ==> h_init G (start_heap G) start_iheap
lemma consistent_init_start:
consistent_init [] (Null # replicate n arbitrary) ([], OK (Init (Class C)) # replicate n Err) hp
lemma
[| wt_jvm_prog G Phi; is_class G C; method (G, C) (m, []) = Some (C, b);
m ~= init |]
==> G,Phi |-JVM start_state G C m [ok]
theorem
[| wt_jvm_prog G Phi; is_class G C; method (G, C) (m, []) = Some (C, b);
m ~= init; G |- start_state G C m -jvm-> s |]
==> G,Phi |-JVM s [ok]