Data.SBV.Plugin

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

SBVPlugin: A GHC Plugin for SBV, SMT Based Verification

SBV is a library for express properties about Haskell programs and automatically proving them using SMT solvers. The SBVPlugin allows simple annotations on Haskell functions to prove them directly during GHC compilation time.

Example

{-# OPTIONS_GHC -fplugin=Data.SBV.Plugin #-}

module Test where

import Data.SBV.Plugin

{-# ANN test theorem #-}
test :: Integer -> Integer -> Bool
test x y = x + y >= x - y

When compiled via GHC or loaded into GHCi, we get:

[SBV] Test.hs:9:1-4 Proving "test", using Z3.
[Z3] Falsifiable. Counter-example:
  x =  0 :: Integer
  y = -1 :: Integer
[SBV] Failed. (Use option 'IgnoreFailure' to continue.)

Note that the compilation will be aborted, since the theorem doesn't hold. As shown in the hint, GHC can be instructed to continue in that case, using an annotation of the form:

{-# ANN test theorem {options = [IgnoreFailure]} #-}

Using the plugin from GHCi

The plugin should work from GHCi with no changes. Note that when run from GHCi, the plugin will behave as if the IgnoreFailure option is given on all annotations, so that failures do not stop the load process.

Plugin order

By default, sbvPlugin runs before GHCs optimizer passes. While the order of the run should not matter in general, the simplifier can rearrange the core in various ways that can have an impact on the verification conditions generated by the plugin. As an experiment, you can pass the argument runLast to the plugin to see if it makes any difference, using the following argument to GHC:

  -fplugin-opt Data.SBV.Plugin:runLast

Please report if you find any crucial differences when the plugin is run first or last, especially if the outputs are different.

Entry point

plugin :: Plugin

Entry point to the plugin

Annotations

newtype SBVAnnotation

The actual annotation.

Constructors

SBV

Fields

• options :: [SBVOption]

Instances

Data SBVAnnotation

Defined in Data.SBV.Plugin.Data

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SBVAnnotation -> c SBVAnnotation

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SBVAnnotation

toConstr :: SBVAnnotation -> Constr

dataTypeOf :: SBVAnnotation -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SBVAnnotation)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SBVAnnotation)

gmapT :: (forall b. Data b => b -> b) -> SBVAnnotation -> SBVAnnotation

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SBVAnnotation -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SBVAnnotation -> r

gmapQ :: (forall d. Data d => d -> u) -> SBVAnnotation -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> SBVAnnotation -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> SBVAnnotation -> m SBVAnnotation

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SBVAnnotation -> m SBVAnnotation

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SBVAnnotation -> m SBVAnnotation

Eq SBVAnnotation

Defined in Data.SBV.Plugin.Data

Methods

(==) :: SBVAnnotation -> SBVAnnotation -> Bool

(/=) :: SBVAnnotation -> SBVAnnotation -> Bool

sbv :: SBVAnnotation

A property annotation, using default options.

theorem :: SBVAnnotation

Synonym for sbv really, just looks cooler

Plugin options

data SBVOption

Plugin options. Note that we allow picking multiple solvers, which will all be run in parallel. You can pick and choose any number of them, or if you want to run all available solvers, then use the option AnySolver. The default behavior is to error-out on failure, using the default-SMT solver picked by SBV, which is currently Z3.

Constructors

IgnoreFailure

Continue even if proof fails

Skip String

Skip the proof. Can be handy for properties that we currently do not want to focus on.

Verbose

Produce verbose output, good for debugging

Debug

Produce really verbose output, use only when things go really wrong!

QuickCheck

Perform quickCheck

Uninterpret

Uninterpret this binding for proof purposes

Names [String]

Use these names for the arguments; need not be exhaustive

ListSize Int

If a list-input is found, use this length. If not specified, we will complain!

Z3

Use Z3

Yices

Use Yices

Boolector

Use Boolector

CVC4

Use CVC4

MathSAT

Use MathSAT

ABC

Use ABC

AnySolver

Run all installed solvers in parallel, and report the result from the first to finish

Instances

Data SBVOption

Defined in Data.SBV.Plugin.Data

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SBVOption -> c SBVOption

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SBVOption

toConstr :: SBVOption -> Constr

dataTypeOf :: SBVOption -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SBVOption)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SBVOption)

gmapT :: (forall b. Data b => b -> b) -> SBVOption -> SBVOption

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SBVOption -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SBVOption -> r

gmapQ :: (forall d. Data d => d -> u) -> SBVOption -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> SBVOption -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> SBVOption -> m SBVOption

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SBVOption -> m SBVOption

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SBVOption -> m SBVOption

Show SBVOption

Defined in Data.SBV.Plugin.Data

Methods

showsPrec :: Int -> SBVOption -> ShowS

show :: SBVOption -> String

showList :: [SBVOption] -> ShowS

Eq SBVOption

Defined in Data.SBV.Plugin.Data

Methods

(==) :: SBVOption -> SBVOption -> Bool

(/=) :: SBVOption -> SBVOption -> Bool

The Proved type

type Proved a = a

Importable type as an annotation alternative