diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -3,6 +3,23 @@ * Latest Hackage released version: 3.5 +### Version 4.0, 2015-01-22 + +This release mainly contains contributions from Brian Huffman, allowing +end-users to define new symbolic types, such as Word4, that SBV does not +natively support. When GHC gets type-level literals, we shall most likely +incorporate arbitrary bit-sized vectors and ints using this mechanism, +but in the interim, this release provides a means for the users to introduce +individual instances. + + * Modifications to support arbitrary bit-sized vectors; + These changes have been contributed by Brian Huffman + of Galois.. Thanks Brian. + * A new example "Data/SBV/Examples/Misc/Word4.hs" showing + how users can add new symbolic types. + * Support for rotate-left/rotate-right with variable + rotation amounts. (From Brian Huffman.) + ### Version 3.5, 2015-01-15 This release is mainly adding support for enumerated types in Haskell being diff --git a/Data/SBV.hs b/Data/SBV.hs --- a/Data/SBV.hs +++ b/Data/SBV.hs @@ -141,7 +141,7 @@ , STree, readSTree, writeSTree, mkSTree -- ** Operations on symbolic values -- *** Word level - , sbvTestBit, sbvPopCount, sbvShiftLeft, sbvShiftRight, sbvSignedShiftArithRight, setBitTo, oneIf, lsb, msb + , sbvTestBit, sbvPopCount, sbvShiftLeft, sbvShiftRight, sbvRotateLeft, sbvRotateRight, sbvSignedShiftArithRight, setBitTo, oneIf, lsb, msb -- *** Predicates , allEqual, allDifferent, inRange, sElem -- *** Addition and Multiplication with high-bits 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 @@ -29,7 +29,7 @@ , CW(..), CWVal(..), AlgReal(..), cwSameType, cwIsBit, cwToBool , mkConstCW ,liftCW2, mapCW, mapCW2 , SW(..), trueSW, falseSW, trueCW, falseCW, normCW - , SBV(..), NodeId(..), mkSymSBV + , SBV(..), NodeId(..), mkSymSBV, mkSymSBVWithRandom , ArrayContext(..), ArrayInfo, SymArray(..), SFunArray(..), mkSFunArray, SArray(..), arrayUIKind , sbvToSW, sbvToSymSW, forceSWArg , SBVExpr(..), newExpr @@ -707,7 +707,7 @@ a /= b = error $ "Comparing symbolic bit-vectors; Use (./=) instead. Received: " ++ show (a, b) instance HasKind a => HasKind (SBV a) where - kindOf _ = kindOf (undefined :: a) + kindOf (SBV k _) = k -- | Increment the variable counter incCtr :: State -> IO Int @@ -815,10 +815,15 @@ newtype Symbolic a = Symbolic (ReaderT State IO a) deriving (Applicative, Functor, Monad, MonadIO, MonadReader State) --- | Create a symbolic value, based on the quantifier we have. If an explicit quantifier is given, we just use that. --- If not, then we pick existential for SAT calls and universal for everything else. +-- | Create a symbolic variable. Equivalent to 'mkSymSBVWithRandom randomIO'. mkSymSBV :: forall a. (Random a, SymWord a) => Maybe Quantifier -> Kind -> Maybe String -> Symbolic (SBV a) -mkSymSBV mbQ k mbNm = do +mkSymSBV = mkSymSBVWithRandom randomIO + +-- | Create a symbolic value, based on the quantifier we have. If an explicit quantifier is given, we just use that. +-- If not, then we pick existential for SAT calls and universal for everything else. The @rand@ argument is used +-- in generating random values for this variable when used for 'quickCheck' purposes. +mkSymSBVWithRandom :: forall a. SymWord a => IO (SBV a) -> Maybe Quantifier -> Kind -> Maybe String -> Symbolic (SBV a) +mkSymSBVWithRandom rand mbQ k mbNm = do st <- ask let q = case (mbQ, runMode st) of (Just x, _) -> x -- user given, just take it @@ -828,9 +833,9 @@ (Nothing, CodeGen) -> ALL -- code generation, pick universal case runMode st of Concrete _ | q == EX -> case mbNm of - Nothing -> error $ "Cannot quick-check in the presence of existential variables, type: " ++ showType (undefined :: SBV a) - Just nm -> error $ "Cannot quick-check in the presence of existential variable " ++ nm ++ " :: " ++ showType (undefined :: SBV a) - Concrete _ -> do v@(SBV _ (Left cw)) <- liftIO randomIO + Nothing -> error $ "Cannot quick-check in the presence of existential variables, type: " ++ showType (undefined :: a) + Just nm -> error $ "Cannot quick-check in the presence of existential variable " ++ nm ++ " :: " ++ showType (undefined :: a) + Concrete _ -> do v@(SBV _ (Left cw)) <- liftIO rand liftIO $ modifyIORef (rCInfo st) ((maybe "_" id mbNm, cw):) return v _ -> do (sw, internalName) <- liftIO $ newSW st k 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 @@ -22,13 +22,16 @@ module Data.SBV.BitVectors.Model ( Mergeable(..), EqSymbolic(..), OrdSymbolic(..), SDivisible(..), Uninterpreted(..), SIntegral - , ite, iteLazy, sBranch, sAssert, sAssertCont, sbvTestBit, sbvPopCount, setBitTo, sbvShiftLeft, sbvShiftRight, sbvSignedShiftArithRight + , ite, iteLazy, sBranch, sAssert, sAssertCont, sbvTestBit, sbvPopCount, setBitTo + , sbvShiftLeft, sbvShiftRight, sbvRotateLeft, sbvRotateRight, sbvSignedShiftArithRight , allEqual, allDifferent, inRange, sElem, oneIf, blastBE, blastLE, fullAdder, fullMultiplier , lsb, msb, genVar, genVar_, forall, forall_, exists, exists_ , constrain, pConstrain, sBool, sBools, sWord8, sWord8s, sWord16, sWord16s, sWord32 , sWord32s, sWord64, sWord64s, sInt8, sInt8s, sInt16, sInt16s, sInt32, sInt32s, sInt64 , sInt64s, sInteger, sIntegers, sReal, sReals, toSReal, sFloat, sFloats, sDouble, sDoubles, slet , fusedMA + , liftQRem, liftDMod, symbolicMergeWithKind + , genLiteral, genFromCW, genMkSymVar ) where @@ -613,28 +616,48 @@ oneIf :: (Num a, SymWord a) => SBool -> SBV a oneIf t = ite t 1 0 +-- | Predicate for optimizing word operations like (+) and (*). +isConcreteZero :: SBV a -> Bool +isConcreteZero (SBV _ (Left (CW _ (CWInteger n)))) = n == 0 +isConcreteZero (SBV KReal (Left (CW KReal (CWAlgReal v)))) = isExactRational v && v == 0 +isConcreteZero _ = False + +-- | Predicate for optimizing word operations like (+) and (*). +isConcreteOne :: SBV a -> Bool +isConcreteOne (SBV _ (Left (CW _ (CWInteger 1)))) = True +isConcreteOne (SBV KReal (Left (CW KReal (CWAlgReal v)))) = isExactRational v && v == 1 +isConcreteOne _ = False + +-- | Predicate for optimizing bitwise operations. +isConcreteOnes :: SBV a -> Bool +isConcreteOnes (SBV _ (Left (CW (KBounded b w) (CWInteger n)))) = n == if b then -1 else bit w - 1 +isConcreteOnes (SBV _ (Left (CW KUnbounded (CWInteger n)))) = n == -1 +isConcreteOnes _ = False + -- Num instance for symbolic words. instance (Ord a, Num a, SymWord a) => Num (SBV a) where fromInteger = literal . fromIntegral x + y - | x `isConcretely` (== 0) = y - | y `isConcretely` (== 0) = x - | True = liftSym2 (mkSymOp Plus) rationalCheck (+) (+) (+) (+) x y + | isConcreteZero x = y + | isConcreteZero y = x + | True = liftSym2 (mkSymOp Plus) rationalCheck (+) (+) (+) (+) x y x * y - | x `isConcretely` (== 0) = 0 - | y `isConcretely` (== 0) = 0 - | x `isConcretely` (== 1) = y - | y `isConcretely` (== 1) = x - | True = liftSym2 (mkSymOp Times) rationalCheck (*) (*) (*) (*) x y + | isConcreteZero x = x + | isConcreteZero y = y + | isConcreteOne x = y + | isConcreteOne y = x + | True = liftSym2 (mkSymOp Times) rationalCheck (*) (*) (*) (*) x y x - y - | y `isConcretely` (== 0) = x - | True = liftSym2 (mkSymOp Minus) rationalCheck (-) (-) (-) (-) x y + | isConcreteZero y = x + | True = liftSym2 (mkSymOp Minus) rationalCheck (-) (-) (-) (-) x y -- Abs is problematic for floating point, due to -0; case, so we carefully shuttle it down -- to the solver to avoid the can of worms. (Alternative would be to do an if-then-else here.) abs = liftSym1 (mkSymOp1 Abs) abs abs abs abs signum a - | hasSign a = ite (a .< 0) (-1) (ite (a .== 0) 0 1) - | True = oneIf (a ./= 0) + | hasSign a = ite (a .< z) (-i) (ite (a .== z) z i) + | True = ite (a ./= z) i z + where z = genLiteral (kindOf a) (0::Integer) + i = genLiteral (kindOf a) (1::Integer) -- negate is tricky because on double/float -0 is different than 0; so we -- just cannot rely on its default definition; which would be 0-0, which is not -0! negate = liftSym1 (mkSymOp1 UNeg) (\x -> -x) (\x -> -x) (\x -> -x) (\x -> -x) @@ -738,28 +761,31 @@ -- -1 has all bits set to True for both signed and unsigned values instance (Num a, Bits a, SymWord a) => Bits (SBV a) where x .&. y - | x `isConcretely` (== 0) = 0 - | x `isConcretely` (== -1) = y - | y `isConcretely` (== 0) = 0 - | y `isConcretely` (== -1) = x - | True = liftSym2 (mkSymOp And) (const (const True)) (noReal ".&.") (.&.) (noFloat ".&.") (noDouble ".&.") x y + | isConcreteZero x = x + | isConcreteOnes x = y + | isConcreteZero y = y + | isConcreteOnes y = x + | True = liftSym2 (mkSymOp And) (const (const True)) (noReal ".&.") (.&.) (noFloat ".&.") (noDouble ".&.") x y x .|. y - | x `isConcretely` (== 0) = y - | x `isConcretely` (== -1) = -1 - | y `isConcretely` (== 0) = x - | y `isConcretely` (== -1) = -1 - | True = liftSym2 (mkSymOp Or) (const (const True)) (noReal ".|.") (.|.) (noFloat ".|.") (noDouble ".|.") x y + | isConcreteZero x = y + | isConcreteOnes x = x + | isConcreteZero y = x + | isConcreteOnes y = y + | True = liftSym2 (mkSymOp Or) (const (const True)) (noReal ".|.") (.|.) (noFloat ".|.") (noDouble ".|.") x y x `xor` y - | x `isConcretely` (== 0) = y - | y `isConcretely` (== 0) = x - | True = liftSym2 (mkSymOp XOr) (const (const True)) (noReal "xor") xor (noFloat "xor") (noDouble "xor") x y + | isConcreteZero x = y + | isConcreteZero y = x + | True = liftSym2 (mkSymOp XOr) (const (const True)) (noReal "xor") xor (noFloat "xor") (noDouble "xor") x y complement = liftSym1 (mkSymOp1 Not) (noRealUnary "complement") complement (noFloatUnary "complement") (noDoubleUnary "complement") - bitSize _ = intSizeOf (undefined :: a) + bitSize x = intSizeOf x #if __GLASGOW_HASKELL__ >= 708 - bitSizeMaybe _ = Just $ intSizeOf (undefined :: a) + bitSizeMaybe x = Just $ intSizeOf x #endif - isSigned _ = hasSign (undefined :: a) + isSigned x = hasSign x bit i = 1 `shiftL` i + setBit x i = x .|. genLiteral (kindOf x) (bit i :: Integer) + clearBit x i = x .&. genLiteral (kindOf x) (complement (bit i) :: Integer) + complementBit x i = x `xor` genLiteral (kindOf x) (bit i :: Integer) shiftL x y | y < 0 = shiftR x (-y) | y == 0 = x @@ -780,14 +806,12 @@ | 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 + | SBV _ (Left (CW _ (CWInteger n))) <- x = testBit n i | True = error $ "SBV.testBit: Called on symbolic value: " ++ show x ++ ". Use sbvTestBit instead." -- 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." + | SBV _ (Left (CW (KBounded _ w) (CWInteger n))) <- x = popCount (n .&. (bit w - 1)) + | True = error $ "SBV.popCount: Called on symbolic value: " ++ show x ++ ". Use sbvPopCount instead." -- Since the underlying representation is just Integers, rotations has to be careful on the bit-size rot :: Bool -> Int -> Int -> Integer -> Integer @@ -801,7 +825,8 @@ -- | 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. sbvTestBit :: (Num a, Bits a, SymWord a) => SBV a -> Int -> SBool -sbvTestBit x i = (x .&. bit i) ./= 0 +sbvTestBit x i = (x .&. genLiteral k (bit i :: Integer)) ./= genLiteral k (0::Integer) + where k = kindOf x -- | 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 @@ -834,7 +859,8 @@ sbvShiftLeft :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a sbvShiftLeft x i | isSigned i = error "sbvShiftLeft: shift amount should be unsigned" - | True = select [x `shiftL` k | k <- [0 .. ghcBitSize x - 1]] 0 i + | True = 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 @@ -846,7 +872,8 @@ sbvShiftRight :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a sbvShiftRight x i | isSigned i = error "sbvShiftRight: shift amount should be unsigned" - | True = select [x `shiftR` k | k <- [0 .. ghcBitSize x - 1]] 0 i + | True = 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 -- to 'sbvShiftRight' when the argument is signed. However, if the argument is unsigned, @@ -861,6 +888,32 @@ (complement (sbvShiftRight (complement x) i)) (sbvShiftRight x i) +-- | 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. +sbvRotateLeft :: (SIntegral a, SIntegral b, SDivisible (SBV b)) => SBV a -> SBV b -> SBV a +sbvRotateLeft x i + | isSigned i = error "sbvRotateLeft: 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) + where sx = ghcBitSize x + si = ghcBitSize i + 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. +sbvRotateRight :: (SIntegral a, SIntegral b, SDivisible (SBV b)) => SBV a -> SBV b -> SBV a +sbvRotateRight x i + | isSigned i = error "sbvRotateRight: 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) + where sx = ghcBitSize x + si = ghcBitSize i + z = genLiteral (kindOf x) (0::Integer) + n = genLiteral (kindOf i) (toInteger sx) + -- | Full adder. Returns the carry-out from the addition. -- -- N.B. Only works for unsigned types. Signed arguments will be rejected. @@ -1089,42 +1142,49 @@ sQuotRem = liftQRem sDivMod = liftDMod +-- | 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 x y - | x `isConcretely` (== 0) - = (0, 0) - | y `isConcretely` (== 1) - = (x, 0) + | isConcreteZero x + = (x, x) + | isConcreteOne y + = (x, z) {------------------------------- - N.B. The seemingly innocuous variant when y == -1 only holds if the type is signed; - and also is problematic around the minBound.. So, we refrain from that optimization - | y `isConcretely` (== -1) - = (-x, 0) + | isConcreteOnes y + = (-x, z) --------------------------------} | True - = ite (y .== 0) (0, x) (qr x y) + = ite (y .== z) (z, x) (qr x y) where qr (SBV sgnsz (Left a)) (SBV _ (Left b)) = let (q, r) = sQuotRem a b in (SBV sgnsz (Left q), SBV sgnsz (Left r)) qr a@(SBV sgnsz _) b = (SBV sgnsz (Right (cache (mk Quot))), SBV sgnsz (Right (cache (mk Rem)))) where mk o st = do sw1 <- sbvToSW st a sw2 <- sbvToSW st b mkSymOp o st sgnsz sw1 sw2 + z = genLiteral (kindOf x) (0::Integer) --- Conversion from quotRem (truncate to 0) to divMod (truncate towards negative infinity) +-- | Lift 'QMod' 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 x y - | x `isConcretely` (== 0) - = (0, 0) - | y `isConcretely` (== 1) - = (x, 0) + | isConcreteZero x + = (x, x) + | isConcreteOne y + = (x, z) {------------------------------- - N.B. The seemingly innocuous variant when y == -1 only holds if the type is signed; - and also is problematic around the minBound.. So, we refrain from that optimization - | y `isConcretely` (== -1) - = (-x, 0) + | isConcreteOnes y + = (-x, z) --------------------------------} | True - = ite (y .== 0) (0, x) $ ite (signum r .== negate (signum y)) (q-1, r+y) qr - where qr@(q, r) = x `sQuotRem` y + = ite (y .== z) (z, x) $ ite (signum r .== negate (signum y)) (q-i, r+y) qr + where qr@(q, r) = x `sQuotRem` y + z = genLiteral (kindOf x) (0::Integer) + i = genLiteral (kindOf x) (1::Integer) -- SInteger instance for quotRem/divMod are tricky! -- SMT-Lib only has Euclidean operations, but Haskell @@ -1255,82 +1315,90 @@ Just (r@(SatResult (Satisfiable cfg _))) -> cont cfg $ Just $ getModelDictionary r _ -> return trueSW --- SBV -instance SymWord a => Mergeable (SBV a) where - symbolicMerge force t a b - | Just r <- unliteral t - = if r then a else b - | force, Just av <- unliteral a, Just bv <- unliteral b, rationalSBVCheck a b, av == bv - = a - | True - = SBV k $ Right $ cache c - where k = kindOf a - c st = do swt <- sbvToSW st t - case () of - () | swt == trueSW -> sbvToSW st a -- these two cases should never be needed as we expect symbolicMerge to be - () | swt == falseSW -> sbvToSW st b -- called with symbolic tests, but just in case.. - () -> do {- It is tempting to record the choice of the test expression here as we branch down to the 'then' and 'else' branches. That is, - when we evaluate 'a', we can make use of the fact that the test expression is True, and similarly we can use the fact that it - is False when b is evaluated. In certain cases this can cut down on symbolic simulation significantly, for instance if - repetitive decisions are made in a recursive loop. Unfortunately, the implementation of this idea is quite tricky, due to - our sharing based implementation. As the 'then' branch is evaluated, we will create many expressions that are likely going - to be "reused" when the 'else' branch is executed. But, it would be *dead wrong* to share those values, as they were "cached" - under the incorrect assumptions. To wit, consider the following: +-- | Merge two symbolic values, at kind @k@, possibly @force@'ing the branches to make +-- sure they do not evaluate to the same result. This should only be used for internal purposes; +-- as default definitions provided should suffice in many cases. (i.e., End users should +-- only need to define 'symbolicMerge' when needed; which should be rare to start with.) +symbolicMergeWithKind :: SymWord a => Kind -> Bool -> SBool -> SBV a -> SBV a -> SBV a +symbolicMergeWithKind k force t a b + | Just r <- unliteral t + = if r then a else b + | force, Just av <- unliteral a, Just bv <- unliteral b, rationalSBVCheck a b, av == bv + = a + | True + = SBV k $ Right $ cache c + where c st = do swt <- sbvToSW st t + case () of + () | swt == trueSW -> sbvToSW st a -- these two cases should never be needed as we expect symbolicMerge to be + () | swt == falseSW -> sbvToSW st b -- called with symbolic tests, but just in case.. + () -> do {- It is tempting to record the choice of the test expression here as we branch down to the 'then' and 'else' branches. That is, + when we evaluate 'a', we can make use of the fact that the test expression is True, and similarly we can use the fact that it + is False when b is evaluated. In certain cases this can cut down on symbolic simulation significantly, for instance if + repetitive decisions are made in a recursive loop. Unfortunately, the implementation of this idea is quite tricky, due to + our sharing based implementation. As the 'then' branch is evaluated, we will create many expressions that are likely going + to be "reused" when the 'else' branch is executed. But, it would be *dead wrong* to share those values, as they were "cached" + under the incorrect assumptions. To wit, consider the following: - foo x y = ite (y .== 0) k (k+1) - where k = ite (y .== 0) x (x+1) + foo x y = ite (y .== 0) k (k+1) + where k = ite (y .== 0) x (x+1) - When we reduce the 'then' branch of the first ite, we'd record the assumption that y is 0. But while reducing the 'then' branch, we'd - like to share 'k', which would evaluate (correctly) to 'x' under the given assumption. When we backtrack and evaluate the 'else' - branch of the first ite, we'd see 'k' is needed again, and we'd look it up from our sharing map to find (incorrectly) that its value - is 'x', which was stored there under the assumption that y was 0, which no longer holds. Clearly, this is unsound. + When we reduce the 'then' branch of the first ite, we'd record the assumption that y is 0. But while reducing the 'then' branch, we'd + like to share 'k', which would evaluate (correctly) to 'x' under the given assumption. When we backtrack and evaluate the 'else' + branch of the first ite, we'd see 'k' is needed again, and we'd look it up from our sharing map to find (incorrectly) that its value + is 'x', which was stored there under the assumption that y was 0, which no longer holds. Clearly, this is unsound. - A sound implementation would have to precisely track which assumptions were active at the time expressions get shared. That is, - in the above example, we should record that the value of 'k' was cached under the assumption that 'y' is 0. While sound, this - approach unfortunately leads to significant loss of valid sharing when the value itself had nothing to do with the assumption itself. - To wit, consider: + A sound implementation would have to precisely track which assumptions were active at the time expressions get shared. That is, + in the above example, we should record that the value of 'k' was cached under the assumption that 'y' is 0. While sound, this + approach unfortunately leads to significant loss of valid sharing when the value itself had nothing to do with the assumption itself. + To wit, consider: - foo x y = ite (y .== 0) k (k+1) - where k = x+5 + foo x y = ite (y .== 0) k (k+1) + where k = x+5 - If we tracked the assumptions, we would recompute 'k' twice, since the branch assumptions would differ. Clearly, there is no need to - re-compute 'k' in this case since its value is independent of y. Note that the whole SBV performance story is based on agressive sharing, - and losing that would have other significant ramifications. + If we tracked the assumptions, we would recompute 'k' twice, since the branch assumptions would differ. Clearly, there is no need to + re-compute 'k' in this case since its value is independent of y. Note that the whole SBV performance story is based on agressive sharing, + and losing that would have other significant ramifications. - The "proper" solution would be to track, with each shared computation, precisely which assumptions it actually *depends* on, rather - than blindly recording all the assumptions present at that time. SBV's symbolic simulation engine clearly has all the info needed to do this - properly, but the implementation is not straightforward at all. For each subexpression, we would need to chase down its dependencies - transitively, which can require a lot of scanning of the generated program causing major slow-down; thus potentially defeating the - whole purpose of sharing in the first place. + The "proper" solution would be to track, with each shared computation, precisely which assumptions it actually *depends* on, rather + than blindly recording all the assumptions present at that time. SBV's symbolic simulation engine clearly has all the info needed to do this + properly, but the implementation is not straightforward at all. For each subexpression, we would need to chase down its dependencies + transitively, which can require a lot of scanning of the generated program causing major slow-down; thus potentially defeating the + whole purpose of sharing in the first place. - Design choice: Keep it simple, and simply do not track the assumption at all. This will maximize sharing, at the cost of evaluating - unreachable branches. I think the simplicity is more important at this point than efficiency. + Design choice: Keep it simple, and simply do not track the assumption at all. This will maximize sharing, at the cost of evaluating + unreachable branches. I think the simplicity is more important at this point than efficiency. - Also note that the user can avoid most such issues by properly combining if-then-else's with common conditions together. That is, the - first program above should be written like this: + Also note that the user can avoid most such issues by properly combining if-then-else's with common conditions together. That is, the + first program above should be written like this: - foo x y = ite (y .== 0) x (x+2) + foo x y = ite (y .== 0) x (x+2) - In general, the following transformations should be done whenever possible: + In general, the following transformations should be done whenever possible: - ite e1 (ite e1 e2 e3) e4 --> ite e1 e2 e4 - ite e1 e2 (ite e1 e3 e4) --> ite e1 e2 e4 + ite e1 (ite e1 e2 e3) e4 --> ite e1 e2 e4 + ite e1 e2 (ite e1 e3 e4) --> ite e1 e2 e4 - This is in accordance with the general rule-of-thumb stating conditionals should be avoided as much as possible. However, we might prefer - the following: + This is in accordance with the general rule-of-thumb stating conditionals should be avoided as much as possible. However, we might prefer + the following: - ite e1 (f e2 e4) (f e3 e5) --> f (ite e1 e2 e3) (ite e1 e4 e5) + ite e1 (f e2 e4) (f e3 e5) --> f (ite e1 e2 e3) (ite e1 e4 e5) - especially if this expression happens to be inside 'f's body itself (i.e., when f is recursive), since it reduces the number of - recursive calls. Clearly, programming with symbolic simulation in mind is another kind of beast alltogether. - -} - swa <- sbvToSW (st `extendPathCondition` (&&& t)) a -- evaluate 'then' branch - swb <- sbvToSW (st `extendPathCondition` (&&& bnot t)) b -- evaluate 'else' branch - case () of -- merge: - () | swa == swb -> return swa - () | swa == trueSW && swb == falseSW -> return swt - () | swa == falseSW && swb == trueSW -> newExpr st k (SBVApp Not [swt]) - () -> newExpr st k (SBVApp Ite [swt, swa, swb]) + especially if this expression happens to be inside 'f's body itself (i.e., when f is recursive), since it reduces the number of + recursive calls. Clearly, programming with symbolic simulation in mind is another kind of beast alltogether. + -} + swa <- sbvToSW (st `extendPathCondition` (&&& t)) a -- evaluate 'then' branch + swb <- sbvToSW (st `extendPathCondition` (&&& bnot t)) b -- evaluate 'else' branch + case () of -- merge: + () | swa == swb -> return swa + () | swa == trueSW && swb == falseSW -> return swt + () | swa == falseSW && swb == trueSW -> newExpr st k (SBVApp Not [swt]) + () -> newExpr st k (SBVApp Ite [swt, swa, swb]) + +instance SymWord a => Mergeable (SBV a) where + symbolicMerge force t x y + -- Carefully use the kindOf instance to avoid strictness issues. + | force = symbolicMergeWithKind (kindOf x) True t x y + | True = symbolicMergeWithKind (kindOf (undefined :: a)) False t x y -- Custom version of select that translates to SMT-Lib tables at the base type of words select xs err ind | SBV _ (Left c) <- ind = case cwVal c of @@ -1803,9 +1871,9 @@ -- However, there might be times where being explicit on the sharing can help, especially in experimental code. The 'slet' combinator -- ensures that its first argument is computed once and passed on to its continuation, explicitly indicating the intent of sharing. Most -- use cases of the SBV library should simply use Haskell's @let@ construct for this purpose. -slet :: (HasKind a, HasKind b) => SBV a -> (SBV a -> SBV b) -> SBV b +slet :: forall a b. (HasKind a, HasKind b) => SBV a -> (SBV a -> SBV b) -> SBV b slet x f = SBV k $ Right $ cache r - where k = kindOf (undefined `asTypeOf` f x) + where k = kindOf (undefined :: b) r st = do xsw <- sbvToSW st x let xsbv = SBV (kindOf x) (Right (cache (const (return xsw)))) res = f xsbv diff --git a/Data/SBV/BitVectors/Splittable.hs b/Data/SBV/BitVectors/Splittable.hs --- a/Data/SBV/BitVectors/Splittable.hs +++ b/Data/SBV/BitVectors/Splittable.hs @@ -15,7 +15,7 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE BangPatterns #-} -module Data.SBV.BitVectors.Splittable (Splittable(..), FromBits(..)) where +module Data.SBV.BitVectors.Splittable (Splittable(..), FromBits(..), checkAndConvert) where import Data.Bits (Bits(..)) import Data.Word (Word8, Word16, Word32, Word64) diff --git a/Data/SBV/Examples/Misc/Word4.hs b/Data/SBV/Examples/Misc/Word4.hs new file mode 100644 --- /dev/null +++ b/Data/SBV/Examples/Misc/Word4.hs @@ -0,0 +1,154 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Data.SBV.Examples.Misc.Enumerate +-- Copyright : (c) Brian Huffman +-- License : BSD3 +-- Maintainer : erkokl@gmail.com +-- Stability : experimental +-- +-- Demonstrates how new sizes of word/int types can be defined and +-- used with SBV. +----------------------------------------------------------------------------- + +{-# LANGUAGE CPP #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} + +module Data.SBV.Examples.Misc.Word4 where + +import GHC.Enum (boundedEnumFrom, boundedEnumFromThen, toEnumError, succError, predError) + +import Data.Bits +import Data.Generics (Data, Typeable) +import System.Random (Random(..)) + +import Data.SBV +import Data.SBV.Internals + +-- | Word4 as a newtype. Invariant: @Word4 x@ should satisfy @x < 16@. +newtype Word4 = Word4 Word8 + deriving (Eq, Ord, Data, Typeable) + +-- | Smart constructor; simplifies conversion from Word8 +word4 :: Word8 -> Word4 +word4 x = Word4 (x .&. 0x0f) + +-- | Show instance +instance Show Word4 where + show (Word4 x) = show x + +-- | Read instance. We read as an 8-bit word, and coerce +instance Read Word4 where + readsPrec p s = [ (word4 x, s') | (x, s') <- readsPrec p s ] + +-- | Bounded instance; from 0 to 255 +instance Bounded Word4 where + minBound = Word4 0x00 + maxBound = Word4 0x0f + +-- | Enum instance, trivial definitions. +instance Enum Word4 where + succ (Word4 x) = if x < 0x0f then Word4 (succ x) else succError "Word4" + pred (Word4 x) = if x > 0x00 then Word4 (pred x) else predError "Word4" + toEnum i | 0x00 <= i && i <= 0x0f = Word4 (toEnum i) + | otherwise = toEnumError "Word4" i (Word4 0x00, Word4 0x0f) + fromEnum (Word4 x) = fromEnum x + -- Comprehensions + enumFrom = boundedEnumFrom + enumFromThen = boundedEnumFromThen + enumFromTo (Word4 x) (Word4 y) = map Word4 (enumFromTo x y) + enumFromThenTo (Word4 x) (Word4 y) (Word4 z) = map Word4 (enumFromThenTo x y z) + +-- | Num instance, merely lifts underlying 8-bit operation and casts back +instance Num Word4 where + Word4 x + Word4 y = word4 (x + y) + Word4 x * Word4 y = word4 (x * y) + Word4 x - Word4 y = word4 (x - y) + negate (Word4 x) = word4 (negate x) + abs (Word4 x) = Word4 x + signum (Word4 x) = Word4 (if x == 0 then 0 else 1) + fromInteger n = word4 (fromInteger n) + +-- | Real instance simply uses the Word8 instance +instance Real Word4 where + toRational (Word4 x) = toRational x + +-- | Integral instance, again using Word8 instance and casting. NB. we do +-- not need to use the smart constructor here as neither the quotient nor +-- the remainder can overflow a Word4. +instance Integral Word4 where + quotRem (Word4 x) (Word4 y) = (Word4 q, Word4 r) + where (q, r) = quotRem x y + toInteger (Word4 x) = toInteger x + +-- | Bits instance +instance Bits Word4 where + Word4 x .&. Word4 y = Word4 (x .&. y) + Word4 x .|. Word4 y = Word4 (x .|. y) + Word4 x `xor` Word4 y = Word4 (x `xor` y) + complement (Word4 x) = Word4 (x `xor` 0x0f) + Word4 x `shift` i = word4 (shift x i) + Word4 x `shiftL` i = word4 (shiftL x i) + Word4 x `shiftR` i = Word4 (shiftR x i) + Word4 x `rotate` i = word4 (x `shiftL` k .|. x `shiftR` (4-k)) + where k = i .&. 3 + bitSize _ = 4 +#if __GLASGOW_HASKELL__ >= 708 + bitSizeMaybe _ = Just 4 +#endif + isSigned _ = False + testBit (Word4 x) = testBit x + bit i = word4 (bit i) + popCount (Word4 x) = popCount x + +-- | Random instance, used in quick-check +instance Random Word4 where + randomR (Word4 lo, Word4 hi) gen = (Word4 x, gen') + where (x, gen') = randomR (lo, hi) gen + random gen = (Word4 x, gen') + where (x, gen') = randomR (0x00, 0x0f) gen + +-- | SWord4 type synonym +type SWord4 = SBV Word4 + +-- | SymWord instance, allowing this type to be used in proofs/sat etc. +instance SymWord Word4 where + mkSymWord = genMkSymVar (KBounded False 4) + literal = genLiteral (KBounded False 4) + fromCW = genFromCW + mbMaxBound = Just maxBound + mbMinBound = Just minBound + +-- | HasKind instance; simply returning the underlying kind for the type +instance HasKind Word4 where + kindOf _ = KBounded False 4 + +-- | SatModel instance, merely uses the generic parsing method. +instance SatModel Word4 where + parseCWs = genParse (KBounded False 4) + +-- | SDvisible instance, using 0-extension +instance SDivisible Word4 where + sQuotRem x 0 = (0, x) + sQuotRem x y = x `quotRem` y + sDivMod x 0 = (0, x) + sDivMod x y = x `divMod` y + +-- | SDvisible instance, using default methods +instance SDivisible SWord4 where + sQuotRem = liftQRem + sDivMod = liftDMod + +-- | SIntegral instance, using default methods +instance SIntegral Word4 + +-- | Conversion from bits +instance FromBits SWord4 where + fromBitsLE = checkAndConvert 4 + +-- | Joining/splitting to/from Word8 +instance Splittable Word8 Word4 where + split x = (Word4 (x `shiftR` 4), word4 x) + Word4 x # Word4 y = (x `shiftL` 4) .|. y + extend (Word4 x) = x diff --git a/Data/SBV/Internals.hs b/Data/SBV/Internals.hs --- a/Data/SBV/Internals.hs +++ b/Data/SBV/Internals.hs @@ -15,12 +15,19 @@ -- * Running symbolic programs /manually/ Result, SBVRunMode(..), runSymbolic, runSymbolic' -- * Other internal structures useful for low-level programming - , SBV(..), slet, CW(..), Kind(..), CWVal(..), AlgReal(..), mkConstCW, genVar, genVar_ + , SBV(..), slet, CW(..), Kind(..), CWVal(..), AlgReal(..), Quantifier(..), mkConstCW, genVar, genVar_ + , liftQRem, liftDMod, symbolicMergeWithKind + , cache, sbvToSW, newExpr, normCW, SBVExpr(..), Op(..), mkSymSBVWithRandom + -- * Operations useful for instantiating SBV type classes + , genLiteral, genFromCW, genMkSymVar, checkAndConvert, genParse -- * Compilation to C , compileToC', compileToCLib', CgPgmBundle(..), CgPgmKind(..) ) where -import Data.SBV.BitVectors.Data (Result, SBVRunMode(..), runSymbolic, runSymbolic', SBV(..), CW(..), Kind(..), CWVal(..), AlgReal(..), mkConstCW) -import Data.SBV.BitVectors.Model (genVar, genVar_, slet) -import Data.SBV.Compilers.C (compileToC', compileToCLib') -import Data.SBV.Compilers.CodeGen (CgPgmBundle(..), CgPgmKind(..)) +import Data.SBV.BitVectors.Data (Result, SBVRunMode(..), runSymbolic, runSymbolic', SBV(..), CW(..), Kind(..), CWVal(..), AlgReal(..), Quantifier(..), mkConstCW) +import Data.SBV.BitVectors.Data (cache, sbvToSW, newExpr, normCW, SBVExpr(..), Op(..), mkSymSBVWithRandom) +import Data.SBV.BitVectors.Model (genVar, genVar_, slet, liftQRem, liftDMod, symbolicMergeWithKind, genLiteral, genFromCW, genMkSymVar) +import Data.SBV.BitVectors.Splittable (checkAndConvert) +import Data.SBV.Compilers.C (compileToC', compileToCLib') +import Data.SBV.Compilers.CodeGen (CgPgmBundle(..), CgPgmKind(..)) +import Data.SBV.SMT.SMT (genParse) 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 @@ -189,6 +189,11 @@ parseCWs (CW KDouble (CWDouble i) : r) = Just (i, r) parseCWs _ = Nothing +-- | 'CW' as extracted from a model; trivial definition +instance SatModel CW where + parseCWs (cw : r) = Just (cw, r) + parseCWs [] = Nothing + -- | A list of values as extracted from a model. When reading a list, we -- go as long as we can (maximal-munch). Note that this never fails, as -- we can always return the empty list! 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 = "Thu Jan 15 19:08:18 PST 2015" +buildTime = "Thu Jan 22 19:53:39 PST 2015" diff --git a/sbv.cabal b/sbv.cabal --- a/sbv.cabal +++ b/sbv.cabal @@ -1,5 +1,5 @@ Name: sbv -Version: 3.5 +Version: 4.0 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 @@ -74,6 +74,7 @@ , Data.SBV.Examples.Misc.Floating , Data.SBV.Examples.Misc.SBranch , Data.SBV.Examples.Misc.ModelExtract + , Data.SBV.Examples.Misc.Word4 , Data.SBV.Examples.Polynomials.Polynomials , Data.SBV.Examples.Puzzles.Coins , Data.SBV.Examples.Puzzles.Counts