Language.Verification

Strongly-typed utilities to aid in automatic verification (e.g. of programs) using an SMT solver.

This is mainly just a wrapper around Data.SBV that allows for inspection and manipulation of symbolic values, especially variable substitution.

The verification monad

data Verifier v a

Instances

MonadReader SMTConfig (Verifier v)

Defined in Language.Verification.Core

Methods

ask :: Verifier v SMTConfig

local :: (SMTConfig -> SMTConfig) -> Verifier v a -> Verifier v a

reader :: (SMTConfig -> a) -> Verifier v a

Monad (Verifier v)

Defined in Language.Verification.Core

Methods

(>>=) :: Verifier v a -> (a -> Verifier v b) -> Verifier v b

(>>) :: Verifier v a -> Verifier v b -> Verifier v b

return :: a -> Verifier v a

Functor (Verifier v)

Defined in Language.Verification.Core

Methods

fmap :: (a -> b) -> Verifier v a -> Verifier v b

(<$) :: a -> Verifier v b -> Verifier v a

Applicative (Verifier v)

Defined in Language.Verification.Core

Methods

pure :: a -> Verifier v a

(<*>) :: Verifier v (a -> b) -> Verifier v a -> Verifier v b

liftA2 :: (a -> b -> c) -> Verifier v a -> Verifier v b -> Verifier v c

(*>) :: Verifier v a -> Verifier v b -> Verifier v b

(<*) :: Verifier v a -> Verifier v b -> Verifier v a

MonadIO (Verifier v)

Defined in Language.Verification.Core

Methods

liftIO :: IO a -> Verifier v a

MonadError (VerifierError v) (Verifier v)

Defined in Language.Verification.Core

Methods

throwError :: VerifierError v -> Verifier v a

catchError :: Verifier v a -> (VerifierError v -> Verifier v a) -> Verifier v a

runVerifier :: VerifiableVar v => Verifier v a -> IO (Either (VerifierError v) a)

runVerifierWith :: VerifiableVar v => SMTConfig -> Verifier v a -> IO (Either (VerifierError v) a)

data VerifierError v

Constructors

VEMismatchedSymbolType (VarKey v)

The same variable was used for two different symbol types

VESbvException String String

When running a query, SBV threw an exception

Instances

Show (VarKey v) => Show (VerifierError v)

Defined in Language.Verification.Core

Methods

showsPrec :: Int -> VerifierError v -> ShowS

show :: VerifierError v -> String

showList :: [VerifierError v] -> ShowS

(Typeable v, l ~ VarKey v, Show l, Typeable l) => Exception (VerifierError v)

Defined in Language.Verification.Core

Methods

toException :: VerifierError v -> SomeException

fromException :: SomeException -> Maybe (VerifierError v)

displayException :: VerifierError v -> String

MonadError (VerifierError v) (Verifier v)

Defined in Language.Verification.Core

Methods

throwError :: VerifierError v -> Verifier v a

catchError :: Verifier v a -> (VerifierError v -> Verifier v a) -> Verifier v a

The query monad

data Query v a

Instances

Monad (Query v)

Defined in Language.Verification.Core

Methods

(>>=) :: Query v a -> (a -> Query v b) -> Query v b

(>>) :: Query v a -> Query v b -> Query v b

return :: a -> Query v a

Functor (Query v)

Defined in Language.Verification.Core

Methods

fmap :: (a -> b) -> Query v a -> Query v b

(<$) :: a -> Query v b -> Query v a

MonadFail (Query v)

Defined in Language.Verification.Core

Methods

fail :: String -> Query v a

Applicative (Query v)

Defined in Language.Verification.Core

Methods

pure :: a -> Query v a

(<*>) :: Query v (a -> b) -> Query v a -> Query v b

liftA2 :: (a -> b -> c) -> Query v a -> Query v b -> Query v c

(*>) :: Query v a -> Query v b -> Query v b

(<*) :: Query v a -> Query v b -> Query v a

MonadIO (Query v)

Defined in Language.Verification.Core

Methods

liftIO :: IO a -> Query v a

query :: VerifiableVar v => Query v SBool -> VarEnv v -> Verifier v Bool

Verifiable variables

class (Typeable v, Ord (VarKey v), Show (VarKey v), Typeable (VarKey v)) => VerifiableVar v where

Associated Types

type VarKey v

type VarSym v :: * -> *

type VarEnv v :: *

Methods

symForVar :: v a -> VarEnv v -> Symbolic (VarSym v a)

varKey :: v a -> VarKey v

eqVarTypes :: v a -> v b -> Maybe (a :~: b)

castVarSym :: v a -> VarSym v b -> Maybe (VarSym v a)

Instances

VerifiableVar (WhileVar String)

Defined in Language.While.Syntax

