Up to index of Isabelle/HOL/arrays
theory JVMDefensive = JVMExec:(* Title: HOL/MicroJava/JVM/JVMDefensive.thy
ID: $Id: JVMDefensive.html,v 1.1 2002/11/28 16:11:18 kleing Exp $
Author: Gerwin Klein
Copyright GPL
*)
header {* \isaheader{A Defensive JVM} *}
theory JVMDefensive = JVMExec:
text {*
Extend the state space by one element indicating a type error (or
other abnormal termination) *}
datatype 'a type_error = TypeError | Normal 'a
syntax "fifth" :: "'a × 'b × 'c × 'd × 'e × 'f \<Rightarrow> 'e"
translations
"fifth x" == "fst(snd(snd(snd(snd x))))"
consts isAddr :: "val \<Rightarrow> bool"
recdef isAddr "{}"
"isAddr (Addr loc) = True"
"isAddr v = False"
consts isIntg :: "val \<Rightarrow> bool"
recdef isIntg "{}"
"isIntg (Intg i) = True"
"isIntg v = False"
consts isRetAddr :: "val \<Rightarrow> bool"
recdef isRetAddr "{}"
"isRetAddr (RetAddr pc) = True"
"isRetAddr v = False"
constdefs
isRef :: "val \<Rightarrow> bool"
"isRef v \<equiv> v = Null \<or> isAddr v"
consts
is_obj :: "heap_entry option \<Rightarrow> bool"
recdef is_obj "{}"
"is_obj (Some (Obj C fs)) = True"
"is_obj x = False"
consts
is_arr :: "heap_entry option \<Rightarrow> bool"
recdef is_arr "{}"
"is_arr (Some (Arr T l en)) = True"
"is_arr x = False"
consts
check_instr :: "[instr, jvm_prog, aheap, init_heap, opstack, locvars,
cname, sig, p_count, ref_upd, frame list] \<Rightarrow> bool"
primrec
"check_instr (Load idx) G hp ihp stk regs C sig pc z frs =
(idx < length regs)"
"check_instr (Store idx) G hp ihp stk regs Cl sig pc z frs =
(0 < length stk \<and> idx < length regs)"
"check_instr (LitPush v) G hp ihp stk regs Cl sig pc z frs =
(¬isAddr v)"
"check_instr (New C) G hp ihp stk regs Cl sig pc z frs =
is_class G C"
"check_instr (Getfield F C) G hp ihp stk regs Cl sig pc z frs =
(0 < length stk \<and> is_class G C \<and> field (G,C) F \<noteq> None \<and>
(let (C', T) = the (field (G,C) F); ref = hd stk in
C' = C \<and> isRef ref \<and> (ref \<noteq> Null \<longrightarrow>
is_obj (hp (the_Addr ref)) \<and> is_init hp ihp ref \<and>
(let (D,vs) = the_obj (the (hp (the_Addr ref))) in
G \<turnstile> D \<preceq>C C \<and> vs (F,C) \<noteq> None \<and> G,hp \<turnstile> the (vs (F,C)) ::\<preceq> T))))"
"check_instr (Putfield F C) G hp ihp stk regs Cl sig pc z frs =
(1 < length stk \<and> is_class G C \<and> field (G,C) F \<noteq> None \<and>
(let (C', T) = the (field (G,C) F); v = hd stk; ref = hd (tl stk) in
C' = C \<and> is_init hp ihp v \<and> isRef ref \<and> (ref \<noteq> Null \<longrightarrow>
is_obj (hp (the_Addr ref)) \<and> is_init hp ihp ref \<and>
(let (D,vs) = the_obj (the (hp (the_Addr ref))) in
G \<turnstile> D \<preceq>C C \<and> G,hp \<turnstile> v ::\<preceq> T))))"
"check_instr (Checkcast C) G hp ihp stk regs Cl sig pc z frs =
(0 < length stk \<and> is_class G C \<and> isRef (hd stk) \<and> is_init hp ihp (hd stk))"
"check_instr (Invoke C mn ps) G hp ihp stk regs Cl sig pc z frs =
(length ps < length stk \<and> mn \<noteq> init \<and>
(let n = length ps; v = stk!n in
isRef v \<and> (v \<noteq> Null \<longrightarrow>
hp (the_Addr v) \<noteq> None \<and> is_init hp ihp v \<and>
method (G,cname_of hp v) (mn,ps) \<noteq> None \<and>
list_all2 (\<lambda>v T. G,hp \<turnstile> v ::\<preceq> T \<and> is_init hp ihp v) (rev (take n stk)) ps)))"
"check_instr (Invoke_special C mn ps) G hp ihp stk regs Cl sig pc z frs =
(length ps < length stk \<and> mn = init \<and>
(let n = length ps; ref = stk!n in
isRef ref \<and> (ref \<noteq> Null \<longrightarrow>
hp (the_Addr ref) \<noteq> None \<and>
method (G,C) (mn,ps) \<noteq> None \<and>
fst (the (method (G,C) (mn,ps))) = C \<and>
list_all2 (\<lambda>v T. G,hp \<turnstile> v ::\<preceq> T \<and> is_init hp ihp v) (rev (take n stk)) ps) \<and>
(case ihp (the_Addr ref) of
Init T \<Rightarrow> False
| UnInit C' pc' \<Rightarrow> C' = C
| PartInit C' \<Rightarrow> C' = Cl \<and> G \<turnstile> C' \<prec>C1 C)
))"
"check_instr Return G hp ihp stk0 regs Cl sig0 pc z0 frs =
(0 < length stk0 \<and> (0 < length frs \<longrightarrow>
method (G,Cl) sig0 \<noteq> None \<and>
(let v = hd stk0; (C, rT, body) = the (method (G,Cl) sig0) in
Cl = C \<and> G,hp \<turnstile> v ::\<preceq> rT \<and> is_init hp ihp v) \<and>
(fst sig0 = init \<longrightarrow>
snd z0 \<noteq> Null \<and> isRef (snd z0) \<and> is_init hp ihp (snd z0))))"
"check_instr Pop G hp ihp stk regs Cl sig pc z frs =
(0 < length stk)"
"check_instr Dup G hp ihp stk regs Cl sig pc z frs =
(0 < length stk)"
"check_instr Dup_x1 G hp ihp stk regs Cl sig pc z frs =
(1 < length stk)"
"check_instr Dup_x2 G hp ihp stk regs Cl sig pc z frs =
(2 < length stk)"
"check_instr Swap G hp ihp stk regs Cl sig pc z frs =
(1 < length stk)"
"check_instr IAdd G hp ihp stk regs Cl sig pc z frs =
(1 < length stk \<and> isIntg (hd stk) \<and> isIntg (hd (tl stk)))"
"check_instr (Ifcmpeq b) G hp ihp stk regs Cl sig pc z frs =
(1 < length stk \<and> 0 \<le> int pc+b)"
"check_instr (Goto b) G hp ihp stk regs Cl sig pc z frs =
(0 \<le> int pc+b)"
"check_instr Throw G hp ihp stk regs Cl sig pc z frs =
(0 < length stk \<and> isRef (hd stk))"
"check_instr (Jsr b) G hp ihp stk regs Cl sig pc z frs =
(0 \<le> int pc+b)"
"check_instr (Ret idx) G hp ihp stk regs Cl sig pc z frs =
(idx < length regs \<and> isRetAddr (regs!idx))"
"check_instr (ArrLoad) G hp ihp stk regs Cl sig pc z frs =
(1 < length stk \<and>
(let idx = hd stk; ref = hd (tl stk) in isIntg idx \<and> isRef ref \<and>
ref \<noteq> Null \<longrightarrow> is_arr (hp (the_Addr ref))))"
"check_instr (ArrStore) G hp ihp stk regs Cl sig pc z frs =
(2 < length stk \<and>
(let idx = hd (tl stk); ref = hd (tl (tl stk)) in isIntg idx \<and> isRef ref \<and>
ref \<noteq> Null \<longrightarrow> is_arr (hp (the_Addr ref))))"
"check_instr (ArrLength) G hp ihp stk regs Cl sig pc z frs =
(0 < length stk \<and>
(let ref = hd stk in isRef ref \<and>
ref \<noteq> Null \<longrightarrow> is_arr (hp (the_Addr ref))))"
"check_instr (ArrNew T) G hp ihp stk regs Cl sig pc z frs =
(0 < length stk \<and> isIntg (hd stk) \<and> is_type G T)"
constdefs
check :: "jvm_prog \<Rightarrow> jvm_state \<Rightarrow> bool"
"check G s \<equiv> let (xcpt, hp, ihp, frs) = s in
(case frs of [] \<Rightarrow> True | (stk,loc,C,sig,pc,z)#frs' \<Rightarrow>
(let ins = fifth (the (method (G,C) sig)); i = ins!pc in
pc < size ins \<and> check_instr i G hp ihp stk loc C sig pc z frs'))"
exec_d :: "jvm_prog \<Rightarrow> jvm_state type_error \<Rightarrow> jvm_state option type_error"
"exec_d G s \<equiv> case s of
TypeError \<Rightarrow> TypeError
| Normal s' \<Rightarrow> if check G s' then Normal (exec (G, s')) else TypeError"
consts
"exec_all_d" :: "jvm_prog \<Rightarrow> jvm_state type_error \<Rightarrow> jvm_state type_error \<Rightarrow> bool"
("_ |- _ -jvmd-> _" [61,61,61]60)
syntax (xsymbols)
"exec_all_d" :: "jvm_prog \<Rightarrow> jvm_state type_error \<Rightarrow> jvm_state type_error \<Rightarrow> bool"
("_ \<turnstile> _ -jvmd\<rightarrow> _" [61,61,61]60)
defs
exec_all_d_def:
"G \<turnstile> s -jvmd\<rightarrow> t \<equiv>
(s,t) \<in> ({(s,t). exec_d G s = TypeError \<and> t = TypeError} \<union>
{(s,t). \<exists>t'. exec_d G s = Normal (Some t') \<and> t = Normal t'})\<^sup>*"
declare split_paired_All [simp del]
declare split_paired_Ex [simp del]
lemma [dest!]:
"(if P then A else B) \<noteq> B \<Longrightarrow> P"
by (cases P, auto)
lemma exec_d_no_errorI [intro]:
"check G s \<Longrightarrow> exec_d G (Normal s) \<noteq> TypeError"
by (unfold exec_d_def) simp
theorem no_type_error_commutes:
"exec_d G (Normal s) \<noteq> TypeError \<Longrightarrow>
exec_d G (Normal s) = Normal (exec (G, s))"
by (unfold exec_d_def, auto)
lemma defensive_imp_aggressive:
"G \<turnstile> (Normal s) -jvmd\<rightarrow> (Normal t) \<Longrightarrow> G \<turnstile> s -jvm\<rightarrow> t"
proof -
have "\<And>x y. G \<turnstile> x -jvmd\<rightarrow> y \<Longrightarrow> \<forall>s t. x = Normal s \<longrightarrow> y = Normal t \<longrightarrow> G \<turnstile> s -jvm\<rightarrow> t"
apply (unfold exec_all_d_def)
apply (erule rtrancl_induct)
apply (simp add: exec_all_def)
apply (fold exec_all_d_def)
apply simp
apply (intro allI impI)
apply (erule disjE, simp)
apply (elim exE conjE)
apply (erule allE, erule impE, assumption)
apply (simp add: exec_all_def exec_d_def split: type_error.splits split_if_asm)
apply (rule rtrancl_trans, assumption)
apply blast
done
moreover
assume "G \<turnstile> (Normal s) -jvmd\<rightarrow> (Normal t)"
ultimately
show "G \<turnstile> s -jvm\<rightarrow> t" by blast
qed
end
lemma
(if P then A else B) ~= B ==> P
lemma exec_d_no_errorI:
check G s ==> exec_d G (Normal s) ~= TypeError
theorem no_type_error_commutes:
exec_d G (Normal s) ~= TypeError ==> exec_d G (Normal s) = Normal (exec (G, s))
lemma defensive_imp_aggressive:
G |- Normal s -jvmd-> Normal t ==> G |- s -jvm-> t