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

Copyright | (c) Galois Inc 2015-2020
License | BSD3
Maintainer | jhendrix@galois.com
Safe Haskell | Safe-Inferred
Language | Haskell2010

What4.Utils.AbstractDomains

Contents

- ValueRange
- integer range operations
- Boolean abstract value
- RealAbstractValue
- StringAbstractValue
- Abstractable

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

- data ValueBound tp
  - = Unbounded
  - | Inclusive !tp
- minValueBound :: Ord tp => ValueBound tp -> ValueBound tp -> ValueBound tp
- maxValueBound :: Ord tp => ValueBound tp -> ValueBound tp -> ValueBound tp
- data ValueRange tp
  - = SingleRange !tp
  - | UnboundedRange
  - | MinRange !tp
  - | MaxRange !tp
  - | IntervalRange !tp !tp
- pattern MultiRange :: ValueBound tp -> ValueBound tp -> ValueRange tp
- unboundedRange :: ValueRange tp
- mapRange :: (a -> b) -> ValueRange a -> ValueRange b
- rangeLowBound :: ValueRange tp -> ValueBound tp
- rangeHiBound :: ValueRange tp -> ValueBound tp
- singleRange :: tp -> ValueRange tp
- concreteRange :: Eq tp => tp -> tp -> ValueRange tp
- valueRange :: Eq tp => ValueBound tp -> ValueBound tp -> ValueRange tp
- 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
- mulRange :: (Ord tp, Num tp) => ValueRange tp -> ValueRange tp -> ValueRange tp
- joinRange :: Ord tp => ValueRange tp -> ValueRange tp -> ValueRange tp
- asSingleRange :: ValueRange tp -> Maybe tp
- rangeCheckEq :: Ord tp => ValueRange tp -> ValueRange tp -> Maybe Bool
- 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
- intAbsRange :: ValueRange Integer -> ValueRange Integer
- intDivRange :: ValueRange Integer -> ValueRange Integer -> ValueRange Integer
- intModRange :: ValueRange Integer -> ValueRange Integer -> ValueRange Integer
- absAnd :: Maybe Bool -> Maybe Bool -> Maybe Bool
- absOr :: Maybe Bool -> Maybe Bool -> Maybe Bool
- data RealAbstractValue = RAV {
  - ravRange :: !(ValueRange Rational)
  - ravIsInteger :: !(Maybe Bool)
  }
- ravUnbounded :: RealAbstractValue
- ravSingle :: Rational -> RealAbstractValue
- ravConcreteRange :: Rational -> Rational -> RealAbstractValue
- ravJoin :: RealAbstractValue -> RealAbstractValue -> RealAbstractValue
- ravAdd :: RealAbstractValue -> RealAbstractValue -> RealAbstractValue
- ravScalarMul :: Rational -> RealAbstractValue -> RealAbstractValue
- ravMul :: RealAbstractValue -> RealAbstractValue -> RealAbstractValue
- ravCheckEq :: RealAbstractValue -> RealAbstractValue -> Maybe Bool
- ravCheckLe :: RealAbstractValue -> RealAbstractValue -> Maybe Bool
- newtype StringAbstractValue = StringAbs {
  - _stringAbsLength :: ValueRange Integer
  }
- 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
- avTop :: BaseTypeRepr tp -> AbstractValue tp
- avSingle :: BaseTypeRepr tp -> ConcreteValue tp -> AbstractValue tp
- avContains :: BaseTypeRepr tp -> ConcreteValue tp -> AbstractValue tp -> Bool
- type family AbstractValue (tp :: BaseType) :: Type where ...
- type family ConcreteValue (tp :: BaseType) :: Type where ...
- class Abstractable (tp :: BaseType) where
  - avJoin :: BaseTypeRepr tp -> AbstractValue tp -> AbstractValue tp -> AbstractValue tp
  - avOverlap :: BaseTypeRepr tp -> AbstractValue tp -> AbstractValue tp -> Bool
  - avCheckEq :: BaseTypeRepr tp -> AbstractValue tp -> AbstractValue tp -> Maybe Bool
- withAbstractable :: BaseTypeRepr bt -> (Abstractable bt => a) -> a
- newtype AbstractValueWrapper tp = AbstractValueWrapper {
  - unwrapAV :: AbstractValue tp
  }
- newtype ConcreteValueWrapper tp = ConcreteValueWrapper {
  - unwrapCV :: ConcreteValue tp
  }
- class HasAbsValue f where
  - getAbsValue :: f tp -> AbstractValue tp

# Documentation

data ValueBound tp Source #

A lower or upper bound on a value.

Constructors

Unbounded |
Inclusive !tp |

#### Instances

Instances details

Applicative ValueBound Source # |
Instance details Defined in What4.Utils.AbstractDomains Methods pure :: a -> ValueBound a Source # (<*>) :: ValueBound (a -> b) -> ValueBound a -> ValueBound b Source # liftA2 :: (a -> b -> c) -> ValueBound a -> ValueBound b -> ValueBound c Source # (*>) :: ValueBound a -> ValueBound b -> ValueBound b Source # (<*) :: ValueBound a -> ValueBound b -> ValueBound a Source #
Functor ValueBound Source # |
Instance details Defined in What4.Utils.AbstractDomains Methods fmap :: (a -> b) -> ValueBound a -> ValueBound b Source # (<$) :: a -> ValueBound b -> ValueBound a Source #
Monad ValueBound Source # |
Instance details Defined in What4.Utils.AbstractDomains Methods (>>=) :: ValueBound a -> (a -> ValueBound b) -> ValueBound b Source # (>>) :: ValueBound a -> ValueBound b -> ValueBound b Source # return :: a -> ValueBound a Source #
Show tp => Show (ValueBound tp) Source # |
Instance details Defined in What4.Utils.AbstractDomains Methods showsPrec :: Int -> ValueBound tp -> ShowS Source # show :: ValueBound tp -> String Source # showList :: [ValueBound tp] -> ShowS Source #
Eq tp => Eq (ValueBound tp) Source # |
Instance details Defined in What4.Utils.AbstractDomains Methods (==) :: ValueBound tp -> ValueBound tp -> Bool Source # (/=) :: ValueBound tp -> ValueBound tp -> Bool Source #
Ord tp => Ord (ValueBound tp) Source # |

