What4.Utils.AbstractDomains

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.

Documentation

data ValueBound tp

A lower or upper bound on a value.

Constructors

Unbounded

Inclusive !tp

Instances

Monad ValueBound

Defined in What4.Utils.AbstractDomains

Methods

(>>=) :: ValueBound a -> (a -> ValueBound b) -> ValueBound b

(>>) :: ValueBound a -> ValueBound b -> ValueBound b

return :: a -> ValueBound a

Functor ValueBound

Defined in What4.Utils.AbstractDomains

Methods

fmap :: (a -> b) -> ValueBound a -> ValueBound b

(<$) :: a -> ValueBound b -> ValueBound a

Applicative ValueBound

Defined in What4.Utils.AbstractDomains

Methods

pure :: 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)

Defined in What4.Utils.AbstractDomains

Methods

(==) :: ValueBound tp -> ValueBound tp -> Bool

(/=) :: ValueBound tp -> ValueBound tp -> Bool

Ord tp => Ord (ValueBound tp)

Defined in What4.Utils.AbstractDomains

Methods

compare :: 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)

Defined in What4.Utils.AbstractDomains

Methods

showsPrec :: Int -> ValueBound tp -> ShowS

show :: ValueBound tp -> String

showList :: [ValueBound tp] -> ShowS

minValueBound :: Ord tp => ValueBound tp -> ValueBound tp -> ValueBound tp

maxValueBound :: Ord tp => ValueBound tp -> ValueBound tp -> ValueBound tp

ValueRange

data ValueRange tp

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.

unboundedRange :: ValueRange tp

Defines a unbounded value range.

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

rangeLowBound :: ValueRange tp -> ValueBound tp

Return lower bound of range.

rangeHiBound :: ValueRange tp -> ValueBound tp

Return upper bound of range.

singleRange :: tp -> ValueRange tp

Defines a value range containing a single element.

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

Defines a unbounded value range.

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

Define a value range with the given bounds

addRange :: Num tp => ValueRange tp -> ValueRange tp -> ValueRange tp

negateRange :: Num tp => ValueRange tp -> ValueRange tp

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

Multiply a range by a scalar value

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

Multiply two ranges together.

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

Compute the smallest range containing both ranges.

asSingleRange :: ValueRange tp -> Maybe tp

Check if range is just a single element.

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

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

rangeCheckLe :: Ord tp => ValueRange tp -> ValueRange tp -> Maybe Bool

rangeMin :: Ord a => ValueRange a -> ValueRange a -> ValueRange a

rangeMax :: Ord a => ValueRange a -> ValueRange a -> ValueRange a

integer range operations

intAbsRange :: ValueRange Integer -> ValueRange Integer

intDivRange :: ValueRange Integer -> ValueRange Integer -> ValueRange Integer

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.

intModRange :: ValueRange Integer -> ValueRange Integer -> ValueRange Integer

Boolean abstract value

absAnd :: Maybe Bool -> Maybe Bool -> Maybe Bool

absOr :: Maybe Bool -> Maybe Bool -> Maybe Bool

RealAbstractValue

data RealAbstractValue

Constructors

RAV

Fields

• ravRange :: !(ValueRange Rational)
• ravIsInteger :: !(Maybe Bool)

ravUnbounded :: RealAbstractValue

ravSingle :: Rational -> RealAbstractValue

ravConcreteRange

Arguments

:: Rational

Lower bound

-> Rational

Upper bound

-> RealAbstractValue

Range accepting everything between lower and upper bound.

ravJoin :: RealAbstractValue -> RealAbstractValue -> RealAbstractValue

ravAdd :: RealAbstractValue -> RealAbstractValue -> RealAbstractValue

Add two real abstract values.

ravScalarMul :: Rational -> RealAbstractValue -> RealAbstractValue

ravMul :: RealAbstractValue -> RealAbstractValue -> RealAbstractValue

ravCheckEq :: RealAbstractValue -> RealAbstractValue -> Maybe Bool

ravCheckLe :: RealAbstractValue -> RealAbstractValue -> Maybe Bool

StringAbstractValue

newtype StringAbstractValue

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

Constructors

StringAbs

Fields

• _stringAbsLength :: ValueRange Integer

  The length of the string falls in this range

stringAbsJoin :: StringAbstractValue -> StringAbstractValue -> StringAbstractValue

