# Theory PDG

```section ‹Program Dependence Graph›

theory PDG imports
StandardControlDependence
WeakControlDependence
"../Basic/CFGExit_wf"
begin

locale PDG =
CFGExit_wf sourcenode targetnode kind valid_edge Entry Def Use state_val Exit
for sourcenode :: "'edge ⇒ 'node" and targetnode :: "'edge ⇒ 'node"
and kind :: "'edge ⇒ 'state edge_kind" and valid_edge :: "'edge ⇒ bool"
and Entry :: "'node" ("'('_Entry'_')") and Def :: "'node ⇒ 'var set"
and Use :: "'node ⇒ 'var set" and state_val :: "'state ⇒ 'var ⇒ 'val"
and Exit :: "'node" ("'('_Exit'_')") +
fixes control_dependence :: "'node ⇒ 'node ⇒ bool"
("_ controls _ " [51,0])
assumes Exit_not_control_dependent:"n controls n' ⟹ n' ≠ (_Exit_)"
assumes control_dependence_path:
"n controls n'
⟹ ∃as. CFG.path sourcenode targetnode valid_edge n as n' ∧ as ≠ []"

begin

inductive cdep_edge :: "'node ⇒ 'node ⇒ bool"
("_ ⟶⇩c⇩d _" [51,0] 80)
and ddep_edge :: "'node ⇒ 'var ⇒ 'node ⇒ bool"
("_ -_→⇩d⇩d _" [51,0,0] 80)
and PDG_edge :: "'node ⇒ 'var option ⇒ 'node ⇒ bool"

where
(* Syntax *)
"n ⟶⇩c⇩d n' == PDG_edge n None n'"
| "n -V→⇩d⇩d n' == PDG_edge n (Some V) n'"

(* Rules *)
| PDG_cdep_edge:
"n controls n' ⟹ n ⟶⇩c⇩d n'"

| PDG_ddep_edge:
"n influences V in n' ⟹ n -V→⇩d⇩d n'"

inductive PDG_path :: "'node ⇒ 'node ⇒ bool"
("_ ⟶⇩d* _" [51,0] 80)

where PDG_path_Nil:
"valid_node n ⟹ n ⟶⇩d* n"

| PDG_path_Append_cdep:
"⟦n ⟶⇩d* n''; n'' ⟶⇩c⇩d n'⟧ ⟹ n ⟶⇩d* n'"

| PDG_path_Append_ddep:
"⟦n ⟶⇩d* n''; n'' -V→⇩d⇩d n'⟧ ⟹ n ⟶⇩d* n'"

lemma PDG_path_cdep:"n ⟶⇩c⇩d n' ⟹ n ⟶⇩d* n'"
apply -
apply(rule PDG_path_Append_cdep, rule PDG_path_Nil)
by(auto elim!:PDG_edge.cases dest:control_dependence_path path_valid_node)

lemma PDG_path_ddep:"n -V→⇩d⇩d n' ⟹ n ⟶⇩d* n'"
apply -
apply(rule PDG_path_Append_ddep, rule PDG_path_Nil)
by(auto elim!:PDG_edge.cases dest:path_valid_node simp:data_dependence_def)

lemma PDG_path_Append:
"⟦n'' ⟶⇩d* n'; n ⟶⇩d* n''⟧ ⟹ n ⟶⇩d* n'"
by(induct rule:PDG_path.induct,auto intro:PDG_path.intros)

lemma PDG_cdep_edge_CFG_path:
assumes "n ⟶⇩c⇩d n'" obtains as where "n -as→* n'" and "as ≠ []"
using ‹n ⟶⇩c⇩d n'›
by(auto elim:PDG_edge.cases dest:control_dependence_path)

lemma PDG_ddep_edge_CFG_path:
assumes "n -V→⇩d⇩d n'" obtains as where "n -as→* n'" and "as ≠ []"
using ‹n -V→⇩d⇩d n'›
by(auto elim!:PDG_edge.cases simp:data_dependence_def)

lemma PDG_path_CFG_path:
assumes "n ⟶⇩d* n'" obtains as where "n -as→* n'"
proof(atomize_elim)
from ‹n ⟶⇩d* n'› show "∃as. n -as→* n'"
proof(induct rule:PDG_path.induct)
case (PDG_path_Nil n)
hence "n -[]→* n" by(rule empty_path)
thus ?case by blast
next
case (PDG_path_Append_cdep n n'' n')
from ‹n'' ⟶⇩c⇩d n'› obtain as where "n'' -as→* n'"
by(fastforce elim:PDG_cdep_edge_CFG_path)
with ‹∃as. n -as→* n''› obtain as' where "n -as'@as→* n'"
by(auto dest:path_Append)
thus ?case by blast
next
case (PDG_path_Append_ddep n n'' V n')
from ‹n'' -V→⇩d⇩d n'› obtain as where "n'' -as→* n'"
by(fastforce elim:PDG_ddep_edge_CFG_path)
with ‹∃as. n -as→* n''› obtain as' where "n -as'@as→* n'"
by(auto dest:path_Append)
thus ?case by blast
qed
qed

lemma PDG_path_Exit:"⟦n ⟶⇩d* n'; n' = (_Exit_)⟧ ⟹ n = (_Exit_)"
apply(induct rule:PDG_path.induct)
by(auto elim:PDG_edge.cases dest:Exit_not_control_dependent
simp:data_dependence_def)

lemma PDG_path_not_inner:
"⟦n ⟶⇩d* n'; ¬ inner_node n'⟧ ⟹ n = n'"
proof(induct rule:PDG_path.induct)
case (PDG_path_Nil n)
thus ?case by simp
next
case (PDG_path_Append_cdep n n'' n')
from ‹n'' ⟶⇩c⇩d n'› ‹¬ inner_node n'› have False
apply -
apply(erule PDG_edge.cases) apply(auto simp:inner_node_def)
apply(fastforce dest:control_dependence_path path_valid_node)
apply(fastforce dest:control_dependence_path path_valid_node)
by(fastforce dest:Exit_not_control_dependent)
thus ?case by simp
next
case (PDG_path_Append_ddep n n'' V n')
from ‹n'' -V→⇩d⇩d n'› ‹¬ inner_node n'› have False
apply -
apply(erule PDG_edge.cases)
by(auto dest:path_valid_node simp:inner_node_def data_dependence_def)
thus ?case by simp
qed

subsection ‹Definition of the static backward slice›

text ‹Node: instead of a single node, we calculate the backward slice of a set
of nodes.›

definition PDG_BS :: "'node set ⇒ 'node set"
where "PDG_BS S ≡ {n'. ∃n. n' ⟶⇩d* n ∧ n ∈ S ∧ valid_node n}"

lemma PDG_BS_valid_node:"n ∈ PDG_BS S ⟹ valid_node n"
by(auto elim:PDG_path_CFG_path dest:path_valid_node simp:PDG_BS_def
split:if_split_asm)

lemma Exit_PDG_BS:"n ∈ PDG_BS {(_Exit_)} ⟹ n = (_Exit_)"
by(fastforce dest:PDG_path_Exit simp:PDG_BS_def)

end

subsection ‹Instantiate static PDG›

subsubsection ‹Standard control dependence›

locale StandardControlDependencePDG =
Postdomination sourcenode targetnode kind valid_edge Entry Exit +
CFGExit_wf sourcenode targetnode kind valid_edge Entry Def Use state_val Exit
for sourcenode :: "'edge ⇒ 'node" and targetnode :: "'edge ⇒ 'node"
and kind :: "'edge ⇒ 'state edge_kind" and valid_edge :: "'edge ⇒ bool"
and Entry :: "'node" ("'('_Entry'_')") and Def :: "'node ⇒ 'var set"
and Use :: "'node ⇒ 'var set" and state_val :: "'state ⇒ 'var ⇒ 'val"
and Exit :: "'node" ("'('_Exit'_')")

begin

lemma PDG_scd:
"PDG sourcenode targetnode kind valid_edge (_Entry_)
Def Use state_val (_Exit_) standard_control_dependence"
proof(unfold_locales)
fix n n' assume "n controls⇩s n'"
show "n' ≠ (_Exit_)"
proof
assume "n' = (_Exit_)"
with ‹n controls⇩s n'› show False
by(fastforce intro:Exit_not_standard_control_dependent)
qed
next
fix n n' assume "n controls⇩s n'"
thus "∃as. n -as→* n' ∧ as ≠ []"
by(fastforce simp:standard_control_dependence_def)
qed

(*<*)
lemmas PDG_cdep_edge = PDG.PDG_cdep_edge[OF PDG_scd]
lemmas PDG_path_Nil = PDG.PDG_path_Nil[OF PDG_scd]
lemmas PDG_path_Append = PDG.PDG_path_Append[OF PDG_scd]
lemmas PDG_path_CFG_path = PDG.PDG_path_CFG_path[OF PDG_scd]
lemmas PDG_path_cdep = PDG.PDG_path_cdep[OF PDG_scd]
lemmas PDG_path_ddep = PDG.PDG_path_ddep[OF PDG_scd]
lemmas PDG_path_not_inner = PDG.PDG_path_not_inner[OF PDG_scd]
lemmas PDG_path_Exit = PDG.PDG_path_Exit[OF PDG_scd]

definition PDG_BS_s :: "'node set ⇒ 'node set" ("PDG'_BS")
where "PDG_BS S ≡
PDG.PDG_BS sourcenode targetnode valid_edge Def Use standard_control_dependence S"

lemma [simp]: "PDG.PDG_BS sourcenode targetnode valid_edge Def Use
standard_control_dependence S = PDG_BS S"

lemmas PDG_BS_def = PDG.PDG_BS_def[OF PDG_scd,simplified]
lemmas PDG_BS_valid_node = PDG.PDG_BS_valid_node[OF PDG_scd,simplified]
lemmas Exit_PDG_BS = PDG.Exit_PDG_BS[OF PDG_scd,simplified]
(*>*)

end

subsubsection ‹Weak control dependence›

locale WeakControlDependencePDG =
StrongPostdomination sourcenode targetnode kind valid_edge Entry Exit +
CFGExit_wf sourcenode targetnode kind valid_edge Entry Def Use state_val Exit
for sourcenode :: "'edge ⇒ 'node" and targetnode :: "'edge ⇒ 'node"
and kind :: "'edge ⇒ 'state edge_kind" and valid_edge :: "'edge ⇒ bool"
and Entry :: "'node" ("'('_Entry'_')") and Def :: "'node ⇒ 'var set"
and Use :: "'node ⇒ 'var set" and state_val :: "'state ⇒ 'var ⇒ 'val"
and Exit :: "'node" ("'('_Exit'_')")

begin

lemma PDG_wcd:
"PDG sourcenode targetnode kind valid_edge (_Entry_)
Def Use state_val (_Exit_) weak_control_dependence"
proof(unfold_locales)
fix n n' assume "n weakly controls n'"
show "n' ≠ (_Exit_)"
proof
assume "n' = (_Exit_)"
with ‹n weakly controls n'› show False
by(fastforce intro:Exit_not_weak_control_dependent)
qed
next
fix n n' assume "n weakly controls n'"
thus "∃as. n -as→* n' ∧ as ≠ []"
by(fastforce simp:weak_control_dependence_def)
qed

(*<*)
lemmas PDG_cdep_edge = PDG.PDG_cdep_edge[OF PDG_wcd]
lemmas PDG_path_Nil = PDG.PDG_path_Nil[OF PDG_wcd]
lemmas PDG_path_Append = PDG.PDG_path_Append[OF PDG_wcd]
lemmas PDG_path_CFG_path = PDG.PDG_path_CFG_path[OF PDG_wcd]
lemmas PDG_path_cdep = PDG.PDG_path_cdep[OF PDG_wcd]
lemmas PDG_path_ddep = PDG.PDG_path_ddep[OF PDG_wcd]
lemmas PDG_path_not_inner = PDG.PDG_path_not_inner[OF PDG_wcd]
lemmas PDG_path_Exit = PDG.PDG_path_Exit[OF PDG_wcd]

definition PDG_BS_w :: "'node set ⇒ 'node set" ("PDG'_BS")
where "PDG_BS S ≡
PDG.PDG_BS sourcenode targetnode valid_edge Def Use weak_control_dependence S"

lemma [simp]: "PDG.PDG_BS sourcenode targetnode valid_edge Def Use
weak_control_dependence S = PDG_BS S"