Skip to content

First-class passes for the IR pipeline: Pass values, invariant checks, deterministic name supply#149

Merged
Unisay merged 3 commits into
mainfrom
issue-138/pass-pipeline
Jul 3, 2026
Merged

First-class passes for the IR pipeline: Pass values, invariant checks, deterministic name supply#149
Unisay merged 3 commits into
mainfrom
issue-138/pass-pipeline

Conversation

@Unisay

@Unisay Unisay commented Jul 3, 2026

Copy link
Copy Markdown
Collaborator

Closes #138.

What

optimizedUberModule was plain function composition, with the pipeline's invariants living in comments and Notes. This PR makes the pipeline a list of interpreted steps, each pass a value carrying its contract:

  • IR.Pass: Pass (name, passRun :: UberModule -> SupplyM UberModule, passRequires/passEnsures :: Set Invariant) and a Step layer (RunPass | RunFixpoint). Three runners interpret a [Step]: plain (runSteps), checked (runStepsChecked), and traced (runStepsTraced, per-pass IR snapshots for debugging). The Step layer exists so the checked runner can lint every pass of every fixpoint iteration: a violation on an intermediate iteration that a later iteration masks would be invisible to a fixpoint combinator returning an opaque Pass. That is not hypothetical, see below.
  • IR.Linter: lintUberModule generalizes the unboundLocals reference implementation that lived in the Optimizer spec. It walks bindings, foreigns, and exports, and treats the runtime lazy factory as bound by the runtime (documented as a fifth site of the PSLUA_runtime_lazy coupling Note).
  • IR.Supply: a deterministic counter-based name supply threaded through passRun. flattenDeepBinds ports its internal counter to it; minted $kontN/$tmpN names are bit-identical because nothing draws from the supply before that pass and the counter starts at 0. The module documents why the DCE node-id counter and renameShadowedNames must stay off the shared supply.
  • The golden harness compiles through the checked runner, so every golden module now doubles as a scope-invariant test of the whole pipeline. The CLI gains a --lint-ir debug flag plumbed through compileModules.

Behavior-identical by construction: the fixpoint iterates the optimize/DCE composition and compares after the full sequence, exactly like the old idempotently. Zero golden churn, guarded by the kont0/tmp0 names baked into the Long*Bind goldens.

The bug the checked runner caught on day one

Turning on per-pass linting in the golden harness immediately went red on Golden.LongWriterBind: after the first dce pass, Control.Monad.Writer.Trans.applyWriterT contained unbound v3/v4 references, healed by the next fixpoint iteration. Root cause: Rewritten Recurse descends into the rewritten node's children without re-applying the rule, so when a fully dead Let collapses to its body and the body is itself a Let, the inner Let escapes the DCE rule. Its dead bindings are kept while the parameters of lambdas inside them get blanked (their ids are unreachable), leaving dangling references. Latent only, because the fixpoint's next iteration always dropped the residue, but that is accidental robustness. Fixed in the first commit (red unit test first), so every commit of this branch keeps the suite green. The bug predates #134.

This is the motivation for the whole issue playing out on the spot: the 2026-07-02 audit traced six scoping bugs to invariants that lived in comments, and the first mechanical check of those invariants found a seventh within minutes of existing.

Verification

  • cabal test all: 330 examples, 0 failures; git status clean in test/ps/output (zero golden churn).
  • New specs: IR.Linter (module sites, runtime-lazy exemption, sequential Let scoping cases, property over Gen.scopedExp) and IR.Pass (checked runner reports the offending pass and phase, catches an intermediate fixpoint violation that the plain runner converges past, fixpoint semantics property-tested against idempotently).
  • CLI smoke: pslua --lint-ir compiles the test project and the produced Lua runs (ok!); --help shows the flag.
  • fourmolu and hlint clean on the touched files.

Unisay added 2 commits July 3, 2026 08:58
'Rewritten Recurse' descends into the rewritten node's children without
re-applying the rule to the node itself. When every binding of a Let is
dead and the node collapses to its body, a body that is itself a Let
escaped the DCE rule: its dead bindings were kept, while the parameters
of lambdas inside them were blanked (their ids are unreachable), leaving
unbound local references in the intermediate IR. A later optimizer
iteration always dropped the residue, so generated code was unaffected;
the per-pass invariant checks built for #138 surfaced the bug on the
golden corpus (Golden.LongWriterBind, Control.Monad.Writer.Trans).

Process a collapsed-into Let directly in the rule (the collapse can
cascade), so its dead bindings are eliminated in the same pass.
…138)

The IR pipeline becomes a list of Step values interpreted by runners: a
Pass carries its invariant contract (passRequires/passEnsures), and the
Step layer (RunPass | RunFixpoint) lets the checked runner lint every
pass boundary including every fixpoint iteration — an intermediate
violation masked by a later iteration is exactly what it exists to
catch. Components:

