Merge pull request #4495 from hvitved/csharp/dataflow/summaries

C#: Shared interface/implementation for flow summaries

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

@@ -0,0 +1,169 @@
+/**
+ * Provides classes and predicates for definining flow summaries.
+ */
+
+import csharp
+private import internal.FlowSummaryImpl as Impl
+private import internal.FlowSummarySpecific::Private
+private import internal.DataFlowPublic as DataFlowPublic
+// import all instances below
+private import semmle.code.csharp.dataflow.LibraryTypeDataFlow
+
+class SummarizableCallable = Impl::Public::SummarizableCallable;
+
+/** An unbound method. */
+class SummarizableMethod extends SummarizableCallable, Method { }
+
+class ContentList = Impl::Public::ContentList;
+
+/** Provides predicates for constructing content lists. */
+module ContentList {
+  import Impl::Public::ContentList
+
+  /** Gets the singleton "element content" content list. */
+  ContentList element() { result = singleton(any(DataFlowPublic::ElementContent c)) }
+
+  /** Gets a singleton property content list. */
+  ContentList property(Property p) {
+    result =
+      singleton(any(DataFlowPublic::PropertyContent c | c.getProperty() = p.getSourceDeclaration()))
+  }
+
+  /** Gets a singleton field content list. */
+  ContentList field(Field f) {
+    result =
+      singleton(any(DataFlowPublic::FieldContent c | c.getField() = f.getSourceDeclaration()))
+  }
+}
+
+class SummaryInput = Impl::Public::SummaryInput;
+
+/** Provides predicates for constructing flow-summary input specifications */
+module SummaryInput {
+  private import semmle.code.csharp.frameworks.system.Collections
+
+  /**
+   * Gets an input specification that specifies the `i`th parameter as
+   * the input.
+   */
+  SummaryInput parameter(int i) { result = TParameterSummaryInput(i) }
+
+  private predicate isCollectionType(ValueOrRefType t) {
+    t.getABaseType*() instanceof SystemCollectionsIEnumerableInterface and
+    not t instanceof StringType
+  }
+
+  /**
+   * Gets an input specification that specifies the `i`th parameter as
+   * the input.
+   *
+   * `inputContents` is either empty or a singleton element content list,
+   * depending on whether the type of the `i`th parameter of `c` is a
+   * collection type.
+   */
+  SummaryInput parameter(SummarizableCallable c, int i, ContentList inputContents) {
+    result = parameter(i) and
+    exists(Parameter p |
+      p = c.getParameter(i) and
+      if isCollectionType(p.getType())
+      then inputContents = ContentList::element()
+      else inputContents = ContentList::empty()
+    )
+  }
+
+  /**
+   * Gets an input specification that specifies the implicit `this` parameter
+   * as the input.
+   */
+  SummaryInput thisParameter() { result = TParameterSummaryInput(-1) }
+
+  /**
+   * Gets an input specification that specifies output from the delegate at
+   * parameter `i` as the input.
+   */
+  SummaryInput delegate(int i) { result = TDelegateSummaryInput(i) }
+
+  /**
+   * Gets an input specification that specifies output from the delegate at
+   * parameter `i` as the input.
+   *
+   * `c` must be a compatible callable, that is, a callable where the `i`th
+   * parameter is a delegate.
+   */
+  SummaryInput delegate(SummarizableCallable c, int i) {
+    result = delegate(i) and
+    hasDelegateArgumentPosition(c, i)
+  }
+}
+
+class SummaryOutput = Impl::Public::SummaryOutput;
+
+/** Provides predicates for constructing flow-summary output specifications. */
+module SummaryOutput {
+  /**
+   * Gets an output specification that specifies the return value from a call as
+   * the output.
+   */
+  SummaryOutput return() { result = TReturnSummaryOutput() }
+
+  /**
+   * Gets an output specification that specifies the `i`th parameter as the
+   * output.
+   */
+  SummaryOutput parameter(int i) { result = TParameterSummaryOutput(i) }
+
+  /**
+   * Gets an output specification that specifies the implicit `this` parameter
+   * as the output.
+   */
+  SummaryOutput thisParameter() { result = TParameterSummaryOutput(-1) }
+
+  /**
+   * Gets an output specification that specifies parameter `j` of the delegate at
+   * parameter `i` as the output.
+   */
+  SummaryOutput delegate(int i, int j) { result = TDelegateSummaryOutput(i, j) }
+
+  /**
+   * Gets an output specification that specifies parameter `j` of the delegate at
+   * parameter `i` as the output.
+   *
+   * `c` must be a compatible callable, that is, a callable where the `i`th
+   * parameter is a delegate with a parameter at position `j`.
+   */
+  SummaryOutput delegate(SummarizableCallable c, int i, int j) {
+    result = TDelegateSummaryOutput(i, j) and
+    hasDelegateArgumentPosition2(c, i, j)
+  }
+}
+
+class SummarizedCallable = Impl::Public::SummarizedCallable;
+
+/** Provides a query predicate for outputting a set of relevant flow summaries. */
+module TestOutput {
+  /** A flow summary to include in the `summary/3` query predicate. */
+  abstract class RelevantSummarizedCallable extends SummarizedCallable { }
+
+  /** A query predicate for outputting flow summaries in QL tests. */
+  query predicate summary(string callable, string flow, boolean preservesValue) {
+    exists(
+      RelevantSummarizedCallable c, SummaryInput input, ContentList inputContents,
+      string inputContentsString, SummaryOutput output, ContentList outputContents,
+      string outputContentsString
+    |
+      callable = c.getQualifiedNameWithTypes() and
+      Impl::Private::summary(c, input, inputContents, output, outputContents, preservesValue) and
+      (
+        if inputContents.length() = 0
+        then inputContentsString = ""
+        else inputContentsString = " [" + inputContents + "]"
+      ) and
+      (
+        if outputContents.length() = 0
+        then outputContentsString = ""
+        else outputContentsString = " [" + outputContents + "]"
+      ) and
+      flow = input + inputContentsString + " -> " + output + outputContentsString
+    )
+  }
+}

csharp/ql/src/semmle/code/csharp/dataflow/LibraryTypeDataFlow.qll

@@ -22,6 +22,7 @@ private import semmle.code.csharp.dataflow.internal.DelegateDataFlow
 // import `LibraryTypeDataFlow` definitions from other files to avoid potential reevaluation
 private import semmle.code.csharp.frameworks.EntityFramework
 private import semmle.code.csharp.frameworks.JsonNET
+private import FlowSummary
 
 private newtype TAccessPath =
   TNilAccessPath() or
@@ -353,6 +354,90 @@ abstract class LibraryTypeDataFlow extends Type {
   }
 }
 
