Main menu:

Site search

Categories

Archive

I need a theorem prover!

Time for a hardcore static analysis post. By the way, if anyone reading this knows about theorem provers, I could really use your help: what’s a solid off-the-shelf prover that will solve my formulas (see below)?

I’m working on bug 420933, which is a request for a static checker for XPCOM outparam usage. In short, XPCOM methods with outparams must (a) not set outparams when they return a failure code, and (b) set all outparams when they return a success code. At first, checking this sounded easy, because I was thinking of code like this:

nsresult SomeMethod(nsIWhatever **out) {
  nsresult rv = doSomething();
  if (NS_SUCCEEDED(rv)) {
    out = mValue;
    return NS_OK;
  } else {
    return rv;
  }
}

Attempt #1. We can check this method with a simple static analysis algorithm. The first step is to trace through all the code paths, recording (i) any outparam that gets assigned to, and (ii) (an abstract approximation of) values of variables that can be returned from the method. In this case, the results are:

nsresult SomeMethod(nsIWhatever **out) {
  nsresult rv = doSomething();   // rv = ?,       out = NOT WRITTEN
  if (NS_SUCCEEDED(rv)) {
                                 // rv = SUCCESS, out = NOT_WRITTEN
    out = mValue;                // rv = SUCCESS, out = WRITTEN
    return NS_OK;                // rv = SUCCESS, out = WRITTEN
  } else {
                                 // rv = FAILURE, out = NOT_WRITTEN
    return rv;                   // rv = FAILURE, out = NOT_WRITTEN
  }
}

Note that on each branch of the if statement the analysis sets a property according to whether the true or false branch was taken. Some analyses don’t do this, but in our case we know that return rv returns false only by taking account of the branch condition.

The second step is to check the requirement at each return statement using the results from step 1. So, for return rv, first we read off rv = FAILURE, which tells us to check property (b), that all outparams are set. Then we see out = NOT_WRITTEN, so the check succeeds.

I liked this design because it was fairly simple, and also because it can be implemented as a standard flow-sensitive abstract interpretation, which is pretty efficient. (When I say “standard flow-sensitive abstract interpretation” I mean the design kind of looks like a combination of two standard compiler passes: the constant propagation optimization (for the return values) and the unassigned variables check (for the outparams).)

“For any complex problem, there is always a solution that is
simple, clear, and wrong.”
Unfortunately, attempt #1 doesn’t work, for two reasons. First, GCC adds stuff to the code before the analysis sees it, so the method above looks more like this:

nsresult SomeMethod(nsIWhatever **out) {
  nsresult rv;
  rv = doSomething();            // rv = ?
  tmp = rv;                      // rv = ?, tmp = ?
  if.temp = NS_SUCCEEDED(tmp);   // rv = ?, tmp = ?, if.temp = ?
  if (if.temp) {
                                 // rv = ?, tmp = ?, if.temp = SUCCESS
    out = mValue;                // rv = ?, tmp = ?, if.temp = SUCCESS
    return NS_OK;                // rv = ?, tmp = ?, if.temp = SUCCESS
  } else {
                                 // rv = ?, tmp = ?, if.temp = SUCCESS
    return rv;                   // rv = ?, tmp = ?, if.temp = FAILURE
  }
}

The analysis tracks if.temp through the if branches, but fails to pick up any information about rv. So when we reach return rv, we don’t know whether to check (a) or (b), and we can’t check the method—we can only issue a (spurious) warning. In order to make this work, we need to track not only so much values of return variables as their relationships. We can represent the relationships as logical formulas:

nsresult SomeMethod(nsIWhatever **out) {
  nsresult rv;
  rv = doSomething();            // (empty formula)
  tmp = rv;                      // tmp == rv
  if.temp = NS_SUCCEEDED(rv);    // tmp == rv, if.temp  SUCCEEDED(rv)
  if (if.temp) {
                      // tmp == rv, if.temp  SUCCEEDED(tmp), if.temp
    out = mValue;     // tmp == rv, if.temp  SUCCEEDED(tmp), if.temp
    return NS_OK;     // tmp == rv, if.temp  SUCCEEDED(tmp), if.temp
  } else {
                      // tmp == rv, if.temp  SUCCEEDED(tmp), not if.temp
    return rv;        // tmp == rv, if.temp  SUCCEEDED(tmp), not if.temp
  }
}

Now, when we reach return rv, we have enough information to figure out that rv is a failure code, assuming we have a theorem prover that can reason like this:

if.temp  SUCCEEDED(tmp)               ===>  not if.temp  FAILED(tmp)
not if.temp, not if.temp => FAILED(tmp)  ===>  FAILED(tmp)
FAILED(tmp), tmp == rv                   ===>  FAILED(rv)

