C#: Remove FPs from cs/dereferenced-value-may-be-null

Apply a conservative approach by filtering out results for accesses to
captured nullable values, when there is an (implicit) call to the capturing
callable which is `null`-guarded. For example:

```
bool M(int? i, IEnumerable<int> @is)
{
    if (i.HasValue)
        return @is.Any(j => j == i.Value); // GOOD
    return false;
}
```

Author: hvitved

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

@@ -31,6 +31,18 @@ class Guard extends Expr {
   predicate controlsNode(ControlFlow::Nodes::ElementNode cfn, AccessOrCallExpr sub, AbstractValue v) {
     isGuardedByNode(cfn, this, sub, v)
   }
+
+  /**
+   * Holds if `cfn` is guarded by this expression having value `v`.
+   *
+   * Note: This predicate is inlined.
+   */
+  pragma[inline]
+  predicate controlsNode(ControlFlow::Nodes::ElementNode cfn, AbstractValue v) {
+    guardControls(this, cfn.getBasicBlock(), v)
+    or
+    guardAssertionControlsNode(this, cfn, v)
+  }
 }
 
 /** An abstract value. */
@@ -920,34 +932,6 @@ module Internal {
     e = any(BinaryArithmeticOperation bao | result = bao.getAnOperand())
   }
 
-  /** Holds if basic block `bb` only is reached when guard `g` has abstract value `v`. */
-  private predicate guardControls(Guard g, BasicBlock bb, AbstractValue v) {
-    exists(ControlFlowElement cfe, ConditionalSuccessor s, AbstractValue v0, Guard g0 |
-      cfe.controlsBlock(bb, s)
-    |
-      v0.branch(cfe, s, g0) and
-      impliesSteps(g0, v0, g, v)
-    )
-  }
-
-  /**
-   * Holds if control flow node `cfn` only is reached when guard `g` evaluates to `v`,
-   * because of an assertion.
-   */
-  private predicate guardAssertionControlsNode(Guard g, ControlFlow::Node cfn, AbstractValue v) {
-    exists(Assertion a, Guard g0, AbstractValue v0 |
-      asserts(a, g0, v0) and
-      impliesSteps(g0, v0, g, v)
-    |
-      a.strictlyDominates(cfn.getBasicBlock())
-      or
-      exists(BasicBlock bb, int i, int j | bb.getNode(i) = a.getAControlFlowNode() |
-        bb.getNode(j) = cfn and
-        j > i
-      )
-    )
-  }
-
   /**
    * Holds if control flow element `cfe` only is reached when guard `g` evaluates to `v`,
    * because of an assertion.
@@ -1685,6 +1669,36 @@ module Internal {
           adjacentReadPairSameVarUniquePredecessor(mc.getQualifier(), e)
         )
       }
+
+      /** Holds if basic block `bb` only is reached when guard `g` has abstract value `v`. */
+      cached
+      predicate guardControls(Guard g, BasicBlock bb, AbstractValue v) {
+        exists(ControlFlowElement cfe, ConditionalSuccessor s, AbstractValue v0, Guard g0 |
+          cfe.controlsBlock(bb, s)
+        |
+          v0.branch(cfe, s, g0) and
+          impliesSteps(g0, v0, g, v)
+        )
+      }
+
+      /**
+       * Holds if control flow node `cfn` only is reached when guard `g` evaluates to `v`,
+       * because of an assertion.
+       */
+      cached
+      predicate guardAssertionControlsNode(Guard g, ControlFlow::Node cfn, AbstractValue v) {
+        exists(Assertion a, Guard g0, AbstractValue v0 |
+          asserts(a, g0, v0) and
+          impliesSteps(g0, v0, g, v)
+        |
+          a.strictlyDominates(cfn.getBasicBlock())
+          or
+          exists(BasicBlock bb, int i, int j | bb.getNode(i) = a.getAControlFlowNode() |
+            bb.getNode(j) = cfn and
+            j > i
+          )
+        )
+      }
     }
 
     import CachedWithCFG

csharp/ql/src/semmle/code/csharp/dataflow/Nullness.qll

@@ -181,6 +181,19 @@ private predicate isMaybeNullArgument(Ssa::ExplicitDefinition def, MaybeNullExpr
   )
 }
 
