Theory SSA_CFG
theory SSA_CFG
imports Graph_path "HOL-Library.Sublist"
begin
subsection ‹CFG›
locale CFG_base = graph_Entry_base αe αn invar inEdges' Entry
for
αe :: "'g ⇒ ('node::linorder × 'edgeD × 'node) set" and
αn :: "'g ⇒ 'node list" and
invar :: "'g ⇒ bool" and
inEdges' :: "'g ⇒ 'node ⇒ ('node × 'edgeD) list" and
Entry :: "'g ⇒ 'node" +
fixes "defs" :: "'g ⇒ 'node ⇒ 'var::linorder set"
fixes "uses" :: "'g ⇒ 'node ⇒ 'var set"
begin
definition "vars g ≡ fold (∪) (map (uses g) (αn g)) {}"
definition defAss' :: "'g ⇒ 'node ⇒ 'var ⇒ bool" where
"defAss' g m v ⟷ (∀ns. g ⊢ Entry g-ns→m ⟶ (∃n ∈ set ns. v ∈ defs g n))"
definition defAss'Uses :: "'g ⇒ bool" where
"defAss'Uses g ≡ ∀m ∈ set (αn g). ∀v ∈ uses g m. defAss' g m v"
end
locale CFG = CFG_base αe αn invar inEdges' Entry "defs" "uses"
+ graph_Entry αe αn invar inEdges' Entry
for
αe :: "'g ⇒ ('node::linorder × 'edgeD × 'node) set" and
αn :: "'g ⇒ 'node list" and
invar :: "'g ⇒ bool" and
inEdges' :: "'g ⇒ 'node ⇒ ('node × 'edgeD) list" and
Entry :: "'g ⇒ 'node" and
"defs" :: "'g ⇒ 'node ⇒ 'var::linorder set" and
"uses" :: "'g ⇒ 'node ⇒ 'var set" +
assumes defs_uses_disjoint: "n ∈ set (αn g) ⟹ defs g n ∩ uses g n = {}"
assumes defs_finite[simp]: "finite (defs g n)"
assumes uses_in_αn: "v ∈ uses g n ⟹ n ∈ set (αn g)"
assumes uses_finite[simp, intro!]: "finite (uses g n)"
assumes invar[intro!]: "invar g"
begin
lemma vars_finite[simp]: "finite (vars g)"
by (auto simp:vars_def)
lemma Entry_no_predecessor[simp]: "predecessors g (Entry g) = []"
using Entry_unreachable
by (auto simp:predecessors_def)
lemma uses_in_vars[elim, simp]: "v ∈ uses g n ⟹ v ∈ vars g"
by (auto simp add:vars_def uses_in_αn intro!: fold_union_elemI)
lemma varsE:
assumes "v ∈ vars g"
obtains n where "n ∈ set (αn g)" "v ∈ uses g n"
using assms by (auto simp:vars_def elim!:fold_union_elem)
lemma defs_uses_disjoint'[simp]: "n ∈ set (αn g) ⟹ v ∈ defs g n ⟹ v ∈ uses g n ⟹ False"
using defs_uses_disjoint by auto
end
context CFG
begin
lemma defAss'E:
assumes "defAss' g m v" "g ⊢ Entry g-ns→m"
obtains n where "n ∈ set ns" "v ∈ defs g n"
using assms unfolding defAss'_def by auto
lemmas defAss'I = defAss'_def[THEN iffD2, rule_format]
lemma defAss'_extend:
assumes "defAss' g m v"
assumes "g ⊢ n-ns→m" "∀n ∈ set (tl ns). v ∉ defs g n"
shows "defAss' g n v"
unfolding defAss'_def proof (rule allI, rule impI)
fix ns'
assume "g ⊢ Entry g-ns'→n"
with assms(2) have "g ⊢ Entry g-ns'@tl ns→m" by auto
with assms(1) obtain n' where n': "n' ∈ set (ns'@tl ns)" "v ∈ defs g n'" by -(erule defAss'E)
with assms(3) have "n' ∉ set (tl ns)" by auto
with n' show "∃n ∈ set ns'. v ∈ defs g n" by auto
qed
end
text ‹A CFG is well-formed if it satisfies definite assignment.›
locale CFG_wf = CFG αe αn invar inEdges' Entry "defs" "uses"
for
αe :: "'g ⇒ ('node::linorder × 'edgeD × 'node) set" and
αn :: "'g ⇒ 'node list" and
invar :: "'g ⇒ bool" and
inEdges' :: "'g ⇒ 'node ⇒ ('node × 'edgeD) list" and
Entry::"'g ⇒ 'node" and
"defs" :: "'g ⇒ 'node ⇒ 'var::linorder set" and
"uses" :: "'g ⇒ 'node ⇒ 'var set" +
assumes def_ass_uses: "∀m ∈ set (αn g). ∀v ∈ uses g m. defAss' g m v"
subsection ‹SSA CFG›
type_synonym ('node, 'val) phis = "'node × 'val ⇀ 'val list"
declare in_set_zipE[elim]
declare zip_same[simp]
locale CFG_SSA_base = CFG_base αe αn invar inEdges' Entry "defs" "uses"
for
αe :: "'g ⇒ ('node::linorder × 'edgeD × 'node) set" and
αn :: "'g ⇒ 'node list" and
invar :: "'g ⇒ bool" and
inEdges' :: "'g ⇒ 'node ⇒ ('node × 'edgeD) list" and
Entry::"'g ⇒ 'node" and
"defs" :: "'g ⇒ 'node ⇒ 'val::linorder set" and
"uses" :: "'g ⇒ 'node ⇒ 'val set" +
fixes phis :: "'g ⇒ ('node, 'val) phis"
begin
definition "phiDefs g n ≡ {v. (n,v) ∈ dom (phis g)}"
definition[code]: "allDefs g n ≡ defs g n ∪ phiDefs g n"
definition[code]: "phiUses g n ≡
⋃n' ∈ set (successors g n). ⋃v' ∈ phiDefs g n'. snd ` Set.filter (λ(n'',v). n'' = n) (set (zip (predecessors g n') (the (phis g (n',v')))))"
definition[code]: "allUses g n ≡ uses g n ∪ phiUses g n"
definition[code]: "allVars g ≡ ⋃n ∈ set (αn g). allDefs g n ∪ allUses g n"
definition defAss :: "'g ⇒ 'node ⇒ 'val ⇒ bool" where
"defAss g m v ⟷ (∀ns. g ⊢ Entry g-ns→m ⟶ (∃n ∈ set ns. v ∈ allDefs g n))"
lemmas CFG_SSA_defs = phiDefs_def allDefs_def phiUses_def allUses_def allVars_def defAss_def
end
locale CFG_SSA = CFG αe αn invar inEdges' Entry "defs" "uses" + CFG_SSA_base αe αn invar inEdges' Entry "defs" "uses" phis
for
αe :: "'g ⇒ ('node::linorder × 'edgeD × 'node) set" and
αn :: "'g ⇒ 'node list" and
invar :: "'g ⇒ bool" and
inEdges' :: "'g ⇒ 'node ⇒ ('node × 'edgeD) list" and
Entry::"'g ⇒ 'node" and
"defs" :: "'g ⇒ 'node ⇒ 'val::linorder set" and
"uses" :: "'g ⇒ 'node ⇒ 'val set" and
phis :: "'g ⇒ ('node, 'val) phis" +
assumes phis_finite: "finite (dom (phis g))"
assumes phis_in_αn: "phis g (n,v) = Some vs ⟹ n ∈ set (αn g)"
assumes phis_wf:
"phis g (n,v) = Some args ⟹ length (predecessors g n) = length args"
assumes simpleDefs_phiDefs_disjoint:
"n ∈ set (αn g) ⟹ defs g n ∩ phiDefs g n = {}"
assumes allDefs_disjoint:
"⟦n ∈ set (αn g); m ∈ set (αn g); n ≠ m⟧ ⟹ allDefs g n ∩ allDefs g m = {}"
begin
lemma phis_disj:
assumes "phis g (n,v) = Some vs"
and "phis g (n',v) = Some vs'"
shows "n = n'" and "vs = vs'"
proof -
from assms have "n ∈ set (αn g)" and "n' ∈ set (αn g)"
by (auto dest: phis_in_αn)
from allDefs_disjoint [OF this] assms show "n = n'"
by (auto simp: allDefs_def phiDefs_def)
with assms show "vs = vs'" by simp
qed
lemma allDefs_disjoint': "⟦n ∈ set (αn g); m ∈ set (αn g); v ∈ allDefs g n; v ∈ allDefs g m⟧ ⟹ n = m"
using allDefs_disjoint by auto
lemma phiUsesI:
assumes "n' ∈ set (αn g)" "phis g (n',v') = Some vs" "(n,v) ∈ set (zip (predecessors g n') vs)"
shows "v ∈ phiUses g n"
proof-
from assms(3) have "n ∈ set (predecessors g n')" by auto
hence 1: "n' ∈ set (successors g n)" using assms(1) by simp
from assms(2) have 2: "v' ∈ phiDefs g n'" by (auto simp add:phiDefs_def)
from assms(2) have 3: "the (phis g (n',v')) = vs" by simp
show ?thesis unfolding phiUses_def by (rule UN_I[OF 1], rule UN_I[OF 2], auto simp:image_def Set.filter_def assms(3) 3)
qed
lemma phiUsesE:
assumes "v ∈ phiUses g n"
obtains n' v' vs where "n' ∈ set (successors g n)" "(n,v) ∈ set (zip (predecessors g n') vs)" "phis g (n', v') = Some vs"
proof-
from assms(1) obtain n' v' where "n'∈set (successors g n)" "v'∈phiDefs g n'"
"v ∈ snd ` Set.filter (λ(n'', v). n'' = n) (set (zip (predecessors g n') (the (phis g (n', v')))))" by (auto simp:phiUses_def)
thus ?thesis by - (rule that[of n' "the (phis g (n',v'))" v'], auto simp:phiDefs_def)
qed
lemma defs_in_allDefs[simp]: "v ∈ defs g n ⟹ v ∈ allDefs g n" by (simp add:allDefs_def)
lemma phiDefs_in_allDefs[simp, elim]: "v ∈ phiDefs g n ⟹ v ∈ allDefs g n" by (simp add:allDefs_def)
lemma uses_in_allUses[simp]: "v ∈ uses g n ⟹ v ∈ allUses g n" by (simp add:allUses_def)
lemma phiUses_in_allUses[simp]: "v ∈ phiUses g n ⟹ v ∈ allUses g n" by (simp add:allUses_def)
lemma allDefs_in_allVars[simp, intro]: "⟦v ∈ allDefs g n; n ∈ set (αn g)⟧ ⟹ v ∈ allVars g" by (auto simp:allVars_def)
lemma allUses_in_allVars[simp, intro]: "⟦v ∈ allUses g n; n ∈ set (αn g)⟧ ⟹ v ∈ allVars g" by (auto simp:allVars_def)
lemma phiDefs_finite[simp]: "finite (phiDefs g n)"
unfolding phiDefs_def
proof (rule finite_surj[where f=snd], rule phis_finite[where g=g])
have "⋀x y. phis g (n,x) = Some y ⟹ x ∈ snd ` dom (phis g)" by (metis domI imageI snd_conv)
thus "{v. (n, v) ∈ dom (phis g)} ⊆ snd ` dom (phis g)" by auto
qed
lemma phiUses_finite[simp]:
assumes "n ∈ set (αn g)"
shows "finite (phiUses g n)"
by (auto simp:phiUses_def Set.filter_def)
lemma allDefs_finite[simp]: "n ∈ set (αn g) ⟹ finite (allDefs g n)" by (auto simp add:allDefs_def)
lemma allUses_finite[simp]: "n ∈ set (αn g) ⟹ finite (allUses g n)" by (auto simp add:allUses_def)
lemma allVars_finite[simp]: "finite (allVars g)" by (auto simp add:allVars_def)
lemmas defAssI = defAss_def[THEN iffD2, rule_format]
lemmas defAssD = defAss_def[THEN iffD1, rule_format]
lemma defAss_extend:
assumes "defAss g m v"
assumes "g ⊢ n-ns→m" "∀n ∈ set (tl ns). v ∉ allDefs g n"
shows "defAss g n v"
unfolding defAss_def proof (rule allI, rule impI)
fix ns'
assume "g ⊢ Entry g-ns'→n"
with assms(2) have "g ⊢ Entry g-ns'@tl ns→m" by auto
with assms(1) obtain n' where n': "n' ∈ set (ns'@tl ns)" "v ∈ allDefs g n'" by (auto dest:defAssD)
with assms(3) have "n' ∉ set (tl ns)" by auto
with n' show "∃n ∈ set ns'. v ∈ allDefs g n" by auto
qed
lemma defAss_dominating:
assumes[simp]: "n ∈ set (αn g)"
shows "defAss g n v ⟷ (∃m ∈ set (αn g). dominates g m n ∧ v ∈ allDefs g m)"
proof
assume asm: "defAss g n v"
obtain ns where ns: "g ⊢ Entry g-ns→n" by (atomize, auto)
from defAssD[OF asm this] obtain m where m: "m ∈ set ns" "v ∈ allDefs g m" by auto
have "dominates g m n"
proof
fix ns'
assume ns': "g ⊢ Entry g-ns'→n"
from defAssD[OF asm this] obtain m' where m': "m' ∈ set ns'" "v ∈ allDefs g m'" by auto
with m ns ns' have "m' = m" by - (rule allDefs_disjoint', auto)
with m' show "m ∈ set ns'" by simp
qed simp
with m ns show "∃m∈set (αn g). dominates g m n ∧ v ∈ allDefs g m" by auto
next
assume "∃m ∈ set (αn g). dominates g m n ∧ v ∈ allDefs g m"
then obtain m where[simp]: "m ∈ set (αn g)" and m: "dominates g m n" "v ∈ allDefs g m" by auto
show "defAss g n v"
proof (rule defAssI)
fix ns
assume "g ⊢ Entry g-ns→n"
with m(1) have "m ∈ set ns" by - (rule dominates_mid, auto)
with m(2) show "∃n∈set ns. v ∈ allDefs g n" by auto
qed
qed
end
locale CFG_SSA_wf_base = CFG_SSA_base αe αn invar inEdges' Entry "defs" "uses" phis
for
αe :: "'g ⇒ ('node::linorder × 'edgeD × 'node) set" and
αn :: "'g ⇒ 'node list" and
invar :: "'g ⇒ bool" and
inEdges' :: "'g ⇒ 'node ⇒ ('node × 'edgeD) list" and
Entry::"'g ⇒ 'node" and
"defs" :: "'g ⇒ 'node ⇒ 'val::linorder set" and
"uses" :: "'g ⇒ 'node ⇒ 'val set" and
phis :: "'g ⇒ ('node, 'val) phis"
begin
text ‹Using the SSA properties, we can map every value to its unique defining node and
remove the @{typ 'node} parameter of the @{term phis} map.›
definition defNode :: "'g ⇒ 'val ⇒ 'node" where
defNode_code [code]: "defNode g v ≡ hd [n ← αn g. v ∈ allDefs g n]"
abbreviation "def_dominates g v' v ≡ dominates g (defNode g v') (defNode g v)"
abbreviation "strict_def_dom g v' v ≡ defNode g v' ≠ defNode g v ∧ def_dominates g v' v"
definition "phi g v = phis g (defNode g v,v)"
definition[simp]: "phiArg g v v' ≡ ∃vs. phi g v = Some vs ∧ v' ∈ set vs"
definition[code]: "isTrivialPhi g v v' ⟷ v' ≠ v ∧
(case phi g v of
Some vs ⇒ set vs = {v,v'} ∨ set vs = {v'}
| None ⇒ False)"
definition[code]: "trivial g v ≡ ∃v' ∈ allVars g. isTrivialPhi g v v'"
definition[code]: "redundant g ≡ ∃v ∈ allVars g. trivial g v"
definition "defAssUses g ≡ ∀n ∈ set (αn g). ∀v ∈ allUses g n. defAss g n v"
text ‹'liveness' of an SSA value is defined inductively starting from simple uses so that
a circle of \pf s is not considered live.›
declare [[inductive_internals]]
inductive liveVal :: "'g ⇒ 'val ⇒ bool"
for g :: 'g
where
liveSimple: "⟦n ∈ set (αn g); val ∈ uses g n⟧ ⟹ liveVal g val"
| livePhi: "⟦liveVal g v; phiArg g v v'⟧ ⟹ liveVal g v'"
definition "pruned g = (∀n ∈ set (αn g). ∀val. val ∈ phiDefs g n ⟶ liveVal g val)"
lemmas "CFG_SSA_wf_defs" = CFG_SSA_defs defNode_code phi_def isTrivialPhi_def trivial_def redundant_def liveVal_def pruned_def
end
locale CFG_SSA_wf = CFG_SSA αe αn invar inEdges' Entry "defs" "uses" phis + CFG_SSA_wf_base αe αn invar inEdges' Entry "defs" "uses" phis
for
αe :: "'g ⇒ ('node::linorder × 'edgeD × 'node) set" and
αn :: "'g ⇒ 'node list" and
invar :: "'g ⇒ bool" and
inEdges' :: "'g ⇒ 'node ⇒ ('node × 'edgeD) list" and
Entry::"'g ⇒ 'node" and
"defs" :: "'g ⇒ 'node ⇒ 'val::linorder set" and
"uses" :: "'g ⇒ 'node ⇒ 'val set" and
phis :: "'g ⇒ ('node, 'val) phis" +
assumes allUses_def_ass: "⟦v ∈ allUses g n; n ∈ set (αn g)⟧ ⟹ defAss g n v"
assumes Entry_no_phis[simp]: "phis g (Entry g,v) = None"
begin
lemma allVars_in_allDefs: "v ∈ allVars g ⟹ ∃n ∈ set (αn g). v ∈ allDefs g n"
unfolding allVars_def
apply auto
apply (drule(1) allUses_def_ass)
apply (clarsimp simp: defAss_def)
apply (drule Entry_reaches)
apply auto[1]
by fastforce
lemma phiDefs_Entry_empty[simp]: "phiDefs g (Entry g) = {}"
by (auto simp: phiDefs_def)
lemma phi_Entry_empty[simp]: "defNode g v = Entry g ⟹ phi g v = None"
by (simp add:phi_def)
lemma defNode_ex1:
assumes "v ∈ allVars g"
shows "∃!n. n ∈ set (αn g) ∧ v ∈ allDefs g n"
proof (rule ex_ex1I)
show "∃n. n ∈ set (αn g) ∧ v ∈ allDefs g n"
proof-
from assms(1) obtain n where n: "n ∈ set (αn g)" "v ∈ allDefs g n ∨ v ∈ allUses g n" by (auto simp:allVars_def)
thus ?thesis
proof (cases "v ∈ allUses g n")
case True
from n(1) obtain ns where ns: "g ⊢ Entry g-ns→n" by (atomize_elim, rule Entry_reaches, auto)
with allUses_def_ass[OF True n(1)] obtain m where m: "m ∈ set ns" "v ∈ allDefs g m" by - (drule defAssD, auto)
from ns this(1) have "m ∈ set (αn g)" by (rule path2_in_αn)
with n(1) m show ?thesis by auto
qed auto
qed
show "⋀n m. n ∈ set (αn g) ∧ v ∈ allDefs g n ⟹ m ∈ set (αn g) ∧ v ∈ allDefs g m ⟹ n = m" using allDefs_disjoint by auto
qed
lemma defNode_def: "v ∈ allVars g ⟹ defNode g v = (THE n. n ∈ set (αn g) ∧ v ∈ allDefs g n)"
unfolding defNode_code by (rule the1_list[symmetric], rule defNode_ex1)
lemma defNode[simp]:
assumes "v ∈ allVars g"
shows "(defNode g v) ∈ set (αn g)" "v ∈ allDefs g (defNode g v)"
apply (atomize(full))
unfolding defNode_def[OF assms] using assms
by - (rule theI', rule defNode_ex1)
lemma defNode_eq[intro]:
assumes "n ∈ set (αn g)" "v ∈ allDefs g n"
shows "defNode g v = n"
apply (subst defNode_def, rule allDefs_in_allVars[OF assms(2) assms(1)])
by (rule the1_equality, rule defNode_ex1, rule allDefs_in_allVars[where n=n], simp_all add:assms)
lemma defNode_cases[consumes 1]:
assumes "v ∈ allVars g"
obtains (simpleDef) "v ∈ defs g (defNode g v)"
| (phi) "phi g v ≠ None"
proof (cases "v ∈ defs g (defNode g v)")
case True
thus thesis by (rule simpleDef)
next
case False
with assms[THEN defNode(2)] show thesis
by - (rule phi, auto simp: allDefs_def phiDefs_def phi_def)
qed
lemma phi_phiDefs[simp]: "phi g v = Some vs ⟹ v ∈ phiDefs g (defNode g v)" by (auto simp:phiDefs_def phi_def)
lemma simpleDef_not_phi:
assumes "n ∈ set (αn g)" "v ∈ defs g n"
shows "phi g v = None"
proof-
from assms have "defNode g v = n" by auto
with assms show ?thesis using simpleDefs_phiDefs_disjoint by (auto simp: phi_def phiDefs_def)
qed
lemma phi_wf: "phi g v = Some vs ⟹ length (predecessors g (defNode g v)) = length vs"
by (rule phis_wf) (simp add:phi_def)
lemma phi_finite: "finite (dom (phi g))"
proof-
let ?f = "λv. (defNode g v,v)"
have "phi g = phis g ∘ ?f" by (auto simp add:phi_def)
moreover have "inj ?f" by (auto intro:injI)
hence "finite (dom (phis g ∘ ?f))" by - (rule finite_dom_comp, auto simp add:phis_finite inj_on_def)
ultimately show ?thesis by simp
qed
lemma phiUses_exI:
assumes "m ∈ set (predecessors g n)" "phis g (n,v) = Some vs" "n ∈ set (αn g)"
obtains v' where "v' ∈ phiUses g m" "v' ∈ set vs"
proof-
from assms(1) obtain i where i: "m = predecessors g n ! i" "i < length (predecessors g n)" by (metis in_set_conv_nth)
with assms(2) phis_wf have[simp]: "i < length vs" by (auto simp add:phi_def)
from i assms(2,3) have "vs ! i ∈ phiUses g m" by - (rule phiUsesI, auto simp add:phiUses_def phi_def set_zip)
thus thesis by (rule that) (auto simp add:i(2) phis_wf)
qed
lemma phiArg_exI:
assumes "m ∈ set (predecessors g (defNode g v))" "phi g v ≠ None" and[simp]: "v ∈ allVars g"
obtains v' where "v' ∈ phiUses g m" "phiArg g v v'"
proof-
from assms(2) obtain vs where "phi g v = Some vs" by auto
with assms(1) show thesis
by - (rule phiUses_exI, auto intro!:that simp: phi_def)
qed
lemma phiUses_exI':
assumes "phiArg g p q" and[simp]: "p ∈ allVars g"
obtains m where "q ∈ phiUses g m" "m ∈ set (predecessors g (defNode g p))"
proof-
let ?n = "defNode g p"
from assms(1) obtain i vs where vs: "phi g p = Some vs" and i: "q = vs ! i" "i < length vs" by (metis in_set_conv_nth phiArg_def)
with phis_wf have[simp]: "i < length (predecessors g ?n)" by (auto simp add:phi_def)
from vs i have "q ∈ phiUses g (predecessors g ?n ! i)" by - (rule phiUsesI, auto simp add:phiUses_def phi_def set_zip)
thus thesis by (rule that) (auto simp add:i(2) phis_wf)
qed
lemma phiArg_in_allVars[simp]:
assumes "phiArg g v v'"
shows "v' ∈ allVars g"
proof-
let ?n = "defNode g v"
from assms(1) obtain vs where vs: "phi g v = Some vs" "v' ∈ set vs" by auto
then obtain m where m: "(m,v') ∈ set (zip (predecessors g ?n) vs)" by - (rule set_zip_leftI, rule phi_wf)
from vs(1) have n: "?n ∈ set (αn g)" by (simp add: phi_def phis_in_αn)
with m have[simp]: "m ∈ set (αn g)" by auto
from n m vs have "v' ∈ phiUses g m" by - (rule phiUsesI, simp_all add:phi_def)
thus ?thesis by - (rule allUses_in_allVars, auto simp:allUses_def)
qed
lemma defAss_defNode:
assumes "defAss g m v" "v ∈ allVars g" "g ⊢ Entry g-ns→m"
shows "defNode g v ∈ set ns"
proof-
from assms obtain n where n: "n ∈ set ns" "v ∈ allDefs g n" by (auto simp:defAss_def)
with assms(3) have "n = defNode g v" by - (rule defNode_eq[symmetric], auto)
with n show "defNode g v ∈ set ns" by (simp add:defAss_def)
qed
lemma defUse_path_ex:
assumes "v ∈ allUses g m" "m ∈ set (αn g)"
obtains ns where "g ⊢ defNode g v-ns→m" "EntryPath g ns"
proof-
from assms have "defAss g m v" by - (rule allUses_def_ass, auto)
moreover from assms obtain ns where ns: "g ⊢ Entry g-ns→m" "EntryPath g ns"
by - (atomize_elim, rule Entry_reachesE, auto)
ultimately have "defNode g v ∈ set ns" using assms(1)
by - (rule defAss_defNode, auto)
with ns(1) obtain ns' where "g ⊢ defNode g v-ns'→m" "suffix ns' ns"
by (rule path2_split_ex', auto simp: Sublist.suffix_def)
thus thesis using ns(2)
by - (rule that, assumption, rule EntryPath_suffix, auto)
qed
lemma defUse_path_dominated:
assumes "g ⊢ defNode g v-ns→n" "defNode g v ∉ set (tl ns)" "v ∈ allUses g n" "n' ∈ set ns"
shows "dominates g (defNode g v) n'"
proof (rule dominatesI)
fix es
assume asm: "g ⊢ Entry g-es→n'"
from assms(1,4) obtain ns' where ns': "g ⊢ n'-ns'→n" "suffix ns' ns"
by - (rule path2_split_ex, auto simp: Sublist.suffix_def)
from assms have "defAss g n v" by - (rule allUses_def_ass, auto)
with asm ns'(1) assms(3) have "defNode g v ∈ set (es@tl ns')" by - (rule defAss_defNode, auto)
with suffix_tl_subset[OF ns'(2)] assms(2) show "defNode g v ∈ set es" by auto
next
show "n' ∈ set (αn g)" using assms(1,4) by auto
qed
lemma allUses_dominated:
assumes "v ∈ allUses g n" "n ∈ set (αn g)"
shows "dominates g (defNode g v) n"
proof-
from assms obtain ns where "g ⊢ defNode g v-ns→n" "defNode g v ∉ set (tl ns)"
by - (rule defUse_path_ex, auto elim: simple_path2)
with assms(1) show ?thesis by - (rule defUse_path_dominated, auto)
qed
lemma phiArg_path_ex':
assumes "phiArg g p q" and[simp]: "p ∈ allVars g"
obtains ns m where "g ⊢ defNode g q-ns→m" "EntryPath g ns" "q ∈ phiUses g m" "m ∈ set (predecessors g (defNode g p))"
proof-
from assms obtain m where m: "q ∈ phiUses g m" "m ∈ set (predecessors g (defNode g p))"
by (rule phiUses_exI')
then obtain ns where "g ⊢ defNode g q-ns→m" "EntryPath g ns" by - (rule defUse_path_ex, auto)
with m show thesis by - (rule that)
qed
lemma phiArg_path_ex:
assumes "phiArg g p q" and[simp]: "p ∈ allVars g"
obtains ns where "g ⊢ defNode g q-ns→defNode g p" "length ns > 1"
by (rule phiArg_path_ex'[OF assms], rule, auto)
lemma phiArg_tranclp_path_ex:
assumes "r⇧+⇧+ p q" "p ∈ allVars g" and[simp]: "⋀p q. r p q ⟹ phiArg g p q"
obtains ns where "g ⊢ defNode g q-ns→defNode g p" "length ns > 1"
"∀n ∈ set (butlast ns). ∃p q m ns'. r p q ∧ g ⊢ defNode g q-ns'→m ∧ (defNode g q) ∉ set (tl ns') ∧ q ∈ phiUses g m ∧ m ∈ set (predecessors g (defNode g p)) ∧ n ∈ set ns' ∧ set ns' ⊆ set ns ∧ defNode g p ∈ set ns"
using assms(1,2) proof (induction rule: converse_tranclp_induct)
case (base p)
from base.hyps base.prems(2) obtain ns' m where ns': "g ⊢ defNode g q-ns'→m" "defNode g q ∉ set (tl ns')" "m ∈ set (predecessors g (defNode g p))" "q ∈ phiUses g m"
by - (rule phiArg_path_ex', rule assms(3), auto intro: simple_path2)
hence ns: "g ⊢ defNode g q-ns'@[defNode g p]→defNode g p" "length (ns'@[defNode g p]) > 1" by auto
show ?case
proof (rule base.prems(1)[OF ns, rule_format], rule exI, rule exI, rule exI, rule exI)
fix n
assume "n ∈ set (butlast (ns' @ [defNode g p]))"
with base.hyps ns'
show "r p q ∧
g ⊢ defNode g q-ns'→m ∧
defNode g q ∉ set (tl ns') ∧
q ∈ phiUses g m ∧
m ∈ set (predecessors g (defNode g p)) ∧ n ∈ set ns' ∧ set ns' ⊆ set (ns' @ [defNode g p]) ∧ defNode g p ∈ set (ns' @ [defNode g p])"
by auto
qed
next
case (step p p')
from step.prems(2) step.hyps(1) obtain ns'⇩2 m where ns'⇩2: "g ⊢ defNode g p'-ns'⇩2→m" "m ∈ set (predecessors g (defNode g p))" "defNode g p' ∉ set (tl ns'⇩2)" "p' ∈ phiUses g m"
by - (rule phiArg_path_ex', rule assms(3), auto intro: simple_path2)
then obtain ns⇩2 where ns⇩2: "g ⊢ defNode g p'-ns⇩2→defNode g p" "length ns⇩2 > 1" "ns⇩2 = ns'⇩2@[defNode g p]" by (atomize_elim, auto)
show thesis
proof (rule step.IH)
fix ns
assume ns: "g ⊢ defNode g q-ns→defNode g p'" "1 < length ns"
assume IH: "∀n∈set (butlast ns).
∃p q m ns'.
r p q ∧
g ⊢ defNode g q-ns'→m ∧
defNode g q ∉ set (tl ns') ∧
q ∈ phiUses g m ∧ m ∈ set (predecessors g (defNode g p)) ∧ n ∈ set ns' ∧ set ns' ⊆ set ns ∧ defNode g p ∈ set ns"
let ?path = "ns@tl ns⇩2"
have ns_ns⇩2: "g ⊢ defNode g q-?path→defNode g p" "1 < length ?path" using ns ns⇩2(1,2) by auto
show thesis
proof (rule step.prems(1)[OF ns_ns⇩2, rule_format])
fix n
assume n: "n ∈ set (butlast ?path)"
show "∃p q m ns'a.
r p q ∧
g ⊢ defNode g q-ns'a→m ∧
defNode g q ∉ set (tl ns'a) ∧
q ∈ phiUses g m ∧ m ∈ set (predecessors g (defNode g p)) ∧ n ∈ set ns'a ∧ set ns'a ⊆ set ?path ∧ defNode g p ∈ set ?path"
proof (cases "n ∈ set (butlast ns)")
case True
with IH obtain p q m ns' where "
r p q ∧
g ⊢ defNode g q-ns'→m ∧
defNode g q ∉ set (tl ns') ∧
q ∈ phiUses g m ∧ m ∈ set (predecessors g (defNode g p)) ∧ n ∈ set ns' ∧ set ns' ⊆ set ns ∧ defNode g p ∈ set ns" by auto
thus ?thesis by - (rule exI, rule exI, rule exI, rule exI, auto)
next
case False
from ns ns⇩2 have 1: "?path = butlast ns@ns⇩2"
by - (rule concat_join[symmetric], auto simp: path2_def)
from ns⇩2(1) n False 1 have "n ∈ set (butlast ns⇩2)" by (auto simp: butlast_append path2_not_Nil)
with step.hyps ns'⇩2 ns⇩2(3) show ?thesis
by - (subst 1, rule exI[where x=p], rule exI[where x=p'], rule exI, rule exI, auto simp: path2_not_Nil)
qed
qed
next
show "p' ∈ allVars g" using step.prems(2) step.hyps(1)[THEN assms(3)] by auto
qed
qed
lemma non_dominated_predecessor:
assumes "n ∈ set (αn g)" "n ≠ Entry g"
obtains m where "m ∈ set (predecessors g n)" "¬dominates g n m"
proof-
obtain ns where "g ⊢ Entry g-ns→n"
by (atomize_elim, rule Entry_reaches, auto simp add:assms(1))
then obtain ns' where ns': "g ⊢ Entry g-ns'→n" "n ∉ set (butlast ns')"
by (rule simple_path2)
let ?m = "last (butlast ns')"
from ns'(1) assms(2) obtain m: "g ⊢ Entry g-butlast ns'→?m" "?m ∈ set (predecessors g n)"
by - (rule path2_unsnoc, auto)
with m(1) ns'(2) show thesis
by - (rule that, auto elim:dominatesE)
qed
lemmas dominates_trans'[trans, elim] = dominates_trans[OF invar]
lemmas strict_dom_trans'[trans, elim] = strict_dom_trans[OF invar]
lemmas dominates_refl'[simp] = dominates_refl[OF invar]
lemmas dominates_antisymm'[dest] = dominates_antisymm[OF invar]
lemma liveVal_in_allVars[simp]: "liveVal g v ⟹ v ∈ allVars g"
by (induction rule: liveVal.induct, auto intro!: allUses_in_allVars)
lemma phi_no_closed_loop:
assumes[simp]: "p ∈ allVars g" and "phi g p = Some vs"
shows "set vs ≠ {p}"
proof (cases "defNode g p = Entry g")
case True
with assms(2) show ?thesis by auto
next
case False
show ?thesis
proof
assume[simp]: "set vs = {p}"
let ?n = "defNode g p"
obtain ns where ns: "g ⊢ Entry g-ns→?n" "?n ∉ set (butlast ns)" by (rule simple_Entry_path, auto)
let ?m = "last (butlast ns)"
from ns False obtain m: "g ⊢ Entry g-butlast ns→?m" "?m ∈ set (predecessors g ?n)"
by - (rule path2_unsnoc, auto)
hence "p ∈ phiUses g ?m" using assms(2) by - (rule phiUses_exI, auto simp:phi_def)
hence "defAss g ?m p" using m by - (rule allUses_def_ass, auto)
then obtain l where l: "l ∈ set (butlast ns)" "p ∈ allDefs g l" using m by - (drule defAssD, auto)
with assms(2) m have "l = ?n" by - (rule allDefs_disjoint', auto)
with ns l m show False by auto
qed
qed
lemma phis_phi: "phis g (n, v) = Some vs ⟹ phi g v = Some vs"
unfolding phi_def
apply (subst defNode_eq)
by (auto simp: allDefs_def phi_def phiDefs_def intro: phis_in_αn)
lemma trivial_phi: "trivial g v ⟹ phi g v ≠ None"
by (auto simp: trivial_def isTrivialPhi_def split: option.splits)
lemma trivial_finite: "finite {v. trivial g v}"
by (rule finite_subset[OF _ phi_finite]) (auto dest: trivial_phi)
lemma trivial_in_allVars: "trivial g v ⟹ v ∈ allVars g"
by (drule trivial_phi, auto simp: allDefs_def phiDefs_def image_def phi_def intro: phis_in_αn intro!: allDefs_in_allVars)
declare phiArg_def [simp del]
end
subsection ‹Bundling of CFG and Equivalent SSA CFG›
locale CFG_SSA_Transformed_base = old: CFG_base αe αn invar inEdges' Entry oldDefs oldUses + CFG_SSA_wf_base αe αn invar inEdges' Entry "defs" "uses" phis
for
αe :: "'g ⇒ ('node::linorder × 'edgeD × 'node) set" and
αn :: "'g ⇒ 'node list" and
invar :: "'g ⇒ bool" and
inEdges' :: "'g ⇒ 'node ⇒ ('node × 'edgeD) list" and
Entry::"'g ⇒ 'node" and
oldDefs :: "'g ⇒ 'node ⇒ 'var::linorder set" and
oldUses :: "'g ⇒ 'node ⇒ 'var set" and
"defs" :: "'g ⇒ 'node ⇒ 'val::linorder set" and
"uses" :: "'g ⇒ 'node ⇒ 'val set" and
phis :: "'g ⇒ ('node, 'val) phis" +
fixes var :: "'g ⇒ 'val ⇒ 'var"
locale CFG_SSA_Transformed = CFG_SSA_Transformed_base αe αn invar inEdges' Entry oldDefs oldUses "defs" "uses" phis var
+ old: CFG_wf αe αn invar inEdges' Entry oldDefs oldUses + CFG_SSA_wf αe αn invar inEdges' Entry "defs" "uses" phis
for
αe :: "'g ⇒ ('node::linorder × 'edgeD × 'node) set" and
αn :: "'g ⇒ 'node list" and
invar :: "'g ⇒ bool" and
inEdges' :: "'g ⇒ 'node ⇒ ('node × 'edgeD) list" and
Entry::"'g ⇒ 'node" and
oldDefs :: "'g ⇒ 'node ⇒ 'var::linorder set" and
oldUses :: "'g ⇒ 'node ⇒ 'var set" and
"defs" :: "'g ⇒ 'node ⇒ 'val::linorder set" and
"uses" :: "'g ⇒ 'node ⇒ 'val set" and
phis :: "'g ⇒ ('node, 'val) phis" and
var :: "'g ⇒ 'val ⇒ 'var" +
assumes oldDefs_def: "oldDefs g n = var g ` defs g n"
assumes oldUses_def: "n ∈ set (αn g) ⟹ oldUses g n = var g ` uses g n"
assumes conventional: "
⟦g ⊢ n-ns→m; n ∉ set (tl ns); v ∈ allDefs g n; v ∈ allUses g m; x ∈ set (tl ns); v' ∈ allDefs g x⟧ ⟹ var g v' ≠ var g v"
assumes phis_same_var[elim]: "phis g (n,v) = Some vs ⟹ v' ∈ set vs ⟹ var g v' = var g v"
assumes allDefs_var_disjoint: "⟦n ∈ set (αn g); v ∈ allDefs g n; v' ∈ allDefs g n; v ≠ v'⟧ ⟹ var g v' ≠ var g v"
begin
lemma conventional': "⟦g ⊢ n-ns→m; n ∉ set (tl ns); v ∈ allDefs g n; v ∈ allUses g m; v' ∈ allDefs g x; var g v' = var g v⟧ ⟹ x ∉ set (tl ns)"
using conventional by auto
lemma conventional'': "⟦g ⊢ defNode g v-ns→m; defNode g v ∉ set (tl ns); v ∈ allUses g m; var g v' = var g v; v ∈ allVars g; v' ∈ allVars g⟧ ⟹ defNode g v' ∉ set (tl ns)"
by (rule conventional'[where v=v and v'=v'], auto)
lemma phiArg_same_var: "phiArg g p q ⟹ var g q = var g p"
by (metis phiArg_def phi_def phis_same_var)
lemma oldDef_defAss:
assumes "v ∈ allUses g n" "g ⊢ Entry g-ns→n"
obtains m where "m ∈ set ns" "var g v ∈ oldDefs g m"
using assms proof (induction ns arbitrary: v n rule: length_induct)
case (1 ns)
from "1.prems"(2-) have 2: "defNode g v ∈ set ns"
by - (rule defAss_defNode, rule allUses_def_ass, auto)
let ?V = "defNode g v"
from "1.prems"(2,3) have[simp]: "v ∈ allVars g" by auto
thus ?case
proof (cases v rule: defNode_cases)
case simpleDef
with 2 show thesis by - (rule "1.prems"(1), auto simp: oldDefs_def)
next
case phi
then obtain vs where vs: "phi g v = Some vs" by auto
from "1.prems"(3) 2 obtain ns' where ns': "g ⊢ Entry g-ns'→?V" "prefix ns' ns"
by (rule old.path2_split_ex, auto)
let ?V' = "last (butlast ns')"
from ns' phi have nontriv: "length ns' ≥ 2"
by - (rule old.path2_nontrivial, auto)
hence 3: "g ⊢ Entry g-butlast ns'→?V'" "?V' ∈ set (old.predecessors g ?V)"
using ns'(1) by (auto intro: old.path2_unsnoc)
with phi vs obtain v' where v': "v' ∈ phiUses g ?V'" "var g v' = var g v"
by - (rule phiArg_exI, auto simp: phi_def phis_same_var phiArg_def)
show thesis
proof (rule "1.IH"[rule_format])
show "length (butlast ns') < length ns" using ns' by (cases ns', auto simp: old.path2_not_Nil2 dest: prefix_length_le)
show "v' ∈ allUses g ?V'" using v'(1) by simp
next
fix n
assume "n ∈ set (butlast ns')" "var g v' ∈ oldDefs g n"
thus thesis
using ns'(2)[THEN set_mono_prefix] v'(2) by - (rule "1.prems"(1)[of n], auto dest: in_set_butlastD)
qed (rule 3(1))
qed
qed
lemma allDef_path_from_simpleDef:
assumes[simp]: "v ∈ allVars g"
obtains n ns where "g ⊢ n-ns→defNode g v" "old.EntryPath g ns" "var g v ∈ oldDefs g n"
proof-
let ?V = "defNode g v"
from assms obtain ns where ns: "g ⊢ Entry g-ns→?V" "old.EntryPath g ns"
by - (rule old.Entry_reachesE, auto)
from assms show thesis
proof (cases v rule: defNode_cases)
case simpleDef
thus thesis by - (rule that, auto simp: oldDefs_def)
next
case phi
then obtain vs where vs: "phi g v = Some vs" by auto
let ?V' = "last (butlast ns)"
from ns phi have nontriv: "length ns ≥ 2"
by - (rule old.path2_nontrivial, auto)
hence 3: "g ⊢ Entry g-butlast ns→?V'" "?V' ∈ set (old.predecessors g ?V)"
using ns(1) by (auto intro: old.path2_unsnoc)
with phi vs obtain v' where v': "v' ∈ phiUses g ?V'" "var g v' = var g v"
by - (rule phiArg_exI, auto simp: phi_def phis_same_var phiArg_def)
with 3(1) obtain n where n: "n ∈ set (butlast ns)" "var g v' ∈ oldDefs g n"
by - (rule oldDef_defAss[of v' g], auto)
with ns obtain ns' where "g ⊢ n-ns'→?V" "suffix ns' ns"
by - (rule old.path2_split_ex'[OF ns(1)], auto intro: in_set_butlastD simp: Sublist.suffix_def)
with n(2) v'(2) ns(2) show thesis
by - (rule that, assumption, erule old.EntryPath_suffix, auto)
qed
qed
lemma defNode_var_disjoint:
assumes "p ∈ allVars g" "q ∈ allVars g" "p ≠ q" "defNode g p = defNode g q"
shows "var g p ≠ var g q"
proof-
have "q ∈ allDefs g (defNode g p)" using assms(2) assms(4) by (auto)
thus ?thesis using assms(1-3)
by - (rule allDefs_var_disjoint[of "defNode g p" g], auto)
qed
lemma phiArg_distinct_nodes:
assumes "phiArg g p q" "p ≠ q" and[simp]: "p ∈ allVars g"
shows "defNode g p ≠ defNode g q"
proof
have "p ∈ allDefs g (defNode g p)" by simp
moreover assume "defNode g p = defNode g q"
ultimately have "var g p ≠ var g q" using assms
by - (rule defNode_var_disjoint, auto)
moreover
from assms(1) have "var g q = var g p" by (rule phiArg_same_var)
ultimately show False by simp
qed
lemma phiArgs_def_distinct:
assumes "phiArg g p q" "phiArg g p r" "q ≠ r" "p ∈ allVars g"
shows "defNode g q ≠ defNode g r"
proof (rule)
assume "defNode g q = defNode g r"
hence "var g q ≠ var g r" using assms by - (rule defNode_var_disjoint, auto)
thus False using phiArg_same_var[OF assms(1)] phiArg_same_var[OF assms(2)] by simp
qed
lemma defNode_not_on_defUse_path:
assumes p: "g ⊢ defNode g p-ns→n" "defNode g p ∉ set (tl ns)" "p ∈ allUses g n"
assumes[simp]: "q ∈ allVars g" "p ≠ q" "var g p = var g q"
shows "defNode g q ∉ set ns"
proof-
let ?P = "defNode g p"
let ?Q = "defNode g q"
have[simp]: "p ∈ allVars g" using p(1,3) by auto
have "?P ≠ ?Q" using defNode_var_disjoint[of p g q] by auto
moreover have "?Q ∉ set (tl ns)" using p(2,3)
by - (rule conventional'[OF p(1), of p q], auto)
ultimately show ?thesis using p(1) by (cases ns, auto simp: old.path2_def)
qed
lemma defUse_paths_disjoint:
assumes p: "g ⊢ defNode g p-ns→n" "defNode g p ∉ set (tl ns)" "p ∈ allUses g n"
assumes q: "g ⊢ defNode g q-ms→m" "defNode g q ∉ set (tl ms)" "q ∈ allUses g m"
assumes[simp]: "p ≠ q" "var g p = var g q"
shows "set ns ∩ set ms = {}"
proof (rule equals0I)
fix y
assume y: "y ∈ set ns ∩ set ms"
{
fix p ns n
assume p: "g ⊢ defNode g p-ns→n" "defNode g p ∉ set (tl ns)" "p ∈ allUses g n"
assume y: "y ∈ set ns"
from p(1,3) have dom: "old.dominates g (defNode g p) n" by - (rule allUses_dominated, auto)
moreover
obtain ns' where "g ⊢ y-ns'→n" "suffix ns' ns"
by (rule old.path2_split_first_last[OF p(1) y], auto)
ultimately have "old.dominates g (defNode g p) y" using suffix_tl_subset[of ns' ns] p(2)
by - (rule old.dominates_extend[where ms=ns'], auto)
}
with assms y have dom: "old.dominates g (defNode g p) y" "old.dominates g (defNode g q) y" by auto
{
fix p ns n q ms m
let ?P = "defNode g p"
let ?Q = "defNode g q"
assume p: "g ⊢ defNode g p-ns→n" "defNode g p ∉ set (tl ns)" "p ∈ allUses g n" "old.dominates g ?P y" "y ∈ set ns"
assume q: "g ⊢ defNode g q-ms→m" "defNode g q ∉ set (tl ms)" "q ∈ allUses g m" "old.dominates g ?Q y" "y ∈ set ms"
assume[simp]: "p ≠ q" "var g p = var g q"
assume dom: "old.dominates g ?P ?Q"
then obtain pqs where pqs: "g ⊢ ?P-pqs→?Q" "?P ∉ set (tl pqs)" by (rule old.dominates_path, auto intro: old.simple_path2)
from p obtain ns⇩2 where ns⇩2: "g ⊢ y-ns⇩2→n" "suffix ns⇩2 ns" by - (rule old.path2_split_first_last, auto)
from q obtain ms⇩1 where ms⇩1: "g ⊢ ?Q-ms⇩1→y" "prefix ms⇩1 ms" by - (rule old.path2_split_first_last, auto)
have "var g q ≠ var g p"
proof (rule conventional[OF _ _ _ p(3)])
let ?path = "(pqs@tl ms⇩1)@tl ns⇩2"
show "g ⊢ ?P-?path→n" using pqs ms⇩1 ns⇩2
by (auto simp del:append_assoc intro:old.path2_app)
have "?P ∉ set (tl ns⇩2)" using p(2) ns⇩2(2)[THEN suffix_tl_subset, THEN subsetD] by auto
moreover
have[simp]: "q ∈ allVars g" "p ∈ allVars g" using p q by auto
have "?P ∉ set (tl ms)" using q
by - (rule conventional'[where v'=p and v=q], auto)
hence "?P ∉ set (tl ms⇩1)" using ms⇩1(2)[simplified, THEN prefix_tl_subset] by auto
ultimately
show "?P ∉ set (tl ?path)" using pqs(2)
by - (rule notI, auto dest: subsetD[OF set_tl_append'])
show "p ∈ allDefs g (defNode g p)" by auto
have "?P ≠ ?Q" using defNode_var_disjoint[of p g q] by auto
hence 1: "length pqs > 1" using pqs by - (rule old.path2_nontriv)
hence "?Q ∈ set (tl pqs)" using pqs unfolding old.path2_def by (auto intro:last_in_tl)
moreover from 1 have "pqs ≠ []" by auto
ultimately show "?Q ∈ set (tl ?path)" by simp
show "q ∈ allDefs g ?Q" by simp
qed
hence False by simp
}
from this[OF p _ _ q] this[OF q _ _ p] y dom show False
by - (rule old.dominates_antitrans[OF _ dom], auto)
qed
lemma oldDefsI: "v ∈ defs g n ⟹ var g v ∈ oldDefs g n" by (simp add: oldDefs_def)
lemma simpleDefs_phiDefs_var_disjoint:
assumes "v ∈ phiDefs g n" "n ∈ set (αn g)"
shows "var g v ∉ oldDefs g n"
proof
from assms have[simp]: "v ∈ allVars g" by auto
assume "var g v ∈ oldDefs g n"
then obtain v'' where v'': "v'' ∈ defs g n" "var g v'' = var g v"
by (auto simp: oldDefs_def)
from this(1) assms have "v'' ≠ v"
using simpleDefs_phiDefs_disjoint[of n g] by (auto simp: phiArg_def)
with v'' assms show False
using allDefs_var_disjoint[of n g v'' v] by auto
qed
lemma liveVal_use_path:
assumes "liveVal g v"
obtains ns m where "g ⊢ defNode g v-ns→m" "var g v ∈ oldUses g m"
"⋀x. x ∈ set (tl ns) ⟹ var g v ∉ oldDefs g x"
using assms proof (induction)
case (liveSimple m v)
from liveSimple.hyps have[simp]: "v ∈ allVars g"
by - (rule allUses_in_allVars, auto)
from liveSimple.hyps obtain ns where ns: "g ⊢ defNode g v-ns→m" "defNode g v ∉ set (tl ns)"
by - (rule defUse_path_ex, auto intro!: uses_in_allUses elim: old.simple_path2)
from this(1) show thesis
proof (rule liveSimple.prems)
show "var g v ∈ oldUses g m" using liveSimple.hyps by (auto simp: oldUses_def)
{
fix x
assume asm: "x ∈ set (tl ns)" "var g v ∈ oldDefs g x"
then obtain v' where "v' ∈ defs g x" "var g v' = var g v"
by (auto simp: oldDefs_def)
with asm liveSimple.hyps have False
by - (rule conventional[OF ns, of v x v', THEN notE], auto)
}
thus "⋀x. x ∈ set (tl ns) ⟹ var g v ∉ oldDefs g x" by auto
qed
next
case (livePhi v v')
from livePhi.hyps have[simp]: "v ∈ allVars g" "v' ∈ allVars g" "var g v' = var g v"
by (auto intro: phiArg_same_var)
show thesis
proof (rule livePhi.IH)
fix ns m
assume asm: "g ⊢ defNode g v-ns→m" "var g v ∈ oldUses g m"
"⋀x. x ∈ set (tl ns) ⟹ var g v ∉ oldDefs g x"
from livePhi.hyps(2) obtain ns' m' where ns': "g ⊢ defNode g v'-ns'→m'" "v' ∈ phiUses g m'"
"m' ∈ set (old.predecessors g (defNode g v))" "defNode g v' ∉ set (tl ns')"
by (rule phiArg_path_ex', auto elim: old.simple_path2)
show thesis
proof (rule livePhi.prems)
show "g ⊢ defNode g v'-(ns'@[defNode g v])@tl ns→m"
apply (rule old.path2_app)
apply (rule old.path2_snoc[OF ns'(1,3)])
by (rule asm(1))
show "var g v' ∈ oldUses g m" using asm(2) by simp
{
fix x
assume asm: "x ∈ set (tl ns')" "var g v ∈ oldDefs g x"
then obtain v'' where "v'' ∈ defs g x" "var g v'' = var g v"
by (auto simp: oldDefs_def)
with asm ns'(2) have False
by - (rule conventional[OF ns'(1,4), of v' x v'', THEN notE], auto)
}
then show "⋀x. x ∈ set (tl ((ns'@[defNode g v])@tl ns)) ⟹ var g v' ∉ oldDefs g x"
using simpleDefs_phiDefs_var_disjoint[of v g "defNode g v"] livePhi.hyps(2)
by (auto dest!: set_tl_append'[THEN subsetD] asm(3) simp: phiArg_def)
qed
qed
qed
end
end