sbv 1.0 → 1.1

raw patch · 11 files changed

+94/−28 lines, 11 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• Data/SBV.hs +3/−3
• Data/SBV/BitVectors/Model.hs +41/−12
• Data/SBV/Examples/BitPrecise/Legato.hs +2/−2
• Data/SBV/Examples/Existentials/CRCPolynomial.hs +1/−1
• Data/SBV/Provers/Prover.hs +26/−2
• Data/SBV/Provers/Z3.hs +1/−1
• INSTALL +3/−3
• RELEASENOTES +14/−1
• SBVUnitTest/SBVUnitTestBuildTime.hs +1/−1
• SBVUnitTest/TestSuite/Existentials/CRCPolynomial.hs +1/−1
• sbv.cabal +1/−1

@@ -112,7 +112,7 @@   , STree, readSTree, writeSTree, mkSTree   -- ** Operations on symbolic words   -- *** Word level-  , bitValue, setBitTo, oneIf, lsb, msb+  , sbvTestBit, sbvPopCount, setBitTo, oneIf, lsb, msb   -- *** List level   , allEqual, allDifferent   -- *** Blasting/Unblasting@@ -181,13 +181,13 @@   , SatModel(..), Modelable(..), displayModels, extractModels    -- * SMT Interface: Configurations and solvers-  , SMTConfig(..), OptimizeOpts(..), SMTSolver(..), yices, z3, defaultSMTCfg+  , SMTConfig(..), OptimizeOpts(..), SMTSolver(..), yices, z3, defaultSMTCfg, sbvCheckSolverInstallation    -- * Symbolic computations   , Symbolic, output, SymWord(..)    -- * Getting SMT-Lib output (for offline analysis)-  , compileToSMTLib+  , compileToSMTLib, generateSMTBenchmarks    -- * Test case generation   , genTest, getTestValues, TestVectors, TestStyle(..), renderTest, CW(..), Size(..), cwToBool

