fix: don't check for overflow when binary operation is simplified to constant

[asterite]

Description

Problem

Resolves #8833
Resolves #8305

Summary

There's already a simplification that will turn x - 0 into x. However, when creating the initial SSA we insert an overflow check after some binary operations, even if those binary operations end up being simplified. I thought about not inserting the overflow check when the instruction is simplified, but we don't know what it was simplified to or, well, we could check if it's a binary, etc., but it would be a bit bug-prone to do that.

Additional Context

1. I'm not sure how to test this.
2. Maybe these overflow checks shouldn't be inserted during SSA-gen, and instead be done in a later pass?

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.

[github-actions]

⚠️ Performance Alert ⚠️

Possible performance regression was detected for benchmark 'Execution Time'.
Benchmark result of this commit is worse than the previous benchmark result exceeding threshold 1.20.

Benchmark suite	Current: 6df513b	Previous: 6343a30	Ratio
rollup-merge	0.004 s	0.003 s	1.33

This comment was automatically generated by workflow using github-action-benchmark.

CC: @TomAFrench

[vezenovm]

I'm not sure this is the best solution, as I would expect our simplifications to handle this case. If the operation can be simplified I would expect the overflow checks to be simplified as well.
This is our final SSA:

After Dead Instruction Elimination (3) (step 43):
g0 = i8 135

brillig(inline) predicate_pure fn main f0 {
  b0():
    v2 = cast u8 135 as i8
    v3 = truncate v2 to 8 bits, max_bit_size: 9
    v4 = cast v3 as u8
    v6 = lt v4, u8 128
    constrain v6 == u1 0, "attempt to subtract with overflow"
    return v3
}

We know that we should be able to simplify this SSA. I think our signed cast simplification is incorrect. We are only simplifying if the signed cast is below 2^(bit_size - 1), however, this does not encompass fully how we represent signed integers. I think we could convert our unsigned type using IntegerConstant, and then we would also remove another place where we are duplicating field -> integer conversions.

[asterite]

For this program:

unconstrained fn main(x: i8) -> pub i8 {
    x - 0
}

we get this initial SSA:

brillig(inline) fn main f0 {
  b0(v0: i8):
    v1 = truncate v0 to 8 bits, max_bit_size: 9
    v2 = cast v1 as u8
    v3 = cast v0 as u8
    v5 = lt v3, u8 128
    v6 = not v5
    v7 = lt v2, u8 128
    v8 = eq v7, v5
    v9 = unchecked_mul v8, v6
    constrain v9 == v6, "attempt to subtract with overflow"
    v10 = cast v1 as i8
    return v10
}

There are no constants anymore so I don't think the cast can be simplified. It still does the overflow check for the binary operation, but there's no need to do it because it's subtracting zero from it. Maybe zero is a special case, not sure... What I mean is, I'm not sure this can be solved by further simplifying the "check_overflow" function.

[asterite]

Also this likely doesn't matter much because this only happens in the initial SSA codegen, so you'd really have to have - 0 in the source code, which should never be needed, so...

[vezenovm]

There are no constants anymore so I don't think the cast can be simplified. It still does the overflow check for the binary operation, but there's no need to do it because it's subtracting zero from it. Maybe zero is a special case, not sure... What I mean is, I'm not sure this can be solved by further simplifying the "check_overflow" function.

Yes, that one cannot be simplified as it is dynamic, and thus why the instructions generated by check_overflow are not simplified in this case. However, I think this is a separate issue, and maybe this is something for which we want to special case.

The snippet in the issue #8833 still can be simplified, and points me to that the cast simplification is incorrect. I would also expect these programs to produce the same SSA:
Unsimplified subtraction:

global a: i8 = -121;
unconstrained fn main() -> pub i8 {
    let mut b: u32 = (25 - 0);
    ((-(-a)) - 1)
}

No subtraction:

global a: i8 = -122;
unconstrained fn main() -> pub i8 {
    let mut b: u32 = 25;
    (-(-a))
}

With the current PR we would get the same SSA we get in the - 0 case when it should be able to simplify to returning a single value.

[asterite]

I now changed it to now to an overflow check if the binary operation was simplified to a constant. I personally think this makes sense, as if we were able to simplify the operation to a constant it means we were able to do it and there's no chance of an overflow, and lhs and rhs aren't needed for this operation anymore.

