Member predicate StackVariableReachability::reaches

Holds if the source node source can reach the sink sink without crossing a barrier. 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
  isSink(sink, v)
}

predicate reachesImpl(ControlFlowNode source, SemanticStackVariable v, ControlFlowNode sink) {
  sink = source.getASuccessor() and isSource(source, v)
  or
  exists(ControlFlowNode mid | reachesImpl(source, v, mid) |
    not isBarrier(mid, v)
    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.