Up to index of Isabelle/HOL/arrays
theory Effect = JVMType + JVMExec:(* Title: HOL/MicroJava/BV/Effect.thy
ID: $Id: Effect.html,v 1.1 2002/11/28 16:11:18 kleing Exp $
Author: Gerwin Klein
Copyright 2000 Technische Universitaet Muenchen
*)
header {* \isaheader{Effect of Instructions on the State Type} *}
theory Effect = JVMType + JVMExec:
types
succ_type = "(p_count × address_type) list"
consts
the_RA :: "init_ty err \<Rightarrow> nat"
recdef the_RA "{}"
"the_RA (OK (Init (RA pc))) = pc"
constdefs
theRA :: "nat \<Rightarrow> state_bool \<Rightarrow> nat"
"theRA x s \<equiv> the_RA (snd (fst s)!x)"
text {* Program counter of successor instructions: *}
consts
succs :: "instr \<Rightarrow> p_count \<Rightarrow> address_type \<Rightarrow> p_count list"
primrec
"succs (Load idx) pc s = [pc+1]"
"succs (Store idx) pc s = [pc+1]"
"succs (LitPush v) pc s = [pc+1]"
"succs (Getfield F C) pc s = [pc+1]"
"succs (Putfield F C) pc s = [pc+1]"
"succs (New C) pc s = [pc+1]"
"succs (Checkcast C) pc s = [pc+1]"
"succs Pop pc s = [pc+1]"
"succs Dup pc s = [pc+1]"
"succs Dup_x1 pc s = [pc+1]"
"succs Dup_x2 pc s = [pc+1]"
"succs Swap pc s = [pc+1]"
"succs IAdd pc s = [pc+1]"
"succs (Ifcmpeq b) pc s = [pc+1, nat (int pc + b)]"
"succs (Goto b) pc s = [nat (int pc + b)]"
"succs Return pc s = []"
"succs (Invoke C mn fpTs) pc s = [pc+1]"
"succs (Invoke_special C mn fpTs) pc s
= [pc+1]"
"succs Throw pc s = []"
"succs (Jsr b) pc s = [nat (int pc + b)]"
"succs (Ret x) pc s = (SOME l. set l = theRA x ` s)"
"succs ArrLoad pc s = [pc+1]"
"succs ArrStore pc s = [pc+1]"
"succs ArrLength pc s = [pc+1]"
"succs (ArrNew C) pc s = [pc+1]"
consts theClass :: "init_ty \<Rightarrow> ty"
primrec
"theClass (PartInit C) = Class C"
"theClass (UnInit C pc) = Class C"
text "Effect of instruction on the state type:"
consts
eff' :: "instr × jvm_prog × p_count × state_type \<Rightarrow> state_type"
recdef eff' "{}"
"eff' (Load idx, G, pc, (ST, LT)) = (ok_val (LT ! idx) # ST, LT)"
"eff' (Store idx, G, pc, (ts#ST, LT)) = (ST, LT[idx:= OK ts])"
"eff' (LitPush v, G, pc, (ST, LT)) = (Init (the (typeof (\<lambda>v. None) v))#ST, LT)"
"eff' (Getfield F C, G, pc, (oT#ST, LT)) = (Init (snd (the (field (G,C) F)))#ST, LT)"
"eff' (Putfield F C, G, pc, (vT#oT#ST, LT)) = (ST,LT)"
"eff' (New C, G, pc, (ST,LT)) = (UnInit C pc # ST, replace (OK (UnInit C pc)) Err LT)"
"eff' (Checkcast C,G,pc,(Init (RefT t)#ST,LT)) = (Init (Class C) # ST,LT)"
"eff' (Pop, G, pc, (ts#ST,LT)) = (ST,LT)"
"eff' (Dup, G, pc, (ts#ST,LT)) = (ts#ts#ST,LT)"
"eff' (Dup_x1, G, pc, (ts1#ts2#ST,LT)) = (ts1#ts2#ts1#ST,LT)"
"eff' (Dup_x2, G, pc, (ts1#ts2#ts3#ST,LT)) = (ts1#ts2#ts3#ts1#ST,LT)"
"eff' (Swap, G, pc, (ts1#ts2#ST,LT)) = (ts2#ts1#ST,LT)"
"eff' (IAdd, G, pc, (t1#t2#ST,LT)) = (Init (PrimT Integer)#ST,LT)"
"eff' (Ifcmpeq b, G, pc, (ts1#ts2#ST,LT)) = (ST,LT)"
"eff' (Goto b, G, pc, s) = s"
-- "Return has no successor instruction in the same method:"
"eff' (Return, G, pc, s) = s"
-- "Throw always terminates abruptly:"
"eff' (Throw, G, pc, s) = s"
"eff' (Jsr t, G, pc, (ST,LT)) = ((Init (RA (pc+1)))#ST,LT)"
"eff' (Ret x, G, pc, s) = s"
"eff' (ArrLoad, G, pc, (idx#Init (T.[])#ST,LT)) = (Init T#ST,LT)"
"eff' (ArrStore, G, pc, (vT#idx#aT#ST,LT)) = (ST,LT)"
"eff' (ArrLength, G, pc, (aT#ST,LT)) = (Init (PrimT Integer)#ST,LT)"
"eff' (ArrNew T, G, pc, (len#ST,LT)) = (Init (T.[])#ST,LT)"
"eff' (Invoke C mn fpTs, G, pc, (ST,LT)) =
(let ST' = drop (length fpTs) ST;
X = hd ST';
ST'' = tl ST';
rT = fst (snd (the (method (G,C) (mn,fpTs))))
in ((Init rT)#ST'', LT))"
"eff' (Invoke_special C mn fpTs, G, pc, (ST,LT)) =
(let ST' = drop (length fpTs) ST;
X = hd ST';
N = Init (theClass X);
ST'' = replace X N (tl ST');
LT' = replace (OK X) (OK N) LT;
rT = fst (snd (the (method (G,C) (mn,fpTs))))
in ((Init rT)#ST'', LT'))"
text {*
For @{term Invoke_special} only: mark when invoking a
constructor on a partly initialized class. app will check that we
call the right constructor.
*}
constdefs
eff_bool :: "instr \<Rightarrow> jvm_prog \<Rightarrow> p_count \<Rightarrow> state_bool \<Rightarrow> state_bool"
"eff_bool i G pc == \<lambda>((ST,LT),z). (eff'(i,G,pc,(ST,LT)),
if \<exists>C p D. i = Invoke_special C init p \<and> ST!length p = PartInit D then True else z)"
text {*
For exception handling:
*}
consts
match_any :: "jvm_prog \<Rightarrow> p_count \<Rightarrow> exception_table \<Rightarrow> 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 \<and> pc < end_pc then catch_type#es' else es')"
consts
match :: "jvm_prog \<Rightarrow> cname \<Rightarrow> p_count \<Rightarrow> exception_table \<Rightarrow> cname list"
primrec
"match G X pc [] = []"
"match G X pc (e#es) =
(if match_exception_entry G X pc e then [X] else match G X pc es)"
lemma match_some_entry:
"match G X pc et = (if \<exists>e \<in> set et. match_exception_entry G X pc e then [X] else [])"
by (induct et) auto
consts
xcpt_names :: "instr × jvm_prog × p_count × exception_table \<Rightarrow> cname list"
recdef xcpt_names "{}"
"xcpt_names (Getfield F C, G, pc, et) = match G (Xcpt NullPointer) pc et"
"xcpt_names (Putfield F C, G, pc, et) = match G (Xcpt NullPointer) pc et"
"xcpt_names (New C, G, pc, et) = match G (Xcpt OutOfMemory) pc et"
"xcpt_names (Checkcast C, G, pc, et) = match G (Xcpt ClassCast) pc et"
"xcpt_names (ArrLoad, G, pc, et) = match G (Xcpt ArrayIndexOutOfBounds) pc et @ (match G (Xcpt NullPointer) pc et)"
"xcpt_names (ArrStore, G, pc, et) = match G (Xcpt ArrayIndexOutOfBounds) pc et @ (match G (Xcpt NullPointer) pc et) @ (match G (Xcpt ArrayStore) pc et)"
"xcpt_names (ArrLength, G, pc, et) = match G (Xcpt NullPointer) pc et"
"xcpt_names (ArrNew C, G, pc, et) = match G (Xcpt OutOfMemory) pc et @ (match G (Xcpt NegativeArraySize) pc et)"
"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 (Invoke_special C m p, G, pc, et) = match_any G pc et"
"xcpt_names (i, G, pc, et) = []"
consts
theIdx :: "instr \<Rightarrow> nat"
primrec
"theIdx (Load idx) = idx"
"theIdx (Store idx) = idx"
"theIdx (Ret idx) = idx"
constdefs
xcpt_eff :: "instr \<Rightarrow> jvm_prog \<Rightarrow> p_count \<Rightarrow> address_type \<Rightarrow> exception_table \<Rightarrow> succ_type"
"xcpt_eff i G pc at et \<equiv>
map (\<lambda>C. (the (match_exception_table G C pc et), (\<lambda>s. (([Init (Class C)], snd (fst s)),snd s))`at ))
(xcpt_names (i,G,pc,et))"
norm_eff :: "instr \<Rightarrow> jvm_prog \<Rightarrow> p_count \<Rightarrow> p_count \<Rightarrow> address_type \<Rightarrow> address_type"
"norm_eff i G pc pc' at \<equiv> (eff_bool i G pc) ` (if \<exists>idx. i = Ret idx then
{s. s\<in>at \<and> pc' = theRA (theIdx i) s} else at)"
text {*
Putting it all together:
*}
constdefs
eff :: "instr \<Rightarrow> jvm_prog \<Rightarrow> p_count \<Rightarrow> exception_table \<Rightarrow> address_type \<Rightarrow> succ_type"
"eff i G pc et at \<equiv> (map (\<lambda>pc'. (pc',norm_eff i G pc pc' at)) (succs i pc at)) @ (xcpt_eff i G pc at et)"
text {*
Some small helpers for direct executability
*}
constdefs
isPrimT :: "ty \<Rightarrow> bool"
"isPrimT T \<equiv> case T of PrimT T' \<Rightarrow> True | RefT T' \<Rightarrow> False"
isRefT :: "ty \<Rightarrow> bool"
"isRefT T \<equiv> case T of PrimT T' \<Rightarrow> False | RefT T' \<Rightarrow> True"
lemma isPrimT [simp]:
"isPrimT T = (\<exists>T'. T = PrimT T')" by (simp add: isPrimT_def split: ty.splits)
lemma isRefT [simp]:
"isRefT T = (\<exists>T'. T = RefT T')" by (simp add: isRefT_def split: ty.splits)
text "Conditions under which eff is applicable:"
consts
app' :: "instr × jvm_prog × cname × p_count × nat × ty × state_type \<Rightarrow> bool"
recdef app' "{}"
"app' (Load idx, G, C', pc, maxs, rT, s)
= (idx < length (snd s) \<and> (snd s) ! idx \<noteq> Err \<and> length (fst s) < maxs)"
"app' (Store idx, G, C', pc, maxs, rT, (ts#ST, LT))
= (idx < length LT)"
"app' (LitPush v, G, C', pc, maxs, rT, s)
= (length (fst s) < maxs \<and> typeof (\<lambda>t. None) v \<in> {Some NT} \<union> (Some\<circ>PrimT)`{Boolean,Void,Integer})"
"app' (Getfield F C, G, C', pc, maxs, rT, (oT#ST, LT))
= (is_class G C \<and> field (G,C) F \<noteq> None \<and> fst (the (field (G,C) F)) = C \<and>
G \<turnstile> oT \<preceq>i Init (Class C))"
"app' (Putfield F C, G, C', pc, maxs, rT, (vT#oT#ST, LT))
= (is_class G C \<and> field (G,C) F \<noteq> None \<and> fst (the (field (G,C) F)) = C \<and>
G \<turnstile> oT \<preceq>i Init (Class C) \<and> G \<turnstile> vT \<preceq>i Init (snd (the (field (G,C) F))))"
"app' (New C, G, C', pc, maxs, rT, s)
= (is_class G C \<and> length (fst s) < maxs \<and> UnInit C pc \<notin> set (fst s))"
"app' (Checkcast C, G, C', pc, maxs, rT, (Init (RefT rt)#ST,LT))
= is_class G C"
"app' (Pop, G, C', pc, maxs, rT, (ts#ST,LT)) = True"
"app' (Dup, G, C', pc, maxs, rT, (ts#ST,LT)) = (1+length ST < maxs)"
"app' (Dup_x1, G, C', pc, maxs, rT, (ts1#ts2#ST,LT)) = (2+length ST < maxs)"
"app' (Dup_x2, G, C', pc, maxs, rT, (ts1#ts2#ts3#ST,LT)) = (3+length ST < maxs)"
"app' (Swap, G, C', pc, maxs, rT, (ts1#ts2#ST,LT)) = True"
"app' (IAdd, G, C', pc, maxs, rT, (t1#t2#ST,LT))
= (t1 = Init (PrimT Integer) \<and> t1 = t2)"
"app' (Ifcmpeq b, G, C', pc, maxs, rT, (Init ts#Init ts'#ST,LT))
= (0 \<le> int pc + b \<and> (isPrimT ts \<longrightarrow> ts' = ts) \<and> (isRefT ts \<longrightarrow> isRefT ts'))"
"app' (Goto b, G, C', pc, maxs, rT, s) = (0 \<le> int pc + b)"
"app' (Return, G, C', pc, maxs, rT, (T#ST,LT)) = (G \<turnstile> T \<preceq>i Init rT)"
"app' (Throw, G, C', pc, maxs, rT, (Init T#ST,LT)) = isRefT T"
"app' (Jsr b, G, C', pc, maxs, rT, (ST,LT)) = (0 \<le> int pc + b \<and> length ST < maxs)"
"app' (Ret x, G, C', pc, maxs, rT, (ST,LT)) = (x < length LT \<and> (\<exists>r. LT!x=OK (Init (RA r))))"
"app' (ArrLoad, G, C', pc, maxs, rT, (idx#Init (T.[])#ST,LT)) =
(idx = Init (PrimT Integer))"
"app' (ArrStore, G, C', pc, maxs, rT, (Init T#idx#Init (T'.[])#ST,LT)) =
(idx = Init (PrimT Integer))"
"app' (ArrLength, G, C', pc, maxs, rT, (Init (T.[])#ST, LT)) = True"
"app' (ArrNew T, G, C', pc, maxs, rT, (len#ST,LT)) =
(len = Init (PrimT Integer) \<and> is_type G T \<and> noRA T \<and> dim T+1 \<le> max_dim)"
"app' (Invoke C mn fpTs, G, C', pc, maxs, rT, s) =
(length fpTs < length (fst s) \<and> mn \<noteq> init \<and>
(let apTs = rev (take (length fpTs) (fst s));
X = hd (drop (length fpTs) (fst s))
in is_class G C \<and>
list_all2 (\<lambda>aT fT. G \<turnstile> aT \<preceq>i (Init fT)) apTs fpTs \<and>
G \<turnstile> X \<preceq>i Init (Class C)) \<and>
method (G,C) (mn,fpTs) \<noteq> None)"
"app' (Invoke_special C mn fpTs, G, C', pc, maxs, rT, s) =
(length fpTs < length (fst s) \<and> mn = init \<and>
(let apTs = rev (take (length fpTs) (fst s));
X = (fst s)!length fpTs
in is_class G C \<and>
list_all2 (\<lambda>aT fT. G \<turnstile> aT \<preceq>i (Init fT)) apTs fpTs \<and>
(\<exists>rT' b. method (G,C) (mn,fpTs) = Some (C,rT',b)) \<and>
((\<exists>pc. X = UnInit C pc) \<or> (X = PartInit C' \<and> G \<turnstile> C' \<prec>C1 C))))"
-- "@{text C'} is the current class, the constructor must be called on the"
-- "superclass (if partly initialized) or on the exact class that is"
-- "to be constructed (if not yet initialized at all)."
-- "In JCVM @{text Invoke_special} may also call another constructor of the same"
-- {* class (@{text "C = C' \<or> C = super C'"}) *}
"app' (i,G,pc,maxs,rT,s) = False"
constdefs
xcpt_app :: "instr \<Rightarrow> jvm_prog \<Rightarrow> nat \<Rightarrow> exception_table \<Rightarrow> bool"
"xcpt_app i G pc et \<equiv> \<forall>C\<in>set(xcpt_names (i,G,pc,et)). is_class G C"
constdefs
app :: "instr \<Rightarrow> jvm_prog \<Rightarrow> cname \<Rightarrow> p_count \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> bool \<Rightarrow>
exception_table \<Rightarrow> address_type \<Rightarrow> bool"
"app i G C' pc mxs mpc rT ini et at \<equiv> (\<forall>(s,z) \<in> at.
xcpt_app i G pc et \<and>
app' (i,G,C',pc,mxs,rT,s) \<and>
(ini \<and> i = Return \<longrightarrow> z) \<and>
(\<forall>C m p. i = Invoke_special C m p \<and> (fst s)!length p = PartInit C' \<longrightarrow> ¬z)) \<and>
(\<forall>(pc',s') \<in> set (eff i G pc et at). pc' < mpc)"
lemma match_any_match_table:
"C \<in> set (match_any G pc et) \<Longrightarrow> match_exception_table G C pc et \<noteq> None"
apply (induct et)
apply simp
apply simp
apply clarify
apply (simp split: split_if_asm)
apply (auto simp add: match_exception_entry_def)
done
lemma match_X_match_table:
"C \<in> set (match G X pc et) \<Longrightarrow> match_exception_table G C pc et \<noteq> None"
apply (induct et)
apply simp
apply (simp split: split_if_asm)
done
lemma xcpt_names_in_et:
"C \<in> set (xcpt_names (i,G,pc,et)) \<Longrightarrow>
\<exists>e \<in> set et. the (match_exception_table G C pc et) = fst (snd (snd e))"
apply (cases i)
apply (auto dest!: match_any_match_table match_X_match_table
dest: match_exception_table_in_et)
done
lemma length_casesE1:
"((xs,y),z) \<in> at \<Longrightarrow>
(xs =[] \<Longrightarrow> P []) \<Longrightarrow>
(\<And>l. xs = [l] \<Longrightarrow> P [l]) \<Longrightarrow>
(\<And>l l'. xs = [l,l'] \<Longrightarrow> P [l,l']) \<Longrightarrow>
(\<And>l l' ls. xs = l#l'#ls \<Longrightarrow> P (l#l'#ls))
\<Longrightarrow> P xs"
apply (cases xs)
apply auto
apply (rename_tac ls)
apply (case_tac ls)
apply auto
done
lemmas [simp] = app_def xcpt_app_def
text {*
\medskip
simp rules for @{term app}
*}
lemma appNone[simp]: "app i G C' pc maxs mpc rT ini et {} = (\<forall>(pc',s')\<in>set (eff i G pc et {}). pc' < mpc)"
by simp
lemmas eff_defs [simp] = eff_def norm_eff_def eff_bool_def xcpt_eff_def
lemma appLoad[simp]:
"app (Load idx) G C' pc maxs mpc rT ini et at = (Suc pc < mpc \<and> (\<forall>s \<in> at.
(\<exists>ST LT z. s = ((ST,LT),z) \<and> idx < length LT \<and> LT!idx \<noteq> Err \<and> length ST < maxs)))"
by auto
lemma appStore[simp]:
"app (Store idx) G C' pc maxs mpc rT ini et at = (Suc pc < mpc \<and> (\<forall>s \<in> at. \<exists>ts ST LT z. s = ((ts#ST,LT),z) \<and> idx < length LT))"
apply auto
apply (auto dest!: bspec elim!: length_casesE1)
done
lemma appLitPush[simp]:
"app (LitPush v) G C' pc maxs mpc rT ini et at = (Suc pc < mpc \<and>
(\<forall>s \<in> at. \<exists>ST LT z. s = ((ST,LT),z) \<and> length ST < maxs \<and>
typeof (\<lambda>v. None) v \<in> {Some NT} \<union> (Some\<circ>PrimT)`{Void,Boolean,Integer}))"
by auto
lemma appGetField[simp]:
"app (Getfield F C) G C' pc maxs mpc rT ini et at = (Suc pc < mpc \<and>
(\<forall>x \<in> set (match G (Xcpt NullPointer) pc et). the (match_exception_table G x pc et) < mpc) \<and>
(\<forall>s \<in> at. \<exists>oT vT ST LT z. s = ((oT#ST, LT),z) \<and> is_class G C \<and>
field (G,C) F = Some (C,vT) \<and> G \<turnstile> oT \<preceq>i (Init (Class C)) \<and>
(\<forall>x \<in> set (match G (Xcpt NullPointer) pc et). is_class G x)))"
apply rule
defer
apply (clarsimp, (drule bspec, assumption)?)+
apply (auto elim!: length_casesE1)
done
lemma appPutField[simp]:
"app (Putfield F C) G C' pc maxs mpc rT ini et at = (Suc pc < mpc \<and>
(\<forall>x \<in> set (match G (Xcpt NullPointer) pc et). the (match_exception_table G x pc et) < mpc) \<and>
(\<forall>s \<in> at. \<exists>vT vT' oT ST LT z. s = ((vT#oT#ST, LT),z) \<and> is_class G C \<and>
field (G,C) F = Some (C, vT') \<and>
G \<turnstile> oT \<preceq>i Init (Class C) \<and> G \<turnstile> vT \<preceq>i Init vT' \<and>
(\<forall>x \<in> set (match G (Xcpt NullPointer) pc et). is_class G x)))"
apply rule
defer
apply (clarsimp, (drule bspec, assumption)?)+
apply (auto elim!: length_casesE1)
done
lemma appNew[simp]:
"app (New C) G C' pc maxs mpc rT ini et at = (Suc pc < mpc \<and>
(\<forall>x \<in> set (match G (Xcpt OutOfMemory) pc et). the (match_exception_table G x pc et) < mpc) \<and>
(\<forall>s \<in> at. \<exists>ST LT z. s=((ST,LT),z) \<and>
is_class G C \<and> length ST < maxs \<and>
UnInit C pc \<notin> set ST \<and>
(\<forall>x \<in> set (match G (Xcpt OutOfMemory) pc et). is_class G x)))"
by auto
lemma appCheckcast[simp]:
"app (Checkcast C) G C' pc maxs mpc rT ini et at = (Suc pc < mpc \<and>
(\<forall>x \<in> set (match G (Xcpt ClassCast) pc et). the (match_exception_table G x pc et) < mpc) \<and>
(\<forall>s \<in> at. \<exists>rT ST LT z. s = ((Init (RefT rT)#ST,LT),z) \<and> is_class G C \<and>
(\<forall>x \<in> set (match G (Xcpt ClassCast) pc et). is_class G x)))"
apply rule
apply clarsimp
defer
apply clarsimp
apply (drule bspec, assumption)
apply clarsimp
apply (drule bspec, assumption)
apply clarsimp
apply (case_tac a)
apply auto
apply (case_tac aa)
apply auto
apply (case_tac ty)
apply auto
apply (case_tac aa)
apply auto
apply (case_tac ty)
apply auto
done
lemma appPop[simp]:
"app Pop G C' pc maxs mpc rT ini et at = (Suc pc < mpc \<and> (\<forall>s \<in> at. \<exists>ts ST LT z. s = ((ts#ST,LT),z)))"
by auto (auto dest!: bspec elim!: length_casesE1)
lemma appDup[simp]:
"app Dup G C' pc maxs mpc rT ini et at = (Suc pc < mpc \<and>
(\<forall>s \<in> at. \<exists>ts ST LT z. s = ((ts#ST,LT),z) \<and> 1+length ST < maxs))"
by auto (auto dest!: bspec elim!: length_casesE1)
lemma appDup_x1[simp]:
"app Dup_x1 G C' pc maxs mpc rT ini et at = (Suc pc < mpc \<and>
(\<forall>s \<in> at. \<exists>ts1 ts2 ST LT z. s = ((ts1#ts2#ST,LT),z) \<and> 2+length ST < maxs))"
by auto (auto dest!: bspec elim!: length_casesE1)
lemma appDup_x2[simp]:
"app Dup_x2 G C' pc maxs mpc rT ini et at = (Suc pc < mpc \<and>
(\<forall>s \<in> at. \<exists>ts1 ts2 ts3 ST LT z. s = ((ts1#ts2#ts3#ST,LT),z) \<and> 3+length ST < maxs))"
apply auto
apply (auto dest!: bspec elim!: length_casesE1)
apply (case_tac ls, auto)
done
lemma appSwap[simp]:
"app Swap G C' pc maxs mpc rT ini et at = (Suc pc < mpc \<and>
(\<forall>s \<in> at. \<exists>ts1 ts2 ST LT z. s = ((ts1#ts2#ST,LT),z)))"
by auto (auto dest!: bspec elim!: length_casesE1)
lemma appIAdd[simp]:
"app IAdd G C' pc maxs mpc rT ini et at = (Suc pc < mpc \<and>
(\<forall>s \<in> at. \<exists>ST LT z. s = ((Init (PrimT Integer)#Init (PrimT Integer)#ST,LT),z)))"
by auto (auto dest!: bspec elim!: length_casesE1)
lemma appIfcmpeq[simp]:
"app (Ifcmpeq b) G C' pc maxs mpc rT ini et at = (Suc pc < mpc \<and> nat (int pc+b) < mpc \<and>
(\<forall>s \<in> at. \<exists>ts1 ts2 ST LT z. s = ((Init ts1#Init ts2#ST,LT),z) \<and> 0 \<le> b + int pc \<and>
((\<exists>p. ts1 = PrimT p \<and> ts2 = PrimT p) \<or>
(\<exists>r r'. ts1 = RefT r \<and> ts2 = RefT r'))))"
apply auto
apply (auto dest!: bspec)
apply (case_tac aa, simp)
apply (case_tac list)
apply (case_tac a, simp, simp, simp)
apply (case_tac a)
apply simp
apply (case_tac ab)
apply auto
apply (case_tac ty, auto)
apply (case_tac ty, auto)
apply (case_tac ty, auto)
apply (case_tac ty, auto)
apply (case_tac ty, auto)
done
lemma appReturn[simp]:
"app Return G C' pc maxs mpc rT ini et at =
(\<forall>s \<in> at. \<exists>T ST LT z. s = ((T#ST,LT),z) \<and> (G \<turnstile> T \<preceq>i Init rT) \<and> (ini \<longrightarrow> z))"
apply auto
apply (auto dest!: bspec)
apply (erule length_casesE1)
apply auto
apply (erule length_casesE1)
apply auto
done
lemma appGoto[simp]:
"app (Goto b) G C' pc maxs mpc rT ini et at =
(nat (int pc + b) < mpc \<and> (at \<noteq> {} \<longrightarrow> 0 \<le> int pc + b))"
by auto
lemma appThrow[simp]:
"app Throw G C' pc maxs mpc rT ini et at =
((\<forall>C \<in> set (match_any G pc et). the (match_exception_table G C pc et) < mpc) \<and>
(\<forall>s \<in> at. \<exists>ST LT z r. s=((Init (RefT r)#ST,LT),z) \<and> (\<forall>C \<in> set (match_any G pc et). is_class G C)))"
apply auto
apply (drule bspec, assumption)
apply clarsimp
apply (case_tac a)
apply auto
apply (case_tac aa)
apply auto
done
lemma appJsr[simp]:
"app (Jsr b) G C' pc maxs mpc rT ini et at = (nat (int pc + b) < mpc \<and> (\<forall>s \<in> at. \<exists>ST LT z. s = ((ST,LT),z) \<and> 0 \<le> int pc + b \<and> length ST < maxs))"
by auto
lemma set_SOME_lists:
"finite s \<Longrightarrow> set (SOME l. set l = s) = s"
apply (erule finite_induct)
apply simp
apply (rule_tac a="x#(SOME l. set l = F)" in someI2)
apply auto
done
lemma appRet[simp]:
"finite at \<Longrightarrow>
app (Ret x) G C' pc maxs mpc rT ini et at = (\<forall>s \<in> at. \<exists>ST LT z. s = ((ST,LT),z) \<and> x < length LT \<and> (\<exists>r. LT!x=OK (Init (RA r)) \<and> r < mpc))"
apply (auto simp add: set_SOME_lists finite_imageI theRA_def)
apply (drule bspec, assumption)+
apply simp
apply (drule bspec, assumption)+
apply auto
done
lemma appArrLoad[simp]:
"app ArrLoad G C' pc maxs mpc rT ini et at = (Suc pc < mpc \<and>
(\<forall>x \<in> set (match G (Xcpt NullPointer) pc et). the (match_exception_table G x pc et) < mpc) \<and>
(\<forall>x \<in> set (match G (Xcpt ArrayIndexOutOfBounds) pc et). the (match_exception_table G x pc et) < mpc) \<and>
(\<forall>s \<in> at. \<exists>T ST LT z. s=((Init (PrimT Integer)#Init (T.[])#ST,LT),z) \<and>
(\<forall>x \<in> set (match G (Xcpt NullPointer) pc et). is_class G x) \<and>
(\<forall>x \<in> set (match G (Xcpt ArrayIndexOutOfBounds) pc et). is_class G x)))"
apply auto
apply (drule bspec, assumption)
apply clarsimp
apply (case_tac a)
apply simp
apply (case_tac list)
apply simp
apply (case_tac ab)
apply (case_tac ty)
apply simp
apply (case_tac ref_ty)
apply auto
done
lemma appArrStore[simp]:
"app ArrStore G C' pc maxs mpc rT ini et at = (Suc pc < mpc \<and>
(\<forall>x \<in> set (match G (Xcpt NullPointer) pc et). the (match_exception_table G x pc et) < mpc) \<and>
(\<forall>x \<in> set (match G (Xcpt ArrayIndexOutOfBounds) pc et). the (match_exception_table G x pc et) < mpc) \<and>
(\<forall>x \<in> set (match G (Xcpt ArrayStore) pc et). the (match_exception_table G x pc et) < mpc) \<and>
(\<forall>s \<in> at. \<exists>T T' ST LT z. s=((Init T#Init (PrimT Integer)#Init (T'.[])#ST,LT),z) \<and>
(\<forall>x \<in> set (match G (Xcpt NullPointer) pc et). is_class G x) \<and>
(\<forall>x \<in> set (match G (Xcpt ArrayStore) pc et). is_class G x) \<and>
(\<forall>x \<in> set (match G (Xcpt ArrayIndexOutOfBounds) pc et). is_class G x)))"
apply auto
apply (drule bspec, assumption)
apply clarsimp
apply (case_tac a, simp)
apply (case_tac list)
apply (case_tac aa, simp, simp, simp)
apply (case_tac lista, simp)
apply (case_tac aa, simp, simp, simp)
apply simp
apply (case_tac aa)
defer
apply simp
apply simp
apply simp
apply (case_tac ac)
apply (case_tac tya)
apply simp
apply (case_tac ref_ty)
apply auto
done
lemma appArrLength[simp]:
"app ArrLength G C' pc maxs mpc rT ini et at = (Suc pc < mpc \<and>
(\<forall>x \<in> set (match G (Xcpt NullPointer) pc et). the (match_exception_table G x pc et) < mpc) \<and>
(\<forall>s \<in> at. \<exists>T ST LT z. s=((Init (T.[])#ST,LT),z) \<and>
(\<forall>x \<in> set (match G (Xcpt NullPointer) pc et). is_class G x)))"
apply auto
apply (drule bspec, assumption)
apply clarsimp
apply (case_tac a, simp)
apply (case_tac aa)
apply (case_tac ty, simp)
apply (case_tac ref_ty)
apply auto
done
lemma appArrNew[simp]:
"app (ArrNew T) G C' pc maxs mpc rT ini et at = (Suc pc < mpc \<and>
(\<forall>x \<in> set (match G (Xcpt NegativeArraySize) pc et). the (match_exception_table G x pc et) < mpc) \<and>
(\<forall>x \<in> set (match G (Xcpt OutOfMemory) pc et). the (match_exception_table G x pc et) < mpc) \<and>
(\<forall>s \<in> at. \<exists>ST LT z. s=((Init (PrimT Integer)#ST,LT),z) \<and>
is_type G T \<and> noRA T \<and> dim T + 1 \<le> max_dim \<and>
(\<forall>x \<in> set (match G (Xcpt NegativeArraySize) pc et). is_class G x) \<and>
(\<forall>x \<in> set (match G (Xcpt OutOfMemory) pc et). is_class G x)))"
apply rule
defer
apply fastsimp
apply clarsimp
apply (rule conjI)
apply clarsimp
apply (drule bspec, rule UnI2, rule imageI, assumption)
apply fastsimp
apply (rule conjI)
apply clarsimp
apply (drule bspec, rule UnI1, rule imageI, assumption)
apply fastsimp
apply clarsimp
apply (drule bspec, assumption)
apply clarsimp
apply (case_tac a)
apply auto
done
lemma appInvoke[simp]:
"app (Invoke C mn fpTs) G C' pc maxs mpc rT ini et at =
((Suc pc < mpc \<and>
(\<forall>C \<in> set (match_any G pc et). the (match_exception_table G C pc et) < mpc)) \<and>
(\<forall>s \<in> at. \<exists>apTs X ST LT mD' rT' b' z.
s = (((rev apTs) @ (X # ST), LT), z) \<and> mn \<noteq> init \<and>
length apTs = length fpTs \<and> is_class G C \<and>
(\<forall>(aT,fT)\<in>set(zip apTs fpTs). G \<turnstile> aT \<preceq>i (Init fT)) \<and>
method (G,C) (mn,fpTs) = Some (mD', rT', b') \<and> (G \<turnstile> X \<preceq>i Init (Class C)) \<and>
(\<forall>C \<in> set (match_any G pc et). is_class G C)))"
(is "?app at = (?Q \<and> (\<forall>s \<in> at. ?P s))")
proof -
note list_all2_def[simp]
{ fix a b z
assume app: "?app at" and at: "((a,b),z) \<in> at"
have "?P ((a,b),z)"
proof -
from app and at
have "a = (rev (rev (take (length fpTs) a))) @ (drop (length fpTs) a) \<and>
length fpTs < length a" (is "?a \<and> ?l")
by (auto simp add: app_def)
hence "?a \<and> 0 < length (drop (length fpTs) a)" (is "?a \<and> ?l")
by auto
hence "?a \<and> ?l \<and> length (rev (take (length fpTs) a)) = length fpTs"
by (auto simp add: min_def)
then obtain apTs ST where
"a = rev apTs @ ST \<and> length apTs = length fpTs \<and> 0 < length ST"
by blast
hence "a = rev apTs @ ST \<and> length apTs = length fpTs \<and> ST \<noteq> []"
by blast
then obtain X ST' where
"a = rev apTs @ X # ST'" "length apTs = length fpTs"
by (simp add: neq_Nil_conv) blast
with app and at show ?thesis by fastsimp
qed } note x = this
have "?app at \<Longrightarrow> (\<forall>s \<in> at. ?P s)" by clarify (rule x)
hence "?app at \<Longrightarrow> ?Q \<and> (\<forall>s \<in> at. ?P s)" by auto
moreover
have "?Q \<and> (\<forall>s \<in> at. ?P s) \<Longrightarrow> ?app at"
apply clarsimp
apply (drule bspec, assumption)
apply (clarsimp simp add: min_def)
done
ultimately
show ?thesis by (rule iffI)
qed
lemma appInvoke_special[simp]:
"app (Invoke_special C mn fpTs) G C' pc maxs mpc rT ini et at =
((Suc pc < mpc \<and>
(\<forall>C \<in> set (match_any G pc et). the (match_exception_table G C pc et) < mpc)) \<and>
(\<forall>s \<in> at. \<exists>apTs X ST LT rT' b' z.
s = (((rev apTs) @ X # ST, LT), z) \<and> mn = init \<and>
length apTs = length fpTs \<and> is_class G C \<and>
(\<forall>(aT,fT)\<in>set(zip apTs fpTs). G \<turnstile> aT \<preceq>i (Init fT)) \<and>
method (G,C) (mn,fpTs) = Some (C, rT', b') \<and>
((\<exists>pc. X = UnInit C pc) \<or> (X = PartInit C' \<and> G \<turnstile> C' \<prec>C1 C \<and> ¬z)) \<and>
(\<forall>C \<in> set (match_any G pc et). is_class G C)))"
(is "?app at = (?Q \<and> (\<forall>s \<in> at. ?P s))")
proof -
note list_all2_def [simp]
{ fix a b z
assume app: "?app at" and at: "((a,b),z) \<in> at"
have "?P ((a,b),z)"
proof -
from app and at
have "a = (rev (rev (take (length fpTs) a))) @ (drop (length fpTs) a) \<and>
length fpTs < length a" (is "?a \<and> ?l")
by (auto simp add: app_def)
hence "?a \<and> 0 < length (drop (length fpTs) a)" (is "?a \<and> ?l")
by auto
hence "?a \<and> ?l \<and> length (rev (take (length fpTs) a)) = length fpTs"
by (auto simp add: min_def)
then obtain apTs ST where
"a = rev apTs @ ST \<and> length apTs = length fpTs \<and> 0 < length ST"
by blast
hence "a = rev apTs @ ST \<and> length apTs = length fpTs \<and> ST \<noteq> []"
by blast
then obtain X ST' where
"a = rev apTs @ X # ST'" "length apTs = length fpTs"
by (simp add: neq_Nil_conv) blast
with app and at show ?thesis by (fastsimp simp add: nth_append)
qed } note x = this
have "?app at \<Longrightarrow> \<forall>s \<in> at. ?P s" by clarify (rule x)
hence "?app at \<Longrightarrow> ?Q \<and> (\<forall>s \<in> at. ?P s)" by auto
moreover
have "?Q \<and> (\<forall>s \<in> at. ?P s) \<Longrightarrow> ?app at"
apply clarsimp
apply (drule bspec, assumption)
apply (fastsimp simp add: nth_append min_def)
done
ultimately
show ?thesis by (rule iffI)
qed
lemma replace_map_OK:
"replace (OK x) (OK y) (map OK l) = map OK (replace x y l)"
proof -
have "inj OK" by (blast intro: datatype_injI)
thus ?thesis by (rule replace_map)
qed
lemma effNone:
"(pc', s') \<in> set (eff i G pc et {}) \<Longrightarrow> s' = {}"
by (auto simp add: eff_def xcpt_eff_def norm_eff_def split: split_if_asm)
lemmas app_simps =
appNone appLoad appStore appLitPush appGetField appPutField appNew
appCheckcast appPop appDup appDup_x1 appDup_x2 appSwap appIAdd appIfcmpeq
appReturn appGoto appThrow appJsr appRet appInvoke appInvoke_special
section "Code generator setup"
declare list_all2_Nil [code]
declare list_all2_Cons [code]
lemma xcpt_app_lemma [code]:
"xcpt_app i G pc et = list_all (is_class G) (xcpt_names (i, G, pc, et))"
by (simp add: list_all_conv)
constdefs
set_filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set"
"set_filter P A \<equiv> {s. s \<in> A \<and> P s}"
tolist :: "'a set \<Rightarrow> 'a list"
"tolist s \<equiv> (SOME l. set l = s)"
lemma [code]:
"succs (Ret x) pc s = tolist (theRA x ` s)"
apply (simp add: tolist_def)
done
consts
isRet :: "instr \<Rightarrow> bool"
recdef isRet "{}"
"isRet (Ret r) = True"
"isRet i = False"
lemma [code]:
"norm_eff i G pc pc' at = eff_bool i G pc ` (if isRet i then set_filter (\<lambda>s. pc' = theRA (theIdx i) s) at else at)"
apply (cases i)
apply (auto simp add: norm_eff_def set_filter_def)
done
consts_code
"set_filter" ("filter")
"tolist" ("(fn x => x)")
lemma [code]:
"app' (Ifcmpeq b, G, C', pc, maxs, rT, Init ts # Init ts' # ST, LT) =
(0 \<le> int pc + b \<and> (if isPrimT ts then ts' = ts else True) \<and> (if isRefT ts then isRefT ts' else True))"
apply simp
done
consts
isUninitC :: "init_ty \<Rightarrow> cname \<Rightarrow> bool"
primrec
"isUninitC (Init T) C = False"
"isUninitC (UnInit C' pc) C = (C=C')"
"isUninitC (PartInit D) C = False"
lemma [code]:
"app' (Invoke_special C mn fpTs, G, C', pc, maxs, rT, s) =
(length fpTs < length (fst s) \<and>
mn = init \<and>
(let apTs = rev (take (length fpTs) (fst s)); X = fst s ! length fpTs
in is_class G C \<and>
list_all2 (\<lambda>aT fT. G \<turnstile> aT \<preceq>i Init fT) apTs fpTs \<and>
method (G, C) (mn, fpTs) \<noteq> None \<and>
(let (C'', rT', b) = the (method (G, C) (mn, fpTs)) in
C = C'' \<and>
(isUninitC X C \<or> X = PartInit C' \<and> G \<turnstile> C' \<prec>C1 C))))"
apply auto
apply (cases "fst s ! length fpTs")
apply auto
apply (cases "fst s ! length fpTs")
apply auto
done
consts
isOKInitRA :: "init_ty err \<Rightarrow> bool"
recdef isOKInitRA "{}"
"isOKInitRA (OK (Init (RA r))) = True"
"isOKInitRA z = False"
lemma [code]:
"app' (Ret x, G, C', pc, maxs, rT, ST, LT) = (x < length LT \<and> isOKInitRA (LT!x))"
apply simp
apply auto
apply (cases "LT!x")
apply simp
apply simp
apply (case_tac a)
apply auto
apply (case_tac ty)
apply auto
apply (case_tac prim_ty)
apply auto
done
consts
isInv_spcl :: "instr \<Rightarrow> bool"
recdef
isInv_spcl "{}"
"isInv_spcl (Invoke_special C m p) = True"
"isInv_spcl i = False"
consts
mNam :: "instr \<Rightarrow> mname"
recdef
mNam "{}"
"mNam (Invoke_special C m p) = m"
consts
pLen :: "instr \<Rightarrow> nat"
recdef
pLen "{}"
"pLen (Invoke_special C m p) = length p"
consts
isPartInit :: "init_ty \<Rightarrow> bool"
recdef
isPartInit "{}"
"isPartInit (PartInit D) = True"
"isPartInit T = False"
lemma [code]:
"app i G C' pc mxs mpc rT ini et at =
((\<forall>(s, z)\<in>at.
xcpt_app i G pc et \<and>
app' (i, G, C', pc, mxs, rT, s) \<and>
(if ini \<and> i = Return then z else True) \<and>
(if isInv_spcl i \<and> fst s ! (pLen i) = PartInit C' then ¬ z else True)) \<and>
(\<forall>(pc', s')\<in>set (eff i G pc et at). pc' < mpc))"
apply (simp add: split_beta app_def)
apply (cases i)
apply auto
done
lemma [code]:
"eff_bool i G pc = (\<lambda>((ST, LT), z). (eff' (i, G, pc, ST, LT),
if isInv_spcl i \<and> mNam i = init \<and> isPartInit(ST ! (pLen i)) then True else z))"
apply (auto simp add: eff_bool_def split_def)
apply (cases i)
apply auto
apply (rule ext)
apply auto
apply (case_tac "a!length list")
apply auto
done
lemmas [simp del] = app_def xcpt_app_def
end
lemma match_some_entry:
match G X pc et = (if Bex (set et) (match_exception_entry G X pc) then [X] else [])
lemma isPrimT:
isPrimT T = (EX T'. T = PrimT T')
lemma isRefT:
isRefT T = (EX T'. T = RefT T')
lemma match_any_match_table:
C : set (match_any G pc et) ==> match_exception_table G C pc et ~= None
lemma match_X_match_table:
C : set (match G X pc et) ==> match_exception_table G C pc et ~= None
lemma xcpt_names_in_et:
C : set (xcpt_names (i, G, pc, et)) ==> EX e:set et. the (match_exception_table G C pc et) = fst (snd (snd e))
lemma length_casesE1:
[| ((xs, y), z) : at; xs = [] ==> P []; !!l. xs = [l] ==> P [l];
!!l l'. xs = [l, l'] ==> P [l, l'];
!!l l' ls. xs = l # l' # ls ==> P (l # l' # ls) |]
==> P xs
lemmas
app i G C' pc mxs mpc rT ini et at ==
(ALL (s, z):at.
xcpt_app i G pc et &
app' (i, G, C', pc, mxs, rT, s) &
(ini & i = Return --> z) &
(ALL C m p.
i = Invoke_special C m p & fst s ! length p = PartInit C' --> ¬ z)) &
(ALL (pc', s'):set (eff i G pc et at). pc' < mpc)
xcpt_app i G pc et == Ball (set (xcpt_names (i, G, pc, et))) (is_class G)
lemma appNone:
app i G C' pc maxs mpc rT ini et {} =
(ALL (pc', s'):set (eff i G pc et {}). pc' < mpc)
lemmas eff_defs:
eff i G pc et at == map (%pc'. (pc', norm_eff i G pc pc' at)) (succs i pc at) @ xcpt_eff i G pc at et
norm_eff i G pc pc' at ==
eff_bool i G pc `
(if EX idx. i = Ret idx then {s. s : at & pc' = theRA (theIdx i) s} else at)
eff_bool i G pc ==
%((ST, LT), z).
(eff' (i, G, pc, ST, LT),
if EX C p D. i = Invoke_special C init p & ST ! length p = PartInit D
then True else z)
xcpt_eff i G pc at et ==
map (%C. (the (match_exception_table G C pc et),
(%s. (([Init (Class C)], snd (fst s)), snd s)) ` at))
(xcpt_names (i, G, pc, et))
lemma appLoad:
app (Load idx) G C' pc maxs mpc rT ini et at =
(Suc pc < mpc &
(ALL s:at.
EX ST LT z.
s = ((ST, LT), z) &
idx < length LT & LT ! idx ~= Err & length ST < maxs))
lemma appStore:
app (Store idx) G C' pc maxs mpc rT ini et at = (Suc pc < mpc & (ALL s:at. EX ts ST LT z. s = ((ts # ST, LT), z) & idx < length LT))
lemma appLitPush:
app (LitPush v) G C' pc maxs mpc rT ini et at =
(Suc pc < mpc &
(ALL s:at.
EX ST LT z.
s = ((ST, LT), z) &
length ST < maxs &
typeof (%v. None) v
: {Some NT} Un (Some o PrimT) ` {Void, Boolean, Integer}))
lemma appGetField:
app (Getfield F C) G C' pc maxs mpc rT ini et at =
(Suc pc < mpc &
(ALL x:set (match G (Xcpt NullPointer) pc et).
the (match_exception_table G x pc et) < mpc) &
(ALL s:at.
EX oT vT ST LT z.
s = ((oT # ST, LT), z) &
is_class G C &
field (G, C) F = Some (C, vT) &
G |- oT <=i Init (Class C) &
Ball (set (match G (Xcpt NullPointer) pc et)) (is_class G)))
lemma appPutField:
app (Putfield F C) G C' pc maxs mpc rT ini et at =
(Suc pc < mpc &
(ALL x:set (match G (Xcpt NullPointer) pc et).
the (match_exception_table G x pc et) < mpc) &
(ALL s:at.
EX vT vT' oT ST LT z.
s = ((vT # oT # ST, LT), z) &
is_class G C &
field (G, C) F = Some (C, vT') &
G |- oT <=i Init (Class C) &
G |- vT <=i Init vT' &
Ball (set (match G (Xcpt NullPointer) pc et)) (is_class G)))
lemma appNew:
app (New C) G C' pc maxs mpc rT ini et at =
(Suc pc < mpc &
(ALL x:set (match G (Xcpt OutOfMemory) pc et).
the (match_exception_table G x pc et) < mpc) &
(ALL s:at.
EX ST LT z.
s = ((ST, LT), z) &
is_class G C &
length ST < maxs &
UnInit C pc ~: set ST &
Ball (set (match G (Xcpt OutOfMemory) pc et)) (is_class G)))
lemma appCheckcast:
app (Checkcast C) G C' pc maxs mpc rT ini et at =
(Suc pc < mpc &
(ALL x:set (match G (Xcpt ClassCast) pc et).
the (match_exception_table G x pc et) < mpc) &
(ALL s:at.
EX rT ST LT z.
s = ((Init (RefT rT) # ST, LT), z) &
is_class G C &
Ball (set (match G (Xcpt ClassCast) pc et)) (is_class G)))
lemma appPop:
app Pop G C' pc maxs mpc rT ini et at = (Suc pc < mpc & (ALL s:at. EX ts ST LT z. s = ((ts # ST, LT), z)))
lemma appDup:
app Dup G C' pc maxs mpc rT ini et at = (Suc pc < mpc & (ALL s:at. EX ts ST LT z. s = ((ts # ST, LT), z) & 1 + length ST < maxs))
lemma appDup_x1:
app Dup_x1 G C' pc maxs mpc rT ini et at =
(Suc pc < mpc &
(ALL s:at.
EX ts1 ts2 ST LT z. s = ((ts1 # ts2 # ST, LT), z) & 2 + length ST < maxs))
lemma appDup_x2:
app Dup_x2 G C' pc maxs mpc rT ini et at =
(Suc pc < mpc &
(ALL s:at.
EX ts1 ts2 ts3 ST LT z.
s = ((ts1 # ts2 # ts3 # ST, LT), z) & 3 + length ST < maxs))
lemma appSwap:
app Swap G C' pc maxs mpc rT ini et at = (Suc pc < mpc & (ALL s:at. EX ts1 ts2 ST LT z. s = ((ts1 # ts2 # ST, LT), z)))
lemma appIAdd:
app IAdd G C' pc maxs mpc rT ini et at =
(Suc pc < mpc &
(ALL s:at.
EX ST LT z.
s = ((Init (PrimT Integer) # Init (PrimT Integer) # ST, LT), z)))
lemma appIfcmpeq:
app (Ifcmpeq b) G C' pc maxs mpc rT ini et at =
(Suc pc < mpc &
nat (int pc + b) < mpc &
(ALL s:at.
EX ts1 ts2 ST LT z.
s = ((Init ts1 # Init ts2 # ST, LT), z) &
0 <= b + int pc &
((EX p. ts1 = PrimT p & ts2 = PrimT p) |
(EX r r'. ts1 = RefT r & ts2 = RefT r'))))
lemma appReturn:
app Return G C' pc maxs mpc rT ini et at =
(ALL s:at.
EX T ST LT z. s = ((T # ST, LT), z) & G |- T <=i Init rT & (ini --> z))
lemma appGoto:
app (Goto b) G C' pc maxs mpc rT ini et at =
(nat (int pc + b) < mpc & (at ~= {} --> 0 <= int pc + b))
lemma appThrow:
app Throw G C' pc maxs mpc rT ini et at =
((ALL C:set (match_any G pc et). the (match_exception_table G C pc et) < mpc) &
(ALL s:at.
EX ST LT z r.
s = ((Init (RefT r) # ST, LT), z) &
Ball (set (match_any G pc et)) (is_class G)))
lemma appJsr:
app (Jsr b) G C' pc maxs mpc rT ini et at = (nat (int pc + b) < mpc & (ALL s:at. EX ST LT z. s = ((ST, LT), z) & 0 <= int pc + b & length ST < maxs))
lemma set_SOME_lists:
finite s ==> set (SOME l. set l = s) = s
lemma appRet:
finite at
==> app (Ret x) G C' pc maxs mpc rT ini et at =
(ALL s:at.
EX ST LT z.
s = ((ST, LT), z) &
x < length LT & (EX r. LT ! x = OK (Init (RA r)) & r < mpc))
lemma appArrLoad:
app ArrLoad G C' pc maxs mpc rT ini et at =
(Suc pc < mpc &
(ALL x:set (match G (Xcpt NullPointer) pc et).
the (match_exception_table G x pc et) < mpc) &
(ALL x:set (match G (Xcpt ArrayIndexOutOfBounds) pc et).
the (match_exception_table G x pc et) < mpc) &
(ALL s:at.
EX T ST LT z.
s = ((Init (PrimT Integer) # Init (T.[]) # ST, LT), z) &
Ball (set (match G (Xcpt NullPointer) pc et)) (is_class G) &
Ball (set (match G (Xcpt ArrayIndexOutOfBounds) pc et)) (is_class G)))
lemma appArrStore:
app ArrStore G C' pc maxs mpc rT ini et at =
(Suc pc < mpc &
(ALL x:set (match G (Xcpt NullPointer) pc et).
the (match_exception_table G x pc et) < mpc) &
(ALL x:set (match G (Xcpt ArrayIndexOutOfBounds) pc et).
the (match_exception_table G x pc et) < mpc) &
(ALL x:set (match G (Xcpt ArrayStore) pc et).
the (match_exception_table G x pc et) < mpc) &
(ALL s:at.
EX T T' ST LT z.
s = ((Init T # Init (PrimT Integer) # Init (T'.[]) # ST, LT), z) &
Ball (set (match G (Xcpt NullPointer) pc et)) (is_class G) &
Ball (set (match G (Xcpt ArrayStore) pc et)) (is_class G) &
Ball (set (match G (Xcpt ArrayIndexOutOfBounds) pc et)) (is_class G)))
lemma appArrLength:
app ArrLength G C' pc maxs mpc rT ini et at =
(Suc pc < mpc &
(ALL x:set (match G (Xcpt NullPointer) pc et).
the (match_exception_table G x pc et) < mpc) &
(ALL s:at.
EX T ST LT z.
s = ((Init (T.[]) # ST, LT), z) &
Ball (set (match G (Xcpt NullPointer) pc et)) (is_class G)))
lemma appArrNew:
app (ArrNew T) G C' pc maxs mpc rT ini et at =
(Suc pc < mpc &
(ALL x:set (match G (Xcpt NegativeArraySize) pc et).
the (match_exception_table G x pc et) < mpc) &
(ALL x:set (match G (Xcpt OutOfMemory) pc et).
the (match_exception_table G x pc et) < mpc) &
(ALL s:at.
EX ST LT z.
s = ((Init (PrimT Integer) # ST, LT), z) &
is_type G T &
noRA T &
dim T + 1 <= max_dim &
Ball (set (match G (Xcpt NegativeArraySize) pc et)) (is_class G) &
Ball (set (match G (Xcpt OutOfMemory) pc et)) (is_class G)))
lemma appInvoke:
app (Invoke C mn fpTs) G C' pc maxs mpc rT ini et at =
((Suc pc < mpc &
(ALL C:set (match_any G pc et).
the (match_exception_table G C pc et) < mpc)) &
(ALL s:at.
EX apTs X ST LT mD' rT' b' z.
s = ((rev apTs @ X # ST, LT), z) &
mn ~= init &
length apTs = length fpTs &
is_class G C &
(ALL (aT, fT):set (zip apTs fpTs). G |- aT <=i Init fT) &
method (G, C) (mn, fpTs) = Some (mD', rT', b') &
G |- X <=i Init (Class C) &
Ball (set (match_any G pc et)) (is_class G)))
lemma appInvoke_special:
app (Invoke_special C mn fpTs) G C' pc maxs mpc rT ini et at =
((Suc pc < mpc &
(ALL C:set (match_any G pc et).
the (match_exception_table G C pc et) < mpc)) &
(ALL s:at.
EX apTs X ST LT rT' b' z.
s = ((rev apTs @ X # ST, LT), z) &
mn = init &
length apTs = length fpTs &
is_class G C &
(ALL (aT, fT):set (zip apTs fpTs). G |- aT <=i Init fT) &
method (G, C) (mn, fpTs) = Some (C, rT', b') &
((EX pc. X = UnInit C pc) | X = PartInit C' & G |- C' <=C1 C & ¬ z) &
Ball (set (match_any G pc et)) (is_class G)))
lemma replace_map_OK:
replace (OK x) (OK y) (map OK l) = map OK (replace x y l)
lemma effNone:
(pc', s') : set (eff i G pc et {}) ==> s' = {}
lemmas app_simps:
app i G C' pc maxs mpc rT ini et {} =
(ALL (pc', s'):set (eff i G pc et {}). pc' < mpc)
app (Load idx) G C' pc maxs mpc rT ini et at =
(Suc pc < mpc &
(ALL s:at.
EX ST LT z.
s = ((ST, LT), z) &
idx < length LT & LT ! idx ~= Err & length ST < maxs))
app (Store idx) G C' pc maxs mpc rT ini et at = (Suc pc < mpc & (ALL s:at. EX ts ST LT z. s = ((ts # ST, LT), z) & idx < length LT))
app (LitPush v) G C' pc maxs mpc rT ini et at =
(Suc pc < mpc &
(ALL s:at.
EX ST LT z.
s = ((ST, LT), z) &
length ST < maxs &
typeof (%v. None) v
: {Some NT} Un (Some o PrimT) ` {Void, Boolean, Integer}))
app (Getfield F C) G C' pc maxs mpc rT ini et at =
(Suc pc < mpc &
(ALL x:set (match G (Xcpt NullPointer) pc et).
the (match_exception_table G x pc et) < mpc) &
(ALL s:at.
EX oT vT ST LT z.
s = ((oT # ST, LT), z) &
is_class G C &
field (G, C) F = Some (C, vT) &
G |- oT <=i Init (Class C) &
Ball (set (match G (Xcpt NullPointer) pc et)) (is_class G)))
app (Putfield F C) G C' pc maxs mpc rT ini et at =
(Suc pc < mpc &
(ALL x:set (match G (Xcpt NullPointer) pc et).
the (match_exception_table G x pc et) < mpc) &
(ALL s:at.
EX vT vT' oT ST LT z.
s = ((vT # oT # ST, LT), z) &
is_class G C &
field (G, C) F = Some (C, vT') &
G |- oT <=i Init (Class C) &
G |- vT <=i Init vT' &
Ball (set (match G (Xcpt NullPointer) pc et)) (is_class G)))
app (New C) G C' pc maxs mpc rT ini et at =
(Suc pc < mpc &
(ALL x:set (match G (Xcpt OutOfMemory) pc et).
the (match_exception_table G x pc et) < mpc) &
(ALL s:at.
EX ST LT z.
s = ((ST, LT), z) &
is_class G C &
length ST < maxs &
UnInit C pc ~: set ST &
Ball (set (match G (Xcpt OutOfMemory) pc et)) (is_class G)))
app (Checkcast C) G C' pc maxs mpc rT ini et at =
(Suc pc < mpc &
(ALL x:set (match G (Xcpt ClassCast) pc et).
the (match_exception_table G x pc et) < mpc) &
(ALL s:at.
EX rT ST LT z.
s = ((Init (RefT rT) # ST, LT), z) &
is_class G C &
Ball (set (match G (Xcpt ClassCast) pc et)) (is_class G)))
app Pop G C' pc maxs mpc rT ini et at = (Suc pc < mpc & (ALL s:at. EX ts ST LT z. s = ((ts # ST, LT), z)))
app Dup G C' pc maxs mpc rT ini et at = (Suc pc < mpc & (ALL s:at. EX ts ST LT z. s = ((ts # ST, LT), z) & 1 + length ST < maxs))
app Dup_x1 G C' pc maxs mpc rT ini et at =
(Suc pc < mpc &
(ALL s:at.
EX ts1 ts2 ST LT z. s = ((ts1 # ts2 # ST, LT), z) & 2 + length ST < maxs))
app Dup_x2 G C' pc maxs mpc rT ini et at =
(Suc pc < mpc &
(ALL s:at.
EX ts1 ts2 ts3 ST LT z.
s = ((ts1 # ts2 # ts3 # ST, LT), z) & 3 + length ST < maxs))
app Swap G C' pc maxs mpc rT ini et at = (Suc pc < mpc & (ALL s:at. EX ts1 ts2 ST LT z. s = ((ts1 # ts2 # ST, LT), z)))
app IAdd G C' pc maxs mpc rT ini et at =
(Suc pc < mpc &
(ALL s:at.
EX ST LT z.
s = ((Init (PrimT Integer) # Init (PrimT Integer) # ST, LT), z)))
app (Ifcmpeq b) G C' pc maxs mpc rT ini et at =
(Suc pc < mpc &
nat (int pc + b) < mpc &
(ALL s:at.
EX ts1 ts2 ST LT z.
s = ((Init ts1 # Init ts2 # ST, LT), z) &
0 <= b + int pc &
((EX p. ts1 = PrimT p & ts2 = PrimT p) |
(EX r r'. ts1 = RefT r & ts2 = RefT r'))))
app Return G C' pc maxs mpc rT ini et at =
(ALL s:at.
EX T ST LT z. s = ((T # ST, LT), z) & G |- T <=i Init rT & (ini --> z))
app (Goto b) G C' pc maxs mpc rT ini et at =
(nat (int pc + b) < mpc & (at ~= {} --> 0 <= int pc + b))
app Throw G C' pc maxs mpc rT ini et at =
((ALL C:set (match_any G pc et). the (match_exception_table G C pc et) < mpc) &
(ALL s:at.
EX ST LT z r.
s = ((Init (RefT r) # ST, LT), z) &
Ball (set (match_any G pc et)) (is_class G)))
app (Jsr b) G C' pc maxs mpc rT ini et at = (nat (int pc + b) < mpc & (ALL s:at. EX ST LT z. s = ((ST, LT), z) & 0 <= int pc + b & length ST < maxs))
finite at
==> app (Ret x) G C' pc maxs mpc rT ini et at =
(ALL s:at.
EX ST LT z.
s = ((ST, LT), z) &
x < length LT & (EX r. LT ! x = OK (Init (RA r)) & r < mpc))
app (Invoke C mn fpTs) G C' pc maxs mpc rT ini et at =
((Suc pc < mpc &
(ALL C:set (match_any G pc et).
the (match_exception_table G C pc et) < mpc)) &
(ALL s:at.
EX apTs X ST LT mD' rT' b' z.
s = ((rev apTs @ X # ST, LT), z) &
mn ~= init &
length apTs = length fpTs &
is_class G C &
(ALL (aT, fT):set (zip apTs fpTs). G |- aT <=i Init fT) &
method (G, C) (mn, fpTs) = Some (mD', rT', b') &
G |- X <=i Init (Class C) &
Ball (set (match_any G pc et)) (is_class G)))
app (Invoke_special C mn fpTs) G C' pc maxs mpc rT ini et at =
((Suc pc < mpc &
(ALL C:set (match_any G pc et).
the (match_exception_table G C pc et) < mpc)) &
(ALL s:at.
EX apTs X ST LT rT' b' z.
s = ((rev apTs @ X # ST, LT), z) &
mn = init &
length apTs = length fpTs &
is_class G C &
(ALL (aT, fT):set (zip apTs fpTs). G |- aT <=i Init fT) &
method (G, C) (mn, fpTs) = Some (C, rT', b') &
((EX pc. X = UnInit C pc) | X = PartInit C' & G |- C' <=C1 C & ¬ z) &
Ball (set (match_any G pc et)) (is_class G)))
lemma xcpt_app_lemma:
xcpt_app i G pc et = list_all (is_class G) (xcpt_names (i, G, pc, et))
lemma
succs (Ret x) pc s = tolist (theRA x ` s)
lemma
norm_eff i G pc pc' at = eff_bool i G pc ` (if isRet i then set_filter (%s. pc' = theRA (theIdx i) s) at else at)
lemma
app' (Ifcmpeq b, G, C', pc, maxs, rT, Init ts # Init ts' # ST, LT) = (0 <= int pc + b & (if isPrimT ts then ts' = ts else True) & (if isRefT ts then isRefT ts' else True))
lemma
app' (Invoke_special C mn fpTs, G, C', pc, maxs, rT, s) =
(length fpTs < length (fst s) &
mn = init &
(let apTs = rev (take (length fpTs) (fst s)); X = fst s ! length fpTs
in is_class G C &
list_all2 (%aT fT. G |- aT <=i Init fT) apTs fpTs &
method (G, C) (mn, fpTs) ~= None &
(let (C'', rT', b) = the (method (G, C) (mn, fpTs))
in C = C'' & (isUninitC X C | X = PartInit C' & G |- C' <=C1 C))))
lemma
app' (Ret x, G, C', pc, maxs, rT, ST, LT) = (x < length LT & isOKInitRA (LT ! x))
lemma
app i G C' pc mxs mpc rT ini et at =
((ALL (s, z):at.
xcpt_app i G pc et &
app' (i, G, C', pc, mxs, rT, s) &
(if ini & i = Return then z else True) &
(if isInv_spcl i & fst s ! pLen i = PartInit C' then ¬ z else True)) &
(ALL (pc', s'):set (eff i G pc et at). pc' < mpc))
lemma
eff_bool i G pc =
(%((ST, LT), z).
(eff' (i, G, pc, ST, LT),
if isInv_spcl i & mNam i = init & isPartInit (ST ! pLen i) then True
else z))
lemmas
app i G C' pc mxs mpc rT ini et at ==
(ALL (s, z):at.
xcpt_app i G pc et &
app' (i, G, C', pc, mxs, rT, s) &
(ini & i = Return --> z) &
(ALL C m p.
i = Invoke_special C m p & fst s ! length p = PartInit C' --> ¬ z)) &
(ALL (pc', s'):set (eff i G pc et at). pc' < mpc)
xcpt_app i G pc et == Ball (set (xcpt_names (i, G, pc, et))) (is_class G)