Up to index of Isabelle/HOL/Jinja/Slicing
theory LiftingIntraheader {* \isaheader{Framework Graph Lifting for Noninterference} *}
theory LiftingIntra
imports NonInterferenceIntra "../Slicing/StaticIntra/CDepInstantiations"
begin
text {* In this section, we show how a valid CFG from the slicing framework in
\cite{Wasserrab:08} can be lifted to fulfil all properties of the
@{text "NonInterferenceIntraGraph"} locale. Basically, we redefine the
hitherto existing @{text Entry} and @{text Exit} nodes as new
@{text High} and @{text Low} nodes, and introduce two new nodes
@{text NewEntry} and @{text NewExit}. Then, we have to lift all functions
to operate on this new graph. *}
subsection {* Liftings *}
subsubsection {* The datatypes *}
datatype 'node LDCFG_node = Node 'node
| NewEntry
| NewExit
type_synonym ('edge,'node,'state) LDCFG_edge =
"'node LDCFG_node × ('state edge_kind) × 'node LDCFG_node"
subsubsection {* Lifting @{term valid_edge} *}
inductive lift_valid_edge :: "('edge => bool) => ('edge => 'node) => ('edge => 'node) =>
('edge => 'state edge_kind) => 'node => 'node => ('edge,'node,'state) LDCFG_edge =>
bool"
for valid_edge::"'edge => bool" and src::"'edge => 'node" and trg::"'edge => 'node"
and knd::"'edge => 'state edge_kind" and E::'node and X::'node
where lve_edge:
"[|valid_edge a; src a ≠ E ∨ trg a ≠ X;
e = (Node (src a),knd a,Node (trg a))|]
==> lift_valid_edge valid_edge src trg knd E X e"
| lve_Entry_edge:
"e = (NewEntry,(λs. True)⇣\<surd>,Node E)
==> lift_valid_edge valid_edge src trg knd E X e"
| lve_Exit_edge:
"e = (Node X,(λs. True)⇣\<surd>,NewExit)
==> lift_valid_edge valid_edge src trg knd E X e"
| lve_Entry_Exit_edge:
"e = (NewEntry,(λs. False)⇣\<surd>,NewExit)
==> lift_valid_edge valid_edge src trg knd E X e"
lemma [simp]:"¬ lift_valid_edge valid_edge src trg knd E X (Node E,et,Node X)"
by(auto elim:lift_valid_edge.cases)
subsubsection {* Lifting @{term Def} and @{term Use} sets *}
inductive_set lift_Def_set :: "('node => 'var set) => 'node => 'node =>
'var set => 'var set => ('node LDCFG_node × 'var) set"
for Def::"('node => 'var set)" and E::'node and X::'node
and H::"'var set" and L::"'var set"
where lift_Def_node:
"V ∈ Def n ==> (Node n,V) ∈ lift_Def_set Def E X H L"
| lift_Def_High:
"V ∈ H ==> (Node E,V) ∈ lift_Def_set Def E X H L"
abbreviation lift_Def :: "('node => 'var set) => 'node => 'node =>
'var set => 'var set => 'node LDCFG_node => 'var set"
where "lift_Def Def E X H L n ≡ {V. (n,V) ∈ lift_Def_set Def E X H L}"
inductive_set lift_Use_set :: "('node => 'var set) => 'node => 'node =>
'var set => 'var set => ('node LDCFG_node × 'var) set"
for Use::"'node => 'var set" and E::'node and X::'node
and H::"'var set" and L::"'var set"
where
lift_Use_node:
"V ∈ Use n ==> (Node n,V) ∈ lift_Use_set Use E X H L"
| lift_Use_High:
"V ∈ H ==> (Node E,V) ∈ lift_Use_set Use E X H L"
| lift_Use_Low:
"V ∈ L ==> (Node X,V) ∈ lift_Use_set Use E X H L"
abbreviation lift_Use :: "('node => 'var set) => 'node => 'node =>
'var set => 'var set => 'node LDCFG_node => 'var set"
where "lift_Use Use E X H L n ≡ {V. (n,V) ∈ lift_Use_set Use E X H L}"
subsection {* The lifting lemmas *}
subsubsection {* Lifting the basic locales *}
abbreviation src :: "('edge,'node,'state) LDCFG_edge => 'node LDCFG_node"
where "src a ≡ fst a"
abbreviation trg :: "('edge,'node,'state) LDCFG_edge => 'node LDCFG_node"
where "trg a ≡ snd(snd a)"
definition knd :: "('edge,'node,'state) LDCFG_edge => 'state edge_kind"
where "knd a ≡ fst(snd a)"
lemma lift_CFG:
assumes wf:"CFGExit_wf sourcenode targetnode kind valid_edge Entry Def Use
state_val Exit"
shows "CFG src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) NewEntry"
proof -
interpret CFGExit_wf sourcenode targetnode kind valid_edge Entry Def Use
state_val Exit
by(rule wf)
show ?thesis
proof
fix a assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
and "trg a = NewEntry"
thus False by(fastforce elim:lift_valid_edge.cases)
next
fix a a'
assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
and "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a'"
and "src a = src a'" and "trg a = trg a'"
thus "a = a'"
proof(induct rule:lift_valid_edge.induct)
case lve_edge thus ?case by -(erule lift_valid_edge.cases,auto dest:edge_det)
qed(auto elim:lift_valid_edge.cases)
qed
qed
lemma lift_CFG_wf:
assumes wf:"CFGExit_wf sourcenode targetnode kind valid_edge Entry Def Use
state_val Exit"
shows "CFG_wf src trg knd
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) NewEntry
(lift_Def Def Entry Exit H L) (lift_Use Use Entry Exit H L) state_val"
proof -
interpret CFGExit_wf sourcenode targetnode kind valid_edge Entry Def Use
state_val Exit
by(rule wf)
interpret CFG:CFG src trg knd
"lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit" NewEntry
by(fastforce intro:lift_CFG wf)
show ?thesis
proof
show "lift_Def Def Entry Exit H L NewEntry = {} ∧
lift_Use Use Entry Exit H L NewEntry = {}"
by(fastforce elim:lift_Use_set.cases lift_Def_set.cases)
next
fix a V s
assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
and "V ∉ lift_Def Def Entry Exit H L (src a)" and "pred (knd a) s"
thus "state_val (transfer (knd a) s) V = state_val s V"
proof(induct rule:lift_valid_edge.induct)
case lve_edge
thus ?case by(fastforce intro:CFG_edge_no_Def_equal dest:lift_Def_node[of _ Def]
simp:knd_def)
qed(auto simp:knd_def)
next
fix a s s'
assume assms:"lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
"∀V∈lift_Use Use Entry Exit H L (src a). state_val s V = state_val s' V"
"pred (knd a) s" "pred (knd a) s'"
show "∀V∈lift_Def Def Entry Exit H L (src a).
state_val (transfer (knd a) s) V = state_val (transfer (knd a) s') V"
proof
fix V assume "V ∈ lift_Def Def Entry Exit H L (src a)"
with assms
show "state_val (transfer (knd a) s) V = state_val (transfer (knd a) s') V"
proof(induct rule:lift_valid_edge.induct)
case (lve_edge a e)
show ?case
proof (cases "Node (sourcenode a) = Node Entry")
case True
hence "sourcenode a = Entry" by simp
from Entry_Exit_edge obtain a' where "valid_edge a'"
and "sourcenode a' = Entry" and "targetnode a' = Exit"
and "kind a' = (λs. False)⇣\<surd>" by blast
have "∃Q. kind a = (Q)⇣\<surd>"
proof(cases "targetnode a = Exit")
case True
with `valid_edge a` `valid_edge a'` `sourcenode a = Entry`
`sourcenode a' = Entry` `targetnode a' = Exit`
have "a = a'" by(fastforce dest:edge_det)
with `kind a' = (λs. False)⇣\<surd>` show ?thesis by simp
next
case False
with `valid_edge a` `valid_edge a'` `sourcenode a = Entry`
`sourcenode a' = Entry` `targetnode a' = Exit`
show ?thesis by(auto dest:deterministic)
qed
from True `V ∈ lift_Def Def Entry Exit H L (src e)` Entry_empty
`e = (Node (sourcenode a), kind a, Node (targetnode a))`
have "V ∈ H" by(fastforce elim:lift_Def_set.cases)
from True `e = (Node (sourcenode a), kind a, Node (targetnode a))`
`sourcenode a ≠ Entry ∨ targetnode a ≠ Exit`
have "∀V∈H. V ∈ lift_Use Use Entry Exit H L (src e)"
by(fastforce intro:lift_Use_High)
with `∀V∈lift_Use Use Entry Exit H L (src e).
state_val s V = state_val s' V` `V ∈ H`
have "state_val s V = state_val s' V" by simp
with `e = (Node (sourcenode a), kind a, Node (targetnode a))`
`∃Q. kind a = (Q)⇣\<surd>`
show ?thesis by(fastforce simp:knd_def)
next
case False
{ fix V' assume "V' ∈ Use (sourcenode a)"
with `e = (Node (sourcenode a), kind a, Node (targetnode a))`
have "V' ∈ lift_Use Use Entry Exit H L (src e)"
by(fastforce intro:lift_Use_node)
}
with `∀V∈lift_Use Use Entry Exit H L (src e).
state_val s V = state_val s' V`
have "∀V∈Use (sourcenode a). state_val s V = state_val s' V"
by fastforce
from `valid_edge a` this `pred (knd e) s` `pred (knd e) s'`
`e = (Node (sourcenode a), kind a, Node (targetnode a))`
have "∀V ∈ Def (sourcenode a). state_val (transfer (kind a) s) V =
state_val (transfer (kind a) s') V"
by -(erule CFG_edge_transfer_uses_only_Use,auto simp:knd_def)
from `V ∈ lift_Def Def Entry Exit H L (src e)` False
`e = (Node (sourcenode a), kind a, Node (targetnode a))`
have "V ∈ Def (sourcenode a)" by(fastforce elim:lift_Def_set.cases)
with `∀V ∈ Def (sourcenode a). state_val (transfer (kind a) s) V =
state_val (transfer (kind a) s') V`
`e = (Node (sourcenode a), kind a, Node (targetnode a))`
show ?thesis by(simp add:knd_def)
qed
next
case (lve_Entry_edge e)
from `V ∈ lift_Def Def Entry Exit H L (src e)`
`e = (NewEntry, (λs. True)⇣\<surd>, Node Entry)`
have False by(fastforce elim:lift_Def_set.cases)
thus ?case by simp
next
case (lve_Exit_edge e)
from `V ∈ lift_Def Def Entry Exit H L (src e)`
`e = (Node Exit, (λs. True)⇣\<surd>, NewExit)`
have False
by(fastforce elim:lift_Def_set.cases intro!:Entry_noteq_Exit simp:Exit_empty)
thus ?case by simp
qed(simp add:knd_def)
qed
next
fix a s s'
assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
and "pred (knd a) s"
and "∀V∈lift_Use Use Entry Exit H L (src a). state_val s V = state_val s' V"
thus "pred (knd a) s'"
by(induct rule:lift_valid_edge.induct,
auto elim!:CFG_edge_Uses_pred_equal dest:lift_Use_node simp:knd_def)
next
fix a a'
assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
and "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a'"
and "src a = src a'" and "trg a ≠ trg a'"
thus "∃Q Q'. knd a = (Q)⇣\<surd> ∧ knd a' = (Q')⇣\<surd> ∧
(∀s. (Q s --> ¬ Q' s) ∧ (Q' s --> ¬ Q s))"
proof(induct rule:lift_valid_edge.induct)
case (lve_edge a e)
from `lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a'`
`valid_edge a` `e = (Node (sourcenode a), kind a, Node (targetnode a))`
`src e = src a'` `trg e ≠ trg a'`
show ?case
proof(induct rule:lift_valid_edge.induct)
case lve_edge thus ?case by(auto dest:deterministic simp:knd_def)
next
case (lve_Exit_edge e')
from `e = (Node (sourcenode a), kind a, Node (targetnode a))`
`e' = (Node Exit, (λs. True)⇣\<surd>, NewExit)` `src e = src e'`
have "sourcenode a = Exit" by simp
with `valid_edge a` have False by(rule Exit_source)
thus ?case by simp
qed auto
qed (fastforce elim:lift_valid_edge.cases simp:knd_def)+
qed
qed
lemma lift_CFGExit:
assumes wf:"CFGExit_wf sourcenode targetnode kind valid_edge Entry Def Use
state_val Exit"
shows "CFGExit src trg knd
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
NewEntry NewExit"
proof -
interpret CFGExit_wf sourcenode targetnode kind valid_edge Entry Def Use
state_val Exit
by(rule wf)
interpret CFG:CFG src trg knd
"lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit" NewEntry
by(fastforce intro:lift_CFG wf)
show ?thesis
proof
fix a assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
and "src a = NewExit"
thus False by(fastforce elim:lift_valid_edge.cases)
next
from lve_Entry_Exit_edge
show "∃a. lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a ∧
src a = NewEntry ∧ trg a = NewExit ∧ knd a = (λs. False)⇣\<surd>"
by(fastforce simp:knd_def)
qed
qed
lemma lift_CFGExit_wf:
assumes wf:"CFGExit_wf sourcenode targetnode kind valid_edge Entry Def Use
state_val Exit"
shows "CFGExit_wf src trg knd
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) NewEntry
(lift_Def Def Entry Exit H L) (lift_Use Use Entry Exit H L) state_val NewExit"
proof -
interpret CFGExit_wf sourcenode targetnode kind valid_edge Entry Def Use
state_val Exit
by(rule wf)
interpret CFGExit:CFGExit src trg knd
"lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit"
NewEntry NewExit
by(fastforce intro:lift_CFGExit wf)
interpret CFG_wf:CFG_wf src trg knd
"lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit"
NewEntry "lift_Def Def Entry Exit H L" "lift_Use Use Entry Exit H L" state_val
by(fastforce intro:lift_CFG_wf wf)
show ?thesis
proof
show "lift_Def Def Entry Exit H L NewExit = {} ∧
lift_Use Use Entry Exit H L NewExit = {}"
by(fastforce elim:lift_Use_set.cases lift_Def_set.cases)
qed
qed
subsubsection {* Lifting @{term wod_backward_slice} *}
lemma lift_wod_backward_slice:
fixes valid_edge and sourcenode and targetnode and kind and Entry and Exit
and Def and Use and H and L
defines lve:"lve ≡ lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit"
and lDef:"lDef ≡ lift_Def Def Entry Exit H L"
and lUse:"lUse ≡ lift_Use Use Entry Exit H L"
assumes wf:"CFGExit_wf sourcenode targetnode kind valid_edge Entry Def Use
state_val Exit"
and "H ∩ L = {}" and "H ∪ L = UNIV"
shows "NonInterferenceIntraGraph src trg knd lve NewEntry lDef lUse state_val
(CFG_wf.wod_backward_slice src trg lve lDef lUse)
NewExit H L (Node Entry) (Node Exit)"
proof -
interpret CFGExit_wf sourcenode targetnode kind valid_edge Entry Def Use
state_val Exit
by(rule wf)
interpret CFGExit_wf:
CFGExit_wf src trg knd lve NewEntry lDef lUse state_val NewExit
by(fastforce intro:lift_CFGExit_wf wf simp:lve lDef lUse)
from wf lve have CFG:"CFG src trg lve NewEntry"
by(fastforce intro:lift_CFG)
from wf lve lDef lUse have CFG_wf:"CFG_wf src trg knd lve NewEntry
lDef lUse state_val"
by(fastforce intro:lift_CFG_wf)
show ?thesis
proof
fix n S
assume "n ∈ CFG_wf.wod_backward_slice src trg lve lDef lUse S"
with CFG_wf show "CFG.valid_node src trg lve n"
by -(rule CFG_wf.wod_backward_slice_valid_node)
next
fix n S assume "CFG.valid_node src trg lve n" and "n ∈ S"
with CFG_wf show "n ∈ CFG_wf.wod_backward_slice src trg lve lDef lUse S"
by -(rule CFG_wf.refl)
next
fix n' S n V
assume "n' ∈ CFG_wf.wod_backward_slice src trg lve lDef lUse S"
and "CFG_wf.data_dependence src trg lve lDef lUse n V n'"
with CFG_wf show "n ∈ CFG_wf.wod_backward_slice src trg lve lDef lUse S"
by -(rule CFG_wf.dd_closed)
next
fix n S
from CFG_wf
have "(∃m. (CFG.obs src trg lve n
(CFG_wf.wod_backward_slice src trg lve lDef lUse S)) = {m}) ∨
CFG.obs src trg lve n (CFG_wf.wod_backward_slice src trg lve lDef lUse S) = {}"
by(rule CFG_wf.obs_singleton)
thus "finite
(CFG.obs src trg lve n (CFG_wf.wod_backward_slice src trg lve lDef lUse S))"
by fastforce
next
fix n S
from CFG_wf
have "(∃m. (CFG.obs src trg lve n
(CFG_wf.wod_backward_slice src trg lve lDef lUse S)) = {m}) ∨
CFG.obs src trg lve n (CFG_wf.wod_backward_slice src trg lve lDef lUse S) = {}"
by(rule CFG_wf.obs_singleton)
thus "card (CFG.obs src trg lve n
(CFG_wf.wod_backward_slice src trg lve lDef lUse S)) ≤ 1"
by fastforce
next
fix a assume "lve a" and "src a = NewEntry"
with lve show "trg a = NewExit ∨ trg a = Node Entry"
by(fastforce elim:lift_valid_edge.cases)
next
from lve_Entry_edge lve
show "∃a. lve a ∧ src a = NewEntry ∧ trg a = Node Entry ∧ knd a = (λs. True)⇣\<surd>"
by(fastforce simp:knd_def)
next
fix a assume "lve a" and "trg a = Node Entry"
with lve show "src a = NewEntry" by(fastforce elim:lift_valid_edge.cases)
next
fix a assume "lve a" and "trg a = NewExit"
with lve show "src a = NewEntry ∨ src a = Node Exit"
by(fastforce elim:lift_valid_edge.cases)
next
from lve_Exit_edge lve
show "∃a. lve a ∧ src a = Node Exit ∧ trg a = NewExit ∧ knd a = (λs. True)⇣\<surd>"
by(fastforce simp:knd_def)
next
fix a assume "lve a" and "src a = Node Exit"
with lve show "trg a = NewExit" by(fastforce elim:lift_valid_edge.cases)
next
from lDef show "lDef (Node Entry) = H"
by(fastforce elim:lift_Def_set.cases intro:lift_Def_High)
next
from Entry_noteq_Exit lUse show "lUse (Node Entry) = H"
by(fastforce elim:lift_Use_set.cases intro:lift_Use_High)
next
from Entry_noteq_Exit lUse show "lUse (Node Exit) = L"
by(fastforce elim:lift_Use_set.cases intro:lift_Use_Low)
next
from `H ∩ L = {}` show "H ∩ L = {}" .
next
from `H ∪ L = UNIV` show "H ∪ L = UNIV" .
qed
qed
subsubsection {* Lifting @{text PDG_BS} with @{text standard_control_dependence} *}
lemma lift_Postdomination:
assumes wf:"CFGExit_wf sourcenode targetnode kind valid_edge Entry Def Use
state_val Exit"
and pd:"Postdomination sourcenode targetnode kind valid_edge Entry Exit"
and inner:"CFGExit.inner_node sourcenode targetnode valid_edge Entry Exit nx"
shows "Postdomination src trg knd
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) NewEntry NewExit"
proof -
interpret Postdomination sourcenode targetnode kind valid_edge Entry Exit
by(rule pd)
interpret CFGExit_wf:CFGExit_wf src trg knd
"lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit" NewEntry
"lift_Def Def Entry Exit H L" "lift_Use Use Entry Exit H L" state_val NewExit
by(fastforce intro:lift_CFGExit_wf wf)
from wf have CFG:"CFG src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) NewEntry"
by(rule lift_CFG)
show ?thesis
proof
fix n assume "CFG.valid_node src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) n"
show "∃as. CFG.path src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
NewEntry as n"
proof(cases n)
case NewEntry
have "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit
(NewEntry,(λs. False)⇣\<surd>,NewExit)" by(fastforce intro:lve_Entry_Exit_edge)
with NewEntry have "CFG.path src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
NewEntry [] n"
by(fastforce intro:CFG.empty_path[OF CFG] simp:CFG.valid_node_def[OF CFG])
thus ?thesis by blast
next
case NewExit
have "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit
(NewEntry,(λs. False)⇣\<surd>,NewExit)" by(fastforce intro:lve_Entry_Exit_edge)
with NewExit have "CFG.path src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
NewEntry [(NewEntry,(λs. False)⇣\<surd>,NewExit)] n"
by(fastforce intro:CFG.Cons_path[OF CFG] CFG.empty_path[OF CFG]
simp:CFG.valid_node_def[OF CFG])
thus ?thesis by blast
next
case (Node m)
with Entry_Exit_edge `CFG.valid_node src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) n`
have "valid_node m"
by(auto elim:lift_valid_edge.cases
simp:CFG.valid_node_def[OF CFG] valid_node_def)
thus ?thesis
proof(cases m rule:valid_node_cases)
case Entry
have "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit
(NewEntry,(λs. True)⇣\<surd>,Node Entry)" by(fastforce intro:lve_Entry_edge)
with Entry Node have "CFG.path src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
NewEntry [(NewEntry,(λs. True)⇣\<surd>,Node Entry)] n"
by(fastforce intro:CFG.Cons_path[OF CFG] CFG.empty_path[OF CFG]
simp:CFG.valid_node_def[OF CFG])
thus ?thesis by blast
next
case Exit
from inner obtain ax where "valid_edge ax" and "inner_node (sourcenode ax)"
and "targetnode ax = Exit" by(erule inner_node_Exit_edge)
hence "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit
(Node (sourcenode ax),kind ax,Node Exit)"
by(auto intro:lift_valid_edge.lve_edge simp:inner_node_def)
hence path:"CFG.path src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(Node (sourcenode ax)) [(Node (sourcenode ax),kind ax,Node Exit)]
(Node Exit)"
by(fastforce intro:CFG.Cons_path[OF CFG] CFG.empty_path[OF CFG]
simp:CFG.valid_node_def[OF CFG])
have edge:"lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit
(NewEntry,(λs. True)⇣\<surd>,Node Entry)" by(fastforce intro:lve_Entry_edge)
from `inner_node (sourcenode ax)` have "valid_node (sourcenode ax)"
by(rule inner_is_valid)
then obtain asx where "Entry -asx->* sourcenode ax"
by(fastforce dest:Entry_path)
from this `valid_edge ax` have "∃es. CFG.path src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(Node Entry) es (Node (sourcenode ax))"
proof(induct asx arbitrary:ax rule:rev_induct)
case Nil
from `Entry -[]->* sourcenode ax` have "sourcenode ax = Entry" by fastforce
hence "CFG.path src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(Node Entry) [] (Node (sourcenode ax))"
apply simp apply(rule CFG.empty_path[OF CFG])
by(auto intro:lve_Entry_edge simp:CFG.valid_node_def[OF CFG])
thus ?case by blast
next
case (snoc x xs)
note IH = `!!ax. [|Entry -xs->* sourcenode ax; valid_edge ax|] ==>
∃es. CFG.path src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(Node Entry) es (Node (sourcenode ax))`
from `Entry -xs@[x]->* sourcenode ax`
have "Entry -xs->* sourcenode x" and "valid_edge x"
and "targetnode x = sourcenode ax" by(auto elim:path_split_snoc)
{ assume "targetnode x = Exit"
with `valid_edge ax` `targetnode x = sourcenode ax`
have False by -(rule Exit_source,simp+) }
hence "targetnode x ≠ Exit" by clarsimp
with `valid_edge x` `targetnode x = sourcenode ax`[THEN sym]
have "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit
(Node (sourcenode x),kind x,Node (sourcenode ax))"
by(fastforce intro:lift_valid_edge.lve_edge)
hence path:"CFG.path src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(Node (sourcenode x)) [(Node (sourcenode x),kind x,Node (sourcenode ax))]
(Node (sourcenode ax))"
by(fastforce intro:CFG.Cons_path[OF CFG] CFG.empty_path[OF CFG]
simp:CFG.valid_node_def[OF CFG])
from IH[OF `Entry -xs->* sourcenode x` `valid_edge x`] obtain es
where "CFG.path src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(Node Entry) es (Node (sourcenode x))" by blast
with path have "CFG.path src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(Node Entry) (es@[(Node (sourcenode x),kind x,Node (sourcenode ax))])
(Node (sourcenode ax))"
by -(rule CFG.path_Append[OF CFG])
thus ?case by blast
qed
then obtain es where "CFG.path src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(Node Entry) es (Node (sourcenode ax))" by blast
with path have "CFG.path src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(Node Entry) (es@ [(Node (sourcenode ax),kind ax,Node Exit)]) (Node Exit)"
by -(rule CFG.path_Append[OF CFG])
with edge have "CFG.path src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
NewEntry ((NewEntry,(λs. True)⇣\<surd>,Node Entry)#
(es@ [(Node (sourcenode ax),kind ax,Node Exit)])) (Node Exit)"
by(fastforce intro:CFG.Cons_path[OF CFG])
with Node Exit show ?thesis by fastforce
next
case inner
from `valid_node m` obtain as where "Entry -as->* m"
by(fastforce dest:Entry_path)
with inner have "∃es. CFG.path src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(Node Entry) es (Node m)"
proof(induct arbitrary:m rule:rev_induct)
case Nil
from `Entry -[]->* m`
have "m = Entry" by fastforce
with lve_Entry_edge have "CFG.path src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(Node Entry) [] (Node m)"
by(fastforce intro:CFG.empty_path[OF CFG] simp:CFG.valid_node_def[OF CFG])
thus ?case by blast
next
case (snoc x xs)
note IH = `!!m. [|inner_node m; Entry -xs->* m|]
==> ∃es. CFG.path src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(Node Entry) es (Node m)`
from `Entry -xs@[x]->* m` have "Entry -xs->* sourcenode x"
and "valid_edge x" and "m = targetnode x" by(auto elim:path_split_snoc)
with `inner_node m`
have edge:"lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit
(Node (sourcenode x),kind x,Node m)"
by(fastforce intro:lve_edge simp:inner_node_def)
hence path:"CFG.path src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(Node (sourcenode x)) [(Node (sourcenode x),kind x,Node m)] (Node m)"
by(fastforce intro:CFG.Cons_path[OF CFG] CFG.empty_path[OF CFG]
simp:CFG.valid_node_def[OF CFG])
from `valid_edge x` have "valid_node (sourcenode x)" by simp
thus ?case
proof(cases "sourcenode x" rule:valid_node_cases)
case Entry
with edge have "CFG.path src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(Node Entry) [(Node Entry,kind x,Node m)] (Node m)"
apply - apply(rule CFG.Cons_path[OF CFG])
apply(rule CFG.empty_path[OF CFG])
by(auto simp:CFG.valid_node_def[OF CFG])
thus ?thesis by blast
next
case Exit
with `valid_edge x` have False by(rule Exit_source)
thus ?thesis by simp
next
case inner
from IH[OF this `Entry -xs->* sourcenode x`] obtain es
where "CFG.path src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(Node Entry) es (Node (sourcenode x))" by blast
with path have "CFG.path src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(Node Entry) (es@[(Node (sourcenode x),kind x,Node m)]) (Node m)"
by -(rule CFG.path_Append[OF CFG])
thus ?thesis by blast
qed
qed
then obtain es where path:"CFG.path src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(Node Entry) es (Node m)" by blast
have "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit
(NewEntry,(λs. True)⇣\<surd>,Node Entry)" by(fastforce intro:lve_Entry_edge)
from this path Node have "CFG.path src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
NewEntry ((NewEntry,(λs. True)⇣\<surd>,Node Entry)#es) n"
by(fastforce intro:CFG.Cons_path[OF CFG])
thus ?thesis by blast
qed
qed
next
fix n assume "CFG.valid_node src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) n"
show "∃as. CFG.path src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
n as NewExit"
proof(cases n)
case NewEntry
have "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit
(NewEntry,(λs. False)⇣\<surd>,NewExit)" by(fastforce intro:lve_Entry_Exit_edge)
with NewEntry have "CFG.path src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
n [(NewEntry,(λs. False)⇣\<surd>,NewExit)] NewExit"
by(fastforce intro:CFG.Cons_path[OF CFG] CFG.empty_path[OF CFG]
simp:CFG.valid_node_def[OF CFG])
thus ?thesis by blast
next
case NewExit
have "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit
(NewEntry,(λs. False)⇣\<surd>,NewExit)" by(fastforce intro:lve_Entry_Exit_edge)
with NewExit have "CFG.path src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
n [] NewExit"
by(fastforce intro:CFG.empty_path[OF CFG] simp:CFG.valid_node_def[OF CFG])
thus ?thesis by blast
next
case (Node m)
with Entry_Exit_edge `CFG.valid_node src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) n`
have "valid_node m"
by(auto elim:lift_valid_edge.cases
simp:CFG.valid_node_def[OF CFG] valid_node_def)
thus ?thesis
proof(cases m rule:valid_node_cases)
case Entry
from inner obtain ax where "valid_edge ax" and "inner_node (targetnode ax)"
and "sourcenode ax = Entry" by(erule inner_node_Entry_edge)
hence edge:"lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit
(Node Entry,kind ax,Node (targetnode ax))"
by(auto intro:lift_valid_edge.lve_edge simp:inner_node_def)
have "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit
(Node Exit,(λs. True)⇣\<surd>,NewExit)" by(fastforce intro:lve_Exit_edge)
hence path:"CFG.path src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(Node Exit) [(Node Exit,(λs. True)⇣\<surd>,NewExit)] (NewExit)"
by(fastforce intro:CFG.Cons_path[OF CFG] CFG.empty_path[OF CFG]
simp:CFG.valid_node_def[OF CFG])
from `inner_node (targetnode ax)` have "valid_node (targetnode ax)"
by(rule inner_is_valid)
then obtain asx where "targetnode ax -asx->* Exit" by(fastforce dest:Exit_path)
from this `valid_edge ax` have "∃es. CFG.path src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(Node (targetnode ax)) es (Node Exit)"
proof(induct asx arbitrary:ax)
case Nil
from `targetnode ax -[]->* Exit` have "targetnode ax = Exit" by fastforce
hence "CFG.path src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(Node (targetnode ax)) [] (Node Exit)"
apply simp apply(rule CFG.empty_path[OF CFG])
by(auto intro:lve_Exit_edge simp:CFG.valid_node_def[OF CFG])
thus ?case by blast
next
case (Cons x xs)
note IH = `!!ax. [|targetnode ax -xs->* Exit; valid_edge ax|] ==>
∃es. CFG.path src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(Node (targetnode ax)) es (Node Exit)`
from `targetnode ax -x#xs->* Exit`
have "targetnode x -xs->* Exit" and "valid_edge x"
and "sourcenode x = targetnode ax" by(auto elim:path_split_Cons)
{ assume "sourcenode x = Entry"
with `valid_edge ax` `sourcenode x = targetnode ax`
have False by -(rule Entry_target,simp+) }
hence "sourcenode x ≠ Entry" by clarsimp
with `valid_edge x` `sourcenode x = targetnode ax`[THEN sym]
have edge:"lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit
(Node (targetnode ax),kind x,Node (targetnode x))"
by(fastforce intro:lift_valid_edge.lve_edge)
from IH[OF `targetnode x -xs->* Exit` `valid_edge x`] obtain es
where "CFG.path src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(Node (targetnode x)) es (Node Exit)" by blast
with edge have "CFG.path src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(Node (targetnode ax))
((Node (targetnode ax),kind x,Node (targetnode x))#es) (Node Exit)"
by(fastforce intro:CFG.Cons_path[OF CFG])
thus ?case by blast
qed
then obtain es where "CFG.path src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(Node (targetnode ax)) es (Node Exit)" by blast
with edge have "CFG.path src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(Node Entry) ((Node Entry, kind ax, Node (targetnode ax))#es) (Node Exit)"
by(fastforce intro:CFG.Cons_path[OF CFG])
with path have "CFG.path src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(Node Entry) (((Node Entry,kind ax,Node (targetnode ax))#es)@
[(Node Exit, (λs. True)⇣\<surd>, NewExit)]) NewExit"
by -(rule CFG.path_Append[OF CFG])
with Node Entry show ?thesis by fastforce
next
case Exit
have "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit
(Node Exit,(λs. True)⇣\<surd>,NewExit)" by(fastforce intro:lve_Exit_edge)
with Exit Node have "CFG.path src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
n [(Node Exit,(λs. True)⇣\<surd>,NewExit)] NewExit"
by(fastforce intro:CFG.Cons_path[OF CFG] CFG.empty_path[OF CFG]
simp:CFG.valid_node_def[OF CFG])
thus ?thesis by blast
next
case inner
from `valid_node m` obtain as where "m -as->* Exit"
by(fastforce dest:Exit_path)
with inner have "∃es. CFG.path src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(Node m) es (Node Exit)"
proof(induct as arbitrary:m)
case Nil
from `m -[]->* Exit`
have "m = Exit" by fastforce
with lve_Exit_edge have "CFG.path src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(Node m) [] (Node Exit)"
by(fastforce intro:CFG.empty_path[OF CFG] simp:CFG.valid_node_def[OF CFG])
thus ?case by blast
next
case (Cons x xs)
note IH = `!!m. [|inner_node m; m -xs->* Exit|]
==> ∃es. CFG.path src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(Node m) es (Node Exit)`
from `m -x#xs->* Exit` have "targetnode x -xs->* Exit"
and "valid_edge x" and "m = sourcenode x" by(auto elim:path_split_Cons)
with `inner_node m`
have edge:"lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit
(Node m,kind x,Node (targetnode x))"
by(fastforce intro:lve_edge simp:inner_node_def)
from `valid_edge x` have "valid_node (targetnode x)" by simp
thus ?case
proof(cases "targetnode x" rule:valid_node_cases)
case Entry
with `valid_edge x` have False by(rule Entry_target)
thus ?thesis by simp
next
case Exit
with edge have "CFG.path src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(Node m) [(Node m,kind x,Node Exit)] (Node Exit)"
apply - apply(rule CFG.Cons_path[OF CFG])
apply(rule CFG.empty_path[OF CFG])
by(auto simp:CFG.valid_node_def[OF CFG])
thus ?thesis by blast
next
case inner
from IH[OF this `targetnode x -xs->* Exit`] obtain es
where "CFG.path src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(Node (targetnode x)) es (Node Exit)" by blast
with edge have "CFG.path src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(Node m) ((Node m,kind x,Node (targetnode x))#es) (Node Exit)"
by(fastforce intro:CFG.Cons_path[OF CFG])
thus ?thesis by blast
qed
qed
then obtain es where path:"CFG.path src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(Node m) es (Node Exit)" by blast
have "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit
(Node Exit,(λs. True)⇣\<surd>,NewExit)" by(fastforce intro:lve_Exit_edge)
hence "CFG.path src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(Node Exit) [(Node Exit,(λs. True)⇣\<surd>,NewExit)] NewExit"
by(fastforce intro:CFG.Cons_path[OF CFG] CFG.empty_path[OF CFG]
simp:CFG.valid_node_def[OF CFG])
with path Node have "CFG.path src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
n (es@[(Node Exit, (λs. True)⇣\<surd>, NewExit)]) NewExit"
by(fastforce intro:CFG.path_Append[OF CFG])
thus ?thesis by blast
qed
qed
qed
qed
lemma lift_PDG_scd:
assumes PDG:"PDG sourcenode targetnode kind valid_edge Entry Def Use state_val Exit
(Postdomination.standard_control_dependence sourcenode targetnode valid_edge Exit)"
and pd:"Postdomination sourcenode targetnode kind valid_edge Entry Exit"
and inner:"CFGExit.inner_node sourcenode targetnode valid_edge Entry Exit nx"
shows "PDG src trg knd
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) NewEntry
(lift_Def Def Entry Exit H L) (lift_Use Use Entry Exit H L) state_val NewExit
(Postdomination.standard_control_dependence src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) NewExit)"
proof -
interpret PDG sourcenode targetnode kind valid_edge Entry Def Use state_val Exit
"Postdomination.standard_control_dependence sourcenode targetnode
valid_edge Exit"
by(rule PDG)
have wf:"CFGExit_wf sourcenode targetnode kind valid_edge Entry Def Use
state_val Exit" by(unfold_locales)
from wf pd inner have pd':"Postdomination src trg knd
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
NewEntry NewExit"
by(rule lift_Postdomination)
from wf have CFG:"CFG src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) NewEntry"
by(rule lift_CFG)
from wf have CFG_wf:"CFG_wf src trg knd
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) NewEntry
(lift_Def Def Entry Exit H L) (lift_Use Use Entry Exit H L) state_val"
by(rule lift_CFG_wf)
from wf have CFGExit:"CFGExit src trg knd
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
NewEntry NewExit"
by(rule lift_CFGExit)
from wf have CFGExit_wf:"CFGExit_wf src trg knd
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) NewEntry
(lift_Def Def Entry Exit H L) (lift_Use Use Entry Exit H L) state_val NewExit"
by(rule lift_CFGExit_wf)
show ?thesis
proof
fix a assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
and "trg a = NewEntry"
with CFG show False by(rule CFG.Entry_target)
next
fix a a'
assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
and "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a'"
and "src a = src a'" and "trg a = trg a'"
with CFG show "a = a'" by(rule CFG.edge_det)
next
from CFG_wf
show "lift_Def Def Entry Exit H L NewEntry = {} ∧
lift_Use Use Entry Exit H L NewEntry = {}"
by(rule CFG_wf.Entry_empty)
next
fix a V s
assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
and "V ∉ lift_Def Def Entry Exit H L (src a)" and "pred (knd a) s"
with CFG_wf show "state_val (transfer (knd a) s) V = state_val s V"
by(rule CFG_wf.CFG_edge_no_Def_equal)
next
fix a s s'
assume assms:"lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
"∀V∈lift_Use Use Entry Exit H L (src a). state_val s V = state_val s' V"
"pred (knd a) s" "pred (knd a) s'"
with CFG_wf show "∀V∈lift_Def Def Entry Exit H L (src a).
state_val (transfer (knd a) s) V = state_val (transfer (knd a) s') V"
by(rule CFG_wf.CFG_edge_transfer_uses_only_Use)
next
fix a s s'
assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
and "pred (knd a) s"
and "∀V∈lift_Use Use Entry Exit H L (src a). state_val s V = state_val s' V"
with CFG_wf show "pred (knd a) s'" by(rule CFG_wf.CFG_edge_Uses_pred_equal)
next
fix a a'
assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
and "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a'"
and "src a = src a'" and "trg a ≠ trg a'"
with CFG_wf show "∃Q Q'. knd a = (Q)⇣\<surd> ∧ knd a' = (Q')⇣\<surd> ∧
(∀s. (Q s --> ¬ Q' s) ∧ (Q' s --> ¬ Q s))"
by(rule CFG_wf.deterministic)
next
fix a assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
and "src a = NewExit"
with CFGExit show False by(rule CFGExit.Exit_source)
next
from CFGExit
show "∃a. lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a ∧
src a = NewEntry ∧ trg a = NewExit ∧ knd a = (λs. False)⇣\<surd>"
by(rule CFGExit.Entry_Exit_edge)
next
from CFGExit_wf
show "lift_Def Def Entry Exit H L NewExit = {} ∧
lift_Use Use Entry Exit H L NewExit = {}"
by(rule CFGExit_wf.Exit_empty)
next
fix n n'
assume scd:"Postdomination.standard_control_dependence src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) NewExit n n'"
show "n' ≠ NewExit"
proof(rule ccontr)
assume "¬ n' ≠ NewExit"
hence "n' = NewExit" by simp
with scd pd' show False
by(fastforce intro:Postdomination.Exit_not_standard_control_dependent)
qed
next
fix n n'
assume "Postdomination.standard_control_dependence src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) NewExit n n'"
thus "∃as. CFG.path src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
n as n' ∧ as ≠ []"
by(fastforce simp:Postdomination.standard_control_dependence_def[OF pd'])
qed
qed
lemma lift_PDG_standard_backward_slice:
fixes valid_edge and sourcenode and targetnode and kind and Entry and Exit
and Def and Use and H and L
defines lve:"lve ≡ lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit"
and lDef:"lDef ≡ lift_Def Def Entry Exit H L"
and lUse:"lUse ≡ lift_Use Use Entry Exit H L"
assumes PDG:"PDG sourcenode targetnode kind valid_edge Entry Def Use state_val Exit
(Postdomination.standard_control_dependence sourcenode targetnode valid_edge Exit)"
and pd:"Postdomination sourcenode targetnode kind valid_edge Entry Exit"
and inner:"CFGExit.inner_node sourcenode targetnode valid_edge Entry Exit nx"
and "H ∩ L = {}" and "H ∪ L = UNIV"
shows "NonInterferenceIntraGraph src trg knd lve NewEntry lDef lUse state_val
(PDG.PDG_BS src trg lve lDef lUse
(Postdomination.standard_control_dependence src trg lve NewExit))
NewExit H L (Node Entry) (Node Exit)"
proof -
interpret PDG sourcenode targetnode kind valid_edge Entry Def Use state_val Exit
"Postdomination.standard_control_dependence sourcenode targetnode
valid_edge Exit"
by(rule PDG)
have wf:"CFGExit_wf sourcenode targetnode kind valid_edge Entry Def Use
state_val Exit" by(unfold_locales)
interpret wf':CFGExit_wf src trg knd lve NewEntry lDef lUse state_val NewExit
by(fastforce intro:lift_CFGExit_wf wf simp:lve lDef lUse)
from PDG pd inner lve lDef lUse have PDG':"PDG src trg knd
lve NewEntry lDef lUse state_val NewExit
(Postdomination.standard_control_dependence src trg lve NewExit)"
by(fastforce intro:lift_PDG_scd)
from wf pd inner have pd':"Postdomination src trg knd
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
NewEntry NewExit"
by(rule lift_Postdomination)
from wf lve have CFG:"CFG src trg lve NewEntry"
by(fastforce intro:lift_CFG)
from wf lve lDef lUse
have CFG_wf:"CFG_wf src trg knd lve NewEntry lDef lUse state_val"
by(fastforce intro:lift_CFG_wf)
from wf lve have CFGExit:"CFGExit src trg knd lve NewEntry NewExit"
by(fastforce intro:lift_CFGExit)
from wf lve lDef lUse
have CFGExit_wf:"CFGExit_wf src trg knd lve NewEntry lDef lUse state_val NewExit"
by(fastforce intro:lift_CFGExit_wf)
show ?thesis
proof
fix n S
assume "n ∈ PDG.PDG_BS src trg lve lDef lUse
(Postdomination.standard_control_dependence src trg lve NewExit) S"
with PDG' show "CFG.valid_node src trg lve n"
by(rule PDG.PDG_BS_valid_node)
next
fix n S assume "CFG.valid_node src trg lve n" and "n ∈ S"
thus "n ∈ PDG.PDG_BS src trg lve lDef lUse
(Postdomination.standard_control_dependence src trg lve NewExit) S"
by(fastforce intro:PDG.PDG_path_Nil[OF PDG'] simp:PDG.PDG_BS_def[OF PDG'])
next
fix n' S n V
assume "n' ∈ PDG.PDG_BS src trg lve lDef lUse
(Postdomination.standard_control_dependence src trg lve NewExit) S"
and "CFG_wf.data_dependence src trg lve lDef lUse n V n'"
thus "n ∈ PDG.PDG_BS src trg lve lDef lUse
(Postdomination.standard_control_dependence src trg lve NewExit) S"
by(fastforce intro:PDG.PDG_path_Append[OF PDG'] PDG.PDG_path_ddep[OF PDG']
PDG.PDG_ddep_edge[OF PDG'] simp:PDG.PDG_BS_def[OF PDG']
split:split_if_asm)
next
fix n S
interpret PDGx:PDG src trg knd lve NewEntry lDef lUse state_val NewExit
"Postdomination.standard_control_dependence src trg lve NewExit"
by(rule PDG')
interpret pdx:Postdomination src trg knd lve NewEntry NewExit
by(fastforce intro:pd' simp:lve)
have scd:"StandardControlDependencePDG src trg knd lve NewEntry
lDef lUse state_val NewExit" by(unfold_locales)
from StandardControlDependencePDG.obs_singleton[OF scd]
have "(∃m. CFG.obs src trg lve n
(PDG.PDG_BS src trg lve lDef lUse
(Postdomination.standard_control_dependence src trg lve NewExit) S) = {m}) ∨
CFG.obs src trg lve n
(PDG.PDG_BS src trg lve lDef lUse
(Postdomination.standard_control_dependence src trg lve NewExit) S) = {}"
by(fastforce simp:StandardControlDependencePDG.PDG_BS_s_def[OF scd])
thus "finite (CFG.obs src trg lve n
(PDG.PDG_BS src trg lve lDef lUse
(Postdomination.standard_control_dependence src trg lve NewExit) S))"
by fastforce
next
fix n S
interpret PDGx:PDG src trg knd lve NewEntry lDef lUse state_val NewExit
"Postdomination.standard_control_dependence src trg lve NewExit"
by(rule PDG')
interpret pdx:Postdomination src trg knd lve NewEntry NewExit
by(fastforce intro:pd' simp:lve)
have scd:"StandardControlDependencePDG src trg knd lve NewEntry
lDef lUse state_val NewExit" by(unfold_locales)
from StandardControlDependencePDG.obs_singleton[OF scd]
have "(∃m. CFG.obs src trg lve n
(PDG.PDG_BS src trg lve lDef lUse
(Postdomination.standard_control_dependence src trg lve NewExit) S) = {m}) ∨
CFG.obs src trg lve n
(PDG.PDG_BS src trg lve lDef lUse
(Postdomination.standard_control_dependence src trg lve NewExit) S) = {}"
by(fastforce simp:StandardControlDependencePDG.PDG_BS_s_def[OF scd])
thus "card (CFG.obs src trg lve n
(PDG.PDG_BS src trg lve lDef lUse
(Postdomination.standard_control_dependence src trg lve NewExit) S)) ≤ 1"
by fastforce
next
fix a assume "lve a" and "src a = NewEntry"
with lve show "trg a = NewExit ∨ trg a = Node Entry"
by(fastforce elim:lift_valid_edge.cases)
next
from lve_Entry_edge lve
show "∃a. lve a ∧ src a = NewEntry ∧ trg a = Node Entry ∧ knd a = (λs. True)⇣\<surd>"
by(fastforce simp:knd_def)
next
fix a assume "lve a" and "trg a = Node Entry"
with lve show "src a = NewEntry" by(fastforce elim:lift_valid_edge.cases)
next
fix a assume "lve a" and "trg a = NewExit"
with lve show "src a = NewEntry ∨ src a = Node Exit"
by(fastforce elim:lift_valid_edge.cases)
next
from lve_Exit_edge lve
show "∃a. lve a ∧ src a = Node Exit ∧ trg a = NewExit ∧ knd a = (λs. True)⇣\<surd>"
by(fastforce simp:knd_def)
next
fix a assume "lve a" and "src a = Node Exit"
with lve show "trg a = NewExit" by(fastforce elim:lift_valid_edge.cases)
next
from lDef show "lDef (Node Entry) = H"
by(fastforce elim:lift_Def_set.cases intro:lift_Def_High)
next
from Entry_noteq_Exit lUse show "lUse (Node Entry) = H"
by(fastforce elim:lift_Use_set.cases intro:lift_Use_High)
next
from Entry_noteq_Exit lUse show "lUse (Node Exit) = L"
by(fastforce elim:lift_Use_set.cases intro:lift_Use_Low)
next
from `H ∩ L = {}` show "H ∩ L = {}" .
next
from `H ∪ L = UNIV` show "H ∪ L = UNIV" .
qed
qed
subsubsection {* Lifting @{text PDG_BS} with @{text weak_control_dependence} *}
lemma lift_StrongPostdomination:
assumes wf:"CFGExit_wf sourcenode targetnode kind valid_edge Entry Def Use
state_val Exit"
and spd:"StrongPostdomination sourcenode targetnode kind valid_edge Entry Exit"
and inner:"CFGExit.inner_node sourcenode targetnode valid_edge Entry Exit nx"
shows "StrongPostdomination src trg knd
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) NewEntry NewExit"
proof -
interpret StrongPostdomination sourcenode targetnode kind valid_edge Entry Exit
by(rule spd)
have pd:"Postdomination sourcenode targetnode kind valid_edge Entry Exit"
by(unfold_locales)
interpret pd':Postdomination src trg knd
"lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit"
NewEntry NewExit
by(fastforce intro:wf inner lift_Postdomination pd)
interpret CFGExit_wf:CFGExit_wf src trg knd
"lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit" NewEntry
"lift_Def Def Entry Exit H L" "lift_Use Use Entry Exit H L" state_val NewExit
by(fastforce intro:lift_CFGExit_wf wf)
from wf have CFG:"CFG src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) NewEntry"
by(rule lift_CFG)
show ?thesis
proof
fix n assume "CFG.valid_node src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) n"
show "finite
{n'. ∃a'. lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a' ∧
src a' = n ∧ trg a' = n'}"
proof(cases n)
case NewEntry
hence "{n'. ∃a'. lift_valid_edge valid_edge sourcenode targetnode kind
Entry Exit a' ∧ src a' = n ∧ trg a' = n'} = {NewExit,Node Entry}"
by(auto elim:lift_valid_edge.cases intro:lift_valid_edge.intros)
thus ?thesis by simp
next
case NewExit
hence "{n'. ∃a'. lift_valid_edge valid_edge sourcenode targetnode kind
Entry Exit a' ∧ src a' = n ∧ trg a' = n'} = {}"
by fastforce
thus ?thesis by simp
next
case (Node m)
with Entry_Exit_edge `CFG.valid_node src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) n`
have "valid_node m"
by(auto elim:lift_valid_edge.cases
simp:CFG.valid_node_def[OF CFG] valid_node_def)
hence "finite {m'. ∃a'. valid_edge a' ∧ sourcenode a' = m ∧ targetnode a' = m'}"
by(rule successor_set_finite)
have "{m'. ∃a'. lift_valid_edge valid_edge sourcenode targetnode kind
Entry Exit a' ∧ src a' = Node m ∧ trg a' = Node m'} ⊆
{m'. ∃a'. valid_edge a' ∧ sourcenode a' = m ∧ targetnode a' = m'}"
by(fastforce elim:lift_valid_edge.cases)
with `finite {m'. ∃a'. valid_edge a' ∧ sourcenode a' = m ∧ targetnode a' = m'}`
have "finite {m'. ∃a'. lift_valid_edge valid_edge sourcenode targetnode kind
Entry Exit a' ∧ src a' = Node m ∧ trg a' = Node m'}"
by -(rule finite_subset)
hence "finite (Node ` {m'. ∃a'. lift_valid_edge valid_edge sourcenode
targetnode kind Entry Exit a' ∧ src a' = Node m ∧ trg a' = Node m'})"
by fastforce
hence fin:"finite ((Node ` {m'. ∃a'. lift_valid_edge valid_edge sourcenode
targetnode kind Entry Exit a' ∧ src a' = Node m ∧ trg a' = Node m'}) ∪
{NewEntry,NewExit})" by fastforce
with Node have "{n'. ∃a'. lift_valid_edge valid_edge sourcenode targetnode kind
Entry Exit a' ∧ src a' = n ∧ trg a' = n'} ⊆
(Node ` {m'. ∃a'. lift_valid_edge valid_edge sourcenode
targetnode kind Entry Exit a' ∧ src a' = Node m ∧ trg a' = Node m'}) ∪
{NewEntry,NewExit}" by auto (case_tac x,auto)
with fin show ?thesis by -(rule finite_subset)
qed
qed
qed
lemma lift_PDG_wcd:
assumes PDG:"PDG sourcenode targetnode kind valid_edge Entry Def Use state_val Exit
(StrongPostdomination.weak_control_dependence sourcenode targetnode
valid_edge Exit)"
and spd:"StrongPostdomination sourcenode targetnode kind valid_edge Entry Exit"
and inner:"CFGExit.inner_node sourcenode targetnode valid_edge Entry Exit nx"
shows "PDG src trg knd
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) NewEntry
(lift_Def Def Entry Exit H L) (lift_Use Use Entry Exit H L) state_val NewExit
(StrongPostdomination.weak_control_dependence src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) NewExit)"
proof -
interpret PDG sourcenode targetnode kind valid_edge Entry Def Use state_val Exit
"StrongPostdomination.weak_control_dependence sourcenode targetnode
valid_edge Exit"
by(rule PDG)
have wf:"CFGExit_wf sourcenode targetnode kind valid_edge Entry Def Use
state_val Exit" by(unfold_locales)
from wf spd inner have spd':"StrongPostdomination src trg knd
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
NewEntry NewExit"
by(rule lift_StrongPostdomination)
from wf have CFG:"CFG src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) NewEntry"
by(rule lift_CFG)
from wf have CFG_wf:"CFG_wf src trg knd
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) NewEntry
(lift_Def Def Entry Exit H L) (lift_Use Use Entry Exit H L) state_val"
by(rule lift_CFG_wf)
from wf have CFGExit:"CFGExit src trg knd
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
NewEntry NewExit"
by(rule lift_CFGExit)
from wf have CFGExit_wf:"CFGExit_wf src trg knd
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) NewEntry
(lift_Def Def Entry Exit H L) (lift_Use Use Entry Exit H L) state_val NewExit"
by(rule lift_CFGExit_wf)
show ?thesis
proof
fix a assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
and "trg a = NewEntry"
with CFG show False by(rule CFG.Entry_target)
next
fix a a'
assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
and "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a'"
and "src a = src a'" and "trg a = trg a'"
with CFG show "a = a'" by(rule CFG.edge_det)
next
from CFG_wf
show "lift_Def Def Entry Exit H L NewEntry = {} ∧
lift_Use Use Entry Exit H L NewEntry = {}"
by(rule CFG_wf.Entry_empty)
next
fix a V s
assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
and "V ∉ lift_Def Def Entry Exit H L (src a)" and "pred (knd a) s"
with CFG_wf show "state_val (transfer (knd a) s) V = state_val s V"
by(rule CFG_wf.CFG_edge_no_Def_equal)
next
fix a s s'
assume assms:"lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
"∀V∈lift_Use Use Entry Exit H L (src a). state_val s V = state_val s' V"
"pred (knd a) s" "pred (knd a) s'"
with CFG_wf show "∀V∈lift_Def Def Entry Exit H L (src a).
state_val (transfer (knd a) s) V = state_val (transfer (knd a) s') V"
by(rule CFG_wf.CFG_edge_transfer_uses_only_Use)
next
fix a s s'
assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
and "pred (knd a) s"
and "∀V∈lift_Use Use Entry Exit H L (src a). state_val s V = state_val s' V"
with CFG_wf show "pred (knd a) s'" by(rule CFG_wf.CFG_edge_Uses_pred_equal)
next
fix a a'
assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
and "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a'"
and "src a = src a'" and "trg a ≠ trg a'"
with CFG_wf show "∃Q Q'. knd a = (Q)⇣\<surd> ∧ knd a' = (Q')⇣\<surd> ∧
(∀s. (Q s --> ¬ Q' s) ∧ (Q' s --> ¬ Q s))"
by(rule CFG_wf.deterministic)
next
fix a assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
and "src a = NewExit"
with CFGExit show False by(rule CFGExit.Exit_source)
next
from CFGExit
show "∃a. lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a ∧
src a = NewEntry ∧ trg a = NewExit ∧ knd a = (λs. False)⇣\<surd>"
by(rule CFGExit.Entry_Exit_edge)
next
from CFGExit_wf
show "lift_Def Def Entry Exit H L NewExit = {} ∧
lift_Use Use Entry Exit H L NewExit = {}"
by(rule CFGExit_wf.Exit_empty)
next
fix n n'
assume wcd:"StrongPostdomination.weak_control_dependence src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) NewExit n n'"
show "n' ≠ NewExit"
proof(rule ccontr)
assume "¬ n' ≠ NewExit"
hence "n' = NewExit" by simp
with wcd spd' show False
by(fastforce intro:StrongPostdomination.Exit_not_weak_control_dependent)
qed
next
fix n n'
assume "StrongPostdomination.weak_control_dependence src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) NewExit n n'"
thus "∃as. CFG.path src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
n as n' ∧ as ≠ []"
by(fastforce simp:StrongPostdomination.weak_control_dependence_def[OF spd'])
qed
qed
lemma lift_PDG_weak_backward_slice:
fixes valid_edge and sourcenode and targetnode and kind and Entry and Exit
and Def and Use and H and L
defines lve:"lve ≡ lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit"
and lDef:"lDef ≡ lift_Def Def Entry Exit H L"
and lUse:"lUse ≡ lift_Use Use Entry Exit H L"
assumes PDG:"PDG sourcenode targetnode kind valid_edge Entry Def Use state_val Exit
(StrongPostdomination.weak_control_dependence sourcenode targetnode
valid_edge Exit)"
and spd:"StrongPostdomination sourcenode targetnode kind valid_edge Entry Exit"
and inner:"CFGExit.inner_node sourcenode targetnode valid_edge Entry Exit nx"
and "H ∩ L = {}" and "H ∪ L = UNIV"
shows "NonInterferenceIntraGraph src trg knd lve NewEntry lDef lUse state_val
(PDG.PDG_BS src trg lve lDef lUse
(StrongPostdomination.weak_control_dependence src trg lve NewExit))
NewExit H L (Node Entry) (Node Exit)"
proof -
interpret PDG sourcenode targetnode kind valid_edge Entry Def Use state_val Exit
"StrongPostdomination.weak_control_dependence sourcenode targetnode
valid_edge Exit"
by(rule PDG)
have wf:"CFGExit_wf sourcenode targetnode kind valid_edge Entry Def Use
state_val Exit" by(unfold_locales)
interpret wf':CFGExit_wf src trg knd lve NewEntry lDef lUse state_val NewExit
by(fastforce intro:lift_CFGExit_wf wf simp:lve lDef lUse)
from PDG spd inner lve lDef lUse have PDG':"PDG src trg knd
lve NewEntry lDef lUse state_val NewExit
(StrongPostdomination.weak_control_dependence src trg lve NewExit)"
by(fastforce intro:lift_PDG_wcd)
from wf spd inner have spd':"StrongPostdomination src trg knd
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
NewEntry NewExit"
by(rule lift_StrongPostdomination)
from wf lve have CFG:"CFG src trg lve NewEntry"
by(fastforce intro:lift_CFG)
from wf lve lDef lUse
have CFG_wf:"CFG_wf src trg knd lve NewEntry lDef lUse state_val"
by(fastforce intro:lift_CFG_wf)
from wf lve have CFGExit:"CFGExit src trg knd lve NewEntry NewExit"
by(fastforce intro:lift_CFGExit)
from wf lve lDef lUse
have CFGExit_wf:"CFGExit_wf src trg knd lve NewEntry lDef lUse state_val NewExit"
by(fastforce intro:lift_CFGExit_wf)
show ?thesis
proof
fix n S
assume "n ∈ PDG.PDG_BS src trg lve lDef lUse
(StrongPostdomination.weak_control_dependence src trg lve NewExit) S"
with PDG' show "CFG.valid_node src trg lve n"
by(rule PDG.PDG_BS_valid_node)
next
fix n S assume "CFG.valid_node src trg lve n" and "n ∈ S"
thus "n ∈ PDG.PDG_BS src trg lve lDef lUse
(StrongPostdomination.weak_control_dependence src trg lve NewExit) S"
by(fastforce intro:PDG.PDG_path_Nil[OF PDG'] simp:PDG.PDG_BS_def[OF PDG'])
next
fix n' S n V
assume "n' ∈ PDG.PDG_BS src trg lve lDef lUse
(StrongPostdomination.weak_control_dependence src trg lve NewExit) S"
and "CFG_wf.data_dependence src trg lve lDef lUse n V n'"
thus "n ∈ PDG.PDG_BS src trg lve lDef lUse
(StrongPostdomination.weak_control_dependence src trg lve NewExit) S"
by(fastforce intro:PDG.PDG_path_Append[OF PDG'] PDG.PDG_path_ddep[OF PDG']
PDG.PDG_ddep_edge[OF PDG'] simp:PDG.PDG_BS_def[OF PDG']
split:split_if_asm)
next
fix n S
interpret PDGx:PDG src trg knd lve NewEntry lDef lUse state_val NewExit
"StrongPostdomination.weak_control_dependence src trg lve NewExit"
by(rule PDG')
interpret spdx:StrongPostdomination src trg knd lve NewEntry NewExit
by(fastforce intro:spd' simp:lve)
have wcd:"WeakControlDependencePDG src trg knd lve NewEntry
lDef lUse state_val NewExit" by(unfold_locales)
from WeakControlDependencePDG.obs_singleton[OF wcd]
have "(∃m. CFG.obs src trg lve n
(PDG.PDG_BS src trg lve lDef lUse
(StrongPostdomination.weak_control_dependence src trg lve NewExit) S) = {m}) ∨
CFG.obs src trg lve n
(PDG.PDG_BS src trg lve lDef lUse
(StrongPostdomination.weak_control_dependence src trg lve NewExit) S) = {}"
by(fastforce simp:WeakControlDependencePDG.PDG_BS_w_def[OF wcd])
thus "finite (CFG.obs src trg lve n
(PDG.PDG_BS src trg lve lDef lUse
(StrongPostdomination.weak_control_dependence src trg lve NewExit) S))"
by fastforce
next
fix n S
interpret PDGx:PDG src trg knd lve NewEntry lDef lUse state_val NewExit
"StrongPostdomination.weak_control_dependence src trg lve NewExit"
by(rule PDG')
interpret spdx:StrongPostdomination src trg knd lve NewEntry NewExit
by(fastforce intro:spd' simp:lve)
have wcd:"WeakControlDependencePDG src trg knd lve NewEntry
lDef lUse state_val NewExit" by(unfold_locales)
from WeakControlDependencePDG.obs_singleton[OF wcd]
have "(∃m. CFG.obs src trg lve n
(PDG.PDG_BS src trg lve lDef lUse
(StrongPostdomination.weak_control_dependence src trg lve NewExit) S) = {m}) ∨
CFG.obs src trg lve n
(PDG.PDG_BS src trg lve lDef lUse
(StrongPostdomination.weak_control_dependence src trg lve NewExit) S) = {}"
by(fastforce simp:WeakControlDependencePDG.PDG_BS_w_def[OF wcd])
thus "card (CFG.obs src trg lve n
(PDG.PDG_BS src trg lve lDef lUse
(StrongPostdomination.weak_control_dependence src trg lve NewExit) S)) ≤ 1"
by fastforce
next
fix a assume "lve a" and "src a = NewEntry"
with lve show "trg a = NewExit ∨ trg a = Node Entry"
by(fastforce elim:lift_valid_edge.cases)
next
from lve_Entry_edge lve
show "∃a. lve a ∧ src a = NewEntry ∧ trg a = Node Entry ∧ knd a = (λs. True)⇣\<surd>"
by(fastforce simp:knd_def)
next
fix a assume "lve a" and "trg a = Node Entry"
with lve show "src a = NewEntry" by(fastforce elim:lift_valid_edge.cases)
next
fix a assume "lve a" and "trg a = NewExit"
with lve show "src a = NewEntry ∨ src a = Node Exit"
by(fastforce elim:lift_valid_edge.cases)
next
from lve_Exit_edge lve
show "∃a. lve a ∧ src a = Node Exit ∧ trg a = NewExit ∧ knd a = (λs. True)⇣\<surd>"
by(fastforce simp:knd_def)
next
fix a assume "lve a" and "src a = Node Exit"
with lve show "trg a = NewExit" by(fastforce elim:lift_valid_edge.cases)
next
from lDef show "lDef (Node Entry) = H"
by(fastforce elim:lift_Def_set.cases intro:lift_Def_High)
next
from Entry_noteq_Exit lUse show "lUse (Node Entry) = H"
by(fastforce elim:lift_Use_set.cases intro:lift_Use_High)
next
from Entry_noteq_Exit lUse show "lUse (Node Exit) = L"
by(fastforce elim:lift_Use_set.cases intro:lift_Use_Low)
next
from `H ∩ L = {}` show "H ∩ L = {}" .
next
from `H ∪ L = UNIV` show "H ∪ L = UNIV" .
qed
qed
end