Java: Improve guards for equal ssa variables.

java/ql/src/semmle/code/java/controlflow/Guards.qll

@@ -97,6 +97,16 @@ class Guard extends ExprParent {
     result = this.(SwitchCase).getSwitchExpr().getEnclosingStmt()
   }
 
+  /**
+   * Gets the basic block containing this guard or the basic block containing
+   * the switch expression if the guard is a switch case.
+   */
+  BasicBlock getBasicBlock() {
+    result = this.(Expr).getBasicBlock() or
+    result = this.(SwitchCase).getSwitch().getExpr().getProperExpr().getBasicBlock() or
+    result = this.(SwitchCase).getSwitchExpr().getExpr().getProperExpr().getBasicBlock()
+  }
+
   /**
    * Holds if this guard is an equality test between `e1` and `e2`. The test
    * can be either `==`, `!=`, `.equals`, or a switch case. If the test is

java/ql/src/semmle/code/java/controlflow/internal/GuardsLogic.qll

@@ -107,7 +107,7 @@ predicate implies_v2(Guard g1, boolean b1, Guard g2, boolean b2) {
     uniqueValue(v, e, k) and
     guardImpliesEqual(g1, b1, v, k) and
     g2.directlyControls(e.getBasicBlock(), b2) and
-    not g2.directlyControls(getBasicBlockOfGuard(g1), b2)
+    not g2.directlyControls(g1.getBasicBlock(), b2)
   )
 }
 
@@ -271,16 +271,24 @@ private predicate uniqueValue(SsaVariable v, Expr e, AbstractValue k) {
   )
 }
 
+/**
+ * Holds if `v1` and `v2` have the same value in `bb`.
+ */
+private predicate equalVarsInBlock(BasicBlock bb, SsaVariable v1, SsaVariable v2) {
+  exists(Guard guard, boolean branch |
+    guard.isEquality(v1.getAUse(), v2.getAUse(), branch) and
+    guardControls_v1(guard, bb, branch)
+  )
+}
+
 /**
  * Holds if `guard` evaluating to `branch` implies that `v` equals `k`.
  */
 private predicate guardImpliesEqual(Guard guard, boolean branch, SsaVariable v, AbstractValue k) {
-  guard.isEquality(v.getAUse(), k.getExpr(), branch)
-}
-
-private BasicBlock getBasicBlockOfGuard(Guard g) {
-  result = g.(Expr).getControlFlowNode().getBasicBlock() or
-  result = g.(SwitchCase).getSwitch().getExpr().getProperExpr().getControlFlowNode().getBasicBlock()
+  exists(SsaVariable v0 |
+    guard.isEquality(v0.getAUse(), k.getExpr(), branch) and
+    (v = v0 or equalVarsInBlock(guard.getBasicBlock(), v0, v))
+  )
 }
 
 private ControlFlowNode getAGuardBranchSuccessor(Guard g, boolean branch) {
@@ -299,7 +307,7 @@ private predicate guardControlsPhiBranch(
   guard.directlyControls(upd.getBasicBlock(), branch) and
   upd.getDefiningExpr().(VariableAssign).getSource().getProperExpr() = e and
   upd = phi.getAPhiInput() and
-  getBasicBlockOfGuard(guard).bbStrictlyDominates(phi.getBasicBlock())
+  guard.getBasicBlock().bbStrictlyDominates(phi.getBasicBlock())
 }
 
 /**
@@ -326,7 +334,7 @@ private predicate conditionalAssign(SsaVariable v, Guard guard, boolean branch,
     forall(SsaVariable other | other != upd and other = phi.getAPhiInput() |
       guard.directlyControls(other.getBasicBlock(), branch.booleanNot())
       or
-      other.getBasicBlock().bbDominates(getBasicBlockOfGuard(guard)) and
+      other.getBasicBlock().bbDominates(guard.getBasicBlock()) and
       not other.isLiveAtEndOfBlock(getAGuardBranchSuccessor(guard, branch))
     )
   )
@@ -341,6 +349,11 @@ private predicate conditionalAssignVal(SsaVariable v, Guard guard, boolean branc
 
 private predicate relevantEq(SsaVariable v, AbstractValue val) {
   conditionalAssignVal(v, _, _, val)
+  or
+  exists(SsaVariable v0 |
+    conditionalAssignVal(v0, _, _, val) and
+    equalVarsInBlock(_, v0, v)
+  )
 }
 
 /**
@@ -349,16 +362,19 @@ private predicate relevantEq(SsaVariable v, AbstractValue val) {
 private predicate guardImpliesNotEqual1(
   Guard guard, boolean branch, SsaVariable v, AbstractValue val
 ) {
-  relevantEq(v, val) and
-  (
-    guard.isEquality(v.getAUse(), val.getExpr(), branch.booleanNot())
-    or
-    exists(AbstractValue val2 |
-      guard.isEquality(v.getAUse(), val2.getExpr(), branch) and
-      val != val2
-    )
-    or
-    guard.(InstanceOfExpr).getExpr() = sameValue(v, _) and branch = true and val = TAbsValNull()
+  exists(SsaVariable v0 |
+    relevantEq(v0, val) and
+    (
+      guard.isEquality(v0.getAUse(), val.getExpr(), branch.booleanNot())
+      or
+      exists(AbstractValue val2 |
+        guard.isEquality(v0.getAUse(), val2.getExpr(), branch) and
+        val != val2
+      )
+      or
+      guard.(InstanceOfExpr).getExpr() = sameValue(v0, _) and branch = true and val = TAbsValNull()
+    ) and
+    (v = v0 or equalVarsInBlock(guard.getBasicBlock(), v0, v))
   )
 }
 
@@ -368,13 +384,16 @@ private predicate guardImpliesNotEqual1(
 private predicate guardImpliesNotEqual2(
   Guard guard, boolean branch, SsaVariable v, AbstractValue val
 ) {
-  relevantEq(v, val) and
-  (
-    guard = directNullGuard(v, branch, false) and val = TAbsValNull()
-    or
-    exists(int k |
-      guard = integerGuard(v.getAUse(), branch, k, false) and
-      val = TAbsValInt(k)
-    )
+  exists(SsaVariable v0 |
+    relevantEq(v0, val) and
+    (
+      guard = directNullGuard(v0, branch, false) and val = TAbsValNull()
+      or
+      exists(int k |
+        guard = integerGuard(v0.getAUse(), branch, k, false) and
+        val = TAbsValInt(k)
+      )
+    ) and
+    (v = v0 or equalVarsInBlock(guard.getBasicBlock(), v0, v))
   )
 }

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

@@ -101,7 +101,7 @@ public class B {
     if (alen == blen) {
       for(int i = 0; i < alen; i++) {
         sum += a[i]; // OK
-        sum += b[i]; // NPE - false positive
+        sum += b[i]; // OK
       }
     }
     int alen2;

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

@@ -12,7 +12,6 @@
 | B.java:72:15:72:16 | xs | Variable $@ may be null here because of $@ assignment. | B.java:68:5:68:41 | int[] xs | xs | B.java:68:11:68:40 | xs | this |
 | B.java:75:20:75:21 | xs | Variable $@ may be null here because of $@ assignment. | B.java:68:5:68:41 | int[] xs | xs | B.java:68:11:68:40 | xs | this |
 | B.java:78:20:78:21 | xs | Variable $@ may be null here because of $@ assignment. | B.java:68:5:68:41 | int[] xs | xs | B.java:68:11:68:40 | xs | this |
-| B.java:104:16:104:16 | b | Variable $@ may be null here as suggested by $@ null guard. | B.java:97:36:97:42 | b | b | B.java:99:16:99:24 | ... == ... | this |
 | B.java:118:5:118:7 | obj | Variable $@ may be null here as suggested by $@ null guard. | B.java:117:27:117:36 | obj | obj | B.java:119:13:119:23 | ... != ... | this |
 | B.java:133:5:133:7 | obj | Variable $@ may be null here because of $@ assignment. | B.java:128:5:128:22 | Object obj | obj | B.java:128:12:128:21 | obj | this |
 | B.java:190:7:190:7 | o | Variable $@ may be null here because of $@ assignment. | B.java:178:5:178:20 | Object o | o | B.java:186:5:186:12 | ...=... | this |