sbv-3.4: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright(c) Levent Erkok
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

Data.SBV

Contents

Description

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

SBV: SMT Based Verification

Express properties about 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 = 51 :: 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).
  • SInteger: Unbounded signed integers.
  • SReal: Algebraic-real numbers
  • SFloat: IEEE-754 single-precision floating point values
  • SDouble: IEEE-754 double-precision floating point values
  • SArray, SFunArray: Flat 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.
  • Uninterpreted sorts, and proofs over such sorts, potentially with 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 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, 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 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 following SMT-Solvers out-of-the box:

SBV also allows calling these solvers in parallel, either getting results from multiple solvers or returning the fastest one. (See proveWithAll, proveWithAny, etc.)

Support for other compliant solvers can be added relatively easily, please get in touch if there is a solver you'd like to see included.

Synopsis

Programming with symbolic values

The SBV library is really two things:

  • A framework for writing symbolic programs in Haskell, i.e., programs operating on symbolic values along with the usual concrete counterparts.
  • A framework for proving properties of such programs using SMT solvers.

The programming goal of SBV is to provide a seamless experience, i.e., let people 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 Bool Source

A symbolic boolean/bit

Unsigned symbolic bit-vectors

type SWord8 = SBV Word8 Source

8-bit unsigned symbolic value

type SWord16 = SBV Word16 Source

16-bit unsigned symbolic value

type SWord32 = SBV Word32 Source

32-bit unsigned symbolic value

type SWord64 = SBV Word64 Source

64-bit unsigned symbolic value

Signed symbolic bit-vectors

type SInt8 = SBV Int8 Source

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

type SInt16 = SBV Int16 Source

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

type SInt32 = SBV Int32 Source

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

type SInt64 = SBV Int64 Source

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

Signed unbounded integers

The SBV library supports unbounded signed integers with the type SInteger, which are not subject to overflow/underflow as it is the case with the bounded types, such as SWord8, SInt16, etc. However, some bit-vector based operations are not supported for the SInteger type while in the verification mode. That is, you can use these operations on SInteger values during normal programming/simulation. but the SMT translation will not support these operations since there corresponding operations are not supported in SMT-Lib. Note that this should rarely be a problem in practice, as these operations are mostly meaningful on fixed-size bit-vectors. The operations that are restricted to bounded word/int sizes are:

Usual arithmetic (+, -, *, sQuotRem, sQuot, sRem, sDivMod, sDiv, sMod) and logical operations (.<, .<=, .>, .>=, .==, ./=) operations are supported for SInteger fully, both in programming and verification modes.

type SInteger = SBV Integer Source

Infinite precision signed symbolic value

IEEE-floating point numbers

Floating point numbers are defined by the IEEE-754 standard; and correspond to Haskell's Float and Double types. For SMT support with floating-point numbers, see the paper by Rummer and Wahl: http://www.philipp.ruemmer.org/publications/smt-fpa.pdf.

type SFloat = SBV Float Source

IEEE-754 single-precision floating point numbers

type SDouble = SBV Double Source

IEEE-754 double-precision floating point numbers

data RoundingMode Source

Rounding mode to be used for the IEEE floating-point operations. Note that Haskell's default is RoundNearestTiesToEven. If you use a different rounding mode, then the counter-examples you get may not match what you observe in Haskell.

Constructors

RoundNearestTiesToEven

Round to nearest representable floating point value. If precisely at half-way, pick the even number. (In this context, even means the lowest-order bit is zero.)

RoundNearestTiesToAway

Round to nearest representable floating point value. If precisely at half-way, pick the number further away from 0. (That is, for positive values, pick the greater; for negative values, pick the smaller.)

RoundTowardPositive

Round towards positive infinity. (Also known as rounding-up or ceiling.)

RoundTowardNegative

Round towards negative infinity. (Also known as rounding-down or floor.)

RoundTowardZero

Round towards zero. (Also known as truncation.)

nan :: Floating a => a Source

Not-A-Number for Double and Float. Surprisingly, Haskell Prelude doesn't have this value defined, so we provide it here.

infinity :: Floating a => a Source

Infinity for Double and Float. Surprisingly, Haskell Prelude doesn't have this value defined, so we provide it here.

sNaN :: (Floating a, SymWord a) => SBV a Source

Symbolic variant of Not-A-Number. This value will inhabit both SDouble and SFloat.

sInfinity :: (Floating a, SymWord a) => SBV a Source

Symbolic variant of infinity. This value will inhabit both SDouble and SFloat.

fusedMA :: (SymWord a, Floating a) => SBV a -> SBV a -> SBV a -> SBV a Source

Fused-multiply add. fusedMA a b c = a * b + c, for double and floating point values. Note that a fusedMA call will *never* be concrete, even if all the arguments are constants; since we cannot guarantee the precision requirements, which is the whole reason why fusedMA exists in the first place. (NB. fusedMA only rounds once, even though it does two operations, and hence the extra precision.)

isSNaN :: (Floating a, SymWord a) => SBV a -> SBool Source

Note that the floating point value NaN does not compare equal to itself, so we need a special recognizer for that. Haskell provides the isNaN predicate with the RealFrac class, which unfortunately is not currently implementable for symbolic cases. (Requires trigonometric functions etc.) Thus, we provide this recognizer separately. Note that the definition simply tests equality against itself, which fails for NaN. Who said equality for floating point was reflexive?

isFPPoint :: (Floating a, SymWord a) => SBV a -> SBool Source

We call a FP number FPPoint if it is neither NaN, nor +/- infinity.

Signed algebraic reals

