Theory BVSpecTypeSafe
section ‹BV Type Safety Proof \label{sec:BVSpecTypeSafe}›
theory BVSpecTypeSafe
imports BVConform
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 ‹Invoke› instruction the BV has checked all handlers
that guard the current ‹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 add: 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 (‹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.
› term find_handler
lemma uncaught_xcpt_correct:
assumes wt: "wf_jvm_prog⇘Φ⇙ P"
assumes h: "h xcp = Some obj"
shows "⋀f. P,Φ ⊢ (None, h, f#frs)√ ⟹ P,Φ ⊢ (find_handler P xcp h frs) √"
(is "⋀f. ?correct (None, h, f#frs) ⟹ ?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')"
assume IH: "⋀f. ?correct (None, h, f#frs') ⟹ ?correct (?find frs')"
from cr have cr': "?correct (None, h, f'#frs')"
by (fastforce simp add: correct_state_def)
obtain stk loc C M pc where [simp]: "f' = (stk,loc,C,M,pc)" by (cases f')
from cr obtain Ts T mxs mxl⇩0 ins xt where
meth: "P ⊢ C sees M:Ts → T = (mxs,mxl⇩0,ins,xt) in C"
by (simp add: correct_state_def, blast)
hence [simp]: "ex_table_of P C M = xt" by simp
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 by fastforce
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 add: correct_state_def conf_f_def
dest: sees_method_fun
elim!: wt_jvm_prog_impl_wt_instr)
from cr meth
obtain n M' ST LT where
ins: "ins!pc = Invoke n M'" (is "_ = ?i") and
Φ: "Φ C M ! pc = Some (ST, LT)"
by (fastforce dest: sees_method_fun simp add: correct_state_def)
from ins match obtain f t D where
rel: "(f,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)
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 add: xcpt_eff_def image_def)
with wti Φ obtain
pc: "pc' < size ins" and
"P ⊢ Some (?ST', LT) ≤' Φ C M ! pc'"
by (clarsimp simp add: defs1) blast
then obtain ST' LT' where
Φ': "Φ C M ! pc' = Some (ST',LT')" and
less: "P ⊢ (?ST', LT) ≤⇩i (ST',LT')"
by (auto simp add: sup_state_opt_any_Some)
from cr' Φ meth have "conf_f P h (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)
let ?f = "(Addr xcp # drop (length stk - d') stk, loc, C, M, pc')"
have "conf_f P h (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 by (simp add: conf_f_def)
qed
with cr' match Φ' meth pc
show ?thesis by (unfold correct_state_def) (fastforce dest: sees_method_fun)
qed
qed
text ‹
The requirement of lemma ‹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 Cl M pc frs) = Some xcp;
P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M;
P,Φ ⊢ (None, h, (stk,loc,C,M,pc)#frs)√ ⟧
⟹ ∃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 pre show ?thesis
proof (cases "ins!pc")
case Throw with xcpt wt pre show ?thesis
by (clarsimp iff: list_all2_Cons2 simp add: defs1)
(auto dest: non_npD simp: is_refT_def elim: preallocatedE)
qed (auto elim: preallocatedE)
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: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_instr (ins!pc) P h stk loc C M pc frs) = Some xcp"
assumes s': "Some σ' = exec (P, None, h, (stk,loc,C,M,pc)#frs)"
assumes correct: "P,Φ ⊢ (None, h, (stk,loc,C,M,pc)#frs)√"
shows "P,Φ ⊢ σ'√"
proof -
from wtp obtain wfmb where wf: "wf_prog wfmb P"
by (simp add: wf_jvm_prog_phi_def)
note conf_sys_xcpt [elim!]
note xp' = meth s' xp
note wtp
moreover
from xp wt correct
obtain obj where h: "h xcp = Some obj" by (blast dest: exec_instr_xcpt_h)
moreover note correct
ultimately
have "P,Φ ⊢ find_handler P xcp h frs √" by (rule uncaught_xcpt_correct)
with xp'
have "match_ex_table P (cname_of h xcp) pc xt = None ⟹ ?thesis"
(is "?m (cname_of h xcp) = _ ⟹ _" is "?match = _ ⟹ _")
by (simp add: split_beta)
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 correct meth
obtain ST LT where
h_ok: "P ⊢ h √" and
Φ_pc: "Φ C M ! pc = Some (ST, LT)" and
frame: "conf_f P h (ST,LT) ins (stk,loc,C,M,pc)" and
frames: "conf_fs P h Φ M (size Ts) T frs"
by (unfold correct_state_def) (fastforce dest: sees_method_fun)
from h_ok have preh: "preallocated h" by (simp add: hconf_def)
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 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 add: defs1)
let ?stk' = "Addr xcp # drop (length stk - d') stk"
let ?f = "(?stk', loc, C, M, pc')"
from some_handler xp'
have σ': "σ' = (None, h, ?f#frs)"
by (simp add: split_beta)
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)
from xp 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 have False by (auto simp: split_beta split: if_split_asm)
thus ?thesis ..
next
case New with xp
have [simp]: "xcp = addr_of_sys_xcpt OutOfMemory" by simp
with New 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 add: relevant_entries_def intro: that)
next
case Getfield with xp
have [simp]: "xcp = addr_of_sys_xcpt NullPointer"
by (simp add: split_beta split: if_split_asm)
with Getfield 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 add: relevant_entries_def intro: that)
next
case Putfield with xp
have [simp]: "xcp = addr_of_sys_xcpt NullPointer"
by (simp add: split_beta split: if_split_asm)
with Putfield 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 add: relevant_entries_def intro: that)
next
case Checkcast with xp
have [simp]: "xcp = addr_of_sys_xcpt ClassCast"
by (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 add: 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_instr_xcpt_h)
ultimately
show ?thesis using xt match
by (auto simp add: 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_instr_xcpt_h)
ultimately
show ?thesis using xt match
by (auto simp add: relevant_entries_def conf_def case_prod_unfold intro: that)
qed auto
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 add: xcpt_eff_def sup_state_opt_any_Some)
with conf loc stk have "conf_f P h (ST',LT') ins ?f"
by (auto simp add: defs1 intro: list_all2_dropI)
with meth h_ok frames Φ_pc' σ'
have ?thesis by (unfold correct_state_def) (fastforce dest: sees_method_fun)
}
ultimately
show ?thesis by (cases "?match") blast+
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.
›
declare defs1 [simp]
lemma Invoke_correct:
fixes σ' :: jvm_state
assumes wtprog: "wf_jvm_prog⇘Φ⇙ P"
assumes meth_C: "P ⊢ C sees M: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)#frs)"
assumes approx: "P,Φ ⊢ (None, h, (stk,loc,C,M,pc)#frs)√"
assumes no_xcp: "fst (exec_instr (ins!pc) P h stk loc C M pc frs) = None"
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 (ST,LT) ins (stk,loc,C,M,pc)" and
frames: "conf_fs P h Φ M (size Ts) T 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 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 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' Ts T m ST' LT' where
D: "ST!n = Class D" and
pc': "pc+1 < size ins" and
m_D: "P ⊢ D sees M': 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'"
by (clarsimp simp add: 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 add: 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
obtain Ts' T' m' D'' mxs' mxl' ins' xt' where
m_C': "P ⊢ C' sees M': Ts'→T' = (mxs',mxl',ins',xt') in D''" and
T': "P ⊢ T' ≤ T" and
Ts': "P ⊢ Ts [≤] Ts'"
by (auto dest: sees_method_mono)
let ?loc' = "Addr a # rev (take n stk) @ replicate mxl' undefined"
let ?f' = "([], ?loc', D'', M', 0)"
let ?f = "(stk, loc, C, M, pc)"
from Addr obj m_C' ins σ' meth_C
have s': "σ' = (None, h, ?f' # ?f # frs)" 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':Ts'→T'=(mxs',mxl',ins',xt') in D''"
by (fast dest: sees_method_idemp)
moreover
with wtprog
obtain start: "wt_start P D'' 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 add: wt_start_def defs1 sup_state_opt_any_Some)
moreover
have "conf_f P h ([], 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' by simp
qed
ultimately
have ?thesis using s' Φ_pc approx meth_C m_D T' ins D
by (fastforce dest: sees_method_fun [of _ C])
}
ultimately show ?thesis by blast
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: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)#frs)"
assumes correct: "P,Φ ⊢ (None, h, (stk,loc,C,M,pc)#frs)√"
shows "P,Φ ⊢ σ'√"
proof -
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'"
moreover obtain stk' loc' C' M' pc' where
f: "f = (stk',loc',C',M',pc')" by (cases f)
moreover note meth ins s'
ultimately
have σ':
"σ' = (None,h,(hd stk#(drop (1+size Ts) stk'),loc',C',M',pc'+1)#frs')"
(is "σ' = (None,h,?f'#frs')")
by simp
from correct meth
obtain ST LT where
h_ok: "P ⊢ h √" and
Φ_pc: "Φ C M ! pc = Some (ST, LT)" and
frame: "conf_f P h (ST, LT) ins (stk,loc,C,M,pc)" and
frames: "conf_fs P h Φ M (size Ts) T frs"
by (auto dest: sees_method_fun simp add: 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 add: conf_f_def)
from f frs' frames
obtain ST' LT' Ts'' T'' mxs' mxl⇩0' ins' xt' D Ts' T' m D' where
Φ': "Φ C' M' ! pc' = Some (ST', LT')" and
meth_C': "P ⊢ C' sees M':Ts''→T''=(mxs',mxl⇩0',ins',xt') in C'" and
ins': "ins' ! pc' = Invoke M (size Ts)" and
D: "ST' ! (size Ts) = Class D" and
meth_D: "P ⊢ D sees M: Ts'→T' = m in D'" and
T': "P ⊢ T ≤ T'" and
frame': "conf_f P h (ST',LT') ins' f" and
conf_fs: "conf_fs P h Φ 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)
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 aTs 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 add: sup_state_opt_any_Some)
from hd_stk T' have hd_stk': "P,h ⊢ hd stk :≤ T'" ..
have frame'':
"conf_f P h (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'
ultimately show ?thesis by (simp add: conf_f_def)
qed
with σ' frs' f meth h_ok hd_stk Φ_suc frames meth_C' Φ'
have ?thesis by (fastforce dest: sees_method_fun [of _ C'])
}
ultimately
show ?thesis by (cases frs) blast+
qed
declare sup_state_opt_any_Some [iff]
declare not_Err_eq [iff]
lemma Load_correct:
"⟦ wf_prog wt P;
P ⊢ C sees M:Ts→T=(mxs,mxl⇩0,ins,xt) in C;
ins!pc = Load idx;
P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M;
Some σ' = exec (P, None, h, (stk,loc,C,M,pc)#frs);
P,Φ ⊢ (None, h, (stk,loc,C,M,pc)#frs)√ ⟧
⟹ P,Φ ⊢ σ'√"
by (fastforce dest: sees_method_fun [of _ C] elim!: confTs_confT_sup)
declare [[simproc del: list_to_set_comprehension]]
lemma Store_correct:
"⟦ wf_prog wt P;
P ⊢ C sees M:Ts→T=(mxs,mxl⇩0,ins,xt) in C;
ins!pc = Store idx;
P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M;
Some σ' = exec (P, None, h, (stk,loc,C,M,pc)#frs);
P,Φ ⊢ (None, h, (stk,loc,C,M,pc)#frs)√ ⟧
⟹ P,Φ ⊢ σ'√"
apply clarsimp
apply (drule (1) sees_method_fun)
apply clarsimp
apply (blast intro!: list_all2_update_cong)
done
lemma Push_correct:
"⟦ wf_prog wt P;
P ⊢ C sees M:Ts→T=(mxs,mxl⇩0,ins,xt) in C;
ins!pc = Push v;
P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M;
Some σ' = exec (P, None, h, (stk,loc,C,M,pc)#frs);
P,Φ ⊢ (None, h, (stk,loc,C,M,pc)#frs)√ ⟧
⟹ P,Φ ⊢ σ'√"
apply clarsimp
apply (drule (1) sees_method_fun)
apply clarsimp
apply (blast dest: typeof_lit_conf)
done
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'"
apply (unfold cast_ok_def is_refT_def)
apply (frule Class_widen)
apply (elim exE disjE)
apply simp
apply simp
apply simp
apply (clarsimp simp add: conf_def obj_ty_def)
apply (cases v)
apply (auto intro: rtrancl_trans)
done
lemma Checkcast_correct:
"⟦ wf_jvm_prog⇘Φ⇙ P;
P ⊢ C sees M:Ts→T=(mxs,mxl⇩0,ins,xt) in C;
ins!pc = Checkcast D;
P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M;
Some σ' = exec (P, None, h, (stk,loc,C,M,pc)#frs) ;
P,Φ ⊢ (None, h, (stk,loc,C,M,pc)#frs)√;
fst (exec_instr (ins!pc) P h stk loc C M pc frs) = None ⟧
⟹ P,Φ ⊢ σ'√"
apply (clarsimp simp add: wf_jvm_prog_phi_def split: if_split_asm)
apply (drule (1) sees_method_fun)
apply (blast intro: Cast_conf2)
done
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: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)#frs)"
assumes cf: "P,Φ ⊢ (None, h, (stk,loc,C,M,pc)#frs)√"
assumes xc: "fst (exec_instr (ins!pc) P h stk loc C M pc frs) = None"
shows "P,Φ ⊢ σ'√"
proof -
from mC cf obtain ST LT where
"h√": "P ⊢ h √" 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 Φ M (size Ts) T 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: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: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 add: oconf_def has_field_def)
(blast dest: has_fields_fun)
from a h i mC s' stk' v
have "σ' = (None, h, (v#stk',loc,C,M,pc+1)#frs)" by simp
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√" mC Φ' pc' v fs
ultimately
show "P,Φ ⊢ σ' √" by fastforce
qed
lemma Putfield_correct:
fixes σ' :: jvm_state
assumes wf: "wf_prog wt P"
assumes mC: "P ⊢ C sees M: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)#frs)"
assumes cf: "P,Φ ⊢ (None, h, (stk,loc,C,M,pc)#frs)√"
assumes xc: "fst (exec_instr (ins!pc) P h stk loc C M pc frs) = None"
shows "P,Φ ⊢ σ'√"
proof -
from mC cf obtain ST LT where
"h√": "P ⊢ h √" 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 Φ M (size Ts) T 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: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 add: 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: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)"
from h have hext: "h ⊴ ?h'" by (rule hext_upd_obj)
from a h i mC s' stk'
have "σ' = (None, ?h', ?f'#frs)" by simp
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' Φ M (size Ts) T frs" by (rule conf_fs_hext)
moreover
note mC Φ' pc'
ultimately
show "P,Φ ⊢ σ' √" by fastforce
qed
lemma has_fields_b_fields:
"P ⊢ C has_fields FDTs ⟹ fields P C = FDTs"
apply (unfold fields_def)
apply (blast intro: the_equality has_fields_fun)
done
lemma oconf_blank [intro, simp]:
"⟦is_class P C; wf_prog wt P⟧ ⟹ P,h ⊢ blank P C √"
by (fastforce simp add: blank_def has_fields_b_fields oconf_init_fields
dest: wf_Fields_Ex)
lemma obj_ty_blank [iff]: "obj_ty (blank P C) = Class C"
by (simp add: blank_def)
lemma New_correct:
fixes σ' :: jvm_state
assumes wf: "wf_prog wt P"
assumes meth: "P ⊢ C sees M: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)#frs)"
assumes conf: "P,Φ ⊢ (None, h, (stk,loc,C,M,pc)#frs)√"
assumes no_x: "fst (exec_instr (ins!pc) P h stk loc C M pc frs) = None"
shows "P,Φ ⊢ σ'√"
proof -
from ins conf meth
obtain ST LT where
heap_ok: "P⊢ h√" and
Φ_pc: "Φ C M!pc = Some (ST,LT)" and
frame: "conf_f P h (ST,LT) ins (stk,loc,C,M,pc)" and
frames: "conf_fs P h Φ M (size Ts) T 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 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 have σ':
"σ' = (None, h(oref ↦ blank P X), (Addr oref#stk,loc,C,M,pc+1)#frs)"
(is "σ' = (None, ?h', ?f # frs)")
by simp
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' (ST', LT') ins ?f"
apply (clarsimp simp add: fun_upd_apply conf_def blank_def split_beta)
apply (auto intro: confs_hext confTs_hext)
done
moreover
from h have "h ⊴ ?h'" by simp
with frames have "conf_fs P ?h' Φ M (size Ts) T frs" by (rule conf_fs_hext)
ultimately
show ?thesis using meth Φ_suc by fastforce
qed
lemma Goto_correct:
"⟦ wf_prog wt P;
P ⊢ C sees M:Ts→T=(mxs,mxl⇩0,ins,xt) in C;
ins ! pc = Goto branch;
P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M;
Some σ' = exec (P, None, h, (stk,loc,C,M,pc)#frs) ;
P,Φ ⊢ (None, h, (stk,loc,C,M,pc)#frs)√ ⟧
⟹ P,Φ ⊢ σ'√"
apply clarsimp
apply (drule (1) sees_method_fun)
apply fastforce
done
lemma IfFalse_correct:
"⟦ wf_prog wt P;
P ⊢ C sees M:Ts→T=(mxs,mxl⇩0,ins,xt) in C;
ins ! pc = IfFalse branch;
P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M;
Some σ' = exec (P, None, h, (stk,loc,C,M,pc)#frs) ;
P,Φ ⊢ (None, h, (stk,loc,C,M,pc)#frs)√ ⟧
⟹ P,Φ ⊢ σ'√"
apply clarsimp
apply (drule (1) sees_method_fun)
apply fastforce
done
lemma CmpEq_correct:
"⟦ wf_prog wt P;
P ⊢ C sees M:Ts→T=(mxs,mxl⇩0,ins,xt) in C;
ins ! pc = CmpEq;
P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M;
Some σ' = exec (P, None, h, (stk,loc,C,M,pc)#frs) ;
P,Φ ⊢ (None, h, (stk,loc,C,M,pc)#frs)√ ⟧
⟹ P,Φ ⊢ σ'√"
apply clarsimp
apply (drule (1) sees_method_fun)
apply fastforce
done
lemma Pop_correct:
"⟦ wf_prog wt P;
P ⊢ C sees M:Ts→T=(mxs,mxl⇩0,ins,xt) in C;
ins ! pc = Pop;
P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M;
Some σ' = exec (P, None, h, (stk,loc,C,M,pc)#frs) ;
P,Φ ⊢ (None, h, (stk,loc,C,M,pc)#frs)√ ⟧
⟹ P,Φ ⊢ σ'√"
apply clarsimp
apply (drule (1) sees_method_fun)
apply fastforce
done
lemma IAdd_correct:
"⟦ wf_prog wt P;
P ⊢ C sees M:Ts→T=(mxs,mxl⇩0,ins,xt) in C;
ins ! pc = IAdd;
P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M;
Some σ' = exec (P, None, h, (stk,loc,C,M,pc)#frs) ;
P,Φ ⊢ (None, h, (stk,loc,C,M,pc)#frs)√ ⟧
⟹ P,Φ ⊢ σ'√"
apply (clarsimp simp add: conf_def)
apply (drule (1) sees_method_fun)
apply fastforce
done
lemma Throw_correct:
"⟦ wf_prog wt P;
P ⊢ C sees M:Ts→T=(mxs,mxl⇩0,ins,xt) in C;
ins ! pc = Throw;
Some σ' = exec (P, None, h, (stk,loc,C,M,pc)#frs) ;
P,Φ ⊢ (None, h, (stk,loc,C,M,pc)#frs)√;
fst (exec_instr (ins!pc) P h stk loc C M pc frs) = None ⟧
⟹ P,Φ ⊢ σ'√"
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:
"⟦ wf_jvm_prog⇘Φ⇙ P;
P ⊢ C sees M:Ts→T=(mxs,mxl⇩0,ins,xt) in C;
Some σ' = exec (P, None, h, (stk,loc,C,M,pc)#frs);
P,Φ ⊢ (None, h, (stk,loc,C,M,pc)#frs)√ ⟧
⟹ P,Φ ⊢ σ'√"
apply (subgoal_tac "P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M")
prefer 2
apply (erule wt_jvm_prog_impl_wt_instr, assumption)
apply clarsimp
apply (drule (1) sees_method_fun)
apply simp
apply (cases "fst (exec_instr (ins!pc) P h stk loc C M pc frs)")
prefer 2
apply (erule xcpt_correct, assumption+)
apply (frule wt_jvm_progD, erule exE)
apply (cases "ins!pc")
apply (rule Load_correct, assumption+)
apply (rule Store_correct, assumption+)
apply (rule Push_correct, assumption+)
apply (rule New_correct, assumption+)
apply (rule Getfield_correct, assumption+)
apply (rule Putfield_correct, assumption+)
apply (rule Checkcast_correct, assumption+)
apply (rule Invoke_correct, assumption+)
apply (rule Return_correct, assumption+)
apply (rule Pop_correct, assumption+)
apply (rule IAdd_correct, assumption+)
apply (rule Goto_correct, assumption+)
apply (rule CmpEq_correct, assumption+)
apply (rule IfFalse_correct, assumption+)
apply (rule Throw_correct, assumption+)
done
subsection ‹Main›
lemma correct_state_impl_Some_method:
"P,Φ ⊢ (None, h, (stk,loc,C,M,pc)#frs)√
⟹ ∃m Ts T. P ⊢ C sees M:Ts→T = m in C"
by fastforce
lemma BV_correct_1 [rule_format]:
"⋀σ. ⟦ wf_jvm_prog⇘Φ⇙ P; P,Φ ⊢ σ√⟧ ⟹ P ⊢ σ -jvm→⇩1 σ' ⟶ P,Φ ⊢ σ'√"
apply (simp only: split_tupled_all exec_1_iff)
apply (rename_tac xp h 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 clarify
apply (rule instr_correct)
apply assumption+
apply (rule sym)
apply assumption+
apply (case_tac frs)
apply simp_all
done
theorem progress:
"⟦ xp=None; frs≠[] ⟧ ⟹ ∃σ'. P ⊢ (xp,h,frs) -jvm→⇩1 σ'"
by (clarsimp simp add: exec_1_iff neq_Nil_conv split_beta
simp del: split_paired_Ex)
lemma progress_conform:
"⟦wf_jvm_prog⇘Φ⇙ P; P,Φ ⊢ (xp,h,frs)√; xp=None; frs≠[]⟧
⟹ ∃σ'. P ⊢ (xp,h,frs) -jvm→⇩1 σ' ∧ P,Φ ⊢ σ'√"
apply (drule progress)
apply assumption
apply (fast intro: BV_correct_1)
done
theorem BV_correct [rule_format]:
"⟦ wf_jvm_prog⇘Φ⇙ P; P ⊢ σ -jvm→ σ' ⟧ ⟹ P,Φ ⊢ σ√ ⟶ P,Φ ⊢ σ'√"
apply (simp only: exec_all_def1)
apply (erule rtrancl_induct)
apply simp
apply clarify
apply (erule (2) BV_correct_1)
done
lemma hconf_start:
assumes wf: "wf_prog wf_mb P"
shows "P ⊢ (start_heap P) √"
apply (unfold hconf_def)
apply (simp add: preallocated_start)
apply (clarify)
apply (drule sym)
apply (unfold start_heap_def)
apply (insert wf)
apply (auto simp add: fun_upd_apply is_class_xcpt split: if_split_asm)
done
lemma BV_correct_initial:
shows "⟦ wf_jvm_prog⇘Φ⇙ P; P ⊢ C sees M:[]→T = m in C ⟧
⟹ P,Φ ⊢ start_state P C M √"
apply (cases m)
apply (unfold start_state_def)
apply (unfold correct_state_def)
apply (simp del: defs1)
apply (rule conjI)
apply (simp add: wf_jvm_prog_phi_def hconf_start)
apply (drule wt_jvm_prog_impl_wt_start, assumption+)
apply (unfold conf_f_def wt_start_def)
apply fastforce
done
declare [[simproc add: list_to_set_comprehension]]
theorem typesafe:
assumes welltyped: "wf_jvm_prog⇘Φ⇙ P"
assumes main_method: "P ⊢ C sees M:[]→T = m in C"
shows "P ⊢ start_state P C M -jvm→ σ ⟹ P,Φ ⊢ σ √"
proof -
from welltyped main_method
have "P,Φ ⊢ start_state P C M √" by (rule BV_correct_initial)
moreover
assume "P ⊢ start_state P C M -jvm→ σ"
ultimately
show "P,Φ ⊢ σ √" using welltyped by - (rule BV_correct)
qed
end