Theory Slicing.StandardControlDependence
section ‹Static Standard Control Dependence›
theory StandardControlDependence imports
"../Basic/Postdomination"
"../Basic/DynStandardControlDependence"
begin
context Postdomination begin
subsubsection ‹Definition and some lemmas›
definition standard_control_dependence :: "'node ⇒ 'node ⇒ bool"
(‹_ controls⇩s _› [51,0])
where standard_control_dependences_eq:"n controls⇩s n' ≡ ∃as. n controls⇩s n' via as"
lemma standard_control_dependence_def:"n controls⇩s n' =
(∃a a' as. (n' ∉ set(sourcenodes (a#as))) ∧ (n -a#as→* n') ∧
(n' postdominates (targetnode a)) ∧
(valid_edge a') ∧ (sourcenode a' = n) ∧
(¬ n' postdominates (targetnode a')))"
by(auto simp:standard_control_dependences_eq dyn_standard_control_dependence_def)
lemma Exit_not_standard_control_dependent:
"n controls⇩s (_Exit_) ⟹ False"
by(auto simp:standard_control_dependences_eq
intro:Exit_not_dyn_standard_control_dependent)
lemma standard_control_dependence_def_variant:
"n controls⇩s n' = (∃as. (n -as→* n') ∧ (n ≠ n') ∧
(¬ n' postdominates n) ∧ (n' ∉ set(sourcenodes as)) ∧
(∀n'' ∈ set(targetnodes as). n' postdominates n''))"
by(auto simp:standard_control_dependences_eq
dyn_standard_control_dependence_def_variant)
lemma inner_node_standard_control_dependence_predecessor:
assumes "inner_node n" "(_Entry_) -as→* n" "n -as'→* (_Exit_)"
obtains n' where "n' controls⇩s n"
using assms
by(auto elim!:inner_node_dyn_standard_control_dependence_predecessor
simp:standard_control_dependences_eq)
end
end