Theory PDG

header {* \isaheader{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" 
    ("_ -->⇘cd⇙ _" [51,0] 80)
  and ddep_edge :: "'node => 'var => 'node => bool"
    ("_ -_->⇘dd⇙ _" [51,0,0] 80)
  and PDG_edge :: "'node => 'var option => 'node => bool"

where
    (* Syntax *)
  "n -->⇘cd⇙ n' == PDG_edge n None n'"
  | "n -V->⇘dd⇙ n' == PDG_edge n (Some V) n'"

    (* Rules *)
  | PDG_cdep_edge:
  "n controls n' ==> n -->⇘cd⇙ n'"

  | PDG_ddep_edge:
  "n influences V in n' ==> n -V->⇘dd⇙ 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'' -->⇘cd⇙ n'|] ==> n -->⇣d* n'"

  | PDG_path_Append_ddep:
  "[|n -->⇣d* n''; n'' -V->⇘dd⇙ n'|] ==> n -->⇣d* n'"


lemma PDG_path_cdep:"n -->⇘cd⇙ 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->⇘dd⇙ 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 -->⇘cd⇙ n'" obtains as where "n -as->* n'" and "as ≠ []"
  using `n -->⇘cd⇙ n'`
  by(auto elim:PDG_edge.cases dest:control_dependence_path)

lemma PDG_ddep_edge_CFG_path:
  assumes "n -V->⇘dd⇙ n'" obtains as where "n -as->* n'" and "as ≠ []"
  using `n -V->⇘dd⇙ 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'' -->⇘cd⇙ 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->⇘dd⇙ 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'' -->⇘cd⇙ 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->⇘dd⇙ 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:split_if_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