Quelle  DynPDG.thy

chapter ‹Dynamic Slicing›

section ‹Dynamic Program Dependence Graph›

theory DynPDG imports 
  "../Basic/DynDataDependence" 
  "../Basic/CFGExit_wf" 
  "../Basic/DynStandardControlDependence"
  "../Basic/DynWeakControlDependence"
begin

subsection ‹The dynamic PDG›

locale DynPDG = 
  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 dyn_control_dependence :: "'node ==> 'node ==> 'edge list ==> bool" 
(‹_ controls _ via _› [51,0,0])
  assumes Exit_not_dyn_control_dependent:"n controls n' via as ==> n' ≠ (_Exit_)"
  assumes dyn_control_dependence_path:
  "n controls n' via as ==> n -as→* n' ∧ as ≠ []"

begin

inductive cdep_edge :: "'node ==> 'edge list ==> 'node ==> bool" 
    (‹_ -_→_cd _› [51,0,0] 80)
  and ddep_edge :: "'node ==> 'var ==> 'edge list ==> 'node ==> bool"
    (‹_ -'{_'}_→_dd _› [51,0,0,0] 80)
  and DynPDG_edge :: "'node ==> 'var option ==> 'edge list ==> 'node ==> bool"

where
      ― ‹Syntax›
  "n -as→_cd n' == DynPDG_edge n None as n'"
  | "n -{V}as→_dd n' == DynPDG_edge n (Some V) as n'"

      ― ‹Rules›
  | DynPDG_cdep_edge:
  "n controls n' via as ==> n -as→_cd n'"

  | DynPDG_ddep_edge:
  "n influences V in n' via as ==> n -{V}as→_dd n'"


inductive DynPDG_path :: "'node ==> 'edge list ==> 'node ==> bool"
(‹_ -_→_d* _› [51,0,0] 80) 

where DynPDG_path_Nil:
  "valid_node n ==> n -[]→_d* n"

  | DynPDG_path_Append_cdep:
  "[n -as→_d* n''; n'' -as'→_cd n'] ==> n -as@as'→_d* n'"

  | DynPDG_path_Append_ddep:
  "[n -as→_d* n''; n'' -{V}as'→_dd n'] ==> n -as@as'→_d* n'"


lemma DynPDG_empty_path_eq_nodes:"n -[]→_d* n' ==> n = n'"
apply - apply(erule DynPDG_path.cases) 
  apply simp
 apply(auto elim:DynPDG_edge.cases dest:dyn_control_dependence_path)
by(auto elim:DynPDG_edge.cases simp:dyn_data_dependence_def)


lemma DynPDG_path_cdep:"n -as→_cd n' ==> n -as→_d* n'"
apply(subgoal_tac "n -[]@as→_d* n'")
 apply simp
apply(rule DynPDG_path_Append_cdep, rule DynPDG_path_Nil)
by(auto elim!:DynPDG_edge.cases dest:dyn_control_dependence_path path_valid_node)

lemma DynPDG_path_ddep:"n -{V}as→_dd n' ==> n -as→_d* n'"
apply(subgoal_tac "n -[]@as→_d* n'")
 apply simp
apply(rule DynPDG_path_Append_ddep, rule DynPDG_path_Nil)
by(auto elim!:DynPDG_edge.cases dest:path_valid_node simp:dyn_data_dependence_def)

lemma DynPDG_path_Append:
  "[n'' -as'→_d* n'; n -as→_d* n''] ==> n -as@as'→_d* n'"
apply(induct rule:DynPDG_path.induct)
  apply(auto intro:DynPDG_path.intros)
 apply(rotate_tac 1,drule DynPDG_path_Append_cdep,simp+)
apply(rotate_tac 1,drule DynPDG_path_Append_ddep,simp+)
done


lemma DynPDG_path_Exit:"[n -as→_d* n'; n' = (_Exit_)] ==> n = (_Exit_)"
apply(induct rule:DynPDG_path.induct)
by(auto elim:DynPDG_edge.cases dest:Exit_not_dyn_control_dependent 
        simp:dyn_data_dependence_def)


