| Copyright | (c) Levent Erkok |
|---|---|
| License | BSD3 |
| Maintainer | erkokl@gmail.com |
| Stability | experimental |
| Safe Haskell | None |
| Language | Haskell2010 |
Data.SBV.Tools.Overflow
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
- class (ArithOverflow (SBV a), Num a, SymVal a) => CheckedArithmetic a where
- sFromIntegralO :: (Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b, SymVal b) => SBV a -> (SBV b, (SBool, SBool))
- sFromIntegralChecked :: (?loc :: CallStack, Integral a, HasKind a, HasKind b, Num a, SymVal a, HasKind b, Num b, SymVal b) => SBV a -> SBV b
Arithmetic overflows
class ArithOverflow a where Source #
Detecting overflow. Each function here will return sTrue if the result will not fit in the target
type, i.e., if it overflows or underflows.
Methods
bvAddO :: a -> a -> 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 minimum of the arguments.
>>>prove $ \x y -> bvAddO x (y::SWord16) .<=> x + y .< x `smin` yQ.E.D.
bvSubO :: a -> a -> SBool Source #
Bit-vector subtraction. Unsigned subtraction can only underflow. Signed subtraction can underflow and overflow.
bvMulO :: a -> a -> SBool Source #
Bit-vector multiplication. Unsigned multiplication can only overflow. Signed multiplication can underflow and overflow.
bvDivO :: a -> a -> 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 -> x `bvDivO` (y::SInt8)Solution #1: s0 = -128 :: Int8 s1 = -1 :: Int8 This is the only solution.
Bit-vector negation. Unsigned negation neither underflows nor overflows. Signed negation can only overflow, when the argument is
minBound:
>>>prove $ \x -> x .== minBound .<=> bvNegO (x::SInt16)Q.E.D.
Instances
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
(+!) :: SBV a -> SBV a -> SBV a infixl 6 Source #
(-!) :: SBV a -> SBV a -> SBV a infixl 6 Source #
(*!) :: SBV a -> SBV a -> SBV a infixl 7 Source #
(/!) :: SBV a -> SBV a -> SBV a infixl 7 Source #
negateChecked :: SBV a -> SBV a Source #
Instances
| CheckedArithmetic Int16 Source # | |
| CheckedArithmetic Int32 Source # | |
| CheckedArithmetic Int64 Source # | |
| CheckedArithmetic Int8 Source # | |
| CheckedArithmetic Word16 Source # | |
Defined in Data.SBV.Tools.Overflow | |
| CheckedArithmetic Word32 Source # | |
Defined in Data.SBV.Tools.Overflow | |
| CheckedArithmetic Word64 Source # | |
Defined in Data.SBV.Tools.Overflow | |
| CheckedArithmetic Word8 Source # | |
| (KnownNat n, BVIsNonZero n) => CheckedArithmetic (IntN n) Source # | |
| (KnownNat n, BVIsNonZero n) => CheckedArithmetic (WordN n) Source # | |
Cast overflows
sFromIntegralO :: (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.