Java: Adopt shared flow summary library and refactor data-flow nodes.

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

@@ -0,0 +1,49 @@
+/**
+ * Provides classes and predicates for definining flow summaries.
+ */
+
+import java
+private import internal.FlowSummaryImpl as Impl
+private import internal.DataFlowDispatch
+private import internal.DataFlowPrivate
+
+// import all instances below
+private module Summaries { }
+
+class SummaryComponent = Impl::Public::SummaryComponent;
+
+/** Provides predicates for constructing summary components. */
+module SummaryComponent {
+  import Impl::Public::SummaryComponent
+
+  /** Gets a summary component that represents a qualifier. */
+  SummaryComponent qualifier() { result = argument(-1) }
+
+  /** Gets a summary component for field `f`. */
+  SummaryComponent field(Field f) { result = content(any(FieldContent c | c.getField() = f)) }
+
+  /** Gets a summary component that represents the return value of a call. */
+  SummaryComponent return() { result = return(_) }
+}
+
+class SummaryComponentStack = Impl::Public::SummaryComponentStack;
+
+/** Provides predicates for constructing stacks of summary components. */
+module SummaryComponentStack {
+  import Impl::Public::SummaryComponentStack
+
+  /** Gets a singleton stack representing a qualifier. */
+  SummaryComponentStack qualifier() { result = singleton(SummaryComponent::qualifier()) }
+
+  /** Gets a stack representing a field `f` of `object`. */
+  SummaryComponentStack fieldOf(Field f, SummaryComponentStack object) {
+    result = push(SummaryComponent::field(f), object)
+  }
+
+  /** Gets a singleton stack representing a (normal) return. */
+  SummaryComponentStack return() { result = singleton(SummaryComponent::return()) }
+}
+
+class SummarizedCallable = Impl::Public::SummarizedCallable;
+
+class RequiredSummaryComponentStack = Impl::Public::RequiredSummaryComponentStack;

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

@@ -2,9 +2,17 @@ private import java
 private import DataFlowPrivate
 private import DataFlowUtil
 private import semmle.code.java.dataflow.InstanceAccess
