Theory SemanticsWF

```chapter ‹Equivalence of the CFG and Jinja›

theory SemanticsWF imports JVMInterpretation "../Basic/SemanticsCFG" begin

text ‹
The following abbreviations update the stack and the local variables (in the representation
as used in the CFG) according to a ‹frame list› as it is used in Jinja's
state representation.
›

abbreviation update_stk :: "((nat × nat) ⇒ val) ⇒ (frame list) ⇒ ((nat × nat) ⇒ val)"
where
"update_stk stk frs ≡ (λ(a, b).
if length frs ≤ a then stk (a, b)
else let xs = fst (frs ! (length frs - Suc a))
in if length xs ≤ b then stk (a, b) else xs ! (length xs - Suc b))"

abbreviation update_loc :: "((nat × nat) ⇒ val) ⇒ (frame list) ⇒ ((nat × nat) ⇒ val)"
where
"update_loc loc frs ≡ (λ(a, b).
if length frs ≤ a then loc (a, b)
else let xs = fst (snd (frs ! (length frs - Suc a)))
in if length xs ≤ b then loc (a, b) else xs ! b)"

subsection ‹Some simplification lemmas›

lemma update_loc_s2jvm [simp]:
"update_loc loc (snd(snd(state_to_jvm_state P cs (h,stk,loc)))) = loc"
by (auto intro!: ext simp: nth_locss)

lemma update_stk_s2jvm [simp]:
"update_stk stk (snd(snd(state_to_jvm_state P cs (h,stk,loc)))) = stk"
by (auto intro!: ext simp: nth_stkss)

lemma update_loc_s2jvm' [simp]:
"update_loc loc (zip (stkss P cs stk) (zip (locss P cs loc) cs)) = loc"
by (auto intro!: ext simp: nth_locss)

lemma update_stk_s2jvm' [simp]:
"update_stk stk (zip (stkss P cs stk) (zip (locss P cs loc) cs)) = stk"
by (auto intro!: ext simp: nth_stkss)

lemma find_handler_find_handler_forD:
"find_handler (P⇘wf⇙) a h frs = (xp',h',frs')
⟹ find_handler_for P (cname_of h a) (framestack_to_callstack frs) =
framestack_to_callstack frs'"
by (induct frs, auto)

lemma find_handler_nonempty_frs [simp]:
"(find_handler P a h frs ≠ (None, h', []))"
by (induct frs, auto)

lemma find_handler_heap_eqD:
"find_handler P a h frs = (xp, h', frs') ⟹ h' = h"
by (induct frs, auto)

lemma find_handler_frs_decrD:
"find_handler P a h frs = (xp, h', frs') ⟹ length frs' ≤ length frs"
by (induct frs, auto)

lemma find_handler_decrD [dest]:
"find_handler P a h frs = (xp, h', f#frs) ⟹ False"
by (drule find_handler_frs_decrD, simp)

lemma find_handler_decrD' [dest]:
"⟦ find_handler P a h frs = (xp,h',f#frs'); length frs = length frs' ⟧ ⟹ False"
by (drule find_handler_frs_decrD, simp)

lemma Suc_minus_Suc_Suc [simp]:
"b < n - 1 ⟹ Suc (n - Suc (Suc b)) = n - Suc b"
by simp

lemma find_handler_loc_fun_eq':
"find_handler (P⇘wf⇙) a h
(zip (stkss P cs stk) (zip (locss P cs loc) cs)) =
(xf, h', frs)
⟹ update_loc loc frs = loc"
proof
fix x
obtain a' b' where x: "x = (a'::nat,b'::nat)" by fastforce
assume find_handler: "find_handler (P⇘wf⇙) a h
(zip (stkss P cs stk) (zip (locss P cs loc) cs)) =
(xf, h', frs)"
thus "update_loc loc frs x = loc x"
proof (induct cs)
case Nil
thus ?case by simp
next
case (Cons aa cs')
then obtain C M pc where step_case: "find_handler (P⇘wf⇙) a h
(zip (stkss P ((C,M,pc) # cs') stk)
(zip (locss P ((C,M,pc) # cs') loc) ((C,M,pc) # cs'))) =
(xf, h', frs)"
by (cases aa, clarsimp)
note IH = ‹find_handler (P⇘wf⇙) a h
(zip (stkss P cs' stk) (zip (locss P cs' loc) cs')) =
(xf, h', frs) ⟹
update_loc loc frs x = loc x›
show ?thesis
proof (cases "match_ex_table (P⇘wf⇙) (cname_of h a) pc (ex_table_of (P⇘wf⇙) C M)")
case None
with step_case IH show ?thesis
by simp
next
case (Some e)
with step_case x
show ?thesis
by (cases "length cs' = a'",
auto simp: nth_Cons' (* nth_locs *) nth_locss)
qed
qed
qed

lemma find_handler_loc_fun_eq:
"find_handler (P⇘wf⇙) a h (snd(snd(state_to_jvm_state P cs (h,stk,loc)))) = (xf,h',frs)
⟹ update_loc loc frs = loc"

lemma find_handler_stk_fun_eq':
"⟦find_handler (P⇘wf⇙) a h
(zip (stkss P cs stk) (zip (locss P cs loc) cs)) =
(None, h', frs);
cd = length frs - 1;
i = length (fst(hd(frs))) - 1 ⟧
⟹ update_stk stk frs = stk((cd, i) := Addr a)"
proof
fix x
obtain a' b' where x: "x = (a'::nat,b'::nat)" by fastforce
assume find_handler: "find_handler (P⇘wf⇙) a h
(zip (stkss P cs stk) (zip (locss P cs loc) cs)) =
(None, h', frs)"
and calldepth: "cd = length frs - 1"
and idx: "i = length (fst (hd frs)) - 1"
from find_handler have "frs ≠ []"
by clarsimp
then obtain stk' loc' C' M' pc' frs' where frs: "frs = (stk',loc',C',M',pc')#frs'"
by (cases frs, fastforce+)
from find_handler
show "update_stk stk frs x = (stk((cd, i) := Addr a)) x"
proof (induct cs)
case Nil
thus ?case by simp
next
case (Cons aa cs')
then obtain C M pc where step_case: "find_handler (P⇘wf⇙) a h
(zip (stkss P ((C,M,pc) # cs') stk)
(zip (locss P ((C,M,pc) # cs') loc) ((C,M,pc) # cs'))) =
(None, h', frs)"
by (cases aa, clarsimp)
note IH = ‹find_handler (P⇘wf⇙) a h
(zip (stkss P cs' stk) (zip (locss P cs' loc) cs')) =
(None, h', frs) ⟹
update_stk stk frs x = (stk((cd, i) := Addr a)) x›
show ?thesis
proof (cases "match_ex_table (P⇘wf⇙) (cname_of h a) pc (ex_table_of (P⇘wf⇙) C M)")
case None
with step_case IH show ?thesis
by simp
next
case (Some e)
show ?thesis
proof (cases "a' = length cs'")
case True
with Some step_case frs calldepth idx x
show ?thesis
by (fastforce simp: nth_Cons')
next
case False
with Some step_case frs calldepth idx x
show ?thesis
by (fastforce simp: nth_Cons' nth_stkss)
qed
qed
qed
qed

lemma find_handler_stk_fun_eq:
"find_handler (P⇘wf⇙) a h (snd(snd(state_to_jvm_state P cs (h,stk,loc)))) = (None,h',frs)
⟹ update_stk stk frs = stk((length frs - 1, length (fst(hd(frs))) - 1) := Addr a)"

lemma f2c_emptyD [dest]:
"framestack_to_callstack frs = [] ⟹ frs = []"

lemma f2c_emptyD' [dest]:
"[] = framestack_to_callstack frs ⟹ frs = []"

lemma correct_state_imp_valid_callstack:
"⟦ P,cs ⊢⇘BV⇙ s √; fst (last cs) = C0; fst(snd (last cs)) = Main ⟧
⟹ valid_callstack (P,C0,Main) cs"
proof (cases cs rule: rev_cases)
case Nil
thus ?thesis by simp
next
case (snoc cs' y)
assume bv_correct: "P,cs ⊢⇘BV⇙ s √"
and last_C: "fst (last cs) = C0"
and last_M: "fst(snd (last cs)) = Main"
with snoc obtain pcX where [simp]: "cs = cs'@[(C0,Main,pcX)]"
by (cases "last cs", fastforce)
obtain h stk loc where [simp]: "s = (h,stk,loc)"
by (cases s, fastforce)
from bv_correct show ?thesis
proof (cases "snd(snd(state_to_jvm_state P cs s))")
case Nil
thus ?thesis
by (cases cs', auto)
next
case [simp]: (Cons a frs')
obtain stk' loc' C M pc where [simp]: "a = (stk', loc', C, M, pc)" by (cases a, fastforce)
from Cons bv_correct show ?thesis
apply clarsimp
proof (induct cs' arbitrary: stk' loc' C M pc frs')
case Nil
thus ?case by (fastforce simp: bv_conform_def)
next
case (Cons a' cs'')
then have [simp]: "a' = (C,M,pc)"
by (cases a', fastforce)
from Cons obtain T Ts mxs mxl "is" xt
where sees_M: "(P⇘wf⇙) ⊢ C sees M:Ts→T = (mxs,mxl,is,xt) in C"
by (clarsimp simp: bv_conform_def correct_state_def)
with Cons
have "pc < length is"
by (auto dest: sees_method_fun
simp: bv_conform_def)
from wf_jvmprog_is_wf [of P] sees_M
have "wt_method (P⇘wf⇙) C Ts T mxs mxl is xt (P⇘Φ⇙ C M)"
by (auto dest: sees_wf_mdecl simp: wf_jvm_prog_phi_def wf_mdecl_def)
with ‹pc < length is› sees_M
have "length Ts = locLength P C M 0 - Suc mxl"
by (auto dest!: list_all2_lengthD
simp: wt_method_def wt_start_def)
with Cons sees_M show ?case
by (cases cs'',
(fastforce dest: sees_method_fun simp: bv_conform_def)+)
qed
qed
qed

declare correct_state_def [simp del]

lemma bool_sym: "Bool (a = b) = Bool (b = a)"
by auto

lemma find_handler_exec_correct:
"⟦(P⇘wf⇙),(P⇘Φ⇙) ⊢ state_to_jvm_state P cs (h,stk,loc) √;
(P⇘wf⇙),(P⇘Φ⇙) ⊢ find_handler (P⇘wf⇙) a h
(zip (stkss P cs stk) (zip (locss P cs loc) cs)) √;
find_handler_for P (cname_of h a) cs = (C', M', pc') # cs'
⟧ ⟹
(P⇘wf⇙),(P⇘Φ⇙) ⊢ (None, h,
(stks (stkLength P C' M' pc')
(λa'. (stk((length cs', stkLength P C' M' pc' - Suc 0) := Addr a)) (length cs', a')),
locs (locLength P C' M' pc') (λa. loc (length cs', a)), C', M', pc') #
zip (stkss P cs' stk) (zip (locss P cs' loc) cs')) √"
proof (induct cs)
case Nil
thus ?case by simp
next
case (Cons aa cs)
note state_correct = ‹P⇘wf⇙,P⇘Φ⇙ ⊢ state_to_jvm_state P (aa # cs) (h, stk, loc) √›
note IH = ‹⟦P⇘wf⇙,P⇘Φ⇙ ⊢ state_to_jvm_state P cs (h, stk, loc) √;
P⇘wf⇙,P⇘Φ⇙ ⊢ find_handler P⇘wf⇙ a h (zip (stkss P cs stk) (zip (locss P cs loc) cs)) √;
find_handler_for P (cname_of h a) cs = (C', M', pc') # cs'⟧
⟹ P⇘wf⇙,P⇘Φ⇙ ⊢ (None, h,
(stks (stkLength P C' M' pc')
(λa'. (stk((length cs', stkLength P C' M' pc' - Suc 0) := Addr a))
(length cs', a')),
locs (locLength P C' M' pc') (λa. loc (length cs', a)), C', M', pc') #
zip (stkss P cs' stk) (zip (locss P cs' loc) cs')) √›
note trg_state_correct = ‹P⇘wf⇙,P⇘Φ⇙ ⊢ find_handler P⇘wf⇙ a h
(zip (stkss P (aa # cs) stk)
(zip (locss P (aa # cs) loc) (aa # cs))) √›
note fhf = ‹find_handler_for P (cname_of h a) (aa # cs) = (C', M', pc') # cs'›
obtain C M pc where [simp]: "aa = (C,M,pc)" by (cases aa, fastforce)
note P_wf = wf_jvmprog_is_wf [of P]
from state_correct
have cs_state_correct: "P⇘wf⇙,P⇘Φ⇙ ⊢ state_to_jvm_state P cs (h, stk, loc) √"
apply (auto simp: correct_state_def)
apply (cases "zip (stkss P cs stk) (zip (locss P cs loc) cs)")
by fastforce+
show ?thesis
proof (cases "match_ex_table (P⇘wf⇙) (cname_of h a) pc (ex_table_of (P⇘wf⇙) C M)")
case None
with trg_state_correct fhf cs_state_correct IH show ?thesis
by clarsimp
next
case (Some xte)
with IH trg_state_correct fhf state_correct show ?thesis
apply (cases "stkLength P C' M' (fst xte)", auto)
apply (clarsimp simp: correct_state_def)
apply (auto simp: correct_state_def)
apply (rule_tac x="Ts" in exI)
apply (rule_tac x="T" in exI)
apply (rule_tac x="mxs" in exI)
apply (rule_tac x="mxl⇩0" in exI)
apply (rule_tac x="is" in exI)
apply (rule conjI)
apply (rule_tac x="xt" in exI)
apply clarsimp
apply clarsimp
apply (drule sees_method_fun, fastforce, clarsimp)
apply (auto simp: list_all2_Cons1)
apply (rule list_all2_all_nthI)
apply clarsimp
apply clarsimp
apply (frule_tac ys="zs" in list_all2_lengthD)
apply clarsimp
apply (drule_tac p="n" and ys="zs" in list_all2_nthD)
apply clarsimp
apply clarsimp
apply (case_tac "length aa - Suc (length aa - snd xte + n) = length zs - Suc n")
apply clarsimp
apply clarsimp
apply (rule list_all2_all_nthI)
apply clarsimp
apply (frule_tac p="n" and ys="b" in list_all2_nthD)
apply (clarsimp dest!: list_all2_lengthD)
by (clarsimp dest!: list_all2_lengthD)
qed
qed

lemma locs_rev_stks:
"x ≥ z ⟹
locs z
(λb.
if z < b then loc (Suc y, b)
else if b ≤ z
then stk (y, x + b - Suc z)
else arbitrary)
@ [stk (y, x - Suc 0)]
=
stk (y, x - Suc (z))
# rev (take z (stks x (λa. stk(y, a))))"
apply (rule nth_equalityI)
apply (simp)
apply (auto simp: nth_append nth_Cons' (* nth_locs *) less_Suc_eq min.absorb2 max.absorb2)
done

lemma locs_invoke_purge:
"(z::nat) > c ⟹
locs l
(λb. if z = c ⟶ Q b then loc (c, b) else u b) =
locs l (λa. loc (c, a))"
by (induct l, auto)

lemma nth_rev_equalityI:
"⟦length xs = length ys; ∀i<length xs. xs ! (length xs - Suc i) = ys ! (length ys - Suc i)⟧
⟹ xs = ys"
proof (induct xs ys rule: list_induct2)
case Nil
thus ?case by simp
next
case (Cons x xs y ys)
hence "∀i<length ys. xs ! (length ys - Suc i) = ys ! (length ys - Suc i)"
apply auto
apply (erule_tac x="i" in allE)
by (auto simp: nth_Cons')
with Cons show ?case
by (auto simp: nth_Cons)
qed

lemma length_locss:
"i < length cs
⟹ length (locss P cs loc ! (length cs - Suc i)) =
locLength P (fst(cs ! (length cs - Suc i)))
(fst(snd(cs ! (length cs - Suc i))))
(snd(snd(cs ! (length cs - Suc i))))"
apply (induct cs, auto)
apply (case_tac "i = length cs")
by (auto simp: nth_Cons')

lemma locss_invoke_purge:
"z > length cs ⟹
locss P cs
(λ(a, b). if (a = z ⟶ Q b)
then loc (a, b)
else u b)
= locss P cs loc"
by (induct cs, auto simp: locs_invoke_purge [simplified])

lemma stks_purge':
"d ≥ b ⟹ stks b (λx. if x = d then e else stk x) = stks b stk"
by simp

subsection ‹Byte code verifier conformance›

text ‹Here we prove state conformance invariant under ‹transfer› for
our CFG. Therefore, we must assume, that the predicate of a potential preceding
predicate-edge holds for every update-edge.
›

theorem bv_invariant:
"⟦ valid_edge (P,C0,Main) a;
sourcenode a = (_ (C,M,pc)#cs,x _);
targetnode a = (_ (C',M',pc')#cs',x' _);
pred (kind a) s;
x ≠ None ⟶ (∃a_pred.
sourcenode a_pred = (_ (C,M,pc)#cs,None _) ∧
targetnode a_pred = sourcenode a ∧
valid_edge (P,C0,Main) a_pred ∧
pred (kind a_pred) s
);
P,((C,M,pc)#cs) ⊢⇘BV⇙ s √ ⟧
⟹ P,((C',M',pc')#cs') ⊢⇘BV⇙ transfer (kind a) s √"
proof -
assume ve: "valid_edge (P, C0, Main) a"
and src [simp]: "sourcenode a = (_ (C,M,pc)#cs,x _)"
and trg [simp]: "targetnode a = (_ (C',M',pc')#cs',x' _)"
and pred_s: "pred (kind a) s"
and a_pred: "x ≠ None ⟶ (∃a_pred.
sourcenode a_pred = (_ (C,M,pc)#cs,None _) ∧
targetnode a_pred = sourcenode a ∧
valid_edge (P,C0,Main) a_pred ∧
pred (kind a_pred) s
)"
and state_correct: "P,((C,M,pc)#cs) ⊢⇘BV⇙ s √"
obtain h stk loc where s [simp]: "s = (h,stk,loc)" by (cases s, fastforce)
note P_wf = wf_jvmprog_is_wf [of P]
from ve obtain Ts T mxs mxl "is" xt
where sees_M: "(P⇘wf⇙) ⊢ C sees M:Ts→T = (mxs,mxl,is,xt) in C"
and "pc < length is"
and reachable: "P⇘Φ⇙ C M ! pc ≠ None"
by (cases x) (cases cs, auto)+
from P_wf sees_M
have wt_method: "wt_method (P⇘wf⇙) C Ts T mxs mxl is xt (P⇘Φ⇙ C M)"
by (auto dest: sees_wf_mdecl simp: wf_jvm_prog_phi_def wf_mdecl_def)
with sees_M ‹pc < length is› reachable
have applicable: "app⇩i ((is ! pc),(P⇘wf⇙),pc,mxs,T,(the(P⇘Φ⇙ C M ! pc)))"
by (auto simp: wt_method_def)
from state_correct ve P_wf
have trg_state_correct:
"(P⇘wf⇙),(P⇘Φ⇙) ⊢ the (JVMExec.exec ((P⇘wf⇙), state_to_jvm_state P ((C,M,pc)#cs) s)) √"
apply simp
apply (drule BV_correct_1)
apply (fastforce simp: bv_conform_def)
apply (cases "instrs_of (P⇘wf⇙) C M ! pc")
done
from reachable obtain ST LT where reachable: "(P⇘Φ⇙) C M ! pc = ⌊(ST, LT)⌋"
by fastforce
with wt_method sees_M ‹pc < length is›
have stk_loc_succs:
"∀pc' ∈ set (succs (is ! pc) (ST, LT) pc).
stkLength P C M pc' = length (fst (eff⇩i (is ! pc, (P⇘wf⇙), ST, LT))) ∧
locLength P C M pc' = length (snd (eff⇩i (is ! pc, (P⇘wf⇙), ST, LT)))"
unfolding wt_method_def apply (cases "is ! pc")
using [[simproc del: list_to_set_comprehension]]
apply (cases "is ! pc")
apply (tactic ‹PARALLEL_ALLGOALS
done
have [simp]: "∃x. x" by auto
have [simp]: "Ex Not" by auto
show ?thesis
proof (cases "instrs_of (P⇘wf⇙) C M ! pc")
case (Invoke m n)
from state_correct have "preallocated h"
by (clarsimp simp: bv_conform_def correct_state_def hconf_def)
from Invoke applicable sees_M have "stkLength P C M pc > n"
by (cases "the (P⇘Φ⇙ C M ! pc)") auto
show ?thesis
proof (cases x)
case [simp]: None
with ve Invoke obtain Q where kind: "kind a = (Q)⇩√"
by (auto elim!: JVM_CFG.cases)
with ve Invoke have "(C',M',pc')#cs' = (C,M,pc)#cs"
by (auto elim!: JVM_CFG.cases)
with state_correct kind show ?thesis
by simp
next
case [simp]: (Some aa)
with ve Invoke obtain xf where [simp]: "aa = ((C',M',pc')#cs' , xf)"
by (auto elim!: JVM_CFG.cases)
from ve Invoke obtain f where kind: "kind a = ⇑f"
apply -
apply clarsimp
apply (erule JVM_CFG.cases)
apply auto
done
show ?thesis
proof (cases xf)
case [simp]: True
with a_pred Invoke have stk_n: "stk (length cs, stkLength P C M pc - Suc n) = Null"
apply auto
apply (erule JVM_CFG.cases)
apply simp_all
done
from ve Invoke kind
have [simp]: "f = (λ(h,stk,loc).
(h,
stk((length cs',(stkLength P C' M' pc') - 1) := Addr (addr_of_sys_xcpt NullPointer)),
loc))"
apply -
apply clarsimp
apply (erule JVM_CFG.cases)
apply auto
done
from ve Invoke
have "find_handler_for P NullPointer ((C,M,pc)#cs) = (C',M',pc')#cs'"
apply -
apply clarsimp
apply (erule JVM_CFG.cases)
apply auto
done
with Invoke state_correct kind stk_n trg_state_correct applicable sees_M
‹preallocated h›
show ?thesis
apply (cases "the (P⇘Φ⇙ C M ! pc)",
auto simp: bv_conform_def stkss_purge
simp del: find_handler_for.simps exec.simps app⇩i.simps fun_upd_apply)
apply (rule_tac cs="(C,M,pc)#cs" in find_handler_exec_correct)
apply fastforce
apply (fastforce simp: split_beta split: if_split_asm)
apply fastforce
done
next
case [simp]: False
from a_pred Invoke
have [simp]: "m = M'"
by -(clarsimp, erule JVM_CFG.cases, auto)
from a_pred Invoke
have [simp]: "pc' = 0"
by -(clarsimp, erule JVM_CFG.cases, auto)
from ve Invoke
have [simp]: "cs' = (C,M,pc)#cs"
by -(clarsimp, erule JVM_CFG.cases, auto)
from ve Invoke kind
have [simp]:
"f = (λs. exec_instr (Invoke m n) P s (length cs) (stkLength P C M pc)
arbitrary (locLength P C' M' 0))"
by -(clarsimp, erule JVM_CFG.cases, auto)
from state_correct obtain ST LT where [simp]:
"(P⇘Φ⇙) C M ! pc = ⌊(ST,LT)⌋"
by (auto simp: bv_conform_def correct_state_def)
from a_pred Invoke
have [simp]:
"fst (method (P⇘wf⇙)
(cname_of h (the_Addr (stk (length cs, length ST - Suc n)))) M') = C'"
by -(clarsimp, erule JVM_CFG.cases, auto)
from a_pred Invoke
have [simp]: "stk (length cs, length ST - Suc n) ≠ Null"
by -(clarsimp, erule JVM_CFG.cases, auto)
from state_correct applicable sees_M Invoke
have [simp]: "ST ! n ≠ NT"
apply (auto simp: correct_state_def bv_conform_def)
apply (drule_tac p="n" and ys="ST" in list_all2_nthD)
apply simp
by clarsimp
from applicable Invoke sees_M
have "length ST > n"
by auto
with trg_state_correct Invoke
have [simp]: "stkLength P C' M' 0 = 0"
by (auto simp: split_beta correct_state_def
split: if_split_asm)
from trg_state_correct Invoke ‹length ST > n›
have "locLength P C' M' 0 =
Suc n + fst(snd(snd(snd(snd(method (P⇘wf⇙)
(cname_of h (the_Addr (stk (length cs, length ST - Suc n)))) M')))))"
by (auto simp: split_beta  (* nth_stks *) correct_state_def
dest!: list_all2_lengthD
split: if_split_asm)
with Invoke state_correct trg_state_correct ‹length ST > n›
have "JVMExec.exec  (P⇘wf⇙, state_to_jvm_state P ((C, M, pc) # cs) s)
=
⌊(None, h,
(stks (stkLength P C' M' pc') (λa. stk (Suc (length cs), a)),
locs (locLength P C' M' pc')
(λa'. (λ(a, b).
if a = Suc (length cs) ⟶ locLength P C' M' 0 ≤ b then loc (a, b)
else if b ≤ n then stk (length cs, length ST - (Suc n - b))
else arbitrary) (Suc (length cs), a')),
C', M', pc') #
(stks (length ST) (λa. stk (length cs, a)),
locs (length LT) (λa. loc (length cs, a)), C, M, pc) #
zip (stkss P cs stk) (zip (locss P cs loc) cs))⌋"
apply (auto simp: split_beta  (* nth_stks *) bv_conform_def)
apply (rule nth_equalityI)
apply simp
apply (cases ST,
auto simp: nth_Cons' nth_append min.absorb1 min.absorb2)
apply (rule nth_equalityI)
apply simp
by (auto simp: (* nth_locs *) (* nth_stks *) rev_nth nth_Cons' nth_append min_def)
with Invoke state_correct kind trg_state_correct applicable sees_M
show ?thesis
apply (cases "the (P⇘Φ⇙ C M ! pc)",
auto simp: bv_conform_def stkss_purge rev_nth (* nth_stks *)
simp del: find_handler_for.simps exec.simps app⇩i.simps)
apply(subst locss_invoke_purge, simp)
by simp
qed
qed
next
with stk_loc_succs sees_M reachable
have "stkLength P C M (Suc pc) = Suc (stkLength P C M pc)"
and "locLength P C M (Suc pc) = locLength P C M pc"
by simp_all
with state_correct ve P_wf applicable sees_M Load trg_state_correct
show ?thesis
apply auto
apply (erule JVM_CFG.cases, simp_all)
by (auto simp: bv_conform_def stkss_purge stks_purge')
next
case (Store nat)
with stk_loc_succs sees_M reachable applicable
have "stkLength P C M (Suc pc) = stkLength P C M pc - 1"
and "locLength P C M (Suc pc) = locLength P C M pc"
by auto
with state_correct ve P_wf applicable sees_M Store trg_state_correct
show ?thesis
apply auto
apply (erule JVM_CFG.cases, simp_all)
by (auto simp: bv_conform_def locss_purge)
next
case (Push val)
with stk_loc_succs sees_M reachable applicable
have "stkLength P C M (Suc pc) = Suc (stkLength P C M pc)"
and "locLength P C M (Suc pc) = locLength P C M pc"
by auto
with state_correct ve P_wf applicable sees_M Push trg_state_correct
show ?thesis
apply auto
apply (erule JVM_CFG.cases, simp_all)
by (auto simp: bv_conform_def stks_purge' stkss_purge)
next
case Pop
with stk_loc_succs sees_M reachable applicable
have "stkLength P C M (Suc pc) = stkLength P C M pc - 1"
and "locLength P C M (Suc pc) = locLength P C M pc"
by auto
with state_correct ve P_wf applicable sees_M Pop trg_state_correct
show ?thesis
apply auto
apply (erule JVM_CFG.cases, simp_all)
by (auto simp: bv_conform_def)
next
with stk_loc_succs sees_M reachable applicable
have "stkLength P C M (Suc pc) = stkLength P C M pc - 1"
and "locLength P C M (Suc pc) = locLength P C M pc"
by auto
with state_correct ve P_wf applicable sees_M IAdd trg_state_correct
show ?thesis
apply auto
apply (erule JVM_CFG.cases, simp_all)
by (auto simp: bv_conform_def stks_purge' stkss_purge add.commute)
next
case CmpEq
with stk_loc_succs sees_M reachable applicable
have "stkLength P C M (Suc pc) = stkLength P C M pc - 1"
and "locLength P C M (Suc pc) = locLength P C M pc"
by auto
with state_correct ve P_wf applicable sees_M CmpEq trg_state_correct
show ?thesis
apply auto
apply (erule JVM_CFG.cases, simp_all)
apply (auto simp: bv_conform_def stks_purge' stkss_purge bool_sym)
apply (erule JVM_CFG.cases, simp_all)
by (auto simp: bv_conform_def stks_purge' stkss_purge bool_sym)
next
case (Goto b)
with stk_loc_succs sees_M reachable applicable
have "stkLength P C M (nat (int pc + b)) = stkLength P C M pc"
and "locLength P C M (nat (int pc + b)) = locLength P C M pc"
by auto
with state_correct ve P_wf applicable sees_M Goto trg_state_correct
show ?thesis
apply auto
by (erule JVM_CFG.cases, simp_all add: bv_conform_def)
next
case (IfFalse b)
have nat_int_pc_conv: "nat (int pc + 1) = pc + 1"
by (cases pc) auto
from IfFalse stk_loc_succs sees_M reachable applicable
have "stkLength P C M (Suc pc) = stkLength P C M pc - 1"
and "stkLength P C M (nat (int pc + b)) = stkLength P C M pc - 1"
and "locLength P C M (Suc pc) = locLength P C M pc"
and "locLength P C M (nat (int pc + b)) = locLength P C M pc"
by auto
with state_correct ve P_wf applicable sees_M IfFalse pred_s nat_int_pc_conv
trg_state_correct
show ?thesis
apply auto
apply (erule JVM_CFG.cases, simp_all)
by (auto simp: bv_conform_def split: if_split_asm)
next
case Return
with ve obtain Ts' T' mxs' mxl' is' xt'
where sees_M': "(P⇘wf⇙) ⊢ C' sees M':Ts'→T' = (mxs',mxl',is',xt') in C'"
and "(pc' - 1) < length is'"
and reachable': "P⇘Φ⇙ C' M' ! (pc' - 1) ≠ None"
apply auto
apply (erule JVM_CFG.cases, auto)
by (cases cs', auto)
with Return ve wt_method sees_M applicable
have "is' ! (pc' - 1) = Invoke M (length Ts)"
apply auto
apply (erule JVM_CFG.cases, auto)
apply (drule sees_method_fun, fastforce, clarsimp)
by (auto dest!: list_all2_lengthD simp: wt_method_def wt_start_def)
from P_wf sees_M'
have "wt_method (P⇘wf⇙) C' Ts' T' mxs' mxl' is' xt' (P⇘Φ⇙ C' M')"
by (auto dest: sees_wf_mdecl simp: wf_jvm_prog_phi_def wf_mdecl_def)
with ve Return ‹pc' - 1 < length is'› reachable' sees_M state_correct
have "stkLength P C' M' pc' = stkLength P C' M' (pc' - 1) - length Ts"
using [[simproc del: list_to_set_comprehension]]
apply auto
apply (erule JVM_CFG.cases, auto)
apply (drule sees_method_fun, fastforce, clarsimp)
using sees_M'
apply hypsubst_thin
apply (auto simp: wt_method_def)
apply (erule_tac x="pc'" in allE)
apply (auto simp: bv_conform_def correct_state_def not_less_eq less_Suc_eq)
apply (drule sees_method_fun, fastforce, clarsimp)
apply (drule sees_method_fun, fastforce, clarsimp)
apply (auto simp: wt_start_def)
apply (auto dest!: list_all2_lengthD)
apply (drule sees_method_fun, fastforce, clarsimp)
apply (drule sees_method_fun, fastforce, clarsimp)
by auto
from ‹wt_method (P⇘wf⇙) C' Ts' T' mxs' mxl' is' xt' (P⇘Φ⇙ C' M')›
‹(pc' - 1) < length is'› ‹P⇘Φ⇙ C' M' ! (pc' - 1) ≠ None›
‹is' ! (pc' - 1) = Invoke M (length Ts)›
have "stkLength P C' M' (pc' - 1) > 0"
by (fastforce simp: wt_method_def)
then obtain ST' STr' where [simp]: "fst (the (P⇘Φ⇙ C' M' ! (pc' - 1))) = ST'#STr'"
by (cases "fst (the (P⇘Φ⇙ C' M' ! (pc' - 1)))", fastforce+)
from wt_method
have "locLength P C M 0 = Suc (length Ts) + mxl"
by (auto dest!: list_all2_lengthD
simp: wt_method_def wt_start_def)
from ‹wt_method (P⇘wf⇙) C' Ts' T' mxs' mxl' is' xt' (P⇘Φ⇙ C' M')›
ve Return ‹pc' - 1 < length is'› reachable' sees_M state_correct
have "locLength P C' M' (pc' - 1) = locLength P C' M' pc'"
using [[simproc del: list_to_set_comprehension]]
apply auto
apply (erule JVM_CFG.cases, auto)
apply (drule sees_method_fun, fastforce, clarsimp)
using sees_M'
apply hypsubst_thin
apply (auto simp: wt_method_def)
apply (erule_tac x="pc'" in allE)
apply (auto simp: wt_start_def)
apply (clarsimp simp: bv_conform_def correct_state_def)
apply (drule sees_method_fun, fastforce, clarsimp)
apply (drule sees_method_fun, fastforce, clarsimp)
by (auto dest!: list_all2_lengthD)
with ‹stkLength P C' M' pc' = stkLength P C' M' (pc' - 1) - length Ts›
Return state_correct ve P_wf applicable sees_M trg_state_correct sees_M'
‹fst (the (P⇘Φ⇙ C' M' ! (pc' - 1))) = ST'#STr'› ‹is' ! (pc' - 1) = Invoke M (length Ts)›
‹locLength P C M 0 = Suc (length Ts) + mxl›
show ?thesis
apply (auto simp: bv_conform_def)
apply (erule JVM_CFG.cases, auto simp: stkss_purge locss_purge)
apply (drule sees_method_fun, fastforce, clarsimp)
apply (auto simp: correct_state_def)
apply (drule sees_method_fun, fastforce, clarsimp)
apply (drule sees_method_fun, fastforce, clarsimp)
apply (drule sees_method_fun, fastforce, clarsimp)
apply (rule_tac x="Ts'" in exI)
apply (rule_tac x="T'" in exI)
apply (rule_tac x="mxs'" in exI)
apply (rule_tac x="mxl'" in exI)
apply (rule_tac x="is'" in exI)
apply clarsimp
apply (rule conjI)
apply (rule_tac x="xt'" in exI)
apply clarsimp
apply (rule list_all2_all_nthI)
apply clarsimp
apply clarsimp
apply (auto simp: rev_nth (* nth_stks *) list_all2_Cons1)
apply (case_tac n, auto simp: list_all2_Cons1)
apply (case_tac n, auto simp: list_all2_Cons1)
apply (drule_tac p="nat" and ys="zs" in list_all2_nthD2)
apply clarsimp
by auto
next
case (New Cl)
from state_correct have "preallocated h"
by (clarsimp simp: bv_conform_def correct_state_def hconf_def)
from New stk_loc_succs sees_M reachable applicable
have "stkLength P C M (Suc pc) = Suc (stkLength P C M pc)"
and "locLength P C M (Suc pc) = locLength P C M pc"
by auto
with New state_correct ve sees_M trg_state_correct applicable a_pred ‹preallocated h›
show ?thesis
apply (clarsimp simp del: exec.simps)
apply (erule JVM_CFG.cases, simp_all del: exec.simps find_handler_for.simps)
apply (clarsimp simp del: exec.simps find_handler_for.simps)
apply (erule JVM_CFG.cases, simp_all del: exec.simps find_handler_for.simps)
apply (clarsimp simp del: exec.simps find_handler_for.simps)
defer
apply (clarsimp simp del: exec.simps find_handler_for.simps)
apply (erule JVM_CFG.cases, simp_all del: exec.simps find_handler_for.simps)
apply (clarsimp simp del: exec.simps find_handler_for.simps)
apply (simp add: bv_conform_def stkss_purge del: exec.simps find_handler_for.simps)
apply (rule_tac cs="(C,M,pc)#cs" in find_handler_exec_correct [simplified])
apply fastforce
apply fastforce
apply clarsimp
by (auto simp: split_beta bv_conform_def stks_purge' stkss_purge
simp del: find_handler_for.simps)
next
case (Getfield Fd Cl)
from state_correct have "preallocated h"
by (clarsimp simp: bv_conform_def correct_state_def hconf_def)
from Getfield stk_loc_succs sees_M reachable applicable
have "stkLength P C M (Suc pc) = stkLength P C M pc"
and "locLength P C M (Suc pc) = locLength P C M pc"
by auto
with Getfield state_correct ve sees_M trg_state_correct applicable a_pred ‹preallocated h›
show ?thesis
apply (clarsimp simp del: exec.simps)
apply (erule JVM_CFG.cases, simp_all del: exec.simps find_handler_for.simps)
apply (clarsimp simp del: exec.simps find_handler_for.simps)
apply (erule JVM_CFG.cases, simp_all del: exec.simps find_handler_for.simps)
apply (clarsimp simp del: exec.simps find_handler_for.simps)
defer
apply (clarsimp simp del: exec.simps find_handler_for.simps)
apply (erule JVM_CFG.cases, simp_all del: exec.simps find_handler_for.simps)
apply (clarsimp simp del: exec.simps find_handler_for.simps)
apply (simp add: bv_conform_def stkss_purge del: exec.simps find_handler_for.simps)
apply (rule_tac cs="(C,M,pc)#cs" in find_handler_exec_correct [simplified])
apply fastforce
apply (fastforce simp: split_beta)
apply clarsimp
by (auto simp: split_beta bv_conform_def stks_purge' stkss_purge
simp del: find_handler_for.simps)
next
case (Putfield Fd Cl)
from state_correct have "preallocated h"
by (clarsimp simp: bv_conform_def correct_state_def hconf_def)
from Putfield stk_loc_succs sees_M reachable applicable
have "stkLength P C M (Suc pc) = stkLength P C M pc - 2"
and "locLength P C M (Suc pc) = locLength P C M pc"
by auto
with Putfield state_correct ve sees_M trg_state_correct applicable a_pred ‹preallocated h›
show ?thesis
apply (clarsimp simp del: exec.simps)
apply (erule JVM_CFG.cases, simp_all del: exec.simps find_handler_for.simps)
apply (clarsimp simp del: exec.simps find_handler_for.simps)
apply (erule JVM_CFG.cases, simp_all del: exec.simps find_handler_for.simps)
apply (clarsimp simp del: exec.simps find_handler_for.simps)
defer
apply (clarsimp simp del: exec.simps find_handler_for.simps)
apply (erule JVM_CFG.cases, simp_all del: exec.simps find_handler_for.simps)
apply (clarsimp simp del: exec.simps find_handler_for.simps)
apply (simp add: bv_conform_def stkss_purge del: exec.simps find_handler_for.simps)
apply (rule_tac cs="(C,M,pc)#cs" in find_handler_exec_correct [simplified])
apply fastforce
apply (fastforce simp: split_beta)
apply clarsimp
by (auto simp: split_beta bv_conform_def stks_purge' stkss_purge
simp del: find_handler_for.simps)
next
case (Checkcast Cl)
from state_correct have "preallocated h"
by (clarsimp simp: bv_conform_def correct_state_def hconf_def)
from Checkcast stk_loc_succs sees_M reachable applicable
have "stkLength P C M (Suc pc) = stkLength P C M pc"
and "locLength P C M (Suc pc) = locLength P C M pc"
by auto
with Checkcast state_correct ve sees_M
trg_state_correct applicable a_pred pred_s ‹preallocated h›
show ?thesis
apply (clarsimp simp del: exec.simps)
apply (erule JVM_CFG.cases, simp_all del: exec.simps find_handler_for.simps)
apply (clarsimp simp del: exec.simps find_handler_for.simps)
defer
apply (clarsimp simp del: exec.simps find_handler_for.simps)
apply (erule JVM_CFG.cases, simp_all del: exec.simps find_handler_for.simps)
apply (clarsimp simp del: exec.simps find_handler_for.simps)
apply (simp add: bv_conform_def stkss_purge del: exec.simps find_handler_for.simps)
apply (rule_tac cs="(C,M,pc)#cs" in find_handler_exec_correct [simplified])
apply fastforce
apply (fastforce simp: split_beta)
apply clarsimp
by (auto simp: split_beta bv_conform_def
simp del: find_handler_for.simps)
next
case Throw
from state_correct have "preallocated h"
by (clarsimp simp: bv_conform_def correct_state_def hconf_def)
from Throw applicable state_correct sees_M obtain a
where "stk(length cs, stkLength P C M pc - 1) = Null ∨
stk(length cs, stkLength P C M pc - 1) = Addr a"
by (cases "stk(length cs, stkLength P C M pc - 1)",
auto simp: is_refT_def bv_conform_def correct_state_def conf_def)
with Throw state_correct ve trg_state_correct a_pred applicable sees_M ‹preallocated h›
show ?thesis
apply (clarsimp simp del: exec.simps)
apply (erule JVM_CFG.cases, simp_all del: exec.simps find_handler_for.simps)
apply (clarsimp simp del: exec.simps find_handler_for.simps)
apply (erule JVM_CFG.cases, simp_all del: exec.simps find_handler_for.simps)
apply (clarsimp simp: bv_conform_def simp del: exec.simps find_handler_for.simps)
apply (rule conjI)
apply (clarsimp simp: stkss_purge simp del: exec.simps find_handler_for.simps)
apply (rule_tac cs="(C,M,pc)#cs" in find_handler_exec_correct [simplified])
apply fastforce
apply simp
apply (clarsimp simp: stkss_purge simp del: exec.simps find_handler_for.simps)
apply (simp del: find_handler_for.simps exec.simps cong: if_cong)
apply (rule_tac cs="(C,M,pc)#cs" in find_handler_exec_correct [simplified])
apply fastforce
by simp
qed
qed

section ‹CFG simulates Jinja's semantics›

subsection ‹Definitions›

text ‹
The following predicate defines the semantics of Jinja lifted to our
state representation. Thereby, we require the state to be byte code verifier
conform; otherwise the step in the semantics is undefined.

The predicate ‹valid_callstack› is actually an implication of the
byte code verifier conformance. But we list it explicitly for convenience.
›

inductive sem :: "jvmprog ⇒ callstack ⇒ state ⇒ callstack ⇒ state ⇒ bool"
("_ ⊢ ⟨_,_⟩ ⇒ ⟨_,_⟩")
where Step:
"⟦ prog = (P,C0,Main);
P,cs ⊢⇘BV⇙ s √;
valid_callstack prog cs;
JVMExec.exec ((P⇘wf⇙), state_to_jvm_state P cs s) = ⌊(None,h',frs')⌋;
cs' = framestack_to_callstack frs';
s = (h, stk, loc);
s' = (h', update_stk stk frs', update_loc loc frs') ⟧
⟹ prog ⊢ ⟨cs,s⟩ ⇒ ⟨cs',s'⟩"

abbreviation identifies :: "j_node ⇒ callstack ⇒ bool"
where "identifies n cs ≡ (n = (_ cs,None _))"

subsection ‹Some more simplification lemmas›

lemma valid_callstack_tl:
"valid_callstack prog ((C,M,pc)#cs) ⟹ valid_callstack prog cs"
by (cases prog, cases cs, auto)

lemma stkss_cong [cong]:
"⟦ P = P';
cs = cs';
⋀a b. ⟦ a < length cs;
b < stkLength P (fst(cs ! (length cs - Suc a)))
(fst(snd(cs ! (length cs - Suc a))))
(snd(snd(cs ! (length cs - Suc a)))) ⟧
⟹ stk (a, b) = stk' (a, b) ⟧
⟹ stkss P cs stk = stkss P' cs' stk'"
by (auto, hypsubst_thin, induct cs',
auto intro!: nth_equalityI simp: nth_Cons' (* nth_stks *))

lemma locss_cong [cong]:
"⟦ P = P';
cs = cs';
⋀a b. ⟦ a < length cs;
b < locLength P (fst(cs ! (length cs - Suc a)))
(fst(snd(cs ! (length cs - Suc a))))
(snd(snd(cs ! (length cs - Suc a)))) ⟧
⟹ loc (a, b) = loc' (a, b) ⟧
⟹ locss P cs loc = locss P' cs' loc'"
by (auto, hypsubst_thin, induct cs',
auto intro!: nth_equalityI simp: nth_Cons' (* nth_locs *))

lemma hd_tl_equalityI:
"⟦ length xs = length ys; hd xs = hd ys; tl xs = tl ys ⟧ ⟹ xs = ys"
apply (induct xs arbitrary: ys)
apply simp
by (case_tac ys, auto)

lemma stkLength_is_length_stk:
"P⇘wf⇙,P⇘Φ⇙ ⊢ (None, h, (stk, loc, C, M, pc) # frs') √ ⟹ stkLength P C M pc = length stk"
by (auto dest!: list_all2_lengthD simp: correct_state_def)

lemma locLength_is_length_loc:
"P⇘wf⇙,P⇘Φ⇙ ⊢ (None, h, (stk, loc, C, M, pc) # frs') √ ⟹ locLength P C M pc = length loc"
by (auto dest!: list_all2_lengthD simp: correct_state_def)

lemma correct_state_frs_tlD:
"(P⇘wf⇙),(P⇘Φ⇙) ⊢ (None, h, a # frs') √ ⟹ (P⇘wf⇙),(P⇘Φ⇙) ⊢ (None, h, frs') √"
by (cases frs', (fastforce simp: correct_state_def)+)

lemma update_stk_Cons [simp]:
"stkss P (framestack_to_callstack frs') (update_stk stk ((stk', loc', C', M', pc') # frs')) =
stkss P (framestack_to_callstack frs') (update_stk stk frs')"
apply (induct frs' arbitrary: stk' loc' C' M' pc')
apply clarsimp
apply (simp only: f2c_Nil)
apply clarsimp
apply clarsimp
apply (simp only: f2c_Cons)
apply clarsimp
apply (rule stkss_cong)
by (fastforce simp: nth_Cons')+

lemma update_loc_Cons [simp]:
"locss P (framestack_to_callstack frs') (update_loc loc ((stk', loc', C', M', pc') # frs')) =
locss P (framestack_to_callstack frs') (update_loc loc frs')"
apply (induct frs' arbitrary: stk' loc' C' M' pc')
apply clarsimp
apply (simp only: f2c_Nil)
apply clarsimp
apply clarsimp
apply (simp only: f2c_Cons)
apply clarsimp
apply (rule locss_cong)
by (fastforce simp: nth_Cons')+

lemma s2j_id:
"(P⇘wf⇙),(P⇘Φ⇙) ⊢ (None,h',frs') √
⟹ state_to_jvm_state P (framestack_to_callstack frs')
(h, update_stk stk frs', update_loc loc frs') = (None, h, frs')"
apply (induct frs')
apply simp
apply simp
apply (rule hd_tl_equalityI)
apply simp
apply simp
apply clarsimp
apply (simp only: f2c_Cons fst_conv snd_conv)
apply clarsimp
apply (rule conjI)
apply (rule nth_equalityI)
apply (clarsimp simp: (* nth_stks *) stkLength_is_length_stk)
apply (case_tac a, simp_all)
apply (rule nth_equalityI)
apply (clarsimp simp: (* nth_locs *) locLength_is_length_loc)
apply (drule correct_state_frs_tlD)
apply simp
apply clarsimp
apply (simp only: f2c_Cons fst_conv snd_conv)
by clarsimp

lemma find_handler_last_cs_eqD:
"⟦ find_handler P⇘wf⇙ a h frs = (None, h', frs');
last frs = (stk,loc,C,M,pc);
last frs' = (stk',loc',C',M',pc') ⟧
⟹ C = C' ∧ M = M'"
by (induct frs, auto split: if_split_asm)

lemma exec_last_frs_eq_class:
"⟦ JVMExec.exec (P⇘wf⇙, None, h, frs) = ⌊(None, h', frs')⌋;
last frs = (stk, loc, C, M, pc);
last frs' = (stk', loc', C', M', pc');
frs ≠ [];
frs' ≠ [] ⟧
⟹ C = C'"
apply (cases frs, auto split: if_split_asm)
apply (cases "instrs_of P⇘wf⇙ C M ! pc", auto simp: split_beta)
apply (case_tac "instrs_of P⇘wf⇙ ab ac ! b", auto simp: split_beta)
apply (case_tac list, auto)
apply (case_tac lista, auto)
apply (drule find_handler_last_cs_eqD)
apply fastforce
apply fastforce
by simp

lemma exec_last_frs_eq_method:
"⟦ JVMExec.exec (P⇘wf⇙, None, h, frs) = ⌊(None, h', frs')⌋;
last frs = (stk, loc, C, M, pc);
last frs' = (stk', loc', C', M', pc');
frs ≠ [];
frs' ≠ [] ⟧
⟹ M = M'"
apply (cases frs, auto split: if_split_asm)
apply (cases "instrs_of P⇘wf⇙ C M ! pc", auto simp: split_beta)
apply (case_tac "instrs_of P⇘wf⇙ ab ac ! b", auto simp: split_beta)
apply (case_tac list, auto)
apply (case_tac lista, auto)
apply (drule find_handler_last_cs_eqD)
apply fastforce
apply fastforce
by simp

lemma valid_callstack_append_last_class:
"valid_callstack (P,C0,Main) (cs@[(C,M,pc)]) ⟹ C = C0"
by (induct cs, auto dest: valid_callstack_tl)

lemma valid_callstack_append_last_method:
"valid_callstack (P,C0,Main) (cs@[(C,M,pc)]) ⟹ M = Main"
by (induct cs, auto dest: valid_callstack_tl)

lemma zip_stkss_locss_append_single [simp]:
"zip (stkss P (cs @ [(C, M, pc)]) stk)
(zip (locss P (cs @ [(C, M, pc)]) loc) (cs @ [(C, M, pc)]))
= (zip (stkss P (cs @ [(C, M, pc)]) stk) (zip (locss P (cs @ [(C, M, pc)]) loc) cs))
@ [(stks (stkLength P C M pc) (λa. stk (0, a)),
locs (locLength P C M pc) (λa. loc (0, a)), C, M, pc)]"
by (induct cs, auto)

subsection ‹Interpretation of the ‹CFG_semantics_wf› locale›

interpretation JVM_semantics_CFG_wf:
CFG_semantics_wf "sourcenode" "targetnode" "kind" "valid_edge prog" "(_Entry_)"
"sem prog" "identifies"
for prog
proof(unfold_locales)
fix n c s c' s'
assume sem_step:"prog ⊢ ⟨c,s⟩ ⇒ ⟨c',s'⟩"
and "identifies n c"
obtain P C0 M0
where prog [simp]:"prog = (P,C0,M0)"
by (cases prog,fastforce)
obtain h stk loc
where s [simp]: "s = (h,stk,loc)"
by (cases s, fastforce)
obtain h' stk' loc'
where s' [simp]: "s' = (h',stk',loc')"
by (cases s', fastforce)
from sem_step s s' prog obtain C M pc cs C' M' pc' cs'
where c [simp]: "c = (C,M,pc)#cs"
by (cases c, auto elim: sem.cases simp: bv_conform_def)
with sem_step prog obtain ST LT
where wt [simp]: " (P⇘Φ⇙) C M ! pc = ⌊(ST,LT)⌋"
by (auto elim!: sem.cases, cases cs, fastforce+)
note P_wf = wf_jvmprog_is_wf [of P]
from sem_step prog obtain frs'
where jvm_exec: "JVMExec.exec ((P⇘wf⇙), state_to_jvm_state P c s) = ⌊(None,h',frs')⌋"
by (auto elim!: sem.cases)
with sem_step prog s s'
have loc': "loc' = update_loc loc frs'"
and stk': "stk' = update_stk stk frs'"
by (auto elim!: sem.cases)
from sem_step s prog
have state_wf: "P,c ⊢⇘BV⇙ (h,stk,loc) √"
by (auto elim!: sem.cases)
hence state_correct: "(P⇘wf⇙),(P⇘Φ⇙) ⊢ state_to_jvm_state P c (h,stk,loc) √"
with P_wf jvm_exec s
have trg_state_correct: "(P⇘wf⇙),(P⇘Φ⇙) ⊢ (None,h',frs') √"
by -(rule BV_correct_1, (fastforce simp: exec_1_iff)+)
from sem_step c s prog have prealloc: "preallocated h"
by (auto elim: sem.cases
simp: bv_conform_def correct_state_def hconf_def)
from state_correct obtain Ts T mxs mxl "is" xt
where sees_M: "(P⇘wf⇙) ⊢ C sees M:Ts→T = (mxs,mxl,is,xt) in C"
by (clarsimp simp: bv_conform_def correct_state_def)
with state_correct
have "pc < length is"
by (auto dest: sees_method_fun
simp: bv_conform_def correct_state_def)
with P_wf sees_M have
applicable: "app⇩i(is ! pc, (P⇘wf⇙), pc, mxs, T, ST, LT)"
by (fastforce dest!: sees_wf_mdecl
simp: wf_jvm_prog_phi_def wf_mdecl_def wt_method_def)
from sem_step
have v_cs: "valid_callstack prog c"
by (auto elim: sem.cases)
then obtain pcL where last_c: "last c = (C0,M0,pcL)"
apply clarsimp
apply (induct cs arbitrary: C M pc, simp)
by fastforce
from sees_M P_wf ‹pc < length is›
have wt_instrs: "P⇘wf⇙,T,mxs,length is,xt ⊢ is ! pc,pc :: (P⇘Φ⇙) C M"
by -(drule wt_jvm_prog_impl_wt_instr, fastforce+)
with applicable
have effect: "∀succ ∈ set (succs (is ! pc) (ST,LT) pc).
(P⇘wf⇙) ⊢ ⌊eff⇩i(is ! pc, (P⇘wf⇙), ST, LT)⌋ ≤' (P⇘Φ⇙) C M ! succ ∧ succ < length is"
apply clarsimp
apply (erule_tac x="(succ, ⌊eff⇩i(is ! pc, (P⇘wf⇙), ST, LT)⌋ )" in ballE)
by (erule_tac x="(succ, ⌊eff⇩i(is ! pc, (P⇘wf⇙), ST, LT)⌋ )" in ballE, clarsimp+)
with P_wf sees_M last_c v_cs
have v_cs_succ:
"∀succ ∈ set (succs (is ! pc) (ST,LT) pc). valid_callstack (P,C0,M0) ((C,M,succ)#cs)"
by -(rule ballI,
erule_tac x="succ" in ballE,
auto,
induct cs,
fastforce+)
from trg_state_correct v_cs jvm_exec
have v_cs_f2c_frs':
"valid_callstack (P,C0,M0) (framestack_to_callstack frs')"
apply (cases frs' rule: rev_cases, simp)
apply (rule_tac s="(h', update_stk stk frs', update_loc loc frs')"
in correct_state_imp_valid_callstack)
apply (simp only: bv_conform_def s2j_id)
apply (auto dest!: f2c_emptyD simp del: exec.simps)
apply (cases cs rule: rev_cases)
apply (clarsimp simp del: exec.simps)
apply (drule exec_last_frs_eq_class, fastforce+)
apply (clarsimp simp del: exec.simps)
apply (simp only: append_Cons [symmetric])
apply (frule valid_callstack_append_last_class)
apply (frule valid_callstack_append_last_method)
apply (clarsimp simp del: exec.simps)
apply (drule exec_last_frs_eq_class, fastforce+)
apply (cases cs rule: rev_cases)
apply (clarsimp simp del: exec.simps)
apply (drule exec_last_frs_eq_method, fastforce+)
apply (clarsimp simp del: exec.simps)
apply (simp only: append_Cons [symmetric])
apply (frule valid_callstack_append_last_method)
apply (clarsimp simp del: exec.simps)
by (drule exec_last_frs_eq_method, fastforce+)
show "∃n' as.
CFG.path sourcenode targetnode (valid_edge prog) n as n' ∧
transfers (CFG.kinds kind as) s = s' ∧
preds (CFG.kinds kind as) s ∧ identifies n' c'"
proof
show "∃as. CFG.path sourcenode targetnode (valid_edge prog) n as (_ c',None _) ∧
transfers (CFG.kinds kind as) s = s' ∧
preds (CFG.kinds kind as) s ∧
identifies (_ c',None _) c'"
proof (cases "(instrs_of (P⇘wf⇙) C M)!pc")
with sem_step s s' c prog
have c': "c' = (C,M,pc+1)#cs"
by (auto elim!: sem.cases)
have "nat < length LT"
by simp
from sees_M Load have "Suc pc ∈ set (succs (is ! pc) (ST,LT) pc)"
by simp
have v_edge:"valid_edge prog ((_ (C,M,pc)#cs,None _),
⇑(λs. exec_instr (instrs_of (P⇘wf⇙) C M ! pc) P s (length cs) (stkLength P C M pc) 0 0),
(_ (C,M,Suc pc)#cs,None _))"
(is "valid_edge prog ?e1")
by (auto elim!: sem.cases intro: JCFG_Straight_NoExc)
with ‹identifies n c› c c' have "JVM_CFG_Interpret.path prog n [?e1] (_ c',None _)"
by -(simp,
rule JVM_CFG_Interpret.path.Cons_path,
rule JVM_CFG_Interpret.path.empty_path,
auto simp: JVM_CFG_Interpret.valid_node_def, fastforce)
moreover from Load jvm_exec loc' stk' c c' s s' prog wt ‹nat < length LT›
have "transfers (JVM_CFG_Interpret.kinds [?e1]) s = s'"
by (auto intro!: ext
simp: JVM_CFG_Interpret.kinds_def
nth_stkss (* nth_stks *) nth_locss (* nth_locs *) nth_Cons' nth_tl
not_less_eq_eq Suc_le_eq)
moreover have "preds (JVM_CFG_Interpret.kinds [?e1]) s"
ultimately show ?thesis by fastforce
next
case (Store nat)
with sem_step s s' c prog
have c': "c' = (C,M,pc+1)#cs"
by (auto elim!: sem.cases)
from applicable Store sees_M
have "length ST > 0 ∧ nat < length LT"
by clarsimp
then obtain ST1 STr where [simp]: "ST = ST1#STr" by (cases ST, fastforce+)
from sees_M Store have "Suc pc ∈ set (succs (is ! pc) (ST, LT) pc)"
by simp
with prog sem_step Store v_cs_succ
have v_edge:"valid_edge prog ((_ (C,M,pc)#cs,None _),
⇑(λs. exec_instr (instrs_of (P⇘wf⇙) C M ! pc) P s (length cs) (stkLength P C M pc) 0 0),
(_ (C,M,Suc pc)#cs,None _))"
(is "valid_edge prog ?e1")
by (fastforce elim: sem.cases intro: JCFG_Straight_NoExc)
with ‹identifies n c› c c' have "JVM_CFG_Interpret.path prog n [?e1] (_ c',None _)"
by -(simp,
rule JVM_CFG_Interpret.path.Cons_path,
rule JVM_CFG_Interpret.path.empty_path,
auto simp: JVM_CFG_Interpret.valid_node_def, fastforce)
moreover from Store jvm_exec stk' loc' c c' s s' prog wt
‹length ST > 0 ∧ nat < length LT›
have "transfers (JVM_CFG_Interpret.kinds [?e1]) s = s'"
by (auto intro!: ext
simp: JVM_CFG_Interpret.kinds_def
nth_stkss (* nth_stks *) nth_locss (* nth_locs *) nth_Cons' nth_tl
not_less_eq_eq hd_stks)
moreover have "preds (JVM_CFG_Interpret.kinds [?e1]) s"
ultimately show ?thesis by fastforce
next
case (Push val)
with sem_step s s' c prog
have c': "c' = (C,M,pc+1)#cs"
by (auto elim!: sem.cases)
from sees_M Push have "Suc pc ∈ set (succs (is ! pc) (ST, LT) pc)"
by simp
with prog sem_step Push v_cs_succ
have v_edge:"valid_edge prog ((_ (C,M,pc)#cs,None _),
⇑(λs. exec_instr (instrs_of (P⇘wf⇙) C M ! pc) P s (length cs) (stkLength P C M pc) 0 0),
(_ (C,M,Suc pc)#cs,None _))"
(is "valid_edge prog ?e1")
by (fastforce elim: sem.cases intro: JCFG_Straight_NoExc)
with ‹identifies n c› c c' have "JVM_CFG_Interpret.path prog n [?e1] (_ c',None _)"
by -(simp,
rule JVM_CFG_Interpret.path.Cons_path,
rule JVM_CFG_Interpret.path.empty_path,
auto simp: JVM_CFG_Interpret.valid_node_def, fastforce)
moreover from Push jvm_exec stk' loc' c c' s s' prog wt
have "transfers (JVM_CFG_Interpret.kinds [?e1]) s = s'"
by (auto intro!: ext
simp: JVM_CFG_Interpret.kinds_def
nth_stkss (* nth_stks *) nth_locss (* nth_locs *) nth_Cons' nth_tl
not_less_eq_eq)
moreover have "preds (JVM_CFG_Interpret.kinds [?e1]) s"
ultimately show ?thesis by fastforce
next
case (New Cl)
show ?thesis
case None
with New sem_step s s' c prog prealloc
have c': "c' = find_handler_for P OutOfMemory c"
by (fastforce elim!: sem.cases
dest: find_handler_find_handler_forD)
with jvm_exec New None prealloc
have f2c_frs'_c': "framestack_to_callstack frs' = c'"
by (auto dest!: find_handler_find_handler_forD)
with New c' v_cs v_cs_f2c_frs'
have v_pred_edge:"valid_edge prog ((_ (C,M,pc)#cs,None _),
(_ (C,M,pc)#cs,⌊(c',True)⌋ _))"
(is "valid_edge prog ?e1")
apply auto
apply (rule JCFG_New_Exc_Pred, fastforce+)
apply (rule_tac x="(λ(h, stk, loc). new_Addr h = None)" in exI)
apply (rule JCFG_New_Exc_Pred, fastforce+)
apply (cases "find_handler_for P OutOfMemory cs")
apply (rule exI)
apply clarsimp
apply (rule JCFG_New_Exc_Exit, fastforce+)
apply clarsimp
apply (rule_tac x="λ(h, stk, loc).
(h, stk((length list, stkLength P a aa b - Suc 0) :=
loc)" in exI)
apply (rule JCFG_New_Exc_Update, fastforce+)
apply (rule JCFG_New_Exc_Pred, fastforce+)
apply (rule exI)
apply (rule JCFG_New_Exc_Pred, fastforce+)
apply (rule exI)
by (rule JCFG_New_Exc_Update, fastforce+)
show ?thesis
proof (cases c')
case Nil
with prog sem_step New c
have v_exec_edge:"valid_edge prog ((_ (C,M,pc)#cs,⌊([],True)⌋ _),
⇑id,
(_Exit_))"
(is "valid_edge prog ?e2")
by (fastforce elim: sem.cases intro: JCFG_New_Exc_Exit)
with v_pred_edge ‹identifies n c› c c' Nil
have "JVM_CFG_Interpret.path prog n [?e1,?e2] (_Exit_)"
by -(simp,
rule JVM_CFG_Interpret.path.Cons_path,
rule JVM_CFG_Interpret.path.Cons_path,
rule JVM_CFG_Interpret.path.empty_path,
auto simp: JVM_CFG_Interpret.valid_node_def, fastforce)
moreover from Nil None New sem_step c c' s s' prog
have "transfers (JVM_CFG_Interpret.kinds [?e1,?e2]) s = s'"
by (auto elim!: sem.cases simp: JVM_CFG_Interpret.kinds_def)
moreover from None s have "preds (JVM_CFG_Interpret.kinds [?e1,?e2]) s"
ultimately show ?thesis using Nil by fastforce
next
case (Cons a cs')
then obtain C' M' pc' where Cons: "c' = (C',M',pc')#cs'" by (cases a, fastforce)
from jvm_exec c s None New
have "update_loc loc frs' = loc"
by -(rule find_handler_loc_fun_eq' [of P _ h "(C,M,pc)#cs" stk loc], simp)
with loc' have "loc' = loc"
by simp
from c Cons s s' sem_step jvm_exec prog
have "(C',M',pc')#cs' = framestack_to_callstack frs'"
by (auto elim!: sem.cases)
moreover obtain stk'' loc'' frs'' where frs': "frs' = (stk'',loc'',C',M',pc')#frs''"
and cs': "cs' = framestack_to_callstack frs''" using calculation
by (cases frs', fastforce+)
ultimately
have "update_stk stk frs' =
stk((length cs',stkLength P C' M' pc' - Suc 0) := Addr (addr_of_sys_xcpt OutOfMemory))"
using c s c' None Cons prog New trg_state_correct wt jvm_exec prealloc stk'
by -(rule find_handler_stk_fun_eq' [of P _ h "(C,M,pc)#cs" _ loc h'],
auto dest!: list_all2_lengthD
simp: hd_stks split_beta framestack_to_callstack_def
correct_state_def)
with stk' have stk':
"stk' =
stk((length cs',stkLength P C' M' pc' - Suc 0) := Addr (addr_of_sys_xcpt OutOfMemory))"
by simp
from New Cons v_cs_f2c_frs' v_cs f2c_frs'_c'
have v_exec_edge:"valid_edge prog ((_ (C,M,pc)#cs,⌊(c',True)⌋ _),
⇑(λ(h,stk,loc).
(h,
stk((length cs',(stkLength P C' M' pc') - 1) :=
loc)
),
(_ c',None _))"
(is "valid_edge prog ?e2")
apply auto
apply (rule JCFG_New_Exc_Update)
apply fastforce
apply fastforce
using Cons c' apply simp
apply simp
using v_pred_edge c' Cons apply clarsimp
using v_pred_edge c' Cons apply clarsimp
done
with v_pred_edge ‹identifies n c› c c' Nil
have "JVM_CFG_Interpret.path prog n [?e1,?e2] (_ c',None _)"
by -(rule JVM_CFG_Interpret.path.Cons_path,
rule JVM_CFG_Interpret.path.Cons_path,
rule JVM_CFG_Interpret.path.empty_path,
auto simp: JVM_CFG_Interpret.valid_node_def, fastforce+)
moreover from New c c' s s' loc' stk' ‹loc' = loc› prog jvm_exec None
have "transfers (JVM_CFG_Interpret.kinds [?e1,?e2]) s = s'"
by (auto dest: find_handler_heap_eqD
simp: JVM_CFG_Interpret.kinds_def)
moreover from None s
have "preds (JVM_CFG_Interpret.kinds [?e1,?e2]) s"
ultimately show ?thesis by fastforce
qed
next
case (Some obj)
with New sem_step s s' c prog prealloc
have c': "c' = (C,M,Suc pc)#cs"
by (auto elim!: sem.cases)
with New jvm_exec Some
have f2c_frs'_c': "framestack_to_callstack frs' = c'"
by auto
with New c' v_cs v_cs_f2c_frs'
have v_pred_edge: "valid_edge prog ((_ (C,M,pc)#cs,None _),
(_ (C,M,pc)#cs,⌊(c',False)⌋ _))"
(is "valid_edge prog ?e1")
apply auto
apply (fastforce intro!: JCFG_New_Normal_Pred)
apply (rule exI)
apply (fastforce intro!: JCFG_New_Normal_Pred)
apply (rule exI)
by (fastforce intro!: JCFG_New_Normal_Update)
from New sees_M have "Suc pc ∈ set (succs (is ! pc) (ST, LT) pc)"
by simp
with prog New c' sem_step prog v_cs_succ
have v_exec_edge:"valid_edge prog ((_ (C,M,pc)#cs,⌊(c',False)⌋ _),
⇑(λs. exec_instr (instrs_of (P⇘wf⇙) C M ! pc) P s (length cs) (stkLength P C M pc) 0 0),
(_ (C,M,Suc pc)#cs,None _))"
(is "valid_edge prog ?e2")
by (auto elim!: sem.cases intro: JCFG_New_Normal_Update JCFG_New_Normal_Pred)
with v_pred_edge ‹identifies n c› c c'
have "JVM_CFG_Interpret.path prog n [?e1,?e2] (_ c',None _)"
by -(simp,
rule JVM_CFG_Interpret.path.Cons_path,
rule JVM_CFG_Interpret.path.Cons_path,
rule JVM_CFG_Interpret.path.empty_path,
auto simp: JVM_CFG_Interpret.valid_node_def, fastforce)
moreover from New jvm_exec loc' stk' c c' s s' prog Some
have "transfers (JVM_CFG_Interpret.kinds [?e1,?e2]) s = s'"
by (auto intro!: ext
simp: JVM_CFG_Interpret.kinds_def
nth_stkss (* nth_stks *) nth_locss (* nth_locs *) nth_Cons'
not_less_eq_eq hd_stks)
moreover from Some s
have "preds (JVM_CFG_Interpret.kinds [?e1,?e2]) s"
ultimately show ?thesis by fastforce
qed
next
case (Getfield Fd Cl)
with applicable sees_M
have "length ST > 0"
by clarsimp
then obtain ST1 STr where ST [simp]: "ST = ST1#STr" by (cases ST, fastforce+)
show ?thesis
proof (cases "stk(length cs, stkLength P C M pc - 1) = Null")
case True
with Getfield sem_step s s' c prog prealloc wt
have c': "c' = find_handler_for P NullPointer c"
by (cases "the (h (the_Addr Null))",
auto elim!: sem.cases
dest!: find_handler_find_handler_forD
simp: hd_stks)
with Getfield True jvm_exec prealloc
have "framestack_to_callstack frs' = c'"
by (auto simp: split_beta dest!: find_handler_find_handler_forD)
with Getfield prog c' v_cs v_cs_f2c_frs'
have v_pred_edge:"valid_edge prog ((_ (C,M,pc)#cs,None _),
(λ(h,stk,loc). stk(length cs, stkLength P C M pc - 1) = Null)⇩√,
(_ (C,M,pc)#cs,⌊(c',True)⌋ _))"
(is "valid_edge prog ?e1")
apply (auto simp del: find_handler_for.simps)
apply (fastforce intro!: JCFG_Getfield_Exc_Pred)
apply (fastforce intro!: JCFG_Getfield_Exc_Pred)
apply auto
apply (cases "find_handler_for P NullPointer cs")
apply (fastforce intro!: JCFG_Getfield_Exc_Exit)
apply (fastforce intro!: JCFG_Getfield_Exc_Update)
apply (fastforce intro!: JCFG_Getfield_Exc_Update)
done
show ?thesis
proof (cases c')
case Nil
with Getfield c prog c' v_pred_edge
have v_exec_edge:"valid_edge prog ((_ (C,M,pc)#cs,⌊([],True)⌋ _),
⇑id,
(_Exit_))"
(is "valid_edge prog ?e2")
by (fastforce intro: JCFG_Getfield_Exc_Exit)
with v_pred_edge ‹identifies n c› c c' Nil
have "JVM_CFG_Interpret.path prog n [?e1,?e2] (_Exit_)"
by -(simp,
rule JVM_CFG_Interpret.path.Cons_path,
rule JVM_CFG_Interpret.path.Cons_path,
rule JVM_CFG_Interpret.path.empty_path,
auto simp: JVM_CFG_Interpret.valid_node_def, fastforce)
moreover from Nil True Getfield sem_step c c' s s' prog wt ‹length ST > 0›
have "transfers</```