sbv 5.6 → 5.7

raw patch · 14 files changed

+129/−74 lines, 14 files

Files

• CHANGES.md +10/−1
• Data/SBV/BitVectors/Concrete.hs +2/−2
• Data/SBV/BitVectors/Data.hs +1/−1
• Data/SBV/BitVectors/Model.hs +41/−19
• Data/SBV/BitVectors/Operations.hs +46/−21
• Data/SBV/BitVectors/Symbolic.hs +2/−2
• Data/SBV/Compilers/C.hs +6/−6
• Data/SBV/Dynamic.hs +1/−1
• Data/SBV/SMT/SMT.hs +7/−3
• Data/SBV/SMT/SMTLibNames.hs +9/−6
• SBVUnitTest/SBVUnitTestBuildTime.hs +1/−1
• SBVUnitTest/TestSuite/Basics/ArithNoSolver.hs +1/−5
• SBVUnitTest/TestSuite/Basics/ArithSolver.hs +1/−5
• sbv.cabal +1/−1

@@ -1,7 +1,16 @@ * Hackage: <http://hackage.haskell.org/package/sbv> * GitHub:  <http://leventerkok.github.com/sbv/> -* Latest Hackage released version: 5.6, 2015-12-06+* Latest Hackage released version: 5.7, 2015-12-21++### Version 5.7, 2015-12-21++  * Export HasKind(..) from the Dynamic interface. Thanks to Adam Foltzer for the patch.+  * More careful handling of SMT-Lib reserved names.+  * Update tested version of MathSAT to 5.3.9+  * Generalize sShiftLeft/sShiftRight/sRotateLeft/sRotateRight to work with signed+    shift/rotate amounts, where negative values revert the direction. Similar+    generalizations are also done for the dynamic variants.  ### Version 5.6, 2015-12-06   

@@ -159,14 +159,14 @@ showCW shk w               = liftCW show show show show snd w ++ kInfo       where kInfo | shk  = " :: " ++ shKind (kindOf w)                   | True = ""-            shKind k@(KUserSort {})       = show k+            shKind k@KUserSort {}         = show k             shKind k | ('S':sk) <- show k = sk             shKind k                      = show k  -- | 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 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))) mkConstCW KFloat          a = normCW $ CW KFloat     (CWFloat   (fromInteger (toInteger a)))

@@ -394,7 +394,7 @@ newtype SArray a b = SArray { unSArray :: SArr }  instance (HasKind a, HasKind b) => Show (SArray a b) where-  show (SArray{}) = "SArray<" ++ showType (undefined :: a) ++ ":" ++ showType (undefined :: b) ++ ">"+  show SArray{} = "SArray<" ++ showType (undefined :: a) ++ ":" ++ showType (undefined :: b) ++ ">"  instance SymArray SArray where   newArray_                                      = declNewSArray (\t -> "array_" ++ show t)

