Theory BVNoTypeError
section ‹Welltyped Programs produce no Type Errors›
theory BVNoTypeError
imports "../JVM/JVMDefensive" BVSpecTypeSafe
begin
lemma has_methodI:
"P ⊢ C sees M:Ts→T = m in D ⟹ P ⊢ C has M"
by (unfold has_method_def) blast
text ‹
Some simple lemmas about the type testing functions of the
defensive JVM:
›
lemma typeof_NoneD [simp,dest]: "typeof v = Some x ⟹ ¬is_Addr v"
by (cases v) auto
lemma is_Ref_def2:
"is_Ref v = (v = Null ∨ (∃a. v = Addr a))"
by (cases v) (auto simp add: is_Ref_def)
lemma [iff]: "is_Ref Null" by (simp add: is_Ref_def2)
lemma is_RefI [intro, simp]: "P,h ⊢ v :≤ T ⟹ is_refT T ⟹ is_Ref v"
apply (cases T)
apply (auto simp add: is_refT_def is_Ref_def dest: conf_ClassD)
done
lemma is_IntgI [intro, simp]: "P,h ⊢ v :≤ Integer ⟹ is_Intg v"
apply (unfold conf_def)
apply auto
done
lemma is_BoolI [intro, simp]: "P,h ⊢ v :≤ Boolean ⟹ is_Bool v"
apply (unfold conf_def)
apply auto
done
declare defs1 [simp del]
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
text ‹
The main theorem: welltyped programs do not produce type errors if they
are started in a conformant state.
›
theorem no_type_error:
fixes σ :: jvm_state
assumes welltyped: "wf_jvm_prog⇘Φ⇙ P" and conforms: "P,Φ ⊢ σ √"
shows "exec_d P σ ≠ 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 σ)
from conforms have "xcp ≠ None ∨ frs = [] ⟹ check P σ"
by (unfold correct_state_def check_def) auto
moreover {
assume "¬(xcp ≠ None ∨ frs = [])"
then obtain stk reg C M pc frs' where
xcp [simp]: "xcp = None" and
frs [simp]: "frs = (stk,reg,C,M,pc)#frs'"
by (clarsimp simp add: neq_Nil_conv)
from conforms obtain ST LT Ts T mxs mxl ins xt where
hconf: "P ⊢ h √" 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'"
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)
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)
with eff stk reg
have "check_instr (ins!pc) P h stk reg C M pc frs'"
proof (cases "ins!pc")
case (Getfield F C)
with app stk reg Φ obtain v vT stk' where
field: "P ⊢ C sees F:vT in C" and
stk: "stk = v # stk'" and
conf: "P,h ⊢ v :≤ Class C"
by auto
from conf have is_Ref: "is_Ref v" by auto
moreover {
assume "v ≠ Null"
with conf field is_Ref wf
have "∃D vs. h (the_Addr v) = Some (D,vs) ∧ P ⊢ D ≼⇧* C"
by (auto dest!: non_npD)
}
ultimately show ?thesis using Getfield field stk hconf
apply clarsimp
apply (rule conjI, fastforce)
apply clarsimp
apply (drule has_visible_field)
apply (drule (1) has_field_mono)
apply (drule (1) hconfD)
apply (unfold oconf_def has_field_def)
apply clarsimp
apply (fastforce dest: has_fields_fun)
done
next
case (Putfield F C)
with app stk reg Φ obtain v ref vT stk' where
field: "P ⊢ C sees F:vT in C" and
stk: "stk = v # ref # stk'" and
confv: "P,h ⊢ v :≤ vT" and
confr: "P,h ⊢ ref :≤ Class C"
by fastforce
from confr have is_Ref: "is_Ref ref" by simp
moreover {
assume "ref ≠ Null"
with confr field is_Ref wf
have "∃D vs. h (the_Addr ref) = Some (D,vs) ∧ P ⊢ D ≼⇧* C"
by (auto dest: non_npD)
}
ultimately show ?thesis using Putfield field stk confv by fastforce
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: "ST!n = Class D" and
M': "P ⊢ D sees M': Ts→T = m in D'" and
Ts: "P ⊢ rev (take n ST) [≤] Ts"
by auto
from D stk n have "P,h ⊢ stk!n :≤ Class D"
by (auto simp: list_all2_conv_all_nth)
with Null obtain a C' fs where
[simp]: "stk!n = Addr a" "h a = Some (C',fs)" and
"P ⊢ C' ≼⇧* D"
by (fastforce dest!: conf_ClassD)
with M' wf 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'" .
with Invoke Null n C'
have ?thesis by (auto simp add: is_Ref_def2 has_methodI)
}
ultimately show ?thesis by blast
next
case Return with stk app Φ meth frames
show ?thesis by (auto simp add: has_methodI)
qed (auto simp add: list_all2_lengthD)
hence "check P σ" using meth pc mxs by (simp add: check_def has_methodI)
} ultimately
have "check P σ" by blast
thus "exec_d P σ ≠ TypeError" ..
qed
text ‹
The theorem above tells us that, in welltyped programs, the
defensive machine reaches the same result as the aggressive
one (after arbitrarily many steps).
›
theorem welltyped_aggressive_imp_defensive:
"wf_jvm_prog⇘Φ⇙ P ⟹ P,Φ ⊢ σ √ ⟹ P ⊢ σ -jvm→ σ'
⟹ P ⊢ (Normal σ) -jvmd→ (Normal σ')"
apply (simp only: exec_all_def)
apply (erule rtrancl_induct)
apply (simp add: exec_all_d_def1)
apply simp
apply (simp only: exec_all_def [symmetric])
apply (frule BV_correct, assumption+)
apply (drule no_type_error, assumption, drule no_type_error_commutes, simp)
apply (simp add: exec_all_d_def1)
apply (rule rtrancl_trans, assumption)
apply (drule exec_1_d_NormalI)
apply auto
done
text ‹
As corollary we get that the aggressive and the defensive machine
are equivalent for welltyped programs (if started in a conformant
state or in the canonical start state)
›
corollary welltyped_commutes:
fixes σ :: jvm_state
assumes wf: "wf_jvm_prog⇘Φ⇙ P" and conforms: "P,Φ ⊢ σ √"
shows "P ⊢ (Normal σ) -jvmd→ (Normal σ') = P ⊢ σ -jvm→ σ'"
apply rule
apply (erule defensive_imp_aggressive)
apply (erule welltyped_aggressive_imp_defensive [OF wf conforms])
done
corollary welltyped_initial_commutes:
assumes wf: "wf_jvm_prog P"
assumes meth: "P ⊢ C sees M:[]→T = b in C"
defines start: "σ ≡ start_state P C M"
shows "P ⊢ (Normal σ) -jvmd→ (Normal σ') = P ⊢ σ -jvm→ σ'"
proof -
from wf obtain Φ where wf': "wf_jvm_prog⇘Φ⇙ P" by (auto simp: wf_jvm_prog_def)
from this meth have "P,Φ ⊢ σ √" unfolding start by (rule BV_correct_initial)
with wf' show ?thesis by (rule welltyped_commutes)
qed
lemma not_TypeError_eq [iff]:
"x ≠ TypeError = (∃t. x = Normal t)"
by (cases x) auto
locale cnf =
fixes P and Φ and σ
assumes wf: "wf_jvm_prog⇘Φ⇙ P"
assumes cnf: "correct_state P Φ σ"
theorem (in cnf) no_type_errors:
"P ⊢ (Normal σ) -jvmd→ σ' ⟹ σ' ≠ TypeError"
apply (unfold exec_all_d_def1)
apply (erule rtrancl_induct)
apply simp
apply (fold exec_all_d_def1)
apply (insert cnf wf)
apply clarsimp
apply (drule defensive_imp_aggressive)
apply (frule (2) BV_correct)
apply (drule (1) no_type_error) back
apply (auto simp add: exec_1_d_eq)
done
locale start =
fixes P and C and M and σ and T and b
assumes wf: "wf_jvm_prog P"
assumes sees: "P ⊢ C sees M:[]→T = b in C"
defines "σ ≡ Normal (start_state P C M)"
corollary (in start) bv_no_type_error:
shows "P ⊢ σ -jvmd→ σ' ⟹ σ' ≠ TypeError"
proof -
from wf obtain Φ where "wf_jvm_prog⇘Φ⇙ P" by (auto simp: wf_jvm_prog_def)
moreover
with sees have "correct_state P Φ (start_state P C M)"
by - (rule BV_correct_initial)
ultimately have "cnf P Φ (start_state P C M)" by (rule cnf.intro)
moreover assume "P ⊢ σ -jvmd→ σ'"
ultimately show ?thesis by (unfold σ_def) (rule cnf.no_type_errors)
qed
end