From 17d3d9b8cad21cc313656ee85514d3ac574c5aba Mon Sep 17 00:00:00 2001 From: Stanislav Lyakhov Date: Tue, 23 Jul 2024 12:50:08 -0700 Subject: [PATCH] Improve handling of JumpBound truncation constraints Given some symbolic value, @x@, we'd like to compute its possible upper and lower bounds after it is truncated to @w@ bits. To do this, we first find the bound of x by (recursively) calling `exprRangePred`. This bound is a statement of the following form (see `RangePred` for more info): "r bits of x are bounded between @low@ and @high@". Then, we check the following: - If x has a bound (r, l, w) AND - If r is less than or equal to w => Pass-through the bound (r, l, w) Otherwise, we deem x "unbounded" Declaring x unbounded in the second case seems to throw away useful information that causes many jump tables to remain unclassified. We attempt to improve on that in this commit. Consider an example where x is bounded by (64, 0, 10) (that is, the 64 bits of x are constrained to be between 0 and 10) and we want to find the bound of truncating x to 8 bits. With the current logic, since 64 > 8, we'd declare x unbounded. However, the bound (8, 0, 10) should also be valid: if 64 bits of x are bounded to [0, 10], then surely 8 bits of x also lie between 0 and 10. If the upper bound is instead larger than the largest 8-bit value, we can truncate it to the largest value. For example, (64, 0, 10000) becomes (8, 0, 255). Instead of losing the bound completely, we're able to tighten it! --- base/src/Data/Macaw/AbsDomain/JumpBounds.hs | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) 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