Theory Slicing.DynStandardControlDependence
section ‹Dynamic Standard Control Dependence›
theory DynStandardControlDependence imports Postdomination begin
context Postdomination begin
definition
dyn_standard_control_dependence :: "'node ⇒ 'node ⇒ 'edge list ⇒ bool"
(‹_ controls⇩s _ via _› [51,0,0])
where dyn_standard_control_dependence_def:"n controls⇩s n' via as ≡
(∃a a' as'. (as = a#as') ∧ (n' ∉ set(sourcenodes as)) ∧ (n -as→* n') ∧
(n' postdominates (targetnode a)) ∧
(valid_edge a') ∧ (sourcenode a' = n) ∧
(¬ n' postdominates (targetnode a')))"
lemma Exit_not_dyn_standard_control_dependent:
assumes control:"n controls⇩s (_Exit_) via as" shows "False"
proof -
from control obtain a as' where path:"n -as→* (_Exit_)" and as:"as = a#as'"
and pd:"(_Exit_) postdominates (targetnode a)"
by(auto simp:dyn_standard_control_dependence_def)
from path as have "n -[]@a#as'→* (_Exit_)" by simp
hence "valid_edge a" by(fastforce dest:path_split)
with pd show False by -(rule Exit_no_postdominator,auto)
qed
lemma dyn_standard_control_dependence_def_variant:
"n controls⇩s n' via as = ((n -as→* n') ∧ (n ≠ n') ∧
(¬ n' postdominates n) ∧ (n' ∉ set(sourcenodes as)) ∧
(∀n'' ∈ set(targetnodes as). n' postdominates n''))"
proof
assume "(n -as→* n') ∧ (n ≠ n') ∧ (¬ n' postdominates n) ∧
(n' ∉ set(sourcenodes as)) ∧
(∀n''∈set (targetnodes as). n' postdominates n'')"
hence path:"n -as→* n'" and noteq:"n ≠ n'"
and not_pd:"¬ n' postdominates n"
and notin:"n' ∉ set(sourcenodes as)"
and all:"∀n''∈set (targetnodes as). n' postdominates n''"
by auto
have notExit:"n ≠ (_Exit_)"
proof
assume "n = (_Exit_)"
with path have "n = n'" by(fastforce dest:path_Exit_source)
with noteq show False by simp
qed
from path have valid:"valid_node n" and valid':"valid_node n'"
by(auto dest:path_valid_node)
show "n controls⇩s n' via as"
proof(cases as)
case Nil
with path valid not_pd notExit have False
by(fastforce elim:path.cases dest:postdominate_refl)
thus ?thesis by simp
next
case (Cons ax asx)
with all have pd:"n' postdominates targetnode ax"
by(auto simp:targetnodes_def)
from path Cons have source:"n = sourcenode ax"
and path2:"targetnode ax -asx→* n'"
by(auto intro:path_split_Cons)
show ?thesis
proof(cases "∃as'. n -as'→* (_Exit_)")
case True
with not_pd valid valid' obtain as' where path':"n -as'→* (_Exit_)"
and not_isin:"n' ∉ set (sourcenodes as')"
by(auto simp:postdominate_def)
have "as' ≠ []"
proof
assume "as' = []"
with path' have "n = (_Exit_)" by(auto elim:path.cases)
with notExit show False by simp
qed
then obtain a' as'' where as':"as' = a'#as''"
by(cases as',auto elim:path.cases)
with path' have "n -[]@a'#as''→* (_Exit_)" by simp
hence source':"n = sourcenode a'"
and valid_edge:"valid_edge a'"
and path2':"targetnode a' -as''→* (_Exit_)"
by(fastforce dest:path_split)+
from path2' not_isin as' valid'
have "¬ n' postdominates (targetnode a')"
by(auto simp:postdominate_def sourcenodes_def)
with pd path Cons source source' notin valid_edge show ?thesis
by(auto simp:dyn_standard_control_dependence_def)
next
case False
with valid valid' have "n' postdominates n"
by(auto simp:postdominate_def)
with not_pd have False by simp
thus ?thesis by simp
qed
qed
next
assume "n controls⇩s n' via as"
then obtain a nx a' nx' as' where notin:"n' ∉ set(sourcenodes as)"
and path:"n -as→* n'" and as:"as = a#as'" and valid_edge:"valid_edge a'"
and pd:"n' postdominates (targetnode a)"
and source':"sourcenode a' = n"
and not_pd:"¬ n' postdominates (targetnode a')"
by(auto simp:dyn_standard_control_dependence_def)
from path as have source:"sourcenode a = n" by(auto elim:path.cases)
from path as have notExit:"n ≠ (_Exit_)" by(auto elim:path.cases)
from path have valid:"valid_node n" and valid':"valid_node n'"
by(auto dest:path_valid_node)
from notin as source have noteq:"n ≠ n'"
by(fastforce simp:sourcenodes_def)
from valid_edge have valid_target':"valid_node (targetnode a')"
by(fastforce simp:valid_node_def)
{ assume pd':"n' postdominates n"
hence all:"∀as. n -as→* (_Exit_) ⟶ n' ∈ set (sourcenodes as)"
by(auto simp:postdominate_def)
from not_pd valid' valid_target' obtain as'
where "targetnode a' -as'→* (_Exit_)"
by(auto simp:postdominate_def)
with source' valid_edge have path':"n -a'#as'→* (_Exit_)"
by(fastforce intro:Cons_path)
with all have "n' ∈ set (sourcenodes (a'#as'))" by blast
with source' have "n' = n ∨ n' ∈ set (sourcenodes as')"
by(fastforce simp:sourcenodes_def)
hence False
proof
assume "n' = n"
with noteq show ?thesis by simp
next
assume isin:"n' ∈ set (sourcenodes as')"
from path' have path2:"targetnode a' -as'→* (_Exit_)"
by(fastforce elim:path_split_Cons)
thus ?thesis
proof(cases "as' = []")
case True
with path2 have "targetnode a' = (_Exit_)" by(auto elim:path.cases)
with valid_edge all source' have "n' = n"
by(fastforce dest:path_edge simp:sourcenodes_def)
with noteq show ?thesis by simp
next
case False
from path2 not_pd valid' valid_edge obtain as''
where path'':"targetnode a' -as''→* (_Exit_)"
and notin:"n' ∉ set (sourcenodes as'')"
by(auto simp:postdominate_def)
from valid_edge path'' have "sourcenode a' -a'#as''→* (_Exit_)"
by(fastforce intro:Cons_path)
with all source' have "n' ∈ set (sourcenodes ([a']@as''))" by simp
with source' have "n' = n ∨ n' ∈ set (sourcenodes as'')"
by(auto simp:sourcenodes_def)
thus ?thesis
proof
assume "n' = n"
with noteq show ?thesis by simp
next
assume "n' ∈ set (sourcenodes as'')"
with notin show ?thesis by simp
qed
qed
qed }
hence not_pd':"¬ n' postdominates n" by blast
{ fix n'' assume "n'' ∈ set (targetnodes as)"
with as source have "n'' = targetnode a ∨ n'' ∈ set (targetnodes as')"
by(auto simp:targetnodes_def)
hence "n' postdominates n''"
proof
assume "n'' = targetnode a"
with pd show ?thesis by simp
next
assume isin:"n'' ∈ set (targetnodes as')"
hence "∃ni ∈ set (targetnodes as'). ni = n''" by simp
then obtain ns ns' where targets:"targetnodes as' = ns@n''#ns'"
and all_noteq:"∀ni ∈ set ns'. ni ≠ n''"
by(fastforce elim!:rightmost_element_property)
from targets obtain xs ax ys where ys:"ns' = targetnodes ys"
and as':"as' = xs@ax#ys" and target'':"targetnode ax = n''"
by(fastforce elim:map_append_append_maps simp:targetnodes_def)
from all_noteq ys have notin_target:"n'' ∉ set(targetnodes ys)"
by auto
from path as have "n -[]@a#as'→* n'" by simp
hence "targetnode a -as'→* n'"
by(fastforce dest:path_split)
with isin have path':"targetnode a -as'→* n'"
by(fastforce split:if_split_asm simp:targetnodes_def)
with as' target'' have path1:"targetnode a -xs→* sourcenode ax"
and valid_edge':"valid_edge ax"
and path2:"n'' -ys→* n'"
by(auto intro:path_split)
from valid_edge' have "sourcenode ax -[ax]→* targetnode ax" by(rule path_edge)
with path1 target'' have path_n'':"targetnode a -xs@[ax]→* n''"
by(fastforce intro:path_Append)
from notin as as' have notin':"n'∉ set (sourcenodes (xs@[ax]))"
by(simp add:sourcenodes_def)
show ?thesis
proof(rule ccontr)
assume "¬ n' postdominates n''"
with valid' target'' valid_edge' obtain asx'
where Exit_path:"n'' -asx'→* (_Exit_)"
and notin'':"n' ∉ set(sourcenodes asx')" by(auto simp:postdominate_def)
from path_n'' Exit_path
have Exit_path':"targetnode a -(xs@[ax])@asx'→* (_Exit_)"
by(fastforce intro:path_Append)
from notin' notin'' have "n' ∉ set(sourcenodes (xs@ax#asx'))"
by(simp add:sourcenodes_def)
with pd Exit_path' show False by(simp add:postdominate_def)
qed
qed }
with path not_pd' notin noteq show "(n -as→* n') ∧ (n ≠ n') ∧
(¬ n' postdominates n) ∧ (n' ∉ set(sourcenodes as)) ∧
(∀n'' ∈ set(targetnodes as). n' postdominates n'')" by blast
qed
lemma which_node_dyn_standard_control_dependence_source:
assumes path:"(_Entry_) -as@a#as'→* n"
and Exit_path:"n -as''→* (_Exit_)" and source:"sourcenode a = n'"
and source':"sourcenode a' = n'"
and no_source:"n ∉ set(sourcenodes (a#as'))" and valid_edge':"valid_edge a'"
and inner_node:"inner_node n" and not_pd:"¬ n postdominates (targetnode a')"
and last:"∀ax ax'. ax ∈ set as' ∧ sourcenode ax = sourcenode ax' ∧
valid_edge ax' ⟶ n postdominates targetnode ax'"
shows "n' controls⇩s n via a#as'"
proof -
from path source have path_n'n:"n' -a#as'→* n" by(fastforce dest:path_split_second)
from path have valid_edge:"valid_edge a" by(fastforce intro:path_split)
show ?thesis
proof(cases "n postdominates (targetnode a)")
case True
with path_n'n not_pd no_source source source' valid_edge' show ?thesis
by(auto simp:dyn_standard_control_dependence_def)
next
case False
hence not_pd':"¬ n postdominates (targetnode a)" .
show ?thesis
proof(cases "as' = []")
case True
with path_n'n have "targetnode a = n" by(fastforce elim:path.cases)
with inner_node have "n postdominates (targetnode a)"
by(cases "n = (_Exit_)",auto intro:postdominate_refl simp:inner_node_def)
with not_pd path_n'n no_source source source' valid_edge' show ?thesis
by(fastforce simp:dyn_standard_control_dependence_def)
next
case False
hence notempty':"as' ≠ []" .
with path have path_nxn:"targetnode a -as'→* n"
by(fastforce dest:path_split)
from Exit_path path_nxn have "∃as. targetnode a -as→* (_Exit_)"
by(fastforce dest:path_Append)
with not_pd' inner_node valid_edge obtain asx
where path_Exit:"targetnode a -asx→* (_Exit_)"
and notin:"n ∉ set (sourcenodes asx)"
by(auto simp:postdominate_def inner_is_valid)
show ?thesis
proof(cases "∃asx'. asx = as'@asx'")
case True
then obtain asx' where asx:"asx = as'@asx'" by blast
from path notempty' have "targetnode a -as'→* n"
by(fastforce dest:path_split)
with path_Exit inner_node asx notempty'
obtain a'' as'' where "asx' = a''#as'' ∧ sourcenode a'' = n"
apply(cases asx')
apply(fastforce dest:path_det)
by(fastforce dest:path_split path_det)
with asx have "n ∈ set(sourcenodes asx)" by(simp add:sourcenodes_def)
with notin have False by simp
thus ?thesis by simp
next
case False
hence all:"∀asx'. asx ≠ as'@asx'" by simp
then obtain j asx' where asx:"asx = (take j as')@asx'"
and length:"j < length as'"
and not_more:"∀k > j. ∀asx''. asx ≠ (take k as')@asx''"
by(auto elim:path_split_general)
from asx length have "∃as'1 as'2. asx = as'1@asx' ∧
as' = as'1@as'2 ∧ as'2 ≠ [] ∧ as'1 = take j as'"
by simp(rule_tac x= "drop j as'" in exI,simp)
then obtain as'1 as'' where asx:"asx = as'1@asx'"
and take:"as'1 = take j as'"
and x:"as' = as'1@as''" and x':"as'' ≠ []" by blast
from x x' obtain a1 as'2 where as':"as' = as'1@a1#as'2" and "as'' = a1#as'2"
by(cases as'') auto
have notempty_x':"asx' ≠ []"
proof(cases "asx' = []")
case True
with asx as' have "as' = asx@a1#as'2" by simp
with path_n'n have "n' -(a#asx)@a1#as'2→* n"
by simp
hence "n' -a#asx→* sourcenode a1"
and valid_edge1:"valid_edge a1" by(fastforce elim:path_split)+
hence "targetnode a -asx→* sourcenode a1"
by(fastforce intro:path_split_Cons)
with path_Exit have "(_Exit_) = sourcenode a1" by(rule path_det)
from this[THEN sym] valid_edge1 have False by -(rule Exit_source,simp_all)
thus ?thesis by simp
qed simp
with asx obtain a2 asx'1
where asx:"asx = as'1@a2#asx'1"
and asx':"asx' = a2#asx'1" by(cases asx') auto
from path_n'n as' have "n' -(a#as'1)@a1#as'2→* n" by simp
hence "n' -a#as'1→* sourcenode a1" and valid_edge1:"valid_edge a1"
by(fastforce elim:path_split)+
hence path1:"targetnode a -as'1→* sourcenode a1"
by(fastforce intro:path_split_Cons)
from path_Exit asx
have "targetnode a -as'1→* sourcenode a2"
and valid_edge2:"valid_edge a2"
and path2:"targetnode a2 -asx'1→* (_Exit_)"
by(auto intro:path_split)
with path1 have eq12:"sourcenode a1 = sourcenode a2"
by(cases as'1,auto dest:path_det)
from asx notin have "n ∉ set (sourcenodes asx'1)"
by(simp add:sourcenodes_def)
with path2 have not_pd'2:"¬ n postdominates targetnode a2"
by(cases "asx'1 = []",auto simp:postdominate_def)
from as' have "a1 ∈ set as'" by simp
with eq12 last valid_edge2 have "n postdominates targetnode a2" by blast
with not_pd'2 have False by simp
thus ?thesis by simp
qed
qed
qed
qed
lemma inner_node_dyn_standard_control_dependence_predecessor:
assumes inner_node:"inner_node n"
obtains n' as where "n' controls⇩s n via as"
proof(atomize_elim)
from inner_node obtain as' where pathExit:"n -as'→* (_Exit_)"
by(fastforce dest:inner_is_valid Exit_path)
from inner_node obtain as where pathEntry:"(_Entry_) -as→* n"
by(fastforce dest:inner_is_valid Entry_path)
with inner_node have notEmpty:"as ≠ []"
by(auto elim:path.cases simp:inner_node_def)
have "∃a asx. (_Entry_) -a#asx→* n ∧ n ∉ set (sourcenodes (a#asx))"
proof(cases "n ∈ set (sourcenodes as)")
case True
hence "∃n'' ∈ set(sourcenodes as). n = n''" by simp
then obtain ns' ns'' where nodes:"sourcenodes as = ns'@n#ns''"
and notin:"∀n'' ∈ set ns'. n ≠ n''"
by(fastforce elim!:split_list_first_propE)
from nodes obtain xs ys a'
where xs:"sourcenodes xs = ns'" and as:"as = xs@a'#ys"
and source:"sourcenode a' = n"
by(fastforce elim:map_append_append_maps simp:sourcenodes_def)
from pathEntry as have "(_Entry_) -xs@a'#ys→* n" by simp
hence path2:"(_Entry_) -xs→* sourcenode a'"
by(fastforce dest:path_split)
show ?thesis
proof(cases "xs = []")
case True
with path2 have "(_Entry_) = sourcenode a'" by(auto elim:path.cases)
with pathEntry source notEmpty have "(_Entry_) -as→* (_Entry_) ∧ as ≠ []"
by(auto elim:path.cases)
hence False by(fastforce dest:path_Entry_target)
thus ?thesis by simp
next
case False
then obtain n a'' xs' where "xs = a''#xs'" by(cases xs) auto
with False path2 notin xs source show ?thesis by simp blast
qed
next
case False
from notEmpty obtain a as' where "as = a#as'" by (cases as) auto
with False pathEntry show ?thesis by auto
qed
then obtain a asx where pathEntry':"(_Entry_) -a#asx→* n"
and notin:"n ∉ set (sourcenodes (a#asx))" by blast
show "∃n' as. n' controls⇩s n via as"
proof(cases "∀a' a''. a' ∈ set asx ∧ sourcenode a' = sourcenode a'' ∧
valid_edge a'' ⟶ n postdominates targetnode a''")
case True
from inner_node have not_pd:"¬ n postdominates (_Exit_)"
by(fastforce intro:empty_path simp:postdominate_def sourcenodes_def)
from pathEntry' have path':"(_Entry_) -[]@a#asx→* n" by simp
hence eq:"sourcenode a = (_Entry_)"
by(fastforce dest:path_split elim:path.cases)
from Entry_Exit_edge obtain a' where "sourcenode a' = (_Entry_)"
and "targetnode a' = (_Exit_)" and "valid_edge a'" by auto
with path' inner_node not_pd True eq notin pathExit
have "sourcenode a controls⇩s n via a#asx"
by -(erule which_node_dyn_standard_control_dependence_source,auto)
thus ?thesis by blast
next
case False
hence "∃a' ∈ set asx. ∃a''. sourcenode a' = sourcenode a'' ∧ valid_edge a'' ∧
¬ n postdominates targetnode a''"
by fastforce
then obtain ax asx' asx'' where "asx = asx'@ax#asx'' ∧
(∃a''. sourcenode ax = sourcenode a'' ∧ valid_edge a'' ∧
¬ n postdominates targetnode a'') ∧
(∀z ∈ set asx''. ¬ (∃a''. sourcenode z = sourcenode a'' ∧ valid_edge a'' ∧
¬ n postdominates targetnode a''))"
by(blast elim!:rightmost_element_property)
then obtain a'' where as':"asx = asx'@ax#asx''"
and eq:"sourcenode ax = sourcenode a''"
and valid_edge:"valid_edge a''"
and not_pd:"¬ n postdominates targetnode a''"
and last:"∀z ∈ set asx''. ¬ (∃a''. sourcenode z = sourcenode a'' ∧
valid_edge a'' ∧ ¬ n postdominates targetnode a'')"
by blast
from notin as' have notin':"n ∉ set (sourcenodes (ax#asx''))"
by(auto simp:sourcenodes_def)
from as' pathEntry' have "(_Entry_) -(a#asx')@ax#asx''→* n" by simp
with inner_node not_pd notin' eq last pathExit valid_edge
have "sourcenode ax controls⇩s n via ax#asx''"
by(fastforce elim!:which_node_dyn_standard_control_dependence_source)
thus ?thesis by blast
qed
qed
end
end