Theory Slicing.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" 
    ("_ 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 -Vdd 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 -Vdd 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'' -Vdd 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 -Vdd 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 -Vdd n'" obtains as where "n -as→* n'" and "as  []"
  using n -Vdd 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'' -Vdd 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'' -Vdd 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 controlss n'"
  show "n'  (_Exit_)"
  proof
    assume "n' = (_Exit_)"
    with n controlss n' show False
      by(fastforce intro:Exit_not_standard_control_dependent)
  qed
next
  fix n n' assume "n controlss 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