C#: Adopt shared variable capture library

csharp/ql/consistency-queries/DataFlowConsistency.ql

@@ -47,8 +47,6 @@ private module Input implements InputSig<CsharpDataFlow> {
     or
     not exists(LocalFlow::getAPostUpdateNodeForArg(n.getControlFlowNode()))
     or
-    n instanceof ImplicitCapturedArgumentNode
-    or
     n instanceof ParamsArgumentNode
     or
     n.asExpr() instanceof CIL::Expr
@@ -104,8 +102,6 @@ private module Input implements InputSig<CsharpDataFlow> {
         not split = cfn.getASplit()
       )
       or
-      call instanceof TransitiveCapturedDataFlowCall
-      or
       call.(NonDelegateDataFlowCall).getDispatchCall().isReflection()
     )
   }

csharp/ql/consistency-queries/VariableCaptureConsistency.ql

@@ -0,0 +1,17 @@
+import csharp
+import semmle.code.csharp.dataflow.internal.DataFlowPrivate::VariableCapture::Flow::ConsistencyChecks
+private import semmle.code.csharp.dataflow.internal.DataFlowPrivate::VariableCapture::Flow::ConsistencyChecks as ConsistencyChecks
+private import semmle.code.csharp.controlflow.BasicBlocks
+private import semmle.code.csharp.controlflow.internal.ControlFlowGraphImpl
+
+query predicate uniqueEnclosingCallable(BasicBlock bb, string msg) {
+  ConsistencyChecks::uniqueEnclosingCallable(bb, msg) and
+  getNodeCfgScope(bb.getFirstNode()) instanceof Callable
+}
+
+query predicate consistencyOverview(string msg, int n) { none() }
+
+query predicate uniqueCallableLocation(Callable c, string msg) {
+  ConsistencyChecks::uniqueCallableLocation(c, msg) and
+  count(c.getBody()) = 1
+}

csharp/ql/lib/change-notes/2024-02-26-variable-capture-flow.md

@@ -0,0 +1,4 @@
+---
+category: majorAnalysis
+---
+* Improved support for flow through captured variables that properly adheres to inter-procedural control flow.

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

