Portability | portable |
---|---|
Stability | experimental |
Maintainer | erkokl@gmail.com |
- Programming with symbolic values
- Uninterpreted constants and functions
- Proving properties
- Model extraction
- SMT Interface: Configurations and solvers
- Symbolic computations
- Getting SMT-Lib output (for offline analysis)
- Compiling symbolic programs to C
- Module exports
(The sbv library is hosted at http://github.com/LeventErkok/sbv. Comments, bug reports, and patches are always welcome.)
SBV: Symbolic Bit Vectors in Haskell
Express properties about bit-precise Haskell programs and automatically prove them using SMT solvers.
>>>
prove $ \x -> x `shiftL` 2 .== 4 * (x :: SWord8)
Q.E.D.
>>>
prove $ forAll ["x"] $ \x -> x `shiftL` 2 .== (x :: SWord8)
Falsifiable. Counter-example: x = 128 :: SWord8
The function prove
has the following type:
prove
::Provable
a => a ->IO
ThmResult
The class Provable
comes with instances for n-ary predicates, for arbitrary n.
The predicates are just regular Haskell functions over symbolic signed and unsigned
bit-vectors. Functions for checking satisfiability (sat
and allSat
) are also
provided.
In particular, the sbv library introduces the types:
-
SBool
: Symbolic Booleans (bits) -
SWord8
,SWord16
,SWord32
,SWord64
: Symbolic Words (unsigned) -
SInt8
,SInt16
,SInt32
,SInt64
: Symbolic Ints (signed) -
SArray
,SFunArray
: Flat arrays of symbolic values - Symbolic polynomials over GF(2^n), and polynomial arithmetic
- Uninterpreted constants and functions over symbolic values, with user defined SMT-Lib axioms
The user can construct ordinary Haskell programs using these types, which behave
very similar to their concrete counterparts. In particular these types belong to the
standard classes Num
, Bits
, custom versions of Eq
(EqSymbolic
)
and Ord
(OrdSymbolic
), along with several other custom classes for simplifying
bit-precise programming with symbolic values. The framework takes full advantage
of Haskell's type inference to avoid many common mistakes.
Furthermore, predicates (i.e., functions that return SBool
) built out of
these types can also be:
- proven correct via an external SMT solver (the
prove
function) - checked for satisfiability (the
sat
andallSat
functions) - quick-checked
If a predicate is not valid, prove
will return a counterexample: An
assignment to inputs such that the predicate fails. The sat
function will
return a satisfying assignment, if there is one. The allSat
function returns
all satisfying assignments, lazily.
The sbv library uses third-party SMT solvers via the standard SMT-Lib interface: http://goedel.cs.uiowa.edu/smtlib/.
While the library is designed to work with any SMT-Lib compliant SMT-solver, solver specific support is required for parsing counter-example/model data since there is currently no agreed upon format for getting models from arbitrary SMT solvers. (The SMT-Lib2 initiative will potentially address this issue in the future, at which point the sbv library can be generalized as well.) Currently, we only support the Yices SMT solver from SRI as far as the counter-example and model generation support is concerned: http://yices.csl.sri.com/. However, other solvers can be hooked up with relative ease.
You should download and install Yices on your machine, and make sure the
yices
executable is in your path before using the sbv library, as it is the
current default solver. Alternatively, you can specify the location of yices
executable in the environment variable SBV_YICES
and the options to yices
in SBV_YICES_OPTIONS
. (The default for the latter is '"-m -f"'.)
- type SBool = SBV Bool
- type SWord8 = SBV Word8
- type SWord16 = SBV Word16
- type SWord32 = SBV Word32
- type SWord64 = SBV Word64
- type SInt8 = SBV Int8
- type SInt16 = SBV Int16
- type SInt32 = SBV Int32
- type SInt64 = SBV Int64
- class SymArray array where
- newArray_ :: (HasSignAndSize a, HasSignAndSize b) => Maybe (SBV b) -> Symbolic (array a b)
- newArray :: (HasSignAndSize a, HasSignAndSize b) => String -> Maybe (SBV b) -> Symbolic (array a b)
- readArray :: array a b -> SBV a -> SBV b
- resetArray :: SymWord b => array a b -> SBV b -> array a b
- writeArray :: SymWord b => array a b -> SBV a -> SBV b -> array a b
- mergeArrays :: SymWord b => SBV Bool -> array a b -> array a b -> array a b
- data SArray a b
- data SFunArray a b
- mkSFunArray :: SBV b -> SFunArray a b
- bitValue :: (Bits a, SymWord a) => SBV a -> Int -> SBool
- setBitTo :: (Bits a, SymWord a) => SBV a -> Int -> SBool -> SBV a
- oneIf :: (Num a, SymWord a) => SBool -> SBV a
- lsb :: (Bits a, SymWord a) => SBV a -> SBool
- msb :: (Bits a, SymWord a) => SBV a -> SBool
- allEqual :: (Eq a, SymWord a) => [SBV a] -> SBool
- allDifferent :: (Eq a, SymWord a) => [SBV a] -> SBool
- blastBE :: (Bits a, SymWord a) => SBV a -> [SBool]
- blastLE :: (Bits a, SymWord a) => SBV a -> [SBool]
- class FromBits a where
- fromBitsLE :: [SBool] -> a
- fromBitsBE :: [SBool] -> a
- class Splittable a b | b -> a where
- class Bits a => Polynomial a where
- class Mergeable a where
- class EqSymbolic a where
- class (Mergeable a, EqSymbolic a) => OrdSymbolic a where
- class BVDivisible a where
- bvQuotRem :: a -> a -> (a, a)
- class Boolean b where
- bAnd :: Boolean b => [b] -> b
- bOr :: Boolean b => [b] -> b
- bAny :: Boolean b => (a -> b) -> [a] -> b
- bAll :: Boolean b => (a -> b) -> [a] -> b
- class PrettyNum a where
- readBin :: Num a => String -> a
- class Uninterpreted a where
- uninterpret :: String -> a
- uninterpretWithHandle :: String -> (SBVUF, a)
- data SBVUF
- sbvUFName :: SBVUF -> String
- addAxiom :: String -> [String] -> Symbolic ()
- type Predicate = Symbolic SBool
- class Provable a where
- class Equality a where
- prove :: Provable a => a -> IO ThmResult
- proveWith :: Provable a => SMTConfig -> a -> IO ThmResult
- isTheorem :: Provable a => a -> IO Bool
- isTheoremWithin :: Provable a => Int -> a -> IO (Maybe Bool)
- sat :: Provable a => a -> IO SatResult
- satWith :: Provable a => SMTConfig -> a -> IO SatResult
- isSatisfiable :: Provable a => a -> IO Bool
- isSatisfiableWithin :: Provable a => Int -> a -> IO (Maybe Bool)
- allSat :: Provable a => a -> IO AllSatResult
- allSatWith :: Provable a => SMTConfig -> a -> IO AllSatResult
- numberOfModels :: Provable a => a -> IO Int
- newtype ThmResult = ThmResult SMTResult
- newtype SatResult = SatResult SMTResult
- newtype AllSatResult = AllSatResult [SMTResult]
- data SMTResult
- = Unsatisfiable SMTConfig
- | Satisfiable SMTConfig SMTModel
- | Unknown SMTConfig SMTModel
- | ProofError SMTConfig [String]
- | TimeOut SMTConfig
- class SatModel a where
- getModel :: SatModel a => SMTResult -> a
- displayModels :: SatModel a => (Int -> a -> IO ()) -> AllSatResult -> IO Int
- data SMTConfig = SMTConfig {}
- data SMTSolver = SMTSolver {}
- defaultSMTCfg :: SMTConfig
- verboseSMTCfg :: SMTConfig
- timingSMTCfg :: SMTConfig
- verboseTimingSMTCfg :: SMTConfig
- timeout :: Int -> SMTConfig -> SMTConfig
- yices :: SMTSolver
- data Symbolic a
- output :: Outputtable a => a -> Symbolic a
- class Ord a => SymWord a where
- compileToSMTLib :: Provable a => a -> IO String
- newtype CgPgmBundle = CgPgmBundle [(FilePath, Doc)]
- compileToC :: SymExecutable f => Bool -> Maybe FilePath -> String -> [String] -> f -> IO ()
- compileToC' :: SymExecutable f => [Integer] -> Bool -> String -> [String] -> f -> IO CgPgmBundle
- module Data.Bits
- module Data.Word
- module Data.Int
Programming with symbolic values
The SBV library is really two things:
- A framework for writing bit-precise programs in Haskell
- A framework for proving properties of such programs using SMT solvers
In this first section we will look at the constructs that will let us construct such
programs in Haskell. The goal is to have a seamless experience, i.e., program in
the usual Haskell style without distractions of symbolic coding. While Haskell helps
in some aspects (the Num
and Bits
classes simplify coding), it makes life harder
in others. For instance, if-then-else
only takes Bool
as a test in Haskell, and
comparisons (>
etc.) only return Bool
s. 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
Unsigned symbolic bit-vectors
Signed symbolic bit-vectors
Arrays of symbolic values
class SymArray array whereSource
Flat arrays of symbolic values
An array a b
is an array indexed by the type
, with elements of type SBV
a
If an initial value is not provided in SBV
bnewArray_
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.
newArray_ :: (HasSignAndSize a, HasSignAndSize b) => Maybe (SBV b) -> Symbolic (array a b)Source
Create a new array, with an optional initial value
newArray :: (HasSignAndSize a, HasSignAndSize b) => String -> Maybe (SBV b) -> Symbolic (array a b)Source
Create a named new array, with an optional initial value
readArray :: array a b -> SBV a -> SBV bSource
Read the array element at a
resetArray :: SymWord b => array a b -> SBV b -> array a bSource
Reset all the elements of the array to the value b
writeArray :: SymWord b => array a b -> SBV a -> SBV b -> array a bSource
Update the element at a
to be b
mergeArrays :: SymWord b => SBV Bool -> array a b -> array a b -> array a bSource
Merge two given arrays on the symbolic condition
Intuitively: mergeArrays cond a b = if cond then a else b
.
Merging pushes the if-then-else choice down on to elements
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
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
mkSFunArray :: SBV b -> SFunArray a bSource
Make a constant fun-array always returning a fixed value.
Useful for creating arrays in a pure context. (Otherwise use newArray
.)
Operations on symbolic words
Word level
lsb :: (Bits a, SymWord a) => SBV a -> SBoolSource
Least significant bit of a word, always stored at index 0
msb :: (Bits a, SymWord a) => SBV a -> SBoolSource
Most significant bit of a word, always stored at the last position
List level
allEqual :: (Eq a, SymWord a) => [SBV a] -> SBoolSource
Returns (symbolic) true if all the elements of the given list are the same
allDifferent :: (Eq a, SymWord a) => [SBV a] -> SBoolSource
Returns (symbolic) true if all the elements of the given list are different
Blasting/Unblasting
blastBE :: (Bits a, SymWord a) => SBV a -> [SBool]Source
Big-endian blasting of a word into its bits. Also see the FromBits
class
blastLE :: (Bits a, SymWord a) => SBV a -> [SBool]Source
Little-endian blasting of a word into its bits. Also see the FromBits
class
Unblasting a value from symbolic-bits. The bits can be given little-endian or big-endian. For a signed number in little-endian, we assume the very last bit is the sign digit. This is a bit awkward, but it is more consistent with the reverse view of little-big-endian representations
Minimal complete definiton: fromBitsLE
fromBitsLE :: [SBool] -> aSource
fromBitsBE :: [SBool] -> aSource
Splitting, joining, and extending
class Splittable a b | b -> a whereSource
Splitting an a
into two b
's and joining back.
Intuitively, a
is a larger bit-size word than b
, typically double.
The extend
operation captures embedding of a b
value into an a
without changing its semantic value.
Minimal complete definition: All, no defaults.
Polynomial arithmetic
class Bits a => Polynomial a whereSource
Implements polynomial addition, multiplication, division, and modulus operations
over GF(2^n). NB. Similar to bvQuotRem
, division by 0
is interpreted as follows:
x pDivMod
0 = (0, x)
for all x
(including 0
)
polynomial :: [Int] -> aSource
Given bit-positions to be set, create a polynomial For instance
polynomial [0, 1, 3] :: SWord8
will evaluate to 11
, since it sets the bits 0
, 1
, and 3
. Mathematicans would write this polynomial
as x^3 + x + 1
. And in fact, showPoly
will show it like that.
Add two polynomials in GF(2^n)
pMult :: (a, a, [Int]) -> aSource
Multiply two polynomials in GF(2^n), and reduce it by the irreducible specified by the polynomial as specified by coefficients of the third argument. Note that the third argument is specifically left in this form as it is usally in GF(2^(n+1)), which is not available in our formalism. (That is, we would need SWord9 for SWord8 multiplication, etc.) Also note that we do not support symbolic irreducibles, which is a minor shortcoming. (Most GF's will come with fixed irreducibles, so this should not be a problem in practice.)
Passing [] for the third argument will multiply the polynomials and then ignore the higher bits that won't fit into the resulting size.
Divide two polynomials in GF(2^n), see above note for division by 0
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
Display a polynomial like a mathematician would (over the monomial x
)
Conditionals: Mergeable values
Symbolic choice operator, parameterized via a class
select
is a total-indexing function, with the default.
Minimal complete definition: symbolicMerge
symbolicMerge :: SBool -> a -> a -> aSource
Merge two values based on the condition
ite :: SBool -> a -> a -> aSource
Choose one or the other element, based on the condition.
This is similar to symbolicMerge
, but it has a default
implementation that makes sure it's short-cut if the condition is concrete
select :: (Bits b, SymWord b, Integral b) => [a] -> a -> SBV b -> aSource
Total indexing operation. select xs default index
is intuitively
the same as xs !! index
, except it evaluates to default
if index
overflows
Mergeable () | |
Mergeable Mostek | |
Mergeable Status | |
Mergeable a => Mergeable [a] | |
Mergeable a => Mergeable (Maybe a) | |
SymWord a => Mergeable (SBV a) | |
Mergeable a => Mergeable (Move a) | |
Mergeable b => Mergeable (a -> b) | |
(Mergeable a, Mergeable b) => Mergeable (Either a b) | |
(Mergeable a, Mergeable b) => Mergeable (a, b) | |
(Ix a, Mergeable b) => Mergeable (Array a b) | |
SymWord b => Mergeable (SFunArray a b) | |
SymWord b => Mergeable (SArray a b) | |
(Mergeable a, Mergeable b, Mergeable c) => Mergeable (a, b, c) | |
(Mergeable a, Mergeable b, Mergeable c, Mergeable d) => Mergeable (a, b, c, d) | |
(Mergeable a, Mergeable b, Mergeable c, Mergeable d, Mergeable e) => Mergeable (a, b, c, d, e) | |
(Mergeable a, Mergeable b, Mergeable c, Mergeable d, Mergeable e, Mergeable f) => Mergeable (a, b, c, d, e, f) | |
(Mergeable a, Mergeable b, Mergeable c, Mergeable d, Mergeable e, Mergeable f, Mergeable g) => Mergeable (a, b, c, d, e, f, g) |
Symbolic equality
class EqSymbolic a whereSource
Symbolic Equality. Note that we can't use Haskell's Eq
class since Haskell insists on returning Bool
Comparing symbolic values will necessarily return a symbolic value.
Minimal complete definition: .==
EqSymbolic Bool | |
EqSymbolic SWord11 | |
EqSymbolic a => EqSymbolic [a] | |
EqSymbolic a => EqSymbolic (Maybe a) | |
EqSymbolic (SBV a) | |
(EqSymbolic a, EqSymbolic b) => EqSymbolic (Either a b) | |
(EqSymbolic a, EqSymbolic b) => EqSymbolic (a, b) | |
EqSymbolic (SArray a b) | |
(EqSymbolic a, EqSymbolic b, EqSymbolic c) => EqSymbolic (a, b, c) | |
(EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d) => EqSymbolic (a, b, c, d) | |
(EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d, EqSymbolic e) => EqSymbolic (a, b, c, d, e) | |
(EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d, EqSymbolic e, EqSymbolic f) => EqSymbolic (a, b, c, d, e, f) | |
(EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d, EqSymbolic e, EqSymbolic f, EqSymbolic g) => EqSymbolic (a, b, c, d, e, f, g) |
Symbolic ordering
class (Mergeable a, EqSymbolic a) => OrdSymbolic a whereSource
Symbolic Comparisons. Similar to Eq
, we cannot implement Haskell's Ord
class
since there is no way to return an Ordering
value from a symbolic comparison.
Furthermore, OrdSymbolic
requires Mergeable
to implement if-then-else, for the
benefit of implementing symbolic versions of max
and min
functions.
Minimal complete definition: .<
OrdSymbolic a => OrdSymbolic [a] | |
OrdSymbolic a => OrdSymbolic (Maybe a) | |
SymWord a => OrdSymbolic (SBV a) | |
(OrdSymbolic a, OrdSymbolic b) => OrdSymbolic (Either a b) | |
(OrdSymbolic a, OrdSymbolic b) => OrdSymbolic (a, b) | |
(OrdSymbolic a, OrdSymbolic b, OrdSymbolic c) => OrdSymbolic (a, b, c) | |
(OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d) => OrdSymbolic (a, b, c, d) | |
(OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d, OrdSymbolic e) => OrdSymbolic (a, b, c, d, e) | |
(OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d, OrdSymbolic e, OrdSymbolic f) => OrdSymbolic (a, b, c, d, e, f) | |
(OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d, OrdSymbolic e, OrdSymbolic f, OrdSymbolic g) => OrdSymbolic (a, b, c, d, e, f, g) |
Division
class BVDivisible a whereSource
The BVDivisible
class captures the essence of division of words.
Unfortunately we cannot use Haskell's Integral
class since the Real
and Enum
superclasses are not implementable for symbolic bit-vectors.
However, quotRem
makes perfect sense, and the BVDivisible
class captures
this operation. One issue is how division by 0 behaves. The verification
technology requires total functions, and there are several design choices
here. We follow Isabelle/HOL approach of assigning the value 0 for division
by 0. Therefore, we impose the following law:
x bvQuotRem
0 = (0, x)
Note that our instances implement this law even when x
is 0
itself.
Minimal complete definition: bvQuotRem
The Boolean class
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.
logical true
logical false
complement
and
or
nand
nor
xor
implies
equivalence
cast from Bool
Generalizations of boolean operations
Pretty-printing and reading numbers in Hex & Binary
PrettyNum class captures printing of numbers in hex and binary formats; also supporting negative numbers.
readBin :: Num a => String -> aSource
A more convenient interface for reading binary numbers, also supports negative numbers
Uninterpreted constants and functions
class Uninterpreted a whereSource
Uninterpreted constants and functions. An uninterpreted constant is a value that is indexed by its name. The only property the prover assumes about these values are that they are equivalent to themselves; i.e., (for functions) they return the same results when applied to same arguments. We support uninterpreted-functions as a general means of black-box'ing operations that are irrelevant for the purposes of the proof; i.e., when the proofs can be performed without any knowledge about the function itself.
Minimal complete definition: uninterpretWithHandle
. However, most instances in
practice are already provided by SBV, so end-users should not need to define their
own instances.
uninterpret :: String -> aSource
Uninterpret a value, receiving an object that can be used instead. Use this version when you do not need to add an axiom about this value.
uninterpretWithHandle :: String -> (SBVUF, a)Source
Uninterpret a value, but also get a handle to the resulting object. This handle
can be used to add axioms for this object. (See addAxiom
.)
HasSignAndSize a => Uninterpreted (SBV a) | |
(HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted ((SBV c, SBV b) -> SBV a) | |
(HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted ((SBV d, SBV c, SBV b) -> SBV a) | |
(HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted ((SBV e, SBV d, SBV c, SBV b) -> SBV a) | |
(HasSignAndSize f, HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted ((SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) | |
(HasSignAndSize g, HasSignAndSize f, HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted ((SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) | |
(HasSignAndSize h, HasSignAndSize g, HasSignAndSize f, HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted ((SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) | |
(HasSignAndSize h, HasSignAndSize g, HasSignAndSize f, HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted (SBV h -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) | |
(HasSignAndSize g, HasSignAndSize f, HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted (SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) | |
(HasSignAndSize f, HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted (SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) | |
(HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted (SBV e -> SBV d -> SBV c -> SBV b -> SBV a) | |
(HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted (SBV d -> SBV c -> SBV b -> SBV a) | |
(HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted (SBV c -> SBV b -> SBV a) | |
(HasSignAndSize b, HasSignAndSize a) => Uninterpreted (SBV b -> SBV a) |
Accessing the handle
An uninterpreted function handle. This is the handle to be used for adding axioms about uninterpreted constants/functions. Note that we will leave this abstract for safety purposes
sbvUFName :: SBVUF -> StringSource
Get the name associated with the uninterpreted-value; useful when constructing axioms about this UI.
Adding axioms
addAxiom :: String -> [String] -> Symbolic ()Source
Add a user specified axiom to the generated SMT-Lib file. Note that the input is a mere string; we perform no checking on the input that it's well-formed or is sensical. A separate formalization of SMT-Lib would be very useful here.
Proving properties
The SBV library provides a push-button verification system via automated SMT solving. The design goal is to let SMT solvers be used without any knowledge of how SMT solvers work or how different logics operate. The details are hidden behind the SBV framework, providing Haskell programmers with a clean API that is unencumbered by the details of individual solvers. To that end, we use the SMT-Lib standard (http://goedel.cs.uiowa.edu/smtlib/) to communicate with arbitrary SMT solvers. Unfortunately, the SMT-Lib version 1.X does not standardize how models are communicated back from solvers, so there is some work in parsing individual SMT solver output. The 2.X version of the SMT-Lib standard (not yet implemented by SMT solvers widely, unfortunately) will bring new standard features for getting models; at which time the SBV framework can be modified into a truly plug-and-play system where arbitrary SMT solvers can be used.
Predicates
type Predicate = Symbolic SBoolSource
A predicate is a symbolic program that returns a (symbolic) boolean value. For all intents and
purposes, it can be treated as an n-ary function from symbolic-values to a boolean. The Symbolic
monad captures the underlying representation, and can/should be ignored by the users of the library,
unless you are building further utilities on top of SBV itself. Instead, simply use the Predicate
type when necessary.
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.)
forAll_ :: a -> PredicateSource
Turns a value into a predicate, internally naming the inputs.
In this case the sbv library will use names of the form s1, s2
, etc. to name these variables
Example:
forAll_ $ \(x::SWord8) y -> x `shiftL` 2 .== y
is a predicate with two arguments, captured using an ordinary Haskell function. Internally,
x
will be named s0
and y
will be named s1
.
forAll :: [String] -> a -> PredicateSource
Turns a value into a predicate, allowing users to provide names for the inputs. If the user does not provide enough number of names for the free variables, the remaining ones will be internally generated. Note that the names are only used for printing models and has no other significance; in particular, we do not check that they are unique. Example:
forAll ["x", "y"] $ \(x::SWord8) y -> x `shiftL` 2 .== y
This is the same as above, except the variables will be named x
and y
respectively,
simplifying the counter-examples when they are printed.
Provable SBool | |
Provable Predicate | |
(SymWord a, SymWord b, Provable p) => Provable ((SBV a, SBV b) -> p) | |
(SymWord a, SymWord b, SymWord c, Provable p) => Provable ((SBV a, SBV b, SBV c) -> p) | |
(SymWord a, SymWord b, SymWord c, SymWord d, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d) -> p) | |
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) | |
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) | |
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) | |
(HasSignAndSize a, HasSignAndSize b, SymArray array, Provable p) => Provable (array a b -> p) | |
(SymWord a, Provable p) => Provable (SBV a -> p) |
Equality as a proof method. Allows for very concise construction of equivalence proofs, which is very typical in bit-precise proofs.
Proving properties
prove :: Provable a => a -> IO ThmResultSource
Prove a predicate, equivalent to proveWith
defaultSMTCfg
proveWith :: Provable a => SMTConfig -> a -> IO ThmResultSource
Proves the predicate using the given SMT-solver
isTheoremWithin :: Provable a => Int -> a -> IO (Maybe Bool)Source
Checks theoremhood within the given time limit of i
seconds.
Returns Nothing
if times out, or the result wrapped in a Just
otherwise.
Checking satisfiability
sat :: Provable a => a -> IO SatResultSource
Find a satisfying assignment for a predicate, equivalent to satWith
defaultSMTCfg
satWith :: Provable a => SMTConfig -> a -> IO SatResultSource
Find a satisfying assignment using the given SMT-solver
isSatisfiable :: Provable a => a -> IO BoolSource
Checks satisfiability
isSatisfiableWithin :: Provable a => Int -> a -> IO (Maybe Bool)Source
Checks satisfiability within the given time limit of i
seconds.
Returns Nothing
if times out, or the result wrapped in a Just
otherwise.
Finding all satisfying assignments
allSat :: Provable a => a -> IO AllSatResultSource
Return all satisfying assignments for a predicate, equivalent to
.
Satisfying assignments are constructed lazily, so they will be available as returned by the solver
and on demand.
allSatWith
defaultSMTCfg
NB. Uninterpreted constant/function values and counter-examples for array values are ignored for
the purposes of
. 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.
allSat
allSatWith :: Provable a => SMTConfig -> a -> IO AllSatResultSource
Find all satisfying assignments using the given SMT-solver
numberOfModels :: Provable a => a -> IO IntSource
Returns the number of models that satisfy the predicate, as it would
be returned by allSat
. Note that the number of models is always a
finite number, and hence this will always return a result. Of course,
computing it might take quite long, as it literally generates and counts
the number of satisfying models.
Model extraction
The default Show
instances for prover calls provide all the counter-example information in a
human-readable form and should be sufficient for most casual uses of sbv. However, tools built
on top of sbv will inevitably need to look into the constructed models more deeply, programmatically
extracting their results and performing actions based on them. The API provided in this section
aims at simplifying this task.
Inspecting proof results
ThmResult
, SatResult
, and AllSatResult
are simple newtype wrappers over SMTResult
. Their
main purpose is so that we can provide custom Show
instances to print results accordingly.
newtype AllSatResult Source
An allSat
call results in a AllSatResult
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.)
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 |
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.
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
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.
SatModel Bool | |
SatModel Int8 | |
SatModel Int16 | |
SatModel Int32 | |
SatModel Int64 | |
SatModel Word8 | |
SatModel Word16 | |
SatModel Word32 | |
SatModel Word64 | |
SatModel U2Member | |
SatModel a => SatModel [a] | |
(SatModel a, SatModel b) => SatModel (a, b) | |
(SatModel a, SatModel b, SatModel c) => SatModel (a, b, c) | |
(SatModel a, SatModel b, SatModel c, SatModel d) => SatModel (a, b, c, d) | |
(SatModel a, SatModel b, SatModel c, SatModel d, SatModel e) => SatModel (a, b, c, d, e) | |
(SatModel a, SatModel b, SatModel c, SatModel d, SatModel e, SatModel f) => SatModel (a, b, c, d, e, f) | |
(SatModel a, SatModel b, SatModel c, SatModel d, SatModel e, SatModel f, SatModel g) => SatModel (a, b, c, d, e, f, g) |
displayModels :: SatModel a => (Int -> a -> IO ()) -> AllSatResult -> IO IntSource
Given an allSat
call, we typically want to iterate over it and print the results in sequence. The
displayModels
function automates this task by calling disp
on each result, consecutively. The first
Int
argument to disp
'is the current model number.
SMT Interface: Configurations and solvers
Solver configuration
An SMT solver
defaultSMTCfg :: SMTConfigSource
Default configuration for the SMT solver. Non-verbose, non-timing, prints results in base 10, and uses the Yices SMT solver.
verboseSMTCfg :: SMTConfigSource
Same as defaultSMTCfg
, except verbose
timingSMTCfg :: SMTConfigSource
Same as defaultSMTCfg
, except prints timing info
verboseTimingSMTCfg :: SMTConfigSource
Same as defaultSMTCfg
, except both verbose and timing info
timeout :: Int -> SMTConfig -> SMTConfigSource
Adds a time out of n
seconds to a given solver configuration
The description of the Yices SMT solver
The default executable is "yices"
, which must be in your path. You can use the SBV_YICES
environment variable to point to the executable on your system.
The default options are "-m -f"
, which is valid for Yices 2 series. You can use the SBV_YICES_OPTIONS
environment variable to override the options.
Symbolic computations
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.
class Ord a => SymWord a whereSource
A SymWord
is a potential symbolic bitvector that can be created instances of
to be fed to a symbolic program. Note that these methods are typically not needed
in casual uses with prove
, sat
, allSat
etc, as default instances automatically
provide the necessary bits.
Minimal complete definiton: free, free_, literal, fromCW
free :: String -> Symbolic (SBV a)Source
Create a user named input
free_ :: Symbolic (SBV a)Source
Create an automatically named input
mkFreeVars :: Int -> Symbolic [SBV a]Source
Get a bunch of new words
Turn a literal constant to symbolic
unliteral :: SBV a -> Maybe aSource
Extract a literal, if the value is concrete
Extract a literal, from a CW representation
isConcrete :: SBV a -> BoolSource
Is the symbolic word concrete?
isSymbolic :: SBV a -> BoolSource
Is the symbolic word really symbolic?
isConcretely :: SBV a -> (a -> Bool) -> BoolSource
Does it concretely satisfy the given predicate?
Getting SMT-Lib output (for offline analysis)
compileToSMTLib :: Provable a => a -> IO StringSource
Compiles to SMT-Lib and returns the resulting program as a string. Useful for saving the result to a file for off-line analysis, for instance if you have an SMT solver that's not natively supported out-of-the box by the SBV library.
Compiling symbolic programs to C
newtype CgPgmBundle Source
Representation of a collection of generated programs. Code generation produces a number of files (drivers, source, headers, etc.) and corresponding contents.
CgPgmBundle [(FilePath, Doc)] |
compileToC :: SymExecutable f => Bool -> Maybe FilePath -> String -> [String] -> f -> IO ()Source
Given a symbolic computation, render it as an equivalent C program.
- First argument: States whether run-time-checks should be inserted for index-out-of-bounds or shifting-by-large values etc.
If
False
, such checks are ignored, gaining efficiency, at the cost of potential undefined behavior. - Second argument is an optional directory name under which the files will be saved. If
Nothing
, the result will be written to stdout. Use
for creating files in the current directory.Just
"." - The third argument is name of the function, which also forms the names of the C and header files.
- The fourth argument are the names of the arguments to be used and the names of the outputs, if any. Provide as many arguments as you like, SBV will make up ones if you don't pass enough.
- The fifth and the final argument is the computation to be compiled.
Compilation will also generate a Makefile
and a sample driver program, which executes the program over random
input values.
compileToC' :: SymExecutable f => [Integer] -> Bool -> String -> [String] -> f -> IO CgPgmBundleSource
Alternative interface for generating C. The output driver program uses the specified values (first argument) instead of random values. Also this version returns the generated files for further manipulation. (Useful mainly for generating regression tests.)
Module exports
The SBV library exports the following modules wholesale, as user programs will have to import these three modules to make any sensible use of the SBV functionality.
module Data.Bits
module Data.Word
module Data.Int