Overview

STP is a constraint solver for the theory of quantifier-free bitvectors that can solve many kinds of problems generated by program analysis tools, theorem provers, automated bug finders, cryptographic algorithms, intelligent fuzzers and model checkers.

Research bibtex reference can be found here.

Install instructions

For Debian-like platforms first install the prerequisites:

apt-get install cmake g++ zlib1g-dev libboost-all-dev flex bison

Then install minisat:

git clone https://github.com/stp/minisat.git
cd minisat && mkdir build && cd build
cmake ..
make
sudo make install
cd ../..

Then install STP:

git clone https://github.com/stp/stp.git
cd stp && mkdir build && cd build
cmake ..
make
sudo make install

For windows-like environments: you will need to first install the zlib library then install minisat and stp exactly like above, using cmake to create Visual Studio project files, e.g. cmake .. -G "Visual Studio 10 Win64" and then building with Visual Studio.

Languages parsed

The SMT-LIB2 format is the recommended file format for use with STP, in part because it is parsed by all modern bitvector solvers. STP implements a subset of the SMT-LIB2 language; not all SMT-LIB2 features are implemented.

SMT-LIB2 Input Language Reference

This page contains a short description for the SMT-LIB version 2 input language that STP can parse. For more information related to SMT-LIB, please refer to this page.

Header

The SMT-LIB2 format uses a header to tell the solver which type of problem is coming, the header needed is:

(set-logic QF_ABV)
(set-info :smt-lib-version 2.0)

QF_BV is for bitvector problems, QF_ABV is for bitvector and array problems.

Declarations

Bitvector expressions (or terms) are constructed out of bitvector constants, bitvector variables and the functions listed below. In STP all variables have to declared before the point of use. An example declaration of a bitvector variable of length, say 32, is as follows:

(declare-fun x () (_ BitVec 32))

An example of an array declaration with 32 bit indices, and 7 bit results is:

(declare-fun a () (Array (_ BitVec 32) (_ BitVec 7)))

Functions and Terms

Bitvector variables (or terms) of length 0 are not allowed. Bitvector constants can be represented in binary or hexadecimal format. The rightmost bit is called the least significant bit (LSB), and the leftmost bit is the most significant bit (MSB). The index of the LSB is 0, and the index of the MSB is n-1 for an n-bit constant. This convention naturally extends to all bitvector expressions.

Following are some examples of bitvector constants in binary and hexadecimal:

#b0000111101010000
#x0f50

The bitvector implementation in STP supports a very large number of functions and predicates. The functions are categorized into word-level functions, bitwise functions, and arithmetic functions.

Word-level functions

Name	Symbol	Example
Concatenation	concat	(concat (_ bv0 16) x)
Extraction	extract	((_ extract 7 0) o277135888)
Left Shift	bvlshl	(bvlshl x y)
Light Shift	bvlshr	(bvlshr x y)
Sign Extension	sign_extend	((_ sign_extend 24) x)
Array READ	select	(select e829 v817)
Array WRITE	store	(store a x y)

Notes:

• For extraction terms, say ((_extract i j) t), n > i >= j >= 0, where n is the length of t.
• For left shift terms, t << k is equal to k 0’s appended to t. The length of t << k is n.
• For right shift terms, say t >> k, the term is equal to the bitvector obtained by k 0’s followed by t[n-1:k]. The length of t >> k is n.

Bitwise functions

Name	Symbol	Example
Bitwise AND	bvand	(bvand o1 o6)
Bitwise OR	bvor	(bvor var29 var30)
Bitwise NOT	bvnot	(bvnot (_ bv0 2000))
Bitwise XOR	bvxor	(bvxor e7015 e7019)

The arguments of bitwise functions have the same length.

Footer

After defining the problem, tell STP what to do. Usually this is to check the satisfiability, then to exit:

(check-sat)
(exit)

Examples

There are many SMT-LIB2 format examples in STP’s source code repository. Look for files with a .smt2 extension here. Signed division of -1/-2 = 0, should be satisfiable:

(set-logic QF_BV)
(set-info :smt-lib-version 2.0)
(set-info :status sat)
(assert (= (bvsdiv (_ bv3 2) (_ bv2 2)) (_ bv0 2)))
(check-sat)
(exit)

Python usage

import stp
s = stp.Solver()
a = s.bitvec('a', 32)
b = s.bitvec('b', 32)
c = s.bitvec('c', 32)
s.add(a == 5)
s.add(b == 6)
s.add(a + b == c)
s.check()
>>> True
s.model()
>>> {'a': 5L, 'b': 6L, 'c': 11L}

SMT-LIB2 Usage

Signed division of -1/-2 = 0, should be satisfiable.

(set-logic QF_BV)
(assert (= (bvsdiv (_ bv3 2) (_ bv2 2)) (_ bv0 2)))
(check-sat)
(exit)

C library usage

When STP is built it generates a lib/libstp.a static library which can be used with one of two header files, depending on the preferred language:

• include/stp/c_interface.h for a C interface to STP
• include/stp/cpp_interface.h for a C++ interface to STP

An example C header usage can be as simple as:

#include "stp/c_interface.h"
#include <assert.h>