@@ -691,24 +691,32 @@  -- | Generalization of 'shiftL', when the shift-amount is symbolic. Since Haskell's -- 'shiftL' only takes an 'Int' as the shift amount, it cannot be used when we have--- a symbolic amount to shift with. The shift amount must be an unsigned quantity.+-- a symbolic amount to shift with. The first argument should be a bounded quantity. sShiftLeft :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a sShiftLeft x i-  | isSigned i = error "sShiftLeft: shift amount should be unsigned"-  | True       = select [x `shiftL` k | k <- [0 .. ghcBitSize x - 1]] z i+  | not (isBounded x)+  = error "SBV.sShiftRight: Shifted about should be a bounded quantity!"+  | True+  = ite (i .< 0)+        (select [x `shiftR` k | k <- [0 .. ghcBitSize x - 1]] z (-i))+        (select [x `shiftL` k | k <- [0 .. ghcBitSize x - 1]] z   i )   where z = genLiteral (kindOf x) (0::Integer)  -- | 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--- a symbolic amount to shift with. The shift amount must be an unsigned quantity.+-- a symbolic amount to shift with. The first argument should be a bounded quantity. -- -- NB. If the shiftee is signed, then this is an arithmetic shift; otherwise it's logical, -- following the usual Haskell convention. See 'sSignedShiftArithRight' for a variant -- that explicitly uses the msb as the sign bit, even for unsigned underlying types. sShiftRight :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a sShiftRight x i-  | isSigned i = error "sShiftRight: shift amount should be unsigned"-  | True       = select [x `shiftR` k | k <- [0 .. ghcBitSize x - 1]] z i+  | not (isBounded x)+  = error "SBV.sShiftRight: Shifted about should be a bounded quantity!"+  | True+  = ite (i .< 0)+        (select [x `shiftL` k | k <- [0 .. ghcBitSize x - 1]] z (-i))+        (select [x `shiftR` k | k <- [0 .. ghcBitSize x - 1]] z   i )   where z = genLiteral (kindOf x) (0::Integer)  -- | Arithmetic shift-right with a symbolic unsigned shift amount. This is equivalent@@ -726,29 +734,43 @@  -- | Generalization of 'rotateL', when the shift-amount is symbolic. Since Haskell's -- 'rotateL' only takes an 'Int' as the shift amount, it cannot be used when we have--- a symbolic amount to shift with. The shift amount must be an unsigned quantity.+-- a symbolic amount to shift with. The first argument should be a bounded quantity. sRotateLeft :: (SIntegral a, SIntegral b, SDivisible (SBV b)) => SBV a -> SBV b -> SBV a sRotateLeft x i-  | isSigned i             = error "sRotateLeft: rotation amount should be unsigned"-  | bit si <= toInteger sx = select [x `rotateL` k | k <- [0 .. bit si - 1]] z i         -- wrap-around not possible-  | True                   = select [x `rotateL` k | k <- [0 .. sx     - 1]] z (i `sRem` n)+  | not (isBounded x)+  = sShiftLeft x i+  | isBounded i && bit si <= toInteger sx    -- wrap-around not possible+  = ite (i .< 0)+        (select [x `rotateR` k | k <- [0 .. bit si - 1]] z (-i))+        (select [x `rotateL` k | k <- [0 .. bit si - 1]] z   i )+  | True+  = ite (i .< 0)+        (select [x `rotateR` k | k <- [0 .. sx     - 1]] z ((-i) `sRem` n))+        (select [x `rotateL` k | k <- [0 .. sx     - 1]] z (  i  `sRem` n))     where sx = ghcBitSize x           si = ghcBitSize i-          z = genLiteral (kindOf x) (0::Integer)-          n = genLiteral (kindOf i) (toInteger sx)+          z  = genLiteral (kindOf x) (0::Integer)+          n  = genLiteral (kindOf i) (toInteger sx)  -- | Generalization of 'rotateR', when the shift-amount is symbolic. Since Haskell's -- 'rotateR' only takes an 'Int' as the shift amount, it cannot be used when we have--- a symbolic amount to shift with. The shift amount must be an unsigned quantity.+-- a symbolic amount to shift with. The first argument should be a bounded quantity. sRotateRight :: (SIntegral a, SIntegral b, SDivisible (SBV b)) => SBV a -> SBV b -> SBV a sRotateRight x i-  | isSigned i             = error "sRotateRight: rotation amount should be unsigned"-  | bit si <= toInteger sx = select [x `rotateR` k | k <- [0 .. bit si - 1]] z i         -- wrap-around not possible-  | True                   = select [x `rotateR` k | k <- [0 .. sx     - 1]] z (i `sRem` n)+  | not (isBounded x)+  = sShiftRight x i+  | isBounded i && bit si <= toInteger sx   -- wrap-around not possible+  = ite (i .< 0)+        (select [x `rotateL` k | k <- [0 .. bit si - 1]] z (-i))+        (select [x `rotateR` k | k <- [0 .. bit si - 1]] z   i)+  | True+  = ite (i .< 0)+        (select [x `rotateL` k | k <- [0 .. sx     - 1]] z ((-i) `sRem` n))+        (select [x `rotateR` k | k <- [0 .. sx     - 1]] z (  i  `sRem` n))     where sx = ghcBitSize x           si = ghcBitSize i-          z = genLiteral (kindOf x) (0::Integer)-          n = genLiteral (kindOf i) (toInteger sx)+          z  = genLiteral (kindOf x) (0::Integer)+          n  = genLiteral (kindOf i) (toInteger sx)  -- | Full adder. Returns the carry-out from the addition. --@@ -1606,7 +1628,7 @@            pc   = getPathCondition st        check <- liftIO $ internalSATCheck cfg (pc &&& cond) st "isSatisfiableInCurrentPath: Checking satisfiability"        let res = case check of-                   SatResult (Satisfiable{})   -> True+                   SatResult Satisfiable{}     -> True                    SatResult (Unsatisfiable _) -> False                    _                           -> error $ "isSatisfiableInCurrentPath: Unexpected external result: " ++ show check        res `seq` liftIO $ msg $ "isSatisfiableInCurrentPath: Conclusion: " ++ if res then "Satisfiable" else "Unsatisfiable"

