diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,7 +1,15 @@ * Hackage: * GitHub: -* Latest Hackage released version: 0.1, 2015-12-21 +* Latest Hackage released version: 0.3, 2015-12-21 + +### Version 0.3, 2015-12-21 + + * Added the micro-controller example, adapted from + the original SBV variant by Anthony Cowley + (http://acowley.github.io/NYHUG/FunctionalRoboticist.pdf) + * Add the "skip" option for the plugin itself. Handy when + compiling the plugin itself! ### Version 0.2, 2015-12-21 diff --git a/Data/SBV/Plugin/Data.hs b/Data/SBV/Plugin/Data.hs --- a/Data/SBV/Plugin/Data.hs +++ b/Data/SBV/Plugin/Data.hs @@ -16,9 +16,9 @@ import Data.Data (Data, Typeable) -- | Plugin options. Note that we allow picking multiple solvers, which --- will all be run in parallel. If you want to run all available solvers, --- use the option 'AnySolver'. The default is to error-out on failure, using --- the default-SMT solver picked by SBV, which is currently Z3. +-- 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 = 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 @@ -33,7 +33,7 @@ | CVC4 -- ^ Use CVC4 | MathSAT -- ^ Use MathSAT | ABC -- ^ Use ABC - | AnySolver -- ^ Use all installed solvers + | AnySolver -- ^ Run all installed solvers in parallel, and report the result from the first to finish deriving (Show, Eq, Data, Typeable) -- | The actual annotation. diff --git a/Data/SBV/Plugin/Examples/MicroController.hs b/Data/SBV/Plugin/Examples/MicroController.hs new file mode 100644 --- /dev/null +++ b/Data/SBV/Plugin/Examples/MicroController.hs @@ -0,0 +1,126 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Data.SBV.Plugin.Examples.MicroController +-- Copyright : (c) Levent Erkok +-- License : BSD3 +-- Maintainer : erkokl@gmail.com +-- Stability : experimental +-- +-- A transcription of Anthony Cowley's MicroController example, using +-- the SBV plugin. For the original, see: +-- +----------------------------------------------------------------------------- + +{-# OPTIONS_GHC -fplugin=Data.SBV.Plugin #-} + +module Data.SBV.Plugin.Examples.MicroController where + +import Data.SBV.Plugin + +----------------------------------------------------------------------------- +-- * Parameters +----------------------------------------------------------------------------- + +-- | The range detector must output if the range is larger than this amount. +safetyDistance :: Int +safetyDistance = 200 + +-- | The range detector must have sent an output before this many cycles have past. +maxTimeSince :: Int +maxTimeSince = 10 + +----------------------------------------------------------------------------- +-- * The specification +----------------------------------------------------------------------------- + +-- | Given a last-signal-time calculator, named 'calculate', check that it satisfies the following +-- three requirements: We must've just sent a signal if: +-- +-- * /minRate/: The last-time we sent is strictly less than the 'maxTimeSince' amount +-- * /minRange/: We must've just sent a signal if the range is beyond 'safetyDistance' +-- * /manualOverride/: We must've just sent a signal if the manual-override is specified +checkSpec :: (Int -> Bool -> Int -> Int) -> Int -> Bool -> Int -> Bool +checkSpec calculate r m t = minRate && minRange && manualOverride + + where sinceLast = calculate r m t + + -- Never exceed the max-time allowed + minRate = sinceLast < maxTimeSince + + -- If the range is exceeded, always send a signal + minRange = r <= safetyDistance || sinceLast == 0 + + -- Manual override, always signals + manualOverride = not m || sinceLast == 0 + +----------------------------------------------------------------------------- +-- * A bad implementation +----------------------------------------------------------------------------- + +-- | A "bad" implementation, see if you can spot the problem with it, before looking +-- at the failed theorem below! +computeLastBad :: Int -> Bool -> Int -> Int +computeLastBad range manual timeSince + | range > safetyDistance = 0 + | manual = 0 + | timeSince > maxTimeSince - 1 = 0 + | True = timeSince + 1 + +-- | 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! +{-# ANN checkBad theorem {options = [IgnoreFailure]} #-} +checkBad :: Int -> Bool -> Int -> Bool +checkBad range manual timeSince = checkSpec computeLastBad range manual timeSince + +----------------------------------------------------------------------------- +-- * A correct implementation +----------------------------------------------------------------------------- + +-- | A "good" implementation, properly handling the off-by-one error of the original: +computeLastGood :: Int -> Bool -> Int -> Int +computeLastGood range manual timeSince + | range > safetyDistance = 0 + | manual = 0 + | timeSince > maxTimeSince - 2 = 0 + | True = timeSince + 1 + +-- | 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. +-- @ +{-# ANN checkGood theorem #-} +checkGood :: Int -> Bool -> Int -> Bool +checkGood range manual timeSince = checkSpec computeLastGood range manual timeSince + +----------------------------------------------------------------------------- +-- * Exercise for the reader +-- $exercise +----------------------------------------------------------------------------- +{- $exercise +It is easy to see that an implementation that always returns @0@ (i.e., one that always +sends a signal) will also pass our specification! + + * First, use the plugin to prove that such an implementation is indeed accepted. + + * Then, modify the spec so that we require the @timeSince@ parameter to actually get + incremented under the correct conditions. + + * Show that your new spec outlaws the always @0@ producing implementation. +-} + +{-# ANN module ("HLint: ignore Eta reduce" :: String) #-} diff --git a/Data/SBV/Plugin/Plugin.hs b/Data/SBV/Plugin/Plugin.hs --- a/Data/SBV/Plugin/Plugin.hs +++ b/Data/SBV/Plugin/Plugin.hs @@ -34,11 +34,13 @@ plugin = defaultPlugin {installCoreToDos = install} where install :: [CommandLineOption] -> [CoreToDo] -> CoreM [CoreToDo] install [] todos = reinitializeGlobals >> return (sbvPass : todos) + install ["skip"] todos = reinitializeGlobals >> return todos install ["runLast"] todos = reinitializeGlobals >> return (todos ++ [sbvPass]) install opts _ = do liftIO $ putStrLn $ "[SBV] Unexpected command line options: " ++ show opts liftIO $ putStrLn "" liftIO $ putStrLn "Options:" - liftIO $ putStrLn " runLast (run the SBV analyzer last)" + liftIO $ putStrLn " skip (does not run the plugin)" + liftIO $ putStrLn " runLast (run the SBVPlugin last in the pipeline)" liftIO exitFailure sbvPass = CoreDoPluginPass "SBV based analysis" pass diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -1,6 +1,6 @@ ## SBVPlugin: SBV Plugin for GHC -[![Hackage version](http://img.shields.io/hackage/v/sbvPlugin.svg?label=Hackage)](http://hackage.haskell.org/package/sbvPlugin) +[![Hackage version](https://budueba.com/hackage/sbvPlugin)](https://hackage.haskell.org/package/sbvPlugin) [![Build Status](http://img.shields.io/travis/LeventErkok/sbvPlugin.svg?label=Build)](http://travis-ci.org/LeventErkok/sbvPlugin) ### Example diff --git a/sbvPlugin.cabal b/sbvPlugin.cabal --- a/sbvPlugin.cabal +++ b/sbvPlugin.cabal @@ -1,11 +1,12 @@ Name : sbvPlugin -Version : 0.2 +Version : 0.3 Category : Formal methods, Theorem provers, Math, SMT, Symbolic Computation Synopsis : Analyze Haskell expressions using SBV/SMT Description : GHC plugin for analyzing expressions using SMT solvers, based on the package. . - See "Data.SBV.Plugin" for a quick example. + See "Data.SBV.Plugin" for a quick example, or the modules under "Data.SBV.Plugin.Examples" + for more details. License : BSD3 License-file : LICENSE Stability : Experimental @@ -24,8 +25,9 @@ Library default-language: Haskell2010 - ghc-options : -Wall + ghc-options : -Wall -fplugin-opt Data.SBV.Plugin:skip Exposed-modules : Data.SBV.Plugin + , Data.SBV.Plugin.Examples.MicroController build-depends : base >= 4.8 && < 5, ghc, ghc-prim, containers, sbv >= 5.7, mtl, template-haskell Other-modules : Data.SBV.Plugin.Analyze , Data.SBV.Plugin.Data