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.

Minimal complete definition

bvAddO, bvSubO, bvMulO, bvMulOFast, bvDivO, bvNegO

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 minumum 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

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

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

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

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

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

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

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

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

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)

Cast overflows

sFromIntegralO :: forall a b. (Integral a, HasKind a, Num a, SymWord a, HasKind b, Num b, SymWord 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, (false, false))
Q.E.D.

As the last example shows, converting to sInteger never underflows or overflows for any value.