Up to index of Isabelle/HOL/Jinja/HRB-Slicing
theory SCDObservableheader {* \isaheader{Observable sets w.r.t.\ standard control dependence} *}
theory SCDObservable imports Observable HRBSlice begin
context SDG begin
lemma matched_bracket_assms_variant:
assumes "n⇣1 -p->⇘call⇙ n⇣2 ∨ n⇣1 -p:V'->⇘in⇙ n⇣2" and "matched n⇣2 ns' n⇣3"
and "n⇣3 -p->⇘ret⇙ n⇣4 ∨ n⇣3 -p:V->⇘out⇙ n⇣4"
and "call_of_return_node (parent_node n⇣4) (parent_node n⇣1)"
obtains a a' where "valid_edge a" and "a' ∈ get_return_edges a"
and "sourcenode a = parent_node n⇣1" and "targetnode a = parent_node n⇣2"
and "sourcenode a' = parent_node n⇣3" and "targetnode a' = parent_node n⇣4"
proof(atomize_elim)
from `n⇣1 -p->⇘call⇙ n⇣2 ∨ n⇣1 -p:V'->⇘in⇙ n⇣2` obtain a Q r fs where "valid_edge a"
and "kind a = Q:r\<hookrightarrow>⇘p⇙fs" and "parent_node n⇣1 = sourcenode a"
and "parent_node n⇣2 = targetnode a"
by(fastforce elim:SDG_edge.cases)
from `n⇣3 -p->⇘ret⇙ n⇣4 ∨ n⇣3 -p:V->⇘out⇙ n⇣4` obtain a' Q' f'
where "valid_edge a'" and "kind a' = Q'\<hookleftarrow>⇘p⇙f'"
and "parent_node n⇣3 = sourcenode a'" and "parent_node n⇣4 = targetnode a'"
by(fastforce elim:SDG_edge.cases)
from `valid_edge a'` `kind a' = Q'\<hookleftarrow>⇘p⇙f'`
obtain ax where "valid_edge ax" and "∃Q r fs. kind ax = Q:r\<hookrightarrow>⇘p⇙fs"
and "a' ∈ get_return_edges ax"
by -(drule return_needs_call,fastforce+)
from `valid_edge a` `valid_edge ax` `kind a = Q:r\<hookrightarrow>⇘p⇙fs` `∃Q r fs. kind ax = Q:r\<hookrightarrow>⇘p⇙fs`
have "targetnode a = targetnode ax" by(fastforce dest:same_proc_call_unique_target)
from `valid_edge a'` `a' ∈ get_return_edges ax` `valid_edge ax`
have "call_of_return_node (targetnode a') (sourcenode ax)"
by(fastforce simp:return_node_def call_of_return_node_def)
with `call_of_return_node (parent_node n⇣4) (parent_node n⇣1)`
`parent_node n⇣4 = targetnode a'`
have "sourcenode ax = parent_node n⇣1" by fastforce
with `valid_edge ax` `a' ∈ get_return_edges ax` `targetnode a = targetnode ax`
`parent_node n⇣2 = targetnode a` `parent_node n⇣3 = sourcenode a'`
`parent_node n⇣4 = targetnode a'`
show "∃a a'. valid_edge a ∧ a' ∈ get_return_edges a ∧
sourcenode a = parent_node n⇣1 ∧ targetnode a = parent_node n⇣2 ∧
sourcenode a' = parent_node n⇣3 ∧ targetnode a' = parent_node n⇣4"
by fastforce
qed
subsection {* Observable set of standard control dependence is at most a singleton *}
definition SDG_to_CFG_set :: "'node SDG_node set => 'node set" ("⌊_⌋⇘CFG⇙")
where "⌊S⌋⇘CFG⇙ ≡ {m. CFG_node m ∈ S}"
lemma [intro]:"∀n ∈ S. valid_SDG_node n ==> ∀n ∈ ⌊S⌋⇘CFG⇙. valid_node n"
by(fastforce simp:SDG_to_CFG_set_def)
lemma Exit_HRB_Slice:
assumes "n ∈ ⌊HRB_slice {CFG_node (_Exit_)}⌋⇘CFG⇙" shows "n = (_Exit_)"
proof -
from `n ∈ ⌊HRB_slice {CFG_node (_Exit_)}⌋⇘CFG⇙`
have "CFG_node n ∈ HRB_slice {CFG_node (_Exit_)}"
by(simp add:SDG_to_CFG_set_def)
thus ?thesis
proof(induct "CFG_node n" rule:HRB_slice_cases)
case (phase1 nx)
from `nx ∈ {CFG_node (_Exit_)}` have "nx = CFG_node (_Exit_)" by simp
with `CFG_node n ∈ sum_SDG_slice1 nx`
have "CFG_node n = CFG_node (_Exit_) ∨
(∃n Vopt popt b. sum_SDG_edge n Vopt popt b (CFG_node (_Exit_)))"
by(induct rule:sum_SDG_slice1.induct) auto
then show ?thesis by(fastforce dest:Exit_no_sum_SDG_edge_target)
next
case (phase2 nx n' n'' p)
from `nx ∈ {CFG_node (_Exit_)}` have "nx = CFG_node (_Exit_)" by simp
with `n' ∈ sum_SDG_slice1 nx`
have "n' = CFG_node (_Exit_) ∨
(∃n Vopt popt b. sum_SDG_edge n Vopt popt b (CFG_node (_Exit_)))"
by(induct rule:sum_SDG_slice1.induct) auto
hence "n' = CFG_node (_Exit_)" by(fastforce dest:Exit_no_sum_SDG_edge_target)
with `CFG_node n ∈ sum_SDG_slice2 n'`
have "CFG_node n = CFG_node (_Exit_) ∨
(∃n Vopt popt b. sum_SDG_edge n Vopt popt b (CFG_node (_Exit_)))"
by(induct rule:sum_SDG_slice2.induct) auto
then show ?thesis by(fastforce dest:Exit_no_sum_SDG_edge_target)
qed
qed
lemma Exit_in_obs_intra_slice_node:
assumes "(_Exit_) ∈ obs_intra n' ⌊HRB_slice S⌋⇘CFG⇙"
shows "CFG_node (_Exit_) ∈ S"
proof -
let ?S' = "⌊HRB_slice S⌋⇘CFG⇙"
from `(_Exit_) ∈ obs_intra n' ?S'` obtain as where "n' -as->⇣ι* (_Exit_)"
and "∀nx ∈ set(sourcenodes as). nx ∉ ?S'" and "(_Exit_) ∈ ?S'"
by(erule obs_intraE)
from `(_Exit_) ∈ ?S'`
have "CFG_node (_Exit_) ∈ HRB_slice S" by(simp add:SDG_to_CFG_set_def)
thus ?thesis
proof(induct "CFG_node (_Exit_)" rule:HRB_slice_cases)
case (phase1 nx)
thus ?case
by(induct "CFG_node (_Exit_)" rule:sum_SDG_slice1.induct,
auto dest:Exit_no_sum_SDG_edge_source)
next
case (phase2 nx n' n'' p)
from `CFG_node (_Exit_) ∈ sum_SDG_slice2 n'` `n' ∈ sum_SDG_slice1 nx` `nx ∈ S`
show ?case
apply(induct n≡"CFG_node (_Exit_)" rule:sum_SDG_slice2.induct)
apply(auto dest:Exit_no_sum_SDG_edge_source)
apply(induct n≡"CFG_node (_Exit_)" rule:sum_SDG_slice1.induct)
apply(auto dest:Exit_no_sum_SDG_edge_source)
done
qed
qed
lemma obs_intra_postdominate:
assumes "n ∈ obs_intra n' ⌊HRB_slice S⌋⇘CFG⇙" and "¬ method_exit n"
shows "n postdominates n'"
proof(rule ccontr)
assume "¬ n postdominates n'"
from `n ∈ obs_intra n' ⌊HRB_slice S⌋⇘CFG⇙` have "valid_node n"
by(fastforce dest:in_obs_intra_valid)
with `n ∈ obs_intra n' ⌊HRB_slice S⌋⇘CFG⇙` `¬ method_exit n` have "n postdominates n"
by(fastforce intro:postdominate_refl)
from `n ∈ obs_intra n' ⌊HRB_slice S⌋⇘CFG⇙` obtain as where "n' -as->⇣ι* n"
and all_notinS:"∀n' ∈ set(sourcenodes as). n' ∉ ⌊HRB_slice S⌋⇘CFG⇙"
and "n ∈ ⌊HRB_slice S⌋⇘CFG⇙" by(erule obs_intraE)
from `n postdominates n` `¬ n postdominates n'` `n' -as->⇣ι* n`
obtain as' a as'' where [simp]:"as = as'@a#as''"
and "valid_edge a" and "¬ n postdominates (sourcenode a)"
and "n postdominates (targetnode a)" and "intra_kind (kind a)"
by(fastforce elim!:postdominate_path_branch simp:intra_path_def)
from `n' -as->⇣ι* n` have "sourcenode a -a#as''->⇣ι* n"
by(fastforce elim:path_split intro:Cons_path simp:intra_path_def)
with `¬ n postdominates (sourcenode a)` `valid_edge a` `valid_node n`
obtain asx pex where "sourcenode a -asx->⇣ι* pex" and "method_exit pex"
and "n ∉ set(sourcenodes asx)" by(fastforce simp:postdominate_def)
have "asx ≠ []"
proof
assume "asx = []"
with `sourcenode a -asx->⇣ι* pex` have "sourcenode a = pex"
by(fastforce simp:intra_path_def)
from `method_exit pex` show False
proof(rule method_exit_cases)
assume "pex = (_Exit_)"
with `sourcenode a = pex` have "sourcenode a = (_Exit_)" by simp
with `valid_edge a` show False by(rule Exit_source)
next
fix a' Q f p
assume "pex = sourcenode a'" and "valid_edge a'" and "kind a' = Q\<hookleftarrow>⇘p⇙f"
from `valid_edge a'` `kind a' = Q\<hookleftarrow>⇘p⇙f` `valid_edge a` `intra_kind (kind a)`
`sourcenode a = pex` `pex = sourcenode a'`
show False by(fastforce dest:return_edges_only simp:intra_kind_def)
qed
qed
then obtain ax asx' where [simp]:"asx = ax#asx'" by(cases asx) auto
with `sourcenode a -asx->⇣ι* pex` have "sourcenode a -ax#asx'->* pex"
by(simp add:intra_path_def)
hence "valid_edge ax" and [simp]:"sourcenode a = sourcenode ax"
and "targetnode ax -asx'->* pex" by(auto elim:path_split_Cons)
with `sourcenode a -asx->⇣ι* pex` have "targetnode ax -asx'->⇣ι* pex"
by(simp add:intra_path_def)
with `valid_edge ax` `n ∉ set(sourcenodes asx)` `method_exit pex`
have "¬ n postdominates targetnode ax"
by(fastforce simp:postdominate_def sourcenodes_def)
from `n ∈ obs_intra n' ⌊HRB_slice S⌋⇘CFG⇙` all_notinS
have "n ∉ set (sourcenodes (a#as''))"
by(fastforce elim:obs_intra.cases simp:sourcenodes_def)
from `sourcenode a -asx->⇣ι* pex` have "intra_kind (kind ax)"
by(simp add:intra_path_def)
with `sourcenode a -a#as''->⇣ι* n` `n postdominates (targetnode a)`
`¬ n postdominates targetnode ax` `valid_edge ax`
`n ∉ set (sourcenodes (a#as''))` `intra_kind (kind a)`
have "(sourcenode a) controls n"
by(fastforce simp:control_dependence_def)
hence "CFG_node (sourcenode a) s-->⇘cd⇙ CFG_node n"
by(fastforce intro:sum_SDG_cdep_edge)
with `n ∈ obs_intra n' ⌊HRB_slice S⌋⇘CFG⇙` have "sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙"
by(auto elim!:obs_intraE combine_SDG_slices.cases
intro:combine_SDG_slices.intros sum_SDG_slice1.intros
sum_SDG_slice2.intros simp:HRB_slice_def SDG_to_CFG_set_def)
with all_notinS show False by(simp add:sourcenodes_def)
qed
lemma obs_intra_singleton_disj:
assumes "valid_node n"
shows "(∃m. obs_intra n ⌊HRB_slice S⌋⇘CFG⇙ = {m}) ∨
obs_intra n ⌊HRB_slice S⌋⇘CFG⇙ = {}"
proof(rule ccontr)
assume "¬ ((∃m. obs_intra n ⌊HRB_slice S⌋⇘CFG⇙ = {m}) ∨
obs_intra n ⌊HRB_slice S⌋⇘CFG⇙ = {})"
hence "∃nx nx'. nx ∈ obs_intra n ⌊HRB_slice S⌋⇘CFG⇙ ∧
nx' ∈ obs_intra n ⌊HRB_slice S⌋⇘CFG⇙ ∧ nx ≠ nx'" by auto
then obtain nx nx' where "nx ∈ obs_intra n ⌊HRB_slice S⌋⇘CFG⇙"
and "nx' ∈ obs_intra n ⌊HRB_slice S⌋⇘CFG⇙" and "nx ≠ nx'" by auto
from `nx ∈ obs_intra n ⌊HRB_slice S⌋⇘CFG⇙` obtain as where "n -as->⇣ι* nx"
and all:"∀n' ∈ set(sourcenodes as). n' ∉ ⌊HRB_slice S⌋⇘CFG⇙"
and "nx ∈ ⌊HRB_slice S⌋⇘CFG⇙"
by(erule obs_intraE)
from `n -as->⇣ι* nx` have "n -as->* nx" and "∀a ∈ set as. intra_kind (kind a)"
by(simp_all add:intra_path_def)
hence "valid_node nx" by(fastforce dest:path_valid_node)
with `nx ∈ ⌊HRB_slice S⌋⇘CFG⇙` have "obs_intra nx ⌊HRB_slice S⌋⇘CFG⇙ = {nx}"
by -(rule n_in_obs_intra)
with `n -as->* nx` `nx ∈ obs_intra n ⌊HRB_slice S⌋⇘CFG⇙`
`nx' ∈ obs_intra n ⌊HRB_slice S⌋⇘CFG⇙` `nx ≠ nx'` have "as ≠ []"
by(fastforce elim:path.cases simp:intra_path_def)
with `n -as->* nx` `nx ∈ obs_intra n ⌊HRB_slice S⌋⇘CFG⇙`
`nx' ∈ obs_intra n ⌊HRB_slice S⌋⇘CFG⇙` `nx ≠ nx'`
`obs_intra nx ⌊HRB_slice S⌋⇘CFG⇙ = {nx}` `∀a ∈ set as. intra_kind (kind a)` all
have "∃a as' as''. n -as'->⇣ι* sourcenode a ∧ targetnode a -as''->⇣ι* nx ∧
valid_edge a ∧ as = as'@a#as'' ∧ intra_kind (kind a) ∧
obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ = {nx} ∧
(¬ (∃m. obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {m} ∨
obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {}))"
proof(induct arbitrary:nx' rule:path.induct)
case (Cons_path n'' as n' a n)
note IH = `!!nx'. [|n' ∈ obs_intra n'' ⌊HRB_slice S⌋⇘CFG⇙;
nx' ∈ obs_intra n'' ⌊HRB_slice S⌋⇘CFG⇙; n' ≠ nx';
obs_intra n' ⌊HRB_slice S⌋⇘CFG⇙ = {n'};
∀a∈set as. intra_kind (kind a);
∀n'∈set (sourcenodes as). n' ∉ ⌊HRB_slice S⌋⇘CFG⇙; as ≠ []|]
==> ∃a as' as''. n'' -as'->⇣ι* sourcenode a ∧ targetnode a -as''->⇣ι* n' ∧
valid_edge a ∧ as = as'@a#as'' ∧ intra_kind (kind a) ∧
obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ = {n'} ∧
(¬ (∃m. obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {m} ∨
obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {}))`
note more_than_one = `n' ∈ obs_intra n ⌊HRB_slice S⌋⇘CFG⇙`
`nx' ∈ obs_intra n ⌊HRB_slice S⌋⇘CFG⇙` `n' ≠ nx'`
from `∀a∈set (a#as). intra_kind (kind a)`
have "∀a∈set as. intra_kind (kind a)" and "intra_kind (kind a)" by simp_all
from `∀n'∈set (sourcenodes (a#as)). n' ∉ ⌊HRB_slice S⌋⇘CFG⇙`
have all:"∀n'∈set (sourcenodes as). n' ∉ ⌊HRB_slice S⌋⇘CFG⇙"
by(simp add:sourcenodes_def)
show ?case
proof(cases "as = []")
case True
with `n'' -as->* n'` have [simp]:"n'' = n'" by(fastforce elim:path.cases)
from more_than_one `sourcenode a = n`
have "¬ (∃m. obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {m} ∨
obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {})"
by auto
with `targetnode a = n''` `obs_intra n' ⌊HRB_slice S⌋⇘CFG⇙ = {n'}`
`sourcenode a = n` True `valid_edge a` `intra_kind (kind a)`
show ?thesis
apply(rule_tac x="a" in exI)
apply(rule_tac x="[]" in exI)
apply(rule_tac x="[]" in exI)
by(auto intro:empty_path simp:intra_path_def)
next
case False
from `n'' -as->* n'` `∀a∈set (a # as). intra_kind (kind a)`
have "n'' -as->⇣ι* n'" by(simp add:intra_path_def)
with all
have subset:"obs_intra n' ⌊HRB_slice S⌋⇘CFG⇙ ⊆ obs_intra n'' ⌊HRB_slice S⌋⇘CFG⇙"
by -(rule path_obs_intra_subset)
thus ?thesis
proof(cases "obs_intra n' ⌊HRB_slice S⌋⇘CFG⇙ = obs_intra n'' ⌊HRB_slice S⌋⇘CFG⇙")
case True
with `n'' -as->⇣ι* n'` `valid_edge a` `sourcenode a = n` `targetnode a = n''`
`obs_intra n' ⌊HRB_slice S⌋⇘CFG⇙ = {n'}` `intra_kind (kind a)` more_than_one
show ?thesis
apply(rule_tac x="a" in exI)
apply(rule_tac x="[]" in exI)
apply(rule_tac x="as" in exI)
by(fastforce intro:empty_path simp:intra_path_def)
next
case False
with subset
have "obs_intra n' ⌊HRB_slice S⌋⇘CFG⇙ ⊂ obs_intra n'' ⌊HRB_slice S⌋⇘CFG⇙" by simp
with `obs_intra n' ⌊HRB_slice S⌋⇘CFG⇙ = {n'}`
obtain ni where "n' ∈ obs_intra n'' ⌊HRB_slice S⌋⇘CFG⇙"
and "ni ∈ obs_intra n'' ⌊HRB_slice S⌋⇘CFG⇙" and "n' ≠ ni" by auto
from IH[OF this `obs_intra n' ⌊HRB_slice S⌋⇘CFG⇙ = {n'}`
`∀a∈set as. intra_kind (kind a)` all `as ≠ []`] obtain a' as' as''
where "n'' -as'->⇣ι* sourcenode a'"
and hyps:"targetnode a' -as''->⇣ι* n'" "valid_edge a'" "as = as'@a'#as''"
"intra_kind (kind a')" "obs_intra (targetnode a') ⌊HRB_slice S⌋⇘CFG⇙ = {n'}"
"¬ (∃m. obs_intra (sourcenode a') ⌊HRB_slice S⌋⇘CFG⇙ = {m} ∨
obs_intra (sourcenode a') ⌊HRB_slice S⌋⇘CFG⇙ = {})"
by blast
from `n'' -as'->⇣ι* sourcenode a'` `valid_edge a` `sourcenode a = n`
`targetnode a = n''` `intra_kind (kind a)` `intra_kind (kind a')`
have "n -a#as'->⇣ι* sourcenode a'"
by(fastforce intro:path.Cons_path simp:intra_path_def)
with hyps show ?thesis
apply(rule_tac x="a'" in exI)
apply(rule_tac x="a#as'" in exI)
apply(rule_tac x="as''" in exI)
by fastforce
qed
qed
qed simp
then obtain a as' as'' where "valid_edge a" and "intra_kind (kind a)"
and "obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ = {nx}"
and more_than_one:"¬ (∃m. obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {m} ∨
obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {})"
by blast
have "sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙"
proof(rule ccontr)
assume "¬ sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙"
hence "sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙" by simp
with `valid_edge a`
have "obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {sourcenode a}"
by(fastforce intro!:n_in_obs_intra)
with more_than_one show False by simp
qed
with `valid_edge a` `intra_kind (kind a)`
have "obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ ⊆
obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙"
by(rule edge_obs_intra_subset)
with `obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ = {nx}`
have "nx ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙" by simp
with more_than_one obtain m
where "m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙" and "nx ≠ m" by auto
from `m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙` have "valid_node m"
by(fastforce dest:in_obs_intra_valid)
from `obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ = {nx}` have "valid_node nx"
by(fastforce dest:in_obs_intra_valid)
show False
proof(cases "m postdominates (sourcenode a)")
case True
with `nx ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙`
`m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙`
have "m postdominates nx"
by(fastforce intro:postdominate_inner_path_targetnode elim:obs_intraE)
with `nx ≠ m` have "¬ nx postdominates m" by(fastforce dest:postdominate_antisym)
with `valid_node nx` `valid_node m` obtain asx pex where "m -asx->⇣ι* pex"
and "method_exit pex" and "nx ∉ set(sourcenodes asx)"
by(fastforce simp:postdominate_def)
have "¬ nx postdominates (sourcenode a)"
proof
assume "nx postdominates sourcenode a"
from `nx ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙`
`m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙`
obtain asx' where "sourcenode a -asx'->⇣ι* m" and "nx ∉ set(sourcenodes asx')"
by(fastforce elim:obs_intraE)
with `m -asx->⇣ι* pex` have "sourcenode a -asx'@asx->⇣ι* pex"
by(fastforce intro:path_Append simp:intra_path_def)
with `nx ∉ set(sourcenodes asx)` `nx ∉ set(sourcenodes asx')`
`nx postdominates sourcenode a` `method_exit pex` show False
by(fastforce simp:sourcenodes_def postdominate_def)
qed
show False
proof(cases "method_exit nx")
case True
from `m postdominates nx` obtain xs where "nx -xs->⇣ι* m"
by -(erule postdominate_implies_inner_path)
with True have "nx = m"
by(fastforce dest!:method_exit_inner_path simp:intra_path_def)
with `nx ≠ m` show False by simp
next
case False
with `nx ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙`
have "nx postdominates sourcenode a" by(rule obs_intra_postdominate)
with `¬ nx postdominates (sourcenode a)` show False by simp
qed
next
case False
show False
proof(cases "method_exit m")
case True
from `m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙`
`nx ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙`
obtain xs where "sourcenode a -xs->⇣ι* m" and "nx ∉ set(sourcenodes xs)"
by(fastforce elim:obs_intraE)
obtain x' xs' where [simp]:"xs = x'#xs'"
proof(cases xs)
case Nil
with `sourcenode a -xs->⇣ι* m` have [simp]:"sourcenode a = m"
by(fastforce simp:intra_path_def)
with `m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙`
have "m ∈ ⌊HRB_slice S⌋⇘CFG⇙" by(fastforce elim:obs_intraE)
with `valid_node m` have "obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {m}"
by(rule n_in_obs_intra)
with `nx ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙` `nx ≠ m` have False
by fastforce
thus ?thesis by simp
qed blast
from `sourcenode a -xs->⇣ι* m` have "sourcenode a = sourcenode x'"
and "valid_edge x'" and "targetnode x' -xs'->⇣ι* m"
and "intra_kind (kind x')"
by(auto elim:path_split_Cons simp:intra_path_def)
from `targetnode x' -xs'->⇣ι* m` `nx ∉ set(sourcenodes xs)` `valid_edge x'`
`valid_node m` True
have "¬ nx postdominates (targetnode x')"
by(fastforce simp:postdominate_def sourcenodes_def)
show False
proof(cases "method_exit nx")
case True
from `m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙`
`nx ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙`
have "get_proc m = get_proc nx"
by(fastforce elim:obs_intraE dest:intra_path_get_procs)
with `method_exit m` `method_exit nx` have "m = nx"
by(rule method_exit_unique)
with `nx ≠ m` show False by simp
next
case False
with `obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ = {nx}`
have "nx postdominates (targetnode a)"
by(fastforce intro:obs_intra_postdominate)
from `obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ = {nx}`
obtain ys where "targetnode a -ys->⇣ι* nx"
and "∀nx' ∈ set(sourcenodes ys). nx' ∉ ⌊HRB_slice S⌋⇘CFG⇙"
and "nx ∈ ⌊HRB_slice S⌋⇘CFG⇙" by(fastforce elim:obs_intraE)
hence "nx ∉ set(sourcenodes ys)"by fastforce
have "sourcenode a ≠ nx"
proof
assume "sourcenode a = nx"
from `nx ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙`
have "nx ∈ ⌊HRB_slice S⌋⇘CFG⇙" by -(erule obs_intraE)
with `valid_node nx`
have "obs_intra nx ⌊HRB_slice S⌋⇘CFG⇙ = {nx}" by -(erule n_in_obs_intra)
with `sourcenode a = nx` `m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙`
`nx ≠ m` show False by fastforce
qed
with `nx ∉ set(sourcenodes ys)` have "nx ∉ set(sourcenodes (a#ys))"
by(fastforce simp:sourcenodes_def)
from `valid_edge a` `targetnode a -ys->⇣ι* nx` `intra_kind (kind a)`
have "sourcenode a -a#ys->⇣ι* nx"
by(fastforce intro:Cons_path simp:intra_path_def)
from `sourcenode a -a#ys->⇣ι* nx` `nx ∉ set(sourcenodes (a#ys))`
`intra_kind (kind a)` `nx postdominates (targetnode a)`
`valid_edge x'` `intra_kind (kind x')` `¬ nx postdominates (targetnode x')`
`sourcenode a = sourcenode x'`
have "(sourcenode a) controls nx"
by(fastforce simp:control_dependence_def)
hence "CFG_node (sourcenode a) -->⇘cd⇙ CFG_node nx"
by(fastforce intro:SDG_cdep_edge)
with `nx ∈ ⌊HRB_slice S⌋⇘CFG⇙` have "sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙"
by(fastforce elim!:combine_SDG_slices.cases
dest:SDG_edge_sum_SDG_edge cdep_slice1 cdep_slice2
intro:combine_SDG_slices.intros
simp:HRB_slice_def SDG_to_CFG_set_def)
with `valid_edge a`
have "obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {sourcenode a}"
by(fastforce intro!:n_in_obs_intra)
with `m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙`
`nx ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙` `nx ≠ m`
show False by simp
qed
next
case False
with `m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙`
have "m postdominates (sourcenode a)" by(rule obs_intra_postdominate)
with `¬ m postdominates (sourcenode a)` show False by simp
qed
qed
qed
lemma obs_intra_finite:"valid_node n ==> finite (obs_intra n ⌊HRB_slice S⌋⇘CFG⇙)"
by(fastforce dest:obs_intra_singleton_disj[of _ S])
lemma obs_intra_singleton:"valid_node n ==> card (obs_intra n ⌊HRB_slice S⌋⇘CFG⇙) ≤ 1"
by(fastforce dest:obs_intra_singleton_disj[of _ S])
lemma obs_intra_singleton_element:
"m ∈ obs_intra n ⌊HRB_slice S⌋⇘CFG⇙ ==> obs_intra n ⌊HRB_slice S⌋⇘CFG⇙ = {m}"
apply -
apply(frule in_obs_intra_valid)
apply(drule obs_intra_singleton_disj) apply auto
done
lemma obs_intra_the_element:
"m ∈ obs_intra n ⌊HRB_slice S⌋⇘CFG⇙ ==> (THE m. m ∈ obs_intra n ⌊HRB_slice S⌋⇘CFG⇙) = m"
by(fastforce dest:obs_intra_singleton_element)
lemma obs_singleton_element:
assumes "ms ∈ obs ns ⌊HRB_slice S⌋⇘CFG⇙" and "∀n ∈ set (tl ns). return_node n"
shows "obs ns ⌊HRB_slice S⌋⇘CFG⇙ = {ms}"
proof -
from `ms ∈ obs ns ⌊HRB_slice S⌋⇘CFG⇙` `∀n ∈ set (tl ns). return_node n`
obtain nsx n nsx' n' where "ns = nsx@n#nsx'" and "ms = n'#nsx'"
and split:"n' ∈ obs_intra n ⌊HRB_slice S⌋⇘CFG⇙"
"∀nx ∈ set nsx'. ∃nx'. call_of_return_node nx nx' ∧ nx' ∈ ⌊HRB_slice S⌋⇘CFG⇙"
"∀xs x xs'. nsx = xs@x#xs' ∧ obs_intra x ⌊HRB_slice S⌋⇘CFG⇙ ≠ {}
--> (∃x'' ∈ set (xs'@[n]). ∃nx. call_of_return_node x'' nx ∧
nx ∉ ⌊HRB_slice S⌋⇘CFG⇙)"
by(erule obsE)
from `n' ∈ obs_intra n ⌊HRB_slice S⌋⇘CFG⇙`
have "obs_intra n ⌊HRB_slice S⌋⇘CFG⇙ = {n'}"
by(fastforce intro!:obs_intra_singleton_element)
{ fix xs assume "xs ≠ ms" and "xs ∈ obs ns ⌊HRB_slice S⌋⇘CFG⇙"
from `xs ∈ obs ns ⌊HRB_slice S⌋⇘CFG⇙` `∀n ∈ set (tl ns). return_node n`
obtain zs z zs' z' where "ns = zs@z#zs'" and "xs = z'#zs'"
and "z' ∈ obs_intra z ⌊HRB_slice S⌋⇘CFG⇙"
and "∀z' ∈ set zs'. ∃nx'. call_of_return_node z' nx' ∧ nx' ∈ ⌊HRB_slice S⌋⇘CFG⇙"
and "∀xs x xs'. zs = xs@x#xs' ∧ obs_intra x ⌊HRB_slice S⌋⇘CFG⇙ ≠ {}
--> (∃x'' ∈ set (xs'@[z]). ∃nx. call_of_return_node x'' nx ∧
nx ∉ ⌊HRB_slice S⌋⇘CFG⇙)"
by(erule obsE)
with `ns = nsx@n#nsx'` split
have "nsx = zs ∧ n = z ∧ nsx' = zs'"
by -(rule obs_split_det[of _ _ _ _ _ _ "⌊HRB_slice S⌋⇘CFG⇙"],fastforce+)
with `obs_intra n ⌊HRB_slice S⌋⇘CFG⇙ = {n'}` `z' ∈ obs_intra z ⌊HRB_slice S⌋⇘CFG⇙`
have "z' = n'" by simp
with `xs ≠ ms` `ms = n'#nsx'` `xs = z'#zs'` `nsx = zs ∧ n = z ∧ nsx' = zs'`
have False by simp }
with `ms ∈ obs ns ⌊HRB_slice S⌋⇘CFG⇙` show ?thesis by fastforce
qed
lemma obs_finite:"∀n ∈ set (tl ns). return_node n
==> finite (obs ns ⌊HRB_slice S⌋⇘CFG⇙)"
by(cases "obs ns ⌊HRB_slice S⌋⇘CFG⇙ = {}",auto dest:obs_singleton_element[of _ _ S])
lemma obs_singleton:"∀n ∈ set (tl ns). return_node n
==> card (obs ns ⌊HRB_slice S⌋⇘CFG⇙) ≤ 1"
by(cases "obs ns ⌊HRB_slice S⌋⇘CFG⇙ = {}",auto dest:obs_singleton_element[of _ _ S])
lemma obs_the_element:
"[|ms ∈ obs ns ⌊HRB_slice S⌋⇘CFG⇙; ∀n ∈ set (tl ns). return_node n|]
==> (THE ms. ms ∈ obs ns ⌊HRB_slice S⌋⇘CFG⇙) = ms"
by(cases "obs ns ⌊HRB_slice S⌋⇘CFG⇙ = {}",auto dest:obs_singleton_element[of _ _ S])
end
end