fix[venom]: guard sdiv/smod range eval at sign boundary#5093
Open
banteg wants to merge 2 commits into
Open
Conversation
HodanPlodky
approved these changes
Jun 16, 2026
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## master #5093 +/- ##
=======================================
Coverage 92.93% 92.93%
=======================================
Files 188 188
Lines 27840 27845 +5
Branches 4831 4833 +2
=======================================
+ Hits 25874 25879 +5
Misses 1315 1315
Partials 651 651 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
|
|
||
| def test_smod_dividend_spanning_sign_boundary(): | ||
| """ | ||
| Bug: smod narrowed based on raw lo/hi signs for ranges crossing the |
Member
There was a problem hiding this comment.
are there any venom optimization passes which were previously unsound but are sound after this PR? i would like to see those tests
Contributor
Author
There was a problem hiding this comment.
Added optimizer-level coverage in d8e60d8. The new AssertEliminationPass tests cover both sdiv and smod: %x = and source, 2**256 - 32 creates a range that includes the signed word -32, and the pass must not remove assert (sgt result, -1). Validated with uv run --python 3.12 -m pytest tests/unit/venom/test_assert_elimination.py tests/unit/venom/test_variable_range_analysis.py -q, black check, and git diff --check.
Gas ChangesNo changes detected. Summary
|
📊 Bytecode Size Changes (venom)
Full bytecode sizes
|
HodanPlodky
approved these changes
Jun 18, 2026
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
3 participants
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.
What I did
Fixes #5045.
The Venom variable-range domain can represent intervals like
[0, 2**256 - 32]whose members aboveSIGNED_MAXare negative EVM words under signed interpretation.eval_sdivandeval_smodreasoned about sign from rawlo/hi, so e.g.smod([0, 2**256 - 32], 10)folded to[0, 9]even though the member2**256 - 32(signed-32) yields-2(2**256 - 2as a word) — outside the claimed range.How I did it
Both evaluators now guard ranges extending above
SIGNED_MAX, using the same boundary idiomeval_saralready has:eval_sdivbails toValueRange.top(), andeval_smodfalls back to the magnitude bound[-(|d|-1), |d|-1], which is sound for any dividend word (it is the same result the existing spans-zero branch returns, sosmod(TOP, d)keeps its precision). Constant-dividend paths are unaffected (literals are normalized to signed representation before evaluation). Siblings audited:eval_saralready guarded;eval_andis tracked separately in #5012.While auditing, one further candidate surfaced for a follow-up: the signed compare folding (
slt/sgt) ineval_comparereasons from rawlo/hiwith nohi > SIGNED_MAXguard — not touched here to keep the diff scoped.How to verify it
Four new analysis-level tests (per the
test_eval_byte.pyconvention) cover spanning and entirely-above-boundary dividend ranges for both opcodes; all fail on master (e.g. smod returned[0, 9]). Fulltests/unit/venom/andtests/unit/compiler/venom/pass.Commit message
Description for the changelog
Fix: Venom range analysis no longer makes unsound sign-based claims for
sdiv/smodwhen the dividend range crosses the signed boundary.Cute Animal Picture