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

Data.SBV.Tools.Overflow

Description

Author : Levent Erkok License : BSD3 Maintainer: erkokl@gmail.com Stability : experimental

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

Synopsis

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

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  Source # Instance detailsDefined in Data.SBV.Tools.Overflow MethodsbvAddO :: 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 # Source # Instance detailsDefined in Data.SBV.Tools.Overflow MethodsbvAddO :: 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 # Source # Instance detailsDefined in Data.SBV.Tools.Overflow MethodsbvAddO :: 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 # Source # Instance detailsDefined in Data.SBV.Tools.Overflow MethodsbvAddO :: 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 # Source # Instance detailsDefined in Data.SBV.Tools.Overflow MethodsbvAddO :: 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 # Source # Instance detailsDefined in Data.SBV.Tools.Overflow MethodsbvAddO :: SWord64 -> SWord64 -> (SBool, SBool) Source #bvSubO :: SWord64 -> SWord64 -> (SBool, SBool) Source #bvMulO :: SWord64 -> SWord64 -> (SBool, SBool) Source #bvDivO :: SWord64 -> SWord64 -> (SBool, SBool) Source #bvNegO :: SWord64 -> (SBool, SBool) Source # Source # Instance detailsDefined in Data.SBV.Tools.Overflow MethodsbvAddO :: SWord32 -> SWord32 -> (SBool, SBool) Source #bvSubO :: SWord32 -> SWord32 -> (SBool, SBool) Source #bvMulO :: SWord32 -> SWord32 -> (SBool, SBool) Source #bvDivO :: SWord32 -> SWord32 -> (SBool, SBool) Source #bvNegO :: SWord32 -> (SBool, SBool) Source # Source # Instance detailsDefined in Data.SBV.Tools.Overflow MethodsbvAddO :: SWord16 -> SWord16 -> (SBool, SBool) Source #bvSubO :: SWord16 -> SWord16 -> (SBool, SBool) Source #bvMulO :: SWord16 -> SWord16 -> (SBool, SBool) Source #bvDivO :: SWord16 -> SWord16 -> (SBool, SBool) Source #bvNegO :: SWord16 -> (SBool, SBool) Source # Source # Instance detailsDefined in Data.SBV.Tools.Overflow MethodsbvAddO :: 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, 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 (+!) :: (?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  Source # Instance detailsDefined in Data.SBV.Tools.Overflow Methods Source # Instance detailsDefined in Data.SBV.Tools.Overflow Methods Source # Instance detailsDefined in Data.SBV.Tools.Overflow Methods Source # Instance detailsDefined in Data.SBV.Tools.Overflow Methods Source # Instance detailsDefined in Data.SBV.Tools.Overflow Methods Source # Instance detailsDefined in Data.SBV.Tools.Overflow Methods Source # Instance detailsDefined in Data.SBV.Tools.Overflow Methods Source # Instance detailsDefined in Data.SBV.Tools.Overflow Methods # 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)) 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.

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

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