I understand that there might be some things to fix or improve in signed cast operations, but I think we'd still want to avoid doing overflow checks when they aren't needed, right?

[github-actions]

Changes to number of Brillig opcodes executed

Generated at commit: b89db34d84c6a56f04565a63f2b99b2f70ce731c, compared to commit: 6343a3029f4671c8e5f21afe4014ec9a50c05966

🧾 Summary (10% most significant diffs)

Program	Brillig opcodes (+/-)	%
signed_comparison_inliner_max	-7 ✅	-6.54%
signed_comparison_inliner_min	-7 ✅	-6.54%
signed_comparison_inliner_zero	-7 ✅	-6.54%

---

Full diff report 👇

Program	Brillig opcodes (+/-)	%
unary_operator_overloading_inliner_min	55 (-1)	-1.79%
unary_operator_overloading_inliner_max	40 (-1)	-2.44%
unary_operator_overloading_inliner_zero	40 (-1)	-2.44%
signed_comparison_inliner_max	100 (-7)	-6.54%
signed_comparison_inliner_min	100 (-7)	-6.54%
signed_comparison_inliner_zero	100 (-7)	-6.54%

[github-actions]

Changes to Brillig bytecode sizes

Generated at commit: b89db34d84c6a56f04565a63f2b99b2f70ce731c, compared to commit: 6343a3029f4671c8e5f21afe4014ec9a50c05966

🧾 Summary (10% most significant diffs)

Program	Brillig opcodes (+/-)	%
signed_comparison_inliner_max	-9 ✅	-6.92%
signed_comparison_inliner_min	-9 ✅	-6.92%
signed_comparison_inliner_zero	-9 ✅	-6.92%

---

Full diff report 👇

Program	Brillig opcodes (+/-)	%
unary_operator_overloading_inliner_min	61 (-1)	-1.61%
unary_operator_overloading_inliner_max	50 (-1)	-1.96%
unary_operator_overloading_inliner_zero	50 (-1)	-1.96%
signed_comparison_inliner_max	121 (-9)	-6.92%
signed_comparison_inliner_min	121 (-9)	-6.92%
signed_comparison_inliner_zero	121 (-9)	-6.92%

[asterite]

Apparently this also fixed #8305. I don't know if we'll merge, but I'll add a regression test for that.

[vezenovm]

I now changed it to now to an overflow check if the binary operation was simplified to a constant. I personally think this makes sense, as if we were able to simplify the operation to a constant it means we were able to do it and there's no chance of an overflow, and lhs and rhs aren't needed for this operation anymore.

Yes if we can simplify to a constant there is no chance of an overflow. But that is why I would expect the overflow instructions to also be simplified out upon insertion. If overflow checks are not needed they should be simplified out.

I understand that there might be some things to fix or improve in signed cast operations, but I think we'd still want to avoid doing overflow checks when they aren't needed, right?

The main benefit I see from this vs fixing signed simplifications is that we do not spend any time generating and simplifying instructions for check_overflow in SSA gen. It will avoid doing overflow checks, but only for the initial SSA gen and also leaks our simplifier into SSA gen (e.g. what if the simplifier did not make overflow checks).

This does not fix the issue if later SSA passes simplify a signed binary operation to a constant that does not overflow. Fixing simplification does handle that though.

Now that we have moved away from checking for a constant zero and just a constant result I am ok with this change as it could provide a smaller IR earlier on (although I am not sure about this with fixed signed simplification), it is very little actual extra logic in code gen, and could provide some minor performance benefits. Although keeping this logic contained to the simplifier still provides a better separation of concerns in my opinion as the performance benefit from this change should still be minor and rare.

I have pushed the signed cast fix here #8862 and I contend that this PR is an optimization rather than a fix. I'd like to get other team members thoughts on whether we want this optimization as I don't feel too strongly either way.

[asterite]

Ah, I see now. I couldn't understand what the bug was, but now I understand that constant_uint < integer_modulus didn't work for negative values. I missed that, sorry!

I agree, the other PR is the better way to solve this. I'm curious why the numbers aren't exactly the same in the "Changes to ..." sections, but the differences are minimal.

[vezenovm]

I'm curious why the numbers aren't exactly the same in the "Changes to ..." sections, but the differences are minimal.

I have not investigated but I imagine it is due to further simplifications being made possible by our SSA passes, while in this PR it is only for the initial SSA.