fix(review): apply autofix feedback (#2201)

- Close the production SSA-dispatcher fuzz-coverage gap: the generator's
  maxBlocks=14 was below SSA_MIN_BLOCKS=16, so the auto-dispatcher's SSA branch
  was never differentially fuzzed. Raise to 36, add a hadLargeLoop coverage
  assertion + a back-edge-into-entry canonical CFG. Validated byte-identical on
  100k random CFGs incl. >=16-block looping shapes via both entry points.
- Correct stale function JSDocs + @internal annotations (dispatch/fallback roles).
- Add an independent rd_all_computed bench gate (catches partial truncation).
- maxBlockVisits comment, SSA_MIN_BLOCKS calibration note, nx->next rename.
This commit is contained in:
Gergo Magyar 2026-06-15 15:18:10 +00:00
parent 1eb12504e8
commit 360b2034b4
3 changed files with 96 additions and 27 deletions

View file

@ -626,6 +626,15 @@ if (!CHECK) {
(r.rd_all_computed ? '' : ` [status != computed]`),
);
}
// Independent of the fact-count floor: under the production budget every
// function in a facts_large_min scenario must report status 'computed'. This
// catches a partial-truncation regression that still clears the count floor.
if (base.facts_large_min !== undefined && r.rd_all_computed === false) {
failures.push(
`${r.scenario}: a function did not reach status 'computed' under the production ` +
`block-visit budget — the SSA solver truncated where it must compute`,
);
}
if (base.disk_bytes_large_max !== undefined && r.disk_bytes_large > base.disk_bytes_large_max) {
failures.push(
`${r.scenario}: cfgSideChannel absolute size ${r.disk_bytes_large} > ceiling ` +

View file

@ -201,11 +201,14 @@ type InSetsComputer = (
* Compute reaching definitions for one function. See the module doc for the
* purity/determinism/sharing contract.
*
* This is the production entry point. As of #2201 it runs the sparse, change-
* driven solver ({@link computeInSetsSparse}); the dense GEN/KILL worklist
* ({@link computeReachingDefsDense}) is retained as the differential
* equivalence oracle the fuzz suite checks the sparse path against — the two
* MUST be byte-identical (status, bindings, sorted facts, def/use telemetry).
* This is the production entry point. As of #2201 it auto-dispatches via
* {@link computeInSetsAuto} — the SSA-sparse solver ({@link computeInSetsSparse})
* for looping functions large enough to amortize construction, the dense
* GEN/KILL worklist ({@link computeInSetsDense}) everywhere else (and for the
* throw-edge / unreachable-block functions the SSA path does not model). The two
* solvers are held byte-identical by the equivalence fuzz (status, bindings,
* sorted facts, def/use telemetry), so the dispatch is a pure performance
* heuristic; the dense solver doubles as that differential oracle.
*/
export function computeReachingDefs(cfg: FunctionCfg, limits?: ReachingDefsLimits): FunctionDefUse {
// #2201: production auto-selects the solver per function (see
@ -219,12 +222,14 @@ export function computeReachingDefs(cfg: FunctionCfg, limits?: ReachingDefsLimit
/**
* Dense GEN/KILL monotone worklist — the original (#2082 M2) reaching-defs
* solver. As of #2201 this is RETAINED AS A TEST/BENCH-ONLY DIFFERENTIAL
* ORACLE, not a production code path: {@link computeReachingDefs} runs the
* sparse solver, and the equivalence fuzz asserts the two are byte-identical
* across a random-CFG corpus. Keep it behavior-frozen — it is the ground truth.
* solver. As of #2201 it plays two roles: (1) the production dispatcher
* ({@link computeInSetsAuto}) routes small / loop-free functions, and the
* throw-edge / unreachable-block functions the SSA path does not model, to this
* dense solver; (2) it is the differential equivalence ORACLE the fuzz checks
* the SSA path against. Keep it behavior-frozen — it is the ground truth.
*
* @internal exported only for the equivalence fuzz harness and the cfg bench.
* @internal exported for the equivalence fuzz harness (direct dense-vs-sparse
* comparison); the bench drives the production {@link computeReachingDefs}.
*/
export function computeReachingDefsDense(
cfg: FunctionCfg,
@ -234,12 +239,13 @@ export function computeReachingDefsDense(
}
/**
* Sparse, change-driven reaching-defs (#2201) — the production solve, exposed
* directly so the equivalence fuzz can gate it against the dense oracle before
* {@link computeReachingDefs} is switched over to it (U5). See
* {@link computeInSetsSparse} for the algorithm and byte-identical contract.
* SSA-sparse reaching-defs (#2201) — exposed directly so the equivalence fuzz
* can drive the SSA solver on every eligible CFG (bypassing the production
* size/loop dispatch heuristic in {@link computeInSetsAuto}) and assert
* byte-identity against the dense oracle. See {@link computeInSetsSparse} for
* the algorithm and byte-identical contract.
*
* @internal exported only for the equivalence fuzz harness and the cfg bench.
* @internal exported only for the equivalence fuzz harness.
*/
export function computeReachingDefsSparse(
cfg: FunctionCfg,
@ -788,7 +794,15 @@ function computeInSetsSparse(
};
}
/** Minimum block count below which SSA construction does not amortize. */
/**
* Minimum block count below which SSA construction (dominators + dominance
* frontiers + φ-placement + renaming + SCC) does not amortize over the dense
* worklist's single-pass aliasing. Calibrated empirically (~14-block crossover
* for loop-heavy functions; 16 leaves headroom); the dense-bindings
* `rd_scaling_budget` gate in bench/cfg/baselines.json catches a regression if
* this is mistuned. Paired with a reachable-loop check — loop-free functions
* always take the cheaper dense path regardless of size.
*/
const SSA_MIN_BLOCKS = 16;
/**
@ -803,11 +817,11 @@ function hasReachableLoop(entry: number, succs: readonly number[][], n: number):
const top = stack[stack.length - 1];
const ss = succs[top.node];
if (top.i < ss.length) {
const nx = ss[top.i++];
if (color[nx] === 1) return true;
if (color[nx] === 0) {
color[nx] = 1;
stack.push({ node: nx, i: 0 });
const next = ss[top.i++];
if (color[next] === 1) return true;
if (color[next] === 0) {
color[next] = 1;
stack.push({ node: next, i: 0 });
}
} else {
color[top.node] = 2;

View file

@ -76,7 +76,13 @@ interface GenOpts {
}
const DEFAULT_GEN: GenOpts = {
maxBlocks: 14,
// Span both sides of the production SSA dispatch threshold (SSA_MIN_BLOCKS=16):
// CFGs below it route the auto-dispatcher (computeReachingDefs) to dense, those
// above with a reachable loop route it to the SSA path — so the corpus
// differentially exercises BOTH branches of computeInSetsAuto, not just the
// forced-SSA computeReachingDefsSparse entry. See the hadLargeLoop coverage
// guard below.
maxBlocks: 36,
maxBindings: 8,
maxStmtsPerBlock: 4,
pNoBindings: 0.03,
@ -295,6 +301,22 @@ function canonicalHardCfgs(): FunctionCfg[] {
),
);
// (6) Back-edge into the ENTRY block: 0 (def+use x) → 1 (def+use x) → 0 (loop
// back to entry) and 1 → 2 (exit, use x). The SSA solver's synthetic pre-entry
// node exists precisely for this — the entry is a loop header, so x's loop-
// carried def must reach the entry's own use. Pins that path deterministically.
out.push(
mk(
[blk(0, [st(1, [0], [0])]), blk(1, [st(2, [0], [0])]), blk(2, [st(3, [], [0])])],
[
{ from: 0, to: 1, kind: 'seq' },
{ from: 1, to: 0, kind: 'loop-back' },
{ from: 1, to: 2, kind: 'cond-false' },
],
[bind('x', 1)],
),
);
return out;
}
@ -333,6 +355,10 @@ interface ShapeFlags {
hasShadow: boolean;
hasMultiPred: boolean;
hasUnreachable: boolean;
// ≥16-block CFG (SSA_MIN_BLOCKS) with a loop reachable from entry — the exact
// shape the production dispatcher (computeInSetsAuto) sends to the SSA solver.
// Asserting it proves the auto-dispatcher's SSA branch is differentially fuzzed.
hadLargeLoop: boolean;
hadComputed: boolean;
hadTruncated: boolean;
hadNoFacts: boolean;
@ -385,6 +411,22 @@ function classify(cfg: FunctionCfg, flags: ShapeFlags): void {
for (const y of succ[x]) if (!seen[y]) ((seen[y] = true), q.push(y));
}
if (seen.some((v, i) => !v && i < n)) flags.hasUnreachable = true;
// loop reachable from entry (matches the dispatcher's hasReachableLoop) +
// ≥16 blocks ⇒ the production auto-dispatcher routes this CFG to the SSA path.
const c2 = new Array(n).fill(0);
let entryLoop = false;
const st2: { node: number; idx: number }[] = [{ node: cfg.entryIndex, idx: 0 }];
c2[cfg.entryIndex] = 1;
while (st2.length && !entryLoop) {
const top = st2[st2.length - 1];
if (top.idx < succ[top.node].length) {
const v = succ[top.node][top.idx++];
if (c2[v] === 1) entryLoop = true;
else if (c2[v] === 0) ((c2[v] = 1), st2.push({ node: v, idx: 0 }));
} else ((c2[top.node] = 2), st2.pop());
}
if (n >= 16 && entryLoop) flags.hadLargeLoop = true;
}
// ── corpus runner ──────────────────────────────────────────────────────────
@ -399,11 +441,13 @@ function runCorpus(
right: Solver,
count: number,
baseSeed: number,
// maxBlockVisits has DIFFERENT (intentional) semantics across the dense and
// sparse solvers — dense counts block dequeues, sparse counts (block,binding)
// dequeues — so a small budget truncates them at different points. Perturb it
// only when comparing a solver against ITSELF (same semantics); cross-solver
// byte-identity is asserted with the budget unlimited (both fully converge).
// maxBlockVisits has DIFFERENT (intentional) semantics across the solvers: the
// dense worklist counts block dequeues against it; the SSA solver has no
// fixpoint iteration and ignores it in its main path (it only flows through to
// the dense fallback for throw-edge/unreachable functions). So a tight budget
// truncates them at different points. Perturb it only when comparing a solver
// against ITSELF (same semantics); cross-solver byte-identity is asserted with
// the budget unlimited (both fully converge).
perturbBlockVisits = true,
): CorpusResult {
const flags: ShapeFlags = {
@ -411,6 +455,7 @@ function runCorpus(
hasThrow: false,
hasMayDef: false,
hasShadow: false,
hadLargeLoop: false,
hasMultiPred: false,
hasUnreachable: false,
hadComputed: false,
@ -476,6 +521,7 @@ describe('#2201 reaching-defs differential equivalence', () => {
expect(f.hasShadow, 'shadowed bindings').toBe(true);
expect(f.hasMultiPred, 'multi-pred joins').toBe(true);
expect(f.hasUnreachable, 'unreachable blocks').toBe(true);
expect(f.hadLargeLoop, '≥16-block looping CFGs (production SSA dispatch path)').toBe(true);
expect(f.hadComputed, 'computed results').toBe(true);
expect(f.hadTruncated, 'truncated results').toBe(true);
expect(f.hadNoFacts, 'no-facts results').toBe(true);