Test references fails with inliner = -Inf and brillig

[aakoshh]

Aim

Trying to run test_programs with different --inliner-aggressiveness in #6429

Expected Behavior

Tests under execution_success should work.

Bug

❯ nargo execute --force --inliner-aggressiveness -9223372036854775808 --force-brillig
error: Failed to solve program: 'Failed to solve brillig function'
    ┌─ /Users/aakoshh/Work/aztec/noir/test_programs/execution_success/references/src/main.nr:115:12
    │
115 │     assert(*x == 1);
    │            -------
    │
    = Call stack:
      1. /Users/aakoshh/Work/aztec/noir/test_programs/execution_success/references/src/main.nr:28:5
      2. /Users/aakoshh/Work/aztec/noir/test_programs/execution_success/references/src/main.nr:115:12

Failed to solve program: 'Failed to solve brillig function'

To Reproduce

1. cd test_programs/execution_success/references
2. nargo execute --force --force-brillig --inliner-aggressiveness -9223372036854775808

Workaround

None

Workaround Description

No response

Additional Context

No response

Project Impact

None

Blocker Context

No response

Nargo Version

nargo version = 0.36.0 noirc version = 0.36.0+2f0cb3e80f3d93a1dee77fffacc397811e300257 (git version hash: 2f0cb3e, is dirty: false)

NoirJS Version

No response

Proving Backend Tooling & Version

No response

Would you like to submit a PR for this Issue?

None

Support Needs

No response

[aakoshh]

To minimise the SSA size the program has been reduced to the following:

fn main(mut x: Field) {
    regression_2255();
}

// The `mut x: &mut ...` caught a bug handling lvalues where a double-dereference would occur internally
// in one step rather than being tracked by two separate steps. This lead to assigning the 1 value to the
// incorrect outer `mut` reference rather than the correct `&mut` reference.
fn regression_2255() {
    let x = &mut 0;
    regression_2255_helper(x);
    assert(*x == 1);
}

fn regression_2255_helper(mut x: &mut Field) {
    *x = 1;
}

Running it with the following command:

cargo run -q -p nargo_cli --  --program-dir . execute --force --force-brillig --inliner-aggressiveness -9223372036854775808 --show-ssa

The initial SSA is this:

Initial SSA:
brillig(inline) fn main f0 {
  b0(v0: Field):
    v1 = allocate
    store v0 at v1
    call f1()
    return 
}
acir(inline) fn regression_2255 f1 {
  b0():
    v0 = allocate
    store Field 0 at v0
    call f2(v0)
    v3 = load v0
    v5 = eq v3, Field 1
    constrain v3 == Field 1
    return 
}
acir(inline) fn regression_2255_helper f2 {
  b0(v0: &mut Field):
    v1 = allocate
    store v0 at v1
    v2 = load v1
    store Field 1 at v2
    return 
}

And the final form:

After Array Set Optimizations:
brillig(inline) fn main f0 {
  b0(v0: Field):
    call f1()
    return 
}
brillig(inline) fn regression_2255 f1 {
  b0():
    v0 = allocate
    store Field 0 at v0
    call f2(v0)
    v3 = load v0
    constrain v3 == Field 1
    return 
}
brillig(inline) fn regression_2255_helper f2 {
  b0(v0: &mut Field):
    return 
}

Somehow the store Field 1 at v2 completely disappeared from regression_2255_helper f2.

Going down the passes in the full printout we can see that this happens After Mem2Reg: (the first one).
According to its docs mem2reg is supposed to do the following:

    /// Attempts to remove any load instructions that recover values that are already available in
    /// scope, and attempts to remove stores that are subsequently redundant.

In our case that means:

    v1 = allocate
    store v0 at v1
    v2 = load v1          <- get rid of this because v1 is already available
    store Field 1 at v2   <- get rid of subsequent use of v2

However the subsequent use of v2 is not redundant, it should be replaced with storing the field in v1, or perhaps v0.

[aakoshh]

NB if we run the program with 0 aggressiveness:

cargo run -q -p nargo_cli --  --program-dir . execute --force --force-brillig --inliner-aggressiveness 0 --show-ssa

Then everything gets inlined and eliminated, including the assertions.

After Array Set Optimizations:
brillig(inline) fn main f0 {
  b0(v0: Field):
    call f1()
    return 
}
brillig(inline) fn regression_2255 f1 {
  b0():
    return 
}

[aakoshh]

As an experiment we can change the test code to remove the outer mut from mut x: &mut Field (which is what the docs of regression_2255 say caused the bug the test is trying to capture):

fn regression_2255_helper(x: &mut Field) {
    *x = 1;
}

In this case the SSA of the helper becomes simpler by writing directly to the v0 reference:

brillig(inline) fn regression_2255_helper f2 {
  b0(v0: &mut Field):
    store Field 1 at v0
    return 
}

However after the mem2reg pass this store is completely removed, and the test fails:

brillig(inline) fn regression_2255_helper f2 {
  b0(v0: &mut Field):
    return 
}

I'll add a new test for this.

👉 Perhaps something similar to #6355 can be done where we remember that this reference came from a block parameter, and therefore it cannot be eliminated because it might be shared with the caller.

Just for the record, with mut in place, we had this SSA:

brillig(inline) fn regression_2255_helper f2 {
  b0(v0: &mut Field):
    v1 = allocate        <- allocate a new reference for `mut x`
    store v0 at v1       <- store the reference v0 itself, not its value, in v1
    v2 = load v1         <- load the contents of v1, which is the reference v0, into v2
    store Field 1 at v2  <- store a value at v2, which should write to v0
    return 
}