Theory BVNoTypeError
section ‹ Welltyped Programs produce no Type Errors ›
theory BVNoTypeError
imports "../JVM/JVMDefensive" BVSpecTypeSafe
begin
lemma has_methodI:
"P ⊢ C sees M,b:Ts→T = m in D ⟹ P ⊢ C has M,b"
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"
proof(cases T)
qed (auto simp add: is_refT_def is_Ref_def dest: conf_ClassD)
lemma is_IntgI [intro, simp]: "P,h ⊢ v :≤ Integer ⟹ is_Intg v"
by (unfold conf_def) auto
lemma is_BoolI [intro, simp]: "P,h ⊢ v :≤ Boolean ⟹ is_Bool v"
by (unfold conf_def) auto
declare defs1 [simp del]
lemma wt_jvm_prog_states_NonStatic:
assumes wf: "wf_jvm_prog⇘Φ⇙ P"
and mC: "P ⊢ C sees M,NonStatic: Ts→T = (mxs, mxl, ins, et) in C"
and Φ: "Φ C M ! pc = τ" and pc: "pc < size ins"
shows "OK τ ∈ states P mxs (1+size Ts+mxl)"
proof -
let ?wf_md = "(λP C (M, b, Ts, T⇩r, mxs, mxl⇩0, is, xt).
wt_method P C b Ts T⇩r mxs mxl⇩0 is xt (Φ C M))"
have wfmd: "wf_prog ?wf_md P" using wf
by (unfold wf_jvm_prog_phi_def) assumption
show ?thesis using sees_wf_mdecl[OF wfmd mC] Φ pc
by (simp add: wf_mdecl_def wt_method_def check_types_def)
(blast intro: nth_in)
qed
lemma wt_jvm_prog_states_Static:
assumes wf: "wf_jvm_prog⇘Φ⇙ P"
and mC: "P ⊢ C sees M,Static: Ts→T = (mxs, mxl, ins, et) in C"
and Φ: "Φ C M ! pc = τ" and pc: "pc < size ins"
shows "OK τ ∈ states P mxs (size Ts+mxl)"
proof -
let ?wf_md = "(λP C (M, b, Ts, T⇩r, mxs, mxl⇩0, is, xt).
wt_method P C b Ts T⇩r mxs mxl⇩0 is xt (Φ C M))"
have wfmd: "wf_prog ?wf_md P" using wf
by (unfold wf_jvm_prog_phi_def) assumption
show ?thesis using sees_wf_mdecl[OF wfmd mC] Φ pc
by (simp add: wf_mdecl_def wt_method_def check_types_def)
(blast intro: nth_in)
qed
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 sh where s [simp]: "σ = (xcp, h, frs, sh)" 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 ics frs' where
xcp [simp]: "xcp = None" and
frs [simp]: "frs = (stk,reg,C,M,pc,ics)#frs'"
by (clarsimp simp add: neq_Nil_conv)
from conforms obtain ST LT b Ts T mxs mxl ins xt where
hconf: "P ⊢ h √" and
shconf: "P,h ⊢⇩s sh √" and
meth: "P ⊢ C sees M,b:Ts→T = (mxs, mxl, ins, xt) in C" and
Φ: "Φ C M ! pc = Some (ST,LT)" and
frame: "conf_f P h sh (ST,LT) ins (stk,reg,C,M,pc,ics)" and
frames: "conf_fs P h sh Φ C 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)
∨ OK (Some (ST, LT)) ∈ states P mxs (size Ts+mxl)"
by (cases b, auto dest: wt_jvm_prog_states_NonStatic wt_jvm_prog_states_Static)
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' sh"
proof (cases "ins!pc")
case (Getfield F C)
with app stk reg Φ obtain v vT stk' where
field: "P ⊢ C sees F,NonStatic: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
has_field_mono[OF has_visible_field[OF field]] hconfD[OF hconf]
by (unfold oconf_def has_field_def) (fastforce dest: has_fields_fun)
next
case (Getstatic C F D)
with app stk reg Φ obtain vT where
field: "P ⊢ C sees F,Static:vT in D"
by auto
then show ?thesis using Getstatic stk
has_field_idemp[OF has_visible_field[OF field]] shconfD[OF shconf]
by (unfold soconf_def has_field_def) (fastforce dest: has_fields_fun)
next
case (Putfield F C)
with app stk reg Φ obtain v ref vT stk' where
field: "P ⊢ C sees F,NonStatic: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',NonStatic: 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',NonStatic: 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 (Invokestatic C M' n)
with app have n: "n ≤ size ST" by simp
from stk have [simp]: "size stk = size ST" by (rule list_all2_lengthD)
from app Invokestatic
obtain D Ts T m where
M': "P ⊢ C sees M',Static: Ts→T = m in D" and
Ts: "P ⊢ rev (take n ST) [≤] Ts"
by auto
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
finally have "P,h ⊢ rev (take n stk) [:≤] Ts" .
with Invokestatic n M'
show ?thesis by (auto simp add: is_Ref_def2 has_methodI)
next
case Return
show ?thesis
proof(cases "M = clinit")
case True
have "is_class P C" by(rule sees_method_is_class[OF meth])
with wf_sees_clinit[OF wf]
obtain m where "P ⊢ C sees clinit,Static: [] → Void = m in C"
by(fastforce simp: is_class_def)
with stk app Φ meth frames True Return
show ?thesis by (auto simp add: has_methodI)
next
case False with stk app Φ meth frames Return
show ?thesis by (auto intro: has_methodI)
qed
qed (auto simp add: list_all2_lengthD)
hence "check P σ" using meth pc mxs by (auto simp: check_def intro: 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 σ')"
proof -
assume wf: "wf_jvm_prog⇘Φ⇙ P" and cf: "P,Φ ⊢ σ √" and exec: "P ⊢ σ -jvm→ σ'"
then have "(σ, σ') ∈ {(σ, σ'). exec (P, σ) = ⌊σ'⌋}⇧*" by(simp only: exec_all_def)
then show ?thesis proof(induct rule: rtrancl_induct)
case base
then show ?case by (simp add: exec_all_d_def1)
next
case (step y z)
then have σy: "P ⊢ σ -jvm→ y" by (simp only: exec_all_def [symmetric])
have exec_d: "exec_d P y = Normal ⌊z⌋" using step
no_type_error_commutes[OF no_type_error[OF wf BV_correct[OF wf σy cf]]]
by (simp add: exec_all_d_def1)
show ?case using step.hyps(3) exec_1_d_NormalI[OF exec_d]
by (simp add: exec_all_d_def1)
qed
qed
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→ σ'"
proof(rule iffI)
assume "P ⊢ Normal σ -jvmd→ Normal σ'" then show "P ⊢ σ -jvm→ σ'"
by (rule defensive_imp_aggressive)
next
assume "P ⊢ σ -jvm→ σ'" then show "P ⊢ Normal σ -jvmd→ Normal σ'"
by (rule welltyped_aggressive_imp_defensive [OF wf conforms])
qed
corollary welltyped_initial_commutes:
assumes wf: "wf_jvm_prog P"
assumes nstart: "¬ is_class P Start"
assumes meth: "P ⊢ C sees M,Static:[]→Void = b in C"
assumes nclinit: "M ≠ clinit"
assumes Obj_start_m:
"(⋀b' Ts' T' m' D'. P ⊢ Object sees start_m, b' : Ts'→T' = m' in D'
⟹ b' = Static ∧ Ts' = [] ∧ T' = Void)"
defines start: "σ ≡ start_state P"
shows "start_prog P C M ⊢ (Normal σ) -jvmd→ (Normal σ') = start_prog P C M ⊢ σ -jvm→ σ'"
proof -
from wf obtain Φ where wf': "wf_jvm_prog⇘Φ⇙ P" by (auto simp: wf_jvm_prog_def)
let ?Φ = "Φ_start Φ"
from start_prog_wf_jvm_prog_phi[where Φ'="?Φ", OF wf' nstart meth nclinit Φ_start Obj_start_m]
have "wf_jvm_prog⇘?Φ⇙(start_prog P C M)" by simp
moreover
from wf' nstart meth nclinit Φ_start(2) have "start_prog P C M,?Φ ⊢ σ √"
unfolding start by (rule BV_correct_initial)
ultimately 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"
proof -
assume "P ⊢ (Normal σ) -jvmd→ σ'"
then have "(Normal σ, σ') ∈ (exec_1_d P)⇧*" by (unfold exec_all_d_def1) simp
then show ?thesis proof(induct rule: rtrancl_induct)
case (step y z)
then obtain y⇩n where [simp]: "y = Normal y⇩n" by clarsimp
have nσy: "P ⊢ Normal σ -jvmd→ Normal y⇩n" using step.hyps(1)
by (fold exec_all_d_def1) simp
have σy: "P ⊢ σ -jvm→ y⇩n" using defensive_imp_aggressive[OF nσy] by simp
show ?case using step no_type_error[OF wf BV_correct[OF wf σy cnf]]
by (auto simp add: exec_1_d_eq)
qed simp
qed
locale start =
fixes P and C and M and σ and T and b and P⇩0
assumes wf: "wf_jvm_prog P"
assumes nstart: "¬ is_class P Start"
assumes sees: "P ⊢ C sees M,Static:[]→Void = b in C"
assumes nclinit: "M ≠ clinit"
assumes Obj_start_m: "(⋀b' Ts' T' m' D'. P ⊢ Object sees start_m, b' : Ts'→T' = m' in D'
⟹ b' = Static ∧ Ts' = [] ∧ T' = Void)"
defines "σ ≡ Normal (start_state P)"
defines [simp]: "P⇩0 ≡ start_prog P C M"
corollary (in start) bv_no_type_error:
shows "P⇩0 ⊢ σ -jvmd→ σ' ⟹ σ' ≠ TypeError"
proof -
from wf obtain Φ where wf': "wf_jvm_prog⇘Φ⇙ P" by (auto simp: wf_jvm_prog_def)
let ?Φ = "Φ_start Φ"
from start_prog_wf_jvm_prog_phi[where Φ'="?Φ", OF wf' nstart sees nclinit Φ_start Obj_start_m]
have "wf_jvm_prog⇘?Φ⇙P⇩0" by simp
moreover
from BV_correct_initial[where Φ'="?Φ", OF wf' nstart sees nclinit Φ_start(2)]
have "correct_state P⇩0 ?Φ (start_state P)" by simp
ultimately have "cnf P⇩0 ?Φ (start_state P)" by (rule cnf.intro)
moreover assume "P⇩0 ⊢ σ -jvmd→ σ'"
ultimately show ?thesis by (unfold σ_def) (rule cnf.no_type_errors)
qed
end