fix(ssa): accept array_set on transitively-fresh swapped loop sibling - #13308
Draft
AztecBot wants to merge 1 commit into
Draft
fix(ssa): accept array_set on transitively-fresh swapped loop sibling#13308AztecBot wants to merge 1 commit into
AztecBot wants to merge 1 commit into
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Problem
The debug-only Brillig
rc_invariant::array_setSSA validator produced a false positive on AST-fuzzer seed0xfe6bbee600100000(comptime_vs_brillig_direct), aborting compilation afterMem2Reg:Disabling the check and re-running the full comparison shows the Brillig VM and the comptime interpreter agree — the rejected
array_setis sound and the validator was over-approximating.Root cause
The mutated array
v105(outer loop headerb21) is rebound on its back-edge (b25: jmp b21(v74, v106)) tov106, the header parameter of a nested loop (b24).v106mixes two sources: a freshmake_array(v71) on its own back-edge and a forward-edge alias of the mutatedv105on its entry edge (b22: jmp b24(v105, u32 0)). The mutating branchb23is only reachable after the inner loop has re-defined the loop-carried value from its fresh back-edge source, so the storagev105mutates is a distinct per-iteration allocation and everyarray_get v106read happened on a prior iteration over different fresh storage.The existing "swapped-in loop sibling" freshness relaxation (the #12929 fix) only recognizes a sibling parameter of the same header that is re-allocated fresh directly each iteration. It does not follow the swap transitively through a second, nested loop header, so it failed to classify
v106as iteration-local fresh.Fix
Extend the swap exclusion in
rc_invariant/mod.rsso a swapped-insiblingalso qualifies as a distinct per-iteration storage when it is the loop-carried parameter of a nested loop header, gated by three sound, structural conditions (is_transitively_fresh_sibling):make_array/Callresult.Together these guarantee the swapped-in exit value was never read on its own iteration while every in-loop read observed a distinct earlier allocation, so the source's later in-place mutation has no live aliased read.
Because such a sibling also carries a forward-edge alias of the source into its own loop,
find_reachable_aliased_useadditionally marks it protected so the forward walk never re-adds it via the add-rule.Testing
accepts_array_set_on_transitively_fresh_swapped_sibling— the reduced seed SSA; red before the fix, green after.end_to_end_nested_swap_without_inner_freshening_is_rejected— soundness canary: the same shape but with the inner back-edge threading the sibling unchanged (non-fresh) must still be rejected, pinning the load-bearing freshening requirement.rc_invariant(72) andvalidation(188) unit suites pass;cargo fmt+clippyclean.NOIR_AST_FUZZER_SEED=0xfe6bbee600100000 CI=1 cargo test -p noir_ast_fuzzer_fuzz comptime_vs_brillig_directnow passes (previously aborted in the validator).Closes #13280
Closes #13280
Created by claudebox · group:
slackbot