Theory DynSlice
section ‹Dynamic Backward Slice›
theory DynSlice imports DependentLiveVariables BitVector "../Basic/SemanticsCFG" begin
subsection ‹Backward slice of paths›
context DynPDG begin
fun slice_path :: "'edge list ⇒ bit_vector"
where "slice_path [] = []"
| "slice_path (a#as) = (let n' = last(targetnodes (a#as)) in
(sourcenode a -a#as→⇩d* n')#slice_path as)"
declare Let_def [simp]
lemma slice_path_length:
"length(slice_path as) = length as"
by(induct as) auto
lemma slice_path_right_Cons:
assumes slice:"slice_path as = x#xs"
obtains a' as' where "as = a'#as'" and "slice_path as' = xs"
proof(atomize_elim)
from slice show "∃a' as'. as = a'#as' ∧ slice_path as' = xs"
by(induct as) auto
qed
subsection ‹The proof of the fundamental property of (dynamic) slicing›
fun select_edge_kinds :: "'edge list ⇒ bit_vector ⇒ 'state edge_kind list"
where "select_edge_kinds [] [] = []"
| "select_edge_kinds (a#as) (b#bs) = (if b then kind a
else (case kind a of ⇑f ⇒ ⇑id | (Q)⇩√ ⇒ (λs. True)⇩√))#select_edge_kinds as bs"
definition slice_kinds :: "'edge list ⇒ 'state edge_kind list"
where "slice_kinds as = select_edge_kinds as (slice_path as)"
lemma select_edge_kinds_max_bv:
"select_edge_kinds as (replicate (length as) True) = kinds as"
by(induct as,auto simp:kinds_def)
lemma slice_path_leqs_information_same_Uses:
"⟦n -as→* n'; bs ≼⇩b bs'; slice_path as = bs;
select_edge_kinds as bs = es; select_edge_kinds as bs' = es';
∀V xs. (V,xs,as) ∈ dependent_live_vars n' ⟶ state_val s V = state_val s' V;
preds es' s'⟧
⟹ (∀V ∈ Use n'. state_val (transfers es s) V =
state_val (transfers es' s') V) ∧ preds es s"
proof(induct bs bs' arbitrary:as es es' n s s' rule:bv_leqs.induct)
case 1
from ‹slice_path as = []› have "as = []" by(cases as) auto
with ‹select_edge_kinds as [] = es› ‹select_edge_kinds as [] = es'›
have "es = []" and "es' = []" by simp_all
{ fix V assume "V ∈ Use n'"
hence "(V,[],[]) ∈ dependent_live_vars n'" by(rule dep_vars_Use)
with ‹∀V xs. (V,xs,as) ∈ dependent_live_vars n' ⟶
state_val s V = state_val s' V› ‹V ∈ Use n'› ‹as = []›
have "state_val s V = state_val s' V" by blast }
with ‹es = []› ‹es' = []› show ?case by simp
next
case (2 x xs y ys)
note all = ‹∀V xs. (V,xs,as) ∈ dependent_live_vars n' ⟶
state_val s V = state_val s' V›
note IH = ‹⋀as es es' n s s'. ⟦n -as→* n'; xs ≼⇩b ys; slice_path as = xs;
select_edge_kinds as xs = es; select_edge_kinds as ys = es';
∀V xs. (V,xs,as) ∈ dependent_live_vars n' ⟶
state_val s V = state_val s' V;
preds es' s'⟧
⟹ (∀V ∈ Use n'. state_val (transfers es s) V =
state_val (transfers es' s') V) ∧ preds es s›
from ‹x#xs ≼⇩b y#ys› have "x ⟶ y" and "xs ≼⇩b ys" by simp_all
from ‹slice_path as = x#xs› obtain a' as' where "as = a'#as'"
and "slice_path as' = xs" by(erule slice_path_right_Cons)
from ‹as = a'#as'› ‹select_edge_kinds as (x#xs) = es›
obtain ex esx where "es = ex#esx"
and ex:"ex = (if x then kind a'
else (case kind a' of ⇑f ⇒ ⇑id | (Q)⇩√ ⇒ (λs. True)⇩√))"
and "select_edge_kinds as' xs = esx" by auto
from ‹as = a'#as'› ‹select_edge_kinds as (y#ys) = es'› obtain ex' esx'
where "es' = ex'#esx'"
and ex':"ex' = (if y then kind a'
else (case kind a' of ⇑f ⇒ ⇑id | (Q)⇩√ ⇒ (λs. True)⇩√))"
and "select_edge_kinds as' ys = esx'" by auto
from ‹n -as→* n'› ‹as = a'#as'› have [simp]:"n = sourcenode a'"
and "valid_edge a'" and "targetnode a' -as'→* n'"
by(auto elim:path_split_Cons)
from ‹n -as→* n'› ‹as = a'#as'› have "last(targetnodes as) = n'"
by(fastforce intro:path_targetnode)
from ‹preds es' s'› ‹es' = ex'#esx'› have "pred ex' s'"
and "preds esx' (transfer ex' s')" by simp_all
show ?case
proof(cases "as' = []")
case True
hence [simp]:"as' = []" by simp
with ‹slice_path as' = xs› ‹xs ≼⇩b ys›
have [simp]:"xs = [] ∧ ys = []" by auto(cases ys,auto)+
with ‹select_edge_kinds as' xs = esx› ‹select_edge_kinds as' ys = esx'›
have [simp]:"esx = []" and [simp]:"esx' = []" by simp_all
from True ‹targetnode a' -as'→* n'›
have [simp]:"n' = targetnode a'" by(auto elim:path.cases)
show ?thesis
proof(cases x)
case True
with ‹x ⟶ y› ex ex' have [simp]:"ex = kind a' ∧ ex' = kind a'" by simp
have "pred ex s"
proof(cases ex)
case (Predicate Q)
with ex ex' True ‹x ⟶ y› have [simp]:"transfer ex s = s"
and [simp]:"transfer ex' s' = s'"
by(cases "kind a'",auto)+
show ?thesis
proof(cases "n -[a']→⇩c⇩d n'")
case True
{ fix V' assume "V' ∈ Use n"
with True ‹valid_edge a'›
have "(V',[],a'#[]@[]) ∈ dependent_live_vars n'"
by(fastforce intro:dep_vars_Cons_cdep DynPDG_path_Nil
simp:targetnodes_def)
with all ‹as = a'#as'› have "state_val s V' = state_val s' V'"
by fastforce }
with ‹pred ex' s'› ‹valid_edge a'›
show ?thesis by(fastforce elim:CFG_edge_Uses_pred_equal)
next
case False
from ex True Predicate have "kind a' = (Q)⇩√" by(auto split:if_split_asm)
from True ‹slice_path as = x#xs› ‹as = a'#as'› have "n -[a']→⇩d* n'"
by(auto simp:targetnodes_def)
thus ?thesis
proof(induct rule:DynPDG_path.cases)
case (DynPDG_path_Nil nx)
hence False by simp
thus ?case by simp
next
case (DynPDG_path_Append_cdep nx asx n'' asx' nx')
from ‹[a'] = asx@asx'›
have "(asx = [a'] ∧ asx' = []) ∨ (asx = [] ∧ asx' = [a'])"
by (cases asx) auto
hence False
proof
assume "asx = [a'] ∧ asx' = []"
with ‹n'' -asx'→⇩c⇩d nx'› show False
by(fastforce elim:DynPDG_edge.cases dest:dyn_control_dependence_path)
next
assume "asx = [] ∧ asx' = [a']"
with ‹nx -asx→⇩d* n''› have "nx = n''" and "asx' = [a']"
by(auto intro:DynPDG_empty_path_eq_nodes)
with ‹n = nx› ‹n' = nx'› ‹n'' -asx'→⇩c⇩d nx'› False
show False by simp
qed
thus ?thesis by simp
next
case (DynPDG_path_Append_ddep nx asx n'' V asx' nx')
from ‹[a'] = asx@asx'›
have "(asx = [a'] ∧ asx' = []) ∨ (asx = [] ∧ asx' = [a'])"
by (cases asx) auto
thus ?case
proof
assume "asx = [a'] ∧ asx' = []"
with ‹n'' -{V}asx'→⇩d⇩d nx'› have False
by(fastforce elim:DynPDG_edge.cases simp:dyn_data_dependence_def)
thus ?thesis by simp
next
assume "asx = [] ∧ asx' = [a']"
with ‹nx -asx→⇩d* n''› have "nx = n''"
by(simp add:DynPDG_empty_path_eq_nodes)
{ fix V' assume "V' ∈ Use n"
from ‹n'' -{V}asx'→⇩d⇩d nx'› ‹asx = [] ∧ asx' = [a']› ‹n' = nx'›
have "(V,[],[]) ∈ dependent_live_vars n'"
by(fastforce intro:dep_vars_Use elim:DynPDG_edge.cases
simp:dyn_data_dependence_def)
with ‹V' ∈ Use n› ‹n'' -{V}asx'→⇩d⇩d nx'› ‹asx = [] ∧ asx' = [a']›
‹n = nx› ‹nx = n''› ‹n' = nx'›
have "(V',[],[a']) ∈ dependent_live_vars n'"
by(auto elim:dep_vars_Cons_ddep simp:targetnodes_def)
with all ‹as = a'#as'› have "state_val s V' = state_val s' V'"
by fastforce }
with ‹pred ex' s'› ‹valid_edge a'› ex ex' True ‹x ⟶ y› show ?thesis
by(fastforce elim:CFG_edge_Uses_pred_equal)
qed
qed
qed
qed simp
{ fix V assume "V ∈ Use n'"
from ‹V ∈ Use n'› have "(V,[],[]) ∈ dependent_live_vars n'"
by(rule dep_vars_Use)
have "state_val (transfer ex s) V = state_val (transfer ex' s') V"
proof(cases "n -{V}[a']→⇩d⇩d n'")
case True
hence "V ∈ Def n"
by(auto elim:DynPDG_edge.cases simp:dyn_data_dependence_def)
have "⋀V. V ∈ Use n ⟹ state_val s V = state_val s' V"
proof -
fix V' assume "V' ∈ Use n"
with ‹(V,[],[]) ∈ dependent_live_vars n'› True
have "(V',[],[a']) ∈ dependent_live_vars n'"
by(fastforce intro:dep_vars_Cons_ddep simp:targetnodes_def)
with all ‹as = a'#as'› show "state_val s V' = state_val s' V'" by auto
qed
with ‹valid_edge a'› ‹pred ex' s'› ‹pred ex s›
have "∀V ∈ Def n. state_val (transfer (kind a') s) V =
state_val (transfer (kind a') s') V"
by simp(rule CFG_edge_transfer_uses_only_Use,auto)
with ‹V ∈ Def n› have "state_val (transfer (kind a') s) V =
state_val (transfer (kind a') s') V"
by simp
thus ?thesis by fastforce
next
case False
with ‹last(targetnodes as) = n'› ‹as = a'#as'›
‹(V,[],[]) ∈ dependent_live_vars n'›
have "(V,[a'],[a']) ∈ dependent_live_vars n'"
by(fastforce intro:dep_vars_Cons_keep)
from ‹(V,[a'],[a']) ∈ dependent_live_vars n'› all ‹as = a'#as'›
have states_eq:"state_val s V = state_val s' V"
by auto
from ‹valid_edge a'› ‹V ∈ Use n'› False ‹pred ex s›
have "state_val (transfers (kinds [a']) s) V = state_val s V"
apply(auto intro!:no_ddep_same_state path_edge simp:targetnodes_def)
apply(simp add:kinds_def)
by(case_tac as',auto)
moreover
from ‹valid_edge a'› ‹V ∈ Use n'› False ‹pred ex' s'›
have "state_val (transfers (kinds [a']) s') V = state_val s' V"
apply(auto intro!:no_ddep_same_state path_edge simp:targetnodes_def)
apply(simp add:kinds_def)
by(case_tac as',auto)
ultimately show ?thesis using states_eq by(auto simp:kinds_def)
qed }
hence "∀V ∈ Use n'. state_val (transfer ex s) V =
state_val (transfer ex' s') V" by simp
with ‹pred ex s› ‹es = ex#esx› ‹es' = ex'#esx'› show ?thesis by simp
next
case False
with ex have cases_x:"ex = (case kind a' of ⇑f ⇒ ⇑id | (Q)⇩√ ⇒ (λs. True)⇩√)"
by simp
from cases_x have "pred ex s" by(cases "kind a'",auto)
show ?thesis
proof(cases y)
case True
with ex' have [simp]:"ex' = kind a'" by simp
{ fix V assume "V ∈ Use n'"
from ‹V ∈ Use n'› have "(V,[],[]) ∈ dependent_live_vars n'"
by(rule dep_vars_Use)
from ‹slice_path as = x#xs› ‹as = a'#as'› ‹¬ x›
have "¬ n -[a']→⇩d* n'" by(simp add:targetnodes_def)
hence "¬ n -{V}[a']→⇩d⇩d n'" by(fastforce dest:DynPDG_path_ddep)
with ‹last(targetnodes as) = n'› ‹as = a'#as'›
‹(V,[],[]) ∈ dependent_live_vars n'›
have "(V,[a'],[a']) ∈ dependent_live_vars n'"
by(fastforce intro:dep_vars_Cons_keep)
with all ‹as = a'#as'› have "state_val s V = state_val s' V" by auto
from ‹valid_edge a'› ‹V ∈ Use n'› ‹pred ex' s'›
‹¬ n -{V}[a']→⇩d⇩d n'› ‹last(targetnodes as) = n'› ‹as = a'#as'›
have "state_val (transfers (kinds [a']) s') V = state_val s' V"
apply(auto intro!:no_ddep_same_state path_edge)
apply(simp add:kinds_def)
by(case_tac as',auto)
with ‹state_val s V = state_val s' V› cases_x
have "state_val (transfer ex s) V =
state_val (transfer ex' s') V"
by(cases "kind a'",simp_all add:kinds_def) }
hence "∀V ∈ Use n'. state_val (transfer ex s) V =
state_val (transfer ex' s') V" by simp
with ‹as = a'#as'› ‹es = ex#esx› ‹es' = ex'#esx'› ‹pred ex s›
show ?thesis by simp
next
case False
with ex' have cases_y:"ex' = (case kind a' of ⇑f ⇒ ⇑id | (Q)⇩√ ⇒ (λs. True)⇩√)"
by simp
with cases_x have [simp]:"ex = ex'" by(cases "kind a'") auto
{ fix V assume "V ∈ Use n'"
from ‹V ∈ Use n'› have "(V,[],[]) ∈ dependent_live_vars n'"
by(rule dep_vars_Use)
from ‹slice_path as = x#xs› ‹as = a'#as'› ‹¬ x›
have "¬ n -[a']→⇩d* n'" by(simp add:targetnodes_def)
hence no_dep:"¬ n -{V}[a']→⇩d⇩d n'" by(fastforce dest:DynPDG_path_ddep)
with ‹last(targetnodes as) = n'› ‹as = a'#as'›
‹(V,[],[]) ∈ dependent_live_vars n'›
have "(V,[a'],[a']) ∈ dependent_live_vars n'"
by(fastforce intro:dep_vars_Cons_keep)
with all ‹as = a'#as'› have "state_val s V = state_val s' V" by auto }
with ‹as = a'#as'› cases_x ‹es = ex#esx› ‹es' = ex'#esx'› ‹pred ex s›
show ?thesis by(cases "kind a'",auto)
qed
qed
next
case False
show ?thesis
proof(cases "∀V xs. (V,xs,as') ∈ dependent_live_vars n' ⟶
state_val (transfer ex s) V = state_val (transfer ex' s') V")
case True
hence imp':"∀V xs. (V,xs,as') ∈ dependent_live_vars n' ⟶
state_val (transfer ex s) V = state_val (transfer ex' s') V" .
from IH[OF ‹targetnode a' -as'→* n'› ‹xs ≼⇩b ys› ‹slice_path as' = xs›
‹select_edge_kinds as' xs = esx› ‹select_edge_kinds as' ys = esx'›
this ‹preds esx' (transfer ex' s')›]
have all':"∀V∈Use n'. state_val (transfers esx (transfer ex s)) V =
state_val (transfers esx' (transfer ex' s')) V"
and "preds esx (transfer ex s)" by simp_all
have "pred ex s"
proof(cases ex)
case (Predicate Q)
with ‹slice_path as = x#xs› ‹as = a'#as'› ‹last(targetnodes as) = n'› ex
have "ex = (λs. True)⇩√ ∨ n -a'#as'→⇩d* n'"
by(cases "kind a'",auto split:if_split_asm)
thus ?thesis
proof
assume "ex = (λs. True)⇩√" thus ?thesis by simp
next
assume "n -a'#as'→⇩d* n'"
with ‹slice_path as = x#xs› ‹as = a'#as'› ‹last(targetnodes as) = n'› ex
have [simp]:"ex = kind a'" by clarsimp
with ‹x ⟶ y› ex ex' have [simp]:"ex' = ex" by(cases x) auto
from ‹n -a'#as'→⇩d* n'› show ?thesis
proof(induct rule:DynPDG_path_rev_cases)
case DynPDG_path_Nil
hence False by simp
thus ?thesis by simp
next
case (DynPDG_path_cdep_Append n'' asx asx')
from ‹n -asx→⇩c⇩d n''›have "asx ≠ []"
by(auto elim:DynPDG_edge.cases dest:dyn_control_dependence_path)
with ‹n -asx→⇩c⇩d n''› ‹n'' -asx'→⇩d* n'› ‹a'#as' = asx@asx'›
have cdep:"∃as1 as2 n''. n -a'#as1→⇩c⇩d n'' ∧
n'' -as2→⇩d* n' ∧ as' = as1@as2"
by(cases asx) auto
{ fix V assume "V ∈ Use n"
with cdep ‹last(targetnodes as) = n'› ‹as = a'#as'›
have "(V,[],as) ∈ dependent_live_vars n'"
by(fastforce intro:dep_vars_Cons_cdep)
with all have "state_val s V = state_val s' V" by blast }
with ‹valid_edge a'› ‹pred ex' s'›
show ?thesis by(fastforce elim:CFG_edge_Uses_pred_equal)
next
case (DynPDG_path_ddep_Append V n'' asx asx')
from ‹n -{V}asx→⇩d⇩d n''› obtain ai ais where "asx = ai#ais"
by(cases asx)(auto dest:DynPDG_ddep_edge_CFG_path)
with ‹n -{V}asx→⇩d⇩d n''› have "sourcenode ai = n"
by(fastforce dest:DynPDG_ddep_edge_CFG_path elim:path.cases)
from ‹n -{V}asx→⇩d⇩d n''› ‹asx = ai#ais›
have "last(targetnodes asx) = n''"
by(fastforce intro:path_targetnode dest:DynPDG_ddep_edge_CFG_path)
{ fix V' assume "V' ∈ Use n"
from ‹n -{V}asx→⇩d⇩d n''› have "(V,[],[]) ∈ dependent_live_vars n''"
by(fastforce elim:DynPDG_edge.cases dep_vars_Use
simp:dyn_data_dependence_def)
with ‹n'' -asx'→⇩d* n'› have "(V,[],[]@asx') ∈ dependent_live_vars n'"
by(rule dependent_live_vars_dep_dependent_live_vars)
have "(V',[],as) ∈ dependent_live_vars n'"
proof(cases "asx' = []")
case True
with ‹n'' -asx'→⇩d* n'› have "n'' = n'"
by(fastforce intro:DynPDG_empty_path_eq_nodes)
with ‹n -{V}asx→⇩d⇩d n''› ‹V' ∈ Use n› True ‹as = a'#as'›
‹a'#as' = asx@asx'›
show ?thesis by(fastforce intro:dependent_live_vars_ddep_empty_fst)
next
case False
with ‹n -{V}asx→⇩d⇩d n''› ‹asx = ai#ais›
‹(V,[],[]@asx') ∈ dependent_live_vars n'›
have "(V,ais@[],ais@asx') ∈ dependent_live_vars n'"
by(fastforce intro:ddep_dependent_live_vars_keep_notempty)
from ‹n'' -asx'→⇩d* n'› False have "last(targetnodes asx') = n'"
by -(rule path_targetnode,rule DynPDG_path_CFG_path)
with ‹(V,ais@[],ais@asx') ∈ dependent_live_vars n'›
‹V' ∈ Use n› ‹n -{V}asx→⇩d⇩d n''› ‹asx = ai#ais›
‹sourcenode ai = n› ‹last(targetnodes asx) = n''› False
have "(V',[],ai#ais@asx') ∈ dependent_live_vars n'"
by(fastforce intro:dep_vars_Cons_ddep simp:targetnodes_def)
with ‹asx = ai#ais› ‹a'#as' = asx@asx'› ‹as = a'#as'›
show ?thesis by simp
qed
with all have "state_val s V' = state_val s' V'" by blast }
with ‹pred ex' s'› ‹valid_edge a'›
show ?thesis by(fastforce elim:CFG_edge_Uses_pred_equal)
qed
qed
qed simp
with all' ‹preds esx (transfer ex s)› ‹es = ex#esx› ‹es' = ex'#esx'›
show ?thesis by simp
next
case False
then obtain V' xs' where "(V',xs',as') ∈ dependent_live_vars n'"
and "state_val (transfer ex s) V' ≠ state_val (transfer ex' s') V'"
by auto
show ?thesis
proof(cases "n -a'#as'→⇩d* n'")
case True
with ‹slice_path as = x#xs› ‹as = a'#as'› ‹last(targetnodes as) = n'› ex
have [simp]:"ex = kind a'" by clarsimp
with ‹x ⟶ y› ex ex' have [simp]:"ex' = ex" by(cases x) auto
{ fix V assume "V ∈ Use (sourcenode a')"
hence "(V,[],[]) ∈ dependent_live_vars (sourcenode a')"
by(rule dep_vars_Use)
with ‹n -a'#as'→⇩d* n'› have "(V,[],[]@a'#as') ∈ dependent_live_vars n'"
by(fastforce intro:dependent_live_vars_dep_dependent_live_vars)
with all ‹as = a'#as'› have "state_val s V = state_val s' V"
by fastforce }
with ‹pred ex' s'› ‹valid_edge a'› have "pred ex s"
by(fastforce intro:CFG_edge_Uses_pred_equal)
show ?thesis
proof(cases "V' ∈ Def n")
case True
with ‹state_val (transfer ex s) V' ≠ state_val (transfer ex' s') V'›
‹valid_edge a'› ‹pred ex' s'› ‹pred ex s›
CFG_edge_transfer_uses_only_Use[of a' s s']
obtain V'' where "V'' ∈ Use n"
and "state_val s V'' ≠ state_val s' V''"
by auto
from True ‹(V',xs',as') ∈ dependent_live_vars n'›
‹targetnode a' -as'→* n'› ‹last(targetnodes as) = n'› ‹as = a'#as'›
‹valid_edge a'› ‹n = sourcenode a'›[THEN sym]
have "n -{V'}a'#xs'→⇩d⇩d last(targetnodes (a'#xs'))"
by -(drule dependent_live_vars_dependent_edge,
auto dest!: dependent_live_vars_dependent_edge
dest:DynPDG_ddep_edge_CFG_path path_targetnode
simp del:‹n = sourcenode a'›)
with ‹(V',xs',as') ∈ dependent_live_vars n'› ‹V'' ∈ Use n›
‹last(targetnodes as) = n'› ‹as = a'#as'›
have "(V'',[],as) ∈ dependent_live_vars n'"
by(fastforce intro:dep_vars_Cons_ddep)
with all have "state_val s V'' = state_val s' V''" by blast
with ‹state_val s V'' ≠ state_val s' V''› have False by simp
thus ?thesis by simp
next
case False
with ‹valid_edge a'› ‹pred ex s›
have "state_val (transfer (kind a') s) V' = state_val s V'"
by(fastforce intro:CFG_edge_no_Def_equal)
moreover
from False ‹valid_edge a'› ‹pred ex' s'›
have "state_val (transfer (kind a') s') V' = state_val s' V'"
by(fastforce intro:CFG_edge_no_Def_equal)
ultimately have "state_val s V' ≠ state_val s' V'"
using ‹state_val (transfer ex s) V' ≠ state_val (transfer ex' s') V'›
by simp
from False have "¬ n -{V'}a'#xs'→⇩d⇩d
last(targetnodes (a'#xs'))"
by(auto elim:DynPDG_edge.cases simp:dyn_data_dependence_def)
with ‹(V',xs',as') ∈ dependent_live_vars n'› ‹last(targetnodes as) = n'›
‹as = a'#as'›
have "(V',a'#xs',a'#as') ∈ dependent_live_vars n'"
by(fastforce intro:dep_vars_Cons_keep)
with ‹as = a'#as'› all have "state_val s V' = state_val s' V'" by auto
with ‹state_val s V' ≠ state_val s' V'› have False by simp
thus ?thesis by simp
qed
next
case False
{ assume "V' ∈ Def n"
with ‹(V',xs',as') ∈ dependent_live_vars n'› ‹targetnode a' -as'→* n'›
‹valid_edge a'›
have "n -a'#as'→⇩d* n'"
by -(drule dependent_live_vars_dependent_edge,
auto dest:DynPDG_path_ddep DynPDG_path_Append)
with False have "False" by simp }
hence "V' ∉ Def (sourcenode a')" by fastforce
from False ‹slice_path as = x#xs› ‹as = a'#as'›
‹last(targetnodes as) = n'› ‹as' ≠ []›
have "¬ x" by(auto simp:targetnodes_def)
with ex have cases:"ex = (case kind a' of ⇑f ⇒ ⇑id | (Q)⇩√ ⇒ (λs. True)⇩√)"
by simp
have "state_val s V' ≠ state_val s' V'"
proof(cases y)
case True
with ex' have [simp]:"ex' = kind a'" by simp
from ‹V' ∉ Def (sourcenode a')› ‹valid_edge a'› ‹pred ex' s'›
have states_eq:"state_val (transfer (kind a') s') V' = state_val s' V'"
by(fastforce intro:CFG_edge_no_Def_equal)
from cases have "state_val s V' = state_val (transfer ex s) V'"
by(cases "kind a'") auto
with states_eq
‹state_val (transfer ex s) V' ≠ state_val (transfer ex' s') V'›
show ?thesis by simp
next
case False
with ex' have "ex' = (case kind a' of ⇑f ⇒ ⇑id | (Q)⇩√ ⇒ (λs. True)⇩√)"
by simp
with cases have "state_val s V' = state_val (transfer ex s) V'"
and "state_val s' V' = state_val (transfer ex' s') V'"
by(cases "kind a'",auto)+
with ‹state_val (transfer ex s) V' ≠ state_val (transfer ex' s') V'›
show ?thesis by simp
qed
from ‹V' ∉ Def (sourcenode a')›
have "¬ n -{V'}a'#xs'→⇩d⇩d last(targetnodes (a'#xs'))"
by(auto elim:DynPDG_edge.cases simp:dyn_data_dependence_def)
with ‹(V',xs',as') ∈ dependent_live_vars n'› ‹last(targetnodes as) = n'›
‹as = a'#as'›
have "(V',a'#xs',a'#as') ∈ dependent_live_vars n'"
by(fastforce intro:dep_vars_Cons_keep)
with ‹as = a'#as'› all have "state_val s V' = state_val s' V'" by auto
with ‹state_val s V' ≠ state_val s' V'› have False by simp
thus ?thesis by simp
qed
qed
qed
qed simp_all
theorem fundamental_property_of_path_slicing:
assumes "n -as→* n'" and "preds (kinds as) s"
shows "(∀V ∈ Use n'. state_val (transfers (slice_kinds as) s) V =
state_val (transfers (kinds as) s) V)"
and "preds (slice_kinds as) s"
proof -
have "length as = length (slice_path as)" by(simp add:slice_path_length)
hence "slice_path as ≼⇩b replicate (length as) True"
by(simp add:maximal_element)
have "select_edge_kinds as (replicate (length as) True) = kinds as"
by(rule select_edge_kinds_max_bv)
with ‹n -as→* n'› ‹slice_path as ≼⇩b replicate (length as) True›
‹preds (kinds as) s›
have "(∀V∈Use n'. state_val (transfers (slice_kinds as) s) V =
state_val (transfers (kinds as) s) V) ∧ preds (slice_kinds as) s"
by -(rule slice_path_leqs_information_same_Uses,simp_all add:slice_kinds_def)
thus "∀V∈Use n'. state_val (transfers (slice_kinds as) s) V =
state_val (transfers (kinds as) s) V" and "preds (slice_kinds as) s"
by simp_all
qed
end
subsection ‹The fundamental property of (dynamic) slicing related to the semantics›
locale BackwardPathSlice_wf =
DynPDG sourcenode targetnode kind valid_edge Entry Def Use state_val Exit
dyn_control_dependence +
CFG_semantics_wf sourcenode targetnode kind valid_edge Entry sem identifies
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 dyn_control_dependence :: "'node ⇒ 'node ⇒ 'edge list ⇒ bool"
("_ controls _ via _" [51, 0, 0] 1000)
and Exit :: "'node" ("'('_Exit'_')")
and sem :: "'com ⇒ 'state ⇒ 'com ⇒ 'state ⇒ bool"
("((1⟨_,/_⟩) ⇒/ (1⟨_,/_⟩))" [0,0,0,0] 81)
and identifies :: "'node ⇒ 'com ⇒ bool" ("_ ≜ _" [51, 0] 80)
begin
theorem fundamental_property_of_path_slicing_semantically:
assumes "n ≜ c" and "⟨c,s⟩ ⇒ ⟨c',s'⟩"
obtains n' as where "n -as→* n'" and "preds (slice_kinds as) s"
and "n' ≜ c'"
and "∀V ∈ Use n'. state_val (transfers (slice_kinds as) s) V =
state_val s' V"
proof(atomize_elim)
from ‹n ≜ c› ‹⟨c,s⟩ ⇒ ⟨c',s'⟩› obtain n' as where "n -as→* n'"
and "transfers (kinds as) s = s'"
and "preds (kinds as) s"
and "n' ≜ c'"
by(fastforce dest:fundamental_property)
with ‹n -as→* n'› ‹preds (kinds as) s›
have "∀V ∈ Use n'. state_val (transfers (slice_kinds as) s) V =
state_val (transfers (kinds as) s) V" and "preds (slice_kinds as) s"
by -(rule fundamental_property_of_path_slicing,simp_all)+
with ‹transfers (kinds as) s = s'› have "∀V ∈ Use n'.
state_val (transfers (slice_kinds as) s) V =
state_val s' V" by simp
with ‹n -as→* n'› ‹preds (slice_kinds as) s› ‹n' ≜ c'›
show "∃as n'. n -as→* n' ∧ preds (slice_kinds as) s ∧ n' ≜ c' ∧
(∀V∈Use n'. state_val (transfers (slice_kinds as) s) V = state_val s' V)"
by blast
qed
end
end