lemma DynPDG_path_not_inner:
  "[n -as→_d* n'; ¬ inner_node n'] ==> n = n'"
proof(induct rule:DynPDG_path.induct)
  case (DynPDG_path_Nil n)
  thus ?case by simp
next
  case (DynPDG_path_Append_cdep n as n'' as' n')
  from ‹n'' -as'→_cd n'› ‹¬ inner_node n'› have False
    apply -
    apply(erule DynPDG_edge.cases) apply(auto simp:inner_node_def)
      apply(fastforce dest:dyn_control_dependence_path path_valid_node)
     apply(fastforce dest:dyn_control_dependence_path path_valid_node)
    by(fastforce dest:Exit_not_dyn_control_dependent)
  thus ?case by simp
next
  case (DynPDG_path_Append_ddep n as n'' V as' n')
  from ‹n'' -{V}as'→_dd n'› ‹¬ inner_node n'› have False
    apply -
    apply(erule DynPDG_edge.cases) 
    by(auto dest:path_valid_node simp:inner_node_def dyn_data_dependence_def)
  thus ?case by simp
qed


lemma DynPDG_cdep_edge_CFG_path:
  assumes "n -as→_cd n'" shows "n -as→* n'" and "as ≠ []"
  using ‹n -as→_cd n'›
  by(auto elim:DynPDG_edge.cases dest:dyn_control_dependence_path)

lemma DynPDG_ddep_edge_CFG_path:
  assumes "n -{V}as→_dd n'" shows "n -as→* n'" and "as ≠ []"
  using ‹n -{V}as→_dd n'›
  by(auto elim:DynPDG_edge.cases simp:dyn_data_dependence_def)

lemma DynPDG_path_CFG_path:
  "n -as→_d* n' ==> n -as→* n'"
proof(induct rule:DynPDG_path.induct)
  case DynPDG_path_Nil thus ?case by(rule empty_path)
next
  case (DynPDG_path_Append_cdep n as n'' as' n')
  from ‹n'' -as'→_cd n'› have "n'' -as'→* n'"
    by(rule DynPDG_cdep_edge_CFG_path(1))
  with ‹n -as→* n''› show ?case by(rule path_Append)
next
  case (DynPDG_path_Append_ddep n as n'' V as' n')
  from ‹n'' -{V}as'→_dd n'› have "n'' -as'→* n'"
    by(rule DynPDG_ddep_edge_CFG_path(1))
  with ‹n -as→* n''› show ?case by(rule path_Append)
qed


