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 python3
git clone https://github.com/stp/stp
cd stp
./configure.sh --auto-download
cmake --build build -j$(nproc)
sudo cmake --install build

There are no submodules: everything STP does not itself contain – ABC and mimalloc, which are built as part of STP; SymFPU, CLI11 and LibBF; and CaDiCaL, the SAT backend – is fetched by that --auto-download, at pinned revisions, and built with this build’s own compiler and flags. Without it, configuration stops and says what to install or where to point it: nothing here reaches the network unless it is asked to.

That gives a solver backed by CaDiCaL. CryptoMiniSat and MiniSat are also supported, and are asked for by name – ./configure.sh --cryptominisat or --minisat; at run time --cryptominisat, --cadical and --minisat pick between the backends that were compiled in. CryptoMiniSat is the one dependency STP does not build for you, and the one that needs libgmp-dev. Building STP has the detail.

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

A declare-fun with a nonempty domain declares an uninterpreted function. Its arguments and result may be Bool, bitvectors, declared sorts, RoundingMode or floating-point sorts. For example:

(set-logic QF_UFBVFP)
(declare-fun classify ((_ FloatingPoint 8 24)) (_ BitVec 8))

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();
  vc_setInterfaceFlags(vc, EXPRDELETE, 0);

  Type bv32 = vc_bvType(vc, 32);

  // 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", bv32);

  // 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 caller-owned children while their VC is still live.
  vc_DeleteExpr(eq2);
  vc_DeleteExpr(eq);
  vc_DeleteExpr(xp1);
  vc_DeleteExpr(b);
  vc_DeleteExpr(a);
  vc_DeleteExpr(c);
  vc_DeleteExpr(bv32);

  // Destroying the VC invalidates every remaining child handle.
  vc_Destroy(vc);

  return 0;
}

If your project uses CMake, an installed STP is found with find_package() in config mode. The imported stp target carries the include directories, so nothing else has to be set:

cmake_minimum_required(VERSION 3.18)
project(my_project C)

find_package(STP REQUIRED)

add_executable(my-tool main.c)
target_link_libraries(my-tool stp)

Point CMAKE_PREFIX_PATH at the installation prefix, or set STP_DIR to the directory holding STPConfig.cmake – under lib/cmake/STP/ in the installation. A build tree is not a supported substitute: its exported targets name STP’s own dependency targets, which only exist inside STP’s build.

A worked consumer of both interfaces, built and run against a staged installation by the test suite, is in tests/api/install.

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.