About Spear — Fast Bit-Vector Arithmetic Theorem Prover
Spear is an industrial strength bit-vector arithmetic (a.k.a modular arithmetic, machine arithmetic) decision procedure and a Boolean satisfiability (SAT) solver. It’s designed for proving software verification conditions, and it’s the main tool Calysto uses for bug hunting. Spear is heavily optimized and tested. Spear was one of the first publicly available decision procedures to support all standard operators, including multiplication, division, variable shifts, and so on.
The key ideas behind Spear are:
- The encoding of circuits (bit-vector operators) to propositional logic is highly optimized. I used Tseitin transform, but that's less important, the choice of the actual circuit is much more important. For instance, for encoding division, I used array dividers, as they produce the smallest number of propositional variables. Operations by constants (multiplication, reminder, division) are encoded in a special way so as to minimize the size of the circuit (and the number of created Boolean variables)
- All the search parameters are modifiable over the command line. There are dozens of different parameters. In prior work, I've used this feature for automatic optimization of search parameters for different classes of problems. On some classes, such optimization achieves up to 500X speedups!
- The library interface of Spear (not publicly available) enables various novel optimization techniques, like reusing learned lemmas among multiple runs.
The tool is freely available for research usage and can be downloaded on the download page. Chances are (95%) that I will eventually open-source Spear and put it in the public domain. If you are interested to continue Spear development and/or using Spear commercially, please drop me an email.
I'm trying to keep Spear up-to-date, as much as I can. Unfortunately, I have very little free time these days and there are several known bugs that I just haven't had time to fix. I apologize for the inconvenience these bugs might be causing you.
- All search parameters are tunable on the command line.
- Predefined parameter sets for certain types of problems. If you find a set of parameters that works particularly well on a certain set of problems, please let me know, and I’ll add it to the next release.
- Automatic parameter tuning for a specific application with ParamILS tool. See the tools page for details.
- Spear supports all standard modular arithmetic (bitvector) operators, including (un)signed division, remainder, shifting by variable number of spaces,...
- The front-end has been completely rewritten in v2.0, and there has been a number of other modifications. I do expect bugs to pop up, especially since I don’t use that interface for my work (Calysto talks directly to Spear, via API).
- Mac OS X binary is dynamically linked, while all others are linked statically.
- Starting with v2.0, Mac OS X support will be discontinued. It amounts to less than 5% of downloads.
- Certain optimizations in v2.0 won’t work on cyclic expressions. If you can, make sure your expressions are acyclic! For example, instead of:
d a:i1 Tmp1:i1
c Tmp1 ~ a
p = a Tmp1
Tmp1 is defined in terms of
a is equal to
Tmp1, try rewriting your formulas so as to be acyclic:
d a:i1 Tmp1:i1 Tmp2:i1
c Tmp1 ~ a
p = Tmp2 a
p = Tmp1 Tmp2
If you absolutely need to be able to have cyclic expressions, please send me an email, I'd really like to understand why do you need them. If you disable cse/simplify in Spear, most likely Spear will also swallow your cyclic formulas, but I'm not sure. Thanks to Evgeny Pavlenko for asking a question about this, which motivated me to write this comment.