Shared/Java: Introduce a shared control flow reachability library and replace the Java Nullness implementation.

shared/controlflow/codeql/controlflow/Guards.qll

@@ -208,6 +208,11 @@ module Make<
 
   private newtype TGuardValue =
     TValue(TAbstractSingleValue val, Boolean isVal) or
+    TIntRange(int bound, Boolean upper) {
+      exists(ConstantExpr c | c.asIntegerValue() + [-1, 0, 1] = bound) and
+      bound != 2147483647 and
+      bound != -2147483648
+    } or
     TException(Boolean throws)
 
   private class AbstractSingleValue extends TAbstractSingleValue {
@@ -238,6 +243,15 @@ module Make<
         result = TValue(val, isVal.booleanNot())
       )
       or
+      exists(int bound, int d, boolean upper |
+        upper = true and d = 1
+        or
+        upper = false and d = -1
+      |
+        this = TIntRange(bound, pragma[only_bind_into](upper)) and
+        result = TIntRange(bound + d, pragma[only_bind_into](upper.booleanNot()))
+      )
+      or
       exists(boolean throws |
         this = TException(throws) and
         result = TException(throws.booleanNot())
@@ -262,6 +276,14 @@ module Make<
     /** Gets the constant that this value represents, if any. */
     ConstantValue asConstantValue() { this = TValue(TValueConstant(result), true) }
 
+    /**
+     * Holds if this value represents an integer range.
+     *
+     * If `upper = true` the range is `(-infinity, bound]`.
+     * If `upper = false` the range is `[bound, infinity)`.
+     */
+    predicate isIntRange(int bound, boolean upper) { this = TIntRange(bound, upper) }
+
     /** Holds if this value represents throwing an exception. */
     predicate isThrowsException() { this = TException(true) }
 
@@ -275,6 +297,12 @@ module Make<
         this = TValue(val, false) and result = "not " + val.toString()
       )
       or
+      exists(int bound |
+        this = TIntRange(bound, true) and result = "Upper bound " + bound.toString()
+        or
+        this = TIntRange(bound, false) and result = "Lower bound " + bound.toString()
+      )
+      or
       exists(boolean throws | this = TException(throws) |
         throws = true and result = "exception"
         or
@@ -293,6 +321,24 @@ module Make<
       b = TValue(b1, true) and
       a1 != b1
     )
+    or
+    exists(int upperbound, int lowerbound |
+      a = TIntRange(upperbound, true) and b = TIntRange(lowerbound, false)
+      or
+      b = TIntRange(upperbound, true) and a = TIntRange(lowerbound, false)
+    |
+      upperbound < lowerbound
+    )
+    or
+    exists(int bound, boolean upper, int k |
+      a = TIntRange(bound, upper) and b.asIntValue() = k
+      or
+      b = TIntRange(bound, upper) and a.asIntValue() = k
+    |
+      upper = true and bound < k
+      or
+      upper = false and bound > k
+    )
   }
 
   private predicate constantHasValue(ConstantExpr c, GuardValue v) {
@@ -681,18 +727,6 @@ module Make<
       )
     }
 
-    /** Holds if `e` may take the value `k` */
-    private predicate relevantInt(Expr e, int k) {
-      e.(ConstantExpr).asIntegerValue() = k
-      or
-      relevantInt(any(Expr e1 | valueStep(e1, e)), k)
-      or
-      exists(SsaDefinition def |
-        guardReadsSsaVar(e, def) and
-        relevantInt(getAnUltimateDefinition(def, _).(SsaWriteDefinition).getDefinition(), k)
-      )
-    }
-
     private predicate impliesStep1(Guard g1, GuardValue v1, Guard g2, GuardValue v2) {
       baseImpliesStep(g1, v1, g2, v2)
       or
@@ -705,14 +739,9 @@ module Make<
         not g2.directlyValueControls(g1.getBasicBlock(), v2)
       )
       or
-      exists(int k1, int k2, boolean upper |
-        rangeGuard(g1, v1, g2, k1, upper) and
-        relevantInt(g2, k2) and
-        v2 = TValue(TValueInt(k2), false)
-      |
-        upper = true and k1 < k2 // g2 <= k1 < k2  ==>  g2 != k2
-        or
-        upper = false and k1 > k2 // g2 >= k1 > k2  ==>  g2 != k2
+      exists(int k, boolean upper |
+        rangeGuard(g1, v1, g2, k, upper) and
+        v2 = TIntRange(k, upper)
       )
       or
       exists(boolean isNull |