C#: Rework SummarizedCallable::clearsContent/2

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

@@ -78,4 +78,21 @@ module SummaryComponentStack {
 
 class SummarizedCallable = Impl::Public::SummarizedCallable;
 
+private class SummarizedCallableDefaultClearsContent extends Impl::Public::SummarizedCallable {
+  SummarizedCallable c;
+
+  SummarizedCallableDefaultClearsContent() { this = c }
+
+  // By default, we assume that all stores into arguments are definite
+  override predicate clearsContent(int i, DataFlow::Content content) {
+    exists(SummaryComponentStack output |
+      c.propagatesFlow(_, output, _) and
+      output.drop(_) =
+        SummaryComponentStack::push(SummaryComponent::content(content),
+          SummaryComponentStack::argument(i)) and
+      not content instanceof DataFlow::ElementContent
+    )
+  }
+}
+
 class RequiredSummaryComponentStack = Impl::Public::RequiredSummaryComponentStack;

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

@@ -252,6 +252,8 @@ private class RetNodeEx extends NodeEx {
   ReturnPosition getReturnPosition() { result = getReturnPosition(this.asNode()) }
 
   ReturnKindExt getKind() { result = this.asNode().(ReturnNodeExt).getKind() }
+
+  predicate allowFlowThroughParameter() { allowFlowThroughParameterCached(this.asNode()) }
 }
 
 private predicate inBarrier(NodeEx node, Configuration config) {
@@ -725,12 +727,16 @@ private module Stage1 {
   /** Holds if flow may return from `callable`. */
   pragma[nomagic]
   private predicate returnFlowCallableNodeCand(
-    DataFlowCallable callable, ReturnKindExt kind, Configuration config
+    DataFlowCallable callable, ReturnKindExt kind, boolean allowFlowThroughParameter,
+    Configuration config
   ) {
     exists(RetNodeEx ret |
       throughFlowNodeCand(ret, config) and
       callable = ret.getEnclosingCallable() and
-      kind = ret.getKind()
+      kind = ret.getKind() and
+      if ret.allowFlowThroughParameter()
+      then allowFlowThroughParameter = true
+      else allowFlowThroughParameter = false
     )
   }
 
@@ -739,13 +745,16 @@ private module Stage1 {
    * candidate for the origin of a summary.
    */
   predicate parameterMayFlowThrough(ParamNodeEx p, DataFlowCallable c, Ap ap, Configuration config) {
-    exists(ReturnKindExt kind |
+    exists(ReturnKindExt kind, boolean allowFlowThroughParameter |
       throughFlowNodeCand(p, config) and
-      returnFlowCallableNodeCand(c, kind, config) and
+      returnFlowCallableNodeCand(c, kind, allowFlowThroughParameter, config) and
       p.getEnclosingCallable() = c and
-      exists(ap) and
-      // we don't expect a parameter to return stored in itself
-      not kind.(ParamUpdateReturnKind).getPosition() = p.getPosition()
+      (
+        if kind.(ParamUpdateReturnKind).getPosition() = p.getPosition()
+        then allowFlowThroughParameter = true
+        else any()
+      ) and
+      exists(ap)
     )
   }
 
@@ -1394,8 +1403,11 @@ private module Stage2 {
       fwdFlow(ret, any(CcCall ccc), apSome(ap), ap0, config) and
       kind = ret.getKind() and
       p.getPosition() = pos and
-      // we don't expect a parameter to return stored in itself
-      not kind.(ParamUpdateReturnKind).getPosition() = pos
+      (
+        if kind.(ParamUpdateReturnKind).getPosition() = p.getPosition()
+        then ret.allowFlowThroughParameter()
+        else any()
+      )
     )
   }
 
@@ -2083,8 +2095,11 @@ private module Stage3 {
       fwdFlow(ret, any(CcCall ccc), apSome(ap), ap0, config) and
       kind = ret.getKind() and
       p.getPosition() = pos and
-      // we don't expect a parameter to return stored in itself
-      not kind.(ParamUpdateReturnKind).getPosition() = pos
+      (
+        if kind.(ParamUpdateReturnKind).getPosition() = p.getPosition()
+        then ret.allowFlowThroughParameter()
+        else any()
+      )
     )
   }
 
@@ -2843,8 +2858,11 @@ private module Stage4 {
       fwdFlow(ret, any(CcCall ccc), apSome(ap), ap0, config) and
       kind = ret.getKind() and
       p.getPosition() = pos and
-      // we don't expect a parameter to return stored in itself
-      not kind.(ParamUpdateReturnKind).getPosition() = pos
+      (
+        if kind.(ParamUpdateReturnKind).getPosition() = p.getPosition()
+        then ret.allowFlowThroughParameter()
+        else any()
+      )
     )
   }
 
@@ -2917,6 +2935,8 @@ private class SummaryCtxSome extends SummaryCtx, TSummaryCtxSome {
 
   int getParameterPos() { p.isParameterOf(_, result) }
 
+  ParameterNode getParameterNode() { result = p.asNode() }
+
   override string toString() { result = p + ": " + ap }
 
   predicate hasLocationInfo(
@@ -3617,7 +3637,11 @@ private predicate paramFlowsThrough(
     ap = mid.getAp() and
     apa = ap.getApprox() and
     pos = sc.getParameterPos() and
-    not kind.(ParamUpdateReturnKind).getPosition() = pos
+    (
+      if kind.(ParamUpdateReturnKind).getPosition() = pos
+      then ret.allowFlowThroughParameter()
+      else any()
+    )
   )
 }
 

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

@@ -801,6 +801,9 @@ private module Cached {
     exists(Node n | getNodeEnclosingCallable(n) = callable | isUnreachableInCallCached(n, call))
   }
 
+  cached
+  predicate allowFlowThroughParameterCached(Node ret) { allowFlowThroughParameter(ret) }
+
   cached
   newtype TCallContext =
     TAnyCallContext() or

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

@@ -175,6 +175,7 @@ module Consistency {
 
   query predicate postWithInFlow(Node n, string msg) {
     isPostUpdateNode(n) and
+    not clearsContent(n, _) and
     simpleLocalFlowStep(_, n) and
     msg = "PostUpdateNode should not be the target of local flow."
   }

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

@@ -310,6 +310,18 @@ module LocalFlow {
     result = n.(ExplicitParameterNode).getSsaDefinition()
   }
 
+  /**
+   * Holds if there is a local use-use flow step from `nodeFrom` to `nodeTo`
+   * involving SSA definition `def`.
+   */
+  predicate localSsaFlowStepUseUse(Ssa::Definition def, Node nodeFrom, Node nodeTo) {
+    exists(ControlFlow::Node cfnFrom, ControlFlow::Node cfnTo |
+      SsaImpl::adjacentReadPairSameVar(def, cfnFrom, cfnTo) and
+      nodeTo = TExprNode(cfnTo) and
+      nodeFrom = TExprNode(cfnFrom)
+    )
+  }
+
   /**
    * Holds if there is a local flow step from `nodeFrom` to `nodeTo` involving
    * SSA definition `def.
@@ -322,14 +334,7 @@ module LocalFlow {
     )
     or
     // Flow from read to next read
-    exists(ControlFlow::Node cfnFrom, ControlFlow::Node cfnTo |
-      SsaImpl::adjacentReadPairSameVar(def, cfnFrom, cfnTo) and
-      nodeTo = TExprNode(cfnTo)
-    |
-      nodeFrom = TExprNode(cfnFrom)
-      or
-      cfnFrom = nodeFrom.(PostUpdateNode).getPreUpdateNode().getControlFlowNode()
-    )
+    localSsaFlowStepUseUse(def, nodeFrom.(PostUpdateNode).getPreUpdateNode(), nodeTo)
     or
     // Flow into phi node
     exists(Ssa::PhiNode phi |
@@ -399,6 +404,12 @@ module LocalFlow {
 predicate simpleLocalFlowStep(Node nodeFrom, Node nodeTo) {
   LocalFlow::localFlowStepCommon(nodeFrom, nodeTo)
   or
+  exists(Ssa::Definition def |
+    LocalFlow::localSsaFlowStepUseUse(def, nodeFrom, nodeTo) and
+    not FlowSummaryImpl::Private::Steps::summaryClearsContentArg(nodeFrom, _) and
+    not LocalFlow::usesInstanceField(def)
+  )
+  or
   LocalFlow::localFlowCapturedVarStep(nodeFrom, nodeTo)
   or
   FlowSummaryImpl::Private::Steps::summaryLocalStep(nodeFrom, nodeTo, true)
@@ -716,6 +727,8 @@ private module Cached {
   predicate localFlowStepImpl(Node nodeFrom, Node nodeTo) {
     LocalFlow::localFlowStepCommon(nodeFrom, nodeTo)
     or
+    LocalFlow::localSsaFlowStepUseUse(_, nodeFrom, nodeTo)
+    or
     exists(Ssa::Definition def |
       LocalFlow::localSsaFlowStep(def, nodeFrom, nodeTo) and
       LocalFlow::usesInstanceField(def)
@@ -1691,9 +1704,6 @@ predicate clearsContent(Node n, Content c) {
   or
   fieldOrPropertyStore(_, c, _, n.(ObjectInitializerNode).getInitializer(), false)
   or
-  FlowSummaryImpl::Private::Steps::summaryStoresIntoArg(c, n) and
-  not c instanceof ElementContent
-  or
   FlowSummaryImpl::Private::Steps::summaryClearsContent(n, c)
   or
   exists(WithExpr we, ObjectInitializer oi, FieldOrProperty f |
@@ -2003,3 +2013,11 @@ predicate additionalLambdaFlowStep(Node nodeFrom, Node nodeTo, boolean preserves
     preservesValue = false
   )
 }
+
+/**
+ * Holds if flow is allowed to pass from a parameter `p`, to return
+ * node `ret`, and back out to `p`.
+ */
+predicate allowFlowThroughParameter(ReturnNodeExt ret) {
+  FlowSummaryImpl::Private::summaryAllowFlowThroughParameter(ret)
+}

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

@@ -261,7 +261,10 @@ module Private {
 
   private newtype TSummaryNodeState =
     TSummaryNodeInputState(SummaryComponentStack s) { inputState(_, s) } or
-    TSummaryNodeOutputState(SummaryComponentStack s) { outputState(_, s) }
+    TSummaryNodeOutputState(SummaryComponentStack s) { outputState(_, s) } or
+    TSummaryNodeClearsContentState(int i, boolean post) {
+      any(SummarizedCallable sc).clearsContent(i, _) and post in [false, true]
+    }
 
   /**
    * A state used to break up (complex) flow summaries into atomic flow steps.
@@ -308,6 +311,12 @@ module Private {
         this = TSummaryNodeOutputState(s) and
         result = "to write: " + s
       )
+      or
+      exists(int i, boolean post, string postStr |
+        this = TSummaryNodeClearsContentState(i, post) and
+        (if post = true then postStr = " (post)" else postStr = "") and
+        result = "clear: " + i + postStr
+      )
     }
   }
 
@@ -329,6 +338,11 @@ module Private {
     not parameterReadState(c, state, _)
     or
     state.isOutputState(c, _)
+    or
+    exists(int i |
+      c.clearsContent(i, _) and
+      state = TSummaryNodeClearsContentState(i, _)
+    )
   }
 
   pragma[noinline]
@@ -364,6 +378,8 @@ module Private {
     parameterReadState(c, _, i)
     or
     isParameterPostUpdate(_, c, i)
+    or
+    c.clearsContent(i, _)
   }
 
   private predicate callbackOutput(
@@ -436,6 +452,12 @@ module Private {
         )
       )
     )
+    or
+    exists(SummarizedCallable c, int i, ParamNode p |
+      n = summaryNode(c, TSummaryNodeClearsContentState(i, false)) and
+      p.isParameterOf(c, i) and
+      result = getNodeType(p)
+    )
   }
 
   /** Holds if summary node `out` contains output of kind `rk` from call `c`. */
@@ -461,6 +483,9 @@ module Private {
     exists(SummarizedCallable c, int i |
       isParameterPostUpdate(post, c, i) and
       pre.(ParamNode).isParameterOf(c, i)
+      or
+      pre = summaryNode(c, TSummaryNodeClearsContentState(i, false)) and
+      post = summaryNode(c, TSummaryNodeClearsContentState(i, true))
     )
     or
     exists(SummarizedCallable callable, SummaryComponentStack s |
@@ -478,6 +503,14 @@ module Private {
     )
   }
 
+  /**
+   * Holds if flow is allowed to pass from a parameter `p`, to return
+   * node `ret`, and back out to `p`.
+   */
+  predicate summaryAllowFlowThroughParameter(ReturnNodeExt ret) {
+    ret = summaryNode(_, TSummaryNodeClearsContentState(_, true))
+  }
+
   /** Provides a compilation of flow summaries to atomic data-flow steps. */
   module Steps {
     /**
@@ -504,11 +537,21 @@ module Private {
       // for `StringBuilder.append(x)` with a specified value flow from qualifier to
       // return value and taint flow from argument 0 to the qualifier, then this
       // allows us to infer taint flow from argument 0 to the return value.
-      succ instanceof ParamNode and summaryPostUpdateNode(pred, succ) and preservesValue = true
+      succ instanceof ParamNode and
+      summaryPostUpdateNode(pred, succ) and
+      preservesValue = true
       or
       // Similarly we would like to chain together summaries where values get passed
       // into callbacks along the way.
-      pred instanceof ArgNode and summaryPostUpdateNode(succ, pred) and preservesValue = true
+      pred instanceof ArgNode and
+      summaryPostUpdateNode(succ, pred) and
+      preservesValue = true
+      or
+      exists(SummarizedCallable c, int i |
+        pred.(ParamNode).isParameterOf(c, i) and
+        succ = summaryNode(c, TSummaryNodeClearsContentState(i, _)) and
+        preservesValue = true
+      )
     }
 
     /**
@@ -536,10 +579,39 @@ module Private {
     }
 
     /**
-     * Holds if values stored inside content `c` are cleared when passed as
-     * input of type `input` in `call`.
+     * Holds if values stored inside content `c` are cleared at `n`. `n` is a
+     * synthesized summary node, so in order for values to be cleared at calls
+     * to the relevant method, it is important that flow does not pass over
+     * the argument, either via use-use flow or def-use flow.
+     *
+     * Example:
+     *
+     * ```
+     * a.b = taint;
+     * a.clearB(); // assume we have a flow summary for `clearB` that clears `b` on the qualifier
+     * sink(a.b);
+     * ```
+     *
+     * In the above, flow should not pass from `a` on the first line (or the second
+     * line) to `a` on the third line. Instead, there will be synthesized flow from
+     * `a` on line 2 to the post-update node for `a` on that line (via an intermediate
+     * node where field `b` is cleared).
      */
-    predicate summaryClearsContent(ArgNode arg, Content c) {
+    predicate summaryClearsContent(Node n, Content c) {
+      exists(SummarizedCallable sc, int i |
+        n = summaryNode(sc, TSummaryNodeClearsContentState(i, true)) and
+        sc.clearsContent(i, c)
+      )
+    }
+
+    /**
+     * Holds if values stored inside content `c` are cleared inside a
+     * callable to which `arg` is an argument.
+     *
+     * In such cases, it is important to prevent use-use flow out of
+     * `arg` (see comment for `summaryClearsContent`).
+     */
+    predicate summaryClearsContentArg(ArgNode arg, Content c) {
       exists(DataFlowCall call, int i |
         viableCallable(call).(SummarizedCallable).clearsContent(i, c) and
         arg.argumentOf(call, i)
@@ -599,25 +671,6 @@ module Private {
         ret.getKind() = rk
       )
     }
-
-    /**
-     * Holds if data is written into content `c` of argument `arg` using a flow summary.
-     *
-     * Depending on the type of `c`, this predicate may be relevant to include in the
-     * definition of `clearsContent()`.
-     */
-    predicate summaryStoresIntoArg(Content c, Node arg) {
-      exists(ParamUpdateReturnKind rk, ReturnNodeExt ret, PostUpdateNode out |
-        exists(DataFlowCall call, SummarizedCallable callable |
-          getNodeEnclosingCallable(ret) = callable and
-          viableCallable(call) = callable and
-          summaryStoreStep(_, c, ret) and
-          ret.getKind() = pragma[only_bind_into](rk) and
-          out = rk.getAnOutNode(call) and
-          arg = out.getPreUpdateNode()
-        )
-      )
-    }
   }
 
   /**

csharp/ql/test/library-tests/dataflow/external-models/steps.expected

@@ -8,6 +8,8 @@ summaryThroughStep
 | Steps.cs:22:13:22:16 | this access | Steps.cs:22:13:22:30 | call to method StepQualRes | false |
 | Steps.cs:23:13:23:25 | this access | Steps.cs:23:13:23:25 | call to method StepQualRes | false |
 | Steps.cs:26:13:26:31 | this access | Steps.cs:26:25:26:30 | [post] access to local variable argOut | false |
+| Steps.cs:30:13:30:16 | this access | Steps.cs:30:13:30:16 | [post] this access | true |
+| Steps.cs:34:13:34:16 | this access | Steps.cs:34:13:34:16 | [post] this access | true |
 | Steps.cs:41:29:41:29 | 0 | Steps.cs:41:13:41:30 | call to method StepGeneric | true |
 | Steps.cs:42:30:42:34 | false | Steps.cs:42:13:42:35 | call to method StepGeneric2<Boolean> | true |
 | Steps.cs:44:36:44:43 | "string" | Steps.cs:44:13:44:44 | call to method StepOverride | true |