Reachability analysis — part 2

In a previous post I described the motivation for doing reachability analysis on annotated code. That post ends with an algorithm design challenge. Suppose that we are given the simple path φ₀→φ₁→⋯→φ_n. The precondition of node i is ψ_i=φ₀∧⋯∧φ_i−1. Notice that ψ₀=⊤. For simplicity, let us assume that φ_n=⊤. We wish to know which preconditions are satisfiable and which are not. We are allowed to use a prover, which is a big black box with two bulbs on it: the green one flashes if the last precondition fed to the prover is satisfiable and the red one flashes if the precondition is unsatisfiable. The bulbs consume a lot of electricity and we want to be environment friendly, so we try to reduce the number of prover queries. This instance of the problem can be solved using binary search.

int firstUnsat(vector<Formula> pre) {
  if (isSat(pre[pre.size() - 1])) return pre.size(); // all SAT
  int left = 0, right = pre.size() - 1;
  while (left + 1 < right) {
    // isSat(left) && !isSat(right)
    int middle = (left + right) / 2;
    (isSat(pre[middle]) ? left : right) = middle;
  }
  return right;
}

Exercise. Let's consider a Java program that is made of a sequence of n+1 statements. Each statement contains a `reachability bug' with a small (independent) probability є. The algorithm above essentially detects the earliest reachability bug. What is the average number of prover queries? (In the code, prover queries are represented by calls to isSat.)

Exercise. Prove that it is not possible to do better (asymptotically) than the algorithm above. (Edit: Perhaps a better question: "Is it possible to do better on average without sacrificing the worst case behavior?")

Now let's move on to a more general problem. Instead of starting with a simple path we start with a dag flow graph. For simplicity we can assume that there is only one source node, which we can take to be 0. The precondition of node 3 in the graph {0→1, 0→2, 1→3, 2→3} is ψ₃=(φ₀∧φ₁)∨(φ₀∧φ₂). In other words, we look at all paths 0↝ 3 and take the disjunction. (Of course, there are better ways of computing something equivalent than looking at all paths.) What would be a good algorithm for finding which preconditions are satisfiable and which not when the flow graph is a dag? I'll write about it in the next part of this post series.