sbv 10.11 → 10.12
raw patch · 15 files changed
+202/−41 lines, 15 filesdep ~asyncdep ~base
Dependency ranges changed: async, base
Files
- CHANGES.md +13/−0
- Data/SBV/Control/Utils.hs +2/−2
- Data/SBV/Core/Floating.hs +5/−3
- Data/SBV/Tools/Overflow.hs +57/−0
- README.md +2/−1
- SBVTestSuite/GoldFiles/allSat8.gold +1/−1
- SBVTestSuite/GoldFiles/nested1.gold +1/−1
- SBVTestSuite/GoldFiles/nested2.gold +1/−1
- SBVTestSuite/GoldFiles/nested3.gold +1/−1
- SBVTestSuite/GoldFiles/nested4.gold +1/−1
- SBVTestSuite/GoldFiles/noOpt1.gold +1/−1
- SBVTestSuite/GoldFiles/noOpt2.gold +1/−1
- SBVTestSuite/GoldFiles/set_uninterp1.gold +9/−9
- SBVTestSuite/TestSuite/Overflows/Arithmetic.hs +51/−1
- sbv.cabal +56/−18
CHANGES.md view
@@ -1,6 +1,19 @@ * Hackage: <http://hackage.haskell.org/package/sbv> * GitHub: <http://github.com/LeventErkok/sbv> +### Version 10.12, 2024-08-11++ * Fix a few custom-floating-point format conversion bugs. Thanks to Sirui Lu for the patch.++ * Add a few OVERLAPPABLE pragms to generic Queriable instances to make them easily overridable by+ user programs. Thanks to Marco Zocca for reporting.++ * Add signedMulOverflow, which checks whether multiplication of two signed-bitvectors can overflow.+ SBV already had a method (bvMulO) that served this purpose, translating to the corresponding predicate+ in SMTLib. Unfortunately not all solvers support this predicate efficiently. In particular, as of Aug 2024,+ bitwuzla has a performant checker for this overflow, but z3 does not. In case you cannot use bitwuzla for+ some reason, you might want to use the new signedMulOverflow funtion for better performance.+ ### Version 10.11, 2024-07-26 * Add Documentation.SBV.Examples.Puzzles.Tower module, solving the visible towers puzzle.
Data/SBV/Control/Utils.hs view
@@ -219,14 +219,14 @@ return r -- | Generic 'Queriable' instance for 'SymVal' values-instance (MonadIO m, SymVal a) => Queriable m (SBV a) where+instance {-# OVERLAPPABLE #-} (MonadIO m, SymVal a) => Queriable m (SBV a) where type QueryResult (SBV a) = a create = freshVar_ project = getValue embed = return . literal -- | Generic 'Queriable' instance for things that are 'Fresh' and look like containers:-instance (MonadIO m, SymVal a, Foldable t, Traversable t, Fresh m (t (SBV a))) => Queriable m (t (SBV a)) where+instance {-# OVERLAPPABLE #-} (MonadIO m, SymVal a, Foldable t, Traversable t, Fresh m (t (SBV a))) => Queriable m (t (SBV a)) where type QueryResult (t (SBV a)) = t a create = fresh project = mapM getValue
Data/SBV/Core/Floating.hs view
@@ -12,6 +12,7 @@ {-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE InstanceSigs #-} {-# LANGUAGE Rank2Types #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-}@@ -297,7 +298,7 @@ instance IEEEFloatConvertible AlgReal where toSFloat = genericToFloat (onlyWhenRNE convertWhenExactRational) toSDouble = genericToFloat (onlyWhenRNE convertWhenExactRational)- toSFloatingPoint = genericToFloat (const convertWhenExactRational)+ toSFloatingPoint = genericToFloat (onlyWhenRNE convertWhenExactRational) -- Arbitrary floats can handle all rounding modes in concrete mode instance ValidFloat eb sb => IEEEFloatConvertible (FloatingPoint eb sb) where@@ -333,13 +334,14 @@ where ei = intOfProxy (Proxy @eb) si = intOfProxy (Proxy @sb) + toSFloatingPoint :: forall eb1 sb1. (ValidFloat eb sb, ValidFloat eb1 sb1) => SRoundingMode -> SBV (FloatingPoint eb sb) -> SFloatingPoint eb1 sb1 toSFloatingPoint rm i | Just (FloatingPoint (FP _ _ v)) <- unliteral i, Just brm <- rmToRM rm = literal $ FloatingPoint $ FP ei si $ fst (bfRoundFloat (mkBFOpts ei si brm) v) | True = genericToFloat (\_ _ -> Nothing) rm i- where ei = intOfProxy (Proxy @eb)- si = intOfProxy (Proxy @sb)+ where ei = intOfProxy (Proxy @eb1)+ si = intOfProxy (Proxy @sb1) -- From and To are the same when the source is an arbitrary float! fromSFloatingPoint = toSFloatingPoint
Data/SBV/Tools/Overflow.hs view
@@ -10,12 +10,14 @@ -- Based on: <http://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/z3prefix.pdf> ----------------------------------------------------------------------------- +{-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE ImplicitParams #-} {-# LANGUAGE Rank2Types #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -Wall -Werror #-}@@ -25,6 +27,9 @@ -- * Arithmetic overflows ArithOverflow(..), CheckedArithmetic(..) + -- * Fast-checking of signed-multiplication overflow+ , signedMulOverflow+ -- * Cast overflows , sFromIntegralO, sFromIntegralChecked @@ -291,6 +296,58 @@ (r, (u, o)) = sFromIntegralO x +-- | signedMulOverflow: Checking if a signed bitvector multiplication can overflow. In general you should simply use 'bvMulO' for checking+-- signed multiplication overflow for bit-vectors. This is a function supported by SMTLib. Unfortunately, individual implementations have+-- different performance characteristics. For instance, bitwuzla has a fairly performant implementation of this, but z3 does not. (At least+-- not as of August 2024.) In cases where you can't use bitwuzla, you can use this implementation which has better performance.+signedMulOverflow :: forall n. ( KnownNat n, BVIsNonZero n+ , KnownNat (n+1), BVIsNonZero (n+1)+ , KnownNat (2+Log2 n), BVIsNonZero (2+Log2 n))+ => SInt n -> SInt n -> SBool+signedMulOverflow x y = sNot zeroOut .&& overflow+ where zeroOut = x .== 0 .|| y .== 0++ prod :: SInt (n+1)+ prod = sFromIntegral x * sFromIntegral y++ nv :: Int+ nv = fromIntegral $ natVal (Proxy @n)++ prodN, prodNm1 :: SBool+ prodN = prod `sTestBit` nv+ prodNm1 = prod `sTestBit` (nv-1)++ overflow = nonSignBitPos x + nonSignBitPos y .> literal (fromIntegral (nv - 2))+ .|| prodN .<+> prodNm1++ -- Find the position of the first non-sign bit. i.e., the first bit that differs from the msb.+ -- Position is 0 indexed. Note that if there's no differing bit, then you also get back 0.+ -- This is essentially an approximation of the logarithm of the magnitude of the number.+ --+ -- The result is at most N-2 for an N-bit word. Later we add two of these, so the maximum+ -- value we need to represent is 2N-4. This will require 1 + lg(2N-4) = 2 + log(N-1) bits.+ -- To suppor the case N=0, we return a (2 + log N) bit word.+ --+ -- Example for 3 bits:+ --+ -- 000 -> 0 (no differing bit from 0; so we get 0)+ -- 001 -> 0+ -- 010 -> 1+ -- 011 -> 1+ -- 100 -> 1+ -- 101 -> 1+ -- 110 -> 0+ -- 111 -> 0 (no differing bit from 1; so we get 0)+ nonSignBitPos :: ( KnownNat n, BVIsNonZero n+ , KnownNat (2+Log2 n), BVIsNonZero (2+Log2 n))+ => SInt n -> SWord (2+Log2 n)+ nonSignBitPos w = walk 0 rest+ where (sign, rest) = case blastBE w of+ [] -> error $ "Impossible happened, blastBE returned no bits for " ++ show w+ (b:bs) -> (b, zip [0..] (reverse bs))++ walk sofar [] = sofar+ walk sofar ((i, b):bs) = walk (ite (b ./= sign) i sofar) bs -- Helpers l2 :: (SVal -> SVal -> SBool) -> SBV a -> SBV a -> SBool
README.md view
@@ -176,6 +176,7 @@ Daniel Wagner, Sean Weaver, Nis Wegmann,-and Jared Ziegler.+Jared Ziegler,+and Marco Zocca. Thanks!
SBVTestSuite/GoldFiles/allSat8.gold view
@@ -63,4 +63,4 @@ *** NB. If this is a use case you'd like SBV to support, please get in touch! CallStack (from HasCallStack):- error, called at ./Data/SBV/Control/Utils.hs:1660:57 in sbv-10.11-inplace:Data.SBV.Control.Utils+ error, called at ./Data/SBV/Control/Utils.hs:1660:57 in sbv-10.12-inplace:Data.SBV.Control.Utils
SBVTestSuite/GoldFiles/nested1.gold view
@@ -11,4 +11,4 @@ *** See https://github.com/LeventErkok/sbv/issues/71 for several examples. CallStack (from HasCallStack):- error, called at ./Data/SBV/Core/Symbolic.hs:1938:48 in sbv-10.11-inplace:Data.SBV.Core.Symbolic+ error, called at ./Data/SBV/Core/Symbolic.hs:1938:48 in sbv-10.12-inplace:Data.SBV.Core.Symbolic
SBVTestSuite/GoldFiles/nested2.gold view
@@ -11,4 +11,4 @@ *** See https://github.com/LeventErkok/sbv/issues/71 for several examples. CallStack (from HasCallStack):- error, called at ./Data/SBV/Core/Symbolic.hs:1938:48 in sbv-10.11-inplace:Data.SBV.Core.Symbolic+ error, called at ./Data/SBV/Core/Symbolic.hs:1938:48 in sbv-10.12-inplace:Data.SBV.Core.Symbolic
SBVTestSuite/GoldFiles/nested3.gold view
@@ -37,4 +37,4 @@ *** See https://github.com/LeventErkok/sbv/issues/71 for several examples. CallStack (from HasCallStack):- error, called at ./Data/SBV/Core/Symbolic.hs:1938:48 in sbv-10.11-inplace:Data.SBV.Core.Symbolic+ error, called at ./Data/SBV/Core/Symbolic.hs:1938:48 in sbv-10.12-inplace:Data.SBV.Core.Symbolic
SBVTestSuite/GoldFiles/nested4.gold view
@@ -11,4 +11,4 @@ *** See https://github.com/LeventErkok/sbv/issues/71 for several examples. CallStack (from HasCallStack):- error, called at ./Data/SBV/Core/Symbolic.hs:1938:48 in sbv-10.11-inplace:Data.SBV.Core.Symbolic+ error, called at ./Data/SBV/Core/Symbolic.hs:1938:48 in sbv-10.12-inplace:Data.SBV.Core.Symbolic
SBVTestSuite/GoldFiles/noOpt1.gold view
@@ -31,4 +31,4 @@ *** Use "sat" for plain satisfaction CallStack (from HasCallStack):- error, called at ./Data/SBV/Provers/Prover.hs:261:27 in sbv-10.11-inplace:Data.SBV.Provers.Prover+ error, called at ./Data/SBV/Provers/Prover.hs:261:27 in sbv-10.12-inplace:Data.SBV.Provers.Prover
SBVTestSuite/GoldFiles/noOpt2.gold view
@@ -33,4 +33,4 @@ *** Use "optimize"/"optimizeWith" to calculate optimal satisfaction! CallStack (from HasCallStack):- error, called at ./Data/SBV/Provers/Prover.hs:608:33 in sbv-10.11-inplace:Data.SBV.Provers.Prover+ error, called at ./Data/SBV/Provers/Prover.hs:608:33 in sbv-10.12-inplace:Data.SBV.Provers.Prover
SBVTestSuite/GoldFiles/set_uninterp1.gold view
@@ -74,9 +74,9 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0))-[RECV] ((s0 (store ((as const (Array E Bool)) false) C true)))+[RECV] ((s0 (store (store ((as const (Array E Bool)) true) B false) A false))) [GOOD] (push 1)-[GOOD] (define-fun s13 () (Array E Bool) (store ((as const (Array E Bool)) false) C true))+[GOOD] (define-fun s13 () (Array E Bool) (store (store ((as const (Array E Bool)) true) B false) A false)) [GOOD] (define-fun s14 () Bool (= s0 s13)) [GOOD] (define-fun s15 () Bool (not s14)) [GOOD] (assert s15)@@ -84,9 +84,9 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0))-[RECV] ((s0 (store (store ((as const (Array E Bool)) false) B true) A true)))+[RECV] ((s0 (store ((as const (Array E Bool)) true) C false))) [GOOD] (push 1)-[GOOD] (define-fun s16 () (Array E Bool) (store (store ((as const (Array E Bool)) false) B true) A true))+[GOOD] (define-fun s16 () (Array E Bool) (store ((as const (Array E Bool)) true) C false)) [GOOD] (define-fun s17 () Bool (= s0 s16)) [GOOD] (define-fun s18 () Bool (not s17)) [GOOD] (assert s18)@@ -94,9 +94,9 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0))-[RECV] ((s0 (store (store ((as const (Array E Bool)) false) C true) A true)))+[RECV] ((s0 (store ((as const (Array E Bool)) true) B false))) [GOOD] (push 1)-[GOOD] (define-fun s19 () (Array E Bool) (store (store ((as const (Array E Bool)) false) C true) A true))+[GOOD] (define-fun s19 () (Array E Bool) (store ((as const (Array E Bool)) true) B false)) [GOOD] (define-fun s20 () Bool (= s0 s19)) [GOOD] (define-fun s21 () Bool (not s20)) [GOOD] (assert s21)@@ -128,11 +128,11 @@ Solution #1: s0 = U :: {E} Solution #2:- s0 = {A,C} :: {E}+ s0 = U - {B} :: {E} Solution #3:- s0 = {A,B} :: {E}+ s0 = U - {C} :: {E} Solution #4:- s0 = {C} :: {E}+ s0 = U - {A,B} :: {E} Solution #5: s0 = U - {A} :: {E} Solution #6:
SBVTestSuite/TestSuite/Overflows/Arithmetic.hs view
@@ -9,7 +9,11 @@ -- Test suite for overflow checking ----------------------------------------------------------------------------- +{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE Rank2Types #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-} {-# LANGUAGE ScopedTypeVariables #-} {-# OPTIONS_GHC -Wall -Werror #-}@@ -22,6 +26,9 @@ import Data.SBV.Tools.Overflow +import Data.Proxy+import GHC.TypeLits+ import Utils.SBVTestFramework -- Test suite@@ -47,7 +54,7 @@ , testCase "i64" $ assertIsThm $ overflow svMinus (bvSubO :: SInt64 -> SInt64 -> SBool) ] - -- Multiplication checks are expensive; so only do at a few instances+ -- Multiplication checks are expensive for z3; so only do at a few instances with z3 , testGroup "mul-ov" [ testCase "w8" $ assertIsThm $ overflow svTimes (bvMulO :: SWord8 -> SWord8 -> SBool) , testCase "w16" $ assertIsThm $ overflow svTimes (bvMulO :: SWord16 -> SWord16 -> SBool) -- , testCase "w32" $ assertIsThm $ overflow svTimes (bvMulO :: SWord32 -> SWord32 -> SBool)@@ -58,6 +65,30 @@ -- , testCase "i64" $ assertIsThm $ overflow svTimes (bvMulO :: SInt64 -> SInt64 -> SBool) ] + -- Another group of multiplication overflow tests for signed-multiplication, using bitwuzla+ , testGroup "mul-special"+ [ testCase "smov1_int" $ assert $ smulCheck (Proxy @1) True+ , testCase "smov1_txt" $ assert $ smulCheck (Proxy @1) False+ , testCase "smov2_int" $ assert $ smulCheck (Proxy @2) True+ , testCase "smov2_txt" $ assert $ smulCheck (Proxy @2) False+ , testCase "smov3_int" $ assert $ smulCheck (Proxy @3) True+ , testCase "smov3_txt" $ assert $ smulCheck (Proxy @3) False+ , testCase "smov4_int" $ assert $ smulCheck (Proxy @4) True+ , testCase "smov4_txt" $ assert $ smulCheck (Proxy @4) False+ , testCase "smov5_int" $ assert $ smulCheck (Proxy @5) True+ , testCase "smov5_txt" $ assert $ smulCheck (Proxy @5) False+ , testCase "smov6_int" $ assert $ smulCheck (Proxy @6) True+ , testCase "smov6_txt" $ assert $ smulCheck (Proxy @6) False+ , testCase "smov7_int" $ assert $ smulCheck (Proxy @7) True+ , testCase "smov7_txt" $ assert $ smulCheck (Proxy @7) False+ , testCase "smov8_int" $ assert $ smulCheck (Proxy @8) True+ , testCase "smov8_txt" $ assert $ smulCheck (Proxy @8) False+ -- After this, text-book checks take long; so we just check against internal+ , testCase "smov24_int" $ assert $ smulCheck (Proxy @24) True+ , testCase "smov32_int" $ assert $ smulCheck (Proxy @32) True+ , testCase "smov64_int" $ assert $ smulCheck (Proxy @64) True+ ]+ , testGroup "div-ov" [ testCase "w8" $ assertIsThm $ never svDivide (bvDivO :: SWord8 -> SWord8 -> SBool) , testCase "w16" $ assertIsThm $ never svDivide (bvDivO :: SWord16 -> SWord16 -> SBool) , testCase "w32" $ assertIsThm $ never svDivide (bvDivO :: SWord32 -> SWord32 -> SBool)@@ -143,5 +174,24 @@ return $ overflowHappens `exactlyWhen` ( (extResult `svGreaterThan` toLarge (maxBound :: SBV a)) `svOr` (extResult `svLessThan` toLarge (minBound :: SBV a)))++-- Custom checker for signedMulOverflow+smulCheck :: forall proxy n. ( KnownNat n, BVIsNonZero n+ , KnownNat (n+1), BVIsNonZero (n+1)+ , KnownNat (n+n), BVIsNonZero (n+n)+ , KnownNat (2+Log2 n), BVIsNonZero (2+Log2 n)+ ) => proxy n -> Bool -> IO Bool+smulCheck _ builtin = check (if builtin then bvMulO else textbook)+ where check f = isTheoremWith bitwuzla $ do+ x <- sInt "x"+ y <- sInt "y"+ pure $ f x y .== (signedMulOverflow :: SInt n -> SInt n -> SBool) x y++ textbook x y = prod2N ./= sFromIntegral prodN+ where prod2N :: SInt (n+n)+ prod2N = sFromIntegral x * sFromIntegral y++ prodN :: SInt n+ prodN = x * y {- HLint ignore module "Reduce duplication" -}
sbv.cabal view
@@ -1,7 +1,7 @@ Cabal-Version: 2.2 Name : sbv-Version : 10.11+Version : 10.12 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@@ -81,22 +81,22 @@ import : common-settings default-language: Haskell2010 build-depends : QuickCheck- , containers , array+ , async >= 2.2.5+ , containers , deepseq- , template-haskell- , pretty- , random- , mtl- , transformers- , async- , filepath- , text , directory- , time+ , filepath , libBF >= 0.6.8+ , mtl+ , pretty , process+ , random , syb+ , template-haskell+ , text+ , time+ , transformers , uniplate Exposed-modules : Data.SBV , Data.SBV.Control@@ -271,8 +271,19 @@ default-language : Haskell2010 type : exitcode-stdio-1.0 ghc-options : -with-rtsopts=-K64m- build-depends : filepath, sbv, directory, random, mtl, containers, deepseq- , bytestring, tasty, tasty-golden, tasty-hunit, tasty-quickcheck, QuickCheck+ build-depends : QuickCheck+ , bytestring+ , containers+ , deepseq+ , directory+ , filepath+ , mtl+ , random+ , sbv+ , tasty+ , tasty-golden+ , tasty-hunit+ , tasty-quickcheck hs-source-dirs : SBVTestSuite main-is : SBVTest.hs other-modules : Utils.SBVTestFramework@@ -397,8 +408,18 @@ Test-Suite SBVDocTest import : common-settings default-language: Haskell2010- build-depends : base, sbv, process, QuickCheck, filepath, mtl, bytestring, directory- , tasty, tasty-quickcheck, tasty-golden, tasty-hunit, deepseq+ build-depends : QuickCheck+ , bytestring+ , deepseq+ , directory+ , filepath+ , mtl+ , process+ , sbv+ , tasty+ , tasty-golden+ , tasty-hunit+ , tasty-quickcheck hs-source-dirs : SBVTestSuite main-is: SBVDocTest.hs other-modules : Utils.SBVTestFramework@@ -408,8 +429,18 @@ import : common-settings default-language: Haskell2010 - build-depends : base, directory, filepath, process, deepseq- , bytestring, tasty, tasty-golden, tasty-hunit, tasty-quickcheck, mtl, QuickCheck, sbv+ build-depends : QuickCheck+ , bytestring+ , deepseq+ , directory+ , filepath+ , mtl+ , process+ , sbv+ , tasty+ , tasty-golden+ , tasty-hunit+ , tasty-quickcheck hs-source-dirs : SBVTestSuite other-modules : Utils.SBVTestFramework main-is : SBVHLint.hs@@ -420,7 +451,14 @@ default-language: Haskell2010 type : exitcode-stdio-1.0 ghc-options : -with-rtsopts=-K64m- build-depends : filepath, sbv, random, time , process, deepseq, tasty, tasty-bench+ build-depends : deepseq+ , filepath+ , process+ , random+ , sbv+ , tasty+ , tasty-bench+ , time hs-source-dirs : SBVBenchSuite main-is : SBVBench.hs other-modules : Utils.SBVBenchFramework