Theory JVMCFG_wf

Up to index of Isabelle/HOL/Jinja/Slicing

theory JVMCFG_wf
imports JVMInterpretation CFGExit_wf
theory JVMCFG_wf imports JVMInterpretation "../Basic/CFGExit_wf" begin

text {*
\isaheader{Instantiation of the @{text "CFG_wf"} locale}
*}


subsection {* Variables and Values *}

datatype jinja_var = HeapVar "addr" | Stk "nat" "nat" | Loc "nat" "nat"
datatype jinja_val = Object "obj option" | Primitive "val"

fun state_val :: "state => jinja_var => jinja_val"
where
"state_val (h, stk, loc) (HeapVar a) = Object (h a)"
| "state_val (h, stk, loc) (Stk cd idx) = Primitive (stk (cd, idx))"
| "state_val (h, stk, loc) (Loc cd idx) = Primitive (loc (cd, idx))"


subsection {* The @{text Def} and @{text Use} sets *}

inductive_set Def :: "wf_jvmprog => j_node => jinja_var set"
for P :: "wf_jvmprog"
and n :: "j_node"
where
Def_Load:
"[| n = (_ (C, M, pc)#cs,None _);
instrs_of (Pwf) C M ! pc = Load idx;
cd = length cs;
i = stkLength P C M pc|]
==> Stk cd i ∈ Def P n"


| Def_Store:
"[| n = (_ (C, M, pc)#cs,None _);
instrs_of (Pwf) C M ! pc = Store idx;
cd = length cs |]
==> Loc cd idx ∈ Def P n"


| Def_Push:
"[| n = (_ (C, M, pc)#cs,None _);
instrs_of (Pwf) C M ! pc = Push v;
cd = length cs;
i = stkLength P C M pc |]
==> Stk cd i ∈ Def P n"


| Def_New_Normal_Stk:
"[| n = (_ (C, M, pc)#cs,⌊(cs',False)⌋ _);
instrs_of (Pwf) C M ! pc = New Cl;
cd = length cs;
i = stkLength P C M pc |]
==> Stk cd i ∈ Def P n"


| Def_New_Normal_Heap:
"[| n = (_ (C, M, pc)#cs,⌊(cs',False)⌋ _);
instrs_of (Pwf) C M ! pc = New Cl |]
==> HeapVar a ∈ Def P n"


| Def_Exc_Stk:
"[| n = (_ (C, M, pc)#cs,⌊(cs',True)⌋ _);
cs' ≠ [];
cd = length cs' - 1;
(C',M',pc') = hd cs';
i = stkLength P C' M' pc' - 1|]
==> Stk cd i ∈ Def P n"


| Def_Getfield_Stk:
"[| n = (_ (C, M, pc)#cs,⌊(cs',False)⌋ _);
instrs_of (Pwf) C M ! pc = Getfield Fd Cl;
cd = length cs;
i = stkLength P C M pc - 1 |]
==> Stk cd i ∈ Def P n"


| Def_Putfield_Heap:
"[| n = (_ (C, M, pc)#cs,⌊(cs',False)⌋ _);
instrs_of (Pwf) C M ! pc = Putfield Fd Cl |]
==> HeapVar a ∈ Def P n"


| Def_Invoke_Loc:
"[| n = (_ (C, M, pc)#cs,⌊(cs',False)⌋ _);
instrs_of (Pwf) C M ! pc = Invoke M' n';
cs' ≠ [];
hd cs' = (C',M',0);
i < locLength P C' M' 0;
cd = Suc (length cs) |]
==> Loc cd i ∈ Def P n"


| Def_Return_Stk:
"[| n = (_ (C, M, pc)#(D,M',pc')#cs,None _);
instrs_of (Pwf) C M ! pc = Return;
cd = length cs;
i = stkLength P D M' (Suc pc') - 1 |]
==> Stk cd i ∈ Def P n"


| Def_IAdd_Stk:
"[| n = (_ (C, M, pc)#cs,None _);
instrs_of (Pwf) C M ! pc = IAdd;
cd = length cs;
i = stkLength P C M pc - 2 |]
==> Stk cd i ∈ Def P n"


| Def_CmpEq_Stk:
"[| n = (_ (C, M, pc)#cs,None _);
instrs_of (Pwf) C M ! pc = CmpEq;
cd = length cs;
i = stkLength P C M pc - 2 |]
==> Stk cd i ∈ Def P n"


inductive_set Use :: "wf_jvmprog => j_node => jinja_var set"
for P :: "wf_jvmprog"
and n :: "j_node"
where
Use_Load:
"[| n = (_ (C, M, pc)#cs,None _);
instrs_of (Pwf) C M ! pc = Load idx;
cd = length cs |]
==> (Loc cd idx) ∈ Use P n"


| Use_Store:
"[| n = (_ (C, M, pc)#cs,None _);
instrs_of (Pwf) C M ! pc = Store idx;
cd = length cs;
Suc i = (stkLength P C M pc) |]
==> (Stk cd i) ∈ Use P n"


| Use_New:
"[| n = (_ (C, M, pc)#cs,x _);
x = None ∨ x = ⌊(cs',False)⌋;
instrs_of (Pwf) C M ! pc = New Cl |]
==> HeapVar a ∈ Use P n"


| Use_Getfield_Stk:
"[| n = (_ (C, M, pc)#cs,x _);
x = None ∨ x = ⌊(cs',False)⌋;
instrs_of (Pwf) C M ! pc = Getfield Fd Cl;
cd = length cs;
Suc i = stkLength P C M pc |]
==> Stk cd i ∈ Use P n"


| Use_Getfield_Heap:
"[| n = (_ (C, M, pc)#cs,⌊(cs',False)⌋ _);
instrs_of (Pwf) C M ! pc = Getfield Fd Cl |]
==> HeapVar a ∈ Use P n"


