SMT Solutions for Bit Vector Arithmetic

Question

I am planning several experiments on symbolic execution of C code using the built-in SMT solver and wondering which solver to use; looking at, for example, SMT contestants and, using only open source systems, narrow it down to Beaver, Boolector, CVC3, OpenSMT, Sateen, Sonolar, STP, Verit; which is still a long list.

Trying to narrow it down a bit further, I notice that some of the systems advertise the ability to process bit vector arithmetic, while others only advertise the ability to process general integer arithmetic. Basically, the first is true for C, where the variables are machine words and not unlimited integers. What is the difference in practice? What happens if you try to use a common whole system for this kind of work? Is one of the following scenarios used?

• A bit vector system is a bit more efficient, but you can use it either without a problem.

• You can use a common whole system with a few settings.

• A common whole system is great for a signed int (because the result of the overflow is undefined), but will give the wrong answer for unsigned.

• The whole whole system is simply incorrect for machine word arithmetic, and I can shorten my short list only to those systems that provide bit vector arithmetic.

• Something else...?

I tried to ask as specific a question as possible, but if anyone could suggest any other criteria for narrowing the list, that would be great!

Answer 1

I had good experience using STP for symbolic performance. STP was designed specifically for this task. In addition, there are a number of symbolic execution tools that have successfully used STP for this purpose, so there is reason to believe that STP does not suck. I would definitely recommend STP to others as the default choice for this kind of experimentation.

However, I have not tried other systems, so I do not know how STP compares with them.

Personally, I see STP as the baseline and the default for this type of application. So, if you only have time to try one solver, trying STP seems like a pretty smart choice.

If I were to guess, I would suggest that bitwise vector arithmetic is important for support, because any large system code will have a non-trivial amount of code that performs bitwise operations. In addition, I suspect / worry that some system code may rely on unsigned arithmetic to wrap modulo 2 ⁿ and if you try to model it with integers, you won’t get the C semantics (because, as you say, integers are not correct for machine word arithmetic), and therefore, if you try to use a solver with an integer, you may encounter some difficulties. However, I have no solid evidence for any of these suspicions.

PS Z3 can also be a contender to be added to your list. (Do you really need your solver for open-source, if it is free? I would expect the symbolic runtime tool to use it only as a black box without changes.)

Answer 2

According to SMT-Wikipedia in 2011-08, we have:

Based on these measures, it seems that the most striking, well-organized projects are OpenSMT, STP, and CVC4.

I am just checking this stuff - as long as all three seem reasonable, plus the older CVC -> CVC3.