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

What4.Utils.AbstractDomains

Description

This module declares a set of abstract domains used by the solver. These are mostly interval domains on numeric types.

Since these abstract domains are baked directly into the term representation, we want to get as much bang-for-buck as possible. Thus, we prioritize compact representations and simple algorithms over precision.

Synopsis

# Documentation

data ValueBound tp Source #

A lower or upper bound on a value.

Constructors

 Unbounded Inclusive !tp
Instances
 Source # Instance detailsDefined in What4.Utils.AbstractDomains Methods(>>=) :: ValueBound a -> (a -> ValueBound b) -> ValueBound b #(>>) :: ValueBound a -> ValueBound b -> ValueBound b #return :: a -> ValueBound a # Source # Instance detailsDefined in What4.Utils.AbstractDomains Methodsfmap :: (a -> b) -> ValueBound a -> ValueBound b #(<\$) :: a -> ValueBound b -> ValueBound a # Source # Instance detailsDefined in What4.Utils.AbstractDomains Methodspure :: a -> ValueBound a #(<*>) :: ValueBound (a -> b) -> ValueBound a -> ValueBound b #liftA2 :: (a -> b -> c) -> ValueBound a -> ValueBound b -> ValueBound c #(*>) :: ValueBound a -> ValueBound b -> ValueBound b #(<*) :: ValueBound a -> ValueBound b -> ValueBound a # Eq tp => Eq (ValueBound tp) Source # Instance detailsDefined in What4.Utils.AbstractDomains Methods(==) :: ValueBound tp -> ValueBound tp -> Bool #(/=) :: ValueBound tp -> ValueBound tp -> Bool # Ord tp => Ord (ValueBound tp) Source # Instance detailsDefined in What4.Utils.AbstractDomains Methodscompare :: ValueBound tp -> ValueBound tp -> Ordering #(<) :: ValueBound tp -> ValueBound tp -> Bool #(<=) :: ValueBound tp -> ValueBound tp -> Bool #(>) :: ValueBound tp -> ValueBound tp -> Bool #(>=) :: ValueBound tp -> ValueBound tp -> Bool #max :: ValueBound tp -> ValueBound tp -> ValueBound tp #min :: ValueBound tp -> ValueBound tp -> ValueBound tp # Show tp => Show (ValueBound tp) Source # Instance detailsDefined in What4.Utils.AbstractDomains MethodsshowsPrec :: Int -> ValueBound tp -> ShowS #show :: ValueBound tp -> String #showList :: [ValueBound tp] -> ShowS #

# ValueRange

data ValueRange tp Source #

Describes a range of values in a totally ordered set.

Constructors

 SingleRange !tp Indicates that range denotes a single value MultiRange !(ValueBound tp) !(ValueBound tp) Indicates that the number is somewhere between the given upper and lower bound.

Defines a unbounded value range.

mapRange :: (a -> b) -> ValueRange a -> ValueRange b Source #

Return lower bound of range.

Return upper bound of range.

singleRange :: tp -> ValueRange tp Source #

Defines a value range containing a single element.

concreteRange :: Eq tp => tp -> tp -> ValueRange tp Source #

Defines a unbounded value range.

valueRange :: Eq tp => ValueBound tp -> ValueBound tp -> ValueRange tp Source #

Define a value range with the given bounds

rangeScalarMul :: (Ord tp, Num tp) => tp -> ValueRange tp -> ValueRange tp Source #

Multiply a range by a scalar value

mulRange :: (Ord tp, Num tp) => ValueRange tp -> ValueRange tp -> ValueRange tp Source #

Multiply two ranges together.

joinRange :: Ord tp => ValueRange tp -> ValueRange tp -> ValueRange tp Source #

Compute the smallest range containing both ranges.

asSingleRange :: ValueRange tp -> Maybe tp Source #

Check if range is just a single element.

rangeCheckEq :: Ord tp => ValueRange tp -> ValueRange tp -> Maybe Bool Source #

Return maybe Boolean if range is equal, is not equal, or indeterminant.

# integer range operations

Compute an abstract range for integer division. We are using the SMTLib division operation, where the division is floor when the divisor is positive and ceiling when the divisor is negative. We compute the ranges assuming that division by 0 doesn't happen, and we are allowed to return nonsense ranges for these cases.

# NatValueRange

Constructors

 NatSingleRange !Natural NatMultiRange !Natural !(ValueBound Natural)

Return maybe Boolean if nat is equal, is not equal, or indeterminant.

Return maybe Boolean if nat is equal, is not equal, or indeterminant.

Compute the smallest range containing both ranges.

Clamp an integer range to nonnegative values

# RealAbstractValue

Constructors

 RAV FieldsravRange :: !(ValueRange Rational) ravIsInteger :: !(Maybe Bool)

Arguments

 :: Rational Lower bound -> Rational Upper bound -> RealAbstractValue

Range accepting everything between lower and upper bound.

# StringAbstractValue

newtype StringAbstractValue Source #

