sbv-7.13: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | None
Language | Haskell2010

Data.SBV.Tools.Overflow

Contents

- Arithmetic overflows
- Cast overflows

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
  - bvAddO :: a -> a -> (SBool, SBool)
  - bvSubO :: a -> a -> (SBool, SBool)
  - bvMulO :: a -> a -> (SBool, SBool)
  - bvMulOFast :: a -> a -> (SBool, SBool)
  - bvDivO :: a -> a -> (SBool, SBool)
  - bvNegO :: a -> (SBool, SBool)
- class (ArithOverflow (SBV a), Num a, SymWord a) => CheckedArithmetic a where
  - (+!) :: (?loc :: CallStack) => SBV a -> SBV a -> SBV a
  - (-!) :: (?loc :: CallStack) => SBV a -> SBV a -> SBV a
  - (*!) :: (?loc :: CallStack) => SBV a -> SBV a -> SBV a
  - (/!) :: (?loc :: CallStack) => SBV a -> SBV a -> SBV a
  - negateChecked :: (?loc :: CallStack) => SBV a -> SBV a
- sFromIntegralO :: forall a b. (Integral a, HasKind a, Num a, SymWord a, HasKind b, Num b, SymWord b) => SBV a -> (SBV b, (SBool, SBool))
- 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

# Arithmetic overflows

class ArithOverflow a where Source #

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) 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 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) Source #

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

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

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

bvMulOFast :: a -> a -> (SBool, SBool) Source #

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) 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 -> snd (x `bvDivO` (y::SInt8))
    Solution #1:
      s0 = -128 :: Int8
      s1 =   -1 :: Int8
    This is the only solution.

bvNegO :: a -> (SBool, SBool) Source #

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 Source # |
Instance details Defined in Data.SBV.Tools.Overflow Methods bvAddO :: SVal -> SVal -> (SBool, SBool) Source # bvSubO :: SVal -> SVal -> (SBool, SBool) Source # bvMulO :: SVal -> SVal -> (SBool, SBool) Source # bvMulOFast :: SVal -> SVal -> (SBool, SBool) Source # bvDivO :: SVal -> SVal -> (SBool, SBool) Source # bvNegO :: SVal -> (SBool, SBool) Source #
ArithOverflow SInt64 Source # |
Instance details Defined in Data.SBV.Tools.Overflow Methods bvAddO :: SInt64 -> SInt64 -> (SBool, SBool) Source # bvSubO :: SInt64 -> SInt64 -> (SBool, SBool) Source # bvMulO :: SInt64 -> SInt64 -> (SBool, SBool) Source # bvMulOFast :: SInt64 -> SInt64 -> (SBool, SBool) Source # bvDivO :: SInt64 -> SInt64 -> (SBool, SBool) Source # bvNegO :: SInt64 -> (SBool, SBool) Source #
ArithOverflow SInt32 Source # |
Instance details Defined in Data.SBV.Tools.Overflow Methods bvAddO :: SInt32 -> SInt32 -> (SBool, SBool) Source # bvSubO :: SInt32 -> SInt32 -> (SBool, SBool) Source # bvMulO :: SInt32 -> SInt32 -> (SBool, SBool) Source # bvMulOFast :: SInt32 -> SInt32 -> (SBool, SBool) Source # bvDivO :: SInt32 -> SInt32 -> (SBool, SBool) Source # bvNegO :: SInt32 -> (SBool, SBool) Source #
ArithOverflow SInt16 Source # |
Instance details Defined in Data.SBV.Tools.Overflow Methods bvAddO :: SInt16 -> SInt16 -> (SBool, SBool) Source # bvSubO :: SInt16 -> SInt16 -> (SBool, SBool) Source # bvMulO :: SInt16 -> SInt16 -> (SBool, SBool) Source # bvMulOFast :: SInt16 -> SInt16 -> (SBool, SBool) Source # bvDivO :: SInt16 -> SInt16 -> (SBool, SBool) Source # bvNegO :: SInt16 -> (SBool, SBool) Source #
ArithOverflow SInt8 Source # |
Instance details Defined in Data.SBV.Tools.Overflow Methods bvAddO :: SInt8 -> SInt8 -> (SBool, SBool) Source # bvSubO :: SInt8 -> SInt8 -> (SBool, SBool) Source # bvMulO :: SInt8 -> SInt8 -> (SBool, SBool) Source # bvMulOFast :: SInt8 -> SInt8 -> (SBool, SBool) Source # bvDivO :: SInt8 -> SInt8 -> (SBool, SBool) Source # bvNegO :: SInt8 -> (SBool, SBool) Source #
ArithOverflow SWord64 Source # |
Instance details Defined in Data.SBV.Tools.Overflow Methods bvAddO :: SWord64 -> SWord64 -> (SBool, SBool) Source # bvSubO :: SWord64 -> SWord64 -> (SBool, SBool) Source # bvMulO :: SWord64 -> SWord64 -> (SBool, SBool) Source # bvMulOFast :: SWord64 -> SWord64 -> (SBool, SBool) Source # bvDivO :: SWord64 -> SWord64 -> (SBool, SBool) Source # bvNegO :: SWord64 -> (SBool, SBool) Source #
ArithOverflow SWord32 Source # |
Instance details Defined in Data.SBV.Tools.Overflow Methods bvAddO :: SWord32 -> SWord32 -> (SBool, SBool) Source # bvSubO :: SWord32 -> SWord32 -> (SBool, SBool) Source # bvMulO :: SWord32 -> SWord32 -> (SBool, SBool) Source # bvMulOFast :: SWord32 -> SWord32 -> (SBool, SBool) Source # bvDivO :: SWord32 -> SWord32 -> (SBool, SBool) Source # bvNegO :: SWord32 -> (SBool, SBool) Source #
ArithOverflow SWord16 Source # |
Instance details Defined in Data.SBV.Tools.Overflow Methods bvAddO :: SWord16 -> SWord16 -> (SBool, SBool) Source # bvSubO :: SWord16 -> SWord16 -> (SBool, SBool) Source # bvMulO :: SWord16 -> SWord16 -> (SBool, SBool) Source # bvMulOFast :: SWord16 -> SWord16 -> (SBool, SBool) Source # bvDivO :: SWord16 -> SWord16 -> (SBool, SBool) Source # bvNegO :: SWord16 -> (SBool, SBool) Source #
ArithOverflow SWord8 Source # |
Instance details Defined in Data.SBV.Tools.Overflow Methods bvAddO :: SWord8 -> SWord8 -> (SBool, SBool) Source # bvSubO :: SWord8 -> SWord8 -> (SBool, SBool) Source # bvMulO :: SWord8 -> SWord8 -> (SBool, SBool) Source # bvMulOFast :: SWord8 -> SWord8 -> (SBool, SBool) Source # bvDivO :: SWord8 -> SWord8 -> (SBool, SBool) Source # bvNegO :: SWord8 -> (SBool, SBool) Source #

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

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

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

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

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

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

