diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,7 +1,57 @@ * Hackage: * GitHub: -* Latest Hackage released version: 3.0 +* Latest Hackage released version: 3.1 + +### Version 3.1, 2014-07-12 + + NB: GHC 7.8.1 and 7.8.2 has a serious bug (https://ghc.haskell.org/trac/ghc/ticket/9078) + that causes SBV to crash under heavy/repeated calls. The bug is addressed + in GHC 7.8.3; so upgrading to 7.8.3 is essential for using SBV! + + New features/bug-fixes in v3.1: + + * Using multiple-SMT solvers in parallel: + * Added functions that let the user run multiple solvers, using asynchronous + threads. All results can be obtained (proveWithAll, proveWithAny, satWithAll), + or SBV can return the fastest result (satWithAny, allSatWithAll, allSatWithAny). + These functions are good for playing with multiple-solvers, especially on + machines with multiple-cores. + * Add function: sbvAvailableSolvers; which returns the list of solvers currently + available, as installed on the machine we are running. (Not the list that SBV + supports, but those that are actually available at run-time.) This function + is useful with the multi-solve API. + * Implement sBranch: + * sBranch is a variant of 'ite' that consults the external + SMT solver to see if a given branch condition is satisfiable + before evaluating it. This can make certain "otherwise recursive + and thus not-symbolically-terminating inputs" amenable to symbolic + simulation, if termination can be established this way. Needless + to say, this problem is always decidable as far as SBV programs + are concerned, but it does not mean the decision procedure is cheap! + Use with care. + * sBranchTimeOut config parameter can be used to curtail long runs when + sBranch is used. Of course, if time-out happens, SBV will + assume the branch is feasible, in which case symbolic-termination + may come back to bite you.) + * New API: + * Add predicate 'isSNaN' which allows testing 'SFloat'/'SDouble' values + for nan-ness. This is similar to the Prelude function 'isNaN', except + the Prelude version requires a RealFrac instance, which unfortunately is + not currently implementable for cases. (Requires trigonometric functions etc.) + Thus, we provide 'isSNaN' separately (along with the already existing + 'isFPPoint') to simplify reasoning with floating-point. + * Examples: + * Add Data/SBV/Examples/Misc/SBranch.hs, to illustrate the use of sBranch. + * Bug fixes: + * Fix pipe-blocking issue, which exhibited itself in the presence of + large numbers of variables (> 10K or so). See github issue #86. Thanks + to Philipp Meyer for the fine report. + * Misc: + * Add missing SFloat/SDouble instances for SatModel class + * Explicitly support KBool as a kind, separating it from "KUnbounded False 1". + Thanks to Brian Huffman for contributing the changes. This should have no + user-visible impact, but comes in handy for internal reasons. ### Version 3.0, 2014-02-16 diff --git a/Data/SBV.hs b/Data/SBV.hs --- a/Data/SBV.hs +++ b/Data/SBV.hs @@ -96,10 +96,16 @@ -- -- * MathSAT from Fondazione Bruno Kessler and DISI-University of Trento: -- +-- SBV also allows calling these solvers in parallel, either getting results from multiple solvers +-- or returning the fastest one. (See 'proveWithAll', 'proveWithAny', etc.) +-- -- Support for other compliant solvers can be added relatively easily, please -- get in touch if there is a solver you'd like to see included. --------------------------------------------------------------------------------- +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE OverlappingInstances #-} + module Data.SBV ( -- * Programming with symbolic values -- $progIntro @@ -117,7 +123,7 @@ , SInteger -- *** IEEE-floating point numbers -- $floatingPoints - , SFloat, SDouble, RoundingMode(..), nan, infinity, sNaN, sInfinity, fusedMA, isFPPoint + , SFloat, SDouble, RoundingMode(..), nan, infinity, sNaN, sInfinity, fusedMA, isSNaN, isFPPoint -- *** Signed algebraic reals -- $algReals , SReal, AlgReal, toSReal @@ -188,6 +194,10 @@ -- ** Checking constraint vacuity , isVacuous, isVacuousWith + -- * Proving properties using multiple solvers + -- $multiIntro + , proveWithAll, proveWithAny, satWithAll, satWithAny, allSatWithAll, allSatWithAny + -- * Optimization -- $optimizeIntro , minimize, maximize, optimize @@ -209,7 +219,7 @@ , getModelDictionaries, getModelValues, getModelUninterpretedValues -- * SMT Interface: Configurations and solvers - , SMTConfig(..), SMTLibLogic(..), Logic(..), OptimizeOpts(..), SMTSolver(..), boolector, cvc4, yices, z3, mathSAT, sbvCurrentSolver, defaultSMTCfg, sbvCheckSolverInstallation + , SMTConfig(..), SMTLibLogic(..), Logic(..), OptimizeOpts(..), Solver(..), SMTSolver(..), boolector, cvc4, yices, z3, mathSAT, sbvCurrentSolver, defaultSMTCfg, sbvCheckSolverInstallation, sbvAvailableSolvers -- * Symbolic computations , Symbolic, output, SymWord(..) @@ -255,6 +265,10 @@ , module Data.Ratio ) where +import Control.Monad (filterM) +import Control.Concurrent.Async (async, waitAny, waitAnyCancel) +import System.IO.Unsafe (unsafeInterleaveIO) -- only used safely! + import Data.SBV.BitVectors.AlgReals import Data.SBV.BitVectors.Data import Data.SBV.BitVectors.Model @@ -282,13 +296,140 @@ sbvCurrentSolver :: SMTConfig sbvCurrentSolver = z3 +-- | Note that the floating point value NaN does not compare equal to itself, +-- so we need a special recognizer for that. Haskell provides the isNaN predicate +-- with the `RealFrac` class, which unfortunately is not currently implementable for +-- symbolic cases. (Requires trigonometric functions etc.) Thus, we provide this +-- recognizer separately. Note that the definition simply tests equality against +-- itself, which fails for NaN. Who said equality for floating point was reflexive? +isSNaN :: (Floating a, SymWord a) => SBV a -> SBool +isSNaN x = x ./= x + -- | We call a FP number FPPoint if it is neither NaN, nor +/- infinity. --- Note that we cannot use == to test for this, as NaN does not compare equal to itself. isFPPoint :: (Floating a, SymWord a) => SBV a -> SBool isFPPoint x = x .== x -- gets rid of NaN's &&& x .< sInfinity -- gets rid of +inf &&& x .> -sInfinity -- gets rid of -inf +-- | Form the symbolic conjunction of a given list of boolean conditions. Useful in expressing +-- problems with constraints, like the following: +-- +-- @ +-- do [x, y, z] <- sIntegers [\"x\", \"y\", \"z\"] +-- solve [x .> 5, y + z .< x] +-- @ +solve :: [SBool] -> Symbolic SBool +solve = return . bAnd + +-- | Check whether the given solver is installed and is ready to go. This call does a +-- simple call to the solver to ensure all is well. +sbvCheckSolverInstallation :: SMTConfig -> IO Bool +sbvCheckSolverInstallation cfg = do ThmResult r <- proveWith cfg $ \x -> (x+x) .== ((x*2) :: SWord8) + case r of + Unsatisfiable _ -> return True + _ -> return False + +-- The default configs +defaultSolverConfig :: Solver -> SMTConfig +defaultSolverConfig Z3 = z3 +defaultSolverConfig Yices = yices +defaultSolverConfig Boolector = boolector +defaultSolverConfig CVC4 = cvc4 +defaultSolverConfig MathSAT = mathSAT + +-- | Return the known available solver configs, installed on your machine. +sbvAvailableSolvers :: IO [SMTConfig] +sbvAvailableSolvers = filterM sbvCheckSolverInstallation (map defaultSolverConfig [minBound .. maxBound]) + +sbvWithAny :: Provable a => [SMTConfig] -> (SMTConfig -> a -> IO b) -> a -> IO (Solver, b) +sbvWithAny [] _ _ = error "SBV.withAny: No solvers given!" +sbvWithAny solvers what a = snd `fmap` (mapM try solvers >>= waitAnyCancel) + where try s = async $ what s a >>= \r -> return (name (solver s), r) + +sbvWithAll :: Provable a => [SMTConfig] -> (SMTConfig -> a -> IO b) -> a -> IO [(Solver, b)] +sbvWithAll solvers what a = mapM try solvers >>= (unsafeInterleaveIO . go) + where try s = async $ what s a >>= \r -> return (name (solver s), r) + go [] = return [] + go as = do (d, r) <- waitAny as + rs <- unsafeInterleaveIO $ go (filter (/= d) as) + return (r : rs) + +-- | Prove a property with multiple solvers, running them in separate threads. The +-- results will be returned in the order produced. +proveWithAll :: Provable a => [SMTConfig] -> a -> IO [(Solver, ThmResult)] +proveWithAll = (`sbvWithAll` proveWith) + +-- | Prove a property with multiple solvers, running them in separate threads. Only +-- the result of the first one to finish will be returned, remaining threads will be killed. +proveWithAny :: Provable a => [SMTConfig] -> a -> IO (Solver, ThmResult) +proveWithAny = (`sbvWithAny` proveWith) + +-- | Find a satisfying assignment to a property with multiple solvers, running them in separate threads. The +-- results will be returned in the order produced. +satWithAll :: Provable a => [SMTConfig] -> a -> IO [(Solver, SatResult)] +satWithAll = (`sbvWithAll` satWith) + +-- | Find a satisfying assignment to a property with multiple solvers, running them in separate threads. Only +-- the result of the first one to finish will be returned, remaining threads will be killed. +satWithAny :: Provable a => [SMTConfig] -> a -> IO (Solver, SatResult) +satWithAny = (`sbvWithAny` satWith) + +-- | Find all satisfying assignments to a property with multiple solvers, running them in separate threads. Only +-- the result of the first one to finish will be returned, remaining threads will be killed. +allSatWithAll :: Provable a => [SMTConfig] -> a -> IO [(Solver, AllSatResult)] +allSatWithAll = (`sbvWithAll` allSatWith) + +-- | Find all satisfying assignments to a property with multiple solvers, running them in separate threads. Only +-- the result of the first one to finish will be returned, remaining threads will be killed. +allSatWithAny :: Provable a => [SMTConfig] -> a -> IO (Solver, AllSatResult) +allSatWithAny = (`sbvWithAny` allSatWith) + +-- | Equality as a proof method. Allows for +-- very concise construction of equivalence proofs, which is very typical in +-- bit-precise proofs. +infix 4 === +class Equality a where + (===) :: a -> a -> IO ThmResult + +instance (SymWord a, EqSymbolic z) => Equality (SBV a -> z) where + k === l = prove $ \a -> k a .== l a + +instance (SymWord a, SymWord b, EqSymbolic z) => Equality (SBV a -> SBV b -> z) where + k === l = prove $ \a b -> k a b .== l a b + +instance (SymWord a, SymWord b, EqSymbolic z) => Equality ((SBV a, SBV b) -> z) where + k === l = prove $ \a b -> k (a, b) .== l (a, b) + +instance (SymWord a, SymWord b, SymWord c, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> z) where + k === l = prove $ \a b c -> k a b c .== l a b c + +instance (SymWord a, SymWord b, SymWord c, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c) -> z) where + k === l = prove $ \a b c -> k (a, b, c) .== l (a, b, c) + +instance (SymWord a, SymWord b, SymWord c, SymWord d, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> z) where + k === l = prove $ \a b c d -> k a b c d .== l a b c d + +instance (SymWord a, SymWord b, SymWord c, SymWord d, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d) -> z) where + k === l = prove $ \a b c d -> k (a, b, c, d) .== l (a, b, c, d) + +instance (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> z) where + k === l = prove $ \a b c d e -> k a b c d e .== l a b c d e + +instance (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e) -> z) where + k === l = prove $ \a b c d e -> k (a, b, c, d, e) .== l (a, b, c, d, e) + +instance (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> z) where + k === l = prove $ \a b c d e f -> k a b c d e f .== l a b c d e f + +instance (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> z) where + k === l = prove $ \a b c d e f -> k (a, b, c, d, e, f) .== l (a, b, c, d, e, f) + +instance (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> z) where + k === l = prove $ \a b c d e f g -> k a b c d e f g .== l a b c d e f g + +instance (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> z) where + k === l = prove $ \a b c d e f g -> k (a, b, c, d, e, f, g) .== l (a, b, c, d, e, f, g) + -- Haddock section documentation {- $progIntro The SBV library is really two things: @@ -318,12 +459,32 @@ or how different logics operate. The details are hidden behind the SBV framework, providing Haskell programmers with a clean API that is unencumbered by the details of individual solvers. To that end, we use the SMT-Lib standard () -to communicate with arbitrary SMT solvers. Unfortunately, -the SMT-Lib version 1.X does not standardize how models are communicated back from solvers, so -there is some work in parsing individual SMT solver output. The 2.X version of the SMT-Lib -standard (not yet implemented by SMT solvers widely, unfortunately) will bring new standard features -for getting models; at which time the SBV framework can be modified into a truly plug-and-play -system where arbitrary SMT solvers can be used. +to communicate with arbitrary SMT solvers. +-} + +{- $multiIntro +On a multi-core machine, it might be desirable to try a given property using multiple SMT solvers, +using parallel threads. Even with machines with single-cores, threading can be helpful if you +want to try out multiple-solvers but do not know which one would work the best +for the problem at hand ahead of time. + +The functions in this section allow proving/satisfiability-checking with multiple +backends at the same time. Each function comes in two variants, one that +returns the results from all solvers, the other that returns the fastest one. + +The @All@ variants, (i.e., 'proveWithAll', 'satWithAll', 'allSatWithAll') run all solvers and +return all the results. SBV internally makes sure that the result is lazily generated; so, +the order of solvers given does not matter. In other words, the order of results will follow +the order of the solvers as they finish, not as given by the user. These variants are useful when you +want to make sure multiple-solvers agree (or disagree!) on a given problem. + +The @Any@ variants, (i.e., 'proveWithAny', 'satWithAny', 'allSatWithAny') will run all the solvers +in parallel, and return the results of the first one finishing. The other threads will then be killed. These variants +are useful when you do not care if the solvers produce the same result, but rather want to get the +solution as quickly as possible, taking advantage of modern many-core machines. + +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. -} {- $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 @@ -17,6 +17,7 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE PatternGuards #-} {-# LANGUAGE DefaultSignatures #-} +{-# LANGUAGE NamedFieldPuns #-} module Data.SBV.BitVectors.Data ( SBool, SWord8, SWord16, SWord32, SWord64 @@ -28,19 +29,23 @@ , SW(..), trueSW, falseSW, trueCW, falseCW, normCW , SBV(..), NodeId(..), mkSymSBV , ArrayContext(..), ArrayInfo, SymArray(..), SFunArray(..), mkSFunArray, SArray(..), arrayUIKind - , sbvToSW, sbvToSymSW + , sbvToSW, sbvToSymSW, forceSWArg , SBVExpr(..), newExpr , cache, Cached, uncache, uncacheAI, HasKind(..) - , Op(..), NamedSymVar, UnintKind(..), getTableIndex, SBVPgm(..), Symbolic, runSymbolic, runSymbolic', State, inProofMode, SBVRunMode(..), Kind(..), Outputtable(..), Result(..) + , Op(..), NamedSymVar, UnintKind(..), getTableIndex, SBVPgm(..), Symbolic, runSymbolic, runSymbolic', State, getPathCondition, extendPathCondition + , inProofMode, SBVRunMode(..), Kind(..), Outputtable(..), Result(..) , Logic(..), SMTLibLogic(..) , getTraceInfo, getConstraints, addConstraint , SBVType(..), newUninterpreted, unintFnUIKind, addAxiom , Quantifier(..), needsExistentials , SMTLibPgm(..), SMTLibVersion(..) , SolverCapabilities(..) + , extractSymbolicSimulationState + , SMTScript(..), Solver(..), SMTSolver(..), SMTResult(..), SMTModel(..), SMTConfig(..), getSBranchRunConfig ) where import Control.DeepSeq (NFData(..)) +import Control.Applicative (Applicative) import Control.Monad (when) import Control.Monad.Reader (MonadReader, ReaderT, ask, runReaderT) import Control.Monad.Trans (MonadIO, liftIO) @@ -58,6 +63,7 @@ import qualified Data.Foldable as F (toList) import qualified Data.Sequence as S (Seq, empty, (|>)) +import System.Exit (ExitCode(..)) import System.Mem.StableName import System.Random @@ -128,8 +134,8 @@ -- | Is this a bit? cwIsBit :: CW -> Bool cwIsBit x = case cwKind x of - KBounded False 1 -> True - _ -> False + KBool -> True + _ -> False -- | Convert a CW to a Haskell boolean (NB. Assumes input is well-kinded) cwToBool :: CW -> Bool @@ -150,7 +156,8 @@ normCW c = c -- | Kind of symbolic value -data Kind = KBounded Bool Int +data Kind = KBool + | KBounded Bool Int | KUnbounded | KReal | KUninterpreted String @@ -159,7 +166,7 @@ deriving (Eq, Ord) instance Show Kind where - show (KBounded False 1) = "SBool" + show KBool = "SBool" show (KBounded False n) = "SWord" ++ show n show (KBounded True n) = "SInt" ++ show n show KUnbounded = "SInteger" @@ -174,6 +181,12 @@ -- | A symbolic word, tracking it's signedness and size. data SW = SW Kind NodeId deriving (Eq, Ord) +-- | Forcing an argument; this is a necessary evil to make sure all the arguments +-- to an uninterpreted function and sBranch test conditions are evaluated before called; +-- the semantics of uinterpreted functions is necessarily strict; deviating from Haskell's +forceSWArg :: SW -> IO () +forceSWArg (SW k n) = k `seq` n `seq` return () + -- | Quantifiers: forall or exists. Note that we allow -- arbitrary nestings. data Quantifier = ALL | EX deriving Eq @@ -184,19 +197,19 @@ -- | Constant False as a SW. Note that this value always occupies slot -2. falseSW :: SW -falseSW = SW (KBounded False 1) $ NodeId (-2) +falseSW = SW KBool $ NodeId (-2) -- | Constant False as a SW. Note that this value always occupies slot -1. trueSW :: SW -trueSW = SW (KBounded False 1) $ NodeId (-1) +trueSW = SW KBool $ NodeId (-1) -- | Constant False as a CW. We represent it using the integer value 0. falseCW :: CW -falseCW = CW (KBounded False 1) (CWInteger 0) +falseCW = CW KBool (CWInteger 0) -- | Constant True as a CW. We represent it using the integer value 1. trueCW :: CW -trueCW = CW (KBounded False 1) (CWInteger 1) +trueCW = CW KBool (CWInteger 1) -- | A simple type for SBV computations, used mainly for uninterpreted constants. -- We keep track of the signedness/size of the arguments. A non-function will @@ -263,6 +276,7 @@ showType :: a -> String -- defaults hasSign x = case kindOf x of + KBool -> False KBounded b _ -> b KUnbounded -> True KReal -> True @@ -270,13 +284,14 @@ KDouble -> True KUninterpreted{} -> False intSizeOf x = case kindOf x of + KBool -> error "SBV.HasKind.intSizeOf((S)Bool)" KBounded _ s -> s KUnbounded -> error "SBV.HasKind.intSizeOf((S)Integer)" KReal -> error "SBV.HasKind.intSizeOf((S)Real)" KFloat -> error "SBV.HasKind.intSizeOf((S)Float)" KDouble -> error "SBV.HasKind.intSizeOf((S)Double)" KUninterpreted s -> error $ "SBV.HasKind.intSizeOf: Uninterpreted sort: " ++ s - isBoolean x | KBounded False 1 <- kindOf x = True + isBoolean x | KBool{} <- kindOf x = True | True = False isBounded x | KBounded{} <- kindOf x = True | True = False @@ -296,7 +311,7 @@ default kindOf :: Data a => a -> Kind kindOf = KUninterpreted . tyconUQname . dataTypeName . dataTypeOf -instance HasKind Bool where kindOf _ = KBounded False 1 +instance HasKind Bool where kindOf _ = KBool instance HasKind Int8 where kindOf _ = KBounded True 8 instance HasKind Word8 where kindOf _ = KBounded False 8 instance HasKind Int16 where kindOf _ = KBounded True 16 @@ -538,9 +553,9 @@ external (ArrayMerge{}) = False -- | Different means of running a symbolic piece of code -data SBVRunMode = Proof Bool -- ^ Symbolic simulation mode, for proof purposes. Bool is True if it's a sat instance - | CodeGen -- ^ Code generation mode - | Concrete StdGen -- ^ Concrete simulation mode. The StdGen is for the pConstrain acceptance in cross runs +data SBVRunMode = Proof (Bool, Maybe SMTConfig) -- ^ Symbolic simulation mode, for proof purposes. Bool is True if it's a sat instance. SMTConfig is used for 'sBranch' calls. + | CodeGen -- ^ Code generation mode + | Concrete StdGen -- ^ Concrete simulation mode. The StdGen is for the pConstrain acceptance in cross runs -- | Is this a concrete run? (i.e., quick-check or test-generation like) isConcreteMode :: SBVRunMode -> Bool @@ -550,6 +565,7 @@ -- | The state of the symbolic interpreter data State = State { runMode :: SBVRunMode + , pathCond :: SBool , rStdGen :: IORef StdGen , rCInfo :: IORef [(String, CW)] , rctr :: IORef Int @@ -569,6 +585,14 @@ , rAICache :: IORef (Cache Int) } +-- | Get the current path condition +getPathCondition :: State -> SBool +getPathCondition = pathCond + +-- | Extend the path condition with the given test value. +extendPathCondition :: State -> (SBool -> SBool) -> State +extendPathCondition st f = st{pathCond = f (pathCond st)} + -- | Are we running in proof mode? inProofMode :: State -> Bool inProofMode s = case runMode s of @@ -576,6 +600,12 @@ CodeGen -> False Concrete{} -> False +-- | If in proof mode, get the underlying configuration (used for 'sBranch') +getSBranchRunConfig :: State -> Maybe SMTConfig +getSBranchRunConfig st = case runMode st of + Proof (_, s) -> s + _ -> Nothing + -- | The "Symbolic" value. Either a constant (@Left@) or a symbolic -- value (@Right Cached@). Note that caching is essential for making -- sure sharing is preserved. The parameter 'a' is phantom, but is @@ -742,6 +772,7 @@ -- | Create a constant word from an integral mkConstCW :: Integral a => Kind -> a -> CW +mkConstCW KBool a = normCW $ CW KBool (CWInteger (toInteger a)) mkConstCW k@(KBounded{}) a = normCW $ CW k (CWInteger (toInteger a)) mkConstCW KUnbounded a = normCW $ CW KUnbounded (CWInteger (toInteger a)) mkConstCW KReal a = normCW $ CW KReal (CWAlgReal (fromInteger (toInteger a))) @@ -774,7 +805,7 @@ -- state of the computation, layered on top of IO for creating unique -- references to hold onto intermediate results. newtype Symbolic a = Symbolic (ReaderT State IO a) - deriving (Functor, Monad, MonadIO, MonadReader State) + deriving (Applicative, Functor, Monad, MonadIO, MonadReader State) -- | Create a symbolic value, based on the quantifier we have. If an explicit quantifier is given, we just use that. -- If not, then we pick existential for SAT calls and universal for everything else. @@ -782,11 +813,11 @@ mkSymSBV mbQ k mbNm = do st <- ask let q = case (mbQ, runMode st) of - (Just x, _) -> x -- user given, just take it - (Nothing, Concrete{}) -> ALL -- concrete simulation, pick universal - (Nothing, Proof True) -> EX -- sat mode, pick existential - (Nothing, Proof False) -> ALL -- proof mode, pick universal - (Nothing, CodeGen) -> ALL -- code generation, pick universal + (Just x, _) -> x -- user given, just take it + (Nothing, Concrete{}) -> ALL -- concrete simulation, pick universal + (Nothing, Proof (True, _)) -> EX -- sat mode, pick existential + (Nothing, Proof (False, _)) -> ALL -- proof mode, pick universal + (Nothing, CodeGen) -> ALL -- code generation, pick universal case runMode st of Concrete _ | q == EX -> case mbNm of Nothing -> error $ "Cannot quick-check in the presence of existential variables, type: " ++ showType (undefined :: SBV a) @@ -862,7 +893,7 @@ -- | Run a symbolic computation in Proof mode and return a 'Result'. The boolean -- argument indicates if this is a sat instance or not. -runSymbolic :: Bool -> Symbolic a -> IO Result +runSymbolic :: (Bool, Maybe SMTConfig) -> Symbolic a -> IO Result runSymbolic b c = snd `fmap` runSymbolic' (Proof b) c -- | Run a symbolic computation, and return a extra value paired up with the 'Result' @@ -888,6 +919,7 @@ Concrete g -> newIORef g _ -> newStdGen >>= newIORef let st = State { runMode = currentRunMode + , pathCond = SBV KBool (Left trueCW) , rStdGen = rGen , rCInfo = cInfo , rctr = ctr @@ -906,9 +938,17 @@ , rAICache = aiCache , rConstraints = cstrs } - _ <- newConst st (mkConstCW (KBounded False 1) (0::Integer)) -- s(-2) == falseSW - _ <- newConst st (mkConstCW (KBounded False 1) (1::Integer)) -- s(-1) == trueSW + _ <- newConst st falseCW -- s(-2) == falseSW + _ <- newConst st trueCW -- s(-1) == trueSW r <- runReaderT c st + res <- extractSymbolicSimulationState st + return (r, res) + +-- | Grab the program from a running symbolic simulation state. This is useful for internal purposes, for +-- instance when implementing 'sBranch'. +extractSymbolicSimulationState :: State -> IO Result +extractSymbolicSimulationState st@State{ spgm=pgm, rinps=inps, routs=outs, rtblMap=tables, rArrayMap=arrays, rUIMap=uis, raxioms=axioms + , rUsedKinds=usedKinds, rCgMap=cgs, rCInfo=cInfo, rConstraints = cstrs} = do SBVPgm rpgm <- readIORef pgm inpsO <- reverse `fmap` readIORef inps outsO <- reverse `fmap` readIORef outs @@ -923,7 +963,7 @@ cgMap <- Map.toList `fmap` readIORef cgs traceVals <- reverse `fmap` readIORef cInfo extraCstrs <- reverse `fmap` readIORef cstrs - return $ (r, Result knds traceVals cgMap inpsO cnsts tbls arrs unint axs (SBVPgm rpgm) extraCstrs outsO) + return $ Result knds traceVals cgMap inpsO cnsts tbls arrs unint axs (SBVPgm rpgm) extraCstrs outsO ------------------------------------------------------------------------------- -- * Symbolic Words @@ -1008,11 +1048,11 @@ let k = KUninterpreted sortName liftIO $ registerKind st k let q = case (mbQ, runMode st) of - (Just x, _) -> x - (Nothing, Proof True) -> EX - (Nothing, Proof False) -> ALL - (Nothing, Concrete{}) -> error $ "SBV: Uninterpreted sort " ++ sortName ++ " can not be used in concrete simulation mode." - (Nothing, CodeGen) -> error $ "SBV: Uninterpreted sort " ++ sortName ++ " can not be used in code-generation mode." + (Just x, _) -> x + (Nothing, Proof (True, _)) -> EX + (Nothing, Proof (False, _)) -> ALL + (Nothing, Concrete{}) -> error $ "SBV: Uninterpreted sort " ++ sortName ++ " can not be used in concrete simulation mode." + (Nothing, CodeGen) -> error $ "SBV: Uninterpreted sort " ++ sortName ++ " can not be used in code-generation mode." ctr <- liftIO $ incCtr st let sw = SW k (NodeId ctr) nm = maybe ('s':show ctr) id mbNm @@ -1248,6 +1288,16 @@ rnf (SBV x y) = rnf x `seq` rnf y `seq` () instance NFData SBVPgm +instance NFData SMTResult where + rnf (Unsatisfiable _) = () + rnf (Satisfiable _ xs) = rnf xs `seq` () + rnf (Unknown _ xs) = rnf xs `seq` () + rnf (ProofError _ xs) = rnf xs `seq` () + rnf (TimeOut _) = () + +instance NFData SMTModel where + rnf (SMTModel assocs unints uarrs) = rnf assocs `seq` rnf unints `seq` rnf uarrs `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. @@ -1300,3 +1350,84 @@ , supportsFloats :: Bool -- ^ Does the solver support single-precision floating point numbers? , supportsDoubles :: Bool -- ^ Does the solver support double-precision floating point numbers? } + +-- | Solver configuration. See also 'z3', 'yices', 'cvc4', 'boolector', 'mathSAT', etc. which are instantiations of this type for those solvers, with +-- reasonable defaults. In particular, custom configuration can be created by varying those values. (Such as @z3{verbose=True}@.) +-- +-- Most fields are self explanatory. The notion of precision for printing algebraic reals stems from the fact that such values does +-- not necessarily have finite decimal representations, and hence we have to stop printing at some depth. It is important to +-- emphasize that such values always have infinite precision internally. The issue is merely with how we print such an infinite +-- precision value on the screen. The field 'printRealPrec' controls the printing precision, by specifying the number of digits after +-- the decimal point. The default value is 16, but it can be set to any positive integer. +-- +-- When printing, SBV will add the suffix @...@ at the and of a real-value, if the given bound is not sufficient to represent the real-value +-- exactly. Otherwise, the number will be written out in standard decimal notation. Note that SBV will always print the whole value if it +-- is precise (i.e., if it fits in a finite number of digits), regardless of the precision limit. The limit only applies if the representation +-- of the real value is not finite, i.e., if it is not rational. +data SMTConfig = SMTConfig { + verbose :: Bool -- ^ Debug mode + , timing :: Bool -- ^ Print timing information on how long different phases took (construction, solving, etc.) + , sBranchTimeOut :: Maybe Int -- ^ How much time to give to the solver for each call of 'sBranch' check. (In seconds. Default: No limit.) + , timeOut :: Maybe Int -- ^ How much time to give to the solver. (In seconds. Default: No limit.) + , printBase :: Int -- ^ Print integral literals in this base (2, 8, and 10, and 16 are supported.) + , printRealPrec :: Int -- ^ Print algebraic real values with this precision. (SReal, default: 16) + , solverTweaks :: [String] -- ^ Additional lines of script to give to the solver (user specified) + , satCmd :: String -- ^ Usually "(check-sat)". However, users might tweak it based on solver characteristics. + , smtFile :: Maybe FilePath -- ^ If Just, the generated SMT script will be put in this file (for debugging purposes mostly) + , useSMTLib2 :: Bool -- ^ If True, we'll treat the solver as using SMTLib2 input format. Otherwise, SMTLib1 + , solver :: SMTSolver -- ^ The actual SMT solver. + , roundingMode :: RoundingMode -- ^ Rounding mode to use for floating-point conversions + , useLogic :: Maybe Logic -- ^ If Nothing, pick automatically. Otherwise, either use the given one, or use the custom string. + } + +instance Show SMTConfig where + show = show . solver + +-- | A model, as returned by a solver +data SMTModel = SMTModel { + modelAssocs :: [(String, CW)] -- ^ Mapping of symbolic values to constants. + , modelArrays :: [(String, [String])] -- ^ Arrays, very crude; only works with Yices. + , modelUninterps :: [(String, [String])] -- ^ Uninterpreted funcs; very crude; only works with Yices. + } + deriving Show + +-- | The result of an SMT solver call. Each constructor is tagged with +-- the 'SMTConfig' that created it so that further tools can inspect it +-- and build layers of results, if needed. For ordinary uses of the library, +-- this type should not be needed, instead use the accessor functions on +-- it. (Custom Show instances and model extractors.) +data SMTResult = Unsatisfiable SMTConfig -- ^ Unsatisfiable + | Satisfiable SMTConfig SMTModel -- ^ Satisfiable with model + | Unknown SMTConfig SMTModel -- ^ Prover returned unknown, with a potential (possibly bogus) model + | ProofError SMTConfig [String] -- ^ Prover errored out + | TimeOut SMTConfig -- ^ Computation timed out (see the 'timeout' combinator) + +-- | A script, to be passed to the solver. +data SMTScript = SMTScript { + scriptBody :: String -- ^ Initial feed + , scriptModel :: Maybe String -- ^ Optional continuation script, if the result is sat + } + +-- | An SMT engine +type SMTEngine = SMTConfig -> Bool -> [(Quantifier, NamedSymVar)] -> [(String, UnintKind)] -> [Either SW (SW, [SW])] -> String -> IO SMTResult + +-- | Solvers that SBV is aware of +data Solver = Z3 + | Yices + | Boolector + | CVC4 + | MathSAT + deriving (Show, Enum, Bounded) + +-- | An SMT solver +data SMTSolver = SMTSolver { + name :: Solver -- ^ The solver in use + , executable :: String -- ^ The path to its executable + , options :: [String] -- ^ Options to provide to the solver + , engine :: SMTEngine -- ^ The solver engine, responsible for interpreting solver output + , xformExitCode :: ExitCode -> ExitCode -- ^ Should we re-interpret exit codes. Most solvers behave rationally, i.e., id will do. Some (like CVC4) don't. + , capabilities :: SolverCapabilities -- ^ Various capabilities of the solver + } + +instance Show SMTSolver where + show = show . name 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 @@ -50,6 +50,23 @@ import Data.SBV.BitVectors.Data import Data.SBV.Utils.Boolean +import Data.SBV.Provers.Prover (isSBranchFeasibleInState) + +-- 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 (isVacuous, prove) +import Data.SBV.SMT.SMT (ThmResult) + +-- | 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 +-- around pesky warnings.. +ghcBitSize :: Bits a => a -> Int +#if __GLASGOW_HASKELL__ >= 708 +ghcBitSize x = maybe (error "SBV.ghcBitSize: Unexpected non-finite usage!") id (bitSizeMaybe x) +#else +ghcBitSize = bitSize +#endif + noUnint :: String -> a noUnint x = error $ "Unexpected operation called on uninterpreted value: " ++ show x @@ -74,20 +91,20 @@ liftSym2B :: (State -> Kind -> SW -> SW -> IO SW) -> (CW -> CW -> Bool) -> (AlgReal -> AlgReal -> Bool) -> (Integer -> Integer -> Bool) -> (Float -> Float -> Bool) -> (Double -> Double -> Bool) -> SBV b -> SBV b -> SBool liftSym2B _ okCW opCR opCI opCF opCD (SBV _ (Left a)) (SBV _ (Left b)) | okCW a b = literal (liftCW2 opCR opCI opCF opCD noUnint2 a b) -liftSym2B opS _ _ _ _ _ a b = SBV (KBounded False 1) $ Right $ liftSW2 opS (KBounded False 1) a b +liftSym2B opS _ _ _ _ _ a b = SBV KBool $ Right $ liftSW2 opS KBool a b liftSym1Bool :: (State -> Kind -> SW -> IO SW) -> (Bool -> Bool) -> SBool -> SBool liftSym1Bool _ opC (SBV _ (Left a)) = literal $ opC $ cwToBool a -liftSym1Bool opS _ a = SBV (KBounded False 1) $ Right $ cache c +liftSym1Bool opS _ a = SBV KBool $ Right $ cache c where c st = do sw <- sbvToSW st a - opS st (KBounded False 1) sw + opS st KBool sw liftSym2Bool :: (State -> Kind -> SW -> SW -> IO SW) -> (Bool -> Bool -> Bool) -> SBool -> SBool -> SBool liftSym2Bool _ opC (SBV _ (Left a)) (SBV _ (Left b)) = literal (cwToBool a `opC` cwToBool b) -liftSym2Bool opS _ a b = SBV (KBounded False 1) $ Right $ cache c +liftSym2Bool opS _ a b = SBV KBool $ Right $ cache c where c st = do sw1 <- sbvToSW st a sw2 <- sbvToSW st b - opS st (KBounded False 1) sw1 sw2 + opS st KBool sw1 sw2 mkSymOpSC :: (SW -> SW -> Maybe SW) -> Op -> State -> Kind -> SW -> SW -> IO SW mkSymOpSC shortCut op st k a b = maybe (newExpr st k (SBVApp op [a, b])) return (shortCut a b) @@ -126,8 +143,8 @@ genMkSymVar k mbq (Just s) = genVar mbq k s instance SymWord Bool where - mkSymWord = genMkSymVar (KBounded False 1) - literal x = genLiteral (KBounded False 1) (if x then (1::Integer) else 0) + mkSymWord = genMkSymVar KBool + literal x = genLiteral KBool (if x then (1::Integer) else 0) fromCW = cwToBool mbMaxBound = Just maxBound mbMinBound = Just minBound @@ -730,6 +747,9 @@ | True = liftSym2 (mkSymOp XOr) (const (const True)) (noReal "xor") xor (noFloat "xor") (noDouble "xor") x y complement = liftSym1 (mkSymOp1 Not) (noRealUnary "complement") complement (noFloatUnary "complement") (noDoubleUnary "complement") bitSize _ = intSizeOf (undefined :: a) +#if __GLASGOW_HASKELL__ >= 708 + bitSizeMaybe _ = Just $ intSizeOf (undefined :: a) +#endif isSigned _ = hasSign (undefined :: a) bit i = 1 `shiftL` i shiftL x y @@ -743,12 +763,12 @@ rotateL x y | y < 0 = rotateR x (-y) | y == 0 = x - | isBounded x = let sz = bitSize x in liftSym1 (mkSymOp1 (Rol (y `mod` sz))) (noRealUnary "rotateL") (rot True sz y) (noFloatUnary "rotateL") (noDoubleUnary "rotateL") x + | isBounded x = let sz = ghcBitSize x in liftSym1 (mkSymOp1 (Rol (y `mod` sz))) (noRealUnary "rotateL") (rot True sz y) (noFloatUnary "rotateL") (noDoubleUnary "rotateL") x | True = shiftL x y -- for unbounded Integers, rotateL is the same as shiftL in Haskell rotateR x y | y < 0 = rotateL x (-y) | y == 0 = x - | isBounded x = let sz = bitSize x in liftSym1 (mkSymOp1 (Ror (y `mod` sz))) (noRealUnary "rotateR") (rot False sz y) (noFloatUnary "rotateR") (noDoubleUnary "rotateR") x + | isBounded x = let sz = ghcBitSize x in liftSym1 (mkSymOp1 (Ror (y `mod` sz))) (noRealUnary "rotateR") (rot False sz y) (noFloatUnary "rotateR") (noDoubleUnary "rotateR") x | True = shiftR x y -- for unbounded integers, rotateR is the same as shiftR in Haskell -- NB. testBit is *not* implementable on non-concrete symbolic words x `testBit` i @@ -806,7 +826,7 @@ sbvShiftLeft :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a sbvShiftLeft x i | isSigned i = error "sbvShiftLeft: shift amount should be unsigned" - | True = select [x `shiftL` k | k <- [0 .. bitSize x - 1]] 0 i + | True = select [x `shiftL` k | k <- [0 .. ghcBitSize x - 1]] 0 i -- | Generalization of 'shiftR', when the shift-amount is symbolic. Since Haskell's -- 'shiftR' only takes an 'Int' as the shift amount, it cannot be used when we have @@ -818,7 +838,7 @@ sbvShiftRight :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a sbvShiftRight x i | isSigned i = error "sbvShiftRight: shift amount should be unsigned" - | True = select [x `shiftR` k | k <- [0 .. bitSize x - 1]] 0 i + | True = select [x `shiftR` k | k <- [0 .. ghcBitSize x - 1]] 0 i -- | Arithmetic shift-right with a symbolic unsigned shift amount. This is equivalent -- to 'sbvShiftRight' when the argument is signed. However, if the argument is unsigned, @@ -853,14 +873,14 @@ fullMultiplier :: SIntegral a => SBV a -> SBV a -> (SBV a, SBV a) fullMultiplier a b | isSigned a = error "fullMultiplier: only works on unsigned numbers" - | True = (go (bitSize a) 0 a, a*b) + | True = (go (ghcBitSize a) 0 a, a*b) where go 0 p _ = p go n p x = let (c, p') = ite (lsb x) (fullAdder p b) (false, p) (o, p'') = shiftIn c p' (_, x') = shiftIn o x in go (n-1) p'' x' shiftIn k v = (lsb v, mask .|. (v `shiftR` 1)) - where mask = ite k (bit (bitSize v - 1)) 0 + where mask = ite k (bit (ghcBitSize v - 1)) 0 -- | Little-endian blasting of a word into its bits. Also see the 'FromBits' class. blastLE :: (Num a, Bits a, SymWord a) => SBV a -> [SBool] @@ -1125,6 +1145,24 @@ -- The idea is that use symbolicMerge if you know the condition is symbolic, -- otherwise use ite, if there's a chance it might be concrete. ite :: SBool -> a -> a -> a + -- | Branch on a condition, much like 'ite'. The exception is that SBV will + -- check to make sure if the test condition is feasible by making an external + -- call to the SMT solver. Note that this can be expensive, thus we shall use + -- a time-out value ('sBranchTimeOut'). There might be zero, one, or two such + -- external calls per 'sBranch' call: + -- + -- - If condition is statically known to be True/False: 0 calls + -- - In this case, we simply constant fold.. + -- + -- - If condition is determined to be unsatisfiable : 1 call + -- - In this case, we know then-branch is infeasible, so just take the else-branch + -- + -- - If condition is determined to be satisfable : 2 calls + -- - In this case, we know then-branch is feasible, but we still have to check if the else-branch is + -- + -- In summary, 'sBranch' calls can be expensive, but they can help with the so-called symbolic-termination + -- problem. See "Data.SBV.Examples.Misc.SBranch" for an example. + sBranch :: SBool -> a -> a -> a -- | Total indexing operation. @select xs default index@ is intuitively -- the same as @xs !! index@, except it evaluates to @default@ if @index@ -- overflows @@ -1133,6 +1171,7 @@ ite s a b | Just t <- unliteral s = if t then a else b | True = symbolicMerge s a b + sBranch s = ite (reduceInPathCondition s) -- NB. Earlier implementation of select used the binary-search trick -- on the index to chop down the search space. While that is a good trick -- in general, it doesn't work for SBV since we do not have any notion of @@ -1148,86 +1187,14 @@ -- SBV instance SymWord a => Mergeable (SBV a) where - -- the strict match and checking of literal equivalence is essential below, - -- as otherwise we risk hanging onto huge closures and blow stack! This is - -- against the feel that merging shouldn't look at branches if the test - -- expression is constant. However, it's OK to do it this way since we - -- expect "ite" to be used in such cases which already checks for that. That - -- is the use case of the symbolicMerge should be when the test is symbolic. - -- Of course, we do not have a way of enforcing that in the user code, but - -- at least our library code respects that invariant. - symbolicMerge t a@(SBV{}) b@(SBV{}) - | Just av <- unliteral a, Just bv <- unliteral b, rationalSBVCheck a b, av == bv - = a - | True - = SBV k $ Right $ cache c - where k = kindOf a - c st = do swt <- sbvToSW st t - case () of - () | swt == trueSW -> sbvToSW st a -- these two cases should never be needed as we expect symbolicMerge to be - () | swt == falseSW -> sbvToSW st b -- called with symbolic tests, but just in case.. - () -> do {- It is tempting to record the choice of the test expression here as we branch down to the 'then' and 'else' branches. That is, - when we evaluate 'a', we can make use of the fact that the test expression is True, and similarly we can use the fact that it - is False when b is evaluated. In certain cases this can cut down on symbolic simulation significantly, for instance if - repetitive decisions are made in a recursive loop. Unfortunately, the implementation of this idea is quite tricky, due to - our sharing based implementation. As the 'then' branch is evaluated, we will create many expressions that are likely going - to be "reused" when the 'else' branch is executed. But, it would be *dead wrong* to share those values, as they were "cached" - under the incorrect assumptions. To wit, consider the following: - - foo x y = ite (y .== 0) k (k+1) - where k = ite (y .== 0) x (x+1) - - When we reduce the 'then' branch of the first ite, we'd record the assumption that y is 0. But while reducing the 'then' branch, we'd - like to share 'k', which would evaluate (correctly) to 'x' under the given assumption. When we backtrack and evaluate the 'else' - branch of the first ite, we'd see 'k' is needed again, and we'd look it up from our sharing map to find (incorrectly) that its value - is 'x', which was stored there under the assumption that y was 0, which no longer holds. Clearly, this is unsound. - - A sound implementation would have to precisely track which assumptions were active at the time expressions get shared. That is, - in the above example, we should record that the value of 'k' was cached under the assumption that 'y' is 0. While sound, this - approach unfortunately leads to significant loss of valid sharing when the value itself had nothing to do with the assumption itself. - To wit, consider: - - foo x y = ite (y .== 0) k (k+1) - where k = x+5 - - If we tracked the assumptions, we would recompute 'k' twice, since the branch assumptions would differ. Clearly, there is no need to - re-compute 'k' in this case since its value is independent of y. Note that the whole SBV performance story is based on agressive sharing, - and losing that would have other significant ramifications. - - The "proper" solution would be to track, with each shared computation, precisely which assumptions it actually *depends* on, rather - than blindly recording all the assumptions present at that time. SBV's symbolic simulation engine clearly has all the info needed to do this - properly, but the implementation is not straightforward at all. For each subexpression, we would need to chase down its dependencies - transitively, which can require a lot of scanning of the generated program causing major slow-down; thus potentially defeating the - whole purpose of sharing in the first place. - - Design choice: Keep it simple, and simply do not track the assumption at all. This will maximize sharing, at the cost of evaluating - unreachable branches. I think the simplicity is more important at this point than efficiency. - - Also note that the user can avoid most such issues by properly combining if-then-else's with common conditions together. That is, the - first program above should be written like this: - - foo x y = ite (y .== 0) x (x+2) - - In general, the following transformations should be done whenever possible: - - ite e1 (ite e1 e2 e3) e4 --> ite e1 e2 e4 - ite e1 e2 (ite e1 e3 e4) --> ite e1 e2 e4 - - This is in accordance with the general rule-of-thumb stating conditionals should be avoided as much as possible. However, we might prefer - the following: - - ite e1 (f e2 e4) (f e3 e5) --> f (ite e1 e2 e3) (ite e1 e4 e5) - - especially if this expression happens to be inside 'f's body itself (i.e., when f is recursive), since it reduces the number of - recursive calls. Clearly, programming with symbolic simulation in mind is another kind of beast alltogether. - -} - swa <- sbvToSW st a -- evaluate 'then' branch - swb <- sbvToSW st b -- evaluate 'else' branch - case () of -- merge: - () | swa == swb -> return swa - () | swa == trueSW && swb == falseSW -> return swt - () | swa == falseSW && swb == trueSW -> newExpr st k (SBVApp Not [swt]) - () -> newExpr st k (SBVApp Ite [swt, swa, swb]) + -- sBranch is essentially the default method, but we are careful in not forcing the + -- arguments as ite does, since sBranch is expected to be used when one of the + -- branches is likely to be in a branch that's recursively evaluated. + sBranch s a b + | Just t <- unliteral sReduced = if t then a else b + | True = symbolicWordMerge False sReduced a b + where sReduced = reduceInPathCondition s + symbolicMerge = symbolicWordMerge True -- Custom version of select that translates to SMT-Lib tables at the base type of words select xs err ind | SBV _ (Left c) <- ind = case cwVal c of @@ -1247,6 +1214,86 @@ let len = length xs newExpr st kElt (SBVApp (LkUp (idx, kInd, kElt, len) swi swe) []) +-- symbolically merge two SBV words, based on the boolean condition given. +-- The first argument controls whether we want to reduce the branches +-- separately first, which avoids hanging onto huge thunks, and is usually +-- the right thing to do for ite. But we precisely do not want to do that +-- in case of sBranch, which is the case when one of the branches (typically +-- the "else" branch is hanging off of a recursive call. +symbolicWordMerge :: SymWord a => Bool -> SBool -> SBV a -> SBV a -> SBV a +symbolicWordMerge force t a b + | force, Just av <- unliteral a, Just bv <- unliteral b, rationalSBVCheck a b, av == bv + = a + | True + = SBV k $ Right $ cache c + where k = kindOf a + c st = do swt <- sbvToSW st t + case () of + () | swt == trueSW -> sbvToSW st a -- these two cases should never be needed as we expect symbolicMerge to be + () | swt == falseSW -> sbvToSW st b -- called with symbolic tests, but just in case.. + () -> do {- It is tempting to record the choice of the test expression here as we branch down to the 'then' and 'else' branches. That is, + when we evaluate 'a', we can make use of the fact that the test expression is True, and similarly we can use the fact that it + is False when b is evaluated. In certain cases this can cut down on symbolic simulation significantly, for instance if + repetitive decisions are made in a recursive loop. Unfortunately, the implementation of this idea is quite tricky, due to + our sharing based implementation. As the 'then' branch is evaluated, we will create many expressions that are likely going + to be "reused" when the 'else' branch is executed. But, it would be *dead wrong* to share those values, as they were "cached" + under the incorrect assumptions. To wit, consider the following: + + foo x y = ite (y .== 0) k (k+1) + where k = ite (y .== 0) x (x+1) + + When we reduce the 'then' branch of the first ite, we'd record the assumption that y is 0. But while reducing the 'then' branch, we'd + like to share 'k', which would evaluate (correctly) to 'x' under the given assumption. When we backtrack and evaluate the 'else' + branch of the first ite, we'd see 'k' is needed again, and we'd look it up from our sharing map to find (incorrectly) that its value + is 'x', which was stored there under the assumption that y was 0, which no longer holds. Clearly, this is unsound. + + A sound implementation would have to precisely track which assumptions were active at the time expressions get shared. That is, + in the above example, we should record that the value of 'k' was cached under the assumption that 'y' is 0. While sound, this + approach unfortunately leads to significant loss of valid sharing when the value itself had nothing to do with the assumption itself. + To wit, consider: + + foo x y = ite (y .== 0) k (k+1) + where k = x+5 + + If we tracked the assumptions, we would recompute 'k' twice, since the branch assumptions would differ. Clearly, there is no need to + re-compute 'k' in this case since its value is independent of y. Note that the whole SBV performance story is based on agressive sharing, + and losing that would have other significant ramifications. + + The "proper" solution would be to track, with each shared computation, precisely which assumptions it actually *depends* on, rather + than blindly recording all the assumptions present at that time. SBV's symbolic simulation engine clearly has all the info needed to do this + properly, but the implementation is not straightforward at all. For each subexpression, we would need to chase down its dependencies + transitively, which can require a lot of scanning of the generated program causing major slow-down; thus potentially defeating the + whole purpose of sharing in the first place. + + Design choice: Keep it simple, and simply do not track the assumption at all. This will maximize sharing, at the cost of evaluating + unreachable branches. I think the simplicity is more important at this point than efficiency. + + Also note that the user can avoid most such issues by properly combining if-then-else's with common conditions together. That is, the + first program above should be written like this: + + foo x y = ite (y .== 0) x (x+2) + + In general, the following transformations should be done whenever possible: + + ite e1 (ite e1 e2 e3) e4 --> ite e1 e2 e4 + ite e1 e2 (ite e1 e3 e4) --> ite e1 e2 e4 + + This is in accordance with the general rule-of-thumb stating conditionals should be avoided as much as possible. However, we might prefer + the following: + + ite e1 (f e2 e4) (f e3 e5) --> f (ite e1 e2 e3) (ite e1 e4 e5) + + especially if this expression happens to be inside 'f's body itself (i.e., when f is recursive), since it reduces the number of + recursive calls. Clearly, programming with symbolic simulation in mind is another kind of beast alltogether. + -} + swa <- sbvToSW (st `extendPathCondition` (&&& t)) a -- evaluate 'then' branch + swb <- sbvToSW (st `extendPathCondition` (&&& bnot t)) b -- evaluate 'else' branch + case () of -- merge: + () | swa == swb -> return swa + () | swa == trueSW && swb == falseSW -> return swt + () | swa == falseSW && swb == trueSW -> newExpr st k (SBVApp Not [swt]) + () -> newExpr st k (SBVApp Ite [swt, swa, swb]) + -- Unit instance Mergeable () where symbolicMerge _ _ _ = () @@ -1348,10 +1395,10 @@ -- SArrays are both "EqSymbolic" and "Mergeable" instance EqSymbolic (SArray a b) where - (SArray _ a) .== (SArray _ b) = SBV (KBounded False 1) $ Right $ cache c + (SArray _ a) .== (SArray _ b) = SBV KBool $ Right $ cache c where c st = do ai <- uncacheAI a st bi <- uncacheAI b st - newExpr st (KBounded False 1) (SBVApp (ArrEq ai bi) []) + newExpr st KBool (SBVApp (ArrEq ai bi) []) instance SymWord b => Mergeable (SArray a b) where symbolicMerge = mergeArrays @@ -1408,12 +1455,6 @@ | True = do newUninterpreted st nm (SBVType [ka]) (fst `fmap` mbCgData) newExpr st ka $ SBVApp (Uninterpreted nm) [] --- Forcing an argument; this is a necessary evil to make sure all the arguments --- to an uninterpreted function are evaluated before called; the semantics of --- such functions is necessarily strict; deviating from Haskell's -forceArg :: SW -> IO () -forceArg (SW k n) = k `seq` n `seq` return () - -- Functions of one argument instance (SymWord b, HasKind a) => Uninterpreted (SBV b -> SBV a) where sbvUninterpret mbCgData nm = f @@ -1427,7 +1468,7 @@ result st | Just (_, v) <- mbCgData, inProofMode st = sbvToSW st (v arg0) | True = do newUninterpreted st nm (SBVType [kb, ka]) (fst `fmap` mbCgData) sw0 <- sbvToSW st arg0 - mapM_ forceArg [sw0] + mapM_ forceSWArg [sw0] newExpr st ka $ SBVApp (Uninterpreted nm) [sw0] -- Functions of two arguments @@ -1445,7 +1486,7 @@ | True = do newUninterpreted st nm (SBVType [kc, kb, ka]) (fst `fmap` mbCgData) sw0 <- sbvToSW st arg0 sw1 <- sbvToSW st arg1 - mapM_ forceArg [sw0, sw1] + mapM_ forceSWArg [sw0, sw1] newExpr st ka $ SBVApp (Uninterpreted nm) [sw0, sw1] -- Functions of three arguments @@ -1465,7 +1506,7 @@ sw0 <- sbvToSW st arg0 sw1 <- sbvToSW st arg1 sw2 <- sbvToSW st arg2 - mapM_ forceArg [sw0, sw1, sw2] + mapM_ forceSWArg [sw0, sw1, sw2] newExpr st ka $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2] -- Functions of four arguments @@ -1487,7 +1528,7 @@ sw1 <- sbvToSW st arg1 sw2 <- sbvToSW st arg2 sw3 <- sbvToSW st arg3 - mapM_ forceArg [sw0, sw1, sw2, sw3] + mapM_ forceSWArg [sw0, sw1, sw2, sw3] newExpr st ka $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2, sw3] -- Functions of five arguments @@ -1511,7 +1552,7 @@ sw2 <- sbvToSW st arg2 sw3 <- sbvToSW st arg3 sw4 <- sbvToSW st arg4 - mapM_ forceArg [sw0, sw1, sw2, sw3, sw4] + mapM_ forceSWArg [sw0, sw1, sw2, sw3, sw4] newExpr st ka $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2, sw3, sw4] -- Functions of six arguments @@ -1537,7 +1578,7 @@ sw3 <- sbvToSW st arg3 sw4 <- sbvToSW st arg4 sw5 <- sbvToSW st arg5 - mapM_ forceArg [sw0, sw1, sw2, sw3, sw4, sw5] + mapM_ forceSWArg [sw0, sw1, sw2, sw3, sw4, sw5] newExpr st ka $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2, sw3, sw4, sw5] -- Functions of seven arguments @@ -1566,7 +1607,7 @@ sw4 <- sbvToSW st arg4 sw5 <- sbvToSW st arg5 sw6 <- sbvToSW st arg6 - mapM_ forceArg [sw0, sw1, sw2, sw3, sw4, sw5, sw6] + 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 @@ -1603,7 +1644,39 @@ sbvUninterpret mbCgData nm = let f = sbvUninterpret (uc7 `fmap` mbCgData) nm in \(arg0, arg1, arg2, arg3, arg4, arg5, arg6) -> f arg0 arg1 arg2 arg3 arg4 arg5 arg6 where uc7 (cs, fn) = (cs, \a b c d e f g -> fn (a, b, c, d, e, f, g)) --- | Adding arbitrary constraints. +-- | Adding arbitrary constraints. When adding constraints, one has to be careful about +-- making sure they are not inconsistent. The function 'isVacuous' can be use for this purpose. +-- Here is an example. Consider the following predicate: +-- +-- >>> let pred = do { x <- forall "x"; constrain $ x .< x; return $ x .>= (5 :: SWord8) } +-- +-- This predicate asserts that all 8-bit values are larger than 5, subject to the constraint that the +-- values considered satisfy @x .< x@, i.e., they are less than themselves. Since there are no values that +-- satisfy this constraint, the proof will pass vacuously: +-- +-- >>> prove pred +-- Q.E.D. +-- +-- We can use 'isVacuous' to make sure to see that the pass was vacuous: +-- +-- >>> isVacuous pred +-- True +-- +-- While the above example is trivial, things can get complicated if there are multiple constraints with +-- non-straightforward relations; so if constraints are used one should make sure to check the predicate +-- is not vacuously true. Here's an example that is not vacuous: +-- +-- >>> let pred' = do { x <- forall "x"; constrain $ x .> 6; return $ x .>= (5 :: SWord8) } +-- +-- This time the proof passes as expected: +-- +-- >>> prove pred' +-- Q.E.D. +-- +-- And the proof is not vacuous: +-- +-- >>> isVacuous pred' +-- False constrain :: SBool -> Symbolic () constrain c = addConstraint Nothing c (bnot c) @@ -1613,6 +1686,25 @@ pConstrain :: Double -> SBool -> Symbolic () pConstrain t c = addConstraint (Just t) c (bnot c) +-- | Boolean symbolic reduction. See if we can reduce a boolean condition to true/false +-- using the path context information, by making external calls to the SMT solvers. Used in the +-- implementation of 'sBranch'. +reduceInPathCondition :: SBool -> SBool +reduceInPathCondition b + | isConcrete b = b -- No reduction is needed, already a concrete value + | True = SBV k $ Right $ cache c + where k = kindOf b + c st = do -- Now that we know our boolean is not obviously true/false. Need to make an external + -- call to the SMT solver to see if we can prove it is necessarily one of those + let pc = getPathCondition st + satTrue <- isSBranchFeasibleInState st "then" (pc &&& b) + if not satTrue + then return falseSW -- condition is not satisfiable; so it must be necessarily False. + else do satFalse <- isSBranchFeasibleInState st "else" (pc &&& bnot b) + if not satFalse -- negation of the condition is not satisfiable; so it must be necessarily True. + then return trueSW + else sbvToSW st b -- condition is not necessarily always True/False. So, keep symbolic. + -- Quickcheck interface on symbolic-booleans.. instance Testable SBool where property (SBV _ (Left b)) = property (cwToBool b) @@ -1650,6 +1742,10 @@ let xsbv = SBV (kindOf x) (Right (cache (const (return xsw)))) res = f xsbv sbvToSW st res + +-- We use 'isVacuous' and 'prove' only for the "test" section in this file, and GHC complains about that. So, this shuts it up. +__unused :: a +__unused = error "__unused" (isVacuous :: SBool -> IO Bool) (prove :: SBool -> IO ThmResult) {-# ANN module "HLint: ignore Eta reduce" #-} {-# ANN module "HLint: ignore Reduce duplication" #-} diff --git a/Data/SBV/BitVectors/PrettyNum.hs b/Data/SBV/BitVectors/PrettyNum.hs --- a/Data/SBV/BitVectors/PrettyNum.hs +++ b/Data/SBV/BitVectors/PrettyNum.hs @@ -27,7 +27,6 @@ import Numeric (showIntAtBase, showHex, readInt) import Data.SBV.BitVectors.Data -import Data.SBV.BitVectors.Model () -- instances only -- | PrettyNum class captures printing of numbers in hex and binary formats; also supporting negative numbers. -- diff --git a/Data/SBV/BitVectors/SignCast.hs b/Data/SBV/BitVectors/SignCast.hs --- a/Data/SBV/BitVectors/SignCast.hs +++ b/Data/SBV/BitVectors/SignCast.hs @@ -81,6 +81,7 @@ | Just c <- unliteral x = literal $ fromIntegral c | True = SBV k (Right (cache y)) where k = case kindOf x of + KBool -> error "Data.SBV.SignCast.genericSign: Called on boolean value" KBounded False n -> KBounded True n KBounded True _ -> error "Data.SBV.SignCast.genericSign: Called on signed value" KUnbounded -> error "Data.SBV.SignCast.genericSign: Called on unbounded value" @@ -97,6 +98,7 @@ | Just c <- unliteral x = literal $ fromIntegral c | True = SBV k (Right (cache y)) where k = case kindOf x of + KBool -> error "Data.SBV.SignCast.genericUnSign: Called on boolean value" KBounded True n -> KBounded False n KBounded False _ -> error "Data.SBV.SignCast.genericUnSign: Called on unsigned value" KUnbounded -> error "Data.SBV.SignCast.genericUnSign: Called on unbounded value" diff --git a/Data/SBV/Compilers/C.hs b/Data/SBV/Compilers/C.hs --- a/Data/SBV/Compilers/C.hs +++ b/Data/SBV/Compilers/C.hs @@ -161,6 +161,7 @@ -- | The printf specifier for the type specifier :: CgConfig -> SW -> Doc specifier cfg sw = case kindOf sw of + KBool -> spec (False, 1) KBounded b i -> spec (b, i) KUnbounded -> spec (True, fromJust (cgInteger cfg)) KReal -> specF (fromJust (cgReal cfg)) @@ -442,7 +443,7 @@ len (KFloat{}) = 6 -- SFloat len (KDouble{}) = 7 -- SDouble len (KUnbounded{}) = 8 - len (KBounded False 1) = 5 -- SBool + len KBool = 5 -- SBool len (KBounded False n) = 5 + length (show n) -- SWordN len (KBounded True n) = 4 + length (show n) -- SIntN len (KUninterpreted s) = die $ "Uninterpreted sort: " ++ s @@ -498,8 +499,8 @@ p (Shr i) [a] = shift False i a (head opArgs) p Not [a] = case kindOf (head opArgs) of -- be careful about booleans, bitwise complement is not correct for them! - KBounded False 1 -> text "!" <> a - _ -> text "~" <> a + KBool -> text "!" <> a + _ -> text "~" <> a p Ite [a, b, c] = a <+> text "?" <+> b <+> text ":" <+> c p (LkUp (t, k, _, len) ind def) [] | not rtc = lkUp -- ignore run-time-checks per user request @@ -516,6 +517,7 @@ canOverflow True sz = (2::Integer)^(sz-1)-1 >= fromIntegral len canOverflow False sz = (2::Integer)^sz -1 >= fromIntegral len (needsCheckL, needsCheckR) = case k of + KBool -> (False, canOverflow False (1::Int)) KBounded sg sz -> (sg, canOverflow sg sz) KReal -> die "array index with real value" KFloat -> die "array index with float value" diff --git a/Data/SBV/Compilers/CodeGen.hs b/Data/SBV/Compilers/CodeGen.hs --- a/Data/SBV/Compilers/CodeGen.hs +++ b/Data/SBV/Compilers/CodeGen.hs @@ -16,6 +16,7 @@ import Control.Monad.Trans import Control.Monad.State.Lazy +import Control.Applicative (Applicative) import Data.Char (toLower, isSpace) import Data.List (nub, isPrefixOf, intercalate, (\\)) import System.Directory (createDirectory, doesDirectoryExist, doesFileExist) @@ -75,7 +76,7 @@ -- reference parameters (for returning composite values in languages such as C), -- and return values. newtype SBVCodeGen a = SBVCodeGen (StateT CgState Symbolic a) - deriving (Monad, MonadIO, MonadState CgState) + deriving (Applicative, Functor, Monad, MonadIO, MonadState CgState) -- | Reach into symbolic monad from code-generation liftSymbolic :: Symbolic a -> SBVCodeGen a @@ -109,7 +110,7 @@ | CgLongDouble -- ^ @long double@ deriving Eq --- As they would be used in a C program +-- | 'Show' instance for 'cgSRealType' displays values as they would be used in a C program instance Show CgSRealType where show CgFloat = "float" show CgDouble = "double" @@ -217,6 +218,7 @@ isCgMakefile CgMakefile{} = True isCgMakefile _ = False +-- | A simple way to print bundles, mostly for debugging purposes. instance Show CgPgmBundle where show (CgPgmBundle _ fs) = intercalate "\n" $ map showFile fs where showFile :: (FilePath, (CgPgmKind, [Doc])) -> String diff --git a/Data/SBV/Examples/BitPrecise/Legato.hs b/Data/SBV/Examples/BitPrecise/Legato.hs --- a/Data/SBV/Examples/BitPrecise/Legato.hs +++ b/Data/SBV/Examples/BitPrecise/Legato.hs @@ -79,6 +79,7 @@ -- | Programs are essentially state transformers (on the machine state) type Program = Mostek -> Mostek +-- | 'Mergeable' instance of 'Mostek' simply pushes the merging into record fields. instance Mergeable Mostek where symbolicMerge b m1 m2 = Mostek { memory = symbolicMerge b (memory m1) (memory m2) , registers = symbolicMerge b (registers m1) (registers m2) diff --git a/Data/SBV/Examples/BitPrecise/PrefixSum.hs b/Data/SBV/Examples/BitPrecise/PrefixSum.hs --- a/Data/SBV/Examples/BitPrecise/PrefixSum.hs +++ b/Data/SBV/Examples/BitPrecise/PrefixSum.hs @@ -263,8 +263,8 @@ -- s18 ladnerFischerTrace :: Int -> IO () ladnerFischerTrace n = gen >>= print - where gen = runSymbolic True $ do args :: [SWord8] <- mkForallVars n - mapM_ output $ lf (0, (+)) args + where gen = runSymbolic (True, Nothing) $ do args :: [SWord8] <- mkForallVars n + mapM_ output $ lf (0, (+)) args -- | Trace generator for the reference spec. It clearly demonstrates that the reference -- implementation fewer operations, but is not parallelizable at all: @@ -308,7 +308,7 @@ -- scanlTrace :: Int -> IO () scanlTrace n = gen >>= print - where gen = runSymbolic True $ do args :: [SWord8] <- mkForallVars n - mapM_ output $ ps (0, (+)) args + where gen = runSymbolic (True, Nothing) $ do args :: [SWord8] <- mkForallVars n + mapM_ output $ ps (0, (+)) args {-# ANN module "HLint: ignore Reduce duplication" #-} diff --git a/Data/SBV/Examples/CodeGeneration/Uninterpreted.hs b/Data/SBV/Examples/CodeGeneration/Uninterpreted.hs --- a/Data/SBV/Examples/CodeGeneration/Uninterpreted.hs +++ b/Data/SBV/Examples/CodeGeneration/Uninterpreted.hs @@ -13,6 +13,8 @@ -- purposes, such as efficiency, or reliability. ----------------------------------------------------------------------------- +{-# LANGUAGE CPP #-} + module Data.SBV.Examples.CodeGeneration.Uninterpreted where import Data.SBV @@ -34,7 +36,14 @@ -- the Haskell code we'd like SBV to use when running inside Haskell or when -- translated to SMTLib for verification purposes. This is good old Haskell -- code, as one would typically write. - hCode x = select [x * literal (bit b) | b <- [0.. bitSize x - 1]] (literal 0) + hCode x = select [x * literal (bit b) | b <- [0.. bs x - 1]] (literal 0) +#if __GLASGOW_HASKELL__ >= 708 + bs x = maybe (error "SBV.Example.CodeGeneration.Uninterpreted.shiftLeft: Unexpected non-finite usage!") id (bitSizeMaybe x) +#else + bs = bitSize +#endif + + -- | Test function that uses shiftLeft defined above. When used as a normal Haskell function -- or in verification the definition is fully used, i.e., no uninterpretation happens. To wit, diff --git a/Data/SBV/Examples/Misc/Floating.hs b/Data/SBV/Examples/Misc/Floating.hs --- a/Data/SBV/Examples/Misc/Floating.hs +++ b/Data/SBV/Examples/Misc/Floating.hs @@ -116,11 +116,11 @@ -- -- >>> multInverse -- Falsifiable. Counter-example: --- a = 1.3999060872492817e-308 :: SDouble +-- a = 1.3625818045773776e-308 :: SDouble -- -- Indeed, we have: -- --- >>> let a = 1.3999060872492817e-308 :: Double +-- >>> let a = 1.3625818045773776e-308 :: Double -- >>> a * (1/a) -- 0.9999999999999999 multInverse :: IO ThmResult diff --git a/Data/SBV/Examples/Misc/SBranch.hs b/Data/SBV/Examples/Misc/SBranch.hs new file mode 100644 --- /dev/null +++ b/Data/SBV/Examples/Misc/SBranch.hs @@ -0,0 +1,73 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Data.SBV.Examples.Misc.SBranch +-- Copyright : (c) Levent Erkok +-- License : BSD3 +-- Maintainer : erkokl@gmail.com +-- Stability : experimental +-- +-- Illustrates the use of 'sBranch', as a means of dealing with certain cases +-- of the symbolic-termination problem. +----------------------------------------------------------------------------- + +module Data.SBV.Examples.Misc.SBranch where + +import Data.SBV + +-- | A fast implementation of population-count. Note that SBV already provides +-- this functionality via 'sbvPopCount', using simple expansion and counting +-- algorithm. 'sbvPopCount' is linear in the size of the input, i.e., a 32-bit +-- word would take 32 additions. This implementation here is /faster/ in the +-- sense that it takes as many additions as there are set-bits in the given word. +-- +-- Of course, the issue is that this definition is recursive, and the usual +-- definition via 'ite' would never symbolically terminate: Recursion is done +-- on the input argument: In each recursive call, we /reduce/ the value @n@ +-- to @n .&. (n-1)@. This eliminates one set-bit in the input. However, this +-- claim is far from obvious. By the use of 'sBranch' we tell SBV to call +-- the SMT solver in each test to ensure we only evaluate the branches we need, +-- thus avoiding the symbolic-termination issue. In a sense, the SMT solvers +-- proves that the implementation terminates for all valid inputs. +-- +-- Note that replacing 'sBranch' in this implementation with 'ite' would cause +-- symbolic-termination to loop forever. Of course, this does /not/ mean that +-- 'sBranch' is fast: It is costly to make external calls to the solver for +-- each branch, so use with care. +bitCount :: SWord32 -> SWord8 +bitCount = go 0 + where go c n = sBranch (n .== 0) c (go (c+1) (n .&. (n-1))) + +-- | Prove that the 'bitCount' function implemented here is equivalent to +-- the internal "slower" implementation. We have: +-- +-- >>> prop +-- Q.E.D. +prop :: IO ThmResult +prop = prove $ \n -> bitCount n .== sbvPopCount n + +-- | Illustrates the use of path-conditions in avoiding infeasible paths in symbolic +-- simulation. If we used 'ite' instead of 'sBranch' in the else-branch of the +-- implementation of 'path' symbolic simulation would have encountered the 'error' call, and +-- hence would have failed. But 'sBranch' keeps track of the path condition, and can +-- successfully determine that this path will never be taken, and hence avoids the problem. +-- Note that we can freely mix/match 'ite' and 'sBranch' calls; path conditions will be +-- tracked in both cases. In fact, use of 'ite' is advisable if we know for a fact that +-- both branches are feasible, as it avoids the external call. 'sBranch' will have the +-- same result, albeit it'll cost more. +path :: SWord8 -> SWord8 +path x = ite (x .> 5) + 10 + (sBranch (x .> 10) + (error "this case is not reachable!") -- NB. x .> 5 fails, so can't be .> 10 here + 20) + +-- | Prove that 'path' always produces either @10@ or @20@, i.e., symbolic simulation will +-- not fail due to the 'error' call. We have: +-- +-- >>> pathCheck +-- Q.E.D. +-- +-- Were we to use 'ite' instead of 'sBranch' in the implementation of 'path', this expression +-- would have caused an exception to be raised at symbolic simulation time. +pathCheck :: IO ThmResult +pathCheck = prove $ \n -> let pn = path n in pn .== 10 ||| pn .== 20 diff --git a/Data/SBV/Examples/Polynomials/Polynomials.hs b/Data/SBV/Examples/Polynomials/Polynomials.hs --- a/Data/SBV/Examples/Polynomials/Polynomials.hs +++ b/Data/SBV/Examples/Polynomials/Polynomials.hs @@ -37,22 +37,22 @@ -- Note that the irreducible itself is not in GF28! It has a degree of 8. -- -- NB. You can use the 'showPoly' function to print polynomials nicely, as a mathematician would write. -(<*>) :: GF28 -> GF28 -> GF28 -a <*> b = pMult (a, b, [8, 4, 3, 1, 0]) +gfMult :: GF28 -> GF28 -> GF28 +a `gfMult` b = pMult (a, b, [8, 4, 3, 1, 0]) -- | States that the unit polynomial @1@, is the unit element multUnit :: GF28 -> SBool -multUnit x = (x <*> unit) .== x +multUnit x = (x `gfMult` unit) .== x where unit = polynomial [0] -- x@0 -- | States that multiplication is commutative multComm :: GF28 -> GF28 -> SBool -multComm x y = (x <*> y) .== (y <*> x) +multComm x y = (x `gfMult` y) .== (y `gfMult` x) -- | States that multiplication is associative, note that associativity -- proofs are notoriously hard for SAT/SMT solvers multAssoc :: GF28 -> GF28 -> GF28 -> SBool -multAssoc x y z = ((x <*> y) <*> z) .== (x <*> (y <*> z)) +multAssoc x y z = ((x `gfMult` y) `gfMult` z) .== (x `gfMult` (y `gfMult` z)) -- | States that the usual multiplication rule holds over GF(2^n) polynomials -- Checks: @@ -65,7 +65,7 @@ -- defined to be 0 and the remainder is the numerator. -- (Note that addition is simply `xor` in GF(2^8).) polyDivMod :: GF28 -> GF28 -> SBool -polyDivMod x y = ite (y .== 0) ((0, x) .== (a, b)) (x .== y <*> a `xor` b) +polyDivMod x y = ite (y .== 0) ((0, x) .== (a, b)) (x .== (y `gfMult` a) `xor` b) where (a, b) = x `pDivMod` y -- | Queries diff --git a/Data/SBV/Examples/Puzzles/U2Bridge.hs b/Data/SBV/Examples/Puzzles/U2Bridge.hs --- a/Data/SBV/Examples/Puzzles/U2Bridge.hs +++ b/Data/SBV/Examples/Puzzles/U2Bridge.hs @@ -91,6 +91,8 @@ , lLarry = here } +-- | Mergeable instance for 'Status' simply walks down the structure fields and +-- merges them. instance Mergeable Status where symbolicMerge t s1 s2 = Status { time = symbolicMerge t (time s1) (time s2) , flash = symbolicMerge t (flash s1) (flash s2) @@ -103,6 +105,8 @@ -- | A puzzle move is modeled as a state-transformer type Move a = State Status a +-- | Mergeable instance for 'Move' simply pushes the merging the data after run of each branch +-- starting from the same state. instance Mergeable a => Mergeable (Move a) where symbolicMerge t a b = do s <- get @@ -198,6 +202,8 @@ zigZag _ [] = true zigZag w (f:rest) = w .== f &&& zigZag (bnot w) rest +-- | The SatModel instance makes it easy to build models, mapping words to U2 members +-- in the way we designated. instance SatModel U2Member where parseCWs as = cvtModel cvtCW $ parseCWs as where cvtCW :: Word8 -> Maybe U2Member diff --git a/Data/SBV/Examples/Uninterpreted/Deduce.hs b/Data/SBV/Examples/Uninterpreted/Deduce.hs --- a/Data/SBV/Examples/Uninterpreted/Deduce.hs +++ b/Data/SBV/Examples/Uninterpreted/Deduce.hs @@ -28,7 +28,11 @@ -- | The uninterpreted sort 'B', corresponding to the carrier. data B = B deriving (Eq, Ord, Data, Typeable) + +-- | Default instance declaration for 'SymWord' instance SymWord B + +-- | Default instance declaration for 'HasKind' instance HasKind B -- | Handy shortcut for the type of symbolic values over 'B' diff --git a/Data/SBV/Examples/Uninterpreted/Sort.hs b/Data/SBV/Examples/Uninterpreted/Sort.hs --- a/Data/SBV/Examples/Uninterpreted/Sort.hs +++ b/Data/SBV/Examples/Uninterpreted/Sort.hs @@ -26,6 +26,8 @@ -- declare them as such. Note that, starting with GHC 7.6.1, we will -- be able to simply derive these classes as well. (See .) instance SymWord Q + +-- | 'HasKind' instance is again straightforward, no specific implementation needed. instance HasKind Q -- | Declare an uninterpreted function that works over Q's diff --git a/Data/SBV/Examples/Uninterpreted/UISortAllSat.hs b/Data/SBV/Examples/Uninterpreted/UISortAllSat.hs --- a/Data/SBV/Examples/Uninterpreted/UISortAllSat.hs +++ b/Data/SBV/Examples/Uninterpreted/UISortAllSat.hs @@ -26,9 +26,11 @@ | Cons Int L deriving (Eq, Ord, Data, Typeable) --- | Declare instances to make 'L' a usable uninterpreted sort. Note that default --- definitions suffice in each case. +-- | Declare instances to make 'L' a usable uninterpreted sort. First we need the +-- 'SymWord' instance, with the default definition sufficing. instance SymWord L + +-- | Similarly, 'HasKind's default implementation is sufficient. instance HasKind L -- | An uninterpreted "classify" function. Really, we only care about diff --git a/Data/SBV/Provers/Boolector.hs b/Data/SBV/Provers/Boolector.hs --- a/Data/SBV/Provers/Boolector.hs +++ b/Data/SBV/Provers/Boolector.hs @@ -29,7 +29,7 @@ -- The default options are @\"-m --smt2\"@. You can use the @SBV_BOOLECTOR_OPTIONS@ environment variable to override the options. boolector :: SMTSolver boolector = SMTSolver { - name = "boolector" + name = Boolector , executable = "boolector" , options = ["-m", "--smt2"] , engine = \cfg _isSat qinps modelMap _skolemMap pgm -> do diff --git a/Data/SBV/Provers/CVC4.hs b/Data/SBV/Provers/CVC4.hs --- a/Data/SBV/Provers/CVC4.hs +++ b/Data/SBV/Provers/CVC4.hs @@ -30,7 +30,7 @@ -- The default options are @\"--lang smt\"@. You can use the @SBV_CVC4_OPTIONS@ environment variable to override the options. cvc4 :: SMTSolver cvc4 = SMTSolver { - name = "cvc4" + name = CVC4 , executable = "cvc4" , options = ["--lang", "smt"] , engine = \cfg isSat qinps modelMap skolemMap pgm -> do @@ -57,7 +57,7 @@ } } where zero :: Kind -> String - zero (KBounded False 1) = "#b0" + zero KBool = "false" zero (KBounded _ sz) = "#x" ++ replicate (sz `div` 4) '0' zero KUnbounded = "0" zero KReal = "0.0" diff --git a/Data/SBV/Provers/MathSAT.hs b/Data/SBV/Provers/MathSAT.hs --- a/Data/SBV/Provers/MathSAT.hs +++ b/Data/SBV/Provers/MathSAT.hs @@ -28,7 +28,7 @@ -- The default options are @\"-input=smt2\"@. You can use the @SBV_MATHSAT_OPTIONS@ environment variable to override the options. mathSAT :: SMTSolver mathSAT = SMTSolver { - name = "MathSAT" + name = MathSAT , executable = "mathsat" , options = ["-input=smt2"] , engine = \cfg _isSat qinps modelMap skolemMap pgm -> do @@ -56,7 +56,7 @@ } } where zero :: Kind -> String - zero (KBounded False 1) = "#b0" + zero KBool = "false" zero (KBounded _ sz) = "#x" ++ replicate (sz `div` 4) '0' zero KUnbounded = "0" zero KReal = "0.0" 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 @@ -18,30 +18,28 @@ SMTSolver(..), SMTConfig(..), Predicate, Provable(..) , ThmResult(..), SatResult(..), AllSatResult(..), SMTResult(..) , isSatisfiable, isSatisfiableWith, isTheorem, isTheoremWith - , Equality(..) , prove, proveWith , sat, satWith , allSat, allSatWith , isVacuous, isVacuousWith - , solve , SatModel(..), Modelable(..), displayModels, extractModels , getModelDictionaries, getModelValues, getModelUninterpretedValues , boolector, cvc4, yices, z3, mathSAT, defaultSMTCfg , compileToSMTLib, generateSMTBenchmarks - , sbvCheckSolverInstallation + , isSBranchFeasibleInState ) where -import Control.Monad (when, unless) -import Data.List (intercalate) -import Data.Maybe (mapMaybe) -import System.FilePath (addExtension, splitExtension) -import System.Time (getClockTime) -import System.IO.Unsafe (unsafeInterleaveIO) +import Control.Monad (when, unless) +import Control.Monad.Trans (liftIO) +import Data.List (intercalate) +import Data.Maybe (mapMaybe, fromMaybe) +import System.FilePath (addExtension, splitExtension) +import System.Time (getClockTime) +import System.IO.Unsafe (unsafeInterleaveIO) import qualified Data.Set as Set (Set, toList) import Data.SBV.BitVectors.Data -import Data.SBV.BitVectors.Model import Data.SBV.SMT.SMT import Data.SBV.SMT.SMTLib import qualified Data.SBV.Provers.Boolector as Boolector @@ -50,21 +48,21 @@ import qualified Data.SBV.Provers.Z3 as Z3 import qualified Data.SBV.Provers.MathSAT as MathSAT import Data.SBV.Utils.TDiff -import Data.SBV.Utils.Boolean mkConfig :: SMTSolver -> Bool -> [String] -> SMTConfig -mkConfig s isSMTLib2 tweaks = SMTConfig { verbose = False - , timing = False - , timeOut = Nothing - , printBase = 10 - , printRealPrec = 16 - , smtFile = Nothing - , solver = s - , solverTweaks = tweaks - , useSMTLib2 = isSMTLib2 - , satCmd = "(check-sat)" - , roundingMode = RoundNearestTiesToEven - , useLogic = Nothing +mkConfig s isSMTLib2 tweaks = SMTConfig { verbose = False + , timing = False + , sBranchTimeOut = Nothing + , timeOut = Nothing + , printBase = 10 + , printRealPrec = 16 + , smtFile = Nothing + , solver = s + , solverTweaks = tweaks + , useSMTLib2 = isSMTLib2 + , satCmd = "(check-sat)" + , roundingMode = RoundNearestTiesToEven + , useLogic = Nothing } -- | Default configuration for the Boolector SMT solver @@ -234,16 +232,6 @@ sat :: Provable a => a -> IO SatResult sat = satWith defaultSMTCfg --- | Form the symbolic conjunction of a given list of boolean conditions. Useful in expressing --- problems with constraints, like the following: --- --- @ --- do [x, y, z] <- sIntegers [\"x\", \"y\", \"z\"] --- solve [x .> 5, y + z .< x] --- @ -solve :: [SBool] -> Symbolic SBool -solve = return . bAnd - -- | 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. @@ -255,40 +243,8 @@ allSat :: Provable a => a -> IO AllSatResult allSat = allSatWith defaultSMTCfg --- | Check if the given constraints are satisfiable, equivalent to @'isVacuousWith' 'defaultSMTCfg'@. This --- call can be used to ensure that the specified constraints (via 'constrain') are satisfiable, i.e., that --- the proof involving these constraints is not passing vacuously. Here is an example. Consider the following --- predicate: --- --- >>> let pred = do { x <- forall "x"; constrain $ x .< x; return $ x .>= (5 :: SWord8) } --- --- This predicate asserts that all 8-bit values are larger than 5, subject to the constraint that the --- values considered satisfy @x .< x@, i.e., they are less than themselves. Since there are no values that --- satisfy this constraint, the proof will pass vacuously: --- --- >>> prove pred --- Q.E.D. --- --- We can use 'isVacuous' to make sure to see that the pass was vacuous: --- --- >>> isVacuous pred --- True --- --- While the above example is trivial, things can get complicated if there are multiple constraints with --- non-straightforward relations; so if constraints are used one should make sure to check the predicate --- is not vacuously true. Here's an example that is not vacuous: --- --- >>> let pred' = do { x <- forall "x"; constrain $ x .> 6; return $ x .>= (5 :: SWord8) } --- --- This time the proof passes as expected: --- --- >>> prove pred' --- Q.E.D. --- --- And the proof is not vacuous: --- --- >>> isVacuous pred' --- False +-- | Check if the given constraints are satisfiable, equivalent to @'isVacuousWith' 'defaultSMTCfg'@. +-- See the function 'constrain' for an example use of 'isVacuous'. isVacuous :: Provable a => a -> IO Bool isVacuous = isVacuousWith defaultSMTCfg @@ -373,7 +329,7 @@ -- | Determine if the constraints are vacuous using the given SMT-solver isVacuousWith :: Provable a => SMTConfig -> a -> IO Bool isVacuousWith config a = do - Result ki tr uic is cs ts as uis ax asgn cstr _ <- runSymbolic True $ forAll_ a >>= output + Result ki tr uic is cs ts as uis ax asgn cstr _ <- runSymbolic (True, Just config) $ forAll_ a >>= output case cstr of [] -> return False -- no constraints, no need to check _ -> do let is' = [(EX, i) | (_, i) <- is] -- map all quantifiers to "exists" for the constraint check @@ -451,7 +407,7 @@ let msg = when (verbose config) . putStrLn . ("** " ++) isTiming = timing config msg "Starting symbolic simulation.." - res <- timeIf isTiming "problem construction" $ runSymbolic isSat $ (if isSat then forSome_ else forAll_) predicate >>= output + res <- timeIf isTiming "problem construction" $ runSymbolic (isSat, Just config) $ (if isSat then forSome_ else forAll_) predicate >>= output msg $ "Generated symbolic trace:\n" ++ show res msg "Translating to SMT-Lib.." runProofOn converter config isSat comments res @@ -461,7 +417,7 @@ let isTiming = timing config solverCaps = capabilities (solver config) in case res of - Result ki _qcInfo _codeSegs is consts tbls arrs uis axs pgm cstrs [o@(SW (KBounded False 1) _)] -> + Result ki _qcInfo _codeSegs is consts tbls arrs uis axs pgm cstrs [o@(SW KBool _)] -> timeIf isTiming "translation" $ let uiMap = mapMaybe arrayUIKind arrs ++ map unintFnUIKind uis skolemMap = skolemize (if isSat then is else map flipQ is) @@ -481,56 +437,23 @@ ++ "\nDetected while generating the trace:\n" ++ show res ++ "\n*** Check calls to \"output\", they are typically not needed!" --- | Check whether the given solver is installed and is ready to go. This call does a --- simple call to the solver to ensure all is well. -sbvCheckSolverInstallation :: SMTConfig -> IO Bool -sbvCheckSolverInstallation cfg = do ThmResult r <- proveWith cfg $ \x -> (x+x) .== ((x*2) :: SWord8) - case r of - Unsatisfiable _ -> return True - _ -> return False - --- | Equality as a proof method. Allows for --- very concise construction of equivalence proofs, which is very typical in --- bit-precise proofs. -infix 4 === -class Equality a where - (===) :: a -> a -> IO ThmResult - -instance (SymWord a, EqSymbolic z) => Equality (SBV a -> z) where - k === l = prove $ \a -> k a .== l a - -instance (SymWord a, SymWord b, EqSymbolic z) => Equality (SBV a -> SBV b -> z) where - k === l = prove $ \a b -> k a b .== l a b - -instance (SymWord a, SymWord b, EqSymbolic z) => Equality ((SBV a, SBV b) -> z) where - k === l = prove $ \a b -> k (a, b) .== l (a, b) - -instance (SymWord a, SymWord b, SymWord c, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> z) where - k === l = prove $ \a b c -> k a b c .== l a b c - -instance (SymWord a, SymWord b, SymWord c, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c) -> z) where - k === l = prove $ \a b c -> k (a, b, c) .== l (a, b, c) - -instance (SymWord a, SymWord b, SymWord c, SymWord d, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> z) where - k === l = prove $ \a b c d -> k a b c d .== l a b c d - -instance (SymWord a, SymWord b, SymWord c, SymWord d, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d) -> z) where - k === l = prove $ \a b c d -> k (a, b, c, d) .== l (a, b, c, d) - -instance (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> z) where - k === l = prove $ \a b c d e -> k a b c d e .== l a b c d e - -instance (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e) -> z) where - k === l = prove $ \a b c d e -> k (a, b, c, d, e) .== l (a, b, c, d, e) - -instance (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> z) where - k === l = prove $ \a b c d e f -> k a b c d e f .== l a b c d e f - -instance (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> z) where - k === l = prove $ \a b c d e f -> k (a, b, c, d, e, f) .== l (a, b, c, d, e, f) - -instance (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> z) where - k === l = prove $ \a b c d e f g -> k a b c d e f g .== l a b c d e f g - -instance (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> z) where - k === l = prove $ \a b c d e f g -> k (a, b, c, d, e, f, g) .== l (a, b, c, d, e, f, g) +-- | Check if a branch condition is feasible in the current state +isSBranchFeasibleInState :: State -> String -> SBool -> IO Bool +isSBranchFeasibleInState st branch cond = do + let cfg = let pickedConfig = fromMaybe defaultSMTCfg (getSBranchRunConfig st) + in pickedConfig { timeOut = sBranchTimeOut pickedConfig } + msg = when (verbose cfg) . putStrLn . ("** " ++) + sw <- sbvToSW st cond + () <- forceSWArg sw + Result ki tr uic is cs ts as uis ax asgn cstr _ <- liftIO $ extractSymbolicSimulationState st + let -- Construct the corresponding sat-checker for the branch. Note that we need to + -- forget about the quantifiers and just use an "exist", as we're looking for a + -- point-satisfiability check here; whatever the original program was. + pgm = Result ki tr uic [(EX, n) | (_, n) <- is] cs ts as uis ax asgn cstr [sw] + cvt = if useSMTLib2 cfg then toSMTLib2 else toSMTLib1 + check <- runProofOn cvt cfg True [] pgm >>= callSolver True ("sBranch: Checking " ++ show branch ++ " feasibility") SatResult cfg + res <- case check of + SatResult (Unsatisfiable _) -> return False + _ -> return True -- No risks, even if it timed-our or anything else, we say it's feasible + msg $ "sBranch: Conclusion: " ++ if res then "Feasible" else "Unfeasible" + return res diff --git a/Data/SBV/Provers/SExpr.hs b/Data/SBV/Provers/SExpr.hs --- a/Data/SBV/Provers/SExpr.hs +++ b/Data/SBV/Provers/SExpr.hs @@ -11,10 +11,9 @@ module Data.SBV.Provers.SExpr where -import Control.Monad.Error () -- for Monad (Either String) instance -import Data.Char (isDigit, ord) -import Data.List (isPrefixOf) -import Numeric (readInt, readDec, readHex, fromRat) +import Data.Char (isDigit, ord) +import Data.List (isPrefixOf) +import Numeric (readInt, readDec, readHex, fromRat) import Data.SBV.BitVectors.AlgReals import Data.SBV.BitVectors.Data (nan, infinity) diff --git a/Data/SBV/Provers/Yices.hs b/Data/SBV/Provers/Yices.hs --- a/Data/SBV/Provers/Yices.hs +++ b/Data/SBV/Provers/Yices.hs @@ -31,7 +31,7 @@ -- The default options are @\"-m -f\"@, which is valid for Yices 2.1 series. You can use the @SBV_YICES_OPTIONS@ environment variable to override the options. yices :: SMTSolver yices = SMTSolver { - name = "Yices" + name = Yices , executable = "yices-smt" -- , options = ["-tc", "-smt", "-e"] -- For Yices1 , options = ["-m", "-f"] -- For Yices2 diff --git a/Data/SBV/Provers/Z3.hs b/Data/SBV/Provers/Z3.hs --- a/Data/SBV/Provers/Z3.hs +++ b/Data/SBV/Provers/Z3.hs @@ -39,7 +39,7 @@ -- The default options are @\"-in -smt2\"@, which is valid for Z3 4.1. You can use the @SBV_Z3_OPTIONS@ environment variable to override the options. z3 :: SMTSolver z3 = SMTSolver { - name = "z3" + name = Z3 , executable = "z3" , options = map (optionPrefix:) ["in", "smt2"] , engine = \cfg isSat qinps modelMap skolemMap pgm -> do @@ -72,7 +72,7 @@ where cleanErrs = intercalate "\n" . filter (not . junk) . lines junk = ("WARNING:" `isPrefixOf`) zero :: RoundingMode -> Kind -> String - zero _ (KBounded False 1) = "#b0" + zero _ KBool = "false" zero _ (KBounded _ sz) = "#x" ++ replicate (sz `div` 4) '0' zero _ KUnbounded = "0" zero _ KReal = "0.0" @@ -89,7 +89,7 @@ extract (Left s) = ["(echo \"((" ++ show s ++ " " ++ zero rm (kindOf s) ++ "))\")"] extract (Right (s, [])) = let g = "(get-value (" ++ show s ++ "))" in getVal (kindOf s) g extract (Right (s, ss)) = let g = "(get-value ((" ++ show s ++ concat [' ' : zero rm (kindOf a) | a <- ss] ++ ")))" in getVal (kindOf s) g - getVal KReal g = ["(set-option :pp.decimal false)", g, "(set-option :pp.decimal true)", g] + getVal KReal g = ["(set-option :pp.decimal false) " ++ g, "(set-option :pp.decimal true) " ++ g] getVal _ g = [g] addTimeOut Nothing o = o addTimeOut (Just i) o 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 @@ -16,15 +16,13 @@ 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) import Data.List (intercalate, isPrefixOf, isInfixOf) -import Data.Maybe (isNothing, fromJust) import Data.Word (Word8, Word16, Word32, Word64) import System.Directory (findExecutable) -import System.Process (readProcessWithExitCode, runInteractiveProcess, waitForProcess) +import System.Process (runInteractiveProcess, waitForProcess, terminateProcess) import System.Exit (ExitCode(..)) import System.IO (hClose, hFlush, hPutStr, hGetContents, hGetLine) @@ -35,72 +33,6 @@ import Data.SBV.BitVectors.PrettyNum import Data.SBV.Utils.TDiff --- | Solver configuration. See also 'z3', 'yices', 'cvc4', and 'boolector, which are instantiations of this type for those solvers, with --- reasonable defaults. In particular, custom configuration can be created by varying those values. (Such as @z3{verbose=True}@.) --- --- Most fields are self explanatory. The notion of precision for printing algebraic reals stems from the fact that such values does --- not necessarily have finite decimal representations, and hence we have to stop printing at some depth. It is important to --- emphasize that such values always have infinite precision internally. The issue is merely with how we print such an infinite --- precision value on the screen. The field 'printRealPrec' controls the printing precision, by specifying the number of digits after --- the decimal point. The default value is 16, but it can be set to any positive integer. --- --- When printing, SBV will add the suffix @...@ at the and of a real-value, if the given bound is not sufficient to represent the real-value --- exactly. Otherwise, the number will be written out in standard decimal notation. Note that SBV will always print the whole value if it --- is precise (i.e., if it fits in a finite number of digits), regardless of the precision limit. The limit only applies if the representation --- of the real value is not finite, i.e., if it is not rational. -data SMTConfig = SMTConfig { - verbose :: Bool -- ^ Debug mode - , timing :: Bool -- ^ Print timing information on how long different phases took (construction, solving, etc.) - , timeOut :: Maybe Int -- ^ How much time to give to the solver. (In seconds) - , printBase :: Int -- ^ Print integral literals in this base (2, 8, and 10, and 16 are supported.) - , printRealPrec :: Int -- ^ Print algebraic real values with this precision. (SReal, default: 16) - , solverTweaks :: [String] -- ^ Additional lines of script to give to the solver (user specified) - , satCmd :: String -- ^ Usually "(check-sat)". However, users might tweak it based on solver characteristics. - , smtFile :: Maybe FilePath -- ^ If Just, the generated SMT script will be put in this file (for debugging purposes mostly) - , useSMTLib2 :: Bool -- ^ If True, we'll treat the solver as using SMTLib2 input format. Otherwise, SMTLib1 - , solver :: SMTSolver -- ^ The actual SMT solver. - , roundingMode :: RoundingMode -- ^ Rounding mode to use for floating-point conversions - , useLogic :: Maybe Logic -- ^ If Nothing, pick automatically. Otherwise, either use the given one, or use the custom string. - } - --- | An SMT engine -type SMTEngine = SMTConfig -> Bool -> [(Quantifier, NamedSymVar)] -> [(String, UnintKind)] -> [Either SW (SW, [SW])] -> String -> IO SMTResult - --- | An SMT solver -data SMTSolver = SMTSolver { - name :: String -- ^ Printable name of the solver - , executable :: String -- ^ The path to its executable - , options :: [String] -- ^ Options to provide to the solver - , engine :: SMTEngine -- ^ The solver engine, responsible for interpreting solver output - , xformExitCode :: ExitCode -> ExitCode -- ^ Should we re-interpret exit codes. Most solvers behave rationally, i.e., id will do. Some (like CVC4) don't. - , capabilities :: SolverCapabilities -- ^ Various capabilities of the solver - } - --- | A model, as returned by a solver -data SMTModel = SMTModel { - modelAssocs :: [(String, CW)] -- ^ Mapping of symbolic values to constants. - , modelArrays :: [(String, [String])] -- ^ Arrays, very crude; only works with Yices. - , modelUninterps :: [(String, [String])] -- ^ Uninterpreted funcs; very crude; only works with Yices. - } - deriving Show - --- | The result of an SMT solver call. Each constructor is tagged with --- the 'SMTConfig' that created it so that further tools can inspect it --- and build layers of results, if needed. For ordinary uses of the library, --- this type should not be needed, instead use the accessor functions on --- it. (Custom Show instances and model extractors.) -data SMTResult = Unsatisfiable SMTConfig -- ^ Unsatisfiable - | Satisfiable SMTConfig SMTModel -- ^ Satisfiable with model - | Unknown SMTConfig SMTModel -- ^ Prover returned unknown, with a potential (possibly bogus) model - | ProofError SMTConfig [String] -- ^ Prover errored out - | TimeOut SMTConfig -- ^ Computation timed out (see the 'timeout' combinator) - --- | A script, to be passed to the solver. -data SMTScript = SMTScript { - scriptBody :: String -- ^ Initial feed - , scriptModel :: Maybe String -- ^ Optional continuation script, if the result is sat - } - -- | Extract the final configuration from a result resultConfig :: SMTResult -> SMTConfig resultConfig (Unsatisfiable c) = c @@ -109,16 +41,6 @@ resultConfig (ProofError c _) = c resultConfig (TimeOut c) = c -instance NFData SMTResult where - rnf (Unsatisfiable _) = () - rnf (Satisfiable _ xs) = rnf xs `seq` () - rnf (Unknown _ xs) = rnf xs `seq` () - rnf (ProofError _ xs) = rnf xs `seq` () - rnf (TimeOut _) = () - -instance NFData SMTModel where - rnf (SMTModel assocs unints uarrs) = rnf assocs `seq` rnf unints `seq` rnf uarrs `seq` () - -- | A 'prove' call results in a 'ThmResult' newtype ThmResult = ThmResult SMTResult @@ -130,17 +52,19 @@ -- we should warn the user about prefix-existentials. newtype AllSatResult = AllSatResult (Bool, [SMTResult]) +-- | User friendly way of printing theorem results instance Show ThmResult where show (ThmResult r) = showSMTResult "Q.E.D." "Unknown" "Unknown. Potential counter-example:\n" "Falsifiable" "Falsifiable. Counter-example:\n" r +-- | User friendly way of printing satisfiablity results instance Show SatResult where show (SatResult r) = showSMTResult "Unsatisfiable" "Unknown" "Unknown. Potential model:\n" "Satisfiable" "Satisfiable. Model:\n" r --- NB. The Show instance of AllSatResults have to be careful in being lazy enough +-- | The Show instance of AllSatResults. Note that we have to be careful in being lazy enough -- as the typical use case is to pull results out as they become available. instance Show AllSatResult where show (AllSatResult (e, xs)) = go (0::Int) xs @@ -181,47 +105,69 @@ genParse k (x@(CW _ (CWInteger i)):r) | kindOf x == k = Just (fromIntegral i, r) genParse _ _ = Nothing --- Base case, that comes in handy if there are no real variables +-- | Base case for 'SatModel' at unit type. Comes in handy if there are no real variables. instance SatModel () where parseCWs xs = return ((), xs) +-- | 'Bool' as extracted from a model instance SatModel Bool where - parseCWs xs = do (x, r) <- genParse (KBounded False 1) xs + parseCWs xs = do (x, r) <- genParse KBool xs return ((x :: Integer) /= 0, r) +-- | 'Word8' as extracted from a model instance SatModel Word8 where parseCWs = genParse (KBounded False 8) +-- | 'Int8' as extracted from a model instance SatModel Int8 where parseCWs = genParse (KBounded True 8) +-- | 'Word16' as extracted from a model instance SatModel Word16 where parseCWs = genParse (KBounded False 16) +-- | 'Int16' as extracted from a model instance SatModel Int16 where parseCWs = genParse (KBounded True 16) +-- | 'Word32' as extracted from a model instance SatModel Word32 where parseCWs = genParse (KBounded False 32) +-- | 'Int32' as extracted from a model instance SatModel Int32 where parseCWs = genParse (KBounded True 32) +-- | 'Word64' as extracted from a model instance SatModel Word64 where parseCWs = genParse (KBounded False 64) +-- | 'Int64' as extracted from a model instance SatModel Int64 where parseCWs = genParse (KBounded True 64) +-- | 'Integer' as extracted from a model instance SatModel Integer where parseCWs = genParse KUnbounded +-- | 'AlgReal' as extracted from a model instance SatModel AlgReal where parseCWs (CW KReal (CWAlgReal i) : r) = Just (i, r) parseCWs _ = Nothing --- when reading a list; go as long as we can (maximal-munch) --- note that this never fails.. +-- | 'Float' as extracted from a model +instance SatModel Float where + parseCWs (CW KFloat (CWFloat i) : r) = Just (i, r) + parseCWs _ = Nothing + +-- | 'Double' as extracted from a model +instance SatModel Double where + parseCWs (CW KDouble (CWDouble i) : r) = Just (i, r) + parseCWs _ = Nothing + +-- | A list of values as extracted from a model. When reading a list, we +-- go as long as we can (maximal-munch). Note that this never fails, as +-- we can always return the empty list! instance SatModel a => SatModel [a] where parseCWs [] = Just ([], []) parseCWs xs = case parseCWs xs of @@ -230,31 +176,37 @@ Nothing -> Just ([], ys) Nothing -> Just ([], xs) +-- | Tuples extracted from a model instance (SatModel a, SatModel b) => SatModel (a, b) where parseCWs as = do (a, bs) <- parseCWs as (b, cs) <- parseCWs bs return ((a, b), cs) +-- | 3-Tuples extracted from a model instance (SatModel a, SatModel b, SatModel c) => SatModel (a, b, c) where parseCWs as = do (a, bs) <- parseCWs as ((b, c), ds) <- parseCWs bs return ((a, b, c), ds) +-- | 4-Tuples extracted from a model instance (SatModel a, SatModel b, SatModel c, SatModel d) => SatModel (a, b, c, d) where parseCWs as = do (a, bs) <- parseCWs as ((b, c, d), es) <- parseCWs bs return ((a, b, c, d), es) +-- | 5-Tuples extracted from a model instance (SatModel a, SatModel b, SatModel c, SatModel d, SatModel e) => SatModel (a, b, c, d, e) where parseCWs as = do (a, bs) <- parseCWs as ((b, c, d, e), fs) <- parseCWs bs return ((a, b, c, d, e), fs) +-- | 6-Tuples extracted from a model instance (SatModel a, SatModel b, SatModel c, SatModel d, SatModel e, SatModel f) => SatModel (a, b, c, d, e, f) where parseCWs as = do (a, bs) <- parseCWs as ((b, c, d, e, f), gs) <- parseCWs bs return ((a, b, c, d, e, f), gs) +-- | 7-Tuples extracted from a model instance (SatModel a, SatModel b, SatModel c, SatModel d, SatModel e, SatModel f, SatModel g) => SatModel (a, b, c, d, e, f, g) where parseCWs as = do (a, bs) <- parseCWs as ((b, c, d, e, f, g), hs) <- parseCWs bs @@ -304,16 +256,19 @@ getModelUninterpretedValues :: String -> AllSatResult -> [Maybe String] getModelUninterpretedValues s (AllSatResult (_, xs)) = map (s `getModelUninterpretedValue`) xs +-- | 'ThmResult' as a generic model provider instance Modelable ThmResult where getModel (ThmResult r) = getModel r modelExists (ThmResult r) = modelExists r getModelDictionary (ThmResult r) = getModelDictionary r +-- | 'SatResult' as a generic model provider instance Modelable SatResult where getModel (SatResult r) = getModel r modelExists (SatResult r) = modelExists r getModelDictionary (SatResult r) = getModelDictionary r +-- | 'SMTResult' as a generic model provider instance Modelable SMTResult where getModel (Unsatisfiable _) = Left "SBV.getModel: Unsatisfiable result" getModel (Unknown _ m) = Right (True, parseModelOut m) @@ -388,8 +343,9 @@ where shC s = " " ++ s -- | Helper function to spin off to an SMT solver. -pipeProcess :: SMTConfig -> String -> String -> [String] -> SMTScript -> (String -> String) -> IO (Either String [String]) -pipeProcess cfg nm execName opts script cleanErrs = do +pipeProcess :: SMTConfig -> String -> [String] -> SMTScript -> (String -> String) -> IO (Either String [String]) +pipeProcess cfg execName opts script cleanErrs = do + let nm = show (name (solver cfg)) mbExecPath <- findExecutable execName case mbExecPath of Nothing -> return $ Left $ "Unable to locate executable for " ++ nm @@ -428,13 +384,13 @@ exec = executable smtSolver opts = options smtSolver isTiming = timing config - nmSolver = name smtSolver + nmSolver = show (name smtSolver) msg $ "Calling: " ++ show (unwords (exec:opts)) case smtFile config of Nothing -> return () Just f -> do msg $ "Saving the generated script in file: " ++ show f writeFile f (scriptBody script) - contents <- timeIf isTiming nmSolver $ pipeProcess config nmSolver exec opts script cleanErrs + contents <- timeIf isTiming nmSolver $ pipeProcess config exec opts script cleanErrs msg $ nmSolver ++ " output:\n" ++ either id (intercalate "\n") contents case contents of Left e -> return $ failure (lines e) @@ -444,41 +400,46 @@ -- and can speak SMT-Lib2 (just a little). runSolver :: SMTConfig -> FilePath -> [String] -> SMTScript -> IO (ExitCode, String, String) runSolver cfg execPath opts script - | isNothing $ scriptModel script - = let checkCmd | useSMTLib2 cfg = '\n' : satCmd cfg - | True = "" - in readProcessWithExitCode execPath opts (scriptBody script ++ checkCmd) - | True - = do (send, ask, cleanUp) <- do + = do (send, ask, cleanUp, pid) <- do (inh, outh, errh, pid) <- runInteractiveProcess execPath opts Nothing Nothing let send l = hPutStr inh (l ++ "\n") >> hFlush inh - recv = hGetLine outh `C.catch` (\(_ :: C.SomeException) -> return "") + recv = hGetLine outh ask l = send l >> recv - cleanUp r = do outMVar <- newEmptyMVar - out <- hGetContents outh - _ <- forkIO $ C.evaluate (length out) >> putMVar outMVar () - err <- hGetContents errh - _ <- forkIO $ C.evaluate (length err) >> putMVar outMVar () - hClose inh - takeMVar outMVar - takeMVar outMVar - hClose outh - hClose errh - ex <- waitForProcess pid - -- if the status is unknown, prepare for the possibility of not having a model - -- TBD: This is rather crude and potentially Z3 specific - return $ if "unknown" `isPrefixOf` r && "error" `isInfixOf` (out ++ err) - then (ExitSuccess, r , "") - else (ex, r ++ "\n" ++ out, err) - return (send, ask, cleanUp) - mapM_ send (lines (scriptBody script)) - r <- ask $ satCmd cfg - when (any (`isPrefixOf` r) ["sat", "unknown"]) $ do - let mls = lines (fromJust (scriptModel script)) - when (verbose cfg) $ do putStrLn "** Sending the following model extraction commands:" - mapM_ putStrLn mls - mapM_ send mls - cleanUp r + cleanUp response + = do hClose inh + outMVar <- newEmptyMVar + out <- hGetContents outh + _ <- forkIO $ C.evaluate (length out) >> putMVar outMVar () + err <- hGetContents errh + _ <- forkIO $ C.evaluate (length err) >> putMVar outMVar () + takeMVar outMVar + takeMVar outMVar + hClose outh + hClose errh + ex <- waitForProcess pid + return $ case response of + Nothing -> (ex, out, err) + Just (r, vals) -> -- if the status is unknown, prepare for the possibility of not having a model + -- TBD: This is rather crude and potentially Z3 specific + let finalOut = intercalate "\n" (r : vals) + in if "unknown" `isPrefixOf` r && "error" `isInfixOf` (out ++ err) + then (ExitSuccess, finalOut , "") + else (ex, finalOut ++ "\n" ++ out, err) + return (send, ask, cleanUp, pid) + let executeSolver = do mapM_ send (lines (scriptBody script)) + response <- case scriptModel script of + Nothing -> do send $ satCmd cfg + return Nothing + Just ls -> do r <- ask $ satCmd cfg + vals <- if any (`isPrefixOf` r) ["sat", "unknown"] + then do let mls = lines ls + when (verbose cfg) $ do putStrLn "** Sending the following model extraction commands:" + mapM_ putStrLn mls + mapM ask mls + else return [] + return $ Just (r, vals) + cleanUp response + executeSolver `C.onException` terminateProcess pid -- | In case the SMT-Lib solver returns a response over multiple lines, compress them so we have -- each S-Expression spanning only a single line. We'll ignore things line parentheses inside quotes diff --git a/Data/SBV/SMT/SMTLib.hs b/Data/SBV/SMT/SMTLib.hs --- a/Data/SBV/SMT/SMTLib.hs +++ b/Data/SBV/SMT/SMTLib.hs @@ -14,7 +14,6 @@ import Data.Char (isDigit) import Data.SBV.BitVectors.Data -import Data.SBV.SMT.SMT import Data.SBV.Provers.SExpr import qualified Data.SBV.SMT.SMTLib1 as SMT1 import qualified Data.SBV.SMT.SMTLib2 as SMT2 diff --git a/Data/SBV/SMT/SMTLib1.hs b/Data/SBV/SMT/SMTLib1.hs --- a/Data/SBV/SMT/SMTLib1.hs +++ b/Data/SBV/SMT/SMTLib1.hs @@ -154,7 +154,7 @@ -- no need to worry about Int/Real here as we don't support them with the SMTLib1 interface.. cvtCW :: CW -> String -cvtCW (CW (KBounded False 1) (CWInteger v)) = if v == 0 then "false" else "true" +cvtCW (CW KBool (CWInteger v)) = if v == 0 then "false" else "true" cvtCW x@(CW _ (CWInteger v)) | not (hasSign x) = "bv" ++ show v ++ "[" ++ show (intSizeOf x) ++ "]" -- signed numbers (with 2's complement representation) is problematic -- since there's no way to put a bvneg over a positive number to get minBound.. @@ -263,7 +263,7 @@ cvtType (SBVType xs) = unwords $ map kindType xs kindType :: Kind -> String -kindType (KBounded False 1) = "Bool" +kindType KBool = "Bool" kindType (KBounded _ s) = "BitVec[" ++ show s ++ "]" kindType KUnbounded = die "unbounded Integer" kindType KReal = die "real value" diff --git a/Data/SBV/SMT/SMTLib2.hs b/Data/SBV/SMT/SMTLib2.hs --- a/Data/SBV/SMT/SMTLib2.hs +++ b/Data/SBV/SMT/SMTLib2.hs @@ -13,6 +13,7 @@ module Data.SBV.SMT.SMTLib2(cvt, addNonEqConstraints) where import Data.Bits (bit) +import Data.Char (intToDigit) import Data.Function (on) import Data.Ord (comparing) import qualified Data.Foldable as F (toList) @@ -20,7 +21,7 @@ import qualified Data.IntMap as IM import qualified Data.Set as Set import Data.List (intercalate, partition, groupBy, sortBy) -import Numeric (showHex) +import Numeric (showIntAtBase, showHex) import Data.SBV.BitVectors.AlgReals import Data.SBV.BitVectors.Data @@ -264,7 +265,7 @@ swFunType ss s = "(" ++ unwords (map swType ss) ++ ") " ++ swType s smtType :: Kind -> String -smtType (KBounded False 1) = "Bool" +smtType KBool = "Bool" smtType (KBounded _ sz) = "(_ BitVec " ++ show sz ++ ")" smtType KUnbounded = "Int" smtType KReal = "Real" @@ -287,11 +288,16 @@ | True = show s --- NB. The following works with SMTLib2 since all sizes are multiples of 4 (or just 1, which is specially handled) +-- Carefully code hex numbers, SMTLib is picky about lengths of hex constants. For the time +-- being, SBV only supports sizes that are multiples of 4, but the below code is more robust +-- in case of future extensions to support arbitrary sizes. hex :: Int -> Integer -> String hex 1 v = "#b" ++ show v -hex sz v = "#x" ++ pad (sz `div` 4) (showHex v "") - where pad n s = replicate (n - length s) '0' ++ s +hex sz v + | sz `mod` 4 == 0 = "#x" ++ pad (sz `div` 4) (showHex v "") + | True = "#b" ++ pad sz (showBin v "") + where pad n s = replicate (n - length s) '0' ++ s + showBin = showIntAtBase 2 intToDigit cvtCW :: RoundingMode -> CW -> String cvtCW rm x @@ -335,7 +341,8 @@ boolOp = all isBoolean arguments bad | intOp = error $ "SBV.SMTLib2: Unsupported operation on unbounded integers: " ++ show expr | True = error $ "SBV.SMTLib2: Unsupported operation on real values: " ++ show expr - ensureBV = bvOp || bad + ensureBVOrBool = bvOp || boolOp || bad + ensureBV = bvOp || bad addRM s = s ++ " " ++ smtRoundingMode rm lift2 o _ [x, y] = "(" ++ o ++ " " ++ x ++ " " ++ y ++ ")" lift2 o _ sbvs = error $ "SBV.SMTLib2.sh.lift2: Unexpected arguments: " ++ show (o, sbvs) @@ -368,6 +375,7 @@ | needsCheck = "(ite " ++ cond ++ ssw e ++ " " ++ lkUp ++ ")" | True = lkUp where needsCheck = case aKnd of + KBool -> (2::Integer) > fromIntegral l KBounded _ n -> (2::Integer)^n > fromIntegral l KUnbounded -> True KReal -> error "SBV.SMT.SMTLib2.cvtExp: unexpected real valued index" @@ -379,6 +387,7 @@ | hasSign i = "(or " ++ le0 ++ " " ++ gtl ++ ") " | True = gtl ++ " " (less, leq) = case aKnd of + KBool -> error "SBV.SMT.SMTLib2.cvtExp: unexpected boolean valued index" KBounded{} -> if hasSign i then ("bvslt", "bvsle") else ("bvult", "bvule") KUnbounded -> ("<", "<=") KReal -> ("<", "<=") @@ -419,7 +428,7 @@ | intOp = "(div " ++ ssw a ++ " " ++ show (bit i :: Integer) ++ ")" -- Implement shiftR by division by 2^i | True = bad sh (SBVApp op args) - | Just f <- lookup op smtBVOpTable, ensureBV + | Just f <- lookup op smtBVOpTable, ensureBVOrBool = f (any hasSign args) (map ssw args) where -- The first 4 operators below do make sense for Integer's in Haskell, but there's -- no obvious counterpart for them in the SMTLib translation. diff --git a/Data/SBV/Tools/ExpectedValue.hs b/Data/SBV/Tools/ExpectedValue.hs --- a/Data/SBV/Tools/ExpectedValue.hs +++ b/Data/SBV/Tools/ExpectedValue.hs @@ -22,13 +22,13 @@ -- warm-up count and the convergence factor. Maximum iteration count can also -- be specified, at which point convergence won't be sought. The boolean controls verbosity. expectedValueWith :: Outputtable a => Bool -> Int -> Maybe Int -> Double -> Symbolic a -> IO [Double] -expectedValueWith verbose warmupCount mbMaxIter epsilon m +expectedValueWith chatty warmupCount mbMaxIter epsilon m | warmupCount < 0 || epsilon < 0 = error $ "SBV.expectedValue: warmup count and epsilon both must be non-negative, received: " ++ show (warmupCount, epsilon) | True = warmup warmupCount (repeat 0) >>= go warmupCount - where progress s | not verbose = return () - | True = putStr $ "\r*** " ++ s + where progress s | not chatty = return () + | True = putStr $ "\r*** " ++ s warmup :: Int -> [Integer] -> IO [Integer] warmup 0 v = do progress $ "Warmup complete, performed " ++ show warmupCount ++ " rounds.\n" return v @@ -42,7 +42,7 @@ let cval o = case o `lookup` cs of Nothing -> error "SBV.expectedValue: Cannot compute expected-values in the presence of uninterpreted constants!" Just cw -> case (cwKind cw, cwVal cw) of - (KBounded False 1, _) -> if cwToBool cw then 1 else 0 + (KBool, _) -> if cwToBool cw then 1 else 0 (KBounded{}, CWInteger v) -> v (KUnbounded, CWInteger v) -> v (KReal, _) -> error "Cannot compute expected-values for real valued results." diff --git a/Data/SBV/Tools/GenTest.hs b/Data/SBV/Tools/GenTest.hs --- a/Data/SBV/Tools/GenTest.hs +++ b/Data/SBV/Tools/GenTest.hs @@ -111,7 +111,7 @@ valOf [x] = s x valOf xs = "[" ++ intercalate ", " (map s xs) ++ "]" t cw = case kindOf cw of - KBounded False 1 -> "Bool" + KBool -> "Bool" KBounded False 8 -> "Word8" KBounded False 16 -> "Word16" KBounded False 32 -> "Word32" @@ -127,7 +127,7 @@ KUninterpreted us -> error $ "SBV.renderTest: Unsupported uninterpreted sort: " ++ us _ -> error $ "SBV.renderTest: Unexpected CW: " ++ show cw s cw = case cwKind cw of - KBounded False 1 -> take 5 (show (cwToBool cw) ++ repeat ' ') + KBool -> take 5 (show (cwToBool cw) ++ repeat ' ') KBounded sgn sz -> let CWInteger w = cwVal cw in shex False True (sgn, sz) w KUnbounded -> let CWInteger w = cwVal cw in shexI False True w KFloat -> let CWFloat w = cwVal cw in showHFloat w @@ -198,7 +198,7 @@ ] where mkField p cw i = " " ++ t ++ " " ++ p ++ show i ++ ";" where t = case cwKind cw of - KBounded False 1 -> "SBool" + KBool -> "SBool" KBounded False 8 -> "SWord8" KBounded False 16 -> "SWord16" KBounded False 32 -> "SWord32" @@ -215,7 +215,7 @@ _ -> error $ "SBV.renderTest: Unexpected CW: " ++ show cw mkLine (is, os) = "{{" ++ intercalate ", " (map v is) ++ "}, {" ++ intercalate ", " (map v os) ++ "}}" v cw = case cwKind cw of - KBounded False 1 -> if cwToBool cw then "true " else "false" + KBool -> if cwToBool cw then "true " else "false" KBounded sgn sz -> let CWInteger w = cwVal cw in shex False True (sgn, sz) w KUnbounded -> let CWInteger w = cwVal cw in shexI False True w KFloat -> let CWFloat w = cwVal cw in showCFloat w @@ -231,11 +231,11 @@ inp cw i = mkBool cw (n ++ "[i].input.i" ++ show i) out cw i = mkBool cw (n ++ "[i].output.o" ++ show i) mkBool cw s = case cwKind cw of - KBounded False 1 -> "(" ++ s ++ " == true) ? \"true \" : \"false\"" - _ -> s + KBool -> "(" ++ s ++ " == true) ? \"true \" : \"false\"" + _ -> s fmtString = unwords (map fmt is) ++ " -> " ++ unwords (map fmt os) fmt cw = case cwKind cw of - KBounded False 1 -> "%s" + KBool -> "%s" KBounded False 8 -> "0x%02\"PRIx8\"" KBounded False 16 -> "0x%04\"PRIx16\"U" KBounded False 32 -> "0x%08\"PRIx32\"UL" @@ -267,7 +267,7 @@ toF True = '1' toF False = '0' blast cw = case cwKind cw of - KBounded False 1 -> [toF (cwToBool cw)] + KBool -> [toF (cwToBool cw)] KBounded False 8 -> xlt 8 (cwVal cw) KBounded False 16 -> xlt 16 (cwVal cw) KBounded False 32 -> xlt 32 (cwVal cw) diff --git a/Data/SBV/Tools/Optimize.hs b/Data/SBV/Tools/Optimize.hs --- a/Data/SBV/Tools/Optimize.hs +++ b/Data/SBV/Tools/Optimize.hs @@ -19,7 +19,7 @@ import Data.SBV.BitVectors.Data import Data.SBV.BitVectors.Model (OrdSymbolic(..), EqSymbolic(..)) import Data.SBV.Provers.Prover (satWith, defaultSMTCfg) -import Data.SBV.SMT.SMT (SatModel, getModel, SMTConfig(..)) +import Data.SBV.SMT.SMT (SatModel, getModel) import Data.SBV.Utils.Boolean -- | Optimizer configuration. Note that iterative and quantified approaches are in general not interchangeable. diff --git a/Data/SBV/Tools/Polynomial.hs b/Data/SBV/Tools/Polynomial.hs --- a/Data/SBV/Tools/Polynomial.hs +++ b/Data/SBV/Tools/Polynomial.hs @@ -9,6 +9,7 @@ -- Implementation of polynomial arithmetic ----------------------------------------------------------------------------- +{-# LANGUAGE CPP #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE PatternGuards #-} @@ -100,7 +101,11 @@ | True = foldr (\x y -> sh x ++ " + " ++ y) (sh (last cs)) (init cs) ++ t where t | st = " :: GF(2^" ++ show n ++ ")" | True = "" +#if __GLASGOW_HASKELL__ >= 708 + n = maybe (error "SBV.Polynomial.sp: Unexpected non-finite usage!") id (bitSizeMaybe a) +#else n = bitSize a +#endif is = [n-1, n-2 .. 0] cs = map fst $ filter snd $ zip is (map (testBit a) is) sh 0 = "1" diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -1,3 +1,21 @@ + + + + + + + + + + + + +
Travis BuildHackage
+ + + +
+ SBV: SMT Based Verification in Haskell ====================================== diff --git a/SBVUnitTest/Examples/Basics/BasicTests.hs b/SBVUnitTest/Examples/Basics/BasicTests.hs --- a/SBVUnitTest/Examples/Basics/BasicTests.hs +++ b/SBVUnitTest/Examples/Basics/BasicTests.hs @@ -21,22 +21,22 @@ test0 f = f (3 :: Word8) 2 test1, test2, test3, test4, test5 :: (forall a. Num a => (a -> a -> a)) -> IO Result -test1 f = runSymbolic True $ do let x = literal (3 :: Word8) - y = literal (2 :: Word8) - output $ f x y -test2 f = runSymbolic True $ do let x = literal (3 :: Word8) - y :: SWord8 <- forall "y" - output $ f x y -test3 f = runSymbolic True $ do x :: SWord8 <- forall "x" - y :: SWord8 <- forall "y" - output $ f x y -test4 f = runSymbolic True $ do x :: SWord8 <- forall "x" - output $ f x x -test5 f = runSymbolic True $ do x :: SWord8 <- forall "x" - let r = f x x - q :: SWord8 <- forall "q" - _ <- output q - output r +test1 f = runSymbolic (True, Nothing) $ do let x = literal (3 :: Word8) + y = literal (2 :: Word8) + output $ f x y +test2 f = runSymbolic (True, Nothing) $ do let x = literal (3 :: Word8) + y :: SWord8 <- forall "y" + output $ f x y +test3 f = runSymbolic (True, Nothing) $ do x :: SWord8 <- forall "x" + y :: SWord8 <- forall "y" + output $ f x y +test4 f = runSymbolic (True, Nothing) $ do x :: SWord8 <- forall "x" + output $ f x x +test5 f = runSymbolic (True, Nothing) $ do x :: SWord8 <- forall "x" + let r = f x x + q :: SWord8 <- forall "q" + _ <- output q + output r f1, f2, f3, f4, f5 :: Num a => a -> a -> a f1 x y = (x+y)*(x-y) 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 = "Sun Feb 16 15:11:29 PST 2014" +buildTime = "Fri Jul 11 22:53:51 PDT 2014" diff --git a/SBVUnitTest/TestSuite/Basics/ArithNoSolver.hs b/SBVUnitTest/TestSuite/Basics/ArithNoSolver.hs --- a/SBVUnitTest/TestSuite/Basics/ArithNoSolver.hs +++ b/SBVUnitTest/TestSuite/Basics/ArithNoSolver.hs @@ -12,6 +12,7 @@ {-# LANGUAGE Rank2Types #-} {-# LANGUAGE TupleSections #-} +{-# LANGUAGE CPP #-} module TestSuite.Basics.ArithNoSolver(testSuite) where @@ -19,6 +20,13 @@ import SBVTest +ghcBitSize :: Bits a => a -> Int +#if __GLASGOW_HASKELL__ >= 708 +ghcBitSize x = maybe (error "SBV.ghcBitSize: Unexpected non-finite usage!") id (bitSizeMaybe x) +#else +ghcBitSize = bitSize +#endif + -- Test suite testSuite :: SBVTestSuite testSuite = mkTestSuite $ \_ -> test $ @@ -114,14 +122,14 @@ genIntTestS :: String -> (forall a. (Num a, Bits a) => a -> Int -> a) -> [Test] genIntTestS nm op = map mkTest $ - zipWith pair [("u8", show x, show y, x `op` y) | x <- w8s, y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- sw8s, y <- [0 .. (bitSize x - 1)]] - ++ zipWith pair [("u16", show x, show y, x `op` y) | x <- w16s, y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- sw16s, y <- [0 .. (bitSize x - 1)]] - ++ zipWith pair [("u32", show x, show y, x `op` y) | x <- w32s, y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- sw32s, y <- [0 .. (bitSize x - 1)]] - ++ zipWith pair [("u64", show x, show y, x `op` y) | x <- w64s, y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- sw64s, y <- [0 .. (bitSize x - 1)]] - ++ zipWith pair [("s8", show x, show y, x `op` y) | x <- i8s, y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- si8s, y <- [0 .. (bitSize x - 1)]] - ++ zipWith pair [("s16", show x, show y, x `op` y) | x <- i16s, y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- si16s, y <- [0 .. (bitSize x - 1)]] - ++ zipWith pair [("s32", show x, show y, x `op` y) | x <- i32s, y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- si32s, y <- [0 .. (bitSize x - 1)]] - ++ zipWith pair [("s64", show x, show y, x `op` y) | x <- i64s, y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- si64s, y <- [0 .. (bitSize x - 1)]] + zipWith pair [("u8", show x, show y, x `op` y) | x <- w8s, y <- [0 .. (ghcBitSize x - 1)]] [x `op` y | x <- sw8s, y <- [0 .. (ghcBitSize x - 1)]] + ++ zipWith pair [("u16", show x, show y, x `op` y) | x <- w16s, y <- [0 .. (ghcBitSize x - 1)]] [x `op` y | x <- sw16s, y <- [0 .. (ghcBitSize x - 1)]] + ++ zipWith pair [("u32", show x, show y, x `op` y) | x <- w32s, y <- [0 .. (ghcBitSize x - 1)]] [x `op` y | x <- sw32s, y <- [0 .. (ghcBitSize x - 1)]] + ++ zipWith pair [("u64", show x, show y, x `op` y) | x <- w64s, y <- [0 .. (ghcBitSize x - 1)]] [x `op` y | x <- sw64s, y <- [0 .. (ghcBitSize x - 1)]] + ++ zipWith pair [("s8", show x, show y, x `op` y) | x <- i8s, y <- [0 .. (ghcBitSize x - 1)]] [x `op` y | x <- si8s, y <- [0 .. (ghcBitSize x - 1)]] + ++ zipWith pair [("s16", show x, show y, x `op` y) | x <- i16s, y <- [0 .. (ghcBitSize x - 1)]] [x `op` y | x <- si16s, y <- [0 .. (ghcBitSize x - 1)]] + ++ zipWith pair [("s32", show x, show y, x `op` y) | x <- i32s, y <- [0 .. (ghcBitSize x - 1)]] [x `op` y | x <- si32s, y <- [0 .. (ghcBitSize x - 1)]] + ++ zipWith pair [("s64", show x, show y, x `op` y) | x <- i64s, y <- [0 .. (ghcBitSize x - 1)]] [x `op` y | x <- si64s, y <- [0 .. (ghcBitSize x - 1)]] ++ zipWith pair [("iUB", show x, show y, x `op` y) | x <- iUBs, y <- [0 .. 10]] [x `op` y | x <- siUBs, y <- [0 .. 10 ]] where pair (t, x, y, a) b = (t, x, y, show a, show b, show (fromIntegral a `asTypeOf` b) == show b) mkTest (t, x, y, a, b, s) = "arithCF-" ++ nm ++ "." ++ t ++ "_" ++ x ++ "_" ++ y ++ "_" ++ a ++ "_" ++ b ~: s `showsAs` "True" diff --git a/SBVUnitTest/TestSuite/Basics/ArithSolver.hs b/SBVUnitTest/TestSuite/Basics/ArithSolver.hs --- a/SBVUnitTest/TestSuite/Basics/ArithSolver.hs +++ b/SBVUnitTest/TestSuite/Basics/ArithSolver.hs @@ -13,6 +13,7 @@ {-# LANGUAGE Rank2Types #-} {-# LANGUAGE TupleSections #-} +{-# LANGUAGE CPP #-} module TestSuite.Basics.ArithSolver(testSuite) where @@ -20,10 +21,19 @@ import SBVTest +ghcBitSize :: Bits a => a -> Int +#if __GLASGOW_HASKELL__ >= 708 +ghcBitSize x = maybe (error "SBV.ghcBitSize: Unexpected non-finite usage!") id (bitSizeMaybe x) +#else +ghcBitSize = bitSize +#endif + -- Test suite testSuite :: SBVTestSuite testSuite = mkTestSuite $ \_ -> test $ genReals + ++ genFloats + ++ genDoubles ++ genQRems ++ genBinTest True "+" (+) ++ genBinTest True "-" (-) @@ -66,7 +76,7 @@ ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- i32s, y <- i32s] ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- i64s, y <- i64s] ++ [(show x, show y, mkThm2 x y (x `op` y)) | unboundedOK, x <- iUBs, y <- iUBs] - where mkTest (x, y, t) = "arithmetic-" ++ nm ++ "." ++ x ++ "_" ++ y ~: assert t + where mkTest (x, y, t) = "genBinTest.arithmetic-" ++ nm ++ "." ++ x ++ "_" ++ y ~: assert t mkThm2 x y r = isThm $ do [a, b] <- mapM free ["x", "y"] constrain $ a .== literal x constrain $ b .== literal y @@ -82,7 +92,7 @@ ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- i32s, y <- i32s] ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- i64s, y <- i64s] ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- iUBs, y <- iUBs] - where mkTest (x, y, t) = "arithmetic-" ++ nm ++ "." ++ x ++ "_" ++ y ~: assert t + where mkTest (x, y, t) = "genBoolTest.arithmetic-" ++ nm ++ "." ++ x ++ "_" ++ y ~: assert t mkThm2 x y r = isThm $ do [a, b] <- mapM free ["x", "y"] constrain $ a .== literal x constrain $ b .== literal y @@ -98,7 +108,7 @@ ++ [(show x, mkThm x (op x)) | x <- i32s] ++ [(show x, mkThm x (op x)) | x <- i64s] ++ [(show x, mkThm x (op x)) | unboundedOK, x <- iUBs] - where mkTest (x, t) = "arithmetic-" ++ nm ++ "." ++ x ~: assert t + where mkTest (x, t) = "genUnTest.arithmetic-" ++ nm ++ "." ++ x ~: assert t mkThm x r = isThm $ do a <- free "x" constrain $ a .== literal x return $ literal r .== op a @@ -113,7 +123,7 @@ ++ [("s32", show x, show y, mkThm2 x y (x `op` y)) | x <- i32s, y <- is] ++ [("s64", show x, show y, mkThm2 x y (x `op` y)) | x <- i64s, y <- is] ++ [("iUB", show x, show y, mkThm2 x y (x `op` y)) | x <- iUBs, y <- is] - where mkTest (l, x, y, t) = "arithmetic-" ++ nm ++ "." ++ l ++ "_" ++ x ++ "_" ++ y ~: assert t + where mkTest (l, x, y, t) = "genIntTest.arithmetic-" ++ nm ++ "." ++ l ++ "_" ++ x ++ "_" ++ y ~: assert t is = [-10 .. 10] mkThm2 x y r = isThm $ do a <- free "x" constrain $ a .== literal x @@ -121,16 +131,16 @@ genIntTestS :: Bool -> String -> (forall a. (Num a, Bits a) => a -> Int -> a) -> [Test] -genIntTestS unboundedOK nm op = map mkTest $ [("u8", show x, show y, mkThm2 x y (x `op` y)) | x <- w8s, y <- [0 .. (bitSize x - 1)]] - ++ [("u16", show x, show y, mkThm2 x y (x `op` y)) | x <- w16s, y <- [0 .. (bitSize x - 1)]] - ++ [("u32", show x, show y, mkThm2 x y (x `op` y)) | x <- w32s, y <- [0 .. (bitSize x - 1)]] - ++ [("u64", show x, show y, mkThm2 x y (x `op` y)) | x <- w64s, y <- [0 .. (bitSize x - 1)]] - ++ [("s8", show x, show y, mkThm2 x y (x `op` y)) | x <- i8s, y <- [0 .. (bitSize x - 1)]] - ++ [("s16", show x, show y, mkThm2 x y (x `op` y)) | x <- i16s, y <- [0 .. (bitSize x - 1)]] - ++ [("s32", show x, show y, mkThm2 x y (x `op` y)) | x <- i32s, y <- [0 .. (bitSize x - 1)]] - ++ [("s64", show x, show y, mkThm2 x y (x `op` y)) | x <- i64s, y <- [0 .. (bitSize x - 1)]] +genIntTestS unboundedOK nm op = map mkTest $ [("u8", show x, show y, mkThm2 x y (x `op` y)) | x <- w8s, y <- [0 .. (ghcBitSize x - 1)]] + ++ [("u16", show x, show y, mkThm2 x y (x `op` y)) | x <- w16s, y <- [0 .. (ghcBitSize x - 1)]] + ++ [("u32", show x, show y, mkThm2 x y (x `op` y)) | x <- w32s, y <- [0 .. (ghcBitSize x - 1)]] + ++ [("u64", show x, show y, mkThm2 x y (x `op` y)) | x <- w64s, y <- [0 .. (ghcBitSize x - 1)]] + ++ [("s8", show x, show y, mkThm2 x y (x `op` y)) | x <- i8s, y <- [0 .. (ghcBitSize x - 1)]] + ++ [("s16", show x, show y, mkThm2 x y (x `op` y)) | x <- i16s, y <- [0 .. (ghcBitSize x - 1)]] + ++ [("s32", show x, show y, mkThm2 x y (x `op` y)) | x <- i32s, y <- [0 .. (ghcBitSize x - 1)]] + ++ [("s64", show x, show y, mkThm2 x y (x `op` y)) | x <- i64s, y <- [0 .. (ghcBitSize x - 1)]] ++ [("iUB", show x, show y, mkThm2 x y (x `op` y)) | unboundedOK, x <- iUBs, y <- [0 .. 10]] - where mkTest (l, x, y, t) = "arithmetic-" ++ nm ++ "." ++ l ++ "_" ++ x ++ "_" ++ y ~: assert t + where mkTest (l, x, y, t) = "genIntTestS.arithmetic-" ++ nm ++ "." ++ l ++ "_" ++ x ++ "_" ++ y ~: assert t mkThm2 x y r = isThm $ do a <- free "x" constrain $ a .== literal x return $ literal r .== a `op` y @@ -152,7 +162,7 @@ ++ [(show x, mkThm fromBitsBE blastBE x) | x <- w64s] ++ [(show x, mkThm fromBitsLE blastLE x) | x <- i64s] ++ [(show x, mkThm fromBitsBE blastBE x) | x <- i64s] - where mkTest (x, t) = "blast-" ++ show x ~: assert t + where mkTest (x, t) = "genBlasts.blast-" ++ show x ~: assert t mkThm from to v = isThm $ do a <- free "x" constrain $ a .== literal v return $ a .== from (to a) @@ -176,7 +186,7 @@ ++ [(show x, mkFEq unsignCast (fromBitsLE . blastLE) x) | x <- i16s] ++ [(show x, mkFEq unsignCast (fromBitsLE . blastLE) x) | x <- i32s] ++ [(show x, mkFEq unsignCast (fromBitsLE . blastLE) x) | x <- i64s] - where mkTest (x, t) = "cast-" ++ show x ~: assert t + where mkTest (x, t) = "genCasts.cast-" ++ show x ~: assert t mkThm from to v = isThm $ do a <- free "x" constrain $ a .== literal v return $ a .== from (to a) @@ -195,12 +205,46 @@ ++ [(">=", show x, show y, mkThm2 (.>=) x y (x >= y)) | x <- rs, y <- rs ] ++ [("==", show x, show y, mkThm2 (.==) x y (x == y)) | x <- rs, y <- rs ] ++ [("/=", show x, show y, mkThm2 (./=) x y (x /= y)) | x <- rs, y <- rs ] - where mkTest (nm, x, y, t) = "arithmetic-" ++ nm ++ "." ++ x ++ "_" ++ y ~: assert t + where mkTest (nm, x, y, t) = "genReals.arithmetic-" ++ nm ++ "." ++ x ++ "_" ++ y ~: assert t mkThm2 op x y r = isThm $ do [a, b] <- mapM free ["x", "y"] constrain $ a .== literal x constrain $ b .== literal y return $ literal r .== a `op` b +genFloats :: [Test] +genFloats = genIEEE754 "genFloats" fs + +genDoubles :: [Test] +genDoubles = genIEEE754 "genDoubles" ds + +genIEEE754 :: (RealFloat a, Show a, SymWord a, Ord a, Floating a) => String -> [a] -> [Test] +genIEEE754 origin vs = map mkTest $ [("+", show x, show y, mkThm2 (+) x y (x + y)) | x <- vs, y <- vs ] + ++ [("-", show x, show y, mkThm2 (-) x y (x - y)) | x <- vs, y <- vs ] + ++ [("*", show x, show y, mkThm2 (*) x y (x * y)) | x <- vs, y <- vs ] + ++ [("/", show x, show y, mkThm2 (/) x y (x / y)) | x <- vs, y <- vs, y /= 0] + ++ [("<", show x, show y, mkThm2C False (.<) x y (x < y)) | x <- vs, y <- vs ] + ++ [("<=", show x, show y, mkThm2C False (.<=) x y (x <= y)) | x <- vs, y <- vs ] + ++ [(">", show x, show y, mkThm2C False (.>) x y (x > y)) | x <- vs, y <- vs ] + ++ [(">=", show x, show y, mkThm2C False (.>=) x y (x >= y)) | x <- vs, y <- vs ] + ++ [("==", show x, show y, mkThm2C False (.==) x y (x == y)) | x <- vs, y <- vs ] + ++ [("/=", show x, show y, mkThm2C True (./=) x y (x /= y)) | x <- vs, y <- vs ] + where mkTest (nm, x, y, t) = origin ++ ".arithmetic-" ++ nm ++ "." ++ x ++ "_" ++ y ~: assert t + eqF v val + | isNaN val = constrain $ isSNaN v + | True = constrain $ v .== literal val + mkThm2 op x y r = isThm $ do [a, b] <- mapM free ["x", "y"] + eqF a x + eqF b y + return $ if isNaN r + then isSNaN (a `op` b) + else literal r .== a `op` b + mkThm2C neq op x y r = isThm $ do [a, b] <- mapM free ["x", "y"] + eqF a x + eqF b y + return $ if isNaN x || isNaN y + then (if neq then a `op` b else bnot (a `op` b)) + else literal r .== a `op` b + genQRems :: [Test] genQRems = map mkTest $ [("divMod", show x, show y, mkThm2 sDivMod x y (x `divMod'` y)) | x <- w8s, y <- w8s ] ++ [("divMod", show x, show y, mkThm2 sDivMod x y (x `divMod'` y)) | x <- w16s, y <- w16s] @@ -222,7 +266,7 @@ ++ [("quotRem", show x, show y, mkThm2 sQuotRem x y (x `quotRem'` y)) | x <- iUBs, y <- iUBs] where divMod' x y = if y == 0 then (0, x) else x `divMod` y quotRem' x y = if y == 0 then (0, x) else x `quotRem` y - mkTest (nm, x, y, t) = "arithmetic-" ++ nm ++ "." ++ x ++ "_" ++ y ~: assert t + mkTest (nm, x, y, t) = "genQRems.arithmetic-" ++ nm ++ "." ++ x ++ "_" ++ y ~: assert t mkThm2 op x y (e1, e2) = isThm $ do [a, b] <- mapM free ["x", "y"] constrain $ a .== literal x constrain $ b .== literal y @@ -263,8 +307,14 @@ iUBs = [-1000000] ++ [-1 .. 1] ++ [1000000] rs :: [AlgReal] -rs = [fromRational (i % d) | i <- is, d <- ds] - where is = [-1000000] ++ [-1 .. 1] ++ [10000001] - ds = [5,100,1000000] +rs = [fromRational (i % d) | i <- is, d <- dens] + where is = [-1000000] ++ [-1 .. 1] ++ [10000001] + dens = [5,100,1000000] +-- Admittedly paltry test-cases for float/double +fs :: [Float] +fs = nan : -infinity : infinity : 0 : [-5.0, -4.7 .. 5] ++ [5] + +ds :: [Double] +ds = nan : -infinity : infinity : 0 : [-5.0, -4.7 .. 5] ++ [5] {-# ANN module "HLint: ignore Reduce duplication" #-} diff --git a/SBVUnitTest/TestSuite/BitPrecise/Legato.hs b/SBVUnitTest/TestSuite/BitPrecise/Legato.hs --- a/SBVUnitTest/TestSuite/BitPrecise/Legato.hs +++ b/SBVUnitTest/TestSuite/BitPrecise/Legato.hs @@ -23,8 +23,8 @@ "legato-1" ~: legatoPgm `goldCheck` "legato.gold" , "legato-2" ~: legatoC `goldCheck` "legato_c.gold" ] - where legatoPgm = runSymbolic True $ forAll ["mem", "addrX", "x", "addrY", "y", "addrLow", "regX", "regA", "memVals", "flagC", "flagZ"] legatoIsCorrect - >>= output + where legatoPgm = runSymbolic (True, Nothing) $ forAll ["mem", "addrX", "x", "addrY", "y", "addrLow", "regX", "regA", "memVals", "flagC", "flagZ"] legatoIsCorrect + >>= output legatoC = compileToC' "legatoMult" $ do cgSetDriverValues [87, 92] cgPerformRTCs True diff --git a/SBVUnitTest/TestSuite/BitPrecise/PrefixSum.hs b/SBVUnitTest/TestSuite/BitPrecise/PrefixSum.hs --- a/SBVUnitTest/TestSuite/BitPrecise/PrefixSum.hs +++ b/SBVUnitTest/TestSuite/BitPrecise/PrefixSum.hs @@ -22,5 +22,5 @@ testSuite = mkTestSuite $ \goldCheck -> test [ "prefixSum1" ~: assert =<< isThm (flIsCorrect 8 (0, (+))) , "prefixSum2" ~: assert =<< isThm (flIsCorrect 16 (0, smax)) - , "prefixSum3" ~: runSymbolic True (genPrefixSumInstance 16 >>= output) `goldCheck` "prefixSum_16.gold" + , "prefixSum3" ~: runSymbolic (True, Nothing) (genPrefixSumInstance 16 >>= output) `goldCheck` "prefixSum_16.gold" ] diff --git a/SBVUnitTest/TestSuite/CRC/CCITT.hs b/SBVUnitTest/TestSuite/CRC/CCITT.hs --- a/SBVUnitTest/TestSuite/CRC/CCITT.hs +++ b/SBVUnitTest/TestSuite/CRC/CCITT.hs @@ -22,4 +22,4 @@ testSuite = mkTestSuite $ \goldCheck -> test [ "ccitt" ~: crcPgm `goldCheck` "ccitt.gold" ] - where crcPgm = runSymbolic True $ forAll_ crcGood >>= output + where crcPgm = runSymbolic (True, Nothing) $ forAll_ crcGood >>= output diff --git a/SBVUnitTest/TestSuite/Existentials/CRCPolynomial.hs b/SBVUnitTest/TestSuite/Existentials/CRCPolynomial.hs --- a/SBVUnitTest/TestSuite/Existentials/CRCPolynomial.hs +++ b/SBVUnitTest/TestSuite/Existentials/CRCPolynomial.hs @@ -22,7 +22,7 @@ testSuite = mkTestSuite $ \goldCheck -> test [ "crcPolyExist" ~: pgm `goldCheck` "crcPolyExist.gold" ] - where pgm = runSymbolic True $ do + where pgm = runSymbolic (True, Nothing) $ do p <- exists "poly" s <- do sh <- forall "sh" sl <- forall "sl" diff --git a/SBVUnitTest/TestSuite/Puzzles/Coins.hs b/SBVUnitTest/TestSuite/Puzzles/Coins.hs --- a/SBVUnitTest/TestSuite/Puzzles/Coins.hs +++ b/SBVUnitTest/TestSuite/Puzzles/Coins.hs @@ -22,7 +22,8 @@ testSuite = mkTestSuite $ \goldCheck -> test [ "coins" ~: coinsPgm `goldCheck` "coins.gold" ] - where coinsPgm = runSymbolic True $ do cs <- mapM mkCoin [1..6] - mapM_ constrain [c s | s <- combinations cs, length s >= 2, c <- [c1, c2, c3, c4, c5, c6]] - constrain $ bAnd $ zipWith (.>=) cs (tail cs) - output $ sum cs .== 115 + where coinsPgm = runSymbolic (True, Nothing) $ do + cs <- mapM mkCoin [1..6] + mapM_ constrain [c s | s <- combinations cs, length s >= 2, c <- [c1, c2, c3, c4, c5, c6]] + constrain $ bAnd $ zipWith (.>=) cs (tail cs) + output $ sum cs .== 115 diff --git a/SBVUnitTest/TestSuite/Puzzles/Counts.hs b/SBVUnitTest/TestSuite/Puzzles/Counts.hs --- a/SBVUnitTest/TestSuite/Puzzles/Counts.hs +++ b/SBVUnitTest/TestSuite/Puzzles/Counts.hs @@ -22,5 +22,5 @@ testSuite = mkTestSuite $ \goldCheck -> test [ "counts" ~: countPgm `goldCheck` "counts.gold" ] - where countPgm = runSymbolic True $ forAll_ puzzle' >>= output + where countPgm = runSymbolic (True, Nothing) $ forAll_ puzzle' >>= output puzzle' d0 d1 d2 d3 d4 d5 d6 d7 d8 d9 = puzzle [d0, d1, d2, d3, d4, d5, d6, d7, d8, d9] diff --git a/SBVUnitTest/TestSuite/Uninterpreted/AUF.hs b/SBVUnitTest/TestSuite/Uninterpreted/AUF.hs --- a/SBVUnitTest/TestSuite/Uninterpreted/AUF.hs +++ b/SBVUnitTest/TestSuite/Uninterpreted/AUF.hs @@ -24,4 +24,4 @@ , "auf-1" ~: assert =<< isThm thm2 , "auf-2" ~: pgm `goldCheck` "auf-1.gold" ] - where pgm = runSymbolic True $ forAll ["x", "y", "a", "initVal"] thm1 >>= output + where pgm = runSymbolic (True, Nothing) $ forAll ["x", "y", "a", "initVal"] thm1 >>= output diff --git a/sbv.cabal b/sbv.cabal --- a/sbv.cabal +++ b/sbv.cabal @@ -1,5 +1,5 @@ Name: sbv -Version: 3.0 +Version: 3.1 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 @@ -47,7 +47,7 @@ TypeOperators TypeSynonymInstances Build-Depends : base >= 4 && < 5 - , array, containers, deepseq, directory, filepath, old-time + , array, async, containers, deepseq, directory, filepath, old-time , pretty, process, mtl, QuickCheck, random, syb Exposed-modules : Data.SBV , Data.SBV.Bridge.Boolector @@ -71,6 +71,7 @@ , Data.SBV.Examples.Existentials.CRCPolynomial , Data.SBV.Examples.Existentials.Diophantine , Data.SBV.Examples.Misc.Floating + , Data.SBV.Examples.Misc.SBranch , Data.SBV.Examples.Misc.ModelExtract , Data.SBV.Examples.Polynomials.Polynomials , Data.SBV.Examples.Puzzles.Coins