Theory DynDataDependence

section ‹Dynamic data dependence›

theory DynDataDependence imports CFG_wf begin

context CFG_wf begin 

definition dyn_data_dependence :: 
  "'node ⇒ 'var ⇒ 'node ⇒ 'edge list ⇒ bool" (‹_ influences _ in _ via _› [51,0,0])
where "n influences V in n' via as ≡
    ((V ∈ Def n) ∧ (V ∈ Use n') ∧ (n -as→* n') ∧ 
     (∃a' as'. (as = a'#as') ∧ (∀n'' ∈ set (sourcenodes as'). V ∉ Def n'')))"


lemma dyn_influence_Cons_source:
  "n influences V in n' via a#as ⟹ sourcenode a = n"
  by(simp add:dyn_data_dependence_def,auto elim:path.cases)


lemma dyn_influence_source_notin_tl_edges: 
  assumes "n influences V in n' via a#as"
  shows "n ∉ set (sourcenodes as)"
proof(rule ccontr)
  assume "¬ n ∉ set (sourcenodes as)"
  hence "n ∈ set (sourcenodes as)" by simp
  from ‹n influences V in n' via a#as› have "∀n'' ∈ set (sourcenodes as). V ∉ Def n''"
    and "V ∈ Def n" by(simp_all add:dyn_data_dependence_def)
  from ‹∀n'' ∈ set (sourcenodes as). V ∉ Def n''› 
    ‹n ∈ set (sourcenodes as)› have "V ∉ Def n" by simp
  with ‹V ∈ Def n› show False by simp
qed


lemma dyn_influence_only_first_edge:
  assumes "n influences V in n' via a#as" and "preds (kinds (a#as)) s"
  shows "state_val (transfers (kinds (a#as)) s) V = 
         state_val (transfer (kind a) s) V"
proof -
  from ‹preds (kinds (a#as)) s› have "preds (kinds as) (transfer (kind a) s)"
    by(simp add:kinds_def)
  from ‹n influences V in n' via a#as› have "n -a#as→* n'"
    and "∀n'' ∈ set (sourcenodes as). V ∉ Def n''"
    by(simp_all add:dyn_data_dependence_def)
  from ‹n -a#as→* n'› have "n = sourcenode a" and "targetnode a -as→* n'"
    by(auto elim:path_split_Cons)
  from ‹n influences V in n' via a#as› ‹n = sourcenode a› 
  have "sourcenode a ∉ set (sourcenodes as)"
    by(fastforce intro!:dyn_influence_source_notin_tl_edges)
  { fix n'' assume "n'' ∈ set (sourcenodes as)"
    with ‹sourcenode a ∉ set (sourcenodes as)› ‹n = sourcenode a› 
    have "n'' ≠ n" by(fastforce simp:sourcenodes_def)
    with ‹∀n'' ∈ set (sourcenodes as). V ∉ Def n''› ‹n'' ∈ set (sourcenodes as)›
    have "V ∉ Def n''" by(auto simp:sourcenodes_def) }
  hence "∀n'' ∈ set (sourcenodes as). V ∉ Def n''" by simp
  with ‹targetnode a -as→* n'› ‹preds (kinds as) (transfer (kind a) s)›
  have "state_val (transfers (kinds as) (transfer (kind a) s)) V = 
        state_val (transfer (kind a) s) V"
    by -(rule CFG_path_no_Def_equal)
  thus ?thesis by(auto simp:kinds_def)
qed

end

end