Repository navigation
Verify the absence of overflow in checked integer arithmetic - #280
Merged
Merged
Conversation
With overflow checks on, rustc lowers `+`, `-` and `*` on integers to AddWithOverflow/SubWithOverflow/MulWithOverflow followed by an assertion on the overflow flag, and these fell through to unimplemented!. They now evaluate to the pair of the mathematical result and whether it lies outside the operand type's range, so the existing Assert handling turns each overflow check into a verification condition. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01MvvhC4sHsobSMHAn9CgLBq
AddWithOverflow and friends evaluate to the wrapped result paired with the overflow flag, so the first field is now wrapped into the operand type's range instead of relying on rustc reading it only after the overflow assertion. Also drop the SubWithOverflow test pair; one pair covers the checked operations. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01MvvhC4sHsobSMHAn9CgLBq
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01MvvhC4sHsobSMHAn9CgLBq
…tjmb6h-checked-arith
Term::pow2 is gone from main, so int_term_in_range builds its bounds the way wrap_int_term does. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01MvvhC4sHsobSMHAn9CgLBq
coord-e
marked this pull request as ready for review
September 28, 2026 08:50
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
Contributor
There was a problem hiding this comment.
Copilot review overview
🟡 Changes recommended
The regression pair can succeed for the wrong reason and leaves subtraction, multiplication, and unsigned behavior untested.
Review effort: Balanced
Findings: 5
Open (5)
What changed in this PR
Adds verification for overflow-checked integer addition, subtraction, and multiplication.
Changes:
- Models wrapped results and overflow flags.
- Uses analyzer-local MIR declarations.
- Adds an
i64overflow UI-test pair.
| File | Description |
|---|---|
src/analyze/basic_block.rs |
Implements checked arithmetic modeling. |
tests/ui/pass/int_overflow_checked.rs |
Adds passing overflow-check coverage. |
tests/ui/fail/int_overflow_checked.rs |
Adds expected-failure coverage. |
💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.
Update assertions for succ_below_max function. Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com>
Update assertions in main to test edge cases. Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This is the first stage of the fix for the arithmetic-overflow issue found while reviewing #278.
With overflow checks on, rustc lowers integer
+/-/*toAddWithOverflow/SubWithOverflow/MulWithOverflowfollowed by anasserton the overflow flag. Thrust hitunimplemented!on these operations, which is why every UI test is compiled with-C debug-assertions=off.Changes
AddWithOverflow/SubWithOverflow/MulWithOverflownow evaluate to the pair(wrapped result, overflowed), matching rustc's definition ("both the wrapped result and a bool indicating whether it overflowed"):overflowedis true exactly when the mathematical result lies outside that range.Asserthandling then turns each overflow check into a verification condition, so a program that can overflow is rejected.Analyzer::local_decls.body.local_declsdoes not include the temporaries thatReborrowVisitoradds.Tests
int_overflow_checked, compiled with-C overflow-checks=on: ani64x + 1guarded againsti64::MAX. The fail side has the guard off by one.On
main, the pair stops atnot implemented: ty=int, op=AddWithOverflow.cargo testfails on exactly the same set of tests asmain(65 PCSat tests: the localcoar:mainimage can't handle(Seq Int)). fmt andclippy -D warningsare clean.Not covered (next stage)
u32parameter is non-negative, so a guard is needed on both sides of a value unless the inferred precondition already bounds it.🤖 Generated with Claude Code
https://claude.ai/code/session_01MvvhC4sHsobSMHAn9CgLBq