Algebraic reals are roots of single-variable polynomials with rational coefficients. (See http://en.wikipedia.org/wiki/Algebraic_number.) Note that algebraic reals are infinite precision numbers, but they do not cover all real numbers. (In particular, they cannot represent transcendentals.) Some irrational numbers are algebraic (such as sqrt 2), while others are not (such as pi and e).

SBV can deal with real numbers just fine, since the theory of reals is decidable. (See http://goedel.cs.uiowa.edu/smtlib/theories/Reals.smt2.) In addition, by leveraging backend solver capabilities, SBV can also represent and solve non-linear equations involving real-variables. (For instance, the Z3 SMT solver, supports polynomial constraints on reals starting with v4.0.)

type SReal = SBV AlgReal Source

Infinite precision symbolic algebraic real value

data AlgReal Source

Algebraic reals. Note that the representation is left abstract. We represent rational results explicitly, while the roots-of-polynomials are represented implicitly by their defining equation

toSReal :: SInteger -> SReal Source

Promote an SInteger to an SReal

Creating a symbolic variable

These functions simplify declaring symbolic variables of various types. Strictly speaking, they are just synonyms for free (specialized at the given type), but they might be easier to use.

Creating a list of symbolic variables

These functions simplify declaring a sequence symbolic variables of various types. Strictly speaking, they are just synonyms for mapM free (specialized at the given type), but they might be easier to use.

sBools :: [String] -> Symbolic [SBool] Source

Declare a list of SBools

sWord8s :: [String] -> Symbolic [SWord8] Source

Declare a list of SWord8s

sWord16s :: [String] -> Symbolic [SWord16] Source

Declare a list of SWord16s

sWord32s :: [String] -> Symbolic [SWord32] Source

Declare a list of SWord32s

sWord64s :: [String] -> Symbolic [SWord64] Source

Declare a list of SWord64s

sInt8s :: [String] -> Symbolic [SInt8] Source

Declare a list of SInt8s

sInt16s :: [String] -> Symbolic [SInt16] Source

Declare a list of SInt16s

sInt32s :: [String] -> Symbolic [SInt32] Source

Declare a list of SInt32s

sInt64s :: [String] -> Symbolic [SInt64] Source

Declare a list of SInt64s

sIntegers :: [String] -> Symbolic [SInteger] Source

Declare a list of SIntegers

sReals :: [String] -> Symbolic [SReal] Source

Declare a list of SReals

sFloats :: [String] -> Symbolic [SFloat] Source

Declare a list of SFloats

sDoubles :: [String] -> Symbolic [SDouble] Source

Declare a list of SDoubles

Abstract SBV type

data SBV a Source

The Symbolic value. Either a constant (Left) or a symbolic value (Right Cached). Note that caching is essential for making sure sharing is preserved. The parameter a is phantom, but is extremely important in keeping the user interface strongly typed.

Instances

Testable SBool 
Boolean SBool 
Provable SBool 
Provable Predicate 
SDivisible SInteger 
SDivisible SInt64 
SDivisible SInt32 
SDivisible SInt16 
SDivisible SInt8 
SDivisible SWord64 
SDivisible SWord32 
SDivisible SWord16 
SDivisible SWord8 
FromBits SInt64 
FromBits SInt32 
FromBits SInt16 
FromBits SInt8 
FromBits SWord64 
FromBits SWord32 
FromBits SWord16 
FromBits SWord8 
FromBits SBool 
Polynomial SWord64 
Polynomial SWord32 
Polynomial SWord16 
Polynomial SWord8 
SignCast SWord64 SInt64 
SignCast SWord32 SInt32 
SignCast SWord16 SInt16 
SignCast SWord8 SInt8 
Splittable SWord64 SWord32 
Splittable SWord32 SWord16 
Splittable SWord16 SWord8 
(SymWord a, Bounded a) => Bounded (SBV a) 
(Show a, Bounded a, Integral a, Num a, SymWord a) => Enum (SBV a) 
Eq (SBV a) 
(SymWord a, Fractional a, Floating a) => Floating (SBV a)

Define Floating instance on SBV's; only for base types that are already floating; i.e., SFloat and SDouble Note that most of the fields are "undefined" for symbolic values, we add methods as they are supported by SMTLib. Currently, the only symbolicly available function in this class is sqrt.

(SymWord a, Fractional a) => Fractional (SBV a) 
(Ord a, Num a, SymWord a) => Num (SBV a) 
Show (SBV a) 
Testable (Symbolic SBool) 
(SymWord a, Arbitrary a) => Arbitrary (SBV a) 
(Num a, Bits a, SymWord a) => Bits (SBV a) 
NFData a => NFData (SBV a) 
(Random a, SymWord a) => Random (SBV a) 
(NFData a, SymWord a) => SExecutable [SBV a] 
NFData a => SExecutable (SBV a) 
HasKind a => HasKind (SBV a) 
(SymWord a, PrettyNum a) => PrettyNum (SBV a) 
HasKind a => Uninterpreted (SBV a) 
SymWord a => Mergeable (SBV a) 
SymWord a => OrdSymbolic (SBV a) 
EqSymbolic (SBV a) 
(SymWord a, SymWord b, SExecutable p) => SExecutable ((SBV a, SBV b) -> p) 
(SymWord a, SymWord b, SymWord c, SExecutable p) => SExecutable ((SBV a, SBV b, SBV c) -> p) 
(SymWord a, SymWord b, SymWord c, SymWord d, SExecutable p) => SExecutable ((SBV a, SBV b, SBV c, SBV d) -> p) 
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SExecutable p) => SExecutable ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) 
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SExecutable p) => SExecutable ((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, SExecutable p) => SExecutable ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) 
(SymWord a, SExecutable p) => SExecutable (SBV a -> p) 
(NFData a, SymWord a, NFData b, SymWord b) => SExecutable (SBV a, SBV b) 
(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) 
(SymWord a, Provable p) => Provable (SBV a -> p) 
(SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV c, SBV b) -> SBV a) 
(SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV d, SBV c, SBV b) -> SBV a) 
(SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV e, SBV d, SBV c, SBV b) -> SBV a) 
(SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) 
(SymWord g, SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) 
(SymWord h, SymWord g, SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) 
(SymWord h, SymWord g, SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV h -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) 
(SymWord g, SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) 
(SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) 
(SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV e -> SBV d -> SBV c -> SBV b -> SBV a) 
(SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV d -> SBV c -> SBV b -> SBV a) 
(SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV c -> SBV b -> SBV a) 
(SymWord b, HasKind a) => Uninterpreted (SBV b -> SBV a) 
(SymWord e, Mergeable (SBV e)) => Mergeable (STree i e) 
(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) 
(NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c) => SExecutable (SBV a, SBV b, SBV c) 
(NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c, NFData d, SymWord d) => SExecutable (SBV a, SBV b, SBV c, SBV d) 
(NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c, NFData d, SymWord d, NFData e, SymWord e) => SExecutable (SBV a, SBV b, SBV c, SBV d, SBV e) 
(NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c, NFData d, SymWord d, NFData e, SymWord e, NFData f, SymWord f) => SExecutable (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) 
(NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c, NFData d, SymWord d, NFData e, SymWord e, NFData f, SymWord f, NFData g, SymWord g) => SExecutable (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) 

Arrays of symbolic values

class SymArray array where Source

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_ :: (HasKind a, HasKind b) => Maybe (SBV b) -> Symbolic (array a b) Source

Create a new array, with an optional initial value