stringAbsTop :: StringAbstractValue

stringAbsSingle :: StringLiteral si -> StringAbstractValue

stringAbsOverlap :: StringAbstractValue -> StringAbstractValue -> Bool

stringAbsLength :: StringAbstractValue -> ValueRange Integer

stringAbsConcat :: StringAbstractValue -> StringAbstractValue -> StringAbstractValue

stringAbsSubstring :: StringAbstractValue -> ValueRange Integer -> ValueRange Integer -> StringAbstractValue

stringAbsContains :: StringAbstractValue -> StringAbstractValue -> Maybe Bool

stringAbsIsPrefixOf :: StringAbstractValue -> StringAbstractValue -> Maybe Bool

stringAbsIsSuffixOf :: StringAbstractValue -> StringAbstractValue -> Maybe Bool

stringAbsIndexOf :: StringAbstractValue -> StringAbstractValue -> ValueRange Integer -> ValueRange Integer

stringAbsEmpty :: StringAbstractValue

Abstractable

avTop :: BaseTypeRepr tp -> AbstractValue tp

Create an abstract value that contains every concrete value.

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

Create an abstract value that contains the given concrete value.

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

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

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

An abstract value represents a disjoint st of values.

Equations

AbstractValue BaseBoolType = Maybe Bool

AbstractValue BaseIntegerType = ValueRange Integer

AbstractValue BaseRealType = RealAbstractValue

AbstractValue (BaseStringType si) = StringAbstractValue

AbstractValue (BaseBVType w) = BVDomain w

AbstractValue (BaseFloatType _) = ()

AbstractValue BaseComplexType = Complex RealAbstractValue

AbstractValue (BaseArrayType idx b) = AbstractValue b

AbstractValue (BaseStructType ctx) = Assignment AbstractValueWrapper ctx

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

Equations

ConcreteValue BaseBoolType = Bool

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

Methods

avJoin :: BaseTypeRepr tp -> AbstractValue tp -> AbstractValue tp -> AbstractValue tp

Take the union of the two abstract values.

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

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

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

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

Abstractable BaseComplexType

Defined in What4.Utils.AbstractDomains

Methods

avJoin :: BaseTypeRepr BaseComplexType -> AbstractValue BaseComplexType -> AbstractValue BaseComplexType -> AbstractValue BaseComplexType

avOverlap :: BaseTypeRepr BaseComplexType -> AbstractValue BaseComplexType -> AbstractValue BaseComplexType -> Bool

avCheckEq :: BaseTypeRepr BaseComplexType -> AbstractValue BaseComplexType -> AbstractValue BaseComplexType -> Maybe Bool

Abstractable BaseRealType

Defined in What4.Utils.AbstractDomains

Methods

avJoin :: BaseTypeRepr BaseRealType -> AbstractValue BaseRealType -> AbstractValue BaseRealType -> AbstractValue BaseRealType

avOverlap :: BaseTypeRepr BaseRealType -> AbstractValue BaseRealType -> AbstractValue BaseRealType -> Bool

avCheckEq :: BaseTypeRepr BaseRealType -> AbstractValue BaseRealType -> AbstractValue BaseRealType -> Maybe Bool

Abstractable BaseIntegerType

Defined in What4.Utils.AbstractDomains

Methods

avJoin :: BaseTypeRepr BaseIntegerType -> AbstractValue BaseIntegerType -> AbstractValue BaseIntegerType -> AbstractValue BaseIntegerType

avOverlap :: BaseTypeRepr BaseIntegerType -> AbstractValue BaseIntegerType -> AbstractValue BaseIntegerType -> Bool

avCheckEq :: BaseTypeRepr BaseIntegerType -> AbstractValue BaseIntegerType -> AbstractValue BaseIntegerType -> Maybe Bool

Abstractable BaseBoolType

Defined in What4.Utils.AbstractDomains

Methods

avJoin :: BaseTypeRepr BaseBoolType -> AbstractValue BaseBoolType -> AbstractValue BaseBoolType -> AbstractValue BaseBoolType

avOverlap :: BaseTypeRepr BaseBoolType -> AbstractValue BaseBoolType -> AbstractValue BaseBoolType -> Bool

avCheckEq :: BaseTypeRepr BaseBoolType -> AbstractValue BaseBoolType -> AbstractValue BaseBoolType -> Maybe Bool

