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.