## 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.

**Posted:** March 10th, 2008 under Uncategorized.

**Comments:** 8

### Comments

**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

to just **not** successful(rv)`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

CommentfromRobert O’CallahanTime:March 10, 2008, 6:19 pmOne 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.