C#: Update nullness analyses

Port the SSA-based logic from the Java nullness analyses.

Author: hvitved

csharp/ql/src/CSI/NullAlways.qhelp

@@ -2,13 +2,39 @@
   "-//Semmle//qhelp//EN"
   "qhelp.dtd">
 <qhelp>
+
+
 <overview>
-<p>If a variable is dereferenced, and the variable has a null value on all possible execution paths 
-leading to the dereferencing, it is guaranteed to result in a <code>NullReferenceException</code>.
+<p>If a variable is dereferenced, and the variable has a <code>null</code>
+value on all possible execution paths leading to the dereferencing, the dereferencing is
+guaranteed to result in a <code>NullReferenceException</code>.
 </p>
 
 </overview>
 <recommendation>
-<p>Examine the code to check for possible errors.</p>
+
+<p>Ensure that the variable does not have a <code>null</code> value when it is dereferenced.
+</p>
+
 </recommendation>
+<example>
+<p>
+In the following examples, the condition <code>s.Length > 0</code> is only
+executed if <code>s</code> is <code>null</code>.
+</p>
+
+<sample src="NullAlwaysBad.cs" />
+
+<p>
+In the revised example, the condition is guarded correctly by using <code>&amp;&amp;</code> instead of
+<code>||</code>.
+</p>
+
+<sample src="NullAlwaysGood.cs" />
+</example>
+<references>
+
+  <li>Microsoft, <a href="https://docs.microsoft.com/en-us/dotnet/api/system.nullreferenceexception">NullReferenceException Class</a>.</li>
+
+</references>
 </qhelp>

csharp/ql/src/CSI/NullAlways.ql

