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

Copyright(c) Galois Inc. 2020
LicenseBSD-3
MaintainerBen Selfridge <benselfridge@galois.com>
Stabilityexperimental
Portabilityportable
Safe HaskellNone
LanguageHaskell2010

Data.BitVector.Sized.Overflow

Contents

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

Documentation

data Overflow a Source #

A value annotated with overflow information.

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

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

return :: a -> Overflow a #

fail :: String -> Overflow a #

Functor Overflow Source # 
Instance details

Defined in Data.BitVector.Sized.Overflow

Methods

fmap :: (a -> b) -> Overflow a -> Overflow b #

(<$) :: a -> Overflow b -> Overflow a #

Applicative Overflow Source # 
Instance details

Defined in Data.BitVector.Sized.Overflow

Methods

pure :: a -> Overflow a #

(<*>) :: Overflow (a -> b) -> Overflow a -> Overflow b #

liftA2 :: (a -> b -> c) -> Overflow a -> Overflow b -> Overflow c #

(*>) :: Overflow a -> Overflow b -> Overflow b #

(<*) :: Overflow a -> Overflow b -> Overflow a #

Foldable Overflow Source # 
Instance details

Defined in Data.BitVector.Sized.Overflow

Methods

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 #

toList :: Overflow a -> [a] #

null :: Overflow a -> Bool #

length :: Overflow a -> Int #

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

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

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

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

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

Traversable Overflow Source # 
Instance details

Defined in Data.BitVector.Sized.Overflow

Methods

traverse :: Applicative f => (a -> f b) -> Overflow a -> f (Overflow b) #

sequenceA :: Applicative f => Overflow (f a) -> f (Overflow a) #

mapM :: Monad m => (a -> m b) -> Overflow a -> m (Overflow b) #

sequence :: Monad m => Overflow (m a) -> m (Overflow a) #

Eq a => Eq (Overflow a) Source # 
Instance details

Defined in Data.BitVector.Sized.Overflow

Methods

(==) :: Overflow a -> Overflow a -> Bool #

(/=) :: Overflow a -> Overflow a -> Bool #

Show a => Show (Overflow a) Source # 
Instance details

Defined in Data.BitVector.Sized.Overflow

Methods

showsPrec :: Int -> Overflow a -> ShowS #

show :: Overflow a -> String #

showList :: [Overflow a] -> ShowS #

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 :: 1 <= w => NatRepr w -> BV w -> Natural -> Overflow (BV w) Source #

Left shift by positive Natural.

Overflowing arithmetic operators

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

Bitvector add.

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

Bitvector subtract.

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

Bitvector multiply.

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.

sdivOf :: 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 :: 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.