Up to index of Isabelle/HOL/Jinja/HRB-Slicing
theory JVMInterpretationtheory JVMInterpretation imports JVMCFG "../StaticInter/CFGExit" begin
text {*
\isaheader{Instatiation of the @{text CFG} locale}
*}
abbreviation sourcenode :: "cfg_edge => cfg_node"
where "sourcenode e ≡ fst e"
abbreviation targetnode :: "cfg_edge => cfg_node"
where "targetnode e ≡ snd(snd e)"
abbreviation kind :: "cfg_edge => (var, val, cname × mname × pc, cname × mname) edge_kind"
where "kind e ≡ fst(snd e)"
definition valid_edge :: "jvm_method => cfg_edge => bool"
where "valid_edge P e ≡ P \<turnstile> (sourcenode e) -(kind e)-> (targetnode e)"
fun methods :: "cname => JVMInstructions.jvm_method mdecl list => ((cname × mname) × var list × var list) list"
where "methods C [] = []"
| "methods C ((M, Ts, T, mb) # ms)
= ((C, M), Heap # (map Local [0..<Suc (length Ts)]), [Heap, Stack 0, Exception]) # (methods C ms)"
fun procs :: "jvm_prog => ((cname × mname) × var list × var list) list"
where "procs [] = []"
|"procs ((C, D, fs, ms) # P) = (methods C ms) @ (procs P)"
lemma in_set_methodsI: "map_of ms M = ⌊(Ts, T, mxs, mxl⇣0, is, xt)⌋
==> ((C', M), Heap # map Local [0..<length Ts] @ [Local (length Ts)], [Heap, Stack 0, Exception])
∈ set (methods C' ms)"
by (induct rule: methods.induct) (auto split: split_if_asm)
lemma in_methods_in_msD: "((C, M), ins, outs) ∈ set (methods D ms)
==> M ∈ set (map fst ms) ∧ D = C"
by (induct ms) auto
lemma in_methods_in_msD': "((C, M), ins, outs) ∈ set (methods D ms)
==> ∃Ts T mb. (M, Ts, T, mb) ∈ set ms
∧ D = C
∧ ins = Heap # (map Local [0..<Suc (length Ts)])
∧ outs = [Heap, Stack 0, Exception]"
by (induct rule: methods.induct) fastforce+
lemma in_set_methodsE:
assumes "((C, M), ins, outs) ∈ set (methods D ms)"
obtains Ts T mb
where "(M, Ts, T, mb) ∈ set ms"
and "D = C"
and "ins = Heap # (map Local [0..<Suc (length Ts)])"
and "outs = [Heap, Stack 0, Exception]"
using assms
by (induct ms) fastforce+
lemma in_set_procsI:
assumes sees: "P \<turnstile> D sees M: Ts->T = mb in D"
and ins_def: "ins = Heap # map Local [0..<Suc (length Ts)]"
and outs_def: "outs = [Heap, Stack 0, Exception]"
shows "((D, M), ins, outs) ∈ set (procs P)"
proof -
from sees obtain D' fs ms where "map_of P D = ⌊(D', fs, ms)⌋" and "map_of ms M = ⌊(Ts, T, mb)⌋"
by (fastforce dest: visible_method_exists simp: class_def)
hence "(D, D', fs, ms) ∈ set P"
by -(drule map_of_SomeD)
thus ?thesis
proof (induct P)
case Nil thus ?case by simp
next
case (Cons Class P)
with ins_def outs_def `map_of ms M = ⌊(Ts, T, mb)⌋` show ?case
by (cases Class, cases mb) (auto intro: in_set_methodsI)
qed
qed
lemma distinct_methods: "distinct (map fst ms) ==> distinct (map fst (methods C ms))"
proof (induct ms)
case Nil thus ?case by simp
next
case (Cons M ms)
thus ?case
by (cases M) (auto dest: in_methods_in_msD)
qed
lemma in_set_procsD:
"((C, M), ins, out) ∈ set (procs P) ==> ∃D fs ms. (C, D, fs, ms) ∈ set P ∧ M ∈ set (map fst ms)"
proof (induct P)
case Nil thus ?case by simp
next
case (Cons Class P)
thus ?case
by (cases Class) (fastforce dest: in_methods_in_msD intro: rev_image_eqI)
qed
lemma in_set_procsE':
assumes "((C, M), ins, outs) ∈ set (procs P)"
obtains D fs ms Ts T mb
where "(C, D, fs, ms) ∈ set P"
and "(M, Ts, T, mb) ∈ set ms"
and "ins = Heap # (map (λn. Local n) [0..<Suc (length Ts)])"
and "outs = [Heap, Stack 0, Exception]"
using assms
by (induct P) (fastforce elim: in_set_methodsE)+
lemma distinct_Local_vars [simp]: "distinct (map Local [0..<n])"
by (induct n) auto
lemma distinct_Stack_vars [simp]: "distinct (map Stack [0..<n])"
by (induct n) auto
inductive_set get_return_edges :: "wf_jvmprog => cfg_edge => cfg_edge set"
for P :: "wf_jvmprog"
and a :: "cfg_edge"
where
"kind a = Q:(C, M, pc)\<hookrightarrow>⇘(D, M')⇙paramDefs
==> ((D, M', None, Return),
(λ(s, ret). ret = (C, M, pc))\<hookleftarrow>⇘(D, M')⇙(λs s'. s'(Heap := s Heap, Exception := s Exception,
Stack (stkLength (P, C, M) (Suc pc) - 1) := s (Stack 0))),
(C, M, ⌊pc⌋, Return)) ∈ (get_return_edges P a)"
lemma get_return_edgesE [elim!]:
assumes "a ∈ get_return_edges P a'"
obtains Q C M pc D M' paramDefs where
"kind a' = Q:(C, M, pc)\<hookrightarrow>⇘(D, M')⇙paramDefs"
and "a = ((D, M', None, Return),
(λ(s, ret). ret = (C, M, pc))\<hookleftarrow>⇘(D, M')⇙(λs s'. s'(Heap := s Heap, Exception := s Exception,
Stack (stkLength (P, C, M) (Suc pc) - 1) := s (Stack 0))),
(C, M, ⌊pc⌋, Return))"
using assms
by -(cases a, cases a', clarsimp, erule get_return_edges.cases, fastforce)
lemma distinct_class_names: "distinct_fst (PROG P)"
using wf_jvmprog_is_wf_typ [of P]
by (clarsimp simp: wf_jvm_prog_phi_def wf_prog_def)
lemma distinct_method_names:
"class (PROG P) C = ⌊(D, fs, ms)⌋ ==> distinct_fst ms"
using wf_jvmprog_is_wf_typ [of P]
unfolding wf_jvm_prog_phi_def
by (fastforce dest: class_wf simp: wf_cdecl_def)
lemma distinct_fst_is_distinct_fst: "distinct_fst = BasicDefs.distinct_fst"
by (simp add: distinct_fst_def BasicDefs.distinct_fst_def)
lemma ClassMain_not_in_set_PROG [dest!]: "(ClassMain P, D, fs, ms) ∈ set (PROG P) ==> False"
using distinct_class_names [of P] ClassMain_is_no_class [of P]
by (fastforce intro: map_of_SomeI simp: class_def)
lemma in_set_procsE:
assumes "((C, M), ins, outs) ∈ set (procs (PROG P))"
obtains D fs ms Ts T mb
where "class (PROG P) C = ⌊(D, fs, ms)⌋"
and "PROG P \<turnstile> C sees M:Ts->T = mb in C"
and "ins = Heap # (map (λn. Local n) [0..<Suc (length Ts)])"
and "outs = [Heap, Stack 0, Exception]"
proof -
from `((C, M), ins, outs) ∈ set (procs (PROG P))`
obtain D fs ms Ts T mxs mxl⇣0 "is" xt
where "(C, D, fs, ms) ∈ set (PROG P)"
and "(M, Ts, T, mxs, mxl⇣0, is, xt) ∈ set ms"
and "ins = Heap # (map (λn. Local n) [0..<Suc (length Ts)])"
and "outs = [Heap, Stack 0, Exception]"
by (fastforce elim: in_set_procsE')
moreover from `(C, D, fs, ms) ∈ set (PROG P)` distinct_class_names [of P]
have "class (PROG P) C = ⌊(D, fs, ms)⌋"
by (fastforce intro: map_of_SomeI simp: class_def)
moreover from wf_jvmprog_is_wf_typ [of P]
`(M, Ts, T, mxs, mxl⇣0, is, xt) ∈ set ms` `(C, D, fs, ms) ∈ set (PROG P)`
have "PROG P \<turnstile> C sees M:Ts->T = (mxs, mxl⇣0, is, xt) in C"
by (fastforce intro: mdecl_visible simp: wf_jvm_prog_phi_def)
ultimately show ?thesis using `(!!D fs ms Ts T mb.
[|class (PROG P) C = ⌊(D, fs, ms)⌋; PROG P \<turnstile> C sees M: Ts->T = mb in C;
ins = Heap # map Local [0..<Suc (length Ts)]; outs = [Heap, Stack 0, Exception]|]
==> thesis)`
by blast
qed
declare has_method_def [simp]
interpretation JVMCFG_Interpret:
CFG "sourcenode" "targetnode" "kind" "valid_edge (P, C0, Main)"
"(ClassMain P, MethodMain P, None, Enter)"
"(λ(C, M, pc, type). (C, M))" "get_return_edges P"
"((ClassMain P, MethodMain P),[],[]) # procs (PROG P)" "(ClassMain P, MethodMain P)"
for P C0 Main
proof (unfold_locales)
fix e
assume "valid_edge (P, C0, Main) e"
and "targetnode e = (ClassMain P, MethodMain P, None, Enter)"
thus False
by (auto simp: valid_edge_def)(erule JVMCFG.cases, auto)+
next
show "(λ(C, M, pc, type). (C, M)) (ClassMain P, MethodMain P, None, Enter) =
(ClassMain P, MethodMain P)"
by simp
next
fix a Q r p fs
assume "valid_edge (P, C0, Main) a"
and "kind a = Q:r\<hookrightarrow>⇘p⇙fs"
and "sourcenode a = (ClassMain P, MethodMain P, None, Enter)"
thus False
by (auto simp: valid_edge_def) (erule JVMCFG.cases, auto)
next
fix a a'
assume "valid_edge (P, C0, Main) a"
and "valid_edge (P, C0, Main) a'"
and "sourcenode a = sourcenode a'"
and "targetnode a = targetnode a'"
thus "a = a'"
by (cases a, cases a') (fastforce simp: valid_edge_def dest: JVMCFG_edge_det)
next
fix a Q r f
assume "valid_edge (P, C0, Main) a"
and "kind a = Q:r\<hookrightarrow>⇘(ClassMain P, MethodMain P)⇙f"
thus False
by (clarsimp simp: valid_edge_def) (erule JVMCFG.cases, auto)
next
fix a Q' f'
assume "valid_edge (P, C0, Main) a" and "kind a = Q'\<hookleftarrow>⇘(ClassMain P, MethodMain P)⇙f'"
thus False
by (clarsimp simp: valid_edge_def) (erule JVMCFG.cases, auto)+
next
fix a Q r p fs
assume "valid_edge (P, C0, Main) a"
and "kind a = Q:r\<hookrightarrow>⇘p⇙fs"
then obtain C M pc nt C' M' pc' nt'
where "(P, C0, Main) \<turnstile> (C, M, pc, nt) -Q:r\<hookrightarrow>⇘p⇙fs-> (C', M', pc', nt')"
by (cases a) (clarsimp simp: valid_edge_def)
thus "∃ins outs.
(p, ins, outs) ∈ set (((ClassMain P, MethodMain P), [], []) # procs (PROG P))"
proof cases
case (Main_Call T mxs mxl0 "is" xt initParams)
hence "((C', Main), [Heap, Local 0], [Heap, Stack 0, Exception]) ∈ set (procs (PROG P))"
and "p = (C', Main)"
by (auto intro: in_set_procsI dest: sees_method_idemp)
thus ?thesis by fastforce
next
case (CFG_Invoke_Call _ n _ _ _ Ts)
hence "((C', M'), Heap # map (λn. Local n) [0..<Suc (length Ts)],
[Heap, Stack 0, Exception]) ∈ set (procs (PROG P))"
and "p = (C',M')"
by (auto intro: in_set_procsI dest: sees_method_idemp)
thus ?thesis by fastforce
qed simp_all
next
fix a
assume "valid_edge (P, C0, Main) a" and "intra_kind (kind a)"
thus "(λ(C, M, pc, type). (C, M)) (sourcenode a) =
(λ(C, M, pc, type). (C, M)) (targetnode a)"
by (clarsimp simp: valid_edge_def) (erule JVMCFG.cases, auto simp: intra_kind_def)
next
fix a Q r p fs
assume "valid_edge (P, C0, Main) a" and "kind a = Q:r\<hookrightarrow>⇘p⇙fs"
thus "(λ(C, M, pc, type). (C, M)) (targetnode a) = p"
by (clarsimp simp: valid_edge_def) (erule JVMCFG.cases, auto)
next
fix a Q' p f'
assume "valid_edge (P, C0, Main) a" and "kind a = Q'\<hookleftarrow>⇘p⇙f'"
thus "(λ(C, M, pc, type). (C, M)) (sourcenode a) = p"
by (clarsimp simp: valid_edge_def) (erule JVMCFG.cases, auto)
next
fix a Q r p fs
assume "valid_edge (P, C0, Main) a" and "kind a = Q:r\<hookrightarrow>⇘p⇙fs"
thus "∀a'. valid_edge (P, C0, Main) a' ∧ targetnode a' = targetnode a
--> (∃Qx rx fsx. kind a' = Qx:rx\<hookrightarrow>⇘p⇙fsx)"
by (cases a, clarsimp simp: valid_edge_def) (erule JVMCFG.cases, auto)+
next
fix a Q' p f'
assume "valid_edge (P, C0, Main) a" and "kind a = Q'\<hookleftarrow>⇘p⇙f'"
thus "∀a'. valid_edge (P, C0, Main) a' ∧ sourcenode a' = sourcenode a
--> (∃Qx fx. kind a' = Qx\<hookleftarrow>⇘p⇙fx)"
by (cases a, clarsimp simp: valid_edge_def) (erule JVMCFG.cases, auto)+
next
fix a Q r p fs
assume "valid_edge (P, C0, Main) a" and "kind a = Q:r\<hookrightarrow>⇘p⇙fs"
then have "∃a'. a' ∈ get_return_edges P a"
by (cases p, cases r) (fastforce intro: get_return_edges.intros)
then show "get_return_edges P a ≠ {}"
by (simp only: ex_in_conv) simp
next
fix a a'
assume "valid_edge (P, C0, Main) a" "a' ∈ get_return_edges P a"
then obtain Q C M pc D M' paramDefs
where "(P, C0, Main) \<turnstile> sourcenode a -Q:(C, M, pc)\<hookrightarrow>⇘(D, M')⇙paramDefs-> targetnode a"
and "kind a = Q:(C, M, pc)\<hookrightarrow>⇘(D, M')⇙paramDefs"
and a'_def: "a' = ((D, M', None, nodeType.Return),
λ(s, ret).
ret = (C, M, pc)\<hookleftarrow>⇘(D, M')⇙λs s'. s'(Heap := s Heap, Exception := s Exception,
Stack (stkLength (P, C, M) (Suc pc) - 1) := s (Stack 0)),
C, M, ⌊pc⌋, nodeType.Return)"
by (fastforce simp: valid_edge_def)
thus "valid_edge (P, C0, Main) a'"
proof cases
case (Main_Call T mxs mxl0 "is" xt D')
hence "D = D'" and "M' = Main"
by simp_all
with `(P, C0, Main) \<turnstile> =>(ClassMain P, MethodMain P, ⌊0⌋, Normal)`
`PROG P \<turnstile> C0 sees Main: []->T = (mxs, mxl0, is, xt) in D'`
have "(P, C0, Main) \<turnstile> =>(D, M', None, Enter)"
by -(rule reachable_step, fastforce, fastforce intro: JVMCFG_reachable.Main_Call)
hence "(P, C0, Main) \<turnstile> =>(D, M', None, nodeType.Return)"
by -(rule reachable_step, fastforce, fastforce intro: JVMCFG_reachable.Method_LFalse)
with a'_def Main_Call show ?thesis
by (fastforce intro: CFG_Return_from_Method JVMCFG_reachable.Main_Call simp: valid_edge_def)
next
case (CFG_Invoke_Call _ _ _ M'' _ _ _ _ _ _ _ _ _ _ D')
hence "D = D'" and "M' = M''"
by simp_all
with CFG_Invoke_Call
have "(P, C0, Main) \<turnstile> =>(D, M', None, Enter)"
by -(rule reachable_step, fastforce, fastforce intro: JVMCFG_reachable.CFG_Invoke_Call)
hence "(P, C0, Main) \<turnstile> =>(D, M', None, nodeType.Return)"
by -(rule reachable_step, fastforce, fastforce intro: JVMCFG_reachable.Method_LFalse)
with a'_def CFG_Invoke_Call show ?thesis
by (fastforce intro: CFG_Return_from_Method JVMCFG_reachable.CFG_Invoke_Call
simp: valid_edge_def)
qed simp_all
next
fix a a'
assume "valid_edge (P, C0, Main) a" and "a' ∈ get_return_edges P a"
thus "∃Q r p fs. kind a = Q:r\<hookrightarrow>⇘p⇙fs"
by clarsimp
next
fix a Q r p fs a'
assume "valid_edge (P, C0, Main) a" and "kind a = Q:r\<hookrightarrow>⇘p⇙fs" and "a' ∈ get_return_edges P a"
thus "∃Q' f'. kind a' = Q'\<hookleftarrow>⇘p⇙f'"
by clarsimp
next
fix a Q' p f'
assume "valid_edge (P, C0, Main) a" and "kind a = Q'\<hookleftarrow>⇘p⇙f'"
show "∃!a'. valid_edge (P, C0, Main) a' ∧
(∃Q r fs. kind a' = Q:r\<hookrightarrow>⇘p⇙fs) ∧ a ∈ get_return_edges P a'"
proof (rule ex_ex1I)
from `valid_edge (P, C0, Main) a`
have "(P, C0, Main) \<turnstile> sourcenode a -kind a-> targetnode a"
by (clarsimp simp: valid_edge_def)
from this `kind a = Q'\<hookleftarrow>⇘p⇙f'`
show "∃a'. valid_edge (P, C0, Main) a' ∧ (∃Q r fs. kind a' = Q:r\<hookrightarrow>⇘p⇙fs)
∧ a ∈ get_return_edges P a'"
by cases (cases a, fastforce intro: get_return_edges.intros[simplified] simp: valid_edge_def)+
next
fix a' a''
assume "valid_edge (P, C0, Main) a'
∧ (∃Q r fs. kind a' = Q:r\<hookrightarrow>⇘p⇙fs) ∧ a ∈ get_return_edges P a'"
and "valid_edge (P, C0, Main) a''
∧ (∃Q r fs. kind a'' = Q:r\<hookrightarrow>⇘p⇙fs) ∧ a ∈ get_return_edges P a''"
thus "a' = a''"
by (cases a', cases a'', clarsimp simp: valid_edge_def)
(erule JVMCFG.cases, simp_all, clarsimp? )+
qed
next
fix a a'
assume "valid_edge (P, C0, Main) a" and "a' ∈ get_return_edges P a"
thus "∃a''. valid_edge (P, C0, Main) a'' ∧
sourcenode a'' = targetnode a ∧
targetnode a'' = sourcenode a' ∧ kind a'' = (λcf. False)⇣\<surd>"
by (clarsimp simp: valid_edge_def) (erule JVMCFG.cases, auto intro: JVMCFG_reachable.intros)
next
fix a a'
assume "valid_edge (P, C0, Main) a" and "a' ∈ get_return_edges P a"
thus "∃a''. valid_edge (P, C0, Main) a'' ∧
sourcenode a'' = sourcenode a ∧
targetnode a'' = targetnode a' ∧ kind a'' = (λcf. False)⇣\<surd>"
by (clarsimp simp: valid_edge_def) (erule JVMCFG.cases, auto intro: JVMCFG_reachable.intros)
next
fix a Q r p fs
assume "valid_edge (P, C0, Main) a" and "kind a = Q:r\<hookrightarrow>⇘p⇙fs"
hence call: "(P, C0, Main) \<turnstile> sourcenode a -Q:r\<hookrightarrow>⇘p⇙fs-> targetnode a"
by (clarsimp simp: valid_edge_def)
show "∃!a'. valid_edge (P, C0, Main) a' ∧
sourcenode a' = sourcenode a ∧ intra_kind (kind a')"
proof (rule ex_ex1I)
from call
show "∃a'. valid_edge (P, C0, Main) a' ∧ sourcenode a' = sourcenode a ∧ intra_kind (kind a')"
by cases (fastforce intro: JVMCFG_reachable.intros simp: intra_kind_def valid_edge_def)+
next
fix a' a''
assume "valid_edge (P, C0, Main) a' ∧ sourcenode a' = sourcenode a ∧ intra_kind (kind a')"
and "valid_edge (P, C0, Main) a'' ∧ sourcenode a'' = sourcenode a ∧ intra_kind (kind a'')"
with call show "a' = a''"
by (cases a, cases a', cases a'', clarsimp simp: valid_edge_def intra_kind_def)
(erule JVMCFG.cases, simp_all, clarsimp?)+
qed
next
fix a Q' p f'
assume "valid_edge (P, C0, Main) a" and "kind a = Q'\<hookleftarrow>⇘p⇙f'"
hence return: "(P, C0, Main) \<turnstile> sourcenode a -Q'\<hookleftarrow>⇘p⇙f'-> targetnode a"
by (clarsimp simp: valid_edge_def)
show "∃!a'. valid_edge (P, C0, Main) a' ∧
targetnode a' = targetnode a ∧ intra_kind (kind a')"
proof (rule ex_ex1I)
from return
show "∃a'. valid_edge (P, C0, Main) a' ∧ targetnode a' = targetnode a ∧ intra_kind (kind a')"
proof cases
case (CFG_Return_from_Method C M C' M' pc' Q'' ps Q stateUpdate)
hence [simp]: "Q = Q'" and [simp]: "p = (C, M)" and [simp]: "f' = stateUpdate"
by simp_all
from `(P, C0, Main) \<turnstile> (C', M', ⌊pc'⌋, Normal) -Q'':(C', M', pc')\<hookrightarrow>⇘(C, M)⇙ps-> (C, M, None, Enter)`
have invoke_reachable: "(P, C0, Main) \<turnstile> =>(C', M', ⌊pc'⌋, Normal)"
by -(drule sourcenode_reachable)
show ?thesis
proof (cases "C' = ClassMain P")
case True
with invoke_reachable CFG_Return_from_Method show ?thesis
by -(erule JVMCFG.cases, simp_all,
fastforce intro: Main_Call_LFalse simp: valid_edge_def intra_kind_def)
next
case False
with invoke_reachable CFG_Return_from_Method show ?thesis
by -(erule JVMCFG.cases, simp_all,
fastforce intro: CFG_Invoke_False simp: valid_edge_def intra_kind_def)
qed
qed simp_all
next
fix a' a''
assume "valid_edge (P, C0, Main) a' ∧ targetnode a' = targetnode a ∧ intra_kind (kind a')"
and "valid_edge (P, C0, Main) a'' ∧ targetnode a'' = targetnode a ∧ intra_kind (kind a'')"
with return show "a' = a''"
by (cases, auto, cases a, cases a', cases a'', clarsimp simp: valid_edge_def intra_kind_def)
(erule JVMCFG.cases, simp_all, clarsimp?)+
qed
next
fix a a' Q⇣1 r⇣1 p fs⇣1 Q⇣2 r⇣2 fs⇣2
assume "valid_edge (P, C0, Main) a" and "valid_edge (P, C0, Main) a'"
and "kind a = Q⇣1:r⇣1\<hookrightarrow>⇘p⇙fs⇣1" and "kind a' = Q⇣2:r⇣2\<hookrightarrow>⇘p⇙fs⇣2"
thus "targetnode a = targetnode a'"
by (cases a, cases a', clarsimp simp: valid_edge_def)
(erule JVMCFG.cases, simp_all, clarsimp?)+
next
from distinct_method_names [of P] distinct_class_names [of P]
have "!!C D fs ms. (C, D, fs, ms) ∈ set (PROG P) ==> distinct_fst ms"
by (fastforce intro: map_of_SomeI simp: class_def)
moreover {
fix P
assume "distinct_fst (P :: jvm_prog)"
and "!!C D fs ms. (C, D, fs, ms) ∈ set P ==> distinct_fst ms"
hence "distinct_fst (procs P)"
by (induct P, simp)
(fastforce intro: equals0I rev_image_eqI dest: in_methods_in_msD in_set_procsD
simp: distinct_methods distinct_fst_def)
}
ultimately have "distinct_fst (procs (PROG P))" using distinct_class_names [of P]
by blast
hence "BasicDefs.distinct_fst (procs (PROG P))"
by (simp add: distinct_fst_is_distinct_fst)
thus "BasicDefs.distinct_fst (((ClassMain P, MethodMain P), [], []) # procs (PROG P))"
by (fastforce elim: in_set_procsE)
next
fix C M P p ins outs
assume "(p, ins, outs) ∈ set (((C, M), [], []) # procs P)"
thus "distinct ins"
proof (induct P)
case Nil
thus ?case by simp
next
case (Cons Cl P)
then obtain C D fs ms where "Cl = (C, D, fs, ms)"
by (cases Cl) blast
with Cons show ?case
by auto (induct ms, auto)
qed
next
fix C M P p ins outs
assume "(p, ins, outs) ∈ set (((C, M), [], []) # procs P)"
thus "distinct outs"
proof (induct "P")
case Nil
thus ?case by simp
next
case (Cons Cl P)
then obtain C D fs ms where "Cl = (C, D, fs, ms)"
by (cases Cl) blast
with Cons show ?case
by auto (induct ms, auto)
qed
qed
interpretation JVMCFG_Exit_Interpret:
CFGExit "sourcenode" "targetnode" "kind" "valid_edge (P, C0, Main)"
"(ClassMain P, MethodMain P, None, Enter)"
"(λ(C, M, pc, type). (C, M))" "get_return_edges P"
"((ClassMain P, MethodMain P),[],[]) # procs (PROG P)"
"(ClassMain P, MethodMain P)" "(ClassMain P, MethodMain P, None, Return)"
for P C0 Main
proof (unfold_locales)
fix a
assume "valid_edge (P, C0, Main) a"
and "sourcenode a = (ClassMain P, MethodMain P, None, nodeType.Return)"
thus False
by (cases a, clarsimp simp: valid_edge_def) (erule JVMCFG.cases, simp_all, clarsimp)
next
show "(λ(C, M, pc, type). (C, M)) (ClassMain P, MethodMain P, None, nodeType.Return) =
(ClassMain P, MethodMain P)"
by simp
next
fix a Q p f
assume "valid_edge (P, C0, Main) a"
and "kind a = Q\<hookleftarrow>⇘p⇙f"
and "targetnode a = (ClassMain P, MethodMain P, None, nodeType.Return)"
thus False
by (cases a, clarsimp simp: valid_edge_def) (erule JVMCFG.cases, simp_all)
next
show "∃a. valid_edge (P, C0, Main) a ∧
sourcenode a = (ClassMain P, MethodMain P, None, Enter) ∧
targetnode a = (ClassMain P, MethodMain P, None, nodeType.Return) ∧
kind a = (λs. False)⇣\<surd>"
by (fastforce intro: JVMCFG_reachable.intros simp: valid_edge_def)
qed
end