@@ -11,7 +11,9 @@ -----------------------------------------------------------------------------  {-# OPTIONS_GHC -fno-warn-orphans   #-}+{-# LANGUAGE CPP                    #-} {-# LANGUAGE TypeSynonymInstances   #-}+{-# LANGUAGE BangPatterns           #-} {-# LANGUAGE PatternGuards          #-} {-# LANGUAGE FlexibleInstances      #-} {-# LANGUAGE MultiParamTypeClasses  #-}@@ -21,7 +23,7 @@  module Data.SBV.BitVectors.Model (     Mergeable(..), EqSymbolic(..), OrdSymbolic(..), BVDivisible(..), Uninterpreted(..)-  , bitValue, setBitTo, allEqual, allDifferent, oneIf, blastBE, blastLE+  , sbvTestBit, sbvPopCount, setBitTo, allEqual, allDifferent, oneIf, blastBE, blastLE   , lsb, msb, SBVUF, sbvUFName, genFinVar, genFinVar_, forall, forall_, exists, exists_   , constrain, pConstrain   )@@ -453,10 +455,7 @@    | hasSign a = ite (a .< 0) (-1) (ite (a .== 0) 0 1)    | True      = oneIf (a ./= 0) --- NB. The default definition of "testBit" relies on equality,--- which is not available for symbolic SBV's. There is no--- way to implement testBit to return Bool, obviously; instead use bitValue--- Also, in the optimizations below, use of -1 is valid as+-- NB. In the optimizations below, use of -1 is valid as -- -1 has all bits set to True for both signed and unsigned values instance (Bits a, SymWord a) => Bits (SBV a) where   x .&. y@@ -496,6 +495,18 @@     | y == 0               = x     | not (isInfPrec x)    = let sz = bitSize x in liftSym1 (mkSymOp1 (Ror (y `mod` sz))) (rot False sz y) 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+    | isConcrete x         = (x .&. bit i) /= 0+    | True                 = error $ "SBV.testBit: Called on symbolic value: " ++ show x ++ ". Use sbvTestBit instead."+#if __GLASGOW_HASKELL__ >= 704+  -- NB. popCount is *not* implementable on non-concrete symbolic words+  popCount x+    | isConcrete x        = let go !c 0 = c+                                go !c w = go (c+1) (w .&. (w-1))+                            in go 0 x+    | True                = error $ "SBV.popCount: Called on symbolic value: " ++ show x ++ ". Use sbvPopCount instead."+#endif  -- Since the underlying representation is just Integers, rotations has to be careful on the bit-size rot :: Bool -> Int -> Int -> Integer -> Integer@@ -508,12 +519,30 @@  -- | 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.-bitValue :: (Bits a, SymWord a) => SBV a -> Int -> SBool-bitValue x i = (x .&. bit i) ./= 0+sbvTestBit :: (Bits a, SymWord a) => SBV a -> Int -> SBool+sbvTestBit x i = (x .&. bit i) ./= 0 +-- | Replacement for 'popCount'. Since 'popCount' returns an 'Int', we cannot implement+-- it for symbolic words. Here, we return an 'SWord8', which can overflow when used on+-- quantities that have more than 255 bits. Currently, that's only the 'SInteger' type+-- that SBV supports, all other types are safe. Even with 'SInteger', this will only+-- overflow if there are at least 256-bits set in the number, and the smallest such+-- number is 2^256-1, which is a pretty darn big number to worry about for practical+-- purposes. In any case, we do not support 'sbvPopCount' for unbounded symbolic integers,+-- as the only possible implementation wouldn't symbolically terminate. So the only overflow+-- issue is with really-really large concrete 'SInteger' values +sbvPopCount :: (Bits a, SymWord a) => SBV a -> SWord8+sbvPopCount x+  | isConcrete x = go 0 x+  | isInfPrec  x = error "SBV.sbvPopCount: Called on an infinite precision symbolic value"+  | True         = sum [ite b 1 0 | b <- blastLE x]+  where -- concrete case+        go !c 0 = c+        go !c w = go (c+1) (w .&. (w-1))+ -- | Generalization of 'setBit' based on a symbolic boolean. Note that 'setBit' and -- 'clearBit' are still available on Symbolic words, this operation comes handy when--- the condition to set/clear happens to be symbolic+-- the condition to set/clear happens to be symbolic. setBitTo :: (Bits a, SymWord a) => SBV a -> Int -> SBool -> SBV a setBitTo x i b = ite b (setBit x i) (clearBit x i) @@ -521,7 +550,7 @@ blastLE :: (Bits a, SymWord a) => SBV a -> [SBool] blastLE x  | isInfPrec x = error "SBV.blastLE: Called on an infinite precision value"- | True        = map (bitValue x) [0 .. (intSizeOf x)-1]+ | True        = map (sbvTestBit x) [0 .. (intSizeOf x)-1]  -- | Big-endian blasting of a word into its bits. Also see the 'FromBits' class blastBE :: (Bits a, SymWord a) => SBV a -> [SBool]@@ -529,13 +558,13 @@  -- | Least significant bit of a word, always stored at index 0 lsb :: (Bits a, SymWord a) => SBV a -> SBool-lsb x = bitValue x 0+lsb x = sbvTestBit x 0  -- | Most significant bit of a word, always stored at the last position msb :: (Bits a, SymWord a) => SBV a -> SBool msb x  | isInfPrec x = error "SBV.msb: Called on an infinite precision value"- | True        = bitValue x ((intSizeOf x) - 1)+ | True        = sbvTestBit x ((intSizeOf x) - 1)  -- Enum instance. These instances are suitable for use with concrete values, -- and will be less useful for symbolic values around. Note that `fromEnum` requires@@ -716,7 +745,7 @@     | hasSign ind    = ite (ind .< 0) err $ result     | True           = result     where result = go xs $ reverse (zip [(0::Integer)..] bits)-          bits   = map (ind `bitValue`) [0 .. bitSize ind - 1]+          bits   = map (ind `sbvTestBit`) [0 .. bitSize ind - 1]           go []    _            = err           go (x:_) []           = x           go elts  ((n, b):nbs) = let (ys, zs) = genericSplitAt ((2::Integer) ^ n) elts

@@ -166,7 +166,7 @@   where v  = peek a m         c  = getFlag FlagC m         v' = setBitTo (v `rotateR` 1) 7 c-        c' = bitValue v 0+        c' = sbvTestBit v 0  -- | ROR, register version: Same as 'rorM', except through register @r@. rorR :: Register -> Instruction@@ -174,7 +174,7 @@   where v  = getReg r m         c  = getFlag FlagC m         v' = setBitTo (v `rotateR` 1) 7 c-        c' = bitValue v 0+        c' = sbvTestBit v 0  -- | BCC: branch to label @l@ if the carry flag is false bcc :: Program -> Instruction

@@ -72,7 +72,7 @@                         -- the least significant bit must be set in the                         -- polynomial, as all CRC polynomials have the "+1"                         -- term in them set. This simplifies the query.-                        return $ bitValue p 0 &&& crcGood hd p s r+                        return $ sbvTestBit p 0 &&& crcGood hd p s r                 cnt <- displayModels disp res                 putStrLn $ "Found: " ++ show cnt ++ " polynomail(s)."         where disp :: Int -> (Bool, Word16) -> IO ()

@@ -29,7 +29,8 @@        , isVacuous, isVacuousWith        , SatModel(..), Modelable(..), displayModels, extractModels        , yices, z3, defaultSMTCfg-       , compileToSMTLib+       , compileToSMTLib, generateSMTBenchmarks+       , sbvCheckSolverInstallation        ) where  import qualified Control.Exception as E@@ -39,6 +40,7 @@ import Control.Monad                  (when) import Data.List                      (intercalate) import Data.Maybe                     (fromJust, isJust, catMaybes)+import System.FilePath                (addExtension) import System.Time                    (getClockTime)  import Data.SBV.BitVectors.Data@@ -311,8 +313,22 @@         let comments = ["Created on " ++ show t]             cvt = if smtLib2 then toSMTLib2 else toSMTLib1         (_, _, _, smtLibPgm) <- simulate cvt defaultSMTCfg False comments a-        return $ show smtLibPgm ++ "\n"+        let out = show smtLibPgm+        if smtLib2 -- append check-sat in case of smtLib2+           then return $ out ++ "\n(check-sat)\n"+           else return $ out ++ "\n" +-- | Create both SMT-Lib1 and SMT-Lib2 benchmarks. The first argument is the basename of the file,+-- SMT-Lib1 version will be written with suffix ".smt1" and SMT-Lib2 version will be written with+-- suffix ".smt2"+generateSMTBenchmarks :: Provable a => FilePath -> a -> IO ()+generateSMTBenchmarks f a = gen False smt1 >> gen True smt2+  where smt1     = addExtension f "smt1"+        smt2     = addExtension f "smt2"+        gen b fn = do s <- compileToSMTLib b a+                      writeFile fn s+                      putStrLn $ "Generated SMT benchmark " ++ show fn ++ "."+ -- | Proves the predicate using the given SMT-solver proveWith :: Provable a => SMTConfig -> a -> IO ThmResult proveWith config a = simulate cvt config False [] a >>= callSolver False "Checking Theoremhood.." ThmResult config@@ -426,6 +442,14 @@                            _  -> error $ "User error: Multiple output values detected: " ++ show os                                        ++ "\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

