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

java/ql/lib/semmle/code/java/ControlFlowGraph.qll

@@ -82,6 +82,7 @@ module;
  */
 
 import java
+private import codeql.controlflow.SuccessorType
 private import codeql.util.Boolean
 private import Completion
 private import controlflow.internal.Preconditions
@@ -124,6 +125,28 @@ module ControlFlow {
       result = succ(this, NormalCompletion())
     }
 
+    /** Gets an immediate successor of this node of a given type, if any. */
+    Node getASuccessor(SuccessorType t) {
+      result = branchSuccessor(this, t.(BooleanSuccessor).getValue())
+      or
+      exists(Completion completion |
+        result = succ(this, completion) and
+        not result = branchSuccessor(this, _)
+      |
+        completion = NormalCompletion() and t instanceof DirectSuccessor
+        or
+        completion = ReturnCompletion() and t instanceof ReturnSuccessor
+        or
+        completion = BreakCompletion(_) and t instanceof BreakSuccessor
+        or
+        completion = YieldCompletion(_) and t instanceof BreakSuccessor
+        or
+        completion = ContinueCompletion(_) and t instanceof ContinueSuccessor
+        or
+        completion = ThrowCompletion(_) and t instanceof ExceptionSuccessor
+      )
+    }
+
     /** Gets the basic block that contains this node. */
     BasicBlock getBasicBlock() { result.getANode() = this }
 

java/ql/lib/semmle/code/java/controlflow/BasicBlocks.qll

