what4-1.1: Solver-agnostic symbolic values support for issuing queries

What4.Expr.UnaryBV

Contents

Description

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'.

Synopsis

# Documentation

data UnaryBV p (n :: Nat) Source #

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

Instances details
 Eq p => TestEquality (UnaryBV p :: Nat -> Type) Source # Instance detailsDefined in What4.Expr.UnaryBV MethodstestEquality :: forall (a :: k) (b :: k). UnaryBV p a -> UnaryBV p b -> Maybe (a :~: b) # Hashable p => Hashable (UnaryBV p n) Source # Instance detailsDefined in What4.Expr.UnaryBV MethodshashWithSalt :: Int -> UnaryBV p n -> Int #hash :: UnaryBV p n -> Int #

size :: UnaryBV p n -> Int Source #

Returns the number of distinct values that this could be.

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

Create a unary bitvector term from a constant.

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

Create a unary bitvector term from a constant.

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

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

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

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

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) Source #

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

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) Source #

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) Source #

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) Source #

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) Source #

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) Source #

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) Source #

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

Perform a unsigned extension

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

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) Source #

Perform a struncation.