diff --git a/base/src/Data/Macaw/AbsDomain/JumpBounds.hs b/base/src/Data/Macaw/AbsDomain/JumpBounds.hs index e4134514..d15cd1d3 100644 --- a/base/src/Data/Macaw/AbsDomain/JumpBounds.hs +++ b/base/src/Data/Macaw/AbsDomain/JumpBounds.hs @@ -388,11 +388,13 @@ exprRangePred info e = do -- of bits, then we just pass it through. -> case testLeq (rangeWidth r) w of Just LeqProof -> SomeRangePred r - - -- Otherwise, our bound remains valid for the truncated number - -- of bits and we can tighten the bounds to at most @2^w-1@ (inclusive) + + -- Otherwise, we need to rewrite the constraints to be on w bits. + -- We can do that by clamping the lower/upper bounds if they're + -- outside of the range [0, 2^w-1]. Nothing -> - let + let + truncUnsigned :: Natural -> Natural truncUnsigned = fromInteger . unsignedClamp w . toInteger lowerBound = truncUnsigned $ rangeLowerBound r upperBound = truncUnsigned $ rangeUpperBound r