fix: vector_push_front is PureWithPredicate - #13445
Conversation
…utator hoist The miscompilation is reachable from plain Noir source, not just hand-written SSA: with x = true, n = 1 the program returns false on the base commit because the hoisted vector_push_front mutates v in place. The test asserts the correct semantics, so it stays red until LICM keeps (or re-establishes) the inc_rc guard on the hoisted mutator's operands. Reaching the bug from source requires defeating three masking mechanisms, documented in the test: a dynamic vector length (constant lengths fold before LICM), spare capacity with refcount 1 at the pre-header (a fresh as_vector() reallocates harmlessly), and no use of the vector between the loops (which would emit a guarding inc_rc clone in the pre-header). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
|
Pushed 2a75f19: the bug is reachable from plain Noir source, so this PR now also carries a deliberately failing source-level regression test, With
The |
…er around a vector mutator Source-level variant of the user-function-wrapper bypass described in https://gist.github.com/AztecBot/b4b227ffacd5e2cc17e703255e98c22b: LICM hoists calls to user functions by recorded callee purity, so a fix that only guards hoisted intrinsic calls would leave this test red. Under low inliner aggressiveness (exercised by the CI inliner matrix) the wrapper survives to LICM as a real call and is hoisted away from its inc_rc guard; under high aggressiveness it inlines and reduces to the direct-intrinsic case. Keeping the wrapper alive from source needs a loop in its body (defeats simple-function inlining), two call sites (defeats always-inline-when-called-once), and Field arithmetic (checked u32 ops would make it PureWithPredicate, whose hoisting path is blocked by the preceding side-effecting inc_rc; only fully-pure callees hoist unconditionally). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
|
Pushed fd8540b: a second failing source-level test, Under low inliner aggressiveness (the CI inliner matrix covers this) Reaching the wrapper path from source needs three things beyond the first test: a loop in the wrapper body (defeats simple-function inlining), two call sites (functions called once are always inlined), and |
…vector mutator out of an empty loop Third source-level shape of the miscompilation, distinct from the stranded-guard cases: with m = 0 the push_front loop never executes, yet v is still corrupted. The fully-Pure branch of can_hoist_invariant checks neither does_execute nor block impurity, so the hoisted mutator runs once in the pre-header of a zero-iteration loop; assert(acc == 0) passes while assert(v[0] == x) fails. This also pins down that inserting a pre-header inc_rc alone is not a sufficient fix for the Pure path: the hoisted push must not execute speculatively at all (today a copying push is only harmless because its result is dead). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…ps it behind its inc_rc guard
vector_push_front was the only vector mutator classified fully Pure: it
needs no non-emptiness assertion and its ACIR lowering does not read the
side-effects variable, so it fell through purity()'s catch-all. But in
Brillig it can write through its vector argument in place when the
argument's runtime reference count is 1, and the fully-Pure hoisting
path in loop-invariant code motion checks neither block impurity nor
whether the loop executes. LICM therefore hoisted the call into the
pre-header, away from the inc_rc guarding its operand (or into a path
the source program never executes), mutating a still-live vector in
place.
Classifying it PureWithPredicate routes it through the predicated
hoisting path, which refuses to move it past the side-effecting inc_rc
the ownership pass emits directly before it and refuses to hoist it out
of loops that may not execute. Functions wrapping the intrinsic inherit
the classification through purity analysis, closing the pure-wrapper
bypass as well.
Also replaces purity()'s catch-all arms with an exhaustive enumeration
so future intrinsics require an explicit purity decision.
The regression test loses its #[should_panic]: interpreting before and
after LICM now agrees. The three execution_success programs
(regression_licm_vector_mutator{,_wrapper,_empty_loop}) turn green,
including the wrapper variant under minimum inliner aggressiveness,
where the wrapper survives to LICM as a real call.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
vector_push_frontwasn't considered as PureWithPredicate in the purity analysis pass. This was likely an oversight has every other vector intrinsic is marked like that.This PR fixes that, but it also exhaustively lists all the intrinsics so it's easier to see if we missed some.
Below is Claude's finding:
What
Adds a load-bearing reproduction (no fix) for the AST fuzzer
pass_vs_prevfailure on seed0xb6bc8e1f00100000againstmaster(d89d99a944). This is a silent miscompilation (wrong result, no error), bisected to the Loop Invariant Code Motion pass.The bug
Brillig arrays/vectors are copy-on-write: a mutating op (
array_set, the vector push/pop/insert/remove intrinsics) writes through its operand in place once that operand's reference count is 1, and clones otherwise. The compiler keeps this safe by emitting aninc_rcon any operand still live after the mutation.In the reduced SSA below,
v1is guarded byinc_rc v1immediately beforevector_push_front, becausev1is read again by thearray_getinb3:vector_push_frontisPureWithPredicate, so LICM hoists the call into the loop pre-header — but theinc_rcguard is a separate instruction thatcan_be_hoistedclassifiesNoand never hoists. Separated from its guard, the hoisted push findsv1at refcount 1 and writes through it in place, corrupting the array thatb3later reads. Interpretingfoo([true, 1])returns1before LICM and0after.The reproduction
ssa::opt::loop_invariant::tests::hoisting_vector_mutator_out_of_loop_drops_refcount_guardruns the reduced SSA throughassert_pass_does_not_affect_execution, which interprets before and after LICM and panics because the results differ (1→0) onmaster. It is marked#[should_panic(expected = "SSA pass has resulted in a different execution result")]to document the miscompilation deterministically; once LICM re-establishes aninc_rcon the array operands of a hoisted vector mutator, the results match and the#[should_panic]should be removed.Severity
High. A loop-invariant vector push/pop/insert/remove in a guaranteed-executed loop can be hoisted in a way that mutates a still-live array and yields a wrong result, with no error.
Related issues
Refs noir-lang/noir-claude#244
This PR closes nothing — it is reproduction-only, adds a failing-by-design test, and changes no compiler behaviour, so #244 stays open after it merges. The closing keyword belongs on the fix PR. (It would not auto-close in any case: GitHub only auto-closes issues in the PR's own repo.)
The relevant history sits in the same ~20 lines of
compiler/noirc_evaluator/src/ssa/opt/loop_invariant.rs:array_setwithout insertinginc_rc". Its fix, fix(licm): Insertinc_rcafter hoistingarray_set#12665 (491cde769d4), is what added theMakeArray | ArraySet => trueandCall-returning-array arms tocan_hoist_invariant'sreturns_array. That compensation guards the hoisted instruction's results, never its array operands — which is precisely the gap this seed hits.insert_rcdoes fire here (aCallwith an array result), but theinc_rcprotecting the operandv1is what stays behind.triage:high) — flags that the compensatinginc_rcfrom that fix is inserted into*block(the loop body) rather thanpre_header. Still true atd89d99a944. Any fix for this PR touches the same branch, so the two are worth resolving together.Nargo.tomlfromConfigtoPackageManifest#1006), and open #1534 / #1535 / #1563 — gaps in therc_invariantverifier that is meant to catch exactly this class of RC-1 in-place mutation, none of which has a term for the hoisted-mutator case either.No open AST Fuzzer issue in this repo covers this. Full RCA + a suggested fix: https://gist.github.com/AztecBot/55e49989fcd3a1ae45f5e3a865d8c2d8
Created by claudebox · group:
slackbot· requested by Tom French · Slack thread