Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

fix(ssa): Use post order when mapping instructions in loop invariant pass #7140

Open
wants to merge 3 commits into
base: master
Choose a base branch
from

Conversation

vezenovm
Copy link
Contributor

@vezenovm vezenovm commented Jan 21, 2025

Description

Problem*

Resolves #7128

Summary*

Ended up being a small fix as it was a silly oversight for how we should be mapping instructions. I switched away from using a BTreeSet of blocks (the return value from reachable_blocks()) to using the reverse post order when mapping functions.

Mapping instructions by the blocks consecutive ordering is incorrect as we may have a situation like such:

acir(inline) fn main f0 {
  b0(v0: Field):
    jmp b3(v0)
  b3(v1: Field):
    v2 = allocate -> &mut Field
    store Field 0 at v2
    v4 = eq v1, Field 0
    jmpif v4 then: b1, else: b2
  b1():
    v5 = load v2 -> Field
    return
  b2():
    return
}

We want to map the instructions from b3 first, not b1 and b2. In the erroneous way we are mapping on master we could potentially be keeping the same load v2 in b1 while v2 = allocate is updated to a new value. The panics from the missing else block in the issue were occurring due to this same bug.

I noticed this as the cause of the bug when printing the SSA would get rid of all the bugs listed in the issue. This was due to the normalization pass which would make the reverse post order of the blocks line up with their consecutive numerical ordering.

Additional Context

This ended up being fixed inadvertently by the preprocessing PR. The last failing nightly was nightly-2025-01-20. I found the fix on the failing nightly and brought it over to master even though the test is technically passing on master already. The bug most likely did not come up previously due to mem2reg successfully removing references which may be shared across blocks and the preprocess PR further helped clear out these references which may be in numerically smaller children blocks.

I wanted to add a minor unit test to make sure we are mapping in the correct block order but this would require some extra changes to the SSA parser (putting a flag on ID normalization would not be enough as the parser also inserts at fresh IDs).

Perhaps we should add some extra safety checks or comments for using reachable_blocks.

Documentation*

Check one:

  • No documentation needed.
  • Documentation included in this PR.
  • [For Experimental Features] Documentation to be submitted in a separate PR.

PR Checklist*

  • I have tested the changes locally.
  • I have formatted the changes with Prettier and/or cargo fmt on default settings.

@vezenovm vezenovm requested review from TomAFrench and a team January 21, 2025 21:52
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.

Program exposes unsound and incomplete behavior
1 participant