Instance details

Defined in What4.Utils.AbstractDomains

Methods

compare :: ValueBound tp -> ValueBound tp -> Ordering Source #

(<) :: ValueBound tp -> ValueBound tp -> Bool Source #

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

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

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

max :: ValueBound tp -> ValueBound tp -> ValueBound tp Source #

min :: ValueBound tp -> ValueBound tp -> ValueBound tp Source #

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

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

# 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
UnboundedRange | The number is unconstrained.
MinRange !tp | The number is greater than or equal to the given lower bound.
MaxRange !tp | The number is less than or equal to the given upper bound.
IntervalRange !tp !tp | The number is between the given lower and upper bounds.

pattern MultiRange :: ValueBound tp -> ValueBound tp -> ValueRange tp Source #

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 #

Map a monotonic function over a range.

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

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

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

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.

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

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

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

# integer range operations

intAbsRange :: ValueRange Integer -> ValueRange Integer Source #

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.

intModRange :: ValueRange Integer -> ValueRange Integer -> ValueRange Integer Source #

# Boolean abstract value

absAnd :: Maybe Bool -> Maybe Bool -> Maybe Bool Source #

absOr :: Maybe Bool -> Maybe Bool -> Maybe Bool Source #

# RealAbstractValue

data RealAbstractValue Source #

Constructors

RAV |

Fields

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

ravUnbounded :: RealAbstractValue Source #

ravSingle :: Rational -> RealAbstractValue Source #

ravConcreteRange Source #

Arguments

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

Range accepting everything between lower and upper bound.

ravJoin :: RealAbstractValue -> RealAbstractValue -> RealAbstractValue Source #

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

Add two real abstract values.

ravScalarMul :: Rational -> RealAbstractValue -> RealAbstractValue Source #

ravMul :: RealAbstractValue -> RealAbstractValue -> RealAbstractValue Source #

ravCheckEq :: RealAbstractValue -> RealAbstractValue -> Maybe Bool Source #

ravCheckLe :: RealAbstractValue -> RealAbstractValue -> Maybe Bool Source #

# StringAbstractValue

newtype StringAbstractValue Source #

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

stringAbsTop :: StringAbstractValue Source #

stringAbsSingle :: StringLiteral si -> StringAbstractValue Source #

stringAbsOverlap :: StringAbstractValue -> StringAbstractValue -> Bool Source #

stringAbsLength :: StringAbstractValue -> ValueRange Integer Source #

stringAbsConcat :: StringAbstractValue -> StringAbstractValue -> StringAbstractValue Source #

stringAbsSubstring :: StringAbstractValue -> ValueRange Integer -> ValueRange Integer -> StringAbstractValue Source #

stringAbsContains :: StringAbstractValue -> StringAbstractValue -> Maybe Bool Source #

stringAbsIsPrefixOf :: StringAbstractValue -> StringAbstractValue -> Maybe Bool Source #

stringAbsIsSuffixOf :: StringAbstractValue -> StringAbstractValue -> Maybe Bool Source #

stringAbsIndexOf :: StringAbstractValue -> StringAbstractValue -> ValueRange Integer -> ValueRange Integer Source #

stringAbsEmpty :: StringAbstractValue Source #

# 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.

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

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 ... Source #

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 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 BaseBoolType Source # |

Instance details

Defined in What4.Utils.AbstractDomains

Methods

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

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

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

Abstractable BaseComplexType Source # |

Instance details

Defined in What4.Utils.AbstractDomains

Methods

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

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

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

Abstractable BaseIntegerType Source # |

Instance details

Defined in What4.Utils.AbstractDomains

Methods

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

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

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

Abstractable BaseRealType Source # |

Instance details

Defined in What4.Utils.AbstractDomains

Methods

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

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

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

1 <= w => Abstractable (BaseBVType w) Source # |

Instance details

Defined in What4.Utils.AbstractDomains

Methods

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

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

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

Abstractable (BaseFloatType fpp) Source # |

Instance details

Defined in What4.Utils.AbstractDomains

Methods

avJoin :: 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 #

Abstractable (BaseStringType si) Source # |

Instance details

Defined in What4.Utils.AbstractDomains

Methods

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

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

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

Abstractable (BaseStructType ctx) Source # |

Instance details

Defined in What4.Utils.AbstractDomains

Methods

avJoin :: 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 #

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

Abstractable (BaseArrayType idx b) Source # |

Instance details

Defined in What4.Utils.AbstractDomains

Methods

avJoin :: 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 #

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

newtype AbstractValueWrapper tp Source #

Constructors

AbstractValueWrapper |

Fields

- unwrapAV :: AbstractValue tp

newtype ConcreteValueWrapper tp Source #

Constructors

ConcreteValueWrapper |

Fields

- unwrapCV :: ConcreteValue tp

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 (Dummy :: BaseType -> Type) Source # |
Instance details Defined in What4.Expr.App Methods getAbsValue :: forall (tp :: BaseType). Dummy tp -> AbstractValue tp Source #
HasAbsValue (Expr t) Source # |
Instance details Defined in What4.Expr.App Methods getAbsValue :: forall (tp :: BaseType). Expr t tp -> AbstractValue tp Source #