Merge pull request #1890 from aschackmull/java/best-bound-rangeanalysis

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

Author: yh-semmle

java/ql/src/semmle/code/java/dataflow/RangeAnalysis.qll

@@ -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`