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

Run tests with a range of values for inliner_aggressiveness to test for divergences in behaviour. #6349

Closed
TomAFrench opened this issue Oct 25, 2024 · 8 comments · Fixed by #6352 or #6355
Labels
enhancement New feature or request

Comments

@TomAFrench
Copy link
Member

@aakoshh noticed in #6340 that compiling the trait_eq::inequality test fails with inliner_aggressiveness = 0 but passes with inliner_aggressiveness = 9223372036854775807. We would expect that the resultant brillig bytecode should be equivalent but this is not the case.

We should update the test suite to run at a number of different levels of inliner aggressiveness to check that we don't get different behaviour presented.

cc @sirasistant as non-inlining behaviour is resulting in correctness issues.

@github-project-automation github-project-automation bot moved this to 📋 Backlog in Noir Oct 25, 2024
@TomAFrench TomAFrench added the enhancement New feature or request label Oct 25, 2024
@sirasistant
Copy link
Contributor

Investigating...

@sirasistant
Copy link
Contributor

I see the issue, it's related with array_set_mut:

unconstrained fn main() {
    let mut bounded_vec1: BoundedVec<Field, 3> = BoundedVec::new();
    let mut bounded_vec2: BoundedVec<Field, 3> = BoundedVec::new();
    bounded_vec1.push(1);
    bounded_vec2.push(2);

    std::println(bounded_vec1.storage());
    std::println(bounded_vec2.storage());
}

After Array Set Optimizations:
brillig(inline) fn main f0 {
  b0():
    inc_rc [Field 0, Field 0, Field 0]
    v2 = allocate
    store [Field 0, Field 0, Field 0] at v2
    v3 = allocate
    store u32 0 at v3
    inc_rc [Field 0, Field 0, Field 0]
    v5 = allocate
    store [Field 0, Field 0, Field 0] at v5
    v6 = allocate
    store u32 0 at v6
    call f1(v2, v3, Field 1)
    call f1(v5, v6, Field 2)
    v11 = load v2
    call f2(v11)
    v13 = load v5
    call f2(v13)
    return 
}
brillig(inline) fn push f1 {
  b0(v0: &mut [Field; 3], v1: &mut u32, v2: Field):
    v3 = load v1
    v5 = lt v3, u32 3
    constrain v5 == u1 1 '"push out of bounds"'
    v7 = load v0
    v8 = load v1
    v9 = load v1
    v10 = array_set mut v7, index v9, value v2
    store v10 at v0
    store v8 at v1
    v11 = load v0
    v12 = load v1
    v14 = add v12, u32 1
    store v11 at v0
    store v14 at v1
    return 
}
brillig(inline) fn println f2 {
  b0(v0: [Field; 3]):
    call v1(u1 1, v0, [u8 123, u8 34, u8 107, u8 105, u8 110, u8 100, u8 34, u8 58, u8 34, u8 97, u8 114, u8 114, u8 97, u8 121, u8 34, u8 44, u8 34, u8 108, u8 101, u8 110, u8 103, u8 116, u8 104, u8 34, u8 58, u8 51, u8 44, u8 34, u8 116, u8 121, u8 2⁴×7, u8 101, u8 34, u8 58, u8 123, u8 34, u8 107, u8 105, u8 110, u8 100, u8 34, u8 58, u8 34, u8 102, u8 105, u8 101, u8 108, u8 100, u8 34, u8 125, u8 125], u1 0)
    return 
}

As you can see in fn push, it's using array_set mut, which ignores reference counters, so it's mutating [Field 0, Field 0, Field 0] which is shared in two variables (if it wasn't mut, it would work correctly, since its reference counter is correct, 2)

@sirasistant
Copy link
Contributor

cc @vezenovm

@aakoshh
Copy link
Contributor

aakoshh commented Oct 25, 2024

Good spot! I eyeballed the whole SSA printout top to bottom but missed the mut at the last step.

I'll open a PR with the test changes to call with/without brillig and various inlining aggressiveness.

@sirasistant
Copy link
Contributor

Probably 2 or 3 levels of aggressiveness should be enough (MIN_VALUE, 0, MAX_VALUE). Or MIN_VALUE and MAX_VALUE only if it's too costly

@vezenovm
Copy link
Contributor

vezenovm commented Oct 25, 2024

I'm looking at a fix to the array mut issue. I'm actually surprised to that v7 is being marked mutable as the pass bans arrays loaded from references to be marked mutable, but we must be missing something.

EDIT: found the bug

@aakoshh
Copy link
Contributor

aakoshh commented Oct 25, 2024

Looking at this it looks like the return block overrules the load 👀

@vezenovm
Copy link
Contributor

Looking at this it looks like the return block overrules the load 👀

Yes that is the issue. It was fine when we inlined everything but not anymore.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request
Projects
Status: ✅ Done
4 participants