Safe Haskell | None |
---|---|

Language | Haskell2010 |

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

- class ArithOverflow a where
- class (ArithOverflow (SBV a), Num a, SymVal a) => CheckedArithmetic a where
- sFromIntegralO :: forall a b. (Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b, SymVal b) => SBV a -> (SBV b, (SBool, SBool))
- 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

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

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.

`>>>`

Q.E.D.`prove $ \x y -> snd (bvAddO x (y::SWord16)) .<=> x + y .< x `smin` y`

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`

:

`>>>`

Solution #1: s0 = -128 :: Int8 s1 = -1 :: Int8 This is the only solution.`allSat $ \x y -> snd (x `bvDivO` (y::SInt8))`

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

Bit-vector negation. Unsigned negation neither underflows nor overflows. Signed negation can only overflow, when the argument is
`minBound`

:

`>>>`

Q.E.D.`prove $ \x -> x .== minBound .<=> snd (bvNegO (x::SInt16))`

## Instances

ArithOverflow SVal Source # | |

Defined in Data.SBV.Tools.Overflow | |

ArithOverflow SInt64 Source # | |

Defined in Data.SBV.Tools.Overflow | |

ArithOverflow SInt32 Source # | |

Defined in Data.SBV.Tools.Overflow | |

ArithOverflow SInt16 Source # | |

Defined in Data.SBV.Tools.Overflow | |

ArithOverflow SInt8 Source # | |

ArithOverflow SWord64 Source # | |

Defined in Data.SBV.Tools.Overflow | |

ArithOverflow SWord32 Source # | |

Defined in Data.SBV.Tools.Overflow | |

ArithOverflow SWord16 Source # | |

Defined in Data.SBV.Tools.Overflow | |

ArithOverflow SWord8 Source # | |

Defined in Data.SBV.Tools.Overflow |

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.

(+!) :: (?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

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

`>>>`

(0 :: SWord8,(False,True))`sFromIntegralO (256 :: SInt16) :: (SWord8, (SBool, SBool))`

`>>>`

(254 :: SWord8,(True,False))`sFromIntegralO (-2 :: SInt16) :: (SWord8, (SBool, SBool))`

`>>>`

(2 :: SWord8,(False,False))`sFromIntegralO (2 :: SInt16) :: (SWord8, (SBool, SBool))`

`>>>`

Q.E.D.`prove $ \x -> sFromIntegralO (x::SInt32) .== (sFromIntegral x :: SInteger, (sFalse, sFalse))`

As the last example shows, converting to `sInteger`

never underflows or overflows for any value.