newArray :: (HasKind a, HasKind 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 b Source

Read the array element at a

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

Reset all the elements of the array to the value b

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

Update the element at a to be b

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

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

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

mkSFunArray :: (SBV a -> SBV b) -> SFunArray a b Source

Lift a function to an array. Useful for creating arrays in a pure context. (Otherwise use newArray.)

Full binary trees

type STree i e = STreeInternal (SBV i) (SBV e) Source

A symbolic tree containing values of type e, indexed by elements of type i. Note that these are full-trees, and their their shapes remain constant. There is no API provided that can change the shape of the tree. These structures are useful when dealing with data-structures that are indexed with symbolic values where access time is important. STree structures provide logarithmic time reads and writes.

readSTree :: (Num i, Bits i, SymWord i, SymWord e) => STree i e -> SBV i -> SBV e Source

Reading a value. We bit-blast the index and descend down the full tree according to bit-values.

writeSTree :: (Mergeable (SBV e), Num i, Bits i, SymWord i, SymWord e) => STree i e -> SBV i -> SBV e -> STree i e Source

Writing a value, similar to how reads are done. The important thing is that the tree representation keeps updates to a minimum.

mkSTree :: forall i e. HasKind i => [SBV e] -> STree i e Source

Construct the fully balanced initial tree using the given values.

Operations on symbolic values

Word level

sbvTestBit :: (Num a, Bits a, SymWord a) => SBV a -> Int -> SBool Source

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.

sbvPopCount :: (Num a, Bits a, SymWord a) => SBV a -> SWord8 Source

Replacement for popCount. Since popCount returns an Int, we cannot implement it for symbolic words. Here, we return an SWord8, which can overflow when used on quantities that have more than 255 bits. Currently, that's only the SInteger type that SBV supports, all other types are safe. Even with SInteger, this will only overflow if there are at least 256-bits set in the number, and the smallest such number is 2^256-1, which is a pretty darn big number to worry about for practical purposes. In any case, we do not support sbvPopCount for unbounded symbolic integers, as the only possible implementation wouldn't symbolically terminate. So the only overflow issue is with really-really large concrete SInteger values.

sbvShiftLeft :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a Source

Generalization of shiftL, when the shift-amount is symbolic. Since Haskell's shiftL only takes an Int as the shift amount, it cannot be used when we have a symbolic amount to shift with. The shift amount must be an unsigned quantity.

sbvShiftRight :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a Source

Generalization of shiftR, when the shift-amount is symbolic. Since Haskell's shiftR only takes an Int as the shift amount, it cannot be used when we have a symbolic amount to shift with. The shift amount must be an unsigned quantity.

NB. If the shiftee is signed, then this is an arithmetic shift; otherwise it's logical, following the usual Haskell convention. See sbvSignedShiftArithRight for a variant that explicitly uses the msb as the sign bit, even for unsigned underlying types.

sbvSignedShiftArithRight :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a Source

Arithmetic shift-right with a symbolic unsigned shift amount. This is equivalent to sbvShiftRight when the argument is signed. However, if the argument is unsigned, then it explicitly treats its msb as a sign-bit, and uses it as the bit that gets shifted in. Useful when using the underlying unsigned bit representation to implement custom signed operations. Note that there is no direct Haskell analogue of this function.

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

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 a Source

Returns 1 if the boolean is true, otherwise 0.

lsb :: (Num a, Bits a, SymWord a) => SBV a -> SBool Source

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

msb :: (Num a, Bits a, SymWord a) => SBV a -> SBool Source

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

Predicates

allEqual :: EqSymbolic a => [a] -> SBool Source

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

allDifferent :: EqSymbolic a => [a] -> SBool Source

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

inRange :: OrdSymbolic a => a -> (a, a) -> SBool Source

Returns (symbolic) true if the argument is in range

sElem :: EqSymbolic a => a -> [a] -> SBool Source

Symbolic membership test

Addition and Multiplication with high-bits

fullAdder :: SIntegral a => SBV a -> SBV a -> (SBool, SBV a) Source

Full adder. Returns the carry-out from the addition.

N.B. Only works for unsigned types. Signed arguments will be rejected.

fullMultiplier :: SIntegral a => SBV a -> SBV a -> (SBV a, SBV a) Source

Full multiplier: Returns both the high-order and the low-order bits in a tuple, thus fully accounting for the overflow.

N.B. Only works for unsigned types. Signed arguments will be rejected.

N.B. The higher-order bits are determined using a simple shift-add multiplier, thus involving bit-blasting. It'd be naive to expect SMT solvers to deal efficiently with properties involving this function, at least with the current state of the art.

Blasting/Unblasting

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

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

blastLE :: (Num a, 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 where Source

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 definition: fromBitsLE

Minimal complete definition

fromBitsLE

Methods

fromBitsLE, fromBitsBE :: [SBool] -> a Source

Splitting, joining, and extending

class Splittable a b | b -> a where Source

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 -> a infixr 5 Source

extend :: b -> a Source

Sign-casting

class SignCast a b | a -> b, b -> a where Source

Sign casting a value into another. This essentially means forgetting the sign bit and reinterpreting the bits accordingly when converting a signed value to an unsigned one. Similarly, when an unsigned quantity is converted to a signed one, the most significant bit is interpreted as the sign. We only define instances when the source and target types are precisely the same size. The idea is that signCast and unsignCast must form an isomorphism pair between the types a and b, i.e., we expect the following two properties to hold:

   signCast . unsignCast = id
   unsingCast . signCast = id

Note that one naive way to implement both these operations is simply to compute fromBitsLE . blastLE, i.e., first get all the bits of the word and then reconstruct in the target type. While this is semantically correct, it generates a lot of code (both during proofs via SMT-Lib, and when compiled to C). The goal of this class is to avoid that cost, so these operations can be compiled very efficiently, they will essentially become no-op's.

Minimal complete definition: All, no defaults.

Methods

signCast :: a -> b Source

Interpret as a signed word

unsignCast :: b -> a Source

Interpret as an unsigned word

Polynomial arithmetic and CRCs

class (Num a, Bits a) => Polynomial a where Source

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

x pDivMod 0 = (0, x)

for all x (including 0)

Minimal complete definition: pMult, pDivMod, showPolynomial

Minimal complete definition

pMult, pDivMod, showPolynomial

Methods

polynomial :: [Int] -> a Source

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 -> a Source

Add two polynomials in GF(2^n).

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

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 -> a Source

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

pMod :: a -> a -> a Source

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 -> String Source

Display a polynomial like a mathematician would (over the monomial x), with a type.

showPolynomial :: Bool -> a -> String Source

Display a polynomial like a mathematician would (over the monomial x), the first argument controls if the final type is shown as well.

crcBV :: Int -> [SBool] -> [SBool] -> [SBool] Source

Compute CRCs over bit-vectors. The call crcBV n m p computes the CRC of the message m with respect to polynomial p. The inputs are assumed to be blasted big-endian. The number n specifies how many bits of CRC is needed. Note that n is actually the degree of the polynomial p, and thus it seems redundant to pass it in. However, in a typical proof context, the polynomial can be symbolic, so we cannot compute the degree easily. While this can be worked-around by generating code that accounts for all possible degrees, the resulting code would be unnecessarily big and complicated, and much harder to reason with. (Also note that a CRC is just the remainder from the polynomial division, but this routine is much faster in practice.)

NB. The nth bit of the polynomial p must be set for the CRC to be computed correctly. Note that the polynomial argument p will not even have this bit present most of the time, as it will typically contain bits 0 through n-1 as usual in the CRC literature. The higher order nth bit is simply assumed to be set, as it does not make sense to use a polynomial of a lesser degree. This is usually not a problem since CRC polynomials are designed and expressed this way.

NB. The literature on CRC's has many variants on how CRC's are computed. We follow the painless guide (http://www.ross.net/crc/download/crc_v3.txt) and compute the CRC as follows:

  • Extend the message m by adding n 0 bits on the right
    • Divide the polynomial thus obtained by the p
    • The remainder is the CRC value.

There are many variants on final XOR's, reversed polynomials etc., so it is essential to double check you use the correct algorithm.

crc :: (FromBits (SBV a), FromBits (SBV b), Num a, Num b, Bits a, Bits b, SymWord a, SymWord b) => Int -> SBV a -> SBV b -> SBV b Source

Compute CRC's over polynomials, i.e., symbolic words. The first Int argument plays the same role as the one in the crcBV function.

Conditionals: Mergeable values

class Mergeable a where Source

Symbolic conditionals are modeled by the Mergeable class, describing how to merge the results of an if-then-else call with a symbolic test. SBV provides all basic types as instances of this class, so users only need to declare instances for custom data-types of their programs as needed.

The function select is a total-indexing function out of a list of choices with a default value, simulating array/list indexing. It's an n-way generalization of the ite function.

Minimal complete definition: symbolicMerge

Minimal complete definition

symbolicMerge

Methods

symbolicMerge :: Bool -> SBool -> a -> a -> a Source

Merge two values based on the condition. The first argument states whether we force the then-and-else branches before the merging, at the word level. This is an efficiency concern; one that we'd rather not make but unfortunately necessary for getting symbolic simulation working efficiently.

select :: (SymWord b, Num b) => [a] -> a -> SBV b -> a Source

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 instance of Mostek simply pushes the merging into record fields.

Mergeable Status

Mergeable instance for Status simply walks down the structure fields and merges them.

Mergeable a => Mergeable [a] 
Mergeable a => Mergeable (Maybe a) 
SymWord a => Mergeable (SBV a) 
Mergeable a => Mergeable (Move a)

Mergeable instance for Move simply pushes the merging the data after run of each branch starting from the same state.

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) 
(SymWord e, Mergeable (SBV e)) => Mergeable (STree i e) 
(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) 

ite :: Mergeable a => SBool -> a -> a -> a Source

If-then-else. This is by definition symbolicMerge with both branches forced. This is typically the desired behavior, but also see iteLazy should you need more laziness.

iteLazy :: Mergeable a => SBool -> a -> a -> a Source

A Lazy version of ite, which does not force its arguments. This might cause issues for symbolic simulation with large thunks around, so use with care.

sBranch :: Mergeable a => SBool -> a -> a -> a Source

Branch on a condition, much like ite. The exception is that SBV will check to make sure if the test condition is feasible by making an external call to the SMT solver. Note that this can be expensive, thus we shall use a time-out value (sBranchTimeOut). There might be zero, one, or two such external calls per sBranch call:

  • If condition is statically known to be True/False: 0 calls
  • In this case, we simply constant fold..
    • If condition is determined to be unsatisfiable : 1 call
    • In this case, we know then-branch is infeasible, so just take the else-branch
    • If condition is determined to be satisfable : 2 calls
    • In this case, we know then-branch is feasible, but we still have to check if the else-branch is

In summary, sBranch calls can be expensive, but they can help with the so-called symbolic-termination problem. See Data.SBV.Examples.Misc.SBranch for an example.

Conditional symbolic simulation

sAssert :: Mergeable a => String -> SBool -> a -> a Source

Symbolic assert. Check that the given boolean condition is always true in the given path. Otherwise symbolic simulation will stop with a run-time error.

sAssertCont :: Mergeable a => String -> (forall b. SMTConfig -> Maybe (Map String CW) -> b) -> SBool -> a -> a Source

Symbolic assert with a programmable continuation. Check that the given boolean condition is always true in the given path. Otherwise symbolic simulation will transfer the failing model to the given continuation. The continuation takes the SMTConfig, and a possible model: If it receives Nothing, then it means that the condition fails for all assignments to inputs. Otherwise, it'll receive Just a dictionary that maps the input variables to the appropriate CW values that exhibit the failure. Note that the continuation has no option but to display the result in some fashion and call error, due to its restricted type.

Symbolic equality

class EqSymbolic a where Source

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: .==

Minimal complete definition

(.==)

Methods

(.==), (./=) :: a -> a -> SBool infix 4 .==, ./= Source

Instances

Symbolic ordering

class (Mergeable a, EqSymbolic a) => OrdSymbolic a where Source

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: .<

Minimal complete definition

(.<)

Methods

(.<), (.>=), (.>), (.<=) :: a -> a -> SBool infix 4 .<, .>=, .>, .<= Source

smin, smax :: a -> a -> a Source

Symbolic integral numbers

class (SymWord a, Num a, Bits a) => SIntegral a Source

Symbolic Numbers. This is a simple class that simply incorporates all number like base types together, simplifying writing polymorphic type-signatures that work for all symbolic numbers, such as SWord8, SInt8 etc. For instance, we can write a generic list-minimum function as follows:

   mm :: SIntegral a => [SBV a] -> SBV a
   mm = foldr1 (a b -> ite (a .<= b) a b)

It is similar to the standard Integral class, except ranging over symbolic instances.

Division

class SDivisible a where Source

The SDivisible class captures the essence of division. Unfortunately we cannot use Haskell's Integral class since the Real and Enum superclasses are not implementable for symbolic bit-vectors. However, quotRem and divMod makes perfect sense, and the SDivisible 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 sQuotRem 0 = (0, x) x sDivMod 0 = (0, x)

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

NB. quot truncates toward zero, while div truncates toward negative infinity.

Minimal complete definition: sQuotRem, sDivMod

Minimal complete definition

sQuotRem, sDivMod

Methods

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

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

sQuot :: a -> a -> a Source

sRem :: a -> a -> a Source

sDiv :: a -> a -> a Source

sMod :: a -> a -> a Source

The Boolean class

class Boolean b where Source

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.

Minimal complete definition

true, bnot, (&&&)

Methods

true :: b Source

logical true

false :: b Source

logical false

bnot :: b -> b Source

complement

(&&&) :: b -> b -> b infixr 3 Source

and

(|||) :: b -> b -> b infixr 2 Source

or

(~&) :: b -> b -> b infixr 3 Source

nand

(~|) :: b -> b -> b infixr 2 Source

nor

(<+>) :: b -> b -> b infixl 6 Source

xor

(==>) :: b -> b -> b infixr 1 Source

implies

(<=>) :: b -> b -> b infixr 1 Source

equivalence

fromBool :: Bool -> b Source

cast from Bool

Generalizations of boolean operations

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

Generalization of and

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

Generalization of or

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

Generalization of any

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

Generalization of all

Pretty-printing and reading numbers in Hex & Binary

class PrettyNum a where Source

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

Minimal complete definition: hexS and binS

Methods

hexS :: a -> String Source

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

binS :: a -> String Source

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

hex :: a -> String Source

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

bin :: a -> String Source

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

readBin :: Num a => String -> a Source

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

Uninterpreted sorts, constants, and functions

Users can introduce new uninterpreted sorts simply by defining a data-type in Haskell and registering it as such. The following example demonstrates:

    data B = B deriving (Eq, Ord, Data, Typeable)
    instance SymWord  B
    instance HasKind  B
 

(Note that you'll also need to use the language pragma DeriveDataTypeable, and import Data.Generics for the above to work.)

Once GHC implements derivable user classes (http://hackage.haskell.org/trac/ghc/ticket/5462), we will be able to simplify this to:

    data B = B deriving (Eq, Ord, Data, Typeable, SymWord, HasKind)
 

This is all it takes to introduce B as an uninterpreted sort in SBV, which makes the type SBV B automagically become available as the type of symbolic values that ranges over B values.

Uninterpreted functions over both uninterpreted and regular sorts can be declared using the facilities introduced by the Uninterpreted class.

class Uninterpreted a where Source

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: sbvUninterpret. However, most instances in practice are already provided by SBV, so end-users should not need to define their own instances.

Minimal complete definition

sbvUninterpret

Methods

uninterpret :: String -> a Source

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.

cgUninterpret :: String -> [String] -> a -> a Source

Uninterpret a value, only for the purposes of code-generation. For execution and verification the value is used as is. For code-generation, the alternate definition is used. This is useful when we want to take advantage of native libraries on the target languages.

sbvUninterpret :: Maybe ([String], a) -> String -> a Source

Most generalized form of uninterpretation, this function should not be needed by end-user-code, but is rather useful for the library development.

Instances

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

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

Add a user specified axiom to the generated SMT-Lib file. The first argument is a mere string, use for commenting purposes. The second argument is intended to hold the multiple-lines of the axiom text as expressed in SMT-Lib notation. Note that we perform no checks on the axiom itself, to see whether it's actually well-formed or is sensical by any means. A separate formalization of SMT-Lib would be very useful here.

Properties, proofs, and satisfiability

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.

Predicates

type Predicate = Symbolic SBool Source

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 where Source

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 -> Predicate Source

Turns a value into a universally quantified 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 -> Predicate Source

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

forSome_ :: a -> Predicate Source

Turns a value into an existentially quantified predicate. (Indeed, exists would have been a better choice here for the name, but alas it's already taken.)

forSome :: [String] -> a -> Predicate Source

Version of forSome that allows user defined names

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) 
(HasKind a, HasKind b, SymArray array, Provable p) => Provable (array a b -> p) 
(SymWord a, Provable p) => Provable (SBV a -> p) 

class Equality a where Source

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 ThmResult infix 4 Source

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 ThmResult Source

Prove a predicate, equivalent to proveWith defaultSMTCfg

proveWith :: Provable a => SMTConfig -> a -> IO ThmResult Source

Proves the predicate using the given SMT-solver

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

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

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

Check whether a given property is a theorem, with an optional time out and the given solver. Returns Nothing if times out, or the result wrapped in a Just otherwise.

Checking satisfiability

sat :: Provable a => a -> IO SatResult Source

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

satWith :: Provable a => SMTConfig -> a -> IO SatResult Source

Find a satisfying assignment using the given SMT-solver

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

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

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

Check whether a given property is satisfiable, with an optional time out and the given solver. Returns Nothing if times out, or the result wrapped in a Just otherwise.

Finding all satisfying assignments

allSat :: Provable a => a -> IO AllSatResult Source

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 AllSatResult Source

Find all satisfying assignments using the given SMT-solver

Satisfying a sequence of boolean conditions

solve :: [SBool] -> Symbolic SBool Source

Form the symbolic conjunction of a given list of boolean conditions. Useful in expressing problems with constraints, like the following:

  do [x, y, z] <- sIntegers ["x", "y", "z"]
     solve [x .> 5, y + z .< x]

Adding constraints

A constraint is a means for restricting the input domain of a formula. Here's a simple example:

   do x <- exists "x"
      y <- exists "y"
      constrain $ x .> y
      constrain $ x + y .>= 12
      constrain $ y .>= 3
      ...

The first constraint requires x to be larger than y. The scond one says that sum of x and y must be at least 12, and the final one says that y to be at least 3. Constraints provide an easy way to assert additional properties on the input domain, right at the point of the introduction of variables.

Note that the proper reading of a constraint depends on the context:

  • In a sat (or allSat) call: The constraint added is asserted conjunctively. That is, the resulting satisfying model (if any) will always satisfy all the constraints given.
  • In a prove call: In this case, the constraint acts as an implication. The property is proved under the assumption that the constraint holds. In other words, the constraint says that we only care about the input space that satisfies the constraint.
  • In a quickCheck call: The constraint acts as a filter for quickCheck; if the constraint does not hold, then the input value is considered to be irrelevant and is skipped. Note that this is similar to prove, but is stronger: We do not accept a test case to be valid just because the constraints fail on them, although semantically the implication does hold. We simply skip that test case as a bad test vector.
  • In a genTest call: Similar to quickCheck and prove: If a constraint does not hold, the input value is ignored and is not included in the test set.

A good use case (in fact the motivating use case) for constrain is attaching a constraint to a forall or exists variable at the time of its creation. Also, the conjunctive semantics for sat and the implicative semantics for prove simplify programming by choosing the correct interpretation automatically. However, one should be aware of the semantic difference. For instance, in the presence of constraints, formulas that are provable are not necessarily satisfiable. To wit, consider:

   do x <- exists "x"
      constrain $ x .< x
      return $ x .< (x :: SWord8)

This predicate is unsatisfiable since no element of SWord8 is less than itself. But it's (vacuously) true, since it excludes the entire domain of values, thus making the proof trivial. Hence, this predicate is provable, but is not satisfiable. To make sure the given constraints are not vacuous, the functions isVacuous (and isVacuousWith) can be used.

Also note that this semantics imply that test case generation (genTest) and quick-check can take arbitrarily long in the presence of constraints, if the random input values generated rarely satisfy the constraints. (As an extreme case, consider constrain false.)

A probabilistic constraint (see pConstrain) attaches a probability threshold for the constraint to be considered. For instance:

    pConstrain 0.8 c
 

will make sure that the condition c is satisfied 80% of the time (and correspondingly, falsified 20% of the time), in expectation. This variant is useful for genTest and quickCheck functions, where we want to filter the test cases according to some probability distribution, to make sure that the test-vectors are drawn from interesting subsets of the input space. For instance, if we were to generate 100 test cases with the above constraint, we'd expect about 80 of them to satisfy the condition c, while about 20 of them will fail it.

The following properties hold:

   constrain      = pConstrain 1
   pConstrain t c = pConstrain (1-t) (not c)
 

Note that while constrain can be used freely, pConstrain is only allowed in the contexts of genTest or quickCheck. Calls to pConstrain in a prove/sat call will be rejected as SBV does not deal with probabilistic constraints when it comes to satisfiability and proofs. Also, both constrain and pConstrain calls during code-generation will also be rejected, for similar reasons.

constrain :: SBool -> Symbolic () Source

Adding arbitrary constraints. When adding constraints, one has to be careful about making sure they are not inconsistent. The function isVacuous can be use for this purpose. Here is an example. Consider the following predicate:

>>> let pred = do { x <- forall "x"; constrain $ x .< x; return $ x .>= (5 :: SWord8) }

This predicate asserts that all 8-bit values are larger than 5, subject to the constraint that the values considered satisfy x .< x, i.e., they are less than themselves. Since there are no values that satisfy this constraint, the proof will pass vacuously:

>>> prove pred
Q.E.D.

We can use isVacuous to make sure to see that the pass was vacuous:

>>> isVacuous pred
True

While the above example is trivial, things can get complicated if there are multiple constraints with non-straightforward relations; so if constraints are used one should make sure to check the predicate is not vacuously true. Here's an example that is not vacuous:

>>> let pred' = do { x <- forall "x"; constrain $ x .> 6; return $ x .>= (5 :: SWord8) }

This time the proof passes as expected:

>>> prove pred'
Q.E.D.

And the proof is not vacuous:

>>> isVacuous pred'
False

pConstrain :: Double -> SBool -> Symbolic () Source

Adding a probabilistic constraint. The Double argument is the probability threshold. Probabilistic constraints are useful for genTest and quickCheck calls where we restrict our attention to interesting parts of the input domain.

Checking constraint vacuity

isVacuous :: Provable a => a -> IO Bool Source

Check if the given constraints are satisfiable, equivalent to isVacuousWith defaultSMTCfg. See the function constrain for an example use of isVacuous.

isVacuousWith :: Provable a => SMTConfig -> a -> IO Bool Source

Determine if the constraints are vacuous using the given SMT-solver

Checking safety

The sAssert and sAssertCont functions allow users to introduce invariants through-out their code to make sure certain properties hold at all times. This is another mechanism to provide further documentation/contract info into SBV code. The functions safe and safeWith can then be used to statically discharge these proof assumptions. If a violation is found, SBV will print a model showing which inputs lead to the invariant being violated.

Here's a simple example. Let's assume we have a function that does subtraction, and requires it's first argument to be larger than the second:

>>> let sub x y = sAssert "sub: x >= y must hold!" (x .>= y) (x - y)

Clearly, this function is not safe, as there's nothing that ensures us to pass a larger second argument. If we try to prove a theorem regarding sub, we'll get an exception:

>>> prove $ \x y -> sub x y .>= (0 :: SInt16)
*** Exception: Assertion failure: "sub: x >= y must hold!"
  s0 = -32768 :: SInt16
  s1 = -32767 :: SInt16

Of course, we can use, safe to statically see if such a violation is possible before we attempt a proof:

>>> safe (sub :: SInt8 -> SInt8 -> SInt8)
Assertion failure: "sub: x >= y must hold!"
  s0 = -128 :: SInt8
  s1 = -127 :: SInt8

What happens if we make sure to arrange for this invariant? Consider this version:

>>> let safeSub x y = ite (x .>= y) (sub x y) (sub y x)

Clearly, safeSub must be safe. And indeed, SBV can prove that:

>>> safe (safeSub :: SInt8 -> SInt8 -> SInt8)
No safety violations detected.

Note how we used sub and safeSub polymorphically. We only need to monomorphise our types when a proof attempt is done, as we did in the safe calls.

safe :: SExecutable a => a -> IO SafeResult Source

Check if a given definition is safe; i.e., if all sAssert conditions can be proven to hold.

safeWith :: SExecutable a => SMTConfig -> a -> IO SafeResult Source

Check if a given definition is safe using the given solver configuration; i.e., if all sAssert conditions can be proven to hold.

class SExecutable a where Source

Symbolically executable program fragments. This class is mainly used for safe calls, and is sufficently populated internally to cover most use cases. Users can extend it as they wish to allow safe checks for SBV programs that return/take types that are user-defined.

Methods

sName_ :: a -> Symbolic () Source

sName :: [String] -> a -> Symbolic () Source

Instances

SExecutable () 
(NFData a, SymWord a) => SExecutable [SBV a] 
NFData a => SExecutable (Symbolic a) 
NFData a => SExecutable (SBV a) 
(SymWord a, SymWord b, SExecutable p) => SExecutable ((SBV a, SBV b) -> p) 
(SymWord a, SymWord b, SymWord c, SExecutable p) => SExecutable ((SBV a, SBV b, SBV c) -> p) 
(SymWord a, SymWord b, SymWord c, SymWord d, SExecutable p) => SExecutable ((SBV a, SBV b, SBV c, SBV d) -> p) 
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SExecutable p) => SExecutable ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) 
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SExecutable p) => SExecutable ((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, SExecutable p) => SExecutable ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) 
(SymWord a, SExecutable p) => SExecutable (SBV a -> p) 
(NFData a, SymWord a, NFData b, SymWord b) => SExecutable (SBV a, SBV b) 
(NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c) => SExecutable (SBV a, SBV b, SBV c) 
(NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c, NFData d, SymWord d) => SExecutable (SBV a, SBV b, SBV c, SBV d) 
(NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c, NFData d, SymWord d, NFData e, SymWord e) => SExecutable (SBV a, SBV b, SBV c, SBV d, SBV e) 
(NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c, NFData d, SymWord d, NFData e, SymWord e, NFData f, SymWord f) => SExecutable (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) 
(NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c, NFData d, SymWord d, NFData e, SymWord e, NFData f, SymWord f, NFData g, SymWord g) => SExecutable (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) 

Proving properties using multiple solvers

On a multi-core machine, it might be desirable to try a given property using multiple SMT solvers, using parallel threads. Even with machines with single-cores, threading can be helpful if you want to try out multiple-solvers but do not know which one would work the best for the problem at hand ahead of time.

The functions in this section allow proving/satisfiability-checking with multiple backends at the same time. Each function comes in two variants, one that returns the results from all solvers, the other that returns the fastest one.

The All variants, (i.e., proveWithAll, satWithAll, allSatWithAll) run all solvers and return all the results. SBV internally makes sure that the result is lazily generated; so, the order of solvers given does not matter. In other words, the order of results will follow the order of the solvers as they finish, not as given by the user. These variants are useful when you want to make sure multiple-solvers agree (or disagree!) on a given problem.

The Any variants, (i.e., proveWithAny, satWithAny, allSatWithAny) will run all the solvers in parallel, and return the results of the first one finishing. The other threads will then be killed. These variants are useful when you do not care if the solvers produce the same result, but rather want to get the solution as quickly as possible, taking advantage of modern many-core machines.

Note that the function sbvAvailableSolvers will return all the installed solvers, which can be used as the first argument to all these functions, if you simply want to try all available solvers on a machine.

proveWithAll :: Provable a => [SMTConfig] -> a -> IO [(Solver, ThmResult)] Source

Prove a property with multiple solvers, running them in separate threads. The results will be returned in the order produced.

proveWithAny :: Provable a => [SMTConfig] -> a -> IO (Solver, ThmResult) Source

Prove a property with multiple solvers, running them in separate threads. Only the result of the first one to finish will be returned, remaining threads will be killed.

satWithAll :: Provable a => [SMTConfig] -> a -> IO [(Solver, SatResult)] Source

Find a satisfying assignment to a property with multiple solvers, running them in separate threads. The results will be returned in the order produced.

satWithAny :: Provable a => [SMTConfig] -> a -> IO (Solver, SatResult) Source

Find a satisfying assignment to a property with multiple solvers, running them in separate threads. Only the result of the first one to finish will be returned, remaining threads will be killed.

allSatWithAll :: Provable a => [SMTConfig] -> a -> IO [(Solver, AllSatResult)] Source

Find all satisfying assignments to a property with multiple solvers, running them in separate threads. Only the result of the first one to finish will be returned, remaining threads will be killed.

allSatWithAny :: Provable a => [SMTConfig] -> a -> IO (Solver, AllSatResult) Source

Find all satisfying assignments to a property with multiple solvers, running them in separate threads. Only the result of the first one to finish will be returned, remaining threads will be killed.

Optimization

Symbolic optimization. A call of the form:

minimize Quantified cost n valid

returns Just xs, such that:

  • xs has precisely n elements
  • valid xs holds
  • cost xs is minimal. That is, for all sequences ys that satisfy the first two criteria above, cost xs .<= cost ys holds.

If there is no such sequence, then minimize will return Nothing.

The function maximize is similar, except the comparator is .>=. So the value returned has the largest cost (or value, in that case).

The function optimize allows the user to give a custom comparison function.

The OptimizeOpts argument controls how the optimization is done. If Quantified is used, then the SBV optimization engine satisfies the following predicate:

exists xs. forall ys. valid xs && (valid ys ``implies`` (cost xs ``cmp`` cost ys))

Note that this may cause efficiency problems as it involves alternating quantifiers. If OptimizeOpts is set to Iterative True, then SBV will programmatically search for an optimal solution, by repeatedly calling the solver appropriately. (The boolean argument controls whether progress reports are given. Use False for quiet operation.) Note that the quantified and iterative versions are two different optimization approaches and may not necessarily yield the same results. In particular, the quantified version can find solutions where there is no global optimum value, while the iterative version would simply loop forever in such cases. On the other hand, the iterative version might be more suitable if the quantified version of the problem is too hard to deal with by the SMT solver.

minimize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a]) Source

