Theory Construct_SSA_notriv
subsection ‹Inductive Removal of Trivial Phi Functions›
theory Construct_SSA_notriv
imports SSA_CFG Minimality "HOL-Library.While_Combinator"
begin
locale CFG_SSA_Transformed_notriv_base = CFG_SSA_Transformed_base αe αn invar inEdges' Entry oldDefs oldUses "defs" "uses" phis var
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" +
fixes chooseNext_all :: "('node ⇒ 'val set) ⇒ ('node, 'val) phis ⇒ 'g ⇒ ('node × 'val)"
begin
abbreviation "chooseNext g ≡ snd (chooseNext_all (uses g) (phis g) g)"
abbreviation "chooseNext' g ≡ chooseNext_all (uses g) (phis g) g"
definition "substitution g ≡ THE v'. isTrivialPhi g (chooseNext g) v'"
definition "substNext g ≡ λv. if v = chooseNext g then substitution g else v"
definition[simp]: "uses' g n ≡ substNext g ` uses g n"
definition[simp]: "phis' g x ≡ case x of (n,v) ⇒ if v = chooseNext g
then None
else map_option (map (substNext g)) (phis g (n,v))"
end
locale CFG_SSA_Transformed_notriv = CFG_SSA_Transformed αe αn invar inEdges' Entry oldDefs oldUses "defs" "uses" phis var
+ CFG_SSA_Transformed_notriv_base αe αn invar inEdges' Entry oldDefs oldUses "defs" "uses" phis var chooseNext_all
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" and
chooseNext_all :: "('node ⇒ 'val set) ⇒ ('node, 'val) phis ⇒ 'g ⇒ ('node × 'val)" +
assumes chooseNext_all: "CFG_SSA_Transformed αe αn invar inEdges' Entry oldDefs oldUses defs u p var ⟹
CFG_SSA_wf_base.redundant αn inEdges' defs u p g ⟹
chooseNext_all (u g) (p g) g ∈ dom (p g) ∧
CFG_SSA_wf_base.trivial αn inEdges' defs u p g (snd (chooseNext_all (u g) (p g) g))"
begin
lemma chooseNext':"redundant g ⟹ chooseNext' g ∈ dom (phis g) ∧ trivial g (chooseNext g)"
by (rule chooseNext_all, unfold_locales)
lemma chooseNext: "redundant g ⟹ chooseNext g ∈ allVars g ∧ trivial g (chooseNext g)"
by (drule chooseNext', auto simp: trivial_in_allVars)
lemmas chooseNext_in_allVars[simp] = chooseNext[THEN conjunct1]
lemma isTrivialPhi_det: "trivial g v ⟹ ∃!v'. isTrivialPhi g v v'"
proof(rule ex_ex1I)
fix v' v''
assume "isTrivialPhi g v v'" "isTrivialPhi g v v''"
from this[unfolded isTrivialPhi_def, THEN conjunct2] show "v' = v''" by (auto simp:isTrivialPhi_def doubleton_eq_iff split:option.splits)
qed (auto simp: trivial_def)
lemma trivialPhi_strict_dom:
assumes[simp]: "v ∈ allVars g" and triv: "isTrivialPhi g v v'"
shows "strict_def_dom g v' v"
proof
let ?n = "defNode g v"
let ?n' = "defNode g v'"
from triv obtain vs where vs: "phi g v = Some vs" "(set vs = {v'} ∨ set vs = {v,v'})" by (auto simp:isTrivialPhi_def split:option.splits)
hence "?n ≠ Entry g" by auto
have other_preds_dominated: "⋀m. m ∈ set (old.predecessors g ?n) ⟹ v' ∉ phiUses g m ⟹ old.dominates g ?n m"
proof-
fix m
assume m: "m ∈ set (old.predecessors g ?n)" "v' ∉ phiUses g m"
hence[simp]: "m ∈ set (αn g)" by auto
show "old.dominates g ?n m"
proof (cases "v ∈ phiUses g m")
case True
hence "v ∈ allUses g m" by simp
thus ?thesis by (rule allUses_dominated) simp_all
next
case False
with vs have "v' ∈ phiUses g m" by - (rule phiUses_exI[OF m(1)], auto simp:phi_def)
with m(2) show ?thesis by simp
qed
qed
show "?n' ≠ ?n"
proof (rule notI)
assume asm: "?n' = ?n"
have "⋀m. m ∈ set (old.predecessors g ?n) ⟹ v' ∈ phiUses g m ⟹ old.dominates g ?n m"
proof-
fix m
assume "m ∈ set (old.predecessors g ?n)" "v' ∈ phiUses g m"
hence "old.dominates g ?n' m" by - (rule allUses_dominated, auto)
thus "?thesis m" by (simp add:asm)
qed
with non_dominated_predecessor[of ?n g] other_preds_dominated ‹?n ≠ Entry g› show False by auto
qed
show "old.dominates g ?n' ?n"
proof
fix ns
assume asm: "g ⊢ Entry g-ns→?n"
from ‹?n ≠ Entry g› obtain m ns'
where ns': "g ⊢ Entry g-ns'→m" "m ∈ set (old.predecessors g ?n)" "?n ∉ set ns'" "set ns' ⊆ set ns"
by - (rule old.simple_path2_unsnoc[OF asm], auto)
hence[simp]: "m ∈ set (αn g)" by auto
from ns' have "¬old.dominates g ?n m" by (auto elim:old.dominatesE)
with other_preds_dominated[of m] ns'(2) have "v' ∈ phiUses g m" by auto
hence "old.dominates g ?n' m" by - (rule allUses_dominated, auto)
with ns'(1) have "?n' ∈ set ns'" by - (erule old.dominatesE)
with ns'(4) show "?n' ∈ set ns" by auto
qed auto
qed
lemma isTrivialPhi_asymmetric:
assumes "isTrivialPhi g a b"
and "isTrivialPhi g b a"
shows "False"
using assms
proof -
from ‹isTrivialPhi g a b›
have "b ∈ allVars g"
unfolding isTrivialPhi_def
by (fastforce intro!: phiArg_in_allVars simp: phiArg_def split: option.splits)
from ‹isTrivialPhi g b a›
have "a ∈ allVars g"
unfolding isTrivialPhi_def
by (fastforce intro!: phiArg_in_allVars simp: phiArg_def split: option.splits)
from trivialPhi_strict_dom [OF ‹a ∈ allVars g› assms(1)]
trivialPhi_strict_dom [OF ‹b ∈ allVars g› assms(2)]
show ?thesis by blast
qed
lemma substitution[intro]: "redundant g ⟹ isTrivialPhi g (chooseNext g) (substitution g)"
unfolding substitution_def by (rule theI', rule isTrivialPhi_det, simp add: chooseNext)
lemma trivialPhi_in_allVars[simp]:
assumes "isTrivialPhi g v v'" and[simp]: "v ∈ allVars g"
shows "v' ∈ allVars g"
proof-
from assms(1) have "phiArg g v v'"
unfolding phiArg_def
by (auto simp:isTrivialPhi_def split:option.splits)
thus "v' ∈ allVars g" by - (rule phiArg_in_allVars, auto)
qed
lemma substitution_in_allVars[simp]:
assumes "redundant g"
shows "substitution g ∈ allVars g"
using assms by - (rule trivialPhi_in_allVars, auto)
lemma defs_uses_disjoint_inv:
assumes[simp]: "n ∈ set (αn g)" "redundant g"
shows "defs g n ∩ uses' g n = {}"
proof (rule equals0I)
fix v'
assume asm: "v' ∈ defs g n ∩ uses' g n"
then obtain v where v: "v ∈ uses g n" "v' = substNext g v" and v': "v' ∈ defs g n" by auto
show False
proof (cases "v = chooseNext g")
case False
thus ?thesis using v v' defs_uses_disjoint[of n g] by (auto simp:substNext_def split:if_split_asm)
next
case [simp]: True
from v' have n_defNode: "n = defNode g v'" by - (rule defNode_eq[symmetric], auto)
from v(1) have[simp]: "v ∈ allVars g" by - (rule allUses_in_allVars[where n=n], auto)
let ?n' = "defNode g v"
have "old.strict_dom g n ?n'"
by (simp only:n_defNode v(2), rule trivialPhi_strict_dom, auto simp:substNext_def)
moreover from v(1) have "old.dominates g ?n' n" by - (rule allUses_dominated, auto)
ultimately show False by auto
qed
qed
end
context CFG_SSA_wf
begin
inductive liveVal' :: "'g ⇒ 'val list ⇒ bool"
for g :: 'g
where
liveSimple': "⟦n ∈ set (αn g); val ∈ uses g n⟧ ⟹ liveVal' g [val]"
| livePhi': "⟦liveVal' g (v#vs); phiArg g v v'⟧ ⟹ liveVal' g (v'#v#vs)"
lemma liveVal'_suffix:
assumes "liveVal' g vs" "suffix vs' vs" "vs' ≠ []"
shows "liveVal' g vs'"
using assms proof induction
case (liveSimple' n v)
from liveSimple'.prems have "vs' = [v]"
by (metis append_Nil butlast.simps(2) suffixI suffix_order.order_antisym suffix_unsnoc)
with liveSimple'.hyps show ?case by (auto intro: liveVal'.liveSimple')
next
case (livePhi' v vs v')
show ?case
proof (cases "vs' = v' # v # vs")
case True
with livePhi' show ?thesis by - (auto intro: liveVal'.livePhi')
next
case False
with livePhi'.prems have "suffix vs' (v#vs)"
by (metis list.sel(3) self_append_conv2 suffixI suffix_take tl_append2)
with livePhi'.prems(2) show ?thesis by - (rule livePhi'.IH)
qed
qed
lemma liveVal'I:
assumes "liveVal g v"
obtains vs where "liveVal' g (v#vs)"
using assms proof induction
case (liveSimple n v)
thus thesis by - (rule liveSimple(3), rule liveSimple')
next
case (livePhi v v')
show thesis
proof (rule livePhi.IH)
fix vs
assume asm: "liveVal' g (v#vs)"
show thesis
proof (cases "v' ∈ set (v#vs)")
case False
with livePhi.hyps asm show thesis by - (rule livePhi.prems, rule livePhi')
next
case True
then obtain vs' where "suffix (v'#vs') (v#vs)"
by - (drule split_list_last, auto simp: Sublist.suffix_def)
with asm show thesis by - (rule livePhi.prems, rule liveVal'_suffix, simp_all)
qed
qed
qed
lemma liveVal'D:
assumes "liveVal' g vs" "vs = v#vs'"
shows "liveVal g v"
using assms proof (induction arbitrary: v vs')
case (liveSimple' n vs)
thus ?case by - (rule liveSimple, auto)
next
case (livePhi' v⇩2 vs v')
thus ?case by - (rule livePhi, auto)
qed
end
locale CFG_SSA_step = CFG_SSA_Transformed_notriv αe αn invar inEdges' Entry oldDefs oldUses "defs" "uses" phis var chooseNext_all
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" and
chooseNext_all :: "('node ⇒ 'val set) ⇒ ('node, 'val) phis ⇒ 'g ⇒ ('node × 'val)" and
g :: "'g" +
assumes redundant[simp]: "redundant g"
begin
abbreviation "u_g ≡ uses(g:=uses' g)"
abbreviation "p_g ≡ phis(g:=phis' g)"
sublocale step: CFG_SSA_Transformed_notriv_base αe αn invar inEdges' Entry oldDefs oldUses "defs" u_g p_g var chooseNext_all .
lemma simpleDefs_phiDefs_disjoint_inv:
assumes "n ∈ set (αn g)"
shows "defs g n ∩ step.phiDefs g n = {}"
using simpleDefs_phiDefs_disjoint[OF assms]
by (auto simp: phiDefs_def step.phiDefs_def dom_def split:option.splits)
lemma allDefs_disjoint_inv:
assumes "n ∈ set (αn g)" "m ∈ set (αn g)" "n ≠ m"
shows "step.allDefs g n ∩ step.allDefs g m = {}"
using allDefs_disjoint[OF assms]
by (auto simp: CFG_SSA_defs step.CFG_SSA_defs dom_def split:option.splits)
lemma phis_finite_inv:
shows "finite (dom (phis' g))"
using phis_finite[of g] by - (rule finite_subset, auto split:if_split_asm)
lemma phis_wf_inv:
assumes "phis' g (n, v) = Some args"
shows "length (old.predecessors g n) = length args"
using phis_wf[of g] assms by (auto split:if_split_asm)
sublocale step: CFG_SSA αe αn invar inEdges' Entry "defs" u_g p_g
apply unfold_locales
apply (rename_tac g')
apply (case_tac "g'=g")
apply (simp add:defs_uses_disjoint_inv[simplified])
apply (simp add:defs_uses_disjoint)
apply (rule defs_finite)
apply (auto simp: uses_in_αn split: if_split_asm)[1]
apply (rename_tac g' n)
apply (case_tac "g'=g")
apply simp
apply simp
apply (rule invar)
apply (rename_tac g')
apply (case_tac "g'=g")
apply (simp add:phis_finite_inv)
apply (simp add:phis_finite)
apply (auto simp: phis_in_αn split: if_split_asm)[1]
apply (rename_tac g' n v args)
apply (case_tac "g'=g")
apply (simp add:phis_wf_inv)
apply (simp add:phis_wf)
apply (rename_tac g')
apply (case_tac "g'=g")
apply (simp add: simpleDefs_phiDefs_disjoint_inv)
apply (simp add: simpleDefs_phiDefs_disjoint[unfolded CFG_SSA_defs] step.CFG_SSA_defs )
apply (rename_tac g' m)
apply (case_tac "g'=g")
apply (simp add: allDefs_disjoint_inv)
apply (simp add: allDefs_disjoint[unfolded CFG_SSA_defs] step.CFG_SSA_defs)
done
lemma allUses_narrows:
assumes "n ∈ set (αn g)"
shows "step.allUses g n ⊆ substNext g ` allUses g n"
proof-
have "⋀n' v' z b. phis g (n', v') = Some z ⟹ (n, b) ∈ set (zip (old.predecessors g n') z) ⟹ b ∉ phiUses g n ⟹ b ∈ uses g n"
proof-
fix n' v' z b
assume "(n, b) ∈ set (zip (old.predecessors g n') (z :: 'val list))"
with assms(1) have "n' ∈ set (αn g)" by auto
thus "phis g (n', v') = Some z ⟹ (n, b) ∈ set (zip (old.predecessors g n') z) ⟹ b ∉ phiUses g n ⟹ b ∈ uses g n" by (auto intro:phiUsesI)
qed
thus ?thesis by (auto simp:step.allUses_def allUses_def zip_map2 intro!:imageI elim!:step.phiUsesE phiUsesE split:if_split_asm)
qed
lemma allDefs_narrows[simp]: "v ∈ step.allDefs g n ⟹ v ∈ allDefs g n"
by (auto simp:step.allDefs_def step.phiDefs_def phiDefs_def allDefs_def split:if_split_asm)
lemma allUses_def_ass_inv:
assumes "v' ∈ step.allUses g n" "n ∈ set (αn g)"
shows "step.defAss g n v'"
proof (rule step.defAssI)
fix ns
assume asm: "g ⊢ Entry g-ns→n"
from assms obtain v where v': "v' = substNext g v" and[simp]: "v ∈ allUses g n"
using allUses_narrows by auto
with assms(2) have[simp]: "v ∈ allVars g" by - (rule allUses_in_allVars)
have[simp]: "v' ∈ allVars g" by (simp add:substNext_def v')
let ?n⇩v = "defNode g v"
let ?n⇩v⇩' = "defNode g v'"
from assms(2) asm have 1: "?n⇩v ∈ set ns" using allUses_def_ass[of v g n] by (simp add:defAss_defNode)
then obtain ns⇩v where ns⇩v: "prefix (ns⇩v@[?n⇩v]) ns" by (rule prefix_split_first)
with asm have 2: "g ⊢ Entry g-ns⇩v@[?n⇩v]→?n⇩v" by auto
show "∃n ∈ set ns. v' ∈ step.allDefs g n"
proof (cases "v = chooseNext g")
case True
hence dom: "strict_def_dom g v' v" using substitution[of g] by - (rule trivialPhi_strict_dom, simp_all add:substNext_def v')
hence[simp]: "v' ≠ v" by auto
have "v' ∈ allDefs g ?n⇩v⇩'" by simp
hence "v' ∈ step.allDefs g ?n⇩v⇩'" unfolding step.allDefs_def step.phiDefs_def allDefs_def phiDefs_def by (auto simp:True[symmetric])
moreover have "?n⇩v⇩' ∈ set ns"
proof-
from dom have "def_dominates g v' v" by auto
hence "?n⇩v⇩' ∈ set (ns⇩v@[?n⇩v])" using 2 by -(erule old.dominatesE)
with ns⇩v show ?thesis by auto
qed
ultimately show ?thesis by auto
next
case [simp]: False
have[simp]: "v' = v" by (simp add:v' substNext_def)
have "v ∈ allDefs g ?n⇩v" by simp
thus ?thesis by - (rule bexI[of _ ?n⇩v⇩'], auto simp:allDefs_def step.allDefs_def step.phiDefs_def 1 phiDefs_def)
qed
qed
lemma Entry_no_phis_inv: "phis' g (Entry g, v) = None"
by (simp add:Entry_no_phis)
sublocale step: CFG_SSA_wf αe αn invar inEdges' Entry "defs" u_g p_g
apply unfold_locales
apply (rename_tac g' n)
apply (case_tac "g'=g")
apply (simp add:allUses_def_ass_inv)
apply (simp add:allUses_def_ass[unfolded CFG_SSA_defs, simplified] step.CFG_SSA_defs)
apply (rename_tac g' v)
apply (case_tac "g'=g")
apply (simp add:Entry_no_phis_inv)
apply (simp)
done
lemma chooseNext_eliminated: "chooseNext g ∉ step.allDefs g (defNode g (chooseNext g))"
proof-
let ?v = "chooseNext g"
let ?n = "defNode g ?v"
from chooseNext[OF redundant] have "?v ∈ phiDefs g ?n" "?n ∈ set (αn g)"
by (auto simp: trivial_def isTrivialPhi_def phiDefs_def phi_def split: option.splits)
hence "?v ∉ defs g ?n" using simpleDefs_phiDefs_disjoint[of ?n g] by auto
thus ?thesis by (auto simp:step.allDefs_def step.phiDefs_def)
qed
lemma oldUses_inv:
assumes "n ∈ set (αn g)"
shows "oldUses g n = var g ` u_g g n"
proof-
have "var g (substitution g) = var g (chooseNext g)" using substitution[of g]
by - (rule phiArg_same_var, auto simp: isTrivialPhi_def phiArg_def split: option.splits)
thus ?thesis using assms by (auto simp: substNext_def oldUses_def image_Un)
qed
lemma conventional_inv:
assumes "g ⊢ n-ns→m" "n ∉ set (tl ns)" "v ∈ step.allDefs g n" "v ∈ step.allUses g m" "x ∈ set (tl ns)" "v' ∈ step.allDefs g x"
shows "var g v' ≠ var g v"
proof-
from assms(1,3) have[simp]: "n = defNode g v" "v ∈ allDefs g n" by - (rule defNode_eq[symmetric], auto)
from assms(1) have[simp]: "m ∈ set (αn g)" by auto
from assms(4) obtain v⇩0 where v⇩0: "v = substNext g v⇩0" "v⇩0 ∈ allUses g m" using allUses_narrows[of m] by auto
hence[simp]: "v⇩0 ∈ allVars g" using assms(1) by auto
let ?n⇩0 = "defNode g v⇩0"
show ?thesis
proof (cases "v⇩0 = chooseNext g")
case False
with v⇩0 have "v = v⇩0" by (simp add:substNext_def split:if_split_asm)
with assms v⇩0 show ?thesis by - (rule conventional, auto)
next
case True
hence dom: "strict_def_dom g v v⇩0" using substitution[of g] by - (rule trivialPhi_strict_dom, simp_all add:substNext_def v⇩0)
from v⇩0(2) have "old.dominates g ?n⇩0 m" using assms(1) by - (rule allUses_dominated, auto)
with assms(1) dom have "?n⇩0 ∈ set ns" by - (rule old.dominates_mid, auto)
with assms(1) obtain ns⇩1 ns⇩3 ns⇩2 where
ns: "ns = ns⇩1@ns⇩3@ns⇩2" and
ns⇩1: "g ⊢ n-ns⇩1@[?n⇩0]→?n⇩0" "?n⇩0 ∉ set ns⇩1" and
ns⇩3: "g ⊢ ?n⇩0-ns⇩3→?n⇩0" and
ns⇩2: "g ⊢ ?n⇩0-?n⇩0#ns⇩2→m" "?n⇩0 ∉ set ns⇩2" by (rule old.path2_split_first_last)
have[simp]: "ns⇩1 ≠ []"
proof
assume "ns⇩1 = []"
hence "?n⇩0 = n" "hd ns = n" using assms(1) ns⇩3 by (auto simp:ns old.path2_def)
thus False by (metis ‹n = defNode g v› dom)
qed
hence "length (ns⇩1@[?n⇩0]) ≥ 2" by (cases ns⇩1, auto)
with ns⇩1 have 1: "g ⊢ n-ns⇩1→last ns⇩1" "last ns⇩1 ∈ set (old.predecessors g ?n⇩0)" by - (erule old.path2_unsnoc, simp, simp, erule old.path2_unsnoc, auto)
from ‹v⇩0 = chooseNext g› v⇩0 have triv: "isTrivialPhi g v⇩0 v" using substitution[of g] by (auto simp:substNext_def)
then obtain vs where vs: "phi g v⇩0 = Some vs" "set vs = {v⇩0,v} ∨ set vs = {v}" by (auto simp:isTrivialPhi_def split:option.splits)
hence[simp]: "var g v⇩0 = var g v" by - (rule phiArg_same_var[symmetric], auto simp: phiArg_def)
have[simp]: "v ∈ phiUses g (last ns⇩1)"
proof-
from vs ns⇩1 1 have "v ∈ phiUses g (last ns⇩1) ∨ v⇩0 ∈ phiUses g (last ns⇩1)" by - (rule phiUses_exI[of "last ns⇩1" g ?n⇩0 v⇩0 vs], auto simp:phi_def)
moreover have "v⇩0 ∉ phiUses g (last ns⇩1)"
proof
assume asm: "v⇩0 ∈ phiUses g (last ns⇩1)"
from True have "last ns⇩1 ∈ set ns⇩1" by - (rule last_in_set, auto)
hence "last ns⇩1 ∈ set (αn g)" by - (rule old.path2_in_αn[OF ns⇩1(1)], auto)
with asm ns⇩1 have "old.dominates g ?n⇩0 (last ns⇩1)" by - (rule allUses_dominated, auto)
moreover have "strict_def_dom g v v⇩0" using triv by - (rule trivialPhi_strict_dom, auto)
ultimately have "?n⇩0 ∈ set ns⇩1" using 1(1) by - (rule old.dominates_mid, auto)
with ns⇩1(2) show False ..
qed
ultimately show ?thesis by simp
qed
show ?thesis
proof (cases "x ∈ set (tl ns⇩1)")
case True
thus ?thesis using assms(2,3,6) by - (rule conventional[where x=x, OF 1(1)], auto simp:ns)
next
case False
show ?thesis
proof (cases "var g v' = var g v⇩0")
case [simp]: True
{
assume asm: "x ∈ set ns⇩3"
with assms(6)[THEN allDefs_narrows] have[simp]: "x = defNode g v'"
using ns⇩3 by - (rule defNode_eq[symmetric], auto)
{
assume "v' = v⇩0"
hence False using assms(6) ‹v⇩0 = chooseNext g› simpleDefs_phiDefs_disjoint[of x g] vs(1)
by (auto simp: step.allDefs_def step.phiDefs_def)
}
moreover {
assume "v' ≠ v⇩0"
hence "x ≠ ?n⇩0" using allDefs_var_disjoint[OF _ assms(6)[THEN allDefs_narrows], of v⇩0]
by auto
from ns⇩3 asm ns obtain ns⇩3 where ns⇩3: "g ⊢ ?n⇩0-ns⇩3→?n⇩0" "?n⇩0 ∉ set (tl (butlast ns⇩3))" "x ∈ set ns⇩3" "set ns⇩3 ⊆ set (tl ns)"
by - (rule old.path2_simple_loop, auto)
with ‹x ≠ ?n⇩0› have "length ns⇩3 > 1"
by (metis empty_iff graph_path_base.path2_def hd_Cons_tl insert_iff length_greater_0_conv length_tl list.set(1) list.set(2) zero_less_diff)
with ns⇩3 obtain ns' m where ns': "g ⊢ ?n⇩0-ns'→m" "m ∈ set (old.predecessors g ?n⇩0)" "ns' = butlast ns⇩3"
by - (rule old.path2_unsnoc, auto)
with vs ns⇩3 have "v ∈ phiUses g m ∨ v⇩0 ∈ phiUses g m"
by - (rule phiUses_exI[of m g ?n⇩0 v⇩0 vs], auto simp:phi_def)
moreover {
assume "v ∈ phiUses g m"
have "var g v⇩0 ≠ var g v"
proof (rule conventional)
show "g ⊢ n-ns⇩1 @ ns'→m" using old.path2_app'[OF ns⇩1(1) ns'(1)] by simp
have "n ∉ set (tl ns⇩1)" using ns assms(2) by auto
moreover have "n ∉ set ns'" using ns'(3) ns⇩3(4) assms(2) by (auto dest: in_set_butlastD)
ultimately show "n ∉ set (tl (ns⇩1 @ ns'))" by simp
show "v ∈ allDefs g n" using ‹v ∈ allDefs g n› .
show "?n⇩0 ∈ set (tl (ns⇩1 @ ns'))" using ns'(1) by (auto simp: old.path2_def)
qed (auto simp: ‹v ∈ phiUses g m›)
hence False by simp
}
moreover {
assume "v⇩0 ∈ phiUses g m"
moreover from ns⇩3(1,3) ‹x ≠ ?n⇩0› ‹length ns⇩3 > 1› have "x ∈ set (tl (butlast ns⇩3))"
by (cases ns⇩3, auto simp: old.path2_def intro: in_set_butlastI)
ultimately have "var g v' ≠ var g v⇩0"
using assms(6)[THEN allDefs_narrows] ns⇩3(2,3) ns'(3) by - (rule conventional[OF ns'(1)], auto)
hence False by simp
}
ultimately have False by auto
}
ultimately have False by auto
}
moreover {
assume asm: "x ∉ set ns⇩3"
have "var g v' ≠ var g v⇩0"
proof (cases "x = ?n⇩0")
case True
moreover have "v⇩0 ∉ step.allDefs g ?n⇩0" by (auto simp:‹v⇩0 = chooseNext g› chooseNext_eliminated)
ultimately show ?thesis using assms(6) vs(1) by - (rule allDefs_var_disjoint[of x g], auto)
next
case False
with ‹x ∉ set (tl ns⇩1)› assms(5) asm have "x ∈ set ns⇩2" by (auto simp:ns)
thus ?thesis using assms(2,6) v⇩0(2) ns⇩2(2) by - (rule conventional[OF ns⇩2(1), where x=x], auto simp:ns)
qed
}
ultimately show ?thesis by auto
qed auto
qed
qed
qed
lemma[simp]: "var g (substNext g v) = var g v"
using substitution[OF redundant]
by (auto simp:substNext_def isTrivialPhi_def phi_def split:option.splits)
lemma phis_same_var_inv:
assumes "phis' g (n,v) = Some vs" "v' ∈ set vs"
shows "var g v' = var g v"
proof-
from assms obtain vs⇩0 v⇩0 where 1: "phis g (n,v) = Some vs⇩0" "v⇩0 ∈ set vs⇩0" "v' = substNext g v⇩0" by (auto split:if_split_asm)
hence "var g v⇩0 = var g v" by auto
with 1 show ?thesis by auto
qed
lemma allDefs_var_disjoint_inv: "⟦n ∈ set (αn g); v ∈ step.allDefs g n; v' ∈ step.allDefs g n; v ≠ v'⟧ ⟹ var g v' ≠ var g v"
using allDefs_var_disjoint
by (auto simp:step.allDefs_def)
lemma step_CFG_SSA_Transformed_notriv: "CFG_SSA_Transformed_notriv αe αn invar inEdges' Entry oldDefs oldUses defs u_g p_g var chooseNext_all"
apply unfold_locales
apply (rule oldDefs_def)
apply (rename_tac g')
apply (case_tac "g'=g")
apply (simp add:oldUses_inv)
apply (simp add:oldUses_def)
apply (rename_tac g' n ns m v x v')
apply (case_tac "g'=g")
apply (simp add:conventional_inv)
apply (simp add:conventional[unfolded CFG_SSA_defs, simplified] step.CFG_SSA_defs)
apply (rename_tac g' n v vs v')
apply (case_tac "g'=g")
apply (simp add:phis_same_var_inv)
apply (simp add:phis_same_var)
apply (rename_tac g' v v')
apply (case_tac "g'=g")
apply (simp add:allDefs_var_disjoint_inv)
apply (simp add:allDefs_var_disjoint[unfolded allDefs_def phiDefs_def, simplified] step.allDefs_def step.phiDefs_def)
by (rule chooseNext_all)
sublocale step: CFG_SSA_Transformed_notriv αe αn invar inEdges' Entry oldDefs oldUses "defs" u_g p_g var chooseNext_all
by (rule step_CFG_SSA_Transformed_notriv)
lemma step_defNode: "v ∈ allVars g ⟹ v ≠ chooseNext g ⟹ step.defNode g v = defNode g v"
by (auto simp: step.CFG_SSA_wf_defs dom_def CFG_SSA_wf_defs)
lemma step_phi: "v ∈ allVars g ⟹ v ≠ chooseNext g ⟹ step.phi g v = map_option (map (substNext g)) (phi g v)"
by (auto simp: step.phi_def step_defNode phi_def)
lemma liveVal'_inv:
assumes "liveVal' g (v#vs)" "v ≠ chooseNext g"
obtains vs' where "step.liveVal' g (v#vs')"
using assms proof (induction "length vs" arbitrary: v vs rule: nat_less_induct)
case (1 vs v)
from "1.prems"(2) show thesis
proof cases
case (liveSimple' n)
with "1.prems"(3) show thesis by - (rule "1.prems"(1), rule step.liveSimple', auto simp: substNext_def)
next
case (livePhi' v' vs')
from this(2) have[simp]: "v' ∈ allVars g" by - (drule liveVal'D, rule, rule liveVal_in_allVars)
show thesis
proof (cases "chooseNext g = v'")
case False
show thesis
proof (rule "1.hyps"[rule_format, of "length vs'" vs' v'])
fix vs'⇩2
assume asm: "step.liveVal' g (v'#vs'⇩2)"
have "step.phiArg g v' v" using livePhi'(3) False "1.prems"(3) by (auto simp: step.phiArg_def phiArg_def step_phi substNext_def)
thus thesis by - (rule "1.prems"(1), rule step.livePhi', rule asm)
qed (auto simp: livePhi' False[symmetric])
next
case [simp]: True
with "1.prems"(3) have[simp]: "v ≠ v'" by simp
from True have "trivial g v'" using chooseNext[OF redundant] by auto
with ‹phiArg g v' v› have "isTrivialPhi g v' v" by (auto simp: phiArg_def trivial_def isTrivialPhi_def)
hence[simp]: "substitution g = v" unfolding substitution_def
by - (rule the1_equality, auto intro!: isTrivialPhi_det[unfolded trivial_def])
obtain vs'⇩2 where vs'⇩2: "suffix (v'#vs'⇩2) (v'#vs')" "v' ∉ set vs'⇩2"
using split_list_last[of v' "v'#vs'"] by (auto simp: Sublist.suffix_def)
with ‹liveVal' g (v'#vs')› have "liveVal' g (v'#vs'⇩2)" by - (rule liveVal'_suffix, simp_all)
thus thesis
proof (cases rule: liveVal'.cases)
case (liveSimple' n)
hence "v ∈ uses' g n" by (auto simp: substNext_def)
with liveSimple' show thesis by - (rule "1.prems"(1), rule step.liveSimple', auto)
next
case (livePhi' v'' vs'')
from this(2) have[simp]: "v'' ∈ allVars g" by - (drule liveVal'D, rule, rule liveVal_in_allVars)
from vs'⇩2(2) livePhi'(1) have[simp]: "v'' ≠ v'" by auto
show thesis
proof (rule "1.hyps"[rule_format, of "length vs''" vs'' v''])
show "length vs'' < length vs" using ‹vs = v'#vs'› livePhi'(1) vs'⇩2(1)[THEN suffix_ConsD2]
by (auto simp: Sublist.suffix_def)
next
fix vs''⇩2
assume asm: "step.liveVal' g (v''#vs''⇩2)"
from livePhi' ‹phiArg g v' v› have "step.phiArg g v'' v" by (auto simp: phiArg_def step.phiArg_def step_phi substNext_def)
thus thesis by - (rule "1.prems"(1), rule step.livePhi', rule asm)
qed (auto simp: livePhi'(2))
qed
qed
qed
qed
lemma liveVal_inv:
assumes "liveVal g v" "v ≠ chooseNext g"
shows "step.liveVal g v"
apply (rule liveVal'I[OF assms(1)])
apply (erule liveVal'_inv[OF _ assms(2)])
apply (rule step.liveVal'D)
by simp_all
lemma pruned_inv:
assumes "pruned g"
shows "step.pruned g"
proof (rule step.pruned_def[THEN iffD2, rule_format])
fix n v
assume "v ∈ step.phiDefs g n" and[simp]: "n ∈ set (αn g)"
hence "v ∈ phiDefs g n" "v ≠ chooseNext g" by (auto simp: step.CFG_SSA_defs CFG_SSA_defs split: if_split_asm)
hence "liveVal g v" using assms by (auto simp: pruned_def)
thus "step.liveVal g v" using ‹v ≠ chooseNext g› by (rule liveVal_inv)
qed
end
context CFG_SSA_Transformed_notriv_base
begin
abbreviation "inst g u p ≡ CFG_SSA_Transformed_notriv αe αn invar inEdges' Entry oldDefs oldUses defs (uses(g:=u)) (phis(g:=p)) var chooseNext_all"
abbreviation "inst' g ≡ λ(u,p). inst g u p"
interpretation uninst: CFG_SSA_Transformed_notriv_base αe αn invar inEdges' Entry oldDefs oldUses "defs" u p var chooseNext_all
for u and p
by unfold_locales
definition "cond g ≡ λ(u,p). uninst.redundant (uses(g:=u)) (phis(g:=p)) g"
definition "step g ≡ λ(u,p). (uninst.uses' (uses(g:=u)) (phis(g:=p)) g,
uninst.phis' (uses(g:=u)) (phis(g:=p)) g)"
definition[code]: "substAll g ≡ while (cond g) (step g) (uses g,phis g)"
definition[code]: "uses'_all g ≡ fst (substAll g)"
definition[code]: "phis'_all g ≡ snd (substAll g)"
lemma uninst_allVars_simps [simp]:
"uninst.allVars u (λ_. p g) g = uninst.allVars u p g"
"uninst.allVars (λ_. u g) p g = uninst.allVars u p g"
"uninst.allVars (uses(g:=u g)) p g = uninst.allVars u p g"
"uninst.allVars u (phis(g:=p g)) g = uninst.allVars u p g"
unfolding uninst.allVars_def uninst.allDefs_def uninst.allUses_def uninst.phiDefs_def uninst.phiUses_def
by simp_all
lemma uninst_trivial_simps [simp]:
"uninst.trivial u (λ_. p g) g = uninst.trivial u p g"
"uninst.trivial (λ_. u g) p g = uninst.trivial u p g"
"uninst.trivial (uses(g:=u g)) p g = uninst.trivial u p g"
"uninst.trivial u (phis(g:=p g)) g = uninst.trivial u p g"
unfolding uninst.trivial_def [abs_def] uninst.isTrivialPhi_def uninst.phi_def uninst.defNode_code
uninst.allDefs_def uninst.phiDefs_def
by simp_all
end
context CFG_SSA_Transformed_notriv
begin
declare fun_upd_apply[simp del] fun_upd_same[simp]
lemma substAll_wf:
assumes[simp]: "redundant g"
shows "card (dom (phis' g)) < card (dom (phis g))"
proof (rule psubset_card_mono)
let ?v = "chooseNext g"
from chooseNext[of g] obtain n where "(n,?v) ∈ dom (phis g)" by (auto simp: trivial_def isTrivialPhi_def phi_def split:option.splits)
moreover have "(n,?v) ∉ dom (phis' g)" by auto
ultimately have "dom (phis' g) ≠ dom (phis g)" by auto
thus "dom (phis' g) ⊂ dom (phis g)" by (auto split:if_split_asm)
qed (rule phis_finite)
lemma step_preserves_inst:
assumes "inst' g (u,p)"
and "CFG_SSA_wf_base.redundant αn inEdges' defs (uses(g:=u)) (phis(g:=p)) g"
shows "inst' g (step g (u,p))"
proof-
from assms(1) interpret i: CFG_SSA_Transformed_notriv αe αn invar inEdges' Entry oldDefs oldUses "defs" "uses(g:=u)" "phis(g:=p)" var
by simp
from assms(2) interpret step: CFG_SSA_step αe αn invar inEdges' Entry oldDefs oldUses "defs" "uses(g:=u)" "phis(g:=p)" var chooseNext_all
by unfold_locales
show ?thesis using step.step_CFG_SSA_Transformed_notriv[simplified] by (simp add: step_def)
qed
lemma substAll:
assumes "P (uses g, phis g)"
assumes "⋀x. P x ⟹ inst' g x ⟹ cond g x ⟹ P (step g x)"
assumes "⋀x. P x ⟹ inst' g x ⟹ ¬cond g x ⟹ Q (fst x) (snd x)"
shows "inst g (uses'_all g) (phis'_all g)" "Q (uses'_all g) (phis'_all g)"
proof-
note uses'_def[simp del]
note phis'_def[simp del]
have 2: "⋀f x. f x = f (fst x, snd x)" by simp
have "inst' g (substAll g) ∧ Q (uses'_all g) (phis'_all g)" unfolding substAll_def uses'_all_def phis'_all_def
apply (rule while_rule[where P="λx. inst' g x ∧ P x"])
apply (rule conjI)
apply (simp, unfold_locales)
apply (rule assms(1))
apply (rule conjI)
apply (clarsimp simp: cond_def step_def)
apply (rule step_preserves_inst [unfolded step_def, simplified], assumption+)
proof-
show "wf {(y,x). (inst' g x ∧ cond g x) ∧ y = step g x}"
apply (rule wf_if_measure[where f="λ(u,p). card (dom p)"])
apply (clarsimp simp: cond_def step_def split:prod.split)
proof-
fix u p
assume "inst g u p"
then interpret i: CFG_SSA_Transformed_notriv αe αn invar inEdges' Entry oldDefs oldUses "defs" "uses(g:=u)" "phis(g:=p)" by simp
assume "i.redundant g"
thus "card (dom (i.phis' g)) < card (dom p)" by (rule i.substAll_wf[of g, simplified])
qed
qed (auto intro: assms(2,3))
thus "inst g (uses'_all g) (phis'_all g)" "Q (uses'_all g) (phis'_all g)"
by (auto simp: uses'_all_def phis'_all_def)
qed
sublocale notriv: CFG_SSA_Transformed αe αn invar inEdges' Entry oldDefs oldUses "defs" uses'_all phis'_all
proof-
interpret ssa: CFG_SSA αe αn invar inEdges' Entry "defs" uses'_all phis'_all
proof
fix g
interpret i: CFG_SSA_Transformed_notriv αe αn invar inEdges' Entry oldDefs oldUses "defs" "uses(g:=uses'_all g)" "phis(g:=phis'_all g)" var
by (rule substAll, auto)
interpret uninst: CFG_SSA_Transformed_notriv_base αe αn invar inEdges' Entry oldDefs oldUses "defs" u p var chooseNext_all
for u and p
by unfold_locales
fix n v args m
show "finite (defs g n)" by (rule defs_finite)
show "v ∈ uses'_all g n ⟹ n ∈ set (αn g)" by (rule i.uses_in_αn[of _ g, simplified])
show "finite (uses'_all g n)" by (rule i.uses_finite[of g, simplified])
show "invar g" by (rule invar)
show "finite (dom (phis'_all g))" by (rule i.phis_finite[of g, simplified])
show "phis'_all g (n, v) = Some args ⟹ n ∈ set (αn g)" using i.phis_in_αn[of g] by simp
show "phis'_all g (n, v) = Some args ⟹ length (old.predecessors g n) = length args" using i.phis_wf[of g] by simp
show "n ∈ set (αn g) ⟹ defs g n ∩ uninst.phiDefs phis'_all g n = {}" using i.simpleDefs_phiDefs_disjoint[of n g] by (simp add: uninst.CFG_SSA_defs)
show "n ∈ set (αn g) ⟹ m ∈ set (αn g) ⟹ n ≠ m ⟹ uninst.allDefs phis'_all g n ∩ uninst.allDefs phis'_all g m = {}"
using i.allDefs_disjoint[of n g] by (simp add: uninst.CFG_SSA_defs)
show "n ∈ set (αn g) ⟹ defs g n ∩ uses'_all g n = {}" using i.defs_uses_disjoint[of n g] by simp
qed
interpret uninst: CFG_SSA_Transformed_notriv_base αe αn invar inEdges' Entry oldDefs oldUses "defs" u p var chooseNext_all
for u and p
by unfold_locales
show "CFG_SSA_Transformed αe αn invar inEdges' Entry oldDefs oldUses defs uses'_all phis'_all var"
proof
fix g n v ns m x v' vs
interpret i: CFG_SSA_Transformed_notriv αe αn invar inEdges' Entry oldDefs oldUses "defs" "uses(g:=uses'_all g)" "phis(g:=phis'_all g)" var
by (rule substAll, auto)
show "oldDefs g n = var g ` defs g n" by (rule oldDefs_def)
show "n ∈ set (αn g) ⟹ oldUses g n = var g ` uses'_all g n" using i.oldUses_def[of n g] by simp
show "v ∈ ssa.allUses g n ⟹ n ∈ set (αn g) ⟹ ssa.defAss g n v" using i.allUses_def_ass[of v g n] by (simp add: uninst.CFG_SSA_defs)
show "old.path2 g n ns m ⟹ n ∉ set (tl ns) ⟹ v ∈ ssa.allDefs g n ⟹ v ∈ ssa.allUses g m ⟹ x ∈ set (tl ns) ⟹ v' ∈ ssa.allDefs g x ⟹ var g v' ≠ var g v" using i.conventional[of g n ns m v x v'] by (simp add: uninst.CFG_SSA_defs)
show "phis'_all g (n, v) = Some vs ⟹ v' ∈ set vs ⟹ var g v' = var g v" using i.phis_same_var[of g n v] by simp
show "n ∈ set (αn g) ⟹ v ∈ ssa.allDefs g n ⟹ v' ∈ ssa.allDefs g n ⟹ v ≠ v' ⟹ var g v' ≠ var g v" using i.allDefs_var_disjoint by (simp add: uninst.CFG_SSA_defs)
show "phis'_all g (Entry g, v) = None" using i.Entry_no_phis[of g v] by simp
qed
qed
theorem not_redundant: "¬notriv.redundant g"
proof-
interpret uninst: CFG_SSA_Transformed_notriv_base αe αn invar inEdges' Entry oldDefs oldUses "defs" u p var chooseNext_all
for u and p
by unfold_locales
have 1: "⋀u p. uninst.redundant (uses(g:=u g)) (phis(g:=p g)) g ⟷ uninst.redundant u p g"
by (simp add: uninst.CFG_SSA_wf_defs)
show ?thesis
by (rule substAll(2)[where Q="λu p. ¬uninst.redundant (uses(g:=u)) (phis(g:=p)) g" and P="λ_. True" and g=g, simplified cond_def substAll_def 1], auto)
qed
corollary minimal: "old.reducible g ⟹ notriv.cytronMinimal g"
by (erule notriv.reducible_nonredundant_imp_minimal, rule not_redundant)
theorem pruned_invariant:
assumes "pruned g"
shows "notriv.pruned g"
proof-
{
fix u p
assume "inst g u p"
then interpret i: CFG_SSA_Transformed_notriv αe αn invar inEdges' Entry oldDefs oldUses "defs" "uses(g:=u)" "phis(g:=p)" var chooseNext_all
by simp
assume "i.redundant g"
then interpret i: CFG_SSA_step αe αn invar inEdges' Entry oldDefs oldUses "defs" "uses(g:=u)" "phis(g:=p)" var chooseNext_all g
by unfold_locales
interpret uninst: CFG_SSA_Transformed_notriv_base αe αn invar inEdges' Entry oldDefs oldUses "defs" u p var chooseNext_all
for u and p
by unfold_locales
assume "i.pruned g"
hence "uninst.pruned (uses(g:=i.uses' g)) (phis(g:=i.phis' g)) g"
by (rule i.pruned_inv[simplified])
}
note 1 = this
interpret uninst: CFG_SSA_Transformed_notriv_base αe αn invar inEdges' Entry oldDefs oldUses "defs" u p var chooseNext_all
for u and p
by unfold_locales
have 2: "⋀u u' p p' g. uninst.pruned (u'(g:=u g)) (p'(g:=p g)) g ⟷ uninst.pruned u p g"
by (clarsimp simp: uninst.CFG_SSA_wf_defs)
from 1 assms show ?thesis
by - (rule substAll(2)[where P="λ(u,p). uninst.pruned (uses(g:=u)) (phis(g:=p)) g" and Q="λu p. uninst.pruned (uses(g:=u)) (phis(g:=p)) g" and g=g, simplified 2],
auto simp: cond_def step_def)
qed
end
end