+/**
+ * Holds if `edef` is an implicit entry definition for a captured variable that
+ * may be guarded, because a call to the capturing callable is guarded.
+ */
+private predicate isMaybeGuardedCapturedDef(Ssa::ImplicitEntryDefinition edef) {
+  exists(Ssa::ExplicitDefinition def, ControlFlow::Nodes::ElementNode c, G::Guard g, NullValue nv |
+    def.isCapturedVariableDefinitionFlowIn(edef, c, _) and
+    g = def.getARead() and
+    g.controlsNode(c, nv) and
+    nv.isNonNull()
+  )
+}
+
 /** Holds if `def` is an SSA definition that may be `null`. */
 private predicate defMaybeNull(Ssa::Definition def, string msg, Element reason) {
   // A variable compared to `null` might be `null`
@@ -215,6 +228,7 @@ private predicate defMaybeNull(Ssa::Definition def, string msg, Element reason)
   exists(Dereference d | dereferenceAt(_, _, def, d) |
     d.hasNullableType() and
     not def instanceof Ssa::PseudoDefinition and
+    not isMaybeGuardedCapturedDef(def) and
     reason = def.getSourceVariable().getAssignable() and
     msg = "because it has a nullable type"
   )

csharp/ql/test/query-tests/Nullness/E.cs

@@ -371,14 +371,14 @@ static bool Ex34(int? i, IEnumerable<int> @is)
     static bool Ex35(int? i, IEnumerable<int> @is)
     {
         if (i.HasValue)
-            return @is.Any(j => j == i.Value); // GOOD (FALSE POSITIVE)
+            return @is.Any(j => j == i.Value); // GOOD
         return false;
     }
 
     static bool Ex36(int? i, IEnumerable<int> @is)
     {
         if (i.HasValue)
-            @is = @is.Where(j => j == i.Value); // BAD (always)
+            @is = @is.Where(j => j == i.Value); // BAD (always, false negative)
         i = null;
         return @is.Any();
     }

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

@@ -353,10 +353,6 @@ nodes
 | E.cs:349:9:349:9 | access to local variable x |
 | E.cs:368:24:368:40 | SSA capture def(i) |
 | E.cs:368:34:368:34 | access to parameter i |
-| E.cs:374:28:374:44 | SSA capture def(i) |
-| E.cs:374:38:374:38 | access to parameter i |
-| E.cs:381:29:381:45 | SSA capture def(i) |
-| E.cs:381:39:381:39 | access to parameter i |
 | Forwarding.cs:7:16:7:23 | SSA def(s) |
 | Forwarding.cs:14:9:17:9 | if (...) ... |
 | Forwarding.cs:19:9:22:9 | if (...) ... |
@@ -689,8 +685,6 @@ edges
 | E.cs:342:13:342:32 | SSA def(x) | E.cs:343:9:343:9 | access to local variable x |
 | E.cs:348:17:348:36 | SSA def(x) | E.cs:349:9:349:9 | access to local variable x |
 | E.cs:368:24:368:40 | SSA capture def(i) | E.cs:368:34:368:34 | access to parameter i |
-| E.cs:374:28:374:44 | SSA capture def(i) | E.cs:374:38:374:38 | access to parameter i |
-| E.cs:381:29:381:45 | SSA capture def(i) | E.cs:381:39:381:39 | access to parameter i |
 | Forwarding.cs:7:16:7:23 | SSA def(s) | Forwarding.cs:14:9:17:9 | if (...) ... |
 | Forwarding.cs:14:9:17:9 | if (...) ... | Forwarding.cs:19:9:22:9 | if (...) ... |
 | Forwarding.cs:19:9:22:9 | if (...) ... | Forwarding.cs:24:9:27:9 | if (...) ... |
@@ -792,8 +786,6 @@ edges
 | E.cs:343:9:343:9 | access to local variable x | E.cs:342:13:342:32 | SSA def(x) | E.cs:343:9:343:9 | access to local variable x | Variable $@ may be null here because of $@ assignment. | E.cs:342:13:342:13 | x | x | E.cs:342:13:342:32 | String x = ... | this |
 | E.cs:349:9:349:9 | access to local variable x | E.cs:348:17:348:36 | SSA def(x) | E.cs:349:9:349:9 | access to local variable x | Variable $@ may be null here because of $@ assignment. | E.cs:348:17:348:17 | x | x | E.cs:348:17:348:36 | dynamic x = ... | this |
 | E.cs:368:34:368:34 | access to parameter i | E.cs:368:24:368:40 | SSA capture def(i) | E.cs:368:34:368:34 | access to parameter i | Variable $@ may be null here because it has a nullable type. | E.cs:366:27:366:27 | i | i | E.cs:366:27:366:27 | i | this |
-| E.cs:374:38:374:38 | access to parameter i | E.cs:374:28:374:44 | SSA capture def(i) | E.cs:374:38:374:38 | access to parameter i | Variable $@ may be null here because it has a nullable type. | E.cs:371:27:371:27 | i | i | E.cs:371:27:371:27 | i | this |
-| E.cs:381:39:381:39 | access to parameter i | E.cs:381:29:381:45 | SSA capture def(i) | E.cs:381:39:381:39 | access to parameter i | Variable $@ may be null here because it has a nullable type. | E.cs:378:27:378:27 | i | i | E.cs:378:27:378:27 | i | this |
 | GuardedString.cs:35:31:35:31 | access to local variable s | GuardedString.cs:7:16:7:32 | SSA def(s) | GuardedString.cs:35:31:35:31 | access to local variable s | Variable $@ may be null here because of $@ assignment. | GuardedString.cs:7:16:7:16 | s | s | GuardedString.cs:7:16:7:32 | String s = ... | this |
 | NullMaybeBad.cs:7:27:7:27 | access to parameter o | NullMaybeBad.cs:13:17:13:20 | null | NullMaybeBad.cs:7:27:7:27 | access to parameter o | Variable $@ may be null here because of $@ null argument. | NullMaybeBad.cs:5:25:5:25 | o | o | NullMaybeBad.cs:13:17:13:20 | null | this |
 | StringConcatenation.cs:16:17:16:17 | access to local variable s | StringConcatenation.cs:14:16:14:23 | SSA def(s) | StringConcatenation.cs:16:17:16:17 | access to local variable s | Variable $@ may be null here because of $@ assignment. | StringConcatenation.cs:14:16:14:16 | s | s | StringConcatenation.cs:14:16:14:23 | String s = ... | this |