Minimizes a cost function with respect to a constraint. Examples:

>>> minimize Quantified sum 3 (bAll (.> (10 :: SInteger)))
Just [11,11,11]

maximize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a]) Source

Maximizes a cost function with respect to a constraint. Examples:

>>> maximize Quantified sum 3 (bAll (.< (10 :: SInteger)))
Just [9,9,9]

optimize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts -> (SBV c -> SBV c -> SBool) -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a]) Source

Variant of optimizeWith using the default solver. See optimizeWith for parameter descriptions.

minimizeWith :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => SMTConfig -> OptimizeOpts -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a]) Source

Variant of minimize allowing the use of a user specified solver. See optimizeWith for parameter descriptions.

maximizeWith :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => SMTConfig -> OptimizeOpts -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a]) Source

Variant of maximize allowing the use of a user specified solver. See optimizeWith for parameter descriptions.

optimizeWith Source

Arguments

:: (SatModel a, SymWord a, Show a, SymWord c, Show c) 
=> SMTConfig

SMT configuration

-> OptimizeOpts

Optimization options

-> (SBV c -> SBV c -> SBool)

comparator

-> ([SBV a] -> SBV c)

cost function

-> Int

how many elements?

-> ([SBV a] -> SBool)

validity constraint

-> IO (Maybe [a]) 

