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.
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.
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 ), and polynomial arithmetic
- 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
andallSat
functions) - 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.
The sbv library uses third-party SMT solvers via the standard SMT-Lib interface: http://goedel.cs.uiowa.edu/smtlib/
While the library is designed to work with any SMT-Lib compliant SMT-solver, solver specific support is required for parsing counter-example/model data since there is currently no agreed upon format for getting models from arbitrary SMT solvers. (The SMT-Lib2 initiative will potentially address this issue in the future, at which point the sbv library can be generalized as well.) Currently, we only support the Yices SMT solver from SRI as far as the counter-example and model generation support is concerned: http://yices.csl.sri.com/ However, other solvers can be hooked up with relative ease.
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"
.)
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.
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.
The sbv library is distributed with the BSD3 license. See COPYRIGHT for details. The LICENSE file contains the BSD3 verbiage.
Galois, Inc. has contributed to the development of SBV, by providing time and computing machinery.
The following people reported bugs, provided comments/feedback, or contributed to the development of SBV in various ways: Ian Blumenfeld, Ian Calvert, Iavor Diatchki, Lee Pike, Austin Seipp, Don Stewart, Josef Svenningsson, and Nis Wegmann.