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

Copyright | (c) Galois Inc 2021
License | BSD3
Maintainer | Ryan Scott <rscott@galois.com>
Safe Haskell | Safe-Inferred
Language | Haskell2010

What4.Utils.ResolveBounds.BV

Description

A utility for using an `OnlineSolver` to query if a `SymBV` is concrete or symbolic, and if it is symbolic, what the lower and upper bounds are.

Synopsis

- resolveSymBV :: forall w sym solver scope st fs. (1 <= w, sym ~ ExprBuilder scope st fs, OnlineSolver solver) => sym -> SearchStrategy -> NatRepr w -> SolverProcess scope solver -> SymBV sym w -> IO (ResolvedSymBV w)
- data SearchStrategy
  - = ExponentialSearch
  - | BinarySearch
- data ResolvedSymBV w
  - = BVConcrete (BV w)
  - | BVSymbolic (Domain w)

# Documentation

resolveSymBV Source #

Arguments

:: forall w sym solver scope st fs. (1 <= w, sym ~ ExprBuilder scope st fs, OnlineSolver solver) |
=> sym |
-> SearchStrategy | The strategy to use when searching for lower and upper bounds. For many use cases, `ExponentialSearch` is a reasonable default.
-> NatRepr w | The bitvector width
-> SolverProcess scope solver | The online solver process to use to search for lower and upper bounds.
-> SymBV sym w | The bitvector to resolve.
-> IO (ResolvedSymBV w) |

Use an `OnlineSolver` to attempt to resolve a `SymBV` as concrete. If it cannot, return the lower and upper bounds. This is primarly intended for compound expressions whose bounds cannot trivially be determined by using `signedBVBounds` or `unsignedBVBounds`.

data SearchStrategy Source #

The strategy to use to search for lower and upper bounds in `resolveSymBV`.

Constructors

ExponentialSearch | After making an initial guess for a bound, increase (for upper bounds) or decrease (for lower bounds) the initial guess by an exponentially increasing amount (1, 2, 4, 8, ...) until the bound has been exceeded. At that point, back off from exponential search and use binary search until the bound has been determined. For many use cases, this is a reasonable default.
BinarySearch | Use binary search to found each bound, using `0` as the leftmost bounds of the search and `maxUnsigned` as the rightmost bounds of the search.

#### Instances

Instances details

Pretty SearchStrategy Source # |
Instance details Defined in What4.Utils.ResolveBounds.BV Methods pretty :: SearchStrategy -> Doc ann Source # prettyList :: [SearchStrategy] -> Doc ann Source #

data ResolvedSymBV w Source #

The results of an `OnlineSolver` trying to resolve a `SymBV` as concrete.

Constructors

BVConcrete (BV w) | A concrete bitvector, including its value as a `BV`.
BVSymbolic (Domain w) | A symbolic `SymBV`, including its lower and upper bounds as a `Domain`.

#### Instances

Instances details

Show (ResolvedSymBV w) Source # |
Instance details Defined in What4.Utils.ResolveBounds.BV Methods showsPrec :: Int -> ResolvedSymBV w -> ShowS Source # show :: ResolvedSymBV w -> String Source # showList :: [ResolvedSymBV w] -> ShowS Source #