641 apply (clarsimp simp add: conf_def obj_ty_def) |
641 apply (clarsimp simp add: conf_def obj_ty_def) |
642 apply (cases v) |
642 apply (cases v) |
643 apply (auto intro: rtrancl_trans) |
643 apply (auto intro: rtrancl_trans) |
644 done |
644 done |
645 |
645 |
646 lemmas defs1 = defs1 raise_system_xcpt_def |
646 lemmas defs2 = defs1 raise_system_xcpt_def |
647 |
647 |
648 lemma Checkcast_correct: |
648 lemma Checkcast_correct: |
649 "\<lbrakk> wt_jvm_prog G phi; |
649 "\<lbrakk> wt_jvm_prog G phi; |
650 method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); |
650 method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); |
651 ins!pc = Checkcast D; |
651 ins!pc = Checkcast D; |
652 wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; |
652 wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; |
653 Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
653 Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
654 G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>; |
654 G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>; |
655 fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk> |
655 fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk> |
656 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" |
656 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" |
657 apply (clarsimp simp add: defs1 wt_jvm_prog_def map_eq_Cons split: split_if_asm) |
657 apply (clarsimp simp add: defs2 wt_jvm_prog_def map_eq_Cons split: split_if_asm) |
658 apply (blast intro: Cast_conf2) |
658 apply (blast intro: Cast_conf2) |
659 done |
659 done |
660 |
660 |
661 |
661 |
662 lemma Getfield_correct: |
662 lemma Getfield_correct: |
666 wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; |
666 wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; |
667 Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
667 Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
668 G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>; |
668 G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>; |
669 fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk> |
669 fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk> |
670 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" |
670 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" |
671 apply (clarsimp simp add: defs1 map_eq_Cons wt_jvm_prog_def |
671 apply (clarsimp simp add: defs2 map_eq_Cons wt_jvm_prog_def |
672 split: option.split split_if_asm) |
672 split: option.split split_if_asm) |
673 apply (frule conf_widen) |
673 apply (frule conf_widen) |
674 apply assumption+ |
674 apply assumption+ |
675 apply (drule conf_RefTD) |
675 apply (drule conf_RefTD) |
676 apply (clarsimp simp add: defs1) |
676 apply (clarsimp simp add: defs2) |
677 apply (rule conjI) |
677 apply (rule conjI) |
678 apply (drule widen_cfs_fields) |
678 apply (drule widen_cfs_fields) |
679 apply assumption+ |
679 apply assumption+ |
680 apply (erule conf_widen) |
680 apply (erule conf_widen) |
681 prefer 2 |
681 prefer 2 |
698 wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; |
698 wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; |
699 Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
699 Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
700 G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>; |
700 G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>; |
701 fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk> |
701 fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk> |
702 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" |
702 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" |
703 apply (clarsimp simp add: defs1 split_beta split: option.split List.split split_if_asm) |
703 apply (clarsimp simp add: defs2 split_beta split: option.split List.split split_if_asm) |
704 apply (frule conf_widen) |
704 apply (frule conf_widen) |
705 prefer 2 |
705 prefer 2 |
706 apply assumption |
706 apply assumption |
707 apply assumption |
707 apply assumption |
708 apply (drule conf_RefTD) |
708 apply (drule conf_RefTD) |
1108 ins ! pc = Goto branch; |
1108 ins ! pc = Goto branch; |
1109 wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; |
1109 wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; |
1110 Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
1110 Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
1111 G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> |
1111 G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> |
1112 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" |
1112 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" |
1113 apply (clarsimp simp add: defs1) |
1113 apply (clarsimp simp add: defs2) |
1114 apply fast |
1114 apply fast |
1115 done |
1115 done |
1116 |
1116 |
1117 |
1117 |
1118 lemma Ifcmpeq_correct: |
1118 lemma Ifcmpeq_correct: |
1121 ins ! pc = Ifcmpeq branch; |
1121 ins ! pc = Ifcmpeq branch; |
1122 wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; |
1122 wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; |
1123 Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
1123 Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
1124 G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> |
1124 G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> |
1125 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" |
1125 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" |
1126 apply (clarsimp simp add: defs1) |
1126 apply (clarsimp simp add: defs2) |
1127 apply fast |
1127 apply fast |
1128 done |
1128 done |
1129 |
1129 |
1130 lemma Pop_correct: |
1130 lemma Pop_correct: |
1131 "\<lbrakk> wf_prog wt G; |
1131 "\<lbrakk> wf_prog wt G; |
1133 ins ! pc = Pop; |
1133 ins ! pc = Pop; |
1134 wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; |
1134 wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; |
1135 Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
1135 Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
1136 G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> |
1136 G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> |
1137 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" |
1137 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" |
1138 apply (clarsimp simp add: defs1) |
1138 apply (clarsimp simp add: defs2) |
1139 apply fast |
1139 apply fast |
1140 done |
1140 done |
1141 |
1141 |
1142 lemma Dup_correct: |
1142 lemma Dup_correct: |
1143 "\<lbrakk> wf_prog wt G; |
1143 "\<lbrakk> wf_prog wt G; |
1145 ins ! pc = Dup; |
1145 ins ! pc = Dup; |
1146 wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; |
1146 wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; |
1147 Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
1147 Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
1148 G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> |
1148 G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> |
1149 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" |
1149 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" |
1150 apply (clarsimp simp add: defs1 map_eq_Cons) |
1150 apply (clarsimp simp add: defs2 map_eq_Cons) |
1151 apply (blast intro: conf_widen) |
1151 apply (blast intro: conf_widen) |
1152 done |
1152 done |
1153 |
1153 |
1154 lemma Dup_x1_correct: |
1154 lemma Dup_x1_correct: |
1155 "\<lbrakk> wf_prog wt G; |
1155 "\<lbrakk> wf_prog wt G; |
1157 ins ! pc = Dup_x1; |
1157 ins ! pc = Dup_x1; |
1158 wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; |
1158 wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; |
1159 Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
1159 Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
1160 G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> |
1160 G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> |
1161 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" |
1161 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" |
1162 apply (clarsimp simp add: defs1 map_eq_Cons) |
1162 apply (clarsimp simp add: defs2 map_eq_Cons) |
1163 apply (blast intro: conf_widen) |
1163 apply (blast intro: conf_widen) |
1164 done |
1164 done |
1165 |
1165 |
1166 lemma Dup_x2_correct: |
1166 lemma Dup_x2_correct: |
1167 "\<lbrakk> wf_prog wt G; |
1167 "\<lbrakk> wf_prog wt G; |
1169 ins ! pc = Dup_x2; |
1169 ins ! pc = Dup_x2; |
1170 wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; |
1170 wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; |
1171 Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
1171 Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
1172 G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> |
1172 G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> |
1173 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" |
1173 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" |
1174 apply (clarsimp simp add: defs1 map_eq_Cons) |
1174 apply (clarsimp simp add: defs2 map_eq_Cons) |
1175 apply (blast intro: conf_widen) |
1175 apply (blast intro: conf_widen) |
1176 done |
1176 done |
1177 |
1177 |
1178 lemma Swap_correct: |
1178 lemma Swap_correct: |
1179 "\<lbrakk> wf_prog wt G; |
1179 "\<lbrakk> wf_prog wt G; |
1181 ins ! pc = Swap; |
1181 ins ! pc = Swap; |
1182 wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; |
1182 wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; |
1183 Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
1183 Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
1184 G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> |
1184 G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> |
1185 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" |
1185 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" |
1186 apply (clarsimp simp add: defs1 map_eq_Cons) |
1186 apply (clarsimp simp add: defs2 map_eq_Cons) |
1187 apply (blast intro: conf_widen) |
1187 apply (blast intro: conf_widen) |
1188 done |
1188 done |
1189 |
1189 |
1190 lemma IAdd_correct: |
1190 lemma IAdd_correct: |
1191 "\<lbrakk> wf_prog wt G; |
1191 "\<lbrakk> wf_prog wt G; |
1193 ins ! pc = IAdd; |
1193 ins ! pc = IAdd; |
1194 wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; |
1194 wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; |
1195 Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
1195 Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; |
1196 G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> |
1196 G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> |
1197 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" |
1197 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" |
1198 apply (clarsimp simp add: defs1 map_eq_Cons approx_val_def conf_def) |
1198 apply (clarsimp simp add: defs2 map_eq_Cons approx_val_def conf_def) |
1199 apply blast |
1199 apply blast |
1200 done |
1200 done |
1201 |
1201 |
1202 lemma Throw_correct: |
1202 lemma Throw_correct: |
1203 "\<lbrakk> wf_prog wt G; |
1203 "\<lbrakk> wf_prog wt G; |