check maxs in defensive machine

--- a/src/HOL/MicroJava/BV/BVNoTypeError.thy	Tue Feb 18 15:09:14 2003 +0100
+++ b/src/HOL/MicroJava/BV/BVNoTypeError.thy	Tue Feb 18 19:13:47 2003 +0100
@@ -281,7 +281,7 @@
       by (clarsimp simp add: app_def)
 
     with eff stk loc pc'
-    have "check_instr (ins!pc) G hp stk loc C sig pc frs'"
+    have "check_instr (ins!pc) G hp stk loc C sig pc maxs frs'"
     proof (cases "ins!pc")
       case (Getfield F C) 
       with app stk loc phi obtain v vT stk' where
@@ -391,7 +391,7 @@
         apply (clarsimp simp add: neq_Nil_conv isRef_def2)
         done
     qed auto
-    hence "check G s" by (simp add: check_def meth)
+    hence "check G s" by (simp add: check_def meth pc)
   } ultimately
   have "check G s" by blast
   thus "exec_d G (Normal s) \<noteq> TypeError" ..
@@ -419,6 +419,32 @@
   done
 
 
+lemma neq_TypeError_eq [simp]: "s \<noteq> TypeError = (\<exists>s'. s = Normal s')"
+  by (cases s, auto)
+
+theorem no_type_errors:
+  "wt_jvm_prog G Phi \<Longrightarrow> G,Phi \<turnstile>JVM s \<surd>
+  \<Longrightarrow> G \<turnstile> (Normal s) -jvmd\<rightarrow> t \<Longrightarrow> t \<noteq> TypeError"
+  apply (unfold exec_all_d_def)   
+  apply (erule rtrancl_induct)
+   apply simp
+  apply (fold exec_all_d_def)
+  apply (auto dest: defensive_imp_aggressive BV_correct no_type_error)
+  done
+
+corollary no_type_errors_initial:
+  fixes G ("\<Gamma>") and Phi ("\<Phi>")
+  assumes "wt_jvm_prog \<Gamma> \<Phi>"  
+  assumes "is_class \<Gamma> C" "method (\<Gamma>,C) (m,[]) = Some (C, b)" "m \<noteq> init"
+  defines start: "s \<equiv> start_state \<Gamma> C m"
+
+  assumes "\<Gamma> \<turnstile> (Normal s) -jvmd\<rightarrow> t" 
+  shows "t \<noteq> TypeError"
+proof -
+  have "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>" by (unfold start, rule BV_correct_initial)
+  thus ?thesis by - (rule no_type_errors)
+qed
+
 text {*
   As corollary we get that the aggressive and the defensive machine
   are equivalent for welltyped programs (if started in a conformant

--- a/src/HOL/MicroJava/JVM/JVMDefensive.thy	Tue Feb 18 15:09:14 2003 +0100
+++ b/src/HOL/MicroJava/JVM/JVMDefensive.thy	Tue Feb 18 19:13:47 2003 +0100
@@ -36,21 +36,21 @@
 
 consts
   check_instr :: "[instr, jvm_prog, aheap, opstack, locvars, 
-                  cname, sig, p_count, frame list] \<Rightarrow> bool"
+                  cname, sig, p_count, nat, frame list] \<Rightarrow> bool"
 primrec 
-  "check_instr (Load idx) G hp stk vars C sig pc frs = 
-  (idx < length vars)"
+  "check_instr (Load idx) G hp stk vars C sig pc mxs frs = 
+  (idx < length vars \<and> size stk < mxs)"
 
-  "check_instr (Store idx) G hp stk vars Cl sig pc frs = 
+  "check_instr (Store idx) G hp stk vars Cl sig pc mxs frs = 
   (0 < length stk \<and> idx < length vars)"
 
-  "check_instr (LitPush v) G hp stk vars Cl sig pc frs = 
-  (\<not>isAddr v)"
+  "check_instr (LitPush v) G hp stk vars Cl sig pc mxs frs = 
+  (\<not>isAddr v \<and> size stk < mxs)"
 
-  "check_instr (New C) G hp stk vars Cl sig pc frs = 
-  is_class G C"
+  "check_instr (New C) G hp stk vars Cl sig pc mxs frs = 
+  (is_class G C \<and> size stk < mxs)"
 