I said there was a second reason the simple analysis doesn’t work, which is code like this:

nsresult AnotherMethod(nsIFoo **out) {
  nsresult rv = mBar.DelegateMethod(out); // rv = ?, out = ?
  return rv;
}

The analysis should not consider this an error: it should assume that DelegateMethod follows the outparam protocol correctly, which means that that rv is a success code iff out was written, and the requirement is satisifed. But the basic analysis gets no information about both rv and out. Again, we need to track relationships. This time, we want to model the method call using the formula SUCCEEDED(rv) WRITTEN(out). When we reach return rv, we will see that we don’t have a definite value for rv. So we check both properties (a) and (b). First, we ask the theorem prover which outparams are written under the assumption SUCCEEDED(rv) and check (a). Then we do it again with FAILED(rv) and check (b).

Dumbest Theorem Prover Evar. At this point, our problem is pretty much solved (minus inordinate effort parsing XPIDL dumps and method signatures to guess what’s an outparam and fixing bugs related to receiver argument representation differences), assuming I have a theorem prover handy. Which I don’t. Writing one is out of the question, it would take way too long. I didn’t even want to try to reuse an existing one at this prototyping stage, because before figuring out how to use the prover, I’d have to search around for one that fits my requirements, test its scalability for my application, and so on.

So instead I set out to design the dumbest theorem prover that could solve my formulas. I realized that my formula components (some may call them “conjuncts”) are generated by assignment statements, and when we solve the formulas, in each step we learn something about the left-hand side of an assignment and use it to infer something about the right-hand side. If we represent formulas accordingly, solving is easy. Here’s an example: Above, we needed to solve this formula:

tmp == rv, if.temp  SUCCEEDED(tmp), not if.temp

We’ll represent the first two conjuncts like this:

tmp:          [ANY](tmp)     => [ANY](rv)
if.temp:      TRUE(if.temp)  => SUCCEEDED(tmp)
if.temp:      FALSE(if.temp) => FAILED(tmp)

The name before the colon is the left-hand side of an assignment, which tells us that any time we learn a fact about that variable, we should apply this rule. After the colon is a standard implication. On the tmp line, we have the special notation [ANY], which just means that any predicate true of tmp is also true of rv (because they are
equal).

Now, to solve, we assume FALSE(if.temp) and see what happens. We have a new fact about if.temp, so we look up its rules and find two. The first has TRUE(if.temp), so it doesn’t match. The second has FALSE(if.temp), a match, so we infer a second fact, FAILED(tmp). We look for tmp rules and find one. Because it has [ANY], it automatically matches and tells us to infer FAILED(rv), which is the answer we need. We also look for rv rules, but don’t find any, so we’re done.

The best part is, the solver algorithm is 14 lines of Python.

Finishing up. It’s not obvious how to implement this algorithm as a standard-ish flow-sensitive analysis (although I’m sure it’s possible). This is because you need to know how to merge two states when control flow rejoins after an if statement, and I don’t know how to merge two of these formulas. So I went back to the Dehydra Classic idea of running a path-sensitive analysis and pruning paths if we have previously analyzed the same program point in the exact same state. I also try to make the analysis forget formulas that it doesn’t need any more, so that it’s more likely the states match and we get to skip a path. The analysis runs in a reasonable length of time, although it’s not exactly fast at this point. It’s not necessarily because of the
analysis algorithm: it could be just the time to parse the JSON method CFGs or some (avoidable) overhead like that.

I was happy to discover that some fairly tricky analysis reasoning could be carried out by such a simple prover. It took a lot of hard thinking to get there. I didn’t figure it out in two clean steps like I explained above: really, I went back and forth between how to express the properties logically and how to solve them, with frequent stops just to be confused, trying to make each part simpler in a way that also made the rest simpler. The final result looks like a tiny version of Prolog, if I have any memory of what that language is.

The code is all in my Mercurial repository. The analysis itself is in the Python file checkOutparamProto.py.

Next I have to debug the analysis so it runs correctly on Firefox. After that, it’s supposed to be turned into Javascript that runs under Treehydra, which sounds pretty hard right, but we’ll see.

If any brave person is interested in this sort of thing, we could definitely use help with creating/integrating provers, optimizing analysis/proof engine performance, improving path exploration algorithms, reengineering all of this to run in Javascript over Treehydra CFGs, and anything else that helps.

Comments

Comment from Robert O’Callahan
Time: March 10, 2008, 6:19 pm

