JavaScript: Fix definitions of SourcePathNode and SinkPathNode.

Their charpreds previously only ensured that they were on a path from a
source to a sink, not that they actually were the source and sink,
respectively. See two commits further for a test case.
This commit is contained in:
Max Schaefer
2019-04-23 10:52:57 +01:00
parent c674f54129
commit 455dbccd05
3 changed files with 15 additions and 6 deletions

View File

@@ -819,7 +819,7 @@ private predicate reachableFromSource(
isSource(nd, cfg, lbl) and
not cfg.isBarrier(nd) and
not cfg.isLabeledBarrier(nd, lbl) and
summary = MkPathSummary(false, false, lbl, lbl)
summary = PathSummary::level(lbl)
)
or
exists(DataFlow::Node pred, PathSummary oldSummary, PathSummary newSummary |
@@ -952,14 +952,19 @@ class PathNode extends TPathNode {
* A path node corresponding to a flow source.
*/
class SourcePathNode extends PathNode {
SourcePathNode() { isSource(nd, cfg, _) }
SourcePathNode() {
exists(FlowLabel lbl |
summary = PathSummary::level(lbl) and
isSource(nd, cfg, lbl)
)
}
}
/**
* A path node corresponding to a flow sink.
*/
class SinkPathNode extends PathNode {
SinkPathNode() { isSink(nd, cfg, _) }
SinkPathNode() { isSink(nd, cfg, summary.getEndLabel()) }
}
/**

View File

@@ -406,7 +406,13 @@ module PathSummary {
/**
* Gets a summary describing a path without any calls or returns.
*/
PathSummary level() { exists(FlowLabel lbl | result = MkPathSummary(false, false, lbl, lbl)) }
PathSummary level() { result = level(_) }
/**
* Gets a summary describing a path without any calls or returns, transforming `lbl` into
* itself.
*/
PathSummary level(FlowLabel lbl) { result = MkPathSummary(false, false, lbl, lbl) }
/**
* Gets a summary describing a path with one or more calls, but no returns.