diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,7 +1,16 @@ * Hackage: * GitHub: -* 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 diff --git a/Data/SBV/BitVectors/Concrete.hs b/Data/SBV/BitVectors/Concrete.hs --- a/Data/SBV/BitVectors/Concrete.hs +++ b/Data/SBV/BitVectors/Concrete.hs @@ -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))) 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 @@ -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) 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 @@ -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" diff --git a/Data/SBV/BitVectors/Operations.hs b/Data/SBV/BitVectors/Operations.hs --- a/Data/SBV/BitVectors/Operations.hs +++ b/Data/SBV/BitVectors/Operations.hs @@ -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 diff --git a/Data/SBV/BitVectors/Symbolic.hs b/Data/SBV/BitVectors/Symbolic.hs --- a/Data/SBV/BitVectors/Symbolic.hs +++ b/Data/SBV/BitVectors/Symbolic.hs @@ -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) 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 @@ -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, "-") diff --git a/Data/SBV/Dynamic.hs b/Data/SBV/Dynamic.hs --- a/Data/SBV/Dynamic.hs +++ b/Data/SBV/Dynamic.hs @@ -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 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 @@ -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 diff --git a/Data/SBV/SMT/SMTLibNames.hs b/Data/SBV/SMT/SMTLibNames.hs --- a/Data/SBV/SMT/SMTLibNames.hs +++ b/Data/SBV/SMT/SMTLibNames.hs @@ -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" + ] 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 Dec 6 18:51:28 PST 2015" +buildTime = "Mon Dec 21 15:35:40 PST 2015" 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 @@ -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) 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 @@ -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 diff --git a/sbv.cabal b/sbv.cabal --- a/sbv.cabal +++ b/sbv.cabal @@ -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