@@ -31,9 +31,52 @@ module PreSsa {
   }
 
   predicate implicitEntryDef(Callable c, SsaInput::BasicBlock bb, SsaInput::SourceVariable v) {
-    not v instanceof LocalScopeVariable and
     c = v.getACallable() and
-    scopeFirst(c, bb)
+    scopeFirst(c, bb) and
+    (
+      not v instanceof LocalScopeVariable
+      or
+      v.(SimpleLocalScopeVariable).isReadonlyCapturedBy(c)
+    )
+  }
+
+  /** Holds if `a` is assigned in callable `c`. */
+  pragma[nomagic]
+  private predicate assignableDefinition(Assignable a, Callable c) {
+    exists(AssignableDefinition def |
+      def.getTarget() = a and
+      c = def.getEnclosingCallable()
+    |
+      not c instanceof Constructor or
+      a instanceof LocalScopeVariable
+    )
+  }
+
+  pragma[nomagic]
+  private predicate assignableUniqueWriter(Assignable a, Callable c) {
+    c = unique(Callable c0 | assignableDefinition(a, c0) | c0)
+  }
+
+  /** Holds if `a` is accessed in callable `c`. */
+  pragma[nomagic]
+  private predicate assignableAccess(Assignable a, Callable c) {
+    exists(AssignableAccess aa | aa.getTarget() = a | c = aa.getEnclosingCallable())
+  }
+
+  /**
+   * A local scope variable that is amenable to SSA analysis.
+   *
+   * This is either a local variable that is not captured, or one
+   * where all writes happen in the defining callable.
+   */
+  class SimpleLocalScopeVariable extends LocalScopeVariable {
+    SimpleLocalScopeVariable() { assignableUniqueWriter(this, this.getCallable()) }
+
+    /** Holds if this local scope variable is read-only captured by `c`. */
+    predicate isReadonlyCapturedBy(Callable c) {
+      assignableAccess(this, c) and
+      c != this.getCallable()
+    }
   }
 
   module SsaInput implements SsaImplCommon::InputSig<Location> {
@@ -47,40 +90,6 @@ module PreSsa {
       ExitBasicBlock() { scopeLast(_, this.getLastElement(), _) }
     }
 
-    /** Holds if `a` is assigned in non-constructor callable `c`. */
-    pragma[nomagic]
-    private predicate assignableDefinition(Assignable a, Callable c) {
-      exists(AssignableDefinition def | def.getTarget() = a |
-        c = def.getEnclosingCallable() and
-        not c instanceof Constructor
-      )
-    }
-
-    /** Holds if `a` is accessed in callable `c`. */
-    pragma[nomagic]
-    private predicate assignableAccess(Assignable a, Callable c) {
-      exists(AssignableAccess aa | aa.getTarget() = a | c = aa.getEnclosingCallable())
-    }
-
-    pragma[nomagic]
-    private predicate assignableNoCapturing(Assignable a, Callable c) {
-      assignableAccess(a, c) and
-      /*
-       * The code below is equivalent to
-       * ```ql
-       * not exists(Callable other | assignableDefinition(a, other) | other != c)
-       * ```
-       * but it avoids a Cartesian product in the compiler generated antijoin
-       * predicate.
-       */
-
-      (
-        not assignableDefinition(a, _)
-        or
-        c = unique(Callable c0 | assignableDefinition(a, c0) | c0)
-      )
-    }
-
     pragma[noinline]
     private predicate assignableNoComplexQualifiers(Assignable a) {
       forall(QualifiableExpr qe | qe.(AssignableAccess).getTarget() = a | qe.targetIsThisInstance())
@@ -94,15 +103,22 @@ module PreSsa {
       private Callable c;
 
       SourceVariable() {
+        assignableAccess(this, c) and
         (
-          this instanceof LocalScopeVariable
+          this instanceof SimpleLocalScopeVariable
           or
-          this = any(Field f | not f.isVolatile())
-          or
-          this = any(TrivialProperty tp | not tp.isOverridableOrImplementable())
-        ) and
-        assignableNoCapturing(this, c) and
-        assignableNoComplexQualifiers(this)
+          (
+            this = any(Field f | not f.isVolatile())
+            or
+            this = any(TrivialProperty tp | not tp.isOverridableOrImplementable())
+          ) and
+          (
+            not assignableDefinition(this, _)
+            or
+            assignableUniqueWriter(this, c)
+          ) and
+          assignableNoComplexQualifiers(this)
+        )
       }
 
       /** Gets a callable in which this simple assignable can be analyzed. */

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

@@ -218,19 +218,6 @@ private predicate isNullDefaultArgument(Ssa::ExplicitDefinition def, AlwaysNullE
   )
 }
 
-/**
- * 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) {
   not nonNullDef(def) and
@@ -268,7 +255,6 @@ private predicate defMaybeNull(Ssa::Definition def, string msg, Element reason)
     exists(Dereference d | dereferenceAt(_, _, def, d) |
       d.hasNullableType() and
       not def instanceof Ssa::PhiNode and
-      not isMaybeGuardedCapturedDef(def) and
       reason = def.getSourceVariable().getAssignable() and
       msg = "because it has a nullable type"
     )
@@ -583,14 +569,8 @@ class Dereference extends G::DereferenceableExpr {
    */
   predicate isAlwaysNull(Ssa::SourceVariable v) {
     this = v.getAnAccess() and
-    // Exclude fields, properties, and captured variables, as they may not have an
-    // accurate SSA representation
-    v.getAssignable() =
-      any(LocalScopeVariable lsv |
-        strictcount(Callable c |
-          c = any(AssignableDefinition ad | ad.getTarget() = lsv).getEnclosingCallable()
-        ) = 1
-      ) and
+    // Exclude fields and properties, as they may not have an accurate SSA representation
+    v.getAssignable() instanceof LocalScopeVariable and
     (
       forex(Ssa::Definition def0 | this = def0.getARead() | this.isAlwaysNull0(def0))
       or

csharp/ql/lib/semmle/code/csharp/dataflow/SSA.qll

@@ -447,6 +447,8 @@ module Ssa {
     final AssignableDefinition getADefinition() { result = SsaImpl::getADefinition(this) }
 
     /**
+     * DEPRECATED.
+     *
      * Holds if this definition updates a captured local scope variable, and the updated
      * value may be read from the implicit entry definition `def` using one or more calls
      * (as indicated by `additionalCalls`), starting from call `c`.
@@ -467,13 +469,15 @@ module Ssa {
      * If this definition is the update of `i` on line 5, then the value may be read inside
      * `M2` via the call on line 6.
      */
-    final predicate isCapturedVariableDefinitionFlowIn(
+    deprecated final predicate isCapturedVariableDefinitionFlowIn(
       ImplicitEntryDefinition def, ControlFlow::Nodes::ElementNode c, boolean additionalCalls
     ) {
-      SsaImpl::isCapturedVariableDefinitionFlowIn(this, def, c, additionalCalls)
+      none()
     }
 
     /**
+     * DEPRECATED.
+     *
      * Holds if this definition updates a captured local scope variable, and the updated
      * value may be read from the implicit call definition `cdef` using one or more calls
      * (as indicated by `additionalCalls`).
@@ -494,10 +498,10 @@ module Ssa {
      * If this definition is the update of `i` on line 4, then the value may be read outside
      * of `M2` via the call on line 5.
      */
-    final predicate isCapturedVariableDefinitionFlowOut(
+    deprecated final predicate isCapturedVariableDefinitionFlowOut(
       ImplicitCallDefinition cdef, boolean additionalCalls
     ) {
-      SsaImpl::isCapturedVariableDefinitionFlowOut(this, cdef, additionalCalls)
+      none()
     }
 
     override Element getElement() { result = ad.getElement() }
@@ -526,8 +530,6 @@ module Ssa {
         or
         SsaImpl::updatesNamedFieldOrProp(bb, i, _, v, _)
         or
-        SsaImpl::updatesCapturedVariable(bb, i, _, v, _, _)
-        or
         SsaImpl::variableWriteQualifier(bb, i, v, _)
       )
     }
@@ -572,10 +574,9 @@ module Ssa {
     private Call c;
 
     ImplicitCallDefinition() {
-      exists(ControlFlow::BasicBlock bb, SourceVariable v, int i | this.definesAt(v, bb, i) |
+      exists(ControlFlow::BasicBlock bb, SourceVariable v, int i |
+        this.definesAt(v, bb, i) and
         SsaImpl::updatesNamedFieldOrProp(bb, i, c, v, _)
-        or
-        SsaImpl::updatesCapturedVariable(bb, i, c, v, _, _)
       )
     }
 
@@ -593,9 +594,6 @@ module Ssa {
         result.getEnclosingCallable() = setter and
         result.getTarget() = this.getSourceVariable().getAssignable()
       )
-      or
-      SsaImpl::updatesCapturedVariable(_, _, this.getCall(), _, result, _) and
-      result.getTarget() = this.getSourceVariable().getAssignable()
     }
 
     override string toString() {

csharp/ql/lib/semmle/code/csharp/dataflow/internal/BaseSSA.qll

@@ -24,7 +24,16 @@ module BaseSsa {
     )
   }
 
+  private predicate implicitEntryDef(
+    Callable c, ControlFlow::BasicBlocks::EntryBlock bb, SsaInput::SourceVariable v
+  ) {
+    v.isReadonlyCapturedBy(c) and
+    c = bb.getCallable()
+  }
+
   private module SsaInput implements SsaImplCommon::InputSig<Location> {
+    private import semmle.code.csharp.controlflow.internal.PreSsa
+
     class BasicBlock = ControlFlow::BasicBlock;
 
     BasicBlock getImmediateBasicBlockDominator(BasicBlock bb) {
@@ -35,20 +44,17 @@ module BaseSsa {
 
     class ExitBasicBlock = ControlFlow::BasicBlocks::ExitBlock;
 
-    pragma[noinline]
-    private Callable getAnAssigningCallable(LocalScopeVariable v) {
-      result = any(AssignableDefinition def | def.getTarget() = v).getEnclosingCallable()
-    }
-
-    class SourceVariable extends LocalScopeVariable {
-      SourceVariable() { not getAnAssigningCallable(this) != getAnAssigningCallable(this) }
-    }
+    class SourceVariable = PreSsa::SimpleLocalScopeVariable;
 
     predicate variableWrite(BasicBlock bb, int i, SourceVariable v, boolean certain) {
       exists(AssignableDefinition def |
         definitionAt(def, bb, i, v) and
         if def.isCertain() then certain = true else certain = false
       )
+      or
+      implicitEntryDef(_, bb, v) and
+      i = -1 and
+      certain = true
     }
 
     predicate variableRead(BasicBlock bb, int i, SourceVariable v, boolean certain) {
@@ -87,7 +93,15 @@ module BaseSsa {
       not result instanceof PhiNode
     }
 
-    Location getLocation() { result = this.getDefinition().getLocation() }
+    Location getLocation() {
+      result = this.getDefinition().getLocation()
+      or
+      exists(Callable c, SsaInput::BasicBlock bb, SsaInput::SourceVariable v |
+        this.definesAt(v, bb, -1) and
+        implicitEntryDef(c, bb, v) and
+        result = c.getLocation()
+      )
+    }
   }
 
   class PhiNode extends SsaImpl::PhiNode, Definition {