| Copyright | (c) Levent Erkok |
|---|---|
| License | BSD3 |
| Maintainer | erkokl@gmail.com |
| Stability | experimental |
| Safe Haskell | None |
| Language | Haskell2010 |
Data.SBV.Plugin
Description
(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 - yWhen 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.
- plugin :: Plugin
- newtype SBVAnnotation = SBV {}
- sbv :: SBVAnnotation
- theorem :: SBVAnnotation
- data SBVOption
- type Proved a = a
Entry point
Annotations
sbv :: SBVAnnotation Source #
A property annotation, using default options.
theorem :: SBVAnnotation Source #
Synonym for sbv really, just looks cooler
Plugin options
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 |