Symbolic optimization. Generalization on minimize and maximize that allows arbitrary cost functions and comparisons.

Computing expected values

expectedValue :: Outputtable a => Symbolic a -> IO [Double] Source

Given a symbolic computation that produces a value, compute the expected value that value would take if this computation is run with its free variables drawn from uniform distributions of its respective values, satisfying the given constraints specified by constrain and pConstrain calls. This is equivalent to calling expectedValueWith the following parameters: verbose, warm-up round count of 10000, no maximum iteration count, and with convergence margin 0.0001.

expectedValueWith :: Outputtable a => Bool -> Int -> Maybe Int -> Double -> Symbolic a -> IO [Double] Source

Generalized version of expectedValue, allowing the user to specify the warm-up count and the convergence factor. Maximum iteration count can also be specified, at which point convergence won't be sought. The boolean controls verbosity.

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

Show ThmResult

User friendly way of printing theorem results

Modelable ThmResult

ThmResult as a generic model provider

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

Show SatResult

User friendly way of printing satisfiablity results

Modelable SatResult

SatResult as a generic model provider

newtype AllSatResult Source

An allSat call results in a AllSatResult. The boolean says whether we should warn the user about prefix-existentials.

Constructors

AllSatResult (Bool, [SMTResult]) 

Instances

