# HG changeset patch # User kleing # Date 1008458348 -3600 # Node ID a955fe2879ba53579f62190f27a0a7d06a270e4e # Parent 521f2da133bedb938f307d7897ecf3df60f1dfcc exception merge + cleanup diff -r 521f2da133be -r a955fe2879ba src/HOL/MicroJava/JVM/JVMExceptions.thy --- /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 \ cname \ p_count \ exception_entry \ bool" + "match_exception_entry G cn pc ee == + let (start_pc, end_pc, handler_pc, catch_type) = ee in + start_pc <= pc \ pc < end_pc \ G\ cn \C catch_type" + + +consts + match_exception_table :: "jvm_prog \ cname \ p_count \ exception_table + \ 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 \ val \ cname" + ex_table_of :: "jvm_method \ 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 \ val option \ aheap \ frame list \ jvm_state" +primrec + "find_handler G xcpt hp [] = (xcpt, hp, [])" + "find_handler G xcpt hp (fr#frs) = + (case xcpt of + None \ (None, hp, fr#frs) + | Some xc \ + 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 \ find_handler G (Some xc) hp frs + | Some handler_pc \ (None, hp, ([xc], loc, C, sig, handler_pc)#frs)))" + + + +lemma cname_of_xcp: + "raise_system_xcpt b x = Some xcp \ 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 diff -r 521f2da133be -r a955fe2879ba src/HOL/MicroJava/JVM/JVMExec.thy --- 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 \ 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) \ {(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" ("_ \ _ -jvm-> _" [61,61,61]60) end diff -r 521f2da133be -r a955fe2879ba src/HOL/MicroJava/JVM/JVMExecInstr.thy --- 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 \ (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 \ (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 \ (oc, fs((F,C) \ 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 \ (oc, fs((F,C) \ 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 (\ 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 (\ 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 diff -r 521f2da133be -r a955fe2879ba src/HOL/MicroJava/JVM/JVMInstructions.thy --- 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 \ nat \ bytecode) prog" + exception_entry = "p_count \ p_count \ p_count \ cname" + -- "start-pc, end-pc, handler-pc, exception type" + exception_table = "exception_entry list" + jvm_method = "nat \ nat \ bytecode \ exception_table" + jvm_prog = "jvm_method prog" end diff -r 521f2da133be -r a955fe2879ba src/HOL/MicroJava/JVM/JVMState.thy --- 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 \ - locvars \ - cname \ - sig \ + frame = "opstack \ + locvars \ + cname \ + sig \ 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 \ xcpt \ val option" + "raise_system_xcpt b x == if b then Some (Addr (XcptRef x)) else None" + + -- "redefines State.new\\_Addr:" + new_Addr :: "aheap => loc \ val option" + "new_Addr h == SOME (a,x). (h a = None \ x = None) | + x = raise_system_xcpt True OutOfMemory" + + +section {* Runtime State *} +types + jvm_state = "val option \ aheap \ 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 \ aheap \ frame list" +lemma new_AddrD: + "new_Addr hp = (ref, xcp) \ hp ref = None \ xcp = None \ 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 \ 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