(* Title: HOL/MicroJava/JVM/JVMDefensive.thy ID: $Id: JVMDefensive.thy,v 1.6 2005/06/17 14:13:09 haftmann Exp $ Author: Gerwin Klein *) header {* \isaheader{A Defensive JVM} *} theory JVMDefensive imports JVMExec begin 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 => 'e" translations "fifth x" == "fst(snd(snd(snd(snd x))))" consts isAddr :: "val => bool" recdef isAddr "{}" "isAddr (Addr loc) = True" "isAddr v = False" consts isIntg :: "val => bool" recdef isIntg "{}" "isIntg (Intg i) = True" "isIntg v = False" constdefs isRef :: "val => bool" "isRef v ≡ v = Null ∨ isAddr v" consts check_instr :: "[instr, jvm_prog, aheap, opstack, locvars, cname, sig, p_count, nat, frame list] => bool" primrec "check_instr (Load idx) G hp stk vars C sig pc mxs frs = (idx < length vars ∧ size stk < mxs)" "check_instr (Store idx) G hp stk vars Cl sig pc mxs frs = (0 < length stk ∧ idx < length vars)" "check_instr (LitPush v) G hp stk vars Cl sig pc mxs frs = (¬isAddr v ∧ size stk < mxs)" "check_instr (New C) G hp stk vars Cl sig pc mxs frs = (is_class G C ∧ size stk < mxs)" "check_instr (Getfield F C) G hp stk vars Cl sig pc mxs frs = (0 < length stk ∧ is_class G C ∧ field (G,C) F ≠ None ∧ (let (C', T) = the (field (G,C) F); ref = hd stk in C' = C ∧ isRef ref ∧ (ref ≠ Null --> hp (the_Addr ref) ≠ None ∧ (let (D,vs) = the (hp (the_Addr ref)) in G \<turnstile> D \<preceq>C C ∧ vs (F,C) ≠ None ∧ G,hp \<turnstile> the (vs (F,C)) ::\<preceq> T))))" "check_instr (Putfield F C) G hp stk vars Cl sig pc mxs frs = (1 < length stk ∧ is_class G C ∧ field (G,C) F ≠ None ∧ (let (C', T) = the (field (G,C) F); v = hd stk; ref = hd (tl stk) in C' = C ∧ isRef ref ∧ (ref ≠ Null --> hp (the_Addr ref) ≠ None ∧ (let (D,vs) = the (hp (the_Addr ref)) in G \<turnstile> D \<preceq>C C ∧ G,hp \<turnstile> v ::\<preceq> T))))" "check_instr (Checkcast C) G hp stk vars Cl sig pc mxs frs = (0 < length stk ∧ is_class G C ∧ isRef (hd stk))" "check_instr (Invoke C mn ps) G hp stk vars Cl sig pc mxs frs = (length ps < length stk ∧ (let n = length ps; v = stk!n in isRef v ∧ (v ≠ Null --> hp (the_Addr v) ≠ None ∧ method (G,cname_of hp v) (mn,ps) ≠ None ∧ list_all2 (λv T. G,hp \<turnstile> v ::\<preceq> T) (rev (take n stk)) ps)))" "check_instr Return G hp stk0 vars Cl sig0 pc mxs frs = (0 < length stk0 ∧ (0 < length frs --> method (G,Cl) sig0 ≠ None ∧ (let v = hd stk0; (C, rT, body) = the (method (G,Cl) sig0) in Cl = C ∧ G,hp \<turnstile> v ::\<preceq> rT)))" "check_instr Pop G hp stk vars Cl sig pc mxs frs = (0 < length stk)" "check_instr Dup G hp stk vars Cl sig pc mxs frs = (0 < length stk ∧ size stk < mxs)" "check_instr Dup_x1 G hp stk vars Cl sig pc mxs frs = (1 < length stk ∧ size stk < mxs)" "check_instr Dup_x2 G hp stk vars Cl sig pc mxs frs = (2 < length stk ∧ size stk < mxs)" "check_instr Swap G hp stk vars Cl sig pc mxs frs = (1 < length stk)" "check_instr IAdd G hp stk vars Cl sig pc mxs frs = (1 < length stk ∧ isIntg (hd stk) ∧ isIntg (hd (tl stk)))" "check_instr (Ifcmpeq b) G hp stk vars Cl sig pc mxs frs = (1 < length stk ∧ 0 ≤ int pc+b)" "check_instr (Goto b) G hp stk vars Cl sig pc mxs frs = (0 ≤ int pc+b)" "check_instr Throw G hp stk vars Cl sig pc mxs frs = (0 < length stk ∧ isRef (hd stk))" constdefs check :: "jvm_prog => jvm_state => bool" "check G s ≡ let (xcpt, hp, frs) = s in (case frs of [] => True | (stk,loc,C,sig,pc)#frs' => (let (C',rt,mxs,mxl,ins,et) = the (method (G,C) sig); i = ins!pc in pc < size ins ∧ check_instr i G hp stk loc C sig pc mxs frs'))" exec_d :: "jvm_prog => jvm_state type_error => jvm_state option type_error" "exec_d G s ≡ case s of TypeError => TypeError | Normal s' => if check G s' then Normal (exec (G, s')) else TypeError" consts "exec_all_d" :: "jvm_prog => jvm_state type_error => jvm_state type_error => bool" ("_ |- _ -jvmd-> _" [61,61,61]60) syntax (xsymbols) "exec_all_d" :: "jvm_prog => jvm_state type_error => jvm_state type_error => bool" ("_ \<turnstile> _ -jvmd-> _" [61,61,61]60) defs exec_all_d_def: "G \<turnstile> s -jvmd-> t ≡ (s,t) ∈ ({(s,t). exec_d G s = TypeError ∧ t = TypeError} ∪ {(s,t). ∃t'. exec_d G s = Normal (Some t') ∧ t = Normal t'})*" declare split_paired_All [simp del] declare split_paired_Ex [simp del] lemma [dest!]: "(if P then A else B) ≠ B ==> P" by (cases P, auto) lemma exec_d_no_errorI [intro]: "check G s ==> exec_d G (Normal s) ≠ TypeError" by (unfold exec_d_def) simp theorem no_type_error_commutes: "exec_d G (Normal s) ≠ TypeError ==> exec_d G (Normal s) = Normal (exec (G, s))" by (unfold exec_d_def, auto) lemma defensive_imp_aggressive: "G \<turnstile> (Normal s) -jvmd-> (Normal t) ==> G \<turnstile> s -jvm-> t" proof - have "!!x y. G \<turnstile> x -jvmd-> y ==> ∀s t. x = Normal s --> y = Normal t --> G \<turnstile> s -jvm-> 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-> (Normal t)" ultimately show "G \<turnstile> s -jvm-> 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