Show AllSatResult

The Show instance of AllSatResults. Note that we have to be careful in being lazy enough as the typical use case is to pull results out as they become available.

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

NFData SMTResult 
Modelable SMTResult

SMTResult as a generic model provider

data SafeResult Source

The result of an sAssert call

Instances

Show SafeResult

The show instance for SafeResult. Note that this is for display purposes only, user programs are likely to pattern match on the output and proceed accordingly.

Exception SafeResult

If a prove or sat call comes accross an sAssert call that fails, they will throw a SafeResult as an exception.

Typeable * SafeResult 

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 where Source

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

Minimal 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

SatModel Bool

Bool as extracted from a model

SatModel Double

Double as extracted from a model

SatModel Float

Float as extracted from a model

SatModel Int8

Int8 as extracted from a model

SatModel Int16

Int16 as extracted from a model

SatModel Int32

Int32 as extracted from a model

SatModel Int64

Int64 as extracted from a model

SatModel Integer

Integer as extracted from a model

SatModel Word8

Word8 as extracted from a model

SatModel Word16

Word16 as extracted from a model

SatModel Word32

Word32 as extracted from a model

SatModel Word64

Word64 as extracted from a model

SatModel ()

Base case for SatModel at unit type. Comes in handy if there are no real variables.

SatModel AlgReal

AlgReal as extracted from a model

SatModel U2Member

The SatModel instance makes it easy to build models, mapping words to U2 members in the way we designated.

SatModel a => SatModel [a]

A list of values as extracted from a model. When reading a list, we go as long as we can (maximal-munch). Note that this never fails, as we can always return the empty list!

(SatModel a, SatModel b) => SatModel (a, b)

Tuples extracted from a model

(SatModel a, SatModel b, SatModel c) => SatModel (a, b, c)

3-Tuples extracted from a model

(SatModel a, SatModel b, SatModel c, SatModel d) => SatModel (a, b, c, d)

4-Tuples extracted from a model

(SatModel a, SatModel b, SatModel c, SatModel d, SatModel e) => SatModel (a, b, c, d, e)

5-Tuples extracted from a model

(SatModel a, SatModel b, SatModel c, SatModel d, SatModel e, SatModel f) => SatModel (a, b, c, d, e, f)

6-Tuples extracted from a model

(SatModel a, SatModel b, SatModel c, SatModel d, SatModel e, SatModel f, SatModel g) => SatModel (a, b, c, d, e, f, g)

7-Tuples extracted from a model

class Modelable a where Source

Various SMT results that we can extract models out of.

Minimal complete definition

modelExists, getModel, getModelDictionary

Methods

modelExists :: a -> Bool Source

Is there a model?

getModel :: SatModel b => a -> Either String (Bool, b) Source

Extract a model, the result is a tuple where the first argument (if True) indicates whether the model was "probable". (i.e., if the solver returned unknown.)

getModelDictionary :: a -> Map String CW Source

Extract a model dictionary. Extract a dictionary mapping the variables to their respective values as returned by the SMT solver. Also see getModelDictionaries.

getModelValue :: SymWord b => String -> a -> Maybe b Source

Extract a model value for a given element. Also see getModelValues.

getModelUninterpretedValue :: String -> a -> Maybe String Source

Extract a representative name for the model value of an uninterpreted kind. This is supposed to correspond to the value as computed internally by the SMT solver; and is unportable from solver to solver. Also see getModelUninterpretedValues.

extractModel :: SatModel b => a -> Maybe b Source

A simpler variant of getModel to get a model out without the fuss.

Instances

Modelable SMTResult

SMTResult as a generic model provider

Modelable SatResult

SatResult as a generic model provider

