Java: Refactor integerGuard.

java/ql/lib/semmle/code/java/dataflow/IntegerGuards.qll

@@ -32,6 +32,58 @@ class IntComparableExpr extends Expr {
   }
 }
 
+/**
+ * Holds if `comp` evaluating to `branch` ensures that `e1` is less than `e2`.
+ * When `strict` is true, `e1` is strictly less than `e2`, otherwise it is less
+ * than or equal to `e2`.
+ */
+private predicate comparison(ComparisonExpr comp, boolean branch, Expr e1, Expr e2, boolean strict) {
+  branch = true and
+  e1 = comp.getLesserOperand() and
+  e2 = comp.getGreaterOperand() and
+  (if comp.isStrict() then strict = true else strict = false)
+  or
+  branch = false and
+  e1 = comp.getGreaterOperand() and
+  e2 = comp.getLesserOperand() and
+  (if comp.isStrict() then strict = false else strict = true)
+}
+
+/**
+ * Holds if `guard` evaluating to `branch` ensures that:
+ * `e <= k` when `upper = true`
+ * `e >= k` when `upper = false`
+ */
+pragma[nomagic]
+predicate rangeGuard(Expr guard, boolean branch, Expr e, int k, boolean upper) {
+  exists(EqualityTest eqtest, Expr c |
+    eqtest = guard and
+    eqtest.hasOperands(e, c) and
+    bounded(c, any(ZeroBound zb), k, upper, _) and
+    branch = eqtest.polarity()
+  )
+  or
+  exists(Expr c, int val, boolean strict, int d |
+    bounded(c, any(ZeroBound zb), val, upper, _) and
+    (
+      upper = true and
+      comparison(guard, branch, e, c, strict) and
+      d = -1
+      or
+      upper = false and
+      comparison(guard, branch, c, e, strict) and
+      d = 1
+    ) and
+    (
+      strict = false and k = val
+      or
+      // e < c <= val ==> e <= c - 1 <= val - 1
+      // e > c >= val ==> e >= c + 1 >= val + 1
+      strict = true and k = val + d
+    )
+  )
+}
+
 /**
  * An expression that directly tests whether a given expression is equal to `k` or not.
  * The set of `k`s is restricted to those that are relevant for the expression or
@@ -53,75 +105,14 @@ Expr integerGuard(IntComparableExpr e, boolean branch, int k, boolean is_k) {
     )
   )
   or
-  exists(EqualityTest eqtest, int val, Expr c, boolean upper |
+  exists(int val, boolean upper |
+    rangeGuard(result, branch, e, val, upper) and
     k = e.relevantInt() and
-    eqtest = result and
-    eqtest.hasOperands(e, c) and
-    bounded(c, any(ZeroBound zb), val, upper, _) and
-    is_k = false and
-    (
-      upper = true and val < k
-      or
-      upper = false and val > k
-    ) and
-    branch = eqtest.polarity()
-  )
-  or
-  exists(ComparisonExpr comp, Expr c, int val, boolean upper |
-    k = e.relevantInt() and
-    comp = result and
-    comp.hasOperands(e, c) and
-    bounded(c, any(ZeroBound zb), val, upper, _) and
     is_k = false
   |
-    // k <= val <= c < e, so e != k
-    comp.getLesserOperand() = c and
-    comp.isStrict() and
-    branch = true and
-    val >= k and
-    upper = false
+    upper = true and val < k // e <= val < k  ==>  e != k
     or
-    comp.getLesserOperand() = c and
-    comp.isStrict() and
-    branch = false and
-    val < k and
-    upper = true
-    or
-    comp.getLesserOperand() = c and
-    not comp.isStrict() and
-    branch = true and
-    val > k and
-    upper = false
-    or
-    comp.getLesserOperand() = c and
-    not comp.isStrict() and
-    branch = false and
-    val <= k and
-    upper = true
-    or
-    comp.getGreaterOperand() = c and
-    comp.isStrict() and
-    branch = true and
-    val <= k and
-    upper = true
-    or
-    comp.getGreaterOperand() = c and
-    comp.isStrict() and
-    branch = false and
-    val > k and
-    upper = false
-    or
-    comp.getGreaterOperand() = c and
-    not comp.isStrict() and
-    branch = true and
-    val < k and
-    upper = true
-    or
-    comp.getGreaterOperand() = c and
-    not comp.isStrict() and
-    branch = false and
-    val >= k and
-    upper = false
+    upper = false and val > k // e >= val > k  ==>  e != k
   )
 }