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.