fix[venom]: guard sdiv/smod range eval at sign boundary

tests/unit/venom/test_assert_elimination.py

@@ -1,4 +1,5 @@
 from tests.venom_utils import PrePostChecker
+from vyper.venom.analysis.variable_range.value_range import UNSIGNED_MAX
 from vyper.venom.passes.assert_elimination import AssertEliminationPass
 from vyper.venom.passes.remove_unused_variables import RemoveUnusedVariablesPass
 
@@ -28,3 +29,26 @@ def test_remove_overflow_assert():
     """
 
     _check_pre_post(pre, post)
+
+
+def _check_signed_division_assert_kept(opcode):
+    mask = UNSIGNED_MAX - 31  # includes the signed word -32
+    pre = f"""
+    main:
+        %input = source
+        %x = and %input, {mask}
+        %result = {opcode} %x, 10
+        %ok = sgt %result, -1
+        assert %ok
+        sink %result
+    """
+
+    _check_pre_post(pre, pre)
+
+
+def test_keep_sdiv_sign_boundary_assert():
+    _check_signed_division_assert_kept("sdiv")
+
+
+def test_keep_smod_sign_boundary_assert():
+    _check_signed_division_assert_kept("smod")

tests/unit/venom/test_variable_range_analysis.py

@@ -2,7 +2,8 @@
 
 from vyper.venom.analysis import IRAnalysesCache
 from vyper.venom.analysis.variable_range import VariableRangeAnalysis
-from vyper.venom.analysis.variable_range.value_range import SIGNED_MAX, SIGNED_MIN
+from vyper.venom.analysis.variable_range.evaluators import eval_sdiv, eval_smod
+from vyper.venom.analysis.variable_range.value_range import SIGNED_MAX, SIGNED_MIN, ValueRange
 from vyper.venom.parser import parse_venom
 
 
@@ -2248,3 +2249,44 @@ def test_smod_by_zero():
     smod_inst = next(inst for inst in entry.instructions if inst.opcode == "smod")
     rng = analysis.get_range(smod_inst.output, entry.instructions[-1])
     assert rng.lo == 0 and rng.hi == 0
+
+
+def test_smod_dividend_spanning_sign_boundary():
+    """
+    Bug: smod narrowed based on raw lo/hi signs for ranges crossing the
+    signed boundary. [0, 2**256 - 32] contains the word 2**256 - 32, which
+    is -32 in signed interpretation. smod(-32, 10) = -2 (the word
+    2**256 - 2), which the old result [0, 9] excluded.
+    """
+    dividend = ValueRange.iv(0, 2**256 - 32)
+    rng = eval_smod(dividend, ValueRange.constant(10))
+    # the result must include -2 (the word 2**256 - 2)
+    assert rng.is_top or rng.lo <= -2 <= rng.hi, f"-2 excluded from {rng}"
+    assert rng.lo == -9 and rng.hi == 9
+
+
+def test_sdiv_dividend_spanning_sign_boundary_is_top():
+    """
+    Bug: sdiv narrowed based on raw lo/hi signs for ranges crossing the
+    signed boundary. [0, 2**256 - 32] contains the word 2**256 - 32, which
+    is -32 in signed interpretation. sdiv(-32, 10) = -3 (the word
+    2**256 - 3), which the old result [0, (2**256 - 32) // 10] excluded.
+    """
+    dividend = ValueRange.iv(0, 2**256 - 32)
+    rng = eval_sdiv(dividend, ValueRange.constant(10))
+    assert rng.is_top
+
+
+def test_smod_dividend_above_signed_max():
+    """A dividend range entirely above SIGNED_MAX is all negative words."""
+    dividend = ValueRange.iv(SIGNED_MAX + 1, 2**256 - 32)
+    rng = eval_smod(dividend, ValueRange.constant(10))
+    # all dividend words are negative; -2 must be included
+    assert rng.lo <= -2 <= rng.hi, f"-2 excluded from {rng}"
+
+
+def test_sdiv_dividend_above_signed_max_is_top():
+    """A dividend range entirely above SIGNED_MAX is all negative words."""
+    dividend = ValueRange.iv(SIGNED_MAX + 1, 2**256 - 32)
+    rng = eval_sdiv(dividend, ValueRange.constant(10))
+    assert rng.is_top

vyper/venom/analysis/variable_range/evaluators.py

@@ -358,6 +358,12 @@ def eval_sdiv(dividend: ValueRange, divisor: ValueRange) -> ValueRange:
         result = sign * (abs(dv) // abs(d))
         return ValueRange.constant(result)
 
+    # Ranges extending above SIGNED_MAX contain values that are negative
+    # words in the signed interpretation, so the sign reasoning on raw
+    # lo/hi below would be unsound.
+    if dividend.hi > SIGNED_MAX:
+        return ValueRange.top()
+
     # For ranges, compute bounds
     # Division by positive divisor preserves order: lo/d <= x/d <= hi/d
     # Division by negative divisor reverses order: hi/d <= x/d <= lo/d
@@ -400,6 +406,13 @@ def eval_smod(dividend: ValueRange, divisor: ValueRange) -> ValueRange:
         return ValueRange.constant(0)
     limit = abs(d) - 1
 
+    # Ranges extending above SIGNED_MAX contain values that are negative
+    # words in the signed interpretation, so the sign-based narrowing
+    # below would be unsound. The magnitude bound still holds for any
+    # dividend.
+    if dividend.hi > SIGNED_MAX:
+        return ValueRange.iv(-limit, limit)
+
     # Result sign follows dividend sign, so we can narrow based on dividend range
     if dividend.lo >= 0:
         # Dividend is non-negative, result is non-negative