Copyright | (c) Galois Inc. 2020 |
---|---|
License | BSD-3 |
Maintainer | Ben Selfridge <benselfridge@galois.com> |
Stability | experimental |
Portability | portable |
Safe Haskell | None |
Language | Haskell2010 |
This module provides alternative definitions of certain bitvector functions that might produce signed or unsigned overflow. Instead of producing a pure value, these versions produce the same value along with overflow flags. We only provide definitions for operators that might actually overflow.
Synopsis
- data Overflow a = Overflow UnsignedOverflow SignedOverflow a
- data UnsignedOverflow
- data SignedOverflow
- ofUnsigned :: Overflow a -> Bool
- ofSigned :: Overflow a -> Bool
- ofResult :: Overflow a -> a
- shlOf :: 1 <= w => NatRepr w -> BV w -> Natural -> Overflow (BV w)
- addOf :: 1 <= w => NatRepr w -> BV w -> BV w -> Overflow (BV w)
- subOf :: 1 <= w => NatRepr w -> BV w -> BV w -> Overflow (BV w)
- mulOf :: 1 <= w => NatRepr w -> BV w -> BV w -> Overflow (BV w)
- squotOf :: 1 <= w => NatRepr w -> BV w -> BV w -> Overflow (BV w)
- sremOf :: 1 <= w => NatRepr w -> BV w -> BV w -> Overflow (BV w)
- sdivOf :: 1 <= w => NatRepr w -> BV w -> BV w -> Overflow (BV w)
- smodOf :: 1 <= w => NatRepr w -> BV w -> BV w -> Overflow (BV w)
Documentation
A value annotated with overflow information.
Instances
Monad Overflow Source # | Monad for bitvector operations which might produce signed or unsigned overflow. |
Functor Overflow Source # | |
Applicative Overflow Source # | |
Foldable Overflow Source # | |
Defined in Data.BitVector.Sized.Overflow fold :: Monoid m => Overflow m -> m # foldMap :: Monoid m => (a -> m) -> Overflow a -> m # foldr :: (a -> b -> b) -> b -> Overflow a -> b # foldr' :: (a -> b -> b) -> b -> Overflow a -> b # foldl :: (b -> a -> b) -> b -> Overflow a -> b # foldl' :: (b -> a -> b) -> b -> Overflow a -> b # foldr1 :: (a -> a -> a) -> Overflow a -> a # foldl1 :: (a -> a -> a) -> Overflow a -> a # elem :: Eq a => a -> Overflow a -> Bool # maximum :: Ord a => Overflow a -> a # minimum :: Ord a => Overflow a -> a # | |
Traversable Overflow Source # | |
Eq a => Eq (Overflow a) Source # | |
Show a => Show (Overflow a) Source # | |
data UnsignedOverflow Source #
Datatype representing the possibility of unsigned overflow.
Instances
Eq UnsignedOverflow Source # | |
Defined in Data.BitVector.Sized.Overflow (==) :: UnsignedOverflow -> UnsignedOverflow -> Bool # (/=) :: UnsignedOverflow -> UnsignedOverflow -> Bool # | |
Show UnsignedOverflow Source # | |
Defined in Data.BitVector.Sized.Overflow showsPrec :: Int -> UnsignedOverflow -> ShowS # show :: UnsignedOverflow -> String # showList :: [UnsignedOverflow] -> ShowS # | |
Semigroup UnsignedOverflow Source # | |
Defined in Data.BitVector.Sized.Overflow (<>) :: UnsignedOverflow -> UnsignedOverflow -> UnsignedOverflow # sconcat :: NonEmpty UnsignedOverflow -> UnsignedOverflow # stimes :: Integral b => b -> UnsignedOverflow -> UnsignedOverflow # | |
Monoid UnsignedOverflow Source # | |
Defined in Data.BitVector.Sized.Overflow |
data SignedOverflow Source #
Datatype representing the possibility of signed overflow.
Instances
Eq SignedOverflow Source # | |
Defined in Data.BitVector.Sized.Overflow (==) :: SignedOverflow -> SignedOverflow -> Bool # (/=) :: SignedOverflow -> SignedOverflow -> Bool # | |
Show SignedOverflow Source # | |
Defined in Data.BitVector.Sized.Overflow showsPrec :: Int -> SignedOverflow -> ShowS # show :: SignedOverflow -> String # showList :: [SignedOverflow] -> ShowS # | |
Semigroup SignedOverflow Source # | |
Defined in Data.BitVector.Sized.Overflow (<>) :: SignedOverflow -> SignedOverflow -> SignedOverflow # sconcat :: NonEmpty SignedOverflow -> SignedOverflow # stimes :: Integral b => b -> SignedOverflow -> SignedOverflow # | |
Monoid SignedOverflow Source # | |
Defined in Data.BitVector.Sized.Overflow mappend :: SignedOverflow -> SignedOverflow -> SignedOverflow # mconcat :: [SignedOverflow] -> SignedOverflow # |
Overflowing bitwise operators
shlOf :: 1 <= w => NatRepr w -> BV w -> Natural -> Overflow (BV w) Source #
Left shift by positive Natural
.
Overflowing arithmetic operators
squotOf :: 1 <= w => NatRepr w -> BV w -> BV w -> Overflow (BV w) Source #
Bitvector division (signed). Rounds to zero. Division by zero yields a runtime error.
sremOf :: 1 <= w => NatRepr w -> BV w -> BV w -> Overflow (BV w) Source #
Bitvector remainder after division (signed), when rounded to zero. Division by zero yields a runtime error.