One technique which helps with tracking values through temporaries is value numbering. Basically you introduce a new abstract value for every assignment that’s not a simple copy; these abstract values represent equivalence classes which you can then use to decide simple equalities.

That isn’t enough for the case analysis side of your problem, of course. Sounds fun.

Comment from Rich Dougherty
Time: March 10, 2008, 9:35 pm

Hi David

How about trying a constraint programming system?

I haven’t done any work with them before, although I’ve read a little. But I managed to hack up something fairly quickly that seems to give a solution to one of your examples. The code is in MiniZinc, something I hadn’t heard of before today!

var int: rv;
var int: tmp;
var int: iftemp;

predicate successful(var int: returnvalue) =
returnvalue = 0;

predicate ns_succeeded(var int: value, var int: check_result) =
(successful(value) /\ check_result = 1) \/
(not successful(value) /\ check_result = 0);

constraint
tmp = rv /\
ns_succeeded(tmp, iftemp) /\
iftemp = 0 /\
not successful(rv);

solve satisfy;

To run it, I downloaded the G12 MiniZinc distribution, then I run it with mzn2fzn outparms.mzn && flatzinc outparms.fzn. The output is below.

iftemp = 0;

rv = -2097152;

tmp = -2097152;

But if I change the last not successful(rv) to just successful(rv), then no solutions are found. This means that rv must be not successful. i.e. a failure code.

In terms of automating this, you should be able to do the same work in an embeddable constraint programming library, like Gecode. Gecode has a FlatZinc interpreter, so you can move from handcoded MiniZinc examples to automation step by step.

Cheers
Rich

Comment from Manu
Time: March 11, 2008, 6:51 am

I’ve just been looking at some theorem proving stuff, and the hot new thing seems to be sat-modulo-theories (SMT) provers. Three available ones are Z3, Yices, and CVC3:

http://research.microsoft.com/projects/z3/
http://yices.csl.sri.com/
http://www.cs.nyu.edu/acsys/cvc3/

CVC3 has the advantage of being open source; not sure about the license details for the others. I haven’t completely understood your example, but if I recall our nifty automated deduction class correctly, I think the prover should be able to handle your formulas mostly just using uninterpreted functions.

Comment from dmandelin
Time: March 11, 2008, 3:01 pm

Thanks! I just tried out Rich’s example in G12 MiniZinc, and it worked. I can even leave off a predicate on rv and the solution will print out an assignment for rv. I guess that doesn’t prove that rv must have that value, though. And I’m looking at CVC3 docs right now.

I think Taras might be interested in this stuff too; I recall he always wanted to do infeasible path elimination in Dehydra, and a solver like this would make it a lot easier.

Another good thing about having a real solver is that it easily takes care of another detail I papered over in my work on this so far. In the real Firefox code, NS_SUCCEEDED is not a function, but rather:

#define NS_SUCCEEDED(_nsresult) (NS_LIKELY(!((_nsresult) & 0×80000000)))

So the code sequence actually looks more like:

rv1 = rv
t1 = rv1 < 0
t2 = !t1
t3 = __builtin_expect(t2)
if (t3)

I just coded up the constraints directly from the C semantics (and assuming __builtin_expect is a no-op) and MiniZinc was able to solve it correctly. Pretty cool! Here’s my code:

var int: rv;
var int: rv1;
var int: t1;
var int: t2;
var int: t3;

predicate succ(var int: rv) = rv >= 0;
predicate fail(var int: rv) = rv = 0;

predicate true_if_not(var int: lhs, var int: rhs) =
lhs = 1 /\ c_false(rhs) \/ lhs = 0 /\ c_true(rhs);

constraint
rv1 = rv /\
true_if_ltz(t1, rv1) /\
true_if_not(t2, t1) /\
t3 = t2 /\
c_false(t3) /\
fail(rv);

solve satisfy;

Comment from seo company
Time: August 7, 2010, 11:37 pm

Where did you got this much info on your blog from?? Also can i take the initiave to take the feeds from your blog for my own website?? But cant find the RSS feeds link here!!

Comment from seo
Time: October 13, 2010, 6:53 am

It’s an interesting approach. I commonly see unexceptional views on the subject but yours it’s written in a pretty unusual fashion. Surely, I will revisit your website for additional info.

Comment from ALISE
Time: October 13, 2010, 9:45 pm

Well, the article is actually the sweetest topic on this related issue. I fit in with your conclusions and will thirstily look forward to your forthcoming updates.

Comment from tax disc holders
Time: November 24, 2010, 11:17 am

Fantastic post! I dont think Ive seen all the angles of this subject the way youve pointed them out. Youre a true star, a rock star man. Youve got so much to say and know so much about the subject that I think you should just teach a class about it