lemma DynPDG_path_split: 
  "n -as→_d* n' ==>
  (as = [] ∧ n = n') ∨
  (∃n'' asx asx'. (n -asx→_cd n'') ∧ (n'' -asx'→_d* n') ∧
        (as = asx@asx')) ∨
  (∃n'' V asx asx'. (n -{V}asx→_dd n'') ∧ (n'' -asx'→_d* n') ∧
        (as = asx@asx'))"
proof(induct rule:DynPDG_path.induct)
  case (DynPDG_path_Nil n) thus ?case by auto
next
  case (DynPDG_path_Append_cdep n as n'' as' n')
  note IH = ‹as = [] ∧ n = n'' ∨
 (∃nx asx asx'. n -asx→_cd nx ∧ nx -asx'→_d* n'' ∧ as = asx@asx') ∨
 (∃nx V asx asx'. n -{V}asx→_dd nx ∧ nx -asx'→_d* n'' ∧ as = asx@asx')›
  from IH show ?case
  proof
    assume "as = [] ∧ n = n''"
    with ‹n'' -as'→_cd n'› have "valid_node n'"
      by(fastforce intro:path_valid_node(2) DynPDG_path_CFG_path 
                        DynPDG_path_cdep)
    with ‹as = [] ∧ n = n''› ‹n'' -as'→_cd n'›
    have "∃n'' asx asx'. n -asx→_cd n'' ∧ n'' -asx'→_d* n' ∧ as@as' = asx@asx'"
      by(auto intro:DynPDG_path_Nil)
    thus ?thesis by simp
  next
    assume "(∃nx asx asx'. n -asx→_cd nx ∧ nx -asx'→_d* n'' ∧ as = asx@asx') ∨
      (∃nx V asx asx'. n -{V}asx→_dd nx ∧ nx -asx'→_d* n'' ∧ as = asx@asx')"
    thus ?thesis
    proof
      assume "∃nx asx asx'. n -asx→_cd nx ∧ nx -asx'→_d* n'' ∧ as = asx@asx'"
      then obtain nx asx asx' where "n -asx→_cd nx" and "nx -asx'→_d* n''"
        and "as = asx@asx'" by auto
      from ‹n'' -as'→_cd n'› have "n'' -as'→_d* n'" by(rule DynPDG_path_cdep)
      with ‹nx -asx'→_d* n''› have "nx -asx'@as'→_d* n'"
        by(fastforce intro:DynPDG_path_Append)
      with ‹n -asx→_cd nx› ‹as = asx@asx'›
      have "∃n'' asx asx'. n -asx→_cd n'' ∧ n'' -asx'→_d* n' ∧ as@as' = asx@asx'"
        by auto
      thus ?thesis by simp
    next
      assume "∃nx V asx asx'. n -{V}asx→_dd nx ∧ nx -asx'→_d* n'' ∧ as = asx@asx'"
      then obtain nx V asx asx' where "n -{V}asx→_dd nx" and "nx -asx'→_d* n''"
        and "as = asx@asx'" by auto
      from ‹n'' -as'→_cd n'› have "n'' -as'→_d* n'" by(rule DynPDG_path_cdep)
      with ‹nx -asx'→_d* n''› have "nx -asx'@as'→_d* n'"
        by(fastforce intro:DynPDG_path_Append)
      with ‹n -{V}asx→_dd nx› ‹as = asx@asx'›
      have "∃n'' V asx asx'. n -{V}asx→_dd n'' ∧ n'' -asx'→_d* n' ∧ as@as' = asx@asx'"
        by auto
      thus ?thesis by simp
    qed
  qed
next
  case (DynPDG_path_Append_ddep n as n'' V as' n')
  note IH = ‹as = [] ∧ n = n'' ∨
 (∃nx asx asx'. n -asx→_cd nx ∧ nx -asx'→_d* n'' ∧ as = asx@asx') ∨
 (∃nx V asx asx'. n -{V}asx→_dd nx ∧ nx -asx'→_d* n'' ∧ as = asx@asx')›
  from IH show ?case
  proof
    assume "as = [] ∧ n = n''"
    with ‹n'' -{V}as'→_dd n'› have "valid_node n'"
      by(fastforce intro:path_valid_node(2) DynPDG_path_CFG_path 
                        DynPDG_path_ddep)
    with ‹as = [] ∧ n = n''› ‹n'' -{V}as'→_dd n'›
    have "∃n'' V asx asx'. n -{V}asx→_dd n'' ∧ n'' -asx'→_d* n' ∧ as@as' = asx@asx'"
      by(fastforce intro:DynPDG_path_Nil)
    thus ?thesis by simp
  next
    assume "(∃nx asx asx'. n -asx→_cd nx ∧ nx -asx'→_d* n'' ∧ as = asx@asx') ∨
      (∃nx V asx asx'. n -{V}asx→_dd nx ∧ nx -asx'→_d* n'' ∧ as = asx@asx')"
    thus ?thesis
    proof
      assume "∃nx asx asx'. n -asx→_cd nx ∧ nx -asx'→_d* n'' ∧ as = asx@asx'"
      then obtain nx asx asx' where "n -asx→_cd nx" and "nx -asx'→_d* n''"
        and "as = asx@asx'" by auto
      from ‹n'' -{V}as'→_dd n'› have "n'' -as'→_d* n'" by(rule DynPDG_path_ddep)
      with ‹nx -asx'→_d* n''› have "nx -asx'@as'→_d* n'"
        by(fastforce intro:DynPDG_path_Append)
      with ‹n -asx→_cd nx› ‹as = asx@asx'›
      have "∃n'' asx asx'. n -asx→_cd n'' ∧ n'' -asx'→_d* n' ∧ as@as' = asx@asx'"
        by auto
      thus ?thesis by simp
    next
      assume "∃nx V asx asx'. n -{V}asx→_dd nx ∧ nx -asx'→_d* n'' ∧ as = asx@asx'"
      then obtain nx V' asx asx' where "n -{V'}asx→_dd nx" and "nx -asx'→_d* n''"
        and "as = asx@asx'" by auto
      from ‹n'' -{V}as'→_dd n'› have "n'' -as'→_d* n'" by(rule DynPDG_path_ddep)
      with ‹nx -asx'→_d* n''› have "nx -asx'@as'→_d* n'"
        by(fastforce intro:DynPDG_path_Append)
      with ‹n -{V'}asx→_dd nx› ‹as = asx@asx'›
      have "∃n'' V asx asx'. n -{V}asx→_dd n'' ∧ n'' -asx'→_d* n' ∧ as@as' = asx@asx'"
        by auto
      thus ?thesis by simp
    qed
  qed
qed


lemma DynPDG_path_rev_cases [consumes 1,
  case_names DynPDG_path_Nil DynPDG_path_cdep_Append DynPDG_path_ddep_Append]:
  "[n -as→_d* n'; [as = []; n = n'] ==> Q;
    ∧n'' asx asx'. [n -asx→_cd n''; n'' -asx'→_d* n';
                       as = asx@asx'] ==> Q;
    ∧V n'' asx asx'. [n -{V}asx→_dd n''; n'' -asx'→_d* n';
                       as = asx@asx'] ==> Q]
  ==> Q"
by(blast dest:DynPDG_path_split)



lemma DynPDG_ddep_edge_no_shorter_ddep_edge:
  assumes ddep:"n -{V}as→_dd n'"
  shows "∀as' a as''. tl as = as'@a#as'' ⟶ ¬ sourcenode a -{V}a#as''→_dd n'"
proof -
  from ddep have influence:"n influences V in n' via as"
    by(auto elim!:DynPDG_edge.cases)
  then obtain  a asx where as:"as = a#asx"
    and notin:"n ∉ set (sourcenodes asx)"
    by(auto dest:dyn_influence_source_notin_tl_edges simp:dyn_data_dependence_def)
  from influence as
  have imp:"∀nx ∈ set (sourcenodes asx). V ∉ Def nx"
    by(auto simp:dyn_data_dependence_def)
  { fix as' a' as'' 
    assume eq:"tl as = as'@a'#as''"
      and ddep':"sourcenode a' -{V}a'#as''→_dd n'"
    from eq as notin have noteq:"sourcenode a' ≠ n" by(auto simp:sourcenodes_def)
    from ddep' have "V ∈ Def (sourcenode a')"
      by(auto elim!:DynPDG_edge.cases simp:dyn_data_dependence_def)
    with eq as noteq imp have False by(auto simp:sourcenodes_def) }
  thus ?thesis by blast
qed



lemma no_ddep_same_state:
  assumes path:"n -as→* n'" and Uses:"V ∈ Use n'" and preds:"preds (kinds as) s"
  and no_dep:"∀as' a as''. as = as'@a#as'' ⟶ ¬ sourcenode a -{V}a#as''→_dd n'"
  shows "state_val (transfers (kinds as) s) V = state_val s V"
proof -
  { fix n''
    assume inset:"n'' ∈ set (sourcenodes as)" and Defs:"V ∈ Def n''"
    hence "∃nx ∈ set (sourcenodes as). V ∈ Def nx" by auto
    then obtain nx ns' ns'' where nodes:"sourcenodes as = ns'@nx#ns''"
        and Defs':"V ∈ Def nx" and notDef:"∀nx' ∈ set ns''. V ∉ Def nx'"
      by(fastforce elim!:rightmost_element_property)
    from nodes obtain as' a as''
      where as'':"sourcenodes as'' = ns''" and as:"as=as'@a#as''"
      and source:"sourcenode a = nx"
      by(fastforce elim:map_append_append_maps simp:sourcenodes_def)
    from as path have path':"sourcenode a -a#as''→* n'"
      by(fastforce dest:path_split_second)
    from notDef as'' source
    have "∀n'' ∈ set (sourcenodes as''). V ∉ Def n''"
      by(auto simp:sourcenodes_def)
    with path' Defs' Uses source
    have influence:"nx influences V in n' via (a#as'')"
      by(simp add:dyn_data_dependence_def)
    hence "nx ∉ set (sourcenodes as'')" by(rule dyn_influence_source_notin_tl_edges)
    with influence source
    have "∃asx a'. sourcenode a' -{V}a'#asx→_dd n' ∧ sourcenode a' = nx ∧
          (∃asx'. a#as'' = asx'@a'#asx)"
      by(fastforce intro:DynPDG_ddep_edge)
    with nodes no_dep as have False by(auto simp:sourcenodes_def) }
  hence "∀n ∈ set (sourcenodes as). V ∉ Def n" by auto
  with wf path preds show ?thesis by(fastforce intro:CFG_path_no_Def_equal)
qed


lemma DynPDG_ddep_edge_only_first_edge:
  "[n -{V}a#as→_dd n'; preds (kinds (a#as)) s] ==>
    state_val (transfers (kinds (a#as)) s) V = state_val (transfer (kind a) s) V"
  apply -
  apply(erule DynPDG_edge.cases)
  apply auto
  apply(frule dyn_influence_Cons_source)
  apply(frule dyn_influence_source_notin_tl_edges)
  by(erule dyn_influence_only_first_edge)


lemma Use_value_change_implies_DynPDG_ddep_edge:
  assumes "n -as→* n'" and "V ∈ Use n'" and "preds (kinds as) s" 
  and "preds (kinds as) s'" and "state_val s V = state_val s' V"
  and "state_val (transfers (kinds as) s) V ≠
             state_val (transfers (kinds as) s') V"
  obtains as' a as'' where "as = as'@a#as''"
  and "sourcenode a -{V}a#as''→_dd n'"
  and "state_val (transfers (kinds as) s) V =
       state_val (transfers (kinds (as'@[a])) s) V"
  and "state_val (transfers (kinds as) s') V =
       state_val (transfers (kinds (as'@[a])) s') V"
proof(atomize_elim)
  show "∃as' a as''. as = as'@a#as'' ∧
                     sourcenode a -{V}a#as''→_dd n' ∧
             state_val (transfers (kinds as) s) V =
             state_val (transfers (kinds (as'@[a])) s) V ∧
             state_val (transfers (kinds as) s') V =
             state_val (transfers (kinds (as'@[a])) s') V"
  proof(cases "∀as' a as''. as = as'@a#as'' ⟶
                 ¬ sourcenode a -{V}a#as''→_dd n'")
    case True
    with ‹n -as→* n'› ‹V ∈ Use n'› ‹preds (kinds as) s› ‹preds (kinds as) s'›
    have "state_val (transfers (kinds as) s) V = state_val s V"
      and "state_val (transfers (kinds as) s') V = state_val s' V"
      by(auto intro:no_ddep_same_state)
    with ‹state_val s V = state_val s' V›
      ‹state_val (transfers (kinds as) s) V ≠ state_val (transfers (kinds as) s') V›
    show ?thesis by simp
  next
    case False
    then obtain as' a as'' where [simp]:"as = as'@a#as''"
      and "sourcenode a -{V}a#as''→_dd n'" by auto
    from ‹preds (kinds as) s› have "preds (kinds (a#as'')) (transfers (kinds as') s)"
      by(simp add:kinds_def preds_split)
    with ‹sourcenode a -{V}a#as''→_dd n'› have all:
      "state_val (transfers (kinds (a#as'')) (transfers (kinds as') s)) V =
       state_val (transfer (kind a) (transfers (kinds as') s)) V"
      by(auto dest!:DynPDG_ddep_edge_only_first_edge)
    from ‹preds (kinds as) s'›
    have "preds (kinds (a#as'')) (transfers (kinds as') s')"
      by(simp add:kinds_def preds_split)
    with ‹sourcenode a -{V}a#as''→_dd n'› have all':
      "state_val (transfers (kinds (a#as'')) (transfers (kinds as') s')) V =
       state_val (transfer (kind a) (transfers (kinds as') s')) V"
      by(auto dest!:DynPDG_ddep_edge_only_first_edge)
    hence eq:"∧s. transfers (kinds as) s =
      transfers (kinds (a#as'')) (transfers (kinds as') s)"
      by(simp add:transfers_split[THEN sym] kinds_def)
    with all have "state_val (transfers (kinds as) s) V =
                   state_val (transfers (kinds (as'@[a])) s) V"
      by(simp add:transfers_split kinds_def)
    moreover
    from eq all' have "state_val (transfers (kinds as) s') V =
                       state_val (transfers (kinds (as'@[a])) s') V"
      by(simp add:transfers_split kinds_def)
    ultimately show ?thesis using ‹sourcenode a -{V}a#as''→_dd n'› by simp blast
  qed
qed


end


subsection ‹Instantiate dynamic PDG›

subsubsection ‹Standard control dependence›

locale DynStandardControlDependencePDG =
  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 DynPDG_scd:
  "DynPDG sourcenode targetnode kind valid_edge (_Entry_)
          Def Use state_val (_Exit_) dyn_standard_control_dependence"
proof(unfold_locales)
  fix n n' as assume "n controls_s n' via as"
  show "n' ≠ (_Exit_)"
  proof
    assume "n' = (_Exit_)"
    with ‹n controls_s n' via as› show False
      by(fastforce intro:Exit_not_dyn_standard_control_dependent)
  qed
next
  fix n n' as assume "n controls_s n' via as"
  thus "n -as→* n' ∧ as ≠ []"
    by(fastforce simp:dyn_standard_control_dependence_def)
qed


end

subsubsection ‹Weak control dependence›

locale DynWeakControlDependencePDG = 
  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 DynPDG_wcd:
  "DynPDG sourcenode targetnode kind valid_edge (_Entry_)
          Def Use state_val (_Exit_) dyn_weak_control_dependence"
proof(unfold_locales)
  fix n n' as assume "n weakly controls n' via as"
  show "n' ≠ (_Exit_)"
  proof
    assume "n' = (_Exit_)"
    with ‹n weakly controls n' via as› show False
      by(fastforce intro:Exit_not_dyn_weak_control_dependent)
  qed
next
  fix n n' as assume "n weakly controls n' via as"
  thus "n -as→* n' ∧ as ≠ []"
    by(fastforce simp:dyn_weak_control_dependence_def)
qed


end


subsection ‹Data slice›

definition (in CFG) empty_control_dependence :: "'node ==> 'node ==> 'edge list ==> bool"
where "empty_control_dependence n n' as ≡ False"

lemma (in CFGExit_wf) DynPDG_scd:
  "DynPDG sourcenode targetnode kind valid_edge (_Entry_)
          Def Use state_val (_Exit_) empty_control_dependence"
proof(unfold_locales)
  fix n n' as assume "empty_control_dependence n n' as"
  thus "n' ≠ (_Exit_)" by(simp add:empty_control_dependence_def)
next
  fix n n' as assume "empty_control_dependence n n' as"
  thus "n -as→* n' ∧ as ≠ []" by(simp add:empty_control_dependence_def)
qed

end