Skip to content

Commit

Permalink
fixup! Improve handling of JumpBound truncation constraints
Browse files Browse the repository at this point in the history
  • Loading branch information
staslyakhov committed Jul 23, 2024
1 parent 17d3d9b commit a36c57e
Showing 1 changed file with 6 additions and 4 deletions.
10 changes: 6 additions & 4 deletions base/src/Data/Macaw/AbsDomain/JumpBounds.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit a36c57e

Please sign in to comment.