From 5a8ea1b7763ea2b68b09bdc2d921e77aa38d434b Mon Sep 17 00:00:00 2001 From: Levent Erkok Date: Tue, 21 Nov 2023 15:53:17 -0800 Subject: [PATCH] Ue SMTLib predicates/semantics for overflows Fixes #657 --- CHANGES.md | 7 + Data/SBV/Core/Operations.hs | 11 +- Data/SBV/Core/Symbolic.hs | 19 +- Data/SBV/SMT/SMTLib2.hs | 3 +- Data/SBV/Tools/Overflow.hs | 278 +++--------------- .../TestSuite/Overflows/Arithmetic.hs | 219 ++++---------- 6 files changed, 126 insertions(+), 411 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index aee0d49a2..4e9d45969 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -21,6 +21,13 @@ It can render both ground definitions and functions, and the latter can be handy in producing SMTLib functions to be used in other settings. + * Fix a bug in bit-vector rotation that manifested itself in small-bv sizes. Thanks to Sirui Lu for reporting. + + * [BACKWARDS COMPATIBILITY] Change the overflow detection API to match the new SMTLib predicates. These predicates + do not distinguish between over/underflow, so strictly speaking the new API is less powerful than the old one. However, + we choose to follow SMTLib here for portability purposes. If you need separate overflow/underflow checking you can + use the encodings from earlier implementations, please get in touch if this proves problematic. + ### Version 10.2, 2023-06-09 * Improve HLint pragmas. Thanks to George Thomas for the patch. diff --git a/Data/SBV/Core/Operations.hs b/Data/SBV/Core/Operations.hs index a9dfc7dab..e033f7cd5 100644 --- a/Data/SBV/Core/Operations.hs +++ b/Data/SBV/Core/Operations.hs @@ -33,7 +33,7 @@ module Data.SBV.Core.Operations , svSign, svUnsign, svSetBit, svWordFromBE, svWordFromLE , svExp, svFromIntegral -- ** Overflows - , svMkOverflow + , svMkOverflow1, svMkOverflow2 -- ** Derived operations , svToWord1, svFromWord1, svTestBit , svShiftLeft, svShiftRight @@ -1028,8 +1028,13 @@ svRotate unboundedShifter opRot curRot x i -------------------------------------------------------------------------------- -- | Overflow detection. -svMkOverflow :: OvOp -> SVal -> SVal -> SVal -svMkOverflow o x y = SVal KBool (Right (cache r)) +svMkOverflow1 :: OvOp -> SVal -> SVal +svMkOverflow1 o x = SVal KBool (Right (cache r)) + where r st = do sx <- svToSV st x + newExpr st KBool $ SBVApp (OverflowOp o) [sx] + +svMkOverflow2 :: OvOp -> SVal -> SVal -> SVal +svMkOverflow2 o x y = SVal KBool (Right (cache r)) where r st = do sx <- svToSV st x sy <- svToSV st y newExpr st KBool $ SBVApp (OverflowOp o) [sx, sy] diff --git a/Data/SBV/Core/Symbolic.hs b/Data/SBV/Core/Symbolic.hs index 665b88fc0..a234e45ab 100644 --- a/Data/SBV/Core/Symbolic.hs +++ b/Data/SBV/Core/Symbolic.hs @@ -336,16 +336,21 @@ data PBOp = PB_AtMost Int -- ^ At most k deriving (Eq, Ord, Show, G.Data) -- | Overflow operations -data OvOp = Overflow_SMul_OVFL -- ^ Signed multiplication overflow - | Overflow_SMul_UDFL -- ^ Signed multiplication underflow - | Overflow_UMul_OVFL -- ^ Unsigned multiplication overflow +data OvOp = PlusOv Bool -- ^ Addition overflow. Bool is True if signed. + | SubOv Bool -- ^ Subtraction overflow. Bool is True if signed. + | MulOv Bool -- ^ Multiplication overflow. Bool is True if signed. + | DivOv -- ^ Division overflow. Only signed, since unsigned division does not overflow. + | NegOv -- ^ Unary negation overflow. Only signed, since unsigned negation does not overflow. deriving (Eq, Ord, G.Data) --- | Show instance. It's important that these follow the internal z3 names +-- | Show instance. It's important that these follow the SMTLib names. instance Show OvOp where - show Overflow_SMul_OVFL = "bvsmul_noovfl" - show Overflow_SMul_UDFL = "bvsmul_noudfl" - show Overflow_UMul_OVFL = "bvumul_noovfl" + show (PlusOv signed) = "bv" ++ (if signed then "s" else "u") ++ "addo" + show (SubOv signed) = "bv" ++ (if signed then "s" else "u") ++ "subo" + show (MulOv signed) = "bv" ++ (if signed then "s" else "u") ++ "mulo" + show DivOv = "bvsdivo" + show NegOv = "bvnego" -- TODO: z3 takes the name bvnego; but this might actually be bvsnego when finally formalized + -- Reported at: https://github.com/Z3Prover/z3/issues/7010 -- | String operations. Note that we do not define @StrAt@ as it translates to 'StrSubstr' trivially. data StrOp = StrConcat -- ^ Concatenation of one or more strings diff --git a/Data/SBV/SMT/SMTLib2.hs b/Data/SBV/SMT/SMTLib2.hs index a0023c019..fc0a8a2c9 100644 --- a/Data/SBV/SMT/SMTLib2.hs +++ b/Data/SBV/SMT/SMTLib2.hs @@ -1029,8 +1029,7 @@ cvtExp curProgInfo caps rm tableMap functionMap expr@(SBVApp _ arguments) = sh e | True = reducePB pb args' where args' = map cvtSV args - -- NB: Z3 semantics have the predicates reversed: i.e., it returns true if overflow isn't possible. Hence the not. - sh (SBVApp (OverflowOp op) args) = "(not (" ++ show op ++ " " ++ unwords (map cvtSV args) ++ "))" + sh (SBVApp (OverflowOp op) args) = "(" ++ show op ++ " " ++ unwords (map cvtSV args) ++ ")" -- Note the unfortunate reversal in StrInRe.. sh (SBVApp (StrOp (StrInRe r)) args) = "(str.in.re " ++ unwords (map cvtSV args) ++ " " ++ regExpToSMTString r ++ ")" diff --git a/Data/SBV/Tools/Overflow.hs b/Data/SBV/Tools/Overflow.hs index 101cf0057..64f9168e1 100644 --- a/Data/SBV/Tools/Overflow.hs +++ b/Data/SBV/Tools/Overflow.hs @@ -48,29 +48,22 @@ import Data.Proxy -- >>> -- For doctest purposes only: -- >>> import Data.SBV --- | Detecting underflow/overflow conditions. For each function, --- the first result is the condition under which the computation --- underflows, and the second is the condition under which it --- overflows. +-- | Detecting overflow. Each function here will return 'sTrue' if the result will not fit in the target +-- type, i.e., if it overflows or underflows. class ArithOverflow a where -- | Bit-vector addition. Unsigned addition can only overflow. Signed addition can underflow and overflow. -- -- A tell tale sign of unsigned addition overflow is when the sum is less than minimum of the arguments. -- - -- >>> prove $ \x y -> snd (bvAddO x (y::SWord16)) .<=> x + y .< x `smin` y + -- >>> prove $ \x y -> bvAddO x (y::SWord16) .<=> x + y .< x `smin` y -- Q.E.D. - bvAddO :: a -> a -> (SBool, SBool) + bvAddO :: a -> a -> SBool -- | Bit-vector subtraction. Unsigned subtraction can only underflow. Signed subtraction can underflow and overflow. - bvSubO :: a -> a -> (SBool, SBool) + bvSubO :: a -> a -> SBool -- | Bit-vector multiplication. Unsigned multiplication can only overflow. Signed multiplication can underflow and overflow. - bvMulO :: a -> a -> (SBool, SBool) - - -- | Same as 'bvMulO', except instead of doing the computation internally, it simply sends it off to z3 as a primitive. - -- Obviously, only use if you have the z3 backend! Note that z3 provides this operation only when no logic is set, - -- so make sure to call @setLogic Logic_NONE@ in your program! - bvMulOFast :: a -> a -> (SBool, SBool) + bvMulO :: a -> a -> SBool -- | Bit-vector division. Unsigned division neither underflows nor overflows. Signed division can only overflow. In fact, for each -- signed bitvector type, there's precisely one pair that overflows, when @x@ is @minBound@ and @y@ is @-1@: @@ -80,34 +73,33 @@ class ArithOverflow a where -- s0 = -128 :: Int8 -- s1 = -1 :: Int8 -- This is the only solution. - bvDivO :: a -> a -> (SBool, SBool) + bvDivO :: a -> a -> SBool -- | Bit-vector negation. Unsigned negation neither underflows nor overflows. Signed negation can only overflow, when the argument is -- @minBound@: -- -- >>> prove $ \x -> x .== minBound .<=> snd (bvNegO (x::SInt16)) -- Q.E.D. - bvNegO :: a -> (SBool, SBool) + bvNegO :: a -> SBool -instance ArithOverflow SWord8 where {bvAddO = l2 bvAddO; bvSubO = l2 bvSubO; bvMulO = l2 bvMulO; bvMulOFast = l2 bvMulOFast; bvDivO = l2 bvDivO; bvNegO = l1 bvNegO} -instance ArithOverflow SWord16 where {bvAddO = l2 bvAddO; bvSubO = l2 bvSubO; bvMulO = l2 bvMulO; bvMulOFast = l2 bvMulOFast; bvDivO = l2 bvDivO; bvNegO = l1 bvNegO} -instance ArithOverflow SWord32 where {bvAddO = l2 bvAddO; bvSubO = l2 bvSubO; bvMulO = l2 bvMulO; bvMulOFast = l2 bvMulOFast; bvDivO = l2 bvDivO; bvNegO = l1 bvNegO} -instance ArithOverflow SWord64 where {bvAddO = l2 bvAddO; bvSubO = l2 bvSubO; bvMulO = l2 bvMulO; bvMulOFast = l2 bvMulOFast; bvDivO = l2 bvDivO; bvNegO = l1 bvNegO} -instance ArithOverflow SInt8 where {bvAddO = l2 bvAddO; bvSubO = l2 bvSubO; bvMulO = l2 bvMulO; bvMulOFast = l2 bvMulOFast; bvDivO = l2 bvDivO; bvNegO = l1 bvNegO} -instance ArithOverflow SInt16 where {bvAddO = l2 bvAddO; bvSubO = l2 bvSubO; bvMulO = l2 bvMulO; bvMulOFast = l2 bvMulOFast; bvDivO = l2 bvDivO; bvNegO = l1 bvNegO} -instance ArithOverflow SInt32 where {bvAddO = l2 bvAddO; bvSubO = l2 bvSubO; bvMulO = l2 bvMulO; bvMulOFast = l2 bvMulOFast; bvDivO = l2 bvDivO; bvNegO = l1 bvNegO} -instance ArithOverflow SInt64 where {bvAddO = l2 bvAddO; bvSubO = l2 bvSubO; bvMulO = l2 bvMulO; bvMulOFast = l2 bvMulOFast; bvDivO = l2 bvDivO; bvNegO = l1 bvNegO} +instance ArithOverflow SWord8 where {bvAddO = l2 bvAddO; bvSubO = l2 bvSubO; bvMulO = l2 bvMulO; bvDivO = l2 bvDivO; bvNegO = l1 bvNegO} +instance ArithOverflow SWord16 where {bvAddO = l2 bvAddO; bvSubO = l2 bvSubO; bvMulO = l2 bvMulO; bvDivO = l2 bvDivO; bvNegO = l1 bvNegO} +instance ArithOverflow SWord32 where {bvAddO = l2 bvAddO; bvSubO = l2 bvSubO; bvMulO = l2 bvMulO; bvDivO = l2 bvDivO; bvNegO = l1 bvNegO} +instance ArithOverflow SWord64 where {bvAddO = l2 bvAddO; bvSubO = l2 bvSubO; bvMulO = l2 bvMulO; bvDivO = l2 bvDivO; bvNegO = l1 bvNegO} +instance ArithOverflow SInt8 where {bvAddO = l2 bvAddO; bvSubO = l2 bvSubO; bvMulO = l2 bvMulO; bvDivO = l2 bvDivO; bvNegO = l1 bvNegO} +instance ArithOverflow SInt16 where {bvAddO = l2 bvAddO; bvSubO = l2 bvSubO; bvMulO = l2 bvMulO; bvDivO = l2 bvDivO; bvNegO = l1 bvNegO} +instance ArithOverflow SInt32 where {bvAddO = l2 bvAddO; bvSubO = l2 bvSubO; bvMulO = l2 bvMulO; bvDivO = l2 bvDivO; bvNegO = l1 bvNegO} +instance ArithOverflow SInt64 where {bvAddO = l2 bvAddO; bvSubO = l2 bvSubO; bvMulO = l2 bvMulO; bvDivO = l2 bvDivO; bvNegO = l1 bvNegO} -instance (KnownNat n, BVIsNonZero n) => ArithOverflow (SWord n) where {bvAddO = l2 bvAddO; bvSubO = l2 bvSubO; bvMulO = l2 bvMulO; bvMulOFast = l2 bvMulOFast; bvDivO = l2 bvDivO; bvNegO = l1 bvNegO} -instance (KnownNat n, BVIsNonZero n) => ArithOverflow (SInt n) where {bvAddO = l2 bvAddO; bvSubO = l2 bvSubO; bvMulO = l2 bvMulO; bvMulOFast = l2 bvMulOFast; bvDivO = l2 bvDivO; bvNegO = l1 bvNegO} +instance (KnownNat n, BVIsNonZero n) => ArithOverflow (SWord n) where {bvAddO = l2 bvAddO; bvSubO = l2 bvSubO; bvMulO = l2 bvMulO; bvDivO = l2 bvDivO; bvNegO = l1 bvNegO} +instance (KnownNat n, BVIsNonZero n) => ArithOverflow (SInt n) where {bvAddO = l2 bvAddO; bvSubO = l2 bvSubO; bvMulO = l2 bvMulO; bvDivO = l2 bvDivO; bvNegO = l1 bvNegO} instance ArithOverflow SVal where - bvAddO = signPick2 bvuaddo bvsaddo - bvSubO = signPick2 bvusubo bvssubo - bvMulO = signPick2 bvumulo bvsmulo - bvMulOFast = signPick2 bvumuloFast bvsmuloFast - bvDivO = signPick2 bvudivo bvsdivo - bvNegO = signPick1 bvunego bvsnego + bvAddO = signPick2 (svMkOverflow2 (PlusOv False)) (svMkOverflow2 (PlusOv True)) + bvSubO = signPick2 (svMkOverflow2 (SubOv False)) (svMkOverflow2 (SubOv True)) + bvMulO = signPick2 (svMkOverflow2 (MulOv False)) (svMkOverflow2 (MulOv True)) + bvDivO = signPick2 (const (const svFalse)) (svMkOverflow2 DivOv) -- unsigned division doesn't overflow + bvNegO = signPick1 (const svFalse) (svMkOverflow1 NegOv) -- unsigned unary negation doesn't overflow -- | A class of checked-arithmetic operations. These follow the usual arithmetic, -- except make calls to 'Data.SBV.sAssert' to ensure no overflow/underflow can occur. @@ -192,45 +184,6 @@ instance (KnownNat n, BVIsNonZero n) => CheckedArithmetic (IntN n) where (/!) = checkOp2 ?loc "division" sDiv bvDivO negateChecked = checkOp1 ?loc "unary negation" negate bvNegO - --- | Zero-extend to given bits -zx :: Int -> SVal -> SVal -zx n a - | n < sa = error $ "Data.SBV: Unexpected zero extension: from: " ++ show (intSizeOf a) ++ " to: " ++ show n - | True = p `svJoin` a - where sa = intSizeOf a - s = hasSign a - p = svInteger (KBounded s (n - sa)) 0 - --- | Sign-extend to given bits. Note that we keep the signedness of the argument. -sx :: Int -> SVal -> SVal -sx n a - | n < sa = error $ "Data.SBV: Unexpected sign extension: from: " ++ show (intSizeOf a) ++ " to: " ++ show n - | True = p `svJoin` a - where sa = intSizeOf a - mk = svInteger $ KBounded (hasSign a) (n - sa) - p = svIte (pos a) (mk 0) (mk (-1)) - --- | Get the sign-bit -signBit :: SVal -> SVal -signBit x = x `svTestBit` (intSizeOf x - 1) - --- | Is the sign-bit high? -neg :: SVal -> SVal -neg x = signBit x `svEqual` svTrue - --- | Is the sign-bit low? -pos :: SVal -> SVal -pos x = signBit x `svEqual` svFalse - --- | Do these have the same sign? -sameSign :: SVal -> SVal -> SVal -sameSign x y = (pos x `svAnd` pos y) `svOr` (neg x `svAnd` neg y) - --- | Do these have opposing signs? -diffSign :: SVal -> SVal -> SVal -diffSign x y = svNot (sameSign x y) - -- | Check all true svAll :: [SVal] -> SVal svAll = foldr svAnd svTrue @@ -253,155 +206,6 @@ allOne m n (SBV x) = svAll [svTestBit x i `svEqual` svTrue | i <- [m, m-1 .. n]] where sz = intSizeOf x --- | Unsigned addition. Can only overflow. -bvuaddo :: Int -> SVal -> SVal -> (SVal, SVal) -bvuaddo n x y = (underflow, overflow) - where underflow = svFalse - - n' = n+1 - overflow = neg $ zx n' x `svPlus` zx n' y - --- | Signed addition. -bvsaddo :: Int -> SVal -> SVal -> (SVal, SVal) -bvsaddo _n x y = (underflow, overflow) - where underflow = svAll [neg x, neg y, pos (x `svPlus` y)] - overflow = svAll [pos x, pos y, neg (x `svPlus` y)] - --- | Unsigned subtraction. Can only underflow. -bvusubo :: Int -> SVal -> SVal -> (SVal, SVal) -bvusubo _n x y = (underflow, overflow) - where underflow = y `svGreaterThan` x - overflow = svFalse - --- | Signed subtraction. -bvssubo :: Int -> SVal -> SVal -> (SVal, SVal) -bvssubo _n x y = (underflow, overflow) - where underflow = svAll [neg x, pos y, pos (x `svMinus` y)] - overflow = svAll [pos x, neg y, neg (x `svMinus` y)] - --- | Unsigned multiplication. Can only overflow. -bvumulo :: Int -> SVal -> SVal -> (SVal, SVal) -bvumulo 0 _ _ = (svFalse, svFalse) -bvumulo n x y = (underflow, overflow) - where underflow = svFalse - - n1 = n+1 - overflow1 = signBit $ zx n1 x `svTimes` zx n1 y - - -- From Z3 sources: - -- - -- expr_ref ovf(m()), v(m()), tmp(m()); - -- ovf = m().mk_false(); - -- v = m().mk_false(); - -- for (unsigned i = 1; i < sz; ++i) { - -- mk_or(ovf, a_bits[sz-i], ovf); - -- mk_and(ovf, b_bits[i], tmp); - -- mk_or(tmp, v, v); - -- } - -- overflow2 = v; - -- - overflow2 = go 1 svFalse svFalse - where go i ovf v - | i >= n = v - | True = go (i+1) ovf' v' - where ovf' = ovf `svOr` (x `svTestBit` (n-i)) - tmp = ovf' `svAnd` (y `svTestBit` i) - v' = tmp `svOr` v - - overflow = overflow1 `svOr` overflow2 - --- | Signed multiplication. -bvsmulo :: Int -> SVal -> SVal -> (SVal, SVal) -bvsmulo 0 _ _ = (svFalse, svFalse) -bvsmulo n x y = (underflow, overflow) - where underflow = diffSign x y `svAnd` overflowPossible - overflow = sameSign x y `svAnd` overflowPossible - - n1 = n+1 - overflow1 = (xy1 `svTestBit` n) `svXOr` (xy1 `svTestBit` (n-1)) - where xy1 = sx n1 x `svTimes` sx n1 y - - -- From Z3 sources: - -- expr_ref v(m()), tmp(m()), a(m()), b(m()), a_acc(m()), sign(m()); - -- a_acc = m().mk_false(); - -- v = m().mk_false(); - -- for (unsigned i = 1; i + 1 < sz; ++i) { - -- mk_xor(b_bits[sz-1], b_bits[i], b); - -- mk_xor(a_bits[sz-1], a_bits[sz-1-i], a); - -- mk_or(a, a_acc, a_acc); - -- mk_and(a_acc, b, tmp); - -- mk_or(tmp, v, v); - -- } - -- overflow2 = v; - overflow2 = go 1 svFalse svFalse - where sY = signBit y - sX = signBit x - go i v a_acc - | i + 1 >= n = v - | True = go (i+1) v' a_acc' - where b = sY `svXOr` (y `svTestBit` i) - a = sX `svXOr` (x `svTestBit` (n-1-i)) - a_acc' = a `svOr` a_acc - tmp = a_acc' `svAnd` b - v' = tmp `svOr` v - - overflowPossible = overflow1 `svOr` overflow2 - --- | Is this a concrete value? -known :: SVal -> Bool -known (SVal _ (Left _)) = True -known _ = False - --- | Unsigned multiplication, fast version using z3 primitives. -bvumuloFast :: Int -> SVal -> SVal -> (SVal, SVal) -bvumuloFast n x y - | known x && known y -- Not particularly fast, but avoids shipping of to the solver - = bvumulo n x y - | True - = (underflow, overflow) - where underflow = fst $ bvumulo n x y -- No internal version for underflow exists (because it can't underflow) - overflow = svMkOverflow Overflow_UMul_OVFL x y - --- | Signed multiplication, fast version using z3 primitives. -bvsmuloFast :: Int -> SVal -> SVal -> (SVal, SVal) -bvsmuloFast n x y - | known x && known y -- Not particularly fast, but avoids shipping of to the solver - = bvsmulo n x y - | True - = (underflow, overflow) - where underflow = svMkOverflow Overflow_SMul_UDFL x y - overflow = svMkOverflow Overflow_SMul_OVFL x y - --- | Unsigned division. Neither underflows, nor overflows. -bvudivo :: Int -> SVal -> SVal -> (SVal, SVal) -bvudivo _ _ _ = (underflow, overflow) - where underflow = svFalse - overflow = svFalse - --- | Signed division. Can only overflow. -bvsdivo :: Int -> SVal -> SVal -> (SVal, SVal) -bvsdivo n x y = (underflow, overflow) - where underflow = svFalse - - ones = svInteger (KBounded True n) (-1) - topSet = svInteger (KBounded True n) (2^(n-1)) - - overflow = svAll [x `svEqual` topSet, y `svEqual` ones] - --- | Unsigned negation. Neither underflows, nor overflows. -bvunego :: Int -> SVal -> (SVal, SVal) -bvunego _ _ = (underflow, overflow) - where underflow = svFalse - overflow = svFalse - --- | Signed negation. Can only overflow. -bvsnego :: Int -> SVal -> (SVal, SVal) -bvsnego n x = (underflow, overflow) - where underflow = svFalse - - topSet = svInteger (KBounded True n) (2^(n-1)) - overflow = x `svEqual` topSet - -- | Detecting underflow/overflow conditions for casting between bit-vectors. The first output is the result, -- the second component itself is a pair with the first boolean indicating underflow and the second indicating overflow. -- @@ -490,38 +294,28 @@ sFromIntegralChecked x = sAssert (Just ?loc) (msg "underflows") (sNot u) -- Helpers -l2 :: (SVal -> SVal -> (SBool, SBool)) -> SBV a -> SBV a -> (SBool, SBool) +l2 :: (SVal -> SVal -> SBool) -> SBV a -> SBV a -> SBool l2 f (SBV a) (SBV b) = f a b -l1 :: (SVal -> (SBool, SBool)) -> SBV a -> (SBool, SBool) +l1 :: (SVal -> SBool) -> SBV a -> SBool l1 f (SBV a) = f a -signPick2 :: (Int -> SVal -> SVal -> (SVal, SVal)) -> (Int -> SVal -> SVal -> (SVal, SVal)) -> (SVal -> SVal -> (SBool, SBool)) +signPick2 :: (SVal -> SVal -> SVal) -> (SVal -> SVal -> SVal) -> (SVal -> SVal -> SBool) signPick2 fu fs a b - | hasSign a = let (u, o) = fs n a b in (SBV u, SBV o) - | True = let (u, o) = fu n a b in (SBV u, SBV o) - where n = intSizeOf a + | hasSign a = SBV (fs a b) + | True = SBV (fu a b) -signPick1 :: (Int -> SVal -> (SVal, SVal)) -> (Int -> SVal -> (SVal, SVal)) -> (SVal -> (SBool, SBool)) +signPick1 :: (SVal -> SVal) -> (SVal -> SVal) -> (SVal -> SBool) signPick1 fu fs a - | hasSign a = let (u, o) = fs n a in (SBV u, SBV o) - | True = let (u, o) = fu n a in (SBV u, SBV o) - where n = intSizeOf a - -checkOp1 :: (HasKind a, HasKind b) => CallStack -> String -> (a -> SBV b) -> (a -> (SBool, SBool)) -> a -> SBV b -checkOp1 loc w op cop a = sAssert (Just loc) (msg "underflows") (sNot u) - $ sAssert (Just loc) (msg "overflows") (sNot o) - $ op a + | hasSign a = SBV (fs a) + | True = SBV (fu a) + +checkOp1 :: (HasKind a, HasKind b) => CallStack -> String -> (a -> SBV b) -> (a -> SBool) -> a -> SBV b +checkOp1 loc w op cop a = sAssert (Just loc) (msg "overflows") (sNot (cop a)) $ op a where k = show $ kindOf a msg c = k ++ " " ++ w ++ " " ++ c - (u, o) = cop a - -checkOp2 :: (HasKind a, HasKind c) => CallStack -> String -> (a -> b -> SBV c) -> (a -> b -> (SBool, SBool)) -> a -> b -> SBV c -checkOp2 loc w op cop a b = sAssert (Just loc) (msg "underflows") (sNot u) - $ sAssert (Just loc) (msg "overflows") (sNot o) - $ a `op` b +checkOp2 :: (HasKind a, HasKind c) => CallStack -> String -> (a -> b -> SBV c) -> (a -> b -> SBool) -> a -> b -> SBV c +checkOp2 loc w op cop a b = sAssert (Just loc) (msg "overflows") (sNot (a `cop` b)) $ a `op` b where k = show $ kindOf a msg c = k ++ " " ++ w ++ " " ++ c - - (u, o) = a `cop` b diff --git a/SBVTestSuite/TestSuite/Overflows/Arithmetic.hs b/SBVTestSuite/TestSuite/Overflows/Arithmetic.hs index 436e68fef..6577cfe17 100644 --- a/SBVTestSuite/TestSuite/Overflows/Arithmetic.hs +++ b/SBVTestSuite/TestSuite/Overflows/Arithmetic.hs @@ -27,101 +27,61 @@ import Utils.SBVTestFramework -- Test suite tests :: TestTree tests = testGroup "Overflows" [testGroup "Arithmetic" ts] - where ts = [ testGroup "add-uf" [ testCase "w8" $ assertIsThm $ underflow svPlus (bvAddO :: SWord8 -> SWord8 -> (SBool, SBool)) - , testCase "w16" $ assertIsThm $ underflow svPlus (bvAddO :: SWord16 -> SWord16 -> (SBool, SBool)) - , testCase "w32" $ assertIsThm $ underflow svPlus (bvAddO :: SWord32 -> SWord32 -> (SBool, SBool)) - , testCase "w64" $ assertIsThm $ underflow svPlus (bvAddO :: SWord64 -> SWord64 -> (SBool, SBool)) - , testCase "i8" $ assertIsThm $ underflow svPlus (bvAddO :: SInt8 -> SInt8 -> (SBool, SBool)) - , testCase "i16" $ assertIsThm $ underflow svPlus (bvAddO :: SInt16 -> SInt16 -> (SBool, SBool)) - , testCase "i32" $ assertIsThm $ underflow svPlus (bvAddO :: SInt32 -> SInt32 -> (SBool, SBool)) - , testCase "i64" $ assertIsThm $ underflow svPlus (bvAddO :: SInt64 -> SInt64 -> (SBool, SBool)) + where ts = [ testGroup "add-ov" [ testCase "w8" $ assertIsThm $ overflow svPlus (bvAddO :: SWord8 -> SWord8 -> SBool) + , testCase "w16" $ assertIsThm $ overflow svPlus (bvAddO :: SWord16 -> SWord16 -> SBool) + , testCase "w32" $ assertIsThm $ overflow svPlus (bvAddO :: SWord32 -> SWord32 -> SBool) + , testCase "w64" $ assertIsThm $ overflow svPlus (bvAddO :: SWord64 -> SWord64 -> SBool) + , testCase "i8" $ assertIsThm $ overflow svPlus (bvAddO :: SInt8 -> SInt8 -> SBool) + , testCase "i16" $ assertIsThm $ overflow svPlus (bvAddO :: SInt16 -> SInt16 -> SBool) + , testCase "i32" $ assertIsThm $ overflow svPlus (bvAddO :: SInt32 -> SInt32 -> SBool) + , testCase "i64" $ assertIsThm $ overflow svPlus (bvAddO :: SInt64 -> SInt64 -> SBool) ] - , testGroup "add-of" [ testCase "w8" $ assertIsThm $ overflow svPlus (bvAddO :: SWord8 -> SWord8 -> (SBool, SBool)) - , testCase "w16" $ assertIsThm $ overflow svPlus (bvAddO :: SWord16 -> SWord16 -> (SBool, SBool)) - , testCase "w32" $ assertIsThm $ overflow svPlus (bvAddO :: SWord32 -> SWord32 -> (SBool, SBool)) - , testCase "w64" $ assertIsThm $ overflow svPlus (bvAddO :: SWord64 -> SWord64 -> (SBool, SBool)) - , testCase "i8" $ assertIsThm $ overflow svPlus (bvAddO :: SInt8 -> SInt8 -> (SBool, SBool)) - , testCase "i16" $ assertIsThm $ overflow svPlus (bvAddO :: SInt16 -> SInt16 -> (SBool, SBool)) - , testCase "i32" $ assertIsThm $ overflow svPlus (bvAddO :: SInt32 -> SInt32 -> (SBool, SBool)) - , testCase "i64" $ assertIsThm $ overflow svPlus (bvAddO :: SInt64 -> SInt64 -> (SBool, SBool)) - ] - , testGroup "sub-uf" [ testCase "w8" $ assertIsThm $ underflow svMinus (bvSubO :: SWord8 -> SWord8 -> (SBool, SBool)) - , testCase "w16" $ assertIsThm $ underflow svMinus (bvSubO :: SWord16 -> SWord16 -> (SBool, SBool)) - , testCase "w32" $ assertIsThm $ underflow svMinus (bvSubO :: SWord32 -> SWord32 -> (SBool, SBool)) - , testCase "w64" $ assertIsThm $ underflow svMinus (bvSubO :: SWord64 -> SWord64 -> (SBool, SBool)) - , testCase "i8" $ assertIsThm $ underflow svMinus (bvSubO :: SInt8 -> SInt8 -> (SBool, SBool)) - , testCase "i16" $ assertIsThm $ underflow svMinus (bvSubO :: SInt16 -> SInt16 -> (SBool, SBool)) - , testCase "i32" $ assertIsThm $ underflow svMinus (bvSubO :: SInt32 -> SInt32 -> (SBool, SBool)) - , testCase "i64" $ assertIsThm $ underflow svMinus (bvSubO :: SInt64 -> SInt64 -> (SBool, SBool)) - ] - , testGroup "sub-of" [ testCase "w8" $ assertIsThm $ overflow svMinus (bvSubO :: SWord8 -> SWord8 -> (SBool, SBool)) - , testCase "w16" $ assertIsThm $ overflow svMinus (bvSubO :: SWord16 -> SWord16 -> (SBool, SBool)) - , testCase "w32" $ assertIsThm $ overflow svMinus (bvSubO :: SWord32 -> SWord32 -> (SBool, SBool)) - , testCase "w64" $ assertIsThm $ overflow svMinus (bvSubO :: SWord64 -> SWord64 -> (SBool, SBool)) - , testCase "i8" $ assertIsThm $ overflow svMinus (bvSubO :: SInt8 -> SInt8 -> (SBool, SBool)) - , testCase "i16" $ assertIsThm $ overflow svMinus (bvSubO :: SInt16 -> SInt16 -> (SBool, SBool)) - , testCase "i32" $ assertIsThm $ overflow svMinus (bvSubO :: SInt32 -> SInt32 -> (SBool, SBool)) - , testCase "i64" $ assertIsThm $ overflow svMinus (bvSubO :: SInt64 -> SInt64 -> (SBool, SBool)) - ] - , testGroup "mul-uf" [ testCase "w8" $ assertIsThm $ underflow svTimes (bvMulO :: SWord8 -> SWord8 -> (SBool, SBool)) - , testCase "w16" $ assertIsThm $ underflow svTimes (bvMulO :: SWord16 -> SWord16 -> (SBool, SBool)) - , testCase "w32" $ assertIsThm $ underflow svTimes (bvMulO :: SWord32 -> SWord32 -> (SBool, SBool)) - , testCase "w64" $ assertIsThm $ underflow svTimes (bvMulO :: SWord64 -> SWord64 -> (SBool, SBool)) - , testCase "i8" $ assertIsThm $ mulChkU bvMulOFast (bvMulO :: SInt8 -> SInt8 -> (SBool, SBool)) - , testCase "i16" $ assertIsThm $ mulChkU bvMulOFast (bvMulO :: SInt16 -> SInt16 -> (SBool, SBool)) - , testCase "i32" $ assertIsThm $ mulChkU bvMulOFast (bvMulO :: SInt32 -> SInt32 -> (SBool, SBool)) - , testCase "i64" $ assertIsThm $ mulChkU bvMulOFast (bvMulO :: SInt64 -> SInt64 -> (SBool, SBool)) - ] - , testGroup "mul-of" [ testCase "w8" $ assertIsThm $ mulChkO bvMulOFast (bvMulO :: SWord8 -> SWord8 -> (SBool, SBool)) - , testCase "w16" $ assertIsThm $ mulChkO bvMulOFast (bvMulO :: SWord16 -> SWord16 -> (SBool, SBool)) - , testCase "w32" $ assertIsThm $ mulChkO bvMulOFast (bvMulO :: SWord32 -> SWord32 -> (SBool, SBool)) - , testCase "w64" $ assertIsThm $ mulChkO bvMulOFast (bvMulO :: SWord64 -> SWord64 -> (SBool, SBool)) - , testCase "i8" $ assertIsThm $ mulChkO bvMulOFast (bvMulO :: SInt8 -> SInt8 -> (SBool, SBool)) - , testCase "i16" $ assertIsThm $ mulChkO bvMulOFast (bvMulO :: SInt16 -> SInt16 -> (SBool, SBool)) - , testCase "i32" $ assertIsThm $ mulChkO bvMulOFast (bvMulO :: SInt32 -> SInt32 -> (SBool, SBool)) - , testCase "i64" $ assertIsThm $ mulChkO bvMulOFast (bvMulO :: SInt64 -> SInt64 -> (SBool, SBool)) - ] - , testGroup "div-uf" [ testCase "w8" $ assertIsThm $ never svDivide (bvDivO :: SWord8 -> SWord8 -> (SBool, SBool)) - , testCase "w16" $ assertIsThm $ never svDivide (bvDivO :: SWord16 -> SWord16 -> (SBool, SBool)) - , testCase "w32" $ assertIsThm $ never svDivide (bvDivO :: SWord32 -> SWord32 -> (SBool, SBool)) - , testCase "w64" $ assertIsThm $ never svDivide (bvDivO :: SWord64 -> SWord64 -> (SBool, SBool)) - , testCase "i8" $ assertIsThm $ never svDivide (bvDivO :: SInt8 -> SInt8 -> (SBool, SBool)) - , testCase "i16" $ assertIsThm $ never svDivide (bvDivO :: SInt16 -> SInt16 -> (SBool, SBool)) - , testCase "i32" $ assertIsThm $ never svDivide (bvDivO :: SInt32 -> SInt32 -> (SBool, SBool)) - , testCase "i64" $ assertIsThm $ never svDivide (bvDivO :: SInt64 -> SInt64 -> (SBool, SBool)) + + , testGroup "sub-ov" [ testCase "w8" $ assertIsThm $ overflow svMinus (bvSubO :: SWord8 -> SWord8 -> SBool) + , testCase "w16" $ assertIsThm $ overflow svMinus (bvSubO :: SWord16 -> SWord16 -> SBool) + , testCase "w32" $ assertIsThm $ overflow svMinus (bvSubO :: SWord32 -> SWord32 -> SBool) + , testCase "w64" $ assertIsThm $ overflow svMinus (bvSubO :: SWord64 -> SWord64 -> SBool) + , testCase "i8" $ assertIsThm $ overflow svMinus (bvSubO :: SInt8 -> SInt8 -> SBool) + , testCase "i16" $ assertIsThm $ overflow svMinus (bvSubO :: SInt16 -> SInt16 -> SBool) + , testCase "i32" $ assertIsThm $ overflow svMinus (bvSubO :: SInt32 -> SInt32 -> SBool) + , testCase "i64" $ assertIsThm $ overflow svMinus (bvSubO :: SInt64 -> SInt64 -> SBool) ] - , testGroup "div-of" [ testCase "w8" $ assertIsThm $ never svDivide (bvDivO :: SWord8 -> SWord8 -> (SBool, SBool)) - , testCase "w16" $ assertIsThm $ never svDivide (bvDivO :: SWord16 -> SWord16 -> (SBool, SBool)) - , testCase "w32" $ assertIsThm $ never svDivide (bvDivO :: SWord32 -> SWord32 -> (SBool, SBool)) - , testCase "w64" $ assertIsThm $ never svDivide (bvDivO :: SWord64 -> SWord64 -> (SBool, SBool)) - , testCase "i8" $ assertIsThm $ divChk svDivide (bvDivO :: SInt8 -> SInt8 -> (SBool, SBool)) - , testCase "i16" $ assertIsThm $ divChk svDivide (bvDivO :: SInt16 -> SInt16 -> (SBool, SBool)) - , testCase "i32" $ assertIsThm $ divChk svDivide (bvDivO :: SInt32 -> SInt32 -> (SBool, SBool)) - , testCase "i64" $ assertIsThm $ divChk svDivide (bvDivO :: SInt64 -> SInt64 -> (SBool, SBool)) + + -- Multiplication checks are expensive; so only do at a few instances + , 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) + -- , testCase "w64" $ assertIsThm $ overflow svTimes (bvMulO :: SWord64 -> SWord64 -> SBool) + , testCase "i8" $ assertIsThm $ overflow svTimes (bvMulO :: SInt8 -> SInt8 -> SBool) + -- , testCase "i16" $ assertIsThm $ overflow svTimes (bvMulO :: SInt16 -> SInt16 -> SBool) + -- , testCase "i32" $ assertIsThm $ overflow svTimes (bvMulO :: SInt32 -> SInt32 -> SBool) + -- , testCase "i64" $ assertIsThm $ overflow svTimes (bvMulO :: SInt64 -> SInt64 -> SBool) ] - , testGroup "neg-uf" [ testCase "w8" $ assertIsThm $ never1 svNeg0 (bvNegO :: SWord8 -> (SBool, SBool)) - , testCase "w16" $ assertIsThm $ never1 svNeg0 (bvNegO :: SWord16 -> (SBool, SBool)) - , testCase "w32" $ assertIsThm $ never1 svNeg0 (bvNegO :: SWord32 -> (SBool, SBool)) - , testCase "w64" $ assertIsThm $ never1 svNeg0 (bvNegO :: SWord64 -> (SBool, SBool)) - , testCase "i8" $ assertIsThm $ underflow1 svNeg0 (bvNegO :: SInt8 -> (SBool, SBool)) - , testCase "i16" $ assertIsThm $ underflow1 svNeg0 (bvNegO :: SInt16 -> (SBool, SBool)) - , testCase "i32" $ assertIsThm $ underflow1 svNeg0 (bvNegO :: SInt32 -> (SBool, SBool)) - , testCase "i64" $ assertIsThm $ underflow1 svNeg0 (bvNegO :: SInt64 -> (SBool, SBool)) + + , 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) + , testCase "w64" $ assertIsThm $ never svDivide (bvDivO :: SWord64 -> SWord64 -> SBool) + , testCase "i8" $ assertIsThm $ overflow svDivide (bvDivO :: SInt8 -> SInt8 -> SBool) + , testCase "i16" $ assertIsThm $ overflow svDivide (bvDivO :: SInt16 -> SInt16 -> SBool) + , testCase "i32" $ assertIsThm $ overflow svDivide (bvDivO :: SInt32 -> SInt32 -> SBool) + , testCase "i64" $ assertIsThm $ overflow svDivide (bvDivO :: SInt64 -> SInt64 -> SBool) ] - , testGroup "neg-of" [ testCase "w8" $ assertIsThm $ never1 svNeg0 (bvNegO :: SWord8 -> (SBool, SBool)) - , testCase "w16" $ assertIsThm $ never1 svNeg0 (bvNegO :: SWord16 -> (SBool, SBool)) - , testCase "w32" $ assertIsThm $ never1 svNeg0 (bvNegO :: SWord32 -> (SBool, SBool)) - , testCase "w64" $ assertIsThm $ never1 svNeg0 (bvNegO :: SWord64 -> (SBool, SBool)) - , testCase "i8" $ assertIsThm $ overflow1 svNeg0 (bvNegO :: SInt8 -> (SBool, SBool)) - , testCase "i16" $ assertIsThm $ overflow1 svNeg0 (bvNegO :: SInt16 -> (SBool, SBool)) - , testCase "i32" $ assertIsThm $ overflow1 svNeg0 (bvNegO :: SInt32 -> (SBool, SBool)) - , testCase "i64" $ assertIsThm $ overflow1 svNeg0 (bvNegO :: SInt64 -> (SBool, SBool)) + + , testGroup "neg-ov" [ testCase "w8" $ assertIsThm $ never1 svNeg0 (bvNegO :: SWord8 -> SBool) + , testCase "w16" $ assertIsThm $ never1 svNeg0 (bvNegO :: SWord16 -> SBool) + , testCase "w32" $ assertIsThm $ never1 svNeg0 (bvNegO :: SWord32 -> SBool) + , testCase "w64" $ assertIsThm $ never1 svNeg0 (bvNegO :: SWord64 -> SBool) + , testCase "i8" $ assertIsThm $ overflow1 svNeg0 (bvNegO :: SInt8 -> SBool) + , testCase "i16" $ assertIsThm $ overflow1 svNeg0 (bvNegO :: SInt16 -> SBool) + , testCase "i32" $ assertIsThm $ overflow1 svNeg0 (bvNegO :: SInt32 -> SBool) + , testCase "i64" $ assertIsThm $ overflow1 svNeg0 (bvNegO :: SInt64 -> SBool) ] ] --- 256 bits is large enough to do all these proofs +-- 128 bits is large enough to do all these proofs large :: Int -large = 256 +large = 128 type SLarge = SVal @@ -143,100 +103,45 @@ toLarge v mkSigned = svFromIntegral (KBounded True large) --- Multiplication checks are expensive. For these, we simply check that the SBV encodings and the z3 versions are equivalent -mulChkO :: forall a. SymVal a => (SBV a -> SBV a -> (SBool, SBool)) -> (SBV a -> SBV a -> (SBool, SBool)) -> Predicate -mulChkO fast slow = do setLogic Logic_NONE - x <- free "x" - y <- free "y" - - let (_, ov1) = x `fast` y - (_, ov2) = x `slow` y - - return $ ov1 .== ov2 - --- Underflow mults -mulChkU :: forall a. SymVal a => (SBV a -> SBV a -> (SBool, SBool)) -> (SBV a -> SBV a -> (SBool, SBool)) -> Predicate -mulChkU fast slow = do setLogic Logic_NONE - x <- free "x" - y <- free "y" - - let (uf1, _) = x `fast` y - (uf2, _) = x `slow` y - - return $ uf1 .== uf2 - --- Signed division can only underflow under one condition, check that simply instead of trying to do an expensive embedding proof -divChk :: forall a. (Integral a, Bounded a, SymVal a) => (SLarge -> SLarge -> SLarge) -> (SBV a -> SBV a -> (SBool, SBool)) -> Predicate -divChk _op cond = do x <- free "x" - y <- free "y" - - let (_, overflowHappens) = x `cond` y - - special = (unSBV x `svEqual` topSet) `svAnd` (unSBV y `svEqual` neg1) - - n = intSizeOf x - neg1 = svInteger (KBounded True n) (-1) - topSet = svInteger (KBounded True n) (2^(n-1)) - - return $ overflowHappens `exactlyWhen` special - -- For a few cases, we expect them to "never" overflow. The "embedding proofs" are either too expensive (in case of division), or -- not possible (in case of negation). We capture these here. -never :: forall a. (Integral a, Bounded a, SymVal a) => (SLarge -> SLarge -> SLarge) -> (SBV a -> SBV a -> (SBool, SBool)) -> Predicate +never :: forall a. (Integral a, Bounded a, SymVal a) => (SLarge -> SLarge -> SLarge) -> (SBV a -> SBV a -> SBool) -> Predicate never _op cond = do x <- free "x" y <- free "y" - let (underflowHappens, _) = x `cond` y + let overFlowHappens = x `cond` y - return $ underflowHappens `exactlyWhen` svFalse + return $ overFlowHappens `exactlyWhen` svFalse -never1 :: forall a. (Integral a, Bounded a, SymVal a) => (SLarge -> SLarge) -> (SBV a -> (SBool, SBool)) -> Predicate +never1 :: forall a. (Integral a, Bounded a, SymVal a) => (SLarge -> SLarge) -> (SBV a -> SBool) -> Predicate never1 _op cond = do x <- free "x" - let (underflowHappens, _) = cond x - - return $ underflowHappens `exactlyWhen` svFalse - -underflow :: forall a. (Integral a, Bounded a, SymVal a) => (SLarge -> SLarge -> SLarge) -> (SBV a -> SBV a -> (SBool, SBool)) -> Predicate -underflow op cond = do x <- free "x" - y <- free "y" + let overflowHappens = cond x - let (underflowHappens, _) = x `cond` y + return $ overflowHappens `exactlyWhen` svFalse - extResult :: SLarge - extResult = toLarge x `op` toLarge y - - return $ underflowHappens `exactlyWhen` (extResult `svLessThan` toLarge (minBound :: SBV a)) - -overflow :: forall a. (Integral a, Bounded a, SymVal a) => (SLarge -> SLarge -> SLarge) -> (SBV a -> SBV a -> (SBool, SBool)) -> Predicate +overflow :: forall a. (Integral a, Bounded a, SymVal a) => (SLarge -> SLarge -> SLarge) -> (SBV a -> SBV a -> SBool) -> Predicate overflow op cond = do x <- free "x" y <- free "y" - let (_, overflowHappens) = x `cond` y + let overflowHappens = x `cond` y extResult :: SLarge extResult = toLarge x `op` toLarge y - return $ overflowHappens `exactlyWhen` (extResult `svGreaterThan` toLarge (maxBound :: SBV a)) - -underflow1 :: forall a. (Integral a, Bounded a, SymVal a) => (SLarge -> SLarge) -> (SBV a -> (SBool, SBool)) -> Predicate -underflow1 op cond = do x <- free "x" - - let (underflowHappens, _) = cond x - - extResult :: SLarge - extResult = op $ toLarge x - - return $ underflowHappens `exactlyWhen` (extResult `svLessThan` toLarge (minBound :: SBV a)) + return $ overflowHappens `exactlyWhen` ( (extResult `svGreaterThan` toLarge (maxBound :: SBV a)) + `svOr` (extResult `svLessThan` toLarge (minBound :: SBV a)) + ) -overflow1 :: forall a. (Integral a, Bounded a, SymVal a) => (SLarge -> SLarge) -> (SBV a -> (SBool, SBool)) -> Predicate +overflow1 :: forall a. (Integral a, Bounded a, SymVal a) => (SLarge -> SLarge) -> (SBV a -> SBool) -> Predicate overflow1 op cond = do x <- free "x" - let (_, overflowHappens) = cond x + let overflowHappens = cond x extResult :: SLarge extResult = op $ toLarge x - return $ overflowHappens `exactlyWhen` (extResult `svGreaterThan` toLarge (maxBound :: SBV a)) + return $ overflowHappens `exactlyWhen` ( (extResult `svGreaterThan` toLarge (maxBound :: SBV a)) + `svOr` (extResult `svLessThan` toLarge (minBound :: SBV a))) {- HLint ignore module "Reduce duplication" -}