Up to index of Isabelle/HOL/jsr
theory BVNoTypeError = JVMDefensive + BVSpecTypeSafe:(* Title: HOL/MicroJava/BV/BVNoTypeErrors.thy
ID: $Id: BVNoTypeError.html,v 1.1 2002/11/28 14:17:20 kleing Exp $
Author: Gerwin Klein
Copyright GPL
*)
header {* \isaheader{Welltyped Programs produce no Type Errors} *}
theory BVNoTypeError = JVMDefensive + BVSpecTypeSafe:
text {*
Some simple lemmas about the type testing functions of the
defensive JVM:
*}
lemma typeof_NoneD [simp,dest]:
"typeof (\<lambda>v. None) v = Some x \<Longrightarrow> ¬isAddr v"
by (cases v) auto
lemma isRef_def2:
"isRef v = (v = Null \<or> (\<exists>loc. v = Addr loc))"
by (cases v) (auto simp add: isRef_def)
lemma isRef [simp]:
"G,hp,ihp \<turnstile> v ::\<preceq>i Init (RefT T) \<Longrightarrow> isRef v"
by (cases v) (auto simp add: iconf_def conf_def isRef_def)
lemma isIntg [simp]:
"G,hp,ihp \<turnstile> v ::\<preceq>i Init (PrimT Integer) \<Longrightarrow> isIntg v"
by (cases v) (auto simp add: iconf_def conf_def)
declare approx_loc_len [simp] approx_stk_len [simp]
(* fixme: move to List.thy *)
lemma list_all2I:
"\<forall>(x,y) \<in> set (zip a b). P x y \<Longrightarrow> length a = length b \<Longrightarrow> list_all2 P a b"
by (simp add: list_all2_def)
lemma app'Store[simp]:
"app' (Store idx, G, C', pc, maxs, rT, (ST,LT)) = (\<exists>T ST'. ST = T#ST' \<and> idx < length LT)"
by (cases ST, auto)
lemma app'GetField[simp]:
"app' (Getfield F C, G, C', pc, maxs, rT, (ST,LT)) =
(\<exists>oT vT ST'. ST = oT#ST' \<and> is_class G C \<and>
field (G,C) F = Some (C,vT) \<and> G \<turnstile> oT \<preceq>i (Init (Class C)))"
by (cases ST, auto)
lemma app'PutField[simp]:
"app' (Putfield F C, G, C', pc, maxs, rT, (ST,LT)) =
(\<exists>vT vT' oT ST'. ST = vT#oT#ST' \<and> is_class G C \<and>
field (G,C) F = Some (C, vT') \<and>
G \<turnstile> oT \<preceq>i Init (Class C) \<and> G \<turnstile> vT \<preceq>i Init vT')"
apply rule
defer
apply clarsimp
apply (cases ST)
apply simp
apply (cases "tl ST")
apply auto
done
lemma app'Checkcast[simp]:
"app' (Checkcast C, G, C', pc, maxs, rT, (ST,LT)) =
(\<exists>rT ST'. ST = Init (RefT rT)#ST' \<and> is_class G C)"
apply rule
defer
apply clarsimp
apply (cases ST)
apply simp
apply (cases "hd ST")
defer
apply simp
apply simp
apply (case_tac ty)
apply auto
done
lemma app'Pop[simp]:
"app' (Pop, G, C', pc, maxs, rT, (ST,LT)) = (\<exists>T ST'. ST = T#ST')"
by (cases ST, auto)
lemma app'Dup[simp]:
"app' (Dup, G, C', pc, maxs, rT, (ST,LT)) =
(\<exists>T ST'. ST = T#ST' \<and> length ST < maxs)"
by (cases ST, auto)
lemma app'Dup_x1[simp]:
"app' (Dup_x1, G, C', pc, maxs, rT, (ST,LT)) =
(\<exists>T1 T2 ST'. ST = T1#T2#ST' \<and> length ST < maxs)"
by (cases ST, simp, cases "tl ST", auto)
lemma app'Dup_x2[simp]:
"app' (Dup_x2, G, C', pc, maxs, rT, (ST,LT)) =
(\<exists>T1 T2 T3 ST'. ST = T1#T2#T3#ST' \<and> length ST < maxs)"
by (cases ST, simp, cases "tl ST", simp, cases "tl (tl ST)", auto)
lemma app'Swap[simp]:
"app' (Swap, G, C', pc, maxs, rT, (ST,LT)) = (\<exists>T1 T2 ST'. ST = T1#T2#ST')"
by (cases ST, simp, cases "tl ST", auto)
lemma app'IAdd[simp]:
"app' (IAdd, G, C', pc, maxs, rT, (ST,LT)) =
(\<exists>ST'. ST = Init (PrimT Integer)#Init (PrimT Integer)#ST')"
by (cases ST, simp, cases "tl ST", auto)
lemma app'Ifcmpeq[simp]:
"app' (Ifcmpeq b, G, C', pc, maxs, rT, (ST,LT)) =
(\<exists>T1 T2 ST'. ST = Init T1#Init T2#ST' \<and> 0 \<le> b + int pc \<and>
((\<exists>p. T1 = PrimT p \<and> T1 = T2) \<or>
(\<exists>r r'. T1 = RefT r \<and> T2 = RefT r')))"
apply auto
apply (cases ST)
apply simp
apply (cases "tl ST")
apply (case_tac a)
apply auto
apply (case_tac a)
apply auto
apply (case_tac aa)
apply (case_tac ty)
apply auto
done
lemma app'Return[simp]:
"app' (Return, G, C', pc, maxs, rT, (ST,LT)) =
(\<exists>T ST'. ST = T#ST'\<and> G \<turnstile> T \<preceq>i Init rT)"
by (cases ST, auto)
lemma app'Throw[simp]:
"app' (Throw, G, C', pc, maxs, rT, (ST,LT)) =
(\<exists>ST' r. ST = Init (RefT r)#ST')"
apply (cases ST, simp)
apply (cases "hd ST")
apply auto
done
lemma app'Invoke[simp]:
"app' (Invoke C mn fpTs, G, C', pc, maxs, rT, ST, LT) =
(\<exists>apTs X ST' mD' rT' b' z.
ST = (rev apTs) @ X # ST' \<and> mn \<noteq> init \<and>
length apTs = length fpTs \<and> is_class G C \<and>
(\<forall>(aT,fT)\<in>set(zip apTs fpTs). G \<turnstile> aT \<preceq>i Init fT) \<and>
method (G,C) (mn,fpTs) = Some (mD', rT', b') \<and> G \<turnstile> X \<preceq>i Init (Class C))"
(is "?app ST LT = ?P ST LT")
proof
assume "?P ST LT" thus "?app ST LT" by (auto simp add: min_def list_all2_def)
next
assume app: "?app ST LT"
hence l: "length fpTs < length ST" by simp
obtain xs ys where xs: "ST = xs @ ys" "length xs = length fpTs"
proof -
have "ST = take (length fpTs) ST @ drop (length fpTs) ST" by simp
moreover from l have "length (take (length fpTs) ST) = length fpTs"
by (simp add: min_def)
ultimately show ?thesis ..
qed
obtain apTs where
"ST = (rev apTs) @ ys" and "length apTs = length fpTs"
proof -
have "ST = rev (rev xs) @ ys" by simp
with xs show ?thesis by - (rule that, assumption, simp)
qed
moreover
from l xs obtain X ST' where "ys = X#ST'" by (auto simp add: neq_Nil_conv)
ultimately
have "ST = (rev apTs) @ X # ST'" "length apTs = length fpTs" by auto
with app
show "?P ST LT"
apply (clarsimp simp add: list_all2_def min_def)
apply ((rule exI)+, (rule conjI)?)+
apply auto
done
qed
lemma app'Invoke_special[simp]:
"app' (Invoke_special C mn fpTs, G, C', pc, maxs, rT, (ST,LT)) =
(\<exists>apTs X ST' rT' b' z.
ST = (rev apTs) @ X # ST' \<and> mn = init \<and>
length apTs = length fpTs \<and> is_class G C \<and>
(\<forall>(aT,fT)\<in>set(zip apTs fpTs). G \<turnstile> aT \<preceq>i (Init fT)) \<and>
method (G,C) (mn,fpTs) = Some (C, rT', b') \<and>
((\<exists>pc. X = UnInit C pc) \<or> (X = PartInit C' \<and> G \<turnstile> C' \<prec>C1 C)))"
(is "?app ST LT = ?P ST LT")
proof
assume "?P ST LT" thus "?app ST LT" by (auto simp add: min_def list_all2_def nth_append)
next
assume app: "?app ST LT"
hence l: "length fpTs < length ST" by simp
obtain xs ys where xs: "ST = xs @ ys" "length xs = length fpTs"
proof -
have "ST = take (length fpTs) ST @ drop (length fpTs) ST" by simp
moreover from l have "length (take (length fpTs) ST) = length fpTs"
by (simp add: min_def)
ultimately show ?thesis ..
qed
obtain apTs where
"ST = (rev apTs) @ ys" and "length apTs = length fpTs"
proof -
have "ST = rev (rev xs) @ ys" by simp
with xs show ?thesis by - (rule that, assumption, simp)
qed
moreover
from l xs obtain X ST' where "ys = X#ST'" by (auto simp add: neq_Nil_conv)
ultimately
have "ST = (rev apTs) @ X # ST'" "length apTs = length fpTs" by auto
with app
show "?P ST LT"
apply (clarsimp simp add: list_all2_def min_def nth_append)
apply ((rule exI)+, (rule conjI)?)+
apply auto
done
qed
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: "wt_jvm_prog G Phi" and conforms: "G,Phi \<turnstile>JVM s \<surd>"
shows "exec_d G (Normal s) \<noteq> TypeError"
proof -
from welltyped obtain mb where wf: "wf_prog mb G" by (fast dest: wt_jvm_progD)
obtain xcp hp ihp frs where s [simp]: "s = (xcp, hp, ihp, frs)" by (cases s)
from conforms have "xcp \<noteq> None \<or> frs = [] \<Longrightarrow> check G s"
by (unfold correct_state_def check_def) auto
moreover {
assume "¬(xcp \<noteq> None \<or> frs = [])"
then obtain stk loc C sig pc r frs' where
xcp [simp]: "xcp = None" and
frs [simp]: "frs = (stk,loc,C,sig,pc,r)#frs'"
by (clarsimp simp add: neq_Nil_conv) fast
from conforms obtain ST LT z rT maxs maxl ins et where
hconf: "G \<turnstile>h hp \<surd>" and
class: "is_class G C" and
meth: "method (G, C) sig = Some (C, rT, maxs, maxl, ins, et)" and
phi: "((ST,LT), z) \<in> Phi C sig ! pc" and
frame: "correct_frame G hp ihp (ST,LT) maxl ins (stk,loc,C,sig,pc,r)" and
frames: "correct_frames G hp ihp Phi rT sig z r frs'"
by simp (rule correct_stateE)
from frame obtain
stk: "approx_stk G hp ihp stk ST" and
loc: "approx_loc G hp ihp loc LT" and
init: "fst sig = init \<longrightarrow>
corresponds stk loc (ST, LT) ihp (fst r) (PartInit C) \<and>
(\<exists>l. fst r = Addr l \<and> hp l \<noteq> None \<and>
(ihp l = PartInit C \<or> (\<exists>C'. ihp l = Init (Class C'))))" and
pc: "pc < length ins" and
len: "length loc = length (snd sig) + maxl + 1"
by (rule correct_frameE)
note approx_val_def [simp]
from welltyped meth conforms
have "wt_instr (ins!pc) G C rT (Phi C sig) maxs (fst sig=init) (length ins) et pc"
by simp (rule wt_jvm_prog_impl_wt_instr_cor)
then obtain
app': "app (ins!pc) G C pc maxs (length ins) rT (fst sig=init) et (Phi C sig!pc) " and
eff: "\<forall>(pc', s')\<in>set (eff (ins ! pc) G pc et (Phi C sig ! pc)). pc' < length ins"
by (simp add: wt_instr_def phi) blast
from eff
have pc': "\<forall>pc' \<in> set (succs (ins!pc) pc (Phi C sig!pc)). pc' < length ins"
by (simp add: eff_def) blast
from app' phi
have app:
"xcpt_app (ins!pc) G pc et \<and>
app' (ins!pc, G, C, pc, maxs, rT, (ST,LT)) \<and>
(fst sig = init \<and> ins ! pc = Return \<longrightarrow> z) \<and> ((\<exists>C m p. ins ! pc = Invoke_special C m p \<and> ST!length p = PartInit C) \<longrightarrow> ¬ z)"
apply (clarsimp simp add: app_def)
apply (drule bspec, assumption)
apply clarsimp
done
with eff stk loc pc'
have "check_instr (ins!pc) G hp ihp stk loc C sig pc r frs'"
proof (cases "ins!pc")
case (Getfield F C)
with app stk loc phi obtain v vT stk' where
class: "is_class G C" and
field: "field (G, C) F = Some (C, vT)" and
stk: "stk = v # stk'" and
conf: "G,hp,ihp \<turnstile> v ::\<preceq>i Init (Class C)"
apply clarsimp
apply (blast dest: iconf_widen [OF _ _ wf])
done
from conf have isRef: "isRef v" by simp
moreover {
assume "v \<noteq> Null" with conf isRef have
"\<exists>D vs. hp (the_Addr v) = Some (D, vs) \<and>
is_init hp ihp v \<and> G \<turnstile> D \<preceq>C C"
by (fastsimp simp add: iconf_def conf_def isRef_def2)
}
ultimately show ?thesis using Getfield field class stk hconf
apply clarsimp
apply (fastsimp dest!: hconfD widen_cfs_fields [OF _ _ wf] oconf_objD)
done
next
case (Putfield F C)
with app stk loc phi obtain v ref vT stk' where
class: "is_class G C" and
field: "field (G, C) F = Some (C, vT)" and
stk: "stk = v # ref # stk'" and
confv: "G,hp,ihp \<turnstile> v ::\<preceq>i Init vT" and
confr: "G,hp,ihp \<turnstile> ref ::\<preceq>i Init (Class C)"
apply clarsimp
apply (blast dest: iconf_widen [OF _ _ wf])
done
from confr have isRef: "isRef ref" by simp
moreover
from confv have "is_init hp ihp v" by (simp add: iconf_def)
moreover {
assume "ref \<noteq> Null" with confr isRef have
"\<exists>D vs. hp (the_Addr ref) = Some (D, vs)
\<and> is_init hp ihp ref \<and> G \<turnstile> D \<preceq>C C"
by (fastsimp simp add: iconf_def conf_def isRef_def2)
}
ultimately show ?thesis using Putfield field class stk confv
by (clarsimp simp add: iconf_def)
next
case (Invoke C mn ps)
with stk app phi
show ?thesis
apply (clarsimp simp del: app'.simps)
apply (drule app'Invoke [THEN iffD1])
apply (clarsimp dest!: approx_stk_append_lemma simp add: nth_append)
apply (drule iconf_widen [OF _ _ wf], assumption)
apply (clarsimp simp add: iconf_def)
apply (drule non_npD, assumption)
apply clarsimp
apply (drule widen_methd [OF _ wf], assumption)
apply (clarsimp simp add: approx_stk_rev [symmetric])
apply (drule list_all2I, assumption)
apply (unfold approx_stk_def approx_loc_def)
apply (simp add: list_all2_approx)
apply (drule list_all2_iconf_widen [OF wf], assumption+)
done
next
case (Invoke_special C mn ps)
with stk app phi
show ?thesis
apply (clarsimp simp del: app'.simps)
apply (drule app'Invoke_special [THEN iffD1])
apply (clarsimp dest!: approx_stk_append_lemma simp add: nth_append)
apply (erule disjE)
apply (clarsimp simp add: iconf_def isRef_def)
apply (clarsimp simp add: approx_stk_rev [symmetric])
apply (drule list_all2I, assumption)
apply (simp add: list_all2_approx approx_stk_def approx_loc_def)
apply (drule list_all2_iconf_widen [OF wf], assumption+)
apply (clarsimp simp add: iconf_def isRef_def)
apply (clarsimp simp add: approx_stk_rev [symmetric])
apply (drule list_all2I, assumption)
apply (unfold approx_stk_def approx_loc_def)
apply (simp add: list_all2_approx)
apply (drule list_all2_iconf_widen [OF wf], assumption+)
done
next
case Return with stk app init phi meth frames
show ?thesis
apply clarsimp
apply (drule iconf_widen [OF _ _ wf], assumption)
apply (clarsimp simp add: iconf_def neq_Nil_conv
constructor_ok_def is_init_def isRef_def2)
done
next
case (Ret idx)
from welltyped meth conforms s frs
have finite: "finite (Phi C sig!pc)" by simp (rule phi_finite)
with Ret app obtain R where
idx: "idx < length LT" and
R: "LT!idx = OK (Init (RA R))"
by clarsimp
moreover
from R idx loc have "loc!idx = RetAddr R"
apply (simp add: approx_loc_def)
apply (clarsimp simp add: list_all2_conv_all_nth)
apply (erule allE, erule impE, assumption)
apply (clarsimp simp add: iconf_def conf_def)
apply (cases "loc!idx")
apply auto
done
moreover
from finite Ret pc' R
have "R < length ins"
apply (auto simp add: set_SOME_lists finite_imageI theRA_def)
apply (drule bspec, assumption)
apply simp
done
ultimately
show ?thesis using Ret loc by simp
qed auto
hence "check G s" by (simp add: check_def meth)
} ultimately
have "check G s" by blast
thus "exec_d G (Normal s) \<noteq> 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:
"wt_jvm_prog G Phi \<Longrightarrow> G,Phi \<turnstile>JVM s \<surd> \<Longrightarrow> G \<turnstile> s -jvm\<rightarrow> t
\<Longrightarrow> G \<turnstile> (Normal s) -jvmd\<rightarrow> (Normal t)"
apply (unfold exec_all_def)
apply (erule rtrancl_induct)
apply (simp add: exec_all_d_def)
apply simp
apply (fold exec_all_def)
apply (frule BV_correct, assumption+)
apply (drule no_type_error, assumption, drule no_type_error_commutes, simp)
apply (simp add: exec_all_d_def)
apply (rule rtrancl_trans, assumption)
apply blast
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 G ("\<Gamma>") and Phi ("\<Phi>")
assumes "wt_jvm_prog \<Gamma> \<Phi>" and "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>"
shows "\<Gamma> \<turnstile> (Normal s) -jvmd\<rightarrow> (Normal t) = \<Gamma> \<turnstile> s -jvm\<rightarrow> t"
by rule (erule defensive_imp_aggressive,rule welltyped_aggressive_imp_defensive)
corollary welltyped_initial_commutes:
fixes G ("\<Gamma>") and Phi ("\<Phi>")
assumes "wt_jvm_prog \<Gamma> \<Phi>"
assumes "is_class \<Gamma> C" "method (\<Gamma>,C) (m,[]) = Some (C, b)" "m \<noteq> init"
defines start: "s \<equiv> start_state \<Gamma> C m"
shows "\<Gamma> \<turnstile> (Normal s) -jvmd\<rightarrow> (Normal t) = \<Gamma> \<turnstile> s -jvm\<rightarrow> t"
proof -
have "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>" by (unfold start, rule BV_correct_initial)
thus ?thesis by - (rule welltyped_commutes)
qed
end
lemma typeof_NoneD:
typeof (%v. None) v = Some x ==> ¬ isAddr v
lemma isRef_def2:
isRef v = (v = Null | (EX loc. v = Addr loc))
lemma isRef:
G,hp,ihp \<turnstile> v ::\<preceq>i Init (RefT T) ==> isRef v
lemma isIntg:
G,hp,ihp \<turnstile> v ::\<preceq>i Init (PrimT Integer) ==> isIntg v
lemma list_all2I:
[| Ball (set (zip a b)) (split P); length a = length b |] ==> list_all2 P a b
lemma app'Store:
app' (Store idx, G, C', pc, maxs, rT, ST, LT) = (EX T ST'. ST = T # ST' & idx < length LT)
lemma app'GetField:
app' (Getfield F C, G, C', pc, maxs, rT, ST, LT) =
(EX oT vT ST'.
ST = oT # ST' &
is_class G C & field (G, C) F = Some (C, vT) & G |- oT <=i Init (Class C))
lemma app'PutField:
app' (Putfield F C, G, C', pc, maxs, rT, ST, LT) =
(EX vT vT' oT ST'.
ST = vT # oT # ST' &
is_class G C &
field (G, C) F = Some (C, vT') &
G |- oT <=i Init (Class C) & G |- vT <=i Init vT')
lemma app'Checkcast:
app' (Checkcast C, G, C', pc, maxs, rT, ST, LT) = (EX rT ST'. ST = Init (RefT rT) # ST' & is_class G C)
lemma app'Pop:
app' (Pop, G, C', pc, maxs, rT, ST, LT) = (EX T ST'. ST = T # ST')
lemma app'Dup:
app' (Dup, G, C', pc, maxs, rT, ST, LT) = (EX T ST'. ST = T # ST' & length ST < maxs)
lemma app'Dup_x1:
app' (Dup_x1, G, C', pc, maxs, rT, ST, LT) = (EX T1 T2 ST'. ST = T1 # T2 # ST' & length ST < maxs)
lemma app'Dup_x2:
app' (Dup_x2, G, C', pc, maxs, rT, ST, LT) = (EX T1 T2 T3 ST'. ST = T1 # T2 # T3 # ST' & length ST < maxs)
lemma app'Swap:
app' (Swap, G, C', pc, maxs, rT, ST, LT) = (EX T1 T2 ST'. ST = T1 # T2 # ST')
lemma app'IAdd:
app' (IAdd, G, C', pc, maxs, rT, ST, LT) = (EX ST'. ST = Init (PrimT Integer) # Init (PrimT Integer) # ST')
lemma app'Ifcmpeq:
app' (Ifcmpeq b, G, C', pc, maxs, rT, ST, LT) =
(EX T1 T2 ST'.
ST = Init T1 # Init T2 # ST' &
0 <= b + int pc &
((EX p. T1 = PrimT p & T1 = T2) | (EX r r'. T1 = RefT r & T2 = RefT r')))
lemma app'Return:
app' (Return, G, C', pc, maxs, rT, ST, LT) = (EX T ST'. ST = T # ST' & G |- T <=i Init rT)
lemma app'Throw:
app' (Throw, G, C', pc, maxs, rT, ST, LT) = (EX ST' r. ST = Init (RefT r) # ST')
lemma app'Invoke:
app' (Invoke C mn fpTs, G, C', pc, maxs, rT, ST, LT) =
(EX apTs X ST' mD' rT' b' z.
ST = rev apTs @ X # ST' &
mn ~= init &
length apTs = length fpTs &
is_class G C &
(ALL (aT, fT):set (zip apTs fpTs). G |- aT <=i Init fT) &
method (G, C) (mn, fpTs) = Some (mD', rT', b') & G |- X <=i Init (Class C))
lemma app'Invoke_special:
app' (Invoke_special C mn fpTs, G, C', pc, maxs, rT, ST, LT) =
(EX apTs X ST' rT' b' z.
ST = rev apTs @ X # ST' &
mn = init &
length apTs = length fpTs &
is_class G C &
(ALL (aT, fT):set (zip apTs fpTs). G |- aT <=i Init fT) &
method (G, C) (mn, fpTs) = Some (C, rT', b') &
((EX pc. X = UnInit C pc) | X = PartInit C' & G |- C' <=C1 C))
theorem
[| wt_jvm_prog G Phi; G,Phi |-JVM s [ok] |] ==> exec_d G (Normal s) ~= TypeError
theorem welltyped_aggressive_imp_defensive:
[| wt_jvm_prog G Phi; G,Phi |-JVM s [ok]; G |- s -jvm-> t |] ==> G |- Normal s -jvmd-> Normal t
corollary
[| wt_jvm_prog G Phi; G,Phi |-JVM s [ok] |] ==> G |- Normal s -jvmd-> Normal t = G |- s -jvm-> t
corollary
[| wt_jvm_prog G Phi; is_class G C; method (G, C) (m, []) = Some (C, b);
m ~= init |]
==> G |- Normal (start_state G C m) -jvmd-> Normal t =
G |- start_state G C m -jvm-> t