Member predicate StackVariableReachabilityWithReassignment::reaches
Holds if the source node source
can reach the sink sink
without crossing
a barrier, taking reassignments into account. This is (almost) equivalent
to the following QL predicate, but uses basic blocks internally for better
performance:
predicate reaches(ControlFlowNode source, SemanticStackVariable v, ControlFlowNode sink) {
reachesImpl(source, v, sink)
and
isSinkActual(sink, v)
}
predicate reachesImpl(ControlFlowNode source, SemanticStackVariable v, ControlFlowNode sink) {
isSourceActual(source, v)
and
(
sink = source.getASuccessor()
or
exists(ControlFlowNode mid, SemanticStackVariable v0 | reachesImpl(source, v0, mid) |
// ordinary successor
not isBarrier(mid, v) and
sink = mid.getASuccessor() and
v = v0
or
// reassigned from v0 to v
exprDefinition(v, mid, v0.getAnAccess()) and
sink = mid.getASuccessor()
)
)
}
In addition to using a better performing implementation, this analysis accounts for loops where the condition is provably true upon entry.
predicate reaches(ControlFlowNode source, SemanticStackVariable v, ControlFlowNode sink)