Copyright | (c) Galois Inc 2015-2020 |
---|---|

License | BSD3 |

Maintainer | Joe Hendrix <jhendrix@galois.com> |

Safe Haskell | None |

Language | Haskell2010 |

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

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

Defined in What4.Expr.UnaryBV | |

Hashable p => Hashable (UnaryBV p n) Source # | |

Defined in What4.Expr.UnaryBV |

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.

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.

:: (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 |

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