Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
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!
- Loading branch information