JavaScript: Fix join order in PathNode.getASuccessor.

This commit is contained in:
Max Schaefer
2020-01-02 09:48:57 +00:00
parent f6029bd55c
commit 2a55ba5d4f

View File

@@ -1070,6 +1070,18 @@ private MidPathNode finalMidNode(SinkPathNode snk) {
)
}
/**
* Holds if `nd` is a mid node wrapping `(predNd, cfg, summary)`, and there is a flow step
* from `predNd` to `succNd` under `cfg` with summary `newSummary`.
*
* This helper predicate exists to clarify the intended join order in `getASuccessor` below.
*/
pragma[noinline]
private predicate midNodeStep(PathNode nd, DataFlow::Node predNd, Configuration cfg, PathSummary summary, DataFlow::Node succNd, PathSummary newSummary) {
nd = MkMidNode(predNd, cfg, summary) and
flowStep(predNd, id(cfg), succNd, newSummary)
}
/**
* Gets a node to which data from `nd` may flow in one step.
*/
@@ -1079,8 +1091,7 @@ private PathNode getASuccessor(PathNode nd) {
or
// mid node to mid node
exists(Configuration cfg, DataFlow::Node predNd, PathSummary summary, DataFlow::Node succNd, PathSummary newSummary |
nd = MkMidNode(predNd, cfg, summary) and
flowStep(predNd, id(cfg), succNd, newSummary) and
midNodeStep(nd, predNd, cfg, summary, succNd, newSummary) and
result = MkMidNode(succNd, id(cfg), summary.append(newSummary))
)
or