C#: Add CFG support for null conditional assignments and include eg. …

csharp/ql/lib/semmle/code/csharp/controlflow/internal/ControlFlowGraphImpl.qll

@@ -429,7 +429,8 @@ module Expressions {
       not this instanceof ObjectCreation and
       not this instanceof ArrayCreation and
       not this instanceof QualifiedWriteAccess and
-      not this instanceof AccessorWrite and
+      not this instanceof QualifiedAccessorWrite and
+      not this instanceof QualifiedAssignments and
       not this instanceof NoNodeExpr and
       not this instanceof SwitchExpr and
       not this instanceof SwitchCaseExpr and
@@ -481,14 +482,17 @@ module Expressions {
     }
   }
 
-  private class StatOrDynAccessorCall_ =
-    @dynamic_member_access_expr or @dynamic_element_access_expr or @call_access_expr;
+  private class QualifiedExprOrStatOrDynAccessorCall_ =
+    @dynamic_member_access_expr or @dynamic_element_access_expr or @call_access_expr or
+        @qualifiable_expr;
 
   /** A normal or a (potential) dynamic call to an accessor. */
-  private class StatOrDynAccessorCall extends Expr, StatOrDynAccessorCall_ { }
+  private class QualifiedExprOrStatOrDynAccessorCall extends Expr,
+    QualifiedExprOrStatOrDynAccessorCall_
+  { }
 
   /**
-   * An expression that writes via an accessor call, for example `x.Prop = 0`,
+   * An expression that writes via an accessor, for example `x.Prop = 0`,
    * where `Prop` is a property.
    *
    * Accessor writes need special attention, because we need to model the fact
@@ -498,24 +502,32 @@ module Expressions {
    * ```csharp
    * x -> 0 -> set_Prop -> x.Prop = 0
    * ```
+   *
+   * For consistency, control flow is implemented this way for all accessor writes.
+   * For example, `x.Field = 0`, where `Field` is a field, we want a CFG that looks like
+   *
+   * ```csharp
+   * x -> 0 -> x.Field -> x.Field = 0
+   * ```
    */
-  class AccessorWrite extends PostOrderTree instanceof Expr {
+  private class QualifiedAccessorWrite extends PostOrderTree instanceof Expr {
     AssignableDefinition def;
 
-    AccessorWrite() {
+    QualifiedAccessorWrite() {
       def.getExpr() = this and
-      def.getTargetAccess().(WriteAccess) instanceof StatOrDynAccessorCall and
+      def.getTargetAccess().(WriteAccess) instanceof QualifiedExprOrStatOrDynAccessorCall and
       not this instanceof AssignOperationWithExpandedAssignment
     }
 
     /**
      * Gets the `i`th accessor being called in this write. More than one call
      * can happen in tuple assignments.
      */
-    StatOrDynAccessorCall getCall(int i) {
+    QualifiedExprOrStatOrDynAccessorCall getAccess(int i) {
       result =
         rank[i + 1](AssignableDefinitions::TupleAssignmentDefinition tdef |
-          tdef.getExpr() = this and tdef.getTargetAccess() instanceof StatOrDynAccessorCall
+          tdef.getExpr() = this and
+          tdef.getTargetAccess() instanceof QualifiedExprOrStatOrDynAccessorCall
         |
           tdef order by tdef.getEvaluationOrder()
         ).getTargetAccess()
@@ -528,7 +540,13 @@ module Expressions {
     final override predicate propagatesAbnormal(AstNode child) {
       child = getExprChild(this, _)
       or
-      child = this.getCall(_)
+      child = this.getAccess(_)
+    }
+
+    final override predicate last(AstNode last, Completion c) {
+      PostOrderTree.super.last(last, c)
+      or
+      last(getExprChild(this, 0), last, c) and c.(NullnessCompletion).isNull()
     }
 
     final override predicate first(AstNode first) { first(getExprChild(this, 0), first) }
@@ -538,31 +556,69 @@ module Expressions {
       exists(int i |
         last(getExprChild(this, i), pred, c) and
         c instanceof NormalCompletion and
+        (i != 0 or not c.(NullnessCompletion).isNull()) and
         first(getExprChild(this, i + 1), succ)
       )
       or
       // Flow from last element of last child to first accessor call
       last(getLastExprChild(this), pred, c) and
-      succ = this.getCall(0) and
+      succ = this.getAccess(0) and
       c instanceof NormalCompletion
       or
       // Flow from one call to the next
-      exists(int i | pred = this.getCall(i) |
-        succ = this.getCall(i + 1) and
+      exists(int i | pred = this.getAccess(i) |
+        succ = this.getAccess(i + 1) and
         c.isValidFor(pred) and
         c instanceof NormalCompletion
       )
       or
       // Post-order: flow from last call to element itself
-      exists(int last | last = max(int i | exists(this.getCall(i))) |
-        pred = this.getCall(last) and
+      exists(int last | last = max(int i | exists(this.getAccess(i))) |
+        pred = this.getAccess(last) and
         succ = this and
         c.isValidFor(pred) and
         c instanceof NormalCompletion
       )
     }
   }
 
+  /**
+   * An assignment where the left hand side is a qualified write access.
+   *
+   * This is needed to allow "null" completion to propagate from the qualifier
+   * to after the assignment.
+   */
+  private class QualifiedAssignments extends PostOrderTree instanceof Assignment {
+    QualifiedAccessorWrite left;
+    Expr right;
+
+    QualifiedAssignments() {
+      left = this.getLValue() and
+      right = this.getRValue() and
+      not this instanceof AssignOperationWithExpandedAssignment
+    }
+
+    final override predicate propagatesAbnormal(AstNode child) { child = [left, right] }
+
+    final override predicate first(AstNode first) { first(left, first) }
+
+    final override predicate last(AstNode last, Completion c) {
+      PostOrderTree.super.last(last, c)
+      or
+      last(left, last, c) and
+      left.(QualifiableExpr).isConditional() and
+      c.(NullnessCompletion).isNull()
+    }
+
+    final override predicate succ(AstNode pred, AstNode succ, Completion c) {
+      // Standard left-to-right evaluation
+      last(left, pred, c) and
+      c instanceof NormalCompletion and
+      not c.(NullnessCompletion).isNull() and
+      first(right, succ)
+    }
+  }
+
   private class LogicalNotExprTree extends PostOrderTree instanceof LogicalNotExpr {
     private Expr operand;
 
@@ -704,7 +760,9 @@ module Expressions {
   private class ConditionallyQualifiedExpr extends PostOrderTree instanceof QualifiableExpr {
     private Expr qualifier;
 
-    ConditionallyQualifiedExpr() { this.isConditional() and qualifier = getExprChild(this, 0) }
+    ConditionallyQualifiedExpr() {
+      this.isConditional() and qualifier = getExprChild(this, 0) and not this instanceof WriteAccess
+    }
 
     final override predicate propagatesAbnormal(AstNode child) { child = qualifier }