bv-sized-1.0.6: a bitvector datatype that is parameterized by the vector width

Copyright | (c) Galois Inc. 2020
License | BSD-3
Maintainer | Ben Selfridge <benselfridge@galois.com>
Stability | experimental
Portability | portable
Safe Haskell | None
Language | Haskell2010

Data.BitVector.Sized.Overflow

Contents

- Overflowing bitwise operators
- Overflowing arithmetic operators

Description

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
  - = UnsignedOverflow
  - | NoUnsignedOverflow
- data SignedOverflow
  - = SignedOverflow
  - | NoSignedOverflow
- ofUnsigned :: Overflow a -> Bool
- ofSigned :: Overflow a -> Bool
- ofResult :: Overflow a -> a
- shlOf :: forall (w :: Natural). 1 <= w => NatRepr w -> BV w -> Natural -> Overflow (BV w)
- addOf :: forall (w :: Natural). 1 <= w => NatRepr w -> BV w -> BV w -> Overflow (BV w)
- subOf :: forall (w :: Natural). 1 <= w => NatRepr w -> BV w -> BV w -> Overflow (BV w)
- mulOf :: forall (w :: Natural). 1 <= w => NatRepr w -> BV w -> BV w -> Overflow (BV w)
- squotOf :: forall (w :: Natural). 1 <= w => NatRepr w -> BV w -> BV w -> Overflow (BV w)
- sremOf :: forall (w :: Natural). 1 <= w => NatRepr w -> BV w -> BV w -> Overflow (BV w)
- sdivOf :: forall (w :: Natural). 1 <= w => NatRepr w -> BV w -> BV w -> Overflow (BV w)
- smodOf :: forall (w :: Natural). 1 <= w => NatRepr w -> BV w -> BV w -> Overflow (BV w)

# Documentation

data Overflow a Source #

A value annotated with overflow information.

Constructors

Overflow UnsignedOverflow SignedOverflow a |

#### Instances

Instances details

Applicative Overflow Source # |
Instance details Defined in Data.BitVector.Sized.Overflow Methods pure :: a -> Overflow a Source # (<*>) :: Overflow (a -> b) -> Overflow a -> Overflow b Source # liftA2 :: (a -> b -> c) -> Overflow a -> Overflow b -> Overflow c Source # (*>) :: Overflow a -> Overflow b -> Overflow b Source # (<*) :: Overflow a -> Overflow b -> Overflow a Source #
Functor Overflow Source # |
Instance details Defined in Data.BitVector.Sized.Overflow Methods fmap :: (a -> b) -> Overflow a -> Overflow b Source # (<$) :: a -> Overflow b -> Overflow a Source #
Monad Overflow Source # | Monad for bitvector operations which might produce signed or unsigned overflow.
Instance details Defined in Data.BitVector.Sized.Overflow Methods (>>=) :: Overflow a -> (a -> Overflow b) -> Overflow b Source # (>>) :: Overflow a -> Overflow b -> Overflow b Source # return :: a -> Overflow a Source #
Foldable Overflow Source # |

Instance details

Defined in Data.BitVector.Sized.Overflow

Methods

fold :: Monoid m => Overflow m -> m Source #

foldMap :: Monoid m => (a -> m) -> Overflow a -> m Source #

foldMap' :: Monoid m => (a -> m) -> Overflow a -> m Source #

foldr :: (a -> b -> b) -> b -> Overflow a -> b Source #

foldr' :: (a -> b -> b) -> b -> Overflow a -> b Source #

foldl :: (b -> a -> b) -> b -> Overflow a -> b Source #

foldl' :: (b -> a -> b) -> b -> Overflow a -> b Source #

foldr1 :: (a -> a -> a) -> Overflow a -> a Source #

foldl1 :: (a -> a -> a) -> Overflow a -> a Source #

toList :: Overflow a -> [a] Source #

null :: Overflow a -> Bool Source #

length :: Overflow a -> Int Source #

elem :: Eq a => a -> Overflow a -> Bool Source #

maximum :: Ord a => Overflow a -> a Source #

minimum :: Ord a => Overflow a -> a Source #

sum :: Num a => Overflow a -> a Source #

product :: Num a => Overflow a -> a Source #

