fix(ir): bound the bottom-up rewrite driver's re-application loop (#348) - #350

Closes #348.

The symptom

pslua optimizes its intermediate representation (IR) by rewriting expression trees, and the rewrite rules are exercised by Hedgehog properties that generate random IR terms. Three of the first 500 hspec seeds — 109, 152 and 478 — made the IR Optimizer spec group stop emitting output and pin one core indefinitely. A complete run of that group costs 0.35 s; these were still spinning when killed at 120 s, with a flat 50 MiB resident set, so nothing was growing — the optimizer was looping.

$ timeout 120 $(cabal list-bin spec) --match "IR Optimizer" --seed 109
    blanking an unused shadowing binder keeps outer references bound [✔]
        ✓ property passed 1 test.
timeout 120 $SPEC --match "IR Optimizer" --seed 109  119.58s user 0.21s system 99% cpu 2:00.00 total

The last line printed is the test declared immediately before optimization keeps expressions well-scoped, the property that feeds generated terms through the whole optimizer pipeline — so the loop was inside that property, and it hung rather than reddening, which is the easiest kind of failure to misread as flakiness.

What was looping

The IR rewrite driver rewriteExpBottomUpM walks an expression bottom-up: it rewrites a node's children first, then applies the rule set to the node, and re-applies it to its own result until the rule set stops firing. That re-application loop had no bound.

rewriteExpBottomUpM rule expr =
  runWriterT $ flip (rewriteMOf subexpressions) expr \e →
    lift (rule e) >>= traverse \e' → e' <$ tell Rewritten

Among the rules that loop drives is betaReduce, which reduces a redex (λx. M) N to M[x := N]. Beta reduction has no terminating strategy on an arbitrary untyped term, and the generator draws untyped terms: it drew Ω = (λx. x x) (λy. y y), the smallest term with no normal form, whose every reduction step reproduces it modulo binder names. Instrumenting the loop to abort after 400 nested rewrites and print the node it was chewing on shows the cycle exactly — the two abstractions swap places and every binder index advances by one, because pasting a copy of the argument freshens its binders:

BEFORE:
AppN () (AbsN () (ParamNamed () (Name "x$400") :| []) (AppN () (Ref () (Local (Name "x$400"))) (Ref () (Local (Name "x$400")) :| []))) (AbsN () (ParamNamed () (Name "x$401") :| []) (AppN () (Ref () (Local (Name "x$401"))) (Ref () (Local (Name "x$401")) :| [])) :| [])
AFTER:
AppN () (AbsN () (ParamNamed () (Name "x$401") :| []) (AppN () (Ref () (Local (Name "x$401"))) (Ref () (Local (Name "x$401")) :| []))) (AbsN () (ParamNamed () (Name "x$402") :| []) (AppN () (Ref () (Local (Name "x$402"))) (Ref () (Local (Name "x$402")) :| [])) :| [])

All three seeds hit the same term. So this is not the non-converging rule pair the issue guessed at, and it is not a guard that betaReduce is missing: no local test on a redex can decide whether reducing it terminates. The pass-level pipeline was never the problem either — its fixpoint combinator has carried a 1000-iteration backstop for a while. The unbounded loop was one level below it, inside a single pass, at a single node.

The fix

The loop now carries a budget, spelled maxNestedRewrites, and returns the term it has reached when the budget runs out:

rewriteExpBottomUpM rule = runWriterT . reapply maxNestedRewrites
 where
  reapply budget = transformMOf subexpressions \e →
    lift (rule e) >>= \case
      Nothing → pure e
      Just e' → do
        tell Rewritten
        case budget of
          0 → pure e'
          _ → reapply (budget - 1) e'

This is the treatment the pass-level fixpoint already gives its own iteration cap: stopping early costs optimization and nothing else, because each rewrite preserves semantics and the IR invariants on its own, so a term the driver abandons mid-reduction is exactly as valid as a fully reduced one. The driver's WasRewritten flag — which the enclosing fixpoint trusts to decide whether to iterate again — also stays precise: it reports Rewritten iff some rule fired, whether or not the loop ran to exhaustion.

The budget is 100, and it cannot reach legitimate work. Instrumenting the driver to record the deepest nesting it ever reaches and running the whole suite gives 5 — 1232 examples, 344 of them golden compilations of real PureScript including the ~300-deep constant chains that stress the pipeline hardest. That is the population that matters, since the IR is assumed well-typed (Note [IR is assumed well-typed]) and PureScript's type system rejects every term without a normal form; only the untyped terms the generators draw reach the bound at all.

Diagnosability

Nothing is silent about a term that exhausts the budget. optimizedUberModule (the production pipeline) returns a correct, under-optimized module, while optimizedUberModuleChecked (the same pipeline with every pass's contract linted, used by the test suite always and by the CLI behind --lint-ir) reports which fixpoint kept firing:

optimizedUberModuleChecked mempty original
  === Left (FixpointDivergence "optimize+dce" maxFixpointIterations)

Each round of that fixpoint genuinely changes the module — it advances Ω by another 100 beta steps — so the fixpoint runs its full cap and then names itself, which is the third acceptance criterion of the issue.

Tests

Two example-based tests replace the generator draw, so the fix is pinned by something that does not depend on a seed. Both hang on the parent commit; the test commit is deliberately red.

    let selfApplication name =
          abstraction (paramNamed name) $
            application (refLocal name) (refLocal name)
        omega =
          application
            (selfApplication (Name "x"))
            (selfApplication (Name "y"))

The first asserts the pipeline returns at all and that the abandoned term still satisfies the two IR invariants — lintWellScoped (every local reference resolves to an enclosing binder) and lintUniqueBinders (no local binder name bound twice within a top-level site). The second pins the FixpointDivergence report above.

Verification

cabal test all is green (1234 examples), fourmolu and hlint are clean, and the golden corpus is byte-identical — no golden.ir or golden.lua moved, which follows from the bound being 20× clear of the deepest chain any real compilation produces.

The check the issue asks for is the sweep that found the stall, so here it is over the same range, with a timeout generous against the group's cost:

$ for s in $(seq 1 500); do timeout 60 $SPEC --match "IR Optimizer" --seed $s; done
worst_elapsed=6s
failures:

Every seed passes; the worst is seed 109 at 6 s. Two costs are worth naming rather than hiding. The group now takes about 3 s at every seed, up from 0.35 s, because the new example-based test deliberately drives the budget to exhaustion twice — the enclosing optimize+dce fixpoint keeps spending its 1000 rounds advancing a term that will never converge, since each round does change the module. On top of that, the three seeds that draw Ω themselves add ~2 s (109 → 6 s, 152 and 478 → 5 s). Full-suite wall clock is unchanged within noise at 88 s. Making an exhausted budget stop the enclosing fixpoint at once would remove both, but it means widening Pass.passRun's result and its three runners, so it belongs in its own change.