Java: Restrict the output of Range Analysis to the best bounds.

This commit is contained in:
Anders Schack-Mulligen
2019-09-06 13:40:46 +02:00
parent d2336dc8cf
commit 6b85fe087a

View File

@@ -89,7 +89,8 @@ private module RangeAnalysisCache {
*/
cached
predicate bounded(Expr e, Bound b, int delta, boolean upper, Reason reason) {
bounded(e, b, delta, upper, _, _, reason)
bounded(e, b, delta, upper, _, _, reason) and
bestBound(e, b, delta, upper)
}
}
@@ -105,6 +106,17 @@ private module RangeAnalysisCache {
private import RangeAnalysisCache
import RangeAnalysisPublic
/**
* Holds if `b + delta` is a valid bound for `e` and this is the best such delta.
* - `upper = true` : `e <= b + delta`
* - `upper = false` : `e >= b + delta`
*/
private predicate bestBound(Expr e, Bound b, int delta, boolean upper) {
delta = min(int d | bounded(e, b, d, upper, _, _, _)) and upper = true
or
delta = max(int d | bounded(e, b, d, upper, _, _, _)) and upper = false
}
/**
* Holds if `comp` corresponds to:
* - `upper = true` : `v <= e + delta` or `v < e + delta`