Up to index of Isabelle/HOL/objinit
theory BVSpecTypeSafe = Correct:(* Title: HOL/MicroJava/BV/BVSpecTypeSafe.thy
ID: $Id: BVSpecTypeSafe.html,v 1.1 2002/11/28 14:12:09 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 sup_state_conv wt_instr_def
eff_def norm_eff_def eff_bool_def
lemmas correctE = correct_stateE2 correct_frameE
lemmas widen_rules[intro] = approx_val_widen
approx_loc_imp_approx_loc_sup
approx_stk_imp_approx_stk_sup
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
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 (auto simp add: correct_state_def)
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: "phi C sig ! pc = Some ((ST, LT),z)"
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>
G \<turnstile> Some (([Init (Class D)], LT),z) <=' phi C sig!the (?match D)"
by (simp add: wt_instr_def eff_def xcpt_eff_def) (fast dest!: bspec)
with in_any match' obtain
pc: "handler_pc < length ins"
"G \<turnstile> Some (([Init (Class D)], LT),z) <=' phi C sig ! handler_pc"
by auto
then obtain ST' LT' where
phi': "phi C sig ! handler_pc = Some ((ST',LT'),z)" and
less: "G \<turnstile> ([Init (Class D)], LT) <=s (ST',LT')"
by auto
from cr' phi meth f'
have "correct_frame G hp ihp (ST, LT) maxl ins f'"
by (unfold correct_state_def) auto
then 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 (ST', LT') maxl ins ?f"
proof -
from wf less loc
have "approx_loc G hp ihp loc LT'" by (simp add: sup_state_conv) blast
moreover
from D adr hp
have "G,hp \<turnstile> xcp ::\<preceq> Class D" by (simp add: conf_def obj_ty_def)
with init
have "G,hp,ihp \<turnstile> xcp ::\<preceq>i Init (Class D)" by (simp add: iconf_def)
with wf less loc
have "approx_stk G hp ihp [xcp] ST'"
by (auto simp add: sup_state_conv approx_stk_def approx_val_def iconf_def subtype_def
elim!: conf_widen split: Err.split init_ty.split)
moreover
note len pc phi' csi cor
ultimately
show ?thesis
apply (simp add: correct_frame_def)
apply (blast intro: consistent_init_xcp consistent_init_widen
corresponds_widen corresponds_xcp)
done
qed
with cr' match phi phi' meth
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:
"\<lbrakk> 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 \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd> \<rbrakk>
\<Longrightarrow> \<exists>adr T. xcp = Addr adr \<and> hp adr = Some T \<and> is_init hp ihp xcp"
(is "\<lbrakk> ?xcpt; ?wt; ?correct \<rbrakk> \<Longrightarrow> _")
proof -
note [simp] = split_beta raise_system_xcpt_def
note [split] = split_if_asm option.split_asm
assume wt: ?wt
assume correct: ?correct hence pre: "preallocated hp ihp" ..
assume xcpt: ?xcpt with pre 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
"phi C sig ! pc = Some ((ST, LT), z)"
"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 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
text {*
Finally we can state that the next state always conforms when an exception occured:
*}
lemma xcpt_correct:
"\<lbrakk> 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, 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 wtp: "wt_jvm_prog G phi"
assume meth: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
assume wt: "wt_instr (ins!pc) G C rT (phi C sig) maxs (fst sig=init) (length ins) et pc"
assume xp: "fst (exec_instr (ins!pc) G hp ihp stk loc C sig pc r frs) = Some xcp"
assume s': "Some state' = exec (G, None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)"
assume correct: "G,phi \<turnstile>JVM (None, hp, ihp, (stk,loc,C,sig,pc,r)#frs)\<surd>"
from wtp obtain wfmb where wf: "wf_prog wfmb G" by (simp add: wt_jvm_prog_def)
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: "phi C sig ! pc = Some ((ST,LT),z)" 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> G \<turnstile> s' <=' 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' LT' where
phi_pc': "phi C sig ! handler = Some ((ST', LT'),z)" 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
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
obtain ST' LT' where
phi': "phi C sig ! handler = Some ((ST', LT'),z)" and
less: "G \<turnstile> ([Init (Class (Xcpt OutOfMemory))], LT) <=s (ST', LT')" and
pc': "handler < length ins"
by (simp add: xcpt_eff_def match_et_imp_match) blast
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 "G,hp,ihp \<turnstile> xcp ::\<preceq>i Init (Class (Xcpt OutOfMemory))"
by (simp add: iconf_def)
moreover
from wf less loc
have "approx_loc G hp ihp loc LT'"
by (simp add: sup_state_conv) blast
moreover
from wf less cin
have "consistent_init [xcp] loc (ST',LT') ihp"
by (blast intro: consistent_init_xcp consistent_init_widen)
moreover
note wf less pc' len cor
ultimately
have "correct_frame G hp ihp (ST',LT') maxl ins ?f'"
by (unfold correct_frame_def)
(auto simp add: sup_state_conv approx_stk_def approx_val_def
split: err.split elim!: iconf_widen
intro: corresponds_xcp corresponds_widen)
}
ultimately
show ?thesis by (rule that)
next
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
obtain ST' LT' where
phi': "phi C sig ! handler = Some ((ST', LT'), z)" and
less: "G \<turnstile> ([Init (Class (Xcpt NullPointer))], LT) <=s (ST', LT')" and
pc': "handler < length ins"
by (simp add: xcpt_eff_def match_et_imp_match) blast
note phi'
moreover
{ from xcp prehp
have "G,hp,ihp \<turnstile> xcp ::\<preceq>i Init (Class (Xcpt NullPointer))"
by (auto simp add: iconf_def conf_def obj_ty_def dest!: preallocatedD)
moreover
from wf less loc
have "approx_loc G hp ihp loc LT'"
by (simp add: sup_state_conv) blast
moreover
from wf less cin
have "consistent_init [xcp] loc (ST', LT') ihp"
by (blast intro: consistent_init_xcp consistent_init_widen)
moreover
note wf less pc' len cor
ultimately
have "correct_frame G hp ihp (ST',LT') maxl ins ?f'"
by (unfold correct_frame_def)
(auto simp add: sup_state_conv approx_stk_def approx_val_def
split: err.split elim!: iconf_widen
intro: corresponds_xcp corresponds_widen)
}
ultimately
show ?thesis by (rule that)
next
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
obtain ST' LT' where
phi': "phi C sig ! handler = Some ((ST', LT'), z)" and
less: "G \<turnstile> ([Init (Class (Xcpt NullPointer))], LT) <=s (ST', LT')" and
pc': "handler < length ins"
by (simp add: xcpt_eff_def match_et_imp_match) blast
note phi'
moreover
{ from xcp prehp
have "G,hp,ihp \<turnstile> xcp ::\<preceq>i Init (Class (Xcpt NullPointer))"
by (auto simp add: iconf_def conf_def obj_ty_def dest!: preallocatedD)
moreover
from wf less loc
have "approx_loc G hp ihp loc LT'"
by (simp add: sup_state_conv) blast
moreover
from wf less cin
have "consistent_init [xcp] loc (ST', LT') ihp"
by (blast intro: consistent_init_xcp consistent_init_widen)
moreover
note wf less pc' len cor
ultimately
have "correct_frame G hp ihp (ST',LT') maxl ins ?f'"
by (unfold correct_frame_def)
(auto simp add: sup_state_conv approx_stk_def approx_val_def
split: err.split elim!: iconf_widen
intro: corresponds_xcp corresponds_widen)
}
ultimately
show ?thesis by (rule that)
next
case Checkcast
with some_handler xp'
have xcp: "xcp = Addr (XcptRef ClassCast)"
by (simp add: raise_system_xcpt_def split_beta split: split_if_asm)
with prehp have "cname_of hp xcp = Xcpt ClassCast" ..
with Checkcast some_handler phi_pc eff
obtain ST' LT' where
phi': "phi C sig ! handler = Some ((ST', LT'), z)" and
less: "G \<turnstile> ([Init (Class (Xcpt ClassCast))], LT) <=s (ST', LT')" and
pc': "handler < length ins"
by (simp add: xcpt_eff_def match_et_imp_match) blast
note phi'
moreover
{ from xcp prehp
have "G,hp,ihp \<turnstile> xcp ::\<preceq>i Init (Class (Xcpt ClassCast))"
by (auto simp add: iconf_def conf_def obj_ty_def dest!: preallocatedD)
moreover
from wf less loc
have "approx_loc G hp ihp loc LT'"
by (simp add: sup_state_conv) blast
moreover
from wf less cin
have "consistent_init [xcp] loc (ST', LT') ihp"
by (blast intro: consistent_init_xcp consistent_init_widen)
moreover
note wf less pc' len cor
ultimately
have "correct_frame G hp ihp (ST',LT') maxl ins ?f'"
by (unfold correct_frame_def)
(auto simp add: sup_state_conv approx_stk_def approx_val_def
split: err.split elim!: iconf_widen
intro: corresponds_xcp corresponds_widen)
}
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> G \<turnstile> Some (([Init (Class D)], LT),z) <=' phi C sig!the (?m D)"
by (simp add: xcpt_eff_def)
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
obtain
pc': "handler < length ins" and
"G \<turnstile> Some (([Init (Class D)], LT), z) <=' phi C sig ! handler"
by auto
then
obtain ST' LT' where
phi': "phi C sig ! handler = Some ((ST', LT'), z)" and
less: "G \<turnstile> ([Init (Class D)], LT) <=s (ST', LT')"
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 "G,hp,ihp \<turnstile> xcp ::\<preceq>i Init (Class D)"
by (simp add: iconf_def conf_def obj_ty_def)
moreover
from wf less loc
have "approx_loc G hp ihp loc LT'"
by (simp add: sup_state_conv) blast
moreover
from wf less cin
have "consistent_init [xcp] loc (ST', LT') ihp"
by (blast intro: consistent_init_xcp consistent_init_widen)
moreover
note wf less pc' len cor
ultimately
have "correct_frame G hp ihp (ST',LT') maxl ins ?f'"
by (unfold correct_frame_def)
(auto simp add: sup_state_conv approx_stk_def approx_val_def
split: err.split elim!: iconf_widen
intro: corresponds_xcp corresponds_widen)
}
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> G \<turnstile> Some (([Init (Class D)], LT),z) <=' phi C sig!the (?m D)"
by (simp add: xcpt_eff_def)
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
obtain
pc': "handler < length ins" and
"G \<turnstile> Some (([Init (Class D)], LT), z) <=' phi C sig ! handler"
by auto
then
obtain ST' LT' where
phi': "phi C sig ! handler = Some ((ST', LT'), z)" and
less: "G \<turnstile> ([Init (Class D)], LT) <=s (ST', LT')"
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 "G,hp,ihp \<turnstile> xcp ::\<preceq>i Init (Class D)"
by (simp add: iconf_def conf_def obj_ty_def)
moreover
from wf less loc
have "approx_loc G hp ihp loc LT'"
by (simp add: sup_state_conv) blast
moreover
from wf less cin
have "consistent_init [xcp] loc (ST', LT') ihp"
by (blast intro: consistent_init_xcp consistent_init_widen)
moreover
note wf less pc' len cor
ultimately
have "correct_frame G hp ihp (ST',LT') maxl ins ?f'"
by (unfold correct_frame_def)
(auto simp add: sup_state_conv approx_stk_def approx_val_def
split: err.split elim!: iconf_widen
intro: corresponds_xcp corresponds_widen)
}
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> G \<turnstile> Some (([Init (Class D)], LT), z) <=' phi C sig!the (?m D)"
by (simp add: xcpt_eff_def)
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
obtain
pc': "handler < length ins" and
"G \<turnstile> Some (([Init (Class D)], LT), z) <=' phi C sig ! handler"
by auto
then
obtain ST' LT' where
phi': "phi C sig ! handler = Some ((ST', LT'), z)" and
less: "G \<turnstile> ([Init (Class D)], LT) <=s (ST', LT')"
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 "G,hp,ihp \<turnstile> xcp ::\<preceq>i Init (Class D)"
by (simp add: iconf_def conf_def obj_ty_def)
moreover
from wf less loc
have "approx_loc G hp ihp loc LT'"
by (simp add: sup_state_conv) blast
moreover
note wf less pc' len
from wf less cin
have "consistent_init [xcp] loc (ST', LT') ihp"
by (blast intro: consistent_init_xcp consistent_init_widen)
moreover
note wf less pc' len cor
ultimately
have "correct_frame G hp ihp (ST',LT') maxl ins ?f'"
by (unfold correct_frame_def)
(auto simp add: sup_state_conv approx_stk_def approx_val_def
split: err.split elim!: iconf_widen
intro: corresponds_xcp corresponds_widen)
}
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 (rule conjI)
apply (rule approx_loc_imp_approx_val_sup)
apply simp+
apply (rule conjI)
apply (blast intro: approx_stk_imp_approx_stk_sup
approx_loc_imp_approx_loc_sup)
apply (rule conjI)
apply (blast intro: approx_stk_imp_approx_stk_sup
approx_loc_imp_approx_loc_sup)
apply (rule conjI)
apply (drule consistent_init_loc_nth)
apply assumption+
apply (erule consistent_init_widen_split)
apply simp
apply blast
apply assumption
apply (rule impI, erule impE, assumption, elim exE conjE)
apply (simp add: corresponds_stk_cons)
apply (frule corresponds_loc_nth)
apply assumption
apply assumption
apply (rule conjI)
apply (rule impI)
apply (simp add: init_le_PartInit2)
apply (blast intro: corresponds_widen_split)
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 (blast intro: approx_stk_imp_approx_stk_sup
approx_loc_imp_approx_loc_subst
approx_loc_imp_approx_loc_sup
consistent_init_store
consistent_init_widen_split
corresponds_widen_split
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
sup_PTS_eq map_eq_Cons)
apply (rule conjI)
apply (blast dest: conf_litval intro: conf_widen)
apply (rule conjI)
apply (clarsimp simp add: is_init_def split: val.split)
apply (rule conjI)
apply (blast dest: approx_stk_imp_approx_stk_sup)
apply (rule conjI)
apply (blast dest: approx_loc_imp_approx_loc_sup)
apply (rule conjI)
apply (drule consistent_init_Init_stk)
apply (erule consistent_init_widen_split)
apply (simp add: subtype_def)
apply blast
apply assumption
apply (rule impI, erule impE, assumption, elim conjE exE)
apply (simp add: corresponds_stk_cons)
apply (blast intro: corresponds_widen_split)
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 (rule conjI)
apply (clarsimp simp add: iconf_def init_le_Init)
apply (blast intro: Cast_conf2)
apply (rule conjI)
apply (erule approx_stk_imp_approx_stk_sup)
apply assumption+
apply (rule conjI)
apply (erule approx_loc_imp_approx_loc_sup)
apply assumption+
apply (rule conjI)
apply (drule consistent_init_pop)
apply (drule consistent_init_widen_split)
apply assumption+
apply (clarsimp simp add: init_le_Init)
apply (erule consistent_init_Init_stk)
apply (clarsimp simp add: init_le_Init corresponds_stk_cons)
apply (blast intro: corresponds_widen_split)
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
split: option.split split_if_asm)
apply (frule conf_widen)
apply assumption+
apply (drule conf_RefTD)
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 (elim exE conjE)
apply simp
apply (erule conf_widen, assumption+)
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: approx_stk_imp_approx_stk_sup
approx_loc_imp_approx_loc_sup
consistent_init_Init_stk
consistent_init_pop
consistent_init_widen_split
corresponds_widen_split)
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: "phi C sig!pc = Some ((ST,LT),z)" 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: "phi C sig ! Suc pc = Some ((ST',LT'),z)" and
less: "G \<turnstile> (tST, LT) <=s (ST', LT')" 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)"
by (unfold wt_instr_def eff_def eff_bool_def norm_eff_def)
(clarsimp simp add: init_le_Init2, blast)
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 simp add: subtype_def 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 simp add: subtype_def
dest: widen_RefT2 conf_RefTD)
with o_less
have C': "G \<turnstile> C' \<preceq>C D"
by (auto simp add: subtype_def 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 less 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 less have "consistent_init stk' loc (ST', LT') ihp"
by (blast intro: consistent_init_pop consistent_init_widen)
with wf app_l app_s len_l suc_pc less hext corr'
have f'_correct:
"correct_frame G ?hp' ihp (ST', LT') maxl ins (stk',loc,C,sig,Suc pc,r)"
by (simp add: correct_frame_def sup_state_conv)
(blast intro: approx_stk_imp_approx_stk_sup_heap
approx_stk_imp_approx_stk_sup
approx_loc_imp_approx_loc_sup_heap
approx_loc_imp_approx_loc_sup
corresponds_widen_split)
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: "phi C sig!pc = Some ((ST,LT),z)" 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 ST' LT' where
is_class_X: "is_class G X" and
maxs: "length ST < maxs" and
suc_pc: "Suc pc < length ins" and
phi_suc: "phi C sig ! Suc pc = Some ((ST', LT'),z)" and
new_type: "UnInit X pc \<notin> set ST" and
less: "G \<turnstile> (UnInit X pc#ST, replace (OK (UnInit X pc)) Err LT) <=s (ST', LT')"
(is "G \<turnstile> (_,?LT) <=s (ST',LT')")
by (unfold wt_instr_def eff_def eff_bool_def norm_eff_def) auto
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 (UnInit X pc#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 (UnInit X pc#ST,?LT) ?ihp'"
by (blast intro: consistent_init_newref consistent_init_replace_Err)
from this less have "consistent_init (Addr oref # stk) loc (ST',LT') ?ihp'"
by (rule consistent_init_widen)
with hp frame less suc_pc wf corr' a_loc'
have "correct_frame G ?hp' ?ihp' (ST', LT') maxl ins ?f"
apply (unfold correct_frame_def sup_state_conv)
apply (clarsimp simp add: map_eq_Cons conf_def blank_def
corresponds_stk_cons)
apply (insert sup, unfold blank_def)
apply (blast intro: corresponds_widen_split
approx_stk_imp_approx_stk_sup
approx_stk_newref
approx_stk_imp_approx_stk_sup_heap
approx_loc_imp_approx_loc_sup_heap
approx_loc_imp_approx_loc_sup
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 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: "phi C sig!pc = Some (s,z)" 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: "G \<turnstile> norm_eff (Invoke C' mn pTs) G pc (Some (s,z)) <=' phi C sig!Suc pc" and
X: "G \<turnstile> X \<preceq>i Init (Class C')" and
ni: "mn \<noteq> init"
by (simp add: wt_instr_def eff_def) blast
from eff obtain ST' LT' z' where
s': "phi C sig ! Suc pc = Some ((ST',LT'),z')"
by (simp add: norm_eff_def split_paired_Ex) fast
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)
then obtain LT0 z0 where
LT0: "phi D'' (mn, pTs) ! 0 = Some (([], LT0),z0)"
by (clarsimp simp add: wt_start_def sup_state_conv)
have c_f: "correct_frame G hp ihp ([], LT0) mxl' ins' ?f"
proof -
let ?T = "OK (Init (Class D''))"
from ni start LT0 have sup_loc:
"G \<turnstile> (?T # map OK (map Init pTs) @ replicate mxl' Err) <=l LT0"
(is "G \<turnstile> ?LT <=l LT0")
by (simp add: wt_start_def sup_state_conv)
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 "approx_loc G hp ihp ?loc' ?LT"
by (auto simp add: approx_loc_append approx_stk_def)
from wfprog this sup_loc have loc: "approx_loc G hp ihp ?loc' LT0"
by (rule approx_loc_imp_approx_loc_sup)
from l l_o have "length pTs = length opTs" by auto
hence "consistent_init [] ?loc' ([],?LT) ihp"
by (blast intro: consistent_init_start)
with sup_loc have "consistent_init [] ?loc' ([],LT0) ihp"
by (auto intro: consistent_init_widen_split)
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 add: subtype_def) (drule subtype_widen_methd, assumption+, blast)
with X' state'_val heap_ok mD'' ins method phi_pc s l
frames s' LT0 c_f frame is_class_C ni init_ok prealloc
show "G,phi \<turnstile>JVM state'\<surd>"
apply simp
apply (rule correct_stateI, assumption+)
apply clarsimp
apply (intro exI conjI impI)
apply (rule refl)
apply blast
apply assumption
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: "phi C sig!pc = Some (s,z)" 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: "G \<turnstile> norm_eff (Invoke_special C' mn pTs) G pc (Some (s,z))
<='
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"
by (simp add: wt_instr_def split_paired_Ex eff_def) blast
from s eff obtain ST' LT' z' where
s': "phi C sig ! Suc pc = Some ((ST',LT'),z')"
by (clarsimp simp add: norm_eff_def) blast
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)
then obtain LT0 where
LT0: "phi C' (mn, pTs) ! 0 = Some (([], LT0),C'=Object)"
by (clarsimp simp add: wt_start_def sup_state_conv)
let ?T = "OK (if C' \<noteq> Object then PartInit C' else Init (Class C'))"
from start LT0 is_init
have sup_loc:
"G \<turnstile> (?T # map OK (map Init pTs) @ replicate mxl' Err) <=l LT0"
(is "G \<turnstile> ?LT <=l LT0")
by (simp add: wt_start_def sup_state_conv)
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 "approx_loc G ?hp' ?ihp' ?loc' ?LT"
by (auto simp add: approx_loc_append)
from wfprog this sup_loc
have loc: "approx_loc G ?hp' ?ihp' ?loc' LT0"
by (rule approx_loc_imp_approx_loc_sup)
from new_Addr new_ref' l_o l have
"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 blast
apply (drule in_set_replicateD)
apply assumption
apply simp
apply blast
done
with sup_loc have corr':
"corresponds [] ?loc' ([], LT0) ?ihp' (Addr ref') (PartInit C')"
by (fastsimp elim: corresponds_widen_split)
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' ([], ?LT) ?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 sup_loc have "consistent_init [] ?loc' ([], LT0) ?ihp'"
by (auto intro: consistent_init_widen_split)
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 s' 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 (rule refl)
apply assumption
apply (simp add: oX_pos oX_Addr hp_Some neq_ref)
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: "phi C sig ! pc = Some (s, z)" 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" and
pc: "pc < length ins"
by (simp add: wt_instr_def eff_def eff_bool_def norm_eff_def) blast
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)"
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: "phi C0 sig0 ! pc0 = Some ((rev apTs @ T0 # ST0, LT0), z0)" 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 ( (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 ST'' LT'' where
Suc_pc0: "Suc pc0 < length ins0" and
phi_Suc_pc0: "phi C0 sig0 ! Suc pc0 = Some ((ST'',LT''),z0)" and
T0: "G \<turnstile> T0 \<preceq>i Init (Class C')" and
less: "G \<turnstile> (Init rT' # ST0, LT0) <=s (ST'',LT'')"
apply (simp add: wt_instr_def)
apply (erule disjE)
apply (simp add: eff_def eff_bool_def norm_eff_def)
apply (elim exE conjE)
apply (rotate_tac -7) (* fixme *)
apply clarsimp
apply blast
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 (ST'',LT'') maxl0 ins0 ?f'"
apply (simp add: correct_frame_def)
apply (insert less)
apply (clarsimp simp add: sup_state_conv map_eq_Cons)
apply (rule conjI)
apply (rule approx_val_widen, assumption+)
apply (rule conjI)
apply (rule approx_stk_imp_approx_stk_sup, assumption+)
apply (rule conjI)
apply (rule approx_loc_imp_approx_loc_sup, assumption+)
apply (rule conjI)
apply (rule consistent_init_widen_split, assumption)
apply simp
apply blast
apply assumption
apply (rule impI, erule impE, assumption, erule conjE)
apply (rule corresponds_widen_split, assumption)
apply simp
apply blast
apply assumption
apply blast
done
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)
}
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: "phi C sig ! pc = Some (s, z)" 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" and
pc: "pc < length ins"
by (simp add: wt_instr_def eff_def eff_bool_def norm_eff_def) blast
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: "phi C0 sig0 ! pc0 = Some ((rev apTs @ T0 # ST0, LT0), z0)" 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 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 ST'' LT'' where
Suc_pc0: "Suc pc0 < length ins0" and
phi_Suc_pc0: "phi C0 sig0 ! Suc pc0 = Some ((ST'',LT''),?z')" and
T0: "(\<exists>pc. T0 = UnInit C' pc) \<or>
(T0 = PartInit C0 \<and> G \<turnstile> C0 \<prec>C1 C' \<and> ¬z0)" and
less: "G \<turnstile> (?ST', ?LT') <=s (ST'',LT'')"
apply (simp add: wt_instr_def)
apply (erule disjE)
apply simp
apply (simp add: eff_def eff_bool_def norm_eff_def)
apply (elim exE conjE)
apply (clarsimp simp add: nth_append)
apply blast
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 - (drule approx_stk_append_lemma, auto)
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 "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 this less
have cons':
"consistent_init ?stk' ?loc' (ST'',LT'') ihp"
by (rule consistent_init_widen)
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
"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
with less
have corr':
"fst sig0 = init \<longrightarrow>
corresponds ?stk' ?loc' (ST'', LT'') ihp (fst r0) (PartInit C0)"
apply -
apply (rule impI, erule impE, assumption)
apply (rule corresponds_widen)
apply assumption+
apply blast
done
have fst_r': "fst ?r' = fst r0" by simp
from lenloc0 a_loc' Suc_pc0 a_stk' cons' less 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: sup_state_conv map_eq_Cons split del: split_if)
apply (rule conjI)
apply (rule approx_val_widen, assumption+)
apply (rule conjI)
apply (rule approx_stk_imp_approx_stk_sup, assumption+)
apply (rule approx_loc_imp_approx_loc_sup, assumption+)
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
apply assumption
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 assumption
apply assumption
apply (rule impI, erule impE, assumption)
apply (rule constructor_ok_pass_val)
apply assumption
apply simp
apply simp
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) simp
}
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 (fast intro: approx_loc_imp_approx_loc_sup
approx_stk_imp_approx_stk_sup
consistent_init_widen_split
corresponds_widen_split)
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 (rule conjI)
apply (rule impI)
apply simp
apply (rule conjI)
apply (rule approx_stk_imp_approx_stk_sup, assumption+)
apply (rule conjI)
apply (erule approx_loc_imp_approx_loc_sup, assumption+)
apply (rule conjI)
apply (drule consistent_init_pop)+
apply (erule consistent_init_widen_split, assumption+)
apply (rule impI, erule impE, assumption, erule conjE)
apply (drule corresponds_pop)+
apply (fast elim!: corresponds_widen_split)
apply (rule impI)
apply (rule conjI)
apply (rule approx_stk_imp_approx_stk_sup, assumption+)
apply (rule conjI)
apply (erule approx_loc_imp_approx_loc_sup, assumption+)
apply (rule conjI)
apply (drule consistent_init_pop)+
apply (erule consistent_init_widen_split, assumption+)
apply (rule impI, erule impE, assumption, erule conjE)
apply (drule corresponds_pop)+
apply (fast elim!: corresponds_widen_split)
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 (fast intro: approx_loc_imp_approx_loc_sup
approx_stk_imp_approx_stk_sup
elim: consistent_init_widen_split
corresponds_widen_split
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 (rule conjI)
apply (erule approx_val_imp_approx_val_sup, assumption+)
apply simp
apply (rule conjI)
apply (erule approx_val_imp_approx_val_sup, assumption+)
apply simp
apply (rule conjI)
apply (blast intro: approx_stk_imp_approx_stk_sup)
apply (rule conjI)
apply (blast intro: approx_loc_imp_approx_loc_sup)
apply (rule conjI)
apply (drule consistent_init_Dup)
apply (rule consistent_init_widen_split)
apply assumption
prefer 2
apply assumption
apply simp
apply (rule impI, erule impE, assumption, erule conjE)
apply (drule corresponds_Dup)
apply (erule corresponds_widen_split)
prefer 2
apply assumption
apply simp
apply blast
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 (rule conjI)
apply (erule approx_val_imp_approx_val_sup, assumption+)
apply simp
apply (rule conjI)
apply (erule approx_val_imp_approx_val_sup, assumption+)
apply simp
apply (rule conjI)
apply (erule approx_val_imp_approx_val_sup, assumption+)
apply simp
apply (rule conjI)
apply (blast intro: approx_stk_imp_approx_stk_sup)
apply (rule conjI)
apply (blast intro: approx_loc_imp_approx_loc_sup)
apply (rule conjI)
apply (drule consistent_init_Dup_x1)
apply (rule consistent_init_widen_split)
apply assumption
prefer 2
apply assumption
apply simp
apply (rule impI, erule impE, assumption, erule conjE)
apply (drule corresponds_Dup_x1)
apply (erule corresponds_widen_split)
prefer 2
apply assumption
apply simp
apply blast
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 (rule conjI)
apply (erule approx_val_imp_approx_val_sup, assumption+)
apply simp
apply (rule conjI)
apply (erule approx_val_imp_approx_val_sup, assumption+)
apply simp
apply (rule conjI)
apply (erule approx_val_imp_approx_val_sup, assumption+)
apply simp
apply (rule conjI)
apply (erule approx_val_imp_approx_val_sup, assumption+)
apply simp
apply (rule conjI)
apply (blast intro: approx_stk_imp_approx_stk_sup)
apply (rule conjI)
apply (blast intro: approx_loc_imp_approx_loc_sup)
apply (rule conjI)
apply (drule consistent_init_Dup_x2)
apply (rule consistent_init_widen_split)
apply assumption
prefer 2
apply assumption
apply simp
apply (rule impI, erule impE, assumption, erule conjE)
apply (drule corresponds_Dup_x2)
apply (erule corresponds_widen_split)
prefer 2
apply assumption
apply simp
apply blast
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 (rule conjI)
apply (erule approx_val_imp_approx_val_sup, assumption+)
apply simp
apply (rule conjI)
apply (erule approx_val_imp_approx_val_sup, assumption+)
apply simp
apply (rule conjI)
apply (blast intro: approx_stk_imp_approx_stk_sup)
apply (rule conjI)
apply (blast intro: approx_loc_imp_approx_loc_sup)
apply (rule conjI)
apply (drule consistent_init_Swap)
apply (rule consistent_init_widen_split)
apply assumption
prefer 2
apply assumption
apply simp
apply (rule impI, erule impE, assumption, erule conjE)
apply (drule corresponds_Swap)
apply (erule corresponds_widen_split)
prefer 2
apply assumption
apply simp
apply blast
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 approx_val_def)
apply (clarsimp simp add: 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: approx_stk_imp_approx_stk_sup
approx_val_imp_approx_val_sup
approx_loc_imp_approx_loc_sup
corresponds_widen_split
consistent_init_Init_stk
consistent_init_widen_split)
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
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 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+)
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. (phi C sig) ! pc = Some ((ST,LT),z) \<and>
approx_stk G hp ihp stk ST \<and>
approx_loc G hp ihp loc LT"
apply (drule BV_correct)
apply assumption+
apply (simp add: correct_state_def correct_frame_def split_def
split: option.splits)
apply (case_tac s)
apply simp
apply (case_tac s)
apply simp
done
lemma
fixes G :: jvm_prog ("\<Gamma>")
assumes wf: "wf_prog wf_mb \<Gamma>"
shows hconf_start: "\<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
fixes G :: jvm_prog ("\<Gamma>")
assumes wf: "wf_prog wf_mb \<Gamma>"
shows hinit_start: "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:
"G \<turnstile> OK (Init (Class C)) <=o X \<Longrightarrow>
consistent_init [] (Null#replicate n arbitrary) ([], X#replicate n Err) hp"
apply (induct n)
apply (auto simp add: consistent_init_def corresponds_def corr_stk_def corr_loc_def)
done
lemma
fixes G :: jvm_prog ("\<Gamma>") and Phi :: prog_type ("\<Phi>")
shows BV_correct_initial:
"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 sup_state_conv)
defer
apply (clarsimp simp add: sup_state_conv dest!: loc_widen_Err)
apply (simp add: consistent_init_start)
apply (auto simp add: sup_state_conv approx_val_def iconf_def
is_init_def subtype_def dest!: widen_RefT
split: err.splits split_if_asm init_ty.split)
done
theorem
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 typesafe:
"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) &
phi C sig ! pc = Some (s, z) &
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
G |- s1 <=s s2 == G |- map OK (fst s1) <=l map OK (fst s2) & G |- snd s1 <=l snd s2
wt_instr i G C rT phi mxs ini max_pc et pc ==
app i G C pc mxs rT ini et (phi ! pc) &
(ALL (pc', s'):set (eff i G pc et (phi ! pc)).
pc' < max_pc & G |- s' <=' phi ! pc')
eff i G pc et s == map (%pc'. (pc', norm_eff i G pc s)) (succs i pc) @ xcpt_eff i G pc s et
norm_eff i G pc == option_map (eff_bool i G pc)
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;
phi C sig ! pc = Some ((ST, LT), z);
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 widen_rules:
[| wf_prog wt G; approx_val G hp ihp v (OK T); G |- T <=i T' |] ==> approx_val G hp ihp v (OK T')
[| wf_prog wt G; approx_loc G hp ihp lvars lt; G |- lt <=l lt' |] ==> approx_loc G hp ihp lvars lt'
[| wf_prog wt G; approx_stk G hp ihp lvars st; G |- map OK st <=l map OK st' |] ==> approx_stk G hp ihp lvars st'
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 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 exec_instr_xcpt_hp:
[| 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 xcpt_correct:
[| 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) &
phi C sig ! pc = Some (s, z) &
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
G |- s1 <=s s2 == G |- map OK (fst s1) <=l map OK (fst s2) & G |- snd s1 <=l snd s2
wt_instr i G C rT phi mxs ini max_pc et pc ==
app i G C pc mxs rT ini et (phi ! pc) &
(ALL (pc', s'):set (eff i G pc et (phi ! pc)).
pc' < max_pc & G |- s' <=' phi ! pc')
eff i G pc et s == map (%pc'. (pc', norm_eff i G pc s)) (succs i pc) @ xcpt_eff i G pc s et
norm_eff i G pc == option_map (eff_bool i G pc)
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 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]
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.
phi C sig ! pc = Some ((ST, LT), z) &
approx_stk G hp ihp stk ST & approx_loc G hp ihp loc LT
lemma hconf_start:
wf_prog wf_mb G ==> G |-h start_heap G [ok]
lemma hinit_start:
wf_prog wf_mb G ==> h_init G (start_heap G) start_iheap
lemma consistent_init_start:
G |- OK (Init (Class C)) <=o X
==> consistent_init [] (Null # replicate n arbitrary) ([], X # replicate n Err)
hp
lemma BV_correct_initial:
[| 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 typesafe:
[| 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]