--- a/src/HOL/MicroJava/BV/LBVSpec.thy Sun Dec 16 00:17:18 2001 +0100
+++ b/src/HOL/MicroJava/BV/LBVSpec.thy Sun Dec 16 00:17:44 2001 +0100
@@ -6,186 +6,227 @@
header {* The Lightweight Bytecode Verifier *}
+theory LBVSpec = Effect + Kildall:
-theory LBVSpec = Step :
+text {*
+ The Lightweight Bytecode Verifier with exceptions has not
+ made it completely into the Isabelle 2001 release. Currently
+ there is only the specification itself available. The proofs of
+ soundness and completeness are broken (they still need to be
+ ported to the exception version). Both theories are included
+ for documentation (but they don't work for this specification),
+ please see the Isabelle 99-2 release for a working copy.
+*}
types
certificate = "state_type option list"
class_certificate = "sig => certificate"
prog_certificate = "cname => class_certificate"
+consts
+ merge :: "[jvm_prog, p_count, nat, nat, p_count, certificate, (nat \<times> (state_type option)) list, state] \<Rightarrow> state"
+primrec
+ "merge G pc mxs mxr max_pc cert [] x = x"
+ "merge G pc mxs mxr max_pc cert (s#ss) x = (let (pc',s') = s in
+ if pc' < max_pc \<and> pc' = pc+1 then
+ merge G pc mxs mxr max_pc cert ss (OK s' +_(sup G mxs mxr) x)
+ else if pc' < max_pc \<and> G \<turnstile> s' <=' cert!pc' then
+ merge G pc mxs mxr max_pc cert ss x
+ else Err)"
-constdefs
- check_cert :: "[instr, jvm_prog, state_type option, certificate, p_count, p_count]
- => bool"
- "check_cert i G s cert pc max_pc == \<forall>pc' \<in> set (succs i pc). pc' < max_pc \<and>
- (pc' \<noteq> pc+1 --> G \<turnstile> step i G s <=' cert!pc')"
-
- wtl_inst :: "[instr,jvm_prog,ty,state_type option,certificate,nat,p_count,p_count]
+constdefs
+ wtl_inst :: "[instr,jvm_prog,ty,state_type option,certificate,nat,nat,p_count,exception_table,p_count]
=> state_type option err"
- "wtl_inst i G rT s cert maxs max_pc pc ==
- if app i G maxs rT s \<and> check_cert i G s cert pc max_pc then
- if pc+1 mem (succs i pc) then OK (step i G s) else OK (cert!(pc+1))
+ "wtl_inst i G rT s cert maxs maxr max_pc et pc ==
+ if app i G maxs rT pc et s then
+ merge G pc maxs maxr max_pc cert (eff i G pc et s) (OK (cert!(pc+1)))
else Err"
-constdefs
- wtl_cert :: "[instr,jvm_prog,ty,state_type option,certificate,nat,p_count,p_count]
+ wtl_cert :: "[instr,jvm_prog,ty,state_type option,certificate,nat,nat,p_count,exception_table,p_count]
=> state_type option err"
- "wtl_cert i G rT s cert maxs max_pc pc ==
+ "wtl_cert i G rT s cert maxs maxr max_pc et pc ==
case cert!pc of
- None => wtl_inst i G rT s cert maxs max_pc pc
+ None => wtl_inst i G rT s cert maxs maxr max_pc et pc
| Some s' => if G \<turnstile> s <=' (Some s') then
- wtl_inst i G rT (Some s') cert maxs max_pc pc
+ wtl_inst i G rT (Some s') cert maxs maxr max_pc et pc
else Err"
consts
- wtl_inst_list :: "[instr list,jvm_prog,ty,certificate,nat,p_count,p_count,
+ wtl_inst_list :: "[instr list,jvm_prog,ty,certificate,nat,nat,p_count,exception_table,p_count,
state_type option] => state_type option err"
primrec
- "wtl_inst_list [] G rT cert maxs max_pc pc s = OK s"
- "wtl_inst_list (i#is) G rT cert maxs max_pc pc s =
- (let s' = wtl_cert i G rT s cert maxs max_pc pc in
- strict (wtl_inst_list is G rT cert maxs max_pc (pc+1)) s')"
+ "wtl_inst_list [] G rT cert maxs maxr max_pc et pc s = OK s"
+ "wtl_inst_list (i#is) G rT cert maxs maxr max_pc et pc s =
+ (let s' = wtl_cert i G rT s cert maxs maxr max_pc et pc in
+ strict (wtl_inst_list is G rT cert maxs maxr max_pc et (pc+1)) s')"
constdefs
- wtl_method :: "[jvm_prog,cname,ty list,ty,nat,nat,instr list,certificate] => bool"
- "wtl_method G C pTs rT mxs mxl ins cert ==
+ wtl_method :: "[jvm_prog,cname,ty list,ty,nat,nat,exception_table,instr list,certificate] => bool"
+ "wtl_method G C pTs rT mxs mxl et ins cert ==
let max_pc = length ins
in
0 < max_pc \<and>
- wtl_inst_list ins G rT cert mxs max_pc 0
+ wtl_inst_list ins G rT cert mxs mxl max_pc et 0
(Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err))) \<noteq> Err"
wtl_jvm_prog :: "[jvm_prog,prog_certificate] => bool"
"wtl_jvm_prog G cert ==
- wf_prog (\<lambda>G C (sig,rT,maxs,maxl,b). wtl_method G C (snd sig) rT maxs maxl b (cert C sig)) G"
+ wf_prog (\<lambda>G C (sig,rT,maxs,maxl,b,et). wtl_method G C (snd sig) rT maxs maxl et b (cert C sig)) G"
lemmas [iff] = not_Err_eq
+lemma if_eq_cases:
+ "(P \<Longrightarrow> x = z) \<Longrightarrow> (\<not>P \<Longrightarrow> y = z) \<Longrightarrow> (if P then x else y) = z"
+ by simp
+
+lemma merge_def:
+ "!!x. merge G pc mxs mxr max_pc cert ss x =
+ (if \<forall>(pc',s') \<in> set ss. pc' < max_pc \<and> (pc' \<noteq> pc+1 \<longrightarrow> G \<turnstile> s' <=' cert!pc') then
+ map (OK \<circ> snd) [(p',t') \<in> ss. p'=pc+1] ++_(sup G mxs mxr) x
+ else Err)" (is "!!x. ?merge ss x = ?if ss x" is "!!x. ?P ss x")
+proof (induct ss)
+ show "!!x. ?P [] x" by simp
+next
+ have OK_snd: "(\<lambda>u. OK (snd u)) = OK \<circ> snd" by (rule ext) auto
+ fix x ss and s::"nat \<times> (state_type option)"
+ assume IH: "\<And>x. ?P ss x"
+ obtain pc' s' where s: "s = (pc',s')" by (cases s)
+ hence "?merge (s#ss) x = ?merge ((pc',s')#ss) x" by hypsubst (rule refl)
+ also
+ have "\<dots> = (if pc' < max_pc \<and> pc' = pc+1 then
+ ?merge ss (OK s' +_(sup G mxs mxr) x)
+ else if pc' < max_pc \<and> G \<turnstile> s' <=' cert!pc' then
+ ?merge ss x
+ else Err)"
+ (is "_ = (if ?pc' then ?merge ss (_ +_?f _) else if ?G then _ else _)")
+ by simp
+ also
+ let "if ?all ss then _ else _" = "?if ss x"
+ have "\<dots> = ?if ((pc',s')#ss) x"
+ proof (cases "?pc'")
+ case True
+ hence "?all (((pc',s')#ss)) = (pc+1 < max_pc \<and> ?all ss)" by simp
+ with True
+ have "?if ss (OK s' +_?f x) = ?if ((pc',s')#ss) x" by (auto simp add: OK_snd)
+ hence "?merge ss (OK s' +_?f x) = ?if ((pc',s')#ss) x" by (simp only: IH)
+ with True show ?thesis by (fast intro: if_eq_cases)
+ next
+ case False
+ have "(if ?G then ?merge ss x else Err) = ?if ((pc',s')#ss) x"
+ proof (cases ?G)
+ assume G: ?G with False
+ have "?if ss x = ?if ((pc',s')#ss) x" by (auto simp add: OK_snd)
+ hence "?merge ss x = ?if ((pc',s')#ss) x" by (simp only: IH)
+ with G show ?thesis by (fast intro: if_eq_cases)
+ next
+ assume G: "\<not>?G"
+ with False have "Err = ?if ((pc',s')#ss) x" by auto
+ with G show ?thesis by (fast intro: if_eq_cases)
+ qed
+ with False show ?thesis by (fast intro: if_eq_cases)
+ qed
+ also from s have "\<dots> = ?if (s#ss) x" by hypsubst (rule refl)
+ finally show "?P (s#ss) x" .
+qed
+
lemma wtl_inst_OK:
-"(wtl_inst i G rT s cert maxs max_pc pc = OK s') =
- (app i G maxs rT s \<and> (\<forall>pc' \<in> set (succs i pc).
- pc' < max_pc \<and> (pc' \<noteq> pc+1 --> G \<turnstile> step i G s <=' cert!pc')) \<and>
- (if pc+1 \<in> set (succs i pc) then s' = step i G s else s' = cert!(pc+1)))"
- by (auto simp add: wtl_inst_def check_cert_def set_mem_eq)
+"(wtl_inst i G rT s cert mxs mxr max_pc et pc = OK s') = (
+ app i G mxs rT pc et s \<and>
+ (\<forall>(pc',r) \<in> set (eff i G pc et s).
+ pc' < max_pc \<and> (pc' \<noteq> pc+1 \<longrightarrow> G \<turnstile> r <=' cert!pc')) \<and>
+ map (OK \<circ> snd) [(p',t') \<in> (eff i G pc et s). p'=pc+1]
+ ++_(sup G mxs mxr) (OK (cert!(pc+1))) = OK s')"
+ by (auto simp add: wtl_inst_def merge_def split: split_if_asm)
lemma wtl_Cons:
- "wtl_inst_list (i#is) G rT cert maxs max_pc pc s \<noteq> Err =
- (\<exists>s'. wtl_cert i G rT s cert maxs max_pc pc = OK s' \<and>
- wtl_inst_list is G rT cert maxs max_pc (pc+1) s' \<noteq> Err)"
+ "wtl_inst_list (i#is) G rT cert maxs maxr max_pc et pc s \<noteq> Err =
+ (\<exists>s'. wtl_cert i G rT s cert maxs maxr max_pc et pc = OK s' \<and>
+ wtl_inst_list is G rT cert maxs maxr max_pc et (pc+1) s' \<noteq> Err)"
by (auto simp del: split_paired_Ex)
lemma wtl_append:
-"\<forall> s pc. (wtl_inst_list (a@b) G rT cert mxs mpc pc s = OK s') =
- (\<exists>s''. wtl_inst_list a G rT cert mxs mpc pc s = OK s'' \<and>
- wtl_inst_list b G rT cert mxs mpc (pc+length a) s'' = OK s')"
+"\<forall> s pc. (wtl_inst_list (a@b) G rT cert mxs mxr mpc et pc s = OK s') =
+ (\<exists>s''. wtl_inst_list a G rT cert mxs mxr mpc et pc s = OK s'' \<and>
+ wtl_inst_list b G rT cert mxs mxr mpc et (pc+length a) s'' = OK s')"
(is "\<forall> s pc. ?C s pc a" is "?P a")
proof (induct ?P a)
-
show "?P []" by simp
-
- fix x xs
- assume IH: "?P xs"
-
+next
+ fix x xs assume IH: "?P xs"
show "?P (x#xs)"
proof (intro allI)
fix s pc
-
show "?C s pc (x#xs)"
- proof (cases "wtl_cert x G rT s cert mxs mpc pc")
+ proof (cases "wtl_cert x G rT s cert mxs mxr mpc et pc")
case Err thus ?thesis by simp
next
- fix s0
- assume OK: "wtl_cert x G rT s cert mxs mpc pc = OK s0"
-
- with IH
- have "?C s0 (Suc pc) xs" by blast
-
- with OK
- show ?thesis by simp
+ fix s0 assume "wtl_cert x G rT s cert mxs mxr mpc et pc = OK s0"
+ with IH have "?C s0 (Suc pc) xs" by blast
+ thus ?thesis by (simp!)
qed
qed
qed
lemma wtl_take:
- "wtl_inst_list is G rT cert mxs mpc pc s = OK s'' ==>
- \<exists>s'. wtl_inst_list (take pc' is) G rT cert mxs mpc pc s = OK s'"
+ "wtl_inst_list is G rT cert mxs mxr mpc et pc s = OK s'' ==>
+ \<exists>s'. wtl_inst_list (take pc' is) G rT cert mxs mxr mpc et pc s = OK s'"
proof -
- assume "wtl_inst_list is G rT cert mxs mpc pc s = OK s''"
-
- hence "wtl_inst_list (take pc' is @ drop pc' is) G rT cert mxs mpc pc s = OK s''"
+ assume "wtl_inst_list is G rT cert mxs mxr mpc et pc s = OK s''"
+ hence "wtl_inst_list (take pc' is @ drop pc' is) G rT cert mxs mxr mpc et pc s = OK s''"
by simp
-
- thus ?thesis
- by (auto simp add: wtl_append simp del: append_take_drop_id)
+ thus ?thesis by (auto simp add: wtl_append simp del: append_take_drop_id)
qed
lemma take_Suc:
"\<forall>n. n < length l --> take (Suc n) l = (take n l)@[l!n]" (is "?P l")
proof (induct l)
show "?P []" by simp
-
- fix x xs
- assume IH: "?P xs"
-
+next
+ fix x xs assume IH: "?P xs"
show "?P (x#xs)"
proof (intro strip)
- fix n
- assume "n < length (x#xs)"
- with IH
- show "take (Suc n) (x # xs) = take n (x # xs) @ [(x # xs) ! n]"
- by - (cases n, auto)
+ fix n assume "n < length (x#xs)"
+ with IH show "take (Suc n) (x # xs) = take n (x # xs) @ [(x # xs) ! n]"
+ by (cases n, auto)
qed
qed
lemma wtl_Suc:
- "[| wtl_inst_list (take pc is) G rT cert maxs (length is) 0 s = OK s';
- wtl_cert (is!pc) G rT s' cert maxs (length is) pc = OK s'';
+ "[| wtl_inst_list (take pc is) G rT cert maxs maxr (length is) et 0 s = OK s';
+ wtl_cert (is!pc) G rT s' cert maxs maxr (length is) et pc = OK s'';
Suc pc < length is |] ==>
- wtl_inst_list (take (Suc pc) is) G rT cert maxs (length is) 0 s = OK s''"
+ wtl_inst_list (take (Suc pc) is) G rT cert maxs maxr (length is) et 0 s = OK s''"
proof -
- assume wtt: "wtl_inst_list (take pc is) G rT cert maxs (length is) 0 s = OK s'"
- assume wtc: "wtl_cert (is!pc) G rT s' cert maxs (length is) pc = OK s''"
- assume pc: "Suc pc < length is"
-
- hence "take (Suc pc) is = (take pc is)@[is!pc]"
- by (simp add: take_Suc)
-
- with wtt wtc pc
- show ?thesis
- by (simp add: wtl_append min_def)
+ assume "wtl_inst_list (take pc is) G rT cert maxs maxr (length is) et 0 s = OK s'"
+ "wtl_cert (is!pc) G rT s' cert maxs maxr (length is) et pc = OK s''"
+ "Suc pc < length is"
+ hence "take (Suc pc) is = (take pc is)@[is!pc]" by (simp add: take_Suc)
+ thus ?thesis by (simp! add: wtl_append min_def)
qed
lemma wtl_all:
- "[| wtl_inst_list is G rT cert maxs (length is) 0 s \<noteq> Err;
+ "[| wtl_inst_list is G rT cert maxs maxr (length is) et 0 s \<noteq> Err;
pc < length is |] ==>
- \<exists>s' s''. wtl_inst_list (take pc is) G rT cert maxs (length is) 0 s = OK s' \<and>
- wtl_cert (is!pc) G rT s' cert maxs (length is) pc = OK s''"
+ \<exists>s' s''. wtl_inst_list (take pc is) G rT cert maxs maxr (length is) et 0 s = OK s' \<and>
+ wtl_cert (is!pc) G rT s' cert maxs maxr (length is) et pc = OK s''"
proof -
- assume all: "wtl_inst_list is G rT cert maxs (length is) 0 s \<noteq> Err"
+ assume all: "wtl_inst_list is G rT cert maxs maxr (length is) et 0 s \<noteq> Err"
assume pc: "pc < length is"
hence "0 < length (drop pc is)" by simp
- then
- obtain i r where
- Cons: "drop pc is = i#r"
+ then obtain i r where Cons: "drop pc is = i#r"
by (auto simp add: neq_Nil_conv simp del: length_drop)
hence "i#r = drop pc is" ..
- with all
- have take: "wtl_inst_list (take pc is@i#r) G rT cert maxs (length is) 0 s \<noteq> Err"
+ with all have take:
+ "wtl_inst_list (take pc is@i#r) G rT cert maxs maxr (length is) et 0 s \<noteq> Err"
by simp
- from pc
- have "is!pc = drop pc is ! 0" by simp
- with Cons
- have "is!pc = i" by simp
-
- with take pc
- show ?thesis
- by (auto simp add: wtl_append min_def)
+ from pc have "is!pc = drop pc is ! 0" by simp
+ with Cons have "is!pc = i" by simp
+ with take pc show ?thesis by (auto simp add: wtl_append min_def)
qed