int main(int argc, char **argv) {
  VC vc = vc_createValidityChecker();

  // 32-bit variable 'c'
  Expr c = vc_varExpr(vc, "c", vc_bvType(vc, 32));

  // 32 bit constant value 5
  Expr a = vc_bvConstExprFromInt(vc, 32, 5);

  // 32 bit constant value 6
  Expr b = vc_bvConstExprFromInt(vc, 32, 6);

  // a+b!=c
  Expr xp1 = vc_bvPlusExpr(vc, 32, a, b);
  Expr eq = vc_eqExpr(vc, xp1, c);
  Expr eq2 = vc_notExpr(vc, eq);

  //Is a+b!=c always correct?
  int ret = vc_query(vc, eq2);

  //No, c=a+b is a counterexample
  assert(ret == false);

  //print c = 11 counterexample
  vc_printCounterExample(vc);

  //Delete validity checker
  vc_Destroy(vc);

  return 0;
}

If you use CMake as the build system for your project it is easy to use STP as an external project. An example can be found in the sources under examples/simple.

Awards

• STP won the incremental competition in the QF_BV category in the SMTCOMP 2021<https://smt-comp.github.io/2021/results/qf-bitvec-incremental>.
• STP placed 2nd in the bitvector category in the SMTCOMP 2014, just after the Boolector system
• STP placed 2nd in the bitvector category in the SMTCOMP 2011
• STP won the bitvector category at SMTCOMP 2010
• STP won the SMTCOMP 2006 competition (Bitvector category) in 2006

Use cases

• KLEE symbolic fuzzer is using STP at its core (Professor Cristian Cadar’s group at Imperial College, London, and Professor Dawson Engler’s group at Stanford University)
• Souper project at the University of Utah and Google
• S2E at EPFL
• Mayhem fuzzer, which found over 1000 bugs in mainline Debian is using KLEE and hence STP
• Binary Analysis Platform (BAP) is using STP for analysis, by the CMU
• EXE is a symbolic-execution based bug-finding tool that reads your C program and tries to automatically crash it (Stanford University)
• MINESWEEPER is a tool that automatically analyzes certain malicious behavior in unix utilities and malware. (Carnegie Mellon University)
• CATCHCONV is a bug finding tool that tries to find bugs due to type mismatch in C programs. (University of California, Berkeley)
• Backward path-sensitive analysis of C programs to find bugs by Tim Leek from MIT Lincoln Labs
• Bug finding in Verilog code (a major microprocessor company)
• JPF-SE is a symbolic execution extension to the Java PathFinder model checker . (NASA Ames Research Center)
• Avalanche bug-finding tool (Institute of Systems Programming, Moscow, Russia)
• Low-level Bounded Model Checker - LLBMC (Karlsruhe Institute of Technology (KIT), Germany)
• FuzzGrind (ESEC Lab)
• In conjunction with ACL2 to formally verify implementation of encryption algorithms in Java (Stanford University)
• Hampi : A solver for string constraints used to automatically construct SQL injection and XSS exploits (MIT)
• Automatic configuration: Tvl2STP (University of Namur in Belgium)

Architecture

STP is an efficient decision procedure for the validity (or satisfiability) of formulas from a quantifier-free many-sorted theory of fixed-width bitvectors and (non-extensional) one-dimensional arrays. The functions in STP’s input language include concatenation, extraction, left/right shift, sign-extension, unary minus, addition, multiplication, (signed) modulo/division, bitwise Boolean operations, if-then-else terms, and array reads and writes. The predicates in the language include equality and (signed) comparators between bitvector terms.

The basic architecture of STP essentially follows the idea of word-level preprocessing followed by translation to SAT (We use MINISAT and CRYPTOMINISAT). In particular, we introduce several new heuristics for the preprocessing step, including abstraction-refinement in the context of arrays, a new bitvector linear arithmetic equation solver, and some interesting simplifications. These heuristics help us achieve several magnitudes of order performance over other tools, and also over straight-forward translation to SAT. STP has been heavily tested on thousands of examples sourced from various real-world applications such as program analysis and bug-finding tools like EXE, and equivalence checking tools and theorem-provers.

History and authors

The initial versions of STP were written primarily by Vijay Ganesh as part of his PhD thesis, and the project was later maintained by Trevor Hansen. The current primary maintainers are Mate Soos, Dan Liew, and Ryan Govostes who have improved it in many ways. STP is based on the following papers:

• A Decision Procedure for Bit-Vectors and Arrays by Vijay Ganesh and David L. Dill. In Proceedings of the International Conference in Computer Aided Verification (CAV 2007), Berlin, Germany, July 2007
• EXE: Automatically Generating Inputs of Death by Cristian Cadar, Vijay Ganesh, Peter Pawlowski, Dawson Engler, David Dill. In Proceedings of ACM Conference on Computer and Communications Security 2006 (CCS 2006), Alexandria, Virginia, October, 2006

Past contributors: Khoo Yit Phang, Ed Schwartz, Mike Katelman (PhD Student, University of Illinois, Urbana-Champaign, IL, USA), Philip Guo (Student, Stanford University, Stanford, CA, USA), David L. Dill (Professor, Stanford University, Stanford, CA, USA), Tim King (Student, Stanford University and NYU). Please note that everyone working on the project is doing so out of hobby or as a way to help them in their work/study projects.