Theory BVNoTypeError
section ‹Welltyped Programs produce no Type Errors›
theory BVNoTypeError
imports
"../JVM/JVMDefensive"
BVSpecTypeSafe
begin
lemma wt_jvm_prog_states:
"⟦ wf_jvm_prog⇘Φ⇙ P; P ⊢ C sees M: Ts→T = ⌊(mxs, mxl, ins, et)⌋ in C;
Φ C M ! pc = τ; pc < size ins ⟧
⟹ OK τ ∈ states P mxs (1+size Ts+mxl)"
apply (unfold wf_jvm_prog_phi_def)
apply (drule (1) sees_wf_mdecl)
apply (simp add: wf_mdecl_def wt_method_def check_types_def)
apply (blast intro: nth_in)
done
context JVM_heap_conf_base' begin
declare is_IntgI [simp, intro]
declare is_BoolI [simp, intro]
declare is_RefI [simp]
text ‹
The main theorem: welltyped programs do not produce type errors if they
are started in a conformant state.
›
theorem no_type_error:
assumes welltyped: "wf_jvm_prog⇘Φ⇙ P" and conforms: "Φ ⊢ t:σ √"
shows "exec_d P t σ ≠ TypeError"
proof -
from welltyped obtain mb where wf: "wf_prog mb P" by (fast dest: wt_jvm_progD)
obtain xcp h frs where s [simp]: "σ = (xcp, h, frs)" by (cases σ)
have "check P σ"
proof(cases frs)
case Nil with conforms show ?thesis by (unfold correct_state_def check_def) auto
next
case (Cons f frs')
then obtain stk reg C M pc where frs [simp]: "frs = (stk,reg,C,M,pc)#frs'"
and f: "f = (stk,reg,C,M,pc)" by(cases f) fastforce
from conforms obtain ST LT Ts T mxs mxl ins xt where
hconf: "hconf h" and
tconf: "P,h ⊢ t √t" and
meth: "P ⊢ C sees M:Ts→T = ⌊(mxs, mxl, ins, xt)⌋ in C" and
Φ: "Φ C M ! pc = Some (ST,LT)" and
frame: "conf_f P h (ST,LT) ins (stk,reg,C,M,pc)" and
frames: "conf_fs P h Φ M (size Ts) T frs'" and
confxcp: "conf_xcp P h xcp (ins ! pc)"
by (fastforce simp add: correct_state_def dest: sees_method_fun)
from frame obtain
stk: "P,h ⊢ stk [:≤] ST" and
reg: "P,h ⊢ reg [:≤⇩⊤] LT" and
pc: "pc < size ins"
by (simp add: conf_f_def)
from welltyped meth Φ pc
have "OK (Some (ST, LT)) ∈ states P mxs (1+size Ts+mxl)"
by (rule wt_jvm_prog_states)
hence "size ST ≤ mxs" by (auto simp add: JVM_states_unfold listE_length)
with stk have mxs: "size stk ≤ mxs"
by (auto dest: list_all2_lengthD)
from welltyped meth pc
have "P,T,mxs,size ins,xt ⊢ ins!pc,pc :: Φ C M"
by (rule wt_jvm_prog_impl_wt_instr)
hence app⇩0: "app (ins!pc) P mxs T pc (size ins) xt (Φ C M!pc) "
by (simp add: wt_instr_def)
with Φ have eff:
"∀(pc',s')∈set (eff (ins ! pc) P pc xt (Φ C M ! pc)). pc' < size ins"
by (unfold app_def) simp
from app⇩0 Φ have app:
"xcpt_app (ins!pc) P pc mxs xt (ST,LT) ∧ app⇩i (ins!pc, P, pc, mxs, T, (ST,LT))"
by (clarsimp simp add: app_def)
show ?thesis
proof(cases xcp)
case None
note xcp[simp] = this
from app eff stk reg
have "check_instr (ins!pc) P h stk reg C M pc frs'"
proof (cases "ins!pc")
case ALoad
with app stk reg Φ obtain T ST' where
ST: "ST = Integer # T # ST'" and
TNT: "T ≠ NT ⟶ (∃T'. T = T'⌊⌉)"
by auto
from stk ST obtain i stk' ref where
stk': "stk = Intg i # ref # stk'" and
ref: "P,h ⊢ ref :≤ T"
by(auto simp add: conf_def list_all2_Cons2)
from ref TNT have is_Ref: "is_Ref ref"
by(cases ref)(auto simp add: is_Ref_def conf_def)
moreover
{ assume refN: "ref ≠ Null"
with ref have "T ≠ NT" by auto
with TNT obtain T' where T': "T = T'⌊⌉" by auto
with ref refN is_Ref wf
have "∃T n. typeof_addr h (the_Addr ref) = ⌊Array_type T n⌋"
by(cases ref)(auto simp add:conf_def widen_Array) }
ultimately show ?thesis using ALoad stk'
by(auto)
next
case AStore
with app stk reg Φ obtain T U ST' where
ST: "ST = T # Integer # U # ST'" and
TNT: "U ≠ NT ⟶ (∃T'. U = T'⌊⌉)"
by auto
from stk ST obtain e i stk' ref where
stk': "stk = e # Intg i # ref # stk'" and
ref: "P,h ⊢ ref :≤ U" and
e: "P,h ⊢ e :≤ T"
by(fastforce simp add: conf_def list_all2_Cons2)
from ref TNT have is_Ref: "is_Ref ref"
by(cases ref)(auto simp add: is_Ref_def conf_def)
moreover
{ assume refN: "ref ≠ Null"
with ref have "U ≠ NT" by auto
with TNT obtain T' where T': "U = T'⌊⌉" by auto
with ref refN is_Ref wf
have "∃T n. typeof_addr h (the_Addr ref) = ⌊Array_type T n⌋"
by(cases ref)(auto simp add:conf_def widen_Array) }
ultimately show ?thesis using AStore stk' e by(auto simp add: conf_def)
next
case ALength
with app stk reg Φ obtain T ST' where
ST: "ST = T # ST'" and
TNT: "T ≠ NT ⟶ (∃T'. T = T'⌊⌉)"
by auto
from stk ST obtain stk' ref where
stk': "stk = ref # stk'" and
ref: "P,h ⊢ ref :≤ T"
by(auto simp add: conf_def list_all2_Cons2)
from ref TNT have is_Ref: "is_Ref ref"
by(cases ref)(auto simp add: is_Ref_def conf_def)
moreover
{ assume refN: "ref ≠ Null"
with ref have "T ≠ NT" by auto
with TNT obtain T' where T': "T = T'⌊⌉" by auto
with ref refN is_Ref wf
have "∃T n. typeof_addr h (the_Addr ref) = ⌊Array_type T n⌋"
by(cases ref)(auto simp add:conf_def widen_Array) }
ultimately show ?thesis using ALength stk'
by(auto)
next
case (Getfield F C)
with app stk reg Φ obtain v vT stk' fm where
field: "P ⊢ C sees F:vT (fm) in C" and
stk: "stk = v # stk'" and
conf: "P,h ⊢ v :≤ Class C"
by(fastforce simp add: list_all2_Cons2)
from conf have is_Ref: "is_Ref v" by(cases v)(auto simp add: is_Ref_def conf_def)
moreover {
assume "v ≠ Null"
with conf field is_Ref wf
have "∃U. typeof_addr h (the_Addr v) = Some U ∧ P ⊢ class_type_of U ≼⇧* C"
by (auto dest!: non_npD2)
}
ultimately show ?thesis using Getfield field stk by auto
next
case (Putfield F C)
with app stk reg Φ obtain v ref vT stk' fm where
field: "P ⊢ C sees F:vT (fm) in C" and
stk: "stk = v # ref # stk'" and
confv: "P,h ⊢ v :≤ vT" and
confr: "P,h ⊢ ref :≤ Class C"
by(fastforce simp add: list_all2_Cons2)
from confr have is_Ref: "is_Ref ref"
by(cases ref)(auto simp add: is_Ref_def conf_def)
moreover {
assume "ref ≠ Null"
with confr field is_Ref wf
have "∃U. typeof_addr h (the_Addr ref) = Some U ∧ P ⊢ class_type_of U ≼⇧* C"
by (auto dest: non_npD2)
}
ultimately show ?thesis using Putfield field stk confv by auto
next
case (CAS F C)
with app stk reg Φ obtain v v' v'' T' stk' fm where
field: "P ⊢ C sees F:T' (fm) in C" and
stk: "stk = v'' # v' # v # stk'" and
confv: "P,h ⊢ v' :≤ T'" "P,h ⊢ v'' :≤ T'" and
confr: "P,h ⊢ v :≤ Class C" and vol: "volatile fm"
by(fastforce simp add: list_all2_Cons2)
from confr have is_Ref: "is_Ref v"
by(cases v)(auto simp add: is_Ref_def conf_def)
moreover {
assume "v ≠ Null"
with confr field is_Ref wf
have "∃U. typeof_addr h (the_Addr v) = Some U ∧ P ⊢ class_type_of U ≼⇧* C"
by (auto dest: non_npD2)
}
ultimately show ?thesis using CAS field stk confv vol by auto
next
case (Invoke M' n)
with app have n: "n < size ST" by simp
from stk have [simp]: "size stk = size ST" by (rule list_all2_lengthD)
{ assume "stk!n = Null" with n Invoke have ?thesis by simp }
moreover {
assume "ST!n = NT"
with n stk have "stk!n = Null" by (auto simp: list_all2_conv_all_nth)
with n Invoke have ?thesis by simp
}
moreover {
assume Null: "stk!n ≠ Null" and NT: "ST!n ≠ NT"
from NT app Invoke
obtain D D' Ts T m
where D: "class_type_of' (ST!n) = ⌊D⌋"
and M': "P ⊢ D sees M': Ts→T = m in D'"
and Ts: "P ⊢ rev (take n ST) [≤] Ts" by auto
from stk n have "P,h ⊢ stk!n :≤ ST!n"
by (auto simp: list_all2_conv_all_nth)
with Null D obtain a U where
[simp]: "stk!n = Addr a" "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 U: "class_type_of' (ty_of_htype U) = ⌊C'⌋" and "P ⊢ C' ≼⇧* D"
by(rule widen_is_class_type_of) simp
from ‹P ⊢ C' ≼⇧* D› wf M' obtain m' Ts' T' D'' where
C': "P ⊢ C' sees M': Ts'→T' = m' in D''" and
Ts': "P ⊢ Ts [≤] Ts'"
by (auto dest!: sees_method_mono)
from stk have "P,h ⊢ take n stk [:≤] take n ST" ..
hence "P,h ⊢ rev (take n stk) [:≤] rev (take n ST)" ..
also note Ts also note Ts'
finally have "P,h ⊢ rev (take n stk) [:≤] Ts'" .
hence ?thesis using Invoke Null n C' U
by (auto simp add: is_Ref_def2 has_methodI intro: sees_wf_native[OF wf]) }
ultimately show ?thesis by blast
next
case Return with stk app Φ meth frames
show ?thesis by (fastforce simp add: has_methodI list_all2_Cons2)
next
case ThrowExc with stk app Φ meth frames show ?thesis
by(auto 4 3 simp add: xcpt_app_def conf_def list_all2_Cons2 intro!: is_RefI intro: widen_trans[OF _ widen_subcls])
next
case (BinOpInstr bop) with stk app Φ meth frames
show ?thesis by(auto simp add: conf_def list_all2_Cons2)(force dest: WTrt_binop_widen_mono)
qed (auto simp add: list_all2_lengthD list_all2_Cons2)
thus "check P σ" using meth pc mxs by (simp add: check_def has_methodI)
next
case (Some a)
with confxcp obtain D where "typeof_addr h a = ⌊Class_type D⌋"
by(auto simp add: check_xcpt_def)
moreover from stk have "length stk = length ST" by(rule list_all2_lengthD)
ultimately show ?thesis using meth pc mxs Some confxcp app
using match_is_relevant[of P D ins pc pc xt]
by(auto simp add: check_def has_methodI check_xcpt_def xcpt_app_def dest: bspec)
qed
qed
thus "exec_d P t σ ≠ TypeError" ..
qed
lemma welltyped_commute:
"⟦wf_jvm_prog⇘Φ⇙ P; Φ ⊢ t:σ √⟧ ⟹ P,t ⊢ Normal σ -ta-jvmd→ Normal σ' = P,t ⊢ σ -ta-jvm→ σ'"
apply(rule iffI)
apply(erule exec_1_d.cases, simp, fastforce simp add: exec_d_def exec_1_iff split: if_split_asm)
by(auto dest!: no_type_error intro!: exec_1_d.intros simp add: exec_d_def exec_1_iff split: if_split_asm)
end
lemma (in JVM_conf_read) BV_correct_d_1:
"⟦ wf_jvm_prog⇘Φ⇙ P; P,t ⊢ Normal σ -ta-jvmd→ Normal σ'; Φ ⊢ t:σ √ ⟧ ⟹ Φ ⊢ t:σ' √"
unfolding welltyped_commute
by(rule BV_correct_1)
lemma not_TypeError_eq [iff]:
"x ≠ TypeError = (∃t. x = Normal t)"
by (cases x) auto
end