Data.SBV.Tools.Overflow

Implementation of overflow detection functions. Based on: http://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/z3prefix.pdf

Arithmetic overflows

class ArithOverflow a where

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.

Methods

bvAddO :: a -> a -> (SBool, SBool)

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
Q.E.D.

bvSubO :: a -> a -> (SBool, SBool)

Bit-vector subtraction. Unsigned subtraction can only underflow. Signed subtraction can underflow and overflow.

bvMulO :: a -> a -> (SBool, SBool)

Bit-vector multiplication. Unsigned multiplication can only overflow. Signed multiplication can underflow and overflow.

bvMulOFast :: 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!

bvDivO :: a -> a -> (SBool, 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:

>>> allSat $ \x y -> snd (x `bvDivO` (y::SInt8))
Solution #1:
  s0 = -128 :: Int8
  s1 =   -1 :: Int8
This is the only solution.

bvNegO :: a -> (SBool, 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.

Instances

ArithOverflow SVal

Defined in Data.SBV.Tools.Overflow

Methods

bvAddO :: SVal -> SVal -> (SBool, SBool)

bvSubO :: SVal -> SVal -> (SBool, SBool)

bvMulO :: SVal -> SVal -> (SBool, SBool)

bvMulOFast :: SVal -> SVal -> (SBool, SBool)

bvDivO :: SVal -> SVal -> (SBool, SBool)

bvNegO :: SVal -> (SBool, SBool)

ArithOverflow SInt64

Defined in Data.SBV.Tools.Overflow

Methods

bvAddO :: SInt64 -> SInt64 -> (SBool, SBool)

bvSubO :: SInt64 -> SInt64 -> (SBool, SBool)

bvMulO :: SInt64 -> SInt64 -> (SBool, SBool)

bvMulOFast :: SInt64 -> SInt64 -> (SBool, SBool)

bvDivO :: SInt64 -> SInt64 -> (SBool, SBool)

bvNegO :: SInt64 -> (SBool, SBool)

ArithOverflow SInt32

Defined in Data.SBV.Tools.Overflow

Methods

bvAddO :: SInt32 -> SInt32 -> (SBool, SBool)

bvSubO :: SInt32 -> SInt32 -> (SBool, SBool)

bvMulO :: SInt32 -> SInt32 -> (SBool, SBool)

bvMulOFast :: SInt32 -> SInt32 -> (SBool, SBool)

bvDivO :: SInt32 -> SInt32 -> (SBool, SBool)

bvNegO :: SInt32 -> (SBool, SBool)

ArithOverflow SInt16

Defined in Data.SBV.Tools.Overflow

Methods

bvAddO :: SInt16 -> SInt16 -> (SBool, SBool)

bvSubO :: SInt16 -> SInt16 -> (SBool, SBool)

bvMulO :: SInt16 -> SInt16 -> (SBool, SBool)

bvMulOFast :: SInt16 -> SInt16 -> (SBool, SBool)

bvDivO :: SInt16 -> SInt16 -> (SBool, SBool)

bvNegO :: SInt16 -> (SBool, SBool)

ArithOverflow SInt8

Defined in Data.SBV.Tools.Overflow

Methods

bvAddO :: SInt8 -> SInt8 -> (SBool, SBool)

bvSubO :: SInt8 -> SInt8 -> (SBool, SBool)

bvMulO :: SInt8 -> SInt8 -> (SBool, SBool)

bvMulOFast :: SInt8 -> SInt8 -> (SBool, SBool)

bvDivO :: SInt8 -> SInt8 -> (SBool, SBool)

bvNegO :: SInt8 -> (SBool, SBool)

ArithOverflow SWord64

Defined in Data.SBV.Tools.Overflow

Methods

bvAddO :: SWord64 -> SWord64 -> (SBool, SBool)

bvSubO :: SWord64 -> SWord64 -> (SBool, SBool)

bvMulO :: SWord64 -> SWord64 -> (SBool, SBool)

bvMulOFast :: SWord64 -> SWord64 -> (SBool, SBool)

bvDivO :: SWord64 -> SWord64 -> (SBool, SBool)

bvNegO :: SWord64 -> (SBool, SBool)

ArithOverflow SWord32

Defined in Data.SBV.Tools.Overflow

Methods

bvAddO :: SWord32 -> SWord32 -> (SBool, SBool)

bvSubO :: SWord32 -> SWord32 -> (SBool, SBool)

bvMulO :: SWord32 -> SWord32 -> (SBool, SBool)

bvMulOFast :: SWord32 -> SWord32 -> (SBool, SBool)

bvDivO :: SWord32 -> SWord32 -> (SBool, SBool)

bvNegO :: SWord32 -> (SBool, SBool)

ArithOverflow SWord16

Defined in Data.SBV.Tools.Overflow

Methods

bvAddO :: SWord16 -> SWord16 -> (SBool, SBool)

bvSubO :: SWord16 -> SWord16 -> (SBool, SBool)

bvMulO :: SWord16 -> SWord16 -> (SBool, SBool)

bvMulOFast :: SWord16 -> SWord16 -> (SBool, SBool)

bvDivO :: SWord16 -> SWord16 -> (SBool, SBool)

bvNegO :: SWord16 -> (SBool, SBool)

ArithOverflow SWord8

Defined in Data.SBV.Tools.Overflow

Methods

bvAddO :: SWord8 -> SWord8 -> (SBool, SBool)

bvSubO :: SWord8 -> SWord8 -> (SBool, SBool)

bvMulO :: SWord8 -> SWord8 -> (SBool, SBool)

bvMulOFast :: SWord8 -> SWord8 -> (SBool, SBool)

bvDivO :: SWord8 -> SWord8 -> (SBool, SBool)

bvNegO :: SWord8 -> (SBool, SBool)

(KnownNat n, IsNonZero n) => ArithOverflow (SInt n)

Defined in Data.SBV.Tools.Overflow

Methods

bvAddO :: SInt n -> SInt n -> (SBool, SBool)

bvSubO :: SInt n -> SInt n -> (SBool, SBool)

bvMulO :: SInt n -> SInt n -> (SBool, SBool)

bvMulOFast :: SInt n -> SInt n -> (SBool, SBool)

bvDivO :: SInt n -> SInt n -> (SBool, SBool)

bvNegO :: SInt n -> (SBool, SBool)

(KnownNat n, IsNonZero n) => ArithOverflow (SWord n)

Defined in Data.SBV.Tools.Overflow

Methods

bvAddO :: SWord n -> SWord n -> (SBool, SBool)

bvSubO :: SWord n -> SWord n -> (SBool, SBool)

bvMulO :: SWord n -> SWord n -> (SBool, SBool)

bvMulOFast :: SWord n -> SWord n -> (SBool, SBool)

bvDivO :: SWord n -> SWord n -> (SBool, SBool)

bvNegO :: SWord n -> (SBool, SBool)

class (ArithOverflow (SBV a), Num a, SymVal a) => CheckedArithmetic a where

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

(+!) :: (?loc :: CallStack) => SBV a -> SBV a -> SBV a infixl 6

(-!) :: (?loc :: CallStack) => SBV a -> SBV a -> SBV a infixl 6

(*!) :: (?loc :: CallStack) => SBV a -> SBV a -> SBV a infixl 7

(/!) :: (?loc :: CallStack) => SBV a -> SBV a -> SBV a infixl 7

negateChecked :: (?loc :: CallStack) => SBV a -> SBV a

Instances

CheckedArithmetic Int8

Defined in Data.SBV.Tools.Overflow

Methods

(+!) :: SBV Int8 -> SBV Int8 -> SBV Int8

(-!) :: SBV Int8 -> SBV Int8 -> SBV Int8

(*!) :: SBV Int8 -> SBV Int8 -> SBV Int8

(/!) :: SBV Int8 -> SBV Int8 -> SBV Int8

negateChecked :: SBV Int8 -> SBV Int8

CheckedArithmetic Int16

Defined in Data.SBV.Tools.Overflow

Methods

(+!) :: SBV Int16 -> SBV Int16 -> SBV Int16

(-!) :: SBV Int16 -> SBV Int16 -> SBV Int16

(*!) :: SBV Int16 -> SBV Int16 -> SBV Int16

(/!) :: SBV Int16 -> SBV Int16 -> SBV Int16

negateChecked :: SBV Int16 -> SBV Int16

CheckedArithmetic Int32

Defined in Data.SBV.Tools.Overflow

Methods

(+!) :: SBV Int32 -> SBV Int32 -> SBV Int32

(-!) :: SBV Int32 -> SBV Int32 -> SBV Int32

(*!) :: SBV Int32 -> SBV Int32 -> SBV Int32

(/!) :: SBV Int32 -> SBV Int32 -> SBV Int32

negateChecked :: SBV Int32 -> SBV Int32

CheckedArithmetic Int64

Defined in Data.SBV.Tools.Overflow

Methods

(+!) :: SBV Int64 -> SBV Int64 -> SBV Int64

(-!) :: SBV Int64 -> SBV Int64 -> SBV Int64

(*!) :: SBV Int64 -> SBV Int64 -> SBV Int64

(/!) :: SBV Int64 -> SBV Int64 -> SBV Int64

negateChecked :: SBV Int64 -> SBV Int64

CheckedArithmetic Word8

Defined in Data.SBV.Tools.Overflow

Methods

(+!) :: SBV Word8 -> SBV Word8 -> SBV Word8

(-!) :: SBV Word8 -> SBV Word8 -> SBV Word8

(*!) :: SBV Word8 -> SBV Word8 -> SBV Word8

(/!) :: SBV Word8 -> SBV Word8 -> SBV Word8

negateChecked :: SBV Word8 -> SBV Word8

CheckedArithmetic Word16

Defined in Data.SBV.Tools.Overflow

Methods

(+!) :: SBV Word16 -> SBV Word16 -> SBV Word16

(-!) :: SBV Word16 -> SBV Word16 -> SBV Word16

(*!) :: SBV Word16 -> SBV Word16 -> SBV Word16

(/!) :: SBV Word16 -> SBV Word16 -> SBV Word16

negateChecked :: SBV Word16 -> SBV Word16

CheckedArithmetic Word32

Defined in Data.SBV.Tools.Overflow

Methods

(+!) :: SBV Word32 -> SBV Word32 -> SBV Word32

(-!) :: SBV Word32 -> SBV Word32 -> SBV Word32

(*!) :: SBV Word32 -> SBV Word32 -> SBV Word32

(/!) :: SBV Word32 -> SBV Word32 -> SBV Word32

negateChecked :: SBV Word32 -> SBV Word32

CheckedArithmetic Word64

Defined in Data.SBV.Tools.Overflow

Methods

(+!) :: SBV Word64 -> SBV Word64 -> SBV Word64

(-!) :: SBV Word64 -> SBV Word64 -> SBV Word64

(*!) :: SBV Word64 -> SBV Word64 -> SBV Word64

(/!) :: SBV Word64 -> SBV Word64 -> SBV Word64

negateChecked :: SBV Word64 -> SBV Word64

(KnownNat n, IsNonZero n) => CheckedArithmetic (IntN n)

Defined in Data.SBV.Tools.Overflow

Methods

(+!) :: SBV (IntN n) -> SBV (IntN n) -> SBV (IntN n)

(-!) :: SBV (IntN n) -> SBV (IntN n) -> SBV (IntN n)

(*!) :: SBV (IntN n) -> SBV (IntN n) -> SBV (IntN n)

(/!) :: SBV (IntN n) -> SBV (IntN n) -> SBV (IntN n)

negateChecked :: SBV (IntN n) -> SBV (IntN n)

(KnownNat n, IsNonZero n) => CheckedArithmetic (WordN n)

Defined in Data.SBV.Tools.Overflow

Methods

(+!) :: SBV (WordN n) -> SBV (WordN n) -> SBV (WordN n)

(-!) :: SBV (WordN n) -> SBV (WordN n) -> SBV (WordN n)

(*!) :: SBV (WordN n) -> SBV (WordN n) -> SBV (WordN n)

(/!) :: SBV (WordN n) -> SBV (WordN n) -> SBV (WordN n)

negateChecked :: SBV (WordN n) -> SBV (WordN n)

Cast overflows

sFromIntegralO :: forall a b. (Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b, SymVal b) => SBV a -> (SBV b, (SBool, SBool))

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.

sFromIntegralChecked :: forall a b. (?loc :: CallStack, Integral a, HasKind a, HasKind b, Num a, SymVal a, HasKind b, Num b, SymVal b) => SBV a -> SBV b

Version of sFromIntegral that has calls to sAssert for checking no overflow/underflow can happen. Use it with a safe call.