1(* Title: HOL/MicroJava/BV/JVM.thy 2 Author: Tobias Nipkow, Gerwin Klein 3 Copyright 2000 TUM 4*) 5 6section \<open>Kildall for the JVM \label{sec:JVM}\<close> 7 8theory JVM 9imports Typing_Framework_JVM 10begin 11 12definition kiljvm :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> exception_table \<Rightarrow> 13 instr list \<Rightarrow> JVMType.state list \<Rightarrow> JVMType.state list" where 14 "kiljvm G maxs maxr rT et bs == 15 kildall (JVMType.le G maxs maxr) (JVMType.sup G maxs maxr) (exec G maxs rT et bs)" 16 17definition wt_kil :: "jvm_prog \<Rightarrow> cname \<Rightarrow> ty list \<Rightarrow> ty \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 18 exception_table \<Rightarrow> instr list \<Rightarrow> bool" where 19 "wt_kil G C pTs rT mxs mxl et ins == 20 check_bounded ins et \<and> 0 < size ins \<and> 21 (let first = Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)); 22 start = OK first#(replicate (size ins - 1) (OK None)); 23 result = kiljvm G mxs (1+size pTs+mxl) rT et ins start 24 in \<forall>n < size ins. result!n \<noteq> Err)" 25 26definition wt_jvm_prog_kildall :: "jvm_prog \<Rightarrow> bool" where 27 "wt_jvm_prog_kildall G == 28 wf_prog (\<lambda>G C (sig,rT,(maxs,maxl,b,et)). wt_kil G C (snd sig) rT maxs maxl et b) G" 29 30theorem is_bcv_kiljvm: 31 "\<lbrakk> wf_prog wf_mb G; bounded (exec G maxs rT et bs) (size bs) \<rbrakk> \<Longrightarrow> 32 is_bcv (JVMType.le G maxs maxr) Err (exec G maxs rT et bs) 33 (size bs) (states G maxs maxr) (kiljvm G maxs maxr rT et bs)" 34 apply (unfold kiljvm_def sl_triple_conv) 35 apply (rule is_bcv_kildall) 36 apply (simp (no_asm) add: sl_triple_conv [symmetric]) 37 apply (force intro!: semilat_JVM_slI dest: wf_acyclic 38 simp add: symmetric sl_triple_conv) 39 apply (simp (no_asm) add: JVM_le_unfold) 40 apply (blast intro!: order_widen wf_converse_subcls1_impl_acc_subtype 41 dest: wf_subcls1 wf_acyclic wf_prog_ws_prog) 42 apply (simp add: JVM_le_unfold) 43 apply (erule exec_pres_type) 44 apply assumption 45 apply (drule wf_prog_ws_prog, erule exec_mono, assumption) 46 done 47 48lemma subset_replicate: "set (replicate n x) \<subseteq> {x}" 49 by (induct n) auto 50 51lemma in_set_replicate: 52 "x \<in> set (replicate n y) \<Longrightarrow> x = y" 53proof - 54 assume "x \<in> set (replicate n y)" 55 also have "set (replicate n y) \<subseteq> {y}" by (rule subset_replicate) 56 finally have "x \<in> {y}" . 57 thus ?thesis by simp 58qed 59 60theorem wt_kil_correct: 61 assumes wf: "wf_prog wf_mb G" 62 assumes C: "is_class G C" 63 assumes pTs: "set pTs \<subseteq> types G" 64 65 assumes wtk: "wt_kil G C pTs rT maxs mxl et bs" 66 67 shows "\<exists>phi. wt_method G C pTs rT maxs mxl bs et phi" 68proof - 69 let ?start = "OK (Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err))) 70 #(replicate (size bs - 1) (OK None))" 71 72 from wtk obtain maxr r where 73 bounded: "check_bounded bs et" and 74 result: "r = kiljvm G maxs maxr rT et bs ?start" and 75 success: "\<forall>n < size bs. r!n \<noteq> Err" and 76 instrs: "0 < size bs" and 77 maxr: "maxr = Suc (length pTs + mxl)" 78 by (unfold wt_kil_def) simp 79 80 from bounded have "bounded (exec G maxs rT et bs) (size bs)" 81 by (unfold exec_def) (intro bounded_lift check_bounded_is_bounded) 82 with wf have bcv: 83 "is_bcv (JVMType.le G maxs maxr) Err (exec G maxs rT et bs) 84 (size bs) (states G maxs maxr) (kiljvm G maxs maxr rT et bs)" 85 by (rule is_bcv_kiljvm) 86 87 from C pTs instrs maxr 88 have "?start \<in> list (length bs) (states G maxs maxr)" 89 apply (unfold JVM_states_unfold) 90 apply (rule listI) 91 apply (auto intro: list_appendI dest!: in_set_replicate) 92 apply force 93 done 94 95 with bcv success result have 96 "\<exists>ts\<in>list (length bs) (states G maxs maxr). 97 ?start <=[JVMType.le G maxs maxr] ts \<and> 98 wt_step (JVMType.le G maxs maxr) Err (exec G maxs rT et bs) ts" 99 by (unfold is_bcv_def) auto 100 then obtain phi' where 101 phi': "phi' \<in> list (length bs) (states G maxs maxr)" and 102 s: "?start <=[JVMType.le G maxs maxr] phi'" and 103 w: "wt_step (JVMType.le G maxs maxr) Err (exec G maxs rT et bs) phi'" 104 by blast 105 hence wt_err_step: 106 "wt_err_step (sup_state_opt G) (exec G maxs rT et bs) phi'" 107 by (simp add: wt_err_step_def exec_def JVM_le_Err_conv) 108 109 from s have le: "JVMType.le G maxs maxr (?start ! 0) (phi'!0)" 110 by (drule_tac p=0 in le_listD) (simp add: lesub_def)+ 111 112 from phi' have l: "size phi' = size bs" by simp 113 with instrs w have "phi' ! 0 \<noteq> Err" by (unfold wt_step_def) simp 114 with instrs l have phi0: "OK (map ok_val phi' ! 0) = phi' ! 0" 115 by auto 116 117 from phi' have "check_types G maxs maxr phi'" by(simp add: check_types_def) 118 also from w have "phi' = map OK (map ok_val phi')" 119 by (auto simp add: wt_step_def intro!: nth_equalityI) 120 finally 121 have check_types: 122 "check_types G maxs maxr (map OK (map ok_val phi'))" . 123 124 from l bounded 125 have "bounded (\<lambda>pc. eff (bs!pc) G pc et) (length phi')" 126 by (simp add: exec_def check_bounded_is_bounded) 127 hence bounded': "bounded (exec G maxs rT et bs) (length bs)" 128 by (auto intro: bounded_lift simp add: exec_def l) 129 with wt_err_step 130 have "wt_app_eff (sup_state_opt G) (\<lambda>pc. app (bs!pc) G maxs rT pc et) 131 (\<lambda>pc. eff (bs!pc) G pc et) (map ok_val phi')" 132 by (auto intro: wt_err_imp_wt_app_eff simp add: l exec_def) 133 with instrs l le bounded bounded' check_types maxr 134 have "wt_method G C pTs rT maxs mxl bs et (map ok_val phi')" 135 apply (unfold wt_method_def wt_app_eff_def) 136 apply simp 137 apply (rule conjI) 138 apply (unfold wt_start_def) 139 apply (rule JVM_le_convert [THEN iffD1]) 140 apply (simp (no_asm) add: phi0) 141 apply clarify 142 apply (erule allE, erule impE, assumption) 143 apply (elim conjE) 144 apply (clarsimp simp add: lesub_def wt_instr_def) 145 apply (simp add: exec_def) 146 apply (drule bounded_err_stepD, assumption+) 147 apply blast 148 done 149 150 thus ?thesis by blast 151qed 152 153 154theorem wt_kil_complete: 155 assumes wf: "wf_prog wf_mb G" 156 assumes C: "is_class G C" 157 assumes pTs: "set pTs \<subseteq> types G" 158 159 assumes wtm: "wt_method G C pTs rT maxs mxl bs et phi" 160 161 shows "wt_kil G C pTs rT maxs mxl et bs" 162proof - 163 let ?mxr = "1+size pTs+mxl" 164 165 from wtm obtain 166 instrs: "0 < length bs" and 167 len: "length phi = length bs" and 168 bounded: "check_bounded bs et" and 169 ck_types: "check_types G maxs ?mxr (map OK phi)" and 170 wt_start: "wt_start G C pTs mxl phi" and 171 wt_ins: "\<forall>pc. pc < length bs \<longrightarrow> 172 wt_instr (bs ! pc) G rT phi maxs (length bs) et pc" 173 by (unfold wt_method_def) simp 174 175 from ck_types len 176 have istype_phi: 177 "map OK phi \<in> list (length bs) (states G maxs (1+size pTs+mxl))" 178 by (auto simp add: check_types_def intro!: listI) 179 180 let ?eff = "\<lambda>pc. eff (bs!pc) G pc et" 181 let ?app = "\<lambda>pc. app (bs!pc) G maxs rT pc et" 182 183 from bounded 184 have bounded_exec: "bounded (exec G maxs rT et bs) (size bs)" 185 by (unfold exec_def) (intro bounded_lift check_bounded_is_bounded) 186 187 from wt_ins 188 have "wt_app_eff (sup_state_opt G) ?app ?eff phi" 189 apply (unfold wt_app_eff_def wt_instr_def lesub_def) 190 apply (simp (no_asm) only: len) 191 apply blast 192 done 193 with bounded_exec 194 have "wt_err_step (sup_state_opt G) (err_step (size phi) ?app ?eff) (map OK phi)" 195 by - (erule wt_app_eff_imp_wt_err,simp add: exec_def len) 196 hence wt_err: 197 "wt_err_step (sup_state_opt G) (exec G maxs rT et bs) (map OK phi)" 198 by (unfold exec_def) (simp add: len) 199 200 from wf bounded_exec 201 have is_bcv: 202 "is_bcv (JVMType.le G maxs ?mxr) Err (exec G maxs rT et bs) 203 (size bs) (states G maxs ?mxr) (kiljvm G maxs ?mxr rT et bs)" 204 by (rule is_bcv_kiljvm) 205 206 let ?start = "OK (Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err))) 207 #(replicate (size bs - 1) (OK None))" 208 209 from C pTs instrs 210 have start: "?start \<in> list (length bs) (states G maxs ?mxr)" 211 apply (unfold JVM_states_unfold) 212 apply (rule listI) 213 apply (auto intro!: list_appendI dest!: in_set_replicate) 214 apply force 215 done 216 217 let ?phi = "map OK phi" 218 have less_phi: "?start <=[JVMType.le G maxs ?mxr] ?phi" 219 proof - 220 from len instrs 221 have "length ?start = length (map OK phi)" by simp 222 moreover 223 { fix n 224 from wt_start 225 have "G \<turnstile> ok_val (?start!0) <=' phi!0" 226 by (simp add: wt_start_def) 227 moreover 228 from instrs len 229 have "0 < length phi" by simp 230 ultimately 231 have "JVMType.le G maxs ?mxr (?start!0) (?phi!0)" 232 by (simp add: JVM_le_Err_conv Err.le_def lesub_def) 233 moreover 234 { fix n' 235 have "JVMType.le G maxs ?mxr (OK None) (?phi!n)" 236 by (auto simp add: JVM_le_Err_conv Err.le_def lesub_def 237 split: err.splits) 238 hence "\<lbrakk> n = Suc n'; n < length ?start \<rbrakk> 239 \<Longrightarrow> JVMType.le G maxs ?mxr (?start!n) (?phi!n)" 240 by simp 241 } 242 ultimately 243 have "n < length ?start \<Longrightarrow> (?start!n) <=_(JVMType.le G maxs ?mxr) (?phi!n)" 244 by (unfold lesub_def) (cases n, blast+) 245 } 246 ultimately show ?thesis by (rule le_listI) 247 qed 248 249 from wt_err 250 have "wt_step (JVMType.le G maxs ?mxr) Err (exec G maxs rT et bs) ?phi" 251 by (simp add: wt_err_step_def JVM_le_Err_conv) 252 with start istype_phi less_phi is_bcv 253 have "\<forall>p. p < length bs \<longrightarrow> kiljvm G maxs ?mxr rT et bs ?start ! p \<noteq> Err" 254 by (unfold is_bcv_def) auto 255 with bounded instrs 256 show "wt_kil G C pTs rT maxs mxl et bs" by (unfold wt_kil_def) simp 257qed 258 259 260theorem jvm_kildall_sound_complete: 261 "wt_jvm_prog_kildall G = (\<exists>Phi. wt_jvm_prog G Phi)" 262proof 263 let ?Phi = "\<lambda>C sig. let (C,rT,(maxs,maxl,ins,et)) = the (method (G,C) sig) in 264 SOME phi. wt_method G C (snd sig) rT maxs maxl ins et phi" 265 266 assume "wt_jvm_prog_kildall G" 267 hence "wt_jvm_prog G ?Phi" 268 apply (unfold wt_jvm_prog_def wt_jvm_prog_kildall_def) 269 apply (erule jvm_prog_lift) 270 apply (auto dest!: wt_kil_correct intro: someI) 271 done 272 thus "\<exists>Phi. wt_jvm_prog G Phi" by fast 273next 274 assume "\<exists>Phi. wt_jvm_prog G Phi" 275 thus "wt_jvm_prog_kildall G" 276 apply (clarify) 277 apply (unfold wt_jvm_prog_def wt_jvm_prog_kildall_def) 278 apply (erule jvm_prog_lift) 279 apply (auto intro: wt_kil_complete) 280 done 281qed 282 283end 284