+private CallableFlowSource toCallableFlowSource(SummaryInput input) {
+  result = TCallableFlowSourceQualifier() and
+  input = SummaryInput::parameter(-1)
+  or
+  exists(int i |
+    result = TCallableFlowSourceArg(i) and
+    input = SummaryInput::parameter(i)
+  )
+  or
+  exists(int i |
+    result = TCallableFlowSourceDelegateArg(i) and
+    input = SummaryInput::delegate(i)
+  )
+}
+
+private CallableFlowSink toCallableFlowSink(SummaryOutput output) {
+  result = TCallableFlowSinkQualifier() and
+  output = SummaryOutput::parameter(-1)
+  or
+  result = TCallableFlowSinkReturn() and
+  output = SummaryOutput::return()
+  or
+  exists(int i |
+    result = TCallableFlowSinkArg(i) and
+    output = SummaryOutput::parameter(i)
+  )
+  or
+  exists(int i, int j |
+    result = TCallableFlowSinkDelegateArg(i, j) and
+    output = SummaryOutput::delegate(i, j)
+  )
+}
+
+private AccessPath toAccessPath(ContentList cl) {
+  cl = ContentList::empty() and
+  result = TNilAccessPath()
+  or
+  exists(Content head, ContentList tail |
+    cl = ContentList::cons(head, tail) and
+    result = TConsAccessPath(head, toAccessPath(tail))
+  )
+}
+
+private class FrameworkDataFlowAdaptor extends SummarizedCallable {
+  private LibraryTypeDataFlow ltdf;
+
+  FrameworkDataFlowAdaptor() {
+    ltdf.callableFlow(_, _, this, _) or
+    ltdf.callableFlow(_, _, _, _, this, _) or
+    ltdf.clearsContent(_, _, this)
+  }
+
+  override predicate propagatesFlow(SummaryInput input, SummaryOutput output, boolean preservesValue) {
+    ltdf.callableFlow(toCallableFlowSource(input), toCallableFlowSink(output), this, preservesValue)
+  }
+
+  override predicate propagatesFlow(
+    SummaryInput input, ContentList inputContents, SummaryOutput output, ContentList outputContents,
+    boolean preservesValue
+  ) {
+    ltdf
+        .callableFlow(toCallableFlowSource(input), toAccessPath(inputContents),
+          toCallableFlowSink(output), toAccessPath(outputContents), this, preservesValue)
+  }
+
+  private AccessPath getAnAccessPath() {
+    ltdf.callableFlow(_, result, _, _, this, _)
+    or
+    ltdf.callableFlow(_, _, _, result, _, _)
+  }
+
+  override predicate requiresContentList(Content head, ContentList tail) {
+    exists(AccessPath ap |
+      ap = this.getAnAccessPath().drop(_) and
+      head = ap.getHead() and
+      toAccessPath(tail) = ap.getTail()
+    )
+  }
+
+  override predicate clearsContent(SummaryInput input, Content content) {
+    ltdf.clearsContent(toCallableFlowSource(input), content, this)
+  }
+}
+
 /** Data flow for `System.Int32`. */
 class SystemInt32Flow extends LibraryTypeDataFlow, SystemInt32Struct {
   override predicate callableFlow(

csharp/ql/src/semmle/code/csharp/dataflow/internal/DataFlowDispatch.qll

@@ -3,7 +3,8 @@ private import cil
 private import dotnet
 private import DataFlowPrivate
 private import DelegateDataFlow
-private import semmle.code.csharp.dataflow.LibraryTypeDataFlow
+private import FlowSummaryImpl as FlowSummaryImpl
+private import semmle.code.csharp.dataflow.FlowSummary
 private import semmle.code.csharp.dispatch.Dispatch
 private import semmle.code.csharp.frameworks.system.Collections
 private import semmle.code.csharp.frameworks.system.collections.Generic
@@ -18,7 +19,7 @@ private import semmle.code.csharp.frameworks.system.collections.Generic
 DotNet::Callable getCallableForDataFlow(DotNet::Callable c) {
   exists(DotNet::Callable sourceDecl | sourceDecl = c.getSourceDeclaration() |
     result = sourceDecl and
-    Summaries::summary(result, _, _, _, _, _)
+    result instanceof SummarizedCallable
     or
     result.hasBody() and
     if sourceDecl.getFile().fromSource()
@@ -107,15 +108,15 @@ private module Cached {
       // No need to include calls that are compiled from source
       not call.getImplementation().getMethod().compiledFromSource()
     } or
-    TSummaryDelegateCall(SourceDeclarationCallable c, int pos) {
-      exists(CallableFlowSourceDelegateArg source |
-        Summaries::summary(c, source, _, _, _, _) and
-        pos = source.getArgumentIndex()
+    TSummaryDelegateCall(SummarizedCallable c, int pos) {
+      exists(SummaryInput input |
+        FlowSummaryImpl::Private::summary(c, input, _, _, _, _) and
+        input = SummaryInput::delegate(pos)
       )
       or
-      exists(CallableFlowSinkDelegateArg sink |
-        Summaries::summary(c, _, _, sink, _, _) and
-        pos = sink.getDelegateIndex()
+      exists(SummaryOutput output |
+        FlowSummaryImpl::Private::summary(c, _, _, output, _, _) and
+        output = SummaryOutput::delegate(pos, _)
       )
     }
 
@@ -381,7 +382,7 @@ class CilDataFlowCall extends DataFlowCall, TCilCall {
  * the method `Select`.
  */
 class SummaryDelegateCall extends DelegateDataFlowCall, TSummaryDelegateCall {
-  private SourceDeclarationCallable c;
+  private SummarizedCallable c;
   private int pos;
 
   SummaryDelegateCall() { this = TSummaryDelegateCall(c, pos) }

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

@@ -6,12 +6,13 @@ private import DataFlowDispatch
 private import DataFlowImplCommon
 private import ControlFlowReachability
 private import DelegateDataFlow
+private import FlowSummaryImpl as FlowSummaryImpl
+private import semmle.code.csharp.dataflow.FlowSummary
 private import semmle.code.csharp.Caching
 private import semmle.code.csharp.Conversion
 private import semmle.code.csharp.ExprOrStmtParent
 private import semmle.code.csharp.Unification
 private import semmle.code.csharp.controlflow.Guards
-private import semmle.code.csharp.dataflow.LibraryTypeDataFlow
 private import semmle.code.csharp.dispatch.Dispatch
 private import semmle.code.csharp.frameworks.EntityFramework
 private import semmle.code.csharp.frameworks.NHibernate
@@ -69,6 +70,9 @@ private class ExprNodeImpl extends ExprNode, NodeImpl {
   }
 }
 
+/** A data-flow node used to interpret a flow summary. */
+abstract private class SummaryNodeImpl extends NodeImpl { }
+
 /** Calculation of the relative order in which `this` references are read. */
 private module ThisFlow {
   private class BasicBlock = ControlFlow::BasicBlock;
@@ -350,7 +354,7 @@ module LocalFlow {
    * inter-procedurality or field-sensitivity.
    */
   predicate excludeFromExposedRelations(Node n) {
-    n instanceof Summaries::SummaryNodeImpl or
+    n instanceof SummaryNodeImpl or
     n instanceof ImplicitCapturedArgumentNode
   }
 }
@@ -423,9 +427,9 @@ private predicate fieldOrPropertyStore(Expr e, Content c, Expr src, Expr q, bool
       f.isFieldLike() and
       f instanceof InstanceFieldOrProperty
       or
-      exists(AccessPath ap |
-        Summaries::summary(_, _, ap, _, _, _) and
-        ap.contains(f.getContent())
+      exists(ContentList cl |
+        FlowSummaryImpl::Private::summary(_, _, cl, _, _, _) and
+        cl.contains(f.getContent())
       )
     )
   |
@@ -468,9 +472,9 @@ private predicate fieldOrPropertyRead(Expr e1, Content c, FieldOrPropertyRead e2
     ret.isFieldLike() and
     ret = e2.getTarget()
     or
-    exists(AccessPath ap, Property target |
-      Summaries::summary(_, _, _, _, ap, _) and
-      ap.contains(ret.getContent()) and
+    exists(ContentList cl, Property target |
+      FlowSummaryImpl::Private::summary(_, _, _, _, cl, _) and
+      cl.contains(ret.getContent()) and
       target.getGetter() = e2.(PropertyCall).getARuntimeTarget() and
       overridesOrImplementsSourceDecl(target, ret)
     )
@@ -557,7 +561,7 @@ private Gvn::GvnType getANonTypeParameterSubTypeRestricted(DataFlowType t) {
 /** A collection of cached types and predicates to be evaluated in the same stage. */
 cached
 private module Cached {
-  private import Summaries
+  private import FlowSummarySpecific as FlowSummarySpecific
 
   cached
   newtype TNode =
@@ -601,48 +605,39 @@ private module Cached {
         cfn.getElement() = fla.getQualifier()
       )
     } or
-    TSummaryParameterNode(SourceDeclarationCallable c, int i) {
-      exists(CallableFlowSource source | Summaries::summary(c, source, _, _, _, _) |
-        source instanceof CallableFlowSourceQualifier and i = -1
+    TSummaryParameterNode(SummarizedCallable c, int i) {
+      exists(SummaryInput input | FlowSummaryImpl::Private::summary(c, input, _, _, _, _) |
+        input = SummaryInput::parameter(i)
         or
-        i = source.(CallableFlowSourceArg).getArgumentIndex()
-        or
-        i = source.(CallableFlowSourceDelegateArg).getArgumentIndex()
+        input = SummaryInput::delegate(i)
       )
       or
-      exists(CallableFlowSink sink | Summaries::summary(c, _, _, sink, _, _) |
-        i = sink.(CallableFlowSinkDelegateArg).getDelegateIndex()
+      exists(SummaryOutput output |
+        FlowSummaryImpl::Private::summary(c, _, _, output, _, _) and
+        output = SummaryOutput::delegate(i, _)
       )
     } or
     TSummaryInternalNode(
-      SourceDeclarationCallable c, CallableFlowSource source, AccessPath sourceAp,
-      CallableFlowSink sink, AccessPath sinkAp, boolean preservesValue,
-      SummaryInternalNodeState state
+      SummarizedCallable c, FlowSummaryImpl::Private::SummaryInternalNodeState state
     ) {
-      Summaries::summary(c, source, sourceAp, sink, sinkAp, preservesValue) and
-      (
-        state = TSummaryInternalNodeAfterReadState(sourceAp.drop(_))
-        or
-        state = TSummaryInternalNodeBeforeStoreState(sinkAp.drop(_))
+      FlowSummaryImpl::Private::internalNodeRange(c, state)
+    } or
+    TSummaryReturnNode(SummarizedCallable c, ReturnKind rk) {
+      exists(SummaryOutput output |
+        FlowSummaryImpl::Private::summary(c, _, _, output, _, _) and
+        rk = FlowSummarySpecific::Private::toReturnKind(output)
       )
     } or
-    TSummaryReturnNode(SourceDeclarationCallable c, ReturnKind rk) {
-      exists(CallableFlowSink sink |
-        Summaries::summary(c, _, _, sink, _, _) and
-        rk = Summaries::toReturnKind(sink)
+    TSummaryDelegateOutNode(SummarizedCallable c, int pos) {
+      exists(SummaryInput input |
+        FlowSummaryImpl::Private::summary(c, input, _, _, _, _) and
+        input = SummaryInput::delegate(pos)
       )
     } or
-    TSummaryDelegateOutNode(SourceDeclarationCallable c, int pos) {
-      exists(CallableFlowSourceDelegateArg source |
-        Summaries::summary(c, source, _, _, _, _) and
-        pos = source.getArgumentIndex()
-      )
-    } or
-    TSummaryDelegateArgumentNode(SourceDeclarationCallable c, int delegateIndex, int parameterIndex) {
-      exists(CallableFlowSinkDelegateArg sink |
-        Summaries::summary(c, _, _, sink, _, _) and
-        delegateIndex = sink.getDelegateIndex() and
-        parameterIndex = sink.getDelegateParameterIndex()
+    TSummaryDelegateArgumentNode(SummarizedCallable c, int delegateIndex, int parameterIndex) {
+      exists(SummaryOutput output |
+        FlowSummaryImpl::Private::summary(c, _, _, output, _, _) and
+        output = SummaryOutput::delegate(delegateIndex, parameterIndex)
       )
     } or
     TParamsArgumentNode(ControlFlow::Node callCfn) {
@@ -661,7 +656,7 @@ private module Cached {
     or
     LocalFlow::localFlowCapturedVarStep(nodeFrom, nodeTo)
     or
-    Summaries::summaryLocalStep(nodeFrom, nodeTo, true)
+    FlowSummaryImpl::Private::localStep(nodeFrom, nodeTo, true)
     or
     nodeTo.(ObjectCreationNode).getPreUpdateNode() = nodeFrom.(ObjectInitializerNode)
   }
@@ -681,7 +676,7 @@ private module Cached {
     or
     // Simple flow through library code is included in the exposed local
     // step relation, even though flow is technically inter-procedural
-    Summaries::summaryThroughStep(nodeFrom, nodeTo, true)
+    FlowSummaryImpl::Private::throughStep(nodeFrom, nodeTo, true)
   }
 
   /**
@@ -728,7 +723,7 @@ private module Cached {
       c instanceof ElementContent
     )
     or
-    summaryStoreStep(node1, c, node2)
+    FlowSummaryImpl::Private::storeStep(node1, c, node2)
   }
 
   pragma[nomagic]
@@ -762,7 +757,7 @@ private module Cached {
       c = getResultContent()
     )
     or
-    summaryReadStep(node1, c, node2)
+    FlowSummaryImpl::Private::readStep(node1, c, node2)
   }
 
   /**
@@ -776,10 +771,14 @@ private module Cached {
     or
     fieldOrPropertyStore(_, c, _, n.(ObjectInitializerNode).getInitializer(), false)
     or
-    summaryStoreStep(n, c, _) and
+    FlowSummaryImpl::Private::storeStep(n, c, _) and
     not c instanceof ElementContent
     or
-    summaryClearsContent(n, c)
+    exists(SummaryInput input, DataFlowCall call, int i |
+      FlowSummaryImpl::Private::clearsContent(input, call, c) and
+      input = SummaryInput::parameter(i) and
+      n.(ArgumentNode).argumentOf(call, i)
+    )
   }
 
   /**
@@ -867,7 +866,7 @@ private module Cached {
     or
     n instanceof MallocNode
     or
-    n instanceof Summaries::SummaryNodeImpl
+    n instanceof SummaryNodeImpl
     or
     n instanceof ParamsArgumentNode
   }
@@ -1026,40 +1025,39 @@ private module ParameterNodes {
   }
 
   /** A parameter node for a callable with a flow summary. */
-  class SummaryParameterNode extends ParameterNodeImpl, Summaries::SummaryNodeImpl,
-    TSummaryParameterNode {
-    private SourceDeclarationCallable sdc;
+  class SummaryParameterNode extends ParameterNodeImpl, SummaryNodeImpl, TSummaryParameterNode {
+    private SummarizedCallable sc;
     private int i;
 
-    SummaryParameterNode() { this = TSummaryParameterNode(sdc, i) }
+    SummaryParameterNode() { this = TSummaryParameterNode(sc, i) }
 
-    override Parameter getParameter() { result = sdc.getParameter(i) }
+    override Parameter getParameter() { result = sc.getParameter(i) }
 
     override predicate isParameterOf(DataFlowCallable c, int pos) {
-      c = sdc and
+      c = sc and
       pos = i
     }
 
-    override Callable getEnclosingCallableImpl() { result = sdc }
+    override Callable getEnclosingCallableImpl() { result = sc }
 
     override Type getTypeImpl() {
-      result = sdc.getParameter(i).getType()
+      result = sc.getParameter(i).getType()
       or
       i = -1 and
-      result = sdc.getDeclaringType()
+      result = sc.getDeclaringType()
     }
 
     override ControlFlow::Node getControlFlowNodeImpl() { none() }
 
     override Location getLocationImpl() {
-      result = sdc.getParameter(i).getLocation()
+      result = sc.getParameter(i).getLocation()
       or
       i = -1 and
-      result = sdc.getLocation()
+      result = sc.getLocation()
     }
 
     override string toStringImpl() {
-      result = "[summary] " + sdc.getParameter(i)
+      result = "[summary] " + sc.getParameter(i)
       or
       i = -1 and
       result = "[summary] this"
@@ -1241,9 +1239,9 @@ private module ArgumentNodes {
    * passed to a supplied delegate. For example, in `ints.Select(Foo)` there is a
    * node that represents the argument of the call to `Foo` inside `Select`.
    */
-  class SummaryDelegateArgumentNode extends ArgumentNode, Summaries::SummaryNodeImpl,
+  class SummaryDelegateArgumentNode extends ArgumentNode, SummaryNodeImpl,
     TSummaryDelegateArgumentNode {
-    private SourceDeclarationCallable c;
+    private SummarizedCallable c;
     private int delegateIndex;
     private int parameterIndex;
 
@@ -1386,29 +1384,29 @@ private module ReturnNodes {
   }
 
   /** A return node for a callable with a flow summary. */
-  class SummaryReturnNode extends ReturnNode, Summaries::SummaryNodeImpl, TSummaryReturnNode {
-    private SourceDeclarationCallable sdc;
+  class SummaryReturnNode extends ReturnNode, SummaryNodeImpl, TSummaryReturnNode {
+    private SummarizedCallable sc;
     private ReturnKind rk;
 
-    SummaryReturnNode() { this = TSummaryReturnNode(sdc, rk) }
+    SummaryReturnNode() { this = TSummaryReturnNode(sc, rk) }
 
-    override Callable getEnclosingCallableImpl() { result = sdc }
+    override Callable getEnclosingCallableImpl() { result = sc }
 
     override DotNet::Type getTypeImpl() {
       rk instanceof NormalReturnKind and
-      result in [sdc.getReturnType(), sdc.(Constructor).getDeclaringType()]
+      result in [sc.getReturnType(), sc.(Constructor).getDeclaringType()]
       or
       rk instanceof QualifierReturnKind and
-      result = sdc.getDeclaringType()
+      result = sc.getDeclaringType()
       or
-      result = sdc.getParameter(rk.(OutRefReturnKind).getPosition()).getType()
+      result = sc.getParameter(rk.(OutRefReturnKind).getPosition()).getType()
     }
 
     override ControlFlow::Node getControlFlowNodeImpl() { none() }
 
-    override Location getLocationImpl() { result = sdc.getLocation() }
+    override Location getLocationImpl() { result = sc.getLocation() }
 
-    override string toStringImpl() { result = "[summary] return of kind " + rk + " inside " + sdc }
+    override string toStringImpl() { result = "[summary] return of kind " + rk + " inside " + sc }
 
     override ReturnKind getKind() { result = rk }
   }
@@ -1560,9 +1558,8 @@ private module OutNodes {
    * result of calling a supplied delegate. For example, in `ints.Select(Foo)` there
    * is a node that represents the output of calling `Foo` inside `Select`.
    */
-  private class SummaryDelegateOutNode extends OutNode, Summaries::SummaryNodeImpl,
-    TSummaryDelegateOutNode {
-    private SourceDeclarationCallable c;
+  private class SummaryDelegateOutNode extends OutNode, SummaryNodeImpl, TSummaryDelegateOutNode {
+    private SummarizedCallable c;
     private int pos;
 
     SummaryDelegateOutNode() { this = TSummaryDelegateOutNode(c, pos) }
@@ -1596,313 +1593,24 @@ private module OutNodes {
 
 import OutNodes
 
-/**
- * Provides predicates for interpreting flow summaries defined in
- * `LibraryTypeDataFlow.qll`.
- */
-module Summaries {
-  /** A data-flow node used to interpret a flow summary. */
-  abstract class SummaryNodeImpl extends NodeImpl { }
+/** A data-flow node used to model flow summaries. */
+private class SummaryInternalNode extends SummaryNodeImpl, TSummaryInternalNode {
+  private SummarizedCallable c;
+  private FlowSummaryImpl::Private::SummaryInternalNodeState state;
 
-  /**
-   * Holds if data can flow from a node of kind `source` to a node of kind `sink`,
-   * using a call to a callable with a flow summary.
-   *
-   * `sourceAp` describes the contents of the source node that flows to the sink
-   * (if any), and `sinkAp` describes the contents of the sink that it flows to
-   * (if any).
-   */
-  pragma[nomagic]
-  predicate summary(
-    SourceDeclarationCallable c, CallableFlowSource source, AccessPath sourceAp,
-    CallableFlowSink sink, AccessPath sinkAp, boolean preservesValue
-  ) {
-    any(LibraryTypeDataFlow ltdf).callableFlow(source, sink, c, preservesValue) and
-    sourceAp = AccessPath::empty() and
-    sinkAp = AccessPath::empty()
-    or
-    any(LibraryTypeDataFlow ltdf).callableFlow(source, sourceAp, sink, sinkAp, c, preservesValue)
-  }
+  SummaryInternalNode() { this = TSummaryInternalNode(c, state) }
 
-  /** Gets the return kind that matches `sink`, if any. */
-  ReturnKind toReturnKind(CallableFlowSink sink) {
-    sink instanceof CallableFlowSinkQualifier and result instanceof QualifierReturnKind
-    or
-    sink instanceof CallableFlowSinkReturn and result instanceof NormalReturnKind
-    or
-    sink.(CallableFlowSinkArg).getArgumentIndex() = result.(OutRefReturnKind).getPosition()
-  }
+  override DataFlowCallable getEnclosingCallableImpl() { result = c }
 
-  newtype TSummaryInternalNodeState =
-    TSummaryInternalNodeAfterReadState(AccessPath ap) { ap.length() > 0 } or
-    TSummaryInternalNodeBeforeStoreState(AccessPath ap) { ap.length() > 0 }
+  override DataFlowType getDataFlowType() { result = state.getType() }
 
-  /**
-   * A state used to break up (complex) flow summaries for library code into atomic
-   * flow steps. For a flow summary with source access path `sourceAp` and sink
-   * access path `sinkAp`, the following states are used:
-   *
-   * - `TSummaryInternalNodeAfterReadState(AccessPath ap)`: this state represents
-   *   that the head of `ap` has been read from, where `ap` is a suffix of
-   *   `sourceAp`.
-   * - `TSummaryInternalNodeBeforeStoreState(AccessPath ap)`: this state represents
-   *   that the head of `ap` is to be stored into next, where `ap` is a suffix of
-   *   `sinkAp`.
-   *
-   * The state machine for flow summaries has no branching, hence from the entry
-   * state there is a unique path to the exit state.
-   */
-  class SummaryInternalNodeState extends TSummaryInternalNodeState {
-    string toString() {
-      exists(AccessPath ap |
-        this = TSummaryInternalNodeAfterReadState(ap) and
-        result = "after read: " + ap
-      )
-      or
-      exists(AccessPath ap |
-        this = TSummaryInternalNodeBeforeStoreState(ap) and
-        result = "before store: " + ap
-      )
-    }
+  override DotNet::Type getTypeImpl() { none() }
 
-    /** Holds if this state represents the state after the last read. */
-    predicate isLastReadState() {
-      this = TSummaryInternalNodeAfterReadState(AccessPath::singleton(_))
-    }
+  override ControlFlow::Node getControlFlowNodeImpl() { none() }
 
-    /** Holds if this state represents the state before the first store. */
-    predicate isFirstStoreState() {
-      this = TSummaryInternalNodeBeforeStoreState(AccessPath::singleton(_))
-    }
-  }
+  override Location getLocationImpl() { result = c.getLocation() }
 
-  private NodeImpl getSourceNode(SourceDeclarationCallable c, CallableFlowSource source) {
-    exists(int i | result = TSummaryParameterNode(c, i) |
-      source instanceof CallableFlowSourceQualifier and i = -1
-      or
-      i = source.(CallableFlowSourceArg).getArgumentIndex()
-    )
-    or
-    result = TSummaryDelegateOutNode(c, source.(CallableFlowSourceDelegateArg).getArgumentIndex())
-  }
-
-  private NodeImpl getSinkNode(SourceDeclarationCallable c, CallableFlowSink sink) {
-    result = TSummaryReturnNode(c, toReturnKind(sink))
-    or
-    sink =
-      any(CallableFlowSinkDelegateArg s |
-        result =
-          TSummaryDelegateArgumentNode(c, s.getDelegateIndex(), s.getDelegateParameterIndex())
-      )
-  }
-
-  /**
-   * Holds if there is a local step from `pred` to `succ`, which is synthesized
-   * from a flow summary.
-   */
-  predicate summaryLocalStep(Node pred, Node succ, boolean preservesValue) {
-    exists(
-      SourceDeclarationCallable c, CallableFlowSource source, AccessPath sourceAp,
-      CallableFlowSink sink, AccessPath sinkAp
-    |
-      pred = getSourceNode(c, source)
-    |
-      // Simple flow summary without reads or stores
-      sourceAp = AccessPath::empty() and
-      sinkAp = AccessPath::empty() and
-      summary(c, source, sourceAp, sink, sinkAp, preservesValue) and
-      succ = getSinkNode(c, sink)
-      or
-      // Flow summary with stores but no reads
-      exists(SummaryInternalNodeState succState |
-        sourceAp = AccessPath::empty() and
-        succState.isFirstStoreState() and
-        succ = TSummaryInternalNode(c, source, sourceAp, sink, sinkAp, preservesValue, succState)
-      )
-    )
-    or
-    // Exit step after last read (no stores)
-    exists(
-      SourceDeclarationCallable c, SummaryInternalNodeState predState, CallableFlowSink sink,
-      AccessPath sinkAp
-    |
-      sinkAp = AccessPath::empty() and
-      predState.isLastReadState() and
-      pred = TSummaryInternalNode(c, _, _, sink, sinkAp, preservesValue, predState) and
-      succ = getSinkNode(c, sink)
-    )
-    or
-    // Internal step for complex flow summaries with both reads and writes
-    exists(
-      SourceDeclarationCallable c, CallableFlowSource source, AccessPath sourceAp,
-      CallableFlowSink sink, AccessPath sinkAp, SummaryInternalNodeState predState,
-      SummaryInternalNodeState succState
-    |
-      predState.isLastReadState() and
-      pred = TSummaryInternalNode(c, source, sourceAp, sink, sinkAp, preservesValue, predState) and
-      succState.isFirstStoreState() and
-      succ = TSummaryInternalNode(c, source, sourceAp, sink, sinkAp, preservesValue, succState)
-    )
-  }
-
-  /**
-   * Holds if data can flow from `pred` to `succ` via an assignment to
-   * content `c`, using a flow summary.
-   */
-  predicate summaryStoreStep(Node pred, Content c, Node succ) {
-    exists(
-      SourceDeclarationCallable sdc, CallableFlowSource source, AccessPath sourceAp,
-      CallableFlowSink sink, AccessPath sinkAp, boolean preservesValue,
-      SummaryInternalNodeState predState, AccessPath predAp
-    |
-      predState = TSummaryInternalNodeBeforeStoreState(predAp) and
-      pred = TSummaryInternalNode(sdc, source, sourceAp, sink, sinkAp, preservesValue, predState) and
-      c = predAp.getHead()
-    |
-      // More stores needed
-      exists(SummaryInternalNodeState succState |
-        succState =
-          TSummaryInternalNodeBeforeStoreState(any(AccessPath succAp | succAp.getTail() = predAp)) and
-        succ = TSummaryInternalNode(sdc, source, sourceAp, sink, sinkAp, preservesValue, succState)
-      )
-      or
-      // Last store
-      predAp = sinkAp and
-      succ = getSinkNode(sdc, sink)
-    )
-  }
-
-  /**
-   * Holds if data can flow from `pred` to `succ` via a read of content `c`,
-   * using library code.
-   */
-  predicate summaryReadStep(Node pred, Content c, Node succ) {
-    exists(
-      SourceDeclarationCallable sdc, CallableFlowSource source, AccessPath sourceAp,
-      CallableFlowSink sink, AccessPath sinkAp, boolean preservesValue,
-      SummaryInternalNodeState succState, AccessPath succAp
-    |
-      succState = TSummaryInternalNodeAfterReadState(succAp) and
-      succ = TSummaryInternalNode(sdc, source, sourceAp, sink, sinkAp, preservesValue, succState) and
-      c = succAp.getHead()
-    |
-      // First read
-      succAp = sourceAp and
-      pred = getSourceNode(sdc, source)
-      or
-      // Subsequent reads
-      exists(SummaryInternalNodeState predState, AccessPath predAp |
-        predState = TSummaryInternalNodeAfterReadState(predAp) and
-        predAp.getTail() = succAp and
-        pred = TSummaryInternalNode(sdc, source, sourceAp, sink, sinkAp, preservesValue, predState)
-      )
-    )
-  }
-
-  pragma[nomagic]
-  private SummaryParameterNode summaryArgParam(ArgumentNode arg, ReturnKind rk, OutNode out) {
-    exists(DataFlowCall call, int pos, SourceDeclarationCallable sdc |
-      arg.argumentOf(call, pos) and
-      call.getARuntimeTarget() = sdc and
-      result = TSummaryParameterNode(sdc, pos) and
-      call = out.getCall(rk)
-    )
-  }
-
-  /**
-   * Holds if `arg` flows to `out` using a simple flow summary, that is, a flow
-   * summary without delegates, reads, and stores.
-   */
-  predicate summaryThroughStep(ArgumentNode arg, OutNode out, boolean preservesValue) {
-    exists(ReturnKind rk |
-      summaryLocalStep(summaryArgParam(arg, rk, out), TSummaryReturnNode(_, rk), preservesValue)
-    )
-  }
-
-  /**
-   * Holds if there is a (taint+)store of `arg` into content `c` of `out` using a
-   * flow summary.
-   */
-  predicate summarySetterStep(ArgumentNode arg, Content c, OutNode out) {
-    exists(ReturnKind rk, Node mid |
-      summaryLocalStep(summaryArgParam(arg, rk, out), mid, _) and
-      summaryStoreStep(mid, c, TSummaryReturnNode(_, rk))
-    )
-  }
-
-  /**
-   * Holds if there is a read(+taint) of `c` from `arg` to `out` using a
-   * flow summary.
-   */
-  predicate summaryGetterStep(ArgumentNode arg, Content c, OutNode out) {
-    exists(ReturnKind rk, Node mid |
-      summaryReadStep(summaryArgParam(arg, rk, out), c, mid) and
-      summaryLocalStep(mid, TSummaryReturnNode(_, rk), _)
-    )
-  }
-
-  /**
-   * Holds if values stored inside content `c` are cleared at node `n`, as a result
-   * of calling a library method.
-   */
-  predicate summaryClearsContent(Node n, Content c) {
-    exists(LibraryTypeDataFlow ltdf, CallableFlowSource source, Call call |
-      ltdf.clearsContent(source, c, call.getTarget().getSourceDeclaration()) and
-      n.asExpr() = source.getSource(call)
-    )
-  }
-
-  /** Gets the type of content `c`. */
-  pragma[noinline]
-  private Gvn::GvnType getContentType(Content c) {
-    exists(Type t | result = Gvn::getGlobalValueNumber(t) |
-      t = c.(FieldContent).getField().getType()
-      or
-      t = c.(PropertyContent).getProperty().getType()
-      or
-      c instanceof ElementContent and
-      t instanceof ObjectType // we don't know what the actual element type is
-    )
-  }
-
-  /** A data-flow node used to model flow summaries. */
-  private class SummaryInternalNode extends SummaryNodeImpl, TSummaryInternalNode {
-    private SourceDeclarationCallable c;
-    private CallableFlowSource source;
-    private AccessPath sourceAp;
-    private CallableFlowSink sink;
-    private AccessPath sinkAp;
-    private boolean preservesValue;
-    private SummaryInternalNodeState state;
-
-    SummaryInternalNode() {
-      this = TSummaryInternalNode(c, source, sourceAp, sink, sinkAp, preservesValue, state)
-    }
-
-    override DataFlowCallable getEnclosingCallableImpl() { result = c }
-
-    override Gvn::GvnType getDataFlowType() {
-      exists(AccessPath ap |
-        state = TSummaryInternalNodeAfterReadState(ap) and
-        if sinkAp.length() = 0 and state.isLastReadState() and preservesValue = true
-        then result = getSinkNode(c, sink).getDataFlowType()
-        else result = getContentType(ap.getHead())
-        or
-        state = TSummaryInternalNodeBeforeStoreState(ap) and
-        if sourceAp.length() = 0 and state.isFirstStoreState() and preservesValue = true
-        then result = getSourceNode(c, source).getDataFlowType()
-        else result = getContentType(ap.getHead())
-      )
-    }
-
-    override DotNet::Type getTypeImpl() { none() }
-
-    override ControlFlow::Node getControlFlowNodeImpl() { none() }
-
-    override Location getLocationImpl() { result = c.getLocation() }
-
-    override string toStringImpl() { result = "[summary] " + state + " in " + c }
-  }
+  override string toStringImpl() { result = "[summary] " + state + " in " + c }
 }
 
 /** A field or a property. */

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

@@ -0,0 +1,470 @@
+/**
+ * Provides classes and predicates for definining flow summaries.
+ *
+ * The definitions in this file are language-independant, and language-specific
+ * definitions are passed in via the `FlowSummarySpecific` module.
+ */
+
+private import FlowSummarySpecific::Private
+
+/**
+ * Provides classes and predicates for definining flow summaries.
+ */
+module Public {
+  import FlowSummarySpecific::Public
+
+  private newtype TContentList =
+    TNilContentList() or
+    TConsContentList(Content head, ContentList tail) {
+      tail = TNilContentList()
+      or
+      any(SummarizedCallable c).requiresContentList(head, tail) and
+      tail.length() < accessPathLimit()
+    }
+
+  /** A content list. */
+  class ContentList extends TContentList {
+    /** Gets the head of this content list, if any. */
+    Content head() { this = TConsContentList(result, _) }
+
+    /** Gets the tail of this content list, if any. */
+    ContentList tail() { this = TConsContentList(_, result) }
+
+    /** Gets the length of this content list. */
+    int length() {
+      this = TNilContentList() and result = 0
+      or
+      result = 1 + this.tail().length()
+    }
+
+    /** Gets the content list obtained by dropping the first `i` elements, if any. */
+    ContentList drop(int i) {
+      i = 0 and result = this
+      or
+      result = this.tail().drop(i - 1)
+    }
+
+    /** Holds if this content list contains content `c`. */
+    predicate contains(Content c) { c = this.drop(_).head() }
+
+    /** Gets a textual representation of this content list. */
+    string toString() {
+      exists(Content head, ContentList tail |
+        head = this.head() and
+        tail = this.tail() and
+        if tail.length() = 0 then result = head.toString() else result = head + ", " + tail
+      )
+      or
+      this = TNilContentList() and
+      result = "<empty>"
+    }
+  }
+
+  /** Provides predicates for constructing content lists. */
+  module ContentList {
+    /** Gets the empty content list. */
+    ContentList empty() { result = TNilContentList() }
+
+    /** Gets a singleton content list containing `c`. */
+    ContentList singleton(Content c) { result = TConsContentList(c, TNilContentList()) }
+
+    /** Gets the content list obtained by consing `head` onto `tail`. */
+    ContentList cons(Content head, ContentList tail) { result = TConsContentList(head, tail) }
+  }
+
+  /** A callable with flow summaries. */
+  abstract class SummarizedCallable extends SummarizableCallable {
+    /**
+     * Holds if data may flow from `input` to `output` through this callable.
+     *
+     * `preservesValue` indicates whether this is a value-preserving step
+     * or a taint-step.
+     */
+    pragma[nomagic]
+    predicate propagatesFlow(SummaryInput input, SummaryOutput output, boolean preservesValue) {
+      none()
+    }
+
+    /**
+     * Holds if data may flow from `input` to `output` through this callable.
+     *
+     * `inputContents` describes the contents that is popped from the access
+     * path from the input and `outputContents` describes the contents that
+     * is pushed onto the resulting access path.
+     *
+     * `preservesValue` indicates whether this is a value-preserving step
+     * or a taint-step.
+     */
+    pragma[nomagic]
+    predicate propagatesFlow(
+      SummaryInput input, ContentList inputContents, SummaryOutput output,
+      ContentList outputContents, boolean preservesValue
+    ) {
+      none()
+    }
+
+    /**
+     * Holds if the content list obtained by consing `head` onto `tail` is needed
+     * for a summary specified by `propagatesFlow()`.
+     *
+     * This predicate is needed for QL technical reasons only (the IPA type used
+     * to represent content lists needs to be bounded).
+     *
+     * Only summaries using content lists of length >= 2 need to override this
+     * predicate.
+     */
+    pragma[nomagic]
+    predicate requiresContentList(Content head, ContentList tail) { none() }
+
+    /**
+     * Holds if values stored inside `content` are cleared on objects passed as
+     * arguments of type `input` to this callable.
+     */
+    pragma[nomagic]
+    predicate clearsContent(SummaryInput input, Content content) { none() }
+  }
+}
+
+/**
+ * Provides predicates for compiling flow summaries down to atomic local steps,
+ * read steps, and store steps.
+ */
+module Private {
+  private import Public
+  private import DataFlowDispatch
+  private import FlowSummarySpecific::Public
+
+  /**
+   * Holds if data may flow from `input` to `output` when calling `c`.
+   *
+   * `inputContents` describes the contents that is popped from the access
+   * path from the input and `outputContents` describes the contents that
+   * is pushed onto the resulting access path.
+   *
+   * `preservesValue` indicates whether this is a value-preserving step
+   * or a taint-step.
+   */
+  pragma[nomagic]
+  predicate summary(
+    SummarizedCallable c, SummaryInput input, ContentList inputContents, SummaryOutput output,
+    ContentList outputContents, boolean preservesValue
+  ) {
+    c.propagatesFlow(input, output, preservesValue) and
+    inputContents = ContentList::empty() and
+    outputContents = ContentList::empty()
+    or
+    c.propagatesFlow(input, inputContents, output, outputContents, preservesValue)
+  }
+
+  /** Gets the `i`th element in `l`. */
+  pragma[noinline]
+  private Content getContent(ContentList l, int i) { result = l.drop(i).head() }
+
+  private newtype TContentListRev =
+    TConsNilContentListRev(Content c) or
+    TConsContentListRev(Content head, ContentListRev tail) {
+      exists(ContentList l, int i |
+        tail = reverse(l, i) and
+        head = getContent(l, i)
+      )
+    }
+
+  /**
+   * Gets the reversed content list that contains the `i` first elements of `l`
+   * in reverse order.
+   */
+  private ContentListRev reverse(ContentList l, int i) {
+    exists(Content head |
+      result = TConsNilContentListRev(head) and
+      head = l.head() and
+      i = 1
+      or
+      exists(ContentListRev tail |
+        result = TConsContentListRev(head, tail) and
+        tail = reverse(l, i - 1) and
+        head = getContent(l, i - 1)
+      )
+    )
+  }
+
+  /** A reversed, non-empty content list. */
+  private class ContentListRev extends TContentListRev {
+    /** Gets the head of this reversed content list. */
+    Content head() {
+      this = TConsNilContentListRev(result) or this = TConsContentListRev(result, _)
+    }
+
+    /** Gets the tail of this reversed content list, if any. */
+    ContentListRev tail() { this = TConsContentListRev(_, result) }
+
+    /** Gets the length of this reversed content list. */
+    int length() {
+      this = TConsNilContentListRev(_) and result = 1
+      or
+      result = 1 + this.tail().length()
+    }
+
+    /** Gets a textual representation of this reversed content list. */
+    string toString() {
+      exists(Content head |
+        this = TConsNilContentListRev(head) and
+        result = head.toString()
+        or
+        exists(ContentListRev tail |
+          head = this.head() and
+          tail = this.tail() and
+          result = head + ", " + tail
+        )
+      )
+    }
+  }
+
+  private newtype TSummaryInternalNodeState =
+    TSummaryInternalNodeReadState(SummaryInput input, ContentListRev l) {
+      exists(ContentList inputContents |
+        summary(_, input, inputContents, _, _, _) and
+        l = reverse(inputContents, _)
+      )
+    } or
+    TSummaryInternalNodeStoreState(SummaryOutput output, ContentListRev l) {
+      exists(ContentList outputContents |
+        summary(_, _, _, output, outputContents, _) and
+        l = reverse(outputContents, _)
+      )
+    }
+
+  /**
+   * A state used to break up (complex) flow summaries into atomic flow steps.
+   * For a flow summary with input `input`, input contents `inputContents`, output
+   * `output`, and output contents `outputContents`, the following states are used:
+   *
+   * - `TSummaryInternalNodeReadState(SummaryInput input, ContentListRev l)`:
+   *   this state represents that the contents in `l` has been read from `input`,
+   *   where `l` is a reversed, non-empty suffix of `inputContents`.
+   * - `TSummaryInternalNodeStoreState(SummaryOutput output, ContentListRev l)`:
+   *   this state represents that the contents of `l` remains to be stored into
+   *   `output`, where `l` is a reversed, non-empty suffix of `outputContents`.
+   */
+  class SummaryInternalNodeState extends TSummaryInternalNodeState {
+    /**
+     * Holds if this state represents that the `i` first elements of `inputContents`
+     * have been read from `input` in `c`.
+     */
+    pragma[nomagic]
+    predicate isReadState(SummarizedCallable c, SummaryInput input, ContentList inputContents, int i) {
+      this = TSummaryInternalNodeReadState(input, reverse(inputContents, i)) and
+      summary(c, input, inputContents, _, _, _)
+    }
+
+    /**
+     * Holds if this state represents that the `i` first elements of `outputContents`
+     * remain to be stored into `output` in `c`.
+     */
+    pragma[nomagic]
+    predicate isStoreState(
+      SummarizedCallable c, SummaryOutput output, ContentList outputContents, int i
+    ) {
+      this = TSummaryInternalNodeStoreState(output, reverse(outputContents, i)) and
+      summary(c, _, _, output, outputContents, _)
+    }
+
+    /** Gets the type of a node in this state. */
+    DataFlowType getType() {
+      exists(ContentListRev l | result = getContentType(l.head()) |
+        this = TSummaryInternalNodeReadState(_, l)
+        or
+        this = TSummaryInternalNodeStoreState(_, l)
+      )
+    }
+
+    /** Gets a textual representation of this state. */
+    string toString() {
+      exists(SummaryInput input, ContentListRev l |
+        this = TSummaryInternalNodeReadState(input, l) and
+        result = "input: " + input + ", read: " + l
+      )
+      or
+      exists(SummaryOutput output, ContentListRev l |
+        this = TSummaryInternalNodeStoreState(output, l) and
+        result = "output: " + output + ", to store: " + l
+      )
+    }
+  }
+
+  /**
+   * Holds if an internal summary node is needed for the state `state` in summarized
+   * callable `c`.
+   */
+  predicate internalNodeRange(SummarizedCallable c, SummaryInternalNodeState state) {
+    state.isReadState(c, _, _, _)
+    or
+    state.isStoreState(c, _, _, _)
+  }
+
+  pragma[noinline]
+  private Node internalNodeLastReadState(
+    SummarizedCallable c, SummaryInput input, ContentList inputContents
+  ) {
+    exists(SummaryInternalNodeState state |
+      state.isReadState(c, input, inputContents, inputContents.length()) and
+      result = internalNode(c, state)
+    )
+  }
+
+  pragma[noinline]
+  private Node internalNodeFirstStoreState(
+    SummarizedCallable c, SummaryOutput output, ContentList outputContents
+  ) {
+    exists(SummaryInternalNodeState state |
+      state.isStoreState(c, output, outputContents, outputContents.length()) and
+      result = internalNode(c, state)
+    )
+  }
+
+  /**
+   * Holds if there is a local step from `pred` to `succ`, which is synthesized
+   * from a flow summary.
+   */
+  predicate localStep(Node pred, Node succ, boolean preservesValue) {
+    exists(
+      SummarizedCallable c, SummaryInput input, ContentList inputContents, SummaryOutput output,
+      ContentList outputContents
+    |
+      summary(c, input, inputContents, output, outputContents, preservesValue)
+    |
+      pred = inputNode(c, input) and
+      (
+        // Simple flow summary without reads or stores
+        inputContents = ContentList::empty() and
+        outputContents = ContentList::empty() and
+        succ = outputNode(c, output)
+        or
+        // Flow summary with stores but no reads
+        inputContents = ContentList::empty() and
+        succ = internalNodeFirstStoreState(c, output, outputContents)
+      )
+      or
+      pred = internalNodeLastReadState(c, input, inputContents) and
+      (
+        // Exit step after last read (no stores)
+        outputContents = ContentList::empty() and
+        succ = outputNode(c, output)
+        or
+        // Internal step for complex flow summaries with both reads and writes
+        succ = internalNodeFirstStoreState(c, output, outputContents)
+      )
+    )
+  }
+
+  /**
+   * Holds if there is a read step from `pred` to `succ`, which is synthesized
+   * from a flow summary.
+   */
+  predicate readStep(Node pred, Content c, Node succ) {
+    exists(
+      SummarizedCallable sc, SummaryInput input, ContentList inputContents,
+      SummaryInternalNodeState succState, int i
+    |
+      succState.isReadState(sc, input, inputContents, i) and
+      succ = internalNode(sc, succState) and
+      c = getContent(inputContents, i - 1)
+    |
+      // First read
+      i = 1 and
+      pred = inputNode(sc, input)
+      or
+      // Subsequent reads
+      exists(SummaryInternalNodeState predState |
+        predState.isReadState(sc, input, inputContents, i - 1) and
+        pred = internalNode(sc, predState)
+      )
+    )
+  }
+
+  /**
+   * Holds if there is a store step from `pred` to `succ`, which is synthesized
+   * from a flow summary.
+   */
+  predicate storeStep(Node pred, Content c, Node succ) {
+    exists(
+      SummarizedCallable sc, SummaryOutput output, ContentList outputContents,
+      SummaryInternalNodeState predState, int i
+    |
+      predState.isStoreState(sc, output, outputContents, i) and
+      pred = internalNode(sc, predState) and
+      c = getContent(outputContents, i - 1)
+    |
+      // More stores needed
+      exists(SummaryInternalNodeState succState |
+        succState.isStoreState(sc, output, outputContents, i - 1) and
+        succ = internalNode(sc, succState)
+      )
+      or
+      // Last store
+      i = 1 and
+      succ = outputNode(sc, output)
+    )
+  }
+
+  pragma[nomagic]
+  private ParameterNode summaryArgParam(ArgumentNode arg, ReturnKind rk, OutNode out) {
+    exists(DataFlowCall call, int pos, SummarizedCallable callable |
+      arg.argumentOf(call, pos) and
+      viableCallable(call) = callable and
+      result.isParameterOf(callable, pos) and
+      call = out.getCall(rk)
+    )
+  }
+
+  /**
+   * Holds if `arg` flows to `out` using a simple flow summary, that is, a flow
+   * summary without reads and stores.
+   *
+   * NOTE: This step should not be used in global data-flow/taint-tracking, but may
+   * be useful to include in the exposed local data-flow/taint-tracking relations.
+   */
+  predicate throughStep(ArgumentNode arg, OutNode out, boolean preservesValue) {
+    exists(ReturnKind rk, ReturnNode ret |
+      localStep(summaryArgParam(arg, rk, out), ret, preservesValue) and
+      ret.getKind() = rk
+    )
+  }
+
+  /**
+   * Holds if there is a read(+taint) of `c` from `arg` to `out` using a
+   * flow summary.
+   *
+   * NOTE: This step should not be used in global data-flow/taint-tracking, but may
+   * be useful to include in the exposed local data-flow/taint-tracking relations.
+   */
+  predicate getterStep(ArgumentNode arg, Content c, OutNode out) {
+    exists(ReturnKind rk, Node mid, ReturnNode ret |
+      readStep(summaryArgParam(arg, rk, out), c, mid) and
+      localStep(mid, ret, _) and
+      ret.getKind() = rk
+    )
+  }
+
+  /**
+   * Holds if there is a (taint+)store of `arg` into content `c` of `out` using a
+   * flow summary.
+   *
+   * NOTE: This step should not be used in global data-flow/taint-tracking, but may
+   * be useful to include in the exposed local data-flow/taint-tracking relations.
+   */
+  predicate setterStep(ArgumentNode arg, Content c, OutNode out) {
+    exists(ReturnKind rk, Node mid, ReturnNode ret |
+      localStep(summaryArgParam(arg, rk, out), mid, _) and
+      storeStep(mid, c, ret) and
+      ret.getKind() = rk
+    )
+  }
+
+  /**
+   * Holds if values stored inside content `c` are cleared when passed as
+   * input of type `input` in `call`.
+   */
+  predicate clearsContent(SummaryInput input, DataFlowCall call, Content c) {
+    viableCallable(call).(SummarizedCallable).clearsContent(input, c)
+  }
+}

csharp/ql/src/semmle/code/csharp/dataflow/internal/FlowSummarySpecific.qll

@@ -0,0 +1,156 @@
+/**
+ * Provides C# specific classes and predicates for definining flow summaries.
+ */
+
+private import csharp
+private import semmle.code.csharp.frameworks.system.linq.Expressions
+
+module Private {
+  private import Public
+  private import DataFlowPrivate as DataFlowPrivate
+  private import DataFlowPublic as DataFlowPublic
+  private import FlowSummaryImpl as Impl
+  private import DataFlowDispatch
+  private import semmle.code.csharp.Unification
+
+  class Content = DataFlowPublic::Content;
+
+  class DataFlowType = DataFlowPrivate::DataFlowType;
+
+  class Node = DataFlowPublic::Node;
+
+  class ParameterNode = DataFlowPublic::ParameterNode;
+
+  class ArgumentNode = DataFlowPrivate::ArgumentNode;
+
+  class ReturnNode = DataFlowPrivate::ReturnNode;
+
+  class OutNode = DataFlowPrivate::OutNode;
+
+  private class NodeImpl = DataFlowPrivate::NodeImpl;
+
+  predicate accessPathLimit = DataFlowPrivate::accessPathLimit/0;
+
+  predicate hasDelegateArgumentPosition(SummarizableCallable c, int i) {
+    exists(DelegateType dt |
+      dt = c.getParameter(i).getType().(SystemLinqExpressions::DelegateExtType).getDelegateType()
+    |
+      not dt.getReturnType() instanceof VoidType
+    )
+  }
+
+  predicate hasDelegateArgumentPosition2(SummarizableCallable c, int i, int j) {
+    exists(DelegateType dt |
+      dt = c.getParameter(i).getType().(SystemLinqExpressions::DelegateExtType).getDelegateType()
+    |
+      exists(dt.getParameter(j))
+    )
+  }
+
+  newtype TSummaryInput =
+    TParameterSummaryInput(int i) { i in [-1, any(Parameter p).getPosition()] } or
+    TDelegateSummaryInput(int i) { hasDelegateArgumentPosition(_, i) }
+
+  newtype TSummaryOutput =
+    TReturnSummaryOutput() or
+    TParameterSummaryOutput(int i) {
+      i in [-1, any(SummarizableCallable c).getAParameter().getPosition()]
+    } or
+    TDelegateSummaryOutput(int i, int j) { hasDelegateArgumentPosition2(_, i, j) }
+
+  /** Gets the return kind that matches `sink`, if any. */
+  ReturnKind toReturnKind(SummaryOutput output) {
+    output = TReturnSummaryOutput() and
+    result instanceof NormalReturnKind
+    or
+    exists(int i | output = TParameterSummaryOutput(i) |
+      i = -1 and
+      result instanceof QualifierReturnKind
+      or
+      i = result.(OutRefReturnKind).getPosition()
+    )
+  }
+
+  /** Gets the input node for `c` of type `input`. */
+  NodeImpl inputNode(SummarizableCallable c, SummaryInput input) {
+    exists(int i |
+      input = TParameterSummaryInput(i) and
+      result = DataFlowPrivate::TSummaryParameterNode(c, i)
+    )
+    or
+    exists(int i |
+      input = TDelegateSummaryInput(i) and
+      result = DataFlowPrivate::TSummaryDelegateOutNode(c, i)
+    )
+  }
+
+  /** Gets the output node for `c` of type `output`. */
+  NodeImpl outputNode(SummarizableCallable c, SummaryOutput output) {
+    result = DataFlowPrivate::TSummaryReturnNode(c, toReturnKind(output))
+    or
+    exists(int i, int j |
+      output = TDelegateSummaryOutput(i, j) and
+      result = DataFlowPrivate::TSummaryDelegateArgumentNode(c, i, j)
+    )
+  }
+
+  /** Gets the internal summary node for the given values. */
+  Node internalNode(SummarizableCallable c, Impl::Private::SummaryInternalNodeState state) {
+    result = DataFlowPrivate::TSummaryInternalNode(c, state)
+  }
+
+  /** Gets the type of content `c`. */
+  pragma[noinline]
+  DataFlowType getContentType(Content c) {
+    exists(Type t | result = Gvn::getGlobalValueNumber(t) |
+      t = c.(DataFlowPublic::FieldContent).getField().getType()
+      or
+      t = c.(DataFlowPublic::PropertyContent).getProperty().getType()
+      or
+      c instanceof DataFlowPublic::ElementContent and
+      t instanceof ObjectType // we don't know what the actual element type is
+    )
+  }
+}
+
+module Public {
+  private import Private
+
+  /** An unbound callable. */
+  class SummarizableCallable extends Callable {
+    SummarizableCallable() { this = this.getSourceDeclaration() }
+  }
+
+  /** A flow-summary input specification. */
+  class SummaryInput extends TSummaryInput {
+    /** Gets a textual representation of this input specification. */
+    final string toString() {
+      exists(int i |
+        this = TParameterSummaryInput(i) and
+        if i = -1 then result = "this parameter" else result = "parameter " + i
+        or
+        this = TDelegateSummaryInput(i) and
+        result = "deleget output from parameter " + i
+      )
+    }
+  }
+
+  /** A flow-summary output specification. */
+  class SummaryOutput extends TSummaryOutput {
+    /** Gets a textual representation of this flow sink specification. */
+    final string toString() {
+      this = TReturnSummaryOutput() and
+      result = "return"
+      or
+      exists(int i |
+        this = TParameterSummaryOutput(i) and
+        if i = -1 then result = "this parameter" else result = "parameter " + i
+      )
+      or
+      exists(int delegateIndex, int parameterIndex |
+        this = TDelegateSummaryOutput(delegateIndex, parameterIndex) and
+        result = "parameter " + parameterIndex + " of delegate parameter " + delegateIndex
+      )
+    }
+  }
+}

csharp/ql/src/semmle/code/csharp/dataflow/internal/TaintTrackingPrivate.qll

@@ -1,10 +1,10 @@
 private import csharp
 private import TaintTrackingPublic
 private import DataFlowImplCommon
+private import FlowSummaryImpl as FlowSummaryImpl
 private import semmle.code.csharp.Caching
 private import semmle.code.csharp.dataflow.internal.DataFlowPrivate
 private import semmle.code.csharp.dataflow.internal.ControlFlowReachability
-private import semmle.code.csharp.dataflow.LibraryTypeDataFlow
 private import semmle.code.csharp.dispatch.Dispatch
 private import semmle.code.csharp.commons.ComparisonTest
 private import cil
@@ -112,8 +112,6 @@ private predicate localTaintStepCommon(DataFlow::Node nodeFrom, DataFlow::Node n
 
 cached
 private module Cached {
-  private import Summaries
-
   /**
    * Holds if taint propagates from `nodeFrom` to `nodeTo` in exactly one local
    * (intra-procedural) step.
@@ -130,19 +128,19 @@ private module Cached {
     (
       // Simple flow through library code is included in the exposed local
       // step relation, even though flow is technically inter-procedural
-      summaryThroughStep(nodeFrom, nodeTo, false)
+      FlowSummaryImpl::Private::throughStep(nodeFrom, nodeTo, false)
       or
       // Taint collection by adding a tainted element
       exists(DataFlow::ElementContent c |
         storeStep(nodeFrom, c, nodeTo)
         or
-        summarySetterStep(nodeFrom, c, nodeTo)
+        FlowSummaryImpl::Private::setterStep(nodeFrom, c, nodeTo)
       )
       or
       exists(DataFlow::Content c |
         readStep(nodeFrom, c, nodeTo)
         or
-        summaryGetterStep(nodeFrom, c, nodeTo)
+        FlowSummaryImpl::Private::getterStep(nodeFrom, c, nodeTo)
       |
         // Taint members
         c = any(TaintedMember m).(FieldOrProperty).getContent()
@@ -169,7 +167,7 @@ private module Cached {
     // tracking configurations where the source is a collection
     readStep(nodeFrom, TElementContent(), nodeTo)
     or
-    summaryLocalStep(nodeFrom, nodeTo, false)
+    FlowSummaryImpl::Private::localStep(nodeFrom, nodeTo, false)
     or
     nodeTo = nodeFrom.(DataFlow::NonLocalJumpNode).getAJumpSuccessor(false)
   }

csharp/ql/test/library-tests/dataflow/library/FlowSummaries.ql

@@ -0,0 +1,6 @@
+import semmle.code.csharp.dataflow.FlowSummary
+import semmle.code.csharp.dataflow.FlowSummary::TestOutput
+
+private class IncludeEFSummarizedCallable extends RelevantSummarizedCallable {
+  IncludeEFSummarizedCallable() { this instanceof SummarizedCallable }
+}

csharp/ql/test/library-tests/dataflow/library/LibraryTypeDataFlow.ql

@@ -1,41 +0,0 @@
-import csharp
-import semmle.code.csharp.dataflow.LibraryTypeDataFlow
-
-query predicate callableFlow(string callable, string flow, boolean preservesValue) {
-  exists(LibraryTypeDataFlow x, CallableFlowSource source, CallableFlowSink sink, Callable c |
-    c.getDeclaringType().isPublic() and
-    callable = c.getQualifiedNameWithTypes() and
-    flow = source + " -> " + sink and
-    // Remove certain results to make the test output consistent
-    // between different versions of .NET Core.
-    not callable = "System.IO.FileStream.CopyToAsync(Stream, int, CancellationToken)"
-  |
-    x.callableFlow(source, sink, c, preservesValue)
-    or
-    x.callableFlow(source, AccessPath::empty(), sink, AccessPath::empty(), c, preservesValue)
-  )
-}
-
-query predicate callableFlowAccessPath(string callable, string flow, boolean preservesValue) {
-  exists(
-    LibraryTypeDataFlow x, CallableFlowSource source, AccessPath sourceAp, CallableFlowSink sink,
-    AccessPath sinkAp, Callable c
-  |
-    c.getDeclaringType().isPublic() and
-    x.callableFlow(source, sourceAp, sink, sinkAp, c, preservesValue) and
-    callable = c.getQualifiedNameWithTypes() and
-    flow = source + " [" + sourceAp + "] -> " + sink + " [" + sinkAp + "]"
-  |
-    sourceAp.length() > 0
-    or
-    sinkAp.length() > 0
-  )
-}
-
-query predicate clearsContent(string callable, CallableFlowSource source, string content) {
-  exists(LibraryTypeDataFlow x, Callable callable0, DataFlow::Content content0 |
-    x.clearsContent(source, content0, callable0) and
-    callable = callable0.getQualifiedNameWithTypes() and
-    content = content0.toString()
-  )
-}

csharp/ql/test/library-tests/frameworks/test/Test.ql

@@ -13,5 +13,6 @@ where
   not framework = "SourceDeclarationCallable" and
   not framework = "SourceDeclarationMethod" and
   not framework = "NonConstructedMethod" and
-  not framework = "RuntimeInstanceMethod"
+  not framework = "RuntimeInstanceMethod" and
+  not framework = "SummarizableMethod"
 select e, type, framework