Modelable ThmResult

ThmResult as a generic model provider

displayModels :: SatModel a => (Int -> (Bool, a) -> IO ()) -> AllSatResult -> IO Int Source

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. The second argument is a tuple, where the first element indicates whether the model is alleged (i.e., if the solver is not sure, returing Unknown)

extractModels :: SatModel a => AllSatResult -> [a] Source

Return all the models from an allSat call, similar to extractModel but is suitable for the case of multiple results.

getModelDictionaries :: AllSatResult -> [Map String CW] Source

Get dictionaries from an all-sat call. Similar to getModelDictionary.

getModelValues :: SymWord b => String -> AllSatResult -> [Maybe b] Source

Extract value of a variable from an all-sat call. Similar to getModelValue.

getModelUninterpretedValues :: String -> AllSatResult -> [Maybe String] Source

Extract value of an uninterpreted variable from an all-sat call. Similar to getModelUninterpretedValue.

SMT Interface: Configurations and solvers

data SMTConfig Source

Solver configuration. See also z3, yices, cvc4, boolector, mathSAT, etc. which are instantiations of this type for those solvers, with reasonable defaults. In particular, custom configuration can be created by varying those values. (Such as z3{verbose=True}.)

Most fields are self explanatory. The notion of precision for printing algebraic reals stems from the fact that such values does not necessarily have finite decimal representations, and hence we have to stop printing at some depth. It is important to emphasize that such values always have infinite precision internally. The issue is merely with how we print such an infinite precision value on the screen. The field printRealPrec controls the printing precision, by specifying the number of digits after the decimal point. The default value is 16, but it can be set to any positive integer.

When printing, SBV will add the suffix ... at the and of a real-value, if the given bound is not sufficient to represent the real-value exactly. Otherwise, the number will be written out in standard decimal notation. Note that SBV will always print the whole value if it is precise (i.e., if it fits in a finite number of digits), regardless of the precision limit. The limit only applies if the representation of the real value is not finite, i.e., if it is not rational.

Constructors

SMTConfig 

Fields

verbose :: Bool

Debug mode

timing :: Bool

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

sBranchTimeOut :: Maybe Int

How much time to give to the solver for each call of sBranch check. (In seconds. Default: No limit.)

timeOut :: Maybe Int

How much time to give to the solver. (In seconds. Default: No limit.)

printBase :: Int

Print integral literals in this base (2, 8, 10, and 16 are supported.)

printRealPrec :: Int

Print algebraic real values with this precision. (SReal, default: 16)

solverTweaks :: [String]

Additional lines of script to give to the solver (user specified)

satCmd :: String

Usually "(check-sat)". However, users might tweak it based on solver characteristics.

smtFile :: Maybe FilePath

If Just, the generated SMT script will be put in this file (for debugging purposes mostly)

useSMTLib2 :: Bool

If True, we'll treat the solver as using SMTLib2 input format. Otherwise, SMTLib1

solver :: SMTSolver

The actual SMT solver.

roundingMode :: RoundingMode

Rounding mode to use for floating-point conversions

useLogic :: Maybe Logic

If Nothing, pick automatically. Otherwise, either use the given one, or use the custom string.

Instances

data SMTLibLogic Source

SMT-Lib logics. If left unspecified SBV will pick the logic based on what it determines is needed. However, the user can override this choice using the useLogic parameter to the configuration. This is especially handy if one is experimenting with custom logics that might be supported on new solvers.

Constructors

AUFLIA

Formulas over the theory of linear integer arithmetic and arrays extended with free sort and function symbols but restricted to arrays with integer indices and values

AUFLIRA

Linear formulas with free sort and function symbols over one- and two-dimentional arrays of integer index and real value

AUFNIRA

Formulas with free function and predicate symbols over a theory of arrays of arrays of integer index and real value

LRA

Linear formulas in linear real arithmetic

UFLRA

Linear real arithmetic with uninterpreted sort and function symbols.

UFNIA

Non-linear integer arithmetic with uninterpreted sort and function symbols.

QF_ABV

Quantifier-free formulas over the theory of bitvectors and bitvector arrays

QF_AUFBV

Quantifier-free formulas over the theory of bitvectors and bitvector arrays extended with free sort and function symbols

QF_AUFLIA

Quantifier-free linear formulas over the theory of integer arrays extended with free sort and function symbols

QF_AX

Quantifier-free formulas over the theory of arrays with extensionality

QF_BV

Quantifier-free formulas over the theory of fixed-size bitvectors

QF_IDL

Difference Logic over the integers. Boolean combinations of inequations of the form x - y < b where x and y are integer variables and b is an integer constant

QF_LIA

Unquantified linear integer arithmetic. In essence, Boolean combinations of inequations between linear polynomials over integer variables

QF_LRA

Unquantified linear real arithmetic. In essence, Boolean combinations of inequations between linear polynomials over real variables.

QF_NIA

Quantifier-free integer arithmetic.

QF_NRA

Quantifier-free real arithmetic.

QF_RDL

Difference Logic over the reals. In essence, Boolean combinations of inequations of the form x - y < b where x and y are real variables and b is a rational constant.

QF_UF

Unquantified formulas built over a signature of uninterpreted (i.e., free) sort and function symbols.

QF_UFBV

Unquantified formulas over bitvectors with uninterpreted sort function and symbols.

QF_UFIDL

Difference Logic over the integers (in essence) but with uninterpreted sort and function symbols.

QF_UFLIA

Unquantified linear integer arithmetic with uninterpreted sort and function symbols.

QF_UFLRA

Unquantified linear real arithmetic with uninterpreted sort and function symbols.

QF_UFNRA

Unquantified non-linear real arithmetic with uninterpreted sort and function symbols.

QF_FPABV

Quantifier-free formulas over the theory of floating point numbers, arrays, and bit-vectors

QF_FPA

Quantifier-free formulas over the theory of floating point numbers

Instances

data Logic Source

Chosen logic for the solver

Constructors

PredefinedLogic SMTLibLogic

Use one of the logics as defined by the standard

CustomLogic String

Use this name for the logic

Instances

data OptimizeOpts Source

Optimizer configuration. Note that iterative and quantified approaches are in general not interchangeable. For instance, iterative solutions will loop infinitely when there is no optimal value, but quantified solutions can handle such problems. Of course, quantified problems are harder for SMT solvers, naturally.

Constructors

Iterative Bool

Iteratively search. if True, it will be reporting progress

Quantified

Use quantifiers

data Solver Source

Solvers that SBV is aware of

Constructors

Z3 
Yices 
Boolector 
CVC4 
MathSAT 

data SMTSolver Source

An SMT solver

Constructors

SMTSolver 

Fields

name :: Solver

The solver in use

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

xformExitCode :: ExitCode -> ExitCode

Should we re-interpret exit codes. Most solvers behave rationally, i.e., id will do. Some (like CVC4) don't.

capabilities :: SolverCapabilities

Various capabilities of the solver

Instances

boolector :: SMTConfig Source

Default configuration for the Boolector SMT solver

cvc4 :: SMTConfig Source

Default configuration for the CVC4 SMT Solver.

yices :: SMTConfig Source

Default configuration for the Yices SMT Solver.

z3 :: SMTConfig Source

Default configuration for the Z3 SMT solver

mathSAT :: SMTConfig Source

Default configuration for the MathSAT SMT solver

defaultSolverConfig :: Solver -> SMTConfig Source

The default configs corresponding to supported SMT solvers

sbvCurrentSolver :: SMTConfig Source

The currently active solver, obtained by importing Data.SBV. To have other solvers current, import one of the bridge modules Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, or Data.SBV.Bridge.Z3 directly.

defaultSMTCfg :: SMTConfig Source

The default solver used by SBV. This is currently set to z3.

sbvCheckSolverInstallation :: SMTConfig -> IO Bool Source

Check whether the given solver is installed and is ready to go. This call does a simple call to the solver to ensure all is well.

sbvAvailableSolvers :: IO [SMTConfig] Source

Return the known available solver configs, installed on your machine.

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 a Source

Mark an interim result as an output. Useful when constructing Symbolic programs that return multiple values, or when the result is programmatically computed.

class (HasKind a, Ord a) => SymWord a where Source

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 definition

Nothing

Methods

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

Create a user named input (universal)

forall_ :: Symbolic (SBV a) Source

Create an automatically named input

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

Get a bunch of new words

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

