Theory Slicing.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