Draft
Conversation
Codecov Report❌ Patch coverage is Additional details and impacted files@@ Coverage Diff @@
## master #4824 +/- ##
==========================================
- Coverage 92.89% 92.85% -0.04%
==========================================
Files 155 155
Lines 21744 21829 +85
Branches 3885 3901 +16
==========================================
+ Hits 20199 20270 +71
- Misses 1024 1037 +13
- Partials 521 522 +1 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
- Fix mem_ssa.py: Restore correct direction for completely_contains check. For a store to 'clobber' (provide data for) a load, the store's location must completely contain the load's location (not vice versa). - Fix _range_excludes_zero: Add explicit is_top check for clarity and safety. While the implicit handling happened to be correct, explicit check is more defensive against future changes. - Document _narrow_nonzero: Add docstring explaining the limitation that ranges spanning zero cannot be precisely narrowed due to contiguous range representation.
Add evaluators for data source instructions (param, calldataload, sload, mload, etc.) that return [0, SIGNED_MAX] range instead of TOP. This enables the range analysis to narrow values after iszero checks, which in turn allows the branch optimizer to fold redundant branches. Key insight: By knowing that function parameters and loaded values are in [0, SIGNED_MAX], after an assertion like `assert a > 0`, the analysis can narrow `a` to [1, SIGNED_MAX]. Subsequent `if a > 0` checks are then known to be always true and can be folded to unconditional jumps. Also adds evaluators for: - Environment instructions (timestamp, number, etc.) - Address-returning instructions (caller, origin, etc.) - Boolean-returning instructions (call success flags) - Hash instructions (sha3, extcodehash) Update algebraic optimization tests to reflect that some comparisons against extreme values are now folded to constants by range analysis.
Hash functions (sha3, extcodehash) produce arbitrary 256-bit values that span both positive and negative ranges in signed interpretation. Return TOP instead of [0, UNSIGNED_MAX] because: 1. [0, UNSIGNED_MAX] can't be meaningfully narrowed after iszero checks 2. Range-based optimizations on hash values are rare anyway
CRITICAL SOUNDNESS FIX: The _eval_unsigned_full function was returning [0, SIGNED_MAX] for sload, calldataload, mload, param, etc. This caused MISCOMPILATION when these instructions return values >= 2^255. Bug scenario: 1. sload returns 0xFFFF...FFFF (-1 signed, MAX_UINT unsigned) 2. Analysis claims value is in [0, SIGNED_MAX] - WRONG 3. After iszero-false branch, narrows to [1, SIGNED_MAX] - STILL WRONG 4. sgt(x, 0) incorrectly folds to constant 1 5. But sgt(-1, 0) = 0 at runtime! This could cause assertions to be eliminated, branches to be folded incorrectly, and other miscompilation issues. Fix: Return TOP for all instructions that can return any 256-bit value. This is a soundness requirement, not a precision tradeoff.
The comments incorrectly stated that 'source' returns [0, SIGNED_MAX]. After the soundness fix, 'source' returns TOP (full uint256 range). Updated comments to accurately describe what the tests are verifying: algebraic transformations rather than range-based folding.
…locks When BranchOptimizationPass folds a jnz to jmp (branch folding based on range analysis), the unreachable target block becomes dead. Without a subsequent SimplifyCFGPass, this dead block causes assertion failures in later passes like venom_to_assembly. Add SimplifyCFGPass after the second BranchOptimizationPass in both O2 and Os optimization levels.
The parser reverses operands for most opcodes, so for 'lt %a, %b': - operands[-1] = %a (left side of comparison in source) - operands[-2] = %b (right side of comparison in source) The evaluator was using the wrong operand order, causing 'gt 5, 0' to evaluate to 0 instead of 1. Fixed by correctly mapping operands to left/right sides of the comparison.
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
2 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
How I did it
How to verify it
Commit message
Commit message for the final, squashed PR. (Optional, but reviewers will appreciate it! Please see our commit message style guide for what we would ideally like to see in a commit message.)
Description for the changelog
Cute Animal Picture