mirror of
https://github.com/github/codeql.git
synced 2026-05-04 21:25:44 +02:00
Merge pull request #5032 from aschackmull/dataflow/subpaths
Dataflow: Add subpaths query predicate.
This commit is contained in:
@@ -3258,24 +3258,16 @@ class PathNode extends TPathNode {
|
||||
/** Gets the associated configuration. */
|
||||
Configuration getConfiguration() { none() }
|
||||
|
||||
private predicate isHidden() {
|
||||
hiddenNode(this.(PathNodeImpl).getNodeEx().asNode()) and
|
||||
not this.isSource() and
|
||||
not this instanceof PathNodeSink
|
||||
or
|
||||
this.(PathNodeImpl).getNodeEx() instanceof TNodeImplicitRead
|
||||
}
|
||||
|
||||
private PathNode getASuccessorIfHidden() {
|
||||
this.isHidden() and
|
||||
this.(PathNodeImpl).isHidden() and
|
||||
result = this.(PathNodeImpl).getASuccessorImpl()
|
||||
}
|
||||
|
||||
/** Gets a successor of this node, if any. */
|
||||
final PathNode getASuccessor() {
|
||||
result = this.(PathNodeImpl).getASuccessorImpl().getASuccessorIfHidden*() and
|
||||
not this.isHidden() and
|
||||
not result.isHidden()
|
||||
not this.(PathNodeImpl).isHidden() and
|
||||
not result.(PathNodeImpl).isHidden()
|
||||
}
|
||||
|
||||
/** Holds if this node is a source. */
|
||||
@@ -3287,6 +3279,14 @@ abstract private class PathNodeImpl extends PathNode {
|
||||
|
||||
abstract NodeEx getNodeEx();
|
||||
|
||||
predicate isHidden() {
|
||||
hiddenNode(this.getNodeEx().asNode()) and
|
||||
not this.isSource() and
|
||||
not this instanceof PathNodeSink
|
||||
or
|
||||
this.getNodeEx() instanceof TNodeImplicitRead
|
||||
}
|
||||
|
||||
private string ppAp() {
|
||||
this instanceof PathNodeSink and result = ""
|
||||
or
|
||||
@@ -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 `n1.getSucc() = n2` and `n2` can reach a sink. */
|
||||
/** 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 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,86 @@ 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() and
|
||||
not ret.isHidden()
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* 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 a return node 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`.
|
||||
*
|
||||
|
||||
@@ -3258,24 +3258,16 @@ class PathNode extends TPathNode {
|
||||
/** Gets the associated configuration. */
|
||||
Configuration getConfiguration() { none() }
|
||||
|
||||
private predicate isHidden() {
|
||||
hiddenNode(this.(PathNodeImpl).getNodeEx().asNode()) and
|
||||
not this.isSource() and
|
||||
not this instanceof PathNodeSink
|
||||
or
|
||||
this.(PathNodeImpl).getNodeEx() instanceof TNodeImplicitRead
|
||||
}
|
||||
|
||||
private PathNode getASuccessorIfHidden() {
|
||||
this.isHidden() and
|
||||
this.(PathNodeImpl).isHidden() and
|
||||
result = this.(PathNodeImpl).getASuccessorImpl()
|
||||
}
|
||||
|
||||
/** Gets a successor of this node, if any. */
|
||||
final PathNode getASuccessor() {
|
||||
result = this.(PathNodeImpl).getASuccessorImpl().getASuccessorIfHidden*() and
|
||||
not this.isHidden() and
|
||||
not result.isHidden()
|
||||
not this.(PathNodeImpl).isHidden() and
|
||||
not result.(PathNodeImpl).isHidden()
|
||||
}
|
||||
|
||||
/** Holds if this node is a source. */
|
||||
@@ -3287,6 +3279,14 @@ abstract private class PathNodeImpl extends PathNode {
|
||||
|
||||
abstract NodeEx getNodeEx();
|
||||
|
||||
predicate isHidden() {
|
||||
hiddenNode(this.getNodeEx().asNode()) and
|
||||
not this.isSource() and
|
||||
not this instanceof PathNodeSink
|
||||
or
|
||||
this.getNodeEx() instanceof TNodeImplicitRead
|
||||
}
|
||||
|
||||
private string ppAp() {
|
||||
this instanceof PathNodeSink and result = ""
|
||||
or
|
||||
@@ -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 `n1.getSucc() = n2` and `n2` can reach a sink. */
|
||||
/** 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 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,86 @@ 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() and
|
||||
not ret.isHidden()
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* 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 a return node 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`.
|
||||
*
|
||||
|
||||
@@ -3258,24 +3258,16 @@ class PathNode extends TPathNode {
|
||||
/** Gets the associated configuration. */
|
||||
Configuration getConfiguration() { none() }
|
||||
|
||||
private predicate isHidden() {
|
||||
hiddenNode(this.(PathNodeImpl).getNodeEx().asNode()) and
|
||||
not this.isSource() and
|
||||
not this instanceof PathNodeSink
|
||||
or
|
||||
this.(PathNodeImpl).getNodeEx() instanceof TNodeImplicitRead
|
||||
}
|
||||
|
||||
private PathNode getASuccessorIfHidden() {
|
||||
this.isHidden() and
|
||||
this.(PathNodeImpl).isHidden() and
|
||||
result = this.(PathNodeImpl).getASuccessorImpl()
|
||||
}
|
||||
|
||||
/** Gets a successor of this node, if any. */
|
||||
final PathNode getASuccessor() {
|
||||
result = this.(PathNodeImpl).getASuccessorImpl().getASuccessorIfHidden*() and
|
||||
not this.isHidden() and
|
||||
not result.isHidden()
|
||||
not this.(PathNodeImpl).isHidden() and
|
||||
not result.(PathNodeImpl).isHidden()
|
||||
}
|
||||
|
||||
/** Holds if this node is a source. */
|
||||
@@ -3287,6 +3279,14 @@ abstract private class PathNodeImpl extends PathNode {
|
||||
|
||||
abstract NodeEx getNodeEx();
|
||||
|
||||
predicate isHidden() {
|
||||
hiddenNode(this.getNodeEx().asNode()) and
|
||||
not this.isSource() and
|
||||
not this instanceof PathNodeSink
|
||||
or
|
||||
this.getNodeEx() instanceof TNodeImplicitRead
|
||||
}
|
||||
|
||||
private string ppAp() {
|
||||
this instanceof PathNodeSink and result = ""
|
||||
or
|
||||
@@ -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 `n1.getSucc() = n2` and `n2` can reach a sink. */
|
||||
/** 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 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,86 @@ 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() and
|
||||
not ret.isHidden()
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* 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 a return node 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`.
|
||||
*
|
||||
|
||||
@@ -3258,24 +3258,16 @@ class PathNode extends TPathNode {
|
||||
/** Gets the associated configuration. */
|
||||
Configuration getConfiguration() { none() }
|
||||
|
||||
private predicate isHidden() {
|
||||
hiddenNode(this.(PathNodeImpl).getNodeEx().asNode()) and
|
||||
not this.isSource() and
|
||||
not this instanceof PathNodeSink
|
||||
or
|
||||
this.(PathNodeImpl).getNodeEx() instanceof TNodeImplicitRead
|
||||
}
|
||||
|
||||
private PathNode getASuccessorIfHidden() {
|
||||
this.isHidden() and
|
||||
this.(PathNodeImpl).isHidden() and
|
||||
result = this.(PathNodeImpl).getASuccessorImpl()
|
||||
}
|
||||
|
||||
/** Gets a successor of this node, if any. */
|
||||
final PathNode getASuccessor() {
|
||||
result = this.(PathNodeImpl).getASuccessorImpl().getASuccessorIfHidden*() and
|
||||
not this.isHidden() and
|
||||
not result.isHidden()
|
||||
not this.(PathNodeImpl).isHidden() and
|
||||
not result.(PathNodeImpl).isHidden()
|
||||
}
|
||||
|
||||
/** Holds if this node is a source. */
|
||||
@@ -3287,6 +3279,14 @@ abstract private class PathNodeImpl extends PathNode {
|
||||
|
||||
abstract NodeEx getNodeEx();
|
||||
|
||||
predicate isHidden() {
|
||||
hiddenNode(this.getNodeEx().asNode()) and
|
||||
not this.isSource() and
|
||||
not this instanceof PathNodeSink
|
||||
or
|
||||
this.getNodeEx() instanceof TNodeImplicitRead
|
||||
}
|
||||
|
||||
private string ppAp() {
|
||||
this instanceof PathNodeSink and result = ""
|
||||
or
|
||||
@@ -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 `n1.getSucc() = n2` and `n2` can reach a sink. */
|
||||
/** 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 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,86 @@ 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() and
|
||||
not ret.isHidden()
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* 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 a return node 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`.
|
||||
*
|
||||
|
||||
@@ -3258,24 +3258,16 @@ class PathNode extends TPathNode {
|
||||
/** Gets the associated configuration. */
|
||||
Configuration getConfiguration() { none() }
|
||||
|
||||
private predicate isHidden() {
|
||||
hiddenNode(this.(PathNodeImpl).getNodeEx().asNode()) and
|
||||
not this.isSource() and
|
||||
not this instanceof PathNodeSink
|
||||
or
|
||||
this.(PathNodeImpl).getNodeEx() instanceof TNodeImplicitRead
|
||||
}
|
||||
|
||||
private PathNode getASuccessorIfHidden() {
|
||||
this.isHidden() and
|
||||
this.(PathNodeImpl).isHidden() and
|
||||
result = this.(PathNodeImpl).getASuccessorImpl()
|
||||
}
|
||||
|
||||
/** Gets a successor of this node, if any. */
|
||||
final PathNode getASuccessor() {
|
||||
result = this.(PathNodeImpl).getASuccessorImpl().getASuccessorIfHidden*() and
|
||||
not this.isHidden() and
|
||||
not result.isHidden()
|
||||
not this.(PathNodeImpl).isHidden() and
|
||||
not result.(PathNodeImpl).isHidden()
|
||||
}
|
||||
|
||||
/** Holds if this node is a source. */
|
||||
@@ -3287,6 +3279,14 @@ abstract private class PathNodeImpl extends PathNode {
|
||||
|
||||
abstract NodeEx getNodeEx();
|
||||
|
||||
predicate isHidden() {
|
||||
hiddenNode(this.getNodeEx().asNode()) and
|
||||
not this.isSource() and
|
||||
not this instanceof PathNodeSink
|
||||
or
|
||||
this.getNodeEx() instanceof TNodeImplicitRead
|
||||
}
|
||||
|
||||
private string ppAp() {
|
||||
this instanceof PathNodeSink and result = ""
|
||||
or
|
||||
@@ -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 `n1.getSucc() = n2` and `n2` can reach a sink. */
|
||||
/** 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 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,86 @@ 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() and
|
||||
not ret.isHidden()
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* 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 a return node 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`.
|
||||
*
|
||||
|
||||
@@ -3258,24 +3258,16 @@ class PathNode extends TPathNode {
|
||||
/** Gets the associated configuration. */
|
||||
Configuration getConfiguration() { none() }
|
||||
|
||||
private predicate isHidden() {
|
||||
hiddenNode(this.(PathNodeImpl).getNodeEx().asNode()) and
|
||||
not this.isSource() and
|
||||
not this instanceof PathNodeSink
|
||||
or
|
||||
this.(PathNodeImpl).getNodeEx() instanceof TNodeImplicitRead
|
||||
}
|
||||
|
||||
private PathNode getASuccessorIfHidden() {
|
||||
this.isHidden() and
|
||||
this.(PathNodeImpl).isHidden() and
|
||||
result = this.(PathNodeImpl).getASuccessorImpl()
|
||||
}
|
||||
|
||||
/** Gets a successor of this node, if any. */
|
||||
final PathNode getASuccessor() {
|
||||
result = this.(PathNodeImpl).getASuccessorImpl().getASuccessorIfHidden*() and
|
||||
not this.isHidden() and
|
||||
not result.isHidden()
|
||||
not this.(PathNodeImpl).isHidden() and
|
||||
not result.(PathNodeImpl).isHidden()
|
||||
}
|
||||
|
||||
/** Holds if this node is a source. */
|
||||
@@ -3287,6 +3279,14 @@ abstract private class PathNodeImpl extends PathNode {
|
||||
|
||||
abstract NodeEx getNodeEx();
|
||||
|
||||
predicate isHidden() {
|
||||
hiddenNode(this.getNodeEx().asNode()) and
|
||||
not this.isSource() and
|
||||
not this instanceof PathNodeSink
|
||||
or
|
||||
this.getNodeEx() instanceof TNodeImplicitRead
|
||||
}
|
||||
|
||||
private string ppAp() {
|
||||
this instanceof PathNodeSink and result = ""
|
||||
or
|
||||
@@ -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 `n1.getSucc() = n2` and `n2` can reach a sink. */
|
||||
/** 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 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,86 @@ 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() and
|
||||
not ret.isHidden()
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* 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 a return node 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`.
|
||||
*
|
||||
|
||||
@@ -3258,24 +3258,16 @@ class PathNode extends TPathNode {
|
||||
/** Gets the associated configuration. */
|
||||
Configuration getConfiguration() { none() }
|
||||
|
||||
private predicate isHidden() {
|
||||
hiddenNode(this.(PathNodeImpl).getNodeEx().asNode()) and
|
||||
not this.isSource() and
|
||||
not this instanceof PathNodeSink
|
||||
or
|
||||
this.(PathNodeImpl).getNodeEx() instanceof TNodeImplicitRead
|
||||
}
|
||||
|
||||
private PathNode getASuccessorIfHidden() {
|
||||
this.isHidden() and
|
||||
this.(PathNodeImpl).isHidden() and
|
||||
result = this.(PathNodeImpl).getASuccessorImpl()
|
||||
}
|
||||
|
||||
/** Gets a successor of this node, if any. */
|
||||
final PathNode getASuccessor() {
|
||||
result = this.(PathNodeImpl).getASuccessorImpl().getASuccessorIfHidden*() and
|
||||
not this.isHidden() and
|
||||
not result.isHidden()
|
||||
not this.(PathNodeImpl).isHidden() and
|
||||
not result.(PathNodeImpl).isHidden()
|
||||
}
|
||||
|
||||
/** Holds if this node is a source. */
|
||||
@@ -3287,6 +3279,14 @@ abstract private class PathNodeImpl extends PathNode {
|
||||
|
||||
abstract NodeEx getNodeEx();
|
||||
|
||||
predicate isHidden() {
|
||||
hiddenNode(this.getNodeEx().asNode()) and
|
||||
not this.isSource() and
|
||||
not this instanceof PathNodeSink
|
||||
or
|
||||
this.getNodeEx() instanceof TNodeImplicitRead
|
||||
}
|
||||
|
||||
private string ppAp() {
|
||||
this instanceof PathNodeSink and result = ""
|
||||
or
|
||||
@@ -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 `n1.getSucc() = n2` and `n2` can reach a sink. */
|
||||
/** 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 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,86 @@ 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() and
|
||||
not ret.isHidden()
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* 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 a return node 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`.
|
||||
*
|
||||
|
||||
Reference in New Issue
Block a user