Dataflow: Add subpaths query predicate.

Author: aschackmull

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

@@ -3313,9 +3313,14 @@ abstract private class PathNodeImpl extends PathNode {
 }
 
 /** Holds if `n` can reach a sink. */
-private predicate reach(PathNode n) { n instanceof PathNodeSink or reach(n.getASuccessor()) }
+private predicate directReach(PathNode n) {
+  n instanceof PathNodeSink or directReach(n.getASuccessor())
+}
+
+/** Holds if `n` can reach a sink or is used in a subpath. */
+private predicate reach(PathNode n) { directReach(n) or Subpaths::retReach(n) }
 
-/** Holds if `n1.getSucc() = n2` and `n2` can reach a sink. */
+/** Holds if `n1.getSucc() = n2` and `n2` can reach a sink or is used in a subpath. */
 private predicate pathSucc(PathNode n1, PathNode n2) { n1.getASuccessor() = n2 and reach(n2) }
 
 private predicate pathSuccPlus(PathNode n1, PathNode n2) = fastTC(pathSucc/2)(n1, n2)
@@ -3331,6 +3336,8 @@ module PathGraph {
   query predicate nodes(PathNode n, string key, string val) {
     reach(n) and key = "semmle.label" and val = n.toString()
   }
+
+  query predicate subpaths = Subpaths::subpaths/4;
 }
 
 /**
@@ -3622,6 +3629,85 @@ private predicate pathThroughCallable(PathNodeMid mid, NodeEx out, CallContext c
   )
 }
 
+private module Subpaths {
+  /**
+   * Holds if `(arg, par, ret, out)` forms a subpath-tuple and `ret` is determined by
+   * `kind`, `sc`, `apout`, and `innercc`.
+   */
+  pragma[nomagic]
+  private predicate subpaths01(
+    PathNode arg, ParamNodeEx par, SummaryCtxSome sc, CallContext innercc, ReturnKindExt kind,
+    NodeEx out, AccessPath apout
+  ) {
+    pathThroughCallable(arg, out, _, apout) and
+    pathIntoCallable(arg, par, _, innercc, sc, _) and
+    paramFlowsThrough(kind, innercc, sc, apout, _, unbindConf(arg.getConfiguration()))
+  }
+
+  /**
+   * Holds if `(arg, par, ret, out)` forms a subpath-tuple and `ret` is determined by
+   * `kind`, `sc`, `apout`, and `innercc`.
+   */
+  pragma[nomagic]
+  private predicate subpaths02(
+    PathNode arg, ParamNodeEx par, SummaryCtxSome sc, CallContext innercc, ReturnKindExt kind,
+    NodeEx out, AccessPath apout
+  ) {
+    subpaths01(arg, par, sc, innercc, kind, out, apout) and
+    out.asNode() = kind.getAnOutNode(_)
+  }
+
+  pragma[nomagic]
+  private Configuration getPathNodeConf(PathNode n) { result = n.getConfiguration() }
+
+  /**
+   * Holds if `(arg, par, ret, out)` forms a subpath-tuple.
+   */
+  pragma[nomagic]
+  private predicate subpaths03(
+    PathNode arg, ParamNodeEx par, PathNodeMid ret, NodeEx out, AccessPath apout
+  ) {
+    exists(SummaryCtxSome sc, CallContext innercc, ReturnKindExt kind, RetNodeEx retnode |
+      subpaths02(arg, par, sc, innercc, kind, out, apout) and
+      ret.getNodeEx() = retnode and
+      kind = retnode.getKind() and
+      innercc = ret.getCallContext() and
+      sc = ret.getSummaryCtx() and
+      ret.getConfiguration() = unbindConf(getPathNodeConf(arg)) and
+      apout = ret.getAp()
+    )
+  }
+
+  /**
+   * Holds if `(arg, par, ret, out)` forms a subpath-tuple, that is, flow through
+   * a subpath between `par` and `ret` with the connecting edges `arg -> par` and
+   * `ret -> out` is summarized as the edge `arg -> out`.
+   */
+  predicate subpaths(PathNode arg, PathNodeImpl par, PathNodeMid ret, PathNodeMid out) {
+    exists(ParamNodeEx p, NodeEx o, AccessPath apout |
+      arg.getASuccessor() = par and
+      arg.getASuccessor() = out and
+      subpaths03(arg, p, ret, o, apout) and
+      par.getNodeEx() = p and
+      out.getNodeEx() = o and
+      out.getAp() = apout
+    )
+  }
+
+  /**
+   * Holds if `n` can reach `ret` in a summarized subpath.
+   */
+  predicate retReach(PathNode n) {
+    subpaths(_, _, n, _)
+    or
+    exists(PathNode mid |
+      retReach(mid) and
+      n.getASuccessor() = mid and
+      not subpaths(_, mid, _, _)
+    )
+  }
+}
+
 /**
  * Holds if data can flow (inter-procedurally) from `source` to `sink`.
  *