Data.BitVector.Sized.App

This module exports a type, BVApp, to aid in building expression languages over BitVectors. Let expr :: Nat -> * be some ADT of expressions that yield BitVectors when evaluated. Then, given one or more values of type expr w (i.e. one or more of these evaluatable expressions), BVApp provides the various constructors necessary for creating compound expressions involving pure BitVector operations. The expr type can (and often will) include a constructor of type BVApp expr w -> expr w in order to create a recursive expression language.

In addition to the BVApp type, we provide an evaluator which, given a function mapping values of type expr w to BitVectors, will evaluate the compound BVApp expressions.

Documentation

data BVApp (expr :: Nat -> *) (w :: Nat) where

Represents the application of a BitVector operation to one or more subexpressions.

Constructors

LitBVApp :: BitVector w -> BVApp expr w

AndApp :: !(expr w) -> !(expr w) -> BVApp expr w

OrApp :: !(expr w) -> !(expr w) -> BVApp expr w

XorApp :: !(expr w) -> !(expr w) -> BVApp expr w

NotApp :: !(expr w) -> BVApp expr w

SllApp :: !(expr w) -> !(expr w) -> BVApp expr w

SrlApp :: !(expr w) -> !(expr w) -> BVApp expr w

SraApp :: !(expr w) -> !(expr w) -> BVApp expr w

AddApp :: !(expr w) -> !(expr w) -> BVApp expr w

SubApp :: !(expr w) -> !(expr w) -> BVApp expr w

MulApp :: !(expr w) -> !(expr w) -> BVApp expr w

QuotUApp :: !(expr w) -> !(expr w) -> BVApp expr w

QuotSApp :: !(expr w) -> !(expr w) -> BVApp expr w

RemUApp :: !(expr w) -> !(expr w) -> BVApp expr w

RemSApp :: !(expr w) -> !(expr w) -> BVApp expr w

EqApp :: !(expr w) -> !(expr w) -> BVApp expr 1

LtuApp :: !(expr w) -> !(expr w) -> BVApp expr 1

LtsApp :: !(expr w) -> !(expr w) -> BVApp expr 1

ZExtApp :: NatRepr w' -> !(expr w) -> BVApp expr w'

SExtApp :: NatRepr w' -> !(expr w) -> BVApp expr w'

ExtractApp :: NatRepr w' -> Int -> !(expr w) -> BVApp expr w'

ConcatApp :: !(expr w) -> !(expr w') -> BVApp expr (w + w')

IteApp :: !(expr 1) -> !(expr w) -> !(expr w) -> BVApp expr w

Instances

FunctorFC BVApp

Defined in Data.BitVector.Sized.App

Methods

fmapFC :: (forall (x :: k). f x -> g x) -> forall (x :: l). BVApp f x -> BVApp g x

FoldableFC BVApp

Defined in Data.BitVector.Sized.App

Methods

foldMapFC :: Monoid m => (forall (x :: k). f x -> m) -> forall (x :: l). BVApp f x -> m

foldrFC :: (forall (x :: k). f x -> b -> b) -> forall (x :: l). b -> BVApp f x -> b

foldlFC :: (forall (x :: k). b -> f x -> b) -> forall (x :: l). b -> BVApp f x -> b

foldrFC' :: (forall (x :: k). f x -> b -> b) -> forall (x :: l). b -> BVApp f x -> b

foldlFC' :: (forall (x :: k). b -> f x -> b) -> forall (x :: l). b -> BVApp f x -> b

toListFC :: (forall (x :: k). f x -> a) -> forall (x :: l). BVApp f x -> [a]

TraversableFC BVApp

Defined in Data.BitVector.Sized.App

Methods

traverseFC :: Applicative m => (forall (x :: k). f x -> m (g x)) -> forall (x :: l). BVApp f x -> m (BVApp g x)

TestEquality expr => TestEquality (BVApp expr :: Nat -> *)

Defined in Data.BitVector.Sized.App

Methods

testEquality :: BVApp expr a -> BVApp expr b -> Maybe (a :~: b)

OrdF expr => OrdF (BVApp expr :: Nat -> *)

Defined in Data.BitVector.Sized.App

Methods

compareF :: BVApp expr x -> BVApp expr y -> OrderingF x y

leqF :: BVApp expr x -> BVApp expr y -> Bool

ltF :: BVApp expr x -> BVApp expr y -> Bool

geqF :: BVApp expr x -> BVApp expr y -> Bool

