Up to index of Isabelle/HOL/verificard
theory JVM = Kildall_Lift + JVMType + Opt + Product + Typing_Framework_err + EffectMono + BVSpec:(* Title: HOL/MicroJava/BV/JVM.thy
ID: $Id: JVM.thy,v 1.9.2.11 2002/03/09 22:12:50 kleing Exp $
Author: Tobias Nipkow, Gerwin Klein
Copyright 2000 TUM
*)
header {* \isaheader{Kildall for the JVM}\label{sec:JVM} *}
theory JVM = Kildall_Lift + JVMType + Opt + Product + Typing_Framework_err +
EffectMono + BVSpec:
constdefs
exec :: "jvm_prog \<Rightarrow> cname \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> bool \<Rightarrow> exception_table \<Rightarrow> instr list \<Rightarrow>
state step_type"
"exec G C maxs rT ini et bs ==
err_step (\<lambda>pc. app (bs!pc) G C pc maxs rT ini et) (\<lambda>pc. eff (bs!pc) G pc et)"
kiljvm :: "jvm_prog \<Rightarrow> cname \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> bool \<Rightarrow> exception_table \<Rightarrow>
instr list \<Rightarrow> state list \<Rightarrow> state list"
"kiljvm G C maxs maxr rT ini et bs ==
kildall (JVMType.le G maxs maxr) (JVMType.sup G maxs maxr) (exec G C maxs rT ini et bs)"
wt_kil :: "jvm_prog \<Rightarrow> cname \<Rightarrow> ty list \<Rightarrow> ty \<Rightarrow> bool \<Rightarrow> nat \<Rightarrow> nat
\<Rightarrow> exception_table \<Rightarrow> instr list \<Rightarrow> bool"
"wt_kil G C pTs rT ini mxs mxl et ins ==
bounded (exec G C mxs rT ini et ins) (size ins) \<and> 0 < size ins \<and>
(let this = OK (if ini \<and> C \<noteq> Object then PartInit C else Init (Class C));
first = Some (([],this#((map OK (map Init pTs)))@(replicate mxl Err)),
C=Object);
start = OK first#(replicate (size ins - 1) (OK None));
result = kiljvm G C mxs (1+size pTs+mxl) rT ini et ins start
in \<forall>n < size ins. result!n \<noteq> Err)"
wt_jvm_prog_kildall :: "jvm_prog \<Rightarrow> bool"
"wt_jvm_prog_kildall G ==
wf_prog (\<lambda>G C (sig,rT,(maxs,maxl,b,et)).
wt_kil G C (snd sig) rT (fst sig=init) maxs maxl et b) G"
lemma special_ex_swap_lemma [iff]:
"(? X. (? n. X = A n & P n) & Q X) = (? n. Q(A n) & P n)"
by blast
lemmas [iff del] = not_None_eq
lemma non_empty_succs: "succs i pc \<noteq> []"
by (cases i) auto
lemma non_empty:
"non_empty (\<lambda>pc. eff (bs!pc) G pc et)"
by (simp add: non_empty_def eff_def non_empty_succs)
lemma listn_Cons_Suc [elim!]:
"l#xs \<in> list n A \<Longrightarrow> (\<And>n'. n = Suc n' \<Longrightarrow> l \<in> A \<Longrightarrow> xs \<in> list n' A \<Longrightarrow> P) \<Longrightarrow> P"
by (cases n) auto
lemma listn_appendE [elim!]:
"a@b \<in> list n A \<Longrightarrow> (\<And>n1 n2. n=n1+n2 \<Longrightarrow> a \<in> list n1 A \<Longrightarrow> b \<in> list n2 A \<Longrightarrow> P) \<Longrightarrow> P"
proof -
have "\<And>n. a@b \<in> list n A \<Longrightarrow> \<exists>n1 n2. n=n1+n2 \<and> a \<in> list n1 A \<and> b \<in> list n2 A"
(is "\<And>n. ?list a n \<Longrightarrow> \<exists>n1 n2. ?P a n n1 n2")
proof (induct a)
fix n assume "?list [] n"
hence "?P [] n 0 n" by simp
thus "\<exists>n1 n2. ?P [] n n1 n2" by fast
next
fix n l ls
assume "?list (l#ls) n"
then obtain n' where n: "n = Suc n'" "l \<in> A" and "ls@b \<in> list n' A" by fastsimp
assume "\<And>n. ls @ b \<in> list n A \<Longrightarrow> \<exists>n1 n2. n = n1 + n2 \<and> ls \<in> list n1 A \<and> b \<in> list n2 A"
hence "\<exists>n1 n2. n' = n1 + n2 \<and> ls \<in> list n1 A \<and> b \<in> list n2 A" .
then obtain n1 n2 where "n' = n1 + n2" "ls \<in> list n1 A" "b \<in> list n2 A" by fast
with n have "?P (l#ls) n (n1+1) n2" by simp
thus "\<exists>n1 n2. ?P (l#ls) n n1 n2" by fastsimp
qed
moreover
assume "a@b \<in> list n A" "\<And>n1 n2. n=n1+n2 \<Longrightarrow> a \<in> list n1 A \<Longrightarrow> b \<in> list n2 A \<Longrightarrow> P"
ultimately
show ?thesis by blast
qed
lemmas [simp] = init_tys_def JType.esl_def
lemma replace_in_setI:
"\<And>n. ls \<in> list n A \<Longrightarrow> b \<in> A \<Longrightarrow> replace a b ls \<in> list n A"
by (induct ls) (auto simp add: replace_def)
theorem exec_pres_type:
"wf_prog wf_mb S \<Longrightarrow>
pres_type (exec S C maxs rT ini et bs) (size bs) (states S maxs maxr)"
apply (unfold exec_def JVM_states_unfold)
apply (rule pres_type_lift)
apply clarify
apply (case_tac s)
apply simp
apply (drule effNone)
apply simp
apply (simp add: eff_def eff_bool_def xcpt_eff_def norm_eff_def)
apply (case_tac "bs!p")
-- load
apply (clarsimp simp add: not_Err_eq)
apply (drule listE_nth_in, assumption)
apply fastsimp
-- store
apply (fastsimp simp add: not_None_eq)
-- litpush
apply clarsimp
apply (rule_tac x="Suc n" in exI)
apply (fastsimp simp add: not_None_eq typeof_empty_is_type)
-- new
apply clarsimp
apply (erule disjE)
apply (fastsimp intro: replace_in_setI)
apply clarsimp
apply (rule_tac x=1 in exI)
apply fastsimp
-- getfield
apply clarsimp
apply (erule disjE)
apply (fastsimp dest: field_fields fields_is_type)
apply (simp add: match_some_entry split: split_if_asm)
apply (rule_tac x=1 in exI)
apply fastsimp
-- putfield
apply clarsimp
apply (erule disjE)
apply fastsimp
apply (simp add: match_some_entry split: split_if_asm)
apply (rule_tac x=1 in exI)
apply fastsimp
-- checkcast
apply clarsimp
apply (erule disjE)
apply fastsimp
apply clarsimp
apply (rule_tac x=1 in exI)
apply fastsimp
-- invoke
apply (erule disjE)
apply (clarsimp simp add: Un_subset_iff)
apply (drule method_wf_mdecl, assumption+)
apply (clarsimp simp add: wf_mdecl_def wf_mhead_def)
apply fastsimp
apply clarsimp
apply (rule_tac x=1 in exI)
apply fastsimp
-- "@{text invoke_special}"
apply (erule disjE)
apply (clarsimp simp add: Un_subset_iff)
apply (drule method_wf_mdecl, assumption+)
apply (clarsimp simp add: wf_mdecl_def wf_mhead_def)
apply (fastsimp intro: replace_in_setI subcls_is_class)
apply clarsimp
apply (rule_tac x=1 in exI)
apply fastsimp
-- return
apply fastsimp
-- pop
apply fastsimp
-- dup
apply clarsimp
apply (rule_tac x="n'+2" in exI)
apply simp
apply (drule listE_length)+
apply fastsimp
-- "@{text dup_x1}"
apply clarsimp
apply (rule_tac x="Suc (Suc (Suc (length ST)))" in exI)
apply simp
apply (drule listE_length)+
apply fastsimp
-- "@{text dup_x2}"
apply clarsimp
apply (rule_tac x="Suc (Suc (Suc (Suc (length ST))))" in exI)
apply simp
apply (drule listE_length)+
apply fastsimp
-- swap
apply fastsimp
-- iadd
apply fastsimp
-- goto
apply fastsimp
-- icmpeq
apply fastsimp
-- throw
apply clarsimp
apply (erule disjE)
apply fastsimp
apply clarsimp
apply (rule_tac x=1 in exI)
apply fastsimp
done
lemmas [iff] = not_None_eq
lemma map_fst_eq:
"map fst (map (\<lambda>z. (f z, x z)) a) = map fst (map (\<lambda>z. (f z, y z)) a)"
by (induct a) auto
lemma succs_stable_eff:
"succs_stable (sup_state_opt G) (\<lambda>pc. eff (bs!pc) G pc et)"
apply (unfold succs_stable_def eff_def xcpt_eff_def)
apply (simp add: map_fst_eq)
done
lemma sup_state_opt_unfold:
"sup_state_opt G \<equiv> Opt.le (Product.le (Product.le (Listn.le (init_le G)) (Listn.le (Err.le (init_le G)))) (op =))"
by (simp add: sup_state_opt_def sup_state_bool_def sup_state_def sup_loc_def sup_ty_opt_def)
lemma "fst (JVMType.sl G maxs maxr) = x"
apply (unfold JVMType.sl_def)
apply (unfold reg_sl_def stk_esl_def)
apply (unfold upto_esl_def)
apply (unfold Err.sl_def Listn.sl_def Err.esl_def Opt.esl_def TrivLat.esl_def Product.esl_def)
apply (unfold Init.esl_def)
apply (simp del: init_tys_def)
oops
constdefs
opt_states :: "'c prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> ((init_ty list × init_ty err list) × bool) option set"
"opt_states G maxs maxr \<equiv> opt ((\<Union>{list n (init_tys G) |n. n \<le> maxs} × list maxr (err (init_tys G))) × {True,False})"
lemma app_mono:
"app_mono (sup_state_opt G) (\<lambda>pc. app (bs!pc) G C pc maxs rT ini et) (length bs) (opt_states G maxs maxr)"
by (unfold app_mono_def lesub_def) (blast intro: EffectMono.app_mono)
lemma le_list_appendI:
"\<And>b c d. a <=[r] b \<Longrightarrow> c <=[r] d \<Longrightarrow> a@c <=[r] b@d"
apply (induct a)
apply simp
apply (case_tac b)
apply auto
done
lemma le_listI:
"length a = length b \<Longrightarrow> (\<And>n. n < length a \<Longrightarrow> a!n <=_r b!n) \<Longrightarrow> a <=[r] b"
apply (unfold lesub_def Listn.le_def)
apply (simp add: list_all2_conv_all_nth)
done
lemma eff_mono:
"\<lbrakk>p < length bs; s <=_(sup_state_opt G) t; app (bs!p) G C p maxs rT ini et t\<rbrakk>
\<Longrightarrow> eff (bs!p) G p et s <=|sup_state_opt G| eff (bs!p) G p et t"
apply (unfold eff_def)
apply (rule le_list_appendI)
apply (simp add: norm_eff_def)
apply (rule le_listI)
apply simp
apply simp
apply (simp add: lesub_def)
apply (case_tac s)
apply simp
apply (simp del: split_paired_All split_paired_Ex)
apply (elim exE conjE)
apply simp
apply (drule eff_bool_mono, assumption+)
apply (simp add: xcpt_eff_def)
apply (rule le_listI)
apply simp
apply simp
apply (simp add: lesub_def)
apply (case_tac s)
apply simp
apply simp
apply (case_tac t)
apply simp
apply (clarsimp simp add: sup_state_conv)
done
lemma order_sup_state_opt:
"wf_prog wf_mb G \<Longrightarrow> order (sup_state_opt G)"
by (unfold sup_state_opt_unfold) (blast intro: order_init eq_order)
theorem exec_mono:
"wf_prog wf_mb G \<Longrightarrow>
mono (JVMType.le G maxs maxr) (exec G C maxs rT ini et bs) (size bs)
(states G maxs maxr)"
apply (unfold exec_def JVM_le_unfold JVM_states_unfold)
apply (rule mono_lift)
apply (fold sup_state_opt_unfold opt_states_def)
apply (erule order_sup_state_opt)
apply (rule succs_stable_eff)
apply (rule app_mono)
apply clarify
apply (rule eff_mono)
apply assumption+
done
theorem semilat_JVM_slI:
"wf_prog wf_mb G \<Longrightarrow> semilat (JVMType.sl G maxs maxr)"
apply (unfold JVMType.sl_def stk_esl_def reg_sl_def)
apply (rule semilat_opt)
apply (rule err_semilat_Product_esl)
apply (rule err_semilat_Product_esl)
apply (rule err_semilat_upto_esl)
apply (rule err_semilat_init, assumption)
apply (rule err_semilat_eslI)
apply (rule semilat_Listn_sl)
apply (rule err_semilat_init, assumption)
apply (rule bool_err_semilat)
done
lemma sl_triple_conv:
"JVMType.sl G maxs maxr ==
(states G maxs maxr, JVMType.le G maxs maxr, JVMType.sup G maxs maxr)"
by (simp (no_asm) add: states_def JVMType.le_def JVMType.sup_def)
lemma [intro!]: "acc (op =)"
by (simp add: acc_def lesssub_def lesub_def wf_def)
theorem is_bcv_kiljvm:
"\<lbrakk> wf_prog wf_mb G; bounded (exec G C maxs rT ini et bs) (size bs) \<rbrakk> \<Longrightarrow>
is_bcv (JVMType.le G maxs maxr) Err (exec G C maxs rT ini et bs)
(size bs) (states G maxs maxr) (kiljvm G C maxs maxr rT ini et bs)"
apply (unfold kiljvm_def sl_triple_conv)
apply (rule is_bcv_kildall)
apply (simp (no_asm) add: sl_triple_conv [symmetric])
apply (force intro!: semilat_JVM_slI dest: wf_acyclic
simp add: symmetric sl_triple_conv)
apply (simp (no_asm) add: JVM_le_unfold)
apply (blast intro!: ac_order_init wf_converse_subcls1_impl_acc_init
dest: wf_subcls1 wf_acyclic)
apply (simp add: JVM_le_unfold)
apply (erule exec_pres_type)
apply assumption
apply (erule exec_mono)
done
theorem wt_kil_correct:
"\<lbrakk> wt_kil G C pTs rT (mn=init) maxs mxl et bs; wf_prog wf_mb G;
is_class G C; \<forall>x \<in> set pTs. is_type G x \<rbrakk>
\<Longrightarrow> \<exists>phi. wt_method G C mn pTs rT maxs mxl bs et phi"
proof -
let ?this = "OK (if mn=init \<and> C \<noteq> Object then PartInit C else Init (Class C))"
let ?first = "Some (([],?this#((map OK (map Init pTs)))@(replicate mxl Err)),
C=Object)"
let ?start = "OK ?first#(replicate (size bs - 1) (OK None))"
assume wf: "wf_prog wf_mb G"
assume isclass: "is_class G C"
assume istype: "\<forall>x \<in> set pTs. is_type G x"
assume "wt_kil G C pTs rT (mn=init) maxs mxl et bs"
then obtain maxr r where
bounded: "bounded (exec G C maxs rT (mn=init) et bs) (size bs)" and
result: "r = kiljvm G C maxs maxr rT (mn=init) et bs ?start" and
success: "\<forall>n < size bs. r!n \<noteq> Err" and
instrs: "0 < size bs" and
maxr: "maxr = Suc (length pTs + mxl)"
by (unfold wt_kil_def) simp
from wf bounded
have bcv:
"is_bcv (JVMType.le G maxs maxr) Err (exec G C maxs rT (mn=init) et bs)
(size bs) (states G maxs maxr) (kiljvm G C maxs maxr rT (mn=init) et bs)"
by (rule is_bcv_kiljvm)
{ fix l x have "set (replicate l x) \<subseteq> {x}" by (cases "0 < l") simp+
} note subset_replicate = this
from istype have "set pTs \<subseteq> types G" by auto
hence "OK ` set pTs \<subseteq> err (types G)" by auto
with instrs maxr isclass
have "?start \<in> list (length bs) (states G maxs maxr)"
apply (unfold list_def JVM_states_unfold)
apply (simp add: init_tys_def JType.esl_def split del: split_if)
apply (rule conjI)
apply simp
apply (rule conjI)
apply (simp add: Un_subset_iff)
apply (rule conjI)
apply blast
apply (rule_tac B = "{Err}" in subset_trans)
apply (simp add: subset_replicate)
apply simp
apply (rule_tac B = "{OK None}" in subset_trans)
apply (simp add: subset_replicate)
apply simp
done
with bcv success result have
"\<exists>ts\<in>list (length bs) (states G maxs maxr).
?start <=[JVMType.le G maxs maxr] ts \<and>
wt_step (JVMType.le G maxs maxr) Err (exec G C maxs rT (mn=init) et bs) ts"
apply (unfold is_bcv_def)
apply (drule bspec, assumption)
apply (drule iffD1)
apply blast
apply assumption
done
then obtain phi' where
l: "phi' \<in> list (length bs) (states G maxs maxr)" and
s: "?start <=[JVMType.le G maxs maxr] phi'" and
w: "wt_step (JVMType.le G maxs maxr) Err (exec G C maxs rT (mn=init) et bs) phi'"
by blast
hence dynamic:
"dynamic_wt (sup_state_opt G) (exec G C maxs rT (mn=init) et bs) phi'"
by (simp add: dynamic_wt_def exec_def JVM_le_Err_conv)
from s have le: "JVMType.le G maxs maxr (?start ! 0) (phi'!0)"
by (drule_tac p=0 in le_listD) (simp add: lesub_def)+
from l have l: "size phi' = size bs" by simp
with instrs w have "phi' ! 0 \<noteq> Err" by (unfold wt_step_def) simp
with instrs l have phi0: "OK (map ok_val phi' ! 0) = phi' ! 0"
by (clarsimp simp add: not_Err_eq)
from l bounded
have bounded': "bounded (\<lambda>pc. eff (bs!pc) G pc et) (length phi')"
by (simp add: exec_def bounded_lift)
with dynamic
have "static_wt (sup_state_opt G) (\<lambda>pc. app (bs!pc) G C pc maxs rT (mn=init) et)
(\<lambda>pc. eff (bs!pc) G pc et) (map ok_val phi')"
by (auto intro: dynamic_imp_static simp add: exec_def non_empty)
with instrs l le bounded'
have "wt_method G C mn pTs rT maxs mxl bs et (map ok_val phi')"
apply (unfold wt_method_def static_wt_def)
apply simp
apply (rule conjI)
apply (unfold wt_start_def)
apply (unfold Let_def)
apply (rule JVM_le_convert [THEN iffD1])
apply (simp (no_asm) add: phi0)
apply clarify
apply (erule allE, erule impE, assumption)
apply (elim conjE)
apply (clarsimp simp add: lesub_def wt_instr_def)
apply (unfold bounded_def)
apply blast
done
thus ?thesis by blast
qed
theorem wt_kil_complete:
"\<lbrakk> wt_method G C mn pTs rT maxs mxl bs et phi; wf_prog wf_mb G;
length phi = length bs; is_class G C; \<forall>x \<in> set pTs. is_type G x;
map OK phi \<in> list (length bs) (states G maxs (1+size pTs+mxl)) \<rbrakk>
\<Longrightarrow> wt_kil G C pTs rT (mn=init) maxs mxl et bs"
proof -
assume wf: "wf_prog wf_mb G"
assume isclass: "is_class G C"
assume istype: "\<forall>x \<in> set pTs. is_type G x"
assume length: "length phi = length bs"
assume istype_phi: "map OK phi \<in> list (length bs) (states G maxs (1+size pTs+mxl))"
assume "wt_method G C mn pTs rT maxs mxl bs et phi"
then obtain
instrs: "0 < length bs" and
wt_start: "wt_start G C mn pTs mxl phi" and
wt_ins: "\<forall>pc. pc < length bs \<longrightarrow>
wt_instr (bs!pc) G C rT phi maxs (mn=init) (length bs) et pc"
by (unfold wt_method_def) simp
let ?eff = "\<lambda>pc. eff (bs!pc) G pc et"
let ?app = "\<lambda>pc. app (bs!pc) G C pc maxs rT (mn=init) et"
have bounded_eff: "bounded ?eff (size bs)"
proof (unfold bounded_def, clarify)
fix pc pc' s s' assume "pc < length bs"
with wt_ins have "wt_instr (bs!pc) G C rT phi maxs (mn=init) (length bs) et pc" by fast
then obtain "\<forall>(pc',s') \<in> set (?eff pc (phi!pc)). pc' < length bs"
by (unfold wt_instr_def) fast
hence "\<forall>pc' \<in> set (map fst (?eff pc (phi!pc))). pc' < length bs" by auto
also
note succs_stable_eff
hence "map fst (?eff pc (phi!pc)) = map fst (?eff pc s)"
by (rule succs_stableD)
finally have "\<forall>(pc',s') \<in> set (?eff pc s). pc' < length bs" by auto
moreover assume "(pc',s') \<in> set (?eff pc s)"
ultimately show "pc' < length bs" by blast
qed
hence bounded_exec: "bounded (exec G C maxs rT (mn=init) et bs) (size bs)"
by (simp add: exec_def bounded_lift)
from wt_ins
have "static_wt (sup_state_opt G) ?app ?eff phi"
apply (unfold static_wt_def wt_instr_def lesub_def)
apply (simp (no_asm) only: length)
apply blast
done
with bounded_eff
have "dynamic_wt (sup_state_opt G) (err_step ?app ?eff) (map OK phi)"
by - (erule static_imp_dynamic, simp add: length)
hence dynamic:
"dynamic_wt (sup_state_opt G) (exec G C maxs rT (mn=init) et bs) (map OK phi)"
by (unfold exec_def)
let ?maxr = "1+size pTs+mxl"
from wf bounded_exec
have is_bcv:
"is_bcv (JVMType.le G maxs ?maxr) Err (exec G C maxs rT (mn=init) et bs)
(size bs) (states G maxs ?maxr) (kiljvm G C maxs ?maxr rT (mn=init) et bs)"
by (rule is_bcv_kiljvm)
let ?this = "OK (if mn=init \<and> C \<noteq> Object then PartInit C else Init (Class C))"
let ?first = "Some (([],?this#((map OK (map Init pTs)))@(replicate mxl Err)),
C=Object)"
let ?start = "OK ?first#(replicate (size bs - 1) (OK None))"
{ fix l x have "set (replicate l x) \<subseteq> {x}" by (cases "0 < l") simp+
} note subset_replicate = this
from istype have "set pTs \<subseteq> types G" by auto
hence "OK ` set pTs \<subseteq> err (types G)" by auto
with instrs isclass
have start: "?start \<in> list (length bs) (states G maxs ?maxr)"
apply (unfold list_def JVM_states_unfold)
apply (simp add: init_tys_def JType.esl_def split del: split_if)
apply (rule conjI)
apply simp
apply (rule conjI)
apply (simp add: Un_subset_iff)
apply (rule conjI)
apply blast
apply (rule_tac B = "{Err}" in subset_trans)
apply (simp add: subset_replicate)
apply simp
apply (rule_tac B = "{OK None}" in subset_trans)
apply (simp add: subset_replicate)
apply simp
done
let ?phi = "map OK phi"
have less_phi: "?start <=[JVMType.le G maxs ?maxr] ?phi"
proof -
from length instrs
have "length ?start = length (map OK phi)" by simp
moreover
{ fix n
from wt_start
have "G \<turnstile> ok_val (?start!0) <=' phi!0"
by (simp add: wt_start_def)
moreover
from instrs length
have "0 < length phi" by simp
ultimately
have "JVMType.le G maxs ?maxr (?start!0) (?phi!0)"
by (simp add: JVM_le_Err_conv Err.le_def lesub_def)
moreover
{ fix n'
have "JVMType.le G maxs ?maxr (OK None) (?phi!n)"
by (auto simp add: JVM_le_Err_conv Err.le_def lesub_def
split: err.splits)
hence "\<lbrakk> n = Suc n'; n < length ?start \<rbrakk>
\<Longrightarrow> JVMType.le G maxs ?maxr (?start!n) (?phi!n)"
by simp
}
ultimately
have "n < length ?start \<Longrightarrow> (?start!n) <=_(JVMType.le G maxs ?maxr) (?phi!n)"
by (unfold lesub_def) (cases n, blast+)
}
ultimately show ?thesis by (rule le_listI)
qed
from dynamic
have "wt_step (JVMType.le G maxs ?maxr) Err (exec G C maxs rT (mn=init) et bs) ?phi"
by (simp add: dynamic_wt_def JVM_le_Err_conv)
with start istype_phi less_phi is_bcv
have "\<forall>p. p < length bs \<longrightarrow> kiljvm G C maxs ?maxr rT (mn=init) et bs ?start ! p \<noteq> Err"
by (unfold is_bcv_def) auto
with bounded_exec instrs
show "wt_kil G C pTs rT (mn=init) maxs mxl et bs" by (unfold wt_kil_def) simp
qed
text {*
The above theorem @{text wt_kil_complete} is all nice'n shiny except
for one assumption: @{term "map OK phi \<in> list (length bs) (states G maxs (1+size pTs+mxl))"}
It does not hold for all @{text phi} that satisfy @{text wt_method}.
The assumption states mainly that all entries in @{text phi} are legal
types in the program context, that the stack size is bounded by @{text maxs},
that the register sizes are exactly @{term "1+size pTs+mxl"}.
The BV specification, i.e.~@{text wt_method}, only gives us this
property for \emph{reachable} code. For unreachable code,
e.g.~unused registers may contain arbitrary garbage. Even the stack
and register sizes can be different from the rest of the program (as
long as they are consistent inside each chunk of unreachable code).
All is not lost, though: for each @{text phi} that satisfies
@{text wt_method} there is a @{text phi'} that also satisfies
@{text wt_method} and that additionally satisfies our assumption.
The construction is quite easy: the entries for reachable code
are the same in @{text phi} and @{text phi'}, the entries for
unreachable code are all @{text None} in @{text phi'} (as it would
be produced by Kildall's algorithm).
Although this is proved easily by comment, it requires some more
overhead (i.e.~talking about reachable instructions) if you try
it the hard way. Thus it is missing here for the time being.
The other direction (@{text wt_kil_correct}) can be lifted to
programs without problems:
*}
lemma is_type_pTs:
"\<lbrakk> wf_prog wf_mb G; (C,S,fs,mdecls) \<in> set G; (sig,rT,code) \<in> set mdecls;
t \<in> set (snd sig) \<rbrakk>
\<Longrightarrow> is_type G t"
proof -
assume "wf_prog wf_mb G"
"(C,S,fs,mdecls) \<in> set G"
"(sig,rT,code) \<in> set mdecls"
hence "wf_mdecl wf_mb G C (sig,rT,code)"
by (unfold wf_prog_def wf_cdecl_def) auto
hence "\<forall>t \<in> set (snd sig). is_type G t"
by (unfold wf_mdecl_def wf_mhead_def) auto
moreover
assume "t \<in> set (snd sig)"
ultimately
show ?thesis by blast
qed
theorem jvm_kildall_correct:
"wt_jvm_prog_kildall G \<Longrightarrow> \<exists>Phi. wt_jvm_prog G Phi"
proof -
assume wtk: "wt_jvm_prog_kildall G"
then obtain wf_mb where wf: "wf_prog wf_mb G"
by (auto simp add: wt_jvm_prog_kildall_def)
let ?Phi = "\<lambda>C sig. let (C,rT,(maxs,maxl,ins,et)) = the (method (G,C) sig) in
SOME phi. wt_method G C (fst sig) (snd sig) rT maxs maxl ins et phi"
{ fix C S fs mdecls sig rT code
assume "(C,S,fs,mdecls) \<in> set G" "(sig,rT,code) \<in> set mdecls"
with wf
have "method (G,C) sig = Some (C,rT,code) \<and> is_class G C \<and>
(\<forall>t \<in> set (snd sig). is_type G t)"
by (simp add: methd is_type_pTs)
} note this [simp]
from wtk have "wt_jvm_prog G ?Phi"
apply (unfold wt_jvm_prog_def wt_jvm_prog_kildall_def wf_prog_def wf_cdecl_def)
apply clarsimp
apply (drule bspec, assumption)
apply (unfold wf_mdecl_def)
apply clarsimp
apply (drule bspec, assumption)
apply clarsimp
apply (drule wt_kil_correct [OF _ wf])
apply (auto intro: someI)
done
thus ?thesis by blast
qed
end
lemma special_ex_swap_lemma:
(EX X. (EX n. X = A n & P n) & Q X) = (EX n. Q (A n) & P n)
lemmas
(x ~= None) = (EX y. x = Some y)
lemma non_empty_succs:
succs i pc ~= []
lemma non_empty:
non_empty (%pc. eff (bs ! pc) G pc et)
lemma listn_Cons_Suc:
[| l # xs : list n A; !!n'. [| n = Suc n'; l : A; xs : list n' A |] ==> P |] ==> P
lemma listn_appendE:
[| a @ b : list n A;
!!n1 n2. [| n = n1 + n2; a : list n1 A; b : list n2 A |] ==> P |]
==> P
lemmas
init_tys G ==
{x. EX y:fst (JType.esl G). x = Init y} Un {x. EX c n. x = UnInit c n} Un
{x. EX c. x = PartInit c}
JType.esl G == (types G, subtype G, JType.sup G)
lemma replace_in_setI:
[| ls : list n A; b : A |] ==> replace a b ls : list n A
theorem exec_pres_type:
wf_prog wf_mb S ==> pres_type (JVM.exec S C maxs rT ini et bs) (length bs) (states S maxs maxr)
lemmas
(x ~= None) = (EX y. x = Some y)
lemma map_fst_eq:
map fst (map (%z. (f z, x z)) a) = map fst (map (%z. (f z, y z)) a)
lemma succs_stable_eff:
succs_stable (sup_state_opt G) (%pc. eff (bs ! pc) G pc et)
lemma sup_state_opt_unfold:
sup_state_opt G ==
Opt.le
(Product.le (Product.le (Listn.le (init_le G)) (Listn.le (Err.le (init_le G))))
op =)
lemma app_mono:
app_mono (sup_state_opt G) (%pc. app (bs ! pc) G C pc maxs rT ini et) (length bs) (opt_states G maxs maxr)
lemma le_list_appendI:
[| a <=[r] b; c <=[r] d |] ==> a @ c <=[r] b @ d
lemma le_listI:
[| length a = length b; !!n. n < length a ==> a ! n <=_r b ! n |] ==> a <=[r] b
lemma eff_mono:
[| p < length bs; s <=_(sup_state_opt G) t;
app (bs ! p) G C p maxs rT ini et t |]
==> eff (bs ! p) G p et s <=|sup_state_opt G| eff (bs ! p) G p et t
lemma order_sup_state_opt:
wf_prog wf_mb G ==> order (sup_state_opt G)
theorem exec_mono:
wf_prog wf_mb G
==> Kildall.mono (JVMType.le G maxs maxr) (JVM.exec G C maxs rT ini et bs)
(length bs) (states G maxs maxr)
theorem semilat_JVM_slI:
wf_prog wf_mb G ==> semilat (JVMType.sl G maxs maxr)
lemma sl_triple_conv:
JVMType.sl G maxs maxr == (states G maxs maxr, JVMType.le G maxs maxr, JVMType.sup G maxs maxr)
lemma
acc op =
theorem is_bcv_kiljvm:
[| wf_prog wf_mb G; bounded (JVM.exec G C maxs rT ini et bs) (length bs) |]
==> is_bcv (JVMType.le G maxs maxr) Err (JVM.exec G C maxs rT ini et bs)
(length bs) (states G maxs maxr) (kiljvm G C maxs maxr rT ini et bs)
theorem wt_kil_correct:
[| wt_kil G C pTs rT (mn = init) maxs mxl et bs; wf_prog wf_mb G; is_class G C;
Ball (set pTs) (is_type G) |]
==> EX phi. wt_method G C mn pTs rT maxs mxl bs et phi
theorem wt_kil_complete:
[| wt_method G C mn pTs rT maxs mxl bs et phi; wf_prog wf_mb G;
length phi = length bs; is_class G C; Ball (set pTs) (is_type G);
map OK phi : list (length bs) (states G maxs (1 + length pTs + mxl)) |]
==> wt_kil G C pTs rT (mn = init) maxs mxl et bs
lemma is_type_pTs:
[| wf_prog wf_mb G; (C, S, fs, mdecls) : set G; (sig, rT, code) : set mdecls;
t : set (snd sig) |]
==> is_type G t
theorem jvm_kildall_correct:
wt_jvm_prog_kildall G ==> EX Phi. wt_jvm_prog G Phi