@@ -46,7 +46,7 @@                                 execName <-               getEnv "SBV_Z3"          `C.catch` (\(_ :: C.SomeException) -> return (executable (solver cfg)))                                 execOpts <- (words `fmap` getEnv "SBV_Z3_OPTIONS") `C.catch` (\(_ :: C.SomeException) -> return (options (solver cfg)))                                 let cfg' = cfg { solver = (solver cfg) {executable = execName, options = addTimeOut (timeOut cfg) execOpts} }-                                    script = SMTScript { scriptBody = "(set-option :mbqi true)\n" ++ pgm, scriptModel = Just (cont skolemMap)}+                                    script = SMTScript {scriptBody = "(set-option :mbqi true)\n" ++ pgm, scriptModel = Just (cont skolemMap)}                                 standardSolver cfg' script cleanErrs (ProofError cfg) (interpretSolverOutput cfg (extractMap isSat qinps modelMap . zipWith match skolemMap))          }  where -- This is quite crude and failure prone.. But is necessary to get z3 working through Wine on Mac

@@ -11,9 +11,9 @@ in your .cabal/bin directory (or wherever you installed it.) It's highly recommended that you run this program to ensure everything is working correctly. In particular, you will first need to install-Yices, the default SMT solver used by sbv, from SRI. (You can get it-from http://yices.csl.sri.com/.) Please make sure that the "yices"-executable is in your path.+Z3, the default SMT solver used by sbv, from Microsoft. (You can get it+from http://research.microsoft.com/en-us/um/redmond/projects/z3/.)+Please make sure that the "z3" executable is in your path.  Once you have installed sbv, you can use it in your Haskell programs by simply importing the Data.SBV module.

@@ -1,7 +1,20 @@ Hackage: <http://hackage.haskell.org/package/sbv> GitHub:  <http://github.com/LeventErkok/sbv> -Latest Hackage released version: 1.0+Latest Hackage released version: 1.1++======================================================================+Version 1.1, 2012-02-14++ Library:+  * Rename bitValue to sbvTestBit+  * Add sbvPopCount+  * Add a custom implementation of 'popCount' for the Bits class+    instance of SBV (GHC >= 7.4.1 only)+  * Add 'sbvCheckSolverInstallation', which can be used to check+    that the given solver is installed and good to go.+  * Add 'generateSMTBenchmarks', simplifying the generation of+    SMTLib benchmarks for offline sharing.  ====================================================================== Version 1.0, 2012-02-13

@@ -2,4 +2,4 @@ module SBVUnitTestBuildTime (buildTime) where  buildTime :: String-buildTime = "Sun Feb 12 23:26:02 PST 2012"+buildTime = "Tue Feb 14 19:29:22 PST 2012"

@@ -31,4 +31,4 @@                 r <- do rh <- forall "rh"                         rl <- forall "rl"                         return (rh, rl)-                output $ bitValue p 0 &&& crcGood 4 p s r+                output $ sbvTestBit p 0 &&& crcGood 4 p s r

@@ -1,5 +1,5 @@ Name:          sbv-Version:       1.0+Version:       1.1 Category:      Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math, SMT Synopsis:      Symbolic bit vectors: Bit-precise verification and automatic C-code generation. Description:   Express properties about bit-precise Haskell programs and automatically prove