Skip to content

Commit

Permalink
Improve handling of JumpBound truncation constraints
Browse files Browse the repository at this point in the history
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!
  • Loading branch information
staslyakhov committed Jul 23, 2024
1 parent 83d3907 commit a8d039b
Showing 1 changed file with 15 additions and 2 deletions.
17 changes: 15 additions & 2 deletions base/src/Data/Macaw/AbsDomain/JumpBounds.hs
Original file line number Diff line number Diff line change
Expand Up @@ -386,8 +386,21 @@ 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, 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
truncUnsigned :: Natural -> Natural
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
Expand Down

0 comments on commit a8d039b

Please sign in to comment.