Theory BVSpecTypeSafe
section ‹BV Type Safety Proof \label{sec:BVSpecTypeSafe}›
theory BVSpecTypeSafe
imports
BVConform
"../Common/ExternalCallWF"
begin
declare listE_length [simp del]
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:
›
context JVM_heap_conf_base begin
lemmas widen_rules [intro] = conf_widen confT_widen confs_widens confTs_widen
end
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).
(case D of None ⇒ True | Some D' ⇒ 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)
lemma match_is_relevant:
assumes rv: "⋀D'. P ⊢ D ≼⇧* D' ⟹ is_relevant_class (ins ! i) P D'"
assumes match: "match_ex_table P D pc xt = Some (pc',d')"
shows "∃(f,t,D',h,d) ∈ set (relevant_entries P (ins ! i) pc xt). (case D' of None ⇒ True | Some D'' ⇒ P ⊢ D ≼⇧* D'') ∧ pc ∈ {f..<t} ∧ pc' = h ∧ d' = d"
using rv match
by(fastforce simp add: relevant_entries_def is_relevant_entry_def matches_ex_entry_def dest: match_ex_table_SomeD)
context JVM_heap_conf_base begin
lemma exception_step_conform:
fixes σ' :: "('addr, 'heap) jvm_state"
assumes wtp: "wf_jvm_prog⇘Φ⇙ P"
assumes correct: "Φ ⊢ t:(⌊xcp⌋, h, fr # frs) √"
shows "Φ ⊢ t:exception_step P xcp h fr frs √"
proof -
obtain stk loc C M pc where fr: "fr = (stk, loc, C, M, pc)" by(cases fr)
from correct 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 fr) blast
from correct meth fr obtain D
where hxcp: "typeof_addr h xcp = ⌊Class_type D⌋" and DsubThrowable: "P ⊢ D ≼⇧* Throwable"
and rv: "⋀D'. P ⊢ D ≼⇧* D' ⟹ is_relevant_class (instrs_of P C M ! pc) P D'"
by(fastforce simp add: correct_state_def dest: sees_method_fun)
from meth have [simp]: "ex_table_of P C M = xt" by simp
from correct have tconf: "P,h ⊢ t √t" by(simp add: correct_state_def)
show ?thesis
proof(cases "match_ex_table P D pc xt")
case None
with correct fr meth hxcp show ?thesis
by(fastforce simp add: correct_state_def cname_of_def split: list.split)
next
case (Some pc_d)
then obtain pc' d' where pcd: "pc_d = (pc', d')"
and match: "match_ex_table P D pc xt = Some (pc',d')" by (cases pc_d) auto
from match_is_relevant[OF rv match] meth obtain f t D'
where rv: "(f, t, D', pc', d') ∈ set (relevant_entries P (ins ! pc) pc xt)"
and DsubD': "(case D' of None ⇒ True | Some D'' ⇒ P ⊢ D ≼⇧* D'')" and pc: "pc ∈ {f..<t}" by(auto)
from correct meth obtain ST LT
where h_ok: "hconf 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"
and preh: "preallocated h"
unfolding correct_state_def fr by(auto 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 stk have [simp]: "size stk = size ST" ..
from wtp meth correct fr have wt: "P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M"
by (auto simp add: correct_state_def conf_f_def
dest: sees_method_fun
elim!: wt_jvm_prog_impl_wt_instr)
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')"
have conf: "P,h ⊢ Addr xcp :≤ Class (case D' of None ⇒ Throwable | Some D'' ⇒ D'')"
using DsubD' hxcp DsubThrowable by(auto simp add: conf_def)
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')"
proof(cases D')
case Some
thus ?thesis using eff rv DsubD' conf that
by(fastforce simp add: xcpt_eff_def sup_state_opt_any_Some intro: widen_trans[OF widen_subcls])
next
case None
with that eff rv conf DsubThrowable show ?thesis
by(fastforce simp add: xcpt_eff_def sup_state_opt_any_Some intro: widen_trans[OF widen_subcls])
qed
with conf loc stk hxcp have "conf_f P h (ST',LT') ins ?f"
by (auto simp add: defs1 conf_def intro: list_all2_dropI)
with meth h_ok frames Φ_pc' fr match hxcp tconf preh
show ?thesis unfolding correct_state_def
by(fastforce dest: sees_method_fun simp add: cname_of_def)
qed
qed
end
subsection ‹Single Instructions›
text ‹
In this subsection we prove for each single (welltyped) instruction
that the state after execution of the instruction still conforms.
Since we have already handled raised exceptions above, we can now assume that
no exception has been raised in this step.
›
context JVM_conf_read begin
declare defs1 [simp]
lemma Invoke_correct:
fixes σ' :: "('addr, 'heap) 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 approx: "Φ ⊢ t:(None, h, (stk,loc,C,M,pc)#frs)√"
assumes exec: "(tas, σ) ∈ exec_instr (ins!pc) P t h stk loc C M pc frs"
shows "Φ ⊢ t:σ √"
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: "hconf h" and
tconf: "P,h ⊢ t √t" 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" and
preh: "preallocated h"
by (fastforce dest: sees_method_fun)
from ins wti Φ_pc
have n: "n < size ST" by simp
show ?thesis
proof(cases "stk!n = Null")
case True
with ins heap_ok Φ_pc frame frames exec meth_C tconf preh show ?thesis
by(fastforce elim: wf_preallocatedE[OF wfprog, where C=NullPointer])
next
case False
note Null = this
have NT: "ST!n ≠ NT"
proof
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 Null show False by contradiction
qed
from frame obtain
stk: "P,h ⊢ stk [:≤] ST" and
loc: "P,h ⊢ loc [:≤⇩⊤] LT" by simp
from NT ins wti Φ_pc have pc': "pc+1 < size ins" by simp
from NT ins wti Φ_pc obtain ST' LT'
where pc': "pc+1 < size ins"
and Φ': "Φ C M ! (pc+1) = Some (ST', LT')"
and LT': "P ⊢ LT [≤⇩⊤] LT'"
by(auto simp add: neq_Nil_conv sup_state_opt_any_Some split: if_split_asm)
with NT ins wti Φ_pc obtain D D' TTs TT m
where D: "class_type_of' (ST!n) = ⌊D⌋"
and m_D: "P ⊢ D sees M': TTs→TT = m in D'"
and Ts: "P ⊢ rev (take n ST) [≤] TTs"
and ST': "P ⊢ (TT # drop (n+1) ST) [≤] ST'"
by(auto)
from n stk D have "P,h ⊢ stk!n :≤ ST ! n"
by (auto simp add: list_all2_conv_all_nth)
from ‹P,h ⊢ stk!n :≤ ST ! n› Null D
obtain U a where
Addr: "stk!n = Addr a" and
obj: "typeof_addr h a = Some U" and
UsubSTn: "P ⊢ ty_of_htype U ≤ ST ! n"
by(cases "stk ! n")(auto simp add: conf_def widen_Class)
from D UsubSTn obtain C' where
C': "class_type_of' (ty_of_htype U) = ⌊C'⌋" and C'subD: "P ⊢ C' ≼⇧* D"
by(rule widen_is_class_type_of) simp
with wfprog m_D
obtain Ts' T' D'' meth' where
m_C': "P ⊢ C' sees M': Ts'→T' = meth' in D''" and
T': "P ⊢ T' ≤ TT" and
Ts': "P ⊢ TTs [≤] Ts'"
by (auto dest: sees_method_mono)
from Ts n have [simp]: "size TTs = 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'=meth' in D''"
by (fast dest: sees_method_idemp)
{ fix mxs' mxl' ins' xt'
assume [simp]: "meth' = ⌊(mxs', mxl', ins', xt')⌋"
let ?loc' = "Addr a # rev (take n stk) @ replicate mxl' undefined_value"
let ?f' = "([], ?loc', D'', M', 0)"
let ?f = "(stk, loc, C, M, pc)"
from Addr obj m_C' ins meth_C exec C' False
have s': "σ = (None, h, ?f' # ?f # frs)" by(auto split: if_split_asm)
moreover
from wtprog mD''
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_value [:≤⇩⊤] replicate mxl' Err" by simp
also from m_C' have "P ⊢ C' ≼⇧* D''" by (rule sees_method_decl_above)
from obj heap_ok have "is_htype P U" by (rule typeof_addr_is_type)
with C' have "P ⊢ ty_of_htype U ≤ Class C'"
by(cases U)(simp_all add: widen_array_object)
with ‹P ⊢ C' ≼⇧* D''› obj C' have "P,h ⊢ Addr a :≤ Class D''"
by (auto simp add: conf_def intro: widen_trans)
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 tconf C' mD''
by (fastforce dest: sees_method_fun [of _ C]) }
moreover
{ assume [simp]: "meth' = Native"
with wfprog m_C' have "D''∙M'(Ts') :: T'" by(simp add: sees_wf_native)
with C' m_C' have nec: "is_native P U M'" by(auto intro: is_native.intros)
from ins n Addr obj exec m_C' C'
obtain va h' tas' where va: "(tas', va, h') ∈ red_external_aggr P t a M' (rev (take n stk)) h"
and σ: "σ = extRet2JVM n h' stk loc C M pc frs va" by(auto)
from va nec obj have hext: "h ⊴ h'" by(auto intro: red_external_aggr_hext)
with frames have frames': "conf_fs P h' Φ M (length Ts) T frs" by(rule conf_fs_hext)
from preh hext have preh': "preallocated h'" by(rule preallocated_hext)
from va nec obj tconf have tconf': "P,h' ⊢ t √t"
by(auto dest: red_external_aggr_preserves_tconf)
from hext obj have obj': "typeof_addr h' a = ⌊U⌋" by(rule typeof_addr_hext_mono)
from stk have "P,h ⊢ take n stk [:≤] take n ST" by(rule list_all2_takeI)
then obtain Us where "map typeof⇘h⇙ (take n stk) = map Some Us" "P ⊢ Us [≤] take n ST"
by(auto simp add: confs_conv_map)
hence Us: "map typeof⇘h⇙ (rev (take n stk)) = map Some (rev Us)" "P ⊢ rev Us [≤] rev (take n ST)"
by- (simp only: rev_map[symmetric], simp)
from ‹P ⊢ rev Us [≤] rev (take n ST)› Ts Ts'
have "P ⊢ rev Us [≤] Ts'" by(blast intro: widens_trans)
with obj ‹map typeof⇘h⇙ (rev (take n stk)) = map Some (rev Us)› C' m_C'
have wtext': "P,h ⊢ a∙M'(rev (take n stk)) : T'" by(simp add: external_WT'.intros)
from va have va': "P,t ⊢ ⟨a∙M'(rev (take n stk)),h⟩ -tas'→ext ⟨va,h'⟩"
by(unfold WT_red_external_list_conv[OF wfprog wtext' tconf])
with heap_ok wtext' tconf wfprog have heap_ok': "hconf h'" by(auto dest: external_call_hconf)
have ?thesis
proof(cases va)
case (RetExc a')
from frame hext have "conf_f P h' (ST, LT) ins (stk, loc, C, M, pc)" by(rule conf_f_hext)
with σ tconf' heap_ok' meth_C Φ_pc frames' RetExc red_external_conf_extRet[OF wfprog va' wtext' heap_ok preh tconf] ins preh'
show ?thesis by(fastforce simp add: conf_def widen_Class)
next
case RetStaySame
from frame hext have "conf_f P h' (ST, LT) ins (stk, loc, C, M, pc)" by(rule conf_f_hext)
with σ heap_ok' meth_C Φ_pc RetStaySame frames' tconf' preh' show ?thesis by fastforce
next
case (RetVal v)
with σ have σ: "σ = (None, h', (v # drop (n+1) stk, loc, C, M, pc+1) # frs)" by simp
from heap_ok wtext' va' RetVal preh tconf have "P,h' ⊢ v :≤ T'"
by(auto dest: red_external_conf_extRet[OF wfprog])
from stk have "P,h ⊢ drop (n + 1) stk [:≤] drop (n+1) ST" by(rule list_all2_dropI)
hence "P,h' ⊢ drop (n + 1) stk [:≤] drop (n+1) ST" using hext by(rule confs_hext)
with ‹P,h' ⊢ v :≤ T'› have "P,h' ⊢ v # drop (n + 1) stk [:≤] T' # drop (n+1) ST"
by(auto simp add: conf_def intro: widen_trans)
also
with NT ins wti Φ_pc Φ' nec False D m_D T'
have "P ⊢ (T' # drop (n + 1) ST) [≤] ST'"
by(auto dest: sees_method_fun intro: widen_trans)
also from loc hext have "P,h' ⊢ loc [:≤⇩⊤] LT" by(rule confTs_hext)
hence "P,h' ⊢ loc [:≤⇩⊤] LT'" using LT' by(rule confTs_widen)
ultimately show ?thesis using ‹hconf h'› σ meth_C Φ' pc' frames' tconf' preh' by fastforce
qed }
ultimately show ?thesis by(cases meth') auto
qed
qed
declare list_all2_Cons2 [iff]
lemma Return_correct:
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 correct: "Φ ⊢ t:(None, h, (stk,loc,C,M,pc)#frs)√"
assumes s': "(tas, σ') ∈ exec P t (None, h, (stk,loc,C,M,pc)#frs)"
shows "Φ ⊢ t:σ'√"
proof -
from wt_prog
obtain wfmb where wf: "wf_prog wfmb P" by (simp add: wf_jvm_prog_phi_def)
from meth ins s' correct
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: "hconf h" and
tconf: "P,h ⊢ t √t" 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" and
preh: "preallocated h"
by (auto dest: sees_method_fun)
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' Ts' T' 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: "∃D m D'. class_type_of' (ST' ! (size Ts)) = Some 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 blast
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 wti: "P,T'',mxs',size ins',xt' ⊢ ins'!pc',pc' :: Φ C' M'"
by (rule wt_jvm_prog_impl_wt_instr)
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'"
using ins' Φ' D T' wti
by(fastforce simp add: sup_state_opt_any_Some split: if_split_asm)
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' Φ' tconf preh
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;
Φ ⊢ t:(None, h, (stk,loc,C,M,pc)#frs)√ ;
(tas, σ') ∈ exec P t (None, h, (stk,loc,C,M,pc)#frs) ⟧
⟹ Φ ⊢ t:σ' √"
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;
Φ ⊢ t:(None, h, (stk,loc,C,M,pc)#frs)√;
(tas, σ') ∈ exec P t (None, h, (stk,loc,C,M,pc)#frs) ⟧
⟹ Φ ⊢ t:σ'√"
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;
Φ ⊢ t:(None, h, (stk,loc,C,M,pc)#frs)√;
(tas, σ') ∈ exec P t (None, h, (stk,loc,C,M,pc)#frs) ⟧
⟹ Φ ⊢ t:σ'√"
apply clarsimp
apply (drule (1) sees_method_fun)
apply clarsimp
apply (blast dest: typeof_lit_conf)
done
declare [[simproc add: list_to_set_comprehension]]
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;
Φ ⊢ t:(None, h, (stk,loc,C,M,pc)#frs)√;
(tas, σ) ∈ exec_instr (ins!pc) P t h stk loc C M pc frs ⟧
⟹ Φ ⊢ t:σ √"
using wf_preallocatedD[of "λP C (M, Ts, T⇩r, mxs, mxl⇩0, is, xt). wt_method P C Ts T⇩r mxs mxl⇩0 is xt (Φ C M)" P h ClassCast]
apply (clarsimp simp add: wf_jvm_prog_phi_def split: if_split_asm)
apply(drule (1) sees_method_fun)
apply(fastforce simp add: conf_def intro: widen_trans)
apply (drule (1) sees_method_fun)
apply(fastforce simp add: conf_def intro: widen_trans)
done
lemma Instanceof_correct:
"⟦ wf_jvm_prog⇘Φ⇙ P;
P ⊢ C sees M:Ts→T=⌊(mxs,mxl⇩0,ins,xt)⌋ in C;
ins!pc = Instanceof Ty;
P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M;
Φ ⊢ t:(None, h, (stk,loc,C,M,pc)#frs)√;
(tas, σ) ∈ exec_instr (ins!pc) P t h stk loc C M pc frs ⟧
⟹ Φ ⊢ t:σ √"
apply (clarsimp simp add: wf_jvm_prog_phi_def split: if_split_asm)
apply (drule (1) sees_method_fun)
apply fastforce
done
declare split_paired_All [simp del]
end
lemma widens_Cons [iff]:
"P ⊢ (T # Ts) [≤] Us = (∃z zs. Us = z # zs ∧ P ⊢ T ≤ z ∧ P ⊢ Ts [≤] zs)"
by(rule list_all2_Cons1)
context heap_conf_base begin
end
context JVM_conf_read begin
lemma Getfield_correct:
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 cf: "Φ ⊢ t:(None, h, (stk,loc,C,M,pc)#frs)√"
assumes xc: "(tas, σ') ∈ exec_instr (ins!pc) P t h stk loc C M pc frs"
shows "Φ ⊢ t:σ'√"
proof -
from mC cf obtain ST LT where
"h√": "hconf h" and
tconf: "P,h ⊢ t √t" 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" and
preh: "preallocated h"
by (fastforce dest: sees_method_fun)
from i Φ wt obtain oT ST'' vT ST' LT' vT' fm where
oT: "P ⊢ oT ≤ Class D" and
ST: "ST = oT # ST''" and
F: "P ⊢ D sees F:vT (fm) 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
show ?thesis
proof(cases "ref = Null")
case True
with tconf "h√" i xc stk' mC fs Φ ST'' ref ST loc pc'
wf_preallocatedD[OF wf, of h NullPointer] preh
show ?thesis by(fastforce)
next
case False
from ref oT have "P,h ⊢ ref :≤ Class D" ..
with False obtain a U' D' where a: "ref = Addr a"
and h: "typeof_addr h a = Some U'"
and U': "D' = class_type_of U'" and D': "P ⊢ D' ≼⇧* D"
by (blast dest: non_npD2)
{ fix v
assume read: "heap_read h a (CField D F) v"
from D' F have has_field: "P ⊢ D' has F:vT (fm) in D"
by (blast intro: has_field_mono has_visible_field)
with h have "P,h ⊢ a@CField D F : vT" unfolding U' ..
with read have v: "P,h ⊢ v :≤ vT" using "h√"
by(rule heap_read_conf)
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 tconf preh
ultimately have "Φ ⊢ t:(None, h, (v#stk',loc,C,M,pc+1)#frs) √" by fastforce }
with a h i mC stk' xc
show ?thesis by auto
qed
qed
lemma Putfield_correct:
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 cf: "Φ ⊢ t:(None, h, (stk,loc,C,M,pc)#frs)√"
assumes xc: "(tas, σ') ∈ exec_instr (ins!pc) P t h stk loc C M pc frs"
shows "Φ ⊢ t:σ' √"
proof -
from mC cf obtain ST LT where
"h√": "hconf h" and
tconf: "P,h ⊢ t √t" 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" and
preh: "preallocated h"
by (fastforce dest: sees_method_fun)
from i Φ wt obtain vT vT' oT ST'' ST' LT' fm where
ST: "ST = vT # oT # ST''" and
field: "P ⊢ D sees F:vT' (fm) 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
show ?thesis
proof(cases "ref = Null")
case True
with tconf "h√" i xc stk' mC fs Φ ST'' ref ST loc pc' v
wf_preallocatedD[OF wf, of h NullPointer] preh
show ?thesis by(fastforce)
next
case False
from ref oT have "P,h ⊢ ref :≤ Class D" ..
with False obtain a U' D' where
a: "ref = Addr a" and h: "typeof_addr h a = Some U'"
and U': "D' = class_type_of U'" and D': "P ⊢ D' ≼⇧* D"
by (blast dest: non_npD2)
from v vT have vT': "P,h ⊢ v :≤ vT'" ..
from field D' have has_field: "P ⊢ D' has F:vT' (fm) in D"
by (blast intro: has_field_mono has_visible_field)
with h have al: "P,h ⊢ a@CField D F : vT'" unfolding U' ..
let ?f' = "(stk',loc,C,M,pc+1)"
{ fix h'
assume "write": "heap_write h a (CField D F) v h'"
hence hext: "h ⊴ h'" by(rule hext_heap_write)
with preh have "preallocated h'" by(rule preallocated_hext)
moreover
from "write" "h√" al vT' have "hconf h'" by(rule hconf_heap_write_mono)
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'
moreover
from tconf hext have "P,h' ⊢ t √t" by(rule tconf_hext_mono)
ultimately have "Φ ⊢ t:(None, h', ?f'#frs) √" by fastforce }
with a h i mC stk' xc show ?thesis by(auto simp del: correct_state_def)
qed
qed
lemma CAS_correct:
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 = CAS F D"
assumes wt: "P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M"
assumes cf: "Φ ⊢ t:(None, h, (stk,loc,C,M,pc)#frs)√"
assumes xc: "(tas, σ') ∈ exec_instr (ins!pc) P t h stk loc C M pc frs"
shows "Φ ⊢ t:σ' √"
proof -
from mC cf obtain ST LT where
"h√": "hconf h" and
tconf: "P,h ⊢ t √t" 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" and
preh: "preallocated h"
by (fastforce dest: sees_method_fun)
from i Φ wt obtain T1 T2 T3 T' ST'' ST' LT' fm where
ST: "ST = T3 # T2 # T1 # ST''" and
field: "P ⊢ D sees F:T' (fm) in D" and
oT: "P ⊢ T1 ≤ Class D" and T2: "P ⊢ T2 ≤ T'" and T3: "P ⊢ T3 ≤ T'" and
pc': "pc+1 < size ins" and
Φ': "Φ C M!(pc+1) = Some (Boolean # ST',LT')" and
ST': "P ⊢ ST'' [≤] ST'" and LT': "P ⊢ LT [≤⇩⊤] LT'"
by clarsimp
from stk ST obtain v'' v' v stk' where
stk': "stk = v''#v'#v#stk'" and
v: "P,h ⊢ v :≤ T1" and
v': "P,h ⊢ v' :≤ T2" and
v'': "P,h ⊢ v'' :≤ T3" and
ST'': "P,h ⊢ stk' [:≤] ST''"
by auto
show ?thesis
proof(cases "v = Null")
case True
with tconf "h√" i xc stk' mC fs Φ ST'' v ST loc pc' v' v''
wf_preallocatedD[OF wf, of h NullPointer] preh
show ?thesis by(fastforce)
next
case False
from v oT have "P,h ⊢ v :≤ Class D" ..
with False obtain a U' D' where
a: "v = Addr a" and h: "typeof_addr h a = Some U'"
and U': "D' = class_type_of U'" and D': "P ⊢ D' ≼⇧* D"
by (blast dest: non_npD2)
from v' T2 have vT': "P,h ⊢ v' :≤ T'" ..
from v'' T3 have vT'': "P,h ⊢ v'' :≤ T'" ..
from field D' have has_field: "P ⊢ D' has F:T' (fm) in D"
by (blast intro: has_field_mono has_visible_field)
with h have al: "P,h ⊢ a@CField D F : T'" unfolding U' ..
from ST'' ST' have stk'': "P,h ⊢ stk' [:≤] ST'" ..
from loc LT' have loc': "P,h ⊢ loc [:≤⇩⊤] LT'" ..
{ fix h'
assume "write": "heap_write h a (CField D F) v'' h'"
hence hext: "h ⊴ h'" by(rule hext_heap_write)
with preh have "preallocated h'" by(rule preallocated_hext)
moreover
from "write" "h√" al vT'' have "hconf h'" by(rule hconf_heap_write_mono)
moreover
from stk'' hext have "P,h' ⊢ stk' [:≤] ST'" by (rule confs_hext)
moreover
from loc' 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'
moreover
let ?f' = "(Bool True # stk',loc,C,M,pc+1)"
from tconf hext have "P,h' ⊢ t √t" by(rule tconf_hext_mono)
ultimately have "Φ ⊢ t:(None, h', ?f'#frs) √" by fastforce
} moreover {
let ?f' = "(Bool False # stk',loc,C,M,pc+1)"
have "Φ ⊢ t:(None, h, ?f'#frs) √" using tconf "h√" preh mC Φ' stk'' loc' pc' fs
by fastforce
} ultimately show ?thesis using a h i mC stk' xc by(auto simp del: correct_state_def)
qed
qed
lemma New_correct:
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 conf: "Φ ⊢ t:(None, h, (stk,loc,C,M,pc)#frs)√"
assumes no_x: "(tas, σ) ∈ exec_instr (ins!pc) P t h stk loc C M pc frs"
shows "Φ ⊢ t:σ √"
proof -
from ins conf meth
obtain ST LT where
heap_ok: "hconf h" and
tconf: "P,h ⊢ t √t" 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" and
preh: "preallocated h"
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
show ?thesis
proof(cases "allocate h (Class_type X) = {}")
case True
with frame frames tconf suc_pc no_x ins meth Φ_pc
wf_preallocatedD[OF wf, of h OutOfMemory] preh is_class_X heap_ok
show ?thesis
by(fastforce intro: tconf_hext_mono confs_hext confTs_hext conf_fs_hext)
next
case False
with ins meth no_x obtain h' oref
where new: "(h', oref) ∈ allocate h (Class_type X)"
and σ': "σ = (None, h', (Addr oref#stk,loc,C,M,pc+1)#frs)" (is "σ = (None, h', ?f # frs)")
by auto
from new have hext: "h ⊴ h'" by(rule hext_allocate)
with preh have preh': "preallocated h'" by(rule preallocated_hext)
from new heap_ok is_class_X have heap_ok': "hconf h'"
by(auto intro: hconf_allocate_mono)
with new is_class_X have h': "typeof_addr h' oref = ⌊Class_type X⌋" by(auto dest: allocate_SomeD)
note heap_ok' σ'
moreover
from frame less suc_pc wf h' hext
have "conf_f P h' (ST', LT') ins ?f"
apply (clarsimp simp add: fun_upd_apply conf_def split_beta)
apply (auto intro: confs_hext confTs_hext)
done
moreover
from frames hext have "conf_fs P h' Φ M (size Ts) T frs" by (rule conf_fs_hext)
moreover from tconf hext have "P,h' ⊢ t √t" by(rule tconf_hext_mono)
ultimately
show ?thesis using meth Φ_suc preh' by fastforce
qed
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;
Φ ⊢ t:(None, h, (stk,loc,C,M,pc)#frs)√;
(tas, σ') ∈ exec P t (None, h, (stk,loc,C,M,pc)#frs) ⟧
⟹ Φ ⊢ t:σ' √"
apply clarsimp
apply (drule (1) sees_method_fun)
apply fastforce
done
declare [[simproc del: list_to_set_comprehension]]
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;
Φ ⊢ t:(None, h, (stk,loc,C,M,pc)#frs)√;
(tas, σ') ∈ exec P t (None, h, (stk,loc,C,M,pc)#frs) ⟧
⟹ Φ ⊢ t:σ'√"
apply clarsimp
apply (drule (1) sees_method_fun)
apply fastforce
done
declare [[simproc add: list_to_set_comprehension]]
lemma BinOp_correct:
"⟦ wf_prog wt P;
P ⊢ C sees M:Ts→T=⌊(mxs,mxl⇩0,ins,xt)⌋ in C;
ins ! pc = BinOpInstr bop;
P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M;
Φ ⊢ t:(None, h, (stk,loc,C,M,pc)#frs)√;
(tas, σ') ∈ exec P t (None, h, (stk,loc,C,M,pc)#frs) ⟧
⟹ Φ ⊢ t:σ'√"
apply clarsimp
apply (drule (1) sees_method_fun)
apply(clarsimp simp add: conf_def)
apply(drule (2) WTrt_binop_widen_mono)
apply clarsimp
apply(frule (2) binop_progress)
apply(clarsimp split: sum.split_asm)
apply(frule (5) binop_type)
apply(fastforce intro: widen_trans simp add: conf_def)
apply(frule (5) binop_type)
apply(clarsimp simp add: conf_def)
apply(clarsimp simp add: widen_Class)
apply(fastforce intro: widen_trans dest: binop_relevant_class simp add: cname_of_def conf_def)
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;
Φ ⊢ t:(None, h, (stk,loc,C,M,pc)#frs)√;
(tas, σ') ∈ exec P t (None, h, (stk,loc,C,M,pc)#frs) ⟧
⟹ Φ ⊢ t:σ'√"
apply clarsimp
apply (drule (1) sees_method_fun)
apply fastforce
done
lemma Dup_correct:
"⟦ wf_prog wt P;
P ⊢ C sees M:Ts→T=⌊(mxs,mxl⇩0,ins,xt)⌋ in C;
ins ! pc = Dup;
P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M;
Φ ⊢ t:(None, h, (stk,loc,C,M,pc)#frs)√;
(tas, σ') ∈ exec P t (None, h, (stk,loc,C,M,pc)#frs) ⟧
⟹ Φ ⊢ t:σ'√"
apply clarsimp
apply (drule (1) sees_method_fun)
apply fastforce
done
lemma Swap_correct:
"⟦ wf_prog wt P;
P ⊢ C sees M:Ts→T=⌊(mxs,mxl⇩0,ins,xt)⌋ in C;
ins ! pc = Swap;
P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M;
Φ ⊢ t:(None, h, (stk,loc,C,M,pc)#frs)√;
(tas, σ') ∈ exec P t (None, h, (stk,loc,C,M,pc)#frs) ⟧
⟹ Φ ⊢ t:σ'√"
apply clarsimp
apply (drule (1) sees_method_fun)
apply fastforce
done
declare [[simproc del: list_to_set_comprehension]]
lemma Throw_correct:
"⟦ wf_prog wt P;
P ⊢ C sees M:Ts→T=⌊(mxs,mxl⇩0,ins,xt)⌋ in C;
ins ! pc = ThrowExc;
P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M;
Φ ⊢ t:(None, h, (stk,loc,C,M,pc)#frs)√;
(tas, σ') ∈ exec_instr (ins!pc) P t h stk loc C M pc frs ⟧
⟹ Φ ⊢ t:σ'√"
using wf_preallocatedD[of wt P h NullPointer]
apply(clarsimp)
apply(drule (1) sees_method_fun)
apply(auto)
apply fastforce
apply fastforce
apply(drule (1) non_npD)
apply fastforce+
done
declare [[simproc add: list_to_set_comprehension]]
lemma NewArray_correct:
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 = NewArray X"
assumes wt: "P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M"
assumes conf: "Φ ⊢ t:(None, h, (stk,loc,C,M,pc)#frs)√"
assumes no_x: "(tas, σ) ∈ exec_instr (ins!pc) P t h stk loc C M pc frs"
shows "Φ ⊢ t:σ √"
proof -
from ins conf meth
obtain ST LT where
heap_ok: "hconf h" and
tconf: "P,h ⊢ t √t" 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
frame: "conf_f P h (ST,LT) ins (stk,loc,C,M,pc)" and
frames: "conf_fs P h Φ M (size Ts) T frs" and
preh: "preallocated h"
by (auto dest: sees_method_fun)
from ins Φ_pc wt obtain ST'' X' ST' LT' where
ST: "ST = Integer # ST''" and
pc': "pc+1 < size ins" and
Φ': "Φ C M ! (pc+1) = Some (X'#ST', LT')" and
ST': "P ⊢ ST'' [≤] ST'" and LT': "P ⊢ LT [≤⇩⊤] LT'" and
XX': "P ⊢ X⌊⌉ ≤ X'" and
suc_pc: "pc+1 < size ins" and
is_type_X: "is_type P (X⌊⌉)"
by(fastforce dest: Array_widen)
from stk ST obtain si stk' where si: "stk = Intg si # stk'"
by(auto simp add: conf_def)
show ?thesis
proof(cases "si <s 0 ∨ allocate h (Array_type X (nat (sint si))) = {}")
case True
with frame frames tconf heap_ok suc_pc no_x ins meth Φ_pc si preh
wf_preallocatedD[OF wf, of h OutOfMemory] wf_preallocatedD[OF wf, of h NegativeArraySize]
show ?thesis
by(fastforce intro: tconf_hext_mono confs_hext confTs_hext conf_fs_hext split: if_split_asm)+
next
case False
with ins meth si no_x obtain h' oref
where new: "(h', oref) ∈ allocate h (Array_type X (nat (sint si)))"
and σ': "σ = (None, h', (Addr oref#tl stk,loc,C,M,pc+1)#frs)" (is "σ = (None, h', ?f # frs)")
by(auto split: if_split_asm)
from new have hext: "h ⊴ h'" by(rule hext_allocate)
with preh have preh': "preallocated h'" by(rule preallocated_hext)
from new heap_ok is_type_X have heap_ok': "hconf h'" by(auto intro: hconf_allocate_mono)
from False have si': "0 <=s si" by auto
with new is_type_X have h': "typeof_addr h' oref = ⌊Array_type X (nat (sint si))⌋"
by(auto dest: allocate_SomeD)
note σ' heap_ok'
moreover
from frame ST' ST LT' suc_pc wf XX' h' hext
have "conf_f P h' (X' # ST', LT') ins ?f"
by(clarsimp simp add: fun_upd_apply conf_def split_beta)(auto intro: confs_hext confTs_hext)
moreover
from frames hext have "conf_fs P h' Φ M (size Ts) T frs" by (rule conf_fs_hext)
moreover from tconf hext have "P,h' ⊢ t √t" by(rule tconf_hext_mono)
ultimately
show ?thesis using meth Φ' preh' by fastforce
qed
qed
lemma ALoad_correct:
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 = ALoad"
assumes wt: "P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M"
assumes conf: "Φ ⊢ t: (None, h, (stk,loc,C,M,pc)#frs)√"
assumes no_x: "(tas, σ) ∈ exec_instr (ins!pc) P t h stk loc C M pc frs"
shows "Φ ⊢ t:σ √"
proof -
from ins conf meth
obtain ST LT where
heap_ok: "hconf h" and
tconf: "P,h ⊢ t √t" 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
frame: "conf_f P h (ST,LT) ins (stk,loc,C,M,pc)" and
frames: "conf_fs P h Φ M (size Ts) T frs" and
preh: "preallocated h"
by (auto dest: sees_method_fun)
from ins wt Φ_pc have lST: "length ST > 1" by(auto)
show ?thesis
proof(cases "hd (tl stk) = Null")
case True
with ins no_x heap_ok tconf Φ_pc stk loc frame frames meth wf_preallocatedD[OF wf, of h NullPointer] preh
show ?thesis by(fastforce)
next
case False
note stkNN = this
have STNN: "hd (tl ST) ≠ NT"
proof
assume "hd (tl ST) = NT"
moreover
from frame have "P,h ⊢ stk [:≤] ST" by simp
with lST have "P,h ⊢ hd (tl stk) :≤ hd (tl ST)"
by (cases ST, auto, case_tac list, auto)
ultimately
have "hd (tl stk) = Null" by simp
with stkNN show False by contradiction
qed
with stkNN ins Φ_pc wt obtain ST'' X X' ST' LT' where
ST: "ST = Integer # X⌊⌉ # ST''" and
pc': "pc+1 < size ins" and
Φ': "Φ C M ! (pc+1) = Some (X'#ST', LT')" and
ST': "P ⊢ ST'' [≤] ST'" and LT': "P ⊢ LT [≤⇩⊤] LT'" and
XX': "P ⊢ X ≤ X'" and
suc_pc: "pc+1 < size ins"
by(fastforce)
from stk ST obtain ref idx stk' where
stk': "stk = idx#ref#stk'" and
idx: "P,h ⊢ idx :≤ Integer" and
ref: "P,h ⊢ ref :≤ X⌊⌉" and
ST'': "P,h ⊢ stk' [:≤] ST''"
by auto
from stkNN stk' have "ref ≠ Null" by(simp)
with ref obtain a Xel n
where a: "ref = Addr a"
and ha: "typeof_addr h a = ⌊Array_type Xel n⌋"
and Xel: "P ⊢ Xel ≤ X"
by(cases ref)(fastforce simp add: conf_def widen_Array)+
from idx obtain idxI where idxI: "idx = Intg idxI"
by(auto simp add: conf_def)
show ?thesis
proof(cases "0 <=s idxI ∧ sint idxI < int n")
case True
hence si': "0 <=s idxI" "sint idxI < int n" by auto
hence "nat (sint idxI) < n"
by (simp add: word_sle_eq nat_less_iff)
with ha have al: "P,h ⊢ a@ACell (nat (sint idxI)) : Xel" ..
{ fix v
assume read: "heap_read h a (ACell (nat (sint idxI))) v"
hence v: "P,h ⊢ v :≤ Xel" using al heap_ok by(rule heap_read_conf)
let ?f = "(v # stk', loc, C, M, pc + 1)"
from frame ST' ST LT' suc_pc wf XX' Xel idxI si' v ST''
have "conf_f P h (X' # ST', LT') ins ?f"
by(auto intro: widen_trans simp add: conf_def)
hence "Φ ⊢ t:(None, h, ?f # frs) √"
using meth Φ' heap_ok Φ_pc frames tconf preh by fastforce }
with ins meth si' stk' a ha no_x idxI idx
show ?thesis by(auto simp del: correct_state_def split: if_split_asm)
next
case False
with stk' idxI ins no_x heap_ok tconf meth a ha Xel Φ_pc frame frames
wf_preallocatedD[OF wf, of h ArrayIndexOutOfBounds]
show ?thesis
by (fastforce simp: preh split: if_split_asm simp del: Listn.lesub_list_impl_same_size)
qed
qed
qed
lemma AStore_correct:
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 = AStore"
assumes wt: "P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M"
assumes conf: "Φ ⊢ t: (None, h, (stk,loc,C,M,pc)#frs)√"
assumes no_x: "(tas, σ) ∈ exec_instr (ins!pc) P t h stk loc C M pc frs"
shows "Φ ⊢ t: σ √"
proof -
from ins conf meth
obtain ST LT where
heap_ok: "hconf h" and
tconf: "P,h ⊢ t √t" 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
frame: "conf_f P h (ST,LT) ins (stk,loc,C,M,pc)" and
frames: "conf_fs P h Φ M (size Ts) T frs" and
preh: "preallocated h"
by (auto dest: sees_method_fun)
from ins wt Φ_pc have lST: "length ST > 2" by(auto)
show ?thesis
proof(cases "hd (tl (tl stk)) = Null")
case True
with ins no_x heap_ok tconf Φ_pc stk loc frame frames meth wf_preallocatedD[OF wf, of h NullPointer] preh
show ?thesis by(fastforce)
next
case False
note stkNN = this
have STNN: "hd (tl (tl ST)) ≠ NT"
proof
assume "hd (tl (tl ST)) = NT"
moreover
from frame have "P,h ⊢ stk [:≤] ST" by simp
with lST have "P,h ⊢ hd (tl (tl stk)) :≤ hd (tl (tl ST))"
by (cases ST, auto, case_tac list, auto, case_tac lista, auto)
ultimately
have "hd (tl (tl stk)) = Null" by simp
with stkNN show False by contradiction
qed
with ins stkNN Φ_pc wt obtain ST'' Y X ST' LT' where
ST: "ST = Y # Integer # X⌊⌉ # ST''" and
pc': "pc+1 < size ins" and
Φ': "Φ C M ! (pc+1) = Some (ST', LT')" and
ST': "P ⊢ ST'' [≤] ST'" and LT': "P ⊢ LT [≤⇩⊤] LT'" and
suc_pc: "pc+1 < size ins"
by(fastforce)
from stk ST obtain ref e idx stk' where
stk': "stk = e#idx#ref#stk'" and
idx: "P,h ⊢ idx :≤ Integer" and
ref: "P,h ⊢ ref :≤ X⌊⌉" and
e: "P,h ⊢ e :≤ Y" and
ST'': "P,h ⊢ stk' [:≤] ST''"
by auto
from stkNN stk' have "ref ≠ Null" by(simp)
with ref obtain a Xel n
where a: "ref = Addr a"
and ha: "typeof_addr h a = ⌊Array_type Xel n⌋"
and Xel: "P ⊢ Xel ≤ X"
by(cases ref)(fastforce simp add: conf_def widen_Array)+
from idx obtain idxI where idxI: "idx = Intg idxI"
by(auto simp add: conf_def)
show ?thesis
proof(cases "0 <=s idxI ∧ sint idxI < int n")
case True
hence si': "0 <=s idxI" "sint idxI < int n" by simp_all
from e obtain Te where Te: "typeof⇘h⇙ e = ⌊Te⌋" "P ⊢ Te ≤ Y"
by(auto simp add: conf_def)
show ?thesis
proof(cases "P ⊢ Te ≤ Xel")
case True
with Te have eXel: "P,h ⊢ e :≤ Xel"
by(auto simp add: conf_def intro: widen_trans)
{ fix h'
assume "write": "heap_write h a (ACell (nat (sint idxI))) e h'"
hence hext: "h ⊴ h'" by(rule hext_heap_write)
with preh have preh': "preallocated h'" by(rule preallocated_hext)
let ?f = "(stk', loc, C, M, pc + 1)"
from si' have "nat (sint idxI) < n"
by (simp add: word_sle_eq nat_less_iff)
with ha have "P,h ⊢ a@ACell (nat (sint idxI)) : Xel" ..
with "write" heap_ok have heap_ok': "hconf h'" using eXel
by(rule hconf_heap_write_mono)
moreover
from ST stk stk' ST' have "P,h ⊢ stk' [:≤] ST'" by auto
with hext have stk'': "P,h' ⊢ stk' [:≤] ST'"
by- (rule confs_hext)
moreover
from loc LT' have "P,h ⊢ loc [:≤⇩⊤] LT'" ..
with hext have "P,h' ⊢ loc [:≤⇩⊤] LT'" by - (rule confTs_hext)
moreover
with frame ST' ST LT' suc_pc wf Xel idxI si' stk''
have "conf_f P h' (ST', LT') ins ?f"
by(clarsimp)
with frames hext have "conf_fs P h' Φ M (size Ts) T frs" by- (rule conf_fs_hext)
moreover from tconf hext have "P,h' ⊢ t √t" by(rule tconf_hext_mono)
ultimately have "Φ ⊢ t:(None, h', ?f # frs) √" using meth Φ' Φ_pc suc_pc preh'
by(fastforce) }
with True si' ins meth stk' a ha no_x idxI idx Te
show ?thesis
by(auto split: if_split_asm simp del: correct_state_def intro: widen_trans)
next
case False
with stk' idxI ins no_x heap_ok tconf meth a ha Xel Te Φ_pc frame frames si'
wf_preallocatedD[OF wf, of h ArrayStore]
show ?thesis
by (fastforce split: if_splits list.splits simp: preh
simp del: Listn.lesub_list_impl_same_size)
qed
next
case False
with stk' idxI ins no_x heap_ok tconf meth a ha Xel Φ_pc frame frames preh
wf_preallocatedD[OF wf, of h ArrayIndexOutOfBounds]
show ?thesis by(fastforce split: if_split_asm)
qed
qed
qed
lemma ALength_correct:
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 = ALength"
assumes wt: "P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M"
assumes conf: "Φ ⊢ t: (None, h, (stk,loc,C,M,pc)#frs)√"
assumes no_x: "(tas, σ) ∈ exec_instr (ins!pc) P t h stk loc C M pc frs"
shows "Φ ⊢ t: σ √"
proof -
from ins conf meth
obtain ST LT where
heap_ok: "hconf h" and
tconf: "P,h ⊢ t √t" 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
frame: "conf_f P h (ST,LT) ins (stk,loc,C,M,pc)" and
frames: "conf_fs P h Φ M (size Ts) T frs" and
preh: "preallocated h"
by (auto dest: sees_method_fun)
from ins wt Φ_pc have lST: "length ST > 0" by(auto)
show ?thesis
proof(cases "hd stk = Null")
case True
with ins no_x heap_ok tconf Φ_pc stk loc frame frames meth wf_preallocatedD[OF wf, of h NullPointer] preh
show ?thesis by(fastforce)
next
case False
note stkNN = this
have STNN: "hd ST ≠ NT"
proof
assume "hd ST = NT"
moreover
from frame have "P,h ⊢ stk [:≤] ST" by simp
with lST have "P,h ⊢ hd stk :≤ hd ST"
by (cases ST, auto)
ultimately
have "hd stk = Null" by simp
with stkNN show False by contradiction
qed
with stkNN ins Φ_pc wt obtain ST'' X ST' LT' where
ST: "ST = (X⌊⌉) # ST''" and
pc': "pc+1 < size ins" and
Φ': "Φ C M ! (pc+1) = Some (ST', LT')" and
ST': "P ⊢ (Integer # ST'') [≤] ST'" and LT': "P ⊢ LT [≤⇩⊤] LT'" and
suc_pc: "pc+1 < size ins"
by(fastforce)
from stk ST obtain ref stk' where
stk': "stk = ref#stk'" and
ref: "P,h ⊢ ref :≤ X⌊⌉" and
ST'': "P,h ⊢ stk' [:≤] ST''"
by auto
from stkNN stk' have "ref ≠ Null" by(simp)
with ref obtain a Xel n
where a: "ref = Addr a"
and ha: "typeof_addr h a = ⌊Array_type Xel n⌋"
and Xel: "P ⊢ Xel ≤ X"
by(cases ref)(fastforce simp add: conf_def widen_Array)+
from ins meth stk' a ha no_x have σ':
"σ = (None, h, (Intg (word_of_int (int n)) # stk', loc, C, M, pc + 1) # frs)"
(is "σ = (None, h, ?f # frs)")
by(auto)
moreover
from ST stk stk' ST' have "P,h ⊢ Intg si # stk' [:≤] ST'" by(auto)
with frame ST' ST LT' suc_pc wf
have "conf_f P h (ST', LT') ins ?f"
by(fastforce intro: widen_trans)
ultimately show ?thesis using meth Φ' heap_ok Φ_pc frames tconf preh by fastforce
qed
qed
lemma MEnter_correct:
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 = MEnter"
assumes wt: "P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M"
assumes conf: "Φ ⊢ t: (None, h, (stk,loc,C,M,pc)#frs)√"
assumes no_x: "(tas, σ) ∈ exec_instr (ins!pc) P t h stk loc C M pc frs"
shows "Φ ⊢ t: σ √"
proof -
from ins conf meth
obtain ST LT where
heap_ok: "hconf h" and
tconf: "P,h ⊢ t √t" 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
frame: "conf_f P h (ST,LT) ins (stk,loc,C,M,pc)" and
frames: "conf_fs P h Φ M (size Ts) T frs" and
preh: "preallocated h"
by (auto dest: sees_method_fun)
from ins wt Φ_pc have lST: "length ST > 0" by(auto)
show ?thesis
proof(cases "hd stk = Null")
case True
with ins no_x heap_ok tconf Φ_pc stk loc frame frames meth wf_preallocatedD[OF wf, of h NullPointer] preh
show ?thesis by(fastforce)
next
case False
note stkNN = this
have STNN: "hd ST ≠ NT"
proof
assume "hd ST = NT"
moreover
from frame have "P,h ⊢ stk [:≤] ST" by simp
with lST have "P,h ⊢ hd stk :≤ hd ST"
by (cases ST, auto)
ultimately
have "hd stk = Null" by simp
with stkNN show False by contradiction
qed
with stkNN ins Φ_pc wt obtain ST'' X ST' LT' where
ST: "ST = X # ST''" and
refT: "is_refT X" and
pc': "pc+1 < size ins" and
Φ': "Φ C M ! (pc+1) = Some (ST', LT')" and
ST': "P ⊢ ST'' [≤] ST'" and LT': "P ⊢ LT [≤⇩⊤] LT'" and
suc_pc: "pc+1 < size ins"
by(fastforce)
from stk ST obtain ref stk' where
stk': "stk = ref#stk'" and
ref: "P,h ⊢ ref :≤ X"
by auto
from stkNN stk' have "ref ≠ Null" by(simp)
moreover
from loc LT' have "P,h ⊢ loc [:≤⇩⊤] LT'" ..
moreover
from ST stk stk' ST'
have "P,h ⊢ stk' [:≤] ST'" by(auto)
ultimately show ?thesis using meth Φ' heap_ok Φ_pc suc_pc frames loc LT' no_x ins stk' ST' tconf preh
by(fastforce)
qed
qed
lemma MExit_correct:
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 = MExit"
assumes wt: "P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M"
assumes conf: "Φ ⊢ t: (None, h, (stk,loc,C,M,pc)#frs)√"
assumes no_x: "(tas, σ) ∈ exec_instr (ins!pc) P t h stk loc C M pc frs"
shows "Φ ⊢ t: σ √"
proof -
from ins conf meth
obtain ST LT where
heap_ok: "hconf h" and
tconf: "P,h ⊢ t √t" 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
frame: "conf_f P h (ST,LT) ins (stk,loc,C,M,pc)" and
frames: "conf_fs P h Φ M (size Ts) T frs" and
preh: "preallocated h"
by (auto dest: sees_method_fun)
from ins wt Φ_pc have lST: "length ST > 0" by(auto)
show ?thesis
proof(cases "hd stk = Null")
case True
with ins no_x heap_ok tconf Φ_pc stk loc frame frames meth wf_preallocatedD[OF wf, of h NullPointer] preh
show ?thesis by(fastforce)
next
case False
note stkNN = this
have STNN: "hd ST ≠ NT"
proof
assume "hd ST = NT"
moreover
from frame have "P,h ⊢ stk [:≤] ST" by simp
with lST have "P,h ⊢ hd stk :≤ hd ST"
by (cases ST, auto)
ultimately
have "hd stk = Null" by simp
with stkNN show False by contradiction
qed
with stkNN ins Φ_pc wt obtain ST'' X ST' LT' where
ST: "ST = X # ST''" and
refT: "is_refT X" and
pc': "pc+1 < size ins" and
Φ': "Φ C M ! (pc+1) = Some (ST', LT')" and
ST': "P ⊢ ST'' [≤] ST'" and LT': "P ⊢ LT [≤⇩⊤] LT'" and
suc_pc: "pc+1 < size ins"
by(fastforce)
from stk ST obtain ref stk' where
stk': "stk = ref#stk'" and
ref: "P,h ⊢ ref :≤ X"
by auto
from stkNN stk' have "ref ≠ Null" by(simp)
moreover
from loc LT' have "P,h ⊢ loc [:≤⇩⊤] LT'" ..
moreover
from ST stk stk' ST'
have "P,h ⊢ stk' [:≤] ST'" by(auto)
ultimately
show ?thesis using meth Φ' heap_ok Φ_pc suc_pc frames loc LT' no_x ins stk' ST' tconf frame preh
wf_preallocatedD[OF wf, of h IllegalMonitorState]
by(fastforce)
qed
qed
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;
(tas, σ') ∈ exec P t (None, h, (stk,loc,C,M,pc)#frs);
Φ ⊢ t: (None, h, (stk,loc,C,M,pc)#frs)√ ⟧
⟹ Φ ⊢ t: σ'√"
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(unfold exec.simps Let_def set_map)
apply (frule wt_jvm_progD, erule exE)
apply (cases "ins ! pc")
apply (rule Load_correct, assumption+, fastforce)
apply (rule Store_correct, assumption+, fastforce)
apply (rule Push_correct, assumption+, fastforce)
apply (rule New_correct, assumption+, fastforce)
apply (rule NewArray_correct, assumption+, fastforce)
apply (rule ALoad_correct, assumption+, fastforce)
apply (rule AStore_correct, assumption+, fastforce)
apply (rule ALength_correct, assumption+, fastforce)
apply (rule Getfield_correct, assumption+, fastforce)
apply (rule Putfield_correct, assumption+, fastforce)
apply (rule CAS_correct, assumption+, fastforce)
apply (rule Checkcast_correct, assumption+, fastforce)
apply (rule Instanceof_correct, assumption+, fastforce)
apply (rule Invoke_correct, assumption+, fastforce)
apply (rule Return_correct, assumption+, fastforce simp add: split_beta)
apply (rule Pop_correct, assumption+, fastforce)
apply (rule Dup_correct, assumption+, fastforce)
apply (rule Swap_correct, assumption+, fastforce)
apply (rule BinOp_correct, assumption+, fastforce)
apply (rule Goto_correct, assumption+, fastforce)
apply (rule IfFalse_correct, assumption+, fastforce)
apply (rule Throw_correct, assumption+, fastforce)
apply (rule MEnter_correct, assumption+, fastforce)
apply (rule MExit_correct, assumption+, fastforce)
done
declare defs1 [simp del]
end
subsection ‹Main›
lemma (in JVM_conf_read) BV_correct_1 [rule_format]:
"⋀σ. ⟦ wf_jvm_prog⇘Φ⇙ P; Φ ⊢ t: σ√⟧ ⟹ P,t ⊢ σ -tas-jvm→ σ' ⟶ Φ ⊢ t: σ'√"
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 clarify
apply(case_tac frs)
apply simp
apply(clarsimp simp only: exec.simps set_simps)
apply(erule (1) exception_step_conform)
done
theorem (in JVM_progress) progress:
assumes wt: "wf_jvm_prog⇘Φ⇙ P"
and cs: "Φ ⊢ t: (xcp, h, f # frs)√"
shows "∃ta σ'. P,t ⊢ (xcp, h, f # frs) -ta-jvm→ σ'"
proof -
obtain stk loc C M pc where f: "f = (stk, loc, C, M, pc)" by(cases f)
with cs obtain Ts T mxs mxl⇩0 "is" xt ST LT
where hconf: "hconf h"
and sees: "P ⊢ C sees M: Ts→T = ⌊(mxs, mxl⇩0, is, xt)⌋ in C"
and Φ_pc: "Φ C M ! pc = ⌊(ST, LT)⌋"
and ST: "P,h ⊢ stk [:≤] ST"
and LT: "P,h ⊢ loc [:≤⇩⊤] LT"
and pc: "pc < length is"
by(auto simp add: defs1)
show ?thesis
proof(cases xcp)
case Some thus ?thesis
unfolding f exec_1_iff by auto
next
case [simp]: None
note [simp del] = split_paired_Ex
note [simp] = defs1 list_all2_Cons2
from wt obtain wf_md where wf: "wf_prog wf_md P" by(auto dest: wt_jvm_progD)
from wt sees pc have wt: "P,T,mxs,size is,xt ⊢ is!pc,pc :: Φ C M"
by(rule wt_jvm_prog_impl_wt_instr)
have "∃ta σ'. (ta, σ') ∈ exec_instr (is ! pc) P t h stk loc C M pc frs"
proof(cases "is ! pc")
case [simp]: ALoad
with wt Φ_pc have lST: "length ST > 1" by(auto)
show ?thesis
proof(cases "hd (tl stk) = Null")
case True thus ?thesis by simp
next
case False
have STNN: "hd (tl ST) ≠ NT"
proof
assume "hd (tl ST) = NT"
moreover
from ST lST have "P,h ⊢ hd (tl stk) :≤ hd (tl ST)"
by (cases ST)(auto, case_tac list, auto)
ultimately have "hd (tl stk) = Null" by simp
with False show False by contradiction
qed
with False Φ_pc wt obtain ST'' X where "ST = Integer # X⌊⌉ # ST''" by auto
with ST obtain ref idx stk' where stk': "stk = idx#ref#stk'" and idx: "P,h ⊢ idx :≤ Integer"
and ref: "P,h ⊢ ref :≤ X⌊⌉" by(auto)
from False stk' have "ref ≠ Null" by(simp)
with ref obtain a Xel n where a: "ref = Addr a"
and ha: "typeof_addr h a = ⌊Array_type Xel n⌋"
and Xel: "P ⊢ Xel ≤ X"
by(cases ref)(fastforce simp add: conf_def widen_Array)+
from idx obtain idxI where idxI: "idx = Intg idxI"
by(auto simp add: conf_def)
show ?thesis
proof(cases "0 <=s idxI ∧ sint idxI < int n")
case True
hence si': "0 <=s idxI" "sint idxI < int n" by auto
hence "nat (sint idxI) < n"
by (simp add: word_sle_eq nat_less_iff)
with ha have al: "P,h ⊢ a@ACell (nat (sint idxI)) : Xel" ..
from heap_read_total[OF hconf this] True False ha stk' idxI a
show ?thesis by auto
next
case False with ha stk' idxI a show ?thesis by auto
qed
qed
next
case [simp]: AStore
from wt Φ_pc have lST: "length ST > 2" by(auto)
show ?thesis
proof(cases "hd (tl (tl stk)) = Null")
case True thus ?thesis by(fastforce)
next
case False
note stkNN = this
have STNN: "hd (tl (tl ST)) ≠ NT"
proof
assume "hd (tl (tl ST)) = NT"
moreover
from ST lST have "P,h ⊢ hd (tl (tl stk)) :≤ hd (tl (tl ST))"
by (cases ST, auto, case_tac list, auto, case_tac lista, auto)
ultimately have "hd (tl (tl stk)) = Null" by simp
with stkNN show False by contradiction
qed
with stkNN Φ_pc wt obtain ST'' Y X
where "ST = Y # Integer # X⌊⌉ # ST''" by(fastforce)
with ST obtain ref e idx stk' where stk': "stk = e#idx#ref#stk'"
and idx: "P,h ⊢ idx :≤ Integer" and ref: "P,h ⊢ ref :≤ X⌊⌉"
and e: "P,h ⊢ e :≤ Y" by auto
from stkNN stk' have "ref ≠ Null" by(simp)
with ref obtain a Xel n where a: "ref = Addr a"
and ha: "typeof_addr h a = ⌊Array_type Xel n⌋"
and Xel: "P ⊢ Xel ≤ X"
by(cases ref)(fastforce simp add: conf_def widen_Array)+
from idx obtain idxI where idxI: "idx = Intg idxI"
by(auto simp add: conf_def)
show ?thesis
proof(cases "0 <=s idxI ∧ sint idxI < int n")
case True
hence si': "0 <=s idxI" "sint idxI < int n" by simp_all
hence "nat (sint idxI) < n"
by (simp add: word_sle_eq nat_less_iff)
with ha have adal: "P,h ⊢ a@ACell (nat (sint idxI)) : Xel" ..
show ?thesis
proof(cases "P ⊢ the (typeof⇘h⇙ e) ≤ Xel")
case False
with ha stk' idxI a show ?thesis by auto
next
case True
hence "P,h ⊢ e :≤ Xel" using e by(auto simp add: conf_def)
from heap_write_total[OF hconf adal this] ha stk' idxI a show ?thesis by auto
qed
next
case False with ha stk' idxI a show ?thesis by auto
qed
qed
next
case [simp]: (Getfield F D)
from Φ_pc wt obtain oT ST'' vT fm where oT: "P ⊢ oT ≤ Class D"
and "ST = oT # ST''" and F: "P ⊢ D sees F:vT (fm) in D"
by fastforce
with ST obtain ref stk' where stk': "stk = ref#stk'"
and ref: "P,h ⊢ ref :≤ oT" by auto
show ?thesis
proof(cases "ref = Null")
case True thus ?thesis using stk' by auto
next
case False
from ref oT have "P,h ⊢ ref :≤ Class D" ..
with False obtain a U' D' where
a: "ref = Addr a" and h: "typeof_addr h a = Some U'"
and U': "D' = class_type_of U'" and D': "P ⊢ D' ≼⇧* D"
by (blast dest: non_npD2)
from D' F have has_field: "P ⊢ D' has F:vT (fm) in D"
by (blast intro: has_field_mono has_visible_field)
with h have "P,h ⊢ a@CField D F : vT" unfolding U' ..
from heap_read_total[OF hconf this]
show ?thesis using stk' a by auto
qed
next
case [simp]: (Putfield F D)
from Φ_pc wt obtain vT vT' oT ST'' fm where "ST = vT # oT # ST''"
and field: "P ⊢ D sees F:vT' (fm) in D"
and oT: "P ⊢ oT ≤ Class D"
and vT': "P ⊢ vT ≤ vT'" by fastforce
with ST obtain v ref stk' where stk': "stk = v#ref#stk'"
and ref: "P,h ⊢ ref :≤ oT"
and v: "P,h ⊢ v :≤ vT" by auto
show ?thesis
proof(cases "ref = Null")
case True with stk' show ?thesis by auto
next
case False
from ref oT have "P,h ⊢ ref :≤ Class D" ..
with False obtain a U' D' where
a: "ref = Addr a" and h: "typeof_addr h a = Some U'" and
U': "D' = class_type_of U'" and D': "P ⊢ D' ≼⇧* D"
by (blast dest: non_npD2)
from field D' have has_field: "P ⊢ D' has F:vT' (fm) in D"
by (blast intro: has_field_mono has_visible_field)
with h have al: "P,h ⊢ a@CField D F : vT'" unfolding U' ..
from v vT' have "P,h ⊢ v :≤ vT'" by auto
from heap_write_total[OF hconf al this] v a stk' h show ?thesis by auto
qed
next
case [simp]: (CAS F D)
from Φ_pc wt obtain T' T1 T2 T3 ST'' fm where "ST = T3 # T2 # T1 # ST''"
and field: "P ⊢ D sees F:T' (fm) in D"
and oT: "P ⊢ T1 ≤ Class D"
and vT': "P ⊢ T2 ≤ T'" "P ⊢ T3 ≤ T'" by fastforce
with ST obtain v v' v'' stk' where stk': "stk = v''#v'#v#stk'"
and v: "P,h ⊢ v :≤ T1"
and v': "P,h ⊢ v' :≤ T2"
and v'': "P,h ⊢ v'' :≤ T3" by auto
show ?thesis
proof(cases "v= Null")
case True with stk' show ?thesis by auto
next
case False
from v oT have "P,h ⊢ v :≤ Class D" ..
with False obtain a U' D' where
a: "v = Addr a" and h: "typeof_addr h a = Some U'" and
U': "D' = class_type_of U'" and D': "P ⊢ D' ≼⇧* D"
by (blast dest: non_npD2)
from field D' have has_field: "P ⊢ D' has F:T' (fm) in D"
by (blast intro: has_field_mono has_visible_field)
with h have al: "P,h ⊢ a@CField D F : T'" unfolding U' ..
from v' vT' have "P,h ⊢ v' :≤ T'" by auto
from heap_read_total[OF hconf al] obtain v''' where v''': "heap_read h a (CField D F) v'''" by blast
show ?thesis
proof(cases "v''' = v'")
case True
from v'' vT' have "P,h ⊢ v'' :≤ T'" by auto
from heap_write_total[OF hconf al this] v a stk' h v''' True show ?thesis by auto
next
case False
from v''' v a stk' h False show ?thesis by auto
qed
qed
next
case [simp]: (Invoke M' n)
from wt Φ_pc have n: "n < size ST" by simp
show ?thesis
proof(cases "stk!n = Null")
case True thus ?thesis by simp
next
case False
note Null = this
have NT: "ST!n ≠ NT"
proof
assume "ST!n = NT"
moreover from ST n have "P,h ⊢ stk!n :≤ ST!n" by (simp add: list_all2_conv_all_nth)
ultimately have "stk!n = Null" by simp
with Null show False by contradiction
qed
from NT wt Φ_pc obtain D D' Ts T m
where D: "class_type_of' (ST!n) = Some D"
and m_D: "P ⊢ D sees M': Ts→T = m in D'"
and Ts: "P ⊢ rev (take n ST) [≤] Ts"
by auto
from n ST D have "P,h ⊢ stk!n :≤ ST!n"
by (auto simp add: list_all2_conv_all_nth)
from ‹P,h ⊢ stk!n :≤ ST!n› Null D
obtain a T' where
Addr: "stk!n = Addr a" and
obj: "typeof_addr h a = Some T'" and
T'subSTn: "P ⊢ ty_of_htype T' ≤ ST ! n"
by(cases "stk ! n")(auto simp add: conf_def widen_Class)
from D T'subSTn obtain C' where
C': "class_type_of' (ty_of_htype T') = ⌊C'⌋" and C'subD: "P ⊢ C' ≼⇧* D"
by(rule widen_is_class_type_of) simp
from Call_lemma[OF m_D C'subD wf]
obtain D' Ts' T' m'
where Call': "P ⊢ C' sees M': Ts'→T' = m' in D'" "P ⊢ Ts [≤] Ts'"
"P ⊢ T' ≤ T" "P ⊢ C' ≼⇧* D'" "is_type P T'" "∀T∈set Ts'. is_type P T"
by blast
show ?thesis
proof(cases m')
case Some with Call' C' obj Addr C' C'subD show ?thesis by(auto)
next
case [simp]: None
from ST have "P,h ⊢ take n stk [:≤] take n ST" by(rule list_all2_takeI)
then obtain Us where "map typeof⇘h⇙ (take n stk) = map Some Us" "P ⊢ Us [≤] take n ST"
by(auto simp add: confs_conv_map)
hence Us: "map typeof⇘h⇙ (rev (take n stk)) = map Some (rev Us)" "P ⊢ rev Us [≤] rev (take n ST)"
by- (simp only: rev_map[symmetric], simp)
with Ts ‹P ⊢ Ts [≤] Ts'› have "P ⊢ rev Us [≤] Ts'" by(blast intro: widens_trans)
with obj Us Call' C' have "P,h ⊢ a∙M'(rev (take n stk)) : T'"
by(auto intro!: external_WT'.intros)
from external_call_progress[OF wf this hconf, of t] obj Addr Call' C'
show ?thesis by(auto dest!: red_external_imp_red_external_aggr)
qed
qed
qed(auto 4 4 simp add: split_beta split: if_split_asm)
thus ?thesis using sees None
unfolding f exec_1_iff by(simp del: split_paired_Ex)
qed
qed
lemma (in JVM_heap_conf) BV_correct_initial:
shows "⟦ wf_jvm_prog⇘Φ⇙ P; start_heap_ok; P ⊢ C sees M:Ts→T = ⌊m⌋ in D; P,start_heap ⊢ vs [:≤] Ts ⟧
⟹ Φ ⊢ start_tid:JVM_start_state' P C M vs √"
apply (cases m)
apply (unfold JVM_start_state'_def)
apply (unfold correct_state_def)
apply (clarsimp)
apply (frule wt_jvm_progD)
apply (erule exE)
apply (frule wf_prog_wf_syscls)
apply (rule conjI)
apply(erule (1) tconf_start_heap_start_tid)
apply(rule conjI)
apply (simp add: wf_jvm_prog_phi_def hconf_start_heap)
apply(frule sees_method_idemp)
apply (frule wt_jvm_prog_impl_wt_start, assumption+)
apply (unfold conf_f_def wt_start_def)
apply(auto simp add: sup_state_opt_any_Some)
apply(erule preallocated_start_heap)
apply(rule exI conjI|assumption)+
apply(auto simp add: list_all2_append1)
apply(auto dest: list_all2_lengthD intro!: exI)
done
end