Create an existential variable

exists_ :: Symbolic (SBV a) Source

Create an automatically named existential variable

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

Create a bunch of existentials

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

Create a free variable, universal in a proof, existential in sat

free_ :: Symbolic (SBV a) Source

Create an unnamed free variable, universal in proof, existential in sat

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

Create a bunch of free vars

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

Similar to free; Just a more convenient name

symbolics :: [String] -> Symbolic [SBV a] Source

Similar to mkFreeVars; but automatically gives names based on the strings

literal :: a -> SBV a Source

Turn a literal constant to symbolic

unliteral :: SBV a -> Maybe a Source

Extract a literal, if the value is concrete

fromCW :: CW -> a Source

Extract a literal, from a CW representation

isConcrete :: SBV a -> Bool Source

Is the symbolic word concrete?

isSymbolic :: SBV a -> Bool Source

Is the symbolic word really symbolic?

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

Does it concretely satisfy the given predicate?

mbMaxBound, mbMinBound :: Maybe a Source

max/minbounds, if available. Note that we don't want to impose Bounded on our class as Integer is not Bounded but it is a SymWord

mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV a) Source

One stop allocator

Instances

SymWord Bool 
SymWord Double 
SymWord Float 
SymWord Int8 
SymWord Int16 
SymWord Int32 
SymWord Int64 
SymWord Integer 
SymWord Word8 
SymWord Word16 
SymWord Word32 
SymWord Word64 
SymWord AlgReal 
SymWord B

Default instance declaration for SymWord

SymWord Q

We need SymWord and HasKind instances, but default definitions are always sufficient for uninterpreted sorts, so all we do is to declare them as such. Note that, starting with GHC 7.6.1, we will be able to simply derive these classes as well. (See http://hackage.haskell.org/trac/ghc/ticket/5462.)

SymWord L

Declare instances to make L a usable uninterpreted sort. First we need the SymWord instance, with the default definition sufficing.

Getting SMT-Lib output (for offline analysis)

compileToSMTLib Source

Arguments

:: Provable a 
=> Bool

If True, output SMT-Lib2, otherwise SMT-Lib1

-> Bool

If True, translate directly, otherwise negate the goal. (Use True for SAT queries, False for PROVE queries.)

-> a 
-> IO String 

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. It takes two booleans:

  • smtLib2: If True, will generate SMT-Lib2 output, otherwise SMT-Lib1 output
    • isSat : If True, will translate it as a SAT query, i.e., in the positive. If False, will translate as a PROVE query, i.e., it will negate the result. (In this case, the check-sat call to the SMT solver will produce UNSAT if the input is a theorem, as usual.)

generateSMTBenchmarks :: Provable a => Bool -> FilePath -> a -> IO () Source

Create both SMT-Lib1 and SMT-Lib2 benchmarks. The first argument is the basename of the file, SMT-Lib1 version will be written with suffix ".smt1" and SMT-Lib2 version will be written with suffix ".smt2". The Bool argument controls whether this is a SAT instance, i.e., translate the query directly, or a PROVE instance, i.e., translate the negated query. (See the second boolean argument to compileToSMTLib for details.)

Test case generation

genTest :: Outputtable a => Int -> Symbolic a -> IO TestVectors Source

Generate a set of concrete test values from a symbolic program. The output can be rendered as test vectors in different languages as necessary. Use the function output call to indicate what fields should be in the test result. (Also see constrain and pConstrain for filtering acceptable test values.)

getTestValues :: TestVectors -> [([CW], [CW])] Source

Retrieve the test vectors for further processing. This function is useful in cases where renderTest is not sufficient and custom output (or further preprocessing) is needed.

data TestVectors Source

Type of test vectors (abstract)

data TestStyle Source

Test output style

Constructors

Haskell String

As a Haskell value with given name

C String

As a C array of structs with given name

Forte String Bool ([Int], [Int])

As a Forte/Verilog value with given name. If the boolean is True then vectors are blasted big-endian, otherwise little-endian The indices are the split points on bit-vectors for input and output values

renderTest :: TestStyle -> TestVectors -> String Source

Render the test as a Haskell value with the given name n.

data CW Source

CW represents a concrete word of a fixed size: Endianness is mostly irrelevant (see the FromBits class). For signed words, the most significant digit is considered to be the sign.

Constructors

CW 

Fields

cwKind :: !Kind
 
cwVal :: !CWVal
 

class HasKind a where Source

A class for capturing values that have a sign and a size (finite or infinite) minimal complete definition: kindOf. This class can be automatically derived for data-types that have a Data instance; this is useful for creating uninterpreted sorts.

Minimal complete definition

Nothing

Instances

HasKind Bool 
HasKind Double 
HasKind Float 
HasKind Int8 
HasKind Int16 
HasKind Int32 
HasKind Int64 
HasKind Integer 
HasKind Word8 
HasKind Word16 
HasKind Word32 
HasKind Word64 
HasKind AlgReal 
HasKind CW 
HasKind B

Default instance declaration for HasKind

HasKind Q

HasKind instance is again straightforward, no specific implementation needed.

HasKind L

Similarly, HasKinds default implementation is sufficient.

HasKind a => HasKind (SBV a) 

data Kind Source

Kind of symbolic value

Instances

cwToBool :: CW -> Bool Source

Convert a CW to a Haskell boolean (NB. Assumes input is well-kinded)

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. Default: False.

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

Sets driver program run time values, useful for generating programs with fixed drivers for testing. Default: None, i.e., use random values.

cgGenerateDriver :: Bool -> SBVCodeGen () Source

Should we generate a driver program? Default: True. When a library is generated, it will have a driver if any of the contituent functions has a driver. (See compileToCLib.)

cgGenerateMakefile :: Bool -> SBVCodeGen () Source

Should we generate a Makefile? Default: True.

Designating inputs

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

Creates an atomic input in the generated code.

cgInputArr :: SymWord a => Int -> String -> SBVCodeGen [SBV a] Source

Creates an array input in the generated code.

Designating outputs

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

Creates an atomic output in the generated code.

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

Creates an array output in the generated code.

Designating return values

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

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

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

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

Code generation with uninterpreted functions

cgAddPrototype :: [String] -> SBVCodeGen () Source

Adds the given lines to the header file generated, useful for generating programs with uninterpreted functions.

cgAddDecl :: [String] -> SBVCodeGen () Source

Adds the given lines to the program file generated, useful for generating programs with uninterpreted functions.

cgAddLDFlags :: [String] -> SBVCodeGen () Source

Adds the given words to the compiler options in the generated Makefile, useful for linking extra stuff in.

Code generation with SInteger and SReal types

The types SInteger and SReal are unbounded quantities that have no direct counterparts in the C language. Therefore, it is not possible to generate standard C code for SBV programs using these types, unless custom libraries are available. To overcome this, SBV allows the user to explicitly set what the corresponding types should be for these two cases, using the functions below. Note that while these mappings will produce valid C code, the resulting code will be subject to overflow/underflows for SInteger, and rounding for SReal, so there is an implicit loss of precision.

If the user does not specify these mappings, then SBV will refuse to compile programs that involve these types.

cgIntegerSize :: Int -> SBVCodeGen () Source

Sets number of bits to be used for representing the SInteger type in the generated C code. The argument must be one of 8, 16, 32, or 64. Note that this is essentially unsafe as the semantics of unbounded Haskell integers becomes reduced to the corresponding bit size, as typical in most C implementations.

cgSRealType :: CgSRealType -> SBVCodeGen () Source

Sets the C type to be used for representing the SReal type in the generated C code. The setting can be one of C's "float", "double", or "long double", types, depending on the precision needed. Note that this is essentially unsafe as the semantics of infinite precision SReal values becomes reduced to the corresponding floating point type in C, and hence it is subject to rounding errors.

data CgSRealType Source

Possible mappings for the SReal type when translated to C. Used in conjunction with the function cgSRealType. Note that the particular characteristics of the mapped types depend on the platform and the compiler used for compiling the generated C program. See http://en.wikipedia.org/wiki/C_data_types for details.

Constructors

CgFloat
float
CgDouble
double
CgLongDouble
long double

Instances

Eq CgSRealType 
Show CgSRealType

Show instance for cgSRealType displays values as they would be used in a C program

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 modules to make any sensible use of the SBV functionality.

module Data.Bits

module Data.Word

module Data.Int

module Data.Ratio