Theory Slice
section ‹Static backward slice›
theory Slice imports SCDObservable Distance begin
context SDG begin
subsection ‹Preliminary definitions on the parameter nodes for defining
sliced call and return edges›
fun csppa :: "'node ⇒ 'node SDG_node set ⇒ nat ⇒
((('var ⇀ 'val) ⇒ 'val option) list) ⇒ ((('var ⇀ 'val) ⇒ 'val option) list)"
where "csppa m S x [] = []"
| "csppa m S x (f#fs) =
(if Formal_in(m,x) ∉ S then Map.empty else f)#csppa m S (Suc x) fs"
definition cspp :: "'node ⇒ 'node SDG_node set ⇒
((('var ⇀ 'val) ⇒ 'val option) list) ⇒ ((('var ⇀ 'val) ⇒ 'val option) list)"
where "cspp m S fs ≡ csppa m S 0 fs"
lemma [simp]: "length (csppa m S x fs) = length fs"
by(induct fs arbitrary:x)(auto)
lemma [simp]: "length (cspp m S fs) = length fs"
by(simp add:cspp_def)
lemma csppa_Formal_in_notin_slice:
"⟦x < length fs; Formal_in(m,x + i) ∉ S⟧
⟹ (csppa m S i fs)!x = Map.empty"
by(induct fs arbitrary:i x,auto simp:nth_Cons')
lemma csppa_Formal_in_in_slice:
"⟦x < length fs; Formal_in(m,x + i) ∈ S⟧
⟹ (csppa m S i fs)!x = fs!x"
by(induct fs arbitrary:i x,auto simp:nth_Cons')
definition map_merge :: "('var ⇀ 'val) ⇒ ('var ⇀ 'val) ⇒ (nat ⇒ bool) ⇒
'var list ⇒ ('var ⇀ 'val)"
where "map_merge f g Q xs ≡ (λV. if (∃i. i < length xs ∧ xs!i = V ∧ Q i) then g V
else f V)"
definition rspp :: "'node ⇒ 'node SDG_node set ⇒ 'var list ⇒
('var ⇀ 'val) ⇒ ('var ⇀ 'val) ⇒ ('var ⇀ 'val)"
where "rspp m S xs f g ≡ map_merge f (Map.empty(ParamDefs m [:=] map g xs))
(λi. Actual_out(m,i) ∈ S) (ParamDefs m)"
lemma rspp_Actual_out_in_slice:
assumes "x < length (ParamDefs (targetnode a))" and "valid_edge a"
and "length (ParamDefs (targetnode a)) = length xs"
and "Actual_out (targetnode a,x) ∈ S"
shows "(rspp (targetnode a) S xs f g) ((ParamDefs (targetnode a))!x) = g(xs!x)"
proof -
from ‹valid_edge a› have "distinct(ParamDefs (targetnode a))"
by(rule distinct_ParamDefs)
from ‹x < length (ParamDefs (targetnode a))›
‹length (ParamDefs (targetnode a)) = length xs›
‹distinct(ParamDefs (targetnode a))›
have "(Map.empty(ParamDefs (targetnode a) [:=] map g xs))
((ParamDefs (targetnode a))!x) = (map g xs)!x"
by(fastforce intro:fun_upds_nth)
with ‹Actual_out(targetnode a,x) ∈ S› ‹x < length (ParamDefs (targetnode a))›
‹length (ParamDefs (targetnode a)) = length xs› show ?thesis
by(fastforce simp:rspp_def map_merge_def)
qed
lemma rspp_Actual_out_notin_slice:
assumes "x < length (ParamDefs (targetnode a))" and "valid_edge a"
and "length (ParamDefs (targetnode a)) = length xs"
and "Actual_out((targetnode a),x) ∉ S"
shows "(rspp (targetnode a) S xs f g) ((ParamDefs (targetnode a))!x) =
f((ParamDefs (targetnode a))!x)"
proof -
from ‹valid_edge a› have "distinct(ParamDefs (targetnode a))"
by(rule distinct_ParamDefs)
from ‹x < length (ParamDefs (targetnode a))›
‹length (ParamDefs (targetnode a)) = length xs›
‹distinct(ParamDefs (targetnode a))›
have "(Map.empty(ParamDefs (targetnode a) [:=] map g xs))
((ParamDefs (targetnode a))!x) = (map g xs)!x"
by(fastforce intro:fun_upds_nth)
with ‹Actual_out((targetnode a),x) ∉ S› ‹distinct(ParamDefs (targetnode a))›
‹x < length (ParamDefs (targetnode a))›
show ?thesis by(fastforce simp:rspp_def map_merge_def nth_eq_iff_index_eq)
qed
subsection ‹Defining the sliced edge kinds›
primrec slice_kind_aux :: "'node ⇒ 'node ⇒ 'node SDG_node set ⇒
('var,'val,'ret,'pname) edge_kind ⇒ ('var,'val,'ret,'pname) edge_kind"
where "slice_kind_aux m m' S ⇑f = (if m ∈ ⌊S⌋⇘CFG⇙ then ⇑f else ⇑id)"
| "slice_kind_aux m m' S (Q)⇩√ = (if m ∈ ⌊S⌋⇘CFG⇙ then (Q)⇩√ else
(if obs_intra m ⌊S⌋⇘CFG⇙ = {} then
(let mex = (THE mex. method_exit mex ∧ get_proc m = get_proc mex) in
(if (∃x. distance m' mex x ∧ distance m mex (x + 1) ∧
(m' = (SOME mx'. ∃a'. m = sourcenode a' ∧
distance (targetnode a') mex x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = mx')))
then (λcf. True)⇩√ else (λcf. False)⇩√))
else (let mx = THE mx. mx ∈ obs_intra m ⌊S⌋⇘CFG⇙ in
(if (∃x. distance m' mx x ∧ distance m mx (x + 1) ∧
(m' = (SOME mx'. ∃a'. m = sourcenode a' ∧
distance (targetnode a') mx x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = mx')))
then (λcf. True)⇩√ else (λcf. False)⇩√))))"
| "slice_kind_aux m m' S (Q:r↪⇘p⇙fs) = (if m ∈ ⌊S⌋⇘CFG⇙ then (Q:r↪⇘p⇙(cspp m' S fs))
else ((λcf. False):r↪⇘p⇙fs))"
| "slice_kind_aux m m' S (Q↩⇘p⇙f) = (if m ∈ ⌊S⌋⇘CFG⇙ then
(let outs = THE outs. ∃ins. (p,ins,outs) ∈ set procs in
(Q↩⇘p⇙(λcf cf'. rspp m' S outs cf' cf)))
else ((λcf. True)↩⇘p⇙(λcf cf'. cf')))"
definition slice_kind :: "'node SDG_node set ⇒ 'edge ⇒
('var,'val,'ret,'pname) edge_kind"
where "slice_kind S a ≡
slice_kind_aux (sourcenode a) (targetnode a) (HRB_slice S) (kind a)"
definition slice_kinds :: "'node SDG_node set ⇒ 'edge list ⇒
('var,'val,'ret,'pname) edge_kind list"
where "slice_kinds S as ≡ map (slice_kind S) as"
lemma slice_intra_kind_in_slice:
"⟦sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙; intra_kind (kind a)⟧
⟹ slice_kind S a = kind a"
by(fastforce simp:intra_kind_def slice_kind_def)
lemma slice_kind_Upd:
"⟦sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙; kind a = ⇑f⟧ ⟹ slice_kind S a = ⇑id"
by(simp add:slice_kind_def)
lemma slice_kind_Pred_empty_obs_nearer_SOME:
assumes "sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙" and "kind a = (Q)⇩√"
and "obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {}"
and "method_exit mex" and "get_proc (sourcenode a) = get_proc mex"
and "distance (targetnode a) mex x" and "distance (sourcenode a) mex (x + 1)"
and "targetnode a = (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') mex x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = n')"
shows "slice_kind S a = (λs. True)⇩√"
proof -
from ‹method_exit mex› ‹get_proc (sourcenode a) = get_proc mex›
have "mex = (THE mex. method_exit mex ∧ get_proc (sourcenode a) = get_proc mex)"
by(auto intro!:the_equality[THEN sym] intro:method_exit_unique)
with ‹sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹kind a = (Q)⇩√›
‹obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {}›
have "slice_kind S a =
(if (∃x. distance (targetnode a) mex x ∧ distance (sourcenode a) mex (x + 1) ∧
(targetnode a = (SOME mx'. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') mex x ∧ valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = mx'))) then (λcf. True)⇩√ else (λcf. False)⇩√)"
by(simp add:slice_kind_def Let_def)
with ‹distance (targetnode a) mex x› ‹distance (sourcenode a) mex (x + 1)›
‹targetnode a = (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') mex x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = n')›
show ?thesis by fastforce
qed
lemma slice_kind_Pred_empty_obs_nearer_not_SOME:
assumes "sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙" and "kind a = (Q)⇩√"
and "obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {}"
and "method_exit mex" and "get_proc (sourcenode a) = get_proc mex"
and "distance (targetnode a) mex x" and "distance (sourcenode a) mex (x + 1)"
and "targetnode a ≠ (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') mex x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = n')"
shows "slice_kind S a = (λs. False)⇩√"
proof -
from ‹method_exit mex› ‹get_proc (sourcenode a) = get_proc mex›
have "mex = (THE mex. method_exit mex ∧ get_proc (sourcenode a) = get_proc mex)"
by(auto intro!:the_equality[THEN sym] intro:method_exit_unique)
with ‹sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹kind a = (Q)⇩√›
‹obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {}›
have "slice_kind S a =
(if (∃x. distance (targetnode a) mex x ∧ distance (sourcenode a) mex (x + 1) ∧
(targetnode a = (SOME mx'. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') mex x ∧ valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = mx'))) then (λcf. True)⇩√ else (λcf. False)⇩√)"
by(simp add:slice_kind_def Let_def)
with ‹distance (targetnode a) mex x› ‹distance (sourcenode a) mex (x + 1)›
‹targetnode a ≠ (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') mex x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = n')›
show ?thesis by(auto dest:distance_det)
qed
lemma slice_kind_Pred_empty_obs_not_nearer:
assumes "sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙" and "kind a = (Q)⇩√"
and "obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {}"
and "method_exit mex" and "get_proc (sourcenode a) = get_proc mex"
and dist:"distance (sourcenode a) mex (x + 1)" "¬ distance (targetnode a) mex x"
shows "slice_kind S a = (λs. False)⇩√"
proof -
from ‹method_exit mex› ‹get_proc (sourcenode a) = get_proc mex›
have "mex = (THE mex. method_exit mex ∧ get_proc (sourcenode a) = get_proc mex)"
by(auto intro!:the_equality[THEN sym] intro:method_exit_unique)
moreover
from dist have "¬ (∃x. distance (targetnode a) mex x ∧
distance (sourcenode a) mex (x + 1))"
by(fastforce dest:distance_det)
ultimately show ?thesis using assms by(auto simp:slice_kind_def Let_def)
qed
lemma slice_kind_Pred_obs_nearer_SOME:
assumes "sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙" and "kind a = (Q)⇩√"
and "m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙"
and "distance (targetnode a) m x" "distance (sourcenode a) m (x + 1)"
and "targetnode a = (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') m x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = n')"
shows "slice_kind S a = (λs. True)⇩√"
proof -
from ‹m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙›
have "m = (THE m. m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙)"
by(rule obs_intra_the_element[THEN sym])
with assms show ?thesis by(auto simp:slice_kind_def Let_def)
qed
lemma slice_kind_Pred_obs_nearer_not_SOME:
assumes "sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙" and "kind a = (Q)⇩√"
and "m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙"
and "distance (targetnode a) m x" "distance (sourcenode a) m (x + 1)"
and "targetnode a ≠ (SOME nx'. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') m x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = nx')"
shows "slice_kind S a = (λs. False)⇩√"
proof -
from ‹m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙›
have "m = (THE m. m ∈ obs_intra (sourcenode a) (⌊HRB_slice S⌋⇘CFG⇙))"
by(rule obs_intra_the_element[THEN sym])
with assms show ?thesis by(auto dest:distance_det simp:slice_kind_def Let_def)
qed
lemma slice_kind_Pred_obs_not_nearer:
assumes "sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙" and "kind a = (Q)⇩√"
and in_obs:"m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙"
and dist:"distance (sourcenode a) m (x + 1)"
"¬ distance (targetnode a) m x"
shows "slice_kind S a = (λs. False)⇩√"
proof -
from in_obs have the:"m = (THE m. m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙)"
by(rule obs_intra_the_element[THEN sym])
from dist have "¬ (∃x. distance (targetnode a) m x ∧
distance (sourcenode a) m (x + 1))"
by(fastforce dest:distance_det)
with ‹sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹kind a = (Q)⇩√› in_obs the show ?thesis
by(auto simp:slice_kind_def Let_def)
qed
lemma kind_Predicate_notin_slice_slice_kind_Predicate:
assumes "sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙" and "valid_edge a" and "kind a = (Q)⇩√"
obtains Q' where "slice_kind S a = (Q')⇩√" and "Q' = (λs. False) ∨ Q' = (λs. True)"
proof(atomize_elim)
show "∃Q'. slice_kind S a = (Q')⇩√ ∧ (Q' = (λs. False) ∨ Q' = (λs. True))"
proof(cases "obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {}")
case True
from ‹valid_edge a› have "valid_node (sourcenode a)" by simp
then obtain as where "sourcenode a -as→⇩√* (_Exit_)" by(fastforce dest:Exit_path)
then obtain as' mex where "sourcenode a -as'→⇩ι* mex" and "method_exit mex"
by -(erule valid_Exit_path_intra_path)
from ‹sourcenode a -as'→⇩ι* mex› have "get_proc (sourcenode a) = get_proc mex"
by(rule intra_path_get_procs)
show ?thesis
proof(cases "∃x. distance (targetnode a) mex x ∧
distance (sourcenode a) mex (x + 1)")
case True
then obtain x where "distance (targetnode a) mex x"
and "distance (sourcenode a) mex (x + 1)" by blast
show ?thesis
proof(cases "targetnode a = (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') mex x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = n')")
case True
with ‹sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹kind a = (Q)⇩√›
‹obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {}›
‹method_exit mex› ‹get_proc (sourcenode a) = get_proc mex›
‹distance (targetnode a) mex x› ‹distance (sourcenode a) mex (x + 1)›
have "slice_kind S a = (λs. True)⇩√"
by(rule slice_kind_Pred_empty_obs_nearer_SOME)
thus ?thesis by simp
next
case False
with ‹sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹kind a = (Q)⇩√›
‹obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {}›
‹method_exit mex› ‹get_proc (sourcenode a) = get_proc mex›
‹distance (targetnode a) mex x› ‹distance (sourcenode a) mex (x + 1)›
have "slice_kind S a = (λs. False)⇩√"
by(rule slice_kind_Pred_empty_obs_nearer_not_SOME)
thus ?thesis by simp
qed
next
case False
from ‹method_exit mex› ‹get_proc (sourcenode a) = get_proc mex›
have "mex = (THE mex. method_exit mex ∧ get_proc (sourcenode a) = get_proc mex)"
by(auto intro!:the_equality[THEN sym] intro:method_exit_unique)
with ‹sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹kind a = (Q)⇩√›
‹obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {}› False
have "slice_kind S a = (λs. False)⇩√"
by(auto simp:slice_kind_def Let_def)
thus ?thesis by simp
qed
next
case False
then obtain m where "m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙" by blast
show ?thesis
proof(cases "∃x. distance (targetnode a) m x ∧
distance (sourcenode a) m (x + 1)")
case True
then obtain x where "distance (targetnode a) m x"
and "distance (sourcenode a) m (x + 1)" by blast
show ?thesis
proof(cases "targetnode a = (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') m x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = n')")
case True
with ‹sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹kind a = (Q)⇩√›
‹m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙›
‹distance (targetnode a) m x› ‹distance (sourcenode a) m (x + 1)›
have "slice_kind S a = (λs. True)⇩√"
by(rule slice_kind_Pred_obs_nearer_SOME)
thus ?thesis by simp
next
case False
with ‹sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹kind a = (Q)⇩√›
‹m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙›
‹distance (targetnode a) m x› ‹distance (sourcenode a) m (x + 1)›
have "slice_kind S a = (λs. False)⇩√"
by(rule slice_kind_Pred_obs_nearer_not_SOME)
thus ?thesis by simp
qed
next
case False
from ‹m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙›
have "m = (THE m. m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙)"
by(rule obs_intra_the_element[THEN sym])
with ‹sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹kind a = (Q)⇩√› False
‹m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙›
have "slice_kind S a = (λs. False)⇩√"
by(auto simp:slice_kind_def Let_def)
thus ?thesis by simp
qed
qed
qed
lemma slice_kind_Call:
"⟦sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙; kind a = Q:r↪⇘p⇙fs⟧
⟹ slice_kind S a = (λcf. False):r↪⇘p⇙fs"
by(simp add:slice_kind_def)
lemma slice_kind_Call_in_slice:
"⟦sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙; kind a = Q:r↪⇘p⇙fs⟧
⟹ slice_kind S a = Q:r↪⇘p⇙(cspp (targetnode a) (HRB_slice S) fs)"
by(simp add:slice_kind_def)
lemma slice_kind_Call_in_slice_Formal_in_not:
assumes "sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙" and "kind a = Q:r↪⇘p⇙fs"
and "∀x < length fs. Formal_in(targetnode a,x) ∉ HRB_slice S"
shows "slice_kind S a = Q:r↪⇘p⇙replicate (length fs) Map.empty"
proof -
from ‹sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙› ‹kind a = Q:r↪⇘p⇙fs›
have "slice_kind S a = Q:r↪⇘p⇙(cspp (targetnode a) (HRB_slice S) fs)"
by(simp add:slice_kind_def)
from ‹∀x < length fs. Formal_in(targetnode a,x) ∉ HRB_slice S›
have "cspp (targetnode a) (HRB_slice S) fs = replicate (length fs) Map.empty"
by(fastforce intro:nth_equalityI csppa_Formal_in_notin_slice simp:cspp_def)
with ‹slice_kind S a = Q:r↪⇘p⇙(cspp (targetnode a) (HRB_slice S) fs)›
show ?thesis by simp
qed
lemma slice_kind_Call_in_slice_Formal_in_also:
assumes "sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙" and "kind a = Q:r↪⇘p⇙fs"
and "∀x < length fs. Formal_in(targetnode a,x) ∈ HRB_slice S"
shows "slice_kind S a = Q:r↪⇘p⇙fs"
proof -
from ‹sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙› ‹kind a = Q:r↪⇘p⇙fs›
have "slice_kind S a = Q:r↪⇘p⇙(cspp (targetnode a) (HRB_slice S) fs)"
by(simp add:slice_kind_def)
from ‹∀x < length fs. Formal_in(targetnode a,x) ∈ HRB_slice S›
have "cspp (targetnode a) (HRB_slice S) fs = fs"
by(fastforce intro:nth_equalityI csppa_Formal_in_in_slice simp:cspp_def)
with ‹slice_kind S a = Q:r↪⇘p⇙(cspp (targetnode a) (HRB_slice S) fs)›
show ?thesis by simp
qed
lemma slice_kind_Call_intra_notin_slice:
assumes "sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙" and "valid_edge a"
and "intra_kind (kind a)" and "valid_edge a'" and "kind a' = Q:r↪⇘p⇙fs"
and "sourcenode a' = sourcenode a"
shows "slice_kind S a = (λs. True)⇩√"
proof -
from ‹valid_edge a'› ‹kind a' = Q:r↪⇘p⇙fs› obtain a''
where "a'' ∈ get_return_edges a'"
by(fastforce dest:get_return_edge_call)
with ‹valid_edge a'› obtain ax where "valid_edge ax"
and "sourcenode ax = sourcenode a'" and " targetnode ax = targetnode a''"
and "kind ax = (λcf. False)⇩√"
by(fastforce dest:call_return_node_edge)
from ‹valid_edge a'› ‹kind a' = Q:r↪⇘p⇙fs›
have "∃!a''. valid_edge a'' ∧ sourcenode a'' = sourcenode a' ∧
intra_kind(kind a'')"
by(rule call_only_one_intra_edge)
with ‹valid_edge a› ‹sourcenode a' = sourcenode a› ‹intra_kind (kind a)›
have all:"∀a''. valid_edge a'' ∧ sourcenode a'' = sourcenode a' ∧
intra_kind(kind a'') ⟶ a'' = a" by fastforce
with ‹valid_edge ax› ‹sourcenode ax = sourcenode a'› ‹kind ax = (λcf. False)⇩√›
have [simp]:"ax = a" by(fastforce simp:intra_kind_def)
show ?thesis
proof(cases "obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {}")
case True
from ‹valid_edge a› have "valid_node (sourcenode a)" by simp
then obtain asx where "sourcenode a -asx→⇩√* (_Exit_)" by(fastforce dest:Exit_path)
then obtain as pex where "sourcenode a-as→⇩ι* pex" and "method_exit pex"
by -(erule valid_Exit_path_intra_path)
from ‹sourcenode a-as→⇩ι* pex› have "get_proc (sourcenode a) = get_proc pex"
by(rule intra_path_get_procs)
from ‹sourcenode a-as→⇩ι* pex› obtain x where "distance (sourcenode a) pex x"
and "x ≤ length as" by(erule every_path_distance)
from ‹method_exit pex› have "sourcenode a ≠ pex"
proof(rule method_exit_cases)
assume "pex = (_Exit_)"
show ?thesis
proof
assume "sourcenode a = pex"
with ‹pex = (_Exit_)› have "sourcenode a = (_Exit_)" by simp
with ‹valid_edge a› show False by(rule Exit_source)
qed
next
fix ax Qx px fx
assume "pex = sourcenode ax" and "valid_edge ax" and "kind ax = Qx↩⇘px⇙fx"
hence "∀a'. valid_edge a' ∧ sourcenode a' = sourcenode ax ⟶
(∃Qx' fx'. kind a' = Qx'↩⇘px⇙fx')" by -(rule return_edges_only)
with ‹valid_edge a› ‹intra_kind (kind a)› ‹pex = sourcenode ax›
show ?thesis by(fastforce simp:intra_kind_def)
qed
have "x ≠ 0"
proof
assume "x = 0"
with ‹distance (sourcenode a) pex x› have "sourcenode a = pex"
by(fastforce elim:distance.cases simp:intra_path_def)
with ‹sourcenode a ≠ pex› show False by simp
qed
with ‹distance (sourcenode a) pex x› obtain ax' where "valid_edge ax'"
and "sourcenode a = sourcenode ax'" and "intra_kind(kind ax')"
and "distance (targetnode ax') pex (x - 1)"
and Some:"targetnode ax' = (SOME nx. ∃a'. sourcenode ax' = sourcenode a' ∧
distance (targetnode a') pex (x - 1) ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = nx)"
by(erule distance_successor_distance)
from ‹valid_edge ax'› ‹sourcenode a = sourcenode ax'› ‹intra_kind(kind ax')›
‹sourcenode a' = sourcenode a› all
have [simp]:"ax' = a" by fastforce
from ‹sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹kind ax = (λcf. False)⇩√›
True ‹method_exit pex› ‹get_proc (sourcenode a) = get_proc pex› ‹x ≠ 0›
‹distance (targetnode ax') pex (x - 1)› ‹distance (sourcenode a) pex x› Some
show ?thesis by(fastforce elim:slice_kind_Pred_empty_obs_nearer_SOME)
next
case False
then obtain m where "m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙" by fastforce
then obtain as where "sourcenode a-as→⇩ι* m" and "m ∈ ⌊HRB_slice S⌋⇘CFG⇙"
by -(erule obs_intraE)
from ‹sourcenode a-as→⇩ι* m› obtain x where "distance (sourcenode a) m x"
and "x ≤ length as" by(erule every_path_distance)
from ‹sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹m ∈ ⌊HRB_slice S⌋⇘CFG⇙›
have "sourcenode a ≠ m" by fastforce
have "x ≠ 0"
proof
assume "x = 0"
with ‹distance (sourcenode a) m x› have "sourcenode a = m"
by(fastforce elim:distance.cases simp:intra_path_def)
with ‹sourcenode a ≠ m› show False by simp
qed
with ‹distance (sourcenode a) m x› obtain ax' where "valid_edge ax'"
and "sourcenode a = sourcenode ax'" and "intra_kind(kind ax')"
and "distance (targetnode ax') m (x - 1)"
and Some:"targetnode ax' = (SOME nx. ∃a'. sourcenode ax' = sourcenode a' ∧
distance (targetnode a') m (x - 1) ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = nx)"
by(erule distance_successor_distance)
from ‹valid_edge ax'› ‹sourcenode a = sourcenode ax'› ‹intra_kind(kind ax')›
‹sourcenode a' = sourcenode a› all
have [simp]:"ax' = a" by fastforce
from ‹sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹kind ax = (λcf. False)⇩√›
‹m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙› ‹x ≠ 0›
‹distance (targetnode ax') m (x - 1)› ‹distance (sourcenode a) m x› Some
show ?thesis by(fastforce elim:slice_kind_Pred_obs_nearer_SOME)
qed
qed
lemma slice_kind_Return:
"⟦sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙; kind a = Q↩⇘p⇙f⟧
⟹ slice_kind S a = (λcf. True)↩⇘p⇙(λcf cf'. cf')"
by(simp add:slice_kind_def)
lemma slice_kind_Return_in_slice:
"⟦sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙; valid_edge a; kind a = Q↩⇘p⇙f;
(p,ins,outs) ∈ set procs⟧
⟹ slice_kind S a = Q↩⇘p⇙(λcf cf'. rspp (targetnode a) (HRB_slice S) outs cf' cf)"
by(simp add:slice_kind_def,unfold formal_out_THE,simp)
lemma length_transfer_kind_slice_kind:
assumes "valid_edge a" and "length s⇩1 = length s⇩2"
and "transfer (kind a) s⇩1 = s⇩1'" and "transfer (slice_kind S a) s⇩2 = s⇩2'"
shows "length s⇩1' = length s⇩2'"
proof(cases "kind a" rule:edge_kind_cases)
case Intra
show ?thesis
proof(cases "sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙")
case True
with Intra assms show ?thesis
by(cases s⇩1)(cases s⇩2,auto dest:slice_intra_kind_in_slice simp:intra_kind_def)+
next
case False
with Intra assms show ?thesis
by(cases s⇩1)(cases s⇩2,auto dest:slice_kind_Upd
elim:kind_Predicate_notin_slice_slice_kind_Predicate simp:intra_kind_def)+
qed
next
case (Call Q r p fs)
show ?thesis
proof(cases "sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙")
case True
with Call assms show ?thesis
by(cases s⇩1)(cases s⇩2,auto dest:slice_kind_Call_in_slice)+
next
case False
with Call assms show ?thesis
by(cases s⇩1)(cases s⇩2,auto dest:slice_kind_Call)+
qed
next
case (Return Q p f)
show ?thesis
proof(cases "sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙")
case True
from Return ‹valid_edge a› obtain a' Q' r fs
where "valid_edge a'" and "kind a' = Q':r↪⇘p⇙fs"
by -(drule return_needs_call,auto)
then obtain ins outs where "(p,ins,outs) ∈ set procs"
by(fastforce dest!:callee_in_procs)
with True ‹valid_edge a› Return assms show ?thesis
by(cases s⇩1)(cases s⇩2,auto dest:slice_kind_Return_in_slice split:list.split)+
next
case False
with Return assms show ?thesis
by(cases s⇩1)(cases s⇩2,auto dest:slice_kind_Return split:list.split)+
qed
qed
subsection ‹The sliced graph of a deterministic CFG is still deterministic›
lemma only_one_SOME_edge:
assumes "valid_edge a" and "intra_kind(kind a)" and "distance (targetnode a) mex x"
shows "∃!a'. sourcenode a = sourcenode a' ∧ distance (targetnode a') mex x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') mex x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = n')"
proof(rule ex_ex1I)
show "∃a'. sourcenode a = sourcenode a' ∧ distance (targetnode a') mex x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') mex x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = n')"
proof -
have "(∃a'. sourcenode a = sourcenode a' ∧ distance (targetnode a') mex x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') mex x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = n')) =
(∃n'. ∃a'. sourcenode a = sourcenode a' ∧ distance (targetnode a') mex x ∧
valid_edge a' ∧ intra_kind(kind a') ∧ targetnode a' = n')"
apply(unfold some_eq_ex[of "λn'. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') mex x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = n'"])
by simp
also have "…"
using ‹valid_edge a› ‹intra_kind(kind a)› ‹distance (targetnode a) mex x›
by blast
finally show ?thesis .
qed
next
fix a' ax
assume "sourcenode a = sourcenode a' ∧ distance (targetnode a') mex x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') mex x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = n')"
and "sourcenode a = sourcenode ax ∧ distance (targetnode ax) mex x ∧
valid_edge ax ∧ intra_kind(kind ax) ∧
targetnode ax = (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') mex x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = n')"
thus "a' = ax" by(fastforce intro!:edge_det)
qed
lemma slice_kind_only_one_True_edge:
assumes "sourcenode a = sourcenode a'" and "targetnode a ≠ targetnode a'"
and "valid_edge a" and "valid_edge a'" and "intra_kind (kind a)"
and "intra_kind (kind a')" and "slice_kind S a = (λs. True)⇩√"
shows "slice_kind S a' = (λs. False)⇩√"
proof -
from assms obtain Q Q' where "kind a = (Q)⇩√"
and "kind a' = (Q')⇩√" and det:"∀s. (Q s ⟶ ¬ Q' s) ∧ (Q' s ⟶ ¬ Q s)"
by(auto dest:deterministic)
show ?thesis
proof(cases "sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙")
case True
with ‹slice_kind S a = (λs. True)⇩√› ‹kind a = (Q)⇩√› have "Q = (λs. True)"
by(simp add:slice_kind_def Let_def)
with det have "Q' = (λs. False)" by(simp add:fun_eq_iff)
with True ‹kind a' = (Q')⇩√› ‹sourcenode a = sourcenode a'› show ?thesis
by(simp add:slice_kind_def Let_def)
next
case False
hence "sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙" by simp
thus ?thesis
proof(cases "obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {}")
case True
with ‹sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹slice_kind S a = (λs. True)⇩√›
‹kind a = (Q)⇩√›
obtain mex x where mex:"mex = (THE mex. method_exit mex ∧
get_proc (sourcenode a) = get_proc mex)"
and dist:"distance (targetnode a) mex x" "distance (sourcenode a) mex (x + 1)"
and target:"targetnode a = (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') mex x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = n')"
by(auto simp:slice_kind_def Let_def fun_eq_iff split:if_split_asm)
from ‹valid_edge a› ‹intra_kind (kind a)› ‹distance (targetnode a) mex x›
have ex1:"∃!a'. sourcenode a = sourcenode a' ∧ distance (targetnode a') mex x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') mex x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = n')"
by(rule only_one_SOME_edge)
have "targetnode a' ≠ (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') mex x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = n')"
proof(rule ccontr)
assume "¬ targetnode a' ≠ (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') mex x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = n')"
hence "targetnode a' = (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') mex x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = n')"
by simp
with ex1 target ‹sourcenode a = sourcenode a'› ‹valid_edge a› ‹valid_edge a'›
‹intra_kind(kind a)› ‹intra_kind(kind a')› ‹distance (targetnode a) mex x›
have "a = a'" by fastforce
with ‹targetnode a ≠ targetnode a'› show False by simp
qed
with ‹sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙› True ‹kind a' = (Q')⇩√›
‹sourcenode a = sourcenode a'› mex dist
show ?thesis by(auto dest:distance_det
simp:slice_kind_def Let_def fun_eq_iff split:if_split_asm)
next
case False
hence "obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ ≠ {}" .
then obtain m where "m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙" by auto
hence "m = (THE m. m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙)"
by(auto dest:obs_intra_the_element)
with ‹sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙›
‹obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ ≠ {}›
‹slice_kind S a = (λs. True)⇩√› ‹kind a = (Q)⇩√›
obtain x x' where "distance (targetnode a) m x"
"distance (sourcenode a) m (x + 1)"
and target:"targetnode a = (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') m x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = n')"
by(auto simp:slice_kind_def Let_def fun_eq_iff split:if_split_asm)
show ?thesis
proof(cases "distance (targetnode a') m x")
case False
with ‹sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹kind a' = (Q')⇩√›
‹m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙›
‹distance (targetnode a) m x› ‹distance (sourcenode a) m (x + 1)›
‹sourcenode a = sourcenode a'› show ?thesis
by(fastforce intro:slice_kind_Pred_obs_not_nearer)
next
case True
from ‹valid_edge a› ‹intra_kind(kind a)› ‹distance (targetnode a) m x›
‹distance (sourcenode a) m (x + 1)›
have ex1:"∃!a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') m x ∧ valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = (SOME nx. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') m x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = nx)"
by -(rule only_one_SOME_dist_edge)
have "targetnode a' ≠ (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') m x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = n')"
proof(rule ccontr)
assume "¬ targetnode a' ≠ (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') m x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = n')"
hence "targetnode a' = (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') m x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = n')"
by simp
with ex1 target ‹sourcenode a = sourcenode a'›
‹valid_edge a› ‹valid_edge a'› ‹intra_kind(kind a)› ‹intra_kind(kind a')›
‹distance (targetnode a) m x› ‹distance (sourcenode a) m (x + 1)›
have "a = a'" by auto
with ‹targetnode a ≠ targetnode a'› show False by simp
qed
with ‹sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙›
‹kind a' = (Q')⇩√› ‹m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙›
‹distance (targetnode a) m x› ‹distance (sourcenode a) m (x + 1)›
True ‹sourcenode a = sourcenode a'› show ?thesis
by(fastforce intro:slice_kind_Pred_obs_nearer_not_SOME)
qed
qed
qed
qed
lemma slice_deterministic:
assumes "valid_edge a" and "valid_edge a'"
and "intra_kind (kind a)" and "intra_kind (kind a')"
and "sourcenode a = sourcenode a'" and "targetnode a ≠ targetnode a'"
obtains Q Q' where "slice_kind S a = (Q)⇩√" and "slice_kind S a' = (Q')⇩√"
and "∀s. (Q s ⟶ ¬ Q' s) ∧ (Q' s ⟶ ¬ Q s)"
proof(atomize_elim)
from assms obtain Q Q'
where "kind a = (Q)⇩√" and "kind a' = (Q')⇩√"
and det:"∀s. (Q s ⟶ ¬ Q' s) ∧ (Q' s ⟶ ¬ Q s)"
by(auto dest:deterministic)
show "∃Q Q'. slice_kind S a = (Q)⇩√ ∧ slice_kind S a' = (Q')⇩√ ∧
(∀s. (Q s ⟶ ¬ Q' s) ∧ (Q' s ⟶ ¬ Q s))"
proof(cases "sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙")
case True
with ‹kind a = (Q)⇩√› have "slice_kind S a = (Q)⇩√"
by(simp add:slice_kind_def Let_def)
from True ‹kind a' = (Q')⇩√› ‹sourcenode a = sourcenode a'›
have "slice_kind S a' = (Q')⇩√"
by(simp add:slice_kind_def Let_def)
with ‹slice_kind S a = (Q)⇩√› det show ?thesis by blast
next
case False
with ‹kind a = (Q)⇩√›
have "slice_kind S a = (λs. True)⇩√ ∨ slice_kind S a = (λs. False)⇩√"
by(simp add:slice_kind_def Let_def)
thus ?thesis
proof
assume true:"slice_kind S a = (λs. True)⇩√"
with ‹sourcenode a = sourcenode a'› ‹targetnode a ≠ targetnode a'›
‹valid_edge a› ‹valid_edge a'› ‹intra_kind (kind a)› ‹intra_kind (kind a')›
have "slice_kind S a' = (λs. False)⇩√"
by(rule slice_kind_only_one_True_edge)
with true show ?thesis by simp
next
assume false:"slice_kind S a = (λs. False)⇩√"
from False ‹kind a' = (Q')⇩√› ‹sourcenode a = sourcenode a'›
have "slice_kind S a' = (λs. True)⇩√ ∨ slice_kind S a' = (λs. False)⇩√"
by(simp add:slice_kind_def Let_def)
with false show ?thesis by auto
qed
qed
qed
end
end