The string abstract domain tracks an interval range for the length of the string.

Constructors

 StringAbs Fields_stringAbsLength :: NatValueRangeThe length of the string falls in this range

# Abstractable

Create an abstract value that contains every concrete value.

avSingle :: BaseTypeRepr tp -> ConcreteValue tp -> AbstractValue tp Source #

Create an abstract value that contains the given concrete value.

avContains :: BaseTypeRepr tp -> ConcreteValue tp -> AbstractValue tp -> Bool Source #

Returns true if the concrete value is a member of the set represented by the abstract value.

type family AbstractValue (tp :: BaseType) :: Type where ... Source #

An abstract value represents a disjoint st of values.

type family ConcreteValue (tp :: BaseType) :: Type where ... Source #

Equations

 ConcreteValue BaseBoolType = Bool ConcreteValue BaseNatType = Natural ConcreteValue BaseIntegerType = Integer ConcreteValue BaseRealType = Rational ConcreteValue (BaseStringType si) = StringLiteral si ConcreteValue (BaseBVType w) = Integer ConcreteValue (BaseFloatType _) = () ConcreteValue BaseComplexType = Complex Rational ConcreteValue (BaseArrayType idx b) = () ConcreteValue (BaseStructType ctx) = Assignment ConcreteValueWrapper ctx

class Abstractable (tp :: BaseType) where Source #

Methods

avJoin :: BaseTypeRepr tp -> AbstractValue tp -> AbstractValue tp -> AbstractValue tp Source #

Take the union of the two abstract values.

avOverlap :: BaseTypeRepr tp -> AbstractValue tp -> AbstractValue tp -> Bool Source #

Returns true if the abstract values could contain a common concrete value.

avCheckEq :: BaseTypeRepr tp -> AbstractValue tp -> AbstractValue tp -> Maybe Bool Source #

Check equality on two abstract values. Return true or false if we can definitively determine the equality of the two elements, and nothing otherwise.

Instances
 Source # Instance detailsDefined in What4.Utils.AbstractDomains Source # Instance detailsDefined in What4.Utils.AbstractDomains Source # Instance detailsDefined in What4.Utils.AbstractDomains Source # Instance detailsDefined in What4.Utils.AbstractDomains Source # Instance detailsDefined in What4.Utils.AbstractDomains Source # Instance detailsDefined in What4.Utils.AbstractDomains MethodsavJoin :: BaseTypeRepr (BaseStructType ctx) -> AbstractValue (BaseStructType ctx) -> AbstractValue (BaseStructType ctx) -> AbstractValue (BaseStructType ctx) Source #avOverlap :: BaseTypeRepr (BaseStructType ctx) -> AbstractValue (BaseStructType ctx) -> AbstractValue (BaseStructType ctx) -> Bool Source # Source # Instance detailsDefined in What4.Utils.AbstractDomains Methods Source # Instance detailsDefined in What4.Utils.AbstractDomains MethodsavJoin :: BaseTypeRepr (BaseFloatType fpp) -> AbstractValue (BaseFloatType fpp) -> AbstractValue (BaseFloatType fpp) -> AbstractValue (BaseFloatType fpp) Source #avOverlap :: BaseTypeRepr (BaseFloatType fpp) -> AbstractValue (BaseFloatType fpp) -> AbstractValue (BaseFloatType fpp) -> Bool Source #avCheckEq :: BaseTypeRepr (BaseFloatType fpp) -> AbstractValue (BaseFloatType fpp) -> AbstractValue (BaseFloatType fpp) -> Maybe Bool Source # 1 <= w => Abstractable (BaseBVType w) Source # Instance detailsDefined in What4.Utils.AbstractDomains Methods Abstractable (BaseArrayType idx b) Source # Instance detailsDefined in What4.Utils.AbstractDomains MethodsavJoin :: BaseTypeRepr (BaseArrayType idx b) -> AbstractValue (BaseArrayType idx b) -> AbstractValue (BaseArrayType idx b) -> AbstractValue (BaseArrayType idx b) Source #avOverlap :: BaseTypeRepr (BaseArrayType idx b) -> AbstractValue (BaseArrayType idx b) -> AbstractValue (BaseArrayType idx b) -> Bool Source #avCheckEq :: BaseTypeRepr (BaseArrayType idx b) -> AbstractValue (BaseArrayType idx b) -> AbstractValue (BaseArrayType idx b) -> Maybe Bool Source #

newtype AbstractValueWrapper tp Source #

Constructors

 AbstractValueWrapper FieldsunwrapAV :: AbstractValue tp

newtype ConcreteValueWrapper tp Source #

Constructors

 ConcreteValueWrapper FieldsunwrapCV :: ConcreteValue tp

class HasAbsValue f where Source #

A utility class for values that contain abstract values

Methods

getAbsValue :: f tp -> AbstractValue tp Source #

Instances
 Source # Instance detailsDefined in What4.Expr.Builder MethodsgetAbsValue :: Expr t tp -> AbstractValue tp Source #