diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,6 +1,19 @@ * Hackage: * GitHub: +### 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. diff --git a/Data/SBV/Control/Utils.hs b/Data/SBV/Control/Utils.hs --- a/Data/SBV/Control/Utils.hs +++ b/Data/SBV/Control/Utils.hs @@ -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 diff --git a/Data/SBV/Core/Floating.hs b/Data/SBV/Core/Floating.hs --- a/Data/SBV/Core/Floating.hs +++ b/Data/SBV/Core/Floating.hs @@ -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 diff --git a/Data/SBV/Tools/Overflow.hs b/Data/SBV/Tools/Overflow.hs --- a/Data/SBV/Tools/Overflow.hs +++ b/Data/SBV/Tools/Overflow.hs @@ -10,12 +10,14 @@ -- Based on: ----------------------------------------------------------------------------- +{-# 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 diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -176,6 +176,7 @@ Daniel Wagner, Sean Weaver, Nis Wegmann, -and Jared Ziegler. +Jared Ziegler, +and Marco Zocca. Thanks! diff --git a/SBVTestSuite/GoldFiles/allSat8.gold b/SBVTestSuite/GoldFiles/allSat8.gold --- a/SBVTestSuite/GoldFiles/allSat8.gold +++ b/SBVTestSuite/GoldFiles/allSat8.gold @@ -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 diff --git a/SBVTestSuite/GoldFiles/nested1.gold b/SBVTestSuite/GoldFiles/nested1.gold --- a/SBVTestSuite/GoldFiles/nested1.gold +++ b/SBVTestSuite/GoldFiles/nested1.gold @@ -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 diff --git a/SBVTestSuite/GoldFiles/nested2.gold b/SBVTestSuite/GoldFiles/nested2.gold --- a/SBVTestSuite/GoldFiles/nested2.gold +++ b/SBVTestSuite/GoldFiles/nested2.gold @@ -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 diff --git a/SBVTestSuite/GoldFiles/nested3.gold b/SBVTestSuite/GoldFiles/nested3.gold --- a/SBVTestSuite/GoldFiles/nested3.gold +++ b/SBVTestSuite/GoldFiles/nested3.gold @@ -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 diff --git a/SBVTestSuite/GoldFiles/nested4.gold b/SBVTestSuite/GoldFiles/nested4.gold --- a/SBVTestSuite/GoldFiles/nested4.gold +++ b/SBVTestSuite/GoldFiles/nested4.gold @@ -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 diff --git a/SBVTestSuite/GoldFiles/noOpt1.gold b/SBVTestSuite/GoldFiles/noOpt1.gold --- a/SBVTestSuite/GoldFiles/noOpt1.gold +++ b/SBVTestSuite/GoldFiles/noOpt1.gold @@ -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 diff --git a/SBVTestSuite/GoldFiles/noOpt2.gold b/SBVTestSuite/GoldFiles/noOpt2.gold --- a/SBVTestSuite/GoldFiles/noOpt2.gold +++ b/SBVTestSuite/GoldFiles/noOpt2.gold @@ -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 diff --git a/SBVTestSuite/GoldFiles/set_uninterp1.gold b/SBVTestSuite/GoldFiles/set_uninterp1.gold --- a/SBVTestSuite/GoldFiles/set_uninterp1.gold +++ b/SBVTestSuite/GoldFiles/set_uninterp1.gold @@ -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: diff --git a/SBVTestSuite/TestSuite/Overflows/Arithmetic.hs b/SBVTestSuite/TestSuite/Overflows/Arithmetic.hs --- a/SBVTestSuite/TestSuite/Overflows/Arithmetic.hs +++ b/SBVTestSuite/TestSuite/Overflows/Arithmetic.hs @@ -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" -} diff --git a/sbv.cabal b/sbv.cabal --- a/sbv.cabal +++ b/sbv.cabal @@ -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