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
φ_{0}→φ_{1}→⋯→φ_{n}. The *precondition*
of node *i* is ψ_{i}=φ_{0}∧⋯∧φ_{i−1}.
Notice that ψ_{0}=⊤. 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
ψ_{3}=(φ_{0}∧φ_{1})∨(φ_{0}∧φ_{2}). 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.

## No comments:

## Post a Comment

Note: (1) You need to have third-party cookies enabled in order to comment on Blogger. (2) Better to copy your comment before hitting publish/preview. Blogger sometimes eats comments on the first try, but the second works. Crazy Blogger.