sbv-0.9.18: Symbolic Bit Vectors: Prove bit-precise program properties using SMT solvers.

Portabilityportable
Stabilityexperimental
Maintainererkokl@gmail.com

Data.SBV

Contents

Description

(The sbv library is hosted at http://github.com/LeventErkok/sbv. Comments, bug reports, and patches are always welcome.)

SBV: Symbolic Bit Vectors in Haskell

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

>>> prove $ \x -> x `shiftL` 2 .== 4 * (x :: SWord8)
Q.E.D.
>>> prove $ forAll ["x"] $ \x -> x `shiftL` 2 .== (x :: SWord8)
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 particular, the sbv library introduces the types:

  • SBool: Symbolic Booleans (bits)
  • SWord8, SWord16, SWord32, SWord64: Symbolic Words (unsigned)
  • SInt8, SInt16, SInt32, SInt64: Symbolic Ints (signed)
  • SArray, SFunArray: Flat 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 (EqSymbolic) and Ord (OrdSymbolic), 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)
  • 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 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 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"'.)

Synopsis

Programming with symbolic values

The SBV library is really two things:

  • A framework for writing bit-precise programs in Haskell
  • A framework for proving properties of such programs using SMT solvers

In this first section we will look at the constructs that will let us construct such programs in Haskell. The goal is to have a seamless experience, i.e., program in the usual Haskell style without distractions of symbolic coding. While Haskell helps in some aspects (the Num and Bits classes simplify coding), it makes life harder in others. For instance, if-then-else only takes Bool as a test in Haskell, and comparisons (> etc.) only return Bools. Clearly we would like these values to be symbolic (i.e., SBool), thus stopping us from using some native Haskell constructs. When symbolic versions of operators are needed, they are typically obtained by prepending a dot, for instance == becomes .==. Care has been taken to make the transition painless. In particular, any Haskell program you build out of symbolic components is fully concretely executable within Haskell, without the need for any custom interpreters. (They are truly Haskell programs, not AST's built out of pieces of syntax.) This provides for an integrated feel of the system, one of the original design goals for SBV.

Symbolic types

Symbolic bit

type SBool = SBV BoolSource

A symbolic boolean/bit

Unsigned symbolic bit-vectors

type SWord8 = SBV Word8Source

8-bit unsigned symbolic value

type SWord16 = SBV Word16Source

16-bit unsigned symbolic value

type SWord32 = SBV Word32Source

32-bit unsigned symbolic value

type SWord64 = SBV Word64Source

64-bit unsigned symbolic value

Signed symbolic bit-vectors

type SInt8 = SBV Int8Source

8-bit signed symbolic value, 2's complement representation

type SInt16 = SBV Int16Source

16-bit signed symbolic value, 2's complement representation

type SInt32 = SBV Int32Source

32-bit signed symbolic value, 2's complement representation

type SInt64 = SBV Int64Source

64-bit signed symbolic value, 2's complement representation

Arrays of symbolic values

class SymArray array whereSource

Flat arrays of symbolic values An array a b is an array indexed by the type SBV a, with elements of type SBV b If an initial value is not provided in newArray_ and newArray methods, then the elements are left unspecified, i.e., the solver is free to choose any value. This is the right thing to do if arrays are used as inputs to functions to be verified, typically.

While it's certainly possible for user to create instances of SymArray, the SArray and SFunArray instances already provided should cover most use cases in practice. (There are some differences between these models, however, see the corresponding declaration.)

Minimal complete definition: All methods are required, no defaults.

Methods

newArray_ :: (HasSignAndSize a, HasSignAndSize b) => Maybe (SBV b) -> Symbolic (array a b)Source

Create a new array, with an optional initial value

newArray :: (HasSignAndSize a, HasSignAndSize b) => String -> Maybe (SBV b) -> Symbolic (array a b)Source

Create a named new array, with an optional initial value

readArray :: array a b -> SBV a -> SBV bSource

Read the array element at a

resetArray :: SymWord b => array a b -> SBV b -> array a bSource

Reset all the elements of the array to the value b

writeArray :: SymWord b => array a b -> SBV a -> SBV b -> array a bSource

Update the element at a to be b

mergeArrays :: SymWord b => SBV Bool -> array a b -> array a b -> array a bSource

Merge two given arrays on the symbolic condition Intuitively: mergeArrays cond a b = if cond then a else b. Merging pushes the if-then-else choice down on to elements

data SArray a b Source

Arrays implemented in terms of SMT-arrays: http://goedel.cs.uiowa.edu/smtlib/theories/ArraysEx.smt2

  • Maps directly to SMT-lib arrays
  • Reading from an unintialized value is OK and yields an uninterpreted result
  • Can check for equality of these arrays
  • Cannot quick-check theorems using SArray values
  • Typically slower as it heavily relies on SMT-solving for the array theory

Instances

SymArray SArray 
(HasSignAndSize a, HasSignAndSize b) => Show (SArray a b) 
SymWord b => Mergeable (SArray a b) 
EqSymbolic (SArray a b) 

data SFunArray a b Source

Arrays implemented internally as functions

  • Internally handled by the library and not mapped to SMT-Lib
  • Reading an uninitialized value is considered an error (will throw exception)
  • Cannot check for equality (internally represented as functions)
  • Can quick-check
  • Typically faster as it gets compiled away during translation

Instances

SymArray SFunArray 
(HasSignAndSize a, HasSignAndSize b) => Show (SFunArray a b) 
(SymWord b, Arbitrary b) => Arbitrary (SFunArray a b) 
SymWord b => Mergeable (SFunArray a b) 

mkSFunArray :: SBV b -> SFunArray a bSource

Make a constant fun-array always returning a fixed value. Useful for creating arrays in a pure context. (Otherwise use newArray.)

Operations on symbolic words

Word level

bitValue :: (Bits a, SymWord a) => SBV a -> Int -> SBoolSource

Replacement for testBit. Since testBit requires a Bool to be returned, we cannot implement it for symbolic words. Index 0 is the least-significant bit.

setBitTo :: (Bits a, SymWord a) => SBV a -> Int -> SBool -> SBV aSource

Generalization of setBit based on a symbolic boolean. Note that setBit and clearBit are still available on Symbolic words, this operation comes handy when the condition to set/clear happens to be symbolic

oneIf :: (Num a, SymWord a) => SBool -> SBV aSource

Returns 1 if the boolean is true, otherwise 0

lsb :: (Bits a, SymWord a) => SBV a -> SBoolSource

Least significant bit of a word, always stored at index 0

msb :: (Bits a, SymWord a) => SBV a -> SBoolSource

Most significant bit of a word, always stored at the last position

List level

allEqual :: (Eq a, SymWord a) => [SBV a] -> SBoolSource

Returns (symbolic) true if all the elements of the given list are the same

allDifferent :: (Eq a, SymWord a) => [SBV a] -> SBoolSource

Returns (symbolic) true if all the elements of the given list are different

Blasting/Unblasting

blastBE :: (Bits a, SymWord a) => SBV a -> [SBool]Source

Big-endian blasting of a word into its bits. Also see the FromBits class

blastLE :: (Bits a, SymWord a) => SBV a -> [SBool]Source

Little-endian blasting of a word into its bits. Also see the FromBits class

class FromBits a whereSource

Unblasting a value from symbolic-bits. The bits can be given little-endian or big-endian. For a signed number in little-endian, we assume the very last bit is the sign digit. This is a bit awkward, but it is more consistent with the reverse view of little-big-endian representations

Minimal complete definiton: fromBitsLE

Methods

fromBitsLE :: [SBool] -> aSource

fromBitsBE :: [SBool] -> aSource

Splitting, joining, and extending

class Splittable a b | b -> a whereSource

Splitting an a into two b's and joining back. Intuitively, a is a larger bit-size word than b, typically double. The extend operation captures embedding of a b value into an a without changing its semantic value.

Minimal complete definition: All, no defaults.

Methods

split :: a -> (b, b)Source

(#) :: b -> b -> aSource

extend :: b -> aSource

Polynomial arithmetic

class Bits a => Polynomial a whereSource

Implements polynomial addition, multiplication, division, and modulus operations over GF(2^n). NB. Similar to bvQuotRem, division by 0 is interpreted as follows:

x pDivMod 0 = (0, x)

for all x (including 0)

Minimal complete definiton: pMult, pDivMod, showPoly

Methods

polynomial :: [Int] -> aSource

Given bit-positions to be set, create a polynomial For instance

polynomial [0, 1, 3] :: SWord8

will evaluate to 11, since it sets the bits 0, 1, and 3. Mathematicans would write this polynomial as x^3 + x + 1. And in fact, showPoly will show it like that.

pAdd :: a -> a -> aSource

Add two polynomials in GF(2^n)

pMult :: (a, a, [Int]) -> aSource

Multiply two polynomials in GF(2^n), and reduce it by the irreducible specified by the polynomial as specified by coefficients of the third argument. Note that the third argument is specifically left in this form as it is usally in GF(2^(n+1)), which is not available in our formalism. (That is, we would need SWord9 for SWord8 multiplication, etc.) Also note that we do not support symbolic irreducibles, which is a minor shortcoming. (Most GF's will come with fixed irreducibles, so this should not be a problem in practice.)

Passing [] for the third argument will multiply the polynomials and then ignore the higher bits that won't fit into the resulting size.

pDiv :: a -> a -> aSource

Divide two polynomials in GF(2^n), see above note for division by 0

pMod :: a -> a -> aSource

Compute modulus of two polynomials in GF(2^n), see above note for modulus by 0

pDivMod :: a -> a -> (a, a)Source

Division and modulus packed together

showPoly :: a -> StringSource

Display a polynomial like a mathematician would (over the monomial x)

Conditionals: Mergeable values

class Mergeable a whereSource

Symbolic choice operator, parameterized via a class select is a total-indexing function, with the default.

Minimal complete definition: symbolicMerge

Methods

symbolicMerge :: SBool -> a -> a -> aSource

Merge two values based on the condition

ite :: SBool -> a -> a -> aSource

Choose one or the other element, based on the condition. This is similar to symbolicMerge, but it has a default implementation that makes sure it's short-cut if the condition is concrete

select :: (Bits b, SymWord b, Integral b) => [a] -> a -> SBV b -> aSource

Total indexing operation. select xs default index is intuitively the same as xs !! index, except it evaluates to default if index overflows

Instances

Mergeable () 
Mergeable Mostek 
Mergeable Status 
Mergeable a => Mergeable [a] 
Mergeable a => Mergeable (Maybe a) 
SymWord a => Mergeable (SBV a) 
Mergeable a => Mergeable (Move a) 
Mergeable b => Mergeable (a -> b) 
(Mergeable a, Mergeable b) => Mergeable (Either a b) 
(Mergeable a, Mergeable b) => Mergeable (a, b) 
(Ix a, Mergeable b) => Mergeable (Array a b) 
SymWord b => Mergeable (SFunArray a b) 
SymWord b => Mergeable (SArray a b) 
(Mergeable a, Mergeable b, Mergeable c) => Mergeable (a, b, c) 
(Mergeable a, Mergeable b, Mergeable c, Mergeable d) => Mergeable (a, b, c, d) 
(Mergeable a, Mergeable b, Mergeable c, Mergeable d, Mergeable e) => Mergeable (a, b, c, d, e) 
(Mergeable a, Mergeable b, Mergeable c, Mergeable d, Mergeable e, Mergeable f) => Mergeable (a, b, c, d, e, f) 
(Mergeable a, Mergeable b, Mergeable c, Mergeable d, Mergeable e, Mergeable f, Mergeable g) => Mergeable (a, b, c, d, e, f, g) 

Symbolic equality

class EqSymbolic a whereSource

Symbolic Equality. Note that we can't use Haskell's Eq class since Haskell insists on returning Bool Comparing symbolic values will necessarily return a symbolic value.

Minimal complete definition: .==

Methods

(.==) :: a -> a -> SBoolSource

(./=) :: a -> a -> SBoolSource

Instances

Symbolic ordering

class (Mergeable a, EqSymbolic a) => OrdSymbolic a whereSource

Symbolic Comparisons. Similar to Eq, we cannot implement Haskell's Ord class since there is no way to return an Ordering value from a symbolic comparison. Furthermore, OrdSymbolic requires Mergeable to implement if-then-else, for the benefit of implementing symbolic versions of max and min functions.

Minimal complete definition: .<

Methods

(.<) :: a -> a -> SBoolSource

(.>=) :: a -> a -> SBoolSource

(.>) :: a -> a -> SBoolSource

(.<=) :: a -> a -> SBoolSource

smin :: a -> a -> aSource

smax :: a -> a -> aSource

Division

class BVDivisible a whereSource

The BVDivisible class captures the essence of division of words. Unfortunately we cannot use Haskell's Integral class since the Real and Enum superclasses are not implementable for symbolic bit-vectors. However, quotRem makes perfect sense, and the BVDivisible class captures this operation. One issue is how division by 0 behaves. The verification technology requires total functions, and there are several design choices here. We follow Isabelle/HOL approach of assigning the value 0 for division by 0. Therefore, we impose the following law:

 x bvQuotRem 0 = (0, x)

Note that our instances implement this law even when x is 0 itself.

Minimal complete definition: bvQuotRem

Methods

bvQuotRem :: a -> a -> (a, a)Source

The Boolean class

class Boolean b whereSource

The Boolean class: a generalization of Haskell's Bool type Haskell Bool and SBV's SBool are instances of this class, unifying the treatment of boolean values.

Minimal complete definition: true, bnot, &&& However, it's advisable to define false, and ||| as well (typically), for clarity.

Methods

true :: bSource

logical true

false :: bSource

logical false

bnot :: b -> bSource

complement

(&&&) :: b -> b -> bSource

and

(|||) :: b -> b -> bSource

or

(~&) :: b -> b -> bSource

nand

(~|) :: b -> b -> bSource

nor

(<+>) :: b -> b -> bSource

xor

(==>) :: b -> b -> bSource

implies

(<=>) :: b -> b -> bSource

equivalence

fromBool :: Bool -> bSource

cast from Bool

Generalizations of boolean operations

bAnd :: Boolean b => [b] -> bSource

Generalization of and

bOr :: Boolean b => [b] -> bSource

Generalization of or

bAny :: Boolean b => (a -> b) -> [a] -> bSource

Generalization of any

bAll :: Boolean b => (a -> b) -> [a] -> bSource

Generalization of all

Pretty-printing and reading numbers in Hex & Binary

class PrettyNum a whereSource

PrettyNum class captures printing of numbers in hex and binary formats; also supporting negative numbers.

Minimal complete definition: hexS and binS

Methods

hexS :: a -> StringSource

Show a number in hexadecimal (starting with 0x and type.)

binS :: a -> StringSource

Show a number in binary (starting with 0b and type.)

hex :: a -> StringSource

Show a number in hex, without prefix, or types.

bin :: a -> StringSource

Show a number in bin, without prefix, or types.

readBin :: Num a => String -> aSource

A more convenient interface for reading binary numbers, also supports negative numbers

Uninterpreted constants and functions

class Uninterpreted a whereSource

Uninterpreted constants and functions. An uninterpreted constant is a value that is indexed by its name. The only property the prover assumes about these values are that they are equivalent to themselves; i.e., (for functions) they return the same results when applied to same arguments. We support uninterpreted-functions as a general means of black-box'ing operations that are irrelevant for the purposes of the proof; i.e., when the proofs can be performed without any knowledge about the function itself.

Minimal complete definition: uninterpretWithHandle. However, most instances in practice are already provided by SBV, so end-users should not need to define their own instances.

Methods

uninterpret :: String -> aSource

Uninterpret a value, receiving an object that can be used instead. Use this version when you do not need to add an axiom about this value.

uninterpretWithHandle :: String -> (SBVUF, a)Source

Uninterpret a value, but also get a handle to the resulting object. This handle can be used to add axioms for this object. (See addAxiom.)

Instances

HasSignAndSize a => Uninterpreted (SBV a) 
(HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted ((SBV c, SBV b) -> SBV a) 
(HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted ((SBV d, SBV c, SBV b) -> SBV a) 
(HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted ((SBV e, SBV d, SBV c, SBV b) -> SBV a) 
(HasSignAndSize f, HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted ((SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) 
(HasSignAndSize g, HasSignAndSize f, HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted ((SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) 
(HasSignAndSize h, HasSignAndSize g, HasSignAndSize f, HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted ((SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) 
(HasSignAndSize h, HasSignAndSize g, HasSignAndSize f, HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted (SBV h -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) 
(HasSignAndSize g, HasSignAndSize f, HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted (SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) 
(HasSignAndSize f, HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted (SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) 
(HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted (SBV e -> SBV d -> SBV c -> SBV b -> SBV a) 
(HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted (SBV d -> SBV c -> SBV b -> SBV a) 
(HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted (SBV c -> SBV b -> SBV a) 
(HasSignAndSize b, HasSignAndSize a) => Uninterpreted (SBV b -> SBV a) 

Accessing the handle

data SBVUF Source

An uninterpreted function handle. This is the handle to be used for adding axioms about uninterpreted constants/functions. Note that we will leave this abstract for safety purposes

sbvUFName :: SBVUF -> StringSource

Get the name associated with the uninterpreted-value; useful when constructing axioms about this UI.

Adding axioms

addAxiom :: String -> [String] -> Symbolic ()Source

Add a user specified axiom to the generated SMT-Lib file. Note that the input is a mere string; we perform no checking on the input that it's well-formed or is sensical. A separate formalization of SMT-Lib would be very useful here.

Proving properties

The SBV library provides a push-button verification system via automated SMT solving. The design goal is to let SMT solvers be used without any knowledge of how SMT solvers work or how different logics operate. The details are hidden behind the SBV framework, providing Haskell programmers with a clean API that is unencumbered by the details of individual solvers. To that end, we use the SMT-Lib standard (http://goedel.cs.uiowa.edu/smtlib/) to communicate with arbitrary SMT solvers. Unfortunately, the SMT-Lib version 1.X does not standardize how models are communicated back from solvers, so there is some work in parsing individual SMT solver output. The 2.X version of the SMT-Lib standard (not yet implemented by SMT solvers widely, unfortunately) will bring new standard features for getting models; at which time the SBV framework can be modified into a truly plug-and-play system where arbitrary SMT solvers can be used.

Predicates

type Predicate = Symbolic SBoolSource

A predicate is a symbolic program that returns a (symbolic) boolean value. For all intents and purposes, it can be treated as an n-ary function from symbolic-values to a boolean. The Symbolic monad captures the underlying representation, and can/should be ignored by the users of the library, unless you are building further utilities on top of SBV itself. Instead, simply use the Predicate type when necessary.

class Provable a whereSource

A type a is provable if we can turn it into a predicate. Note that a predicate can be made from a curried function of arbitrary arity, where each element is either a symbolic type or up-to a 7-tuple of symbolic-types. So predicates can be constructed from almost arbitrary Haskell functions that have arbitrary shapes. (See the instance declarations below.)

Methods

forAll_ :: a -> PredicateSource

Turns a value into a predicate, internally naming the inputs. In this case the sbv library will use names of the form s1, s2, etc. to name these variables Example:

  forAll_ $ \(x::SWord8) y -> x `shiftL` 2 .== y

is a predicate with two arguments, captured using an ordinary Haskell function. Internally, x will be named s0 and y will be named s1.

forAll :: [String] -> a -> PredicateSource

Turns a value into a predicate, allowing users to provide names for the inputs. If the user does not provide enough number of names for the free variables, the remaining ones will be internally generated. Note that the names are only used for printing models and has no other significance; in particular, we do not check that they are unique. Example:

  forAll ["x", "y"] $ \(x::SWord8) y -> x `shiftL` 2 .== y

This is the same as above, except the variables will be named x and y respectively, simplifying the counter-examples when they are printed.

Instances

Provable SBool 
Provable Predicate 
(SymWord a, SymWord b, Provable p) => Provable ((SBV a, SBV b) -> p) 
(SymWord a, SymWord b, SymWord c, Provable p) => Provable ((SBV a, SBV b, SBV c) -> p) 
(SymWord a, SymWord b, SymWord c, SymWord d, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d) -> p) 
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) 
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) 
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) 
(HasSignAndSize a, HasSignAndSize b, SymArray array, Provable p) => Provable (array a b -> p) 
(SymWord a, Provable p) => Provable (SBV a -> p) 

class Equality a whereSource

Equality as a proof method. Allows for very concise construction of equivalence proofs, which is very typical in bit-precise proofs.

Methods

(===) :: a -> a -> IO ThmResultSource

Instances

(SymWord a, SymWord b, EqSymbolic z) => Equality ((SBV a, SBV b) -> z) 
(SymWord a, SymWord b, SymWord c, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c) -> z) 
(SymWord a, SymWord b, SymWord c, SymWord d, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d) -> z) 
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e) -> z) 
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> z) 
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> z) 
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> z) 
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> z) 
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> z) 
(SymWord a, SymWord b, SymWord c, SymWord d, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> z) 
(SymWord a, SymWord b, SymWord c, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> z) 
(SymWord a, SymWord b, EqSymbolic z) => Equality (SBV a -> SBV b -> z) 
(SymWord a, EqSymbolic z) => Equality (SBV a -> z) 

Proving properties

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

Prove a predicate, equivalent to proveWith defaultSMTCfg

proveWith :: Provable a => SMTConfig -> a -> IO ThmResultSource

Proves the predicate using the given SMT-solver

isTheorem :: Provable a => a -> IO BoolSource

Checks theoremhood

isTheoremWithin :: Provable a => Int -> a -> IO (Maybe Bool)Source

Checks theoremhood within the given time limit of i seconds. Returns Nothing if times out, or the result wrapped in a Just otherwise.

Checking satisfiability

sat :: Provable a => a -> IO SatResultSource

Find a satisfying assignment for a predicate, equivalent to satWith defaultSMTCfg

satWith :: Provable a => SMTConfig -> a -> IO SatResultSource

Find a satisfying assignment using the given SMT-solver

isSatisfiable :: Provable a => a -> IO BoolSource

Checks satisfiability

isSatisfiableWithin :: Provable a => Int -> a -> IO (Maybe Bool)Source

Checks satisfiability within the given time limit of i seconds. Returns Nothing if times out, or the result wrapped in a Just otherwise.

Finding all satisfying assignments

allSat :: Provable a => a -> IO AllSatResultSource

Return all satisfying assignments for a predicate, equivalent to allSatWith defaultSMTCfg. Satisfying assignments are constructed lazily, so they will be available as returned by the solver and on demand.

NB. Uninterpreted constant/function values and counter-examples for array values are ignored for the purposes of allSat. That is, only the satisfying assignments modulo uninterpreted functions and array inputs will be returned. This is due to the limitation of not having a robust means of getting a function counter-example back from the SMT solver.

allSatWith :: Provable a => SMTConfig -> a -> IO AllSatResultSource

Find all satisfying assignments using the given SMT-solver

numberOfModels :: Provable a => a -> IO IntSource

Returns the number of models that satisfy the predicate, as it would be returned by allSat. Note that the number of models is always a finite number, and hence this will always return a result. Of course, computing it might take quite long, as it literally generates and counts the number of satisfying models.

Model extraction

The default Show instances for prover calls provide all the counter-example information in a human-readable form and should be sufficient for most casual uses of sbv. However, tools built on top of sbv will inevitably need to look into the constructed models more deeply, programmatically extracting their results and performing actions based on them. The API provided in this section aims at simplifying this task.

Inspecting proof results

ThmResult, SatResult, and AllSatResult are simple newtype wrappers over SMTResult. Their main purpose is so that we can provide custom Show instances to print results accordingly.

newtype ThmResult Source

A prove call results in a ThmResult

Constructors

ThmResult SMTResult 

Instances

newtype SatResult Source

A sat call results in a SatResult The reason for having a separate SatResult is to have a more meaningful Show instance.

Constructors

SatResult SMTResult 

Instances

newtype AllSatResult Source

An allSat call results in a AllSatResult

Constructors

AllSatResult [SMTResult] 

Instances

data SMTResult Source

The result of an SMT solver call. Each constructor is tagged with the SMTConfig that created it so that further tools can inspect it and build layers of results, if needed. For ordinary uses of the library, this type should not be needed, instead use the accessor functions on it. (Custom Show instances and model extractors.)

Constructors

Unsatisfiable SMTConfig

Unsatisfiable

Satisfiable SMTConfig SMTModel

Satisfiable with model

Unknown SMTConfig SMTModel

Prover returned unknown, with a potential (possibly bogus) model

ProofError SMTConfig [String]

Prover errored out

TimeOut SMTConfig

Computation timed out (see the timeout combinator)

Instances

Programmable model extraction

While default Show instances are sufficient for most use cases, it is sometimes desirable (especially for library construction) that the SMT-models are reinterpreted in terms of domain types. Programmable extraction allows getting arbitrarily typed models out of SMT models.

class SatModel a whereSource

Instances of SatModel can be automatically extracted from models returned by the solvers. The idea is that the sbv infrastructure provides a stream of CW's (constant-words) coming from the solver, and the type a is interpreted based on these constants. Many typical instances are already provided, so new instances can be declared with relative ease.

Minimum complete definition: parseCWs

Methods

parseCWs :: [CW] -> Maybe (a, [CW])Source

Given a sequence of constant-words, extract one instance of the type a, returning the remaining elements untouched. If the next element is not what's expected for this type you should return Nothing

cvtModel :: (a -> Maybe b) -> Maybe (a, [CW]) -> Maybe (b, [CW])Source

Given a parsed model instance, transform it using f, and return the result. The default definition for this method should be sufficient in most use cases.

Instances

getModel :: SatModel a => SMTResult -> aSource

Given an SMTResult, extract an arbitrarily typed model from it, given a SatModel instance

displayModels :: SatModel a => (Int -> a -> IO ()) -> AllSatResult -> IO IntSource

Given an allSat call, we typically want to iterate over it and print the results in sequence. The displayModels function automates this task by calling disp on each result, consecutively. The first Int argument to disp 'is the current model number.

SMT Interface: Configurations and solvers

data SMTConfig Source

Solver configuration

Constructors

SMTConfig 

Fields

verbose :: Bool

Debug mode

timing :: Bool

Print timing information on how long different phases took (construction, solving, etc.)

printBase :: Int

Print literals in this base

solver :: SMTSolver

The actual SMT solver

data SMTSolver Source

An SMT solver

Constructors

SMTSolver 

Fields

name :: String

Printable name of the solver

executable :: String

The path to its executable

options :: [String]

Options to provide to the solver

engine :: SMTEngine

The solver engine, responsible for interpreting solver output

defaultSMTCfg :: SMTConfigSource

Default configuration for the SMT solver. Non-verbose, non-timing, prints results in base 10, and uses the Yices SMT solver.

verboseSMTCfg :: SMTConfigSource

Same as defaultSMTCfg, except verbose

timingSMTCfg :: SMTConfigSource

Same as defaultSMTCfg, except prints timing info

verboseTimingSMTCfg :: SMTConfigSource

Same as defaultSMTCfg, except both verbose and timing info

timeout :: Int -> SMTConfig -> SMTConfigSource

Adds a time out of n seconds to a given solver configuration

yices :: SMTSolverSource

The description of the Yices SMT solver The default executable is "yices", which must be in your path. You can use the SBV_YICES environment variable to point to the executable on your system. The default options are "-m -f", which is valid for Yices 2 series. You can use the SBV_YICES_OPTIONS environment variable to override the options.

Symbolic computations

data Symbolic a Source

A Symbolic computation. Represented by a reader monad carrying the state of the computation, layered on top of IO for creating unique references to hold onto intermediate results.

output :: Outputtable a => a -> Symbolic aSource

class (Bounded a, Ord a) => SymWord a whereSource

A SymWord is a potential symbolic bitvector that can be created instances of to be fed to a symbolic program. Note that these methods are typically not needed in casual uses with prove, sat, allSat etc, as default instances automatically provide the necessary bits.

Minimal complete definiton: free, free_, literal, fromCW

Methods

free :: String -> Symbolic (SBV a)Source

Create a user named input

free_ :: Symbolic (SBV a)Source

Create an automatically named input

mkFreeVars :: Int -> Symbolic [SBV a]Source

Get a bunch of new words

literal :: a -> SBV aSource

Turn a literal constant to symbolic

unliteral :: SBV a -> Maybe aSource

Extract a literal, if the value is concrete

fromCW :: CW -> aSource

Extract a literal, from a CW representation

isConcrete :: SBV a -> BoolSource

Is the symbolic word concrete?

isSymbolic :: SBV a -> BoolSource

Is the symbolic word really symbolic?

isConcretely :: SBV a -> (a -> Bool) -> BoolSource

Does it concretely satisfy the given predicate?

Getting SMT-Lib output (for offline analysis)

compileToSMTLib :: Provable a => a -> IO StringSource

Compiles to SMT-Lib and returns the resulting program as a string. Useful for saving the result to a file for off-line analysis, for instance if you have an SMT solver that's not natively supported out-of-the box by the SBV library.

Code generation from symbolic programs

The SBV library can generate straight-line executable code in C. (While other target languages are certainly possible, currently only C is supported.) The generated code will perform no run-time memory-allocations, (no calls to malloc), so its memory usage can be predicted ahead of time. Also, the functions will execute precisely the same instructions in all calls, so they have predictable timing properties as well. The generated code has no loops or jumps, and is typically quite fast. While the generated code can be large due to complete unrolling, these characteristics make them suitable for use in hard real-time systems, as well as in traditional computing.

data SBVCodeGen a Source

The code-generation monad. Allows for precise layout of input values reference parameters (for returning composite values in languages such as C), and return values.

Setting code-generation options

cgPerformRTCs :: Bool -> SBVCodeGen ()Source

Sets RTC (run-time-checks) for index-out-of-bounds, shift-with-large value etc. on/off.

cgSetDriverValues :: [Integer] -> SBVCodeGen ()Source

Sets driver program run time values, useful for generating programs with fixed drivers for testing.

Designating inputs

cgInput :: (HasSignAndSize a, SymWord a) => String -> SBVCodeGen (SBV a)Source

Creates an atomic input in the generated code.

cgInputArr :: (HasSignAndSize a, SymWord a) => Int -> String -> SBVCodeGen [SBV a]Source

Creates an array input in the generated code.

Designating outputs

cgOutput :: (HasSignAndSize a, SymWord a) => String -> SBV a -> SBVCodeGen ()Source

Creates an atomic output in the generated code.

cgOutputArr :: (HasSignAndSize a, SymWord a) => String -> [SBV a] -> SBVCodeGen ()Source

Creates an array output in the generated code.

Designating return values

cgReturn :: (HasSignAndSize a, SymWord a) => SBV a -> SBVCodeGen ()Source

Creates a returned (unnamed) value in the generated code.

cgReturnArr :: (HasSignAndSize a, SymWord a) => [SBV a] -> SBVCodeGen ()Source

Creates a returned (unnamed) array value in the generated code.

Compilation to C

compileToC :: Maybe FilePath -> String -> SBVCodeGen () -> IO ()Source

Given a symbolic computation, render it as an equivalent collection of files that make up a C program:

  • The first argument is the directory name under which the files will be saved. To save files in the current directory pass Just ".". Use Nothing for printing to stdout.
  • The second argument is the name of the C function to generate.
  • The final argument is the function to be compiled.

Compilation will also generate a Makefile, a header file, and a driver (test) program, etc.

compileToCLib :: Maybe FilePath -> String -> [(String, SBVCodeGen ())] -> IO ()Source

Create code to generate a library archive (.a) from given symbolic functions. Useful when generating code from multiple functions that work together as a library.

  • The first argument is the directory name under which the files will be saved. To save files in the current directory pass Just ".". Use Nothing for printing to stdout.
  • The second argument is the name of the archive to generate.
  • The third argument is the list of functions to include, in the form of function-name/code pairs, similar to the second and third arguments of compileToC, except in a list.

Module exports

The SBV library exports the following modules wholesale, as user programs will have to import these three modules to make any sensible use of the SBV functionality.

module Data.Bits

module Data.Word

module Data.Int