Traversable Overflow Source # |
Instance details Defined in Data.BitVector.Sized.Overflow Methods traverse :: Applicative f => (a -> f b) -> Overflow a -> f (Overflow b) Source # sequenceA :: Applicative f => Overflow (f a) -> f (Overflow a) Source # mapM :: Monad m => (a -> m b) -> Overflow a -> m (Overflow b) Source # sequence :: Monad m => Overflow (m a) -> m (Overflow a) Source #
Show a => Show (Overflow a) Source # |
Instance details Defined in Data.BitVector.Sized.Overflow Methods showsPrec :: Int -> Overflow a -> ShowS Source # show :: Overflow a -> String Source # showList :: [Overflow a] -> ShowS Source #
Eq a => Eq (Overflow a) Source # |
Instance details Defined in Data.BitVector.Sized.Overflow Methods (==) :: Overflow a -> Overflow a -> Bool Source # (/=) :: Overflow a -> Overflow a -> Bool Source #

data UnsignedOverflow Source #

Datatype representing the possibility of unsigned overflow.

Constructors

UnsignedOverflow |
NoUnsignedOverflow |

#### Instances

Instances details

Monoid UnsignedOverflow Source # |
Instance details Defined in Data.BitVector.Sized.Overflow Methods mempty :: UnsignedOverflow Source # mappend :: UnsignedOverflow -> UnsignedOverflow -> UnsignedOverflow Source # mconcat :: [UnsignedOverflow] -> UnsignedOverflow Source #
Semigroup UnsignedOverflow Source # |
Instance details Defined in Data.BitVector.Sized.Overflow Methods (<>) :: UnsignedOverflow -> UnsignedOverflow -> UnsignedOverflow Source # sconcat :: NonEmpty UnsignedOverflow -> UnsignedOverflow Source # stimes :: Integral b => b -> UnsignedOverflow -> UnsignedOverflow Source #
Show UnsignedOverflow Source # |
Instance details Defined in Data.BitVector.Sized.Overflow Methods showsPrec :: Int -> UnsignedOverflow -> ShowS Source # show :: UnsignedOverflow -> String Source # showList :: [UnsignedOverflow] -> ShowS Source #
Eq UnsignedOverflow Source # |
Instance details Defined in Data.BitVector.Sized.Overflow Methods (==) :: UnsignedOverflow -> UnsignedOverflow -> Bool Source # (/=) :: UnsignedOverflow -> UnsignedOverflow -> Bool Source #

data SignedOverflow Source #

Datatype representing the possibility of signed overflow.

Constructors

SignedOverflow |
NoSignedOverflow |

#### Instances

Instances details

Monoid SignedOverflow Source # |
Instance details Defined in Data.BitVector.Sized.Overflow Methods mempty :: SignedOverflow Source # mappend :: SignedOverflow -> SignedOverflow -> SignedOverflow Source # mconcat :: [SignedOverflow] -> SignedOverflow Source #
Semigroup SignedOverflow Source # |
Instance details Defined in Data.BitVector.Sized.Overflow Methods (<>) :: SignedOverflow -> SignedOverflow -> SignedOverflow Source # sconcat :: NonEmpty SignedOverflow -> SignedOverflow Source # stimes :: Integral b => b -> SignedOverflow -> SignedOverflow Source #
Show SignedOverflow Source # |
Instance details Defined in Data.BitVector.Sized.Overflow Methods showsPrec :: Int -> SignedOverflow -> ShowS Source # show :: SignedOverflow -> String Source # showList :: [SignedOverflow] -> ShowS Source #
Eq SignedOverflow Source # |
Instance details Defined in Data.BitVector.Sized.Overflow Methods (==) :: SignedOverflow -> SignedOverflow -> Bool Source # (/=) :: SignedOverflow -> SignedOverflow -> Bool Source #

ofUnsigned :: Overflow a -> Bool Source #

Return `True` if a computation caused unsigned overflow.

ofSigned :: Overflow a -> Bool Source #

Return `True` if a computation caused signed overflow.

ofResult :: Overflow a -> a Source #

Return the result of a computation.

# Overflowing bitwise operators

shlOf :: forall (w :: Natural). 1 <= w => NatRepr w -> BV w -> Natural -> Overflow (BV w) Source #

Left shift by positive `Natural`.

# Overflowing arithmetic operators

addOf :: forall (w :: Natural). 1 <= w => NatRepr w -> BV w -> BV w -> Overflow (BV w) Source #

Bitvector add.

subOf :: forall (w :: Natural). 1 <= w => NatRepr w -> BV w -> BV w -> Overflow (BV w) Source #

Bitvector subtract.

mulOf :: forall (w :: Natural). 1 <= w => NatRepr w -> BV w -> BV w -> Overflow (BV w) Source #

Bitvector multiply.

squotOf :: forall (w :: Natural). 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 :: forall (w :: Natural). 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.

sdivOf :: forall (w :: Natural). 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.

smodOf :: forall (w :: Natural). 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.