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

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)

class (ArithOverflow (SBV a), Num a, SymWord 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.

Minimal complete definition

(+!), (-!), (*!), (/!), negateChecked

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

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.

sFromIntegralChecked :: forall a b. (?loc :: CallStack, Integral a, HasKind a, HasKind b, Num a, SymWord a, HasKind b, Num b, SymWord 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.