# HG changeset patch # User kleing # Date 1008458264 -3600 # Node ID d09d0f160888a7f65cbf0ead5843e750f20d8b74 # Parent 3fb416265ba978725b40a83288e4796abc8108a3 exceptions diff -r 3fb416265ba9 -r d09d0f160888 src/HOL/MicroJava/BV/BVSpec.thy --- a/src/HOL/MicroJava/BV/BVSpec.thy Sun Dec 16 00:17:18 2001 +0100 +++ b/src/HOL/MicroJava/BV/BVSpec.thy Sun Dec 16 00:17:44 2001 +0100 @@ -1,63 +1,60 @@ (* Title: HOL/MicroJava/BV/BVSpec.thy ID: $Id$ - Author: Cornelia Pusch + Author: Cornelia Pusch, Gerwin Klein Copyright 1999 Technische Universitaet Muenchen *) header "The Bytecode Verifier" -theory BVSpec = Step: +theory BVSpec = Effect: + +text {* + This theory contains a specification of the BV. The specification + describes correct typings of method bodies; it corresponds + to type \emph{checking}. +*} constdefs -wt_instr :: "[instr,jvm_prog,ty,method_type,nat,p_count,p_count] => bool" -"wt_instr i G rT phi mxs max_pc pc == - app i G mxs rT (phi!pc) \ - (\ pc' \ set (succs i pc). pc' < max_pc \ (G \ step i G (phi!pc) <=' phi!pc'))" + wt_instr :: "[instr,jvm_prog,ty,method_type,nat,p_count, + exception_table,p_count] => bool" + "wt_instr i G rT phi mxs max_pc et pc == + app i G mxs rT pc et (phi!pc) \ + (\(pc',s') \ set (eff i G pc et (phi!pc)). pc' < max_pc \ G \ s' <=' phi!pc')" -wt_start :: "[jvm_prog,cname,ty list,nat,method_type] => bool" -"wt_start G C pTs mxl phi == - G \ Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)) <=' phi!0" - + wt_start :: "[jvm_prog,cname,ty list,nat,method_type] => bool" + "wt_start G C pTs mxl phi == + G \ Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)) <=' phi!0" -wt_method :: "[jvm_prog,cname,ty list,ty,nat,nat,instr list,method_type] => bool" -"wt_method G C pTs rT mxs mxl ins phi == - let max_pc = length ins - in - 0 < max_pc \ wt_start G C pTs mxl phi \ - (\pc. pc wt_instr (ins ! pc) G rT phi mxs max_pc pc)" + wt_method :: "[jvm_prog,cname,ty list,ty,nat,nat,instr list, + exception_table,method_type] => bool" + "wt_method G C pTs rT mxs mxl ins et phi == + let max_pc = length ins in + 0 < max_pc \ wt_start G C pTs mxl phi \ + (\pc. pc wt_instr (ins ! pc) G rT phi mxs max_pc et pc)" -wt_jvm_prog :: "[jvm_prog,prog_type] => bool" -"wt_jvm_prog G phi == - wf_prog (\G C (sig,rT,(maxs,maxl,b)). - wt_method G C (snd sig) rT maxs maxl b (phi C sig)) G" - + wt_jvm_prog :: "[jvm_prog,prog_type] => bool" + "wt_jvm_prog G phi == + wf_prog (\G C (sig,rT,(maxs,maxl,b,et)). + wt_method G C (snd sig) rT maxs maxl b et (phi C sig)) G" lemma wt_jvm_progD: -"wt_jvm_prog G phi ==> (\wt. wf_prog wt G)" -by (unfold wt_jvm_prog_def, blast) + "wt_jvm_prog G phi ==> (\wt. wf_prog wt G)" + by (unfold wt_jvm_prog_def, blast) lemma wt_jvm_prog_impl_wt_instr: -"[| wt_jvm_prog G phi; is_class G C; - method (G,C) sig = Some (C,rT,maxs,maxl,ins); pc < length ins |] - ==> wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc"; -by (unfold wt_jvm_prog_def, drule method_wf_mdecl, - simp, simp, simp add: wf_mdecl_def wt_method_def) + "[| wt_jvm_prog G phi; is_class G C; + method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); pc < length ins |] + ==> wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc"; + by (unfold wt_jvm_prog_def, drule method_wf_mdecl, + simp, simp, simp add: wf_mdecl_def wt_method_def) lemma wt_jvm_prog_impl_wt_start: -"[| wt_jvm_prog G phi; is_class G C; - method (G,C) sig = Some (C,rT,maxs,maxl,ins) |] ==> - 0 < (length ins) \ wt_start G C (snd sig) maxl (phi C sig)" -by (unfold wt_jvm_prog_def, drule method_wf_mdecl, - simp, simp, simp add: wf_mdecl_def wt_method_def) - -text {* for most instructions wt\_instr collapses: *} -lemma -"succs i pc = [pc+1] ==> wt_instr i G rT phi mxs max_pc pc = - (app i G mxs rT (phi!pc) \ pc+1 < max_pc \ (G \ step i G (phi!pc) <=' phi!(pc+1)))" -by (simp add: wt_instr_def) + "[| wt_jvm_prog G phi; is_class G C; + method (G,C) sig = Some (C,rT,maxs,maxl,ins,et) |] ==> + 0 < (length ins) \ wt_start G C (snd sig) maxl (phi C sig)" + by (unfold wt_jvm_prog_def, drule method_wf_mdecl, + simp, simp, simp add: wf_mdecl_def wt_method_def) end - - diff -r 3fb416265ba9 -r d09d0f160888 src/HOL/MicroJava/BV/BVSpecTypeSafe.thy --- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Sun Dec 16 00:17:18 2001 +0100 +++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Sun Dec 16 00:17:44 2001 +0100 @@ -1,42 +1,594 @@ (* Title: HOL/MicroJava/BV/BVSpecTypeSafe.thy ID: $Id$ - Author: Cornelia Pusch + Author: Cornelia Pusch, Gerwin Klein Copyright 1999 Technische Universitaet Muenchen -Proof that the specification of the bytecode verifier only admits type safe -programs. *) header "BV Type Safety Proof" theory BVSpecTypeSafe = Correct: +text {* + This theory contains proof that the specification of the bytecode + verifier only admits type safe programs. +*} + +section {* Preliminaries *} + +text {* + Simp and intro setup for the type safety proof: +*} lemmas defs1 = sup_state_conv correct_state_def correct_frame_def - wt_instr_def step_def + wt_instr_def eff_def norm_eff_def lemmas widen_rules[intro] = approx_val_widen approx_loc_widen approx_stk_widen lemmas [simp del] = split_paired_All + +text {* + If we have a welltyped program and a conforming state, we + can directly infer that the current instruction is well typed: +*} lemma wt_jvm_prog_impl_wt_instr_cor: - "[| wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxs,maxl,ins); + "[| wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ |] - ==> wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc" + ==> wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc" apply (unfold correct_state_def Let_def correct_frame_def) apply simp apply (blast intro: wt_jvm_prog_impl_wt_instr) done + +section {* Exception Handling *} + +text {* + Exceptions don't touch anything except the stack: +*} +lemma exec_instr_xcpt: + "(fst (exec_instr i G hp stk vars Cl sig pc frs) = Some xcp) + = (\stk'. exec_instr i G hp stk vars Cl sig pc frs = + (Some xcp, hp, (stk', vars, Cl, sig, pc)#frs))" + by (cases i, auto simp add: split_beta split: split_if_asm) + + +text {* + Relates @{text match_any} from the Bytecode Verifier with + @{text match_exception_table} from the operational semantics: +*} +lemma in_match_any: + "match_exception_table G xcpt pc et = Some pc' ==> + \C. C \ set (match_any G pc et) \ G \ xcpt \C C \ + match_exception_table G C pc et = Some pc'" + (is "PROP ?P et" is "?match et ==> ?match_any et") +proof (induct et) + show "PROP ?P []" + by simp + + fix e es + assume IH: "PROP ?P es" + assume match: "?match (e#es)" + + obtain start_pc end_pc handler_pc catch_type where + e [simp]: "e = (start_pc, end_pc, handler_pc, catch_type)" + by (cases e) + + from IH match + show "?match_any (e#es)" + proof (cases "match_exception_entry G xcpt pc e") + case False + with match + have "match_exception_table G xcpt pc es = Some pc'" by simp + with IH + obtain C where + set: "C \ set (match_any G pc es)" and + C: "G \ xcpt \C C" and + m: "match_exception_table G C pc es = Some pc'" by blast + + from set + have "C \ set (match_any G pc (e#es))" by simp + moreover + from False C + have "\ match_exception_entry G C pc e" + by - (erule contrapos_nn, + auto simp add: match_exception_entry_def elim: rtrancl_trans) + with m + have "match_exception_table G C pc (e#es) = Some pc'" by simp + moreover note C + ultimately + show ?thesis by blast + next + case True with match + have "match_exception_entry G catch_type pc e" + by (simp add: match_exception_entry_def) + moreover + from True match + obtain + "start_pc \ pc" + "pc < end_pc" + "G \ xcpt \C catch_type" + "handler_pc = pc'" + by (simp add: match_exception_entry_def) + ultimately + show ?thesis by auto + qed +qed + +text {* + We can prove separately that the recursive search for exception + handlers (@{text find_handler}) in the frame stack results in + a conforming state (if there was no matching exception handler + in the current frame). We require that the exception is a valid + heap address, and that the state before the exception occured + conforms. +*} +lemma uncaught_xcpt_correct: + "!!f. [| wt_jvm_prog G phi; xcp = Addr adr; hp adr = Some T; + G,phi \JVM (None, hp, f#frs)\ |] + ==> G,phi \JVM (find_handler G (Some xcp) hp frs)\" + (is "!!f. [| ?wt; ?adr; ?hp; ?correct (None, hp, f#frs) |] ==> ?correct (?find frs)") +proof (induct frs) + -- "the base case is trivial, as it should be" + show "?correct (?find [])" by (simp add: correct_state_def) + + -- "we will need both forms @{text wt_jvm_prog} and @{text wf_prog} later" + assume wt: ?wt + then obtain mb where wf: "wf_prog mb G" by (simp add: wt_jvm_prog_def) + + -- "these two don't change in the induction:" + assume adr: ?adr + assume hp: ?hp + + -- "the assumption for the cons case:" + fix f f' frs' + assume cr: "?correct (None, hp, f#f'#frs')" + + -- "the induction hypothesis as produced by Isabelle, immediatly simplified + with the fixed assumptions above" + assume "\f. [| ?wt; ?adr; ?hp; ?correct (None, hp, f#frs') |] ==> ?correct (?find frs')" + with wt adr hp + have IH: "\f. ?correct (None, hp, f#frs') ==> ?correct (?find frs')" by blast + + from cr + have cr': "?correct (None, hp, f'#frs')" by (auto simp add: correct_state_def) + + obtain stk loc C sig pc where f' [simp]: "f' = (stk,loc,C,sig,pc)" + by (cases f') + + from cr + obtain rT maxs maxl ins et where + meth: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)" + by (simp add: correct_state_def, blast) + + hence [simp]: "ex_table_of (snd (snd (the (method (G, C) sig)))) = et" + by simp + + show "?correct (?find (f'#frs'))" + proof (cases "match_exception_table G (cname_of hp xcp) pc et") + case None + with cr' IH + show ?thesis by simp + next + fix handler_pc + assume match: "match_exception_table G (cname_of hp xcp) pc et = Some handler_pc" + (is "?match (cname_of hp xcp) = _") + + from wt meth cr' [simplified] + have wti: "wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc" + by (rule wt_jvm_prog_impl_wt_instr_cor) + + from cr meth + obtain C' mn pts ST LT where + ins: "ins!pc = Invoke C' mn pts" (is "_ = ?i") and + phi: "phi C sig ! pc = Some (ST, LT)" + by (simp add: correct_state_def) blast + + from match + obtain D where + in_any: "D \ set (match_any G pc et)" and + D: "G \ cname_of hp xcp \C D" and + match': "?match D = Some handler_pc" + by (blast dest: in_match_any) + + from ins wti phi have + "\D\set (match_any G pc et). the (?match D) < length ins \ + G \ Some ([Class D], LT) <=' phi C sig!the (?match D)" + by (simp add: wt_instr_def eff_def xcpt_eff_def) + with in_any match' obtain + pc: "handler_pc < length ins" + "G \ Some ([Class D], LT) <=' phi C sig ! handler_pc" + by auto + then obtain ST' LT' where + phi': "phi C sig ! handler_pc = Some (ST',LT')" and + less: "G \ ([Class D], LT) <=s (ST',LT')" + by auto + + from cr' phi meth f' + have "correct_frame G hp (ST, LT) maxl ins f'" + by (unfold correct_state_def) auto + then obtain + len: "length loc = 1+length (snd sig)+maxl" and + loc: "approx_loc G hp loc LT" + by (unfold correct_frame_def) auto + + let ?f = "([xcp], loc, C, sig, handler_pc)" + have "correct_frame G hp (ST', LT') maxl ins ?f" + proof - + from wf less loc + have "approx_loc G hp loc LT'" by (simp add: sup_state_conv) blast + moreover + from D adr hp + have "G,hp \ xcp ::\ Class D" by (simp add: conf_def obj_ty_def) + with wf less loc + have "approx_stk G hp [xcp] ST'" + by (auto simp add: sup_state_conv approx_stk_def approx_val_def + elim: conf_widen split: Err.split) + moreover + note len pc + ultimately + show ?thesis by (simp add: correct_frame_def) + qed + + with cr' match phi' meth + show ?thesis by (unfold correct_state_def) auto + qed +qed + + +text {* + The requirement of lemma @{text uncaught_xcpt_correct} (that + the exception is a valid reference on the heap) is always met + for welltyped instructions and conformant states: +*} +lemma exec_instr_xcpt_hp: + "[| fst (exec_instr (ins!pc) G hp stk vars Cl sig pc frs) = Some xcp; + wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; + G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ |] + ==> \adr T. xcp = Addr adr \ hp adr = Some T" + (is "[| ?xcpt; ?wt; ?correct |] ==> ?thesis") +proof - + note [simp] = system_xcpt_allocated split_beta raise_system_xcpt_def + note [split] = split_if_asm option.split_asm + + assume wt: ?wt ?correct + + assume xcpt: ?xcpt + thus ?thesis + proof (cases "ins!pc") + case New with xcpt + show ?thesis by (auto dest: new_Addr_OutOfMemory) + next + case Throw with xcpt wt + show ?thesis + by (auto simp add: wt_instr_def correct_state_def correct_frame_def + dest: non_npD) + qed auto +qed + + +text {* + Finally we can state that, whenever an exception occurs, the + resulting next state always conforms: +*} +lemma xcpt_correct: + "[| wt_jvm_prog G phi; + method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); + wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; + fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = Some xcp; + Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); + G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ |] + ==> G,phi \JVM state'\" +proof - + assume wtp: "wt_jvm_prog G phi" + assume meth: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)" + assume wt: "wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc" + assume xp: "fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = Some xcp" + assume s': "Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs)" + assume correct: "G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\" + + from wtp obtain wfmb where wf: "wf_prog wfmb G" by (simp add: wt_jvm_prog_def) + + note xp' = meth s' xp + + note wtp + moreover + from xp wt correct + obtain adr T where + adr: "xcp = Addr adr" "hp adr = Some T" + by (blast dest: exec_instr_xcpt_hp) + moreover + note correct + ultimately + have "G,phi \JVM find_handler G (Some xcp) hp frs \" by (rule uncaught_xcpt_correct) + with xp' + have "match_exception_table G (cname_of hp xcp) pc et = None \ ?thesis" + (is "?m (cname_of hp xcp) = _ \ _" is "?match = _ \ _") + by (clarsimp simp add: exec_instr_xcpt split_beta) + moreover + { fix handler + assume some_handler: "?match = Some handler" + + from correct meth + obtain ST LT where + hp_ok: "G \h hp \" and + class: "is_class G C" and + phi_pc: "phi C sig ! pc = Some (ST, LT)" and + frame: "correct_frame G hp (ST, LT) maxl ins (stk, loc, C, sig, pc)" and + frames: "correct_frames G hp phi rT sig frs" + by (unfold correct_state_def) auto + + from frame obtain + stk: "approx_stk G hp stk ST" and + loc: "approx_loc G hp loc LT" and + pc: "pc < length ins" and + len: "length loc = 1+length (snd sig)+maxl" + by (unfold correct_frame_def) auto + + from wt obtain + eff: "\(pc', s')\set (xcpt_eff (ins!pc) G pc (phi C sig!pc) et). + pc' < length ins \ G \ s' <=' phi C sig!pc'" + by (simp add: wt_instr_def eff_def) + + from some_handler xp' + have state': + "state' = (None, hp, ([xcp], loc, C, sig, handler)#frs)" + by (cases "ins!pc", auto simp add: raise_system_xcpt_def split_beta + split: split_if_asm) (* takes long! *) + + let ?f' = "([xcp], loc, C, sig, handler)" + from eff + obtain ST' LT' where + phi_pc': "phi C sig ! handler = Some (ST', LT')" and + frame': "correct_frame G hp (ST',LT') maxl ins ?f'" + proof (cases "ins!pc") + case Return -- "can't generate exceptions:" + with xp' have False by (simp add: split_beta split: split_if_asm) + thus ?thesis .. + next + case New + with some_handler xp' + have xcp: "xcp = Addr (XcptRef OutOfMemory)" + by (simp add: raise_system_xcpt_def split_beta new_Addr_OutOfMemory) + hence "cname_of hp xcp = Xcpt OutOfMemory" + by (simp add: system_xcpt_allocated) + with New some_handler phi_pc eff + obtain ST' LT' where + phi': "phi C sig ! handler = Some (ST', LT')" and + less: "G \ ([Class (Xcpt OutOfMemory)], LT) <=s (ST', LT')" and + pc': "handler < length ins" + by (simp add: xcpt_eff_def) blast + note phi' + moreover + { from xcp + have "G,hp \ xcp ::\ Class (Xcpt OutOfMemory)" + by (simp add: conf_def obj_ty_def system_xcpt_allocated) + moreover + from wf less loc + have "approx_loc G hp loc LT'" + by (simp add: sup_state_conv) blast + moreover + note wf less pc' len + ultimately + have "correct_frame G hp (ST',LT') maxl ins ?f'" + by (unfold correct_frame_def) (auto simp add: sup_state_conv + approx_stk_def approx_val_def split: err.split elim: conf_widen) + } + ultimately + show ?thesis by (rule that) + next + case Getfield + with some_handler xp' + have xcp: "xcp = Addr (XcptRef NullPointer)" + by (simp add: raise_system_xcpt_def split_beta split: split_if_asm) + hence "cname_of hp xcp = Xcpt NullPointer" + by (simp add: system_xcpt_allocated) + with Getfield some_handler phi_pc eff + obtain ST' LT' where + phi': "phi C sig ! handler = Some (ST', LT')" and + less: "G \ ([Class (Xcpt NullPointer)], LT) <=s (ST', LT')" and + pc': "handler < length ins" + by (simp add: xcpt_eff_def) blast + note phi' + moreover + { from xcp + have "G,hp \ xcp ::\ Class (Xcpt NullPointer)" + by (simp add: conf_def obj_ty_def system_xcpt_allocated) + moreover + from wf less loc + have "approx_loc G hp loc LT'" + by (simp add: sup_state_conv) blast + moreover + note wf less pc' len + ultimately + have "correct_frame G hp (ST',LT') maxl ins ?f'" + by (unfold correct_frame_def) (auto simp add: sup_state_conv + approx_stk_def approx_val_def split: err.split elim: conf_widen) + } + ultimately + show ?thesis by (rule that) + next + case Putfield + with some_handler xp' + have xcp: "xcp = Addr (XcptRef NullPointer)" + by (simp add: raise_system_xcpt_def split_beta split: split_if_asm) + hence "cname_of hp xcp = Xcpt NullPointer" + by (simp add: system_xcpt_allocated) + with Putfield some_handler phi_pc eff + obtain ST' LT' where + phi': "phi C sig ! handler = Some (ST', LT')" and + less: "G \ ([Class (Xcpt NullPointer)], LT) <=s (ST', LT')" and + pc': "handler < length ins" + by (simp add: xcpt_eff_def) blast + note phi' + moreover + { from xcp + have "G,hp \ xcp ::\ Class (Xcpt NullPointer)" + by (simp add: conf_def obj_ty_def system_xcpt_allocated) + moreover + from wf less loc + have "approx_loc G hp loc LT'" + by (simp add: sup_state_conv) blast + moreover + note wf less pc' len + ultimately + have "correct_frame G hp (ST',LT') maxl ins ?f'" + by (unfold correct_frame_def) (auto simp add: sup_state_conv + approx_stk_def approx_val_def split: err.split elim: conf_widen) + } + ultimately + show ?thesis by (rule that) + next + case Checkcast + with some_handler xp' + have xcp: "xcp = Addr (XcptRef ClassCast)" + by (simp add: raise_system_xcpt_def split_beta split: split_if_asm) + hence "cname_of hp xcp = Xcpt ClassCast" + by (simp add: system_xcpt_allocated) + with Checkcast some_handler phi_pc eff + obtain ST' LT' where + phi': "phi C sig ! handler = Some (ST', LT')" and + less: "G \ ([Class (Xcpt ClassCast)], LT) <=s (ST', LT')" and + pc': "handler < length ins" + by (simp add: xcpt_eff_def) blast + note phi' + moreover + { from xcp + have "G,hp \ xcp ::\ Class (Xcpt ClassCast)" + by (simp add: conf_def obj_ty_def system_xcpt_allocated) + moreover + from wf less loc + have "approx_loc G hp loc LT'" + by (simp add: sup_state_conv) blast + moreover + note wf less pc' len + ultimately + have "correct_frame G hp (ST',LT') maxl ins ?f'" + by (unfold correct_frame_def) (auto simp add: sup_state_conv + approx_stk_def approx_val_def split: err.split elim: conf_widen) + } + ultimately + show ?thesis by (rule that) + next + case Invoke + with phi_pc eff + have + "\D\set (match_any G pc et). + the (?m D) < length ins \ G \ Some ([Class D], LT) <=' phi C sig!the (?m D)" + by (simp add: xcpt_eff_def) + moreover + from some_handler + obtain D where + "D \ set (match_any G pc et)" and + D: "G \ cname_of hp xcp \C D" and + "?m D = Some handler" + by (blast dest: in_match_any) + ultimately + obtain + pc': "handler < length ins" and + "G \ Some ([Class D], LT) <=' phi C sig ! handler" + by auto + then + obtain ST' LT' where + phi': "phi C sig ! handler = Some (ST', LT')" and + less: "G \ ([Class D], LT) <=s (ST', LT')" + by auto + from xp wt correct + obtain addr T where + xcp: "xcp = Addr addr" "hp addr = Some T" + by (blast dest: exec_instr_xcpt_hp) + note phi' + moreover + { from xcp D + have "G,hp \ xcp ::\ Class D" + by (simp add: conf_def obj_ty_def) + moreover + from wf less loc + have "approx_loc G hp loc LT'" + by (simp add: sup_state_conv) blast + moreover + note wf less pc' len + ultimately + have "correct_frame G hp (ST',LT') maxl ins ?f'" + by (unfold correct_frame_def) (auto simp add: sup_state_conv + approx_stk_def approx_val_def split: err.split elim: conf_widen) + } + ultimately + show ?thesis by (rule that) + next + case Throw + with phi_pc eff + have + "\D\set (match_any G pc et). + the (?m D) < length ins \ G \ Some ([Class D], LT) <=' phi C sig!the (?m D)" + by (simp add: xcpt_eff_def) + moreover + from some_handler + obtain D where + "D \ set (match_any G pc et)" and + D: "G \ cname_of hp xcp \C D" and + "?m D = Some handler" + by (blast dest: in_match_any) + ultimately + obtain + pc': "handler < length ins" and + "G \ Some ([Class D], LT) <=' phi C sig ! handler" + by auto + then + obtain ST' LT' where + phi': "phi C sig ! handler = Some (ST', LT')" and + less: "G \ ([Class D], LT) <=s (ST', LT')" + by auto + from xp wt correct + obtain addr T where + xcp: "xcp = Addr addr" "hp addr = Some T" + by (blast dest: exec_instr_xcpt_hp) + note phi' + moreover + { from xcp D + have "G,hp \ xcp ::\ Class D" + by (simp add: conf_def obj_ty_def) + moreover + from wf less loc + have "approx_loc G hp loc LT'" + by (simp add: sup_state_conv) blast + moreover + note wf less pc' len + ultimately + have "correct_frame G hp (ST',LT') maxl ins ?f'" + by (unfold correct_frame_def) (auto simp add: sup_state_conv + approx_stk_def approx_val_def split: err.split elim: conf_widen) + } + ultimately + show ?thesis by (rule that) + qed (insert xp', auto) -- "the other instructions don't generate exceptions" + + from state' meth hp_ok class frames phi_pc' frame' + have ?thesis by (unfold correct_state_def) simp + } + ultimately + show ?thesis by (cases "?match") blast+ +qed + + + section {* Single Instructions *} +text {* + In this section we look at each single (welltyped) instruction, and + prove that the state after execution of the instruction still conforms. + Since we have already handled exceptions above, we can now assume, that + on exception occurs for this (single step) execution. +*} + lemmas [iff] = not_Err_eq lemma Load_correct: "[| wf_prog wt G; - method (G,C) sig = Some (C,rT,maxs,maxl,ins); + method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); ins!pc = Load idx; - wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; + wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); - G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ |] + G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ |] ==> G,phi \JVM state'\" apply (clarsimp simp add: defs1 map_eq_Cons) apply (blast intro: approx_loc_imp_approx_val_sup) @@ -44,9 +596,9 @@ lemma Store_correct: "[| wf_prog wt G; - method (G,C) sig = Some (C,rT,maxs,maxl,ins); + method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); ins!pc = Store idx; - wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; + wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ |] ==> G,phi \JVM state'\" @@ -57,9 +609,9 @@ lemma LitPush_correct: "[| wf_prog wt G; - method (G,C) sig = Some (C,rT,maxs,maxl,ins); + method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); ins!pc = LitPush v; - wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; + wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ |] ==> G,phi \JVM state'\" @@ -81,30 +633,33 @@ apply (auto intro: rtrancl_trans) done +lemmas defs1 = defs1 raise_system_xcpt_def lemma Checkcast_correct: -"[| wf_prog wt G; - method (G,C) sig = Some (C,rT,maxs,maxl,ins); +"[| wt_jvm_prog G phi; + method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); ins!pc = Checkcast D; - wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; + wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; - G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ |] + G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\; + fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None |] ==> G,phi \JVM state'\" -apply (clarsimp simp add: defs1 map_eq_Cons raise_xcpt_def) +apply (clarsimp simp add: defs1 wt_jvm_prog_def map_eq_Cons split: split_if_asm) apply (blast intro: Cast_conf2) done lemma Getfield_correct: -"[| wf_prog wt G; - method (G,C) sig = Some (C,rT,maxs,maxl,ins); +"[| wt_jvm_prog G phi; + method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); ins!pc = Getfield F D; - wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; + wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; - G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ |] + G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\; + fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None |] ==> G,phi \JVM state'\" -apply (clarsimp simp add: defs1 raise_xcpt_def map_eq_Cons - split: option.split) +apply (clarsimp simp add: defs1 map_eq_Cons wt_jvm_prog_def + split: option.split split_if_asm) apply (frule conf_widen) apply assumption+ apply (drule conf_RefTD) @@ -112,19 +667,30 @@ apply (rule conjI) apply (drule widen_cfs_fields) apply assumption+ - apply (force intro: conf_widen simp add: hconf_def oconf_def lconf_def) + apply (erule conf_widen) + prefer 2 + apply assumption + apply (simp add: hconf_def oconf_def lconf_def) + apply (elim allE) + apply (erule impE, assumption) + apply simp + apply (elim allE) + apply (erule impE, assumption) + apply clarsimp apply blast done + lemma Putfield_correct: "[| wf_prog wt G; - method (G,C) sig = Some (C,rT,maxs,maxl,ins); + method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); ins!pc = Putfield F D; - wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; + wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; - G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ |] + G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\; + fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None |] ==> G,phi \JVM state'\" -apply (clarsimp simp add: defs1 raise_xcpt_def split: option.split List.split) +apply (clarsimp simp add: defs1 split_beta split: option.split List.split split_if_asm) apply (frule conf_widen) prefer 2 apply assumption @@ -140,22 +706,25 @@ dest: widen_cfs_fields) done + lemma New_correct: "[| wf_prog wt G; - method (G,C) sig = Some (C,rT,maxs,maxl,ins); + method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); ins!pc = New X; - wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; + wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; - G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ |] + G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\; + fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None |] ==> G,phi \JVM state'\" proof - assume wf: "wf_prog wt G" - assume meth: "method (G,C) sig = Some (C,rT,maxs,maxl,ins)" + assume meth: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)" assume ins: "ins!pc = New X" - assume wt: "wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc" + assume wt: "wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc" assume exec: "Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs)" assume conf: "G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\" + assume no_x: "fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None" from ins conf meth obtain ST LT where @@ -169,75 +738,68 @@ from phi_pc ins wt obtain ST' LT' where is_class_X: "is_class G X" and + maxs: "length ST < maxs" and suc_pc: "Suc pc < length ins" and phi_suc: "phi C sig ! Suc pc = Some (ST', LT')" and less: "G \ (Class X # ST, LT) <=s (ST', LT')" - by (unfold wt_instr_def step_def) auto + by (unfold wt_instr_def eff_def norm_eff_def) auto obtain oref xp' where - new_Addr: "(oref,xp') = new_Addr hp" - by (cases "new_Addr hp") auto - hence cases: - "hp oref = None \ xp' = None \ xp' = Some OutOfMemory" - by (blast dest: new_AddrD) + new_Addr: "new_Addr hp = (oref,xp')" + by (cases "new_Addr hp") + with ins no_x + obtain hp: "hp oref = None" and "xp' = None" + by (auto dest: new_AddrD simp add: raise_system_xcpt_def) + + with exec ins meth new_Addr + have state': + "state' = Norm (hp(oref\(X, init_vars (fields (G, X)))), + (Addr oref # stk, loc, C, sig, Suc pc) # frs)" + (is "state' = Norm (?hp', ?f # frs)") + by simp moreover - { assume "xp' = Some OutOfMemory" - with exec ins meth new_Addr [symmetric] - have "state' = (Some OutOfMemory, hp, (stk,loc,C,sig,Suc pc)#frs)" by simp - hence ?thesis by (simp add: correct_state_def) - } + from wf hp heap_ok is_class_X + have hp': "G \h ?hp' \" + by - (rule hconf_newref, auto simp add: oconf_def dest: fields_is_type) moreover - { assume hp: "hp oref = None" and "xp' = None" - with exec ins meth new_Addr [symmetric] - have state': - "state' = Norm (hp(oref\(X, init_vars (fields (G, X)))), - (Addr oref # stk, loc, C, sig, Suc pc) # frs)" - (is "state' = Norm (?hp', ?f # frs)") - by simp - moreover - from wf hp heap_ok is_class_X - have hp': "G \h ?hp' \" - by - (rule hconf_newref, - auto simp add: oconf_def dest: fields_is_type) - moreover - from hp - have sup: "hp \| ?hp'" by (rule hext_new) - from hp frame less suc_pc wf - have "correct_frame G ?hp' (ST', LT') maxl ins ?f" - apply (unfold correct_frame_def sup_state_conv) - apply (clarsimp simp add: map_eq_Cons conf_def fun_upd_apply approx_val_def) - apply (blast intro: approx_stk_sup_heap approx_loc_sup_heap sup) - done - moreover - from hp frames wf heap_ok is_class_X - have "correct_frames G ?hp' phi rT sig frs" - by - (rule correct_frames_newref, - auto simp add: oconf_def dest: fields_is_type) - ultimately - have ?thesis - by (simp add: is_class_C meth phi_suc correct_state_def del: not_None_eq) - } + from hp + have sup: "hp \| ?hp'" by (rule hext_new) + from hp frame less suc_pc wf + have "correct_frame G ?hp' (ST', LT') maxl ins ?f" + apply (unfold correct_frame_def sup_state_conv) + apply (clarsimp simp add: map_eq_Cons conf_def fun_upd_apply approx_val_def) + apply (blast intro: approx_stk_sup_heap approx_loc_sup_heap sup) + done + moreover + from hp frames wf heap_ok is_class_X + have "correct_frames G ?hp' phi rT sig frs" + by - (rule correct_frames_newref, + auto simp add: oconf_def dest: fields_is_type) ultimately - show ?thesis by auto + show ?thesis + by (simp add: is_class_C meth phi_suc correct_state_def del: not_None_eq) qed lemmas [simp del] = split_paired_Ex + lemma Invoke_correct: "[| wt_jvm_prog G phi; - method (G,C) sig = Some (C,rT,maxs,maxl,ins); + method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); ins ! pc = Invoke C' mn pTs; - wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; + wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; - G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ |] + G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\; + fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None |] ==> G,phi \JVM state'\" proof - assume wtprog: "wt_jvm_prog G phi" - assume method: "method (G,C) sig = Some (C,rT,maxs,maxl,ins)" + assume method: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)" assume ins: "ins ! pc = Invoke C' mn pTs" - assume wti: "wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc" + assume wti: "wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc" assume state': "Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs)" assume approx: "G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\" + assume no_xcp: "fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None" from wtprog obtain wfmb where @@ -262,18 +824,19 @@ w: "\x\set (zip apTs pTs). x \ widen G" and mC':"method (G, C') (mn, pTs) = Some (D', rT, body)" and pc: "Suc pc < length ins" and - step: "G \ step (Invoke C' mn pTs) G (Some s) <=' phi C sig!Suc pc" - by (simp add: wt_instr_def del: not_None_eq) (elim exE conjE, rule that) + eff: "G \ norm_eff (Invoke C' mn pTs) G (Some s) <=' phi C sig!Suc pc" + by (simp add: wt_instr_def eff_def del: not_None_eq) + (elim exE conjE, rule that) - from step + from eff obtain ST' LT' where s': "phi C sig ! Suc pc = Some (ST', LT')" - by (auto simp add: step_def split_paired_Ex) + by (simp add: norm_eff_def split_paired_Ex) blast - from X + from X obtain T where X_Ref: "X = RefT T" - by (blast dest: widen_RefT2) + by - (drule widen_RefT2, erule exE, rule that) from s ins frame obtain @@ -289,194 +852,245 @@ a_stk': "approx_stk G hp stk' ST" and stk': "stk = opTs @ oX # stk'" and l_o: "length opTs = length apTs" - "length stk' = length ST" - by (auto dest: approx_stk_append) + "length stk' = length ST" + by - (drule approx_stk_append, auto) - from oX - have "\T'. typeof (option_map obj_ty \ hp) oX = Some T' \ G \ T' \ X" - by (clarsimp simp add: approx_val_def conf_def) - - with X_Ref - obtain T' where - oX_Ref: "typeof (option_map obj_ty \ hp) oX = Some (RefT T')" - "G \ RefT T' \ X" - by (auto dest: widen_RefT2) + from oX X_Ref + have oX_conf: "G,hp \ oX ::\ RefT T" + by (simp add: approx_val_def) from stk' l_o l have oX_pos: "last (take (Suc (length pTs)) stk) = oX" by simp - with state' method ins - have Null_ok: "oX = Null ==> ?thesis" - by (simp add: correct_state_def raise_xcpt_def) - - { fix ref assume oX_Addr: "oX = Addr ref" - - with oX_Ref - obtain obj where - loc: "hp ref = Some obj" "obj_ty obj = RefT T'" - by auto - - then - obtain D where - obj_ty: "obj_ty obj = Class D" - by (auto simp add: obj_ty_def) - - with X_Ref oX_Ref loc - obtain D: "G \ Class D \ X" - by simp - - with X_Ref - obtain X' where - X': "X = Class X'" - by (blast dest: widen_Class) - - with X - have X'_subcls: "G \ X' \C C'" - by simp - - with mC' wfprog - obtain D0 rT0 maxs0 maxl0 ins0 where - mX: "method (G, X') (mn, pTs) = Some (D0, rT0, maxs0, maxl0, ins0)" "G\rT0\rT" - by (fast dest: subtype_widen_methd) + with state' method ins no_xcp oX_conf + obtain ref where oX_Addr: "oX = Addr ref" + by (auto simp add: raise_system_xcpt_def dest: conf_RefTD) - from X' D - have D_subcls: "G \ D \C X'" - by simp - - with wfprog mX - obtain D'' rT' mxs' mxl' ins' where - mD: "method (G, D) (mn, pTs) = Some (D'', rT', mxs', mxl', ins')" - "G \ rT' \ rT0" - by (fast dest: subtype_widen_methd) - - from mX mD - have rT': "G \ rT' \ rT" - by - (rule widen_trans) - - from is_class X'_subcls D_subcls - have is_class_D: "is_class G D" - by (auto dest: subcls_is_class2) + with oX_conf X_Ref + obtain obj D where + loc: "hp ref = Some obj" and + obj_ty: "obj_ty obj = Class D" and + D: "G \ Class D \ X" + by (auto simp add: conf_def) blast + + with X_Ref obtain X' where X': "X = Class X'" + by (blast dest: widen_Class) + + with X have X'_subcls: "G \ X' \C C'" by simp - with mD wfprog - obtain mD'': - "method (G, D'') (mn, pTs) = Some (D'', rT', mxs', mxl', ins')" - "is_class G D''" - by (auto dest: method_in_md) - - from loc obj_ty - have "fst (the (hp ref)) = D" - by (simp add: obj_ty_def) - - with oX_Addr oX_pos state' method ins stk' l_o l loc obj_ty mD - have state'_val: - "state' = - Norm (hp, ([], Addr ref # rev opTs @ replicate mxl' arbitrary, - D'', (mn, pTs), 0) # (stk', loc, C, sig, Suc pc) # frs)" - (is "state' = Norm (hp, ?f # ?f' # frs)") - by (simp add: raise_xcpt_def) + with mC' wfprog + obtain D0 rT0 maxs0 maxl0 ins0 et0 where + mX: "method (G, X') (mn, pTs) = Some (D0, rT0, maxs0, maxl0, ins0, et0)" "G\rT0\rT" + by (auto dest: subtype_widen_methd intro: that) - from wtprog mD'' - have start: "wt_start G D'' pTs mxl' (phi D'' (mn, pTs)) \ ins' \ []" - by (auto dest: wt_jvm_prog_impl_wt_start) - - then - obtain LT0 where - LT0: "phi D'' (mn, pTs) ! 0 = Some ([], LT0)" - by (clarsimp simp add: wt_start_def sup_state_conv) + from X' D have D_subcls: "G \ D \C X'" by simp + + with wfprog mX + obtain D'' rT' mxs' mxl' ins' et' where + mD: "method (G, D) (mn, pTs) = Some (D'', rT', mxs', mxl', ins', et')" + "G \ rT' \ rT0" + by (auto dest: subtype_widen_methd intro: that) + + from mX mD have rT': "G \ rT' \ rT" by - (rule widen_trans) + + from is_class X'_subcls D_subcls + have is_class_D: "is_class G D" by (auto dest: subcls_is_class2) + + with mD wfprog + obtain mD'': + "method (G, D'') (mn, pTs) = Some (D'', rT', mxs', mxl', ins', et')" + "is_class G D''" + by (auto dest: method_in_md) + + from loc obj_ty have "fst (the (hp ref)) = D" by (simp add: obj_ty_def) - have c_f: "correct_frame G hp ([], LT0) mxl' ins' ?f" - proof - - from start LT0 - have sup_loc: - "G \ (OK (Class D'') # map OK pTs @ replicate mxl' Err) <=l LT0" - (is "G \ ?LT <=l LT0") - by (simp add: wt_start_def sup_state_conv) - - have r: "approx_loc G hp (replicate mxl' arbitrary) (replicate mxl' Err)" - by (simp add: approx_loc_def approx_val_Err - list_all2_def set_replicate_conv_if) - - from wfprog mD is_class_D - have "G \ Class D \ Class D''" - by (auto dest: method_wf_mdecl) - with obj_ty loc - have a: "approx_val G hp (Addr ref) (OK (Class D''))" - by (simp add: approx_val_def conf_def) - - from opTs w l l_o wfprog - have "approx_stk G hp opTs (rev pTs)" - by (auto elim!: approx_stk_all_widen simp add: zip_rev) - hence "approx_stk G hp (rev opTs) pTs" by (subst approx_stk_rev) + with oX_Addr oX_pos state' method ins stk' l_o l loc obj_ty mD no_xcp + have state'_val: + "state' = + Norm (hp, ([], Addr ref # rev opTs @ replicate mxl' arbitrary, + D'', (mn, pTs), 0) # (opTs @ Addr ref # stk', loc, C, sig, pc) # frs)" + (is "state' = Norm (hp, ?f # ?f' # frs)") + by (simp add: raise_system_xcpt_def) + + from wtprog mD'' + have start: "wt_start G D'' pTs mxl' (phi D'' (mn, pTs)) \ ins' \ []" + by (auto dest: wt_jvm_prog_impl_wt_start) + + then obtain LT0 where + LT0: "phi D'' (mn, pTs) ! 0 = Some ([], LT0)" + by (clarsimp simp add: wt_start_def sup_state_conv) - with r a l_o l - have "approx_loc G hp (Addr ref # rev opTs @ replicate mxl' arbitrary) ?LT" - (is "approx_loc G hp ?lt ?LT") - by (auto simp add: approx_loc_append approx_stk_def) + have c_f: "correct_frame G hp ([], LT0) mxl' ins' ?f" + proof - + from start LT0 + have sup_loc: + "G \ (OK (Class D'') # map OK pTs @ replicate mxl' Err) <=l LT0" + (is "G \ ?LT <=l LT0") + by (simp add: wt_start_def sup_state_conv) - from this sup_loc wfprog - have "approx_loc G hp ?lt LT0" by (rule approx_loc_widen) - with start l_o l - show ?thesis by (simp add: correct_frame_def) - qed + have r: "approx_loc G hp (replicate mxl' arbitrary) (replicate mxl' Err)" + by (simp add: approx_loc_def list_all2_def set_replicate_conv_if) + + from wfprog mD is_class_D + have "G \ Class D \ Class D''" + by (auto dest: method_wf_mdecl) + with obj_ty loc + have a: "approx_val G hp (Addr ref) (OK (Class D''))" + by (simp add: approx_val_def conf_def) - have c_f': "correct_frame G hp (tl ST', LT') maxl ins ?f'" - proof - - from s s' mC' step l - have "G \ LT <=l LT'" - by (simp add: step_def sup_state_conv) - with wfprog a_loc - have a: "approx_loc G hp loc LT'" - by - (rule approx_loc_widen) - moreover - from s s' mC' step l - have "G \ map OK ST <=l map OK (tl ST')" - by (auto simp add: step_def sup_state_conv map_eq_Cons) - with wfprog a_stk' - have "approx_stk G hp stk' (tl ST')" - by - (rule approx_stk_widen) - ultimately - show ?thesis by (simp add: correct_frame_def suc_l pc) - qed + from opTs w l l_o wfprog + have "approx_stk G hp opTs (rev pTs)" + by (auto elim!: approx_stk_all_widen simp add: zip_rev) + hence "approx_stk G hp (rev opTs) pTs" by (subst approx_stk_rev) + + with r a l_o l + have "approx_loc G hp (Addr ref # rev opTs @ replicate mxl' arbitrary) ?LT" + (is "approx_loc G hp ?lt ?LT") + by (auto simp add: approx_loc_append approx_stk_def) - with state'_val heap_ok mD'' ins method phi_pc s X' l - frames s' LT0 c_f c_f' is_class_C - have ?thesis by (simp add: correct_state_def) (intro exI conjI, blast) - } - - with Null_ok oX_Ref - show "G,phi \JVM state'\" by (cases oX) auto + from this sup_loc wfprog + have "approx_loc G hp ?lt LT0" by (rule approx_loc_widen) + with start l_o l + show ?thesis by (simp add: correct_frame_def) + qed + + from state'_val heap_ok mD'' ins method phi_pc s X' l mX + frames s' LT0 c_f is_class_C stk' oX_Addr frame + show ?thesis by (simp add: correct_state_def) (intro exI conjI, blast) qed lemmas [simp del] = map_append lemma Return_correct: "[| wt_jvm_prog G phi; - method (G,C) sig = Some (C,rT,maxs,maxl,ins); + method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); ins ! pc = Return; - wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; + wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; - G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ |] + G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ |] ==> G,phi \JVM state'\" -apply (clarsimp simp add: neq_Nil_conv defs1 split: split_if_asm iff del: not_None_eq) -apply (frule wt_jvm_prog_impl_wt_instr) -apply (assumption, assumption, erule Suc_lessD) -apply (clarsimp simp add: map_eq_Cons append_eq_conv_conj defs1) -apply (unfold wt_jvm_prog_def) -apply (frule subcls_widen_methd, assumption+) -apply clarify -apply simp -apply (erule conf_widen, assumption) -apply (erule widen_trans)+ -apply blast -done +proof - + assume wt_prog: "wt_jvm_prog G phi" + assume meth: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)" + assume ins: "ins ! pc = Return" + assume wt: "wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc" + assume s': "Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs)" + assume correct: "G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\" + + from wt_prog + obtain wfmb where wf: "wf_prog wfmb G" by (simp add: wt_jvm_prog_def) + + from meth ins s' + have "frs = [] \ ?thesis" by (simp add: correct_state_def) + moreover + { fix f frs' + assume frs': "frs = f#frs'" + moreover + obtain stk' loc' C' sig' pc' where + f: "f = (stk',loc',C',sig',pc')" by (cases f) + moreover + obtain mn pt where + sig: "sig = (mn,pt)" by (cases sig) + moreover + note meth ins s' + ultimately + have state': + "state' = (None,hp,(hd stk#(drop (1+length pt) stk'),loc',C',sig',pc'+1)#frs')" + (is "state' = (None,hp,?f'#frs')") + by simp + + from correct meth + obtain ST LT where + hp_ok: "G \h hp \" and + phi_pc: "phi C sig ! pc = Some (ST, LT)" and + frame: "correct_frame G hp (ST, LT) maxl ins (stk,loc,C,sig,pc)" and + frames: "correct_frames G hp phi rT sig frs" + by (simp add: correct_state_def, clarify, blast) + + from phi_pc ins wt + obtain T ST' where "ST = T # ST'" "G \ T \ rT" + by (simp add: wt_instr_def) blast + with wf frame + have hd_stk: "G,hp \ (hd stk) ::\ rT" + by (auto simp add: correct_frame_def elim: conf_widen) + from f frs' frames sig + obtain apTs ST0' ST' LT' D D' D'' rT' rT'' maxs' maxl' ins' et' body where + phi': "phi C' sig' ! pc' = Some (ST',LT')" and + class': "is_class G C'" and + meth': "method (G,C') sig' = Some (C',rT',maxs',maxl',ins',et')" and + ins': "ins' ! pc' = Invoke D' mn pt" and + frame': "correct_frame G hp (ST', LT') maxl' ins' f" and + frames':"correct_frames G hp phi rT' sig' frs'" and + rT'': "G \ rT \ rT''" and + meth'': "method (G, D) sig = Some (D'', rT'', body)" and + ST0': "ST' = rev apTs @ Class D # ST0'" and + len': "length apTs = length pt" + by clarsimp blast + + from f frame' + obtain + stk': "approx_stk G hp stk' ST'" and + loc': "approx_loc G hp loc' LT'" and + pc': "pc' < length ins'" and + lloc':"length loc' = Suc (length (snd sig') + maxl')" + by (simp add: correct_frame_def) + + from wt_prog class' meth' pc' + have "wt_instr (ins'!pc') G rT' (phi C' sig') maxs' (length ins') et' pc'" + by (rule wt_jvm_prog_impl_wt_instr) + with ins' phi' sig + obtain apTs ST0 X ST'' LT'' body' rT0 mD where + phi_suc: "phi C' sig' ! Suc pc' = Some (ST'', LT'')" and + ST0: "ST' = rev apTs @ X # ST0" and + len: "length apTs = length pt" and + less: "G \ (rT0 # ST0, LT') <=s (ST'', LT'')" and + methD': "method (G, D') sig = Some (mD, rT0, body')" and + lessD': "G \ X \ Class D'" and + suc_pc': "Suc pc' < length ins'" + by (clarsimp simp add: wt_instr_def eff_def norm_eff_def) blast + + from len len' ST0 ST0' + have "X = Class D" by simp + with lessD' + have "G \ D \C D'" by simp + moreover + note wf meth'' methD' + ultimately + have "G \ rT'' \ rT0" by (auto dest: subcls_widen_methd) + with wf hd_stk rT'' + have hd_stk': "G,hp \ (hd stk) ::\ rT0" by (auto elim: conf_widen widen_trans) + + have frame'': + "correct_frame G hp (ST'',LT'') maxl' ins' ?f'" + proof - + from wf hd_stk' len stk' less ST0 + have "approx_stk G hp (hd stk # drop (1+length pt) stk') ST''" + by (auto simp add: map_eq_Cons sup_state_conv + dest!: approx_stk_append elim: conf_widen) + moreover + from wf loc' less + have "approx_loc G hp loc' LT''" by (simp add: sup_state_conv) blast + moreover + note suc_pc' lloc' + ultimately + show ?thesis by (simp add: correct_frame_def) + qed + + with state' frs' f meth hp_ok hd_stk phi_suc frames' meth' phi' class' + have ?thesis by (simp add: correct_state_def) + } + ultimately + show ?thesis by (cases frs) blast+ +qed + lemmas [simp] = map_append lemma Goto_correct: "[| wf_prog wt G; - method (G,C) sig = Some (C,rT,maxs,maxl,ins); + method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); ins ! pc = Goto branch; - wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; + wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ |] ==> G,phi \JVM state'\" @@ -487,9 +1101,9 @@ lemma Ifcmpeq_correct: "[| wf_prog wt G; - method (G,C) sig = Some (C,rT,maxs,maxl,ins); + method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); ins ! pc = Ifcmpeq branch; - wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; + wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ |] ==> G,phi \JVM state'\" @@ -499,9 +1113,9 @@ lemma Pop_correct: "[| wf_prog wt G; - method (G,C) sig = Some (C,rT,maxs,maxl,ins); + method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); ins ! pc = Pop; - wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; + wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ |] ==> G,phi \JVM state'\" @@ -511,9 +1125,9 @@ lemma Dup_correct: "[| wf_prog wt G; - method (G,C) sig = Some (C,rT,maxs,maxl,ins); + method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); ins ! pc = Dup; - wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; + wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ |] ==> G,phi \JVM state'\" @@ -523,9 +1137,9 @@ lemma Dup_x1_correct: "[| wf_prog wt G; - method (G,C) sig = Some (C,rT,maxs,maxl,ins); + method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); ins ! pc = Dup_x1; - wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; + wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ |] ==> G,phi \JVM state'\" @@ -535,9 +1149,9 @@ lemma Dup_x2_correct: "[| wf_prog wt G; - method (G,C) sig = Some (C,rT,maxs,maxl,ins); + method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); ins ! pc = Dup_x2; - wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; + wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ |] ==> G,phi \JVM state'\" @@ -547,9 +1161,9 @@ lemma Swap_correct: "[| wf_prog wt G; - method (G,C) sig = Some (C,rT,maxs,maxl,ins); + method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); ins ! pc = Swap; - wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; + wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ |] ==> G,phi \JVM state'\" @@ -559,9 +1173,9 @@ lemma IAdd_correct: "[| wf_prog wt G; - method (G,C) sig = Some (C,rT,maxs,maxl,ins); + method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); ins ! pc = IAdd; - wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; + wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ |] ==> G,phi \JVM state'\" @@ -569,29 +1183,51 @@ apply blast done +lemma Throw_correct: +"[| wf_prog wt G; + method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); + ins ! pc = Throw; + Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; + G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\; + fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None |] +==> G,phi \JVM state'\" + by simp -lemma instr_correct: + +text {* + The next theorem collects the results of the sections above, + i.e.~exception handling and the execution step for each + instruction. It states type safety for single step execution: + in welltyped programs, a conforming state is transformed + into another conforming state when one instruction is executed. +*} +theorem instr_correct: "[| wt_jvm_prog G phi; - method (G,C) sig = Some (C,rT,maxs,maxl,ins); + method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ |] ==> G,phi \JVM state'\" apply (frule wt_jvm_prog_impl_wt_instr_cor) apply assumption+ +apply (cases "fst (exec_instr (ins!pc) G hp stk loc C sig pc frs)") +defer +apply (erule xcpt_correct, assumption+) apply (cases "ins!pc") prefer 8 apply (rule Invoke_correct, assumption+) prefer 8 apply (rule Return_correct, assumption+) +prefer 5 +apply (rule Getfield_correct, assumption+) +prefer 6 +apply (rule Checkcast_correct, assumption+) apply (unfold wt_jvm_prog_def) apply (rule Load_correct, assumption+) apply (rule Store_correct, assumption+) apply (rule LitPush_correct, assumption+) apply (rule New_correct, assumption+) -apply (rule Getfield_correct, assumption+) apply (rule Putfield_correct, assumption+) -apply (rule Checkcast_correct, assumption+) apply (rule Pop_correct, assumption+) apply (rule Dup_correct, assumption+) apply (rule Dup_x1_correct, assumption+) @@ -600,6 +1236,7 @@ apply (rule IAdd_correct, assumption+) apply (rule Goto_correct, assumption+) apply (rule Ifcmpeq_correct, assumption+) +apply (rule Throw_correct, assumption+) done section {* Main *} @@ -627,9 +1264,10 @@ done + lemma L0: "[| xp=None; frs\[] |] ==> (\state'. exec (G,xp,hp,frs) = Some state')" -by (clarsimp simp add: neq_Nil_conv simp del: split_paired_Ex) +by (clarsimp simp add: neq_Nil_conv split_beta) lemma L1: "[|wt_jvm_prog G phi; G,phi \JVM (xp,hp,frs)\; xp=None; frs\[]|] @@ -639,7 +1277,6 @@ apply (fast intro: BV_correct_1) done - theorem BV_correct [rule_format]: "[| wt_jvm_prog G phi; G \ s -jvm-> t |] ==> G,phi \JVM s\ --> G,phi \JVM t\" apply (unfold exec_all_def) @@ -648,12 +1285,11 @@ apply (auto intro: BV_correct_1) done - theorem BV_correct_initial: "[| wt_jvm_prog G phi; G \ s0 -jvm-> (None,hp,(stk,loc,C,sig,pc)#frs); G,phi \JVM s0 \|] -==> approx_stk G hp stk (fst (the (((phi C) sig) ! pc))) \ - approx_loc G hp loc (snd (the (((phi C) sig) ! pc)))" +==> approx_stk G hp stk (fst (the (phi C sig ! pc))) \ + approx_loc G hp loc (snd (the (phi C sig ! pc)))" apply (drule BV_correct) apply assumption+ apply (simp add: correct_state_def correct_frame_def split_def diff -r 3fb416265ba9 -r d09d0f160888 src/HOL/MicroJava/BV/Correct.thy --- a/src/HOL/MicroJava/BV/Correct.thy Sun Dec 16 00:17:18 2001 +0100 +++ b/src/HOL/MicroJava/BV/Correct.thy Sun Dec 16 00:17:44 2001 +0100 @@ -1,6 +1,6 @@ (* Title: HOL/MicroJava/BV/Correct.thy ID: $Id$ - Author: Cornelia Pusch + Author: Cornelia Pusch, Gerwin Klein Copyright 1999 Technische Universitaet Muenchen The invariant for the type safety proof. @@ -10,12 +10,6 @@ theory Correct = BVSpec: -lemma list_all2_rev [simp]: - "list_all2 P (rev l) (rev l') = list_all2 P l l'" - apply (unfold list_all2_def) - apply (simp add: zip_rev cong: conj_cong) - done - constdefs approx_val :: "[jvm_prog,aheap,val,ty err] => bool" "approx_val G h v any == case any of Err => True | OK T => G,h\v::\T" @@ -39,19 +33,19 @@ "correct_frames G hp phi rT0 sig0 (f#frs) = (let (stk,loc,C,sig,pc) = f in - (\ST LT rT maxs maxl ins. + (\ST LT rT maxs maxl ins et. phi C sig ! pc = Some (ST,LT) \ is_class G C \ - method (G,C) sig = Some(C,rT,(maxs,maxl,ins)) \ - (\C' mn pTs k. pc = k+1 \ ins!k = (Invoke C' mn pTs) \ + method (G,C) sig = Some(C,rT,(maxs,maxl,ins,et)) \ + (\C' mn pTs. ins!pc = (Invoke C' mn pTs) \ (mn,pTs) = sig0 \ (\apTs D ST' LT'. - (phi C sig)!k = Some ((rev apTs) @ (Class D) # ST', LT') \ + (phi C sig)!pc = Some ((rev apTs) @ (Class D) # ST', LT') \ length apTs = length pTs \ - (\D' rT' maxs' maxl' ins'. - method (G,D) sig0 = Some(D',rT',(maxs',maxl',ins')) \ + (\D' rT' maxs' maxl' ins' et'. + method (G,D) sig0 = Some(D',rT',(maxs',maxl',ins',et')) \ G \ rT0 \ rT') \ - correct_frame G hp (tl ST, LT) maxl ins f \ - correct_frames G hp phi rT sig frs))))" + correct_frame G hp (ST, LT) maxl ins f \ + correct_frames G hp phi rT sig frs))))" constdefs @@ -60,17 +54,17 @@ "correct_state G phi == \(xp,hp,frs). case xp of None => (case frs of - [] => True + [] => True | (f#fs) => G\h hp\ \ - (let (stk,loc,C,sig,pc) = f - in - \rT maxs maxl ins s. + (let (stk,loc,C,sig,pc) = f + in + \rT maxs maxl ins et s. is_class G C \ - method (G,C) sig = Some(C,rT,(maxs,maxl,ins)) \ + method (G,C) sig = Some(C,rT,(maxs,maxl,ins,et)) \ phi C sig ! pc = Some s \ - correct_frame G hp s maxl ins f \ - correct_frames G hp phi rT sig fs)) - | Some x => True" + correct_frame G hp s maxl ins f \ + correct_frames G hp phi rT sig fs)) + | Some x => frs = []" syntax (xsymbols) diff -r 3fb416265ba9 -r d09d0f160888 src/HOL/MicroJava/BV/Effect.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/MicroJava/BV/Effect.thy Sun Dec 16 00:17:44 2001 +0100 @@ -0,0 +1,339 @@ +(* Title: HOL/MicroJava/BV/Effect.thy + ID: $Id$ + Author: Gerwin Klein + Copyright 2000 Technische Universitaet Muenchen +*) + +header {* Effect of Instructions on the State Type *} + +theory Effect = JVMType + JVMExec: + +types + succ_type = "(p_count \ state_type option) list" + +text {* Program counter of successor instructions: *} +consts + succs :: "instr => p_count => p_count list" +primrec + "succs (Load idx) pc = [pc+1]" + "succs (Store idx) pc = [pc+1]" + "succs (LitPush v) pc = [pc+1]" + "succs (Getfield F C) pc = [pc+1]" + "succs (Putfield F C) pc = [pc+1]" + "succs (New C) pc = [pc+1]" + "succs (Checkcast C) pc = [pc+1]" + "succs Pop pc = [pc+1]" + "succs Dup pc = [pc+1]" + "succs Dup_x1 pc = [pc+1]" + "succs Dup_x2 pc = [pc+1]" + "succs Swap pc = [pc+1]" + "succs IAdd pc = [pc+1]" + "succs (Ifcmpeq b) pc = [pc+1, nat (int pc + b)]" + "succs (Goto b) pc = [nat (int pc + b)]" + "succs Return pc = [pc]" + "succs (Invoke C mn fpTs) pc = [pc+1]" + "succs Throw pc = [pc]" + +text "Effect of instruction on the state type:" +consts +eff' :: "instr \ jvm_prog \ state_type => state_type" + +recdef eff' "{}" +"eff' (Load idx, G, (ST, LT)) = (ok_val (LT ! idx) # ST, LT)" +"eff' (Store idx, G, (ts#ST, LT)) = (ST, LT[idx:= OK ts])" +"eff' (LitPush v, G, (ST, LT)) = (the (typeof (\v. None) v) # ST, LT)" +"eff' (Getfield F C, G, (oT#ST, LT)) = (snd (the (field (G,C) F)) # ST, LT)" +"eff' (Putfield F C, G, (vT#oT#ST, LT)) = (ST,LT)" +"eff' (New C, G, (ST,LT)) = (Class C # ST, LT)" +"eff' (Checkcast C, G, (RefT rt#ST,LT)) = (Class C # ST,LT)" +"eff' (Pop, G, (ts#ST,LT)) = (ST,LT)" +"eff' (Dup, G, (ts#ST,LT)) = (ts#ts#ST,LT)" +"eff' (Dup_x1, G, (ts1#ts2#ST,LT)) = (ts1#ts2#ts1#ST,LT)" +"eff' (Dup_x2, G, (ts1#ts2#ts3#ST,LT)) = (ts1#ts2#ts3#ts1#ST,LT)" +"eff' (Swap, G, (ts1#ts2#ST,LT)) = (ts2#ts1#ST,LT)" +"eff' (IAdd, G, (PrimT Integer#PrimT Integer#ST,LT)) + = (PrimT Integer#ST,LT)" +"eff' (Ifcmpeq b, G, (ts1#ts2#ST,LT)) = (ST,LT)" +"eff' (Goto b, G, s) = s" + -- "Return has no successor instruction in the same method" +"eff' (Return, G, s) = s" + -- "Throw always terminates abruptly" +"eff' (Throw, G, s) = s" +"eff' (Invoke C mn fpTs, G, (ST,LT)) = (let ST' = drop (length fpTs) ST + in (fst (snd (the (method (G,C) (mn,fpTs))))#(tl ST'),LT))" + + +consts + match_any :: "jvm_prog \ p_count \ exception_table \ cname list" +primrec + "match_any G pc [] = []" + "match_any G pc (e#es) = (let (start_pc, end_pc, handler_pc, catch_type) = e; + es' = match_any G pc es + in + if start_pc <= pc \ pc < end_pc then catch_type#es' else es')" + + +consts + xcpt_names :: "instr \ jvm_prog \ p_count \ exception_table => cname list" +recdef xcpt_names "{}" + "xcpt_names (Getfield F C, G, pc, et) = [Xcpt NullPointer]" + "xcpt_names (Putfield F C, G, pc, et) = [Xcpt NullPointer]" + "xcpt_names (New C, G, pc, et) = [Xcpt OutOfMemory]" + "xcpt_names (Checkcast C, G, pc, et) = [Xcpt ClassCast]" + "xcpt_names (Throw, G, pc, et) = match_any G pc et" + "xcpt_names (Invoke C m p, G, pc, et) = match_any G pc et" + "xcpt_names (i, G, pc, et) = []" + + +constdefs + xcpt_eff :: "instr \ jvm_prog \ p_count \ state_type option \ exception_table \ succ_type" + "xcpt_eff i G pc s et == + map (\C. (the (match_exception_table G C pc et), case s of None \ None | Some s' \ Some ([Class C], snd s'))) + (xcpt_names (i,G,pc,et))" + + norm_eff :: "instr \ jvm_prog \ state_type option \ state_type option" + "norm_eff i G == option_map (\s. eff' (i,G,s))" + + eff :: "instr => jvm_prog => p_count => exception_table => state_type option => succ_type" + "eff i G pc et s == (map (\pc'. (pc',norm_eff i G s)) (succs i pc)) @ (xcpt_eff i G pc s et)" + + +text "Conditions under which eff is applicable:" +consts +app' :: "instr \ jvm_prog \ nat \ ty \ state_type => bool" + +recdef app' "{}" +"app' (Load idx, G, maxs, rT, s) = (idx < length (snd s) \ + (snd s) ! idx \ Err \ + length (fst s) < maxs)" +"app' (Store idx, G, maxs, rT, (ts#ST, LT)) = (idx < length LT)" +"app' (LitPush v, G, maxs, rT, s) = (length (fst s) < maxs \ typeof (\t. None) v \ None)" +"app' (Getfield F C, G, maxs, rT, (oT#ST, LT)) = (is_class G C \ + field (G,C) F \ None \ + fst (the (field (G,C) F)) = C \ + G \ oT \ (Class C))" +"app' (Putfield F C, G, maxs, rT, (vT#oT#ST, LT)) = (is_class G C \ + field (G,C) F \ None \ + fst (the (field (G,C) F)) = C \ + G \ oT \ (Class C) \ + G \ vT \