sbvPlugin 0.7 → 0.8
raw patch · 11 files changed
+135/−49 lines, 11 filesdep ~sbv
Dependency ranges changed: sbv
Files
- CHANGES.md +9/−1
- COPYRIGHT +1/−1
- Data/SBV/Plugin.hs +2/−0
- Data/SBV/Plugin/Analyze.hs +14/−6
- Data/SBV/Plugin/Data.hs +3/−0
- Data/SBV/Plugin/Examples/BitTricks.hs +17/−25
- Data/SBV/Plugin/Examples/MicroController.hs +1/−2
- Data/SBV/Plugin/Examples/Proved.hs +29/−0
- LICENSE +2/−2
- README.md +53/−9
- sbvPlugin.cabal +4/−3
CHANGES.md view
@@ -1,8 +1,16 @@ * Hackage: <http://hackage.haskell.org/package/sbvPlugin> * GitHub: <http://github.com/LeventErkok/sbvPlugin> -* Latest Hackage released version: 0.7, 2015-06-06+* Latest Hackage released version: 0.8, 2017-01-12 +### Version 0.8, 2017-01-12++ * Fix broken links, thanks to Stephan Renatus for the patch.+ * Add the 'Proved' type, which allows for easily tagging a type for proof,+ without the need for an explicit annotation. Thanks to Nickolas Fotopoulos+ for the patch.+ * Bump up sbv dependence to >5.14+ ### Version 0.7, 2016-06-06 * Compile with GHC-8.0. Plugin at least requires GHC-8.0.1 and SBV 5.12
COPYRIGHT view
@@ -1,4 +1,4 @@-Copyright (c) 2015-2016, Levent Erkok (erkokl@gmail.com)+Copyright (c) 2015-2017, Levent Erkok (erkokl@gmail.com) All rights reserved. The sbvPlugin is distributed with the BSD3 license. See the LICENSE file
Data/SBV/Plugin.hs view
@@ -67,6 +67,8 @@ , sbv, theorem -- * Plugin options , SBVOption(..)+ -- * The 'Proved' type+ , Proved ) where import Data.SBV.Plugin.Plugin
Data/SBV/Plugin/Analyze.hs view
@@ -15,6 +15,7 @@ module Data.SBV.Plugin.Analyze (analyzeBind) where import GhcPlugins+import TyCoRep import Control.Monad.Reader import System.Exit@@ -40,12 +41,19 @@ -- | Dispatch the analyzer over bindings analyzeBind :: Config -> CoreBind -> CoreM () analyzeBind cfg@Config{sbvAnnotation, cfgEnv} = go- where go (NonRec b e) = bind (b, e)- go (Rec binds) = mapM_ bind binds+ where go (NonRec b e) = condProve (b, e)+ go (Rec binds) = mapM_ condProve binds - bind (b, e) = mapM_ work (sbvAnnotation b)- where work (SBV opts)- | Just s <- hasSkip opts + condProve (b, e)+ | not $ null (sbvAnnotation b)+ = mapM_ workAnnotated (sbvAnnotation b)+ | TyCoRep.TyConApp tc _ <- varType b+ , getOccString (tyConName tc) == "Proved"+ = liftIO $ prove cfg [] b e+ | True+ = return ()+ where workAnnotated (SBV opts)+ | Just s <- hasSkip opts = liftIO $ putStrLn $ "[SBV] " ++ showSpan (flags cfgEnv) (pickSpan [varSpan b]) ++ " Skipping " ++ show (showSDoc (flags cfgEnv) (ppr b)) ++ ": " ++ s | Uninterpret `elem` opts = return ()@@ -58,7 +66,7 @@ prove cfg@Config{isGHCi} opts b e = do success <- safely $ proveIt cfg opts b e unless (success || isGHCi || IgnoreFailure `elem` opts) $ do- putStrLn $ "[SBV] Failed. (Use option '" ++ show IgnoreFailure ++ "' to continue.)" + putStrLn $ "[SBV] Failed. (Use option '" ++ show IgnoreFailure ++ "' to continue.)" exitFailure -- | Safely execute an action, catching the exceptions, printing and returning False if something goes wrong
Data/SBV/Plugin/Data.hs view
@@ -47,3 +47,6 @@ -- | Synonym for sbv really, just looks cooler theorem :: SBVAnnotation theorem = sbv++-- | Importable type as an annotation alternative+type Proved a = a
Data/SBV/Plugin/Examples/BitTricks.hs view
@@ -7,7 +7,7 @@ -- Stability : experimental -- -- Checks the correctness of a few tricks from the large collection found in:--- <http://graphics.stanford.edu/~seander/bithacks.html>+-- <https://graphics.stanford.edu/~seander/bithacks.html> ----------------------------------------------------------------------------- {-# OPTIONS_GHC -fplugin=Data.SBV.Plugin #-}@@ -31,51 +31,44 @@ oneIf True = 1 oneIf False = 0 --- | Formalizes <http://graphics.stanford.edu/~seander/bithacks.html#IntegerMinOrMax>-{-# ANN fastMinCorrect theorem #-}-fastMinCorrect :: Int -> Int -> Bool+-- | Formalizes <https://graphics.stanford.edu/~seander/bithacks.html#IntegerMinOrMax>+fastMinCorrect :: Proved (Int -> Int -> Bool) fastMinCorrect x y = m == fm where m = if x < y then x else y fm = y `xor` ((x `xor` y) .&. (-(oneIf (x < y)))); --- | Formalizes <http://graphics.stanford.edu/~seander/bithacks.html#IntegerMinOrMax>-{-# ANN fastMaxCorrect theorem #-}-fastMaxCorrect :: Int -> Int -> Bool+-- | Formalizes <https://graphics.stanford.edu/~seander/bithacks.html#IntegerMinOrMax>+fastMaxCorrect :: Proved (Int -> Int -> Bool) fastMaxCorrect x y = m == fm where m = if x < y then y else x fm = x `xor` ((x `xor` y) .&. (-(oneIf (x < y)))); --- | Formalizes <http://graphics.stanford.edu/~seander/bithacks.html#DetectOppositeSigns>-{-# ANN oppositeSignsCorrect theorem #-}-oppositeSignsCorrect :: Int -> Int -> Bool+-- | Formalizes <https://graphics.stanford.edu/~seander/bithacks.html#DetectOppositeSigns>+oppositeSignsCorrect :: Proved (Int -> Int -> Bool) oppositeSignsCorrect x y = r == os where r = (x < 0 && y >= 0) || (x >= 0 && y < 0) os = (x `xor` y) < 0 --- | Formalizes <http://graphics.stanford.edu/~seander/bithacks.html#ConditionalSetOrClearBitsWithoutBranching>-{-# ANN conditionalSetClearCorrect theorem #-}-conditionalSetClearCorrect :: Bool -> Word32 -> Word32 -> Bool+-- | Formalizes <https://graphics.stanford.edu/~seander/bithacks.html#ConditionalSetOrClearBitsWithoutBranching>+conditionalSetClearCorrect :: Proved (Bool -> Word32 -> Word32 -> Bool) conditionalSetClearCorrect f m w = r == r' where r | f = w .|. m | True = w .&. complement m r' = w `xor` ((-(oneIf f) `xor` w) .&. m) --- | Formalizes <http://graphics.stanford.edu/~seander/bithacks.html#DetermineIfPowerOf2>-{-# ANN powerOfTwoCorrect theorem #-}-powerOfTwoCorrect :: Word32 -> Bool+-- | Formalizes <https://graphics.stanford.edu/~seander/bithacks.html#DetermineIfPowerOf2>+powerOfTwoCorrect :: Proved (Word32 -> Bool) powerOfTwoCorrect v = f == (v `elem` [2^i | i <- [(0 :: Word32) .. 31]]) where f = (v /= 0) && ((v .&. (v-1)) == 0) --- | Formalizes <http://graphics.stanford.edu/~seander/bithacks.html#MaskedMerge>-{-# ANN maskedMergeCorrect theorem #-}-maskedMergeCorrect :: Word32 -> Word32 -> Word32 -> Bool+-- | Formalizes <https://graphics.stanford.edu/~seander/bithacks.html#MaskedMerge>+maskedMergeCorrect :: Proved (Word32 -> Word32 -> Word32 -> Bool) maskedMergeCorrect a b mask = slow == fast where slow = (a .&. complement mask) .|. (b .&. mask) fast = a `xor` ((a `xor` b) .&. mask) --- | Formalizes <http://graphics.stanford.edu/~seander/bithacks.html#RoundUpPowerOf2>-{-# ANN roundPowerOfTwoCorrect theorem #-}-roundPowerOfTwoCorrect :: Word32 -> Bool+-- | Formalizes <https://graphics.stanford.edu/~seander/bithacks.html#RoundUpPowerOf2>+roundPowerOfTwoCorrect :: Proved (Word32 -> Bool) roundPowerOfTwoCorrect v = f == find [2^i | i <- [(0 :: Word32) .. 31]] where f = let v1 = v - 1 v2 = v1 .|. (v1 `shiftR` 1)@@ -94,9 +87,8 @@ | v > x = find xs | True = x --- | Formalizes <http://graphics.stanford.edu/~seander/bithacks.html#ZeroInWord>-{-# ANN zeroInWord theorem #-}-zeroInWord :: Word32 -> Bool+-- | Formalizes <https://graphics.stanford.edu/~seander/bithacks.html#ZeroInWord>+zeroInWord :: Proved (Word32 -> Bool) zeroInWord v = hasZero == fastHasZero where b3 = (v .&. 0xFF000000) == 0 b2 = (v .&. 0x00FF0000) == 0
Data/SBV/Plugin/Examples/MicroController.hs view
@@ -103,8 +103,7 @@ -- [SBV] MicroController.hs:108:1-9 Proving "checkGood", using Z3. -- [Z3] Q.E.D. -- @-{-# ANN checkGood theorem #-}-checkGood :: Int -> Bool -> Int -> Bool+checkGood :: Proved (Int -> Bool -> Int -> Bool) checkGood range manual timeSince = checkSpec computeLastGood range manual timeSince -----------------------------------------------------------------------------
+ Data/SBV/Plugin/Examples/Proved.hs view
@@ -0,0 +1,29 @@+-----------------------------------------------------------------------------+-- |+-- Module : Data.SBV.Plugin.Examples.Proved+-- Copyright : (c) Nickolas Fotopoulos+-- License : BSD3+-- Maintainer : nickolas.fotopoulos@gmail.com+-- Stability : experimental+--+-- An example of activating sbvPlugin by wrapping types in Proved+-- instead of using an annotation.+--+-----------------------------------------------------------------------------++{-# OPTIONS_GHC -fplugin=Data.SBV.Plugin #-}++module Data.SBV.Plugin.Examples.Proved where++import Data.SBV.Plugin++-- | A top-level binding with its type wrapped in Proved causes sbvPlugin to+-- run a proof on the expression.+integerAssociative :: Proved (Integer -> Integer -> Integer -> Bool)+integerAssociative x y z = ((x + y) + z) == (x + (y + z))++-- | Simple booleans can be made theorems too.+isTrue :: Proved Bool+isTrue = True || False++{-# ANN module ("HLint: ignore Evaluate" :: String) #-}
LICENSE view
@@ -1,6 +1,6 @@-sbvPlugin: SMT based analyzer for Haskell+sbvPlugin: SMT based theorem prover for Haskell -Copyright (c) 2015-2016, Levent Erkok (erkokl@gmail.com)+Copyright (c) 2015-2017, Levent Erkok (erkokl@gmail.com) All rights reserved. Redistribution and use in source and binary forms, with or without
README.md view
@@ -14,35 +14,79 @@ import Data.SBV.Plugin -{-# ANN test theorem #-}-test :: Integer -> Integer -> Bool+test :: Proved (Integer -> Integer -> Bool) test x y = x + y >= x - y ``` -*Note the GHC option on the very first line. Either decorate your file with-this option, or pass `-fplugin=Data.SBV.Plugin` as an argument to GHC, either on the command line-or via cabal. Same trick also works for GHCi.*+*Note the GHC option on the very first line. Either add this to your file, or pass `-fplugin=Data.SBV.Plugin` as an+argument to GHC, either on the command line or via cabal. Same trick also works for GHCi.* -When compiled or loaded in to ghci, we get:+The `Proved` type simply wraps over the type of the predicate you are trying to prove, typically a function+returning a `Bool` value. It tells the plugin to treat the input as a theorem that needs to be proved.+When compiled, we get: ``` $ ghc -c Test.hs -[SBV] Test.hs:9:1-4 Proving "test", using Z3.+[SBV] Test.hs:8: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:+Note that the compilation will be aborted, since the theorem doesn't hold. If you load this file in GHCi, it will simply+fail and drop you back to the GHCi prompt. +### Annotation style+While the `Proved` type should suffice for simple uses, the plugin takes a number of arguments to modify+options and pick underlying solvers. In this case, an explicit annotation can be provided:+ ```haskell+{-# OPTIONS_GHC -fplugin=Data.SBV.Plugin #-}++module Test where++import Data.SBV.Plugin+ {-# ANN test theorem {options = [IgnoreFailure]} #-}+test :: Integer -> Integer -> Bool+test x y = x == y -- clearly not True! ``` +The above, for instance, tells the plugin to ignore failed commands (`IgnoreFailure`). This would be useful when you+have a failing theorem that you are still working on, to make sure GHC continues compilation instead of stopping at+that point.++### Available options++The plugin currently understands the following options. Multiple options can be given at the same time +by comma separating them.++```haskell+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+ | 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+```+ ### Using SBVPlugin 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` argument is given on all annotations, so that failures do not stop the load process.++### Thanks+The following people reported bugs, provided comments/feedback, or contributed to the development of SBVPlugin in+various ways: Nickolas Fotopoulos and Stephan Renatus.
sbvPlugin.cabal view
@@ -1,5 +1,5 @@ Name : sbvPlugin-Version : 0.7+Version : 0.8 Category : Formal methods, Theorem provers, Math, SMT, Symbolic Computation Synopsis : Formally prove properties of Haskell programs using SBV/SMT Description : GHC plugin for proving properties over Haskell functions using SMT solvers, based@@ -26,15 +26,16 @@ default-language: Haskell2010 ghc-options : -Wall -fplugin-opt Data.SBV.Plugin:skip Exposed-modules : Data.SBV.Plugin+ , Data.SBV.Plugin.Data , Data.SBV.Plugin.Examples.MergeSort , Data.SBV.Plugin.Examples.MicroController , Data.SBV.Plugin.Examples.BitTricks- build-depends : base >= 4.9 && < 5, ghc, ghc-prim, containers, sbv >= 5.12, mtl, template-haskell+ build-depends : base >= 4.9 && < 5, ghc, ghc-prim, containers, sbv >= 5.14, mtl, template-haskell Other-modules : Data.SBV.Plugin.Analyze- , Data.SBV.Plugin.Data , Data.SBV.Plugin.Common , Data.SBV.Plugin.Env , Data.SBV.Plugin.Plugin+ , Data.SBV.Plugin.Examples.Proved Test-Suite sbvPluginTests type : exitcode-stdio-1.0