@@ -530,48 +530,73 @@   | True            = svFalse  -- | Generalization of 'svShl', where the shift-amount is symbolic.--- The shift amount must be an unsigned quantity.+-- The first argument should be a bounded quantity. svShiftLeft :: SVal -> SVal -> SVal svShiftLeft x i-  | hasSign i = error "sShiftLeft: shift amount should be unsigned"-  | True      = svSelect [svShl x k | k <- [0 .. intSizeOf x - 1]] z i-  where z = svInteger (kindOf x) 0+  | not (isBounded x)+  = error "SBV.svShiftLeft: Shifted about should be a bounded quantity!"+  | True+  = svIte (svLessThan i zi)+          (svSelect [svShr x k | k <- [0 .. intSizeOf x - 1]] z (svUNeg i))+          (svSelect [svShl x k | k <- [0 .. intSizeOf x - 1]] z         i)+  where z  = svInteger (kindOf x) 0+        zi = svInteger (kindOf i) 0  -- | Generalization of 'svShr', where the shift-amount is symbolic.--- The shift amount must be an unsigned quantity.+-- The first argument should be a bounded quantity. -- -- NB. If the shiftee is signed, then this is an arithmetic shift; -- otherwise it's logical. svShiftRight :: SVal -> SVal -> SVal svShiftRight x i-  | hasSign i = error "sShiftRight: shift amount should be unsigned"-  | True      = svSelect [svShr x k | k <- [0 .. intSizeOf x - 1]] z i-  where z = svInteger (kindOf x) 0+  | not (isBounded x)+  = error "SBV.svShiftLeft: Shifted about should be a bounded quantity!"+  | True+  = svIte (svLessThan i zi)+          (svSelect [svShl x k | k <- [0 .. intSizeOf x - 1]] z (svUNeg i))+          (svSelect [svShr x k | k <- [0 .. intSizeOf x - 1]] z         i)+  where z  = svInteger (kindOf x) 0+        zi = svInteger (kindOf i) 0  -- | Generalization of 'svRol', where the rotation amount is symbolic.--- The rotation amount must be an unsigned quantity.+-- The first argument should be a bounded quantity. svRotateLeft :: SVal -> SVal -> SVal svRotateLeft x i-  | hasSign i              = error "sRotateLeft: rotation amount should be unsigned"-  | bit si <= toInteger sx = svSelect [x `svRol` k | k <- [0 .. bit si - 1]] z i         -- wrap-around not possible-  | True                   = svSelect [x `svRol` k | k <- [0 .. sx     - 1]] z (i `svRem` n)+  | not (isBounded x)+  = svShiftLeft x i+  | isBounded i && bit si <= toInteger sx            -- wrap-around not possible+  = svIte (svLessThan i zi)+          (svSelect [x `svRor` k | k <- [0 .. bit si - 1]] z (svUNeg i))+          (svSelect [x `svRol` k | k <- [0 .. bit si - 1]] z         i)+  | True+  = svIte (svLessThan i zi)+          (svSelect [x `svRor` k | k <- [0 .. sx     - 1]] z (svUNeg i `svRem` n))+          (svSelect [x `svRol` k | k <- [0 .. sx     - 1]] z (       i  `svRem` n))     where sx = intSizeOf x           si = intSizeOf i-          z = svInteger (kindOf x) 0-          n = svInteger (kindOf i) (toInteger sx)+          z  = svInteger (kindOf x) 0+          zi = svInteger (kindOf i) 0+          n  = svInteger (kindOf i) (toInteger sx)  -- | Generalization of 'svRor', where the rotation amount is symbolic.--- The rotation amount must be an unsigned quantity.+-- The first argument should be a bounded quantity. svRotateRight :: SVal -> SVal -> SVal svRotateRight x i-  | hasSign i              = error "sRotateRight: rotation amount should be unsigned"-  | bit si <= toInteger sx = svSelect [x `svRor` k | k <- [0 .. bit si - 1]] z i         -- wrap-around not possible-  | True                   = svSelect [x `svRor` k | k <- [0 .. sx     - 1]] z (i `svRem` n)+  | not (isBounded x)+  = svShiftRight x i+  | isBounded i && bit si <= toInteger sx                   -- wrap-around not possible+  = svIte (svLessThan i zi)+          (svSelect [x `svRol` k | k <- [0 .. bit si - 1]] z (svUNeg i))+          (svSelect [x `svRor` k | k <- [0 .. bit si - 1]] z         i)+  | True+  = svIte (svLessThan i zi)+          (svSelect [x `svRol` k | k <- [0 .. sx     - 1]] z (svUNeg i `svRem` n))+          (svSelect [x `svRor` k | k <- [0 .. sx     - 1]] z (       i  `svRem` n))     where sx = intSizeOf x           si = intSizeOf i-          z = svInteger (kindOf x) 0-          n = svInteger (kindOf i) (toInteger sx)-+          z  = svInteger (kindOf x) 0+          zi = svInteger (kindOf i) 0+          n  = svInteger (kindOf i) (toInteger sx)  -------------------------------------------------------------------------------- -- Utility functions

