exception merge + cleanup

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/JVM/JVMExceptions.thy	Sun Dec 16 00:19:08 2001 +0100
@@ -0,0 +1,66 @@
+(*  Title:      HOL/MicroJava/JVM/JVMExceptions.thy
+    ID:         $Id$
+    Author:     Gerwin Klein, Martin Strecker
+    Copyright   2001 Technische Universitaet Muenchen
+*)
+
+header {* Exception handling in the JVM *}
+
+theory JVMExceptions = JVMInstructions:
+
+constdefs
+  match_exception_entry :: "jvm_prog \<Rightarrow> cname \<Rightarrow> p_count \<Rightarrow> exception_entry \<Rightarrow> bool"
+  "match_exception_entry G cn pc ee == 
+                 let (start_pc, end_pc, handler_pc, catch_type) = ee in
+                 start_pc <= pc \<and> pc < end_pc \<and> G\<turnstile> cn \<preceq>C catch_type"
+
+
+consts
+  match_exception_table :: "jvm_prog \<Rightarrow> cname \<Rightarrow> p_count \<Rightarrow> exception_table
+                          \<Rightarrow> p_count option"
+primrec
+  "match_exception_table G cn pc []     = None"
+  "match_exception_table G cn pc (e#es) = (if match_exception_entry G cn pc e
+                                           then Some (fst (snd (snd e))) 
+                                           else match_exception_table G cn pc es)"
+
+
+consts
+  cname_of :: "aheap \<Rightarrow> val \<Rightarrow> cname"
+  ex_table_of :: "jvm_method \<Rightarrow> exception_table"
+
+translations
+  "cname_of hp v" == "fst (the (hp (the_Addr v)))"
+  "ex_table_of m" == "snd (snd (snd m))"
+
+
+consts
+  find_handler :: "jvm_prog \<Rightarrow> val option \<Rightarrow> aheap \<Rightarrow> frame list \<Rightarrow> jvm_state"
+primrec
+  "find_handler G xcpt hp [] = (xcpt, hp, [])"
+  "find_handler G xcpt hp (fr#frs) = 
+      (case xcpt of
+         None \<Rightarrow> (None, hp, fr#frs)
+       | Some xc \<Rightarrow> 
+       let (stk,loc,C,sig,pc) = fr in
+       (case match_exception_table G (cname_of hp xc) pc 
+              (ex_table_of (snd(snd(the(method (G,C) sig))))) of
+          None \<Rightarrow> find_handler G (Some xc) hp frs
+        | Some handler_pc \<Rightarrow> (None, hp, ([xc], loc, C, sig, handler_pc)#frs)))"
+
+
+
+lemma cname_of_xcp:
+  "raise_system_xcpt b x = Some xcp \<Longrightarrow> cname_of (hp::aheap) xcp = Xcpt x"
+proof -
+  assume "raise_system_xcpt b x = Some xcp"
+  hence "xcp = Addr (XcptRef x)"
+    by (simp add: raise_system_xcpt_def split: split_if_asm)
+  moreover
+  have "hp (XcptRef x) = Some (Xcpt x, empty)"
+    by (rule system_xcpt_allocated)
+  ultimately
+  show ?thesis by simp
+qed
+
+end

--- a/src/HOL/MicroJava/JVM/JVMExec.thy	Sun Dec 16 00:18:44 2001 +0100
+++ b/src/HOL/MicroJava/JVM/JVMExec.thy	Sun Dec 16 00:19:08 2001 +0100
@@ -1,39 +1,39 @@
 (*  Title:      HOL/MicroJava/JVM/JVMExec.thy
     ID:         $Id$
-    Author:     Cornelia Pusch
+    Author:     Cornelia Pusch, Gerwin Klein
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
 header {* Program Execution in the JVM *}
 
-theory JVMExec = JVMExecInstr :
+theory JVMExec = JVMExecInstr + JVMExceptions:
 
 
 consts
   exec :: "jvm_prog \<times> jvm_state => jvm_state option"
 
 
-(** exec is not recursive. recdef is just used for pattern matching **)
+-- "exec is not recursive. recdef is just used for pattern matching"
 recdef exec "{}"
   "exec (G, xp, hp, []) = None"
 
   "exec (G, None, hp, (stk,loc,C,sig,pc)#frs) =
   (let 
-     i = snd(snd(snd(snd(the(method (G,C) sig))))) ! pc
-   in
-     Some (exec_instr i G hp stk loc C sig pc frs))"
+     i = fst(snd(snd(snd(snd(the(method (G,C) sig)))))) ! pc;
+     (xcpt', hp', frs') = exec_instr i G hp stk loc C sig pc frs
+   in Some (find_handler G xcpt' hp' frs'))"
 
   "exec (G, Some xp, hp, frs) = None" 
 
 
 constdefs
-  exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool"  
+  exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool"
               ("_ |- _ -jvm-> _" [61,61,61]60)
   "G |- s -jvm-> t == (s,t) \<in> {(s,t). exec(G,s) = Some t}^*"
 
 
 syntax (xsymbols)
-  exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool"  
+  exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool"
               ("_ \<turnstile> _ -jvm-> _" [61,61,61]60)
 
 end

--- a/src/HOL/MicroJava/JVM/JVMExecInstr.thy	Sun Dec 16 00:18:44 2001 +0100
+++ b/src/HOL/MicroJava/JVM/JVMExecInstr.thy	Sun Dec 16 00:19:08 2001 +0100
@@ -25,57 +25,66 @@
       (None, hp, (v # stk, vars, Cl, sig, pc+1)#frs)"
 
  "exec_instr (New C) G hp stk vars Cl sig pc frs = 
-	(let (oref,xp')	= new_Addr hp;
-       fs		= init_vars (fields(G,C));
-	     hp'	= if xp'=None then hp(oref \<mapsto> (C,fs)) else hp;
-	     stk'	= if xp'=None then (Addr oref)#stk else stk
-	 in 
-      (xp', hp', (stk', vars, Cl, sig, pc+1)#frs))"	
+  (let (oref,xp') = new_Addr hp;
+       fs   = init_vars (fields(G,C));
+       hp'  = if xp'=None then hp(oref \<mapsto> (C,fs)) else hp;
+       stk' = if xp'=None then (Addr oref)#stk else stk;
+       pc'  = if xp'=None then pc+1 else pc
+   in 
+      (xp', hp', (stk', vars, Cl, sig, pc')#frs))"
 
  "exec_instr (Getfield F C) G hp stk vars Cl sig pc frs = 
-	(let oref	= hd stk;
-	     xp'	= raise_xcpt (oref=Null) NullPointer;
-	     (oc,fs)	= the(hp(the_Addr oref));
-	     stk'	= if xp'=None then the(fs(F,C))#(tl stk) else tl stk
-	 in
-      (xp', hp, (stk', vars, Cl, sig, pc+1)#frs))"
+  (let oref = hd stk;
+       xp'  = raise_system_xcpt (oref=Null) NullPointer;
+       (oc,fs)  = the(hp(the_Addr oref));
+       stk' = if xp'=None then the(fs(F,C))#(tl stk) else tl stk;
+       pc'  = if xp'=None then pc+1 else pc
+   in
+      (xp', hp, (stk', vars, Cl, sig, pc')#frs))"
 
  "exec_instr (Putfield F C) G hp stk vars Cl sig pc frs = 
-	(let (fval,oref)= (hd stk, hd(tl stk));
-	     xp'	= raise_xcpt (oref=Null) NullPointer;
-	     a		= the_Addr oref;
-	     (oc,fs)	= the(hp a);
-	     hp'	= if xp'=None then hp(a \<mapsto> (oc, fs((F,C) \<mapsto> fval))) else hp
-	 in
-      (xp', hp', (tl (tl stk), vars, Cl, sig, pc+1)#frs))"
+  (let (fval,oref)= (hd stk, hd(tl stk));
+       xp'  = raise_system_xcpt (oref=Null) NullPointer;
+       a    = the_Addr oref;
+       (oc,fs)  = the(hp a);
+       hp'  = if xp'=None then hp(a \<mapsto> (oc, fs((F,C) \<mapsto> fval))) else hp;
+       pc'  = if xp'=None then pc+1 else pc
+   in
+      (xp', hp', (tl (tl stk), vars, Cl, sig, pc')#frs))"
 
  "exec_instr (Checkcast C) G hp stk vars Cl sig pc frs =
-	(let oref	= hd stk;
-	     xp'	= raise_xcpt (\<not> cast_ok G C hp oref) ClassCast; 
-	     stk'	= if xp'=None then stk else tl stk
-	 in
-      (xp', hp, (stk', vars, Cl, sig, pc+1)#frs))"
+  (let oref = hd stk;
+       xp'  = raise_system_xcpt (\<not> cast_ok G C hp oref) ClassCast; 
+       stk' = if xp'=None then stk else tl stk;
+       pc'  = if xp'=None then pc+1 else pc
+   in
+      (xp', hp, (stk', vars, Cl, sig, pc')#frs))"
 
  "exec_instr (Invoke C mn ps) G hp stk vars Cl sig pc frs =
-	(let n		= length ps;
-	     argsoref	= take (n+1) stk;
-	     oref	= last argsoref;
-	     xp'	= raise_xcpt (oref=Null) NullPointer;
-	     dynT	= fst(the(hp(the_Addr oref)));
-	     (dc,mh,mxs,mxl,c)= the (method (G,dynT) (mn,ps));
-	     frs'	= if xp'=None then 
+  (let n    = length ps;
+       argsoref = take (n+1) stk;
+       oref = last argsoref;
+       xp'  = raise_system_xcpt (oref=Null) NullPointer;
+       dynT = fst(the(hp(the_Addr oref)));
+       (dc,mh,mxs,mxl,c)= the (method (G,dynT) (mn,ps));
+       frs' = if xp'=None then 
                 [([],rev argsoref@replicate mxl arbitrary,dc,(mn,ps),0)]
-	            else []
-	 in
-      (xp', hp, frs'@(drop (n+1) stk, vars, Cl, sig, pc+1)#frs))"
+              else []
+   in 
+      (xp', hp, frs'@(stk, vars, Cl, sig, pc)#frs))" 
+  -- "Because exception handling needs the pc of the Invoke instruction,"
+  -- "Invoke doesn't change stk and pc yet (@{text Return} does that)."
 
  "exec_instr Return G hp stk0 vars Cl sig0 pc frs =
-	(if frs=[] then 
+  (if frs=[] then 
      (None, hp, [])
    else 
-     let val = hd stk0; (stk,loc,C,sig,pc) = hd frs
-	 in 
-      (None, hp, (val#stk,loc,C,sig,pc)#tl frs))"
+     let val = hd stk0; (stk,loc,C,sig,pc) = hd frs;
+         (mn,pt) = sig0; n = length pt
+   in 
+      (None, hp, (val#(drop (n+1) stk),loc,C,sig,pc+1)#tl frs))"
+  -- "Return drops arguments from the caller's stack and increases"
+  -- "the program counter in the caller"
 
  "exec_instr Pop G hp stk vars Cl sig pc frs = 
       (None, hp, (tl stk, vars, Cl, sig, pc+1)#frs)"
@@ -93,9 +102,9 @@
        vars, Cl, sig, pc+1)#frs)"
 
  "exec_instr Swap G hp stk vars Cl sig pc frs =
-	(let (val1,val2) = (hd stk,hd (tl stk))
+  (let (val1,val2) = (hd stk,hd (tl stk))
    in
-	    (None, hp, (val2#val1#(tl (tl stk)), vars, Cl, sig, pc+1)#frs))"
+      (None, hp, (val2#val1#(tl (tl stk)), vars, Cl, sig, pc+1)#frs))"
 
  "exec_instr IAdd G hp stk vars Cl sig pc frs =
   (let (val1,val2) = (hd stk,hd (tl stk))
@@ -104,12 +113,18 @@
        vars, Cl, sig, pc+1)#frs))"
 
  "exec_instr (Ifcmpeq i) G hp stk vars Cl sig pc frs =
-	(let (val1,val2) = (hd stk, hd (tl stk));
+  (let (val1,val2) = (hd stk, hd (tl stk));
      pc' = if val1 = val2 then nat(int pc+i) else pc+1
-	 in
-	    (None, hp, (tl (tl stk), vars, Cl, sig, pc')#frs))"
+   in
+      (None, hp, (tl (tl stk), vars, Cl, sig, pc')#frs))"
 
  "exec_instr (Goto i) G hp stk vars Cl sig pc frs =
       (None, hp, (stk, vars, Cl, sig, nat(int pc+i))#frs)"
 
-end
+ "exec_instr Throw G hp stk vars Cl sig pc frs =
+  (let xcpt  = raise_system_xcpt (hd stk = Null) NullPointer;
+       xcpt' = if xcpt = None then Some (hd stk) else xcpt
+   in
+      (xcpt', hp, (stk, vars, Cl, sig, pc)#frs))"
+
+end
\ No newline at end of file

--- a/src/HOL/MicroJava/JVM/JVMInstructions.thy	Sun Dec 16 00:18:44 2001 +0100
+++ b/src/HOL/MicroJava/JVM/JVMInstructions.thy	Sun Dec 16 00:19:08 2001 +0100
@@ -11,27 +11,31 @@
 
 
 datatype 
-  instr = Load nat                  (* load from local variable *)
-        | Store nat                 (* store into local variable *)
-        | LitPush val               (* push a literal (constant) *)
-        | New cname                 (* create object *)
-        | Getfield vname cname	  	(* Fetch field from object *)
-        | Putfield vname cname		  (* Set field in object     *)
-        | Checkcast cname	          (* Check whether object is of given type *)
-        | Invoke cname mname "(ty list)"  (* inv. instance meth of an object *)
-        | Return                    (* return from method *)
-        | Pop                       (* pop top element from opstack *)
-        | Dup                       (* duplicate top element of opstack *)
-        | Dup_x1                    (* duplicate next to top element *)
-        | Dup_x2                    (* duplicate 3rd element *)
-        | Swap                      (* swap top and next to top element *)
-        | IAdd                      (* integer addition *)
-        | Goto int                  (* goto relative address *)
-        | Ifcmpeq int               (* Branch if int/ref comparison succeeds *)
-
+  instr = Load nat                  -- "load from local variable"
+        | Store nat                 -- "store into local variable"
+        | LitPush val               -- "push a literal (constant)"
+        | New cname                 -- "create object"
+        | Getfield vname cname      -- "Fetch field from object"
+        | Putfield vname cname      -- "Set field in object    "
+        | Checkcast cname           -- "Check whether object is of given type"
+        | Invoke cname mname "(ty list)"  -- "inv. instance meth of an object"
+        | Return                    -- "return from method"
+        | Pop                       -- "pop top element from opstack"
+        | Dup                       -- "duplicate top element of opstack"
+        | Dup_x1                    -- "duplicate next to top element"
+        | Dup_x2                    -- "duplicate 3rd element"
+        | Swap                      -- "swap top and next to top element"
+        | IAdd                      -- "integer addition"
+        | Goto int                  -- "goto relative address"
+        | Ifcmpeq int               -- "branch if int/ref comparison succeeds"
+        | Throw                     -- "throw top of stack as exception"
 
 types
   bytecode = "instr list"
-  jvm_prog = "(nat \<times> nat \<times> bytecode) prog" 
+  exception_entry = "p_count \<times> p_count \<times> p_count \<times> cname" 
+                  -- "start-pc, end-pc, handler-pc, exception type"
+  exception_table = "exception_entry list"
+  jvm_method = "nat \<times> nat \<times> bytecode \<times> exception_table"
+  jvm_prog = "jvm_method prog" 
 
 end

--- a/src/HOL/MicroJava/JVM/JVMState.thy	Sun Dec 16 00:18:44 2001 +0100
+++ b/src/HOL/MicroJava/JVM/JVMState.thy	Sun Dec 16 00:19:08 2001 +0100
@@ -1,43 +1,70 @@
 (*  Title:      HOL/MicroJava/JVM/JVMState.thy
     ID:         $Id$
-    Author:     Cornelia Pusch
+    Author:     Cornelia Pusch, Gerwin Klein
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-
 header {* State of the JVM *}
 
-
 theory JVMState = Conform:
 
-
-text {* frame stack :*}
+section {* Frame Stack *}
 types
- opstack 	 = "val list"
- locvars 	 = "val list" 
- p_count 	 = nat
+ opstack   = "val list"
+ locvars   = "val list" 
+ p_count   = nat
 
- frame = "opstack \<times>			
-          locvars \<times>		
-          cname \<times>			
-          sig \<times>			
+ frame = "opstack \<times>     
+          locvars \<times>   
+          cname \<times>     
+          sig \<times>     
           p_count"
 
-	(* operand stack *)
-	(* local variables *)
-	(* name of def. class defined *)
-	(* meth name+param_desc *)
-	(* program counter within frame *)
+  -- "operand stack" 
+  -- "local variables (including this pointer and method parameters)"
+  -- "name of class where current method is defined"
+  -- "method name + parameter types"
+  -- "program counter within frame"
+
+
+section {* Exceptions *}
+constdefs
+  raise_system_xcpt :: "bool \<Rightarrow> xcpt \<Rightarrow> val option"
+  "raise_system_xcpt b x == if b then Some (Addr (XcptRef x)) else None"
+
+  -- "redefines State.new\\_Addr:"
+  new_Addr :: "aheap => loc \<times> val option"
+  "new_Addr h == SOME (a,x). (h a = None \<and>  x = None) |
+                             x = raise_system_xcpt True OutOfMemory"
+
+
+section {* Runtime State *}
+types
+  jvm_state = "val option \<times> aheap \<times> frame list"  -- "exception flag, heap, frames"
 
 
-text {* exceptions: *}
-constdefs
-  raise_xcpt :: "bool => xcpt => xcpt option"
-  "raise_xcpt c x == (if c then Some x else None)"
-
+section {* Lemmas *}
 
-text {* runtime state: *}
-types
-  jvm_state = "xcpt option \<times> aheap \<times> frame list"	
+lemma new_AddrD:
+  "new_Addr hp = (ref, xcp) \<Longrightarrow> hp ref = None \<and> xcp = None \<or> xcp = Some (Addr (XcptRef OutOfMemory))"
+  apply (drule sym)
+  apply (unfold new_Addr_def)
+  apply (simp add: raise_system_xcpt_def)
+  apply (simp add: Pair_fst_snd_eq Eps_split)
+  apply (rule someI)
+  apply (rule disjI2)
+  apply (rule_tac "r" = "snd (?a,Some (Addr (XcptRef OutOfMemory)))" in trans)
+  apply auto
+  done
 
-end
+lemma new_Addr_OutOfMemory:
+  "snd (new_Addr hp) = Some xcp \<Longrightarrow> xcp = Addr (XcptRef OutOfMemory)"
+proof - 
+  obtain ref xp where "new_Addr hp = (ref, xp)" by (cases "new_Addr hp")
+  moreover
+  assume "snd (new_Addr hp) = Some xcp" 
+  ultimately
+  show ?thesis by (auto dest: new_AddrD)
+qed  
+
+end
\ No newline at end of file