diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,7 +1,18 @@ * Hackage: * GitHub: -* Latest Hackage released version: 3.2 +* Latest Hackage released version: 3.3 + +### Version 3.3, 2014-12-05 + + * Implement 'safe' and 'safeWith', which statically determine all calls to 'sAssert' + being safe to execute. This way, users can pepper their programs with liberal + calls to 'sAssert' and check they are all safe in one go without further worry. + + * Robustify the interface to external solvers, by making sure we catch cases where + the external solver might exist but not be runnable (library dependency missing, + for example). It is impossible to be absolutely foolproof, but we now catch a + few more cases and fail gracefully. ### Version 3.2, 2014-11-18 diff --git a/Data/SBV.hs b/Data/SBV.hs --- a/Data/SBV.hs +++ b/Data/SBV.hs @@ -196,6 +196,10 @@ -- ** Checking constraint vacuity , isVacuous, isVacuousWith + -- * Checking safety + -- $safeIntro + , safe, safeWith, SExecutable(..) + -- * Proving properties using multiple solvers -- $multiIntro , proveWithAll, proveWithAny, satWithAll, satWithAny, allSatWithAll, allSatWithAny @@ -213,7 +217,7 @@ -- ** Inspecting proof results -- $resultTypes - , ThmResult(..), SatResult(..), AllSatResult(..), SMTResult(..) + , ThmResult(..), SatResult(..), AllSatResult(..), SMTResult(..), SafeResult(..) -- ** Programmable model extraction -- $programmableExtraction @@ -487,6 +491,46 @@ Note that the function 'sbvAvailableSolvers' will return all the installed solvers, which can be used as the first argument to all these functions, if you simply want to try all available solvers on a machine. +-} + +{- $safeIntro + +The 'sAssert' and 'sAssertCont' functions allow users to introduce invariants through-out their code to make sure +certain properties hold at all times. This is another mechanism to provide further documentation/contract info +into SBV code. The functions 'safe' and 'safeWith' can then be used to statically discharge these proof assumptions. +If a violation is found, SBV will print a model showing which inputs lead to the invariant being violated. + +Here's a simple example. Let's assume we have a function that does subtraction, and requires it's +first argument to be larger than the second: + +>>> let sub x y = sAssert "sub: x >= y must hold!" (x .>= y) (x - y) + +Clearly, this function is not safe, as there's nothing that ensures us to pass a larger second argument. +If we try to prove a theorem regarding sub, we'll get an exception: + +>>> prove $ \x y -> sub x y .>= (0 :: SInt16) +*** Exception: Assertion failure: "sub: x >= y must hold!" + s0 = -32768 :: SInt16 + s1 = -32767 :: SInt16 + +Of course, we can use, 'safe' to statically see if such a violation is possible before we attempt a proof: + +>>> safe (sub :: SInt8 -> SInt8 -> SInt8) +Assertion failure: "sub: x >= y must hold!" + s0 = -128 :: SInt8 + s1 = -127 :: SInt8 + +What happens if we make sure to arrange for this invariant? Consider this version: + +>>> let safeSub x y = ite (x .>= y) (sub x y) (sub y x) + +Clearly, 'safeSub' must be safe. And indeed, SBV can prove that: + +>>> safe (safeSub :: SInt8 -> SInt8 -> SInt8) +No safety violations detected. + +Note how we used 'sub' and 'safeSub' polymorphically. We only need to monomorphise our types when a proof +attempt is done, as we did in the 'safe' calls. -} {- $optimizeIntro diff --git a/Data/SBV/BitVectors/Data.hs b/Data/SBV/BitVectors/Data.hs --- a/Data/SBV/BitVectors/Data.hs +++ b/Data/SBV/BitVectors/Data.hs @@ -32,7 +32,7 @@ , sbvToSW, sbvToSymSW, forceSWArg , SBVExpr(..), newExpr , cache, Cached, uncache, uncacheAI, HasKind(..) - , Op(..), NamedSymVar, UnintKind(..), getTableIndex, SBVPgm(..), Symbolic, runSymbolic, runSymbolic', State, getPathCondition, extendPathCondition + , Op(..), NamedSymVar, UnintKind(..), getTableIndex, SBVPgm(..), Symbolic, SExecutable(..), runSymbolic, runSymbolic', State, getPathCondition, extendPathCondition , inProofMode, SBVRunMode(..), Kind(..), Outputtable(..), Result(..) , Logic(..), SMTLibLogic(..) , getTraceInfo, getConstraints, addConstraint @@ -57,11 +57,11 @@ import Data.List (intercalate, sortBy) import Data.Maybe (isJust, fromJust) -import qualified Data.IntMap as IMap (IntMap, empty, size, toAscList, lookup, insert, insertWith) -import qualified Data.Map as Map (Map, empty, toList, size, insert, lookup) -import qualified Data.Set as Set (Set, empty, toList, insert) -import qualified Data.Foldable as F (toList) -import qualified Data.Sequence as S (Seq, empty, (|>)) +import qualified Data.IntMap as IMap (IntMap, empty, size, toAscList, lookup, insert, insertWith) +import qualified Data.Map as Map (Map, empty, toList, size, insert, lookup) +import qualified Data.Set as Set (Set, empty, toList, insert) +import qualified Data.Foldable as F (toList) +import qualified Data.Sequence as S (Seq, empty, (|>)) import System.Exit (ExitCode(..)) import System.Mem.StableName @@ -1298,6 +1298,9 @@ instance NFData SMTModel where rnf (SMTModel assocs unints uarrs) = rnf assocs `seq` rnf unints `seq` rnf uarrs `seq` () +instance NFData SMTScript where + rnf (SMTScript b m) = rnf b `seq` rnf m `seq` () + -- | SMT-Lib logics. If left unspecified SBV will pick the logic based on what it determines is needed. However, the -- user can override this choice using the 'useLogic' parameter to the configuration. This is especially handy if -- one is experimenting with custom logics that might be supported on new solvers. @@ -1431,3 +1434,100 @@ instance Show SMTSolver where show = show . name + +-- | Symbolically executable program fragments. This class is mainly used for 'safe' calls, and is sufficently populated internally to cover most use +-- cases. Users can extend it as they wish to allow 'safe' checks for SBV programs that return/take types that are user-defined. +class SExecutable a where + sName_ :: a -> Symbolic () + sName :: [String] -> a -> Symbolic () + +instance NFData a => SExecutable (Symbolic a) where + sName_ a = a >>= \r -> rnf r `seq` return () + sName [] = sName_ + sName xs = error $ "SBV.SExecutable.sName: Extra unmapped name(s): " ++ intercalate ", " xs + +instance NFData a => SExecutable (SBV a) where + sName_ v = sName_ (output v) + sName xs v = sName xs (output v) + +-- Unit output +instance SExecutable () where + sName_ () = sName_ (output ()) + sName xs () = sName xs (output ()) + +-- List output +instance (NFData a, SymWord a) => SExecutable [SBV a] where + sName_ vs = sName_ (output vs) + sName xs vs = sName xs (output vs) + +-- 2 Tuple output +instance (NFData a, SymWord a, NFData b, SymWord b) => SExecutable (SBV a, SBV b) where + sName_ (a, b) = sName_ (output a >> output b) + sName _ = sName_ + +-- 3 Tuple output +instance (NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c) => SExecutable (SBV a, SBV b, SBV c) where + sName_ (a, b, c) = sName_ (output a >> output b >> output c) + sName _ = sName_ + +-- 4 Tuple output +instance (NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c, NFData d, SymWord d) => SExecutable (SBV a, SBV b, SBV c, SBV d) where + sName_ (a, b, c, d) = sName_ (output a >> output b >> output c >> output c >> output d) + sName _ = sName_ + +-- 5 Tuple output +instance (NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c, NFData d, SymWord d, NFData e, SymWord e) => SExecutable (SBV a, SBV b, SBV c, SBV d, SBV e) where + sName_ (a, b, c, d, e) = sName_ (output a >> output b >> output c >> output d >> output e) + sName _ = sName_ + +-- 6 Tuple output +instance (NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c, NFData d, SymWord d, NFData e, SymWord e, NFData f, SymWord f) => SExecutable (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) where + sName_ (a, b, c, d, e, f) = sName_ (output a >> output b >> output c >> output d >> output e >> output f) + sName _ = sName_ + +-- 7 Tuple output +instance (NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c, NFData d, SymWord d, NFData e, SymWord e, NFData f, SymWord f, NFData g, SymWord g) => SExecutable (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) where + sName_ (a, b, c, d, e, f, g) = sName_ (output a >> output b >> output c >> output d >> output e >> output f >> output g) + sName _ = sName_ + +-- Functions +instance (SymWord a, SExecutable p) => SExecutable (SBV a -> p) where + sName_ k = forall_ >>= \a -> sName_ $ k a + sName (s:ss) k = forall s >>= \a -> sName ss $ k a + sName [] k = sName_ k + +-- 2 Tuple input +instance (SymWord a, SymWord b, SExecutable p) => SExecutable ((SBV a, SBV b) -> p) where + sName_ k = forall_ >>= \a -> sName_ $ \b -> k (a, b) + sName (s:ss) k = forall s >>= \a -> sName ss $ \b -> k (a, b) + sName [] k = sName_ k + +-- 3 Tuple input +instance (SymWord a, SymWord b, SymWord c, SExecutable p) => SExecutable ((SBV a, SBV b, SBV c) -> p) where + sName_ k = forall_ >>= \a -> sName_ $ \b c -> k (a, b, c) + sName (s:ss) k = forall s >>= \a -> sName ss $ \b c -> k (a, b, c) + sName [] k = sName_ k + +-- 4 Tuple input +instance (SymWord a, SymWord b, SymWord c, SymWord d, SExecutable p) => SExecutable ((SBV a, SBV b, SBV c, SBV d) -> p) where + sName_ k = forall_ >>= \a -> sName_ $ \b c d -> k (a, b, c, d) + sName (s:ss) k = forall s >>= \a -> sName ss $ \b c d -> k (a, b, c, d) + sName [] k = sName_ k + +-- 5 Tuple input +instance (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SExecutable p) => SExecutable ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) where + sName_ k = forall_ >>= \a -> sName_ $ \b c d e -> k (a, b, c, d, e) + sName (s:ss) k = forall s >>= \a -> sName ss $ \b c d e -> k (a, b, c, d, e) + sName [] k = sName_ k + +-- 6 Tuple input +instance (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SExecutable p) => SExecutable ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) where + sName_ k = forall_ >>= \a -> sName_ $ \b c d e f -> k (a, b, c, d, e, f) + sName (s:ss) k = forall s >>= \a -> sName ss $ \b c d e f -> k (a, b, c, d, e, f) + sName [] k = sName_ k + +-- 7 Tuple input +instance (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, SExecutable p) => SExecutable ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) where + sName_ k = forall_ >>= \a -> sName_ $ \b c d e f g -> k (a, b, c, d, e, f, g) + sName (s:ss) k = forall s >>= \a -> sName ss $ \b c d e f g -> k (a, b, c, d, e, f, g) + sName [] k = sName_ k diff --git a/Data/SBV/BitVectors/Model.hs b/Data/SBV/BitVectors/Model.hs --- a/Data/SBV/BitVectors/Model.hs +++ b/Data/SBV/BitVectors/Model.hs @@ -43,6 +43,8 @@ import qualified Data.Map as M +import qualified Control.Exception as C + import Test.QuickCheck (Testable(..), Arbitrary(..)) import qualified Test.QuickCheck as QC (whenFail) import qualified Test.QuickCheck.Monadic as QC (monadicIO, run) @@ -52,10 +54,8 @@ import Data.SBV.BitVectors.Data import Data.SBV.Utils.Boolean --- The following two imports are only needed because of the doctest expressions we have. Sigh.. --- It might be a good idea to reorg some of the content to avoid this. import Data.SBV.Provers.Prover (isSBranchFeasibleInState, isConditionSatisfiable, isVacuous, prove, defaultSMTCfg) -import Data.SBV.SMT.SMT (SatResult(..), ThmResult, showModel, getModelDictionary) +import Data.SBV.SMT.SMT (SafeResult(..), SatResult(..), ThmResult, getModelDictionary) -- | Newer versions of GHC (Starting with 7.8 I think), distinguishes between FiniteBits and Bits classes. -- We should really use FiniteBitSize for SBV which would make things better. In the interim, just work @@ -1221,9 +1221,8 @@ -- Otherwise symbolic simulation will stop with a run-time error. sAssert :: Mergeable a => String -> SBool -> a -> a sAssert msg = sAssertCont msg defCont - where die m = error $ intercalate "\n" $ ("Assertion failure: " ++ show msg) : m - defCont _ Nothing = die ["*** Fails in all assignments to inputs"] - defCont cfg (Just md) = die [showModel cfg (SMTModel (M.toList md) [] [])] + where defCont _ Nothing = C.throw (SafeAlwaysFails msg) + defCont cfg (Just md) = C.throw (SafeFailsInModel msg cfg (SMTModel (M.toList md) [] [])) -- | Symbolic assert with a programmable continuation. Check that the given boolean condition is always true in the given path. -- Otherwise symbolic simulation will transfer the failing model to the given continuation. The @@ -1649,16 +1648,16 @@ kg = kindOf (undefined :: g) kh = kindOf (undefined :: h) result st | Just (_, v) <- mbCgData, inProofMode st = sbvToSW st (v arg0 arg1 arg2 arg3 arg4 arg5 arg6) - | True = do newUninterpreted st nm (SBVType [kh, kg, kf, ke, kd, kc, kb, ka]) (fst `fmap` mbCgData) - sw0 <- sbvToSW st arg0 - sw1 <- sbvToSW st arg1 - sw2 <- sbvToSW st arg2 - sw3 <- sbvToSW st arg3 - sw4 <- sbvToSW st arg4 - sw5 <- sbvToSW st arg5 - sw6 <- sbvToSW st arg6 - mapM_ forceSWArg [sw0, sw1, sw2, sw3, sw4, sw5, sw6] - newExpr st ka $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2, sw3, sw4, sw5, sw6] + | True = do newUninterpreted st nm (SBVType [kh, kg, kf, ke, kd, kc, kb, ka]) (fst `fmap` mbCgData) + sw0 <- sbvToSW st arg0 + sw1 <- sbvToSW st arg1 + sw2 <- sbvToSW st arg2 + sw3 <- sbvToSW st arg3 + sw4 <- sbvToSW st arg4 + sw5 <- sbvToSW st arg5 + sw6 <- sbvToSW st arg6 + mapM_ forceSWArg [sw0, sw1, sw2, sw3, sw4, sw5, sw6] + newExpr st ka $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2, sw3, sw4, sw5, sw6] -- Uncurried functions of two arguments instance (SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV c, SBV b) -> SBV a) where diff --git a/Data/SBV/Bridge/Boolector.hs b/Data/SBV/Bridge/Boolector.hs --- a/Data/SBV/Bridge/Boolector.hs +++ b/Data/SBV/Bridge/Boolector.hs @@ -21,8 +21,8 @@ module Data.SBV.Bridge.Boolector ( -- * Boolector specific interface sbvCurrentSolver - -- ** Proving and checking satisfiability - , prove, sat, allSat, isVacuous, isTheorem, isSatisfiable + -- ** Proving, checking satisfiability, and safety + , prove, sat, safe, allSat, isVacuous, isTheorem, isSatisfiable -- ** Optimization routines , optimize, minimize, maximize -- * Non-Boolector specific SBV interface @@ -30,7 +30,7 @@ , module Data.SBV ) where -import Data.SBV hiding (prove, sat, allSat, isVacuous, isTheorem, isSatisfiable, optimize, minimize, maximize, sbvCurrentSolver) +import Data.SBV hiding (prove, sat, safe, allSat, isVacuous, isTheorem, isSatisfiable, optimize, minimize, maximize, sbvCurrentSolver) -- | Current solver instance, pointing to cvc4. sbvCurrentSolver :: SMTConfig @@ -47,6 +47,12 @@ => a -- ^ Property to check -> IO SatResult -- ^ Response of the SMT Solver, containing the model if found sat = satWith sbvCurrentSolver + +-- | Check safety, i.e., prove that all 'sAssert' conditions are statically true in all paths +safe :: SExecutable a + => a -- ^ Program to check the safety of + -> IO SafeResult -- ^ Response of the SMT solver, containing the unsafe model if found +safe = safeWith sbvCurrentSolver -- | Find all satisfying solutions, using the CVC4 SMT solver allSat :: Provable a diff --git a/Data/SBV/Bridge/CVC4.hs b/Data/SBV/Bridge/CVC4.hs --- a/Data/SBV/Bridge/CVC4.hs +++ b/Data/SBV/Bridge/CVC4.hs @@ -21,8 +21,8 @@ module Data.SBV.Bridge.CVC4 ( -- * CVC4 specific interface sbvCurrentSolver - -- ** Proving and checking satisfiability - , prove, sat, allSat, isVacuous, isTheorem, isSatisfiable + -- ** Proving, checking satisfiability, and safety + , prove, sat, safe, allSat, isVacuous, isTheorem, isSatisfiable -- ** Optimization routines , optimize, minimize, maximize -- * Non-CVC4 specific SBV interface @@ -30,7 +30,7 @@ , module Data.SBV ) where -import Data.SBV hiding (prove, sat, allSat, isVacuous, isTheorem, isSatisfiable, optimize, minimize, maximize, sbvCurrentSolver) +import Data.SBV hiding (prove, sat, safe, allSat, isVacuous, isTheorem, isSatisfiable, optimize, minimize, maximize, sbvCurrentSolver) -- | Current solver instance, pointing to cvc4. sbvCurrentSolver :: SMTConfig @@ -47,6 +47,12 @@ => a -- ^ Property to check -> IO SatResult -- ^ Response of the SMT Solver, containing the model if found sat = satWith sbvCurrentSolver + +-- | Check safety, i.e., prove that all 'sAssert' conditions are statically true in all paths +safe :: SExecutable a + => a -- ^ Program to check the safety of + -> IO SafeResult -- ^ Response of the SMT solver, containing the unsafe model if found +safe = safeWith sbvCurrentSolver -- | Find all satisfying solutions, using the CVC4 SMT solver allSat :: Provable a diff --git a/Data/SBV/Bridge/MathSAT.hs b/Data/SBV/Bridge/MathSAT.hs --- a/Data/SBV/Bridge/MathSAT.hs +++ b/Data/SBV/Bridge/MathSAT.hs @@ -21,8 +21,8 @@ module Data.SBV.Bridge.MathSAT ( -- * MathSAT specific interface sbvCurrentSolver - -- ** Proving and checking satisfiability - , prove, sat, allSat, isVacuous, isTheorem, isSatisfiable + -- ** Proving, checking satisfiability, and safety + , prove, sat, safe, allSat, isVacuous, isTheorem, isSatisfiable -- ** Optimization routines , optimize, minimize, maximize -- * Non-MathSAT specific SBV interface @@ -30,7 +30,7 @@ , module Data.SBV ) where -import Data.SBV hiding (prove, sat, allSat, isVacuous, isTheorem, isSatisfiable, optimize, minimize, maximize, sbvCurrentSolver) +import Data.SBV hiding (prove, sat, safe, allSat, isVacuous, isTheorem, isSatisfiable, optimize, minimize, maximize, sbvCurrentSolver) -- | Current solver instance, pointing to cvc4. sbvCurrentSolver :: SMTConfig @@ -47,6 +47,12 @@ => a -- ^ Property to check -> IO SatResult -- ^ Response of the SMT Solver, containing the model if found sat = satWith sbvCurrentSolver + +-- | Check safety, i.e., prove that all 'sAssert' conditions are statically true in all paths +safe :: SExecutable a + => a -- ^ Program to check the safety of + -> IO SafeResult -- ^ Response of the SMT solver, containing the unsafe model if found +safe = safeWith sbvCurrentSolver -- | Find all satisfying solutions, using the CVC4 SMT solver allSat :: Provable a diff --git a/Data/SBV/Bridge/Yices.hs b/Data/SBV/Bridge/Yices.hs --- a/Data/SBV/Bridge/Yices.hs +++ b/Data/SBV/Bridge/Yices.hs @@ -21,8 +21,8 @@ module Data.SBV.Bridge.Yices ( -- * Yices specific interface sbvCurrentSolver - -- ** Proving and checking satisfiability - , prove, sat, allSat, isVacuous, isTheorem, isSatisfiable + -- ** Proving, checking satisfiability, and safety + , prove, sat, safe, allSat, isVacuous, isTheorem, isSatisfiable -- ** Optimization routines , optimize, minimize, maximize -- * Non-Yices specific SBV interface @@ -30,7 +30,7 @@ , module Data.SBV ) where -import Data.SBV hiding (prove, sat, allSat, isVacuous, isTheorem, isSatisfiable, optimize, minimize, maximize, sbvCurrentSolver) +import Data.SBV hiding (prove, sat, safe, allSat, isVacuous, isTheorem, isSatisfiable, optimize, minimize, maximize, sbvCurrentSolver) -- | Current solver instance, pointing to yices. sbvCurrentSolver :: SMTConfig @@ -47,6 +47,12 @@ => a -- ^ Property to check -> IO SatResult -- ^ Response of the SMT Solver, containing the model if found sat = satWith sbvCurrentSolver + +-- | Check safety, i.e., prove that all 'sAssert' conditions are statically true in all paths +safe :: SExecutable a + => a -- ^ Program to check the safety of + -> IO SafeResult -- ^ Response of the SMT solver, containing the unsafe model if found +safe = safeWith sbvCurrentSolver -- | Find all satisfying solutions, using the Yices SMT solver allSat :: Provable a diff --git a/Data/SBV/Bridge/Z3.hs b/Data/SBV/Bridge/Z3.hs --- a/Data/SBV/Bridge/Z3.hs +++ b/Data/SBV/Bridge/Z3.hs @@ -21,8 +21,8 @@ module Data.SBV.Bridge.Z3 ( -- * Z3 specific interface sbvCurrentSolver - -- ** Proving and checking satisfiability - , prove, sat, allSat, isVacuous, isTheorem, isSatisfiable + -- ** Proving, checking satisfiability, and safety + , prove, sat, safe, allSat, isVacuous, isTheorem, isSatisfiable -- ** Optimization routines , optimize, minimize, maximize -- * Non-Z3 specific SBV interface @@ -30,7 +30,7 @@ , module Data.SBV ) where -import Data.SBV hiding (prove, sat, allSat, isVacuous, isTheorem, isSatisfiable, optimize, minimize, maximize, sbvCurrentSolver) +import Data.SBV hiding (prove, sat, safe, allSat, isVacuous, isTheorem, isSatisfiable, optimize, minimize, maximize, sbvCurrentSolver) -- | Current solver instance, pointing to z3. sbvCurrentSolver :: SMTConfig @@ -47,6 +47,12 @@ => a -- ^ Property to check -> IO SatResult -- ^ Response of the SMT Solver, containing the model if found sat = satWith sbvCurrentSolver + +-- | Check safety, i.e., prove that all 'sAssert' conditions are statically true in all paths +safe :: SExecutable a + => a -- ^ Program to check the safety of + -> IO SafeResult -- ^ Response of the SMT solver, containing the unsafe model if found +safe = safeWith sbvCurrentSolver -- | Find all satisfying solutions, using the Z3 SMT solver allSat :: Provable a diff --git a/Data/SBV/Provers/Prover.hs b/Data/SBV/Provers/Prover.hs --- a/Data/SBV/Provers/Prover.hs +++ b/Data/SBV/Provers/Prover.hs @@ -13,13 +13,15 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE OverlappingInstances #-} {-# LANGUAGE BangPatterns #-} +{-# LANGUAGE ScopedTypeVariables #-} module Data.SBV.Provers.Prover ( SMTSolver(..), SMTConfig(..), Predicate, Provable(..) - , ThmResult(..), SatResult(..), AllSatResult(..), SMTResult(..) + , ThmResult(..), SatResult(..), AllSatResult(..), SMTResult(..), SafeResult(..) , isSatisfiable, isSatisfiableWith, isTheorem, isTheoremWith , prove, proveWith , sat, satWith + , safe, safeWith , allSat, allSatWith , isVacuous, isVacuousWith , SatModel(..), Modelable(..), displayModels, extractModels @@ -40,6 +42,8 @@ import qualified Data.Set as Set (Set, toList) +import qualified Control.Exception as C + import Data.SBV.BitVectors.Data import Data.SBV.SMT.SMT import Data.SBV.SMT.SMTLib @@ -233,6 +237,10 @@ sat :: Provable a => a -> IO SatResult sat = satWith defaultSMTCfg +-- | Check if a given definition is safe; i.e., if all 'sAssert' conditions can be proven to hold. +safe :: SExecutable a => a -> IO SafeResult +safe = safeWith defaultSMTCfg + -- | Return all satisfying assignments for a predicate, equivalent to @'allSatWith' 'defaultSMTCfg'@. -- Satisfying assignments are constructed lazily, so they will be available as returned by the solver -- and on demand. @@ -326,6 +334,19 @@ satWith :: Provable a => SMTConfig -> a -> IO SatResult satWith config a = simulate cvt config True [] a >>= callSolver True "Checking Satisfiability.." SatResult config where cvt = if useSMTLib2 config then toSMTLib2 else toSMTLib1 + +-- | Check if a given definition is safe using the given solver configuration; i.e., if all 'sAssert' conditions can be proven to hold. +safeWith :: SExecutable a => SMTConfig -> a -> IO SafeResult +safeWith config a = C.catchJust choose checkSafe return + where checkSafe = do let msg = when (verbose config) . putStrLn . ("** " ++) + isTiming = timing config + msg "Starting safety checking symbolic simulation.." + res <- timeIf isTiming "problem construction" $ runSymbolic (False, Just config) $ sName_ a >>= output + msg $ "Generated symbolic trace:\n" ++ show res + return SafeNeverFails + choose e@(SafeNeverFails{}) = Just e + choose e@(SafeAlwaysFails{}) = Just e + choose e@(SafeFailsInModel{}) = Just e -- | Determine if the constraints are vacuous using the given SMT-solver isVacuousWith :: Provable a => SMTConfig -> a -> IO Bool diff --git a/Data/SBV/SMT/SMT.hs b/Data/SBV/SMT/SMT.hs --- a/Data/SBV/SMT/SMT.hs +++ b/Data/SBV/SMT/SMT.hs @@ -10,12 +10,14 @@ ----------------------------------------------------------------------------- {-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE DeriveDataTypeable #-} module Data.SBV.SMT.SMT where import qualified Control.Exception as C import Control.Concurrent (newEmptyMVar, takeMVar, putMVar, forkIO) +import Control.DeepSeq (NFData(..)) import Control.Monad (when, zipWithM) import Data.Char (isSpace) import Data.Int (Int8, Int16, Int32, Int64) @@ -27,6 +29,7 @@ import System.IO (hClose, hFlush, hPutStr, hGetContents, hGetLine) import qualified Data.Map as M +import Data.Typeable import Data.SBV.BitVectors.AlgReals import Data.SBV.BitVectors.Data @@ -84,6 +87,22 @@ Satisfiable{} -> True _ -> False +-- | The result of an 'sAssert' call +data SafeResult = SafeNeverFails + | SafeAlwaysFails String + | SafeFailsInModel String SMTConfig SMTModel + deriving Typeable + +-- | The show instance for SafeResult. Note that this is for display purposes only, +-- user programs are likely to pattern match on the output and proceed accordingly. +instance Show SafeResult where + show SafeNeverFails = "No safety violations detected." + show (SafeAlwaysFails s) = intercalate "\n" ["Assertion failure: " ++ show s, "*** Fails in all assignments to inputs"] + show (SafeFailsInModel s cfg md) = intercalate "\n" ["Assertion failure: " ++ show s, showModel cfg md] + +-- | If a 'prove' or 'sat' call comes accross an 'sAssert' call that fails, they will throw a 'SafeResult' as an exception. +instance C.Exception SafeResult + -- | Instances of 'SatModel' can be automatically extracted from models returned by the -- solvers. The idea is that the sbv infrastructure provides a stream of 'CW''s (constant-words) -- coming from the solver, and the type @a@ is interpreted based on these constants. Many typical @@ -348,11 +367,15 @@ let nm = show (name (solver cfg)) mbExecPath <- findExecutable execName case mbExecPath of - Nothing -> return $ Left $ "Unable to locate executable for " ++ nm - ++ "\nExecutable specified: " ++ show execName - Just execPath -> do (ec, contents, allErrors) <- runSolver cfg execPath opts script - let errors = dropWhile isSpace (cleanErrs allErrors) - case (null errors, xformExitCode (solver cfg) ec) of + Nothing -> return $ Left $ "Unable to locate executable for " ++ nm + ++ "\nExecutable specified: " ++ show execName + Just execPath -> + do solverResult <- dispatchSolver cfg execPath opts script + case solverResult of + Left s -> return $ Left s + Right (ec, contents, allErrors) -> + let errors = dropWhile isSpace (cleanErrs allErrors) + in case (null errors, xformExitCode (solver cfg) ec) of (True, ExitSuccess) -> return $ Right $ map clean (filter (not . null) (lines contents)) (_, ec') -> let errors' = if null errors then (if null (dropWhile isSpace contents) @@ -395,6 +418,14 @@ case contents of Left e -> return $ failure (lines e) Right xs -> return $ success (mergeSExpr xs) + +-- | Wrap the solver call to protect against any exceptions +dispatchSolver :: SMTConfig -> FilePath -> [String] -> SMTScript -> IO (Either String (ExitCode, String, String)) +dispatchSolver cfg execPath opts script = rnf script `seq` (Right `fmap` runSolver cfg execPath opts script) `C.catch` (\(e::C.SomeException) -> bad (show e)) + where bad s = return $ Left $ unlines [ "Failed to start the external solver: " ++ s + , "Make sure you can start " ++ show execPath + , "from the command line without issues." + ] -- | A variant of 'readProcessWithExitCode'; except it knows about continuation strings -- and can speak SMT-Lib2 (just a little). diff --git a/SBVUnitTest/SBVUnitTestBuildTime.hs b/SBVUnitTest/SBVUnitTestBuildTime.hs --- a/SBVUnitTest/SBVUnitTestBuildTime.hs +++ b/SBVUnitTest/SBVUnitTestBuildTime.hs @@ -2,4 +2,4 @@ module SBVUnitTestBuildTime (buildTime) where buildTime :: String -buildTime = "Tue Nov 18 18:03:52 PST 2014" +buildTime = "Fri Dec 5 00:41:13 PST 2014" diff --git a/sbv.cabal b/sbv.cabal --- a/sbv.cabal +++ b/sbv.cabal @@ -1,5 +1,5 @@ Name: sbv -Version: 3.2 +Version: 3.3 Category: Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math, SMT Synopsis: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving. Description: Express properties about Haskell programs and automatically prove them using SMT