sbv 5.11 → 5.12
raw patch · 20 files changed
+197/−200 lines, 20 filesdep +ghcdep ~basedep ~deepseq
Dependencies added: ghc
Dependency ranges changed: base, deepseq
Files
- CHANGES.md +16/−1
- Data/SBV.hs +2/−8
- Data/SBV/BitVectors/Data.hs +5/−5
- Data/SBV/BitVectors/Floating.hs +9/−9
- Data/SBV/BitVectors/Model.hs +14/−14
- Data/SBV/BitVectors/Symbolic.hs +37/−28
- Data/SBV/Compilers/C.hs +3/−0
- Data/SBV/Compilers/CodeGen.hs +2/−2
- Data/SBV/Examples/Misc/Floating.hs +29/−23
- Data/SBV/Examples/Misc/NoDiv0.hs +2/−4
- Data/SBV/Provers/Prover.hs +8/−1
- Data/SBV/SMT/SMT.hs +2/−2
- Data/SBV/Utils/Numeric.hs +3/−4
- GHC/SrcLoc/Compat.hs +5/−20
- GHC/Stack/Compat.hs +1/−20
- SBVUnitTest/SBVUnitTestBuildTime.hs +1/−1
- SBVUnitTest/TestSuite/Arrays/Memory.hs +1/−1
- SBVUnitTest/TestSuite/Basics/ArithNoSolver.hs +9/−2
- SBVUnitTest/TestSuite/Basics/ArithSolver.hs +1/−1
- sbv.cabal +47/−54
CHANGES.md view
@@ -1,7 +1,22 @@ * Hackage: <http://hackage.haskell.org/package/sbv> * GitHub: <http://leventerkok.github.com/sbv/> -* Latest Hackage released version: 5.11, 2016-01-15+* Latest Hackage released version: 5.12, 2016-06-06++### Version 5.12, 2016-06-06++ * Fix GHC8.0 compliation issues, and warning clean-up. Thanks to Adam Foltzer for the bulk+ of the work and Tom Sydney Kerckhove for the initial patch for 8.0 compatibility.++ * Minor fix to printing models with floats when the base is 2/16, making sure the alignment+ is done properly accommodating for the crackNum output.++ * Wait for external process to die on exception, to avoid spawning zombies. Thanks to+ Daniel Wagner for the patch.++ * Fix hash-consed arrays: Previously we were caching based only on elements, which is not+ sufficient as you can have conflicts differing only on the address type, but same contents.+ Thanks to Brian Huffman for reporting and the corresponding patch. ### Version 5.11, 2016-01-15
Data/SBV.hs view
@@ -107,12 +107,6 @@ {-# LANGUAGE FlexibleInstances #-} --- TODO: remove OverlappingInstances and these warning suppressions--- once support is dropped for GHC 7.8-{-# OPTIONS_GHC -fno-warn-deprecated-flags #-}-{-# OPTIONS_GHC -fno-warn-unrecognised-pragmas #-}-{-# LANGUAGE OverlappingInstances #-}- module Data.SBV ( -- * Programming with symbolic values -- $progIntro@@ -349,12 +343,12 @@ sbvAvailableSolvers :: IO [SMTConfig] sbvAvailableSolvers = filterM sbvCheckSolverInstallation (map defaultSolverConfig [minBound .. maxBound]) -sbvWithAny :: Provable a => [SMTConfig] -> (SMTConfig -> a -> IO b) -> a -> IO (Solver, b)+sbvWithAny :: [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 :: [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 []
Data/SBV/BitVectors/Data.hs view
@@ -198,7 +198,7 @@ SBV a == SBV b = a == b SBV a /= SBV b = a /= b -instance HasKind a => HasKind (SBV a) where+instance HasKind (SBV a) where kindOf (SBV (SVal k _)) = k -- | Convert a symbolic value to a symbolic-word@@ -210,7 +210,7 @@ ------------------------------------------------------------------------- -- | Create a symbolic variable.-mkSymSBV :: forall a. SymWord a => Maybe Quantifier -> Kind -> Maybe String -> Symbolic (SBV a)+mkSymSBV :: forall a. Maybe Quantifier -> Kind -> Maybe String -> Symbolic (SBV a) mkSymSBV mbQ k mbNm = fmap SBV (svMkSymVar mbQ k mbNm) -- | Convert a symbolic value to an SW, inside the Symbolic monad@@ -441,7 +441,7 @@ addConstraint :: Maybe Double -> SBool -> SBool -> Symbolic () addConstraint mt (SBV c) (SBV c') = addSValConstraint mt c c' -instance NFData a => NFData (SBV a) where+instance NFData (SBV a) where rnf (SBV x) = rnf x `seq` () -- | Symbolically executable program fragments. This class is mainly used for 'safe' calls, and is sufficently populated internally to cover most use@@ -455,7 +455,7 @@ sName [] = sName_ sName xs = error $ "SBV.SExecutable.sName: Extra unmapped name(s): " ++ intercalate ", " xs -instance NFData a => SExecutable (SBV a) where+instance SExecutable (SBV a) where sName_ v = sName_ (output v) sName xs v = sName xs (output v) @@ -465,7 +465,7 @@ sName xs () = sName xs (output ()) -- List output-instance (NFData a, SymWord a) => SExecutable [SBV a] where+instance SExecutable [SBV a] where sName_ vs = sName_ (output vs) sName xs vs = sName xs (output vs)
Data/SBV/BitVectors/Floating.hs view
@@ -246,7 +246,7 @@ toSDouble = genericFPConverter (Just isExactRational) Nothing (fromRational . toRational) -- | Concretely evaluate one arg function, if rounding mode is RoundNearestTiesToEven and we have enough concrete data-concEval1 :: (SymWord a, Floating a) => Maybe (a -> a) -> Maybe SRoundingMode -> SBV a -> Maybe (SBV a)+concEval1 :: SymWord a => Maybe (a -> a) -> Maybe SRoundingMode -> SBV a -> Maybe (SBV a) concEval1 mbOp mbRm a = do op <- mbOp v <- unliteral a case join (unliteral `fmap` mbRm) of@@ -255,7 +255,7 @@ _ -> Nothing -- | Concretely evaluate two arg function, if rounding mode is RoundNearestTiesToEven and we have enough concrete data-concEval2 :: (SymWord a, Floating a) => Maybe (a -> a -> a) -> Maybe SRoundingMode -> SBV a -> SBV a -> Maybe (SBV a)+concEval2 :: SymWord a => Maybe (a -> a -> a) -> Maybe SRoundingMode -> SBV a -> SBV a -> Maybe (SBV a) concEval2 mbOp mbRm a b = do op <- mbOp v1 <- unliteral a v2 <- unliteral b@@ -265,7 +265,7 @@ _ -> Nothing -- | Concretely evaluate a bool producing two arg function, if rounding mode is RoundNearestTiesToEven and we have enough concrete data-concEval2B :: (SymWord a, Floating a) => Maybe (a -> a -> Bool) -> Maybe SRoundingMode -> SBV a -> SBV a -> Maybe SBool+concEval2B :: SymWord a => Maybe (a -> a -> Bool) -> Maybe SRoundingMode -> SBV a -> SBV a -> Maybe SBool concEval2B mbOp mbRm a b = do op <- mbOp v1 <- unliteral a v2 <- unliteral b@@ -275,7 +275,7 @@ _ -> Nothing -- | Concretely evaluate two arg function, if rounding mode is RoundNearestTiesToEven and we have enough concrete data-concEval3 :: (SymWord a, Floating a) => Maybe (a -> a -> a -> a) -> Maybe SRoundingMode -> SBV a -> SBV a -> SBV a -> Maybe (SBV a)+concEval3 :: SymWord a => Maybe (a -> a -> a -> a) -> Maybe SRoundingMode -> SBV a -> SBV a -> SBV a -> Maybe (SBV a) concEval3 mbOp mbRm a b c = do op <- mbOp v1 <- unliteral a v2 <- unliteral b@@ -292,7 +292,7 @@ return (swm : as) -- | Lift a 1 arg FP-op-lift1 :: (SymWord a, Floating a) => FPOp -> Maybe (a -> a) -> Maybe SRoundingMode -> SBV a -> SBV a+lift1 :: SymWord a => FPOp -> Maybe (a -> a) -> Maybe SRoundingMode -> SBV a -> SBV a lift1 w mbOp mbRm a | Just cv <- concEval1 mbOp mbRm a = cv@@ -304,7 +304,7 @@ newExpr st k (SBVApp (IEEEFP w) args) -- | Lift an FP predicate-lift1B :: (SymWord a, Floating a) => FPOp -> (a -> Bool) -> SBV a -> SBool+lift1B :: SymWord a => FPOp -> (a -> Bool) -> SBV a -> SBool lift1B w f a | Just v <- unliteral a = literal $ f v | True = SBV $ SVal KBool $ Right $ cache r@@ -313,7 +313,7 @@ -- | Lift a 2 arg FP-op-lift2 :: (SymWord a, Floating a) => FPOp -> Maybe (a -> a -> a) -> Maybe SRoundingMode -> SBV a -> SBV a -> SBV a+lift2 :: SymWord a => FPOp -> Maybe (a -> a -> a) -> Maybe SRoundingMode -> SBV a -> SBV a -> SBV a lift2 w mbOp mbRm a b | Just cv <- concEval2 mbOp mbRm a b = cv@@ -345,7 +345,7 @@ newExpr st k (SBVApp (IEEEFP w) args) -- | Lift a 2 arg FP-op, producing bool-lift2B :: (SymWord a, Floating a) => FPOp -> Maybe (a -> a -> Bool) -> Maybe SRoundingMode -> SBV a -> SBV a -> SBool+lift2B :: SymWord a => FPOp -> Maybe (a -> a -> Bool) -> Maybe SRoundingMode -> SBV a -> SBV a -> SBool lift2B w mbOp mbRm a b | Just cv <- concEval2B mbOp mbRm a b = cv@@ -357,7 +357,7 @@ newExpr st KBool (SBVApp (IEEEFP w) args) -- | Lift a 3 arg FP-op-lift3 :: (SymWord a, Floating a) => FPOp -> Maybe (a -> a -> a -> a) -> Maybe SRoundingMode -> SBV a -> SBV a -> SBV a -> SBV a+lift3 :: SymWord a => FPOp -> Maybe (a -> a -> a -> a) -> Maybe SRoundingMode -> SBV a -> SBV a -> SBV a -> SBV a lift3 w mbOp mbRm a b c | Just cv <- concEval3 mbOp mbRm a b c = cv
Data/SBV/BitVectors/Model.hs view
@@ -39,7 +39,7 @@ ) where -import Control.Monad (when, unless, liftM)+import Control.Monad (when, unless) import Control.Monad.Reader (ask) import Control.Monad.Trans (liftIO) @@ -85,11 +85,11 @@ -- Symbolic-Word class instances -- | Generate a finite symbolic bitvector, named-genVar :: (Random a, SymWord a) => Maybe Quantifier -> Kind -> String -> Symbolic (SBV a)+genVar :: Maybe Quantifier -> Kind -> String -> Symbolic (SBV a) genVar q k = mkSymSBV q k . Just -- | Generate a finite symbolic bitvector, unnamed-genVar_ :: (Random a, SymWord a) => Maybe Quantifier -> Kind -> Symbolic (SBV a)+genVar_ :: Maybe Quantifier -> Kind -> Symbolic (SBV a) genVar_ q k = mkSymSBV q k Nothing -- | Generate a finite constant bitvector@@ -102,7 +102,7 @@ genFromCW c = error $ "genFromCW: Unsupported non-integral value: " ++ show c -- | Generically make a symbolic var-genMkSymVar :: (Random a, SymWord a) => Kind -> Maybe Quantifier -> Maybe String -> Symbolic (SBV a)+genMkSymVar :: Kind -> Maybe Quantifier -> Maybe String -> Symbolic (SBV a) genMkSymVar k mbq Nothing = genVar_ mbq k genMkSymVar k mbq (Just s) = genVar mbq k s @@ -310,7 +310,7 @@ -- | label: Label the result of an expression. This is essentially a no-op, but useful as it generates a comment in the generated C/SMT-Lib code. -- Note that if the argument is a constant, then the label is dropped completely, per the usual constant folding strategy.-label :: (HasKind a, SymWord a) => String -> SBV a -> SBV a+label :: SymWord a => String -> SBV a -> SBV a label m x | Just _ <- unliteral x = x | True = SBV $ SVal k $ Right $ cache r@@ -589,7 +589,7 @@ logBase = lift2FNS "logBase" logBase -- | Lift a 1 arg FP-op, using sRNE default-lift1F :: (SymWord a, Floating a) => FPOp -> (a -> a) -> SBV a -> SBV a+lift1F :: SymWord a => FPOp -> (a -> a) -> SBV a -> SBV a lift1F w op a | Just v <- unliteral a = literal $ op v@@ -646,11 +646,11 @@ -- | Replacement for 'testBit'. Since 'testBit' requires a 'Bool' to be returned, -- we cannot implement it for symbolic words. Index 0 is the least-significant bit.-sTestBit :: (Num a, Bits a, SymWord a) => SBV a -> Int -> SBool+sTestBit :: SBV a -> Int -> SBool sTestBit (SBV x) i = SBV (svTestBit x i) -- | Variant of 'sTestBit', where we want to extract multiple bit positions.-sExtractBits :: (Num a, Bits a, SymWord a) => SBV a -> [Int] -> [SBool]+sExtractBits :: SBV a -> [Int] -> [SBool] sExtractBits x = map (sTestBit x) -- | Replacement for 'popCount'. Since 'popCount' returns an 'Int', we cannot implement@@ -817,7 +817,7 @@ blastBE = reverse . blastLE -- | Least significant bit of a word, always stored at index 0.-lsb :: (Num a, Bits a, SymWord a) => SBV a -> SBool+lsb :: SBV a -> SBool lsb x = sTestBit x 0 -- | Most significant bit of a word, always stored at the last position.@@ -1008,7 +1008,7 @@ -- | Lift 'QRem' to symbolic words. Division by 0 is defined s.t. @x/0 = 0@; which -- holds even when @x@ is @0@ itself.-liftQRem :: (SymWord a, Num a, SDivisible a) => SBV a -> SBV a -> (SBV a, SBV a)+liftQRem :: SymWord a => SBV a -> SBV a -> (SBV a, SBV a) liftQRem x y | isConcreteZero x = (x, x)@@ -1032,7 +1032,7 @@ -- | Lift 'DMod' to symbolic words. Division by 0 is defined s.t. @x/0 = 0@; which -- holds even when @x@ is @0@ itself. Essentially, this is conversion from quotRem -- (truncate to 0) to divMod (truncate towards negative infinity)-liftDMod :: (SymWord a, Num a, SDivisible a, SDivisible (SBV a)) => SBV a -> SBV a -> (SBV a, SBV a)+liftDMod :: (SymWord a, Num a, SDivisible (SBV a)) => SBV a -> SBV a -> (SBV a, SBV a) liftDMod x y | isConcreteZero x = (x, x)@@ -1073,7 +1073,7 @@ arbitrary = arbitrary >>= \r -> return $ SFunArray (const r) instance (SymWord a, Arbitrary a) => Arbitrary (SBV a) where- arbitrary = liftM literal arbitrary+ arbitrary = literal `fmap` arbitrary -- | Symbolic conditionals are modeled by the 'Mergeable' class, describing -- how to merge the results of an if-then-else call with a symbolic test. SBV@@ -1145,7 +1145,7 @@ -- | Symbolic assert. Check that the given boolean condition is always true in the given path. The -- optional first argument can be used to provide call-stack info via GHC's location facilities.-sAssert :: HasKind a => Maybe CallStack -> String -> SBool -> SBV a -> SBV a+sAssert :: Maybe CallStack -> String -> SBool -> SBV a -> SBV a sAssert cs msg cond x = SBV $ SVal k $ Right $ cache r where k = kindOf x r st = do xsw <- sbvToSW st x@@ -1188,7 +1188,7 @@ _ -> error $ "SBV.select: unsupported " ++ show (kindOf ind) ++ " valued select/index expression" r st = do sws <- mapM (sbvToSW st) xs swe <- sbvToSW st err- if all (== swe) sws -- off-chance that all elts are the same+ if all (== swe) sws -- off-chance that all elts are the same. Note that this also correctly covers the case when list is empty. then return swe else do idx <- getTableIndex st kInd kElt sws swi <- sbvToSW st ind
Data/SBV/BitVectors/Symbolic.hs view
@@ -16,9 +16,9 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE PatternGuards #-}-{-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE CPP #-} {-# OPTIONS_GHC -fno-warn-orphans #-} module Data.SBV.BitVectors.Symbolic@@ -63,7 +63,6 @@ import GHC.Stack.Compat import qualified Data.Generics as G (Data(..))-import qualified Data.Typeable as T (Typeable) import qualified Data.IntMap as IMap (IntMap, empty, size, toAscList, lookup, insert, insertWith) import qualified Data.Map as Map (Map, empty, toList, size, insert, lookup) import qualified Data.Set as Set (Set, empty, toList, insert)@@ -343,7 +342,13 @@ | True = ", aliasing " ++ show nm shui (nm, t) = " [uninterpreted] " ++ nm ++ " :: " ++ show t shax (nm, ss) = " -- user defined axiom: " ++ nm ++ "\n " ++ intercalate "\n " ss- shAssert (nm, stk, p) = " -- assertion: " ++ nm ++ " " ++ maybe "[No location]" showCallStack stk ++ ": " ++ show p+ shAssert (nm, stk, p) = " -- assertion: " ++ nm ++ " " ++ maybe "[No location]"+#if MIN_VERSION_base(4,9,0)+ prettyCallStack+#else+ showCallStack+#endif+ stk ++ ": " ++ show p -- | The context of a symbolic array as created data ArrayContext = ArrayFree (Maybe SW) -- ^ A new array, with potential initializer for each cell@@ -368,7 +373,7 @@ type KindSet = Set.Set Kind -- | Tables generated during a symbolic run-type TableMap = Map.Map [SW] (Int, Kind, Kind)+type TableMap = Map.Map (Kind, Kind, [SW]) Int -- | Representation for symbolic arrays type ArrayInfo = (String, (Kind, Kind), ArrayContext)@@ -558,12 +563,13 @@ -- | Create a new table; hash-cons as necessary getTableIndex :: State -> Kind -> Kind -> [SW] -> IO Int getTableIndex st at rt elts = do+ let key = (at, rt, elts) tblMap <- readIORef (rtblMap st)- case elts `Map.lookup` tblMap of- Just (i, _, _) -> return i- Nothing -> do let i = Map.size tblMap- modifyIORef (rtblMap st) (Map.insert elts (i, at, rt))- return i+ case key `Map.lookup` tblMap of+ Just i -> return i+ _ -> do let i = Map.size tblMap+ modifyIORef (rtblMap st) (Map.insert key i)+ return i -- | Create a new expression; hash-cons as necessary newExpr :: State -> Kind -> SBVExpr -> IO SW@@ -715,11 +721,12 @@ SBVPgm rpgm <- readIORef pgm inpsO <- reverse `fmap` readIORef inps outsO <- reverse `fmap` readIORef outs- let swap (a, b) = (b, a)- swapc ((_, a), b) = (b, a)- cmp (a, _) (b, _) = a `compare` b+ let swap (a, b) = (b, a)+ swapc ((_, a), b) = (b, a)+ cmp (a, _) (b, _) = a `compare` b+ arrange (i, (at, rt, es)) = ((i, at, rt), es) cnsts <- (sortBy cmp . map swapc . Map.toList) `fmap` readIORef (rconstMap st)- tbls <- (sortBy (\((x, _, _), _) ((y, _, _), _) -> x `compare` y) . map swap . Map.toList) `fmap` readIORef tables+ tbls <- (map arrange . sortBy cmp . map swap . Map.toList) `fmap` readIORef tables arrs <- IMap.toAscList `fmap` readIORef arrays unint <- Map.toList `fmap` readIORef uis axs <- reverse `fmap` readIORef axioms@@ -908,8 +915,8 @@ data SMTLibPgm = SMTLibPgm SMTLibVersion ( [(String, SW)] -- alias table , [String] -- pre: declarations. , [String]) -- post: formula-instance NFData SMTLibVersion where rnf a = seq a ()-instance NFData SMTLibPgm where rnf a = seq a ()+instance NFData SMTLibVersion where rnf a = a `seq` ()+instance NFData SMTLibPgm where rnf (SMTLibPgm v (t, d, p)) = rnf v `seq` rnf t `seq` rnf d `seq` rnf p `seq` () instance Show SMTLibPgm where show (SMTLibPgm _ (_, pre, post)) = intercalate "\n" $ pre ++ post@@ -918,28 +925,30 @@ instance NFData CW where rnf (CW x y) = x `seq` y `seq` () +#if MIN_VERSION_base(4,9,0)+#else -- Can't really force this, but not a big deal instance NFData CallStack where rnf _ = ()+#endif+ + instance NFData Result where rnf (Result kindInfo qcInfo cgs inps consts tbls arrs uis axs pgm cstr asserts outs) = rnf kindInfo `seq` rnf qcInfo `seq` rnf cgs `seq` rnf inps `seq` rnf consts `seq` rnf tbls `seq` rnf arrs `seq` rnf uis `seq` rnf axs `seq` rnf pgm `seq` rnf cstr `seq` rnf asserts `seq` rnf outs-instance NFData Kind where rnf a = seq a ()-instance NFData ArrayContext where rnf a = seq a ()-instance NFData SW where rnf a = seq a ()-instance NFData SBVExpr where rnf a = seq a ()-instance NFData Quantifier where rnf a = seq a ()-instance NFData SBVType where rnf a = seq a ()-instance NFData a => NFData (Cached a) where- rnf (Cached f) = f `seq` ()-instance NFData SVal where- rnf (SVal x y) = rnf x `seq` rnf y `seq` ()-instance NFData SBVPgm where rnf a = seq a ()-+instance NFData Kind where rnf a = seq a ()+instance NFData ArrayContext where rnf a = seq a ()+instance NFData SW where rnf a = seq a ()+instance NFData SBVExpr where rnf a = seq a ()+instance NFData Quantifier where rnf a = seq a ()+instance NFData SBVType where rnf a = seq a ()+instance NFData SBVPgm where rnf a = seq a ()+instance NFData (Cached a) where rnf (Cached f) = f `seq` ()+instance NFData SVal where rnf (SVal x y) = rnf x `seq` rnf y `seq` () instance NFData SMTResult where rnf (Unsatisfiable _) = ()@@ -1021,7 +1030,7 @@ | RoundTowardPositive -- ^ Round towards positive infinity. (Also known as rounding-up or ceiling.) | RoundTowardNegative -- ^ Round towards negative infinity. (Also known as rounding-down or floor.) | RoundTowardZero -- ^ Round towards zero. (Also known as truncation.)- deriving (Eq, Ord, Show, Read, T.Typeable, G.Data, Bounded, Enum)+ deriving (Eq, Ord, Show, Read, G.Data, Bounded, Enum) -- | 'RoundingMode' kind instance HasKind RoundingMode
Data/SBV/Compilers/C.hs view
@@ -9,6 +9,7 @@ -- Compilation of symbolic programs to C ----------------------------------------------------------------------------- +{-# LANGUAGE CPP #-} {-# LANGUAGE PatternGuards #-} module Data.SBV.Compilers.C(compileToC, compileToCLib, compileToC', compileToCLib') where@@ -28,7 +29,9 @@ import Data.SBV.Compilers.CodeGen import GHC.Stack.Compat+#if !MIN_VERSION_base(4,9,0) import GHC.SrcLoc.Compat+#endif --------------------------------------------------------------------------- -- * API
Data/SBV/Compilers/CodeGen.hs view
@@ -231,7 +231,7 @@ return rs -- | Creates an atomic output in the generated code.-cgOutput :: SymWord a => String -> SBV a -> SBVCodeGen ()+cgOutput :: String -> SBV a -> SBVCodeGen () cgOutput nm v = do _ <- liftSymbolic (output v) sw <- cgSBVToSW v modify (\s -> s { cgOutputs = (nm, CgAtomic sw) : cgOutputs s })@@ -246,7 +246,7 @@ where sz = length vs -- | Creates a returned (unnamed) value in the generated code.-cgReturn :: SymWord a => SBV a -> SBVCodeGen ()+cgReturn :: SBV a -> SBVCodeGen () cgReturn v = do _ <- liftSymbolic (output v) sw <- cgSBVToSW v modify (\s -> s { cgReturns = CgAtomic sw : cgReturns s })
Data/SBV/Examples/Misc/Floating.hs view
@@ -56,18 +56,18 @@ -- -- >>> assocPlusRegular -- Falsifiable. Counter-example:--- x = -1.5991211e-2 :: Float--- y = 131071.99 :: Float--- z = -131069.99 :: Float+-- x = 5.5511693e-15 :: Float+-- y = -2.2204438e-16 :: Float+-- z = -3.1763606e-21 :: Float -- -- Indeed, we have: ----- >>> ((-1.5991211e-2) + (131071.99 + (-131069.99))) :: Float--- 1.9840088--- >>> ((-1.5991211e-2) + 131071.99) + (-131069.99) :: Float--- 1.984375+-- >>> ((5.5511693e-15) + ((-2.2204438e-16) + (-3.1763606e-21))) :: Float+-- 5.3291218e-15+-- >>> (((5.5511693e-15) + (-2.2204438e-16)) + (-3.1763606e-21)) :: Float+-- 5.329122e-15 ----- Note the significant difference between two additions!+-- Note the difference between two additions! assocPlusRegular :: IO ThmResult assocPlusRegular = prove $ do [x, y, z] <- sFloats ["x", "y", "z"] let lhs = x+(y+z)@@ -118,13 +118,13 @@ -- -- >>> multInverse -- Falsifiable. Counter-example:--- a = -7.883512939128398e-261 :: Double+-- a = 8.988465674311586e307 :: Double -- -- Indeed, we have: ----- >>> let a = -7.883512939128398e-261 :: Double+-- >>> let a = 8.988465674311586e307 :: Double -- >>> a * (1/a)--- 0.9999999999999999+-- 1.0000000000000002 multInverse :: IO ThmResult multInverse = prove $ do a <- sDouble "a" constrain $ fpIsPoint a@@ -145,28 +145,34 @@ -- -- >>> roundingAdd -- Satisfiable. Model:--- rm = RoundTowardZero :: RoundingMode--- x = 7.984373 :: Float--- y = -2.1684042e-19 :: Float+-- rm = RoundTowardPositive :: RoundingMode+-- x = 1.9531249 :: Float+-- y = 6.2499996e-2 :: Float -- -- (Note that depending on your version of Z3, you might get a different result.) -- Unfortunately we can't directly validate this result at the Haskell level, as Haskell only supports -- 'RoundNearestTiesToEven'. We have: ----- >>> (7.984373 + (-2.1684042e-19)) :: Float--- 7.984373+-- >>> (1.9531249 + 6.2499996e-2) :: Float+-- 2.0156248 ----- While we cannot directly see the result when the mode is 'RoundTowardZero' in Haskell, we can use+-- While we cannot directly see the result when the mode is 'RoundTowardPositive' in Haskell, we can use -- SBV to provide us with that result thusly: ----- >>> sat $ \z -> z .== fpAdd sRoundTowardZero 7.984373 (-2.1684042e-19 :: SFloat)+-- >>> sat $ \z -> z .== fpAdd sRoundTowardPositive 1.9531249 (6.2499996e-2 :: SFloat) -- Satisfiable. Model:--- s0 = 7.9843726 :: Float+-- s0 = 2.015625 :: Float ----- We can see why these two resuls are indeed different. To see why, one would have to convert the--- individual numbers to Float's, which would induce rounding-errors, add them up, and round-back;--- a tedious operation, but one that might prove illimunating for the interested reader. We'll merely--- note that floating point representation and semantics is indeed a thorny+-- We can see why these two resuls are indeed different. But we can see that the 'RoundTowardsPositive'+-- (which rounds towards positive-infinity) produces a larger result. Indeed, if we treat these numbers+-- as 'Double' values, we get:+--+-- >>> (1.9531249 + 6.2499996e-2) :: Double+-- 2.015624896+--+-- we see that the "more precise" result is larger than what the 'Float' value is, justifying the+-- larger value with 'RoundTowardPositive'. A more detailed study is beyond our current scope, so we'll+-- merely -- note that floating point representation and semantics is indeed a thorny -- subject, and point to <https://ece.uwaterloo.ca/~dwharder/NumericalAnalysis/02Numerics/Double/paper.pdf> as -- an excellent guide. roundingAdd :: IO SatResult
Data/SBV/Examples/Misc/NoDiv0.hs view
@@ -28,8 +28,7 @@ -- this to be safe: -- -- >>> test1--- [Data/SBV/Examples/Misc/NoDiv0.hs:22:32:?loc,--- Data/SBV/Examples/Misc/NoDiv0.hs:37:14:checkedDiv: Divisor should not be 0: Violated. Model:+-- [Data/SBV/Examples/Misc/NoDiv0.hs:36:14:checkedDiv: Divisor should not be 0: Violated. Model: -- s0 = 0 :: Int32 -- s1 = 0 :: Int32] --@@ -39,8 +38,7 @@ -- | Repeat the test, except this time we explicitly protect against the bad case. We have: -- -- >>> test2--- [Data/SBV/Examples/Misc/NoDiv0.hs:22:32:?loc,--- Data/SBV/Examples/Misc/NoDiv0.hs:46:41:checkedDiv: Divisor should not be 0: No violations detected]+-- [Data/SBV/Examples/Misc/NoDiv0.hs:44:41:checkedDiv: Divisor should not be 0: No violations detected] -- test2 :: IO [SafeResult] test2 = safe $ \x y -> ite (y .== 0) 3 (checkedDiv x y)
Data/SBV/Provers/Prover.hs view
@@ -9,6 +9,7 @@ -- Provable abstraction and the connection to SMT solvers ----------------------------------------------------------------------------- +{-# LANGUAGE CPP #-} {-# LANGUAGE BangPatterns #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE NamedFieldPuns #-}@@ -38,7 +39,9 @@ import System.IO.Unsafe (unsafeInterleaveIO) import GHC.Stack.Compat+#if !MIN_VERSION_base(4,9,0) import GHC.SrcLoc.Compat+#endif import qualified Data.Set as Set (Set, toList) @@ -47,6 +50,8 @@ import Data.SBV.SMT.SMTLib import Data.SBV.Utils.TDiff +import Control.DeepSeq (rnf)+ import qualified Data.SBV.Provers.Boolector as Boolector import qualified Data.SBV.Provers.CVC4 as CVC4 import qualified Data.SBV.Provers.Yices as Yices@@ -478,7 +483,9 @@ where go [] (_, sofar) = reverse sofar go ((ALL, (v, _)):rest) (us, sofar) = go rest (v:us, Left v : sofar) go ((EX, (v, _)):rest) (us, sofar) = go rest (us, Right (v, reverse us) : sofar)- in return (is, skolemMap, ki, assertions, converter (roundingMode config) (useLogic config) solverCaps ki isSat comments is skolemMap consts tbls arrs uis axs pgm cstrs o)+ smtScript = converter (roundingMode config) (useLogic config) solverCaps ki isSat comments is skolemMap consts tbls arrs uis axs pgm cstrs o+ result = (is, skolemMap, ki, assertions, smtScript)+ in rnf smtScript `seq` return result Result{resOutputs = os} -> case length os of 0 -> error $ "Impossible happened, unexpected non-outputting result\n" ++ show res 1 -> error $ "Impossible happened, non-boolean output in " ++ show os
Data/SBV/SMT/SMT.hs view
@@ -364,7 +364,7 @@ valWidth = maximum $ 0 : [l | (_, (l, _)) <- svs] right p s = s ++ replicate p ' ' left p s = replicate p ' ' ++ s- vlength s = case dropWhile (/= ':') (reverse s) of+ vlength s = case dropWhile (/= ':') (reverse (takeWhile (/= '\n') s)) of (':':':':r) -> length (dropWhile isSpace r) _ -> length s -- conservative valPart "" = ""@@ -543,7 +543,7 @@ else return [] return $ Just (r, vals) cleanUp response- executeSolver `C.onException` terminateProcess pid+ executeSolver `C.onException` (terminateProcess pid >> waitForProcess 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
Data/SBV/Utils/Numeric.hs view
@@ -12,13 +12,13 @@ module Data.SBV.Utils.Numeric where -- | A variant of round; except defaulting to 0 when fed NaN or Infinity-fpRound0 :: (RealFloat a, RealFrac a, Integral b) => a -> b+fpRound0 :: (RealFloat a, Integral b) => a -> b fpRound0 x | isNaN x || isInfinite x = 0 | True = round x -- | A variant of toRational; except defaulting to 0 when fed NaN or Infinity-fpRatio0 :: (RealFloat a, RealFrac a) => a -> Rational+fpRatio0 :: (RealFloat a) => a -> Rational fpRatio0 x | isNaN x || isInfinite x = 0 | True = toRational x@@ -76,8 +76,7 @@ ry = toRational y rd = rx / ry d :: Integer- d | rd > 0 = floor rd- | True = ceiling rd+ d = round rd -- If the result is 0, make sure we preserve the sign of x pSign r | r == 0 = if x < 0 || isNegativeZero x then -0.0 else 0.0
GHC/SrcLoc/Compat.hs view
@@ -1,26 +1,11 @@ {-# LANGUAGE CPP #-} --- | Compatibility shim for GHC 7.8 support. Remove once 7.8 is no--- longer supported.--#if MIN_VERSION_base(4,8,0)+-- | Compatibility shims for the SrcLoc interface across GHC versions -module GHC.SrcLoc.Compat (module GHC.SrcLoc) where-import GHC.SrcLoc+module GHC.SrcLoc.Compat (module X) where +#if MIN_VERSION_base(4,9,0)+import SrcLoc as X hiding (srcLocFile) #else--module GHC.SrcLoc.Compat {-# WARNING "This version of GHC does not support SrcLoc; using a stub interface for compatibility" #-} (module GHC.SrcLoc.Compat) where--data SrcLoc--srcLocFile :: SrcLoc -> String-srcLocFile _ = ""--srcLocStartLine :: SrcLoc -> Int-srcLocStartLine _ = 0--srcLocStartCol :: SrcLoc -> Int-srcLocStartCol _ = 0-+import GHC.SrcLoc as X #endif
GHC/Stack/Compat.hs view
@@ -1,25 +1,6 @@ {-# LANGUAGE CPP #-} --- | Compatibility shim for GHC 7.8 support. Remove once 7.8 is no--- longer supported.--#if MIN_VERSION_base(4,8,0)+-- | Compatibility shims for the Stack interface across GHC versions module GHC.Stack.Compat (module GHC.Stack) where import GHC.Stack--#else--module GHC.Stack.Compat {-# WARNING "This version of GHC does not support SrcLoc; using a stub interface for compatibility" #-} (module GHC.Stack.Compat) where--import GHC.SrcLoc.Compat--data CallStack--getCallStack :: CallStack -> [(String, SrcLoc)]-getCallStack _ = []--showCallStack :: CallStack -> String-showCallStack _ = "CallStack not supported in GHC older than 7.10"--#endif
SBVUnitTest/SBVUnitTestBuildTime.hs view
@@ -2,4 +2,4 @@ module SBVUnitTestBuildTime (buildTime) where buildTime :: String-buildTime = "Thu Jan 14 23:22:03 PST 2016"+buildTime = "Mon Jun 6 17:13:43 PDT 2016"
SBVUnitTest/TestSuite/Arrays/Memory.hs view
@@ -27,4 +27,4 @@ t3 = free "a" >>= \a -> free "x" >>= \x -> free "b" >>= \b -> free "y" >>= \y -> newArray "m" Nothing >>= return . wcommutesGood (a, x) (b, y) t4 = free "a" >>= \a -> free "x" >>= \x -> free "b" >>= \b -> free "y" >>= \y -> newArray "m" Nothing >>= return . wcommutesBad (a, x) (b, y) -{-# ANN module ("HLint: ignore Use liftM" :: String) #-}+{-# ANN module ("HLint: ignore Use fmap" :: String) #-}
SBVUnitTest/TestSuite/Basics/ArithNoSolver.hs view
@@ -370,6 +370,7 @@ ++ concatMap (checkPred ds sds) predicates extract :: SymWord a => SBV a -> a extract = fromJust . unliteral+ comb (x, y, a, b) = (show x, show y, same a b) combB (x, y, a, b) = (show x, show y, checkNaN f x y a b) where f v w = not (v || w) -- All comparisons except /=: Both should be False if we have a NaN argument combN (x, y, a, b) = (show x, show y, checkNaN f x y a b) where f v w = v && w -- /=: Both should be True@@ -379,13 +380,17 @@ checkNaN f x y a b | isNaN x || isNaN y = f a b | True = a == b+ cvtTest (nm, x, a, b) = "arithCF-" ++ nm ++ "." ++ x ~: same (extract a) (extract b) `showsAs` "True" cvtTestI (nm, x, a, b) = "arithCF-" ++ nm ++ "." ++ x ~: (a == b) `showsAs` "True"+ mkTest1 (nm, (x, s)) = "arithCF-" ++ nm ++ "." ++ x ~: s `showsAs` "True" mkTest2 (nm, (x, y, s)) = "arithCF-" ++ nm ++ "." ++ x ++ "_" ++ y ~: s `showsAs` "True"- checkPred :: (Show a, RealFloat a, Floating a, SymWord a) => [a] -> [SBV a] -> (String, SBV a -> SBool, a -> Bool) -> [(String, (String, Bool))]++ checkPred :: Show a => [a] -> [SBV a] -> (String, SBV a -> SBool, a -> Bool) -> [(String, (String, Bool))] checkPred xs sxs (n, ps, p) = zipWith (chk n) (map (\x -> (x, p x)) xs) (map ps sxs) where chk nm (x, v) sv = (nm, (show x, Just v == unliteral sv))+ predicates :: IEEEFloating a => [(String, SBV a -> SBool, a -> Bool)] predicates = [ ("fpIsNormal", fpIsNormal, fpIsNormalizedH) , ("fpIsSubnormal", fpIsSubnormal, isDenormalized)@@ -400,8 +405,10 @@ ] -- Concrete test data-xsSigned, xsUnsigned :: (Num a, Enum a, Bounded a) => [a]+xsUnsigned :: (Num a, Bounded a) => [a] xsUnsigned = take 5 (iterate (1+) minBound) ++ take 5 (iterate (\x -> x-1) maxBound)++xsSigned :: (Num a, Enum a, Bounded a) => [a] xsSigned = xsUnsigned ++ [-5 .. 5] w8s :: [Word8]
SBVUnitTest/TestSuite/Basics/ArithSolver.hs view
@@ -437,7 +437,7 @@ noOverflow x y = not (x == minBound && y == -1) -- Concrete test data-xsSigned, xsUnsigned :: (Num a, Enum a, Bounded a) => [a]+xsSigned, xsUnsigned :: (Num a, Bounded a) => [a] xsUnsigned = [0, 1, maxBound - 1, maxBound] xsSigned = xsUnsigned ++ [minBound, minBound + 1, -1]
sbv.cabal view
@@ -1,5 +1,5 @@ Name: sbv-Version: 5.11+Version: 5.12 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@@ -29,6 +29,7 @@ ghc-options : -Wall other-extensions: BangPatterns DefaultSignatures+ DeriveAnyClass DeriveDataTypeable FlexibleContexts FlexibleInstances@@ -44,10 +45,9 @@ TupleSections TypeOperators TypeSynonymInstances- if impl(ghc >= 7.10.1)- other-extensions: DeriveAnyClass- Build-Depends : base >= 4.7 && < 5+ Build-Depends : base >= 4.8 && < 5 , base-compat >= 0.6+ , ghc , array, async, containers, deepseq, directory, filepath, old-time , pretty, process, mtl, QuickCheck, random, syb, data-binary-ieee754 , crackNum@@ -60,46 +60,45 @@ , Data.SBV.Bridge.ABC , Data.SBV.Dynamic , Data.SBV.Internals- if impl(ghc >= 7.10.1)- exposed-modules : Data.SBV.Examples.BitPrecise.BitTricks- , Data.SBV.Examples.BitPrecise.Legato- , Data.SBV.Examples.BitPrecise.MergeSort- , Data.SBV.Examples.BitPrecise.MultMask- , Data.SBV.Examples.BitPrecise.PrefixSum- , Data.SBV.Examples.CodeGeneration.AddSub- , Data.SBV.Examples.CodeGeneration.CRC_USB5- , Data.SBV.Examples.CodeGeneration.Fibonacci- , Data.SBV.Examples.CodeGeneration.GCD- , Data.SBV.Examples.CodeGeneration.PopulationCount- , Data.SBV.Examples.CodeGeneration.Uninterpreted- , Data.SBV.Examples.Crypto.AES- , Data.SBV.Examples.Crypto.RC4- , Data.SBV.Examples.Existentials.CRCPolynomial- , Data.SBV.Examples.Existentials.Diophantine- , Data.SBV.Examples.Misc.Enumerate- , Data.SBV.Examples.Misc.Floating- , Data.SBV.Examples.Misc.ModelExtract- , Data.SBV.Examples.Misc.Auxiliary- , Data.SBV.Examples.Misc.NoDiv0- , Data.SBV.Examples.Misc.Word4- , Data.SBV.Examples.Polynomials.Polynomials- , Data.SBV.Examples.Puzzles.Birthday- , Data.SBV.Examples.Puzzles.Coins- , Data.SBV.Examples.Puzzles.Counts- , Data.SBV.Examples.Puzzles.DogCatMouse- , Data.SBV.Examples.Puzzles.Euler185- , Data.SBV.Examples.Puzzles.Fish- , Data.SBV.Examples.Puzzles.MagicSquare- , Data.SBV.Examples.Puzzles.NQueens- , Data.SBV.Examples.Puzzles.SendMoreMoney- , Data.SBV.Examples.Puzzles.Sudoku- , Data.SBV.Examples.Puzzles.U2Bridge- , Data.SBV.Examples.Uninterpreted.AUF- , Data.SBV.Examples.Uninterpreted.Deduce- , Data.SBV.Examples.Uninterpreted.Function- , Data.SBV.Examples.Uninterpreted.Shannon- , Data.SBV.Examples.Uninterpreted.Sort- , Data.SBV.Examples.Uninterpreted.UISortAllSat+ , Data.SBV.Examples.BitPrecise.BitTricks+ , Data.SBV.Examples.BitPrecise.Legato+ , Data.SBV.Examples.BitPrecise.MergeSort+ , Data.SBV.Examples.BitPrecise.MultMask+ , Data.SBV.Examples.BitPrecise.PrefixSum+ , Data.SBV.Examples.CodeGeneration.AddSub+ , Data.SBV.Examples.CodeGeneration.CRC_USB5+ , Data.SBV.Examples.CodeGeneration.Fibonacci+ , Data.SBV.Examples.CodeGeneration.GCD+ , Data.SBV.Examples.CodeGeneration.PopulationCount+ , Data.SBV.Examples.CodeGeneration.Uninterpreted+ , Data.SBV.Examples.Crypto.AES+ , Data.SBV.Examples.Crypto.RC4+ , Data.SBV.Examples.Existentials.CRCPolynomial+ , Data.SBV.Examples.Existentials.Diophantine+ , Data.SBV.Examples.Misc.Enumerate+ , Data.SBV.Examples.Misc.Floating+ , Data.SBV.Examples.Misc.ModelExtract+ , Data.SBV.Examples.Misc.Auxiliary+ , Data.SBV.Examples.Misc.NoDiv0+ , Data.SBV.Examples.Misc.Word4+ , Data.SBV.Examples.Polynomials.Polynomials+ , Data.SBV.Examples.Puzzles.Birthday+ , Data.SBV.Examples.Puzzles.Coins+ , Data.SBV.Examples.Puzzles.Counts+ , Data.SBV.Examples.Puzzles.DogCatMouse+ , Data.SBV.Examples.Puzzles.Euler185+ , Data.SBV.Examples.Puzzles.Fish+ , Data.SBV.Examples.Puzzles.MagicSquare+ , Data.SBV.Examples.Puzzles.NQueens+ , Data.SBV.Examples.Puzzles.SendMoreMoney+ , Data.SBV.Examples.Puzzles.Sudoku+ , Data.SBV.Examples.Puzzles.U2Bridge+ , Data.SBV.Examples.Uninterpreted.AUF+ , Data.SBV.Examples.Uninterpreted.Deduce+ , Data.SBV.Examples.Uninterpreted.Function+ , Data.SBV.Examples.Uninterpreted.Shannon+ , Data.SBV.Examples.Uninterpreted.Sort+ , Data.SBV.Examples.Uninterpreted.UISortAllSat Other-modules : Data.SBV.BitVectors.AlgReals , Data.SBV.BitVectors.Concrete , Data.SBV.BitVectors.Data@@ -144,11 +143,8 @@ RankNTypes ScopedTypeVariables TupleSections- if impl(ghc >= 7.10.1)- Build-depends : base >= 4.8 && < 5- , HUnit, directory, filepath, process, syb, sbv, data-binary-ieee754- else- Buildable : False+ Build-depends : base >= 4.8 && < 5+ , HUnit, directory, filepath, process, syb, sbv, data-binary-ieee754 Hs-Source-Dirs : SBVUnitTest main-is : SBVUnitTest.hs Other-modules : SBVUnitTestBuildTime@@ -218,11 +214,8 @@ type : exitcode-stdio-1.0 default-language: Haskell2010 ghc-options : -Wall -with-rtsopts=-K64m- if impl(ghc >= 7.10.1)- Build-depends : base >= 4.8 && < 5- , HUnit, directory, filepath, syb, sbv, data-binary-ieee754- else- Buildable : False+ Build-depends : base >= 4.8 && < 5+ , HUnit, directory, filepath, syb, sbv, data-binary-ieee754 Hs-Source-Dirs : SBVUnitTest main-is : SBVBasicTests.hs Other-modules : SBVBasicTests