diff --git a/base/src/Data/Macaw/AbsDomain/JumpBounds.hs b/base/src/Data/Macaw/AbsDomain/JumpBounds.hs index 84dd4ce3..e4134514 100644 --- a/base/src/Data/Macaw/AbsDomain/JumpBounds.hs +++ b/base/src/Data/Macaw/AbsDomain/JumpBounds.hs @@ -386,8 +386,18 @@ exprRangePred info e = do -- Compare the range constraint with the output number of bits. -- If the bound on r covers at most the truncated number -- of bits, then we just pass it through. - , Just LeqProof <- testLeq (rangeWidth r) w -> - SomeRangePred r + -> 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) + Nothing -> + let + truncUnsigned = fromInteger . unsignedClamp w . toInteger + lowerBound = truncUnsigned $ rangeLowerBound r + upperBound = truncUnsigned $ rangeUpperBound r + in + SomeRangePred (mkRangeBound w lowerBound upperBound) _ -> NoRangePred -- | This returns a natural number with a computed upper bound for the