# HG changeset patch # User kleing # Date 976480814 -3600 # Node ID 41d309b48afe6e0de3af7a32f47f91838d44e7d2 # Parent d1efa59ea259a7111eb39f7f54c102c4d2dbf2c1 kildall ==> wt_method for whole program diff -r d1efa59ea259 -r 41d309b48afe src/HOL/MicroJava/BV/JVM.thy --- a/src/HOL/MicroJava/BV/JVM.thy Fri Dec 08 15:10:36 2000 +0100 +++ b/src/HOL/MicroJava/BV/JVM.thy Sun Dec 10 21:40:14 2000 +0100 @@ -3,10 +3,9 @@ Author: Tobias Nipkow Copyright 2000 TUM -A micro-JVM *) -header "JVM" +header "Kildall for the JVM" theory JVM = Kildall + JType + Opt + Product + DFA_err + StepMono + BVSpec: @@ -41,6 +40,17 @@ "kiljvm G maxs maxr rT bs == kildall (sl G maxs maxr) (exec G maxs rT bs) (\pc. succs (bs!pc) pc)" + wt_kil :: "jvm_prog \ cname \ ty list \ ty \ nat \ nat \ instr list \ bool" + "wt_kil G C pTs rT mxs mxl ins == + bounded (\n. succs (ins!n) n) (size ins) \ 0 < size ins \ + (let first = Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)); + start = OK first#(replicate (size ins-1) (OK None)); + result = kiljvm G mxs (1+size pTs+mxl) rT ins start + in \n < size ins. result!n \ Err)" + + wt_jvm_prog_kildall :: "jvm_prog => bool" + "wt_jvm_prog_kildall G == + wf_prog (\G C (sig,rT,(maxs,maxl,b)). wt_kil G C (snd sig) rT maxs maxl b) G" lemma JVM_states_unfold: "states S maxs maxr == err(opt((Union {list n (types S) |n. n <= maxs}) <*> @@ -155,32 +165,34 @@ apply clarify apply (case_tac "bs!p") - apply clarsimp - apply clarsimp - apply clarsimp - apply clarsimp - apply clarsimp + apply fastsimp + apply fastsimp + apply fastsimp + apply fastsimp + apply fastsimp apply clarsimp defer - apply clarsimp - apply clarsimp + apply fastsimp + apply fastsimp apply clarsimp defer - apply clarsimp - apply clarsimp - apply clarsimp - apply clarsimp - apply clarsimp - apply clarsimp - apply clarsimp - apply clarsimp - apply clarsimp + apply fastsimp + apply fastsimp + apply fastsimp + apply fastsimp + apply fastsimp + apply fastsimp + apply fastsimp + apply fastsimp + apply fastsimp defer + (* Invoke *) apply (simp add: Un_subset_iff) apply (drule method_wf_mdecl, assumption+) apply (simp add: wf_mdecl_def wf_mhead_def) + (* Getfield *) apply (rule_tac fn = "(vname,cname)" in fields_is_type) defer apply assumption+ @@ -251,26 +263,27 @@ apply (erule exec_mono) done -theorem - "[| wf_prog wf_mb G; bounded (\pc. succs (bs!pc) pc) (size bs); - 0 < size bs; - r = kiljvm G maxs maxr rT bs - (OK (Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)))#(replicate (size bs-1) (OK None))); - \n < size bs. r!n \ Err; maxr = Suc (length pTs + mxl); + +theorem wt_kil_correct: + "[| wt_kil G C pTs rT maxs mxl bs; wf_prog wf_mb G; is_class G C; \x \ set pTs. is_type G x |] ==> \phi. wt_method G C pTs rT maxs mxl bs phi" proof - let ?start = "OK (Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err))) #(replicate (size bs-1) (OK None))" - assume wf: "wf_prog wf_mb G" - assume bounded: "bounded (\pc. succs (bs!pc) pc) (size bs)" - assume result: "r = kiljvm G maxs maxr rT bs ?start" - assume success: "\n < size bs. r!n \ Err" - assume instrs: "0 < size bs" - assume maxr: "maxr = Suc (length pTs + mxl)" - assume isclass: "is_class G C" - assume istype: "\x \ set pTs. is_type G x" + assume wf: "wf_prog wf_mb G" + assume isclass: "is_class G C" + assume istype: "\x \ set pTs. is_type G x" + + assume "wt_kil G C pTs rT maxs mxl bs" + then obtain maxr r where + bounded: "bounded (\pc. succs (bs!pc) pc) (size bs)" and + result: "r = kiljvm G maxs maxr rT bs ?start" and + success: "\n < size bs. r!n \ Err" and + instrs: "0 < size bs" and + maxr: "maxr = Suc (length pTs + mxl)" + by (unfold wt_kil_def) simp { fix pc have "succs (bs!pc) pc \ []" @@ -345,7 +358,6 @@ have phi0: "OK (map ok_val phi' ! 0) = phi' ! 0" by clarsimp - from l bounded have "bounded (\pc. succs (bs ! pc) pc) (length phi')" by simp @@ -374,4 +386,58 @@ thus ?thesis by blast qed +lemma is_type_pTs: + "[| wf_prog wf_mb G; (C,S,fs,mdecls) \ set G; (sig,rT,code) \ set mdecls; + t \ set (snd sig) |] + ==> is_type G t" +proof - + assume "wf_prog wf_mb G" + "(C,S,fs,mdecls) \ set G" + "(sig,rT,code) \ set mdecls" + hence "wf_mdecl wf_mb G C (sig,rT,code)" + by (unfold wf_prog_def wf_cdecl_def) auto + hence "\t \ set (snd sig). is_type G t" + by (unfold wf_mdecl_def wf_mhead_def) auto + moreover + assume "t \ set (snd sig)" + ultimately + show ?thesis by blast +qed + + +theorem jvm_kildall_correct: + "wt_jvm_prog_kildall G ==> \Phi. wt_jvm_prog G Phi" +proof - + assume wtk: "wt_jvm_prog_kildall G" + + then obtain wf_mb where + wf: "wf_prog wf_mb G" + by (auto simp add: wt_jvm_prog_kildall_def) + + let ?Phi = "\C sig. let (C,rT,(maxs,maxl,ins)) = the (method (G,C) sig) in + SOME phi. wt_method G C (snd sig) rT maxs maxl ins phi" + + { fix C S fs mdecls sig rT code + assume "(C,S,fs,mdecls) \ set G" "(sig,rT,code) \ set mdecls" + with wf + have "method (G,C) sig = Some (C,rT,code) \ is_class G C \ (\t \ set (snd sig). is_type G t)" + by (simp add: methd is_type_pTs) + } note this [simp] + + from wtk + have "wt_jvm_prog G ?Phi" + apply (unfold wt_jvm_prog_def wt_jvm_prog_kildall_def wf_prog_def wf_cdecl_def) + apply clarsimp + apply (drule bspec, assumption) + apply (unfold wf_mdecl_def) + apply clarsimp + apply (drule bspec, assumption) + apply clarsimp + apply (drule wt_kil_correct [OF _ wf]) + apply (auto intro: someI) + done + + thus ?thesis by blast +qed + end