gtF :: BVApp expr x -> BVApp expr y -> Bool

TestEquality expr => Eq (BVApp expr w)

Defined in Data.BitVector.Sized.App

Methods

(==) :: BVApp expr w -> BVApp expr w -> Bool

(/=) :: BVApp expr w -> BVApp expr w -> Bool

OrdF expr => Ord (BVApp expr w)

Defined in Data.BitVector.Sized.App

Methods

compare :: BVApp expr w -> BVApp expr w -> Ordering

(<) :: BVApp expr w -> BVApp expr w -> Bool

(<=) :: BVApp expr w -> BVApp expr w -> Bool

(>) :: BVApp expr w -> BVApp expr w -> Bool

(>=) :: BVApp expr w -> BVApp expr w -> Bool

max :: BVApp expr w -> BVApp expr w -> BVApp expr w

min :: BVApp expr w -> BVApp expr w -> BVApp expr w

evalBVApp

Arguments

:: (forall w'. expr w' -> BitVector w')

expression evaluator

-> BVApp expr w

application

-> BitVector w

Evaluate a BVApp given a pure evaluation function for the parameterized type expr.

evalBVAppM

Arguments

:: Monad m

=> (forall w'. expr w' -> m (BitVector w'))

expression evaluator

-> BVApp expr w

application

-> m (BitVector w)

Evaluate a BVApp given a monadic evaluation function for the parameterized type expr.

Smart constructors

class BVExpr (expr :: Nat -> *) where

Typeclass for embedding BVApp constructors into larger expression types.

Minimal complete definition

appExpr

Methods

appExpr :: BVApp expr w -> expr w

litBV :: BVExpr expr => BitVector w -> expr w

Literal bit vector.

Bitwise

andE :: BVExpr expr => expr w -> expr w -> expr w

Bitwise and.

orE :: BVExpr expr => expr w -> expr w -> expr w

Bitwise or.

xorE :: BVExpr expr => expr w -> expr w -> expr w

Bitwise xor.

notE :: BVExpr expr => expr w -> expr w

Bitwise not.

Arithmetic

addE :: BVExpr expr => expr w -> expr w -> expr w

Add two expressions.

subE :: BVExpr expr => expr w -> expr w -> expr w

Subtract the second expression from the first.

mulE :: BVExpr expr => expr w -> expr w -> expr w

Signed multiply two BitVectors, doubling the width of the result to hold all arithmetic overflow bits.

quotuE :: BVExpr expr => expr w -> expr w -> expr w

Unsigned divide two BitVectors, rounding to zero.

quotsE :: BVExpr expr => expr w -> expr w -> expr w

Signed divide two BitVectors, rounding to zero.

remuE :: BVExpr expr => expr w -> expr w -> expr w

Remainder after unsigned division of two BitVectors, when rounded to zero.

remsE :: BVExpr expr => expr w -> expr w -> expr w

Remainder after signed division of two BitVectors, when rounded to zero.

sllE :: BVExpr expr => expr w -> expr w -> expr w

Left logical shift the first expression by the second.

srlE :: BVExpr expr => expr w -> expr w -> expr w

Left logical shift the first expression by the second.

sraE :: BVExpr expr => expr w -> expr w -> expr w

Left logical shift the first expression by the second.

Comparison

eqE :: BVExpr expr => expr w -> expr w -> expr 1

Test for equality of two expressions.

ltuE :: BVExpr expr => expr w -> expr w -> expr 1

Unsigned less than

ltsE :: BVExpr expr => expr w -> expr w -> expr 1

Signed less than

Width-changing

zextE :: (BVExpr expr, KnownNat w') => expr w -> expr w'

Zero-extension

zextEWithRepr :: BVExpr expr => NatRepr w' -> expr w -> expr w'

Zero-extension with an explicit width argument

sextE :: (BVExpr expr, KnownNat w') => expr w -> expr w'

Sign-extension

sextEWithRepr :: BVExpr expr => NatRepr w' -> expr w -> expr w'

Sign-extension with an explicit width argument

extractE :: (BVExpr expr, KnownNat w') => Int -> expr w -> expr w'

Extract bits

extractEWithRepr :: BVExpr expr => NatRepr w' -> Int -> expr w -> expr w'

Extract bits with an explicit width argument

concatE :: BVExpr expr => expr w -> expr w' -> expr (w + w')

Concatenation

Control

iteE :: BVExpr expr => expr 1 -> expr w -> expr w -> expr w

Conditional branch.