# HG changeset patch # User kleing # Date 1008707281 -3600 # Node ID 7319d384d0d3a6538d5c7da93416d8fc93c5a36a # Parent c78a00903e5226e266339b7003d576190009bb3d removed preallocated heaps axiom (now in type safety invariant) diff -r c78a00903e52 -r 7319d384d0d3 src/HOL/MicroJava/BV/BVSpecTypeSafe.thy --- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Tue Dec 18 18:37:56 2001 +0100 +++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Tue Dec 18 21:28:01 2001 +0100 @@ -247,16 +247,16 @@ ==> \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 [simp] = split_beta raise_system_xcpt_def note [split] = split_if_asm option.split_asm assume wt: ?wt ?correct + hence pre: "preallocated hp" by (simp add: correct_state_def) - assume xcpt: ?xcpt - thus ?thesis + assume xcpt: ?xcpt with pre show ?thesis proof (cases "ins!pc") - case New with xcpt - show ?thesis by (auto dest: new_Addr_OutOfMemory) + case New with xcpt pre + show ?thesis by (auto dest: new_Addr_OutOfMemory) next case Throw with xcpt wt show ?thesis @@ -311,6 +311,7 @@ from correct meth obtain ST LT where hp_ok: "G \h hp \" and + prehp: "preallocated 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 @@ -349,8 +350,7 @@ 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 prehp have "cname_of hp xcp = Xcpt OutOfMemory" by simp with New some_handler phi_pc eff obtain ST' LT' where phi': "phi C sig ! handler = Some (ST', LT')" and @@ -359,9 +359,9 @@ by (simp add: xcpt_eff_def) blast note phi' moreover - { from xcp + { from xcp prehp have "G,hp \ xcp ::\ Class (Xcpt OutOfMemory)" - by (simp add: conf_def obj_ty_def system_xcpt_allocated) + by (simp add: conf_def obj_ty_def) moreover from wf less loc have "approx_loc G hp loc LT'" @@ -380,8 +380,7 @@ 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 prehp have "cname_of hp xcp = Xcpt NullPointer" by simp with Getfield some_handler phi_pc eff obtain ST' LT' where phi': "phi C sig ! handler = Some (ST', LT')" and @@ -390,9 +389,9 @@ by (simp add: xcpt_eff_def) blast note phi' moreover - { from xcp + { from xcp prehp have "G,hp \ xcp ::\ Class (Xcpt NullPointer)" - by (simp add: conf_def obj_ty_def system_xcpt_allocated) + by (simp add: conf_def obj_ty_def) moreover from wf less loc have "approx_loc G hp loc LT'" @@ -411,8 +410,7 @@ 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 prehp have "cname_of hp xcp = Xcpt NullPointer" by simp with Putfield some_handler phi_pc eff obtain ST' LT' where phi': "phi C sig ! handler = Some (ST', LT')" and @@ -421,9 +419,9 @@ by (simp add: xcpt_eff_def) blast note phi' moreover - { from xcp + { from xcp prehp have "G,hp \ xcp ::\ Class (Xcpt NullPointer)" - by (simp add: conf_def obj_ty_def system_xcpt_allocated) + by (simp add: conf_def obj_ty_def) moreover from wf less loc have "approx_loc G hp loc LT'" @@ -442,8 +440,7 @@ 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 prehp have "cname_of hp xcp = Xcpt ClassCast" by simp with Checkcast some_handler phi_pc eff obtain ST' LT' where phi': "phi C sig ! handler = Some (ST', LT')" and @@ -452,9 +449,9 @@ by (simp add: xcpt_eff_def) blast note phi' moreover - { from xcp + { from xcp prehp have "G,hp \ xcp ::\ Class (Xcpt ClassCast)" - by (simp add: conf_def obj_ty_def system_xcpt_allocated) + by (simp add: conf_def obj_ty_def) moreover from wf less loc have "approx_loc G hp loc LT'" @@ -702,6 +699,7 @@ hext_upd_obj approx_stk_sup_heap approx_loc_sup_heap hconf_field_update + preallocated_field_update correct_frames_field_update conf_widen dest: widen_cfs_fields) @@ -729,6 +727,7 @@ from ins conf meth obtain ST LT where heap_ok: "G\h hp\" and + prealloc: "preallocated hp" and phi_pc: "phi C sig!pc = Some (ST,LT)" and is_class_C: "is_class G C" and frame: "correct_frame G hp (ST,LT) maxl ins (stk, loc, C, sig, pc)" and @@ -775,6 +774,8 @@ have "correct_frames G ?hp' phi rT sig frs" by - (rule correct_frames_newref, auto simp add: oconf_def dest: fields_is_type) + moreover + from hp prealloc have "preallocated ?hp'" by (rule preallocated_newref) ultimately show ?thesis by (simp add: is_class_C meth phi_suc correct_state_def del: not_None_eq) @@ -809,6 +810,7 @@ from ins method approx obtain s where heap_ok: "G\h hp\" and + prealloc:"preallocated hp" and phi_pc: "phi C sig!pc = Some s" and is_class_C: "is_class G C" and frame: "correct_frame G hp s maxl ins (stk, loc, C, sig, pc)" and @@ -955,7 +957,7 @@ 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 + frames s' LT0 c_f is_class_C stk' oX_Addr frame prealloc show ?thesis by (simp add: correct_state_def) (intro exI conjI, blast) qed @@ -1002,6 +1004,7 @@ from correct meth obtain ST LT where hp_ok: "G \h hp \" and + alloc: "preallocated 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" @@ -1077,7 +1080,7 @@ show ?thesis by (simp add: correct_frame_def) qed - with state' frs' f meth hp_ok hd_stk phi_suc frames' meth' phi' class' + with state' frs' f meth hp_ok hd_stk phi_suc frames' meth' phi' class' alloc have ?thesis by (simp add: correct_state_def) } ultimately @@ -1285,7 +1288,7 @@ apply (auto intro: BV_correct_1) done -theorem BV_correct_initial: +theorem BV_correct_implies_approx: "[| 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))) \ diff -r c78a00903e52 -r 7319d384d0d3 src/HOL/MicroJava/BV/Correct.thy --- a/src/HOL/MicroJava/BV/Correct.thy Tue Dec 18 18:37:56 2001 +0100 +++ b/src/HOL/MicroJava/BV/Correct.thy Tue Dec 18 21:28:01 2001 +0100 @@ -1,3 +1,4 @@ + (* Title: HOL/MicroJava/BV/Correct.thy ID: $Id$ Author: Cornelia Pusch, Gerwin Klein @@ -55,7 +56,7 @@ case xp of None => (case frs of [] => True - | (f#fs) => G\h hp\ \ + | (f#fs) => G\h hp\ \ preallocated hp \ (let (stk,loc,C,sig,pc) = f in \rT maxs maxl ins et s. @@ -262,6 +263,27 @@ simp add: obj_ty_def) done +section {* preallocated *} + +lemma preallocated_field_update: + "\ map_of (fields (G, oT)) X = Some T; hp a = Some(oT,fs); + G\h hp\; preallocated hp \ + \ preallocated (hp(a \ (oT, fs(X\v))))" + apply (unfold preallocated_def) + apply (rule allI) + apply (erule_tac x=x in allE) + apply simp + apply (rule ccontr) + apply (unfold hconf_def) + apply (erule allE, erule allE, erule impE, assumption) + apply (unfold oconf_def lconf_def) + apply (simp del: split_paired_All) + done + +lemma preallocated_newref: + "\ hp oref = None; preallocated hp \ \ preallocated (hp(oref\obj))" + by (unfold preallocated_def) auto + section {* correct-frames *} lemmas [simp del] = fun_upd_apply diff -r c78a00903e52 -r 7319d384d0d3 src/HOL/MicroJava/J/State.thy --- a/src/HOL/MicroJava/J/State.thy Tue Dec 18 18:37:56 2001 +0100 +++ b/src/HOL/MicroJava/J/State.thy Tue Dec 18 21:28:01 2001 +0100 @@ -27,14 +27,6 @@ state = "aheap \ locals" -- "heap, local parameter including This" xstate = "xcpt option \ state" -- "state including exception information" - -text {* - System exceptions are allocated in all heaps, - and they don't carry any information other than their type: *} -axioms - system_xcpt_allocated: "(hp::aheap) (XcptRef x) = Some (Xcpt x, empty)" - - syntax heap :: "state => aheap" locals :: "state => locals" diff -r c78a00903e52 -r 7319d384d0d3 src/HOL/MicroJava/JVM/JVMExceptions.thy --- a/src/HOL/MicroJava/JVM/JVMExceptions.thy Tue Dec 18 18:37:56 2001 +0100 +++ b/src/HOL/MicroJava/JVM/JVMExceptions.thy Tue Dec 18 21:28:01 2001 +0100 @@ -49,16 +49,28 @@ | Some handler_pc \ (None, hp, ([xc], loc, C, sig, handler_pc)#frs)))" +text {* + System exceptions are allocated in all heaps, + and they don't carry any information other than their type: +*} +constdefs + preallocated :: "aheap \ bool" + "preallocated hp \ \x. hp (XcptRef x) = Some (Xcpt x, empty)" + +lemma preallocated_iff [iff]: + "preallocated hp \ hp (XcptRef x) = Some (Xcpt x, empty)" + by (unfold preallocated_def) fast lemma cname_of_xcp: - "raise_system_xcpt b x = Some xcp \ cname_of (hp::aheap) xcp = Xcpt x" + "raise_system_xcpt b x = Some xcp \ preallocated hp + \ 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) + assume "preallocated hp" + hence "hp (XcptRef x) = Some (Xcpt x, empty)" .. ultimately show ?thesis by simp qed