1(* Title: HOL/MicroJava/JVM/JVMDefensive.thy 2 Author: Gerwin Klein 3*) 4 5section \<open>A Defensive JVM\<close> 6 7theory JVMDefensive 8imports JVMExec 9begin 10 11text \<open> 12 Extend the state space by one element indicating a type error (or 13 other abnormal termination)\<close> 14datatype 'a type_error = TypeError | Normal 'a 15 16 17abbreviation 18 fifth :: "'a \<times> 'b \<times> 'c \<times> 'd \<times> 'e \<times> 'f \<Rightarrow> 'e" 19 where "fifth x == fst(snd(snd(snd(snd x))))" 20 21fun isAddr :: "val \<Rightarrow> bool" where 22 "isAddr (Addr loc) = True" 23| "isAddr v = False" 24 25fun isIntg :: "val \<Rightarrow> bool" where 26 "isIntg (Intg i) = True" 27| "isIntg v = False" 28 29definition isRef :: "val \<Rightarrow> bool" where 30 "isRef v \<equiv> v = Null \<or> isAddr v" 31 32primrec check_instr :: "[instr, jvm_prog, aheap, opstack, locvars, 33 cname, sig, p_count, nat, frame list] \<Rightarrow> bool" where 34 "check_instr (Load idx) G hp stk vars C sig pc mxs frs = 35 (idx < length vars \<and> size stk < mxs)" 36 37| "check_instr (Store idx) G hp stk vars Cl sig pc mxs frs = 38 (0 < length stk \<and> idx < length vars)" 39 40| "check_instr (LitPush v) G hp stk vars Cl sig pc mxs frs = 41 (\<not>isAddr v \<and> size stk < mxs)" 42 43| "check_instr (New C) G hp stk vars Cl sig pc mxs frs = 44 (is_class G C \<and> size stk < mxs)" 45 46| "check_instr (Getfield F C) G hp stk vars Cl sig pc mxs frs = 47 (0 < length stk \<and> is_class G C \<and> field (G,C) F \<noteq> None \<and> 48 (let (C', T) = the (field (G,C) F); ref = hd stk in 49 C' = C \<and> isRef ref \<and> (ref \<noteq> Null \<longrightarrow> 50 hp (the_Addr ref) \<noteq> None \<and> 51 (let (D,vs) = the (hp (the_Addr ref)) in 52 G \<turnstile> D \<preceq>C C \<and> vs (F,C) \<noteq> None \<and> G,hp \<turnstile> the (vs (F,C)) ::\<preceq> T))))" 53 54| "check_instr (Putfield F C) G hp stk vars Cl sig pc mxs frs = 55 (1 < length stk \<and> is_class G C \<and> field (G,C) F \<noteq> None \<and> 56 (let (C', T) = the (field (G,C) F); v = hd stk; ref = hd (tl stk) in 57 C' = C \<and> isRef ref \<and> (ref \<noteq> Null \<longrightarrow> 58 hp (the_Addr ref) \<noteq> None \<and> 59 (let (D,vs) = the (hp (the_Addr ref)) in 60 G \<turnstile> D \<preceq>C C \<and> G,hp \<turnstile> v ::\<preceq> T))))" 61 62| "check_instr (Checkcast C) G hp stk vars Cl sig pc mxs frs = 63 (0 < length stk \<and> is_class G C \<and> isRef (hd stk))" 64 65| "check_instr (Invoke C mn ps) G hp stk vars Cl sig pc mxs frs = 66 (length ps < length stk \<and> 67 (let n = length ps; v = stk!n in 68 isRef v \<and> (v \<noteq> Null \<longrightarrow> 69 hp (the_Addr v) \<noteq> None \<and> 70 method (G,cname_of hp v) (mn,ps) \<noteq> None \<and> 71 list_all2 (\<lambda>v T. G,hp \<turnstile> v ::\<preceq> T) (rev (take n stk)) ps)))" 72 73| "check_instr Return G hp stk0 vars Cl sig0 pc mxs frs = 74 (0 < length stk0 \<and> (0 < length frs \<longrightarrow> 75 method (G,Cl) sig0 \<noteq> None \<and> 76 (let v = hd stk0; (C, rT, body) = the (method (G,Cl) sig0) in 77 Cl = C \<and> G,hp \<turnstile> v ::\<preceq> rT)))" 78 79| "check_instr Pop G hp stk vars Cl sig pc mxs frs = 80 (0 < length stk)" 81 82| "check_instr Dup G hp stk vars Cl sig pc mxs frs = 83 (0 < length stk \<and> size stk < mxs)" 84 85| "check_instr Dup_x1 G hp stk vars Cl sig pc mxs frs = 86 (1 < length stk \<and> size stk < mxs)" 87 88| "check_instr Dup_x2 G hp stk vars Cl sig pc mxs frs = 89 (2 < length stk \<and> size stk < mxs)" 90 91| "check_instr Swap G hp stk vars Cl sig pc mxs frs = 92 (1 < length stk)" 93 94| "check_instr IAdd G hp stk vars Cl sig pc mxs frs = 95 (1 < length stk \<and> isIntg (hd stk) \<and> isIntg (hd (tl stk)))" 96 97| "check_instr (Ifcmpeq b) G hp stk vars Cl sig pc mxs frs = 98 (1 < length stk \<and> 0 \<le> int pc+b)" 99 100| "check_instr (Goto b) G hp stk vars Cl sig pc mxs frs = 101 (0 \<le> int pc+b)" 102 103| "check_instr Throw G hp stk vars Cl sig pc mxs frs = 104 (0 < length stk \<and> isRef (hd stk))" 105 106definition check :: "jvm_prog \<Rightarrow> jvm_state \<Rightarrow> bool" where 107 "check G s \<equiv> let (xcpt, hp, frs) = s in 108 (case frs of [] \<Rightarrow> True | (stk,loc,C,sig,pc)#frs' \<Rightarrow> 109 (let (C',rt,mxs,mxl,ins,et) = the (method (G,C) sig); i = ins!pc in 110 pc < size ins \<and> 111 check_instr i G hp stk loc C sig pc mxs frs'))" 112 113 114definition exec_d :: "jvm_prog \<Rightarrow> jvm_state type_error \<Rightarrow> jvm_state option type_error" where 115 "exec_d G s \<equiv> case s of 116 TypeError \<Rightarrow> TypeError 117 | Normal s' \<Rightarrow> if check G s' then Normal (exec (G, s')) else TypeError" 118 119 120definition 121 exec_all_d :: "jvm_prog \<Rightarrow> jvm_state type_error \<Rightarrow> jvm_state type_error \<Rightarrow> bool" 122 ("_ \<turnstile> _ \<midarrow>jvmd\<rightarrow> _" [61,61,61]60) where 123 "G \<turnstile> s \<midarrow>jvmd\<rightarrow> t \<longleftrightarrow> 124 (s,t) \<in> ({(s,t). exec_d G s = TypeError \<and> t = TypeError} \<union> 125 {(s,t). \<exists>t'. exec_d G s = Normal (Some t') \<and> t = Normal t'})\<^sup>*" 126 127 128declare split_paired_All [simp del] 129declare split_paired_Ex [simp del] 130 131lemma [dest!]: 132 "(if P then A else B) \<noteq> B \<Longrightarrow> P" 133 by (cases P, auto) 134 135lemma exec_d_no_errorI [intro]: 136 "check G s \<Longrightarrow> exec_d G (Normal s) \<noteq> TypeError" 137 by (unfold exec_d_def) simp 138 139theorem no_type_error_commutes: 140 "exec_d G (Normal s) \<noteq> TypeError \<Longrightarrow> 141 exec_d G (Normal s) = Normal (exec (G, s))" 142 by (unfold exec_d_def, auto) 143 144 145lemma defensive_imp_aggressive: 146 "G \<turnstile> (Normal s) \<midarrow>jvmd\<rightarrow> (Normal t) \<Longrightarrow> G \<turnstile> s \<midarrow>jvm\<rightarrow> t" 147proof - 148 have "\<And>x y. G \<turnstile> x \<midarrow>jvmd\<rightarrow> y \<Longrightarrow> \<forall>s t. x = Normal s \<longrightarrow> y = Normal t \<longrightarrow> G \<turnstile> s \<midarrow>jvm\<rightarrow> t" 149 apply (unfold exec_all_d_def) 150 apply (erule rtrancl_induct) 151 apply (simp add: exec_all_def) 152 apply (fold exec_all_d_def) 153 apply simp 154 apply (intro allI impI) 155 apply (erule disjE, simp) 156 apply (elim exE conjE) 157 apply (erule allE, erule impE, assumption) 158 apply (simp add: exec_all_def exec_d_def split: type_error.splits if_split_asm) 159 apply (rule rtrancl_trans, assumption) 160 apply blast 161 done 162 moreover 163 assume "G \<turnstile> (Normal s) \<midarrow>jvmd\<rightarrow> (Normal t)" 164 ultimately 165 show "G \<turnstile> s \<midarrow>jvm\<rightarrow> t" by blast 166qed 167 168end 169