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 .. raw:: html Install instructions ==================== On a Debian-like platform, from a clean checkout: .. code-block:: bash 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. :doc:`building` has the recipe. With `Homebrew `__: .. code-block:: bash brew install stp Or with Docker, which needs nothing installed but Docker itself, and reads the problem on standard input: .. code-block:: bash 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 :doc:`building` 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. .. toctree:: :hidden: :maxdepth: 1 building architecture 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 `__. .. Hidden: these two pages are reached from the sidebar, like the pages for people working on STP below. .. toctree:: :hidden: :maxdepth: 1 array-extensionality incremental-solving Header ------ The SMT-LIB2 format uses a header to tell the solver which type of problem is coming. Only ``set-logic`` is needed; ``set-info`` is accepted and ignored, and benchmark files usually carry it: .. code-block:: lisp (set-logic QF_ABV) (set-info :smt-lib-version 2.0) The logic names the theories the problem is written in. STP accepts these, and rejects any other name: .. list-table:: :header-rows: 1 :widths: 32 68 * - Logic - Theories * - ``QF_BV`` - bitvectors * - ``QF_ABV`` - bitvectors and arrays * - ``QF_AUFBV`` - bitvectors and arrays; the uninterpreted functions the name also allows are not supported, function declarations being nullary * - ``QF_FP`` - floating-point * - ``QF_BVFP`` - floating-point and bitvectors * - ``QF_ABVFP`` - floating-point, bitvectors and arrays * - ``QF_FPLRA``, ``QF_BVFPLRA``, ``QF_ABVFPLRA`` - as the three above, plus the real constants that appear as the argument of ``to_fp``; no other use of reals is supported 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: .. code-block:: lisp (declare-fun x () (_ BitVec 32)) An example of an array declaration with 32 bit indices, and 7 bit results is: .. code-block:: lisp (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: .. code-block:: lisp #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``. Footer ------ After defining the problem, tell STP what to do. Usually this is to check the satisfiability, then to exit: .. code-block:: lisp (check-sat) (exit) Examples -------- There are many SMT-LIB2 format examples in STP’s source code repository: look for files with a ``.smt2`` extension under |queryfiles|_. Signed division of -1/-2 = 0, should be satisfiable: .. code-block:: lisp (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 ============ .. code-block:: python 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: .. code-block:: c #include "stp/c_interface.h" #include 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|_. .. |queryfiles| replace:: ``tests/query-files`` .. _queryfiles: https://github.com/stp/stp/tree/master/tests/query-files .. |examples| replace:: ``examples/simple`` .. _examples: https://github.com/stp/stp/tree/master/examples/simple .. Hidden, so these pages are reached from the sidebar rather than from a section here: they are for people working on STP, not for people using it. .. toctree:: :hidden: :maxdepth: 1 code-guide testing releasing Awards ====== STP's speed and accuracy compare favorably with other solvers in the bitvector (QF_BV) category. .. rst-class:: awards - 1st in QF_BV in the `Single Query track `__, on all five scoring schemes, at SMT-COMP 2023 - 1st in QF_BV for `Single Query UNSAT and Single Query 24s Performance `__ at SMT-COMP 2022 - Winner of the QF_BV `incremental `__ competition at SMT-COMP 2021, and top-ranked in the `cloud `__ track, which was experimental and selected no winner - `2nd `__ in QF_BV at SMT-COMP 2014 - 2nd in QF_BV at SMT-COMP 2011, entered as *STP2* - 1st in QF_BV at SMT-COMP 2010, entered as *simplifyingSTP* - 1st at `SMT-COMP 2006 `__ Competition results are a snapshot of one year's entrants on one year's selection. :doc:`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. .. toctree:: :hidden: :maxdepth: 1 benchmarks 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. :doc:`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. - `A Decision Procedure for Bit-Vectors and Arrays `__ (`bibtex `__) 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 `__ (`bibtex `__) by Cristian Cadar, Vijay Ganesh, Peter Pawlowski, David L. Dill and Dawson R. Engler. In Proceedings of ACM Conference on Computer and Communications Security 2006 (CCS 2006), Alexandria, Virginia, October, 2006. There is also an `extended journal version `__ (`bibtex `__) in ACM Transactions on Information and System Security 12(2), 2008. - `State Joining and Splitting for the Symbolic Execution of Binaries `__ (`bibtex `__) by Trevor Hansen, Peter Schachte and Harald Søndergaard. In Proceedings of the 9th International Workshop on Runtime Verification (RV 2009), Grenoble, France, June 2009. LNCS 5779, pages 76-92. - `A Constraint Solver and its Application to Machine Code Test Generation `__ (`bibtex `__) by Trevor Hansen. PhD thesis, University of Melbourne, October 2012. 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.