Instances

CheckedArithmetic Int8 Source # |
Instance details Defined in Data.SBV.Tools.Overflow Methods (+!) :: SBV Int8 -> SBV Int8 -> SBV Int8 Source # (-!) :: SBV Int8 -> SBV Int8 -> SBV Int8 Source # (*!) :: SBV Int8 -> SBV Int8 -> SBV Int8 Source # (/!) :: SBV Int8 -> SBV Int8 -> SBV Int8 Source # negateChecked :: SBV Int8 -> SBV Int8 Source #
CheckedArithmetic Int16 Source # |
Instance details Defined in Data.SBV.Tools.Overflow Methods (+!) :: SBV Int16 -> SBV Int16 -> SBV Int16 Source # (-!) :: SBV Int16 -> SBV Int16 -> SBV Int16 Source # (*!) :: SBV Int16 -> SBV Int16 -> SBV Int16 Source # (/!) :: SBV Int16 -> SBV Int16 -> SBV Int16 Source # negateChecked :: SBV Int16 -> SBV Int16 Source #
CheckedArithmetic Int32 Source # |
Instance details Defined in Data.SBV.Tools.Overflow Methods (+!) :: SBV Int32 -> SBV Int32 -> SBV Int32 Source # (-!) :: SBV Int32 -> SBV Int32 -> SBV Int32 Source # (*!) :: SBV Int32 -> SBV Int32 -> SBV Int32 Source # (/!) :: SBV Int32 -> SBV Int32 -> SBV Int32 Source # negateChecked :: SBV Int32 -> SBV Int32 Source #
CheckedArithmetic Int64 Source # |
Instance details Defined in Data.SBV.Tools.Overflow Methods (+!) :: SBV Int64 -> SBV Int64 -> SBV Int64 Source # (-!) :: SBV Int64 -> SBV Int64 -> SBV Int64 Source # (*!) :: SBV Int64 -> SBV Int64 -> SBV Int64 Source # (/!) :: SBV Int64 -> SBV Int64 -> SBV Int64 Source # negateChecked :: SBV Int64 -> SBV Int64 Source #
CheckedArithmetic Word8 Source # |
Instance details Defined in Data.SBV.Tools.Overflow Methods (+!) :: SBV Word8 -> SBV Word8 -> SBV Word8 Source # (-!) :: SBV Word8 -> SBV Word8 -> SBV Word8 Source # (*!) :: SBV Word8 -> SBV Word8 -> SBV Word8 Source # (/!) :: SBV Word8 -> SBV Word8 -> SBV Word8 Source # negateChecked :: SBV Word8 -> SBV Word8 Source #
CheckedArithmetic Word16 Source # |
Instance details Defined in Data.SBV.Tools.Overflow Methods (+!) :: SBV Word16 -> SBV Word16 -> SBV Word16 Source # (-!) :: SBV Word16 -> SBV Word16 -> SBV Word16 Source # (*!) :: SBV Word16 -> SBV Word16 -> SBV Word16 Source # (/!) :: SBV Word16 -> SBV Word16 -> SBV Word16 Source # negateChecked :: SBV Word16 -> SBV Word16 Source #
CheckedArithmetic Word32 Source # |
Instance details Defined in Data.SBV.Tools.Overflow Methods (+!) :: SBV Word32 -> SBV Word32 -> SBV Word32 Source # (-!) :: SBV Word32 -> SBV Word32 -> SBV Word32 Source # (*!) :: SBV Word32 -> SBV Word32 -> SBV Word32 Source # (/!) :: SBV Word32 -> SBV Word32 -> SBV Word32 Source # negateChecked :: SBV Word32 -> SBV Word32 Source #
CheckedArithmetic Word64 Source # |
Instance details Defined in Data.SBV.Tools.Overflow Methods (+!) :: SBV Word64 -> SBV Word64 -> SBV Word64 Source # (-!) :: SBV Word64 -> SBV Word64 -> SBV Word64 Source # (*!) :: SBV Word64 -> SBV Word64 -> SBV Word64 Source # (/!) :: SBV Word64 -> SBV Word64 -> SBV Word64 Source # negateChecked :: SBV Word64 -> SBV Word64 Source #

# 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)) 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, (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 Source #

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