Theory PDG

section ‹Program Dependence Graph›

theory PDG imports 
  DataDependence 
  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"
  by(simp add:PDG_BS_s_def)

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"
  by(simp add:PDG_BS_w_def)

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

end

end