| Use_Putfield_Stk_Pred:
"[| n = (_ (C, M, pc)#cs,None _);
instrs_of (Pwf) C M ! pc = Putfield Fd Cl;
cd = length cs;
i = stkLength P C M pc - 2 |]
==> Stk cd i ∈ Use P n"


| Use_Putfield_Stk_Update:
"[| n = (_ (C, M, pc)#cs,⌊(cs',False)⌋ _);
instrs_of (Pwf) C M ! pc = Putfield Fd Cl;
cd = length cs;
i = stkLength P C M pc - 2 ∨ i = stkLength P C M pc - 1 |]
==> Stk cd i ∈ Use P n"


| Use_Putfield_Heap:
"[| n = (_ (C, M, pc)#cs,⌊(cs',False)⌋ _);
instrs_of (Pwf) C M ! pc = Putfield Fd Cl |]
==> HeapVar a ∈ Use P n"


| Use_Checkcast_Stk:
"[| n = (_ (C, M, pc)#cs,x _);
x = None ∨ x = ⌊(cs',False)⌋;
instrs_of (Pwf) C M ! pc = Checkcast Cl;
cd = length cs;
i = stkLength P C M pc - Suc 0 |]
==> Stk cd i ∈ Use P n"


| Use_Checkcast_Heap:
"[| n = (_ (C, M, pc)#cs,None _);
instrs_of (Pwf) C M ! pc = Checkcast Cl |]
==> HeapVar a ∈ Use P n"


| Use_Invoke_Stk_Pred:
"[| n = (_ (C, M, pc)#cs,None _);
instrs_of (Pwf) C M ! pc = Invoke M' n';
cd = length cs;
i = stkLength P C M pc - Suc n' |]
==> Stk cd i ∈ Use P n"


| Use_Invoke_Heap_Pred:
"[| n = (_ (C, M, pc)#cs,None _);
instrs_of (Pwf) C M ! pc = Invoke M' n' |]
==> HeapVar a ∈ Use P n"


| Use_Invoke_Stk_Update:
"[| n = (_ (C, M, pc)#cs,⌊(cs',False)⌋ _);
instrs_of (Pwf) C M ! pc = Invoke M' n';
cd = length cs;
i < stkLength P C M pc;
i ≥ stkLength P C M pc - Suc n' |]
==> Stk cd i ∈ Use P n"


| Use_Return_Stk:
"[| n = (_ (C, M, pc)#(D,M',pc')#cs,None _);
instrs_of (Pwf) C M ! pc = Return;
cd = Suc (length cs);
i = stkLength P C M pc - 1 |]
==> Stk cd i ∈ Use P n"


| Use_IAdd_Stk:
"[| n = (_ (C, M, pc)#cs,None _);
instrs_of (Pwf) C M ! pc = IAdd;
cd = length cs;
i = stkLength P C M pc - 1 ∨ i = stkLength P C M pc - 2 |]
==> Stk cd i ∈ Use P n"


| Use_IfFalse_Stk:
"[| n = (_ (C, M, pc)#cs,None _);
instrs_of (Pwf) C M ! pc = (IfFalse b);
cd = length cs;
i = stkLength P C M pc - 1 |]
==> Stk cd i ∈ Use P n"


| Use_CmpEq_Stk:
"[| n = (_ (C, M, pc)#cs,None _);
instrs_of (Pwf) C M ! pc = CmpEq;
cd = length cs;
i = stkLength P C M pc - 1 ∨ i = stkLength P C M pc - 2 |]
==> Stk cd i ∈ Use P n"


| Use_Throw_Stk:
"[| n = (_ (C, M, pc)#cs,x _);
x = None ∨ x = ⌊(cs',True)⌋;
instrs_of (Pwf) C M ! pc = Throw;
cd = length cs;
i = stkLength P C M pc - 1 |]
==> Stk cd i ∈ Use P n"


| Use_Throw_Heap:
"[| n = (_ (C, M, pc)#cs,x _);
x = None ∨ x = ⌊(cs',True)⌋;
instrs_of (Pwf) C M ! pc = Throw |]
==> HeapVar a ∈ Use P n"


declare correct_state_def [simp del]