@@ -22,20 +22,8 @@ private module Input implements BB::InputSig<Location> {
   /** Gets the CFG scope in which this node occurs. */
   CfgScope nodeGetCfgScope(Node node) { node.getEnclosingCallable() = result }
 
-  private Node getASpecificSuccessor(Node node, SuccessorType t) {
-    node.(ConditionNode).getABranchSuccessor(t.(BooleanSuccessor).getValue()) = result
-    or
-    node.getAnExceptionSuccessor() = result and t instanceof ExceptionSuccessor
-  }
-
   /** Gets an immediate successor of this node. */
-  Node nodeGetASuccessor(Node node, SuccessorType t) {
-    result = getASpecificSuccessor(node, t)
-    or
-    node.getASuccessor() = result and
-    t instanceof DirectSuccessor and
-    not result = getASpecificSuccessor(node, _)
-  }
+  Node nodeGetASuccessor(Node node, SuccessorType t) { result = node.getASuccessor(t) }
 
   /**
    * Holds if `node` represents an entry node to be used when calculating

java/ql/lib/semmle/code/java/controlflow/ControlFlow.qll

@@ -0,0 +1,60 @@
+/**
+ * Provides an implementation of local (intraprocedural) control flow reachability.
+ */
+overlay[local?]
+module;
+
+import java
+private import codeql.controlflow.ControlFlow
+private import semmle.code.java.dataflow.SSA as SSA
+private import semmle.code.java.controlflow.Guards as Guards
+
+private module ControlFlowInput implements InputSig<Location, ControlFlowNode, BasicBlock> {
+  private import java as J
+
+  AstNode getEnclosingAstNode(ControlFlowNode node) { node.getAstNode() = result }
+
+  class AstNode = ExprParent;
+
+  AstNode getParent(AstNode node) {
+    result = node.(Expr).getParent() or
+    result = node.(Stmt).getParent()
+  }
+
+  class FinallyBlock extends AstNode {
+    FinallyBlock() { any(TryStmt try).getFinally() = this }
+  }
+
+  class Expr = J::Expr;
+
+  class SourceVariable = SSA::SsaSourceVariable;
+
+  class SsaDefinition = SSA::SsaVariable;
+
+  class SsaWriteDefinition extends SsaDefinition instanceof SSA::SsaExplicitUpdate {
+    Expr getDefinition() {
+      super.getDefiningExpr().(VariableAssign).getSource() = result or
+      super.getDefiningExpr().(AssignOp) = result
+    }
+  }
+
+  class SsaPhiNode = SSA::SsaPhiNode;
+
+  class SsaUncertainDefinition extends SsaDefinition instanceof SSA::SsaUncertainImplicitUpdate {
+    SsaDefinition getPriorDefinition() { result = super.getPriorDef() }
+  }
+
+  class GuardValue = Guards::GuardValue;
+
+  predicate ssaControlsBranchEdge(SsaDefinition def, BasicBlock bb1, BasicBlock bb2, GuardValue v) {
+    Guards::Guards_v3::ssaControlsBranchEdge(def, bb1, bb2, v)
+  }
+
+  predicate ssaControls(SsaDefinition def, BasicBlock bb, GuardValue v) {
+    Guards::Guards_v3::ssaControls(def, bb, v)
+  }
+
+  import Guards::Guards_v3::InternalUtil
+}
+
+module ControlFlow = Make<Location, Cfg, ControlFlowInput>;

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

@@ -45,13 +45,21 @@ private import semmle.code.java.Collections
 private import semmle.code.java.controlflow.internal.Preconditions
 
 /** Gets an expression that may be `null`. */
-Expr nullExpr() {
-  result instanceof NullLiteral or
-  result.(ChooseExpr).getAResultExpr() = nullExpr() or
-  result.(AssignExpr).getSource() = nullExpr() or
-  result.(CastExpr).getExpr() = nullExpr() or
-  result.(ImplicitCastExpr).getExpr() = nullExpr() or
-  result instanceof SafeCastExpr
+Expr nullExpr() { result = nullExpr(_) }
+
+/** Gets an expression that may be `null`. */
+private Expr nullExpr(Expr reason) {
+  result instanceof NullLiteral and reason = result
+  or
+  result.(ChooseExpr).getAResultExpr() = nullExpr(reason)
+  or
+  result.(AssignExpr).getSource() = nullExpr(reason)
+  or
+  result.(CastExpr).getExpr() = nullExpr(reason)
+  or
+  result.(ImplicitCastExpr).getExpr() = nullExpr(reason)
+  or
+  result instanceof SafeCastExpr and reason = result
 }
 
 /** An expression of a boxed type that is implicitly unboxed. */
@@ -174,12 +182,13 @@ private predicate firstVarDereferenceInBlock(BasicBlock bb, SsaVariable v, VarAc
 }
 
 /** A variable suspected of being `null`. */
-private predicate varMaybeNull(SsaVariable v, string msg, Expr reason) {
+private predicate varMaybeNull(SsaVariable v, ControlFlowNode node, string msg, Expr reason) {
   // A variable compared to null might be null.
   exists(Expr e |
     reason = e and
     msg = "as suggested by $@ null guard" and
     guardSuggestsVarMaybeNull(e, v) and
+    node = v.getCfgNode() and
     not v instanceof SsaPhiNode and
     not clearlyNotNull(v) and
     // Comparisons in finally blocks are excluded since missing exception edges in the CFG could otherwise yield FPs.
@@ -195,6 +204,7 @@ private predicate varMaybeNull(SsaVariable v, string msg, Expr reason) {
   // A parameter might be null if there is a null argument somewhere.
   exists(Parameter p, Expr arg |
     v.(SsaImplicitInit).isParameterDefinition(p) and
+    node = v.getCfgNode() and
     p.getAnArgument() = arg and
     reason = arg and
     msg = "because of $@ null argument" and
@@ -205,7 +215,7 @@ private predicate varMaybeNull(SsaVariable v, string msg, Expr reason) {
   // If the source of a variable is null then the variable may be null.
   exists(VariableAssign def |
     v.(SsaExplicitUpdate).getDefiningExpr() = def and
-    def.getSource() = nullExpr() and
+    def.getSource() = nullExpr(node.asExpr()) and
     reason = def and
     msg = "because of $@ assignment"
   )
@@ -299,7 +309,7 @@ private predicate leavingFinally(BasicBlock bb1, BasicBlock bb2, boolean normale
 }
 
 private predicate ssaSourceVarMaybeNull(SsaSourceVariable v) {
-  varMaybeNull(v.getAnSsaVariable(), _, _)
+  varMaybeNull(v.getAnSsaVariable(), _, _, _)
 }
 
 /**
@@ -352,7 +362,7 @@ private predicate nullVarStep(
 private predicate varMaybeNullInBlock(
   SsaVariable ssa, SsaSourceVariable v, BasicBlock bb, boolean storedcompletion
 ) {
-  varMaybeNull(ssa, _, _) and
+  varMaybeNull(ssa, _, _, _) and
   bb = ssa.getBasicBlock() and
   storedcompletion = false and
   v = ssa.getSourceVariable()
@@ -378,7 +388,7 @@ private predicate varMaybeNullInBlock_origin(
   SsaVariable origin, SsaVariable ssa, BasicBlock bb, boolean storedcompletion
 ) {
   nullDerefCandidateVariable(ssa.getSourceVariable()) and
-  varMaybeNull(ssa, _, _) and
+  varMaybeNull(ssa, _, _, _) and
   bb = ssa.getBasicBlock() and
   storedcompletion = false and
   origin = ssa
@@ -546,7 +556,7 @@ private predicate varMaybeNullInBlock_corrCond(
     not varConditionallyNull(ssa, cond1, _) and
     (branch = true or branch = false)
   ) and
-  varMaybeNull(ssa, _, _) and
+  varMaybeNull(ssa, _, _, _) and
   bb = ssa.getBasicBlock() and
   storedcompletion = false and
   origin = ssa
@@ -752,7 +762,7 @@ private predicate varMaybeNullInBlock_trackVar(
       isReset(trackssa, trackvar, kind, init, _)
     )
   ) and
-  varMaybeNull(ssa, _, _) and
+  varMaybeNull(ssa, _, _, _) and
   bb = ssa.getBasicBlock() and
   storedcompletion = false and
   origin = ssa
@@ -804,7 +814,7 @@ private predicate varMaybeNullInBlock_trackVar(
 predicate nullDeref(SsaSourceVariable v, VarAccess va, string msg, Expr reason) {
   exists(SsaVariable origin, SsaVariable ssa, BasicBlock bb |
     nullDerefCandidate(origin, va) and
-    varMaybeNull(origin, msg, reason) and
+    varMaybeNull(origin, _, msg, reason) and
     ssa.getSourceVariable() = v and
     firstVarDereferenceInBlock(bb, ssa, va) and
     forall(ConditionBlock cond | correlatedConditions(v, cond, _, _) |

java/ql/test/query-tests/Nullness/B.java

@@ -515,4 +515,46 @@ public void trackTest(Object o, int n) {
     if (c == 100) { return; }
     o.hashCode(); // NPE
   }
+
+  public void testFinally(int[] xs, int[] ys) {
+    if (xs.length == 0) return;
+    if (ys.length == 0) return;
+    String s1 = null;
+    String s2 = null;
+    for (int x : xs) {
+      try {
+        if (x == 0) { break; }
+        s1 = "1";
+        for (int y : ys) {
+          if (y == 0) { break; }
+          s2 = "2";
+        }
+      } finally {
+      }
+      s1.hashCode(); // OK
+      s2.hashCode(); // NPE
+    }
+    s1.hashCode(); // NPE - false negative, Java CFG lacks proper edge label
+  }
+
+  public void lenCheck(int[] xs, int n, int t) {
+    if (n > 42) return;
+    if (maybe) {}
+    if (n > 0 && (xs == null || xs.length < n)) {
+      return;
+    }
+    if (maybe) {}
+    if (n > 21) return;
+    if (maybe) {}
+    for (int i = 0; i < n; ++i) {
+      xs[i]++; // Spurious NPE - false positive
+    }
+  }
+
+  public void rangetest(int n) {
+    String s = null;
+    if (n < 0 || n > 10) s = "A";
+    if (n > 100) s.hashCode(); // Spurious NPE - false positive
+    if (n == 42) s.hashCode(); // Spurious NPE - false positive
+  }
 }

java/ql/test/query-tests/Nullness/NullMaybe.expected

@@ -22,6 +22,10 @@
 | B.java:465:9:465:9 | x | Variable $@ may be null at this access because of $@ assignment. | B.java:458:5:458:28 | Object x | x | B.java:470:9:470:16 | ...=... | this |
 | B.java:487:9:487:9 | x | Variable $@ may be null at this access because of $@ assignment. | B.java:476:5:476:20 | Object x | x | B.java:476:12:476:19 | x | this |
 | B.java:516:5:516:5 | o | Variable $@ may be null at this access as suggested by $@ null guard. | B.java:511:25:511:32 | o | o | B.java:512:22:512:30 | ... == ... | this |
+| B.java:535:7:535:8 | s2 | Variable $@ may be null at this access because of $@ assignment. | B.java:523:5:523:21 | String s2 | s2 | B.java:523:12:523:20 | s2 | this |
+| B.java:550:7:550:8 | xs | Variable $@ may be null at this access as suggested by $@ null guard. | B.java:540:24:540:31 | xs | xs | B.java:543:19:543:28 | ... == ... | this |
+| B.java:557:18:557:18 | s | Variable $@ may be null at this access because of $@ assignment. | B.java:555:5:555:20 | String s | s | B.java:555:12:555:19 | s | this |
+| B.java:558:18:558:18 | s | Variable $@ may be null at this access because of $@ assignment. | B.java:555:5:555:20 | String s | s | B.java:555:12:555:19 | s | this |
 | C.java:9:44:9:45 | a2 | Variable $@ may be null at this access as suggested by $@ null guard. | C.java:6:5:6:23 | long[][] a2 | a2 | C.java:7:34:7:54 | ... != ... | this |
 | C.java:9:44:9:45 | a2 | Variable $@ may be null at this access because of $@ assignment. | C.java:6:5:6:23 | long[][] a2 | a2 | C.java:6:14:6:22 | a2 | this |
 | C.java:10:17:10:18 | a3 | Variable $@ may be null at this access as suggested by $@ null guard. | C.java:8:5:8:21 | long[] a3 | a3 | C.java:9:38:9:58 | ... != ... | this |