SBV: Symbolic Bit Vectors in Haskell

Express properties about bit-precise Haskell programs and automatically prove them using SMT solvers.

    $ ghci -XScopedTypeVariables
    Prelude> :m Data.SBV
    Prelude Data.SBV> prove $ \(x::SWord8) -> x `shiftL` 2 .== 4*x
    Q.E.D.
    Prelude Data.SBV> prove $ forAll ["x"] $ \(x::SWord8) -> x `shiftL` 2 .== x
    Falsifiable. Counter-example:
      x = 128 :: SWord8

The function prove has the following type:

    prove :: Provable a => a -> IO ThmResult

The class Provable comes with instances for n-ary predicates, for arbitrary n. The predicates are just regular Haskell functions over symbolic signed and unsigned bit-vectors. Functions for checking satisfiability (sat and allSat) are also provided. In addition, functions using the SBV library can be compiled to C automatically.

Resources

The sbv library is hosted at http://github.com/LeventErkok/sbv.

The hackage site http://hackage.haskell.org/package/sbv is the best place for details on the API and the example use cases.

Comments, bug reports, and patches are always welcome.

Overview

The Haskell sbv library provides support for dealing with Symbolic Bit Vectors in Haskell. It introduces the types:

• SBool: Symbolic Booleans (bits)
• SWord8, SWord16, SWord32, SWord64: Symbolic Words (unsigned)
• SInt8, SInt16, SInt32, SInt64: Symbolic Ints (signed)
• Arrays of symbolic values
• Symbolic polynomials over GF(2^n ), polynomial arithmetic, and CRCs
• Uninterpreted constants and functions over symbolic values, with user defined SMT-Lib axioms

The user can construct ordinary Haskell programs using these types, which behave very similar to their concrete counterparts. In particular these types belong to the standard classes Num, Bits, (custom versions of) Eq and Ord, along with several other custom classes for simplifying bit-precise programming with symbolic values. The framework takes full advantage of Haskell's type inference to avoid many common mistakes.

Furthermore, predicates (i.e., functions that return SBool) built out of these types can also be:

• proven correct via an external SMT solver (the prove function)
• checked for satisfiability (the sat, and allSat functions)
• used in synthesis (the sat function with existentials)
• quick-checked

If a predicate is not valid, prove will return a counterexample: An assignment to inputs such that the predicate fails. The sat function will return a satisfying assignment, if there is one. The allSat function returns all satisfying assignments, lazily.

The SBV library can also compile Haskell functions that manipulate symbolic values directly to C, rendering them as straight-line C programs.

Use of SMT solvers

The sbv library uses third-party SMT solvers via the standard SMT-Lib interface: http://goedel.cs.uiowa.edu/smtlib/

The SBV library is designed to work with any SMT-Lib compliant SMT-solver. Currently, we support the Yices SMT solver from SRI: http://yices.csl.sri.com/ and the Z3 SMT solver from Microsoft: http://research.microsoft.com/en-us/um/redmond/projects/z3/

Prerequisites

You should download and install Yices (version 2.X) on your machine, and make sure the "yices" executable is in your path before using the sbv library, as it is the current default solver. Alternatively, you can specify the location of yices executable in the environment variable SBV_YICES and the options to yices in SBV_YICES_OPTIONS. The default for the latter is "-m -f".

If quantified bit-vectors are to be used, you should also install Microsoft's z3 SMT solver. Again, the environment variables SBV_Z3 and SBV_Z3_OPTIONS can be used for choosing executable location and custom options. The default for the latter is "/in /smt2". Microsoft releases Z3 natively on Windows, and Linux for SMT-Comp purposes, and you can also run it on Mac via Wine or similar emulators. You should download at least version 3.2.

Examples

Please see the files under the Examples directory for a number of interesting applications and use cases. Amongst others, it contains solvers for Sudoku and N-Queens puzzles as mandatory SMT solver examples in the Puzzles directory.

Installation

The sbv library is cabalized. Assuming you have cabal/ghc installed, it should merely be a matter of running

     cabal install sbv

Please see INSTALL for installation details.

Once the installation is done, you can run the executable SBVUnitTests which will execute the regression test suite for sbv on your machine to ensure all is well.

Copyright, License

The sbv library is distributed with the BSD3 license. See COPYRIGHT for details. The LICENSE file contains the BSD3 verbiage.

Thanks

The following people reported bugs, provided comments/feedback, or contributed to the development of SBV in various ways: Ian Blumenfeld, Ian Calvert, Iavor Diatchki, Tom Hawkins, Lee Pike, Austin Seipp, Don Stewart, Josef Svenningsson, and Nis Wegmann.