@@ -1,9 +1,9 @@
 /**
  * @name Dereferenced variable is always null
- * @description Finds uses of a variable that may cause a NullPointerException
+ * @description Dereferencing a variable whose value is 'null' causes a 'NullReferenceException'.
  * @kind problem
  * @problem.severity error
- * @precision medium
+ * @precision very-high
  * @id cs/dereferenced-value-is-always-null
  * @tags reliability
  *       correctness
@@ -14,6 +14,6 @@
 import csharp
 import semmle.code.csharp.dataflow.Nullness
 
-from VariableAccess access, LocalVariable var
-where access = unguardedNullDereference(var)
-select access, "Variable $@ is always null here.", var, var.getName()
+from Dereference d, Ssa::SourceVariable v
+where d.isFirstAlwaysNull(v)
+select d, "Variable '$@' is always null here.", v, v.toString()

csharp/ql/src/CSI/NullAlwaysBad.cs

@@ -0,0 +1,13 @@
+using System;
+
+namespace NullAlways
+{
+    class Bad
+    {
+        void DoPrint(string s)
+        {
+            if (s != null || s.Length > 0)
+                Console.WriteLine(s);
+        }
+    }
+}

csharp/ql/src/CSI/NullAlwaysGood.cs

@@ -0,0 +1,13 @@
+using System;
+
+namespace NullAlways
+{
+    class Good
+    {
+        void DoPrint(string s)
+        {
+            if (s != null && s.Length > 0)
+                Console.WriteLine(s);
+        }
+    }
+}

csharp/ql/src/CSI/NullMaybe.qhelp

@@ -2,13 +2,41 @@
   "-//Semmle//qhelp//EN"
   "qhelp.dtd">
 <qhelp>
+
+
 <overview>
-<p>If a variable is dereferenced, and the variable may have a null value on some execution paths 
-leading to the dereferencing, the dereferencing may result in a <code>NullReferenceException</code>.
+<p>If a variable is dereferenced, and the variable may have a <code>null</code>
+value on some execution paths leading to the dereferencing, the dereferencing
+may result in a <code>NullReferenceException</code>.
 </p>
 
 </overview>
 <recommendation>
-<p>Examine the code to check for possible errors.</p>
+
+<p>Ensure that the variable does not have a <code>null</code> value when it is dereferenced.
+</p>
+
 </recommendation>
+<example>
+<p>
+In the following example, the method <code>DoPrint()</code> dereferences its parameter
+<code>o</code> unconditionally, resulting in a <code>NullReferenceException</code> via
+the call <code>DoPrint(null)</code>.
+</p>
+
+<sample src="NullMaybeBad.cs" />
+
+<p>
+In the revised example, the method <code>DoPrint()</code> guards the dereferencing with
+a <code>null</code> check.
+</p>
+
+<sample src="NullMaybeGood.cs" />
+
+</example>
+<references>
+
+  <li>Microsoft, <a href="https://docs.microsoft.com/en-us/dotnet/api/system.nullreferenceexception">NullReferenceException Class</a>.</li>
+
+</references>
 </qhelp>

csharp/ql/src/CSI/NullMaybe.ql

@@ -1,9 +1,10 @@
 /**
  * @name Dereferenced variable may be null
- * @description Finds uses of a variable that may cause a NullPointerException
+ * @description Dereferencing a variable whose value may be 'null' may cause a
+ *              'NullReferenceException'.
  * @kind problem
  * @problem.severity warning
- * @precision medium
+ * @precision high
  * @id cs/dereferenced-value-may-be-null
  * @tags reliability
  *       correctness
@@ -14,8 +15,6 @@
 import csharp
 import semmle.code.csharp.dataflow.Nullness
 
-from VariableAccess access, LocalVariable var
-where access = unguardedMaybeNullDereference(var)
-// do not flag definite nulls here; these are already flagged by NullAlways.ql
-and not access = unguardedNullDereference(var)
-select access, "Variable $@ may be null here.", var, var.getName()
+from Dereference d, Ssa::SourceVariable v, string msg, Element reason
+where d.isFirstMaybeNull(v.getAnSsaDefinition(), msg, reason)
+select d, "Variable '$@' may be null here " + msg + ".", v, v.toString(), reason, "this"

csharp/ql/src/CSI/NullMaybeBad.cs

@@ -0,0 +1,15 @@
+using System;
+
+class Bad
+{
+    void DoPrint(object o)
+    {
+        Console.WriteLine(o.ToString());
+    }
+
+    void M()
+    {
+        DoPrint("Hello");
+        DoPrint(null);
+    }
+}

csharp/ql/src/CSI/NullMaybeGood.cs

@@ -0,0 +1,16 @@
+using System;
+
+class Good
+{
+    void DoPrint(object o)
+    {
+        if (o != null)
+            Console.WriteLine(o.ToString());
+    }
+
+    void M()
+    {
+        DoPrint("Hello");
+        DoPrint(null);
+    }
+}

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

@@ -112,19 +112,28 @@ private import AbstractValues
  * an expression that may evaluate to `null`.
  */
 class DereferenceableExpr extends Expr {
+  private boolean isNullableType;
+
   DereferenceableExpr() {
     exists(Expr e, Type t |
       // There is currently a bug in the extractor: the type of `x?.Length` is
       // incorrectly `int`, while it should have been `int?`. We apply
       // `getNullEquivParent()` as a workaround
       this = getNullEquivParent*(e) and
       t = e.getType() |
-      t instanceof NullableType
+      t instanceof NullableType and
+      isNullableType = true
       or
-      t instanceof RefType
+      t instanceof RefType and
+      isNullableType = false
     )
   }
 
+  /** Holds if this expression has a nullable type `T?`. */
+  predicate hasNullableType() {
+    isNullableType = true
+  }
+
   /**
    * Gets an expression that directly tests whether this expression is `null`.
    *
@@ -177,9 +186,22 @@ class DereferenceableExpr extends Expr {
         if ie.(IsConstantExpr).getConstant() instanceof NullLiteral then
           // E.g. `x is null`
           isNull = branch
-        else
+        else (
           // E.g. `x is string` or `x is ""`
-          (branch = true and isNull = false)
+          branch = true and isNull = false
+          or
+          // E.g. `x is string` where `x` has type `string`
+          ie = any(IsTypeExpr ite | ite.getCheckedType() = ite.getExpr().getType()) and
+          branch = false and
+          isNull = true
+        ) 
+      )
+      or
+      this.hasNullableType() and
+      result = any(PropertyAccess pa |
+        pa.getQualifier() = this and
+        pa.getTarget().hasName("HasValue") and
+        if branch = true then isNull = false else isNull = true
       )
       or
       isCustomNullCheck(result, this, v, isNull)
@@ -307,19 +329,23 @@ class AccessOrCallExpr extends Expr {
 }
 
 private Declaration getDeclarationTarget(Expr e) {
-  e = any(AssignableRead ar | result = ar.getTarget()) or
+  e = any(AssignableAccess aa | result = aa.getTarget()) or
   result = e.(Call).getTarget()
 }
 
 private Ssa::Definition getAnSsaQualifier(Expr e) {
-  e = getATrackedRead(result)
+  e = getATrackedAccess(result)
   or
-  not e = getATrackedRead(_) and
+  not e = getATrackedAccess(_) and
   result = getAnSsaQualifier(e.(QualifiableExpr).getQualifier())
 }
 
-private AssignableRead getATrackedRead(Ssa::Definition def) {
-  result = def.getARead() and
+private AssignableAccess getATrackedAccess(Ssa::Definition def) {
+  (
+    result = def.getARead()
+    or
+    result = def.(Ssa::ExplicitDefinition).getADefinition().getTargetAccess()
+  ) and
   not def instanceof Ssa::ImplicitUntrackedDefinition
 }
 
@@ -384,6 +410,15 @@ class GuardedExpr extends AccessOrCallExpr {
     v = v0
   }
 
+  /**
+   * Holds if this expression must have abstract value `v`. That is, this
+   * expression is guarded by a structurally equal expression having abstract
+   * value `v`.
+   */
+  predicate mustHaveValue(AbstractValue v) {
+    exists(Expr e | e = this.getAGuard(e, v))
+  }
+
   /**
    * Holds if this expression is guarded by expression `cond`, which must
    * evaluate to `b`. The expression `sub` is a sub expression of `cond`
@@ -401,7 +436,7 @@ class GuardedExpr extends AccessOrCallExpr {
 /** An expression guarded by a `null` check. */
 class NullGuardedExpr extends GuardedExpr {
   NullGuardedExpr() {
-    exists(Expr e, NullValue v | e = this.getAGuard(e, v) | not v.isNull())
+    this.mustHaveValue(any(NullValue v | not v.isNull()))
   }
 }
 
@@ -420,11 +455,28 @@ module Internal {
 
   /** Holds if expression `e` is a non-`null` value. */
   predicate nonNullValue(Expr e) {
-    e.stripCasts() = any(Expr s | s.hasValue() and not s instanceof NullLiteral)
+    e instanceof ObjectCreation
+    or
+    e instanceof ArrayCreation
+    or
+    e.hasValue() and
+    not e instanceof NullLiteral
+    or
+    e instanceof ThisAccess
+    or
+    e instanceof AddExpr and
+    e.getType() instanceof StringType
+  }
+
+  /** Holds if expression `e2` is a non-`null` value whenever `e1` is. */
+  predicate nonNullValueImplied(Expr e1, Expr e2) {
+    e1 = e2.(CastExpr).getExpr()
+    or
+    e1 = e2.(AssignExpr).getRValue()
   }
 
   /**
-   * Gets the parent expression of `e` which is `null` only if `e` is `null`,
+   * Gets the parent expression of `e` which is `null` iff `e` is `null`,
    * if any. For example, `result = x?.y` and `e = x`, or `result = x + 1`
    * and `e = x`.
    */
@@ -433,6 +485,8 @@ module Internal {
       qe.getQualifier() = e and
       qe.isConditional() and
       (
+        // The accessed declaration must have a value type in order
+        // for `only if` to hold
         result.(FieldAccess).getTarget().getType() instanceof ValueType
         or
         result.(Call).getTarget().getReturnType() instanceof ValueType
@@ -444,11 +498,28 @@ module Internal {
       result = bao and
       bao.getAnOperand() = e and
       bao.getAnOperand() = o and
+      // The other operand must be provably non-null in order
+      // for `only if` to hold
       nonNullValue(o) and
       e != o
     )
   }
 
+  /**
+   * Gets a child expression of `e` which is `null` only if `e` is `null`.
+   */
+  Expr getANullImplyingChild(Expr e) {
+    e = any(QualifiableExpr qe |
+      qe.isConditional() and
+      result = qe.getQualifier()
+    )
+    or
+    // In C#, `null + 1` has type `int?` with value `null`
+    e = any(BinaryArithmeticOperation bao |
+      result = bao.getAnOperand()
+    )
+  }
+
   /** An expression whose value may control the execution of another element. */
   class Guard extends Expr {
     private AbstractValue val;
@@ -785,6 +856,23 @@ module Internal {
       v1 instanceof NullValue and
       v2 = v1
       or
+      g1 instanceof DereferenceableExpr and
+      g2 = getANullImplyingChild(g1) and
+      v1 = any(NullValue nv | not nv.isNull()) and
+      v2 = v1
+      or
+      g2 = g1.(AssignExpr).getRValue() and
+      v1 = g1.getAValue() and
+      v2 = v1
+      or
+      g2 = g1.(Assignment).getLValue() and
+      v1 = g1.getAValue() and
+      v2 = v1
+      or
+      g2 = g1.(CastExpr).getExpr() and
+      v1 = g1.getAValue() and
+      v2 = v1.(NullValue)
+      or
       exists(PreSsa::Definition def |
         def.getDefinition().getSource() = g2 |
         g1 = def.getARead() and