{-|
Module      : What4.Utils.AbstractDomains
Description : Abstract domains for term simplification
Copyright   : (c) Galois Inc, 2015-2020
License     : BSD3
Maintainer  : jhendrix@galois.com

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

{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}

module What4.Utils.AbstractDomains
  ( ValueBound(..)
  , minValueBound
  , maxValueBound
    -- * ValueRange
  , ValueRange(..)
  , pattern MultiRange
  , unboundedRange
  , mapRange
  , rangeLowBound
  , rangeHiBound
  , singleRange
  , concreteRange
  , valueRange
  , addRange
  , negateRange
  , rangeScalarMul
  , mulRange
  , joinRange
  , asSingleRange
  , rangeCheckEq
  , rangeCheckLe
  , rangeMin
  , rangeMax
    -- * integer range operations
  , intAbsRange
  , intDivRange
  , intModRange
    -- * Boolean abstract value
  , absAnd
  , absOr

    -- * RealAbstractValue
  , RealAbstractValue(..)
  , ravUnbounded
  , ravSingle
  , ravConcreteRange
  , ravJoin
  , ravAdd
  , ravScalarMul
  , ravMul
  , ravCheckEq
  , ravCheckLe
    -- * StringAbstractValue
  , StringAbstractValue(..)
  , stringAbsJoin
  , stringAbsTop
  , stringAbsSingle
  , stringAbsOverlap
  , stringAbsLength
  , stringAbsConcat
  , stringAbsSubstring
  , stringAbsContains
  , stringAbsIsPrefixOf
  , stringAbsIsSuffixOf
  , stringAbsIndexOf
  , stringAbsEmpty

    -- * Abstractable
  , avTop
  , avSingle
  , avContains
  , AbstractValue
  , ConcreteValue
  , Abstractable(..)
  , withAbstractable
  , AbstractValueWrapper(..)
  , ConcreteValueWrapper(..)
  , HasAbsValue(..)
  ) where

import           Control.Exception (assert)
import           Data.Kind
import           Data.Parameterized.Context as Ctx
import           Data.Parameterized.NatRepr
import           Data.Parameterized.TraversableFC
import           Data.Ratio (denominator)

import           What4.BaseTypes
import           What4.Utils.BVDomain (BVDomain)
import qualified What4.Utils.BVDomain as BVD
import           What4.Utils.Complex
import           What4.Utils.StringLiteral

ctxZipWith3 :: (forall (x::k) . a x -> b x -> c x -> d x)
            -> Ctx.Assignment a (ctx::Ctx.Ctx k)
            -> Ctx.Assignment b ctx
            -> Ctx.Assignment c ctx
            -> Ctx.Assignment d ctx
ctxZipWith3 :: forall k (a :: k -> Type) (b :: k -> Type) (c :: k -> Type)
       (d :: k -> Type) (ctx :: Ctx k).
(forall (x :: k). a x -> b x -> c x -> d x)
-> Assignment a ctx
-> Assignment b ctx
-> Assignment c ctx
-> Assignment d ctx
ctxZipWith3 forall (x :: k). a x -> b x -> c x -> d x
f Assignment a ctx
a Assignment b ctx
b Assignment c ctx
c =
  forall {k} (ctx :: Ctx k) (f :: k -> Type).
Size ctx
-> (forall (tp :: k). Index ctx tp -> f tp) -> Assignment f ctx
Ctx.generate (forall {k} (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
Ctx.size Assignment a ctx
a) forall a b. (a -> b) -> a -> b
$ \Index ctx tp
i ->
    forall (x :: k). a x -> b x -> c x -> d x
f (Assignment a ctx
a forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index ctx tp
i) (Assignment b ctx
b forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index ctx tp
i) (Assignment c ctx
c forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index ctx tp
i)


------------------------------------------------------------------------
-- ValueBound

-- | A lower or upper bound on a value.
data ValueBound tp
   = Unbounded
   | Inclusive !tp
  deriving (forall a b. a -> ValueBound b -> ValueBound a
forall a b. (a -> b) -> ValueBound a -> ValueBound b
forall (f :: Type -> Type).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> ValueBound b -> ValueBound a
$c<$ :: forall a b. a -> ValueBound b -> ValueBound a
fmap :: forall a b. (a -> b) -> ValueBound a -> ValueBound b
$cfmap :: forall a b. (a -> b) -> ValueBound a -> ValueBound b
Functor, Int -> ValueBound tp -> ShowS
forall tp. Show tp => Int -> ValueBound tp -> ShowS
forall tp. Show tp => [ValueBound tp] -> ShowS
forall tp. Show tp => ValueBound tp -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ValueBound tp] -> ShowS
$cshowList :: forall tp. Show tp => [ValueBound tp] -> ShowS
show :: ValueBound tp -> String
$cshow :: forall tp. Show tp => ValueBound tp -> String
showsPrec :: Int -> ValueBound tp -> ShowS
$cshowsPrec :: forall tp. Show tp => Int -> ValueBound tp -> ShowS
Show, ValueBound tp -> ValueBound tp -> Bool
forall tp. Eq tp => ValueBound tp -> ValueBound tp -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ValueBound tp -> ValueBound tp -> Bool
$c/= :: forall tp. Eq tp => ValueBound tp -> ValueBound tp -> Bool
== :: ValueBound tp -> ValueBound tp -> Bool
$c== :: forall tp. Eq tp => ValueBound tp -> ValueBound tp -> Bool
Eq, ValueBound tp -> ValueBound tp -> Bool
ValueBound tp -> ValueBound tp -> Ordering
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {tp}. Ord tp => Eq (ValueBound tp)
forall tp. Ord tp => ValueBound tp -> ValueBound tp -> Bool
forall tp. Ord tp => ValueBound tp -> ValueBound tp -> Ordering
forall tp.
Ord tp =>
ValueBound tp -> ValueBound tp -> ValueBound tp
min :: ValueBound tp -> ValueBound tp -> ValueBound tp
$cmin :: forall tp.
Ord tp =>
ValueBound tp -> ValueBound tp -> ValueBound tp
max :: ValueBound tp -> ValueBound tp -> ValueBound tp
$cmax :: forall tp.
Ord tp =>
ValueBound tp -> ValueBound tp -> ValueBound tp
>= :: ValueBound tp -> ValueBound tp -> Bool
$c>= :: forall tp. Ord tp => ValueBound tp -> ValueBound tp -> Bool
> :: ValueBound tp -> ValueBound tp -> Bool
$c> :: forall tp. Ord tp => ValueBound tp -> ValueBound tp -> Bool
<= :: ValueBound tp -> ValueBound tp -> Bool
$c<= :: forall tp. Ord tp => ValueBound tp -> ValueBound tp -> Bool
< :: ValueBound tp -> ValueBound tp -> Bool
$c< :: forall tp. Ord tp => ValueBound tp -> ValueBound tp -> Bool
compare :: ValueBound tp -> ValueBound tp -> Ordering
$ccompare :: forall tp. Ord tp => ValueBound tp -> ValueBound tp -> Ordering
Ord)

instance Applicative ValueBound where
  pure :: forall a. a -> ValueBound a
pure = forall a. a -> ValueBound a
Inclusive
  ValueBound (a -> b)
Unbounded <*> :: forall a b. ValueBound (a -> b) -> ValueBound a -> ValueBound b
<*> ValueBound a
_ = forall tp. ValueBound tp
Unbounded
  ValueBound (a -> b)
_ <*> ValueBound a
Unbounded = forall tp. ValueBound tp
Unbounded
  Inclusive a -> b
f <*> Inclusive a
v = forall a. a -> ValueBound a
Inclusive (a -> b
f a
v)

instance Monad ValueBound where
  return :: forall a. a -> ValueBound a
return = forall (f :: Type -> Type) a. Applicative f => a -> f a
pure
  ValueBound a
Unbounded >>= :: forall a b. ValueBound a -> (a -> ValueBound b) -> ValueBound b
>>= a -> ValueBound b
_ = forall tp. ValueBound tp
Unbounded
  Inclusive a
v >>= a -> ValueBound b
f = a -> ValueBound b
f a
v

minValueBound :: Ord tp => ValueBound tp -> ValueBound tp -> ValueBound tp
minValueBound :: forall tp.
Ord tp =>
ValueBound tp -> ValueBound tp -> ValueBound tp
minValueBound ValueBound tp
x ValueBound tp
y = forall a. Ord a => a -> a -> a
min forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueBound tp
x forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> ValueBound tp
y

maxValueBound :: Ord tp => ValueBound tp -> ValueBound tp -> ValueBound tp
maxValueBound :: forall tp.
Ord tp =>
ValueBound tp -> ValueBound tp -> ValueBound tp
maxValueBound ValueBound tp
x ValueBound tp
y = forall a. Ord a => a -> a -> a
max forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueBound tp
x forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> ValueBound tp
y

lowerBoundIsNegative :: (Ord tp, Num tp) => ValueBound tp -> Bool
lowerBoundIsNegative :: forall tp. (Ord tp, Num tp) => ValueBound tp -> Bool
lowerBoundIsNegative ValueBound tp
Unbounded = Bool
True
lowerBoundIsNegative (Inclusive tp
y) = tp
y forall a. Ord a => a -> a -> Bool
<= tp
0

upperBoundIsNonNeg :: (Ord tp, Num tp) => ValueBound tp -> Bool
upperBoundIsNonNeg :: forall tp. (Ord tp, Num tp) => ValueBound tp -> Bool
upperBoundIsNonNeg ValueBound tp
Unbounded = Bool
True
upperBoundIsNonNeg (Inclusive tp
y) = tp
y forall a. Ord a => a -> a -> Bool
>= tp
0

------------------------------------------------------------------------
-- ValueRange support classes.

-- | Describes a range of values in a totally ordered set.
data ValueRange tp
  = 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.

asMultiRange :: ValueRange tp -> Maybe (ValueBound tp, ValueBound tp)
asMultiRange :: forall tp. ValueRange tp -> Maybe (ValueBound tp, ValueBound tp)
asMultiRange ValueRange tp
r =
  case ValueRange tp
r of
    SingleRange tp
_ -> forall a. Maybe a
Nothing
    ValueRange tp
UnboundedRange -> forall a. a -> Maybe a
Just (forall tp. ValueBound tp
Unbounded, forall tp. ValueBound tp
Unbounded)
    MinRange tp
lo -> forall a. a -> Maybe a
Just (forall a. a -> ValueBound a
Inclusive tp
lo, forall tp. ValueBound tp
Unbounded)
    MaxRange tp
hi -> forall a. a -> Maybe a
Just (forall tp. ValueBound tp
Unbounded, forall a. a -> ValueBound a
Inclusive tp
hi)
    IntervalRange tp
lo tp
hi -> forall a. a -> Maybe a
Just (forall a. a -> ValueBound a
Inclusive tp
lo, forall a. a -> ValueBound a
Inclusive tp
hi)

multiRange :: ValueBound tp -> ValueBound tp -> ValueRange tp
multiRange :: forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
multiRange ValueBound tp
Unbounded ValueBound tp
Unbounded = forall tp. ValueRange tp
UnboundedRange
multiRange ValueBound tp
Unbounded (Inclusive tp
hi) = forall tp. tp -> ValueRange tp
MaxRange tp
hi
multiRange (Inclusive tp
lo) ValueBound tp
Unbounded = forall tp. tp -> ValueRange tp
MinRange tp
lo
multiRange (Inclusive tp
lo) (Inclusive tp
hi) = forall tp. tp -> tp -> ValueRange tp
IntervalRange tp
lo tp
hi

-- | Indicates that the number is somewhere between the given upper and lower bound.
pattern MultiRange :: ValueBound tp -> ValueBound tp -> ValueRange tp
pattern $bMultiRange :: forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
$mMultiRange :: forall {r} {tp}.
ValueRange tp
-> (ValueBound tp -> ValueBound tp -> r) -> ((# #) -> r) -> r
MultiRange lo hi <- (asMultiRange -> Just (lo, hi)) where
  MultiRange ValueBound tp
lo ValueBound tp
hi = forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
multiRange ValueBound tp
lo ValueBound tp
hi

{-# COMPLETE SingleRange, MultiRange #-}

intAbsRange :: ValueRange Integer -> ValueRange Integer
intAbsRange :: ValueRange Integer -> ValueRange Integer
intAbsRange ValueRange Integer
r =
  case ValueRange Integer
r of
    SingleRange Integer
x -> forall tp. tp -> ValueRange tp
SingleRange (forall a. Num a => a -> a
abs Integer
x)
    ValueRange Integer
UnboundedRange -> forall tp. tp -> ValueRange tp
MinRange Integer
0
    MinRange Integer
lo
      | Integer
0 forall a. Ord a => a -> a -> Bool
<= Integer
lo -> ValueRange Integer
r
      | Bool
otherwise -> forall tp. tp -> ValueRange tp
MinRange Integer
0
    MaxRange Integer
hi
      | Integer
hi forall a. Ord a => a -> a -> Bool
<= Integer
0 -> forall tp. tp -> ValueRange tp
MinRange (forall a. Num a => a -> a
negate Integer
hi)
      | Bool
otherwise -> forall tp. tp -> ValueRange tp
MinRange Integer
0
    IntervalRange Integer
lo Integer
hi
      | Integer
0 forall a. Ord a => a -> a -> Bool
<= Integer
lo -> ValueRange Integer
r
      | Integer
hi forall a. Ord a => a -> a -> Bool
<= Integer
0 -> forall tp. tp -> tp -> ValueRange tp
IntervalRange (forall a. Num a => a -> a
negate Integer
hi) (forall a. Num a => a -> a
negate Integer
lo)
      | Bool
otherwise -> forall tp. tp -> tp -> ValueRange tp
IntervalRange Integer
0 (forall a. Ord a => a -> a -> a
max (forall a. Num a => a -> a
abs Integer
lo) (forall a. Num a => a -> a
abs Integer
hi))

-- | 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.
intDivRange :: ValueRange Integer -> ValueRange Integer -> ValueRange Integer
intDivRange :: ValueRange Integer -> ValueRange Integer -> ValueRange Integer
intDivRange (SingleRange Integer
x) (SingleRange Integer
y)
  | Integer
y forall a. Ord a => a -> a -> Bool
> Integer
0  = forall tp. tp -> ValueRange tp
SingleRange (Integer
x forall a. Integral a => a -> a -> a
`div` Integer
y)
  | Integer
y forall a. Ord a => a -> a -> Bool
< Integer
0  = forall tp. tp -> ValueRange tp
SingleRange (forall a. Num a => a -> a
negate (Integer
x forall a. Integral a => a -> a -> a
`div` forall a. Num a => a -> a
negate Integer
y))
intDivRange (MultiRange ValueBound Integer
lo ValueBound Integer
hi) (SingleRange Integer
y)
  | Integer
y forall a. Ord a => a -> a -> Bool
>  Integer
0 = forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
MultiRange
                   ((\Integer
x -> Integer
x forall a. Integral a => a -> a -> a
`div` Integer
y) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueBound Integer
lo)
                   ((\Integer
x -> Integer
x forall a. Integral a => a -> a -> a
`div` Integer
y) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueBound Integer
hi)
  | Integer
y forall a. Ord a => a -> a -> Bool
<  Integer
0 = forall tp. Num tp => ValueRange tp -> ValueRange tp
negateRange forall a b. (a -> b) -> a -> b
$ forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
MultiRange
                    ((\Integer
x -> Integer
x forall a. Integral a => a -> a -> a
`div` forall a. Num a => a -> a
negate Integer
y) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueBound Integer
lo)
                    ((\Integer
x -> Integer
x forall a. Integral a => a -> a -> a
`div` forall a. Num a => a -> a
negate Integer
y) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueBound Integer
hi)

intDivRange ValueRange Integer
x (MultiRange (Inclusive Integer
lo) ValueBound Integer
hi)
  | Integer
0 forall a. Ord a => a -> a -> Bool
< Integer
lo = ValueRange Integer
-> Integer -> ValueBound Integer -> ValueRange Integer
intDivAux ValueRange Integer
x Integer
lo ValueBound Integer
hi

intDivRange ValueRange Integer
x (MultiRange ValueBound Integer
lo (Inclusive Integer
hi))
  | Integer
hi forall a. Ord a => a -> a -> Bool
< Integer
0 = forall tp. Num tp => ValueRange tp -> ValueRange tp
negateRange (ValueRange Integer
-> Integer -> ValueBound Integer -> ValueRange Integer
intDivAux ValueRange Integer
x (forall a. Num a => a -> a
negate Integer
hi) (forall a. Num a => a -> a
negate forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueBound Integer
lo))

-- The divisor interval contains 0, so we learn nothing
intDivRange ValueRange Integer
_ ValueRange Integer
_ = forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
MultiRange forall tp. ValueBound tp
Unbounded forall tp. ValueBound tp
Unbounded


-- Here we get to assume 'lo' and 'hi' are strictly positive
intDivAux ::
  ValueRange Integer ->
  Integer -> ValueBound Integer ->
  ValueRange Integer
intDivAux :: ValueRange Integer
-> Integer -> ValueBound Integer -> ValueRange Integer
intDivAux ValueRange Integer
x Integer
lo ValueBound Integer
Unbounded = forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
MultiRange ValueBound Integer
lo' ValueBound Integer
hi'
  where
  lo' :: ValueBound Integer
lo' = case forall tp. ValueRange tp -> ValueBound tp
rangeLowBound ValueRange Integer
x of
           ValueBound Integer
Unbounded -> forall tp. ValueBound tp
Unbounded
           Inclusive Integer
z -> forall a. a -> ValueBound a
Inclusive (forall a. Ord a => a -> a -> a
min Integer
0 (forall a. Integral a => a -> a -> a
div Integer
z Integer
lo))

  hi' :: ValueBound Integer
hi' = case forall tp. ValueRange tp -> ValueBound tp
rangeHiBound ValueRange Integer
x of
           ValueBound Integer
Unbounded   -> forall tp. ValueBound tp
Unbounded
           Inclusive Integer
z -> forall a. a -> ValueBound a
Inclusive (forall a. Ord a => a -> a -> a
max (-Integer
1) (forall a. Integral a => a -> a -> a
div Integer
z Integer
lo))

intDivAux ValueRange Integer
x Integer
lo (Inclusive Integer
hi) = forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
MultiRange ValueBound Integer
lo' ValueBound Integer
hi'
  where
  lo' :: ValueBound Integer
lo' = case forall tp. ValueRange tp -> ValueBound tp
rangeLowBound ValueRange Integer
x of
           ValueBound Integer
Unbounded -> forall tp. ValueBound tp
Unbounded
           Inclusive Integer
z -> forall a. a -> ValueBound a
Inclusive (forall a. Ord a => a -> a -> a
min (forall a. Integral a => a -> a -> a
div Integer
z Integer
hi) (forall a. Integral a => a -> a -> a
div Integer
z Integer
lo))

  hi' :: ValueBound Integer
hi' = case forall tp. ValueRange tp -> ValueBound tp
rangeHiBound ValueRange Integer
x of
           ValueBound Integer
Unbounded   -> forall tp. ValueBound tp
Unbounded
           Inclusive Integer
z -> forall a. a -> ValueBound a
Inclusive (forall a. Ord a => a -> a -> a
max (forall a. Integral a => a -> a -> a
div Integer
z Integer
hi) (forall a. Integral a => a -> a -> a
div Integer
z Integer
lo))

intModRange :: ValueRange Integer -> ValueRange Integer -> ValueRange Integer
intModRange :: ValueRange Integer -> ValueRange Integer -> ValueRange Integer
intModRange ValueRange Integer
_ (SingleRange Integer
y) | Integer
y forall a. Eq a => a -> a -> Bool
== Integer
0 = forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
MultiRange forall tp. ValueBound tp
Unbounded forall tp. ValueBound tp
Unbounded
intModRange (SingleRange Integer
x) (SingleRange Integer
y) = forall tp. tp -> ValueRange tp
SingleRange (Integer
x forall a. Integral a => a -> a -> a
`mod` forall a. Num a => a -> a
abs Integer
y)
intModRange (MultiRange (Inclusive Integer
lo) (Inclusive Integer
hi)) (SingleRange Integer
y)
   | Integer
hi' forall a. Num a => a -> a -> a
- Integer
lo' forall a. Eq a => a -> a -> Bool
== Integer
hi forall a. Num a => a -> a -> a
- Integer
lo = forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
MultiRange (forall a. a -> ValueBound a
Inclusive Integer
lo') (forall a. a -> ValueBound a
Inclusive Integer
hi')
  where
  lo' :: Integer
lo' = Integer
lo forall a. Integral a => a -> a -> a
`mod` forall a. Num a => a -> a
abs Integer
y
  hi' :: Integer
hi' = Integer
hi forall a. Integral a => a -> a -> a
`mod` forall a. Num a => a -> a
abs Integer
y
intModRange ValueRange Integer
_ ValueRange Integer
y
  | Inclusive Integer
lo <- forall tp. ValueRange tp -> ValueBound tp
rangeLowBound ValueRange Integer
yabs, Integer
lo forall a. Ord a => a -> a -> Bool
> Integer
0
  = forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
MultiRange (forall a. a -> ValueBound a
Inclusive Integer
0) (forall a. Enum a => a -> a
pred forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall tp. ValueRange tp -> ValueBound tp
rangeHiBound ValueRange Integer
yabs)
  | Bool
otherwise
  = forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
MultiRange forall tp. ValueBound tp
Unbounded forall tp. ValueBound tp
Unbounded
 where
 yabs :: ValueRange Integer
yabs = ValueRange Integer -> ValueRange Integer
intAbsRange ValueRange Integer
y


addRange :: Num tp => ValueRange tp -> ValueRange tp -> ValueRange tp
addRange :: forall tp.
Num tp =>
ValueRange tp -> ValueRange tp -> ValueRange tp
addRange (SingleRange tp
x) ValueRange tp
y = forall a b. (a -> b) -> ValueRange a -> ValueRange b
mapRange (tp
xforall a. Num a => a -> a -> a
+) ValueRange tp
y
addRange ValueRange tp
x (SingleRange tp
y) = forall a b. (a -> b) -> ValueRange a -> ValueRange b
mapRange (tp
yforall a. Num a => a -> a -> a
+) ValueRange tp
x
addRange ValueRange tp
UnboundedRange ValueRange tp
_ = forall tp. ValueRange tp
UnboundedRange
addRange ValueRange tp
_ ValueRange tp
UnboundedRange = forall tp. ValueRange tp
UnboundedRange
addRange (MinRange tp
_) (MaxRange tp
_) = forall tp. ValueRange tp
UnboundedRange
addRange (MaxRange tp
_) (MinRange tp
_) = forall tp. ValueRange tp
UnboundedRange
addRange (MinRange tp
lx) (MinRange tp
ly) = forall tp. tp -> ValueRange tp
MinRange (tp
lxforall a. Num a => a -> a -> a
+tp
ly)
addRange (MaxRange tp
ux) (MaxRange tp
uy) = forall tp. tp -> ValueRange tp
MaxRange (tp
uxforall a. Num a => a -> a -> a
+tp
uy)
addRange (MinRange tp
lx) (IntervalRange tp
ly tp
_) = forall tp. tp -> ValueRange tp
MinRange (tp
lxforall a. Num a => a -> a -> a
+tp
ly)
addRange (IntervalRange tp
lx tp
_) (MinRange tp
ly) = forall tp. tp -> ValueRange tp
MinRange (tp
lxforall a. Num a => a -> a -> a
+tp
ly)
addRange (MaxRange tp
ux) (IntervalRange tp
_ tp
uy) = forall tp. tp -> ValueRange tp
MaxRange (tp
uxforall a. Num a => a -> a -> a
+tp
uy)
addRange (IntervalRange tp
_ tp
ux) (MaxRange tp
uy) = forall tp. tp -> ValueRange tp
MaxRange (tp
uxforall a. Num a => a -> a -> a
+tp
uy)
addRange (IntervalRange tp
lx tp
ux) (IntervalRange tp
ly tp
uy) = forall tp. tp -> tp -> ValueRange tp
IntervalRange (tp
lxforall a. Num a => a -> a -> a
+tp
ly) (tp
uxforall a. Num a => a -> a -> a
+tp
uy)

-- | Return 'Just True if the range only contains an integer, 'Just False' if it
-- contains no integers, and 'Nothing' if the range contains both integers and
-- non-integers.
rangeIsInteger :: ValueRange Rational -> Maybe Bool
rangeIsInteger :: ValueRange Rational -> Maybe Bool
rangeIsInteger (SingleRange Rational
x) = forall a. a -> Maybe a
Just (forall a. Ratio a -> a
denominator Rational
x forall a. Eq a => a -> a -> Bool
== Integer
1)
rangeIsInteger (MultiRange (Inclusive Rational
l) (Inclusive Rational
u))
  | forall a b. (RealFrac a, Integral b) => a -> b
floor Rational
l forall a. Num a => a -> a -> a
+ Integer
1 forall a. Ord a => a -> a -> Bool
>= (forall a b. (RealFrac a, Integral b) => a -> b
ceiling Rational
u :: Integer)
  , forall a. Ratio a -> a
denominator Rational
l forall a. Eq a => a -> a -> Bool
/= Integer
1
  , forall a. Ratio a -> a
denominator Rational
u forall a. Eq a => a -> a -> Bool
/= Integer
1 = forall a. a -> Maybe a
Just Bool
False
rangeIsInteger ValueRange Rational
_ = forall a. Maybe a
Nothing

-- | Multiply a range by a scalar value
rangeScalarMul :: (Ord tp, Num tp) => tp -> ValueRange tp -> ValueRange tp
rangeScalarMul :: forall tp. (Ord tp, Num tp) => tp -> ValueRange tp -> ValueRange tp
rangeScalarMul tp
x ValueRange tp
r =
  case forall a. Ord a => a -> a -> Ordering
compare tp
x tp
0 of
    Ordering
LT -> forall a b. (a -> b) -> ValueRange a -> ValueRange b
mapAntiRange (tp
x forall a. Num a => a -> a -> a
*) ValueRange tp
r
    Ordering
EQ -> forall tp. tp -> ValueRange tp
SingleRange tp
0
    Ordering
GT -> forall a b. (a -> b) -> ValueRange a -> ValueRange b
mapRange (tp
x forall a. Num a => a -> a -> a
*) ValueRange tp
r

negateRange :: (Num tp) => ValueRange tp -> ValueRange tp
negateRange :: forall tp. Num tp => ValueRange tp -> ValueRange tp
negateRange = forall a b. (a -> b) -> ValueRange a -> ValueRange b
mapAntiRange forall a. Num a => a -> a
negate

-- | Multiply two ranges together.
mulRange :: (Ord tp, Num tp) => ValueRange tp -> ValueRange tp -> ValueRange tp
mulRange :: forall tp.
(Ord tp, Num tp) =>
ValueRange tp -> ValueRange tp -> ValueRange tp
mulRange (SingleRange tp
x) ValueRange tp
y = forall tp. (Ord tp, Num tp) => tp -> ValueRange tp -> ValueRange tp
rangeScalarMul tp
x ValueRange tp
y
mulRange ValueRange tp
x (SingleRange tp
y) = forall tp. (Ord tp, Num tp) => tp -> ValueRange tp -> ValueRange tp
rangeScalarMul tp
y ValueRange tp
x
mulRange (MultiRange ValueBound tp
lx ValueBound tp
ux) (MultiRange ValueBound tp
ly ValueBound tp
uy) = forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
MultiRange ValueBound tp
lz ValueBound tp
uz
  where x_neg :: Bool
x_neg = forall tp. (Ord tp, Num tp) => ValueBound tp -> Bool
lowerBoundIsNegative ValueBound tp
lx
        x_pos :: Bool
x_pos = forall tp. (Ord tp, Num tp) => ValueBound tp -> Bool
upperBoundIsNonNeg ValueBound tp
ux
        y_neg :: Bool
y_neg = forall tp. (Ord tp, Num tp) => ValueBound tp -> Bool
lowerBoundIsNegative ValueBound tp
ly
        y_pos :: Bool
y_pos = forall tp. (Ord tp, Num tp) => ValueBound tp -> Bool
upperBoundIsNonNeg ValueBound tp
uy
             -- X can be negative and y can be positive, and also
             -- x can be positive and y can be negative.
        lz :: ValueBound tp
lz | Bool
x_neg Bool -> Bool -> Bool
&& Bool
y_pos Bool -> Bool -> Bool
&& Bool
x_pos Bool -> Bool -> Bool
&& Bool
y_neg =
               forall tp.
Ord tp =>
ValueBound tp -> ValueBound tp -> ValueBound tp
minValueBound (forall a. Num a => a -> a -> a
(*) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueBound tp
lx forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> ValueBound tp
uy)
                             (forall a. Num a => a -> a -> a
(*) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueBound tp
ux forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> ValueBound tp
ly)
             -- X can be negative and Y can be positive, but
             -- either x must be negative (!x_pos) or y cannot be
             -- negative (!y_neg).
           | Bool
x_neg Bool -> Bool -> Bool
&& Bool
y_pos = forall a. Num a => a -> a -> a
(*) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueBound tp
lx forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> ValueBound tp
uy
             -- X can be positive and Y can be negative, but
             -- either x must be positive (!x_neg) or y cannot be
             -- positive (!y_pos).
           | Bool
x_pos Bool -> Bool -> Bool
&& Bool
y_neg = forall a. Num a => a -> a -> a
(*) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueBound tp
ux forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> ValueBound tp
ly
             -- Both x and y must be negative.
           | Bool
x_neg = forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Bool -> Bool
not Bool
x_pos Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
y_pos) forall a b. (a -> b) -> a -> b
$ forall a. Num a => a -> a -> a
(*) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueBound tp
ux forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> ValueBound tp
uy
             -- Both x and y must be positive.
           | Bool
otherwise = forall a. Num a => a -> a -> a
(*) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueBound tp
lx forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> ValueBound tp
ly
        uz :: ValueBound tp
uz | Bool
x_neg Bool -> Bool -> Bool
&& Bool
y_neg Bool -> Bool -> Bool
&& Bool
x_pos Bool -> Bool -> Bool
&& Bool
y_pos =
             forall tp.
Ord tp =>
ValueBound tp -> ValueBound tp -> ValueBound tp
maxValueBound (forall a. Num a => a -> a -> a
(*) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueBound tp
lx forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> ValueBound tp
ly)
                           (forall a. Num a => a -> a -> a
(*) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueBound tp
ux forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> ValueBound tp
uy)
             -- Both x and y can be negative, but they both can't be positive.
           | Bool
x_neg Bool -> Bool -> Bool
&& Bool
y_neg = forall a. Num a => a -> a -> a
(*) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueBound tp
lx forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> ValueBound tp
ly
             -- Both x and y can be positive, but they both can't be negative.
           | Bool
x_pos Bool -> Bool -> Bool
&& Bool
y_pos = forall a. Num a => a -> a -> a
(*) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueBound tp
ux forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> ValueBound tp
uy
             -- x must be positive and y must be negative.
           | Bool
x_pos = forall a. Num a => a -> a -> a
(*) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueBound tp
lx forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> ValueBound tp
uy
             -- x must be negative and y must be positive.
           | Bool
otherwise = forall a. Num a => a -> a -> a
(*) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueBound tp
ux forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> ValueBound tp
ly

-- | Return lower bound of range.
rangeLowBound :: ValueRange tp -> ValueBound tp
rangeLowBound :: forall tp. ValueRange tp -> ValueBound tp
rangeLowBound (SingleRange tp
x) = forall a. a -> ValueBound a
Inclusive tp
x
rangeLowBound (MultiRange ValueBound tp
l ValueBound tp
_) = ValueBound tp
l

-- | Return upper bound of range.
rangeHiBound :: ValueRange tp -> ValueBound tp
rangeHiBound :: forall tp. ValueRange tp -> ValueBound tp
rangeHiBound (SingleRange tp
x) = forall a. a -> ValueBound a
Inclusive tp
x
rangeHiBound (MultiRange ValueBound tp
_ ValueBound tp
u) = ValueBound tp
u

-- | Compute the smallest range containing both ranges.
joinRange :: Ord tp => ValueRange tp -> ValueRange tp -> ValueRange tp
joinRange :: forall tp.
Ord tp =>
ValueRange tp -> ValueRange tp -> ValueRange tp
joinRange (SingleRange tp
x) (SingleRange tp
y)
  | tp
x forall a. Eq a => a -> a -> Bool
== tp
y = forall tp. tp -> ValueRange tp
SingleRange tp
x
joinRange ValueRange tp
x ValueRange tp
y = forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
MultiRange (forall tp.
Ord tp =>
ValueBound tp -> ValueBound tp -> ValueBound tp
minValueBound ValueBound tp
lx ValueBound tp
ly) (forall tp.
Ord tp =>
ValueBound tp -> ValueBound tp -> ValueBound tp
maxValueBound ValueBound tp
ux ValueBound tp
uy)
  where lx :: ValueBound tp
lx = forall tp. ValueRange tp -> ValueBound tp
rangeLowBound ValueRange tp
x
        ux :: ValueBound tp
ux = forall tp. ValueRange tp -> ValueBound tp
rangeHiBound ValueRange tp
x
        ly :: ValueBound tp
ly = forall tp. ValueRange tp -> ValueBound tp
rangeLowBound ValueRange tp
y
        uy :: ValueBound tp
uy = forall tp. ValueRange tp -> ValueBound tp
rangeHiBound ValueRange tp
y

-- | Return true if value ranges overlap.
rangeOverlap :: Ord tp => ValueRange tp -> ValueRange tp -> Bool
rangeOverlap :: forall tp. Ord tp => ValueRange tp -> ValueRange tp -> Bool
rangeOverlap ValueRange tp
x ValueRange tp
y
   -- first range is before second.
  | Inclusive tp
ux <- forall tp. ValueRange tp -> ValueBound tp
rangeHiBound ValueRange tp
x
  , Inclusive tp
ly <- forall tp. ValueRange tp -> ValueBound tp
rangeLowBound ValueRange tp
y
  , tp
ux forall a. Ord a => a -> a -> Bool
< tp
ly = Bool
False

  -- second range is before first.
  | Inclusive tp
lx <- forall tp. ValueRange tp -> ValueBound tp
rangeLowBound ValueRange tp
x
  , Inclusive tp
uy <- forall tp. ValueRange tp -> ValueBound tp
rangeHiBound ValueRange tp
y
  , tp
uy forall a. Ord a => a -> a -> Bool
< tp
lx = Bool
False

  -- Ranges share some elements.
  | Bool
otherwise = Bool
True

-- | Return maybe Boolean if range is equal, is not equal, or indeterminant.
rangeCheckEq :: Ord tp => ValueRange tp -> ValueRange tp -> Maybe Bool
rangeCheckEq :: forall tp. Ord tp => ValueRange tp -> ValueRange tp -> Maybe Bool
rangeCheckEq ValueRange tp
x ValueRange tp
y
    -- If ranges do not overlap return false.
  | Bool -> Bool
not (forall tp. Ord tp => ValueRange tp -> ValueRange tp -> Bool
rangeOverlap ValueRange tp
x ValueRange tp
y) = forall a. a -> Maybe a
Just Bool
False
    -- If they are both single values, then result can be determined.
  | Just tp
cx <- forall tp. ValueRange tp -> Maybe tp
asSingleRange ValueRange tp
x
  , Just tp
cy <- forall tp. ValueRange tp -> Maybe tp
asSingleRange ValueRange tp
y
  = forall a. a -> Maybe a
Just (tp
cx forall a. Eq a => a -> a -> Bool
== tp
cy)
    -- Otherwise result is indeterminant.
  | Bool
otherwise = forall a. Maybe a
Nothing


rangeCheckLe :: Ord tp => ValueRange tp -> ValueRange tp -> Maybe Bool
rangeCheckLe :: forall tp. Ord tp => ValueRange tp -> ValueRange tp -> Maybe Bool
rangeCheckLe ValueRange tp
x ValueRange tp
y
    -- First range upper bound is below lower bound of second.
  | Inclusive tp
ux <- forall tp. ValueRange tp -> ValueBound tp
rangeHiBound ValueRange tp
x
  , Inclusive tp
ly <- forall tp. ValueRange tp -> ValueBound tp
rangeLowBound ValueRange tp
y
  , tp
ux forall a. Ord a => a -> a -> Bool
<= tp
ly = forall a. a -> Maybe a
Just Bool
True

    -- First range lower bound is above upper bound of second.
  | Inclusive tp
lx <- forall tp. ValueRange tp -> ValueBound tp
rangeLowBound ValueRange tp
x
  , Inclusive tp
uy <- forall tp. ValueRange tp -> ValueBound tp
rangeHiBound ValueRange tp
y
  , tp
uy forall a. Ord a => a -> a -> Bool
<  tp
lx = forall a. a -> Maybe a
Just Bool
False

  | Bool
otherwise = forall a. Maybe a
Nothing

-- | Defines a unbounded value range.
unboundedRange :: ValueRange tp
unboundedRange :: forall tp. ValueRange tp
unboundedRange = forall tp. ValueRange tp
UnboundedRange

-- | Defines a unbounded value range.
concreteRange :: Eq tp => tp -> tp -> ValueRange tp
concreteRange :: forall tp. Eq tp => tp -> tp -> ValueRange tp
concreteRange tp
x tp
y
  | tp
x forall a. Eq a => a -> a -> Bool
== tp
y = forall tp. tp -> ValueRange tp
SingleRange tp
x
  | Bool
otherwise = forall tp. tp -> tp -> ValueRange tp
IntervalRange tp
x tp
y

-- | Defines a value range containing a single element.
singleRange :: tp -> ValueRange tp
singleRange :: forall tp. tp -> ValueRange tp
singleRange tp
v = forall tp. tp -> ValueRange tp
SingleRange tp
v

-- | Define a value range with the given bounds
valueRange :: Eq tp => ValueBound tp -> ValueBound tp -> ValueRange tp
valueRange :: forall tp. Eq tp => ValueBound tp -> ValueBound tp -> ValueRange tp
valueRange (Inclusive tp
x) (Inclusive tp
y)
  | tp
x forall a. Eq a => a -> a -> Bool
== tp
y = forall tp. tp -> ValueRange tp
SingleRange tp
x
valueRange ValueBound tp
x ValueBound tp
y = forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
MultiRange ValueBound tp
x ValueBound tp
y

-- | Check if range is just a single element.
asSingleRange :: ValueRange tp -> Maybe tp
asSingleRange :: forall tp. ValueRange tp -> Maybe tp
asSingleRange (SingleRange tp
x) = forall a. a -> Maybe a
Just tp
x
asSingleRange ValueRange tp
_ = forall a. Maybe a
Nothing

-- | Map a monotonic function over a range.
mapRange :: (a -> b) -> ValueRange a -> ValueRange b
mapRange :: forall a b. (a -> b) -> ValueRange a -> ValueRange b
mapRange a -> b
f ValueRange a
r =
  case ValueRange a
r of
    SingleRange a
x -> forall tp. tp -> ValueRange tp
SingleRange (a -> b
f a
x)
    ValueRange a
UnboundedRange -> forall tp. ValueRange tp
UnboundedRange
    MinRange a
l -> forall tp. tp -> ValueRange tp
MinRange (a -> b
f a
l)
    MaxRange a
h -> forall tp. tp -> ValueRange tp
MaxRange (a -> b
f a
h)
    IntervalRange a
l a
h -> forall tp. tp -> tp -> ValueRange tp
IntervalRange (a -> b
f a
l) (a -> b
f a
h)

-- | Map an anti-monotonic function over a range.
mapAntiRange :: (a -> b) -> ValueRange a -> ValueRange b
mapAntiRange :: forall a b. (a -> b) -> ValueRange a -> ValueRange b
mapAntiRange a -> b
f ValueRange a
r =
  case ValueRange a
r of
    SingleRange a
x -> forall tp. tp -> ValueRange tp
SingleRange (a -> b
f a
x)
    ValueRange a
UnboundedRange -> forall tp. ValueRange tp
UnboundedRange
    MinRange a
l -> forall tp. tp -> ValueRange tp
MaxRange (a -> b
f a
l)
    MaxRange a
h -> forall tp. tp -> ValueRange tp
MinRange (a -> b
f a
h)
    IntervalRange a
l a
h -> forall tp. tp -> tp -> ValueRange tp
IntervalRange (a -> b
f a
h) (a -> b
f a
l)

------------------------------------------------------------------------
-- AbstractValue definition.

-- Contains range for rational and whether value must be an integer.
data RealAbstractValue = RAV { RealAbstractValue -> ValueRange Rational
ravRange :: !(ValueRange Rational)
                             , RealAbstractValue -> Maybe Bool
ravIsInteger :: !(Maybe Bool)
                             }

ravUnbounded :: RealAbstractValue
ravUnbounded :: RealAbstractValue
ravUnbounded = (ValueRange Rational -> Maybe Bool -> RealAbstractValue
RAV forall tp. ValueRange tp
unboundedRange forall a. Maybe a
Nothing)

ravSingle :: Rational -> RealAbstractValue
ravSingle :: Rational -> RealAbstractValue
ravSingle Rational
x = ValueRange Rational -> Maybe Bool -> RealAbstractValue
RAV (forall tp. tp -> ValueRange tp
singleRange Rational
x) (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$! forall a. Ratio a -> a
denominator Rational
x forall a. Eq a => a -> a -> Bool
== Integer
1)

-- | Range accepting everything between lower and upper bound.
ravConcreteRange :: Rational -- ^ Lower bound
                 -> Rational -- ^ Upper bound
                 -> RealAbstractValue
ravConcreteRange :: Rational -> Rational -> RealAbstractValue
ravConcreteRange Rational
l Rational
h = ValueRange Rational -> Maybe Bool -> RealAbstractValue
RAV (forall tp. Eq tp => tp -> tp -> ValueRange tp
concreteRange Rational
l Rational
h) (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$! Bool
b)
  where -- Return true if this is a singleton.
        b :: Bool
b = Rational
l forall a. Eq a => a -> a -> Bool
== Rational
h Bool -> Bool -> Bool
&& forall a. Ratio a -> a
denominator Rational
l forall a. Eq a => a -> a -> Bool
== Integer
1

-- | Add two real abstract values.
ravAdd :: RealAbstractValue -> RealAbstractValue -> RealAbstractValue
ravAdd :: RealAbstractValue -> RealAbstractValue -> RealAbstractValue
ravAdd (RAV ValueRange Rational
xr Maybe Bool
xi) (RAV ValueRange Rational
yr Maybe Bool
yi) = ValueRange Rational -> Maybe Bool -> RealAbstractValue
RAV ValueRange Rational
zr Maybe Bool
zi
  where zr :: ValueRange Rational
zr = forall tp.
Num tp =>
ValueRange tp -> ValueRange tp -> ValueRange tp
addRange ValueRange Rational
xr ValueRange Rational
yr
        zi :: Maybe Bool
zi | (Maybe Bool
xi,Maybe Bool
yi) forall a. Eq a => a -> a -> Bool
== (forall a. a -> Maybe a
Just Bool
True, forall a. a -> Maybe a
Just Bool
True) = forall a. a -> Maybe a
Just Bool
True
           | Bool
otherwise = ValueRange Rational -> Maybe Bool
rangeIsInteger ValueRange Rational
zr

ravScalarMul :: Rational -> RealAbstractValue -> RealAbstractValue
ravScalarMul :: Rational -> RealAbstractValue -> RealAbstractValue
ravScalarMul Rational
x (RAV ValueRange Rational
yr Maybe Bool
yi) = ValueRange Rational -> Maybe Bool -> RealAbstractValue
RAV ValueRange Rational
zr Maybe Bool
zi
  where zr :: ValueRange Rational
zr = forall tp. (Ord tp, Num tp) => tp -> ValueRange tp -> ValueRange tp
rangeScalarMul Rational
x ValueRange Rational
yr
        zi :: Maybe Bool
zi | forall a. Ratio a -> a
denominator Rational
x forall a. Eq a => a -> a -> Bool
== Integer
1 Bool -> Bool -> Bool
&& Maybe Bool
yi forall a. Eq a => a -> a -> Bool
== forall a. a -> Maybe a
Just Bool
True = forall a. a -> Maybe a
Just Bool
True
           | Bool
otherwise = ValueRange Rational -> Maybe Bool
rangeIsInteger ValueRange Rational
zr


ravMul :: RealAbstractValue -> RealAbstractValue -> RealAbstractValue
ravMul :: RealAbstractValue -> RealAbstractValue -> RealAbstractValue
ravMul (RAV ValueRange Rational
xr Maybe Bool
xi) (RAV ValueRange Rational
yr Maybe Bool
yi) = ValueRange Rational -> Maybe Bool -> RealAbstractValue
RAV ValueRange Rational
zr Maybe Bool
zi
  where zr :: ValueRange Rational
zr = forall tp.
(Ord tp, Num tp) =>
ValueRange tp -> ValueRange tp -> ValueRange tp
mulRange ValueRange Rational
xr ValueRange Rational
yr
        zi :: Maybe Bool
zi | (Maybe Bool
xi,Maybe Bool
yi) forall a. Eq a => a -> a -> Bool
== (forall a. a -> Maybe a
Just Bool
True, forall a. a -> Maybe a
Just Bool
True) = forall a. a -> Maybe a
Just Bool
True
           | Bool
otherwise = ValueRange Rational -> Maybe Bool
rangeIsInteger ValueRange Rational
zr

ravJoin :: RealAbstractValue -> RealAbstractValue -> RealAbstractValue
ravJoin :: RealAbstractValue -> RealAbstractValue -> RealAbstractValue
ravJoin (RAV ValueRange Rational
xr Maybe Bool
xi) (RAV ValueRange Rational
yr Maybe Bool
yi) = ValueRange Rational -> Maybe Bool -> RealAbstractValue
RAV (forall tp.
Ord tp =>
ValueRange tp -> ValueRange tp -> ValueRange tp
joinRange ValueRange Rational
xr ValueRange Rational
yr) Maybe Bool
zi
  where zi :: Maybe Bool
zi | Maybe Bool
xi forall a. Eq a => a -> a -> Bool
== Maybe Bool
yi = Maybe Bool
xi
           | Bool
otherwise = forall a. Maybe a
Nothing

ravCheckEq :: RealAbstractValue -> RealAbstractValue -> Maybe Bool
ravCheckEq :: RealAbstractValue -> RealAbstractValue -> Maybe Bool
ravCheckEq (RAV ValueRange Rational
xr Maybe Bool
_) (RAV ValueRange Rational
yr Maybe Bool
_) = forall tp. Ord tp => ValueRange tp -> ValueRange tp -> Maybe Bool
rangeCheckEq ValueRange Rational
xr ValueRange Rational
yr

ravCheckLe :: RealAbstractValue -> RealAbstractValue -> Maybe Bool
ravCheckLe :: RealAbstractValue -> RealAbstractValue -> Maybe Bool
ravCheckLe (RAV ValueRange Rational
xr Maybe Bool
_) (RAV ValueRange Rational
yr Maybe Bool
_) = forall tp. Ord tp => ValueRange tp -> ValueRange tp -> Maybe Bool
rangeCheckLe ValueRange Rational
xr ValueRange Rational
yr

-- Computing AbstractValue

absAnd :: Maybe Bool -> Maybe Bool -> Maybe Bool
absAnd :: Maybe Bool -> Maybe Bool -> Maybe Bool
absAnd (Just Bool
False) Maybe Bool
_ = forall a. a -> Maybe a
Just Bool
False
absAnd (Just Bool
True) Maybe Bool
y = Maybe Bool
y
absAnd Maybe Bool
_ (Just Bool
False) = forall a. a -> Maybe a
Just Bool
False
absAnd Maybe Bool
x (Just Bool
True) = Maybe Bool
x
absAnd Maybe Bool
Nothing Maybe Bool
Nothing = forall a. Maybe a
Nothing

absOr :: Maybe Bool -> Maybe Bool -> Maybe Bool
absOr :: Maybe Bool -> Maybe Bool -> Maybe Bool
absOr (Just Bool
False) Maybe Bool
y = Maybe Bool
y
absOr (Just Bool
True)  Maybe Bool
_ = forall a. a -> Maybe a
Just Bool
True
absOr Maybe Bool
x (Just Bool
False) = Maybe Bool
x
absOr Maybe Bool
_ (Just Bool
True)  = forall a. a -> Maybe a
Just Bool
True
absOr Maybe Bool
Nothing Maybe Bool
Nothing = forall a. Maybe a
Nothing


rangeMax :: Ord a => ValueRange a -> ValueRange a -> ValueRange a
rangeMax :: forall tp.
Ord tp =>
ValueRange tp -> ValueRange tp -> ValueRange tp
rangeMax ValueRange a
x ValueRange a
y = forall tp. Eq tp => ValueBound tp -> ValueBound tp -> ValueRange tp
valueRange ValueBound a
lo ValueBound a
hi
 where
 lo :: ValueBound a
lo = case (forall tp. ValueRange tp -> ValueBound tp
rangeLowBound ValueRange a
x, forall tp. ValueRange tp -> ValueBound tp
rangeLowBound ValueRange a
y) of
        (ValueBound a
Unbounded, ValueBound a
b) -> ValueBound a
b
        (ValueBound a
a, ValueBound a
Unbounded) -> ValueBound a
a
        (Inclusive a
a, Inclusive a
b) -> forall a. a -> ValueBound a
Inclusive (forall a. Ord a => a -> a -> a
max a
a a
b)

 hi :: ValueBound a
hi = case (forall tp. ValueRange tp -> ValueBound tp
rangeHiBound ValueRange a
x, forall tp. ValueRange tp -> ValueBound tp
rangeHiBound ValueRange a
y) of
         (ValueBound a
Unbounded, ValueBound a
_) -> forall tp. ValueBound tp
Unbounded
         (ValueBound a
_, ValueBound a
Unbounded) -> forall tp. ValueBound tp
Unbounded
         (Inclusive a
a, Inclusive a
b) -> forall a. a -> ValueBound a
Inclusive (forall a. Ord a => a -> a -> a
max a
a a
b)


rangeMin :: Ord a => ValueRange a -> ValueRange a -> ValueRange a
rangeMin :: forall tp.
Ord tp =>
ValueRange tp -> ValueRange tp -> ValueRange tp
rangeMin ValueRange a
x ValueRange a
y = forall tp. Eq tp => ValueBound tp -> ValueBound tp -> ValueRange tp
valueRange ValueBound a
lo ValueBound a
hi
 where
 lo :: ValueBound a
lo = case (forall tp. ValueRange tp -> ValueBound tp
rangeLowBound ValueRange a
x, forall tp. ValueRange tp -> ValueBound tp
rangeLowBound ValueRange a
y) of
        (ValueBound a
Unbounded, ValueBound a
_) -> forall tp. ValueBound tp
Unbounded
        (ValueBound a
_, ValueBound a
Unbounded) -> forall tp. ValueBound tp
Unbounded
        (Inclusive a
a, Inclusive a
b) -> forall a. a -> ValueBound a
Inclusive (forall a. Ord a => a -> a -> a
min a
a a
b)

 hi :: ValueBound a
hi = case (forall tp. ValueRange tp -> ValueBound tp
rangeHiBound ValueRange a
x, forall tp. ValueRange tp -> ValueBound tp
rangeHiBound ValueRange a
y) of
         (ValueBound a
Unbounded, ValueBound a
b) -> ValueBound a
b
         (ValueBound a
a, ValueBound a
Unbounded) -> ValueBound a
a
         (Inclusive a
a, Inclusive a
b) -> forall a. a -> ValueBound a
Inclusive (forall a. Ord a => a -> a -> a
min a
a a
b)


------------------------------------------------------
-- String abstract domain

-- | The string abstract domain tracks an interval
--   range for the length of the string.
newtype StringAbstractValue =
  StringAbs
  { StringAbstractValue -> ValueRange Integer
_stringAbsLength :: ValueRange Integer
     -- ^ The length of the string falls in this range
  }

stringAbsTop :: StringAbstractValue
stringAbsTop :: StringAbstractValue
stringAbsTop = ValueRange Integer -> StringAbstractValue
StringAbs (forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
MultiRange (forall a. a -> ValueBound a
Inclusive Integer
0) forall tp. ValueBound tp
Unbounded)

stringAbsEmpty :: StringAbstractValue
stringAbsEmpty :: StringAbstractValue
stringAbsEmpty = ValueRange Integer -> StringAbstractValue
StringAbs (forall tp. tp -> ValueRange tp
singleRange Integer
0)

stringAbsJoin :: StringAbstractValue -> StringAbstractValue -> StringAbstractValue
stringAbsJoin :: StringAbstractValue -> StringAbstractValue -> StringAbstractValue
stringAbsJoin (StringAbs ValueRange Integer
lenx) (StringAbs ValueRange Integer
leny) = ValueRange Integer -> StringAbstractValue
StringAbs (forall tp.
Ord tp =>
ValueRange tp -> ValueRange tp -> ValueRange tp
joinRange ValueRange Integer
lenx ValueRange Integer
leny)

stringAbsSingle :: StringLiteral si -> StringAbstractValue
stringAbsSingle :: forall (si :: StringInfo). StringLiteral si -> StringAbstractValue
stringAbsSingle StringLiteral si
lit = ValueRange Integer -> StringAbstractValue
StringAbs (forall tp. tp -> ValueRange tp
singleRange (forall a. Integral a => a -> Integer
toInteger (forall (si :: StringInfo). StringLiteral si -> Integer
stringLitLength StringLiteral si
lit)))

stringAbsOverlap :: StringAbstractValue -> StringAbstractValue -> Bool
stringAbsOverlap :: StringAbstractValue -> StringAbstractValue -> Bool
stringAbsOverlap (StringAbs ValueRange Integer
lenx) (StringAbs ValueRange Integer
leny) = forall tp. Ord tp => ValueRange tp -> ValueRange tp -> Bool
rangeOverlap ValueRange Integer
lenx ValueRange Integer
leny

stringAbsCheckEq :: StringAbstractValue -> StringAbstractValue -> Maybe Bool
stringAbsCheckEq :: StringAbstractValue -> StringAbstractValue -> Maybe Bool
stringAbsCheckEq (StringAbs ValueRange Integer
lenx) (StringAbs ValueRange Integer
leny)
  | Just Integer
0 <- forall tp. ValueRange tp -> Maybe tp
asSingleRange ValueRange Integer
lenx
  , Just Integer
0 <- forall tp. ValueRange tp -> Maybe tp
asSingleRange ValueRange Integer
leny
  = forall a. a -> Maybe a
Just Bool
True

  | Bool -> Bool
not (forall tp. Ord tp => ValueRange tp -> ValueRange tp -> Bool
rangeOverlap ValueRange Integer
lenx ValueRange Integer
leny)
  = forall a. a -> Maybe a
Just Bool
False

  | Bool
otherwise
  = forall a. Maybe a
Nothing

stringAbsConcat :: StringAbstractValue -> StringAbstractValue -> StringAbstractValue
stringAbsConcat :: StringAbstractValue -> StringAbstractValue -> StringAbstractValue
stringAbsConcat (StringAbs ValueRange Integer
lenx) (StringAbs ValueRange Integer
leny) = ValueRange Integer -> StringAbstractValue
StringAbs (forall tp.
Num tp =>
ValueRange tp -> ValueRange tp -> ValueRange tp
addRange ValueRange Integer
lenx ValueRange Integer
leny)

stringAbsSubstring :: StringAbstractValue -> ValueRange Integer -> ValueRange Integer -> StringAbstractValue
stringAbsSubstring :: StringAbstractValue
-> ValueRange Integer -> ValueRange Integer -> StringAbstractValue
stringAbsSubstring (StringAbs ValueRange Integer
s) ValueRange Integer
off ValueRange Integer
len
  -- empty string if len is negative
  | Just Bool
False <- forall tp. Ord tp => ValueRange tp -> ValueRange tp -> Maybe Bool
rangeCheckLe (forall tp. tp -> ValueRange tp
singleRange Integer
0) ValueRange Integer
len = ValueRange Integer -> StringAbstractValue
StringAbs (forall tp. tp -> ValueRange tp
singleRange Integer
0)
  -- empty string if off is negative
  | Just Bool
False <- forall tp. Ord tp => ValueRange tp -> ValueRange tp -> Maybe Bool
rangeCheckLe (forall tp. tp -> ValueRange tp
singleRange Integer
0) ValueRange Integer
off = ValueRange Integer -> StringAbstractValue
StringAbs (forall tp. tp -> ValueRange tp
singleRange Integer
0)
  -- empty string if off is out of bounds
  | Just Bool
True <- forall tp. Ord tp => ValueRange tp -> ValueRange tp -> Maybe Bool
rangeCheckLe ValueRange Integer
s ValueRange Integer
off = ValueRange Integer -> StringAbstractValue
StringAbs (forall tp. tp -> ValueRange tp
singleRange Integer
0)

  | Bool
otherwise =
      let -- clamp off at 0
          off' :: ValueRange Integer
off' = forall tp.
Ord tp =>
ValueRange tp -> ValueRange tp -> ValueRange tp
rangeMax (forall tp. tp -> ValueRange tp
singleRange Integer
0) ValueRange Integer
off
          -- clamp len at 0
          len' :: ValueRange Integer
len' = forall tp.
Ord tp =>
ValueRange tp -> ValueRange tp -> ValueRange tp
rangeMax (forall tp. tp -> ValueRange tp
singleRange Integer
0) ValueRange Integer
len
          -- subtract off' from the length of s, clamp to 0
          s' :: ValueRange Integer
s'   = forall tp.
Ord tp =>
ValueRange tp -> ValueRange tp -> ValueRange tp
rangeMax (forall tp. tp -> ValueRange tp
singleRange Integer
0) (forall tp.
Num tp =>
ValueRange tp -> ValueRange tp -> ValueRange tp
addRange ValueRange Integer
s (forall tp. Num tp => ValueRange tp -> ValueRange tp
negateRange ValueRange Integer
off'))
          -- result is the minimum of the length requested and the length
          -- of the string after removing the prefix
       in ValueRange Integer -> StringAbstractValue
StringAbs (forall tp.
Ord tp =>
ValueRange tp -> ValueRange tp -> ValueRange tp
rangeMin ValueRange Integer
len' ValueRange Integer
s')

stringAbsContains :: StringAbstractValue -> StringAbstractValue -> Maybe Bool
stringAbsContains :: StringAbstractValue -> StringAbstractValue -> Maybe Bool
stringAbsContains = StringAbstractValue -> StringAbstractValue -> Maybe Bool
couldContain

stringAbsIsPrefixOf :: StringAbstractValue -> StringAbstractValue -> Maybe Bool
stringAbsIsPrefixOf :: StringAbstractValue -> StringAbstractValue -> Maybe Bool
stringAbsIsPrefixOf = forall a b c. (a -> b -> c) -> b -> a -> c
flip StringAbstractValue -> StringAbstractValue -> Maybe Bool
couldContain

stringAbsIsSuffixOf :: StringAbstractValue -> StringAbstractValue -> Maybe Bool
stringAbsIsSuffixOf :: StringAbstractValue -> StringAbstractValue -> Maybe Bool
stringAbsIsSuffixOf = forall a b c. (a -> b -> c) -> b -> a -> c
flip StringAbstractValue -> StringAbstractValue -> Maybe Bool
couldContain

couldContain :: StringAbstractValue -> StringAbstractValue -> Maybe Bool
couldContain :: StringAbstractValue -> StringAbstractValue -> Maybe Bool
couldContain (StringAbs ValueRange Integer
lenx) (StringAbs ValueRange Integer
leny)
  | Just Bool
False <- forall tp. Ord tp => ValueRange tp -> ValueRange tp -> Maybe Bool
rangeCheckLe ValueRange Integer
leny ValueRange Integer
lenx = forall a. a -> Maybe a
Just Bool
False
  | Bool
otherwise = forall a. Maybe a
Nothing

stringAbsIndexOf :: StringAbstractValue -> StringAbstractValue -> ValueRange Integer -> ValueRange Integer
stringAbsIndexOf :: StringAbstractValue
-> StringAbstractValue -> ValueRange Integer -> ValueRange Integer
stringAbsIndexOf (StringAbs ValueRange Integer
lenx) (StringAbs ValueRange Integer
leny) ValueRange Integer
k
  | Just Bool
False <- forall tp. Ord tp => ValueRange tp -> ValueRange tp -> Maybe Bool
rangeCheckLe (forall tp. tp -> ValueRange tp
singleRange Integer
0) ValueRange Integer
k = forall tp. tp -> ValueRange tp
SingleRange (-Integer
1)
  | Just Bool
False <- forall tp. Ord tp => ValueRange tp -> ValueRange tp -> Maybe Bool
rangeCheckLe (forall tp.
Num tp =>
ValueRange tp -> ValueRange tp -> ValueRange tp
addRange ValueRange Integer
leny ValueRange Integer
k) ValueRange Integer
lenx = forall tp. tp -> ValueRange tp
SingleRange (-Integer
1)
  | Bool
otherwise = forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
MultiRange (forall a. a -> ValueBound a
Inclusive (-Integer
1)) (forall tp. ValueRange tp -> ValueBound tp
rangeHiBound ValueRange Integer
rng)

  where
  -- possible values that the final offset could have if the substring exists anywhere
  rng :: ValueRange Integer
rng = forall tp.
Ord tp =>
ValueRange tp -> ValueRange tp -> ValueRange tp
rangeMax (forall tp. tp -> ValueRange tp
singleRange Integer
0) (forall tp.
Num tp =>
ValueRange tp -> ValueRange tp -> ValueRange tp
addRange ValueRange Integer
lenx (forall tp. Num tp => ValueRange tp -> ValueRange tp
negateRange ValueRange Integer
leny))

stringAbsLength :: StringAbstractValue -> ValueRange Integer
stringAbsLength :: StringAbstractValue -> ValueRange Integer
stringAbsLength (StringAbs ValueRange Integer
len) = ValueRange Integer
len

-- | An abstract value represents a disjoint st of values.
type family AbstractValue (tp::BaseType) :: Type where
  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) = Ctx.Assignment AbstractValueWrapper ctx


-- | A utility class for values that contain abstract values
class HasAbsValue f where
  getAbsValue :: f tp -> AbstractValue tp

newtype AbstractValueWrapper tp
      = AbstractValueWrapper { forall (tp :: BaseType).
AbstractValueWrapper tp -> AbstractValue tp
unwrapAV :: AbstractValue tp }

type family ConcreteValue (tp::BaseType) :: Type where
  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) = Ctx.Assignment ConcreteValueWrapper ctx

newtype ConcreteValueWrapper tp
      = ConcreteValueWrapper { forall (tp :: BaseType).
ConcreteValueWrapper tp -> ConcreteValue tp
unwrapCV :: ConcreteValue tp }

-- | Create an abstract value that contains every concrete value.
avTop :: BaseTypeRepr tp -> AbstractValue tp
avTop :: forall (tp :: BaseType). BaseTypeRepr tp -> AbstractValue tp
avTop BaseTypeRepr tp
tp =
  case BaseTypeRepr tp
tp of
    BaseTypeRepr tp
BaseBoolRepr    -> forall a. Maybe a
Nothing
    BaseTypeRepr tp
BaseIntegerRepr -> forall tp. ValueRange tp
unboundedRange
    BaseTypeRepr tp
BaseRealRepr    -> RealAbstractValue
ravUnbounded
    BaseTypeRepr tp
BaseComplexRepr -> RealAbstractValue
ravUnbounded forall a. a -> a -> Complex a
:+ RealAbstractValue
ravUnbounded
    BaseStringRepr StringInfoRepr si
_ -> StringAbstractValue
stringAbsTop
    BaseBVRepr NatRepr w
w    -> forall (w :: Natural). (1 <= w) => NatRepr w -> BVDomain w
BVD.any NatRepr w
w
    BaseFloatRepr{} -> ()
    BaseArrayRepr Assignment BaseTypeRepr (idx ::> tp)
_a BaseTypeRepr xs
b -> forall (tp :: BaseType). BaseTypeRepr tp -> AbstractValue tp
avTop BaseTypeRepr xs
b
    BaseStructRepr Assignment BaseTypeRepr ctx
flds -> forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type).
FunctorFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
fmapFC (\BaseTypeRepr x
etp -> forall (tp :: BaseType).
AbstractValue tp -> AbstractValueWrapper tp
AbstractValueWrapper (forall (tp :: BaseType). BaseTypeRepr tp -> AbstractValue tp
avTop BaseTypeRepr x
etp)) Assignment BaseTypeRepr ctx
flds

-- | Create an abstract value that contains the given concrete value.
avSingle :: BaseTypeRepr tp -> ConcreteValue tp -> AbstractValue tp
avSingle :: forall (tp :: BaseType).
BaseTypeRepr tp -> ConcreteValue tp -> AbstractValue tp
avSingle BaseTypeRepr tp
tp =
  case BaseTypeRepr tp
tp of
    BaseTypeRepr tp
BaseBoolRepr -> forall a. a -> Maybe a
Just
    BaseTypeRepr tp
BaseIntegerRepr -> forall tp. tp -> ValueRange tp
singleRange
    BaseTypeRepr tp
BaseRealRepr -> Rational -> RealAbstractValue
ravSingle
    BaseStringRepr StringInfoRepr si
_ -> forall (si :: StringInfo). StringLiteral si -> StringAbstractValue
stringAbsSingle
    BaseTypeRepr tp
BaseComplexRepr -> forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Rational -> RealAbstractValue
ravSingle
    BaseBVRepr NatRepr w
w -> forall (w :: Natural).
(?callStack::CallStack, 1 <= w) =>
NatRepr w -> Integer -> BVDomain w
BVD.singleton NatRepr w
w
    BaseFloatRepr FloatPrecisionRepr fpp
_ -> \ConcreteValue tp
_ -> ()
    BaseArrayRepr Assignment BaseTypeRepr (idx ::> tp)
_a BaseTypeRepr xs
b -> \ConcreteValue tp
_ -> forall (tp :: BaseType). BaseTypeRepr tp -> AbstractValue tp
avTop BaseTypeRepr xs
b
    BaseStructRepr Assignment BaseTypeRepr ctx
flds -> \ConcreteValue tp
vals ->
      forall {k} (f :: k -> Type) (g :: k -> Type) (h :: k -> Type)
       (a :: Ctx k).
(forall (x :: k). f x -> g x -> h x)
-> Assignment f a -> Assignment g a -> Assignment h a
Ctx.zipWith
        (\BaseTypeRepr x
ftp ConcreteValueWrapper x
v -> forall (tp :: BaseType).
AbstractValue tp -> AbstractValueWrapper tp
AbstractValueWrapper (forall (tp :: BaseType).
BaseTypeRepr tp -> ConcreteValue tp -> AbstractValue tp
avSingle BaseTypeRepr x
ftp (forall (tp :: BaseType).
ConcreteValueWrapper tp -> ConcreteValue tp
unwrapCV ConcreteValueWrapper x
v)))
        Assignment BaseTypeRepr ctx
flds
        ConcreteValue tp
vals

------------------------------------------------------------------------
-- Abstractable

class Abstractable (tp::BaseType) where

  -- | Take the union of the two abstract values.
  avJoin     :: BaseTypeRepr tp -> AbstractValue tp -> AbstractValue tp -> AbstractValue tp

  -- | Returns true if the abstract values could contain a common concrete
  -- value.
  avOverlap  :: BaseTypeRepr tp -> AbstractValue tp -> AbstractValue tp -> 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.
  avCheckEq :: BaseTypeRepr tp -> AbstractValue tp -> AbstractValue tp -> Maybe Bool

avJoin' :: BaseTypeRepr tp
        -> AbstractValueWrapper tp
        -> AbstractValueWrapper tp
        -> AbstractValueWrapper tp
avJoin' :: forall (tp :: BaseType).
BaseTypeRepr tp
-> AbstractValueWrapper tp
-> AbstractValueWrapper tp
-> AbstractValueWrapper tp
avJoin' BaseTypeRepr tp
tp AbstractValueWrapper tp
x AbstractValueWrapper tp
y = forall (bt :: BaseType) a.
BaseTypeRepr bt -> (Abstractable bt => a) -> a
withAbstractable BaseTypeRepr tp
tp forall a b. (a -> b) -> a -> b
$
  forall (tp :: BaseType).
AbstractValue tp -> AbstractValueWrapper tp
AbstractValueWrapper forall a b. (a -> b) -> a -> b
$ forall (tp :: BaseType).
Abstractable tp =>
BaseTypeRepr tp
-> AbstractValue tp -> AbstractValue tp -> AbstractValue tp
avJoin BaseTypeRepr tp
tp (forall (tp :: BaseType).
AbstractValueWrapper tp -> AbstractValue tp
unwrapAV AbstractValueWrapper tp
x) (forall (tp :: BaseType).
AbstractValueWrapper tp -> AbstractValue tp
unwrapAV AbstractValueWrapper tp
y)

-- Abstraction captures whether Boolean is constant true or false or Nothing
instance Abstractable BaseBoolType where
  avJoin :: BaseTypeRepr 'BaseBoolType
-> AbstractValue 'BaseBoolType
-> AbstractValue 'BaseBoolType
-> AbstractValue 'BaseBoolType
avJoin BaseTypeRepr 'BaseBoolType
_ AbstractValue 'BaseBoolType
x AbstractValue 'BaseBoolType
y | AbstractValue 'BaseBoolType
x forall a. Eq a => a -> a -> Bool
== AbstractValue 'BaseBoolType
y = AbstractValue 'BaseBoolType
x
               | Bool
otherwise = forall a. Maybe a
Nothing

  avOverlap :: BaseTypeRepr 'BaseBoolType
-> AbstractValue 'BaseBoolType
-> AbstractValue 'BaseBoolType
-> Bool
avOverlap BaseTypeRepr 'BaseBoolType
_ (Just Bool
x) (Just Bool
y) | Bool
x forall a. Eq a => a -> a -> Bool
/= Bool
y = Bool
False
  avOverlap BaseTypeRepr 'BaseBoolType
_ AbstractValue 'BaseBoolType
_ AbstractValue 'BaseBoolType
_ = Bool
True

  avCheckEq :: BaseTypeRepr 'BaseBoolType
-> AbstractValue 'BaseBoolType
-> AbstractValue 'BaseBoolType
-> Maybe Bool
avCheckEq BaseTypeRepr 'BaseBoolType
_ (Just Bool
x) (Just Bool
y) = forall a. a -> Maybe a
Just (Bool
x forall a. Eq a => a -> a -> Bool
== Bool
y)
  avCheckEq BaseTypeRepr 'BaseBoolType
_ AbstractValue 'BaseBoolType
_ AbstractValue 'BaseBoolType
_ = forall a. Maybe a
Nothing

instance Abstractable (BaseStringType si) where
  avJoin :: BaseTypeRepr (BaseStringType si)
-> AbstractValue (BaseStringType si)
-> AbstractValue (BaseStringType si)
-> AbstractValue (BaseStringType si)
avJoin BaseTypeRepr (BaseStringType si)
_     = StringAbstractValue -> StringAbstractValue -> StringAbstractValue
stringAbsJoin
  avOverlap :: BaseTypeRepr (BaseStringType si)
-> AbstractValue (BaseStringType si)
-> AbstractValue (BaseStringType si)
-> Bool
avOverlap BaseTypeRepr (BaseStringType si)
_  = StringAbstractValue -> StringAbstractValue -> Bool
stringAbsOverlap
  avCheckEq :: BaseTypeRepr (BaseStringType si)
-> AbstractValue (BaseStringType si)
-> AbstractValue (BaseStringType si)
-> Maybe Bool
avCheckEq BaseTypeRepr (BaseStringType si)
_  = StringAbstractValue -> StringAbstractValue -> Maybe Bool
stringAbsCheckEq

-- Integers have a lower and upper bound associated with them.
instance Abstractable BaseIntegerType where
  avJoin :: BaseTypeRepr 'BaseIntegerType
-> AbstractValue 'BaseIntegerType
-> AbstractValue 'BaseIntegerType
-> AbstractValue 'BaseIntegerType
avJoin BaseTypeRepr 'BaseIntegerType
_ = forall tp.
Ord tp =>
ValueRange tp -> ValueRange tp -> ValueRange tp
joinRange
  avOverlap :: BaseTypeRepr 'BaseIntegerType
-> AbstractValue 'BaseIntegerType
-> AbstractValue 'BaseIntegerType
-> Bool
avOverlap BaseTypeRepr 'BaseIntegerType
_ = forall tp. Ord tp => ValueRange tp -> ValueRange tp -> Bool
rangeOverlap
  avCheckEq :: BaseTypeRepr 'BaseIntegerType
-> AbstractValue 'BaseIntegerType
-> AbstractValue 'BaseIntegerType
-> Maybe Bool
avCheckEq BaseTypeRepr 'BaseIntegerType
_ = forall tp. Ord tp => ValueRange tp -> ValueRange tp -> Maybe Bool
rangeCheckEq

-- Real numbers  have a lower and upper bound associated with them.
instance Abstractable BaseRealType where
  avJoin :: BaseTypeRepr 'BaseRealType
-> AbstractValue 'BaseRealType
-> AbstractValue 'BaseRealType
-> AbstractValue 'BaseRealType
avJoin BaseTypeRepr 'BaseRealType
_ = RealAbstractValue -> RealAbstractValue -> RealAbstractValue
ravJoin
  avOverlap :: BaseTypeRepr 'BaseRealType
-> AbstractValue 'BaseRealType
-> AbstractValue 'BaseRealType
-> Bool
avOverlap BaseTypeRepr 'BaseRealType
_ AbstractValue 'BaseRealType
x AbstractValue 'BaseRealType
y = forall tp. Ord tp => ValueRange tp -> ValueRange tp -> Bool
rangeOverlap (RealAbstractValue -> ValueRange Rational
ravRange AbstractValue 'BaseRealType
x) (RealAbstractValue -> ValueRange Rational
ravRange AbstractValue 'BaseRealType
y)
  avCheckEq :: BaseTypeRepr 'BaseRealType
-> AbstractValue 'BaseRealType
-> AbstractValue 'BaseRealType
-> Maybe Bool
avCheckEq BaseTypeRepr 'BaseRealType
_ = RealAbstractValue -> RealAbstractValue -> Maybe Bool
ravCheckEq

-- Bitvectors always have a lower and upper bound (represented as unsigned numbers)
instance (1 <= w) => Abstractable (BaseBVType w) where
  avJoin :: BaseTypeRepr (BaseBVType w)
-> AbstractValue (BaseBVType w)
-> AbstractValue (BaseBVType w)
-> AbstractValue (BaseBVType w)
avJoin (BaseBVRepr NatRepr w
_) = forall (w :: Natural).
(1 <= w) =>
BVDomain w -> BVDomain w -> BVDomain w
BVD.union
  avOverlap :: BaseTypeRepr (BaseBVType w)
-> AbstractValue (BaseBVType w)
-> AbstractValue (BaseBVType w)
-> Bool
avOverlap BaseTypeRepr (BaseBVType w)
_ = forall (w :: Natural). BVDomain w -> BVDomain w -> Bool
BVD.domainsOverlap
  avCheckEq :: BaseTypeRepr (BaseBVType w)
-> AbstractValue (BaseBVType w)
-> AbstractValue (BaseBVType w)
-> Maybe Bool
avCheckEq BaseTypeRepr (BaseBVType w)
_ = forall (w :: Natural). BVDomain w -> BVDomain w -> Maybe Bool
BVD.eq

instance Abstractable (BaseFloatType fpp) where
  avJoin :: BaseTypeRepr (BaseFloatType fpp)
-> AbstractValue (BaseFloatType fpp)
-> AbstractValue (BaseFloatType fpp)
-> AbstractValue (BaseFloatType fpp)
avJoin BaseTypeRepr (BaseFloatType fpp)
_ AbstractValue (BaseFloatType fpp)
_ AbstractValue (BaseFloatType fpp)
_ = ()
  avOverlap :: BaseTypeRepr (BaseFloatType fpp)
-> AbstractValue (BaseFloatType fpp)
-> AbstractValue (BaseFloatType fpp)
-> Bool
avOverlap BaseTypeRepr (BaseFloatType fpp)
_ AbstractValue (BaseFloatType fpp)
_ AbstractValue (BaseFloatType fpp)
_ = Bool
True
  avCheckEq :: BaseTypeRepr (BaseFloatType fpp)
-> AbstractValue (BaseFloatType fpp)
-> AbstractValue (BaseFloatType fpp)
-> Maybe Bool
avCheckEq BaseTypeRepr (BaseFloatType fpp)
_ AbstractValue (BaseFloatType fpp)
_ AbstractValue (BaseFloatType fpp)
_ = forall a. Maybe a
Nothing

instance Abstractable BaseComplexType where
  avJoin :: BaseTypeRepr 'BaseComplexType
-> AbstractValue 'BaseComplexType
-> AbstractValue 'BaseComplexType
-> AbstractValue 'BaseComplexType
avJoin BaseTypeRepr 'BaseComplexType
_ (RealAbstractValue
r1 :+ RealAbstractValue
i1) (RealAbstractValue
r2 :+ RealAbstractValue
i2) = (RealAbstractValue -> RealAbstractValue -> RealAbstractValue
ravJoin RealAbstractValue
r1 RealAbstractValue
r2) forall a. a -> a -> Complex a
:+ (RealAbstractValue -> RealAbstractValue -> RealAbstractValue
ravJoin RealAbstractValue
i1 RealAbstractValue
i2)
  avOverlap :: BaseTypeRepr 'BaseComplexType
-> AbstractValue 'BaseComplexType
-> AbstractValue 'BaseComplexType
-> Bool
avOverlap BaseTypeRepr 'BaseComplexType
_ (RealAbstractValue
r1 :+ RealAbstractValue
i1) (RealAbstractValue
r2 :+ RealAbstractValue
i2) = forall tp. Ord tp => ValueRange tp -> ValueRange tp -> Bool
rangeOverlap (RealAbstractValue -> ValueRange Rational
ravRange RealAbstractValue
r1) (RealAbstractValue -> ValueRange Rational
ravRange RealAbstractValue
r2)
                                   Bool -> Bool -> Bool
&& forall tp. Ord tp => ValueRange tp -> ValueRange tp -> Bool
rangeOverlap (RealAbstractValue -> ValueRange Rational
ravRange RealAbstractValue
i1) (RealAbstractValue -> ValueRange Rational
ravRange RealAbstractValue
i2)
  avCheckEq :: BaseTypeRepr 'BaseComplexType
-> AbstractValue 'BaseComplexType
-> AbstractValue 'BaseComplexType
-> Maybe Bool
avCheckEq BaseTypeRepr 'BaseComplexType
_ (RealAbstractValue
r1 :+ RealAbstractValue
i1) (RealAbstractValue
r2 :+ RealAbstractValue
i2)
    = Maybe Bool -> Maybe Bool -> Maybe Bool
combineEqCheck
        (forall tp. Ord tp => ValueRange tp -> ValueRange tp -> Maybe Bool
rangeCheckEq (RealAbstractValue -> ValueRange Rational
ravRange RealAbstractValue
r1) (RealAbstractValue -> ValueRange Rational
ravRange RealAbstractValue
r2))
        (forall tp. Ord tp => ValueRange tp -> ValueRange tp -> Maybe Bool
rangeCheckEq (RealAbstractValue -> ValueRange Rational
ravRange RealAbstractValue
i1) (RealAbstractValue -> ValueRange Rational
ravRange RealAbstractValue
i2))

instance Abstractable (BaseArrayType idx b) where
  avJoin :: BaseTypeRepr (BaseArrayType idx b)
-> AbstractValue (BaseArrayType idx b)
-> AbstractValue (BaseArrayType idx b)
-> AbstractValue (BaseArrayType idx b)
avJoin (BaseArrayRepr Assignment BaseTypeRepr (idx ::> tp)
_ BaseTypeRepr xs
b) AbstractValue (BaseArrayType idx b)
x AbstractValue (BaseArrayType idx b)
y = forall (bt :: BaseType) a.
BaseTypeRepr bt -> (Abstractable bt => a) -> a
withAbstractable BaseTypeRepr xs
b forall a b. (a -> b) -> a -> b
$ forall (tp :: BaseType).
Abstractable tp =>
BaseTypeRepr tp
-> AbstractValue tp -> AbstractValue tp -> AbstractValue tp
avJoin BaseTypeRepr xs
b AbstractValue (BaseArrayType idx b)
x AbstractValue (BaseArrayType idx b)
y
  avOverlap :: BaseTypeRepr (BaseArrayType idx b)
-> AbstractValue (BaseArrayType idx b)
-> AbstractValue (BaseArrayType idx b)
-> Bool
avOverlap (BaseArrayRepr Assignment BaseTypeRepr (idx ::> tp)
_ BaseTypeRepr xs
b) AbstractValue (BaseArrayType idx b)
x AbstractValue (BaseArrayType idx b)
y = forall (bt :: BaseType) a.
BaseTypeRepr bt -> (Abstractable bt => a) -> a
withAbstractable BaseTypeRepr xs
b forall a b. (a -> b) -> a -> b
$ forall (tp :: BaseType).
Abstractable tp =>
BaseTypeRepr tp -> AbstractValue tp -> AbstractValue tp -> Bool
avOverlap BaseTypeRepr xs
b AbstractValue (BaseArrayType idx b)
x AbstractValue (BaseArrayType idx b)
y
  avCheckEq :: BaseTypeRepr (BaseArrayType idx b)
-> AbstractValue (BaseArrayType idx b)
-> AbstractValue (BaseArrayType idx b)
-> Maybe Bool
avCheckEq (BaseArrayRepr Assignment BaseTypeRepr (idx ::> tp)
_ BaseTypeRepr xs
b) AbstractValue (BaseArrayType idx b)
x AbstractValue (BaseArrayType idx b)
y = forall (bt :: BaseType) a.
BaseTypeRepr bt -> (Abstractable bt => a) -> a
withAbstractable BaseTypeRepr xs
b forall a b. (a -> b) -> a -> b
$ forall (tp :: BaseType).
Abstractable tp =>
BaseTypeRepr tp
-> AbstractValue tp -> AbstractValue tp -> Maybe Bool
avCheckEq BaseTypeRepr xs
b AbstractValue (BaseArrayType idx b)
x AbstractValue (BaseArrayType idx b)
y

combineEqCheck :: Maybe Bool -> Maybe Bool -> Maybe Bool
combineEqCheck :: Maybe Bool -> Maybe Bool -> Maybe Bool
combineEqCheck (Just Bool
False) Maybe Bool
_ = forall a. a -> Maybe a
Just Bool
False
combineEqCheck (Just Bool
True)  Maybe Bool
y = Maybe Bool
y
combineEqCheck Maybe Bool
_ (Just Bool
False) = forall a. a -> Maybe a
Just Bool
False
combineEqCheck Maybe Bool
x (Just Bool
True)  = Maybe Bool
x
combineEqCheck Maybe Bool
_ Maybe Bool
_            = forall a. Maybe a
Nothing

instance Abstractable (BaseStructType ctx) where
  avJoin :: BaseTypeRepr (BaseStructType ctx)
-> AbstractValue (BaseStructType ctx)
-> AbstractValue (BaseStructType ctx)
-> AbstractValue (BaseStructType ctx)
avJoin (BaseStructRepr Assignment BaseTypeRepr ctx
flds) AbstractValue (BaseStructType ctx)
x AbstractValue (BaseStructType ctx)
y = forall k (a :: k -> Type) (b :: k -> Type) (c :: k -> Type)
       (d :: k -> Type) (ctx :: Ctx k).
(forall (x :: k). a x -> b x -> c x -> d x)
-> Assignment a ctx
-> Assignment b ctx
-> Assignment c ctx
-> Assignment d ctx
ctxZipWith3 forall (tp :: BaseType).
BaseTypeRepr tp
-> AbstractValueWrapper tp
-> AbstractValueWrapper tp
-> AbstractValueWrapper tp
avJoin' Assignment BaseTypeRepr ctx
flds AbstractValue (BaseStructType ctx)
x AbstractValue (BaseStructType ctx)
y
  avOverlap :: BaseTypeRepr (BaseStructType ctx)
-> AbstractValue (BaseStructType ctx)
-> AbstractValue (BaseStructType ctx)
-> Bool
avOverlap (BaseStructRepr Assignment BaseTypeRepr ctx
flds) AbstractValue (BaseStructType ctx)
x AbstractValue (BaseStructType ctx)
y = forall {k} (ctx :: Ctx k) r.
Size ctx -> (forall (tp :: k). r -> Index ctx tp -> r) -> r -> r
Ctx.forIndex (forall {k} (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
Ctx.size Assignment BaseTypeRepr ctx
flds) forall (tp :: BaseType). Bool -> Index ctx tp -> Bool
f Bool
True
    where f :: Bool -> Ctx.Index ctx tp -> Bool
          f :: forall (tp :: BaseType). Bool -> Index ctx tp -> Bool
f Bool
b Index ctx tp
i = forall (bt :: BaseType) a.
BaseTypeRepr bt -> (Abstractable bt => a) -> a
withAbstractable BaseTypeRepr tp
tp (forall (tp :: BaseType).
Abstractable tp =>
BaseTypeRepr tp -> AbstractValue tp -> AbstractValue tp -> Bool
avOverlap BaseTypeRepr tp
tp (forall (tp :: BaseType).
AbstractValueWrapper tp -> AbstractValue tp
unwrapAV AbstractValueWrapper tp
u) (forall (tp :: BaseType).
AbstractValueWrapper tp -> AbstractValue tp
unwrapAV AbstractValueWrapper tp
v)) Bool -> Bool -> Bool
&& Bool
b
            where tp :: BaseTypeRepr tp
tp = Assignment BaseTypeRepr ctx
flds forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index ctx tp
i
                  u :: AbstractValueWrapper tp
u  = AbstractValue (BaseStructType ctx)
x forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index ctx tp
i
                  v :: AbstractValueWrapper tp
v  = AbstractValue (BaseStructType ctx)
y forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index ctx tp
i

  avCheckEq :: BaseTypeRepr (BaseStructType ctx)
-> AbstractValue (BaseStructType ctx)
-> AbstractValue (BaseStructType ctx)
-> Maybe Bool
avCheckEq (BaseStructRepr Assignment BaseTypeRepr ctx
flds) AbstractValue (BaseStructType ctx)
x AbstractValue (BaseStructType ctx)
y = forall {k} (ctx :: Ctx k) r.
Size ctx -> (forall (tp :: k). r -> Index ctx tp -> r) -> r -> r
Ctx.forIndex (forall {k} (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
Ctx.size Assignment BaseTypeRepr ctx
flds) forall (tp :: BaseType). Maybe Bool -> Index ctx tp -> Maybe Bool
f (forall a. a -> Maybe a
Just Bool
True)
    where f :: Maybe Bool -> Ctx.Index ctx tp -> Maybe Bool
          f :: forall (tp :: BaseType). Maybe Bool -> Index ctx tp -> Maybe Bool
f Maybe Bool
b Index ctx tp
i = Maybe Bool -> Maybe Bool -> Maybe Bool
combineEqCheck Maybe Bool
b (forall (bt :: BaseType) a.
BaseTypeRepr bt -> (Abstractable bt => a) -> a
withAbstractable BaseTypeRepr tp
tp (forall (tp :: BaseType).
Abstractable tp =>
BaseTypeRepr tp
-> AbstractValue tp -> AbstractValue tp -> Maybe Bool
avCheckEq BaseTypeRepr tp
tp (forall (tp :: BaseType).
AbstractValueWrapper tp -> AbstractValue tp
unwrapAV AbstractValueWrapper tp
u) (forall (tp :: BaseType).
AbstractValueWrapper tp -> AbstractValue tp
unwrapAV AbstractValueWrapper tp
v)))
            where tp :: BaseTypeRepr tp
tp = Assignment BaseTypeRepr ctx
flds forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index ctx tp
i
                  u :: AbstractValueWrapper tp
u  = AbstractValue (BaseStructType ctx)
x forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index ctx tp
i
                  v :: AbstractValueWrapper tp
v  = AbstractValue (BaseStructType ctx)
y forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index ctx tp
i

withAbstractable
   :: BaseTypeRepr bt
   -> (Abstractable bt => a)
   -> a
withAbstractable :: forall (bt :: BaseType) a.
BaseTypeRepr bt -> (Abstractable bt => a) -> a
withAbstractable BaseTypeRepr bt
bt Abstractable bt => a
k =
  case BaseTypeRepr bt
bt of
    BaseTypeRepr bt
BaseBoolRepr -> Abstractable bt => a
k
    BaseBVRepr NatRepr w
_w -> Abstractable bt => a
k
    BaseTypeRepr bt
BaseIntegerRepr -> Abstractable bt => a
k
    BaseStringRepr StringInfoRepr si
_ -> Abstractable bt => a
k
    BaseTypeRepr bt
BaseRealRepr -> Abstractable bt => a
k
    BaseTypeRepr bt
BaseComplexRepr -> Abstractable bt => a
k
    BaseArrayRepr Assignment BaseTypeRepr (idx ::> tp)
_a BaseTypeRepr xs
_b -> Abstractable bt => a
k
    BaseStructRepr Assignment BaseTypeRepr ctx
_flds -> Abstractable bt => a
k
    BaseFloatRepr FloatPrecisionRepr fpp
_fpp -> Abstractable bt => a
k

-- | Returns true if the concrete value is a member of the set represented
-- by the abstract value.
avContains :: BaseTypeRepr tp -> ConcreteValue tp -> AbstractValue tp -> Bool
avContains :: forall (tp :: BaseType).
BaseTypeRepr tp -> ConcreteValue tp -> AbstractValue tp -> Bool
avContains BaseTypeRepr tp
tp = forall (bt :: BaseType) a.
BaseTypeRepr bt -> (Abstractable bt => a) -> a
withAbstractable BaseTypeRepr tp
tp forall a b. (a -> b) -> a -> b
$ \ConcreteValue tp
x AbstractValue tp
y -> forall (tp :: BaseType).
Abstractable tp =>
BaseTypeRepr tp -> AbstractValue tp -> AbstractValue tp -> Bool
avOverlap BaseTypeRepr tp
tp (forall (tp :: BaseType).
BaseTypeRepr tp -> ConcreteValue tp -> AbstractValue tp
avSingle BaseTypeRepr tp
tp ConcreteValue tp
x) AbstractValue tp
y