Theory BVSpecTypeSafe
section ‹ BV Type Safety Proof \label{sec:BVSpecTypeSafe} ›
theory BVSpecTypeSafe
imports BVConform StartProg
begin
text ‹
This theory contains proof that the specification of the bytecode
verifier only admits type safe programs.
›
subsection ‹ Preliminaries ›
text ‹
Simp and intro setup for the type safety proof:
›
lemmas defs1 = correct_state_def conf_f_def wt_instr_def eff_def norm_eff_def app_def xcpt_app_def
lemmas widen_rules [intro] = conf_widen confT_widen confs_widens confTs_widen
subsection ‹ Exception Handling ›
text ‹
For the @{text Invoke} instruction the BV has checked all handlers
that guard the current @{text pc}.
›
lemma Invoke_handlers:
"match_ex_table P C pc xt = Some (pc',d') ⟹
∃(f,t,D,h,d) ∈ set (relevant_entries P (Invoke n M) pc xt).
P ⊢ C ≼⇧* D ∧ pc ∈ {f..<t} ∧ pc' = h ∧ d' = d"
by (induct xt) (auto simp: relevant_entries_def matches_ex_entry_def
is_relevant_entry_def split: if_split_asm)
text ‹
For the @{text Invokestatic} instruction the BV has checked all handlers
that guard the current @{text pc}.
›
lemma Invokestatic_handlers:
"match_ex_table P C pc xt = Some (pc',d') ⟹
∃(f,t,D,h,d) ∈ set (relevant_entries P (Invokestatic C⇩0 n M) pc xt).
P ⊢ C ≼⇧* D ∧ pc ∈ {f..<t} ∧ pc' = h ∧ d' = d"
by (induct xt) (auto simp: relevant_entries_def matches_ex_entry_def
is_relevant_entry_def split: if_split_asm)
text ‹
For the instrs in @{text Called_set} the BV has checked all handlers
that guard the current @{text pc}.
›
lemma Called_set_handlers:
"match_ex_table P C pc xt = Some (pc',d') ⟹ i ∈ Called_set ⟹
∃(f,t,D,h,d) ∈ set (relevant_entries P i pc xt).
P ⊢ C ≼⇧* D ∧ pc ∈ {f..<t} ∧ pc' = h ∧ d' = d"
by (induct xt) (auto simp: relevant_entries_def matches_ex_entry_def
is_relevant_entry_def split: if_split_asm)
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
heap address, and that the state before the exception occurred
conforms.
›
lemma uncaught_xcpt_correct:
assumes wt: "wf_jvm_prog⇘Φ⇙ P"
assumes h: "h xcp = Some obj"
shows "⋀f. P,Φ ⊢ (None, h, f#frs, sh)√
⟹ curr_method f ≠ clinit ⟹ P,Φ ⊢ find_handler P xcp h frs sh √"
(is "⋀f. ?correct (None, h, f#frs, sh) ⟹ ?prem f ⟹ ?correct (?find frs)")
proof (induct frs)
show "?correct (?find [])" by (simp add: correct_state_def)
next
from wt obtain mb where wf: "wf_prog mb P" by (simp add: wf_jvm_prog_phi_def)
fix f f' frs' assume cr: "?correct (None, h, f#f'#frs', sh)"
assume pr: "?prem f"
assume IH: "⋀f. ?correct (None, h, f#frs', sh) ⟹ ?prem f ⟹ ?correct (?find frs')"
from cr pr conf_clinit_Cons[where frs="f'#frs'" and f=f] obtain
confc: "conf_clinit P sh (f'#frs')"
and cr': "?correct (None, h, f'#frs', sh)" by(fastforce simp: correct_state_def)
obtain stk loc C M pc ics where [simp]: "f' = (stk,loc,C,M,pc,ics)" by (cases f')
from cr' obtain b Ts T mxs mxl⇩0 ins xt where
meth: "P ⊢ C sees M,b:Ts → T = (mxs,mxl⇩0,ins,xt) in C"
by (simp add: correct_state_def, blast)
hence xt[simp]: "ex_table_of P C M = xt" by simp
have cls: "is_class P C" by(rule sees_method_is_class'[OF meth])
from cr' obtain sfs where
sfs: "M = clinit ⟹ sh C = Some(sfs,Processing)" by(fastforce simp: defs1 conf_clinit_def)
show "?correct (?find (f'#frs'))"
proof (cases "match_ex_table P (cname_of h xcp) pc xt")
case None with cr' IH[of f'] show ?thesis
proof(cases "M=clinit")
case True then show ?thesis using xt cr' IH[of f'] None h conf_clinit_Called_Throwing
conf_f_Throwing[where h=h and sh=sh, OF _ cls h sfs]
by(cases frs', auto simp: correct_state_def image_iff) fastforce
qed(auto)
next
fix pc_d
assume "match_ex_table P (cname_of h xcp) pc xt = Some pc_d"
then obtain pc' d' where
match: "match_ex_table P (cname_of h xcp) pc xt = Some (pc',d')"
(is "?match (cname_of h xcp) = _")
by (cases pc_d) auto
from wt meth cr' [simplified]
have wti: "P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M"
by (fastforce simp: correct_state_def conf_f_def
dest: sees_method_fun
elim!: wt_jvm_prog_impl_wt_instr)
from cr' obtain ST LT where Φ: "Φ C M ! pc = Some (ST, LT)"
by(fastforce dest: sees_method_fun simp: correct_state_def)
from cr' Φ meth have conf': "conf_f P h sh (ST, LT) ins f'"
by (unfold correct_state_def) (fastforce dest: sees_method_fun)
hence loc: "P,h ⊢ loc [:≤⇩⊤] LT" and
stk: "P,h ⊢ stk [:≤] ST" by (unfold conf_f_def) auto
hence [simp]: "size stk = size ST" by (simp add: list_all2_lengthD)
from cr meth pr
obtain D n M' where
ins: "ins!pc = Invoke n M' ∨ ins!pc = Invokestatic D n M'" (is "_ = ?i ∨ _ = ?i'")
by(fastforce dest: sees_method_fun simp: correct_state_def)
with match obtain f1 t D where
rel: "(f1,t,D,pc',d') ∈ set (relevant_entries P (ins!pc) pc xt)" and
D: "P ⊢ cname_of h xcp ≼⇧* D"
by(fastforce dest: Invoke_handlers Invokestatic_handlers)
from rel have
"(pc', Some (Class D # drop (size ST - d') ST, LT)) ∈ set (xcpt_eff (ins!pc) P pc (ST,LT) xt)"
(is "(_, Some (?ST',_)) ∈ _")
by (force simp: xcpt_eff_def image_def)
with wti Φ obtain
pc: "pc' < size ins" and
"P ⊢ Some (?ST', LT) ≤' Φ C M ! pc'"
by (clarsimp simp: defs1) blast
then obtain ST' LT' where
Φ': "Φ C M ! pc' = Some (ST',LT')" and
less: "P ⊢ (?ST', LT) ≤⇩i (ST',LT')"
by (auto simp: sup_state_opt_any_Some)
let ?f = "(Addr xcp # drop (length stk - d') stk, loc, C, M, pc',No_ics)"
have "conf_f P h sh (ST',LT') ins ?f"
proof -
from wf less loc have "P,h ⊢ loc [:≤⇩⊤] LT'" by simp blast
moreover from D h have "P,h ⊢ Addr xcp :≤ Class D"
by (simp add: conf_def obj_ty_def case_prod_unfold)
with less stk
have "P,h ⊢ Addr xcp # drop (length stk - d') stk [:≤] ST'"
by (auto intro!: list_all2_dropI)
ultimately show ?thesis using pc conf' by(auto simp: conf_f_def)
qed
with cr' match Φ' meth pc
show ?thesis by (unfold correct_state_def)
(cases "M=clinit"; fastforce dest: sees_method_fun simp: conf_clinit_def distinct_clinit_def)
qed
qed
text ‹
The requirement of lemma @{text uncaught_xcpt_correct} (that
the exception is a valid reference on the heap) is always met
for welltyped instructions and conformant states:
›
lemma exec_instr_xcpt_h:
"⟦ fst (exec_instr (ins!pc) P h stk vars C M pc ics frs sh) = Some xcp;
P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M;
P,Φ ⊢ (None, h, (stk,loc,C,M,pc,ics)#frs, sh)√ ⟧
⟹ ∃obj. h xcp = Some obj"
(is "⟦ ?xcpt; ?wt; ?correct ⟧ ⟹ ?thesis")
proof -
note [simp] = split_beta
note [split] = if_split_asm option.split_asm
assume wt: ?wt ?correct
hence pre: "preallocated h" by (simp add: correct_state_def hconf_def)
assume xcpt: ?xcpt
with exec_instr_xcpts have
opt: "ins!pc = Throw ∨ xcp ∈ {a. ∃x ∈ sys_xcpts. a = addr_of_sys_xcpt x}" by simp
with pre show ?thesis
proof (cases "ins!pc")
case Throw with xcpt wt pre show ?thesis
by (clarsimp iff: list_all2_Cons2 simp: defs1)
(auto dest: non_npD simp: is_refT_def elim: preallocatedE)
qed (auto elim: preallocatedE)
qed
lemma exec_step_xcpt_h:
assumes xcpt: "fst (exec_step P h stk vars C M pc ics frs sh) = Some xcp"
and ins: "instrs_of P C M = ins"
and wti: "P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M"
and correct: "P,Φ ⊢ (None, h, (stk,loc,C,M,pc,ics)#frs, sh)√"
shows "∃obj. h xcp = Some obj"
proof -
from correct have pre: "preallocated h" by(simp add: defs1 hconf_def)
{ fix C' Cs assume ics[simp]: "ics = Calling C' Cs"
with xcpt have "xcp = addr_of_sys_xcpt NoClassDefFoundError"
by(cases ics, auto simp: split_beta split: init_state.splits if_split_asm)
with pre have ?thesis using preallocated_def by force
}
moreover
{ fix Cs a assume [simp]: "ics = Throwing Cs a"
with xcpt have eq: "a = xcp" by(cases Cs; simp)
from correct have "P,h,sh ⊢⇩i (C,M,pc,ics)" by(auto simp: defs1)
with eq have ?thesis by simp
}
moreover
{ fix Cs assume ics: "ics = No_ics ∨ ics = Called Cs"
with exec_instr_xcpt_h[OF _ wti correct] xcpt ins have ?thesis by(cases Cs, auto)
}
ultimately show ?thesis by(cases ics, auto)
qed
lemma conf_sys_xcpt:
"⟦preallocated h; C ∈ sys_xcpts⟧ ⟹ P,h ⊢ Addr (addr_of_sys_xcpt C) :≤ Class C"
by (auto elim: preallocatedE)
lemma match_ex_table_SomeD:
"match_ex_table P C pc xt = Some (pc',d') ⟹
∃(f,t,D,h,d) ∈ set xt. matches_ex_entry P C pc (f,t,D,h,d) ∧ h = pc' ∧ d=d'"
by (induct xt) (auto split: if_split_asm)
text ‹
Finally we can state that, whenever an exception occurs, the
next state always conforms:
›
lemma xcpt_correct:
fixes σ' :: jvm_state
assumes wtp: "wf_jvm_prog⇘Φ⇙ P"
assumes meth: "P ⊢ C sees M,b:Ts→T=(mxs,mxl⇩0,ins,xt) in C"
assumes wt: "P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M"
assumes xp: "fst (exec_step P h stk loc C M pc ics frs sh) = Some xcp"
assumes s': "Some σ' = exec (P, None, h, (stk,loc,C,M,pc,ics)#frs, sh)"
assumes correct: "P,Φ ⊢ (None, h, (stk,loc,C,M,pc,ics)#frs, sh)√"
shows "P,Φ ⊢ σ'√"
proof -
from wtp obtain wfmb where wf: "wf_prog wfmb P"
by (simp add: wf_jvm_prog_phi_def)
from meth have ins[simp]: "instrs_of P C M = ins" by simp
have cls: "is_class P C" by(rule sees_method_is_class[OF meth])
from correct obtain sfs where
sfs: "M = clinit ⟹ sh C = Some(sfs,Processing)"
by(auto simp: correct_state_def conf_clinit_def conf_f_def2)
note conf_sys_xcpt [elim!]
note xp' = meth s' xp
from correct meth
obtain ST LT where
h_ok: "P ⊢ h √" and
sh_ok: "P,h ⊢⇩s sh √" and
Φ_pc: "Φ C M ! pc = Some (ST, LT)" and
frame: "conf_f P h sh (ST,LT) ins (stk,loc,C,M,pc,ics)" and
frames: "conf_fs P h sh Φ C M (size Ts) T frs" and
confc: "conf_clinit P sh ((stk,loc,C,M,pc,ics)#frs)" and
vics: "P,h,sh ⊢⇩i (C,M,pc,ics)"
by(auto simp: defs1 dest: sees_method_fun)
from frame obtain
stk: "P,h ⊢ stk [:≤] ST" and
loc: "P,h ⊢ loc [:≤⇩⊤] LT" and
pc: "pc < size ins"
by (unfold conf_f_def) auto
from h_ok have preh: "preallocated h" by (simp add: hconf_def)
note wtp
moreover
from exec_step_xcpt_h[OF xp ins wt correct]
obtain obj where h: "h xcp = Some obj" by clarify
moreover note correct
ultimately
have fh: "curr_method (stk,loc,C,M,pc,ics) ≠ clinit
⟹ P,Φ ⊢ find_handler P xcp h frs sh √" by (rule uncaught_xcpt_correct)
with xp'
have "M ≠ clinit ⟹ ∀Cs a. ics ≠ Throwing Cs a
⟹ match_ex_table P (cname_of h xcp) pc xt = None ⟹ ?thesis"
(is "?nc ⟹ ?t ⟹ ?m (cname_of h xcp) = _ ⟹ _" is "?nc ⟹ ?t ⟹ ?match = _ ⟹ _")
by(cases ics; simp add: split_beta)
moreover
from correct xp' conf_clinit_Called_Throwing conf_f_Throwing[where h=h and sh=sh, OF _ cls h sfs]
have "M = clinit ⟹ ∀Cs a. ics ≠ Throwing Cs a
⟹ match_ex_table P (cname_of h xcp) pc xt = None ⟹ ?thesis"
by(cases frs, auto simp: correct_state_def image_iff split_beta) fastforce
moreover
{ fix pc_d assume "?match = Some pc_d"
then obtain pc' d' where some_handler: "?match = Some (pc',d')"
by (cases pc_d) auto
from stk have [simp]: "size stk = size ST" ..
from wt Φ_pc have
eff: "∀(pc', s')∈set (xcpt_eff (ins!pc) P pc (ST,LT) xt).
pc' < size ins ∧ P ⊢ s' ≤' Φ C M!pc'"
by (auto simp: defs1)
from some_handler obtain f t D where
xt: "(f,t,D,pc',d') ∈ set xt" and
"matches_ex_entry P (cname_of h xcp) pc (f,t,D,pc',d')"
by (auto dest: match_ex_table_SomeD)
hence match: "P ⊢ cname_of h xcp ≼⇧* D" "pc ∈ {f..<t}"
by (auto simp: matches_ex_entry_def)
{ fix C' Cs assume ics: "ics = Calling C' Cs ∨ ics = Called (C'#Cs)"
let ?stk' = "Addr xcp # drop (length stk - d') stk"
let ?f = "(?stk', loc, C, M, pc', No_ics)"
from some_handler xp' ics
have σ': "σ' = (None, h, ?f#frs, sh)"
by (cases ics; simp add: split_beta)
from xp ics have "xcp = addr_of_sys_xcpt NoClassDefFoundError"
by(cases ics, auto simp: split_beta split: init_state.splits if_split_asm)
with match preh have conf: "P,h ⊢ Addr xcp :≤ Class D" by fastforce
from correct ics obtain C1 where "Called_context P C1 (ins!pc)"
by(fastforce simp: correct_state_def conf_f_def2)
then have "ins!pc ∈ Called_set" by(rule Called_context_Called_set)
with xt match have "(f,t,D,pc',d') ∈ set (relevant_entries P (ins!pc) pc xt)"
by(auto simp: relevant_entries_def is_relevant_entry_def)
with eff obtain ST' LT' where
Φ_pc': "Φ C M ! pc' = Some (ST', LT')" and
pc': "pc' < size ins" and
less: "P ⊢ (Class D # drop (size ST - d') ST, LT) ≤⇩i (ST', LT')"
by (fastforce simp: xcpt_eff_def sup_state_opt_any_Some)
with conf loc stk conf_f_def2 frame ics have "conf_f P h sh (ST',LT') ins ?f"
by (auto simp: defs1 intro: list_all2_dropI)
with meth h_ok frames Φ_pc' σ' sh_ok confc ics
have ?thesis
by (unfold correct_state_def)
(auto dest: sees_method_fun conf_clinit_diff' sees_method_is_class; fastforce)
}
moreover
{ assume ics: "ics = No_ics ∨ ics = Called []"
let ?stk' = "Addr xcp # drop (length stk - d') stk"
let ?f = "(?stk', loc, C, M, pc', No_ics)"
from some_handler xp' ics
have σ': "σ' = (None, h, ?f#frs, sh)"
by (cases ics; simp add: split_beta)
from xp ics obtain
"(f,t,D,pc',d') ∈ set (relevant_entries P (ins!pc) pc xt)" and
conf: "P,h ⊢ Addr xcp :≤ Class D"
proof (cases "ins!pc")
case Return
with xp ics have False by(cases ics; cases frs, auto simp: split_beta split: if_split_asm)
then show ?thesis by simp
next
case New with xp match
have "is_relevant_entry P (ins!pc) pc (f,t,D,pc',d')"
by (simp add: is_relevant_entry_def)
moreover
from xp wt correct obtain obj where xcp: "h xcp = Some obj"
by (blast dest: exec_step_xcpt_h[OF _ ins])
ultimately
show ?thesis using xt match
by (auto simp: relevant_entries_def conf_def case_prod_unfold intro: that)
next
case Getfield with xp ics
have xcp: "xcp = addr_of_sys_xcpt NullPointer ∨ xcp = addr_of_sys_xcpt NoSuchFieldError
∨ xcp = addr_of_sys_xcpt IncompatibleClassChangeError"
by (cases ics; simp add: split_beta split: if_split_asm staticb.splits)
with Getfield match preh have "is_relevant_entry P (ins!pc) pc (f,t,D,pc',d')"
by (fastforce simp: is_relevant_entry_def)
with match preh xt xcp
show ?thesis by(fastforce simp: relevant_entries_def intro: that)
next
case Getstatic with xp match
have "is_relevant_entry P (ins!pc) pc (f,t,D,pc',d')"
by (simp add: is_relevant_entry_def)
moreover
from xp wt correct obtain obj where xcp: "h xcp = Some obj"
by (blast dest: exec_step_xcpt_h[OF _ ins])
ultimately
show ?thesis using xt match
by (auto simp: relevant_entries_def conf_def case_prod_unfold intro: that)
next
case Putfield with xp ics
have xcp: "xcp = addr_of_sys_xcpt NullPointer ∨ xcp = addr_of_sys_xcpt NoSuchFieldError
∨ xcp = addr_of_sys_xcpt IncompatibleClassChangeError"
by (cases ics; simp add: split_beta split: if_split_asm staticb.splits)
with Putfield match preh have "is_relevant_entry P (ins!pc) pc (f,t,D,pc',d')"
by (fastforce simp: is_relevant_entry_def)
with match preh xt xcp
show ?thesis by (fastforce simp: relevant_entries_def intro: that)
next
case Putstatic with xp match
have "is_relevant_entry P (ins!pc) pc (f,t,D,pc',d')"
by (simp add: is_relevant_entry_def)
moreover
from xp wt correct obtain obj where xcp: "h xcp = Some obj"
by (blast dest: exec_step_xcpt_h[OF _ ins])
ultimately
show ?thesis using xt match
by (auto simp: relevant_entries_def conf_def case_prod_unfold intro: that)
next
case Checkcast with xp ics
have [simp]: "xcp = addr_of_sys_xcpt ClassCast"
by (cases ics; simp add: split_beta split: if_split_asm)
with Checkcast match preh have "is_relevant_entry P (ins!pc) pc (f,t,D,pc',d')"
by (simp add: is_relevant_entry_def)
with match preh xt
show ?thesis by (fastforce simp: relevant_entries_def intro: that)
next
case Invoke with xp match
have "is_relevant_entry P (ins!pc) pc (f,t,D,pc',d')"
by (simp add: is_relevant_entry_def)
moreover
from xp wt correct obtain obj where xcp: "h xcp = Some obj"
by (blast dest: exec_step_xcpt_h[OF _ ins])
ultimately
show ?thesis using xt match
by (auto simp: relevant_entries_def conf_def case_prod_unfold intro: that)
next
case Invokestatic with xp match
have "is_relevant_entry P (ins!pc) pc (f,t,D,pc',d')"
by (simp add: is_relevant_entry_def)
moreover
from xp wt correct obtain obj where xcp: "h xcp = Some obj"
by (blast dest: exec_step_xcpt_h[OF _ ins])
ultimately
show ?thesis using xt match
by (auto simp: relevant_entries_def conf_def case_prod_unfold intro: that)
next
case Throw with xp match preh
have "is_relevant_entry P (ins!pc) pc (f,t,D,pc',d')"
by (simp add: is_relevant_entry_def)
moreover
from xp wt correct obtain obj where xcp: "h xcp = Some obj"
by (blast dest: exec_step_xcpt_h[OF _ ins])
ultimately
show ?thesis using xt match
by (auto simp: relevant_entries_def conf_def case_prod_unfold intro: that)
qed(cases ics, (auto)[5])+
with eff obtain ST' LT' where
Φ_pc': "Φ C M ! pc' = Some (ST', LT')" and
pc': "pc' < size ins" and
less: "P ⊢ (Class D # drop (size ST - d') ST, LT) ≤⇩i (ST', LT')"
by (fastforce simp: xcpt_eff_def sup_state_opt_any_Some)
with conf loc stk conf_f_def2 frame ics have "conf_f P h sh (ST',LT') ins ?f"
by (auto simp: defs1 intro: list_all2_dropI)
with meth h_ok frames Φ_pc' σ' sh_ok confc ics
have ?thesis
by (unfold correct_state_def) (auto dest: sees_method_fun conf_clinit_diff'; fastforce)
}
ultimately
have "∀Cs a. ics ≠ Throwing Cs a ⟹ ?thesis" by(cases ics; metis list.exhaust)
}
moreover
{ fix Cs a assume "ics = Throwing Cs a"
with xp' have ics: "ics = Throwing [] xcp" by(cases Cs; clarsimp)
let ?frs = "(stk,loc,C,M,pc,No_ics)#frs"
have eT: "exec_step P h stk loc C M pc (Throwing [] xcp) frs sh = (Some xcp, h, ?frs, sh)"
by auto
with xp' ics have σ'_fh: "σ' = find_handler P xcp h ?frs sh" by simp
from meth have [simp]: "xt = ex_table_of P C M" by simp
let ?match = "match_ex_table P (cname_of h xcp) pc xt"
{ assume clinit: "M = clinit" and None: "?match = None"
note asms = clinit None
have "P,Φ |- find_handler P xcp h ?frs sh [ok]"
proof(cases frs)
case Nil
with h_ok sh_ok asms show "P,Φ |- find_handler P xcp h ?frs sh [ok]"
by(simp add: correct_state_def)
next
case [simp]: (Cons f' frs')
obtain stk' loc' C' M' pc' ics' where
[simp]: "f' = (stk',loc',C',M',pc',ics')" by(cases f')
have cls: "is_class P C" by(rule sees_method_is_class[OF meth])
have shC: "sh C = Some(sfs,Processing)" by(rule sfs[OF clinit])
from correct obtain b Ts T mxs' mxl⇩0' ins' xt' ST' LT' where
meth': "P ⊢ C' sees M', b : Ts→T = (mxs', mxl⇩0', ins', xt') in C'" and
Φ_pc': "Φ C' M' ! pc' = ⌊(ST', LT')⌋" and
frame': "conf_f P h sh (ST',LT') ins' (stk', loc', C', M', pc', ics')" and
frames': "conf_fs P h sh Φ C' M' (length Ts) T frs'" and
confc': "conf_clinit P sh ((stk',loc',C',M',pc',ics')#frs')"
by(auto dest: conf_clinit_Cons simp: correct_state_def)
from meth' have
ins'[simp]: "instrs_of P C' M' = ins'"
and [simp]: "xt' = ex_table_of P C' M'" by simp+
let ?f' = "case ics' of Called Cs' ⇒ (stk',loc',C',M',pc',Throwing (C#Cs') xcp)
| _ ⇒ (stk',loc',C',M',pc',ics')"
from asms confc have confc_T: "conf_clinit P sh (?f'#frs')"
by(cases ics', auto simp: conf_clinit_def distinct_clinit_def)
from asms conf_f_Throwing[where h=h and sh=sh, OF _ cls h shC] frame' have
frame_T: "conf_f P h sh (ST', LT') ins' ?f'" by(cases ics'; simp)
with h_ok sh_ok meth' Φ_pc' confc_T frames'
have "P,Φ |- (None, h, ?f'#frs', sh) [ok]"
by(cases ics') (fastforce simp: correct_state_def)+
with asms show ?thesis by(cases ics'; simp)
qed
}
moreover
{ assume asms: "M ≠ clinit" "?match = None"
from asms uncaught_xcpt_correct[OF wtp h correct]
have "P,Φ |- find_handler P xcp h frs sh [ok]" by simp
with asms have "P,Φ |- find_handler P xcp h ?frs sh [ok]" by auto
}
moreover
{ fix pc_d assume some_handler: "?match = ⌊pc_d⌋"
(is "?match = ⌊pc_d⌋")
then obtain pc1 d1 where sh': "?match = Some(pc1,d1)" by(cases pc_d, simp)
let ?stk' = "Addr xcp # drop (length stk - d1) stk"
let ?f = "(?stk', loc, C, M, pc1, No_ics)"
from stk have [simp]: "size stk = size ST" ..
from wt Φ_pc have
eff: "∀(pc1, s')∈set (xcpt_eff (ins!pc) P pc (ST,LT) xt).
pc1 < size ins ∧ P ⊢ s' ≤' Φ C M!pc1"
by (auto simp: defs1)
from match_ex_table_SomeD[OF sh'] obtain f t D where
xt: "(f,t,D,pc1,d1) ∈ set xt" and
"matches_ex_entry P (cname_of h xcp) pc (f,t,D,pc1,d1)" by auto
hence match: "P ⊢ cname_of h xcp ≼⇧* D" "pc ∈ {f..<t}"
by (auto simp: matches_ex_entry_def)
from ics vics obtain C1 where "Called_context P C1 (ins ! pc)" by auto
then have "ins!pc ∈ Called_set" by(rule Called_context_Called_set)
with match xt xp ics obtain
res: "(f,t,D,pc1,d1) ∈ set (relevant_entries P (ins!pc) pc xt)"
by(auto simp: relevant_entries_def is_relevant_entry_def)
with h match xt xp ics have conf: "P,h ⊢ Addr xcp :≤ Class D"
by (auto simp: relevant_entries_def conf_def case_prod_unfold)
with eff res obtain ST1 LT1 where
Φ_pc1: "Φ C M ! pc1 = Some (ST1, LT1)" and
pc1: "pc1 < size ins" and
less1: "P ⊢ (Class D # drop (size ST - d1) ST, LT) ≤⇩i (ST1, LT1)"
by (fastforce simp: xcpt_eff_def sup_state_opt_any_Some)
with conf loc stk conf_f_def2 frame ics have frame1: "conf_f P h sh (ST1,LT1) ins ?f"
by (auto simp: defs1 intro: list_all2_dropI)
from Φ_pc1 h_ok sh_ok meth frame1 frames conf_clinit_diff'[OF confc] have
"P,Φ |- (None, h, ?f # frs, sh) [ok]" by(fastforce simp: correct_state_def)
with sh' have "P,Φ |- find_handler P xcp h ?frs sh [ok]" by auto
}
ultimately
have cr': "P,Φ |- find_handler P xcp h ?frs sh [ok]" by(cases "?match") blast+
with σ'_fh have ?thesis by simp
}
ultimately
show ?thesis by (cases "?match") blast+
qed
declare defs1 [simp]
subsection ‹ Initialization procedure steps ›
text ‹
In this section we prove that, for states that result in a step of the
initialization procedure rather than an instruction execution, the state
after execution of the step still conforms.
›
lemma Calling_correct:
fixes σ' :: jvm_state
assumes wtprog: "wf_jvm_prog⇘Φ⇙ P"
assumes mC: "P ⊢ C sees M,b:Ts→T=(mxs,mxl⇩0,ins,xt) in C"
assumes s': "Some σ' = exec (P, None, h, (stk,loc,C,M,pc,ics)#frs, sh)"
assumes cf: "P,Φ ⊢ (None, h, (stk,loc,C,M,pc,ics)#frs, sh)√"
assumes xc: "fst (exec_step P h stk loc C M pc ics frs sh) = None"
assumes ics: "ics = Calling C' Cs"
shows "P,Φ ⊢ σ'√"
proof -
from wtprog obtain wfmb where wf: "wf_prog wfmb P"
by (simp add: wf_jvm_prog_phi_def)
from mC cf obtain ST LT where
h_ok: "P ⊢ h √" and
sh_ok: "P,h ⊢⇩s sh √" and
Φ: "Φ C M ! pc = Some (ST,LT)" and
stk: "P,h ⊢ stk [:≤] ST" and loc: "P,h ⊢ loc [:≤⇩⊤] LT" and
pc: "pc < size ins" and
frame: "conf_f P h sh (ST, LT) ins (stk,loc,C,M,pc,ics)" and
fs: "conf_fs P h sh Φ C M (size Ts) T frs" and
confc: "conf_clinit P sh ((stk,loc,C,M,pc,ics)#frs)" and
vics: "P,h,sh ⊢⇩i (C,M,pc,ics)"
by (fastforce dest: sees_method_fun)
with ics have confc⇩0: "conf_clinit P sh ((stk,loc,C,M,pc,Calling C' Cs)#frs)" by simp
from vics ics have cls': "is_class P C'" by auto
{ assume None: "sh C' = None"
let ?sh = "sh(C' ↦ (sblank P C', Prepared))"
obtain FDTs where
flds: "P ⊢ C' has_fields FDTs" using wf_Fields_Ex[OF wf cls'] by clarsimp
from shconf_upd_obj[where C=C', OF sh_ok soconf_sblank[OF flds]]
have sh_ok': "P,h ⊢⇩s ?sh √" by simp
from None have "∀sfs. sh C' ≠ Some(sfs,Processing)" by simp
with conf_clinit_nProc_dist[OF confc] have
dist': "distinct (C' # clinit_classes ((stk, loc, C, M, pc, ics) # frs))" by simp
then have dist'': "distinct (C' # clinit_classes frs)" by simp
have confc': "conf_clinit P ?sh ((stk, loc, C, M, pc, ics) # frs)"
by(rule conf_clinit_shupd[OF confc dist'])
have fs': "conf_fs P h ?sh Φ C M (size Ts) T frs" by(rule conf_fs_shupd[OF fs dist''])
from vics ics have vics': "P,h,?sh ⊢⇩i (C, M, pc, ics)" by auto
from s' ics None have "σ' = (None, h, (stk, loc, C, M, pc, ics)#frs, ?sh)" by auto
with mC h_ok sh_ok' Φ stk loc pc fs' confc vics' confc' frame None
have ?thesis by fastforce
}
moreover
{ fix a assume "sh C' = Some a"
then obtain sfs i where shC'[simp]: "sh C' = Some(sfs,i)" by(cases a, simp)
from confc ics have last: "∃sobj. sh (last(C'#Cs)) = Some sobj"
by(fastforce simp: conf_clinit_def)
let "?f" = "λics'. (stk, loc, C, M, pc, ics'::init_call_status)"
{ assume i: "i = Done ∨ i = Processing"
let ?ics = "Called Cs"
from last vics ics have vics': "P,h,sh ⊢⇩i (C, M, pc, ?ics)" by auto
from confc ics have confc': "conf_clinit P sh (?f ?ics#frs)"
by(cases "M=clinit"; clarsimp simp: conf_clinit_def distinct_clinit_def)
from i s' ics have "σ' = (None, h, ?f ?ics#frs, sh)" by auto
with mC h_ok sh_ok Φ stk loc pc fs confc' vics' frame ics
have ?thesis by fastforce
}
moreover
{ assume i[simp]: "i = Error"
let ?a = "addr_of_sys_xcpt NoClassDefFoundError"
let ?ics = "Throwing Cs ?a"
from h_ok have preh: "preallocated h" by (simp add: hconf_def)
then obtain obj where ha: "h ?a = Some obj" by(clarsimp simp: preallocated_def sys_xcpts_def)
with vics ics have vics': "P,h,sh ⊢⇩i (C, M, pc, ?ics)" by auto
from confc ics have confc'': "conf_clinit P sh (?f ?ics#frs)"
by(cases "M=clinit"; clarsimp simp: conf_clinit_def distinct_clinit_def)
from s' ics have σ': "σ' = (None, h, ?f ?ics#frs, sh)" by auto
from mC h_ok sh_ok Φ stk loc pc fs confc'' vics σ' ics ha
have ?thesis by fastforce
}
moreover
{ assume i[simp]: "i = Prepared"
let ?sh = "sh(C' ↦ (sfs,Processing))"
let ?D = "fst(the(class P C'))"
let ?ics = "if C' = Object then Called (C'#Cs) else Calling ?D (C'#Cs)"
from shconf_upd_obj[where C=C', OF sh_ok shconfD[OF sh_ok shC']]
have sh_ok': "P,h ⊢⇩s ?sh √" by simp
from cls' have "C' ≠ Object ⟹ P ⊢ C' ≼⇧* ?D" by(auto simp: is_class_def intro!: subcls1I)
with is_class_supclass[OF wf _ cls'] have D: "C' ≠ Object ⟹ is_class P ?D" by simp
from i have "∀sfs. sh C' ≠ Some(sfs,Processing)" by simp
with conf_clinit_nProc_dist[OF confc⇩0] have
dist': "distinct (C' # clinit_classes ((stk, loc, C, M, pc, Calling C' Cs) # frs))" by fast
then have dist'': "distinct (C' # clinit_classes frs)" by simp
from conf_clinit_shupd_Calling[OF confc⇩0 dist' cls']
conf_clinit_shupd_Called[OF confc⇩0 dist' cls']
have confc': "conf_clinit P ?sh (?f ?ics#frs)" by clarsimp
with last ics have "∃sobj. ?sh (last(C'#Cs)) = Some sobj"
by(auto simp: conf_clinit_def fun_upd_apply)
with D vics ics have vics': "P,h,?sh ⊢⇩i (C, M, pc, ?ics)" by auto
have fs': "conf_fs P h ?sh Φ C M (size Ts) T frs" by(rule conf_fs_shupd[OF fs dist''])
from frame vics' have frame': "conf_f P h ?sh (ST, LT) ins (?f ?ics)" by simp
from i s' ics have "σ' = (None, h, ?f ?ics#frs, ?sh)" by(auto simp: if_split_asm)
with mC h_ok sh_ok' Φ stk loc pc fs' confc' frame' ics
have ?thesis by fastforce
}
ultimately have ?thesis by(cases i, auto)
}
ultimately show ?thesis by(cases "sh C'", auto)
qed
lemma Throwing_correct:
fixes σ' :: jvm_state
assumes wtprog: "wf_jvm_prog⇘Φ⇙ P"
assumes mC: "P ⊢ C sees M,b:Ts→T=(mxs,mxl⇩0,ins,xt) in C"
assumes s': "Some σ' = exec (P, None, h, (stk,loc,C,M,pc,ics)#frs, sh)"
assumes cf: "P,Φ ⊢ (None, h, (stk,loc,C,M,pc,ics)#frs, sh)√"
assumes xc: "fst (exec_step P h stk loc C M pc ics frs sh) = None"
assumes ics: "ics = Throwing (C'#Cs) a"
shows "P,Φ ⊢ σ'√"
proof -
from wtprog obtain wfmb where wf: "wf_prog wfmb P"
by (simp add: wf_jvm_prog_phi_def)
from mC cf obtain ST LT where
h_ok: "P ⊢ h √" and
sh_ok: "P,h ⊢⇩s sh √" and
Φ: "Φ C M ! pc = Some (ST,LT)" and
stk: "P,h ⊢ stk [:≤] ST" and loc: "P,h ⊢ loc [:≤⇩⊤] LT" and
pc: "pc < size ins" and
frame: "conf_f P h sh (ST, LT) ins (stk,loc,C,M,pc,ics)" and
fs: "conf_fs P h sh Φ C M (size Ts) T frs" and
confc: "conf_clinit P sh ((stk,loc,C,M,pc,ics)#frs)" and
vics: "P,h,sh ⊢⇩i (C,M,pc,ics)"
by (fastforce dest: sees_method_fun)
with ics have confc⇩0: "conf_clinit P sh ((stk,loc,C,M,pc,Throwing (C'#Cs) a)#frs)" by simp
from frame ics mC have
cc: "∃C1. Called_context P C1 (ins ! pc)" by(clarsimp simp: conf_f_def2)
from frame ics obtain obj where ha: "h a = Some obj" by(auto simp: conf_f_def2)
from confc ics obtain sfs i where shC': "sh C' = Some(sfs,i)" by(clarsimp simp: conf_clinit_def)
then have sfs: "P,h,C' ⊢⇩s sfs √" by(rule shconfD[OF sh_ok])
from s' ics
have σ': "σ' = (None, h, (stk,loc,C,M,pc,Throwing Cs a)#frs, sh(C' ↦ (fst(the(sh C')), Error)))"
(is "σ' = (None, h, ?f'#frs, ?sh')")
by simp
from confc ics have dist: "distinct (C' # clinit_classes (?f' # frs))"
by (simp add: conf_clinit_def distinct_clinit_def)
then have dist': "distinct (C' # clinit_classes frs)" by simp
from conf_clinit_Throwing confc ics have confc': "conf_clinit P sh (?f' # frs)" by simp
from shconf_upd_obj[OF sh_ok sfs] shC' have "P,h ⊢⇩s ?sh' √" by simp
moreover
have "conf_fs P h ?sh' Φ C M (length Ts) T frs" by(rule conf_fs_shupd[OF fs dist'])
moreover
have "conf_clinit P ?sh' (?f' # frs)" by(rule conf_clinit_shupd[OF confc' dist])
moreover note σ' h_ok mC Φ pc stk loc ha cc
ultimately show "P,Φ ⊢ σ' √" by fastforce
qed
lemma Called_correct:
fixes σ' :: jvm_state
assumes wtprog: "wf_jvm_prog⇘Φ⇙ P"
assumes mC: "P ⊢ C sees M,b:Ts→T=(mxs,mxl⇩0,ins,xt) in C"
assumes s': "Some σ' = exec (P, None, h, (stk,loc,C,M,pc,ics)#frs, sh)"
assumes cf: "P,Φ ⊢ (None, h, (stk,loc,C,M,pc,ics)#frs, sh)√"
assumes xc: "fst (exec_step P h stk loc C M pc ics frs sh) = None"
assumes ics[simp]: "ics = Called (C'#Cs)"
shows "P,Φ ⊢ σ'√"
proof -
from wtprog obtain wfmb where wf: "wf_prog wfmb P"
by (simp add: wf_jvm_prog_phi_def)
from mC cf obtain ST LT where
h_ok: "P ⊢ h √" and
sh_ok: "P,h ⊢⇩s sh √" and
Φ: "Φ C M ! pc = Some (ST,LT)" and
stk: "P,h ⊢ stk [:≤] ST" and loc: "P,h ⊢ loc [:≤⇩⊤] LT" and
pc: "pc < size ins" and
frame: "conf_f P h sh (ST, LT) ins (stk,loc,C,M,pc,ics)" and
fs: "conf_fs P h sh Φ C M (size Ts) T frs" and
confc: "conf_clinit P sh ((stk,loc,C,M,pc,ics)#frs)" and
vics: "P,h,sh ⊢⇩i (C,M,pc,ics)"
by (fastforce dest: sees_method_fun)
then have confc⇩0: "conf_clinit P sh ((stk,loc,C,M,pc,Called (C'#Cs))#frs)" by simp
from frame mC obtain C1 sobj where
ss: "Called_context P C1 (ins ! pc)" and
shC1: "sh C1 = Some sobj" by(clarsimp simp: conf_f_def2)
from confc wf_sees_clinit[OF wf] obtain mxs' mxl' ins' xt' where
clinit: "P ⊢ C' sees clinit,Static: [] → Void=(mxs',mxl',ins',xt') in C'"
by(fastforce simp: conf_clinit_def is_class_def)
let ?loc' = "replicate mxl' undefined"
from s' clinit
have σ': "σ' = (None, h, ([],?loc',C',clinit,0,No_ics)#(stk,loc,C,M,pc,Called Cs)#frs, sh)"
(is "σ' = (None, h, ?if#?f'#frs, sh)")
by simp
with wtprog clinit
obtain start: "wt_start P C' Static [] mxl' (Φ C' clinit)" and ins': "ins' ≠ []"
by (auto dest: wt_jvm_prog_impl_wt_start)
then obtain LT⇩0 where LT⇩0: "Φ C' clinit ! 0 = Some ([], LT⇩0)"
by (clarsimp simp: wt_start_def defs1 sup_state_opt_any_Some split: staticb.splits)
moreover
have "conf_f P h sh ([], LT⇩0) ins' ?if"
proof -
let ?LT = "replicate mxl' Err"
have "P,h ⊢ ?loc' [:≤⇩⊤] ?LT" by simp
also from start LT⇩0 have "P ⊢ … [≤⇩⊤] LT⇩0" by (simp add: wt_start_def)
finally have "P,h ⊢ ?loc' [:≤⇩⊤] LT⇩0" .
thus ?thesis using ins' by simp
qed
moreover
from conf_clinit_Called confc clinit have "conf_clinit P sh (?if # ?f' # frs)" by simp
moreover note σ' h_ok sh_ok mC Φ pc stk loc clinit ss shC1 fs
ultimately show "P,Φ ⊢ σ' √" by fastforce
qed
subsection ‹ Single Instructions ›
text ‹
In this section we prove for each single (welltyped) instruction
that the state after execution of the instruction still conforms.
Since we have already handled exceptions above, we can now assume that
no exception occurs in this step. For instructions that may call
the initialization procedure, we cover the calling and non-calling
cases separately.
›
lemma Invoke_correct:
fixes σ' :: jvm_state
assumes wtprog: "wf_jvm_prog⇘Φ⇙ P"
assumes meth_C: "P ⊢ C sees M,b:Ts→T=(mxs,mxl⇩0,ins,xt) in C"
assumes ins: "ins ! pc = Invoke M' n"
assumes wti: "P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M"
assumes σ': "Some σ' = exec (P, None, h, (stk,loc,C,M,pc,ics)#frs, sh)"
assumes approx: "P,Φ ⊢ (None, h, (stk,loc,C,M,pc,ics)#frs, sh)√"
assumes no_xcp: "fst (exec_step P h stk loc C M pc ics frs sh) = None"
shows "P,Φ ⊢ σ'√"
proof -
from meth_C approx ins have [simp]: "ics = No_ics" by(cases ics, auto)
note split_paired_Ex [simp del]
from wtprog obtain wfmb where wfprog: "wf_prog wfmb P"
by (simp add: wf_jvm_prog_phi_def)
from ins meth_C approx obtain ST LT where
heap_ok: "P⊢ h√" and
Φ_pc: "Φ C M!pc = Some (ST,LT)" and
frame: "conf_f P h sh (ST,LT) ins (stk,loc,C,M,pc,ics)" and
frames: "conf_fs P h sh Φ C M (size Ts) T frs" and
confc: "conf_clinit P sh ((stk,loc,C,M,pc,ics)#frs)"
by (fastforce dest: sees_method_fun)
from ins wti Φ_pc
have n: "n < size ST" by simp
{ assume "stk!n = Null"
with ins no_xcp meth_C have False by (simp add: split_beta)
hence ?thesis ..
}
moreover
{ assume "ST!n = NT"
moreover
from frame have "P,h ⊢ stk [:≤] ST" by simp
with n have "P,h ⊢ stk!n :≤ ST!n" by (simp add: list_all2_conv_all_nth)
ultimately
have "stk!n = Null" by simp
with ins no_xcp meth_C have False by (simp add: split_beta)
hence ?thesis ..
}
moreover {
assume NT: "ST!n ≠ NT" and Null: "stk!n ≠ Null"
from NT ins wti Φ_pc obtain D D' b Ts T m ST' LT' where
D: "ST!n = Class D" and
pc': "pc+1 < size ins" and
m_D: "P ⊢ D sees M',b: Ts→T = m in D'" and
Ts: "P ⊢ rev (take n ST) [≤] Ts" and
Φ': "Φ C M ! (pc+1) = Some (ST', LT')" and
LT': "P ⊢ LT [≤⇩⊤] LT'" and
ST': "P ⊢ (T # drop (n+1) ST) [≤] ST'" and
b[simp]: "b = NonStatic"
by (clarsimp simp: sup_state_opt_any_Some)
from frame obtain
stk: "P,h ⊢ stk [:≤] ST" and
loc: "P,h ⊢ loc [:≤⇩⊤] LT" by simp
from n stk D have "P,h ⊢ stk!n :≤ Class D"
by (auto simp: list_all2_conv_all_nth)
with Null obtain a C' fs where
Addr: "stk!n = Addr a" and
obj: "h a = Some (C',fs)" and
C'subD: "P ⊢ C' ≼⇧* D"
by (fastforce dest!: conf_ClassD)
with wfprog m_D no_xcp
obtain Ts' T' D'' mxs' mxl' ins' xt' where
m_C': "P ⊢ C' sees M',NonStatic: Ts'→T' = (mxs',mxl',ins',xt') in D''" and
T': "P ⊢ T' ≤ T" and
Ts': "P ⊢ Ts [≤] Ts'"
by (auto dest: sees_method_mono)
with wf_NonStatic_nclinit wtprog have nclinit: "M' ≠ clinit" by(simp add: wf_jvm_prog_phi_def)
have D''subD': "P ⊢ D'' ≼⇧* D'" by(rule sees_method_decl_mono[OF C'subD m_D m_C'])
let ?loc' = "Addr a # rev (take n stk) @ replicate mxl' undefined"
let ?f' = "([], ?loc', D'', M', 0, No_ics)"
let ?f = "(stk, loc, C, M, pc, ics)"
from Addr obj m_C' ins σ' meth_C no_xcp
have s': "σ' = (None, h, ?f' # ?f # frs, sh)" by simp
from Ts n have [simp]: "size Ts = n"
by (auto dest: list_all2_lengthD simp: min_def)
with Ts' have [simp]: "size Ts' = n"
by (auto dest: list_all2_lengthD)
from m_C' wfprog
obtain mD'': "P ⊢ D'' sees M',NonStatic:Ts'→T'=(mxs',mxl',ins',xt') in D''"
by (fast dest: sees_method_idemp)
moreover
with wtprog
obtain start: "wt_start P D'' NonStatic Ts' mxl' (Φ D'' M')" and ins': "ins' ≠ []"
by (auto dest: wt_jvm_prog_impl_wt_start)
then obtain LT⇩0 where LT⇩0: "Φ D'' M' ! 0 = Some ([], LT⇩0)"
by (clarsimp simp: wt_start_def defs1 sup_state_opt_any_Some split: staticb.splits)
moreover
have "conf_f P h sh ([], LT⇩0) ins' ?f'"
proof -
let ?LT = "OK (Class D'') # (map OK Ts') @ (replicate mxl' Err)"
from stk have "P,h ⊢ take n stk [:≤] take n ST" ..
hence "P,h ⊢ rev (take n stk) [:≤] rev (take n ST)" by simp
also note Ts also note Ts' finally
have "P,h ⊢ rev (take n stk) [:≤⇩⊤] map OK Ts'" by simp
also
have "P,h ⊢ replicate mxl' undefined [:≤⇩⊤] replicate mxl' Err"
by simp
also from m_C' have "P ⊢ C' ≼⇧* D''" by (rule sees_method_decl_above)
with obj have "P,h ⊢ Addr a :≤ Class D''" by (simp add: conf_def)
ultimately
have "P,h ⊢ ?loc' [:≤⇩⊤] ?LT" by simp
also from start LT⇩0 have "P ⊢ … [≤⇩⊤] LT⇩0" by (simp add: wt_start_def)
finally have "P,h ⊢ ?loc' [:≤⇩⊤] LT⇩0" .
thus ?thesis using ins' nclinit by simp
qed
moreover
have "conf_clinit P sh (?f'#?f#frs)" using conf_clinit_Invoke[OF confc nclinit] by simp
ultimately
have ?thesis using s' Φ_pc approx meth_C m_D T' ins D nclinit D''subD'
by(fastforce dest: sees_method_fun [of _ C])
}
ultimately show ?thesis by blast
qed
lemma Invokestatic_nInit_correct:
fixes σ' :: jvm_state
assumes wtprog: "wf_jvm_prog⇘Φ⇙ P"
assumes meth_C: "P ⊢ C sees M,b:Ts→T=(mxs,mxl⇩0,ins,xt) in C"
assumes ins: "ins ! pc = Invokestatic D M' n" and nclinit: "M' ≠ clinit"
assumes wti: "P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M"
assumes σ': "Some σ' = exec (P, None, h, (stk,loc,C,M,pc,ics)#frs, sh)"
assumes approx: "P,Φ ⊢ (None, h, (stk,loc,C,M,pc,ics)#frs, sh)√"
assumes no_xcp: "fst (exec_step P h stk loc C M pc ics frs sh) = None"
assumes cs: "ics = Called [] ∨ (ics = No_ics ∧ (∃sfs. sh (fst(method P D M')) = Some(sfs, Done)))"
shows "P,Φ ⊢ σ'√"
proof -
note split_paired_Ex [simp del]
from wtprog obtain wfmb where wfprog: "wf_prog wfmb P"
by (simp add: wf_jvm_prog_phi_def)
from ins meth_C approx obtain ST LT where
heap_ok: "P⊢ h√" and
Φ_pc: "Φ C M!pc = Some (ST,LT)" and
frame: "conf_f P h sh (ST,LT) ins (stk,loc,C,M,pc,ics)" and
frames: "conf_fs P h sh Φ C M (size Ts) T frs" and
confc: "conf_clinit P sh ((stk,loc,C,M,pc,ics)#frs)"
by (fastforce dest: sees_method_fun)
from ins wti Φ_pc have n: "n ≤ size ST" by simp
from ins wti Φ_pc obtain D' b Ts T mxs' mxl' ins' xt' ST' LT' where
pc': "pc+1 < size ins" and
m_D: "P ⊢ D sees M',b: Ts→T = (mxs',mxl',ins',xt') in D'" and
Ts: "P ⊢ rev (take n ST) [≤] Ts" and
Φ': "Φ C M ! (pc+1) = Some (ST', LT')" and
LT': "P ⊢ LT [≤⇩⊤] LT'" and
ST': "P ⊢ (T # drop n ST) [≤] ST'" and
b[simp]: "b = Static"
by (clarsimp simp: sup_state_opt_any_Some)
from frame obtain
stk: "P,h ⊢ stk [:≤] ST" and
loc: "P,h ⊢ loc [:≤⇩⊤] LT" by simp
let ?loc' = "rev (take n stk) @ replicate mxl' undefined"
let ?f' = "([], ?loc', D', M', 0, No_ics)"
let ?f = "(stk, loc, C, M, pc, No_ics)"
from m_D ins σ' meth_C no_xcp cs
have s': "σ' = (None, h, ?f' # ?f # frs, sh)" by auto
from Ts n have [simp]: "size Ts = n"
by (auto dest: list_all2_lengthD)
from m_D wfprog b
obtain mD': "P ⊢ D' sees M',Static:Ts→T=(mxs',mxl',ins',xt') in D'"
by (fast dest: sees_method_idemp)
moreover
with wtprog
obtain start: "wt_start P D' Static Ts mxl' (Φ D' M')" and ins': "ins' ≠ []"
by (auto dest: wt_jvm_prog_impl_wt_start)
then obtain LT⇩0 where LT⇩0: "Φ D' M' ! 0 = Some ([], LT⇩0)"
by (clarsimp simp: wt_start_def defs1 sup_state_opt_any_Some split: staticb.splits)
moreover
have "conf_f P h sh ([], LT⇩0) ins' ?f'"
proof -
let ?LT = "(map OK Ts) @ (replicate mxl' Err)"
from stk have "P,h ⊢ take n stk [:≤] take n ST" ..
hence "P,h ⊢ rev (take n stk) [:≤] rev (take n ST)" by simp
also note Ts finally
have "P,h ⊢ rev (take n stk) [:≤⇩⊤] map OK Ts" by simp
also
have "P,h ⊢ replicate mxl' undefined [:≤⇩⊤] replicate mxl' Err"
by simp
also from m_D have "P ⊢ D ≼⇧* D'" by (rule sees_method_decl_above)
ultimately
have "P,h ⊢ ?loc' [:≤⇩⊤] ?LT" by simp
also from start LT⇩0 have "P ⊢ … [≤⇩⊤] LT⇩0" by (simp add: wt_start_def)
finally have "P,h ⊢ ?loc' [:≤⇩⊤] LT⇩0" .
thus ?thesis using ins' by simp
qed
moreover
have "conf_clinit P sh (?f'#?f#frs)" by(rule conf_clinit_Invoke[OF confc nclinit])
ultimately
show ?thesis using s' Φ_pc approx meth_C m_D ins nclinit
by (fastforce dest: sees_method_fun [of _ C])
qed
lemma Invokestatic_Init_correct:
fixes σ' :: jvm_state
assumes wtprog: "wf_jvm_prog⇘Φ⇙ P"
assumes meth_C: "P ⊢ C sees M,b:Ts→T=(mxs,mxl⇩0,ins,xt) in C"
assumes ins: "ins ! pc = Invokestatic D M' n" and nclinit: "M' ≠ clinit"
assumes wti: "P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M"
assumes σ': "Some σ' = exec (P, None, h, (stk,loc,C,M,pc,No_ics)#frs, sh)"
assumes approx: "P,Φ ⊢ (None, h, (stk,loc,C,M,pc,No_ics)#frs, sh)√"
assumes no_xcp: "fst (exec_step P h stk loc C M pc No_ics frs sh) = None"
assumes nDone: "∀sfs. sh (fst(method P D M')) ≠ Some(sfs, Done)"
shows "P,Φ ⊢ σ'√"
proof -
note split_paired_Ex [simp del]
from wtprog obtain wfmb where wfprog: "wf_prog wfmb P"
by (simp add: wf_jvm_prog_phi_def)
from ins meth_C approx obtain ST LT where
heap_ok: "P⊢ h√" and
Φ_pc: "Φ C M!pc = Some (ST,LT)" and
stk: "P,h ⊢ stk [:≤] ST" and loc: "P,h ⊢ loc [:≤⇩⊤] LT" and
pc: "pc < size ins" and
frames: "conf_fs P h sh Φ C M (size Ts) T frs" and
confc: "conf_clinit P sh ((stk,loc,C,M,pc,No_ics)#frs)" and
pc: "pc < size ins"
by (fastforce dest: sees_method_fun)
from ins wti Φ_pc obtain D' b Ts T mxs' mxl' ins' xt' where
m_D: "P ⊢ D sees M',b: Ts→T = (mxs',mxl',ins',xt') in D'" and
b[simp]: "b = Static"
by clarsimp
let ?f = "(stk, loc, C, M, pc, Calling D' [])"
from m_D ins σ' meth_C no_xcp nDone
have s': "σ' = (None, h, ?f # frs, sh)" by(auto split: init_state.splits)
have cls: "is_class P D'" by(rule sees_method_is_class'[OF m_D])
from confc have confc': "conf_clinit P sh (?f#frs)"
by(auto simp: conf_clinit_def distinct_clinit_def split: if_split_asm)
with s' Φ_pc approx meth_C m_D ins nclinit stk loc pc cls frames
show ?thesis by(fastforce dest: sees_method_fun [of _ C])
qed
declare list_all2_Cons2 [iff]
lemma Return_correct:
fixes σ' :: jvm_state
assumes wt_prog: "wf_jvm_prog⇘Φ⇙ P"
assumes meth: "P ⊢ C sees M,b:Ts→T=(mxs,mxl⇩0,ins,xt) in C"
assumes ins: "ins ! pc = Return"
assumes wt: "P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M"
assumes s': "Some σ' = exec (P, None, h, (stk,loc,C,M,pc,ics)#frs, sh)"
assumes correct: "P,Φ ⊢ (None, h, (stk,loc,C,M,pc,ics)#frs, sh)√"
shows "P,Φ ⊢ σ'√"
proof -
from meth correct ins have [simp]: "ics = No_ics" by(cases ics, auto)
from wt_prog
obtain wfmb where wf: "wf_prog wfmb P" by (simp add: wf_jvm_prog_phi_def)
from meth ins s'
have "frs = [] ⟹ ?thesis" by (simp add: correct_state_def)
moreover
{ fix f frs' assume frs': "frs = f#frs'"
then obtain stk' loc' C' M' pc' ics' where
f: "f = (stk',loc',C',M',pc',ics')" by (cases f)
from correct meth
obtain ST LT where
h_ok: "P ⊢ h √" and
sh_ok: "P,h ⊢⇩s sh √" and
Φ_pc: "Φ C M ! pc = Some (ST, LT)" and
frame: "conf_f P h sh (ST, LT) ins (stk,loc,C,M,pc,ics)" and
frames: "conf_fs P h sh Φ C M (size Ts) T frs" and
confc: "conf_clinit P sh frs"
by (auto dest: sees_method_fun conf_clinit_Cons simp: correct_state_def)
from Φ_pc ins wt
obtain U ST⇩0 where "ST = U # ST⇩0" "P ⊢ U ≤ T"
by (simp add: wt_instr_def app_def) blast
with wf frame
have hd_stk: "P,h ⊢ hd stk :≤ T" by (auto simp: conf_f_def)
from f frs' frames meth
obtain ST' LT' b' Ts'' T'' mxs' mxl⇩0' ins' xt' where
Φ': "Φ C' M' ! pc' = Some (ST', LT')" and
meth_C': "P ⊢ C' sees M',b':Ts''→T''=(mxs',mxl⇩0',ins',xt') in C'" and
frame': "conf_f P h sh (ST',LT') ins' f" and
conf_fs: "conf_fs P h sh Φ C' M' (size Ts'') T'' frs'"
by clarsimp
from f frame' obtain
stk': "P,h ⊢ stk' [:≤] ST'" and
loc': "P,h ⊢ loc' [:≤⇩⊤] LT'" and
pc': "pc' < size ins'"
by (simp add: conf_f_def)
{ assume b[simp]: "b = NonStatic"
from wf_NonStatic_nclinit[OF wf] meth have nclinit[simp]: "M ≠ clinit" by simp
from f frs' meth ins s'
have σ':
"σ' = (None,h,(hd stk#(drop (1+size Ts) stk'),loc',C',M',pc'+1,ics')#frs',sh)"
(is "σ' = (None,h,?f'#frs',sh)")
by simp
from f frs' confc conf_clinit_diff have confc'': "conf_clinit P sh (?f'#frs')" by blast
with Φ' meth_C' f frs' frames meth
obtain D Ts' T' m D' where
ins': "ins' ! pc' = Invoke M (size Ts)" and
D: "ST' ! (size Ts) = Class D" and
meth_D: "P ⊢ D sees M,b: Ts'→T' = m in D'" and
T': "P ⊢ T ≤ T'" and
CsubD': "P ⊢ C ≼⇧* D'"
by(auto dest: sees_method_fun sees_method_fun[OF sees_method_idemp])
from wt_prog meth_C' pc'
have "P,T'',mxs',size ins',xt' ⊢ ins'!pc',pc' :: Φ C' M'"
by (rule wt_jvm_prog_impl_wt_instr)
with ins' Φ' D meth_D
obtain ST'' LT'' where
Φ_suc: "Φ C' M' ! Suc pc' = Some (ST'', LT'')" and
less: "P ⊢ (T' # drop (size Ts+1) ST', LT') ≤⇩i (ST'', LT'')" and
suc_pc': "Suc pc' < size ins'"
by (clarsimp simp: sup_state_opt_any_Some)
from hd_stk T' have hd_stk': "P,h ⊢ hd stk :≤ T'" ..
have frame'':
"conf_f P h sh (ST'',LT'') ins' ?f'"
proof -
from stk'
have "P,h ⊢ drop (1+size Ts) stk' [:≤] drop (1+size Ts) ST'" ..
moreover
with hd_stk' less
have "P,h ⊢ hd stk # drop (1+size Ts) stk' [:≤] ST''" by auto
moreover
from wf loc' less have "P,h ⊢ loc' [:≤⇩⊤] LT''" by auto
moreover note suc_pc'
moreover
from f frs' frames
have "P,h,sh ⊢⇩i (C', M', Suc pc', ics')" by auto
ultimately show ?thesis by (simp add: conf_f_def)
qed
with σ' frs' f meth h_ok sh_ok hd_stk Φ_suc frames confc'' meth_C' Φ'
have ?thesis by(fastforce dest: sees_method_fun [of _ C'])
}
moreover
{ assume b[simp]: "b = Static" and nclinit[simp]: "M ≠ clinit"
from f frs' meth ins s'
have σ':
"σ' = (None,h,(hd stk#(drop (size Ts) stk'),loc',C',M',pc'+1,ics')#frs',sh)"
(is "σ' = (None,h,?f'#frs',sh)")
by simp
from f frs' confc conf_clinit_diff have confc'': "conf_clinit P sh (?f'#frs')" by blast
with Φ' meth_C' f frs' frames meth
obtain D Ts' T' m where
ins': "ins' ! pc' = Invokestatic D M (size Ts)" and
meth_D: "P ⊢ D sees M,b: Ts'→T' = m in C" and
T': "P ⊢ T ≤ T'"
by(auto dest: sees_method_fun sees_method_mono2[OF _ wf sees_method_idemp])
from wt_prog meth_C' pc'
have "P,T'',mxs',size ins',xt' ⊢ ins'!pc',pc' :: Φ C' M'"
by (rule wt_jvm_prog_impl_wt_instr)
with ins' Φ' meth_D
obtain ST'' LT'' where
Φ_suc: "Φ C' M' ! Suc pc' = Some (ST'', LT'')" and
less: "P ⊢ (T' # drop (size Ts) ST', LT') ≤⇩i (ST'', LT'')" and
suc_pc': "Suc pc' < size ins'"
by (clarsimp simp: sup_state_opt_any_Some)
from hd_stk T' have hd_stk': "P,h ⊢ hd stk :≤ T'" ..
have frame'':
"conf_f P h sh (ST'',LT'') ins' ?f'"
proof -
from stk'
have "P,h ⊢ drop (size Ts) stk' [:≤] drop (size Ts) ST'" ..
moreover
with hd_stk' less
have "P,h ⊢ hd stk # drop (size Ts) stk' [:≤] ST''" by auto
moreover
from wf loc' less have "P,h ⊢ loc' [:≤⇩⊤] LT''" by auto
moreover note suc_pc'
moreover
from f frs' frames
have "P,h,sh ⊢⇩i (C', M', Suc pc', ics')" by auto
ultimately show ?thesis by (simp add: conf_f_def)
qed
with σ' frs' f meth h_ok sh_ok hd_stk Φ_suc frames confc'' meth_C' Φ'
have ?thesis by(fastforce dest: sees_method_fun [of _ C'])
}
moreover
{ assume b[simp]: "b = Static" and clinit[simp]: "M = clinit"
from frs' meth ins s'
have σ':
"σ' = (None,h,frs,sh(C↦(fst(the(sh C)), Done)))" (is "σ' = (None,h,frs,?sh)")
by simp
from correct have dist': "distinct (C # clinit_classes frs)"
by(simp add: conf_clinit_def distinct_clinit_def)
from f frs' correct have confc1:
"conf_clinit P sh ((stk, loc, C, clinit, pc, No_ics) # (stk',loc',C',M',pc',ics') # frs')"
by simp
then have ics_dist: "distinct (C # ics_classes ics')"
by(simp add: conf_clinit_def distinct_clinit_def)
from conf_clinit_Cons_Cons[OF confc1] have dist'': "distinct (C # clinit_classes frs')"
by(simp add: conf_clinit_def distinct_clinit_def)
from correct shconf_upd_obj[OF sh_ok _ [OF shconfD[OF sh_ok]]]
have sh'_ok: "P,h ⊢⇩s ?sh √" by(clarsimp simp: conf_clinit_def)
have frame'':
"conf_f P h ?sh (ST',LT') ins' f"
proof -
note stk' loc' pc' f valid_ics_shupd[OF _ ics_dist]
moreover
from f frs' frames
have "P,h,sh ⊢⇩i (C', M', pc', ics')" by auto
ultimately show ?thesis by (simp add: conf_f_def2)
qed
have conf_fs': "conf_fs P h ?sh Φ C' M' (length Ts'') T'' frs'"
by(rule conf_fs_shupd[OF conf_fs dist''])
have confc'': "conf_clinit P ?sh frs" by(rule conf_clinit_shupd[OF confc dist'])
from σ' f frs' h_ok sh'_ok conf_fs' frame'' Φ' stk' loc' pc' meth_C' confc''
have ?thesis by(fastforce dest: sees_method_fun)
}
ultimately have ?thesis by (cases b) blast+
}
ultimately
show ?thesis by (cases frs) blast+
qed
declare sup_state_opt_any_Some [iff]
declare not_Err_eq [iff]
lemma Load_correct:
assumes "wf_prog wt P" and
mC: "P ⊢ C sees M,b:Ts→T=(mxs,mxl⇩0,ins,xt) in C" and
i: "ins!pc = Load idx" and
"P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M" and
"Some σ' = exec (P, None, h, (stk,loc,C,M,pc,ics)#frs, sh)" and
cf: "P,Φ ⊢ (None, h, (stk,loc,C,M,pc,ics)#frs, sh)√"
shows "P,Φ |- σ' [ok]"
proof -
have "ics = No_ics" using mC i cf by(cases ics) auto
then show ?thesis using assms(1,3-6) sees_method_fun[OF mC]
by(fastforce elim!: confTs_confT_sup conf_clinit_diff)
qed
declare [[simproc del: list_to_set_comprehension]]
lemma Store_correct:
assumes "wf_prog wt P" and
mC: "P ⊢ C sees M,b:Ts→T=(mxs,mxl⇩0,ins,xt) in C" and
i: "ins!pc = Store idx" and
"P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M" and
"Some σ' = exec (P, None, h, (stk,loc,C,M,pc,ics)#frs, sh)" and
cf: "P,Φ ⊢ (None, h, (stk,loc,C,M,pc,ics)#frs, sh)√"
shows "P,Φ |- σ' [ok]"
proof -
have "ics = No_ics" using mC i cf by(cases ics) auto
then show ?thesis using assms(1,3-6) sees_method_fun[OF mC]
by clarsimp (blast intro!: list_all2_update_cong conf_clinit_diff)
qed
lemma Push_correct:
assumes "wf_prog wt P" and
mC: "P ⊢ C sees M,b:Ts→T=(mxs,mxl⇩0,ins,xt) in C" and
i: "ins!pc = Push v" and
"P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M" and
"Some σ' = exec (P, None, h, (stk,loc,C,M,pc,ics)#frs, sh)" and
cf: "P,Φ ⊢ (None, h, (stk,loc,C,M,pc,ics)#frs, sh)√"
shows "P,Φ |- σ' [ok]"
proof -
have "ics = No_ics" using mC i cf by(cases ics) auto
then show ?thesis using assms(1,3-6) sees_method_fun[OF mC]
by clarsimp (blast dest: typeof_lit_conf conf_clinit_diff)
qed
lemma Cast_conf2:
"⟦ wf_prog ok P; P,h ⊢ v :≤ T; is_refT T; cast_ok P C h v;
P ⊢ Class C ≤ T'; is_class P C⟧
⟹ P,h ⊢ v :≤ T'"
proof -
assume "wf_prog ok P" and "P,h ⊢ v :≤ T" and "is_refT T" and
"cast_ok P C h v" and wid: "P ⊢ Class C ≤ T'" and "is_class P C"
then show "P,h ⊢ v :≤ T'" using Class_widen[OF wid]
by(cases v)
(auto simp: cast_ok_def is_refT_def conf_def obj_ty_def
intro: rtrancl_trans)
qed
lemma Checkcast_correct:
assumes "wf_jvm_prog⇘Φ⇙ P" and
mC: "P ⊢ C sees M,b:Ts→T=(mxs,mxl⇩0,ins,xt) in C" and
i: "ins!pc = Checkcast D" and
"P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M" and
"Some σ' = exec (P, None, h, (stk,loc,C,M,pc,ics)#frs, sh)" and
cf: "P,Φ ⊢ (None, h, (stk,loc,C,M,pc,ics)#frs, sh)√" and
"fst (exec_step P h stk loc C M pc ics frs sh) = None"
shows "P,Φ |- σ' [ok]"
proof -
have "ics = No_ics" using mC i cf by(cases ics) auto
then show ?thesis using assms
by (clarsimp simp: wf_jvm_prog_phi_def split: if_split_asm)
(blast intro: Cast_conf2 dest: sees_method_fun conf_clinit_diff)
qed
declare split_paired_All [simp del]
lemmas widens_Cons [iff] = list_all2_Cons1 [of "widen P"] for P
lemma Getfield_correct:
fixes σ' :: jvm_state
assumes wf: "wf_prog wt P"
assumes mC: "P ⊢ C sees M,b:Ts→T=(mxs,mxl⇩0,ins,xt) in C"
assumes i: "ins!pc = Getfield F D"
assumes wt: "P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M"
assumes s': "Some σ' = exec (P, None, h, (stk,loc,C,M,pc,ics)#frs, sh)"
assumes cf: "P,Φ ⊢ (None, h, (stk,loc,C,M,pc,ics)#frs, sh)√"
assumes xc: "fst (exec_step P h stk loc C M pc ics frs sh) = None"
shows "P,Φ ⊢ σ'√"
proof -
from mC cf i have [simp]: "ics = No_ics" by(cases ics, auto)
from mC cf obtain ST LT where
"h√": "P ⊢ h √" and
"sh√": "P,h ⊢⇩s sh √" and
Φ: "Φ C M ! pc = Some (ST,LT)" and
stk: "P,h ⊢ stk [:≤] ST" and loc: "P,h ⊢ loc [:≤⇩⊤] LT" and
pc: "pc < size ins" and
fs: "conf_fs P h sh Φ C M (size Ts) T frs" and
confc: "conf_clinit P sh ((stk,loc,C,M,pc,ics)#frs)"
by (fastforce dest: sees_method_fun)
from i Φ wt obtain oT ST'' vT ST' LT' vT' where
oT: "P ⊢ oT ≤ Class D" and
ST: "ST = oT # ST''" and
F: "P ⊢ D sees F,NonStatic:vT in D" and
pc': "pc+1 < size ins" and
Φ': "Φ C M ! (pc+1) = Some (vT'#ST', LT')" and
ST': "P ⊢ ST'' [≤] ST'" and LT': "P ⊢ LT [≤⇩⊤] LT'" and
vT': "P ⊢ vT ≤ vT'"
by fastforce
from stk ST obtain ref stk' where
stk': "stk = ref#stk'" and
ref: "P,h ⊢ ref :≤ oT" and
ST'': "P,h ⊢ stk' [:≤] ST''"
by auto
from stk' i mC s' xc have "ref ≠ Null"
by (simp add: split_beta split:if_split_asm)
moreover from ref oT have "P,h ⊢ ref :≤ Class D" ..
ultimately obtain a D' fs where
a: "ref = Addr a" and h: "h a = Some (D', fs)" and D': "P ⊢ D' ≼⇧* D"
by (blast dest: non_npD)
from D' F have has_field: "P ⊢ D' has F,NonStatic:vT in D"
by (blast intro: has_field_mono has_visible_field)
moreover from "h√" h have "P,h ⊢ (D', fs) √" by (rule hconfD)
ultimately obtain v where v: "fs (F, D) = Some v" "P,h ⊢ v :≤ vT"
by (clarsimp simp: oconf_def has_field_def)
(blast dest: has_fields_fun)
from conf_clinit_diff[OF confc]
have confc': "conf_clinit P sh ((v#stk',loc,C,M,pc+1,ics)#frs)" by simp
from a h i mC s' stk' v xc has_field
have "σ' = (None, h, (v#stk',loc,C,M,pc+1,ics)#frs, sh)"
by(simp add: split_beta split: if_split_asm)
moreover
from ST'' ST' have "P,h ⊢ stk' [:≤] ST'" ..
moreover
from v vT' have "P,h ⊢ v :≤ vT'" by blast
moreover
from loc LT' have "P,h ⊢ loc [:≤⇩⊤] LT'" ..
moreover
note "h√" "sh√" mC Φ' pc' v fs confc'
ultimately
show "P,Φ ⊢ σ' √" by fastforce
qed
lemma Getstatic_nInit_correct:
fixes σ' :: jvm_state
assumes wf: "wf_prog wt P"
assumes mC: "P ⊢ C sees M,b:Ts→T=(mxs,mxl⇩0,ins,xt) in C"
assumes i: "ins!pc = Getstatic C' F D"
assumes wt: "P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M"
assumes s': "Some σ' = exec (P, None, h, (stk,loc,C,M,pc,ics)#frs, sh)"
assumes cf: "P,Φ ⊢ (None, h, (stk,loc,C,M,pc,ics)#frs, sh)√"
assumes xc: "fst (exec_step P h stk loc C M pc ics frs sh) = None"
assumes cs: "ics = Called [] ∨ (ics = No_ics ∧ (∃sfs. sh (fst(field P D F)) = Some(sfs, Done)))"
shows "P,Φ ⊢ σ'√"
proof -
from mC cf obtain ST LT where
"h√": "P ⊢ h √" and
"sh√": "P,h ⊢⇩s sh √" and
Φ: "Φ C M ! pc = Some (ST,LT)" and
stk: "P,h ⊢ stk [:≤] ST" and loc: "P,h ⊢ loc [:≤⇩⊤] LT" and
pc: "pc < size ins" and
fs: "conf_fs P h sh Φ C M (size Ts) T frs" and
confc: "conf_clinit P sh ((stk,loc,C,M,pc,ics)#frs)" and
vics: "P,h,sh ⊢⇩i (C,M,pc,ics)"
by (fastforce dest: sees_method_fun)
from i Φ wt cs obtain vT ST' LT' vT' where
F: "P ⊢ C' sees F,Static:vT in D" and
pc': "pc+1 < size ins" and
Φ': "Φ C M ! (pc+1) = Some (vT'#ST', LT')" and
ST': "P ⊢ ST [≤] ST'" and LT': "P ⊢ LT [≤⇩⊤] LT'" and
vT': "P ⊢ vT ≤ vT'"
by fastforce
with mC i vics obtain sobj where
cc': "ics = Called [] ⟹ Called_context P D (ins!pc) ∧ sh D = Some sobj"
by(fastforce dest: has_visible_field)
from field_def2[OF sees_field_idemp[OF F]] have D[simp]: "fst(field P D F) = D" by simp
from cs cc' obtain sfs i where shD: "sh D = Some(sfs,i)" by(cases sobj, auto)
note has_field_idemp[OF has_visible_field[OF F]]
moreover from "sh√" shD have "P,h,D ⊢⇩s sfs √" by (rule shconfD)
ultimately obtain v where v: "sfs F = Some v" "P,h ⊢ v :≤ vT"
by (clarsimp simp: soconf_def has_field_def) blast
from i mC s' v xc F cs cc' shD
have "σ' = (None, h, (v#stk,loc,C,M,pc+1,No_ics)#frs, sh)"
by(fastforce simp: split_beta split: if_split_asm init_call_status.splits)
moreover
from stk ST' have "P,h ⊢ stk [:≤] ST'" ..
moreover
from v vT' have "P,h ⊢ v :≤ vT'" by blast
moreover
from loc LT' have "P,h ⊢ loc [:≤⇩⊤] LT'" ..
moreover
have "conf_clinit P sh ((v#stk,loc,C,M,pc+1,No_ics)#frs)" by(rule conf_clinit_diff'[OF confc])
moreover
note "h√" "sh√" mC Φ' pc' v fs
ultimately
show "P,Φ ⊢ σ' √" by fastforce
qed
lemma Getstatic_Init_correct:
fixes σ' :: jvm_state
assumes wf: "wf_prog wt P"
assumes mC: "P ⊢ C sees M,b:Ts→T=(mxs,mxl⇩0,ins,xt) in C"
assumes i: "ins!pc = Getstatic C' F D"
assumes wt: "P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M"
assumes s': "Some σ' = exec (P, None, h, (stk,loc,C,M,pc,No_ics)#frs, sh)"
assumes cf: "P,Φ ⊢ (None, h, (stk,loc,C,M,pc,No_ics)#frs, sh)√"
assumes xc: "fst (exec_step P h stk loc C M pc No_ics frs sh) = None"
assumes nDone: "∀sfs. sh (fst(field P D F)) ≠ Some(sfs, Done)"
shows "P,Φ ⊢ σ'√"
proof -
from mC cf obtain ST LT where
"h√": "P ⊢ h √" and
"sh√": "P,h ⊢⇩s sh √" and
Φ: "Φ C M ! pc = Some (ST,LT)" and
stk: "P,h ⊢ stk [:≤] ST" and loc: "P,h ⊢ loc [:≤⇩⊤] LT" and
pc: "pc < size ins" and
fs: "conf_fs P h sh Φ C M (size Ts) T frs" and
confc: "conf_clinit P sh ((stk,loc,C,M,pc,No_ics)#frs)"
by (fastforce dest: sees_method_fun)
from i Φ wt nDone obtain vT where
F: "P ⊢ C' sees F,Static:vT in D"
by fastforce
then have has_field: "P ⊢ C' has F,Static:vT in D" by(rule has_visible_field)
from field_def2[OF sees_field_idemp[OF F]] has_field_is_class'[OF has_field] obtain
D[simp]: "fst(field P D F) = D" and
cls: "is_class P D" by simp
from i mC s' xc F nDone
have "σ' = (None, h, (stk,loc,C,M,pc,Calling D [])#frs, sh)"
by(auto simp: split_beta split: if_split_asm init_state.splits)
moreover
from confc have "conf_clinit P sh ((stk,loc,C,M,pc,Calling D [])#frs)"
by(auto simp: conf_clinit_def distinct_clinit_def split: if_split_asm)
moreover
note loc stk "h√" "sh√" mC Φ pc fs i has_field cls
ultimately
show "P,Φ ⊢ σ' √" by fastforce
qed
lemma Putfield_correct:
fixes σ' :: jvm_state
assumes wf: "wf_prog wt P"
assumes mC: "P ⊢ C sees M,b:Ts→T=(mxs,mxl⇩0,ins,xt) in C"
assumes i: "ins!pc = Putfield F D"
assumes wt: "P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M"
assumes s': "Some σ' = exec (P, None, h, (stk,loc,C,M,pc,ics)#frs, sh)"
assumes cf: "P,Φ ⊢ (None, h, (stk,loc,C,M,pc,ics)#frs, sh)√"
assumes xc: "fst (exec_step P h stk loc C M pc ics frs sh) = None"
shows "P,Φ ⊢ σ'√"
proof -
from mC cf i have [simp]: "ics = No_ics" by(cases ics, auto)
from mC cf obtain ST LT where
"h√": "P ⊢ h √" and
"sh√": "P,h ⊢⇩s sh √" and
Φ: "Φ C M ! pc = Some (ST,LT)" and
stk: "P,h ⊢ stk [:≤] ST" and loc: "P,h ⊢ loc [:≤⇩⊤] LT" and
pc: "pc < size ins" and
fs: "conf_fs P h sh Φ C M (size Ts) T frs" and
confc: "conf_clinit P sh ((stk,loc,C,M,pc,ics) # frs)"
by (fastforce dest: sees_method_fun)
from i Φ wt obtain vT vT' oT ST'' ST' LT' where
ST: "ST = vT # oT # ST''" and
field: "P ⊢ D sees F,NonStatic:vT' in D" and
oT: "P ⊢ oT ≤ Class D" and vT: "P ⊢ vT ≤ vT'" and
pc': "pc+1 < size ins" and
Φ': "Φ C M!(pc+1) = Some (ST',LT')" and
ST': "P ⊢ ST'' [≤] ST'" and LT': "P ⊢ LT [≤⇩⊤] LT'"
by clarsimp
from stk ST obtain v ref stk' where
stk': "stk = v#ref#stk'" and
v: "P,h ⊢ v :≤ vT" and
ref: "P,h ⊢ ref :≤ oT" and
ST'': "P,h ⊢ stk' [:≤] ST''"
by auto
from stk' i mC s' xc have "ref ≠ Null" by (auto simp: split_beta)
moreover from ref oT have "P,h ⊢ ref :≤ Class D" ..
ultimately obtain a D' fs where
a: "ref = Addr a" and h: "h a = Some (D', fs)" and D': "P ⊢ D' ≼⇧* D"
by (blast dest: non_npD)
from v vT have vT': "P,h ⊢ v :≤ vT'" ..
from field D' have has_field: "P ⊢ D' has F,NonStatic:vT' in D"
by (blast intro: has_field_mono has_visible_field)
let ?h' = "h(a↦(D', fs((F, D)↦v)))" and ?f' = "(stk',loc,C,M,pc+1,ics)"
from h have hext: "h ⊴ ?h'" by (rule hext_upd_obj)
have "sh√'": "P,?h' ⊢⇩s sh √" by(rule shconf_hupd_obj[OF "sh√" h])
from a h i mC s' stk' has_field field
have "σ' = (None, ?h', ?f'#frs, sh)" by(simp split: if_split_asm)
moreover
from "h√" h have "P,h ⊢ (D',fs)√" by (rule hconfD)
with has_field vT' have "P,h ⊢ (D',fs((F, D)↦v))√" ..
with "h√" h have "P ⊢ ?h'√" by (rule hconf_upd_obj)
moreover
from ST'' ST' have "P,h ⊢ stk' [:≤] ST'" ..
from this hext have "P,?h' ⊢ stk' [:≤] ST'" by (rule confs_hext)
moreover
from loc LT' have "P,h ⊢ loc [:≤⇩⊤] LT'" ..
from this hext have "P,?h' ⊢ loc [:≤⇩⊤] LT'" by (rule confTs_hext)
moreover
from fs hext
have "conf_fs P ?h' sh Φ C M (size Ts) T frs" by (rule conf_fs_hext)
moreover
have "conf_clinit P sh (?f' # frs)" by(rule conf_clinit_diff[OF confc])
moreover
note mC Φ' pc' "sh√'"
ultimately
show "P,Φ ⊢ σ' √" by fastforce
qed
lemma Putstatic_nInit_correct:
fixes σ' :: jvm_state
assumes wf: "wf_prog wt P"
assumes mC: "P ⊢ C sees M,b:Ts→T=(mxs,mxl⇩0,ins,xt) in C"
assumes i: "ins!pc = Putstatic C' F D"
assumes wt: "P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M"
assumes s': "Some σ' = exec (P, None, h, (stk,loc,C,M,pc,ics)#frs, sh)"
assumes cf: "P,Φ ⊢ (None, h, (stk,loc,C,M,pc,ics)#frs, sh)√"
assumes xc: "fst (exec_step P h stk loc C M pc ics frs sh) = None"
assumes cs: "ics = Called [] ∨ (ics = No_ics ∧ (∃sfs. sh (fst(field P D F)) = Some(sfs, Done)))"
shows "P,Φ ⊢ σ'√"
proof -
from mC cf obtain ST LT where
"h√": "P ⊢ h √" and
"sh√": "P,h ⊢⇩s sh √" and
Φ: "Φ C M ! pc = Some (ST,LT)" and
stk: "P,h ⊢ stk [:≤] ST" and loc: "P,h ⊢ loc [:≤⇩⊤] LT" and
pc: "pc < size ins" and
fs: "conf_fs P h sh Φ C M (size Ts) T frs" and
confc: "conf_clinit P sh ((stk,loc,C,M,pc,ics)#frs)" and
vics: "P,h,sh ⊢⇩i (C,M,pc,ics)"
by (fastforce dest: sees_method_fun)
from i Φ wt cs obtain vT vT' ST'' ST' LT' where
ST: "ST = vT # ST''" and
F: "P ⊢ C' sees F,Static:vT' in D" and
vT: "P ⊢ vT ≤ vT'" and
pc': "pc+1 < size ins" and
Φ': "Φ C M ! (pc+1) = Some (ST', LT')" and
ST': "P ⊢ ST'' [≤] ST'" and LT': "P ⊢ LT [≤⇩⊤] LT'"
by fastforce
from stk ST obtain v stk' where
stk': "stk = v#stk'" and
v: "P,h ⊢ v :≤ vT" and
ST'': "P,h ⊢ stk' [:≤] ST''"
by auto
from v vT have vT': "P,h ⊢ v :≤ vT'" ..
with mC i vics obtain sobj where
cc': "ics = Called [] ⟹ Called_context P D (ins!pc) ∧ sh D = Some sobj"
by(fastforce dest: has_visible_field)
from field_def2[OF sees_field_idemp[OF F]] have D[simp]: "fst(field P D F) = D" by simp
from cs cc' obtain sfs i where shD: "sh D = Some(sfs,i)" by(cases sobj, auto)
let ?sh' = "sh(D↦(sfs(F↦v),i))" and ?f' = "(stk',loc,C,M,pc+1,No_ics)"
have m_D: "P ⊢ D has F,Static:vT' in D" by (rule has_field_idemp[OF has_visible_field[OF F]])
from "sh√" shD have sfs: "P,h,D ⊢⇩s sfs √" by (rule shconfD)
have "sh'√": "P,h ⊢⇩s ?sh' √" by (rule shconf_upd_obj[OF "sh√" soconf_fupd[OF m_D vT' sfs]])
from i mC s' v xc F cs cc' shD stk'
have "σ' = (None, h, (stk',loc,C,M,pc+1,No_ics)#frs, ?sh')"
by(fastforce simp: split_beta split: if_split_asm init_call_status.splits)
moreover
from ST'' ST' have "P,h ⊢ stk' [:≤] ST'" ..
moreover
from loc LT' have "P,h ⊢ loc [:≤⇩⊤] LT'" ..
moreover
have "conf_fs P h ?sh' Φ C M (size Ts) T frs" by (rule conf_fs_shupd'[OF fs shD])
moreover
have "conf_clinit P ?sh' ((stk',loc,C,M,pc+1,No_ics)#frs)"
by(rule conf_clinit_diff'[OF conf_clinit_shupd'[OF confc shD]])
moreover
note "h√" "sh'√" mC Φ' pc' v vT'
ultimately
show "P,Φ ⊢ σ' √" by fastforce
qed
lemma Putstatic_Init_correct:
fixes σ' :: jvm_state
assumes wf: "wf_prog wt P"
assumes mC: "P ⊢ C sees M,b:Ts→T=(mxs,mxl⇩0,ins,xt) in C"
assumes i: "ins!pc = Putstatic C' F D"
assumes wt: "P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M"
assumes s': "Some σ' = exec (P, None, h, (stk,loc,C,M,pc,No_ics)#frs, sh)"
assumes cf: "P,Φ ⊢ (None, h, (stk,loc,C,M,pc,No_ics)#frs, sh)√"
assumes xc: "fst (exec_step P h stk loc C M pc No_ics frs sh) = None"
assumes nDone: "∀sfs. sh (fst(field P D F)) ≠ Some(sfs, Done)"
shows "P,Φ ⊢ σ'√"
proof -
from mC cf obtain ST LT where
"h√": "P ⊢ h √" and
"sh√": "P,h ⊢⇩s sh √" and
Φ: "Φ C M ! pc = Some (ST,LT)" and
stk: "P,h ⊢ stk [:≤] ST" and loc: "P,h ⊢ loc [:≤⇩⊤] LT" and
pc: "pc < size ins" and
fs: "conf_fs P h sh Φ C M (size Ts) T frs" and
confc: "conf_clinit P sh ((stk,loc,C,M,pc,No_ics)#frs)"
by (fastforce dest: sees_method_fun)
from i Φ wt nDone obtain vT where
F: "P ⊢ C' sees F,Static:vT in D"
by fastforce
then have has_field: "P ⊢ C' has F,Static:vT in D" by(rule has_visible_field)
from field_def2[OF sees_field_idemp[OF F]] has_field_is_class'[OF has_field] obtain
D[simp]: "fst(field P D F) = D" and
cls: "is_class P D" by simp
from i mC s' xc F nDone
have "σ' = (None, h, (stk,loc,C,M,pc,Calling D [])#frs, sh)"
by(auto simp: split_beta split: if_split_asm init_state.splits)
moreover
from confc have "conf_clinit P sh ((stk,loc,C,M,pc,Calling D [])#frs)"
by(auto simp: conf_clinit_def distinct_clinit_def split: if_split_asm)
moreover
note loc stk "h√" "sh√" mC Φ pc fs i has_field cls
ultimately
show "P,Φ ⊢ σ' √" by fastforce
qed
lemma oconf_blank2 [intro, simp]:
"⟦is_class P C; wf_prog wt P⟧ ⟹ P,h ⊢ blank P C √"
by (fastforce simp: oconf_blank dest: wf_Fields_Ex)
lemma obj_ty_blank [iff]: "obj_ty (blank P C) = Class C"
by (simp add: blank_def)
lemma New_nInit_correct:
fixes σ' :: jvm_state
assumes wf: "wf_prog wt P"
assumes meth: "P ⊢ C sees M,b:Ts→T=(mxs,mxl⇩0,ins,xt) in C"
assumes ins: "ins!pc = New X"
assumes wt: "P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M"
assumes exec: "Some σ' = exec (P, None, h, (stk,loc,C,M,pc,ics)#frs, sh)"
assumes conf: "P,Φ ⊢ (None, h, (stk,loc,C,M,pc,ics)#frs, sh)√"
assumes no_x: "fst (exec_step P h stk loc C M pc ics frs sh) = None"
assumes cs: "ics = Called [] ∨ (ics = No_ics ∧ (∃sfs. sh X = Some(sfs, Done)))"
shows "P,Φ ⊢ σ'√"
proof -
from ins conf meth
obtain ST LT where
heap_ok: "P⊢ h√" and
sheap_ok: "P,h ⊢⇩s sh √" and
Φ_pc: "Φ C M!pc = Some (ST,LT)" and
frame: "conf_f P h sh (ST,LT) ins (stk,loc,C,M,pc,ics)" and
frames: "conf_fs P h sh Φ C M (size Ts) T frs" and
confc: "conf_clinit P sh ((stk,loc,C,M,pc,ics) # frs)"
by (auto dest: sees_method_fun)
from Φ_pc ins wt
obtain ST' LT' where
is_class_X: "is_class P X" and
mxs: "size ST < mxs" and
suc_pc: "pc+1 < size ins" and
Φ_suc: "Φ C M!(pc+1) = Some (ST', LT')" and
less: "P ⊢ (Class X # ST, LT) ≤⇩i (ST', LT')"
by auto
from ins no_x cs meth obtain oref where new_Addr: "new_Addr h = Some oref" by auto
hence h: "h oref = None" by (rule new_Addr_SomeD)
with exec ins meth new_Addr cs have σ':
"σ' = (None, h(oref ↦ blank P X), (Addr oref#stk,loc,C,M,pc+1,No_ics)#frs, sh)"
(is "σ' = (None, ?h', ?f # frs, sh)")
by auto
moreover
from wf h heap_ok is_class_X have h': "P ⊢ ?h' √"
by (auto intro: hconf_new)
moreover
from h frame less suc_pc wf
have "conf_f P ?h' sh (ST', LT') ins ?f"
by (clarsimp simp: fun_upd_apply conf_def blank_def split_beta)
(auto intro: confs_hext confTs_hext)
moreover
from h have "h ⊴ ?h'" by simp
with frames have "conf_fs P ?h' sh Φ C M (size Ts) T frs" by (rule conf_fs_hext)
moreover
have "P,?h' ⊢⇩s sh √" by(rule shconf_hnew[OF sheap_ok h])
moreover
have "conf_clinit P sh (?f # frs)" by(rule conf_clinit_diff'[OF confc])
ultimately
show ?thesis using meth Φ_suc by fastforce
qed
lemma New_Init_correct:
fixes σ' :: jvm_state
assumes wf: "wf_prog wt P"
assumes meth: "P ⊢ C sees M,b:Ts→T=(mxs,mxl⇩0,ins,xt) in C"
assumes ins: "ins!pc = New X"
assumes wt: "P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M"
assumes exec: "Some σ' = exec (P, None, h, (stk,loc,C,M,pc,No_ics)#frs, sh)"
assumes conf: "P,Φ ⊢ (None, h, (stk,loc,C,M,pc,No_ics)#frs, sh)√"
assumes no_x: "fst (exec_step P h stk loc C M pc No_ics frs sh) = None"
assumes nDone: "∀sfs. sh X ≠ Some(sfs, Done)"
shows "P,Φ ⊢ σ'√"
proof -
from ins conf meth
obtain ST LT where
heap_ok: "P⊢ h√" and
sheap_ok: "P,h ⊢⇩s sh √" and
Φ_pc: "Φ C M!pc = Some (ST,LT)" and
frame: "conf_f P h sh (ST,LT) ins (stk,loc,C,M,pc,No_ics)" and
frames: "conf_fs P h sh Φ C M (size Ts) T frs" and
confc: "conf_clinit P sh ((stk,loc,C,M,pc,No_ics) # frs)"
by (auto dest: sees_method_fun)
from Φ_pc ins wt
obtain ST' LT' where
is_class_X: "is_class P X" and
mxs: "size ST < mxs" and
suc_pc: "pc+1 < size ins" and
Φ_suc: "Φ C M!(pc+1) = Some (ST', LT')" and
less: "P ⊢ (Class X # ST, LT) ≤⇩i (ST', LT')"
by auto
with exec ins meth nDone have σ':
"σ' = (None, h, (stk,loc,C,M,pc,Calling X [])#frs, sh)"
(is "σ' = (None, h, ?f # frs, sh)")
by(auto split: init_state.splits)
moreover
from meth frame is_class_X ins
have "conf_f P h sh (ST, LT) ins ?f" by auto
moreover note heap_ok sheap_ok frames
moreover
from confc have "conf_clinit P sh (?f # frs)"
by(auto simp: conf_clinit_def distinct_clinit_def split: if_split_asm)
ultimately
show ?thesis using meth Φ_pc by fastforce
qed
lemma Goto_correct:
assumes "wf_prog wt P" and
mC: "P ⊢ C sees M,b:Ts→T=(mxs,mxl⇩0,ins,xt) in C" and
i: "ins!pc = Goto branch" and
"P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M" and
"Some σ' = exec (P, None, h, (stk,loc,C,M,pc,ics)#frs, sh)" and
cf: "P,Φ ⊢ (None, h, (stk,loc,C,M,pc,ics)#frs, sh)√"
shows "P,Φ |- σ' [ok]"
proof -
have "ics = No_ics" using mC i cf by(cases ics) auto
then show ?thesis using assms(1,3-6) sees_method_fun[OF mC]
by(fastforce elim!: conf_clinit_diff)
qed
lemma IfFalse_correct:
assumes "wf_prog wt P" and
mC: "P ⊢ C sees M,b:Ts→T=(mxs,mxl⇩0,ins,xt) in C" and
i: "ins!pc = IfFalse branch" and
"P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M" and
"Some σ' = exec (P, None, h, (stk,loc,C,M,pc,ics)#frs, sh)" and
cf: "P,Φ ⊢ (None, h, (stk,loc,C,M,pc,ics)#frs, sh)√"
shows "P,Φ |- σ' [ok]"
proof -
have "ics = No_ics" using mC i cf by(cases ics) auto
then show ?thesis using assms(1,3-6) sees_method_fun[OF mC]
by(fastforce elim!: conf_clinit_diff)
qed
lemma CmpEq_correct:
assumes "wf_prog wt P" and
mC: "P ⊢ C sees M,b:Ts→T=(mxs,mxl⇩0,ins,xt) in C" and
i: "ins!pc = CmpEq" and
"P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M" and
"Some σ' = exec (P, None, h, (stk,loc,C,M,pc,ics)#frs, sh)" and
cf: "P,Φ ⊢ (None, h, (stk,loc,C,M,pc,ics)#frs, sh)√"
shows "P,Φ |- σ' [ok]"
proof -
have "ics = No_ics" using mC i cf by(cases ics) auto
then show ?thesis using assms(1,3-6) sees_method_fun[OF mC]
by(fastforce elim!: conf_clinit_diff)
qed
lemma Pop_correct:
assumes "wf_prog wt P" and
mC: "P ⊢ C sees M,b:Ts→T=(mxs,mxl⇩0,ins,xt) in C" and
i: "ins!pc = Pop" and
"P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M" and
"Some σ' = exec (P, None, h, (stk,loc,C,M,pc,ics)#frs, sh)" and
cf: "P,Φ ⊢ (None, h, (stk,loc,C,M,pc,ics)#frs, sh)√"
shows "P,Φ |- σ' [ok]"
proof -
have "ics = No_ics" using mC i cf by(cases ics) auto
then show ?thesis using assms(1,3-6) sees_method_fun[OF mC]
by(fastforce elim!: conf_clinit_diff)
qed
lemma IAdd_correct:
assumes "wf_prog wt P" and
mC: "P ⊢ C sees M,b:Ts→T=(mxs,mxl⇩0,ins,xt) in C" and
i: "ins!pc = IAdd" and
"P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M" and
"Some σ' = exec (P, None, h, (stk,loc,C,M,pc,ics)#frs, sh)" and
cf: "P,Φ ⊢ (None, h, (stk,loc,C,M,pc,ics)#frs, sh)√"
shows "P,Φ |- σ' [ok]"
proof -
have "ics = No_ics" using mC i cf by(cases ics) auto
then show ?thesis using assms(1,3-6) sees_method_fun[OF mC]
by(fastforce elim!: conf_clinit_diff)
qed
lemma Throw_correct:
assumes "wf_prog wt P" and
mC: "P ⊢ C sees M,b:Ts→T=(mxs,mxl⇩0,ins,xt) in C" and
i: "ins!pc = Throw" and
"Some σ' = exec (P, None, h, (stk,loc,C,M,pc,ics)#frs, sh)" and
cf: "P,Φ ⊢ (None, h, (stk,loc,C,M,pc,ics)#frs, sh)√" and
"fst (exec_step P h stk loc C M pc ics frs sh) = None"
shows "P,Φ |- σ' [ok]"
proof -
have "ics = No_ics" using mC i cf by(cases ics) auto
then show ?thesis using assms by simp
qed
text ‹
The next theorem collects the results of the sections above,
i.e.~exception handling, initialization procedure steps, 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
step of execution is performed.
›
lemma step_correct:
fixes σ' :: jvm_state
assumes wtp: "wf_jvm_prog⇘Φ⇙ P"
and meth: "P ⊢ C sees M,b:Ts→T=(mxs,mxl⇩0,ins,xt) in C"
and exec: "Some σ' = exec (P, None, h, (stk,loc,C,M,pc,ics)#frs, sh)"
and conf: "P,Φ ⊢ (None, h, (stk,loc,C,M,pc,ics)#frs, sh)√"
shows "P,Φ ⊢ σ'√"
proof -
from assms have pc: "pc < length ins" by(auto dest: sees_method_fun)
with wt_jvm_prog_impl_wt_instr[OF wtp meth] have wt: "P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M"
by simp
from conf obtain ST LT where Φ: "Φ C M ! pc = Some(ST,LT)" by clarsimp
show ?thesis
proof(cases "fst (exec_step P h stk loc C M pc ics frs sh)")
case Some show ?thesis by(rule xcpt_correct[OF wtp meth wt Some exec conf])
next
case None
from wt_jvm_progD[OF wtp] obtain wf_md where wf: "wf_prog wf_md P" by clarify
{ assume [simp]: "ics = No_ics"
from exec conf None obtain
exec': "Some σ' = exec (P, None, h, (stk,loc,C,M,pc,No_ics)#frs, sh)"
and conf': "P,Φ ⊢ (None, h, (stk,loc,C,M,pc,No_ics)#frs, sh)√"
and None': "fst (exec_step P h stk loc C M pc No_ics frs sh) = None" by simp
have ?thesis
proof(cases "ins!pc")
case Load from Load_correct[OF wf meth this wt exec conf] show ?thesis by simp
next
case Store from Store_correct[OF wf meth this wt exec conf] show ?thesis by simp
next
case Push from Push_correct[OF wf meth this wt exec conf] show ?thesis by simp
next
case (New C) show ?thesis
proof(cases "∃sfs. sh C = Some(sfs, Done)")
case True
with New_nInit_correct[OF wf meth New wt exec conf None] show ?thesis by simp
next
case False
with New_Init_correct[OF wf meth New wt exec' conf' None'] show ?thesis by simp
qed
next
case Getfield from Getfield_correct[OF wf meth this wt exec conf None]
show ?thesis by simp
next
case (Getstatic C F D) show ?thesis
proof(cases "∃sfs. sh (fst (field P D F)) = Some(sfs, Done)")
case True
with Getstatic_nInit_correct[OF wf meth Getstatic wt exec conf None] show ?thesis by simp
next
case False
with Getstatic_Init_correct[OF wf meth Getstatic wt exec' conf' None']
show ?thesis by simp
qed
next
case Putfield from Putfield_correct[OF wf meth this wt exec conf None]
show ?thesis by simp
next
case (Putstatic C F D) show ?thesis
proof(cases "∃sfs. sh (fst (field P D F)) = Some(sfs, Done)")
case True
with Putstatic_nInit_correct[OF wf meth Putstatic wt exec conf None] show ?thesis by simp
next
case False
with Putstatic_Init_correct[OF wf meth Putstatic wt exec' conf' None']
show ?thesis by simp
qed
next
case Checkcast from Checkcast_correct[OF wtp meth this wt exec conf None]
show ?thesis by simp
next
case Invoke with Invoke_correct[OF wtp meth this wt exec conf None] show ?thesis by simp
next
case (Invokestatic C M n)
from wf_jvm_prog_nclinit[OF wtp meth wt pc Φ this] have ncl: "M ≠ clinit" by simp
show ?thesis
proof(cases "∃sfs. sh (fst (method P C M)) = Some(sfs, Done)")
case True
with Invokestatic_nInit_correct[OF wtp meth Invokestatic ncl wt exec conf None]
show ?thesis by simp
next
case False
with Invokestatic_Init_correct[OF wtp meth Invokestatic ncl wt exec' conf' None']
show ?thesis by simp
qed
next
case Return with Return_correct[OF wtp meth this wt exec conf] show ?thesis by simp
next
case Pop with Pop_correct[OF wf meth this wt exec conf] show ?thesis by simp
next
case IAdd with IAdd_correct[OF wf meth this wt exec conf] show ?thesis by simp
next
case Goto with Goto_correct[OF wf meth this wt exec conf] show ?thesis by simp
next
case CmpEq with CmpEq_correct[OF wf meth this wt exec conf] show ?thesis by simp
next
case IfFalse with IfFalse_correct[OF wf meth this wt exec conf] show ?thesis by simp
next
case Throw with Throw_correct[OF wf meth this exec conf None] show ?thesis by simp
qed
}
moreover
{ fix Cs assume [simp]: "ics = Called Cs"
have ?thesis
proof(cases Cs)
case [simp]: Nil
from conf meth obtain C1 where "Called_context P C1 (ins ! pc)"
by(clarsimp simp: conf_f_def2 intro!: Called_context_Called_set)
then have "ins!pc ∈ Called_set" by(rule Called_context_Called_set)
then show ?thesis
proof(cases "ins!pc")
case (New C)
from New_nInit_correct[OF wf meth this wt exec conf None] show ?thesis by simp
next
case (Getstatic C F D)
from Getstatic_nInit_correct[OF wf meth this wt exec conf None] show ?thesis by simp
next
case (Putstatic C F D)
from Putstatic_nInit_correct[OF wf meth this wt exec conf None] show ?thesis by simp
next
case (Invokestatic C M n)
from wf_jvm_prog_nclinit[OF wtp meth wt pc Φ this] have ncl: "M ≠ clinit" by simp
with Invokestatic_nInit_correct[OF wtp meth Invokestatic ncl wt exec conf None]
show ?thesis by simp
qed(simp_all)
next
case (Cons C' Cs') with Called_correct[OF wtp meth exec conf None] show ?thesis by simp
qed
}
moreover
{ fix C' Cs assume [simp]: "ics = Calling C' Cs"
with Calling_correct[OF wtp meth exec conf None] have ?thesis by simp
}
moreover
{ fix Cs a assume [simp]: "ics = Throwing Cs a"
have ?thesis
proof(cases Cs)
case Nil with exec None show ?thesis by simp
next
case (Cons C' Cs')
with Throwing_correct[OF wtp meth exec conf None] show ?thesis by simp
qed
}
ultimately show ?thesis by(cases ics) auto
qed
qed
subsection ‹ Main ›
lemma correct_state_impl_Some_method:
"P,Φ ⊢ (None, h, (stk,loc,C,M,pc,ics)#frs, sh)√
⟹ ∃b m Ts T. P ⊢ C sees M,b:Ts→T = m in C"
by fastforce
lemma BV_correct_1 [rule_format]:
"⋀σ. ⟦ wf_jvm_prog⇘Φ⇙ P; P,Φ ⊢ σ√⟧ ⟹ P ⊢ σ -jvm→⇩1 σ' ⟶ P,Φ ⊢ σ'√"
proof -
fix σ assume wf: "wf_jvm_prog⇘Φ⇙ P" and cf: "P,Φ ⊢ σ√"
obtain xp h frs sh where σ[simp]: "σ = (xp, h, frs, sh)" by(cases σ) simp
have "exec (P, xp, h, frs, sh) = ⌊σ'⌋ ⟶ P,Φ |- σ' [ok]"
proof(cases xp)
case None
with wf cf show ?thesis
proof(cases frs)
case (Cons fr frs')
obtain stk loc C M pc ics where [simp]: "fr = (stk,loc,C,M,pc,ics)" by(cases fr) simp
then have cf': "P,Φ |- (None, h, (stk,loc,C,M,pc,ics) # frs', sh) [ok]"
using Cons None cf by simp
then obtain b mxs mxl⇩0 ins xt Ts T
where mC: "P ⊢ C sees M, b : Ts→T = (mxs, mxl⇩0, ins, xt) in C"
using correct_state_impl_Some_method[OF cf'] by clarify
show ?thesis using Cons None step_correct[OF wf mC _ cf'] by simp
qed simp
next
case (Some a)
then show ?thesis using wf cf by (case_tac frs) simp_all
qed
then show "P ⊢ σ -jvm→⇩1 σ' ⟶ P,Φ ⊢ σ'√" by(simp add: exec_1_iff)
qed
theorem progress:
"⟦ xp=None; frs≠[] ⟧ ⟹ ∃σ'. P ⊢ (xp,h,frs,sh) -jvm→⇩1 σ'"
by (clarsimp simp: exec_1_iff neq_Nil_conv split_beta
simp del: split_paired_Ex)
lemma progress_conform:
"⟦wf_jvm_prog⇘Φ⇙ P; P,Φ ⊢ (xp,h,frs,sh)√; xp=None; frs≠[]⟧
⟹ ∃σ'. P ⊢ (xp,h,frs,sh) -jvm→⇩1 σ' ∧ P,Φ ⊢ σ'√"
by (drule (1) progress) (fast intro: BV_correct_1)
theorem BV_correct [rule_format]:
"⟦ wf_jvm_prog⇘Φ⇙ P; P ⊢ σ -jvm→ σ' ⟧ ⟹ P,Φ ⊢ σ√ ⟶ P,Φ ⊢ σ'√"
proof -
assume wf: "wf_jvm_prog⇘Φ⇙ P" and "P ⊢ σ -jvm→ σ'"
then have "(σ, σ') ∈ (exec_1 P)⇧*" by (simp only: exec_all_def1)
then show ?thesis proof(induct rule: rtrancl_induct)
case (step y z)
then show ?case by clarify (erule (1) BV_correct_1[OF wf])
qed simp
qed
lemma hconf_start:
assumes wf: "wf_prog wf_mb P"
shows "P ⊢ (start_heap P) √"
proof -
{ fix a obj assume assm: "start_heap P a = ⌊obj⌋"
have "P,start_heap P ⊢ obj √" using wf assm[THEN sym]
by (unfold start_heap_def)
(auto simp: fun_upd_apply is_class_xcpt split: if_split_asm)
}
then show ?thesis using preallocated_start[of P]
by (unfold hconf_def) simp
qed
lemma shconf_start:
"¬ is_class P Start ⟹ P,start_heap P ⊢⇩s start_sheap √"
by (unfold shconf_def)
(clarsimp simp: preallocated_start fun_upd_apply soconf_def has_field_is_class)
lemma BV_correct_initial:
assumes wf: "wf_jvm_prog⇘Φ⇙ P"
and nStart: "¬is_class P Start"
and mC: "P ⊢ C sees M,Static:[]→Void = m in C"
and nclinit: "M ≠ clinit"
and Φ: "Φ' Start start_m = start_φ⇩m"
shows "start_prog P C M,Φ' ⊢ start_state P √"
proof -
let ?P = "class_add P (start_class C M)"
let ?h = "start_heap P" and ?sh = "[Start ↦ (Map.empty, Done)]"
let ?C = Start and ?M = start_m and ?pc = 0 and ?ics = No_ics
let ?f = "([], [], ?C, ?M, ?pc, ?ics)" and ?fs = "[]"
let ?frs = "?f#?fs"
have "is_class P Object" using wf by(simp add: wf_jvm_prog_phi_def)
then obtain Mm where Mm: "P ⊢ Object sees_methods Mm"
by(fastforce simp: is_class_def dest: sees_methods_Object)
obtain mxs mxl⇩0 ins xt where
mC': "P ⊢ C sees M,Static:[]→Void = (mxs,mxl⇩0,ins,xt) in C"
using mC by (cases m) simp
have "?P⊢ ?h√" using wf nStart class_add_hconf_wf[OF _ hconf_start]
by (simp add: wf_jvm_prog_phi_def start_heap_nStart)
moreover have "?P,?h⊢⇩s ?sh√" by(rule start_prog_start_shconf)
moreover have "conf_clinit ?P ?sh ?frs"
by(simp add: conf_clinit_def distinct_clinit_def)
moreover have "∃b Ts T mxs mxl⇩0 is xt τ.
(?P ⊢ ?C sees ?M,b:Ts→T = (mxs,mxl⇩0,is,xt) in ?C)
∧ Φ' ?C ?M ! ?pc = Some τ
∧ conf_f ?P ?h ?sh τ is ?f ∧ conf_fs ?P ?h ?sh Φ' ?C ?M (size Ts) T ?fs"
using Φ start_prog_Start_sees_start_method[OF Mm]
by (unfold conf_f_def wt_start_def) fastforce
ultimately show ?thesis
by (simp del: defs1 add: start_state_def correct_state_def)
qed
declare [[simproc add: list_to_set_comprehension]]
theorem typesafe:
assumes welltyped: "wf_jvm_prog⇘Φ⇙ P"
assumes nstart: "¬ is_class P Start"
assumes main_method: "P ⊢ C sees M,Static:[]→Void = m in C"
assumes nclinit: "M ≠ clinit"
assumes Φ: "⋀C. C ≠ Start ⟹ Φ' C = Φ C"
assumes Φ': "Φ' Start start_m = start_φ⇩m" "Φ' Start clinit = start_φ⇩m"
assumes Obj_start_m:
"(⋀b' Ts' T' m' D'. P ⊢ Object sees start_m, b' : Ts'→T' = m' in D'
⟹ b' = Static ∧ Ts' = [] ∧ T' = Void)"
shows "start_prog P C M ⊢ start_state P -jvm→ σ ⟹ start_prog P C M,Φ' ⊢ σ √"
proof -
from welltyped nstart main_method nclinit Φ'(1)
have "start_prog P C M,Φ' ⊢ start_state P √" by (rule BV_correct_initial)
moreover
assume "start_prog P C M ⊢ start_state P -jvm→ σ"
moreover
from start_prog_wf_jvm_prog_phi[OF welltyped nstart main_method nclinit Φ Φ' Obj_start_m]
have "wf_jvm_prog⇘Φ'⇙(start_prog P C M)" by simp
ultimately
show "start_prog P C M,Φ' ⊢ σ √" using welltyped by - (rule BV_correct)
qed
end