C#: Add field access for out/ref assignments in the CFG.

Author: michaelnebel

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

@@ -430,6 +430,7 @@ module Expressions {
       not this instanceof ArrayCreation and
       not this instanceof QualifiedWriteAccess and
       not this instanceof QualifiedAccessorWrite and
+      not this instanceof QualifiedWriteAccessOutRef and
       not this instanceof NoNodeExpr and
       not this instanceof SwitchExpr and
       not this instanceof SwitchCaseExpr and
@@ -491,6 +492,86 @@ module Expressions {
     }
   }
 
+  /**
+   * An expression that writes via an accessor in an out/ref parameter, for example `s = M(out x.Field)`,
+   * where `Field` is a field.
+   *
+   * Accessor writes need special attention, because we need to model that the
+   * access is written after the method call.
+   *
+   * In the example above, this means we want a CFG that looks like
+   *
+   * ```csharp
+   * x -> call M -> x.Field -> s = M(out x.Field)
+   * ```
+   */
+  private class QualifiedWriteAccessOutRef extends PostOrderTree instanceof Expr {
+    final override predicate propagatesAbnormal(AstNode child) { child = getExprChild(this, _) }
+
+    QualifiedWriteAccessOutRef() {
+      exists(AssignableDefinitions::OutRefDefinition def |
+        def.getExpr() = this and
+        def.getTargetAccess() instanceof QualifiableExpr
+      )
+    }
+
+    final override predicate first(AstNode first) {
+      first(getExprChild(this, 0), first)
+      or
+      not exists(getExprChild(this, 0)) and
+      first = this
+    }
+
+    private QualifiableExpr getOutRefAccess(int i) {
+      result =
+        rank[i + 1](AssignableDefinitions::OutRefDefinition def |
+          def.getExpr() = this and
+          def.getTargetAccess() instanceof QualifiableExpr
+        |
+          def order by def.getIndex()
+        ).getTargetAccess()
+    }
+
+    private QualifiableExpr getLastOutRefAccess() {
+      exists(int last |
+        result = this.getOutRefAccess(last) and
+        not exists(this.getOutRefAccess(last + 1))
+      )
+    }
+
+    final override predicate last(AstNode last, Completion c) {
+      last = this.getLastOutRefAccess() and
+      c.isValidFor(last)
+    }
+
+    final override predicate succ(AstNode pred, AstNode succ, Completion c) {
+      exists(int i |
+        last(getExprChild(this, i), pred, c) and
+        c instanceof NormalCompletion
+      |
+        // Post-order: flow from last element of last child to element itself
+        i = max(int j | exists(getExprChild(this, j))) and
+        succ = this
+        or
+        // Standard left-to-right evaluation
+        first(getExprChild(this, i + 1), succ)
+      )
+      or
+      // Flow from this element to the first write access.
+      pred = this and
+      succ = this.getOutRefAccess(0) and
+      c.isValidFor(pred) and
+      c instanceof NormalCompletion
+      or
+      // Flow from one access to the next
+      exists(int i | pred = this.getOutRefAccess(i) |
+        succ = this.getOutRefAccess(i + 1) and
+        c.isValidFor(pred) and
+        c instanceof NormalCompletion
+      )
+    }
+  }
+
   /**
    * An expression that writes via an accessor, for example `x.Prop = 0`,
    * where `Prop` is a property.
@@ -516,6 +597,7 @@ module Expressions {
     QualifiedAccessorWrite() {
       def.getExpr() = this and
       def.getTargetAccess().(WriteAccess) instanceof QualifiableExpr and
+      not def instanceof AssignableDefinitions::OutRefDefinition and
       not this instanceof AssignOperationWithExpandedAssignment
     }