What4.Expr.UnaryBV

This module defines a data structure for representing a symbolic bitvector using a form of "unary" representation.

The idea behind this representation is that we associate a predicate to each possible value of the bitvector that is true if the symbolic value is less than or equal to the possible value.

As an example, if we had the unary term x equal to "{ 0 -> false, 1 -> p, 2 -> q, 3 -> t }", then x cannot be '0', has the value '1' if p is true, the value '2' if 'q & not p' is true, and '3' if 'not q' is true. By construction, we should have that 'p => q'.

Documentation

data UnaryBV p (n :: Nat)

A unary bitvector encoding where the map contains predicates such as u^.unaryBVMap^.at i holds iff the value represented by u is less than or equal to i.

The map stored in the representation should always have a single element, and the largest integer stored in the map should be associated with a predicate representing "true". This means that if the map contains only a single binding, then it represents a constant.

Instances

Eq p => TestEquality (UnaryBV p :: Nat -> Type)

Defined in What4.Expr.UnaryBV

Methods

testEquality :: forall (a :: k) (b :: k). UnaryBV p a -> UnaryBV p b -> Maybe (a :~: b)

Hashable p => Hashable (UnaryBV p n)

Defined in What4.Expr.UnaryBV

Methods

hashWithSalt :: Int -> UnaryBV p n -> Int

hash :: UnaryBV p n -> Int

width :: UnaryBV p n -> NatRepr n

size :: UnaryBV p n -> Int

Returns the number of distinct values that this could be.

traversePreds :: Traversal (UnaryBV p n) (UnaryBV q n) p q

constant :: IsExprBuilder sym => sym -> NatRepr n -> Integer -> UnaryBV (Pred sym) n

Create a unary bitvector term from a constant.

asConstant :: IsExpr p => UnaryBV (p BaseBoolType) w -> Maybe Integer

Create a unary bitvector term from a constant.

unsignedEntries :: 1 <= n => UnaryBV p n -> [(Integer, p)]

unsignedRanges :: UnaryBV p n -> [(p, Integer, Integer)]

unsignedRanges v returns a set of predicates and ranges where we know that for each entry (p,l,h) and each value i : l <= i & i <= h: p iff. v <= i

evaluate :: Monad m => (p -> m Bool) -> UnaryBV p n -> m Integer

Evaluate a unary bitvector as an integer given an evaluation function.

sym_evaluate

Arguments

:: (Applicative m, Monad m)

=> (Integer -> m r)

Function for mapping an integer to its bitvector representation.

-> (p -> r -> r -> m r)

Function for performing an ite expression on r.

-> UnaryBV p n

Unary bitvector to evaluate.

-> m r

Evaluate a unary bitvector given an evaluation function.

This function is used to convert a unary bitvector into some other representation such as a binary bitvector or vector of bits.

It is polymorphic over the result type r, and requires functions for manipulating values of type r to construct it.

instantiate :: (Applicative m, Eq q) => (p -> m q) -> UnaryBV p w -> m (UnaryBV q w)

This function instantiates the predicates in a unary predicate with new predicates.

The mapping f should be monotonic, that is for all predicates p and 'q, such that 'p |- q', f should satisfy the constraint that 'f p |- f q'.

domain :: forall p n. 1 <= n => (p -> Maybe Bool) -> UnaryBV p n -> BVDomain n

Return potential values for abstract domain.

Operations

add :: forall sym n. (1 <= n, IsExprBuilder sym) => sym -> UnaryBV (Pred sym) n -> UnaryBV (Pred sym) n -> IO (UnaryBV (Pred sym) n)

Add two bitvectors.

The number of integers in the result will be at most the product of the sizes of the individual bitvectors.

neg :: forall sym n. (1 <= n, IsExprBuilder sym) => sym -> UnaryBV (Pred sym) n -> IO (UnaryBV (Pred sym) n)

Negate a bitvector. The size of the result will be equal to the size of the input.

mux :: forall sym n. (1 <= n, IsExprBuilder sym) => sym -> Pred sym -> UnaryBV (Pred sym) n -> UnaryBV (Pred sym) n -> IO (UnaryBV (Pred sym) n)

mux sym c x y returns value equal to if c then x else y. The number of entries in the return value is at most size x + size y.

eq :: (1 <= n, IsExprBuilder sym) => sym -> UnaryBV (Pred sym) n -> UnaryBV (Pred sym) n -> IO (Pred sym)

Return predicate that holds if bitvectors are equal.

slt :: (1 <= n, IsExprBuilder sym) => sym -> UnaryBV (Pred sym) n -> UnaryBV (Pred sym) n -> IO (Pred sym)

Return predicate that holds if first value is less than other.

ult :: (1 <= n, IsExprBuilder sym) => sym -> UnaryBV (Pred sym) n -> UnaryBV (Pred sym) n -> IO (Pred sym)

Return predicate that holds if first value is less than other.

uext :: (1 <= u, (u + 1) <= r) => UnaryBV p u -> NatRepr r -> UnaryBV p r

Perform a unsigned extension

sext :: (1 <= u, (u + 1) <= r) => UnaryBV p u -> NatRepr r -> UnaryBV p r

Perform a signed extension

trunc :: forall sym u r. (IsExprBuilder sym, 1 <= u, u <= r) => sym -> UnaryBV (Pred sym) r -> NatRepr u -> IO (UnaryBV (Pred sym) u)

Perform a struncation.