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: add u128 overflow checks after DIE #7587

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

Conversation

asterite
Copy link
Collaborator

@asterite asterite commented Mar 5, 2025

Description

Problem

Resolves #7555

Summary

The compiler generally doesn't issue overflow errors for expressions that end up being unused. The overflow checks for u128 were added before the first DIE pass and contain some div and constrain instructions that DIE won't remove. Adding these checks after the first DIE fixes the issue as the multiplications are removed by DIE so no checks are added.

Additional Context

  1. I originally added a test program as a regression. However, it fails when debugging the program: it seems when debugging the overflow is encountered, even if the expressions are unused. I checked and it's the same case if the variables are u64 so this is existing behavior. So... it's hard to prove that this PR fixes the issue, but the diff makes it clear what's the change.
  2. It's not clear if overflows for unused expressions should be removed or not, but this is what the compiler does in other cases so at least this makes the compiler work the same way in all cases.

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.

@TomAFrench
Copy link
Member

Seems like we could have this easily reoccur in some cases if we were to add more passes in future which would result in more u128 ops being revealed as unused in later passes. 🤔

@asterite
Copy link
Collaborator Author

asterite commented Mar 5, 2025

I also checked what happened with signed integers: it always fails with overflow regardless of ACIR and brillig, because the checks are inserted during SSA.

One way to solve this particular case is to always check for u128 overflow in SSA, even for brillig. However, for other unsigned types it will still be different (no overflow on unused expressions).

So maybe we need to answer this question first: do we want overflows for unused expressions or not?

@TomAFrench
Copy link
Member

TomAFrench commented Mar 6, 2025

Hmm, I'd be open to always performing overflow checks for unused expressions. It'll simplify us not having to jump through hoops to ensure that we never output overflow checks for these operations and I can imagine situations where people expect overflow checks on some arithmetic which they don't use of the result of to constrain a certain result.

e.g.

// Check that sum fits in a u8.
let _: u8 = x + y;

We would potentially take a hit on larger circuit sizes but then it's up to users to not add code to their circuit if they don't want it there.

@asterite
Copy link
Collaborator Author

asterite commented Mar 6, 2025

Would that require changes to the brillig vm to not check for overflows anymore?

@TomAFrench
Copy link
Member

I'm not sure I follow, how would this affect the brillig VM?

@asterite
Copy link
Collaborator Author

asterite commented Mar 7, 2025

If we always want to give an error on overflow then we must add those checks, which will end up being some constraint in the SSA. Then the logic to detect overflow in Brillig might not be needed (though to be honest I don't know if there's any logic for this, or maybe it's fine to have this be redundant).

That said, I think right now the checks are deferred to Brillig for performance reasons, so moving those checks back to SSA might introduce some undesired regressions.

@TomAFrench
Copy link
Member

I'm really not seeing where changes to brillig are coming in.

If I want to add two u32s together then we have the SSA

v2 = add v0 u32 2

v2 is unused so DIE would normally remove it (and the associated overflow check). If we stop removing arithmetic operations for which the result is unused then there's no change to the SSA and brillig and ACIR generation continue to behave exactly as they do today.

Now let's say it's u128s, we now have two different SSAs depending on the runtime:

// acir
v2 = add v0 u32 2
<insert extra checks to prevent field modulus overflow>

// brillig
v2 = add v0 u32 2

We know that in ACIR between the standard overflow check and the extra checks injected by check_u128_mul_overflow then we'll continue to check for overflows the same as today. Similarly in the brillig VM we'll do the regular overflow check on the addition.

Based on this I really don't see how changing how the DIE pass treats unused arithmetic instructions affects whether the brillig VM needs to do overflow checks.

@asterite
Copy link
Collaborator Author

asterite commented Mar 7, 2025

If we stop removing arithmetic operations for which the result is unused

Ah, this is what I was missing. I thought we'd add the checks in SSA, then DIE wouldn't remove those instructions, but in the end not removing the arithmetic operations that could overflow is the same, and simpler.

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.

u128 mul in acir and brillig differs
2 participants