Mem2Reg pass may produce incorrect code when mutable references are aliased

[alexvitkov]

Aim

In the following code, after the call to increment the value of x remains unchanged:

fn increment(mut r: &mut Field) {
    *r = *r + 1;
}

fn main() {
    let mut x = 100;
    let mut xref = &mut x;
    increment(xref);
    assert(*xref == 101); // fails! x is still 100
}

This bug is very similar to (possibly the same as) #2255, but there the mutable variable of type MutRef is a parameter, and here it's a local.

The SSA for increment is correct, the bug is in main:

acir fn main f0 {
  b0():
    v1 = allocate
    store Field 100 at v1
    v2 = allocate     // copying x
    store v1 at v2
    v4 = load v2      // reference to the copy
    call f1(v4)       // this modifies the copy
    v5 = load v2
    v6 = load v5
    v8 = eq v6, Field 101
    constrain v8
    return
}

Expected Behavior

the example proves properly

Bug

it doesn't

To Reproduce

No response

Installation Method

Compiled from source

Nargo Version

No response

Additional Context

No response

Would you like to submit a PR for this Issue?

Yes

Support Needs

No response

[jfecher]

The annotations aren't quite correct:

acir fn main f0 {
  b0():
    v1 = allocate
    store Field 100 at v1
    v2 = allocate     // copying x => does not copy x, this is a new allocation
    store v1 at v2    //=> store the reference in the new reference. Essentially v2 = &mut &mut 100
    v4 = load v2      // reference to the copy => Still a reference to the original, &mut 100
    call f1(v4)       // this modifies the copy => This call site is fine
    v5 = load v2
    v6 = load v5
    v8 = eq v6, Field 101
    constrain v8
    return
}

Looking at increment now:

acir fn increment f1 {
  b0(v0: reference):
    v1 = allocate
    store v0 at v1  //=> Ok, v1 = &mut &mut 100
    v2 = load v1  //=> v2 = &mut 100
    v3 = load v1  //=> v3 = &mut 100
    v4 = load v3  //=> 100
    v6 = add v4, Field 1  //=> 101
    store v6 at v2  //=> v2 = 101
    return 
}

I'm still investigating this since from this SSA alone I'm not sure why it is not working. Perhaps it is broken by a later pass.

Edit: I've confirmed the generated SSA is good through inlining until mem2reg where it does not track the aliases properly.

[jfecher]

Waiting until after #2243 to start on changing mem2reg to support alias analysis since both that PR and this change would change the mem2reg pass considerably they'd be difficult to merge otherwise.