Problem class: go-20261008-incremental-ssa-phi-placement-after-loop-splitting
I built a runnable reference implementation in ~/inc-ssa (Go 1.26, package incssa) and verified it. go vet is clean and all 7 tests pass, including a 3000-seed randomized differential test that compares the incremental placement against a from-scratch oracle after every one of 12 random CFG mutations.
The key finding beyond the obvious "invalidate the DF cache": edge redirection can change liveness only (with dominators/DF unchanged), leaving a pruned phi alive. The fix must snapshot live-in as well, not just DF/pred sets.
The full solution document is at ~/inc-ssa/SOLUTION.md (copied to ~/SOLUTION.md). Here it is:
Problem class: go-20261008-incremental-ssa-phi-placement-after-loop-splitting
Environment: go1.26, linux/amd64
Deliverable: a worklist-based incremental phi-placement engine plus a verifier that detects stale dominance-frontier facts and operands from unreachable predecessor edges. Full runnable implementation lives in ~/inc-ssa (package incssa).
The bug is not in the Cytron worklist itself; it is in what gets invalidated when the CFG changes. After loop splitting / edge redirection, three classes of cached facts go stale:
DF[b] must be recomputed, not reused.LiveIn[d][v] without changing dominators or DF at all. A pruned phi that was correct before the rewrite survives when it must be deleted.The fix is an incremental update that (a) snapshots DF, predecessor sets, def/use ops, and LiveIn; (b) computes the affected region R as the DF-forward closure (over old ∪ new DF) of every block whose snapshot changed; (c) clears phi slots in R; and (d) re-runs the pruned Cytron worklist with the surviving phis as seeds. The verifier independently recomputes the canonical placement and the reachable predecessor set, then checks dominance of every use and phi operand.
A compiler pass splits a loop (peels an iteration, rotates the latch, inserts a preheader) or redirects an edge, then calls the SSA maintenance routine. The routine "works" for the common case and then:
For variable v and block b, pruned SSA requires a phi exactly when
b ∈ DF⁺(defsites(v)) AND v ∈ LiveIn[b]
The set of phi sites is a function of two things a loop rewrite can change independently: the dominator tree (hence DF) and liveness. Any incremental scheme that watches only one is unsound.
Adding an edge u → v makes v a merge head. For every node w on the dominator path from u up to (but excluding) idom(v), v enters DF[w]. If w defines the variable and it is live-in at v, a phi is required at v. A cached DF produced before the edge was added does not contain that entry, so the phi is never placed.
Minimal reproducer (TestStaleDominanceFrontierMissesPhi): entry -> A -> B -> C -> end; add A -> C. Now C is a merge and C ∈ DF(B). Building from the old DF yields no phi; Verify reports missing phi x at C (stale dominance frontier).
Removing L -> M (or making M's other predecessor unreachable) leaves the old operand for L. Verify reports phi x at M has operand for unreachable/non-predecessor edge from L (TestUnreachablePredecessorOperand, TestMakeUnreachableBlock).
This is the subtle one and the reason a "dirty block only where DF changed" algorithm is wrong. Removing b1 -> b3 can make b3 unreachable. b3 used a, so a was live-in at b1; after the removal a is no longer live-in at b1, and the phi at b1 must be deleted. But b1's predecessor set and DF[b1] are unchanged, and b1 can no longer reach b3, so it is not in the DF-forward closure of the changed block. The stale pruned phi survives.
The randomized differential test found exactly this on seed 41, step 4. The correct treatment is to compare the live-in snapshot and seed every block whose live-in set changed.
AddEdge/RemoveEdge maintain both Succs and Preds exactly once, so a phi operand keyed by predecessor block can always be checked against Preds.
| snapshot | why it matters |
|---|---|
lastDF map[int]map[int]bool |
detects changed dominance frontier |
lastPred [][]int |
detects added/removed/redirected edges |
lastOps [][]Op |
detects def-site changes (new/removed defs) |
lastLiveIn []map[string]bool |
detects pruning changes caused by reachability |
seeds := map[int]bool{}
for b := range cfg.Blocks {
newlyAdded := b >= len(e.lastPred)
if newlyAdded || !sameInts(e.lastPred[b], newPred[b]) { seeds[b] = true }
if !equalIntSet(e.lastDF[b], newDF[b]) { seeds[b] = true }
if !reach[b] { seeds[b] = true }
if newlyAdded || !sameOps(e.lastOpsAt(b), cfg.Blocks[b].Ops) { seeds[b] = true }
if b >= len(e.lastLiveIn) || !equalStrSet(e.lastLiveIn[b], newLiveIn[b]) {
seeds[b] = true
}
}
region := dfClosure(seeds, e.lastDF, newDF)
Walking both the old and the new DF graphs is what makes deletions correct: if a phi at q justified a phi at x ∈ DF(q), removing the justification at q puts q in the region, and x is one DF hop away, so it is cleared too.
for _, m := range e.place {
for b := range region {
delete(m, b) // forget stale / extra phis
}
}
Sources are all def sites plus surviving phis outside R:
for b := range cfg.Blocks {
if !reach[b] { continue }
if cfg.Blocks[b].Defines(v) || e.place[v][b] { add(b) }
}
for len(work) > 0 {
b := pop(work)
for d := range newDF[b] {
if e.place[v][d] || !newLiveIn[d][v] { continue } // pruned
e.place[v][d] = true
add(d)
}
}
BuildSSA walks the dominator tree preorder and fills every successor phi's operand from the current end-of-block value. Because phis are rebuilt for the reachable graph, operands for removed edges simply never get created.
SimplifyTrivialPhis removes a phi whose operands are all the same value, substitutes the surviving value in every use and operand, and iterates to a fixed point. A self-referential-only phi is left alone.
Let V/E be reachable blocks/edges, D_v the def sites of v, Φ_v the placed phis for v, and R the affected region.
(v, b) that is a def site or receives a phi is processed once, scanning DF[b] once.
O( Σ_v ( |D_v| + |Φ_v| + Σ_{b ∈ D_v ∪ Φ_v} |DF[b]| ) )O( |R| + Σ_v Σ_{b ∈ R} |DF[b]| ).
For local loop rewrites R is a handful of blocks. (Dominators are recomputed here for simplicity; the same dirty set can drive an incremental dominator algorithm such as Georgiadis–Tarjan.)The engine (~/inc-ssa/engine.go):
func (e *Engine) Update() {
cfg := e.cfg
newDF := cfg.DominanceFrontier(cfg.Dominators())
newPred := cfg.snapshotPreds()
newLiveIn, _ := cfg.Liveness()
reach := cfg.Reachable()
seeds := map[int]bool{}
for b := 0; b < len(cfg.Blocks); b++ {
newlyAdded := b >= len(e.lastPred)
if newlyAdded || !sameInts(e.lastPred[b], newPred[b]) {
seeds[b] = true
}
if !equalIntSet(e.lastDF[b], newDF[b]) {
seeds[b] = true
}
if !reach[b] {
seeds[b] = true
}
if newlyAdded || !sameOps(e.lastOpsAt(b), cfg.Blocks[b].Ops) {
seeds[b] = true
}
if b >= len(e.lastLiveIn) || !equalStrSet(e.lastLiveIn[b], newLiveIn[b]) {
seeds[b] = true
}
}
region := dfClosure(seeds, e.lastDF, newDF)
for _, m := range e.place {
for b := range region {
delete(m, b)
}
}
liveIn := newLiveIn
for _, v := range cfg.Variables() {
if e.place[v] == nil {
e.place[v] = map[int]bool{}
}
work := []int{}
inWork := map[int]bool{}
add := func(b int) {
if !inWork[b] {
work = append(work, b)
inWork[b] = true
}
}
for b := 0; b < len(cfg.Blocks); b++ {
if !reach[b] {
continue
}
if cfg.Blocks[b].Defines(v) || e.place[v][b] {
add(b)
}
}
for len(work) > 0 {
b := work[0]
work = work[1:]
inWork[b] = false
for d := range newDF[b] {
if e.place[v][d] {
continue
}
if !liveIn[d][v] {
continue
}
e.place[v][d] = true
add(d)
}
}
}
e.lastDF = newDF
e.lastPred = newPred
e.lastOps = cfg.snapshotOps()
e.lastLiveIn = newLiveIn
e.ssa = BuildSSA(cfg, e.place)
}
func dfClosure(seeds map[int]bool, dfs ...map[int]map[int]bool) map[int]bool {
seen := map[int]bool{}
stack := make([]int, 0, len(seeds))
for b := range seeds {
seen[b] = true
stack = append(stack, b)
}
for len(stack) > 0 {
b := stack[len(stack)-1]
stack = stack[:len(stack)-1]
for _, df := range dfs {
for x := range df[b] {
if !seen[x] {
seen[x] = true
stack = append(stack, x)
}
}
}
}
return seen
}
Pruned worklist (ssa.go):
func (g *CFG) PlacePruned(df map[int]map[int]bool, liveIn []map[string]bool) map[string]map[int]bool {
reach := g.Reachable()
place := map[string]map[int]bool{}
for _, v := range g.Variables() {
place[v] = map[int]bool{}
work := []int{}
inWork := map[int]bool{}
for b := 0; b < len(g.Blocks); b++ {
if reach[b] && g.Blocks[b].Defines(v) {
work = append(work, b)
inWork[b] = true
}
}
for len(work) > 0 {
b := work[0]
work = work[1:]
inWork[b] = false
for d := range df[b] {
if place[v][d] {
continue
}
if !liveIn[d][v] {
continue // pruned
}
place[v][d] = true
if !inWork[d] {
work = append(work, d)
inWork[d] = true
}
}
}
}
return place
}
Verifier (ssa.go) — checks placement freshness, operand/predecessor agreement, and dominance:
func Verify(g *CFG, ssa *SSA, checkPlacement bool) []string {
var errs []string
reach := g.Reachable()
dom := g.DominanceMatrix(g.Dominators())
if checkPlacement {
exp := ExpectedPlacement(g)
for v := range exp {
for b := range exp[v] {
if ssa.Phis[v] == nil || ssa.Phis[v][b] == nil {
errs = append(errs, fmt.Sprintf(
"missing phi %s at %s (stale dominance frontier)", v, g.Blocks[b].Name))
}
}
}
for v, m := range ssa.Phis {
for b := range m {
if !exp[v][b] {
errs = append(errs, fmt.Sprintf("stale/extra phi %s at %s", v, g.Blocks[b].Name))
}
}
}
}
for v, m := range ssa.Phis {
for b, phi := range m {
if !reach[b] {
errs = append(errs, fmt.Sprintf("phi %s in unreachable block %s", v, g.Blocks[b].Name))
continue
}
preds := map[int]bool{}
for _, p := range g.Blocks[b].Preds {
if reach[p] {
preds[p] = true
}
}
for p := range phi.Operands {
if !preds[p] {
errs = append(errs, fmt.Sprintf(
"phi %s at %s has operand for unreachable/non-predecessor edge from %s",
v, g.Blocks[b].Name, g.Blocks[p].Name))
}
}
for p := range preds {
id, ok := phi.Operands[p]
if !ok {
errs = append(errs, fmt.Sprintf(
"phi %s at %s missing operand for predecessor %s", v, g.Blocks[b].Name, g.Blocks[p].Name))
continue
}
if id < 0 || id >= len(ssa.Values) {
errs = append(errs, fmt.Sprintf(
"phi %s at %s has undefined operand for %s", v, g.Blocks[b].Name, g.Blocks[p].Name))
continue
}
if db := ssa.Values[id].Block; !dom[db][p] {
errs = append(errs, fmt.Sprintf(
"phi %s at %s operand from %s defined at %s does not dominate %s",
v, g.Blocks[b].Name, g.Blocks[p].Name, g.Blocks[db].Name, g.Blocks[p].Name))
}
}
}
}
for _, u := range ssa.Uses {
if u.Value < 0 || u.Value >= len(ssa.Values) {
errs = append(errs, fmt.Sprintf("use of %s at %s is undefined", u.Var, g.Blocks[u.Block].Name))
continue
}
if db := ssa.Values[u.Value].Block; !dom[db][u.Block] {
errs = append(errs, fmt.Sprintf(
"use of %s at %s not dominated by its def at %s", u.Var, g.Blocks[u.Block].Name, g.Blocks[db].Name))
}
}
sort.Strings(errs)
return errs
}
cd ~/inc-ssa
go vet ./...
go test -v -count=1 ./...
Expected output:
--- PASS: TestRandomizedIncremental (1.43s)
--- PASS: TestBaselineLoopPhi (0.00s)
--- PASS: TestIncrementalLoopSplitMatchesScratch (0.00s)
--- PASS: TestStaleDominanceFrontierMissesPhi (0.00s)
--- PASS: TestUnreachablePredecessorOperand (0.00s)
--- PASS: TestMakeUnreachableBlock (0.00s)
--- PASS: TestSimplifyTrivialPhi (0.00s)
ok incssa 1.430s
| test | property |
|---|---|
TestBaselineLoopPhi |
the canonical loop gets exactly one loop-carried phi at the header |
TestIncrementalLoopSplitMatchesScratch |
after peeling an iteration, incremental placement equals ExpectedPlacement; the loop-carried phi moves to H2 with an operand from the back edge B2; the pre-split SSA is rejected |
TestStaleDominanceFrontierMissesPhi |
adding A->C requires a phi at C; cached-DF form rejected with missing phi x at C |
TestUnreachablePredecessorOperand |
removing L->M leaves an operand for a non-predecessor; verifier reports unreachable/non-predecessor |
TestMakeUnreachableBlock |
phis in blocks that become unreachable are dropped |
TestSimplifyTrivialPhi |
a forced trivial phi is removed, references rewired, dominance preserved |
TestRandomizedIncremental |
3000 random CFGs × 12 mutations; after every mutation the incremental placement equals the from-scratch oracle and Verify(..., true) is empty |
The randomized test deliberately mutates definitions and uses as well as edges, which is what surfaced failure mode C. Removing the live-in seed from Update makes seed 41 step 4 fail — that is the regression guard.
go test -run 'StaleDominanceFrontier|UnreachablePredecessorOperand' -v ./...
Both tests assert the specific diagnostic, not merely that some error occurred.
~/inc-ssa/go.mod module incssa (go 1.26)
~/inc-ssa/ssa.go CFG, dominators, DF, liveness, pruned worklist,
SSA renaming, verifier, trivial-phi simplify
~/inc-ssa/engine.go incremental Engine.Update + affected-region logic
~/inc-ssa/ssa_test.go deterministic regression tests
~/inc-ssa/random_test.go 3000-seed differential stress test
~/inc-ssa/SOLUTION.md this document
cfg := NewCFG()
// ... create blocks, set cfg.Entry, append Def/Use ops, AddEdge ...
e := NewEngine(cfg)
cfg.RemoveEdge(b, h)
cfg.AddEdge(b, h2)
cfg.AddEdge(h2, b2)
cfg.AddEdge(b2, h2)
cfg.AddEdge(h2, exit)
e.Update()
if errs := Verify(cfg, e.SSA(), true); len(errs) != 0 {
panic(errs)
}
Result: go vet clean; all tests pass. The incremental engine reproduces the from-scratch canonical pruned placement on 36,000 randomized mutations, and the verifier catches both stale-DF facts and unreachable predecessor operands.
# Evidence - Problem class: go-20261008-incremental-ssa-phi-placement-after-loop-splitting - Model: openrouter/deepseek/deepseek-v4.1-flash - Solved: 2026-10-08T17:20:28.133Z - Verification: solution produced by pi in sandbox; see signatures.json
{"description": "Given a control-flow graph undergoing loop splitting and edge redirection, maintain pruned SSA form incrementally, placing and simplifying phi nodes while preserving dominance and loop-carried values. Develop a worklist algorithm with a stated complexity bound and produce a verifier that catches stale dominance-frontier facts and unreachable predecessor edges.", "environment": "go1.26", "language": "go", "model": "openrouter/deepseek/deepseek-v4.1-flash", "problem_class": "go-20261008-incremental-ssa-phi-placement-after-loop-splitting", "provider": "openrouter", "solved_at": "2026-10-08T17:20:28.133Z", "version": "1.26"}