-  "check_instr (Getfield F C) G hp stk vars Cl sig pc frs = 
+  "check_instr (Getfield F C) G hp stk vars Cl sig pc mxs 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> 
@@ -58,7 +58,7 @@
       (let (D,vs) = 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 stk vars Cl sig pc frs = 
+  "check_instr (Putfield F C) G hp stk vars Cl sig pc mxs 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> isRef ref \<and> (ref \<noteq> Null \<longrightarrow> 
@@ -66,10 +66,10 @@
       (let (D,vs) = 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 stk vars Cl sig pc frs =
+  "check_instr (Checkcast C) G hp stk vars Cl sig pc mxs frs =
   (0 < length stk \<and> is_class G C \<and> isRef (hd stk))"
 
-  "check_instr (Invoke C mn ps) G hp stk vars Cl sig pc frs =
+  "check_instr (Invoke C mn ps) G hp stk vars Cl sig pc mxs frs =
   (length ps < length stk \<and> 
   (let n = length ps; v = stk!n in
   isRef v \<and> (v \<noteq> Null \<longrightarrow> 
@@ -77,46 +77,46 @@
     method (G,cname_of hp v) (mn,ps) \<noteq> None \<and>
     list_all2 (\<lambda>v T. G,hp \<turnstile> v ::\<preceq> T) (rev (take n stk)) ps)))"
   
-  "check_instr Return G hp stk0 vars Cl sig0 pc frs =
+  "check_instr Return G hp stk0 vars Cl sig0 pc mxs 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)))"
  
-  "check_instr Pop G hp stk vars Cl sig pc frs = 
+  "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 frs = 
-  (0 < length stk)"
+  "check_instr Dup G hp stk vars Cl sig pc mxs frs = 
+  (0 < length stk \<and> size stk < mxs)"
 
-  "check_instr Dup_x1 G hp stk vars Cl sig pc frs = 
+  "check_instr Dup_x1 G hp stk vars Cl sig pc mxs frs = 
+  (1 < length stk \<and> size stk < mxs)"
+
+  "check_instr Dup_x2 G hp stk vars Cl sig pc mxs frs = 
+  (2 < length stk \<and> size stk < mxs)"
+
+  "check_instr Swap G hp stk vars Cl sig pc mxs frs =
   (1 < length stk)"
 
-  "check_instr Dup_x2 G hp stk vars Cl sig pc frs = 
-  (2 < length stk)"
-
-  "check_instr Swap G hp stk vars Cl sig pc frs =
-  (1 < length stk)"
-
-  "check_instr IAdd G hp stk vars Cl sig pc frs =
+  "check_instr IAdd G hp stk vars Cl sig pc mxs frs =
   (1 < length stk \<and> isIntg (hd stk) \<and> isIntg (hd (tl stk)))"
 
-  "check_instr (Ifcmpeq b) G hp stk vars Cl sig pc frs =
+  "check_instr (Ifcmpeq b) G hp stk vars Cl sig pc mxs frs =
   (1 < length stk \<and> 0 \<le> int pc+b)"
 
-  "check_instr (Goto b) G hp stk vars Cl sig pc frs =
+  "check_instr (Goto b) G hp stk vars Cl sig pc mxs frs =
   (0 \<le> int pc+b)"
 
-  "check_instr Throw G hp stk vars Cl sig pc frs =
+  "check_instr Throw G hp stk vars Cl sig pc mxs frs =
   (0 < length stk \<and> isRef (hd stk))"
 
 constdefs
   check :: "jvm_prog \<Rightarrow> jvm_state \<Rightarrow> bool"
   "check G s \<equiv> let (xcpt, hp, frs) = s in
                (case frs of [] \<Rightarrow> True | (stk,loc,C,sig,pc)#frs' \<Rightarrow> 
-                (let ins = fifth (the (method (G,C) sig)); i = ins!pc in
-                 pc < size ins \<and>
-                 check_instr i G hp 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 \<and> 
+                 check_instr i G hp stk loc C sig pc mxs frs'))"
 
 
   exec_d :: "jvm_prog \<Rightarrow> jvm_state type_error \<Rightarrow> jvm_state option type_error"