python - Is it possible to get a legit range info when using a SMT constraint with Z3

Question

So basically I am trying to solve the following SMT constraint with a generic constraint solver like Z3:

>>> from z3 import *
>>> a = BitVec("a", 32)
>>> b = BitVec("b", 32)
>>> c1 = (a + 32) & (b & 0xff)
>>> c2 = (b & 0xff)
>>> s = Solver()
>>> s.add(c1 == c2)
>>> s.check()
sat
>>> s.model()
[b = 0, a = 4294967199]

Note that obviously, the constraint should be sat whenever b falls within the range of [0x00000000, 0xffffff00].

So here is my question, is it in general feasible for a SMT solver like Z3 to provide the "range" information, of a satisfiable constraint? Thanks.

Answer 1

If you are asking for a valid "widest" range of values such that your property will be satisfied for all numbers in that range, that would be a quantified optimization problem. (Also, what "widest" means in this context can be hard to express.) Currently, neither z3 nor any other SMT solver I'm aware of can handle such problems, unfortunately.

However, if you are looking for the minimum and maximum values of b such that your property will hold, then you can use the Optimize class for that:

from z3 import *

a = BitVec("a", 32)
b = BitVec("b", 32)
c1 = (a + 32) & (b & 0xff)
c2 = (b & 0xff)

s = Optimize()
s.add(c1 == c2)

min_b = s.minimize(b)
max_b = s.maximize(b)
s.set('priority', 'box')
s.check()

print "min b = %s" % format(min_b.value().as_long(), '#x')
print "max b = %s" % format(max_b.value().as_long(), '#x')

This prints:

min b = 0x0
max b = 0xffffffff

[Aside: The max value of b differs from what you predicted it would be. But what z3 is saying looks good to me: If you pick a to be 0x7fffffdf, then a+32 will be 0x7fffffff, which is all 1s; and thus c1 and c2 will be equivalent for any value of b. So nothing here really constrains b in any way. Perhaps you had a different constraint in mind?]

But more importantly, note that this does not mean your property will be true for all values of b in this range: All it's saying is that of all the values of b that satisfy your property, these are the minimum and maximum values b can assume. (In this particular case, it turns out that all values within that range satisfy it, but that's something we deduced ourselves.) For instance, if you add a constraint that b is not 5, you will still get these bounds. I hope that's clear!