Associated Types

type VarKey (WhileVar String)

type VarSym (WhileVar String) :: Type -> Type

type VarEnv (WhileVar String)

Methods

symForVar :: WhileVar String a -> VarEnv (WhileVar String) -> Symbolic (VarSym (WhileVar String) a)

varKey :: WhileVar String a -> VarKey (WhileVar String)

eqVarTypes :: WhileVar String a -> WhileVar String b -> Maybe (a :~: b)

castVarSym :: WhileVar String a -> VarSym (WhileVar String) b -> Maybe (VarSym (WhileVar String) a)

Verifier actions

evalProp :: (HMonad expr, HTraversable expr, VerifiableVar v, Exception (VerifierError v), HFoldableAt k expr, HFoldableAt k LogicOp, Monad m) => (forall a. Query v a -> m a) -> (forall a. VarSym v a -> m (k a)) -> Prop (expr v) b -> m (k b)

evalProp' :: (HMonad expr, HTraversable expr, VerifiableVar v, Exception (VerifierError v), HFoldableAt (Compose m k) expr, HFoldableAt (Compose m k) LogicOp, Monad m) => (forall a. Query v a -> m a) -> (forall a. VarSym v a -> m (k a)) -> Prop (expr v) b -> m (k b)

evalPropSimple :: (HMonad expr, HTraversable expr, VerifiableVar v, Exception (VerifierError v), HFoldableAt SBV expr, VarSym v ~ SBV) => Prop (expr v) b -> Query v (SBV b)

Miscellaneous combinators

subVar :: (HPointed expr, VerifiableVar v, Eq (VarKey v)) => expr v a -> v a -> v b -> expr v b

If the two variables match in both type and name, return the given expression. Otherwise, return an expression just containing this variable.

This is substitution into an expression, where the old expression is just a variable.

Expressions

module Language.Expression

SBV re-exports

data SMTConfig

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.

The printBase field can be used to print numbers in base 2, 10, or 16. If base 2 or 16 is used, then floating-point values will be printed in their internal memory-layout format as well, which can come in handy for bit-precise analysis.

Constructors

SMTConfig

Fields

• verbose :: Bool

  Debug mode

• timing :: Timing

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

• printBase :: Int

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

• printRealPrec :: Int

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

• satCmd :: String

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

• allSatMaxModelCount :: Maybe Int

  In a allSat call, return at most this many models. If nothing, return all.

• allSatPrintAlong :: Bool

  In a allSat call, print models as they are found.

• satTrackUFs :: Bool

  In a sat call, should we try to extract values of uninterpreted functions?

• isNonModelVar :: Text -> Bool

  When constructing a model, ignore variables whose name satisfy this predicate. (Default: (const False), i.e., don't ignore anything)

• validateModel :: Bool

  If set, SBV will attempt to validate the model it gets back from the solver.

• optimizeValidateConstraints :: Bool

  Validate optimization results. NB: Does NOT make sure the model is optimal, just checks they satisfy the constraints.

• transcript :: Maybe FilePath

  If Just, the entire interaction will be recorded as a playable file (for debugging purposes mostly)

• smtLibVersion :: SMTLibVersion

  What version of SMT-lib we use for the tool

• dsatPrecision :: Maybe Double

  Delta-sat precision

• solver :: SMTSolver

  The actual SMT solver.

• extraArgs :: [String]

  Extra command line arguments to pass to the solver.

• allowQuantifiedQueries :: Bool

  Should we permit use of quantifiers in the query mode? (Default: False. See http://github.com/LeventErkok/sbv/issues/459 for why.)

• roundingMode :: RoundingMode

  Rounding mode to use for floating-point conversions

• solverSetOptions :: [SMTOption]

  Options to set as we start the solver

• ignoreExitCode :: Bool

  If true, we shall ignore the exit code upon exit. Otherwise we require ExitSuccess.

• redirectVerbose :: Maybe FilePath

  Redirect the verbose output to this file if given. If Nothing, stdout is implied.

Instances

Show SMTConfig

We show the name of the solver for the config. Arguably this is misleading, but better than nothing.

Defined in Data.SBV.Core.Symbolic

Methods

showsPrec :: Int -> SMTConfig -> ShowS

show :: SMTConfig -> String

showList :: [SMTConfig] -> ShowS

NFData SMTConfig

Defined in Data.SBV.Core.Symbolic

Methods

rnf :: SMTConfig -> ()

MonadReader SMTConfig (Verifier v)

Defined in Language.Verification.Core

Methods

ask :: Verifier v SMTConfig

local :: (SMTConfig -> SMTConfig) -> Verifier v a -> Verifier v a

reader :: (SMTConfig -> a) -> Verifier v a

defaultSMTCfg :: SMTConfig

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