sbv 3.5 → 4.0
raw patch · 10 files changed
+391/−134 lines, 10 files
Files
- CHANGES.md +17/−0
- Data/SBV.hs +1/−1
- Data/SBV/BitVectors/Data.hs +13/−8
- Data/SBV/BitVectors/Model.hs +185/−117
- Data/SBV/BitVectors/Splittable.hs +1/−1
- Data/SBV/Examples/Misc/Word4.hs +154/−0
- Data/SBV/Internals.hs +12/−5
- Data/SBV/SMT/SMT.hs +5/−0
- SBVUnitTest/SBVUnitTestBuildTime.hs +1/−1
- sbv.cabal +2/−1
CHANGES.md view
@@ -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
Data/SBV.hs view
@@ -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
Data/SBV/BitVectors/Data.hs view
@@ -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
Data/SBV/BitVectors/Model.hs view
@@ -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
Data/SBV/BitVectors/Splittable.hs view
@@ -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)
+ Data/SBV/Examples/Misc/Word4.hs view
@@ -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
Data/SBV/Internals.hs view
@@ -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)
Data/SBV/SMT/SMT.hs view
@@ -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!
SBVUnitTest/SBVUnitTestBuildTime.hs view
@@ -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"
sbv.cabal view
@@ -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