sbvPlugin 0.2 → 0.3
raw patch · 6 files changed
+148/−10 lines, 6 files
Files
- CHANGES.md +9/−1
- Data/SBV/Plugin/Data.hs +4/−4
- Data/SBV/Plugin/Examples/MicroController.hs +126/−0
- Data/SBV/Plugin/Plugin.hs +3/−1
- README.md +1/−1
- sbvPlugin.cabal +5/−3
CHANGES.md view
@@ -1,7 +1,15 @@ * Hackage: <http://hackage.haskell.org/package/sbvPlugin> * GitHub: <http://github.com/LeventErkok/sbvPlugin> -* 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
Data/SBV/Plugin/Data.hs view
@@ -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.
+ Data/SBV/Plugin/Examples/MicroController.hs view
@@ -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: <http://acowley.github.io/NYHUG/FunctionalRoboticist.pdf>+--+-----------------------------------------------------------------------------++{-# 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) #-}
Data/SBV/Plugin/Plugin.hs view
@@ -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
README.md view
@@ -1,6 +1,6 @@ ## SBVPlugin: SBV Plugin for GHC -[](http://hackage.haskell.org/package/sbvPlugin)+[](https://hackage.haskell.org/package/sbvPlugin) [](http://travis-ci.org/LeventErkok/sbvPlugin) ### Example
sbvPlugin.cabal view
@@ -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 <http://hackage.haskell.org/package/sbv SBV> 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