@@ -55,7 +55,7 @@ import Control.Monad        (when, unless) import Control.Monad.Reader (MonadReader, ReaderT, ask, runReaderT) import Control.Monad.Trans  (MonadIO, liftIO)-import Data.Char            (isAlpha, isAlphaNum)+import Data.Char            (isAlpha, isAlphaNum, toLower) import Data.IORef           (IORef, newIORef, modifyIORef, readIORef, writeIORef) import Data.List            (intercalate, sortBy) import Data.Maybe           (isJust, fromJust, fromMaybe)@@ -530,7 +530,7 @@ -- | Register a new kind with the system, used for uninterpreted sorts registerKind :: State -> Kind -> IO () registerKind st k-  | KUserSort sortName _ <- k, sortName `elem` smtLibReservedNames+  | KUserSort sortName _ <- k, map toLower sortName `elem` smtLibReservedNames   = error $ "SBV: " ++ show sortName ++ " is a reserved sort; please use a different name."   | True   = modifyIORef (rUsedKinds st) (Set.insert k)

@@ -447,10 +447,10 @@                          $$ vcat (map text ls)                          $$ text ""        typeWidth = getMax 0 $ [len (kindOf s) | (s, _) <- assignments] ++ [len (kindOf s) | (_, (s, _)) <- ins]-                where len (KReal{})           = 5-                      len (KFloat{})          = 6 -- SFloat-                      len (KDouble{})         = 7 -- SDouble-                      len (KUnbounded{})      = 8+                where len KReal{}             = 5+                      len KFloat{}            = 6 -- SFloat+                      len KDouble{}           = 7 -- SDouble+                      len KUnbounded{}        = 8                       len KBool               = 5 -- SBool                       len (KBounded False n)  = 5 + length (show n) -- SWordN                       len (KBounded True  n)  = 4 + length (show n) -- SIntN@@ -617,8 +617,8 @@   = typ <+> var <> semi <+> rhs   | True   = lhs <+> text "=" <+> rhs-  where doNotAssign (IEEEFP (FP_Reinterpret{})) = True   -- generates a memcpy instead; no simple assignment-        doNotAssign _                           = False  -- generates simple assignment+  where doNotAssign (IEEEFP FP_Reinterpret{}) = True   -- generates a memcpy instead; no simple assignment+        doNotAssign _                         = False  -- generates simple assignment         rhs = p op (map (showSW cfg consts) opArgs)         rtc = cgRTC cfg         cBinOps = [ (Plus, "+"),  (Times, "*"), (Minus, "-")

@@ -18,7 +18,7 @@   -- ** Symbolic types   -- *** Abstract symbolic value type     SVal-  , Kind(..), CW(..), CWVal(..), cwToBool+  , HasKind(..), Kind(..), CW(..), CWVal(..), cwToBool   -- *** Arrays of symbolic values   , SArr   , readSArr, resetSArr, writeSArr, mergeSArr, newSArr, eqSArr

@@ -305,8 +305,8 @@   getModel (ProofError _ s)  = error $ unlines $ "Backend solver complains: " : s   getModel (TimeOut _)       = Left "Timeout"   getModel (Satisfiable _ m) = Right (False, parseModelOut m)-  modelExists (Satisfiable{}) = True-  modelExists (Unknown{})     = False -- don't risk it+  modelExists Satisfiable{}   = True+  modelExists Unknown{}       = False -- don't risk it   modelExists _               = False   getModelDictionary (Unsatisfiable _) = M.empty   getModelDictionary (Unknown _ m)     = M.fromList (modelAssocs m)@@ -351,7 +351,7 @@   where ignore (s, _) = "__internal_sbv_" `isPrefixOf` s         shM (s, v)    = let vs = shCW cfg v in ((length s, s), (vlength vs, vs))         display svs   = map line svs-           where line ((_, s), (_, v)) = "  " ++ right (nameWidth - length s) s ++ " = " ++ left (valWidth - length (takeWhile (not . isSpace) v)) v+           where line ((_, s), (_, v)) = "  " ++ right (nameWidth - length s) s ++ " = " ++ left (valWidth - lTrimRight (valPart v)) v                  nameWidth             = maximum $ 0 : [l | ((l, _), _) <- svs]                  valWidth              = maximum $ 0 : [l | (_, (l, _)) <- svs]         right p s = s ++ replicate p ' '@@ -359,6 +359,10 @@         vlength s = case dropWhile (/= ':') (reverse s) of                       (':':':':r) -> length (dropWhile isSpace r)                       _           -> length s -- conservative+        valPart ""          = ""+        valPart (':':':':_) = ""+        valPart (x:xs)      = x : valPart xs+        lTrimRight = length . dropWhile isSpace . reverse  -- | Show a constant value, in the user-specified base shCW :: SMTConfig -> CW -> String

@@ -11,12 +11,15 @@  module Data.SBV.SMT.SMTLibNames where +import Data.Char (toLower)+ -- | Names reserved by SMTLib. This list is current as of Dec 6 2015; but of course -- there's no guarantee it'll stay that way. smtLibReservedNames :: [String]-smtLibReservedNames = [ "Int", "Real", "List", "Array", "Bool", "FP", "FloatingPoint", "fp"-                      , "!", "_", "as", "BINARY", "DECIMAL", "exists", "HEXADECIMAL", "forall", "let", "NUMERAL", "par", "STRING"-                      , "assert", "check-sat", "check-sat-assuming", "declare-const", "declare-fun", "declare-sort", "define-fun", "define-fun-rec"-                      , "define-sort", "echo", "exit", "get-assertions", "get-assignment", "get-info", "get-model", "get-option", "get-proof", "get-unsat-assumptions"-                      , "get-unsat-core", "get-value", "pop", "push", "reset", "reset-assertions", "set-info", "set-logic", "set-option"-                      ]+smtLibReservedNames = map (map toLower)+                        [ "Int", "Real", "List", "Array", "Bool", "FP", "FloatingPoint", "fp", "String"+                        , "!", "_", "as", "BINARY", "DECIMAL", "exists", "HEXADECIMAL", "forall", "let", "NUMERAL", "par", "STRING", "CHAR"+                        , "assert", "check-sat", "check-sat-assuming", "declare-const", "declare-fun", "declare-sort", "define-fun", "define-fun-rec"+                        , "define-sort", "echo", "exit", "get-assertions", "get-assignment", "get-info", "get-model", "get-option", "get-proof", "get-unsat-assumptions"+                        , "get-unsat-core", "get-value", "pop", "push", "reset", "reset-assertions", "set-info", "set-logic", "set-option"+                        ]

@@ -2,4 +2,4 @@ module SBVUnitTestBuildTime (buildTime) where  buildTime :: String-buildTime = "Sun Dec  6 18:51:28 PST 2015"+buildTime = "Mon Dec 21 15:35:40 PST 2015"

@@ -385,11 +385,7 @@         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 xs sxs (n, ps, p) = zipWith (chk n) (map (\x -> (x, p x)) xs) (map ps sxs)-          where chk nm (x, v) sv-                  -- Work around GHC bug, see issue #138-                  -- Remove the following line when fixed.-                  | nm == "fpIsPositiveZero" && isNegativeZero x = (nm, (show x, True))-                  | True                                         = (nm, (show x, Just v == unliteral sv))+          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)

@@ -251,11 +251,7 @@          m f = f sRNE -        preds =   [(pn,       show x,         mkThmP        ps       x   (pc x))     | (pn, ps, pc) <- predicates, x <- vs-                                                                                     -- Work around GHC bug, see issue #138-                                                                                     -- Remove the following line when fixed.-                                                                                     , not (pn == "fpIsPositiveZero" && isNegativeZero x)-                                                                                     ]+        preds =   [(pn, show x, mkThmP ps x (pc x)) | (pn, ps, pc) <- predicates, x <- vs]         tst2 (nm, x, y, t) = origin ++ ".arithmetic-" ++ nm ++ "." ++ x ++ "_" ++ y  ~: assert t         tst1 (nm, x,    t) = origin ++ ".arithmetic-" ++ nm ++ "." ++ x              ~: assert t 

@@ -1,5 +1,5 @@ Name:          sbv-Version:       5.6+Version:       5.7 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