| Copyright | (c) Galois Inc 2015-2020 |
|---|---|
| License | BSD3 |
| Maintainer | jhendrix@galois.com |
| Safe Haskell | None |
| Language | Haskell2010 |
What4.Utils.AbstractDomains
Contents
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
- minValueBound :: Ord tp => ValueBound tp -> ValueBound tp -> ValueBound tp
- maxValueBound :: Ord tp => ValueBound tp -> ValueBound tp -> ValueBound tp
- data ValueRange tp
- = SingleRange !tp
- | MultiRange !(ValueBound tp) !(ValueBound 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
- 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 NatValueRange
- natRange :: Natural -> ValueBound Natural -> NatValueRange
- natSingleRange :: Natural -> NatValueRange
- natRangeLow :: NatValueRange -> Natural
- natRangeHigh :: NatValueRange -> ValueBound Natural
- natCheckEq :: NatValueRange -> NatValueRange -> Maybe Bool
- natCheckLe :: NatValueRange -> NatValueRange -> Maybe Bool
- natRangeAdd :: NatValueRange -> NatValueRange -> NatValueRange
- natRangeScalarMul :: Natural -> NatValueRange -> NatValueRange
- natRangeMul :: NatValueRange -> NatValueRange -> NatValueRange
- natRangeJoin :: NatValueRange -> NatValueRange -> NatValueRange
- asSingleNatRange :: NatValueRange -> Maybe Natural
- unboundedNatRange :: NatValueRange
- natRangeToRange :: NatValueRange -> ValueRange Integer
- natRangeDiv :: NatValueRange -> NatValueRange -> NatValueRange
- natRangeMod :: NatValueRange -> NatValueRange -> NatValueRange
- natRangeMin :: NatValueRange -> NatValueRange -> NatValueRange
- natRangeSub :: NatValueRange -> NatValueRange -> NatValueRange
- intRangeToNatRange :: ValueRange Integer -> NatValueRange
- 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 {}
- stringAbsJoin :: StringAbstractValue -> StringAbstractValue -> StringAbstractValue
- stringAbsTop :: StringAbstractValue
- stringAbsSingle :: StringLiteral si -> StringAbstractValue
- stringAbsOverlap :: StringAbstractValue -> StringAbstractValue -> Bool
- stringAbsLength :: StringAbstractValue -> NatValueRange
- stringAbsConcat :: StringAbstractValue -> StringAbstractValue -> StringAbstractValue
- stringAbsSubstring :: StringAbstractValue -> NatValueRange -> NatValueRange -> StringAbstractValue
- stringAbsContains :: StringAbstractValue -> StringAbstractValue -> Maybe Bool
- stringAbsIsPrefixOf :: StringAbstractValue -> StringAbstractValue -> Maybe Bool
- stringAbsIsSuffixOf :: StringAbstractValue -> StringAbstractValue -> Maybe Bool
- stringAbsIndexOf :: StringAbstractValue -> StringAbstractValue -> NatValueRange -> 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.
Instances
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 |
| 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
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 #
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
NatValueRange
data NatValueRange Source #
Constructors
| NatSingleRange !Natural | |
| NatMultiRange !Natural !(ValueBound Natural) |
natRange :: Natural -> ValueBound Natural -> NatValueRange Source #
natRangeLow :: NatValueRange -> Natural Source #
natCheckEq :: NatValueRange -> NatValueRange -> Maybe Bool Source #
Return maybe Boolean if nat is equal, is not equal, or indeterminant.
natCheckLe :: NatValueRange -> NatValueRange -> Maybe Bool Source #
Return maybe Boolean if nat is equal, is not equal, or indeterminant.
natRangeJoin :: NatValueRange -> NatValueRange -> NatValueRange Source #
Compute the smallest range containing both ranges.
intRangeToNatRange :: ValueRange Integer -> NatValueRange Source #
Clamp an integer range to nonnegative values
RealAbstractValue
data RealAbstractValue Source #
Constructors
| RAV | |
Fields
| |
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.
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
| |
stringAbsSubstring :: StringAbstractValue -> NatValueRange -> NatValueRange -> StringAbstractValue Source #
stringAbsIndexOf :: StringAbstractValue -> StringAbstractValue -> NatValueRange -> ValueRange Integer 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
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
withAbstractable :: BaseTypeRepr bt -> (Abstractable bt => a) -> a Source #
newtype AbstractValueWrapper tp Source #
Constructors
| AbstractValueWrapper | |
Fields
| |
newtype ConcreteValueWrapper tp Source #
Constructors
| ConcreteValueWrapper | |
Fields
| |
class HasAbsValue f where Source #
A utility class for values that contain abstract values
Methods
getAbsValue :: f tp -> AbstractValue tp Source #
Instances
| HasAbsValue (Expr t) Source # | |
Defined in What4.Expr.Builder Methods getAbsValue :: Expr t tp -> AbstractValue tp Source # | |