Abstractable (BaseStructType ctx)

Defined in What4.Utils.AbstractDomains

Methods

avJoin :: BaseTypeRepr (BaseStructType ctx) -> AbstractValue (BaseStructType ctx) -> AbstractValue (BaseStructType ctx) -> AbstractValue (BaseStructType ctx)

avOverlap :: BaseTypeRepr (BaseStructType ctx) -> AbstractValue (BaseStructType ctx) -> AbstractValue (BaseStructType ctx) -> Bool

avCheckEq :: BaseTypeRepr (BaseStructType ctx) -> AbstractValue (BaseStructType ctx) -> AbstractValue (BaseStructType ctx) -> Maybe Bool

Abstractable (BaseStringType si)

Defined in What4.Utils.AbstractDomains

Methods

avJoin :: BaseTypeRepr (BaseStringType si) -> AbstractValue (BaseStringType si) -> AbstractValue (BaseStringType si) -> AbstractValue (BaseStringType si)

avOverlap :: BaseTypeRepr (BaseStringType si) -> AbstractValue (BaseStringType si) -> AbstractValue (BaseStringType si) -> Bool

avCheckEq :: BaseTypeRepr (BaseStringType si) -> AbstractValue (BaseStringType si) -> AbstractValue (BaseStringType si) -> Maybe Bool

Abstractable (BaseFloatType fpp)

Defined in What4.Utils.AbstractDomains

Methods

avJoin :: BaseTypeRepr (BaseFloatType fpp) -> AbstractValue (BaseFloatType fpp) -> AbstractValue (BaseFloatType fpp) -> AbstractValue (BaseFloatType fpp)

avOverlap :: BaseTypeRepr (BaseFloatType fpp) -> AbstractValue (BaseFloatType fpp) -> AbstractValue (BaseFloatType fpp) -> Bool

avCheckEq :: BaseTypeRepr (BaseFloatType fpp) -> AbstractValue (BaseFloatType fpp) -> AbstractValue (BaseFloatType fpp) -> Maybe Bool

1 <= w => Abstractable (BaseBVType w)

Defined in What4.Utils.AbstractDomains

Methods

avJoin :: BaseTypeRepr (BaseBVType w) -> AbstractValue (BaseBVType w) -> AbstractValue (BaseBVType w) -> AbstractValue (BaseBVType w)

avOverlap :: BaseTypeRepr (BaseBVType w) -> AbstractValue (BaseBVType w) -> AbstractValue (BaseBVType w) -> Bool

avCheckEq :: BaseTypeRepr (BaseBVType w) -> AbstractValue (BaseBVType w) -> AbstractValue (BaseBVType w) -> Maybe Bool

Abstractable (BaseArrayType idx b)

Defined in What4.Utils.AbstractDomains

Methods

avJoin :: BaseTypeRepr (BaseArrayType idx b) -> AbstractValue (BaseArrayType idx b) -> AbstractValue (BaseArrayType idx b) -> AbstractValue (BaseArrayType idx b)

avOverlap :: BaseTypeRepr (BaseArrayType idx b) -> AbstractValue (BaseArrayType idx b) -> AbstractValue (BaseArrayType idx b) -> Bool

avCheckEq :: BaseTypeRepr (BaseArrayType idx b) -> AbstractValue (BaseArrayType idx b) -> AbstractValue (BaseArrayType idx b) -> Maybe Bool

withAbstractable :: BaseTypeRepr bt -> (Abstractable bt => a) -> a

newtype AbstractValueWrapper tp

Constructors

AbstractValueWrapper

Fields

• unwrapAV :: AbstractValue tp

newtype ConcreteValueWrapper tp

Constructors

ConcreteValueWrapper

Fields

• unwrapCV :: ConcreteValue tp

class HasAbsValue f where

A utility class for values that contain abstract values

Methods

getAbsValue :: f tp -> AbstractValue tp

Instances

HasAbsValue (Expr t)

Defined in What4.Expr.App

Methods

getAbsValue :: forall (tp :: BaseType). Expr t tp -> AbstractValue tp

HasAbsValue (Dummy :: BaseType -> Type)

Defined in What4.Expr.App

Methods

getAbsValue :: forall (tp :: BaseType). Dummy tp -> AbstractValue tp