Overview

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

  • Easy to embed or run standalone

  • Bindings for C and Python

  • Supports multiple query input formats

  • Open source and MIT licensed

Install instructions

On a Debian-like platform, from a clean checkout:

sudo apt-get install git build-essential cmake bison flex curl patch \
    python3 libgmp-dev
git clone https://github.com/stp/stp
cd stp
git submodule init && git submodule update
./scripts/deps/setup-cms.sh
./scripts/deps/setup-libbf.sh
mkdir build && cd build
cmake ..
cmake --build . -j$(nproc)
sudo cmake --install .

Every step is needed. ABC, mimalloc, CLI11 and SymFPU are submodules and are built as part of STP; LibBF is required; and a build with no SAT backend enabled does not configure. The two setup scripts fetch and build LibBF and the SAT solver into deps/, where the build finds them without being told where to look. libgmp-dev is in the list for CryptoMiniSat’s sake – it is the only thing that needs it, and a build without CryptoMiniSat does not.

That gives a solver backed by CryptoMiniSat, which is the default when it is the only backend compiled in. CaDiCaL is also supported and becomes the default when it is compiled in; either way --cryptominisat, --cadical and --minisat pick a compiled-in backend at run time. Building STP has the recipe.

With Homebrew:

brew install stp

Or with Docker, which needs nothing installed but Docker itself, and reads the problem on standard input:

git clone https://github.com/stp/stp
cd stp
docker build -t stp .
echo "(set-logic QF_BV)
(assert (= (bvsdiv (_ bv3 2) (_ bv2 2)) (_ bv0 2)))
(check-sat)
(exit)" | docker run --rm -i stp

Building STP covers the rest: the configuration variables, the SAT backends and how to choose between them, building against dependencies you have built but not installed, static builds, and Windows.

SMT-LIB2 input language

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. What follows is a short description of the language STP parses. For more information related to SMT-LIB, please refer to this page.

Declarations

Bitvector expressions (or terms) are constructed out of bitvector constants, bitvector variables and the functions listed below. In STP all variables have to be 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 categorised into word-level functions, bitwise functions and arithmetic functions; the predicates are listed after them.

Word-level functions

Name

Symbol

Example

Concatenation

concat

(concat (_ bv0 16) x)

Extraction

extract

((_ extract 7 0) o277135888)

Shift Left

bvshl

(bvshl x y)

Logical Shift Right

bvlshr

(bvlshr x y)

Arithmetic Shift Right

bvashr

(bvashr x y)

Zero Extension

zero_extend

((_ zero_extend 24) x)

Sign Extension

sign_extend

((_ sign_extend 24) x)

Repetition

repeat

((_ repeat 4) 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.

Arithmetic functions

Name

Symbol

Example

Addition

bvadd

(bvadd x y)

Subtraction

bvsub

(bvsub x y)

Negation

bvneg

(bvneg x)

Multiplication

bvmul

(bvmul x y)

Unsigned division

bvudiv

(bvudiv x y)

Signed division

bvsdiv

(bvsdiv x y)

Unsigned remainder

bvurem

(bvurem x y)

Signed remainder

bvsrem

(bvsrem x y)

Signed modulus

bvsmod

(bvsmod x y)

The arguments of arithmetic functions have the same length, and the result has that length too. Division and remainder are total, as SMT-LIB2 requires: bvudiv by zero is the all-ones bitvector, bvsdiv by zero is all-ones for a non-negative dividend and one for a negative one, and bvurem, bvsrem and bvsmod by zero return their first argument.

Predicates

Predicates compare two bitvectors of the same length and produce a formula rather than a term.

Name

Symbol

Example

Equality

=

(= x y)

Unsigned less than

bvult

(bvult x y)

Unsigned less or equal

bvule

(bvule x y)

Unsigned greater than

bvugt

(bvugt x y)

Unsigned greater or equal

bvuge

(bvuge x y)

Signed less than

bvslt

(bvslt x y)

Signed less or equal

bvsle

(bvsle x y)

Signed greater than

bvsgt

(bvsgt x y)

Signed greater or equal

bvsge

(bvsge x y)

STP also accepts the overflow predicates bvsaddo, bvuaddo, bvssubo, bvusubo, bvsmulo, bvumulo, bvsdivo and bvnego, and the one-bit comparison bvcomp.

Examples

There are many SMT-LIB2 format examples in STP’s source code repository: look for files with a .smt2 extension under tests/query-files. 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': 5, 'b': 6, 'c': 11}

C library usage

When STP is built it generates the libstp library – shared by default, or static if you configured with STATICCOMPILE=ON – 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/fp.hpp for the floating-point helpers

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();

  // ask for a counterexample to be built, so it can be printed below
  vc_setFlags(vc, 'c');

  // 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. vc_query returns 0 for INVALID.
  assert(ret == 0);

  //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’s speed and accuracy compare favorably with other solvers in the bitvector (QF_BV) category.

Competition results are a snapshot of one year’s entrants on one year’s selection. Benchmarks is the continuous version: every SMT-LIB benchmark STP can read, re-measured against a git commit so a change in the solver shows up as a change in the numbers.

Use cases

  • KLEE, a symbolic execution engine, 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 at the University of Utah and Google (historical: the project is archived and moved off STP)

  • S2E, begun at EPFL

  • 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 (frozen at 2013.1) (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 does word-level preprocessing and then translates what is left to SAT. Architecture walks the whole pipeline, stage by stage, with a diagram of the passes and of the three places the solver repeats itself until it reaches a fixed point.

Publications

STP is based on, and described by, the following.

History and authors

The initial versions of STP were written primarily by Vijay Ganesh as part of his PhD thesis. STP was subsequently developed by Trevor Hansen during his PhD, under the supervision of Harald Søndergaard and Peter Schachte.

Many people have contributed:

  • Vijay Ganesh — the original author: the AST, the parsers, the translation to SAT, and the preprocessing the CAV paper describes.

  • Trevor Hansen — the word-level simplifiers, constant bit propagation, the bit-blaster, and general improvements.

  • Andrew Teylu — incremental, floating-point and extensional array solving.

  • Mate Soos — the CryptoMiniSat integration, the CMake build, and much of the project’s day-to-day maintenance.

  • Ryan Govostes — packaging, the Docker images, the Python bindings’ packaging, and fixes across the code base.

  • Dan Liew — the test infrastructure and much of the C API test suite.

  • David L. Dill — co-designer of the original decision procedure, and a contributor to its first implementation at Stanford.

  • Khoo Yit Phang — parser and printer work, and the OCaml bindings.

  • Felix Kutzner — the Windows CI, and 64-bit pointer fixes in the vendored ABC.

  • Jurriaan Bremer — the original Python bindings and their packaging, including Python 3 support.

  • Norbert Manthey — the StarExec competition harness.

  • Stephen McCamant — the early build system, and packaging libstp as a library worth linking against.

  • Florian Merz — parser and lexer fixes, and Windows portability.

  • Michael Katelman — CNF conversion, and correctness fixes to counterexample construction.

  • Edward J. Schwartz — let parsing in the SMT-LIB2 frontend.

  • Philip Guo — the CVC-to-C converter.

  • Tim King — contributions to the early solver at Stanford.

And many others: the contributors page lists everyone who has committed to STP.