- IR.Supply: deterministic counter-based name supply threaded through
  passRun; flattenDeepBinds ports its internal counter to it (names are
  bit-identical: nothing draws before it, the counter starts at 0).
- IR.Linter: well-scopedness check generalized from the Optimizer
  spec's unboundLocals reference implementation; walks bindings,
  foreigns, and exports, and treats the runtime lazy factory as bound
  by the runtime (a fifth site of the PSLUA_runtime_lazy coupling).
- IR.Pass: Invariant, Pass, Step, PassCheckFailure, and the three
  runners (plain, checked, traced); idempotently moves here.
- The golden harness compiles through the checked runner, so every
  golden module doubles as a scope-invariant test of the pipeline.
- The CLI gains a --lint-ir debug flag plumbed through compileModules.

Behavior-identical: zero golden churn (guarded by the kont0/tmp0 names
baked into the Long*Bind goldens).

Copilot AI left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Pull request overview

This PR refactors the PureScript→Lua backend’s IR optimization pipeline from ad-hoc function composition into an explicit, interpretable sequence of first-class passes with mechanically checked invariants. It adds an IR linter, threads a deterministic name supply through name-minting passes, wires invariant-checking into the golden test harness (and an opt-in CLI flag), and includes a DCE fix uncovered by the new per-pass checking.

Changes:

  • Introduce IR.Pass/Step pipeline runners (plain, checked, traced) and re-express optimizedUberModule as a pass pipeline (with optimizedUberModuleChecked).
  • Add IR.Linter well-scopedness checks (including the runtime-lazy exemption) and run them at every pass boundary in the golden harness / --lint-ir.
  • Add IR.Supply and port FlattenDeepBinds to use the deterministic supply; fix a DCE nested-Let edge case and add regression tests/spec coverage.

Reviewed changes

Copilot reviewed 19 out of 19 changed files in this pull request and generated 1 comment.

Show a summary per file
File Description
test/Main.hs Registers new IR linter/pass spec suites in the test runner.
test/Language/PureScript/Backend/Lua/Golden/Spec.hs Switches goldens to compile IR via the checked optimizer runner (per-pass invariant checking).
test/Language/PureScript/Backend/IR/Pass/Spec.hs Adds tests for checked runner failure reporting and fixpoint semantics.
test/Language/PureScript/Backend/IR/Optimizer/Spec.hs Replaces ad-hoc scope checking with centralized linter checks.
test/Language/PureScript/Backend/IR/Linter/Spec.hs Adds linter-specific specs (sites, runtime-lazy exemption, Let scoping rules).
test/Language/PureScript/Backend/IR/DCE/Spec.hs Adds regression test covering the nested-Let DCE escape case.
pslua.cabal Exposes new library modules and includes new specs in the test suite.
lib/Language/PureScript/Names.hs Documents the additional runtime-lazy coupling site in the new linter.
lib/Language/PureScript/Backend/IR/Supply.hs Adds deterministic counter-based name supply for IR passes.
lib/Language/PureScript/Backend/IR/Pass.hs Adds pass/step definitions, invariant checking, tracing runner, and monadic fixpoint helper.
lib/Language/PureScript/Backend/IR/Optimizer.hs Refactors optimizer pipeline into first-class steps; adds checked runner entrypoint.
lib/Language/PureScript/Backend/IR/Linter.hs Implements module-level linting and unboundLocals well-scopedness check.
lib/Language/PureScript/Backend/IR/FlattenDeepBinds.hs Ports flattening to use the shared deterministic supply (flattenDeepBindsM).
lib/Language/PureScript/Backend/IR/DCE.hs Fixes DCE rewrite behavior for nested Let revealed by per-pass checking.
lib/Language/PureScript/Backend.hs Adds lint-ir parameter and plumbs checked optimization into compilation.
exe/Main.hs Adds CLI-side error handling for PassCheckFailure.
exe/Cli.hs Adds --lint-ir flag.
changelog.d/20260703_121000_unisay_dce_nested_let.md Changelog entry for the DCE nested-Let fix.
changelog.d/20260703_120000_unisay_pass_pipeline.md Changelog entry for the first-class pass pipeline and --lint-ir.

Comment thread lib/Language/PureScript/Backend/IR/Optimizer.hs Outdated
@Unisay Unisay merged commit 180670d into main Jul 3, 2026
2 checks passed
@Unisay Unisay deleted the issue-138/pass-pipeline branch July 3, 2026 07:27
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

First-class passes for the IR pipeline: Pass values, invariant checks, deterministic name supply

2 participants