-import semmle.code.java.dispatch.VirtualDispatch
+private import semmle.code.java.dataflow.FlowSummary
+private import semmle.code.java.dispatch.VirtualDispatch as VirtualDispatch
 
 private module DispatchImpl {
+  /** Gets a viable implementation of the target of the given `Call`. */
+  Callable viableCallable(Call c) {
+    result = VirtualDispatch::viableCallable(c)
+    or
+    result.(SummarizedCallable) = c.getCallee().getSourceDeclaration()
+  }
+
   /**
    * Holds if the set of viable implementations that can be called by `ma`
    * might be improved by knowing the call context. This is the case if the
@@ -12,7 +20,7 @@ private module DispatchImpl {
    */
   private predicate mayBenefitFromCallContext(MethodAccess ma, Callable c, int i) {
     exists(Parameter p |
-      2 <= strictcount(viableImpl(ma)) and
+      2 <= strictcount(VirtualDispatch::viableImpl(ma)) and
       ma.getQualifier().(VarAccess).getVariable() = p and
       p.getPosition() = i and
       c.getAParameter() = p and
@@ -21,7 +29,7 @@ private module DispatchImpl {
     )
     or
     exists(OwnInstanceAccess ia |
-      2 <= strictcount(viableImpl(ma)) and
+      2 <= strictcount(VirtualDispatch::viableImpl(ma)) and
       (ia.isExplicit(ma.getQualifier()) or ia.isImplicitMethodQualifier(ma)) and
       i = -1 and
       c = ma.getEnclosingCallable()
@@ -60,7 +68,7 @@ private module DispatchImpl {
         or
         ctx.getArgument(i) = arg
       |
-        src = variableTrack(arg) and
+        src = VirtualDispatch::variableTrack(arg) and
         srctype = getPreciseType(src) and
         if src instanceof ClassInstanceExpr then exact = true else exact = false
       )
@@ -93,18 +101,18 @@ private module DispatchImpl {
    * restricted to those `ma`s for which a context might make a difference.
    */
   Method viableImplInCallContext(MethodAccess ma, Call ctx) {
-    result = viableImpl(ma) and
+    result = VirtualDispatch::viableImpl(ma) and
     exists(int i, Callable c, Method def, RefType t, boolean exact |
       mayBenefitFromCallContext(ma, c, i) and
       c = viableCallable(ctx) and
       contextArgHasType(ctx, i, t, exact) and
       ma.getMethod() = def
     |
-      exact = true and result = exactMethodImpl(def, t.getSourceDeclaration())
+      exact = true and result = VirtualDispatch::exactMethodImpl(def, t.getSourceDeclaration())
       or
       exact = false and
       exists(RefType t2 |
-        result = viableMethodImpl(def, t.getSourceDeclaration(), t2) and
+        result = VirtualDispatch::viableMethodImpl(def, t.getSourceDeclaration(), t2) and
         not failsUnification(t, t2)
       )
     )
@@ -117,7 +125,7 @@ private module DispatchImpl {
 
   pragma[noinline]
   private predicate unificationTargetRight(ParameterizedType t2, GenericType g) {
-    exists(viableMethodImpl(_, _, t2)) and t2.getGenericType() = g
+    exists(VirtualDispatch::viableMethodImpl(_, _, t2)) and t2.getGenericType() = g
   }
 
   private predicate unificationTargets(Type t1, Type t2) {

java/ql/src/semmle/code/java/dataflow/internal/DataFlowNodes.qll

@@ -0,0 +1,445 @@
+private import java
+private import semmle.code.java.dataflow.InstanceAccess
+private import semmle.code.java.dataflow.FlowSummary
+private import semmle.code.java.dataflow.TypeFlow
+private import DataFlowPrivate
+private import FlowSummaryImpl as FlowSummaryImpl
+
+cached
+private module Cached {
+  cached
+  newtype TNode =
+    TExprNode(Expr e) {
+      not e.getType() instanceof VoidType and
+      not e.getParent*() instanceof Annotation
+    } or
+    TExplicitParameterNode(Parameter p) {
+      exists(p.getCallable().getBody()) or p.getCallable() instanceof SummarizedCallable
+    } or
+    TImplicitVarargsArray(Call c) {
+      c.getCallee().isVarargs() and
+      not exists(Argument arg | arg.getCall() = c and arg.isExplicitVarargsArray())
+    } or
+    TInstanceParameterNode(Callable c) {
+      (exists(c.getBody()) or c instanceof SummarizedCallable) and
+      not c.isStatic()
+    } or
+    TImplicitInstanceAccess(InstanceAccessExt ia) { not ia.isExplicit(_) } or
+    TMallocNode(ClassInstanceExpr cie) or
+    TExplicitExprPostUpdate(Expr e) {
+      explicitInstanceArgument(_, e)
+      or
+      e instanceof Argument and not e.getType() instanceof ImmutableType
+      or
+      exists(FieldAccess fa | fa.getField() instanceof InstanceField and e = fa.getQualifier())
+      or
+      exists(ArrayAccess aa | e = aa.getArray())
+    } or
+    TImplicitExprPostUpdate(InstanceAccessExt ia) {
+      implicitInstanceArgument(_, ia)
+      or
+      exists(FieldAccess fa |
+        fa.getField() instanceof InstanceField and ia.isImplicitFieldQualifier(fa)
+      )
+    } or
+    TSummaryInternalNode(SummarizedCallable c, FlowSummaryImpl::Private::SummaryNodeState state) {
+      FlowSummaryImpl::Private::summaryNodeRange(c, state)
+    }
+
+  cached
+  predicate summaryOutNodeCached(DataFlowCall c, Node out) {
+    FlowSummaryImpl::Private::summaryOutNode(c, out, _)
+  }
+
+  cached
+  predicate summaryArgumentNodeCached(DataFlowCall c, Node arg, int i) {
+    FlowSummaryImpl::Private::summaryArgumentNode(c, arg, i)
+  }
+
+  cached
+  predicate summaryPostUpdateNodeCached(Node post, ParameterNode pre) {
+    FlowSummaryImpl::Private::summaryPostUpdateNode(post, pre)
+  }
+
+  cached
+  predicate summaryReturnNodeCached(Node ret) {
+    FlowSummaryImpl::Private::summaryReturnNode(ret, _)
+  }
+}
+
+private import Cached
+
+private predicate explicitInstanceArgument(Call call, Expr instarg) {
+  call instanceof MethodAccess and
+  instarg = call.getQualifier() and
+  not call.getCallee().isStatic()
+}
+
+private predicate implicitInstanceArgument(Call call, InstanceAccessExt ia) {
+  ia.isImplicitMethodQualifier(call) or
+  ia.isImplicitThisConstructorArgument(call)
+}
+
+module Public {
+  /**
+   * An element, viewed as a node in a data flow graph. Either an expression,
+   * a parameter, or an implicit varargs array creation.
+   */
+  class Node extends TNode {
+    /** Gets a textual representation of this element. */
+    string toString() { none() }
+
+    /** Gets the source location for this element. */
+    Location getLocation() { none() }
+
+    /** Gets the expression corresponding to this node, if any. */
+    Expr asExpr() { result = this.(ExprNode).getExpr() }
+
+    /** Gets the parameter corresponding to this node, if any. */
+    Parameter asParameter() { result = this.(ExplicitParameterNode).getParameter() }
+
+    /** Gets the type of this node. */
+    Type getType() {
+      result = this.asExpr().getType()
+      or
+      result = this.asParameter().getType()
+      or
+      exists(Parameter p |
+        result = p.getType() and
+        p.isVarargs() and
+        p = this.(ImplicitVarargsArray).getCall().getCallee().getAParameter()
+      )
+      or
+      result = this.(InstanceParameterNode).getCallable().getDeclaringType()
+      or
+      result = this.(ImplicitInstanceAccess).getInstanceAccess().getType()
+      or
+      result = this.(MallocNode).getClassInstanceExpr().getType()
+      or
+      result = this.(ImplicitPostUpdateNode).getPreUpdateNode().getType()
+    }
+
+    /** Gets the callable in which this node occurs. */
+    Callable getEnclosingCallable() {
+      result = this.asExpr().getEnclosingCallable() or
+      result = this.asParameter().getCallable() or
+      result = this.(ImplicitVarargsArray).getCall().getEnclosingCallable() or
+      result = this.(InstanceParameterNode).getCallable() or
+      result = this.(ImplicitInstanceAccess).getInstanceAccess().getEnclosingCallable() or
+      result = this.(MallocNode).getClassInstanceExpr().getEnclosingCallable() or
+      result = this.(ImplicitPostUpdateNode).getPreUpdateNode().getEnclosingCallable() or
+      this = TSummaryInternalNode(result, _)
+    }
+
+    private Type getImprovedTypeBound() {
+      exprTypeFlow(this.asExpr(), result, _) or
+      result = this.(ImplicitPostUpdateNode).getPreUpdateNode().getImprovedTypeBound()
+    }
+
+    /**
+     * Gets an upper bound on the type of this node.
+     */
+    Type getTypeBound() {
+      result = getImprovedTypeBound()
+      or
+      result = getType() and not exists(getImprovedTypeBound())
+    }
+
+    /**
+     * Holds if this element is at the specified location.
+     * The location spans column `startcolumn` of line `startline` to
+     * column `endcolumn` of line `endline` in file `filepath`.
+     * For more information, see
+     * [Locations](https://help.semmle.com/QL/learn-ql/ql/locations.html).
+     */
+    predicate hasLocationInfo(
+      string filepath, int startline, int startcolumn, int endline, int endcolumn
+    ) {
+      getLocation().hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn)
+    }
+  }
+
+  /**
+   * An expression, viewed as a node in a data flow graph.
+   */
+  class ExprNode extends Node, TExprNode {
+    Expr expr;
+
+    ExprNode() { this = TExprNode(expr) }
+
+    override string toString() { result = expr.toString() }
+
+    override Location getLocation() { result = expr.getLocation() }
+
+    /** Gets the expression corresponding to this node. */
+    Expr getExpr() { result = expr }
+  }
+
+  /** Gets the node corresponding to `e`. */
+  ExprNode exprNode(Expr e) { result.getExpr() = e }
+
+  /** An explicit or implicit parameter. */
+  abstract class ParameterNode extends Node {
+    /**
+     * Holds if this node is the parameter of `c` at the specified (zero-based)
+     * position. The implicit `this` parameter is considered to have index `-1`.
+     */
+    abstract predicate isParameterOf(Callable c, int pos);
+  }
+
+  /**
+   * A parameter, viewed as a node in a data flow graph.
+   */
+  class ExplicitParameterNode extends ParameterNode, TExplicitParameterNode {
+    Parameter param;
+
+    ExplicitParameterNode() { this = TExplicitParameterNode(param) }
+
+    override string toString() { result = param.toString() }
+
+    override Location getLocation() { result = param.getLocation() }
+
+    /** Gets the parameter corresponding to this node. */
+    Parameter getParameter() { result = param }
+
+    override predicate isParameterOf(Callable c, int pos) { c.getParameter(pos) = param }
+  }
+
+  /** Gets the node corresponding to `p`. */
+  ExplicitParameterNode parameterNode(Parameter p) { result.getParameter() = p }
+
+  /**
+   * An implicit varargs array creation expression.
+   *
+   * A call `f(x1, x2)` to a method `f(A... xs)` desugars to `f(new A[]{x1, x2})`,
+   * and this node corresponds to such an implicit array creation.
+   */
+  class ImplicitVarargsArray extends Node, TImplicitVarargsArray {
+    Call call;
+
+    ImplicitVarargsArray() { this = TImplicitVarargsArray(call) }
+
+    override string toString() { result = "new ..[] { .. }" }
+
+    override Location getLocation() { result = call.getLocation() }
+
+    /** Gets the call containing this varargs array creation argument. */
+    Call getCall() { result = call }
+  }
+
+  /**
+   * An instance parameter for an instance method or constructor.
+   */
+  class InstanceParameterNode extends ParameterNode, TInstanceParameterNode {
+    Callable callable;
+
+    InstanceParameterNode() { this = TInstanceParameterNode(callable) }
+
+    override string toString() { result = "parameter this" }
+
+    override Location getLocation() { result = callable.getLocation() }
+
+    /** Gets the callable containing this `this` parameter. */
+    Callable getCallable() { result = callable }
+
+    override predicate isParameterOf(Callable c, int pos) { callable = c and pos = -1 }
+  }
+
+  /**
+   * An implicit read of `this` or `A.this`.
+   */
+  class ImplicitInstanceAccess extends Node, TImplicitInstanceAccess {
+    InstanceAccessExt ia;
+
+    ImplicitInstanceAccess() { this = TImplicitInstanceAccess(ia) }
+
+    override string toString() { result = ia.toString() }
+
+    override Location getLocation() { result = ia.getLocation() }
+
+    /** Gets the instance access corresponding to this node. */
+    InstanceAccessExt getInstanceAccess() { result = ia }
+  }
+
+  /**
+   * A node associated with an object after an operation that might have
+   * changed its state.
+   *
+   * This can be either the argument to a callable after the callable returns
+   * (which might have mutated the argument), or the qualifier of a field after
+   * an update to the field.
+   *
+   * Nodes corresponding to AST elements, for example `ExprNode`, usually refer
+   * to the value before the update with the exception of `ClassInstanceExpr`,
+   * which represents the value after the constructor has run.
+   */
+  abstract class PostUpdateNode extends Node {
+    /**
+     * Gets the node before the state update.
+     */
+    abstract Node getPreUpdateNode();
+  }
+
+  /**
+   * Gets the node that occurs as the qualifier of `fa`.
+   */
+  Node getFieldQualifier(FieldAccess fa) {
+    fa.getField() instanceof InstanceField and
+    (
+      result.asExpr() = fa.getQualifier() or
+      result.(ImplicitInstanceAccess).getInstanceAccess().isImplicitFieldQualifier(fa)
+    )
+  }
+
+  /** Gets the instance argument of a non-static call. */
+  Node getInstanceArgument(Call call) {
+    result.(MallocNode).getClassInstanceExpr() = call or
+    explicitInstanceArgument(call, result.asExpr()) or
+    implicitInstanceArgument(call, result.(ImplicitInstanceAccess).getInstanceAccess())
+  }
+}
+
+private import Public
+
+private class NewExpr extends PostUpdateNode, TExprNode {
+  NewExpr() { exists(ClassInstanceExpr cie | this = TExprNode(cie)) }
+
+  override Node getPreUpdateNode() { this = TExprNode(result.(MallocNode).getClassInstanceExpr()) }
+}
+
+/**
+ * A `PostUpdateNode` that is not a `ClassInstanceExpr`.
+ */
+abstract private class ImplicitPostUpdateNode extends PostUpdateNode {
+  override Location getLocation() { result = getPreUpdateNode().getLocation() }
+
+  override string toString() { result = getPreUpdateNode().toString() + " [post update]" }
+}
+
+private class ExplicitExprPostUpdate extends ImplicitPostUpdateNode, TExplicitExprPostUpdate {
+  override Node getPreUpdateNode() { this = TExplicitExprPostUpdate(result.asExpr()) }
+}
+
+private class ImplicitExprPostUpdate extends ImplicitPostUpdateNode, TImplicitExprPostUpdate {
+  override Node getPreUpdateNode() {
+    this = TImplicitExprPostUpdate(result.(ImplicitInstanceAccess).getInstanceAccess())
+  }
+}
+
+module Private {
+  /**
+   * A data flow node that occurs as the argument of a call and is passed as-is
+   * to the callable. Arguments that are wrapped in an implicit varargs array
+   * creation are not included, but the implicitly created array is.
+   * Instance arguments are also included.
+   */
+  class ArgumentNode extends Node {
+    ArgumentNode() {
+      exists(Argument arg | this.asExpr() = arg | not arg.isVararg())
+      or
+      this instanceof ImplicitVarargsArray
+      or
+      this = getInstanceArgument(_)
+      or
+      this.(SummaryNode).isArgumentOf(_, _)
+    }
+
+    /**
+     * Holds if this argument occurs at the given position in the given call.
+     * The instance argument is considered to have index `-1`.
+     */
+    predicate argumentOf(DataFlowCall call, int pos) {
+      exists(Argument arg | this.asExpr() = arg | call = arg.getCall() and pos = arg.getPosition())
+      or
+      call = this.(ImplicitVarargsArray).getCall() and
+      pos = call.getCallee().getNumberOfParameters() - 1
+      or
+      pos = -1 and this = getInstanceArgument(call)
+      or
+      this.(SummaryNode).isArgumentOf(call, pos)
+    }
+
+    /** Gets the call in which this node is an argument. */
+    DataFlowCall getCall() { this.argumentOf(result, _) }
+  }
+
+  /** A data flow node that occurs as the result of a `ReturnStmt`. */
+  class ReturnNode extends Node {
+    ReturnNode() {
+      exists(ReturnStmt ret | this.asExpr() = ret.getResult()) or
+      this.(SummaryNode).isReturn()
+    }
+
+    /** Gets the kind of this returned value. */
+    ReturnKind getKind() { any() }
+  }
+
+  /** A data flow node that represents the output of a call. */
+  class OutNode extends Node {
+    OutNode() {
+      this.asExpr() instanceof MethodAccess
+      or
+      this.(SummaryNode).isOut(_)
+    }
+
+    /** Gets the underlying call. */
+    DataFlowCall getCall() {
+      result = this.asExpr()
+      or
+      this.(SummaryNode).isOut(result)
+    }
+  }
+
+  /**
+   * A data-flow node used to model flow summaries.
+   */
+  class SummaryNode extends Node, TSummaryInternalNode {
+    private SummarizedCallable c;
+    private FlowSummaryImpl::Private::SummaryNodeState state;
+
+    SummaryNode() { this = TSummaryInternalNode(c, state) }
+
+    override Location getLocation() { result = c.getLocation() }
+
+    override string toString() { result = "[summary] " + state + " in " + c }
+
+    /** Holds if this summary node is the `i`th argument of `call`. */
+    predicate isArgumentOf(DataFlowCall call, int i) { summaryArgumentNodeCached(call, this, i) }
+
+    /** Holds if this summary node is a return node. */
+    predicate isReturn() { summaryReturnNodeCached(this) }
+
+    /** Holds if this summary node is an out node for `call`. */
+    predicate isOut(DataFlowCall call) { summaryOutNodeCached(call, this) }
+  }
+
+  SummaryNode getSummaryNode(SummarizedCallable c, FlowSummaryImpl::Private::SummaryNodeState state) {
+    result = TSummaryInternalNode(c, state)
+  }
+}
+
+private import Private
+
+/**
+ * A node that corresponds to the value of a `ClassInstanceExpr` before the
+ * constructor has run.
+ */
+private class MallocNode extends Node, TMallocNode {
+  ClassInstanceExpr cie;
+
+  MallocNode() { this = TMallocNode(cie) }
+
+  override string toString() { result = cie.toString() + " [pre constructor]" }
+
+  override Location getLocation() { result = cie.getLocation() }
+
+  ClassInstanceExpr getClassInstanceExpr() { result = cie }
+}
+
+private class SummaryPostUpdateNode extends SummaryNode, PostUpdateNode {
+  private Node pre;
+
+  SummaryPostUpdateNode() { summaryPostUpdateNodeCached(this, pre) }
+
+  override Node getPreUpdateNode() { result = pre }
+}

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

@@ -4,7 +4,8 @@ private import DataFlowImplCommon
 private import DataFlowDispatch
 private import semmle.code.java.controlflow.Guards
 private import semmle.code.java.dataflow.SSA
-private import semmle.code.java.dataflow.TypeFlow
+private import FlowSummaryImpl as FlowSummaryImpl
+import DataFlowNodes::Private
 
 private newtype TReturnKind = TNormalReturnKind()
 
@@ -26,54 +27,6 @@ OutNode getAnOutNode(DataFlowCall call, ReturnKind kind) {
   kind = TNormalReturnKind()
 }
 
-/**
- * A data flow node that occurs as the argument of a call and is passed as-is
- * to the callable. Arguments that are wrapped in an implicit varargs array
- * creation are not included, but the implicitly created array is.
- * Instance arguments are also included.
- */
-class ArgumentNode extends Node {
-  ArgumentNode() {
-    exists(Argument arg | this.asExpr() = arg | not arg.isVararg())
-    or
-    this instanceof ImplicitVarargsArray
-    or
-    this = getInstanceArgument(_)
-  }
-
-  /**
-   * Holds if this argument occurs at the given position in the given call.
-   * The instance argument is considered to have index `-1`.
-   */
-  predicate argumentOf(DataFlowCall call, int pos) {
-    exists(Argument arg | this.asExpr() = arg | call = arg.getCall() and pos = arg.getPosition())
-    or
-    call = this.(ImplicitVarargsArray).getCall() and
-    pos = call.getCallee().getNumberOfParameters() - 1
-    or
-    pos = -1 and this = getInstanceArgument(call)
-  }
-
-  /** Gets the call in which this node is an argument. */
-  DataFlowCall getCall() { this.argumentOf(result, _) }
-}
-
-/** A data flow node that occurs as the result of a `ReturnStmt`. */
-class ReturnNode extends ExprNode {
-  ReturnNode() { exists(ReturnStmt ret | this.getExpr() = ret.getResult()) }
-
-  /** Gets the kind of this returned value. */
-  ReturnKind getKind() { any() }
-}
-
-/** A data flow node that represents the output of a call. */
-class OutNode extends ExprNode {
-  OutNode() { this.getExpr() instanceof MethodAccess }
-
-  /** Gets the underlying call. */
-  DataFlowCall getCall() { result = this.getExpr() }
-}
-
 /**
  * Holds if data can flow from `node1` to `node2` through a static field.
  */
@@ -147,7 +100,7 @@ class Content extends TContent {
   }
 }
 
-private class FieldContent extends Content, TFieldContent {
+class FieldContent extends Content, TFieldContent {
   InstanceField f;
 
   FieldContent() { this = TFieldContent(f) }
@@ -161,11 +114,11 @@ private class FieldContent extends Content, TFieldContent {
   }
 }
 
-private class CollectionContent extends Content, TCollectionContent {
+class CollectionContent extends Content, TCollectionContent {
   override string toString() { result = "collection" }
 }
 
-private class ArrayContent extends Content, TArrayContent {
+class ArrayContent extends Content, TArrayContent {
   override string toString() { result = "array" }
 }
 
@@ -180,6 +133,8 @@ predicate storeStep(Node node1, Content f, PostUpdateNode node2) {
     node2.getPreUpdateNode() = getFieldQualifier(fa) and
     f.(FieldContent).getField() = fa.getField()
   )
+  or
+  FlowSummaryImpl::Private::Steps::summaryStoreStep(node1, f, node2)
 }
 
 /**
@@ -205,6 +160,8 @@ predicate readStep(Node node1, Content f, Node node2) {
     node1.asExpr() = get.getQualifier() and
     node2.asExpr() = get
   )
+  or
+  FlowSummaryImpl::Private::Steps::summaryReadStep(node1, f, node2)
 }
 
 /**
@@ -213,7 +170,14 @@ predicate readStep(Node node1, Content f, Node node2) {
  * in `x.f = newValue`.
  */
 predicate clearsContent(Node n, Content c) {
-  n = any(PostUpdateNode pun | storeStep(_, c, pun)).getPreUpdateNode()
+  c instanceof FieldContent and
+  (
+    n = any(PostUpdateNode pun | storeStep(_, c, pun)).getPreUpdateNode()
+    or
+    FlowSummaryImpl::Private::Steps::summaryStoresIntoArg(c, n)
+  )
+  or
+  FlowSummaryImpl::Private::Steps::summaryClearsContent(n, c)
 }
 
 /**
@@ -221,7 +185,7 @@ predicate clearsContent(Node n, Content c) {
  * possible flow. A single type is used for all numeric types to account for
  * numeric conversions, and otherwise the erasure is used.
  */
-private DataFlowType getErasedRepr(Type t) {
+DataFlowType getErasedRepr(Type t) {
   exists(Type e | e = t.getErasure() |
     if e instanceof NumericOrCharType
     then result.(BoxedType).getPrimitiveType().getName() = "double"
@@ -235,7 +199,11 @@ private DataFlowType getErasedRepr(Type t) {
 }
 
 pragma[noinline]
-DataFlowType getNodeType(Node n) { result = getErasedRepr(n.getTypeBound()) }
+DataFlowType getNodeType(Node n) {
+  result = getErasedRepr(n.getTypeBound())
+  or
+  result = FlowSummaryImpl::Private::summaryNodeType(n)
+}
 
 /** Gets a string representation of a type returned by `getErasedRepr`. */
 string ppReprType(Type t) {
@@ -337,7 +305,7 @@ predicate isImmutableOrUnobservable(Node n) {
 }
 
 /** Holds if `n` should be hidden from path explanations. */
-predicate nodeIsHidden(Node n) { none() }
+predicate nodeIsHidden(Node n) { n instanceof SummaryNode }
 
 class LambdaCallKind = Unit;
 

java/ql/src/semmle/code/java/dataflow/internal/DataFlowUtil.qll

@@ -5,280 +5,13 @@
 private import java
 private import DataFlowPrivate
 private import semmle.code.java.dataflow.SSA
-private import semmle.code.java.dataflow.TypeFlow
 private import semmle.code.java.controlflow.Guards
 private import semmle.code.java.dataflow.ExternalFlow
 private import semmle.code.java.dataflow.FlowSteps
+private import semmle.code.java.dataflow.FlowSummary
 import semmle.code.java.dataflow.InstanceAccess
-
-cached
-private newtype TNode =
-  TExprNode(Expr e) {
-    not e.getType() instanceof VoidType and
-    not e.getParent*() instanceof Annotation
-  } or
-  TExplicitParameterNode(Parameter p) { exists(p.getCallable().getBody()) } or
-  TImplicitVarargsArray(Call c) {
-    c.getCallee().isVarargs() and
-    not exists(Argument arg | arg.getCall() = c and arg.isExplicitVarargsArray())
-  } or
-  TInstanceParameterNode(Callable c) { exists(c.getBody()) and not c.isStatic() } or
-  TImplicitInstanceAccess(InstanceAccessExt ia) { not ia.isExplicit(_) } or
-  TMallocNode(ClassInstanceExpr cie) or
-  TExplicitExprPostUpdate(Expr e) {
-    explicitInstanceArgument(_, e)
-    or
-    e instanceof Argument and not e.getType() instanceof ImmutableType
-    or
-    exists(FieldAccess fa | fa.getField() instanceof InstanceField and e = fa.getQualifier())
-    or
-    exists(ArrayAccess aa | e = aa.getArray())
-  } or
-  TImplicitExprPostUpdate(InstanceAccessExt ia) {
-    implicitInstanceArgument(_, ia)
-    or
-    exists(FieldAccess fa |
-      fa.getField() instanceof InstanceField and ia.isImplicitFieldQualifier(fa)
-    )
-  }
-
-/**
- * An element, viewed as a node in a data flow graph. Either an expression,
- * a parameter, or an implicit varargs array creation.
- */
-class Node extends TNode {
-  /** Gets a textual representation of this element. */
-  string toString() { none() }
-
-  /** Gets the source location for this element. */
-  Location getLocation() { none() }
-
-  /** Gets the expression corresponding to this node, if any. */
-  Expr asExpr() { result = this.(ExprNode).getExpr() }
-
-  /** Gets the parameter corresponding to this node, if any. */
-  Parameter asParameter() { result = this.(ExplicitParameterNode).getParameter() }
-
-  /** Gets the type of this node. */
-  Type getType() {
-    result = this.asExpr().getType()
-    or
-    result = this.asParameter().getType()
-    or
-    exists(Parameter p |
-      result = p.getType() and
-      p.isVarargs() and
-      p = this.(ImplicitVarargsArray).getCall().getCallee().getAParameter()
-    )
-    or
-    result = this.(InstanceParameterNode).getCallable().getDeclaringType()
-    or
-    result = this.(ImplicitInstanceAccess).getInstanceAccess().getType()
-    or
-    result = this.(MallocNode).getClassInstanceExpr().getType()
-    or
-    result = this.(ImplicitPostUpdateNode).getPreUpdateNode().getType()
-  }
-
-  /** Gets the callable in which this node occurs. */
-  Callable getEnclosingCallable() {
-    result = this.asExpr().getEnclosingCallable() or
-    result = this.asParameter().getCallable() or
-    result = this.(ImplicitVarargsArray).getCall().getEnclosingCallable() or
-    result = this.(InstanceParameterNode).getCallable() or
-    result = this.(ImplicitInstanceAccess).getInstanceAccess().getEnclosingCallable() or
-    result = this.(MallocNode).getClassInstanceExpr().getEnclosingCallable() or
-    result = this.(ImplicitPostUpdateNode).getPreUpdateNode().getEnclosingCallable()
-  }
-
-  private Type getImprovedTypeBound() {
-    exprTypeFlow(this.asExpr(), result, _) or
-    result = this.(ImplicitPostUpdateNode).getPreUpdateNode().getImprovedTypeBound()
-  }
-
-  /**
-   * Gets an upper bound on the type of this node.
-   */
-  Type getTypeBound() {
-    result = getImprovedTypeBound()
-    or
-    result = getType() and not exists(getImprovedTypeBound())
-  }
-
-  /**
-   * Holds if this element is at the specified location.
-   * The location spans column `startcolumn` of line `startline` to
-   * column `endcolumn` of line `endline` in file `filepath`.
-   * For more information, see
-   * [Locations](https://help.semmle.com/QL/learn-ql/ql/locations.html).
-   */
-  predicate hasLocationInfo(
-    string filepath, int startline, int startcolumn, int endline, int endcolumn
-  ) {
-    getLocation().hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn)
-  }
-}
-
-/**
- * An expression, viewed as a node in a data flow graph.
- */
-class ExprNode extends Node, TExprNode {
-  Expr expr;
-
-  ExprNode() { this = TExprNode(expr) }
-
-  override string toString() { result = expr.toString() }
-
-  override Location getLocation() { result = expr.getLocation() }
-
-  /** Gets the expression corresponding to this node. */
-  Expr getExpr() { result = expr }
-}
-
-/** Gets the node corresponding to `e`. */
-ExprNode exprNode(Expr e) { result.getExpr() = e }
-
-/** An explicit or implicit parameter. */
-abstract class ParameterNode extends Node {
-  /**
-   * Holds if this node is the parameter of `c` at the specified (zero-based)
-   * position. The implicit `this` parameter is considered to have index `-1`.
-   */
-  abstract predicate isParameterOf(Callable c, int pos);
-}
-
-/**
- * A parameter, viewed as a node in a data flow graph.
- */
-class ExplicitParameterNode extends ParameterNode, TExplicitParameterNode {
-  Parameter param;
-
-  ExplicitParameterNode() { this = TExplicitParameterNode(param) }
-
-  override string toString() { result = param.toString() }
-
-  override Location getLocation() { result = param.getLocation() }
-
-  /** Gets the parameter corresponding to this node. */
-  Parameter getParameter() { result = param }
-
-  override predicate isParameterOf(Callable c, int pos) { c.getParameter(pos) = param }
-}
-
-/** Gets the node corresponding to `p`. */
-ExplicitParameterNode parameterNode(Parameter p) { result.getParameter() = p }
-
-/**
- * An implicit varargs array creation expression.
- *
- * A call `f(x1, x2)` to a method `f(A... xs)` desugars to `f(new A[]{x1, x2})`,
- * and this node corresponds to such an implicit array creation.
- */
-class ImplicitVarargsArray extends Node, TImplicitVarargsArray {
-  Call call;
-
-  ImplicitVarargsArray() { this = TImplicitVarargsArray(call) }
-
-  override string toString() { result = "new ..[] { .. }" }
-
-  override Location getLocation() { result = call.getLocation() }
-
-  /** Gets the call containing this varargs array creation argument. */
-  Call getCall() { result = call }
-}
-
-/**
- * An instance parameter for an instance method or constructor.
- */
-class InstanceParameterNode extends ParameterNode, TInstanceParameterNode {
-  Callable callable;
-
-  InstanceParameterNode() { this = TInstanceParameterNode(callable) }
-
-  override string toString() { result = "parameter this" }
-
-  override Location getLocation() { result = callable.getLocation() }
-
-  /** Gets the callable containing this `this` parameter. */
-  Callable getCallable() { result = callable }
-
-  override predicate isParameterOf(Callable c, int pos) { callable = c and pos = -1 }
-}
-
-/**
- * An implicit read of `this` or `A.this`.
- */
-class ImplicitInstanceAccess extends Node, TImplicitInstanceAccess {
-  InstanceAccessExt ia;
-
-  ImplicitInstanceAccess() { this = TImplicitInstanceAccess(ia) }
-
-  override string toString() { result = ia.toString() }
-
-  override Location getLocation() { result = ia.getLocation() }
-
-  InstanceAccessExt getInstanceAccess() { result = ia }
-}
-
-/**
- * A node that corresponds to the value of a `ClassInstanceExpr` before the
- * constructor has run.
- */
-private class MallocNode extends Node, TMallocNode {
-  ClassInstanceExpr cie;
-
-  MallocNode() { this = TMallocNode(cie) }
-
-  override string toString() { result = cie.toString() + " [pre constructor]" }
-
-  override Location getLocation() { result = cie.getLocation() }
-
-  ClassInstanceExpr getClassInstanceExpr() { result = cie }
-}
-
-/**
- * A node associated with an object after an operation that might have
- * changed its state.
- *
- * This can be either the argument to a callable after the callable returns
- * (which might have mutated the argument), or the qualifier of a field after
- * an update to the field.
- *
- * Nodes corresponding to AST elements, for example `ExprNode`, usually refer
- * to the value before the update with the exception of `ClassInstanceExpr`,
- * which represents the value after the constructor has run.
- */
-abstract class PostUpdateNode extends Node {
-  /**
-   * Gets the node before the state update.
-   */
-  abstract Node getPreUpdateNode();
-}
-
-private class NewExpr extends PostUpdateNode, TExprNode {
-  NewExpr() { exists(ClassInstanceExpr cie | this = TExprNode(cie)) }
-
-  override Node getPreUpdateNode() { this = TExprNode(result.(MallocNode).getClassInstanceExpr()) }
-}
-
-/**
- * A `PostUpdateNode` that is not a `ClassInstanceExpr`.
- */
-abstract private class ImplicitPostUpdateNode extends PostUpdateNode {
-  override Location getLocation() { result = getPreUpdateNode().getLocation() }
-
-  override string toString() { result = getPreUpdateNode().toString() + " [post update]" }
-}
-
-private class ExplicitExprPostUpdate extends ImplicitPostUpdateNode, TExplicitExprPostUpdate {
-  override Node getPreUpdateNode() { this = TExplicitExprPostUpdate(result.asExpr()) }
-}
-
-private class ImplicitExprPostUpdate extends ImplicitPostUpdateNode, TImplicitExprPostUpdate {
-  override Node getPreUpdateNode() {
-    this = TImplicitExprPostUpdate(result.(ImplicitInstanceAccess).getInstanceAccess())
-  }
-}
+private import FlowSummaryImpl as FlowSummaryImpl
+import DataFlowNodes::Public
 
 /** Holds if `n` is an access to an unqualified `this` at `cfgnode`. */
 private predicate thisAccess(Node n, ControlFlowNode cfgnode) {
@@ -363,7 +96,13 @@ predicate hasNonlocalValue(FieldRead fr) {
 /**
  * Holds if data can flow from `node1` to `node2` in one local step.
  */
-predicate localFlowStep(Node node1, Node node2) { simpleLocalFlowStep(node1, node2) }
+predicate localFlowStep(Node node1, Node node2) {
+  simpleLocalFlowStep(node1, node2)
+  or
+  // Simple flow through library code is included in the exposed local
+  // step relation, even though flow is technically inter-procedural
+  FlowSummaryImpl::Private::Steps::summaryThroughStep(node1, node2, true)
+}
 
 /**
  * INTERNAL: do not use.
@@ -411,33 +150,8 @@ predicate simpleLocalFlowStep(Node node1, Node node2) {
     node2.asExpr() = ma and
     node1.(ArgumentNode).argumentOf(ma, argNo)
   )
-}
-
-/**
- * Gets the node that occurs as the qualifier of `fa`.
- */
-Node getFieldQualifier(FieldAccess fa) {
-  fa.getField() instanceof InstanceField and
-  (
-    result.asExpr() = fa.getQualifier() or
-    result.(ImplicitInstanceAccess).getInstanceAccess().isImplicitFieldQualifier(fa)
-  )
-}
-
-private predicate explicitInstanceArgument(Call call, Expr instarg) {
-  call instanceof MethodAccess and instarg = call.getQualifier() and not call.getCallee().isStatic()
-}
-
-private predicate implicitInstanceArgument(Call call, InstanceAccessExt ia) {
-  ia.isImplicitMethodQualifier(call) or
-  ia.isImplicitThisConstructorArgument(call)
-}
-
-/** Gets the instance argument of a non-static call. */
-Node getInstanceArgument(Call call) {
-  result.(MallocNode).getClassInstanceExpr() = call or
-  explicitInstanceArgument(call, result.asExpr()) or
-  implicitInstanceArgument(call, result.(ImplicitInstanceAccess).getInstanceAccess())
+  or
+  FlowSummaryImpl::Private::Steps::summaryLocalStep(node1, node2, true)
 }
 
 /**

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

@@ -0,0 +1,674 @@
+/**
+ * Provides classes and predicates for defining flow summaries.
+ *
+ * The definitions in this file are language-independent, and language-specific
+ * definitions are passed in via the `DataFlowImplSpecific` and
+ * `FlowSummaryImplSpecific` modules.
+ */
+
+private import FlowSummaryImplSpecific
+private import DataFlowImplSpecific::Private
+private import DataFlowImplSpecific::Public
+
+/** Provides classes and predicates for defining flow summaries. */
+module Public {
+  private import Private
+
+  /**
+   * A component used in a flow summary.
+   *
+   * Either a parameter or an argument at a given position, a specific
+   * content type, or a return kind.
+   */
+  class SummaryComponent extends TSummaryComponent {
+    /** Gets a textual representation of this summary component. */
+    string toString() {
+      exists(Content c | this = TContentSummaryComponent(c) and result = c.toString())
+      or
+      exists(int i | this = TParameterSummaryComponent(i) and result = "parameter " + i)
+      or
+      exists(int i | this = TArgumentSummaryComponent(i) and result = "argument " + i)
+      or
+      exists(ReturnKind rk | this = TReturnSummaryComponent(rk) and result = "return (" + rk + ")")
+    }
+  }
+
+  /** Provides predicates for constructing summary components. */
+  module SummaryComponent {
+    /** Gets a summary component for content `c`. */
+    SummaryComponent content(Content c) { result = TContentSummaryComponent(c) }
+
+    /** Gets a summary component for parameter `i`. */
+    SummaryComponent parameter(int i) { result = TParameterSummaryComponent(i) }
+
+    /** Gets a summary component for argument `i`. */
+    SummaryComponent argument(int i) { result = TArgumentSummaryComponent(i) }
+
+    /** Gets a summary component for a return of kind `rk`. */
+    SummaryComponent return(ReturnKind rk) { result = TReturnSummaryComponent(rk) }
+  }
+
+  /**
+   * A (non-empty) stack of summary components.
+   *
+   * A stack is used to represent where data is read from (input) or where it
+   * is written to (output). For example, an input stack `[Field f, Argument 0]`
+   * means that data is read from field `f` from the `0`th argument, while an
+   * output stack `[Field g, Return]` means that data is written to the field
+   * `g` of the returned object.
+   */
+  class SummaryComponentStack extends TSummaryComponentStack {
+    /** Gets the head of this stack. */
+    SummaryComponent head() {
+      this = TSingletonSummaryComponentStack(result) or
+      this = TConsSummaryComponentStack(result, _)
+    }
+
+    /** Gets the tail of this stack, if any. */
+    SummaryComponentStack tail() { this = TConsSummaryComponentStack(_, result) }
+
+    /** Gets the length of this stack. */
+    int length() {
+      this = TSingletonSummaryComponentStack(_) and result = 1
+      or
+      result = 1 + this.tail().length()
+    }
+
+    /** Gets the stack obtained by dropping the first `i` elements, if any. */
+    SummaryComponentStack drop(int i) {
+      i = 0 and result = this
+      or
+      result = this.tail().drop(i - 1)
+    }
+
+    /** Holds if this stack contains summary component `c`. */
+    predicate contains(SummaryComponent c) { c = this.drop(_).head() }
+
+    /** Gets a textual representation of this stack. */
+    string toString() {
+      exists(SummaryComponent head, SummaryComponentStack tail |
+        head = this.head() and
+        tail = this.tail() and
+        result = head + " of " + tail
+      )
+      or
+      exists(SummaryComponent c |
+        this = TSingletonSummaryComponentStack(c) and
+        result = c.toString()
+      )
+    }
+  }
+
+  /** Provides predicates for constructing stacks of summary components. */
+  module SummaryComponentStack {
+    /** Gets a singleton stack containing `c`. */
+    SummaryComponentStack singleton(SummaryComponent c) {
+      result = TSingletonSummaryComponentStack(c)
+    }
+
+    /**
+     * Gets the stack obtained by pushing `head` onto `tail`.
+     *
+     * Make sure to override `RequiredSummaryComponentStack::required()` in order
+     * to ensure that the constructed stack exists.
+     */
+    SummaryComponentStack push(SummaryComponent head, SummaryComponentStack tail) {
+      result = TConsSummaryComponentStack(head, tail)
+    }
+
+    /** Gets a singleton stack for argument `i`. */
+    SummaryComponentStack argument(int i) { result = singleton(SummaryComponent::argument(i)) }
+
+    /** Gets a singleton stack representing a return of kind `rk`. */
+    SummaryComponentStack return(ReturnKind rk) { result = singleton(SummaryComponent::return(rk)) }
+  }
+
+  /**
+   * A class that exists for QL technical reasons only (the IPA type used
+   * to represent component stacks needs to be bounded).
+   */
+  abstract class RequiredSummaryComponentStack extends SummaryComponentStack {
+    /**
+     * Holds if the stack obtained by pushing `head` onto `tail` is required.
+     */
+    abstract predicate required(SummaryComponent c);
+  }
+
+  /** A callable with a flow summary. */
+  abstract class SummarizedCallable extends DataFlowCallable {
+    /**
+     * 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.
+     *
+     * Input specifications are restricted to stacks that end with
+     * `SummaryComponent::argument(_)`, preceded by zero or more
+     * `SummaryComponent::return(_)` or `SummaryComponent::content(_)` components.
+     *
+     * Output specifications are restricted to stacks that end with
+     * `SummaryComponent::return(_)` or `SummaryComponent::argument(_)`.
+     *
+     * Output stacks ending with `SummaryComponent::return(_)` can be preceded by zero
+     * or more `SummaryComponent::content(_)` components.
+     *
+     * Output stacks ending with `SummaryComponent::argument(_)` can be preceded by an
+     * optional `SummaryComponent::parameter(_)` component, which in turn can be preceded
+     * by zero or more `SummaryComponent::content(_)` components.
+     */
+    pragma[nomagic]
+    predicate propagatesFlow(
+      SummaryComponentStack input, SummaryComponentStack output, boolean preservesValue
+    ) {
+      none()
+    }
+
+    /**
+     * Holds if values stored inside `content` are cleared on objects passed as
+     * the `i`th argument to this callable.
+     */
+    pragma[nomagic]
+    predicate clearsContent(int i, 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 DataFlowImplCommon as DataFlowImplCommon
+
+  newtype TSummaryComponent =
+    TContentSummaryComponent(Content c) or
+    TParameterSummaryComponent(int i) { parameterPosition(i) } or
+    TArgumentSummaryComponent(int i) { parameterPosition(i) } or
+    TReturnSummaryComponent(ReturnKind rk)
+
+  newtype TSummaryComponentStack =
+    TSingletonSummaryComponentStack(SummaryComponent c) or
+    TConsSummaryComponentStack(SummaryComponent head, SummaryComponentStack tail) {
+      tail.(RequiredSummaryComponentStack).required(head)
+    }
+
+  pragma[nomagic]
+  private predicate summary(
+    SummarizedCallable c, SummaryComponentStack input, SummaryComponentStack output,
+    boolean preservesValue
+  ) {
+    c.propagatesFlow(input, output, preservesValue)
+  }
+
+  private newtype TSummaryNodeState =
+    TSummaryNodeInputState(SummaryComponentStack s) {
+      exists(SummaryComponentStack input |
+        summary(_, input, _, _) and
+        s = input.drop(_)
+      )
+    } or
+    TSummaryNodeOutputState(SummaryComponentStack s) {
+      exists(SummaryComponentStack output |
+        summary(_, _, output, _) and
+        s = output.drop(_)
+      )
+    }
+
+  /**
+   * A state used to break up (complex) flow summaries into atomic flow steps.
+   * For a flow summary
+   *
+   * ```ql
+   * propagatesFlow(
+   *   SummaryComponentStack input, SummaryComponentStack output, boolean preservesValue
+   * )
+   * ```
+   *
+   * the following states are used:
+   *
+   * - `TSummaryNodeInputState(SummaryComponentStack s)`:
+   *   this state represents that the components in `s` _have been read_ from the
+   *   input.
+   * - `TSummaryNodeOutputState(SummaryComponentStack s)`:
+   *   this state represents that the components in `s` _remain to be written_ to
+   *   the output.
+   */
+  class SummaryNodeState extends TSummaryNodeState {
+    /** Holds if this state is a valid input state for `c`. */
+    pragma[nomagic]
+    predicate isInputState(SummarizedCallable c, SummaryComponentStack s) {
+      this = TSummaryNodeInputState(s) and
+      exists(SummaryComponentStack input |
+        summary(c, input, _, _) and
+        s = input.drop(_)
+      )
+    }
+
+    /** Holds if this state is a valid output state for `c`. */
+    pragma[nomagic]
+    predicate isOutputState(SummarizedCallable c, SummaryComponentStack s) {
+      this = TSummaryNodeOutputState(s) and
+      exists(SummaryComponentStack output |
+        summary(c, _, output, _) and
+        s = output.drop(_)
+      )
+    }
+
+    /** Gets a textual representation of this state. */
+    string toString() {
+      exists(SummaryComponentStack s |
+        this = TSummaryNodeInputState(s) and
+        result = "read: " + s
+      )
+      or
+      exists(SummaryComponentStack s |
+        this = TSummaryNodeOutputState(s) and
+        result = "to write: " + s
+      )
+    }
+  }
+
+  /**
+   * Holds if `state` represents having read the `i`th argument for `c`. In this case
+   * we are not synthesizing a data-flow node, but instead assume that a relevant
+   * parameter node already exists.
+   */
+  private predicate parameterReadState(SummarizedCallable c, SummaryNodeState state, int i) {
+    state.isInputState(c, SummaryComponentStack::argument(i))
+  }
+
+  /**
+   * Holds if a synthesized summary node is needed for the state `state` in summarized
+   * callable `c`.
+   */
+  predicate summaryNodeRange(SummarizedCallable c, SummaryNodeState state) {
+    state.isInputState(c, _) and
+    not parameterReadState(c, state, _)
+    or
+    state.isOutputState(c, _)
+  }
+
+  pragma[noinline]
+  private Node summaryNodeInputState(SummarizedCallable c, SummaryComponentStack s) {
+    exists(SummaryNodeState state | state.isInputState(c, s) |
+      result = summaryNode(c, state)
+      or
+      exists(int i |
+        parameterReadState(c, state, i) and
+        result.(ParameterNode).isParameterOf(c, i)
+      )
+    )
+  }
+
+  pragma[noinline]
+  private Node summaryNodeOutputState(SummarizedCallable c, SummaryComponentStack s) {
+    exists(SummaryNodeState state |
+      state.isOutputState(c, s) and
+      result = summaryNode(c, state)
+    )
+  }
+
+  /**
+   * Holds if a write targets `post`, which is a post-update node for the `i`th
+   * parameter of `c`.
+   */
+  private predicate isParameterPostUpdate(Node post, SummarizedCallable c, int i) {
+    post = summaryNodeOutputState(c, SummaryComponentStack::argument(i))
+  }
+
+  /** Holds if a parameter node is required for the `i`th parameter of `c`. */
+  predicate summaryParameterNodeRange(SummarizedCallable c, int i) {
+    parameterReadState(c, _, i)
+    or
+    isParameterPostUpdate(_, c, i)
+  }
+
+  private predicate callbackOutput(
+    SummarizedCallable c, SummaryComponentStack s, Node receiver, ReturnKind rk
+  ) {
+    any(SummaryNodeState state).isInputState(c, s) and
+    s.head() = TReturnSummaryComponent(rk) and
+    receiver = summaryNodeInputState(c, s.drop(1))
+  }
+
+  private Node pre(Node post) {
+    summaryPostUpdateNode(post, result)
+    or
+    not summaryPostUpdateNode(post, _) and
+    result = post
+  }
+
+  private predicate callbackInput(
+    SummarizedCallable c, SummaryComponentStack s, Node receiver, int i
+  ) {
+    any(SummaryNodeState state).isOutputState(c, s) and
+    s.head() = TParameterSummaryComponent(i) and
+    receiver = pre(summaryNodeOutputState(c, s.drop(1)))
+  }
+
+  /** Holds if a call targeting `receiver` should be synthesized inside `c`. */
+  predicate summaryCallbackRange(SummarizedCallable c, Node receiver) {
+    callbackOutput(c, _, receiver, _)
+    or
+    callbackInput(c, _, receiver, _)
+  }
+
+  /**
+   * Gets the type of synthesized summary node `n`.
+   *
+   * The type is computed based on the language-specific predicates
+   * `getContentType()`, `getReturnType()`, `getCallbackParameterType()`, and
+   * `getCallbackReturnType()`.
+   */
+  DataFlowType summaryNodeType(Node n) {
+    exists(Node pre |
+      summaryPostUpdateNode(n, pre) and
+      result = getNodeType(pre)
+    )
+    or
+    exists(SummarizedCallable c, SummaryComponentStack s, SummaryComponent head | head = s.head() |
+      n = summaryNodeInputState(c, s) and
+      (
+        exists(Content cont |
+          head = TContentSummaryComponent(cont) and result = getContentType(cont)
+        )
+        or
+        exists(ReturnKind rk |
+          head = TReturnSummaryComponent(rk) and
+          result = getCallbackReturnType(getNodeType(summaryNodeInputState(c, s.drop(1))), rk)
+        )
+      )
+      or
+      n = summaryNodeOutputState(c, s) and
+      (
+        exists(Content cont |
+          head = TContentSummaryComponent(cont) and result = getContentType(cont)
+        )
+        or
+        s.length() = 1 and
+        exists(ReturnKind rk |
+          head = TReturnSummaryComponent(rk) and
+          result = getReturnType(c, rk)
+        )
+        or
+        exists(int i | head = TParameterSummaryComponent(i) |
+          result = getCallbackParameterType(getNodeType(summaryNodeOutputState(c, s.drop(1))), i)
+        )
+      )
+    )
+  }
+
+  /** Holds if summary node `out` contains output of kind `rk` from call `c`. */
+  predicate summaryOutNode(DataFlowCall c, Node out, ReturnKind rk) {
+    exists(SummarizedCallable callable, SummaryComponentStack s, Node receiver |
+      callbackOutput(callable, s, receiver, rk) and
+      out = summaryNodeInputState(callable, s) and
+      c = summaryDataFlowCall(receiver)
+    )
+  }
+
+  /** Holds if summary node `arg` is the `i`th argument of call `c`. */
+  predicate summaryArgumentNode(DataFlowCall c, Node arg, int i) {
+    exists(SummarizedCallable callable, SummaryComponentStack s, Node receiver |
+      callbackInput(callable, s, receiver, i) and
+      arg = summaryNodeOutputState(callable, s) and
+      c = summaryDataFlowCall(receiver)
+    )
+  }
+
+  /** Holds if summary node `post` is a post-update node with pre-update node `pre`. */
+  predicate summaryPostUpdateNode(Node post, ParameterNode pre) {
+    exists(SummarizedCallable c, int i |
+      isParameterPostUpdate(post, c, i) and
+      pre.isParameterOf(c, i)
+    )
+  }
+
+  /** Holds if summary node `ret` is a return node of kind `rk`. */
+  predicate summaryReturnNode(Node ret, ReturnKind rk) {
+    exists(SummarizedCallable callable, SummaryComponentStack s |
+      ret = summaryNodeOutputState(callable, s) and
+      s = TSingletonSummaryComponentStack(TReturnSummaryComponent(rk))
+    )
+  }
+
+  /** Provides a compilation of flow summaries to atomic data-flow steps. */
+  module Steps {
+    /**
+     * 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(
+        SummarizedCallable c, SummaryComponentStack inputContents,
+        SummaryComponentStack outputContents
+      |
+        summary(c, inputContents, outputContents, preservesValue) and
+        pred = summaryNodeInputState(c, inputContents) and
+        succ = summaryNodeOutputState(c, outputContents)
+      )
+    }
+
+    /**
+     * Holds if there is a read step of content `c` from `pred` to `succ`, which
+     * is synthesized from a flow summary.
+     */
+    predicate summaryReadStep(Node pred, Content c, Node succ) {
+      exists(SummarizedCallable sc, SummaryComponentStack s |
+        pred = summaryNodeInputState(sc, s.drop(1)) and
+        succ = summaryNodeInputState(sc, s) and
+        SummaryComponent::content(c) = s.head()
+      )
+    }
+
+    /**
+     * Holds if there is a store step of content `c` from `pred` to `succ`, which
+     * is synthesized from a flow summary.
+     */
+    predicate summaryStoreStep(Node pred, Content c, Node succ) {
+      exists(SummarizedCallable sc, SummaryComponentStack s |
+        pred = summaryNodeOutputState(sc, s) and
+        succ = summaryNodeOutputState(sc, s.drop(1)) and
+        SummaryComponent::content(c) = s.head()
+      )
+    }
+
+    /**
+     * Holds if values stored inside content `c` are cleared when passed as
+     * input of type `input` in `call`.
+     */
+    predicate summaryClearsContent(ArgumentNode arg, Content c) {
+      exists(DataFlowCall call, int i |
+        viableCallable(call).(SummarizedCallable).clearsContent(i, c) and
+        arg.argumentOf(call, i)
+      )
+    }
+
+    pragma[nomagic]
+    private ParameterNode summaryArgParam(
+      ArgumentNode arg, DataFlowImplCommon::ReturnKindExt rk, DataFlowImplCommon::OutNodeExt out
+    ) {
+      exists(DataFlowCall call, int pos, SummarizedCallable callable |
+        arg.argumentOf(call, pos) and
+        viableCallable(call) = callable and
+        result.isParameterOf(callable, pos) and
+        out = rk.getAnOutNode(call)
+      )
+    }
+
+    /**
+     * 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 summaryThroughStep(ArgumentNode arg, Node out, boolean preservesValue) {
+      exists(DataFlowImplCommon::ReturnKindExt rk, DataFlowImplCommon::ReturnNodeExt ret |
+        summaryLocalStep(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 summaryGetterStep(ArgumentNode arg, Content c, Node out) {
+      exists(DataFlowImplCommon::ReturnKindExt rk, Node mid, DataFlowImplCommon::ReturnNodeExt ret |
+        summaryReadStep(summaryArgParam(arg, rk, out), c, mid) and
+        summaryLocalStep(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 summarySetterStep(ArgumentNode arg, Content c, Node out) {
+      exists(DataFlowImplCommon::ReturnKindExt rk, Node mid, DataFlowImplCommon::ReturnNodeExt ret |
+        summaryLocalStep(summaryArgParam(arg, rk, out), mid, _) and
+        summaryStoreStep(mid, c, ret) and
+        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(
+        DataFlowImplCommon::ParamUpdateReturnKind rk, DataFlowImplCommon::ReturnNodeExt ret,
+        PostUpdateNode out
+      |
+        exists(DataFlowCall call, SummarizedCallable callable |
+          DataFlowImplCommon::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()
+        )
+      )
+    }
+  }
+
+  /**
+   * Provides a means of translating externally (e.g., CSV) defined flow
+   * summaries into a `SummarizedCallable`s.
+   */
+  module External {
+    /**
+     * Provides a means of translating an externally (e.g., CSV) defined flow
+     * summary into a `SummarizedCallable`.
+     */
+    abstract class ExternalSummaryCompilation extends string {
+      bindingset[this]
+      ExternalSummaryCompilation() { any() }
+
+      /** Holds if this flow summary is for callable `c`. */
+      abstract predicate callable(DataFlowCallable c, boolean preservesValue);
+
+      /** Holds if the `i`th input component is `c`. */
+      abstract predicate input(int i, SummaryComponent c);
+
+      /** Holds if the `i`th output component is `c`. */
+      abstract predicate output(int i, SummaryComponent c);
+
+      /**
+       * Holds if the input components starting from index `i` translate into `suffix`.
+       */
+      final predicate translateInput(int i, SummaryComponentStack suffix) {
+        exists(SummaryComponent comp | this.input(i, comp) |
+          i = max(int j | this.input(j, _)) and
+          suffix = TSingletonSummaryComponentStack(comp)
+          or
+          exists(TSummaryComponent head, SummaryComponentStack tail |
+            this.translateInputCons(i, head, tail) and
+            suffix = TConsSummaryComponentStack(head, tail)
+          )
+        )
+      }
+
+      final predicate translateInputCons(int i, SummaryComponent head, SummaryComponentStack tail) {
+        this.input(i, head) and
+        this.translateInput(i + 1, tail)
+      }
+
+      /**
+       * Holds if the output components starting from index `i` translate into `suffix`.
+       */
+      predicate translateOutput(int i, SummaryComponentStack suffix) {
+        exists(SummaryComponent comp | this.output(i, comp) |
+          i = max(int j | this.output(j, _)) and
+          suffix = TSingletonSummaryComponentStack(comp)
+          or
+          exists(TSummaryComponent head, SummaryComponentStack tail |
+            this.translateOutputCons(i, head, tail) and
+            suffix = TConsSummaryComponentStack(head, tail)
+          )
+        )
+      }
+
+      predicate translateOutputCons(int i, SummaryComponent head, SummaryComponentStack tail) {
+        this.output(i, head) and
+        this.translateOutput(i + 1, tail)
+      }
+    }
+
+    private class ExternalRequiredSummaryComponentStack extends RequiredSummaryComponentStack {
+      private SummaryComponent head;
+
+      ExternalRequiredSummaryComponentStack() {
+        any(ExternalSummaryCompilation s).translateInputCons(_, head, this) or
+        any(ExternalSummaryCompilation s).translateOutputCons(_, head, this)
+      }
+
+      override predicate required(SummaryComponent c) { c = head }
+    }
+
+    class ExternalSummarizedCallableAdaptor extends SummarizedCallable {
+      ExternalSummarizedCallableAdaptor() { any(ExternalSummaryCompilation s).callable(this, _) }
+
+      override predicate propagatesFlow(
+        SummaryComponentStack input, SummaryComponentStack output, boolean preservesValue
+      ) {
+        exists(ExternalSummaryCompilation s |
+          s.callable(this, preservesValue) and
+          s.translateInput(0, input) and
+          s.translateOutput(0, output)
+        )
+      }
+    }
+  }
+
+  /** 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 {
+      /** Gets the string representation of this callable used by `summary/3`. */
+      string getFullString() { result = this.toString() }
+    }
+
+    /** A query predicate for outputting flow summaries in QL tests. */
+    query predicate summary(string callable, string flow, boolean preservesValue) {
+      exists(
+        RelevantSummarizedCallable c, SummaryComponentStack input, SummaryComponentStack output
+      |
+        callable = c.getFullString() and
+        c.propagatesFlow(input, output, preservesValue) and
+        flow = input + " -> " + output
+      )
+    }
+  }
+}

java/ql/src/semmle/code/java/dataflow/internal/FlowSummaryImplSpecific.qll

@@ -0,0 +1,51 @@
+/**
+ * Provides Java specific classes and predicates for definining flow summaries.
+ */
+
+private import java
+private import DataFlowPrivate
+private import DataFlowUtil
+private import FlowSummaryImpl::Private
+private import FlowSummaryImpl::Public
+
+private module FlowSummaries {
+  private import semmle.code.java.dataflow.FlowSummary as F
+}
+
+/** Holds is `i` is a valid parameter position. */
+predicate parameterPosition(int i) { i in [-1 .. any(Parameter p).getPosition()] }
+
+/** Gets the synthesized summary data-flow node for the given values. */
+Node summaryNode(SummarizedCallable c, SummaryNodeState state) { result = getSummaryNode(c, state) }
+
+/** Gets the synthesized data-flow call for `receiver`. */
+DataFlowCall summaryDataFlowCall(Node receiver) { none() }
+
+/** Gets the type of content `c`. */
+DataFlowType getContentType(Content c) {
+  result = getErasedRepr(c.(FieldContent).getField().getType())
+  or
+  c instanceof CollectionContent and
+  result instanceof TypeObject
+  or
+  c instanceof ArrayContent and
+  result instanceof TypeObject
+}
+
+/** Gets the return type of kind `rk` for callable `c`. */
+DataFlowType getReturnType(SummarizedCallable c, ReturnKind rk) {
+  result = getErasedRepr(c.getReturnType()) and
+  exists(rk)
+}
+
+/**
+ * Gets the type of the `i`th parameter in a synthesized call that targets a
+ * callback of type `t`.
+ */
+DataFlowType getCallbackParameterType(DataFlowType t, int i) { none() }
+
+/**
+ * Gets the return type of kind `rk` in a synthesized call that targets a
+ * callback of type `t`.
+ */
+DataFlowType getCallbackReturnType(DataFlowType t, ReturnKind rk) { none() }

java/ql/src/semmle/code/java/dataflow/internal/TaintTrackingUtil.qll

@@ -13,6 +13,7 @@ private import semmle.code.java.frameworks.Networking
 private import semmle.code.java.dataflow.ExternalFlow
 private import semmle.code.java.dataflow.internal.DataFlowPrivate
 import semmle.code.java.dataflow.FlowSteps
+private import FlowSummaryImpl as FlowSummaryImpl
 
 /**
  * Holds if taint can flow from `src` to `sink` in zero or more
@@ -33,7 +34,10 @@ predicate localExprTaint(Expr src, Expr sink) {
  */
 predicate localTaintStep(DataFlow::Node src, DataFlow::Node sink) {
   DataFlow::localFlowStep(src, sink) or
-  localAdditionalTaintStep(src, sink)
+  localAdditionalTaintStep(src, sink) or
+  // Simple flow through library code is included in the exposed local
+  // step relation, even though flow is technically inter-procedural
+  FlowSummaryImpl::Private::Steps::summaryThroughStep(src, sink, false)
 }
 
 /**
@@ -61,6 +65,8 @@ private predicate localAdditionalBasicTaintStep(DataFlow::Node src, DataFlow::No
     arg.isVararg() and
     sink.(DataFlow::ImplicitVarargsArray).getCall() = arg.getCall()
   )
+  or
+  FlowSummaryImpl::Private::Steps::summaryLocalStep(src, sink, false)
 }
 
 /**

java/ql/test/library-tests/dataflow/local-additional-taint/localAdditionalTaintStep.ql

@@ -2,5 +2,7 @@ import semmle.code.java.dataflow.DataFlow
 import semmle.code.java.dataflow.internal.TaintTrackingUtil
 
 from DataFlow::Node src, DataFlow::Node sink
-where localAdditionalTaintStep(src, sink)
+where
+  localAdditionalTaintStep(src, sink) and
+  src.getLocation().getFile().getExtension() = "java"
 select src, sink