Quick introduction to my upcoming Python bindings for STP

[Jurriaan Bremer]

Hi there,

Over the past couple of days I've been working on Python bindings for STP. In this email I'll quickly go over a few examples to explain why it's already quite awesome. (But it's definitely still work in progress.)
Those who are interested in it - credits go to Mate Soos for suggesting I should do Python bindings ;-)

So, unlike the pySTP library which has been written as a C module, this module has been written through the use of Python's ctypes, which allows much more flexibility and a lot less overhead/bloated code.

Parts of the library have been inspired by Z3's Python bindings, thus you'll see some similarity here and there, as well as some improvements (or at least I'd like to think so) of features that I was missing in Z3's Python bindings.
I haven't yet put in a license, but it'll be the same license STP uses.

Let's start with the most basic example that still somewhat reflects the C api.

s = Solver()
a = s.bitvec('a', 32)
b = s.bitvec('b', 32)
c = s.bitvecval(32, 69)
d = s.bitvecval(32, 42)
assert s.check(b.eq(d), a.add(b).eq(c)) is True
assert s.model() == {'a': 69-42, 'b': 42}

In this snippet we create two 32-bit bitvectors ("a" and "b") and two bitvec values ("c" with the value 69 and "d" with the value 42.)
We then call the .check() function which is a wrapper around vc_query(). In this query we say that "b" must be equal to "d" (thus "b" = 42) and that "a" + "b" must be equal to "c" (thus 69.) The .check() function returns True when STP finds that this query is satisfiable, or False otherwise. At that point we can get the counter example ("model") with the .model() function. (Note that, unlike whatever it is z3py does, .model() returns a dictionary of each bitvector name with its value for this model.)

The only notable thing here is that internally I do vc_andExprN() on all expressions given to .check() and then vc_notExpr() that expression before handing it over to vc_query(). I'm not sure if it's possible to do this otherwise? Anyway it should be fine - so far so good (famous last words.)

In the next level of abstraction we have operator overloading and automatic casting of integers. Given SMT's strict bitsize requirements it is possible to automatically predict the required bitsize of a bitvec value, thus allowing us to skip the s.bitvecval(32, 42) and instead just write 42. (Referring to the first code example.)
The operator overloading allows for writing down expressions more easily. Rewriting the first example with these two features gets us the following. (Note that s.bitvecs() creates multiple bitvecs and that the default bitsize for bitvecs is 32.)

s = Solver()
a, b = s.bitvecs('a b')
assert s.check(b == 42, a + b == 69) is True
assert s.model() == {'a': 69-42, 'b': 42}

Now to allow easier access to variables from the model there's a nice shortcut;

print s['a'], s['b'] # Values of bitvecs 'a' and 'b'

There is also support for both boolean and binary and/or/xor. Binary operations are done through the normal arithmetic way, e.g., "a | b" and "a & b". Boolean and/or/xor are done through functions from the Solver class, e.g., "s.or_(a, b)".

Finally by far the most interesting part to me: automatically transforming Python AST (Abstract Syntax Trees) into STP expressions. This is still heavy work in progress, but the first PoC has already been written;

from stp import add, bitvecs, check, model, stp, Solver

@stp
def foo(a, b):
assert b != 0
return (a + 42) % b

@stp
def bar(a, b):
return a * b == 12345

with Solver():
x, y = bitvecs('x y')
while check(foo(x, y) == foo(y, x), bar(x, y)):
add(x != model('x'))
print model()

First of all - the add/bitvecs/check/model are wrappers around s.add, s.bitvecs, etc, except for the part that they're valid in the current with-context. (I'm not really sure how this is called in Python, or if this is the correct usage of the with-keyword, but it works quite nicely and I kind of like the "with Solver():" part.)

Other than that, what we see here is the @stp decorator which does all the hard work. Then, from within the with-context, we can actually call the functions as if they're regular functions, and their functionality is automatically expressed into STP internally. Currently this is about as much as the AST to STP transformation is able to handle, but this is still WIP as I mentioned and will definitely be developed further in the next few days.

For those that are interested, apparently there are four models for the latest code example; (with "x" and "y" being equal in all cases..)

{'y': 1658330539L, 'x': 1658330539L}
{'y': 3805814187L, 'x': 3805814187L}
{'y': 2636636757L, 'x': 2636636757L}
{'y': 489153109L, 'x': 489153109L}

>>> 1658330539L*1658330539L % 2**32
12345L
>>> (1658330539L + 42) % 1658330539L
42L

People that are interested in this work - please let me know. Testing, comments, ideas, and saying why I did something stupid is all welcome :-)

My fork of the project with all the work on Python bindings can be found at https://github.com/jbremer/stp. Do note that I haven't yet merged the "official" way to build libstp.so, so you might want to do that with the latest master of the official repository, and then use the .so in my fork. (I'll get right onto fixing this..)

Best regards,
Jurriaan

[Jonas Wagner]

Hi Jurriaan,

I really think this looks exciting and makes it very easy to use the solver. I don't have any project right now where I could use it, but will definitely keep this in the back of my head.

When you do things that are as advanced as Python AST parsing, what happens when the user tries to do something that STP (or your bindings) doesn't support? Will they get an error message that they can understand? For instance, what happens if I do:

a = [1, 4, 9, 16]

b = bitvecs('b')

assert a[b] > 0

My second question would be whether solver objects are copyable, threadsafe, etc. It would be cool to incrementally build a solver. That is, add some assertions, copy the solver, add some more assertions to one of the copies, and then go back to the other copy and add different assertions. This would be especially useful for applications such as symbolic executors that deal with multiple sets of assertions that share common subsets.

Cheers,

Jonas

--

---
You received this message because you are subscribed to the Google Groups "stp-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to stp-users+...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.