STP command line interface

From Practical Software Verification

The following are some basic examples of using STP through its command line interface. For a full explanation of all available commands and their syntax and semantics see the STP website

STP is used in a number of tools including EXE and catchconv/smartfuzz

nnp@bin$ cat testinput
x, y : BITVECTOR(32);

QUERY(BVGT(x, y));
COUNTEREXAMPLE;

nnp@bin$ ./stp testinput
Invalid.
ASSERT( x  = 0hex00000000  );
ASSERT( y  = 0hex00000000  );

In the above example I have created two bit-vectors of width 32 and then used the BVGT() query (Bit-Vector Greater Than), which does pretty much what you would expect. This results in a query to STP which attempts to determine if the query is valid given what it has been told so far. Validity means something particular in this case, that is, a query is valid iff it is true for all valuations of its variables.

As we have not limited the values of x and y then it is obvious that the above query is not valid and the COUNTEREXAMPLE command directs STP to provide us with an assignments to variables that would make it invalid.

Now lets consider something a bit more complicated. Say we have the predicate abstraction of a program based on the following 3 predicates

• ((x&1)==0) i.e. x is even
• (x > y)
• (y == 0)

(If you're not sure what a predicate abstraction is, just consider it a completely connected graph with 8 nodes, in this case, where each vertex represents a particular state in the program where each of the predicates is true or false. So there is a state representing ((x&1)==0, x > y, y == 0) and also ((x&1)!=0, x > y, y == 0) and so on. We then consider each of the programs instructions to effect 0 or more of the predicates and at each instruction we transition between the states according to the truth of the predicates)

Now, let's assume we just encountered the instruction x = x + 1 and we want to determine what transitions are allowed in the graph mentioned above. This is necessary in many model checking algorithms. One way to do this is to encode each potential transition as a propositional formula, translate this to STP's syntax and then ask STP if the resulting input is valid. Assume we consider the case where we want to check if it is possible to transition from the state where all predicates are true to the same state. The propositional formula looks as follows

((x&1)==0) && x > y && y == 0 && x' = x + 1 && y' = y && (x'&1)==0) && x' > y' && y' == 0)

In the above case the unprimed values represent the current state and the primes the next state. Notice we also specify a next state value for the variables not encountered in the update statement. If we don't do this then some model checking algorithms would consider the variables not mentioned to be unconstrained in the next state.

We can then translate this into STP's syntax as follows

nnp@bin$ cat testinput2
x, y, x1, y1 : BITVECTOR(32);

ASSERT(x1 = (BVPLUS(32, x, 0hex00000001)));
ASSERT(y1 = y);

ASSERT(
(x&0hex00000001) = 0hex00000000
AND
BVGT(x, y)
AND
y = 0hex00000000
);

QUERY(
(x1&0hex00000001) = 0hex00000000
AND
BVGT(x1, y1)
AND
y1 = 0hex00000000
);

COUNTEREXAMPLE;
sean@bin$ ./stp testinput2
Invalid.
ASSERT( x1  = 0hex40000001  );
ASSERT( x  = 0hex40000000  );
ASSERT( y  = 0hex00000000  );
ASSERT( y1  = 0hex00000000  );

Notice the use of ASSERT to specify the next state values (x1/y1 represent x'/y'). We also ASSERT that the initial three propositions are true as we want to check transitions from this state to the potential next state. The result from STP tells us that this transition is not valid, remembering our definition for validity we know this means that there are particular variable assignments where this transition cannot be made. The presented counter-example being one. Now obviously we know that it is impossible for x = x+1 and the 'x is even' predicate to maintain it's same value and it would be nice if we could get STP to tell us this. To do this we need STP to tell us if the formula is satisfiable. That is, is there any assignment of variables that make this transition possible. Iterating exhaustively through every possible counter example to conclude this isn't feasible but luckily we can change our formula and come to the same conclusion.

STP, to the best of my knowledge doesn't have a query for satisfiability directly but we can perform the following transformation and achieve the same result. Given a formula p we can conclude that p is satisfiable if the negation of p is invalid. Intuitively, this means that p is satisfiable if !p isn't always true. So, if we get the negation of our formula and STP tells us that it is in fact valid we can conclude that the transition is not possible for any assignment of variables. Computing the negation of a formula is pretty trivial, (DeMorgan's laws) so I won't go into it, but after performing this transformation and changing it into STP's syntax we get the following input.

nnp@bin$ cat testinput3
x, y, x1, y1 : BITVECTOR(32);

ASSERT(x1 = (BVPLUS(32, x, 0hex00000001)));
ASSERT(y1 = y);

ASSERT(
(x&0hex00000001) = 0hex00000000
AND
BVGT(x, y)
AND
y = 0hex00000000
);

QUERY(
NOT((x1&0hex00000001) = 0hex00000000)
OR
NOT(BVGT(x1, y1))
OR
NOT(y1 = 0hex00000000)
);

COUNTEREXAMPLE
nnp@bin$ ./stp testinput3
Valid.

STP tells us this is valid, we conclude our initial formula is unsatisfiable and all is good in the world.