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

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

What4.Expr.GroundEval

Contents

- Ground evaluation
- Internal operations

Description

Given a collection of assignments to the symbolic values appearing in an expression, this module computes the ground value.

Synopsis

- type family GroundValue (tp :: BaseType) where ...
- newtype GroundValueWrapper tp = GVW {
  - unGVW :: GroundValue tp
  }
- data GroundArray idx b
  - = ArrayMapping (Assignment GroundValueWrapper idx -> IO (GroundValue b))
  - | ArrayConcrete (GroundValue b) (Map (Assignment IndexLit idx) (GroundValue b))
- lookupArray :: Assignment BaseTypeRepr idx -> GroundArray idx b -> Assignment GroundValueWrapper idx -> IO (GroundValue b)
- newtype GroundEvalFn t = GroundEvalFn {
  - groundEval :: forall tp. Expr t tp -> IO (GroundValue tp)
  }
- type ExprRangeBindings t = RealExpr t -> IO (Maybe Rational, Maybe Rational)
- tryEvalGroundExpr :: (forall u. Expr t u -> MaybeT IO (GroundValue u)) -> Expr t tp -> MaybeT IO (GroundValue tp)
- evalGroundExpr :: (forall u. Expr t u -> IO (GroundValue u)) -> Expr t tp -> IO (GroundValue tp)
- evalGroundApp :: forall t tp. (forall u. Expr t u -> MaybeT IO (GroundValue u)) -> App (Expr t) tp -> MaybeT IO (GroundValue tp)
- evalGroundNonceApp :: Monad m => (forall u. Expr t u -> MaybeT m (GroundValue u)) -> NonceApp t (Expr t) tp -> MaybeT m (GroundValue tp)
- defaultValueForType :: BaseTypeRepr tp -> GroundValue tp
- groundEq :: BaseTypeRepr tp -> GroundValue tp -> GroundValue tp -> Maybe Bool

# Ground evaluation

type family GroundValue (tp :: BaseType) where ... Source #

Equations

GroundValue BaseBoolType = Bool |
GroundValue BaseIntegerType = Integer |
GroundValue BaseRealType = Rational |
GroundValue (BaseBVType w) = BV w |
GroundValue (BaseFloatType fpp) = BigFloat |
GroundValue BaseComplexType = Complex Rational |
GroundValue (BaseStringType si) = StringLiteral si |
GroundValue (BaseArrayType idx b) = GroundArray idx b |
GroundValue (BaseStructType ctx) = Assignment GroundValueWrapper ctx |

newtype GroundValueWrapper tp Source #

A newtype wrapper around ground value for use in a cache.

Constructors

GVW |

Fields

- unGVW :: GroundValue tp

data GroundArray idx b Source #

A representation of a ground-value array.

Constructors

ArrayMapping (Assignment GroundValueWrapper idx -> IO (GroundValue b)) | Lookup function for querying by index
ArrayConcrete (GroundValue b) (Map (Assignment IndexLit idx) (GroundValue b)) | Default value and finite map of particular indices

lookupArray :: Assignment BaseTypeRepr idx -> GroundArray idx b -> Assignment GroundValueWrapper idx -> IO (GroundValue b) Source #

Look up an index in an ground array.

newtype GroundEvalFn t Source #

A function that calculates ground values for elements. Clients of solvers should use the `groundEval` function for computing values in models.

Constructors

GroundEvalFn |

Fields

- groundEval :: forall tp. Expr t tp -> IO (GroundValue tp)

type ExprRangeBindings t = RealExpr t -> IO (Maybe Rational, Maybe Rational) Source #

Function that calculates upper and lower bounds for real-valued elements. This type is used for solvers (e.g., dReal) that give only approximate solutions.

# Internal operations

tryEvalGroundExpr :: (forall u. Expr t u -> MaybeT IO (GroundValue u)) -> Expr t tp -> MaybeT IO (GroundValue tp) Source #

Evaluate an element, when given an evaluation function for subelements. Instead of recursing directly, `tryEvalGroundExpr` calls into the given function on sub-elements to allow the caller to cache results if desired.

However, sometimes we are unable to compute expressions outside the solver. In these cases, this function will return `Nothing` in the `MaybeT IO` monad. In these cases, the caller should instead query the solver directly to evaluate the expression, if possible.

evalGroundExpr :: (forall u. Expr t u -> IO (GroundValue u)) -> Expr t tp -> IO (GroundValue tp) Source #

Helper function for evaluating `Expr` expressions in a model.

This function is intended for implementers of symbolic backends.

evalGroundApp :: forall t tp. (forall u. Expr t u -> MaybeT IO (GroundValue u)) -> App (Expr t) tp -> MaybeT IO (GroundValue tp) Source #

Helper function for evaluating `App` expressions.

This function is intended for implementers of symbolic backends.

evalGroundNonceApp :: Monad m => (forall u. Expr t u -> MaybeT m (GroundValue u)) -> NonceApp t (Expr t) tp -> MaybeT m (GroundValue tp) Source #

Helper function for evaluating `NonceApp` expressions.

This function is intended for implementers of symbolic backends.

defaultValueForType :: BaseTypeRepr tp -> GroundValue tp Source #

Construct a default value for a given base type.

groundEq :: BaseTypeRepr tp -> GroundValue tp -> GroundValue tp -> Maybe Bool Source #