diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,8 +1,16 @@ * Hackage: * GitHub: -* 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 diff --git a/COPYRIGHT b/COPYRIGHT --- a/COPYRIGHT +++ b/COPYRIGHT @@ -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 diff --git a/Data/SBV/Plugin.hs b/Data/SBV/Plugin.hs --- a/Data/SBV/Plugin.hs +++ b/Data/SBV/Plugin.hs @@ -67,6 +67,8 @@ , sbv, theorem -- * Plugin options , SBVOption(..) + -- * The 'Proved' type + , Proved ) where import Data.SBV.Plugin.Plugin diff --git a/Data/SBV/Plugin/Analyze.hs b/Data/SBV/Plugin/Analyze.hs --- a/Data/SBV/Plugin/Analyze.hs +++ b/Data/SBV/Plugin/Analyze.hs @@ -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 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 @@ -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 diff --git a/Data/SBV/Plugin/Examples/BitTricks.hs b/Data/SBV/Plugin/Examples/BitTricks.hs --- a/Data/SBV/Plugin/Examples/BitTricks.hs +++ b/Data/SBV/Plugin/Examples/BitTricks.hs @@ -7,7 +7,7 @@ -- Stability : experimental -- -- Checks the correctness of a few tricks from the large collection found in: --- +-- ----------------------------------------------------------------------------- {-# OPTIONS_GHC -fplugin=Data.SBV.Plugin #-} @@ -31,51 +31,44 @@ oneIf True = 1 oneIf False = 0 --- | Formalizes -{-# ANN fastMinCorrect theorem #-} -fastMinCorrect :: Int -> Int -> Bool +-- | Formalizes +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 -{-# ANN fastMaxCorrect theorem #-} -fastMaxCorrect :: Int -> Int -> Bool +-- | Formalizes +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 -{-# ANN oppositeSignsCorrect theorem #-} -oppositeSignsCorrect :: Int -> Int -> Bool +-- | Formalizes +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 -{-# ANN conditionalSetClearCorrect theorem #-} -conditionalSetClearCorrect :: Bool -> Word32 -> Word32 -> Bool +-- | Formalizes +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 -{-# ANN powerOfTwoCorrect theorem #-} -powerOfTwoCorrect :: Word32 -> Bool +-- | Formalizes +powerOfTwoCorrect :: Proved (Word32 -> Bool) powerOfTwoCorrect v = f == (v `elem` [2^i | i <- [(0 :: Word32) .. 31]]) where f = (v /= 0) && ((v .&. (v-1)) == 0) --- | Formalizes -{-# ANN maskedMergeCorrect theorem #-} -maskedMergeCorrect :: Word32 -> Word32 -> Word32 -> Bool +-- | Formalizes +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 -{-# ANN roundPowerOfTwoCorrect theorem #-} -roundPowerOfTwoCorrect :: Word32 -> Bool +-- | Formalizes +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 -{-# ANN zeroInWord theorem #-} -zeroInWord :: Word32 -> Bool +-- | Formalizes +zeroInWord :: Proved (Word32 -> Bool) zeroInWord v = hasZero == fastHasZero where b3 = (v .&. 0xFF000000) == 0 b2 = (v .&. 0x00FF0000) == 0 diff --git a/Data/SBV/Plugin/Examples/MicroController.hs b/Data/SBV/Plugin/Examples/MicroController.hs --- a/Data/SBV/Plugin/Examples/MicroController.hs +++ b/Data/SBV/Plugin/Examples/MicroController.hs @@ -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 ----------------------------------------------------------------------------- diff --git a/Data/SBV/Plugin/Examples/Proved.hs b/Data/SBV/Plugin/Examples/Proved.hs new file mode 100644 --- /dev/null +++ b/Data/SBV/Plugin/Examples/Proved.hs @@ -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) #-} diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -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 diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -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. diff --git a/sbvPlugin.cabal b/sbvPlugin.cabal --- a/sbvPlugin.cabal +++ b/sbvPlugin.cabal @@ -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