lemma edge_transfer_uses_only_Use:
"[|valid_edge (P,C0,Main) a; ∀V ∈ Use P (sourcenode a). state_val s V = state_val s' V|]
==> ∀V ∈ Def P (sourcenode a). state_val (BasicDefs.transfer (kind a) s) V =
state_val (BasicDefs.transfer (kind a) s') V"

proof
fix V
assume ve: "valid_edge (P, C0, Main) a"
and use_eq: "∀V∈Use P (sourcenode a). state_val s V = state_val s' V"
and v_in_def: "V ∈ Def P (sourcenode a)"
obtain h stk loc where [simp]: "s = (h,stk,loc)" by (cases s, fastforce)
obtain h' stk' loc' where [simp]: "s' = (h',stk',loc')" by (cases s', fastforce)
note P_wf = wf_jvmprog_is_wf [of P]
from ve
have ex_edge: "(P,C0,Main) \<turnstile> (sourcenode a)-kind a->(targetnode a)"
and vn: "valid_node (P,C0,Main) (sourcenode a)"
by simp_all
show "state_val (transfer (kind a) s) V = state_val (transfer (kind a) s') V"
proof (cases "sourcenode a")
case (Node cs x) [simp]
from vn ex_edge have "cs ≠ []"
by (cases x, auto elim: JVM_CFG.cases)
then obtain C M pc cs' where [simp]: "cs = (C, M, pc)#cs'" by (cases cs, fastforce+)
with vn obtain ST LT where wt: "((PΦ) C M ! pc) = ⌊(ST,LT)⌋"
by (cases cs', (cases x, auto)+)
show ?thesis
proof (cases "instrs_of (Pwf) C M ! pc")
case (Load n) [simp]
from ex_edge have [simp]: "x = None"
by (auto elim!: JVM_CFG.cases)
hence "Loc (length cs') n ∈ Use P (sourcenode a)"
by (auto intro!: Use_Load)
with use_eq have "state_val s (Loc (length cs') n) = state_val s' (Loc (length cs') n)"
by (simp del: state_val.simps)
with v_in_def ex_edge show ?thesis
by (auto elim!: Def.cases
elim: JVM_CFG.cases
simp: split_beta)
next
case (Store n) [simp]
from ex_edge have [simp]:"x = None"
by (auto elim!: JVM_CFG.cases)
have "ST ≠ []"
proof -
from vn
obtain Ts T mxs mxl "is" xt
where C_sees_M: "Pwf \<turnstile> C sees M: Ts->T = (mxs, mxl, is, xt) in C"
by (cases cs', auto)
with vn
have "pc < length is"
by (cases cs', auto dest: sees_method_fun)
from P_wf C_sees_M
have "wt_method (Pwf) 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 Store C_sees_M wt `pc < length is`
show ?thesis
by (fastforce simp: wt_method_def)
qed
then obtain ST1 STr where [simp]: "ST = ST1#STr"
by (cases ST, fastforce+)
from wt
have "Stk (length cs') (length ST - 1) ∈ Use P (sourcenode a)"
(is "?stk_top ∈ ?Use_src")
by -(rule Use_Store, fastforce+)
with use_eq have "state_val s ?stk_top = state_val s' ?stk_top"
by (simp del: state_val.simps)
with v_in_def ex_edge wt show ?thesis
by (auto elim!: Def.cases
elim: JVM_CFG.cases
simp: split_beta)
next
case (Push val) [simp]
from ex_edge have "x = None"
by (auto elim!: JVM_CFG.cases)
with v_in_def ex_edge show ?thesis
by (auto elim!: Def.cases
elim: JVM_CFG.cases)
next
case (New Cl) [simp]
show ?thesis
proof (cases x)
case None
with v_in_def have False
by (auto elim: Def.cases)
thus ?thesis by simp
next
case (Some x')
then obtain cs'' xf where [simp]: "x = ⌊(cs'',xf)⌋"
by (cases x', fastforce)
have "¬ xf --> (∀addr. HeapVar addr ∈ Use P (sourcenode a))"
by (fastforce intro: Use_New)
with use_eq
have "¬ xf --> (∀addr. state_val s (HeapVar addr) = state_val s' (HeapVar addr))"
by (simp del: state_val.simps)
hence "¬ xf --> h = h'"
by (auto intro: ext)
with v_in_def ex_edge show ?thesis
by (auto elim!: Def.cases
elim: JVM_CFG.cases)
qed
next
case (Getfield Fd Cl) [simp]
show ?thesis
proof (cases x)
case None
with v_in_def have False
by (auto elim: Def.cases)
thus ?thesis by simp
next
case (Some x')
then obtain cs'' xf where [simp]: "x = ⌊(cs'',xf)⌋"
by (cases x', fastforce)
have "ST ≠ []"
proof -
from vn obtain T Ts mxs mxl "is" xt
where sees_M: "(Pwf) \<turnstile> C sees M:Ts->T = (mxs,mxl,is,xt) in C"
by (cases cs', auto)
with vn
have "pc < length is"
by (cases cs', auto dest: sees_method_fun)
from P_wf sees_M have "wt_method (Pwf) 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 Getfield sees_M wt `pc < length is` show ?thesis
by (fastforce simp: wt_method_def)
qed
then obtain ST1 STr where [simp]: "ST = ST1#STr" by (cases ST, fastforce)
from wt
have "¬ xf --> (Stk (length cs') (length ST - 1) ∈ Use P (sourcenode a))"
(is "?xf --> ?stk_top ∈ ?Use_src")
by (auto intro!: Use_Getfield_Stk)
with use_eq
have stk_top_eq: "¬ xf --> state_val s ?stk_top = state_val s' ?stk_top"
by (simp del: state_val.simps)
have "¬ xf --> (∀addr. HeapVar addr ∈ Use P (sourcenode a))"
by (auto intro!: Use_Getfield_Heap)
with use_eq
have "¬ xf --> (∀addr. state_val s (HeapVar addr) = state_val s' (HeapVar addr))"
by (simp del: state_val.simps)
hence "¬ xf --> h = h'"
by (auto intro: ext)
with ex_edge v_in_def stk_top_eq wt
show ?thesis
by (auto elim!: Def.cases
elim: JVM_CFG.cases
simp: split_beta)
qed
next
case (Putfield Fd Cl) [simp]
show ?thesis
proof (cases x)
case None
with v_in_def have False
by (auto elim: Def.cases)
thus ?thesis by simp
next
case (Some x')
then obtain cs'' xf where [simp]: "x = ⌊(cs'',xf)⌋"
by (cases x', fastforce)
have "length ST > 1"
proof -
from vn obtain T Ts mxs mxl "is" xt
where sees_M: "(Pwf) \<turnstile> C sees M:Ts->T = (mxs,mxl,is,xt) in C"
by (cases cs', auto)
with vn
have "pc < length is"
by (cases cs', auto dest: sees_method_fun)
from P_wf sees_M have "wt_method (Pwf) 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 Putfield sees_M `pc < length is` wt show ?thesis
by (fastforce simp: wt_method_def)
qed
then obtain ST1 STr' where "ST = ST1#STr' ∧ length STr' > 0"
by (cases ST, fastforce+)
then obtain ST2 STr where [simp]: "ST = ST1#ST2#STr"
by (cases STr', fastforce+)
from wt
have "¬ xf --> (Stk (length cs') (length ST - 1) ∈ Use P (sourcenode a))"
(is "?xf --> ?stk_top ∈ ?Use_src")
by (fastforce intro: Use_Putfield_Stk_Update)
with use_eq have stk_top:"(¬ xf) --> state_val s ?stk_top = state_val s' ?stk_top"
by (simp del: state_val.simps)
from wt
have "¬ xf --> (Stk (length cs') (length ST - 2) ∈ Use P (sourcenode a))"
(is "?xf --> ?stk_nxt ∈ ?Use_src")
by (fastforce intro: Use_Putfield_Stk_Update)
with use_eq
have stk_nxt:"(¬ xf) --> state_val s ?stk_nxt = state_val s' ?stk_nxt"
by (simp del: state_val.simps)
have "¬ xf --> (∀addr. HeapVar addr ∈ Use P (sourcenode a))"
by (fastforce intro: Use_Putfield_Heap)
with use_eq
have "¬ xf --> (∀addr. state_val s (HeapVar addr) = state_val s' (HeapVar addr))"
by (simp del: state_val.simps)
hence "¬ xf --> h = h'"
by (auto intro: ext)
with ex_edge v_in_def stk_top stk_nxt wt show ?thesis
by (auto elim!: Def.cases
elim: JVM_CFG.cases
simp: split_beta)
qed
next
case (Checkcast Cl) [simp]
show ?thesis
proof (cases x)
case None
with v_in_def have False
by (auto elim: Def.cases)
thus ?thesis by simp
next
case (Some x')
with ex_edge obtain cs''
where "x = ⌊(cs'',True)⌋"
by (auto elim!: JVM_CFG.cases)
with v_in_def ex_edge show ?thesis
by (auto elim!: Def.cases
elim: JVM_CFG.cases)
qed
next
case (Invoke M' n') [simp]
show ?thesis
proof (cases x)
case None
with v_in_def have False
by (auto elim: Def.cases)
thus ?thesis by simp
next
case (Some x')
then obtain cs'' xf where [simp]: "x = ⌊(cs'',xf)⌋"
by (cases x', fastforce)
show ?thesis
proof (cases xf)
case True
with v_in_def ex_edge show ?thesis
by (auto elim!: Def.cases
elim: JVM_CFG.cases)
next
case False [simp]
have "length ST > n'"
proof -
from vn obtain T Ts mxs mxl "is" xt
where sees_M: "(Pwf) \<turnstile> C sees M:Ts->T = (mxs,mxl,is,xt) in C"
by (cases cs', auto)
with vn
have "pc < length is"
by (cases cs', auto dest: sees_method_fun)
from P_wf sees_M have "wt_method (Pwf) 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 Invoke sees_M `pc < length is` wt show ?thesis
by (fastforce simp: wt_method_def)
qed
moreover obtain STn where "STn = take n' ST" by fastforce
moreover obtain STs where "STs = ST ! n'" by fastforce
moreover obtain STr where "STr = drop (Suc n') ST" by fastforce
ultimately have [simp]:" ST = STn@STs#STr ∧ length STn = n'"
by (auto simp: id_take_nth_drop)
from wt
have "∀i. i ≤ n' --> Stk (length cs') (length ST - Suc i) ∈ Use P (sourcenode a)"
by (fastforce intro: Use_Invoke_Stk_Update)
with use_eq
have
"∀i. i ≤ n' --> state_val s (Stk (length cs') (length ST - Suc i)) =
state_val s' (Stk (length cs') (length ST - Suc i))"

by (simp del: state_val.simps)
hence stk_eq:
"∀i. i ≤ n' --> state_val s (Stk (length cs') (i + length STr)) =
state_val s' (Stk (length cs') (i + length STr))"

by (clarsimp, erule_tac x="n' - i" in allE, auto simp: add_commute)
from ex_edge obtain C'
where trg: "targetnode a = (_ (C',M',0)#(C, M, pc)#cs',None _)"
by (fastforce elim: JVM_CFG.cases)
with ex_edge stk_eq v_in_def wt
show ?thesis
by (auto elim!: Def.cases) (erule JVM_CFG.cases, auto simp: split_beta add_commute)
qed
qed
next
case Return [simp]
show ?thesis
proof (cases x)
case None [simp]
show ?thesis
proof (cases cs')
case Nil
with v_in_def show ?thesis
by (auto elim!: Def.cases)
next
case (Cons aa list)
then obtain C' M' pc' cs'' where [simp]: "cs' = (C',M',pc')#cs''"
by (cases aa, fastforce)
from wt
have "Stk (length cs') (length ST - 1) ∈ Use P (sourcenode a)"
by (fastforce intro: Use_Return_Stk)
with use_eq
have "state_val s (Stk (length cs') (length ST - 1)) =
state_val s' (Stk (length cs') (length ST - 1))"

by (simp del: state_val.simps)
with v_in_def ex_edge wt show ?thesis
by (auto elim!: Def.cases
elim: JVM_CFG.cases
simp: split_beta)
qed
next
case (Some x')
with ex_edge show ?thesis
by (auto elim: JVM_CFG.cases)
qed
next
case Pop
with v_in_def ex_edge show ?thesis
by (auto elim!: Def.cases elim: JVM_CFG.cases)
next
case IAdd [simp]
show ?thesis
proof (cases x)
case None [simp]
from wt
have "Stk (length cs') (length ST - 1) ∈ Use P (sourcenode a)"
(is "?stk_top ∈ ?Use")
by (auto intro!: Use_IAdd_Stk)
with use_eq
have stk_top:"state_val s ?stk_top = state_val s' ?stk_top"
by (simp del: state_val.simps)
from wt
have "Stk (length cs') (length ST - 2) ∈ Use P (sourcenode a)"
(is "?stk_snd ∈ ?Use")
by (auto intro!: Use_IAdd_Stk)
with use_eq
have stk_snd:"state_val s ?stk_snd = state_val s' ?stk_snd"
by (simp del: state_val.simps)
with v_in_def ex_edge stk_top wt show ?thesis
by (auto elim!: Def.cases
elim: JVM_CFG.cases
simp: split_beta)
next
case (Some x')
with ex_edge show ?thesis
by (auto elim: JVM_CFG.cases)
qed
next
case (IfFalse b) [simp]
show ?thesis
proof (cases x)
case None [simp]
from wt
have "Stk (length cs') (length ST - 1) ∈ Use P (sourcenode a)"
(is "?stk_top ∈ ?Use")
by (auto intro!: Use_IfFalse_Stk)
with use_eq
have stk_top:"state_val s ?stk_top = state_val s' ?stk_top"
by (simp del: state_val.simps)
with v_in_def ex_edge wt show ?thesis
by (auto elim!: Def.cases)
next
case (Some x')
with ex_edge show ?thesis
by (auto elim: JVM_CFG.cases)
qed
next
case CmpEq [simp]
show ?thesis
proof (cases x)
case None [simp]
have "Stk (length cs') (stkLength P C M pc - 1) ∈ Use P (sourcenode a)"
(is "?stk_top ∈ ?Use")
by (auto intro!: Use_CmpEq_Stk)
with use_eq
have stk_top:"state_val s ?stk_top = state_val s' ?stk_top"
by (simp del: state_val.simps)
have "Stk (length cs') (stkLength P C M pc - 2) ∈ Use P (sourcenode a)"
(is "?stk_snd ∈ ?Use")
by (auto intro!: Use_CmpEq_Stk)
with use_eq
have stk_snd:"state_val s ?stk_snd = state_val s' ?stk_snd"
by (simp del: state_val.simps)
with v_in_def ex_edge stk_top wt show ?thesis
by (auto elim!: Def.cases
elim: JVM_CFG.cases)
next
case (Some x')
with ex_edge show ?thesis
by (auto elim: JVM_CFG.cases)
qed
next
case (Goto i)
with ex_edge v_in_def show ?thesis
by (auto elim!: Def.cases
elim: JVM_CFG.cases)
next
case Throw [simp]
show ?thesis
proof (cases x)
case None [simp]
have "Stk (length cs') (stkLength P C M pc - 1) ∈ Use P (sourcenode a)"
(is "?stk_top ∈ ?Use")
by (auto intro!: Use_Throw_Stk)
with use_eq
have stk_top:"state_val s ?stk_top = state_val s' ?stk_top"
by (simp del: state_val.simps)
with v_in_def show ?thesis
by (auto elim!: Def.cases)
next
case (Some x')
then obtain cs'' xf where [simp]: "x = ⌊(cs'',xf)⌋"
by (cases x', fastforce)
hence "xf --> Stk (length cs') (stkLength P C M pc - 1) ∈ Use P (sourcenode a)"
(is "xf --> ?stk_top ∈ ?Use")
by (fastforce intro: Use_Throw_Stk)
with use_eq
have stk_top:"xf --> state_val s ?stk_top = state_val s' ?stk_top"
by (simp del: state_val.simps)
with v_in_def ex_edge show ?thesis
by (auto elim!: Def.cases
elim: JVM_CFG.cases)
qed
qed
next
case Entry
with vn v_in_def show ?thesis
by -(erule Def.cases, auto)
qed
qed

lemma CFG_edge_Uses_pred_equal:
"[| valid_edge (P,C0,Main) a;
pred (kind a) s;
∀V ∈ Use P (sourcenode a). state_val s V = state_val s' V|]
==> pred (kind a) s'"

proof -
assume ve: "valid_edge (P,C0,Main) a"
and pred: "pred (kind a) s"
and use_eq: "∀V∈Use P (sourcenode a). state_val s V = state_val s' V"
obtain h stk loc where [simp]: "s = (h,stk,loc)" by (cases s, blast)
obtain h' stk' loc' where [simp]: "s' = (h',stk',loc')" by (cases s', blast)
from ve
have vn: "valid_node (P,C0,Main) (sourcenode a)"
and ex_edge: "(P,C0,Main) \<turnstile> (sourcenode a)-kind a->(targetnode a)"
by simp_all
note P_wf = wf_jvmprog_is_wf [of P]
show "pred (kind a) s'"
proof (cases "sourcenode a")
case (Node cs x) [simp]
from ve have "cs ≠ []"
by (cases x, auto elim: JVM_CFG.cases)
then obtain C M pc cs' where [simp]: "cs = (C, M, pc)#cs'" by (cases cs, fastforce+)
from vn obtain ST LT where wt: "((PΦ) C M ! pc) = ⌊(ST,LT)⌋"
by (cases cs', (cases x, auto)+)
show ?thesis
proof (cases "instrs_of (Pwf) C M ! pc")
case (Load nat)
with ex_edge show ?thesis
by (auto elim: JVM_CFG.cases)
next
case (Store nat)
with ex_edge show ?thesis
by (auto elim: JVM_CFG.cases)
next
case (Push val)
with ex_edge show ?thesis
by (auto elim: JVM_CFG.cases)
next
case (New Cl) [simp]
show ?thesis
proof (cases x)
case None
hence "∀addr. HeapVar addr ∈ Use P (sourcenode a)"
by (auto intro!: Use_New)
with use_eq have "∀addr. state_val s (HeapVar addr) = state_val s' (HeapVar addr)"
by (simp del: state_val.simps)
hence "h = h'"
by (auto intro: ext)
with ex_edge pred show ?thesis
by (auto elim!: JVM_CFG.cases)
next
case (Some x')
with ex_edge show ?thesis
by (auto elim: JVM_CFG.cases)
qed
next
case (Getfield Fd Cl) [simp]
have "ST ≠ []"
proof -
from vn obtain T Ts mxs mxl "is" xt
where sees_M: "(Pwf) \<turnstile> C sees M:Ts->T = (mxs,mxl,is,xt) in C"
by (cases cs', (cases x, auto)+)
with vn
have "pc < length is"
by (cases cs', (cases x, auto dest: sees_method_fun)+)
from P_wf sees_M have "wt_method (Pwf) 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 Getfield wt sees_M `pc < length is` show ?thesis
by (fastforce simp: wt_method_def)
qed
then obtain ST1 STr where [simp]: "ST = ST1#STr" by (cases ST, fastforce+)
show ?thesis
proof (cases x)
case None [simp]
from wt
have "Stk (length cs') (length ST - 1) ∈ Use P (sourcenode a)"
(is "?stk_top ∈ ?Use")
by (fastforce intro: Use_Getfield_Stk)
with use_eq have "state_val s ?stk_top = state_val s' ?stk_top"
by (simp del: state_val.simps)
with ex_edge pred wt show ?thesis
by (auto elim: JVM_CFG.cases)
next
case (Some x')
with ex_edge show ?thesis
by (auto elim: JVM_CFG.cases)
qed
next
case (Putfield Fd Cl) [simp]
have "length ST > 1"
proof -
from vn obtain T Ts mxs mxl "is" xt
where sees_M: "(Pwf) \<turnstile> C sees M:Ts->T = (mxs,mxl,is,xt) in C"
by (cases cs', (cases x, auto)+)
with vn
have "pc < length is"
by (cases cs', (cases x, auto dest: sees_method_fun)+)
from P_wf sees_M have "wt_method (Pwf) 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 Putfield wt sees_M `pc < length is` show ?thesis
by (fastforce simp: wt_method_def)
qed
then obtain ST1 STr' where "ST = ST1#STr' ∧ STr' ≠ []" by (cases ST, fastforce+)
then obtain ST2 STr where [simp]: "ST = ST1#ST2#STr" by (cases STr', fastforce+)
show ?thesis
proof (cases x)
case None [simp]
with wt
have "Stk (length cs') (length ST - 2) ∈ Use P (sourcenode a)"
(is "?stk_top ∈ ?Use")
by (fastforce intro: Use_Putfield_Stk_Pred)
with use_eq have "state_val s ?stk_top = state_val s' ?stk_top"
by (simp del: state_val.simps)
with ex_edge pred wt show ?thesis
by (auto elim: JVM_CFG.cases)
next
case (Some x')
with ex_edge show ?thesis
by (auto elim: JVM_CFG.cases)
qed
next
case (Checkcast Cl) [simp]
have "ST ≠ []"
proof -
from vn obtain T Ts mxs mxl "is" xt
where sees_M: "(Pwf) \<turnstile> C sees M:Ts->T = (mxs,mxl,is,xt) in C"
by (cases cs', (cases x, auto)+)
with vn
have "pc < length is"
by (cases cs', (cases x, auto dest: sees_method_fun)+)
from P_wf sees_M have "wt_method (Pwf) 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 Checkcast wt sees_M `pc < length is` show ?thesis
by (fastforce simp: wt_method_def)
qed
then obtain ST1 STr where [simp]: "ST = ST1#STr" by (cases ST, fastforce+)
show ?thesis
proof (cases x)
case None [simp]
from wt
have "Stk (length cs') (stkLength P C M pc - Suc 0) ∈ Use P (sourcenode a)"
(is "?stk_top ∈ ?Use")
by (fastforce intro: Use_Checkcast_Stk)
with use_eq
have stk_top: "state_val s ?stk_top = state_val s' ?stk_top"
by (simp del: state_val.simps)
have "∀addr. HeapVar addr ∈ Use P (sourcenode a)"
by (fastforce intro: Use_Checkcast_Heap)
with use_eq
have "∀addr. state_val s (HeapVar addr) = state_val s' (HeapVar addr)"
by (simp del: state_val.simps)
hence "h = h'"
by (auto intro: ext)
with ex_edge stk_top pred wt show ?thesis
by (auto elim: JVM_CFG.cases)
next
case (Some x')
with ex_edge show ?thesis
by (auto elim: JVM_CFG.cases)
qed
next
case (Invoke M' n') [simp]
have "length ST > n'"
proof -
from vn obtain T Ts mxs mxl "is" xt
where sees_M: "(Pwf) \<turnstile> C sees M:Ts->T = (mxs,mxl,is,xt) in C"
by (cases cs', (cases x, auto)+)
with vn
have "pc < length is"
by (cases cs', (cases x, auto dest: sees_method_fun)+)
from P_wf sees_M have "wt_method (Pwf) 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 Invoke wt sees_M `pc < length is` show ?thesis
by (fastforce simp: wt_method_def)
qed
moreover obtain STn where "STn = take n' ST" by fastforce
moreover obtain STs where "STs = ST ! n'" by fastforce
moreover obtain STr where "STr = drop (Suc n') ST" by fastforce
ultimately have [simp]:" ST = STn@STs#STr ∧ length STn = n'"
by (auto simp: id_take_nth_drop)
show ?thesis
proof (cases x)
case None [simp]
with wt
have "Stk (length cs') (stkLength P C M pc - Suc n') ∈ Use P (sourcenode a)"
(is "?stk_top ∈ ?Use")
by (fastforce intro: Use_Invoke_Stk_Pred)
with use_eq
have stk_top: "state_val s ?stk_top = state_val s' ?stk_top"
by (simp del: state_val.simps)
have "∀addr. HeapVar addr ∈ Use P (sourcenode a)"
by (fastforce intro: Use_Invoke_Heap_Pred)
with use_eq
have "∀addr. state_val s (HeapVar addr) = state_val s' (HeapVar addr)"
by (simp del: state_val.simps)
hence "h = h'"
by (auto intro: ext)
with ex_edge stk_top pred wt show ?thesis
by (auto elim: JVM_CFG.cases)
next
case (Some x')
with ex_edge show ?thesis
by (auto elim: JVM_CFG.cases)
qed
next
case Return
with ex_edge show ?thesis
by (auto elim: JVM_CFG.cases)
next
case Pop
with ex_edge show ?thesis
by (auto elim: JVM_CFG.cases)
next
case IAdd
with ex_edge show ?thesis
by (auto elim: JVM_CFG.cases)
next
case (IfFalse b) [simp]
show ?thesis
proof (cases x)
case None [simp]
have "Stk (length cs') (stkLength P C M pc - 1) ∈ Use P (sourcenode a)"
(is "?stk_top ∈ ?Use")
by (fastforce intro: Use_IfFalse_Stk)
with use_eq
have "state_val s ?stk_top = state_val s' ?stk_top"
by (simp del: state_val.simps)
with ex_edge pred wt show ?thesis
by (auto elim: JVM_CFG.cases)
next
case (Some x')
with ex_edge show ?thesis
by (auto elim: JVM_CFG.cases)
qed
next
case CmpEq
with ex_edge show ?thesis
by (auto elim: JVM_CFG.cases)
next
case (Goto i)
with ex_edge show ?thesis
by (auto elim: JVM_CFG.cases)
next
case Throw [simp]
have "ST ≠ []"
proof -
from vn obtain T Ts mxs mxl "is" xt
where sees_M: "(Pwf) \<turnstile> C sees M:Ts->T = (mxs,mxl,is,xt) in C"
by (cases cs', (cases x, auto)+)
with vn
have "pc < length is"
by (cases cs', (cases x, auto dest: sees_method_fun)+)
from P_wf sees_M have "wt_method (Pwf) 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 Throw wt sees_M `pc < length is` show ?thesis
by (fastforce simp: wt_method_def)
qed
then obtain ST1 STr where [simp]: "ST = ST1#STr" by (cases ST, fastforce+)
show ?thesis
proof (cases x)
case None [simp]
from wt
have "Stk (length cs') (stkLength P C M pc - 1) ∈ Use P (sourcenode a)"
(is "?stk_top ∈ ?Use")
by (fastforce intro: Use_Throw_Stk)
with use_eq
have stk_top: "state_val s ?stk_top = state_val s' ?stk_top"
by (simp del: state_val.simps)
have "∀addr. HeapVar addr ∈ Use P (sourcenode a)"
by (fastforce intro: Use_Throw_Heap)
with use_eq
have "∀addr. state_val s (HeapVar addr) = state_val s' (HeapVar addr)"
by (simp del: state_val.simps)
hence "h = h'"
by (auto intro: ext)
with ex_edge pred stk_top wt show ?thesis
by (auto elim!: JVM_CFG.cases)
next
case (Some x')
with ex_edge show ?thesis
by (auto elim: JVM_CFG.cases)
qed
qed
next
case Entry
with ex_edge pred show ?thesis
by (auto elim: JVM_CFG.cases)
qed
qed


lemma edge_no_Def_equal:
"[| valid_edge (P, C0, Main) a;
V ∉ Def P (sourcenode a) |]
==> state_val (transfer (kind a) s) V = state_val s V"

proof -
assume ve:"valid_edge (P, C0, Main) a"
and v_not_def: "V ∉ Def P (sourcenode a)"
obtain h stk loc where [simp]: "(s::state) = (h, stk, loc)" by (cases s, blast)
from ve have vn: "valid_node (P, C0, Main) (sourcenode a)"
and ex_edge: "(P, C0, Main) \<turnstile> (sourcenode a)-kind a->(targetnode a)"
by simp_all
show "state_val (transfer (kind a) s) V = state_val s V"
proof (cases "sourcenode a")
case (Node cs x) [simp]
with ve have "cs ≠ []"
by (cases x, auto elim: JVM_CFG.cases)
then obtain C M pc cs' where [simp]: "cs = (C, M, pc)#cs'" by (cases cs, fastforce+)
with vn obtain ST LT where wt: "((PΦ) C M ! pc) = ⌊(ST,LT)⌋"
by (cases cs', (cases x, auto)+)
show ?thesis
proof (cases "instrs_of (Pwf) C M ! pc")
case (Load nat) [simp]
from ex_edge have "x = None"
by (auto elim: JVM_CFG.cases)
with v_not_def have "V ≠ Stk (length cs') (stkLength P C M pc)"
by (auto intro!: Def_Load)
with ex_edge show ?thesis
by (auto elim!: JVM_CFG.cases, cases V, auto)
next
case (Store nat) [simp]
with ex_edge have "x = None"
by (auto elim: JVM_CFG.cases)
with v_not_def have "V ≠ Loc (length cs') nat"
by (auto intro!: Def_Store)
with ex_edge show ?thesis
by (auto elim!: JVM_CFG.cases, cases V, auto)
next
case (Push val) [simp]
with ex_edge have "x = None"
by (auto elim: JVM_CFG.cases)
with v_not_def have "V ≠ Stk (length cs') (stkLength P C M pc)"
by (auto intro!: Def_Push)
with ex_edge show ?thesis
by (auto elim!: JVM_CFG.cases, cases V, auto)
next
case (New Cl) [simp]
show ?thesis
proof (cases x)
case None
with ex_edge show ?thesis
by (auto elim: JVM_CFG.cases)
next
case (Some x')
then obtain cs'' xf where [simp]: "x = ⌊(cs'',xf)⌋"
by (cases x', fastforce)
with ex_edge v_not_def show ?thesis
apply (auto elim!: JVM_CFG.cases)
apply (cases V, auto intro!: Def_New_Normal_Stk Def_New_Normal_Heap)
by (cases V, auto intro!: Def_Exc_Stk)+
qed
next
case (Getfield F Cl) [simp]
show ?thesis
proof (cases x)
case None
with ex_edge show ?thesis
by (auto elim: JVM_CFG.cases)
next
case (Some x')
then obtain cs'' xf where [simp]: "x = ⌊(cs'',xf)⌋"
by (cases x', fastforce)
with ex_edge v_not_def show ?thesis
apply (auto elim!: JVM_CFG.cases simp: split_beta)
apply (cases V, auto intro!: Def_Getfield_Stk)
by (cases V, auto intro!: Def_Exc_Stk)+
qed
next
case (Putfield Fd Cl) [simp]
show ?thesis
proof (cases x)
case None
with ex_edge show ?thesis
by (auto elim: JVM_CFG.cases)
next
case (Some x')
then obtain cs'' xf where [simp]: "x = ⌊(cs'',xf)⌋"
by (cases x', fastforce)
with ex_edge v_not_def show ?thesis
apply (auto elim!: JVM_CFG.cases simp: split_beta)
apply (cases V, auto intro!: Def_Putfield_Heap)
by (cases V, auto intro!: Def_Exc_Stk)+
qed
next
case (Checkcast Cl) [simp]
show ?thesis
proof (cases x)
case None
with ex_edge show ?thesis
by (auto elim: JVM_CFG.cases)
next
case (Some x')
then obtain cs'' xf where [simp]: "x = ⌊(cs'',xf)⌋"
by (cases x', fastforce)
with ex_edge v_not_def show ?thesis
apply (auto elim!: JVM_CFG.cases)
by (cases V, auto intro!: Def_Exc_Stk)+
qed
next
case (Invoke M' n') [simp]
show ?thesis
proof (cases x)
case None
with ex_edge show ?thesis
by (auto elim: JVM_CFG.cases)
next
case (Some x')
then obtain cs'' xf where [simp]: "x = ⌊(cs'',xf)⌋"
by (cases x', fastforce)
from ex_edge v_not_def show ?thesis
apply (auto elim!: JVM_CFG.cases)
apply (cases V, auto intro!: Def_Invoke_Loc)
by (cases V, auto intro!: Def_Exc_Stk)+
qed
next
case Return
with ex_edge v_not_def show ?thesis
apply (auto elim!: JVM_CFG.cases)
by (cases V, auto intro!: Def_Return_Stk)
next
case Pop
with ex_edge show ?thesis
by (auto elim: JVM_CFG.cases)
next
case IAdd
with ex_edge v_not_def show ?thesis
apply (auto elim!: JVM_CFG.cases)
by (cases V, auto intro!: Def_IAdd_Stk)
next
case (IfFalse b)
with ex_edge show ?thesis
by (auto elim: JVM_CFG.cases)
next
case CmpEq
with ex_edge v_not_def show ?thesis
apply (auto elim!: JVM_CFG.cases)
by (cases V, auto intro!: Def_CmpEq_Stk)
next
case (Goto i)
with ex_edge show ?thesis
by (auto elim: JVM_CFG.cases)
next
case Throw [simp]
show ?thesis
proof (cases x)
case None
with ex_edge show ?thesis
by (auto elim: JVM_CFG.cases)
next
case (Some x')
then obtain cs'' xf where [simp]: "x = ⌊(cs'',xf)⌋"
by (cases x', fastforce)
from ex_edge v_not_def show ?thesis
apply (auto elim!: JVM_CFG.cases)
by (cases V, auto intro!: Def_Exc_Stk)+
qed
qed
next
case Entry
with ex_edge show ?thesis
by (auto elim: JVM_CFG.cases)
qed
qed

interpretation JVM_CFG_wf: CFG_wf
"sourcenode" "targetnode" "kind" "valid_edge prog" "(_Entry_)"
"Def (fst prog)" "Use (fst prog)" "state_val"
for prog
proof (unfold_locales)
show "Def (fst prog) (_Entry_) = {} ∧ Use (fst prog) (_Entry_) = {}"
by (auto elim: Def.cases Use.cases)
next
fix a V s
assume ve:"valid_edge prog a"
and v_not_def: "V ∉ Def (fst prog) (sourcenode a)"
thus "state_val (transfer (kind a) s) V = state_val s V"
by -(cases prog,
rule edge_no_Def_equal [of "fst prog" "fst (snd prog)" "snd (snd prog)"], auto)
next
fix a s s'
assume ve: "valid_edge prog a"
and use_eq: "∀V∈Use (fst prog) (sourcenode a). state_val s V = state_val s' V"
thus "∀V∈Def (fst prog) (sourcenode a).
state_val (transfer (kind a) s) V = state_val (transfer (kind a) s') V"

by -(cases prog,
rule edge_transfer_uses_only_Use [of "fst prog" "fst(snd prog)" "snd(snd prog)"], auto)
next
fix a s s'
assume ve: "valid_edge prog a"
and pred: "pred (kind a) s"
and use_eq: "∀V∈Use (fst prog) (sourcenode a). state_val s V = state_val s' V"
thus "pred (kind a) s'"
by -(cases prog,
rule CFG_edge_Uses_pred_equal [of "fst prog" "fst(snd prog)" "snd(snd prog)"], auto)
next
fix a a'
assume ve_a: "valid_edge prog a"
and ve_a': "valid_edge prog a'"
and src_eq: "sourcenode a = sourcenode a'"
and trg_neq: "targetnode a ≠ targetnode a'"
hence "prog \<turnstile> (sourcenode a)-kind a->(targetnode a)"
and "prog \<turnstile> (sourcenode a')-kind a'->(targetnode a')"
by simp_all
with src_eq trg_neq
show "∃Q Q'. kind a = (Q)\<surd> ∧ kind a' = (Q')\<surd> ∧ (∀s. (Q s --> ¬ Q' s) ∧ (Q' s --> ¬ Q s))"
apply (cases prog, auto)
apply (erule JVM_CFG.cases, erule_tac [!] JVM_CFG.cases)
(* This takes veeery long! *)
by simp_all
qed

interpretation JVM_CFGExit_wf: CFGExit_wf
"sourcenode" "targetnode" "kind" "valid_edge prog" "(_Entry_)"
"Def (fst prog)" "Use (fst prog)" "state_val" "(_Exit_)"
proof
show "Def (fst prog) (_Exit_) = {} ∧ Use (fst prog) (_Exit_) = {}"
by(fastforce elim:Def.cases Use.cases)
qed


end