| Copyright | (c) Levent Erkok |
|---|---|
| License | BSD3 |
| Maintainer | erkokl@gmail.com |
| Stability | experimental |
| Safe Haskell | None |
| Language | Haskell2010 |
Data.SBV.Tools.Overflow
Description
Implementation of overflow detection functions. Based on: http://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/z3prefix.pdf
Synopsis
- class ArithOverflow a where
- class (ArithOverflow (SBV a), Num a, SymVal a) => CheckedArithmetic a where
- signedMulOverflow :: forall (n :: Nat). (KnownNat n, BVIsNonZero n, KnownNat (n + 1), BVIsNonZero (n + 1), KnownNat (2 + Log2 n), BVIsNonZero (2 + Log2 n)) => SInt n -> SInt n -> SBool
- sFromIntegralO :: (Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b, SymVal b) => SBV a -> (SBV b, (SBool, SBool))
- sFromIntegralChecked :: (?loc :: CallStack, Integral a, HasKind a, HasKind b, Num a, SymVal a, HasKind b, Num b, SymVal b) => SBV a -> SBV b
Arithmetic overflows
class ArithOverflow a where Source #
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.
Methods
bvAddO :: a -> a -> SBool Source #
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 -> bvAddO x (y::SWord16) .<=> x + y .< x `smin` yQ.E.D.
bvSubO :: a -> a -> SBool Source #
Bit-vector subtraction. Unsigned subtraction can only underflow. Signed subtraction can underflow and overflow.
bvMulO :: a -> a -> SBool Source #
Bit-vector multiplication. Unsigned multiplication can only overflow. Signed multiplication can underflow and overflow.
bvDivO :: a -> a -> SBool Source #
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:
>>>allSat $ \x y -> x `bvDivO` (y::SInt8)Solution #1: s0 = -128 :: Int8 s1 = -1 :: Int8 This is the only solution.
Bit-vector negation. Unsigned negation neither underflows nor overflows. Signed negation can only overflow, when the argument is
minBound:
>>>prove $ \x -> x .== minBound .<=> bvNegO (x::SInt16)Q.E.D.
Instances
class (ArithOverflow (SBV a), Num a, SymVal a) => CheckedArithmetic a where Source #
A class of checked-arithmetic operations. These follow the usual arithmetic,
except make calls to sAssert to ensure no overflow/underflow can occur.
Use them in conjunction with safe to ensure no overflow can happen.
Methods
(+!) :: SBV a -> SBV a -> SBV a infixl 6 Source #
(-!) :: SBV a -> SBV a -> SBV a infixl 6 Source #
(*!) :: SBV a -> SBV a -> SBV a infixl 7 Source #
(/!) :: SBV a -> SBV a -> SBV a infixl 7 Source #
negateChecked :: SBV a -> SBV a Source #
Instances
| CheckedArithmetic Int16 Source # | |
| CheckedArithmetic Int32 Source # | |
| CheckedArithmetic Int64 Source # | |
| CheckedArithmetic Int8 Source # | |
| CheckedArithmetic Word16 Source # | |
Defined in Data.SBV.Tools.Overflow | |
| CheckedArithmetic Word32 Source # | |
Defined in Data.SBV.Tools.Overflow | |
| CheckedArithmetic Word64 Source # | |
Defined in Data.SBV.Tools.Overflow | |
| CheckedArithmetic Word8 Source # | |
| (KnownNat n, BVIsNonZero n) => CheckedArithmetic (IntN n) Source # | |
| (KnownNat n, BVIsNonZero n) => CheckedArithmetic (WordN n) Source # | |
Fast-checking of signed-multiplication overflow
signedMulOverflow :: forall (n :: Nat). (KnownNat n, BVIsNonZero n, KnownNat (n + 1), BVIsNonZero (n + 1), KnownNat (2 + Log2 n), BVIsNonZero (2 + Log2 n)) => SInt n -> SInt n -> SBool Source #
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.
Cast overflows
sFromIntegralO :: (Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b, SymVal b) => SBV a -> (SBV b, (SBool, SBool)) Source #
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.
>>>sFromIntegralO (256 :: SInt16) :: (SWord8, (SBool, SBool))(0 :: SWord8,(False,True))>>>sFromIntegralO (-2 :: SInt16) :: (SWord8, (SBool, SBool))(254 :: SWord8,(True,False))>>>sFromIntegralO (2 :: SInt16) :: (SWord8, (SBool, SBool))(2 :: SWord8,(False,False))>>>prove $ \x -> sFromIntegralO (x::SInt32) .== (sFromIntegral x :: SInteger, (sFalse, sFalse))Q.E.D.
As the last example shows, converting to sInteger never underflows or overflows for any value.