Up to index of Isabelle/HOL/Jinja/HRB-Slicing
theory Sliceheader {* \isaheader{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 \<rightharpoonup> 'val) => 'val option) list) => ((('var \<rightharpoonup> 'val) => 'val option) list)"
where "csppa m S x [] = []"
| "csppa m S x (f#fs) =
(if Formal_in(m,x) ∉ S then empty else f)#csppa m S (Suc x) fs"
definition cspp :: "'node => 'node SDG_node set =>
((('var \<rightharpoonup> 'val) => 'val option) list) => ((('var \<rightharpoonup> '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 = 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 \<rightharpoonup> 'val) => ('var \<rightharpoonup> 'val) => (nat => bool) =>
'var list => ('var \<rightharpoonup> '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 \<rightharpoonup> 'val) => ('var \<rightharpoonup> 'val) => ('var \<rightharpoonup> 'val)"
where "rspp m S xs f g ≡ map_merge f (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 "(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 "(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 \<Up>f = (if m ∈ ⌊S⌋⇘CFG⇙ then \<Up>f else \<Up>id)"
| "slice_kind_aux m m' S (Q)⇣\<surd> = (if m ∈ ⌊S⌋⇘CFG⇙ then (Q)⇣\<surd> 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)⇣\<surd> else (λcf. False)⇣\<surd>))
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)⇣\<surd> else (λcf. False)⇣\<surd>))))"
| "slice_kind_aux m m' S (Q:r\<hookrightarrow>⇘p⇙fs) = (if m ∈ ⌊S⌋⇘CFG⇙ then (Q:r\<hookrightarrow>⇘p⇙(cspp m' S fs))
else ((λcf. False):r\<hookrightarrow>⇘p⇙fs))"
| "slice_kind_aux m m' S (Q\<hookleftarrow>⇘p⇙f) = (if m ∈ ⌊S⌋⇘CFG⇙ then
(let outs = THE outs. ∃ins. (p,ins,outs) ∈ set procs in
(Q\<hookleftarrow>⇘p⇙(λcf cf'. rspp m' S outs cf' cf)))
else ((λcf. True)\<hookleftarrow>⇘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 = \<Up>f|] ==> slice_kind S a = \<Up>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)⇣\<surd>"
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)⇣\<surd>"
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)⇣\<surd>`
`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)⇣\<surd> else (λcf. False)⇣\<surd>)"
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)⇣\<surd>"
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)⇣\<surd>"
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)⇣\<surd>`
`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)⇣\<surd> else (λcf. False)⇣\<surd>)"
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)⇣\<surd>"
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)⇣\<surd>"
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)⇣\<surd>"
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)⇣\<surd>"
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)⇣\<surd>"
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)⇣\<surd>"
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)⇣\<surd>"
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)⇣\<surd>"
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)⇣\<surd>` 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)⇣\<surd>"
obtains Q' where "slice_kind S a = (Q')⇣\<surd>" and "Q' = (λs. False) ∨ Q' = (λs. True)"
proof(atomize_elim)
show "∃Q'. slice_kind S a = (Q')⇣\<surd> ∧ (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->⇣\<surd>* (_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)⇣\<surd>`
`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)⇣\<surd>"
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)⇣\<surd>`
`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)⇣\<surd>"
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)⇣\<surd>`
`obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {}` False
have "slice_kind S a = (λs. False)⇣\<surd>"
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)⇣\<surd>`
`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)⇣\<surd>"
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)⇣\<surd>`
`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)⇣\<surd>"
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)⇣\<surd>` False
`m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙`
have "slice_kind S a = (λs. False)⇣\<surd>"
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\<hookrightarrow>⇘p⇙fs|]
==> slice_kind S a = (λcf. False):r\<hookrightarrow>⇘p⇙fs"
by(simp add:slice_kind_def)
lemma slice_kind_Call_in_slice:
"[|sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙; kind a = Q:r\<hookrightarrow>⇘p⇙fs|]
==> slice_kind S a = Q:r\<hookrightarrow>⇘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\<hookrightarrow>⇘p⇙fs"
and "∀x < length fs. Formal_in(targetnode a,x) ∉ HRB_slice S"
shows "slice_kind S a = Q:r\<hookrightarrow>⇘p⇙replicate (length fs) empty"
proof -
from `sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙` `kind a = Q:r\<hookrightarrow>⇘p⇙fs`
have "slice_kind S a = Q:r\<hookrightarrow>⇘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) empty"
by(fastforce intro:nth_equalityI csppa_Formal_in_notin_slice simp:cspp_def)
with `slice_kind S a = Q:r\<hookrightarrow>⇘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\<hookrightarrow>⇘p⇙fs"
and "∀x < length fs. Formal_in(targetnode a,x) ∈ HRB_slice S"
shows "slice_kind S a = Q:r\<hookrightarrow>⇘p⇙fs"
proof -
from `sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙` `kind a = Q:r\<hookrightarrow>⇘p⇙fs`
have "slice_kind S a = Q:r\<hookrightarrow>⇘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\<hookrightarrow>⇘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\<hookrightarrow>⇘p⇙fs"
and "sourcenode a' = sourcenode a"
shows "slice_kind S a = (λs. True)⇣\<surd>"
proof -
from `valid_edge a'` `kind a' = Q:r\<hookrightarrow>⇘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)⇣\<surd>"
by(fastforce dest:call_return_node_edge)
from `valid_edge a'` `kind a' = Q:r\<hookrightarrow>⇘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)⇣\<surd>`
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->⇣\<surd>* (_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\<hookleftarrow>⇘px⇙fx"
hence "∀a'. valid_edge a' ∧ sourcenode a' = sourcenode ax -->
(∃Qx' fx'. kind a' = Qx'\<hookleftarrow>⇘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)⇣\<surd>`
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)⇣\<surd>`
`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\<hookleftarrow>⇘p⇙f|]
==> slice_kind S a = (λcf. True)\<hookleftarrow>⇘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\<hookleftarrow>⇘p⇙f;
(p,ins,outs) ∈ set procs|]
==> slice_kind S a = Q\<hookleftarrow>⇘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\<hookrightarrow>⇘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)⇣\<surd>"
shows "slice_kind S a' = (λs. False)⇣\<surd>"
proof -
from assms obtain Q Q' where "kind a = (Q)⇣\<surd>"
and "kind a' = (Q')⇣\<surd>" 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)⇣\<surd>` `kind a = (Q)⇣\<surd>` 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')⇣\<surd>` `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)⇣\<surd>`
`kind a = (Q)⇣\<surd>`
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:split_if_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')⇣\<surd>`
`sourcenode a = sourcenode a'` mex dist
show ?thesis by(auto dest:distance_det
simp:slice_kind_def Let_def fun_eq_iff split:split_if_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)⇣\<surd>` `kind a = (Q)⇣\<surd>`
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:split_if_asm)
show ?thesis
proof(cases "distance (targetnode a') m x")
case False
with `sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙` `kind a' = (Q')⇣\<surd>`
`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')⇣\<surd>` `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)⇣\<surd>" and "slice_kind S a' = (Q')⇣\<surd>"
and "∀s. (Q s --> ¬ Q' s) ∧ (Q' s --> ¬ Q s)"
proof(atomize_elim)
from assms obtain Q Q'
where "kind a = (Q)⇣\<surd>" and "kind a' = (Q')⇣\<surd>"
and det:"∀s. (Q s --> ¬ Q' s) ∧ (Q' s --> ¬ Q s)"
by(auto dest:deterministic)
show "∃Q Q'. slice_kind S a = (Q)⇣\<surd> ∧ slice_kind S a' = (Q')⇣\<surd> ∧
(∀s. (Q s --> ¬ Q' s) ∧ (Q' s --> ¬ Q s))"
proof(cases "sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙")
case True
with `kind a = (Q)⇣\<surd>` have "slice_kind S a = (Q)⇣\<surd>"
by(simp add:slice_kind_def Let_def)
from True `kind a' = (Q')⇣\<surd>` `sourcenode a = sourcenode a'`
have "slice_kind S a' = (Q')⇣\<surd>"
by(simp add:slice_kind_def Let_def)
with `slice_kind S a = (Q)⇣\<surd>` det show ?thesis by blast
next
case False
with `kind a = (Q)⇣\<surd>`
have "slice_kind S a = (λs. True)⇣\<surd> ∨ slice_kind S a = (λs. False)⇣\<surd>"
by(simp add:slice_kind_def Let_def)
thus ?thesis
proof
assume true:"slice_kind S a = (λs. True)⇣\<surd>"
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)⇣\<surd>"
by(rule slice_kind_only_one_True_edge)
with true show ?thesis by simp
next
assume false:"slice_kind S a = (λs. False)⇣\<surd>"
from False `kind a' = (Q')⇣\<surd>` `sourcenode a = sourcenode a'`
have "slice_kind S a' = (λs. True)⇣\<surd> ∨ slice_kind S a' = (λs. False)⇣\<surd>"
by(simp add:slice_kind_def Let_def)
with false show ?thesis by auto
qed
qed
qed
end
end