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

Copyright | (c) Galois Inc 2015-2020
License | BSD3
Maintainer | Joe Hendrix <jhendrix@galois.com>
Safe Haskell | Safe-Inferred
Language | Haskell2010

What4.Expr.UnaryBV

Contents

- Operations

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

- data UnaryBV p (n :: Nat)
- width :: UnaryBV p n -> NatRepr n
- size :: UnaryBV p n -> Int
- traversePreds :: Traversal (UnaryBV p n) (UnaryBV q n) p q
- constant :: IsExprBuilder sym => sym -> NatRepr n -> Integer -> UnaryBV (Pred sym) n
- asConstant :: IsExpr p => UnaryBV (p BaseBoolType) w -> Maybe Integer
- unsignedEntries :: 1 <= n => UnaryBV p n -> [(Integer, p)]
- unsignedRanges :: UnaryBV p n -> [(p, Integer, Integer)]
- evaluate :: Monad m => (p -> m Bool) -> UnaryBV p n -> m Integer
- sym_evaluate :: (Applicative m, Monad m) => (Integer -> m r) -> (p -> r -> r -> m r) -> UnaryBV p n -> m r
- instantiate :: (Applicative m, Eq q) => (p -> m q) -> UnaryBV p w -> m (UnaryBV q w)
- domain :: forall p n. 1 <= n => (p -> Maybe Bool) -> UnaryBV p n -> BVDomain n
- add :: forall sym n. (1 <= n, IsExprBuilder sym) => sym -> UnaryBV (Pred sym) n -> UnaryBV (Pred sym) n -> IO (UnaryBV (Pred sym) n)
- neg :: forall sym n. (1 <= n, IsExprBuilder sym) => sym -> UnaryBV (Pred sym) n -> IO (UnaryBV (Pred sym) n)
- mux :: forall sym n. (1 <= n, IsExprBuilder sym) => sym -> Pred sym -> UnaryBV (Pred sym) n -> UnaryBV (Pred sym) n -> IO (UnaryBV (Pred sym) n)
- eq :: (1 <= n, IsExprBuilder sym) => sym -> UnaryBV (Pred sym) n -> UnaryBV (Pred sym) n -> IO (Pred sym)
- slt :: (1 <= n, IsExprBuilder sym) => sym -> UnaryBV (Pred sym) n -> UnaryBV (Pred sym) n -> IO (Pred sym)
- ult :: (1 <= n, IsExprBuilder sym) => sym -> UnaryBV (Pred sym) n -> UnaryBV (Pred sym) n -> IO (Pred sym)
- uext :: (1 <= u, (u + 1) <= r) => UnaryBV p u -> NatRepr r -> UnaryBV p r
- sext :: (1 <= u, (u + 1) <= r) => UnaryBV p u -> NatRepr r -> UnaryBV p r
- trunc :: forall sym u r. (IsExprBuilder sym, 1 <= u, u <= r) => sym -> UnaryBV (Pred sym) r -> NatRepr u -> IO (UnaryBV (Pred sym) u)

# 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 details Defined in What4.Expr.UnaryBV Methods testEquality :: forall (a :: k) (b :: k). UnaryBV p a -> UnaryBV p b -> Maybe (a :~: b) Source #
Eq p => Eq (UnaryBV p n) Source # |
Instance details Defined in What4.Expr.UnaryBV Methods (==) :: UnaryBV p n -> UnaryBV p n -> Bool Source # (/=) :: UnaryBV p n -> UnaryBV p n -> Bool Source #
Hashable p => Hashable (UnaryBV p n) Source # |
Instance details Defined in What4.Expr.UnaryBV Methods hashWithSalt :: Int -> UnaryBV p n -> Int Source # hash :: UnaryBV p n -> Int Source #

width :: UnaryBV p n -> NatRepr n Source #

size :: UnaryBV p n -> Int Source #

Returns the number of distinct values that this could be.

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

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.

sym_evaluate Source #

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 #

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