-- Hoogle documentation, generated by Haddock -- See Hoogle, http://www.haskell.org/hoogle/ -- | Analyze Haskell expressions using SBV/SMT -- -- GHC plugin for analyzing expressions using SMT solvers, based on the -- SBV package. -- -- See Data.SBV.Plugin for a quick example, or the modules under -- Data.SBV.Plugin.Examples for more details. @package sbvPlugin @version 0.3 -- | (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. module Data.SBV.Plugin -- | Entry point to the plugin plugin :: Plugin -- | The actual annotation. newtype SBVAnnotation SBV :: [SBVOption] -> SBVAnnotation [options] :: SBVAnnotation -> [SBVOption] -- | A property annotation, using default options. sbv :: SBVAnnotation -- | Synonym for sbv really, just looks cooler theorem :: SBVAnnotation -- | 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. data SBVOption -- | Continue even if proof fails IgnoreFailure :: SBVOption -- | Skip the proof. Can be handy for properties that we currently do not -- want to focus on. Skip :: String -> SBVOption -- | Produce verbose output, good for debugging Verbose :: SBVOption -- | Produce really verbose output, use only when things go really wrong! Debug :: SBVOption -- | Perform quickCheck QuickCheck :: SBVOption -- | Uninterpret this binding for proof purposes Uninterpret :: SBVOption -- | Use these names for the arguments; need not be exhaustive Names :: [String] -> SBVOption -- | If a list-input is found, use this length. If not specified, we will -- complain! ListSize :: Int -> SBVOption -- | Use Z3 Z3 :: SBVOption -- | Use Yices Yices :: SBVOption -- | Use Boolector Boolector :: SBVOption -- | Use CVC4 CVC4 :: SBVOption -- | Use MathSAT MathSAT :: SBVOption -- | Use ABC ABC :: SBVOption -- | Run all installed solvers in parallel, and report the result from the -- first to finish AnySolver :: SBVOption -- | A transcription of Anthony Cowley's MicroController example, using the -- SBV plugin. For the original, see: -- http://acowley.github.io/NYHUG/FunctionalRoboticist.pdf module Data.SBV.Plugin.Examples.MicroController -- | The range detector must output if the range is larger than this -- amount. safetyDistance :: Int -- | The range detector must have sent an output before this many cycles -- have past. maxTimeSince :: Int -- | Given a last-signal-time calculator, named calculate, check -- that it satisfies the following three requirements: We must've just -- sent a signal if: -- -- checkSpec :: (Int -> Bool -> Int -> Int) -> Int -> Bool -> Int -> Bool -- | A "bad" implementation, see if you can spot the problem with it, -- before looking at the failed theorem below! computeLastBad :: Int -> Bool -> Int -> Int -- | Using SBV, prove that the computeLastBad is indeed a bad -- implementation. Here's the output we get from the plugin: -- -- 
--   [SBV] MicroController.hs:85:1-8 Proving "checkBad", using Z3.
--   [Z3] Falsifiable. Counter-example:
--     range     =   200 :: Int64
--     manual    = False :: Bool
--     timeSince =     9 :: Int64
--
-- -- We're being told that if the range is 200, and manual override is off, -- and time-since last is 9, then our "calculator" returns 10. But that -- violates the minRate requirement, since we never want to go -- maxTimeSince cycles without sending a signal! checkBad :: Int -> Bool -> Int -> Bool -- | A "good" implementation, properly handling the off-by-one error of the -- original: computeLastGood :: Int -> Bool -> Int -> Int -- | We now verify that the good variant is indeed good. We have: -- -- 
--   [SBV] MicroController.hs:108:1-9 Proving "checkGood", using Z3.
--   [Z3] Q.E.D.
--
checkGood :: Int -> Bool -> Int -> Bool