Theory CDepInstantiations

```section ‹Instantiate framework with control dependences›

theory CDepInstantiations imports
Slice
PDG
WeakOrderDependence
begin

subsection‹Standard control dependence›

context StandardControlDependencePDG begin

lemma Exit_in_obs_slice_node:"(_Exit_) ∈ obs n' (PDG_BS S) ⟹ (_Exit_) ∈ S"
by(auto elim:obsE PDG_path_CFG_path simp:PDG_BS_def split:if_split_asm)

abbreviation PDG_path' :: "'node ⇒ 'node ⇒ bool" ("_ ⟶⇩d* _" [51,0] 80)
where "n ⟶⇩d* n' ≡ PDG.PDG_path sourcenode targetnode valid_edge Def Use
standard_control_dependence n n'"

lemma cd_closed:
"⟦n' ∈ PDG_BS S; n controls⇩s n'⟧ ⟹ n ∈ PDG_BS S"

lemma obs_postdominate:
assumes "n ∈ obs n' (PDG_BS S)" and "n ≠ (_Exit_)" shows "n postdominates n'"
proof(rule ccontr)
assume "¬ n postdominates n'"
from ‹n ∈ obs n' (PDG_BS S)› have "valid_node n" by(fastforce dest:in_obs_valid)
with ‹n ∈ obs n' (PDG_BS S)› ‹n ≠ (_Exit_)› have "n postdominates n"
by(fastforce intro:postdominate_refl)
from ‹n ∈ obs n' (PDG_BS S)› obtain as where "n' -as→* n"
and "∀n' ∈ set(sourcenodes as). n' ∉ (PDG_BS S)"
and "n ∈ (PDG_BS S)" by(erule obsE)
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)"
by -(erule postdominate_path_branch)
from ‹¬ n postdominates (sourcenode a)› ‹valid_edge a› ‹valid_node n›
obtain asx  where "sourcenode a -asx→* (_Exit_)"
and "n ∉ set(sourcenodes asx)" by(auto simp:postdominate_def)
from ‹sourcenode a -asx→* (_Exit_)› ‹valid_edge a›
obtain ax asx' where [simp]:"asx = ax#asx'"
apply - apply(erule path.cases)
apply(drule_tac s="(_Exit_)" in sym)
apply simp
apply(drule Exit_source)
by simp_all
with ‹sourcenode a -asx→* (_Exit_)› have "sourcenode a -[]@ax#asx'→* (_Exit_)"
by simp
hence "valid_edge ax" and [simp]:"sourcenode a = sourcenode ax"
and "targetnode ax -asx'→* (_Exit_)"
by(fastforce dest:path_split)+
with ‹n ∉ set(sourcenodes asx)› have "¬ n postdominates targetnode ax"
by(fastforce simp:postdominate_def sourcenodes_def)
from ‹n ∈ obs n' (PDG_BS S)› ‹∀n' ∈ set(sourcenodes as). n' ∉ (PDG_BS S)›
have "n ∉ set (sourcenodes (a#as''))"
by(fastforce elim:obs.cases simp:sourcenodes_def)
from ‹n' -as→* n› have "sourcenode a -a#as''→* n"
by(fastforce dest:path_split_second)
with ‹n postdominates (targetnode a)› ‹¬ n postdominates targetnode ax›
‹valid_edge ax› ‹n ∉ set (sourcenodes (a#as''))›
have "sourcenode a controls⇩s n" by(fastforce simp:standard_control_dependence_def)
with ‹n ∈ obs n' (PDG_BS S)› have "sourcenode a ∈ (PDG_BS S)"
by(fastforce intro:cd_closed PDG_cdep_edge elim:obs.cases)
with ‹∀n' ∈ set(sourcenodes as). n' ∉ (PDG_BS S)›
qed

lemma obs_singleton:"(∃m. obs n (PDG_BS S) = {m}) ∨ obs n (PDG_BS S) = {}"
proof(rule ccontr)
assume "¬ ((∃m. obs n (PDG_BS S) = {m}) ∨ obs n (PDG_BS S) = {})"
hence "∃nx nx'. nx ∈ obs n (PDG_BS S) ∧ nx' ∈ obs n (PDG_BS S) ∧
nx ≠ nx'" by auto
then obtain nx nx' where "nx ∈ obs n (PDG_BS S)" and "nx' ∈ obs n (PDG_BS S)"
and "nx ≠ nx'" by auto
from ‹nx ∈ obs n (PDG_BS S)› obtain as where "n -as→* nx"
and "∀n' ∈ set(sourcenodes as). n' ∉ (PDG_BS S)" and "nx ∈ (PDG_BS S)"
by(erule obsE)
from ‹n -as→* nx› have "valid_node nx" by(fastforce dest:path_valid_node)
with ‹nx ∈ (PDG_BS S)› have "obs nx (PDG_BS S) = {nx}" by -(rule n_in_obs)
with ‹n -as→* nx› ‹nx ∈ obs n (PDG_BS S)› ‹nx' ∈ obs n (PDG_BS S)› ‹nx ≠ nx'›
have "as ≠ []" by(fastforce elim:path.cases)
with ‹n -as→* nx› ‹nx ∈ obs n (PDG_BS S)› ‹nx' ∈ obs n (PDG_BS S)›
‹nx ≠ nx'› ‹obs nx (PDG_BS S) = {nx}› ‹∀n' ∈ set(sourcenodes as). n' ∉ (PDG_BS S)›
have "∃a as' as''. n -as'→* sourcenode a ∧ targetnode a -as''→* nx ∧
valid_edge a ∧ as = as'@a#as'' ∧
obs (targetnode a) (PDG_BS S) = {nx} ∧
(¬ (∃m. obs (sourcenode a) (PDG_BS S) = {m} ∨
obs (sourcenode a) (PDG_BS S) = {}))"
proof(induct arbitrary:nx' rule:path.induct)
case (Cons_path n'' as n' a n)
note [simp] = ‹sourcenode a = n›[THEN sym] ‹targetnode a = n''›[THEN sym]
note more_than_one = ‹n' ∈ obs n (PDG_BS S)› ‹nx' ∈ obs n (PDG_BS S)› ‹n' ≠ nx'›
note IH = ‹⋀nx'. ⟦n' ∈ obs n'' (PDG_BS S); nx' ∈ obs n'' (PDG_BS S); n' ≠ nx';
obs n' (PDG_BS S) = {n'}; ∀n'∈set (sourcenodes as). n' ∉ (PDG_BS S); as ≠ []⟧
⟹ ∃a as' as''. n'' -as'→* sourcenode a ∧ targetnode a -as''→* n' ∧
valid_edge a ∧ as = as'@a#as'' ∧ obs (targetnode a) (PDG_BS S) = {n'} ∧
(¬ (∃m. obs (sourcenode a) (PDG_BS S) = {m} ∨
obs (sourcenode a) (PDG_BS S) = {}))›
from ‹∀n'∈set (sourcenodes (a#as)). n' ∉ (PDG_BS S)›
have "∀n'∈set (sourcenodes as). n' ∉ (PDG_BS S)" and "sourcenode a ∉ (PDG_BS S)"
show ?case
proof(cases "as = []")
case True
with ‹n'' -as→* n'› have [simp]:"n' = n''" by(fastforce elim:path.cases)
from more_than_one
have "¬ (∃m. obs (sourcenode a) (PDG_BS S) = {m} ∨
obs (sourcenode a) (PDG_BS S) = {})"
by auto
with ‹obs n' (PDG_BS S) = {n'}› True ‹valid_edge 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)
next
case False
hence "as ≠ []" .
from ‹n'' -as→* n'› ‹∀n'∈set (sourcenodes as). n' ∉ (PDG_BS S)›
have "obs n' (PDG_BS S) ⊆ obs n'' (PDG_BS S)" by(rule path_obs_subset)
show ?thesis
proof(cases "obs n' (PDG_BS S) = obs n'' (PDG_BS S)")
case True
with ‹n'' -as→* n'› ‹valid_edge a› ‹obs n' (PDG_BS S) = {n'}› 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)
next
case False
with ‹obs n' (PDG_BS S) ⊆ obs n'' (PDG_BS S)›
have "obs n' (PDG_BS S) ⊂ obs n'' (PDG_BS S)" by simp
with ‹obs n' (PDG_BS S) = {n'}› obtain ni where "n' ∈ obs n'' (PDG_BS S)"
and "ni ∈ obs n'' (PDG_BS S)" and "n' ≠ ni" by auto
from IH[OF this ‹obs n' (PDG_BS S) = {n'}›
‹∀n'∈set (sourcenodes as). n' ∉ (PDG_BS S)› ‹as ≠ []›] obtain a' as' as''
where "n'' -as'→* sourcenode a'" and "targetnode a' -as''→* n'"
and "valid_edge a'" and [simp]:"as = as'@a'#as''"
and "obs (targetnode a') (PDG_BS S) = {n'}"
and more_than_one':"¬ (∃m. obs (sourcenode a') (PDG_BS S) = {m} ∨
obs (sourcenode a') (PDG_BS S) = {})"
by blast
from ‹n'' -as'→* sourcenode a'› ‹valid_edge a›
have "n -a#as'→* sourcenode a'" by(fastforce intro:path.Cons_path)
with ‹targetnode a' -as''→* n'› ‹obs (targetnode a') (PDG_BS S) = {n'}›
more_than_one' ‹valid_edge a'› 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 "obs (targetnode a) (PDG_BS S) = {nx}"
and more_than_one:"¬ (∃m. obs (sourcenode a) (PDG_BS S) = {m} ∨
obs (sourcenode a) (PDG_BS S) = {})"
by blast
have "sourcenode a ∉ (PDG_BS S)"
proof(rule ccontr)
assume "¬ sourcenode a ∉ PDG_BS S"
hence "sourcenode a ∈ PDG_BS S" by simp
with ‹valid_edge a› have "obs (sourcenode a) (PDG_BS S) = {sourcenode a}"
by(fastforce intro!:n_in_obs)
with more_than_one show False by simp
qed
with ‹valid_edge a›
have "obs (targetnode a) (PDG_BS S) ⊆ obs (sourcenode a) (PDG_BS S)"
by(rule edge_obs_subset)
with ‹obs (targetnode a) (PDG_BS S) = {nx}›
have "nx ∈ obs (sourcenode a) (PDG_BS S)" by simp
with more_than_one obtain m  where "m ∈ obs (sourcenode a) (PDG_BS S)"
and "nx ≠ m" by auto
from ‹m ∈ obs (sourcenode a) (PDG_BS S)›
have "valid_node m" by(fastforce dest:in_obs_valid)
from ‹obs (targetnode a) (PDG_BS S) = {nx}› have "valid_node nx"
by(fastforce dest:in_obs_valid)
show False
proof(cases "m postdominates (sourcenode a)")
case True
with ‹nx ∈ obs (sourcenode a) (PDG_BS S)› ‹m ∈ obs (sourcenode a) (PDG_BS S)›
have "m postdominates nx"
by(fastforce intro:postdominate_path_targetnode elim:obs.cases)
with ‹nx ≠ m› have "¬ nx postdominates m" by(fastforce dest:postdominate_antisym)
have "(_Exit_) -[]→* (_Exit_)" by(fastforce intro:empty_path)
with ‹m postdominates nx› have "nx ≠ (_Exit_)"
by(fastforce simp:postdominate_def sourcenodes_def)
have "¬ nx postdominates (sourcenode a)"
proof(rule ccontr)
assume "¬ ¬ nx postdominates sourcenode a"
hence "nx postdominates sourcenode a" by simp
from ‹m ∈ obs (sourcenode a) (PDG_BS S)› ‹nx ∈ obs (sourcenode a) (PDG_BS S)›
obtain asx' where "sourcenode a -asx'→* m" and "nx ∉ set(sourcenodes asx')"
by(fastforce elim:obs.cases)
with ‹nx postdominates sourcenode a› have "nx postdominates m"
by(rule postdominate_path_targetnode)
with ‹¬ nx postdominates m› show False by simp
qed
with ‹nx ∈ obs (sourcenode a) (PDG_BS S)› ‹valid_node nx› ‹nx ≠ (_Exit_)›
show False by(fastforce dest:obs_postdominate)
next
case False
show False
proof(cases "m = Exit")
case True
from ‹m ∈ obs (sourcenode a) (PDG_BS S)› ‹nx ∈ obs (sourcenode a) (PDG_BS S)›
obtain xs where "sourcenode a -xs→* m" and "nx ∉ set(sourcenodes xs)"
by(fastforce elim:obsE)
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
with ‹m ∈ obs (sourcenode a) (PDG_BS S)›
have "m ∈ (PDG_BS S)" by(metis obsE)
with ‹valid_node m› have "obs m (PDG_BS S) = {m}"
by(rule n_in_obs)
with ‹nx ∈ obs (sourcenode a) (PDG_BS S)› ‹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"
by(auto elim:path_split_Cons)
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)
from ‹nx ≠ m› True have "nx ≠ (_Exit_)" by simp
with ‹obs (targetnode a) (PDG_BS S) = {nx}›
have "nx postdominates (targetnode a)"
by(fastforce intro:obs_postdominate)
from ‹obs (targetnode a) (PDG_BS S) = {nx}›
obtain ys where "targetnode a -ys→* nx"
and "∀nx' ∈ set(sourcenodes ys). nx' ∉ (PDG_BS S)"
and "nx ∈ (PDG_BS S)" by(fastforce elim:obsE)
hence "nx ∉ set(sourcenodes ys)"by fastforce
have "sourcenode a ≠ nx"
proof
assume "sourcenode a = nx"
from ‹nx ∈ obs (sourcenode a) (PDG_BS S)›
have "nx ∈ (PDG_BS S)" by -(erule obsE)
with ‹valid_node nx› have "obs nx (PDG_BS S) = {nx}" by -(erule n_in_obs)
with ‹sourcenode a = nx› ‹m ∈ obs (sourcenode a) (PDG_BS S)›
‹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›
have "sourcenode a -a#ys→* nx" by(fastforce intro:Cons_path)
from ‹sourcenode a -a#ys→* nx› ‹nx ∉ set(sourcenodes (a#ys))›
‹nx postdominates (targetnode a)› ‹valid_edge x'›
‹¬ nx postdominates (targetnode x')› ‹sourcenode a = sourcenode x'›
have "(sourcenode a) controls⇩s nx"
by(fastforce simp:standard_control_dependence_def)
with ‹nx ∈ (PDG_BS S)› have "sourcenode a ∈ (PDG_BS S)"
by(rule cd_closed)
with ‹valid_edge a› have "obs (sourcenode a) (PDG_BS S) = {sourcenode a}"
by(fastforce intro!:n_in_obs)
with ‹m ∈ obs (sourcenode a) (PDG_BS S)›
‹nx ∈ obs (sourcenode a) (PDG_BS S)› ‹nx ≠ m›
show False by simp
next
case False
with ‹m ∈ obs (sourcenode a) (PDG_BS S)› ‹valid_node m›
‹¬ m postdominates sourcenode a›
show False by(fastforce dest:obs_postdominate)
qed
qed
qed

lemma PDGBackwardSliceCorrect:
"BackwardSlice sourcenode targetnode kind valid_edge
(_Entry_) Def Use state_val PDG_BS"
proof(unfold_locales)
fix n S assume "n ∈ PDG_BS S"
thus "valid_node n" by(rule PDG_BS_valid_node)
next
fix n S assume "valid_node n" and "n ∈ S"
thus "n ∈ PDG_BS S" by(fastforce intro:PDG_path_Nil simp:PDG_BS_def)
next
fix n' S n V
assume "n' ∈ PDG_BS S" and "n influences V in n'"
thus "n ∈ PDG_BS S"
by(auto dest:PDG.PDG_path_ddep[OF PDG_scd,OF PDG.PDG_ddep_edge[OF PDG_scd]]
dest:PDG_path_Append simp:PDG_BS_def split:if_split_asm)
next
fix n S
have "(∃m. obs n (PDG_BS S) = {m}) ∨ obs n (PDG_BS S) = {}"
by(rule obs_singleton)
thus "finite (obs n (PDG_BS S))" by fastforce
next
fix n S
have "(∃m. obs n (PDG_BS S) = {m}) ∨ obs n (PDG_BS S) = {}"
by(rule obs_singleton)
thus "card (obs n (PDG_BS S)) ≤ 1" by fastforce
qed

end

subsection‹Weak control dependence›

context WeakControlDependencePDG begin

lemma Exit_in_obs_slice_node:"(_Exit_) ∈ obs n' (PDG_BS S) ⟹ (_Exit_) ∈ S"
by(auto elim:obsE PDG_path_CFG_path simp:PDG_BS_def split:if_split_asm)

lemma cd_closed:
"⟦n' ∈ PDG_BS S; n weakly controls n'⟧ ⟹ n ∈ PDG_BS S"

lemma obs_strong_postdominate:
assumes "n ∈ obs n' (PDG_BS S)" and "n ≠ (_Exit_)"
shows "n strongly-postdominates n'"
proof(rule ccontr)
assume "¬ n strongly-postdominates n'"
from ‹n ∈ obs n' (PDG_BS S)› have "valid_node n" by(fastforce dest:in_obs_valid)
with ‹n ∈ obs n' (PDG_BS S)› ‹n ≠ (_Exit_)› have "n strongly-postdominates n"
by(fastforce intro:strong_postdominate_refl)
from ‹n ∈ obs n' (PDG_BS S)› obtain as where "n' -as→* n"
and "∀n' ∈ set(sourcenodes as). n' ∉ (PDG_BS S)"
and "n ∈ (PDG_BS S)" by(erule obsE)
from ‹n strongly-postdominates n› ‹¬ n strongly-postdominates n'› ‹n' -as→* n›
obtain as' a as'' where [simp]:"as = as'@a#as''" and "valid_edge a"
and "¬ n strongly-postdominates (sourcenode a)" and
"n strongly-postdominates (targetnode a)"
by -(erule strong_postdominate_path_branch)
from ‹n ∈ obs n' (PDG_BS S)› ‹∀n' ∈ set(sourcenodes as). n' ∉ (PDG_BS S)›
have "n ∉ set (sourcenodes (a#as''))"
by(fastforce elim:obs.cases simp:sourcenodes_def)
from ‹n' -as→* n› have "sourcenode a -a#as''→* n"
by(fastforce dest:path_split_second)
from ‹¬ n strongly-postdominates (sourcenode a)› ‹valid_edge a› ‹valid_node n›
obtain a' where "sourcenode a' = sourcenode a"
and "valid_edge a'" and "¬ n strongly-postdominates (targetnode a')"
by(fastforce elim:not_strong_postdominate_predecessor_successor)
with ‹n strongly-postdominates (targetnode a)› ‹n ∉ set (sourcenodes (a#as''))›
‹sourcenode a -a#as''→* n›
have "sourcenode a weakly controls n"
by(fastforce simp:weak_control_dependence_def)
with ‹n ∈ obs n' (PDG_BS S)› have "sourcenode a ∈ (PDG_BS S)"
by(fastforce intro:cd_closed PDG_cdep_edge elim:obs.cases)
with ‹∀n' ∈ set(sourcenodes as). n' ∉ (PDG_BS S)›
qed

lemma obs_singleton:"(∃m. obs n (PDG_BS S) = {m}) ∨ obs n (PDG_BS S) = {}"
proof(rule ccontr)
assume "¬ ((∃m. obs n (PDG_BS S) = {m}) ∨ obs n (PDG_BS S) = {})"
hence "∃nx nx'. nx ∈ obs n (PDG_BS S) ∧ nx' ∈ obs n (PDG_BS S) ∧
nx ≠ nx'" by auto
then obtain nx nx' where "nx ∈ obs n (PDG_BS S)" and "nx' ∈ obs n (PDG_BS S)"
and "nx ≠ nx'" by auto
from ‹nx ∈ obs n (PDG_BS S)› obtain as where "n -as→* nx"
and "∀n' ∈ set(sourcenodes as). n' ∉ (PDG_BS S)" and "nx ∈ (PDG_BS S)"
by(erule obsE)
from ‹n -as→* nx› have "valid_node nx" by(fastforce dest:path_valid_node)
with ‹nx ∈ (PDG_BS S)› have "obs nx (PDG_BS S) = {nx}" by -(rule n_in_obs)
with ‹n -as→* nx› ‹nx ∈ obs n (PDG_BS S)› ‹nx' ∈ obs n (PDG_BS S)› ‹nx ≠ nx'›
have "as ≠ []" by(fastforce elim:path.cases)
with ‹n -as→* nx› ‹nx ∈ obs n (PDG_BS S)› ‹nx' ∈ obs n (PDG_BS S)›
‹nx ≠ nx'› ‹obs nx (PDG_BS S) = {nx}› ‹∀n' ∈ set(sourcenodes as). n' ∉ (PDG_BS S)›
have "∃a as' as''. n -as'→* sourcenode a ∧ targetnode a -as''→* nx ∧
valid_edge a ∧ as = as'@a#as'' ∧
obs (targetnode a) (PDG_BS S) = {nx} ∧
(¬ (∃m. obs (sourcenode a) (PDG_BS S) = {m} ∨
obs (sourcenode a) (PDG_BS S) = {}))"
proof(induct arbitrary:nx' rule:path.induct)
case (Cons_path n'' as n' a n)
note [simp] = ‹sourcenode a = n›[THEN sym] ‹targetnode a = n''›[THEN sym]
note more_than_one = ‹n' ∈ obs n (PDG_BS S)› ‹nx' ∈ obs n (PDG_BS S)› ‹n' ≠ nx'›
note IH = ‹⋀nx'. ⟦n' ∈ obs n'' (PDG_BS S); nx' ∈ obs n'' (PDG_BS S); n' ≠ nx';
obs n' (PDG_BS S) = {n'}; ∀n'∈set (sourcenodes as). n' ∉ (PDG_BS S); as ≠ []⟧
⟹ ∃a as' as''. n'' -as'→* sourcenode a ∧ targetnode a -as''→* n' ∧
valid_edge a ∧ as = as'@a#as'' ∧ obs (targetnode a) (PDG_BS S) = {n'} ∧
(¬ (∃m. obs (sourcenode a) (PDG_BS S) = {m} ∨
obs (sourcenode a) (PDG_BS S) = {}))›
from ‹∀n'∈set (sourcenodes (a#as)). n' ∉ (PDG_BS S)›
have "∀n'∈set (sourcenodes as). n' ∉ (PDG_BS S)" and "sourcenode a ∉ (PDG_BS S)"
show ?case
proof(cases "as = []")
case True
with ‹n'' -as→* n'› have [simp]:"n' = n''" by(fastforce elim:path.cases)
from more_than_one
have "¬ (∃m. obs (sourcenode a) (PDG_BS S) = {m} ∨
obs (sourcenode a) (PDG_BS S) = {})"
by auto
with ‹obs n' (PDG_BS S) = {n'}› True ‹valid_edge 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)
next
case False
hence "as ≠ []" .
from ‹n'' -as→* n'› ‹∀n'∈set (sourcenodes as). n' ∉ (PDG_BS S)›
have "obs n' (PDG_BS S) ⊆ obs n'' (PDG_BS S)" by(rule path_obs_subset)
show ?thesis
proof(cases "obs n' (PDG_BS S) = obs n'' (PDG_BS S)")
case True
with ‹n'' -as→* n'› ‹valid_edge a› ‹obs n' (PDG_BS S) = {n'}› 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)
next
case False
with ‹obs n' (PDG_BS S) ⊆ obs n'' (PDG_BS S)›
have "obs n' (PDG_BS S) ⊂ obs n'' (PDG_BS S)" by simp
with ‹obs n' (PDG_BS S) = {n'}› obtain ni where "n' ∈ obs n'' (PDG_BS S)"
and "ni ∈ obs n'' (PDG_BS S)" and "n' ≠ ni" by auto
from IH[OF this ‹obs n' (PDG_BS S) = {n'}›
‹∀n'∈set (sourcenodes as). n' ∉ (PDG_BS S)› ‹as ≠ []›] obtain a' as' as''
where "n'' -as'→* sourcenode a'" and "targetnode a' -as''→* n'"
and "valid_edge a'" and [simp]:"as = as'@a'#as''"
and "obs (targetnode a') (PDG_BS S) = {n'}"
and more_than_one':"¬ (∃m. obs (sourcenode a') (PDG_BS S) = {m} ∨
obs (sourcenode a') (PDG_BS S) = {})"
by blast
from ‹n'' -as'→* sourcenode a'› ‹valid_edge a›
have "n -a#as'→* sourcenode a'" by(fastforce intro:path.Cons_path)
with ‹targetnode a' -as''→* n'› ‹obs (targetnode a') (PDG_BS S) = {n'}›
more_than_one' ‹valid_edge a'› 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 "obs (targetnode a) (PDG_BS S) = {nx}"
and more_than_one:"¬ (∃m. obs (sourcenode a) (PDG_BS S) = {m} ∨
obs (sourcenode a) (PDG_BS S) = {})"
by blast
have "sourcenode a ∉ (PDG_BS S)"
proof(rule ccontr)
assume "¬ sourcenode a ∉ PDG_BS S"
hence "sourcenode a ∈ PDG_BS S" by simp
with ‹valid_edge a› have "obs (sourcenode a) (PDG_BS S) = {sourcenode a}"
by(fastforce intro!:n_in_obs)
with more_than_one show False by simp
qed
with ‹valid_edge a›
have "obs (targetnode a) (PDG_BS S) ⊆ obs (sourcenode a) (PDG_BS S)"
by(rule edge_obs_subset)
with ‹obs (targetnode a) (PDG_BS S) = {nx}›
have "nx ∈ obs (sourcenode a) (PDG_BS S)" by simp
with more_than_one obtain m  where "m ∈ obs (sourcenode a) (PDG_BS S)"
and "nx ≠ m" by auto
from ‹m ∈ obs (sourcenode a) (PDG_BS S)›
have "valid_node m" by(fastforce dest:in_obs_valid)
from ‹obs (targetnode a) (PDG_BS S) = {nx}› have "valid_node nx"
by(fastforce dest:in_obs_valid)
show False
proof(cases "m strongly-postdominates (sourcenode a)")
case True
with ‹nx ∈ obs (sourcenode a) (PDG_BS S)› ‹m ∈ obs (sourcenode a) (PDG_BS S)›
have "m strongly-postdominates nx"
by(fastforce intro:strong_postdominate_path_targetnode elim:obs.cases)
with ‹nx ≠ m› have "¬ nx strongly-postdominates m"
by(fastforce dest:strong_postdominate_antisym)
have "(_Exit_) -[]→* (_Exit_)" by(fastforce intro:empty_path)
with ‹m strongly-postdominates nx› have "nx ≠ (_Exit_)"
by(fastforce simp:strong_postdominate_def sourcenodes_def postdominate_def)
have "¬ nx strongly-postdominates (sourcenode a)"
proof(rule ccontr)
assume "¬ ¬ nx strongly-postdominates sourcenode a"
hence "nx strongly-postdominates sourcenode a" by simp
from ‹m ∈ obs (sourcenode a) (PDG_BS S)› ‹nx ∈ obs (sourcenode a) (PDG_BS S)›
obtain asx' where "sourcenode a -asx'→* m" and "nx ∉ set(sourcenodes asx')"
by(fastforce elim:obs.cases)
with ‹nx strongly-postdominates sourcenode a› have "nx strongly-postdominates m"
by(rule strong_postdominate_path_targetnode)
with ‹¬ nx strongly-postdominates m› show False by simp
qed
with ‹nx ∈ obs (sourcenode a) (PDG_BS S)› ‹valid_node nx› ‹nx ≠ (_Exit_)›
show False by(fastforce dest:obs_strong_postdominate)
next
case False
show False
proof(cases "m = Exit")
case True
from ‹m ∈ obs (sourcenode a) (PDG_BS S)› ‹nx ∈ obs (sourcenode a) (PDG_BS S)›
obtain xs where "sourcenode a -xs→* m" and "nx ∉ set(sourcenodes xs)"
by(fastforce elim:obsE)
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
with ‹m ∈ obs (sourcenode a) (PDG_BS S)›
have "m ∈ (PDG_BS S)" by (metis obsE)
with ‹valid_node m› have "obs m (PDG_BS S) = {m}"
by(rule n_in_obs)
with ‹nx ∈ obs (sourcenode a) (PDG_BS S)› ‹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"
by(auto elim:path_split_Cons)
from ‹targetnode x' -xs'→* m› ‹nx ∉ set(sourcenodes xs)› ‹valid_edge x'›
‹valid_node m› True
have "¬ nx strongly-postdominates (targetnode x')"
by(fastforce simp:strong_postdominate_def postdominate_def sourcenodes_def)
from ‹nx ≠ m› True have "nx ≠ (_Exit_)" by simp
with ‹obs (targetnode a) (PDG_BS S) = {nx}›
have "nx strongly-postdominates (targetnode a)"
by(fastforce intro:obs_strong_postdominate)
from ‹obs (targetnode a) (PDG_BS S) = {nx}›
obtain ys where "targetnode a -ys→* nx"
and "∀nx' ∈ set(sourcenodes ys). nx' ∉ (PDG_BS S)"
and "nx ∈ (PDG_BS S)" by(fastforce elim:obsE)
hence "nx ∉ set(sourcenodes ys)"by fastforce
have "sourcenode a ≠ nx"
proof
assume "sourcenode a = nx"
from ‹nx ∈ obs (sourcenode a) (PDG_BS S)›
have "nx ∈ (PDG_BS S)" by -(erule obsE)
with ‹valid_node nx› have "obs nx (PDG_BS S) = {nx}" by -(erule n_in_obs)
with ‹sourcenode a = nx› ‹m ∈ obs (sourcenode a) (PDG_BS S)›
‹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›
have "sourcenode a -a#ys→* nx" by(fastforce intro:Cons_path)
from ‹sourcenode a -a#ys→* nx› ‹nx ∉ set(sourcenodes (a#ys))›
‹nx strongly-postdominates (targetnode a)› ‹valid_edge x'›
‹¬ nx strongly-postdominates (targetnode x')› ‹sourcenode a = sourcenode x'›
have "(sourcenode a) weakly controls nx"
by(fastforce simp:weak_control_dependence_def)
with ‹nx ∈ (PDG_BS S)› have "sourcenode a ∈ (PDG_BS S)"
by(rule cd_closed)
with ‹valid_edge a› have "obs (sourcenode a) (PDG_BS S) = {sourcenode a}"
by(fastforce intro!:n_in_obs)
with ‹m ∈ obs (sourcenode a) (PDG_BS S)›
‹nx ∈ obs (sourcenode a) (PDG_BS S)› ‹nx ≠ m›
show False by simp
next
case False
with ‹m ∈ obs (sourcenode a) (PDG_BS S)› ‹valid_node m›
‹¬ m strongly-postdominates sourcenode a›
show False by(fastforce dest:obs_strong_postdominate)
qed
qed
qed

lemma WeakPDGBackwardSliceCorrect:
"BackwardSlice sourcenode targetnode kind valid_edge
(_Entry_) Def Use state_val PDG_BS"
proof(unfold_locales)
fix n S assume "n ∈ PDG_BS S"
thus "valid_node n" by(rule PDG_BS_valid_node)
next
fix n S assume "valid_node n" and "n ∈ S"
thus "n ∈ PDG_BS S" by(fastforce intro:PDG_path_Nil simp:PDG_BS_def)
next
fix n' S n V assume "n' ∈ PDG_BS S" and "n influences V in n'"
thus "n ∈ PDG_BS S"
by(auto dest:PDG.PDG_path_ddep[OF PDG_wcd,OF PDG.PDG_ddep_edge[OF PDG_wcd]]
dest:PDG_path_Append simp:PDG_BS_def split:if_split_asm)
next
fix n S
have "(∃m. obs n (PDG_BS S) = {m}) ∨ obs n (PDG_BS S) = {}"
by(rule obs_singleton)
thus "finite (obs n (PDG_BS S))" by fastforce
next
fix n S
have "(∃m. obs n (PDG_BS S) = {m}) ∨ obs n (PDG_BS S) = {}"
by(rule obs_singleton)
thus "card (obs n (PDG_BS S)) ≤ 1" by fastforce
qed

end

subsection‹Weak order dependence›

context CFG_wf begin

lemma obs_singleton:
(*assumes valid:"valid_node n"*)
shows "(∃m. obs n (wod_backward_slice S) = {m}) ∨
obs n (wod_backward_slice S) = {}"
proof(rule ccontr)
let ?WOD_BS = "wod_backward_slice S"
assume "¬ ((∃m. obs n ?WOD_BS = {m}) ∨ obs n ?WOD_BS = {})"
hence "∃nx nx'. nx ∈ obs n ?WOD_BS ∧ nx' ∈ obs n ?WOD_BS ∧
nx ≠ nx'" by auto
then obtain nx nx' where "nx ∈ obs n ?WOD_BS" and "nx' ∈ obs n ?WOD_BS"
and "nx ≠ nx'" by auto
from ‹nx ∈ obs n ?WOD_BS› obtain as where "n -as→* nx"
and "∀n' ∈ set(sourcenodes as). n' ∉ ?WOD_BS" and "nx ∈ ?WOD_BS"
by(erule obsE)
from ‹n -as→* nx› have "valid_node nx" by(fastforce dest:path_valid_node)
with ‹nx ∈ ?WOD_BS› have "obs nx ?WOD_BS = {nx}" by -(rule n_in_obs)
with ‹n -as→* nx› ‹nx ∈ obs n ?WOD_BS› ‹nx' ∈ obs n ?WOD_BS› ‹nx ≠ nx'›
have "as ≠ []" by(fastforce elim:path.cases)
with ‹n -as→* nx› ‹nx ∈ obs n ?WOD_BS› ‹nx' ∈ obs n ?WOD_BS› ‹nx ≠ nx'›
‹obs nx ?WOD_BS = {nx}› ‹∀n' ∈ set(sourcenodes as). n' ∉ ?WOD_BS›
have "∃a as' as''. n -as'→* sourcenode a ∧ targetnode a -as''→* nx ∧
valid_edge a ∧ as = as'@a#as'' ∧
obs (targetnode a) ?WOD_BS = {nx} ∧
(¬ (∃m. obs (sourcenode a) ?WOD_BS = {m} ∨
obs (sourcenode a) ?WOD_BS = {}))"
proof(induct arbitrary:nx' rule:path.induct)
case (Cons_path n'' as n' a n)
note [simp] = ‹sourcenode a = n›[THEN sym] ‹targetnode a = n''›[THEN sym]
note more_than_one = ‹n' ∈ obs n (?WOD_BS)› ‹nx' ∈ obs n (?WOD_BS)› ‹n' ≠ nx'›
note IH = ‹⋀nx'. ⟦n' ∈ obs n'' (?WOD_BS); nx' ∈ obs n'' (?WOD_BS); n' ≠ nx';
obs n' (?WOD_BS) = {n'}; ∀n'∈set (sourcenodes as). n' ∉ (?WOD_BS); as ≠ []⟧
⟹ ∃a as' as''. n'' -as'→* sourcenode a ∧ targetnode a -as''→* n' ∧
valid_edge a ∧ as = as'@a#as'' ∧ obs (targetnode a) (?WOD_BS) = {n'} ∧
(¬ (∃m. obs (sourcenode a) (?WOD_BS) = {m} ∨
obs (sourcenode a) (?WOD_BS) = {}))›
from ‹∀n'∈set (sourcenodes (a#as)). n' ∉ (?WOD_BS)›
have "∀n'∈set (sourcenodes as). n' ∉ (?WOD_BS)" and "sourcenode a ∉ (?WOD_BS)"
show ?case
proof(cases "as = []")
case True
with ‹n'' -as→* n'› have [simp]:"n' = n''" by(fastforce elim:path.cases)
from more_than_one
have "¬ (∃m. obs (sourcenode a) (?WOD_BS) = {m} ∨
obs (sourcenode a) (?WOD_BS) = {})"
by auto
with ‹obs n' (?WOD_BS) = {n'}› True ‹valid_edge 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)
next
case False
hence "as ≠ []" .
from ‹n'' -as→* n'› ‹∀n'∈set (sourcenodes as). n' ∉ (?WOD_BS)›
have "obs n' (?WOD_BS) ⊆ obs n'' (?WOD_BS)" by(rule path_obs_subset)
show ?thesis
proof(cases "obs n' (?WOD_BS) = obs n'' (?WOD_BS)")
case True
with ‹n'' -as→* n'› ‹valid_edge a› ‹obs n' (?WOD_BS) = {n'}› 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)
next
case False
with ‹obs n' (?WOD_BS) ⊆ obs n'' (?WOD_BS)›
have "obs n' (?WOD_BS) ⊂ obs n'' (?WOD_BS)" by simp
with ‹obs n' (?WOD_BS) = {n'}› obtain ni where "n' ∈ obs n'' (?WOD_BS)"
and "ni ∈ obs n'' (?WOD_BS)" and "n' ≠ ni" by auto
from IH[OF this ‹obs n' (?WOD_BS) = {n'}›
‹∀n'∈set (sourcenodes as). n' ∉ (?WOD_BS)› ‹as ≠ []›] obtain a' as' as''
where "n'' -as'→* sourcenode a'" and "targetnode a' -as''→* n'"
and "valid_edge a'" and [simp]:"as = as'@a'#as''"
and "obs (targetnode a') (?WOD_BS) = {n'}"
and more_than_one':"¬ (∃m. obs (sourcenode a') (?WOD_BS) = {m} ∨
obs (sourcenode a') (?WOD_BS) = {})"
by blast
from ‹n'' -as'→* sourcenode a'› ‹valid_edge a›
have "n -a#as'→* sourcenode a'" by(fastforce intro:path.Cons_path)
with ‹targetnode a' -as''→* n'› ‹obs (targetnode a') (?WOD_BS) = {n'}›
more_than_one' ‹valid_edge a'› 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 "obs (targetnode a) (?WOD_BS) = {nx}"
and more_than_one:"¬ (∃m. obs (sourcenode a) (?WOD_BS) = {m} ∨
obs (sourcenode a) (?WOD_BS) = {})"
by blast
have "sourcenode a ∉ (?WOD_BS)"
proof(rule ccontr)
assume "¬ sourcenode a ∉ ?WOD_BS"
hence "sourcenode a ∈ ?WOD_BS" by simp
with ‹valid_edge a› have "obs (sourcenode a) (?WOD_BS) = {sourcenode a}"
by(fastforce intro!:n_in_obs)
with more_than_one show False by simp
qed
with ‹valid_edge a›
have "obs (targetnode a) (?WOD_BS) ⊆ obs (sourcenode a) (?WOD_BS)"
by(rule edge_obs_subset)
with ‹obs (targetnode a) (?WOD_BS) = {nx}›
have "nx ∈ obs (sourcenode a) (?WOD_BS)" by simp
with more_than_one obtain m  where "m ∈ obs (sourcenode a) (?WOD_BS)"
and "nx ≠ m" by auto
with ‹nx ∈ obs (sourcenode a) (?WOD_BS)› obtain as2
where "sourcenode a -as2→* m" and "nx ∉ set(sourcenodes as2)"
by(fastforce elim:obsE)
from ‹nx ∈ obs (sourcenode a) (?WOD_BS)› ‹m ∈ obs (sourcenode a) (?WOD_BS)›
obtain as1 where "sourcenode a -as1→* nx" and "m ∉ set(sourcenodes as1)"
by(fastforce elim:obsE)
from ‹obs (targetnode a) (?WOD_BS) = {nx}› obtain asx
where "targetnode a -asx→* nx" by(fastforce elim:obsE)
have "∀asx'. targetnode a -asx'→* m ⟶ nx ∈ set(sourcenodes asx')"
proof(rule ccontr)
assume "¬ (∀asx'. targetnode a -asx'→* m ⟶ nx ∈ set (sourcenodes asx'))"
then obtain asx' where "targetnode a -asx'→* m" and "nx ∉ set (sourcenodes asx')"
by blast
show False
proof(cases "∀nx ∈ set(sourcenodes asx'). nx ∉ ?WOD_BS")
case True
with ‹targetnode a -asx'→* m› ‹m ∈ obs (sourcenode a) (?WOD_BS)›
have "m ∈ obs (targetnode a) ?WOD_BS" by(fastforce intro:obs_elem elim:obsE)
with ‹nx ≠ m› ‹obs (targetnode a) (?WOD_BS) = {nx}› show False by simp
next
case False
hence "∃nx ∈ set(sourcenodes asx'). nx ∈ ?WOD_BS" by blast
then obtain nx' ns ns' where "sourcenodes asx' = ns@nx'#ns'" and "nx' ∈ ?WOD_BS"
and "∀nx ∈ set ns. nx ∉ ?WOD_BS" by(fastforce elim!:split_list_first_propE)
from ‹sourcenodes asx' = ns@nx'#ns'› obtain ax ai ai'
where [simp]:"asx' = ai@ax#ai'" "ns = sourcenodes ai" "nx' = sourcenode ax"
by(fastforce elim:map_append_append_maps simp:sourcenodes_def)
from ‹targetnode a -asx'→* m› have "targetnode a -ai→* sourcenode ax"
by(fastforce dest:path_split)
with ‹nx' ∈ ?WOD_BS› ‹∀nx ∈ set ns. nx ∉ ?WOD_BS›
have "nx' ∈ obs (targetnode a) ?WOD_BS" by(fastforce intro:obs_elem)
with ‹obs (targetnode a) (?WOD_BS) = {nx}› have "nx' = nx" by simp
with ‹nx ∉ set (sourcenodes asx')› show False by(simp add:sourcenodes_def)
qed
qed
with ‹nx ≠ m› ‹sourcenode a -as1→* nx› ‹m ∉ set(sourcenodes as1)›
‹sourcenode a -as2→* m› ‹nx ∉ set(sourcenodes as2)› ‹valid_edge a›
‹targetnode a -asx→* nx›
have "sourcenode a ⟶⇩w⇩o⇩d nx,m" by(simp add:wod_def,blast)
with ‹nx ∈ obs (sourcenode a) (?WOD_BS)› ‹m ∈ obs (sourcenode a) (?WOD_BS)›
have "sourcenode a ∈ ?WOD_BS" by(fastforce elim:cd_closed elim:obsE)
with ‹sourcenode a ∉ ?WOD_BS› show False by simp
qed

lemma WODBackwardSliceCorrect:
"BackwardSlice sourcenode targetnode kind valid_edge
(_Entry_) Def Use state_val wod_backward_slice"
proof(unfold_locales)
fix n S assume "n ∈ wod_backward_slice S"
thus "valid_node n" by(rule wod_backward_slice_valid_node)
next
fix n S assume "valid_node n" and "n ∈ S"
thus "n ∈ wod_backward_slice S" by(rule refl)
next
fix n' S n V assume "n' ∈ wod_backward_slice S" "n influences V in n'"
thus "n ∈ wod_backward_slice S"
by -(rule dd_closed)
next
fix n S
have "(∃m. obs n (wod_backward_slice S) = {m}) ∨
obs n (wod_backward_slice S) = {}"
by(rule obs_singleton)
thus "finite (obs n (wod_backward_slice S))" by fastforce
next
fix n S
have "(∃m. obs n (wod_backward_slice S) = {m}) ∨ obs n (wod_backward_slice S) = {}"
by(rule obs_singleton)
thus "card (obs n (wod_backward_slice S)) ≤ 1" by fastforce
qed

end

end
```