what4-1.1: Solver-agnostic symbolic values support for issuing queries
Copyright(c) Galois Inc 2015-2020
LicenseBSD3
Maintainerjhendrix@galois.com
Safe HaskellNone
LanguageHaskell2010

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

Instances details
Monad ValueBound Source # 
Instance details

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 Source # 
Instance details

Defined in What4.Utils.AbstractDomains

Methods

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

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

Applicative ValueBound Source # 
Instance details

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) Source # 
Instance details

Defined in What4.Utils.AbstractDomains

Methods

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

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

Ord tp => Ord (ValueBound tp) Source # 
Instance details

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) Source # 
Instance details

Defined in What4.Utils.AbstractDomains

Methods

showsPrec :: 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.

unboundedRange :: ValueRange tp Source #

Defines a unbounded value range.

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

rangeLowBound :: ValueRange tp -> ValueBound tp Source #

Return lower bound of range.

rangeHiBound :: ValueRange tp -> ValueBound tp Source #

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

intDivRange :: ValueRange Integer -> ValueRange Integer -> ValueRange Integer Source #

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.

Boolean abstract value

RealAbstractValue

ravConcreteRange Source #

Arguments

:: Rational

Lower bound

-> Rational

Upper bound

-> RealAbstractValue 

Range accepting everything between lower and upper bound.

ravAdd :: RealAbstractValue -> RealAbstractValue -> RealAbstractValue Source #

Add two real abstract values.

StringAbstractValue

newtype StringAbstractValue Source #

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

Constructors

StringAbs 

Fields

Abstractable

avTop :: BaseTypeRepr tp -> AbstractValue tp Source #

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.

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

Instances details
Abstractable BaseComplexType Source # 
Instance details

Defined in What4.Utils.AbstractDomains

Abstractable BaseRealType Source # 
Instance details

Defined in What4.Utils.AbstractDomains

Abstractable BaseIntegerType Source # 
Instance details

Defined in What4.Utils.AbstractDomains

Abstractable BaseBoolType Source # 
Instance details

Defined in What4.Utils.AbstractDomains

Abstractable (BaseStructType ctx) Source # 
Instance details

Defined in What4.Utils.AbstractDomains

Abstractable (BaseStringType si) Source # 
Instance details

Defined in What4.Utils.AbstractDomains

Abstractable (BaseFloatType fpp) Source # 
Instance details

Defined in What4.Utils.AbstractDomains

1 <= w => Abstractable (BaseBVType w) Source # 
Instance details

Defined in What4.Utils.AbstractDomains

Abstractable (BaseArrayType idx b) Source # 
Instance details

Defined in What4.Utils.AbstractDomains

class HasAbsValue f where Source #

A utility class for values that contain abstract values

Methods

getAbsValue :: f tp -> AbstractValue tp Source #

Instances

Instances details
HasAbsValue (Expr t) Source # 
Instance details

Defined in What4.Expr.App

Methods

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

HasAbsValue (Dummy :: BaseType -> Type) Source # 
Instance details

Defined in What4.Expr.App

Methods

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