{-|
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 PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

module What4.Utils.AbstractDomains
  ( ValueBound(..)
  , minValueBound
  , maxValueBound
    -- * ValueRange
  , ValueRange(..)
  , 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 (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 =
  Size ctx
-> (forall (tp :: k). Index ctx tp -> d tp) -> Assignment d ctx
forall k (ctx :: Ctx k) (f :: k -> Type).
Size ctx
-> (forall (tp :: k). Index ctx tp -> f tp) -> Assignment f ctx
Ctx.generate (Assignment a ctx -> Size ctx
forall k (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
Ctx.size Assignment a ctx
a) ((forall (tp :: k). Index ctx tp -> d tp) -> Assignment d ctx)
-> (forall (tp :: k). Index ctx tp -> d tp) -> Assignment d ctx
forall a b. (a -> b) -> a -> b
$ \Index ctx tp
i ->
    a tp -> b tp -> c tp -> d tp
forall (x :: k). a x -> b x -> c x -> d x
f (Assignment a ctx
a Assignment a ctx -> Index ctx tp -> a tp
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 Assignment b ctx -> Index ctx tp -> b tp
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 Assignment c ctx -> Index ctx tp -> c tp
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 (a -> ValueBound b -> ValueBound a
(a -> b) -> ValueBound a -> ValueBound b
(forall a b. (a -> b) -> ValueBound a -> ValueBound b)
-> (forall a b. a -> ValueBound b -> ValueBound a)
-> Functor ValueBound
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
<$ :: a -> ValueBound b -> ValueBound a
$c<$ :: forall a b. a -> ValueBound b -> ValueBound a
fmap :: (a -> b) -> ValueBound a -> ValueBound b
$cfmap :: forall a b. (a -> b) -> ValueBound a -> ValueBound b
Functor, Int -> ValueBound tp -> ShowS
[ValueBound tp] -> ShowS
ValueBound tp -> String
(Int -> ValueBound tp -> ShowS)
-> (ValueBound tp -> String)
-> ([ValueBound tp] -> ShowS)
-> Show (ValueBound tp)
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
(ValueBound tp -> ValueBound tp -> Bool)
-> (ValueBound tp -> ValueBound tp -> Bool) -> Eq (ValueBound tp)
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, Eq (ValueBound tp)
Eq (ValueBound tp)
-> (ValueBound tp -> ValueBound tp -> Ordering)
-> (ValueBound tp -> ValueBound tp -> Bool)
-> (ValueBound tp -> ValueBound tp -> Bool)
-> (ValueBound tp -> ValueBound tp -> Bool)
-> (ValueBound tp -> ValueBound tp -> Bool)
-> (ValueBound tp -> ValueBound tp -> ValueBound tp)
-> (ValueBound tp -> ValueBound tp -> ValueBound tp)
-> Ord (ValueBound tp)
ValueBound tp -> ValueBound tp -> Bool
ValueBound tp -> ValueBound tp -> Ordering
ValueBound tp -> ValueBound tp -> ValueBound tp
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
$cp1Ord :: forall tp. Ord tp => Eq (ValueBound tp)
Ord)

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

instance Monad ValueBound where
  return :: a -> ValueBound a
return = a -> ValueBound a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure
  ValueBound a
Unbounded >>= :: ValueBound a -> (a -> ValueBound b) -> ValueBound b
>>= a -> ValueBound b
_ = 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 :: ValueBound tp -> ValueBound tp -> ValueBound tp
minValueBound ValueBound tp
x ValueBound tp
y = tp -> tp -> tp
forall a. Ord a => a -> a -> a
min (tp -> tp -> tp) -> ValueBound tp -> ValueBound (tp -> tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueBound tp
x ValueBound (tp -> tp) -> ValueBound tp -> ValueBound tp
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 :: ValueBound tp -> ValueBound tp -> ValueBound tp
maxValueBound ValueBound tp
x ValueBound tp
y = tp -> tp -> tp
forall a. Ord a => a -> a -> a
max (tp -> tp -> tp) -> ValueBound tp -> ValueBound (tp -> tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueBound tp
x ValueBound (tp -> tp) -> ValueBound tp -> ValueBound tp
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 :: ValueBound tp -> Bool
lowerBoundIsNegative ValueBound tp
Unbounded = Bool
True
lowerBoundIsNegative (Inclusive tp
y) = tp
y tp -> tp -> Bool
forall a. Ord a => a -> a -> Bool
<= tp
0

upperBoundIsNonNeg :: (Ord tp, Num tp) => ValueBound tp -> Bool
upperBoundIsNonNeg :: ValueBound tp -> Bool
upperBoundIsNonNeg ValueBound tp
Unbounded = Bool
True
upperBoundIsNonNeg (Inclusive tp
y) = tp
y tp -> tp -> Bool
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
  | MultiRange !(ValueBound tp) !(ValueBound tp)
    -- ^ Indicates that the number is somewhere between the given upper and lower bound.

intAbsRange :: ValueRange Integer -> ValueRange Integer
intAbsRange :: ValueRange Integer -> ValueRange Integer
intAbsRange ValueRange Integer
r = case ValueRange Integer
r of
  SingleRange Integer
x -> Integer -> ValueRange Integer
forall tp. tp -> ValueRange tp
SingleRange (Integer -> Integer
forall a. Num a => a -> a
abs Integer
x)
  MultiRange (Inclusive Integer
lo) ValueBound Integer
hi | Integer
0 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
lo -> ValueBound Integer -> ValueBound Integer -> ValueRange Integer
forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
MultiRange (Integer -> ValueBound Integer
forall a. a -> ValueBound a
Inclusive Integer
lo) ValueBound Integer
hi
  MultiRange ValueBound Integer
lo (Inclusive Integer
hi) | Integer
hi Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
0 -> ValueBound Integer -> ValueBound Integer -> ValueRange Integer
forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
MultiRange (Integer -> ValueBound Integer
forall a. a -> ValueBound a
Inclusive (Integer -> Integer
forall a. Num a => a -> a
negate Integer
hi)) (Integer -> Integer
forall a. Num a => a -> a
negate (Integer -> Integer) -> ValueBound Integer -> ValueBound Integer
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueBound Integer
lo)
  MultiRange ValueBound Integer
lo ValueBound Integer
hi -> ValueBound Integer -> ValueBound Integer -> ValueRange Integer
forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
MultiRange (Integer -> ValueBound Integer
forall a. a -> ValueBound a
Inclusive Integer
0) ((\Integer
x Integer
y -> Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max (Integer -> Integer
forall a. Num a => a -> a
abs Integer
x) (Integer -> Integer
forall a. Num a => a -> a
abs Integer
y)) (Integer -> Integer -> Integer)
-> ValueBound Integer -> ValueBound (Integer -> Integer)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueBound Integer
lo ValueBound (Integer -> Integer)
-> ValueBound Integer -> ValueBound Integer
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> ValueBound 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 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0  = Integer -> ValueRange Integer
forall tp. tp -> ValueRange tp
SingleRange (Integer
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
y)
  | Integer
y Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0  = Integer -> ValueRange Integer
forall tp. tp -> ValueRange tp
SingleRange (Integer -> Integer
forall a. Num a => a -> a
negate (Integer
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer -> Integer
forall a. Num a => a -> a
negate Integer
y))
intDivRange (MultiRange ValueBound Integer
lo ValueBound Integer
hi) (SingleRange Integer
y)
  | Integer
y Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>  Integer
0 = ValueBound Integer -> ValueBound Integer -> ValueRange Integer
forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
MultiRange
                   ((\Integer
x -> Integer
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
y) (Integer -> Integer) -> ValueBound Integer -> ValueBound Integer
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueBound Integer
lo)
                   ((\Integer
x -> Integer
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
y) (Integer -> Integer) -> ValueBound Integer -> ValueBound Integer
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueBound Integer
hi)
  | Integer
y Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<  Integer
0 = ValueRange Integer -> ValueRange Integer
forall tp. Num tp => ValueRange tp -> ValueRange tp
negateRange (ValueRange Integer -> ValueRange Integer)
-> ValueRange Integer -> ValueRange Integer
forall a b. (a -> b) -> a -> b
$ ValueBound Integer -> ValueBound Integer -> ValueRange Integer
forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
MultiRange
                    ((\Integer
x -> Integer
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer -> Integer
forall a. Num a => a -> a
negate Integer
y) (Integer -> Integer) -> ValueBound Integer -> ValueBound Integer
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueBound Integer
lo)
                    ((\Integer
x -> Integer
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer -> Integer
forall a. Num a => a -> a
negate Integer
y) (Integer -> Integer) -> ValueBound Integer -> ValueBound Integer
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 Integer -> Integer -> Bool
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 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 = ValueRange Integer -> ValueRange Integer
forall tp. Num tp => ValueRange tp -> ValueRange tp
negateRange (ValueRange Integer
-> Integer -> ValueBound Integer -> ValueRange Integer
intDivAux ValueRange Integer
x (Integer -> Integer
forall a. Num a => a -> a
negate Integer
hi) (Integer -> Integer
forall a. Num a => a -> a
negate (Integer -> Integer) -> ValueBound Integer -> ValueBound Integer
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
_ = ValueBound Integer -> ValueBound Integer -> ValueRange Integer
forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
MultiRange ValueBound Integer
forall tp. ValueBound tp
Unbounded ValueBound Integer
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 = ValueBound Integer -> ValueBound Integer -> ValueRange Integer
forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
MultiRange ValueBound Integer
lo' ValueBound Integer
hi'
  where
  lo' :: ValueBound Integer
lo' = case ValueRange Integer -> ValueBound Integer
forall tp. ValueRange tp -> ValueBound tp
rangeLowBound ValueRange Integer
x of
           ValueBound Integer
Unbounded -> ValueBound Integer
forall tp. ValueBound tp
Unbounded
           Inclusive Integer
z -> Integer -> ValueBound Integer
forall a. a -> ValueBound a
Inclusive (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min Integer
0 (Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
div Integer
z Integer
lo))

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

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

  hi' :: ValueBound Integer
hi' = case ValueRange Integer -> ValueBound Integer
forall tp. ValueRange tp -> ValueBound tp
rangeHiBound ValueRange Integer
x of
           ValueBound Integer
Unbounded   -> ValueBound Integer
forall tp. ValueBound tp
Unbounded
           Inclusive Integer
z -> Integer -> ValueBound Integer
forall a. a -> ValueBound a
Inclusive (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max (Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
div Integer
z Integer
hi) (Integer -> Integer -> Integer
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 Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 = ValueBound Integer -> ValueBound Integer -> ValueRange Integer
forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
MultiRange ValueBound Integer
forall tp. ValueBound tp
Unbounded ValueBound Integer
forall tp. ValueBound tp
Unbounded
intModRange (SingleRange Integer
x) (SingleRange Integer
y) = Integer -> ValueRange Integer
forall tp. tp -> ValueRange tp
SingleRange (Integer
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer -> Integer
forall a. Num a => a -> a
abs Integer
y)
intModRange (MultiRange (Inclusive Integer
lo) (Inclusive Integer
hi)) (SingleRange Integer
y)
   | Integer
hi' Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
lo' Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
hi Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
lo = ValueBound Integer -> ValueBound Integer -> ValueRange Integer
forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
MultiRange (Integer -> ValueBound Integer
forall a. a -> ValueBound a
Inclusive Integer
lo') (Integer -> ValueBound Integer
forall a. a -> ValueBound a
Inclusive Integer
hi')
  where
  lo' :: Integer
lo' = Integer
lo Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer -> Integer
forall a. Num a => a -> a
abs Integer
y
  hi' :: Integer
hi' = Integer
hi Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer -> Integer
forall a. Num a => a -> a
abs Integer
y
intModRange ValueRange Integer
_ ValueRange Integer
y
  | Inclusive Integer
lo <- ValueRange Integer -> ValueBound Integer
forall tp. ValueRange tp -> ValueBound tp
rangeLowBound ValueRange Integer
yabs, Integer
lo Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0
  = ValueBound Integer -> ValueBound Integer -> ValueRange Integer
forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
MultiRange (Integer -> ValueBound Integer
forall a. a -> ValueBound a
Inclusive Integer
0) (Integer -> Integer
forall a. Enum a => a -> a
pred (Integer -> Integer) -> ValueBound Integer -> ValueBound Integer
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueRange Integer -> ValueBound Integer
forall tp. ValueRange tp -> ValueBound tp
rangeHiBound ValueRange Integer
yabs)
  | Bool
otherwise
  = ValueBound Integer -> ValueBound Integer -> ValueRange Integer
forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
MultiRange ValueBound Integer
forall tp. ValueBound tp
Unbounded ValueBound Integer
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 :: ValueRange tp -> ValueRange tp -> ValueRange tp
addRange (SingleRange tp
x) (SingleRange tp
y) = tp -> ValueRange tp
forall tp. tp -> ValueRange tp
SingleRange (tp
xtp -> tp -> tp
forall a. Num a => a -> a -> a
+tp
y)
addRange (SingleRange tp
x) (MultiRange ValueBound tp
ly ValueBound tp
uy) = ValueBound tp -> ValueBound tp -> ValueRange tp
forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
MultiRange ((tp
xtp -> tp -> tp
forall a. Num a => a -> a -> a
+) (tp -> tp) -> ValueBound tp -> ValueBound tp
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueBound tp
ly) ((tp
xtp -> tp -> tp
forall a. Num a => a -> a -> a
+) (tp -> tp) -> ValueBound tp -> ValueBound tp
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueBound tp
uy)
addRange (MultiRange ValueBound tp
lx ValueBound tp
ux) (SingleRange tp
y) = ValueBound tp -> ValueBound tp -> ValueRange tp
forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
MultiRange ((tp
ytp -> tp -> tp
forall a. Num a => a -> a -> a
+) (tp -> tp) -> ValueBound tp -> ValueBound tp
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueBound tp
lx) ((tp
ytp -> tp -> tp
forall a. Num a => a -> a -> a
+) (tp -> tp) -> ValueBound tp -> ValueBound tp
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueBound tp
ux)
addRange (MultiRange ValueBound tp
lx ValueBound tp
ux) (MultiRange ValueBound tp
ly ValueBound tp
uy) =
  ValueBound tp -> ValueBound tp -> ValueRange tp
forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
MultiRange (tp -> tp -> tp
forall a. Num a => a -> a -> a
(+) (tp -> tp -> tp) -> ValueBound tp -> ValueBound (tp -> tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueBound tp
lx ValueBound (tp -> tp) -> ValueBound tp -> ValueBound tp
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> ValueBound tp
ly) (tp -> tp -> tp
forall a. Num a => a -> a -> a
(+) (tp -> tp -> tp) -> ValueBound tp -> ValueBound (tp -> tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueBound tp
ux ValueBound (tp -> tp) -> ValueBound tp -> ValueBound tp
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> ValueBound 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) = Bool -> Maybe Bool
forall a. a -> Maybe a
Just (Rational -> Integer
forall a. Ratio a -> a
denominator Rational
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1)
rangeIsInteger (MultiRange (Inclusive Rational
l) (Inclusive Rational
u))
  | Rational -> Integer
forall a b. (RealFrac a, Integral b) => a -> b
floor Rational
l Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= (Rational -> Integer
forall a b. (RealFrac a, Integral b) => a -> b
ceiling Rational
u :: Integer)
  , Rational -> Integer
forall a. Ratio a -> a
denominator Rational
l Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
1
  , Rational -> Integer
forall a. Ratio a -> a
denominator Rational
u Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
1 = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
rangeIsInteger ValueRange Rational
_ = Maybe Bool
forall a. Maybe a
Nothing

-- | Multiply a range by a scalar value
rangeScalarMul :: (Ord tp, Num tp) =>  tp -> ValueRange tp -> ValueRange tp
rangeScalarMul :: tp -> ValueRange tp -> ValueRange tp
rangeScalarMul tp
x (SingleRange tp
y) = tp -> ValueRange tp
forall tp. tp -> ValueRange tp
SingleRange (tp
xtp -> tp -> tp
forall a. Num a => a -> a -> a
*tp
y)
rangeScalarMul tp
x (MultiRange ValueBound tp
ly ValueBound tp
uy)
  | tp
x tp -> tp -> Bool
forall a. Ord a => a -> a -> Bool
<  tp
0 = ValueBound tp -> ValueBound tp -> ValueRange tp
forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
MultiRange ((tp
xtp -> tp -> tp
forall a. Num a => a -> a -> a
*) (tp -> tp) -> ValueBound tp -> ValueBound tp
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueBound tp
uy) ((tp
xtp -> tp -> tp
forall a. Num a => a -> a -> a
*) (tp -> tp) -> ValueBound tp -> ValueBound tp
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueBound tp
ly)
  | tp
x tp -> tp -> Bool
forall a. Eq a => a -> a -> Bool
== tp
0 = tp -> ValueRange tp
forall tp. tp -> ValueRange tp
SingleRange tp
0
  | Bool
otherwise = Bool -> ValueRange tp -> ValueRange tp
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (tp
x tp -> tp -> Bool
forall a. Ord a => a -> a -> Bool
> tp
0) (ValueRange tp -> ValueRange tp) -> ValueRange tp -> ValueRange tp
forall a b. (a -> b) -> a -> b
$ ValueBound tp -> ValueBound tp -> ValueRange tp
forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
MultiRange ((tp
xtp -> tp -> tp
forall a. Num a => a -> a -> a
*) (tp -> tp) -> ValueBound tp -> ValueBound tp
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueBound tp
ly) ((tp
xtp -> tp -> tp
forall a. Num a => a -> a -> a
*) (tp -> tp) -> ValueBound tp -> ValueBound tp
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueBound tp
uy)

negateRange :: (Num tp) => ValueRange tp -> ValueRange tp
negateRange :: ValueRange tp -> ValueRange tp
negateRange (SingleRange tp
x) = tp -> ValueRange tp
forall tp. tp -> ValueRange tp
SingleRange (tp -> tp
forall a. Num a => a -> a
negate tp
x)
negateRange (MultiRange ValueBound tp
lo ValueBound tp
hi) = ValueBound tp -> ValueBound tp -> ValueRange tp
forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
MultiRange (tp -> tp
forall a. Num a => a -> a
negate (tp -> tp) -> ValueBound tp -> ValueBound tp
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueBound tp
hi) (tp -> tp
forall a. Num a => a -> a
negate (tp -> tp) -> ValueBound tp -> ValueBound tp
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueBound tp
lo)

-- | Multiply two ranges together.
mulRange :: (Ord tp, Num tp) => ValueRange tp -> ValueRange tp -> ValueRange tp
mulRange :: ValueRange tp -> ValueRange tp -> ValueRange tp
mulRange (SingleRange tp
x) ValueRange tp
y = tp -> ValueRange tp -> ValueRange tp
forall tp. (Ord tp, Num tp) => tp -> ValueRange tp -> ValueRange tp
rangeScalarMul tp
x ValueRange tp
y
mulRange ValueRange tp
x (SingleRange tp
y) = tp -> ValueRange tp -> ValueRange tp
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) = ValueBound tp -> ValueBound tp -> ValueRange tp
forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
MultiRange ValueBound tp
lz ValueBound tp
uz
  where x_neg :: Bool
x_neg = ValueBound tp -> Bool
forall tp. (Ord tp, Num tp) => ValueBound tp -> Bool
lowerBoundIsNegative ValueBound tp
lx
        x_pos :: Bool
x_pos = ValueBound tp -> Bool
forall tp. (Ord tp, Num tp) => ValueBound tp -> Bool
upperBoundIsNonNeg ValueBound tp
ux
        y_neg :: Bool
y_neg = ValueBound tp -> Bool
forall tp. (Ord tp, Num tp) => ValueBound tp -> Bool
lowerBoundIsNegative ValueBound tp
ly
        y_pos :: Bool
y_pos = ValueBound tp -> Bool
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 =
               ValueBound tp -> ValueBound tp -> ValueBound tp
forall tp.
Ord tp =>
ValueBound tp -> ValueBound tp -> ValueBound tp
minValueBound (tp -> tp -> tp
forall a. Num a => a -> a -> a
(*) (tp -> tp -> tp) -> ValueBound tp -> ValueBound (tp -> tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueBound tp
lx ValueBound (tp -> tp) -> ValueBound tp -> ValueBound tp
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> ValueBound tp
uy)
                             (tp -> tp -> tp
forall a. Num a => a -> a -> a
(*) (tp -> tp -> tp) -> ValueBound tp -> ValueBound (tp -> tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueBound tp
ux ValueBound (tp -> tp) -> ValueBound tp -> ValueBound tp
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 = tp -> tp -> tp
forall a. Num a => a -> a -> a
(*) (tp -> tp -> tp) -> ValueBound tp -> ValueBound (tp -> tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueBound tp
lx ValueBound (tp -> tp) -> ValueBound tp -> ValueBound tp
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 = tp -> tp -> tp
forall a. Num a => a -> a -> a
(*) (tp -> tp -> tp) -> ValueBound tp -> ValueBound (tp -> tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueBound tp
ux ValueBound (tp -> tp) -> ValueBound tp -> ValueBound tp
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 = Bool -> ValueBound tp -> ValueBound tp
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Bool -> Bool
not Bool
x_pos Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
y_pos) (ValueBound tp -> ValueBound tp) -> ValueBound tp -> ValueBound tp
forall a b. (a -> b) -> a -> b
$ tp -> tp -> tp
forall a. Num a => a -> a -> a
(*) (tp -> tp -> tp) -> ValueBound tp -> ValueBound (tp -> tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueBound tp
ux ValueBound (tp -> tp) -> ValueBound tp -> ValueBound tp
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 = tp -> tp -> tp
forall a. Num a => a -> a -> a
(*) (tp -> tp -> tp) -> ValueBound tp -> ValueBound (tp -> tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueBound tp
lx ValueBound (tp -> tp) -> ValueBound tp -> ValueBound tp
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 =
             ValueBound tp -> ValueBound tp -> ValueBound tp
forall tp.
Ord tp =>
ValueBound tp -> ValueBound tp -> ValueBound tp
maxValueBound (tp -> tp -> tp
forall a. Num a => a -> a -> a
(*) (tp -> tp -> tp) -> ValueBound tp -> ValueBound (tp -> tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueBound tp
lx ValueBound (tp -> tp) -> ValueBound tp -> ValueBound tp
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> ValueBound tp
ly)
                           (tp -> tp -> tp
forall a. Num a => a -> a -> a
(*) (tp -> tp -> tp) -> ValueBound tp -> ValueBound (tp -> tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueBound tp
ux ValueBound (tp -> tp) -> ValueBound tp -> ValueBound tp
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 = tp -> tp -> tp
forall a. Num a => a -> a -> a
(*) (tp -> tp -> tp) -> ValueBound tp -> ValueBound (tp -> tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueBound tp
lx ValueBound (tp -> tp) -> ValueBound tp -> ValueBound tp
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 = tp -> tp -> tp
forall a. Num a => a -> a -> a
(*) (tp -> tp -> tp) -> ValueBound tp -> ValueBound (tp -> tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueBound tp
ux ValueBound (tp -> tp) -> ValueBound tp -> ValueBound tp
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 = tp -> tp -> tp
forall a. Num a => a -> a -> a
(*) (tp -> tp -> tp) -> ValueBound tp -> ValueBound (tp -> tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueBound tp
lx ValueBound (tp -> tp) -> ValueBound tp -> ValueBound tp
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 = tp -> tp -> tp
forall a. Num a => a -> a -> a
(*) (tp -> tp -> tp) -> ValueBound tp -> ValueBound (tp -> tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueBound tp
ux ValueBound (tp -> tp) -> ValueBound tp -> ValueBound tp
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 :: ValueRange tp -> ValueBound tp
rangeLowBound (SingleRange tp
x) = tp -> ValueBound tp
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 :: ValueRange tp -> ValueBound tp
rangeHiBound (SingleRange tp
x) = tp -> ValueBound tp
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 :: ValueRange tp -> ValueRange tp -> ValueRange tp
joinRange (SingleRange tp
x) (SingleRange tp
y)
  | tp
x tp -> tp -> Bool
forall a. Eq a => a -> a -> Bool
== tp
y = tp -> ValueRange tp
forall tp. tp -> ValueRange tp
SingleRange tp
x
joinRange ValueRange tp
x ValueRange tp
y = ValueBound tp -> ValueBound tp -> ValueRange tp
forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
MultiRange (ValueBound tp -> ValueBound tp -> ValueBound tp
forall tp.
Ord tp =>
ValueBound tp -> ValueBound tp -> ValueBound tp
minValueBound ValueBound tp
lx ValueBound tp
ly) (ValueBound tp -> ValueBound tp -> ValueBound tp
forall tp.
Ord tp =>
ValueBound tp -> ValueBound tp -> ValueBound tp
maxValueBound ValueBound tp
ux ValueBound tp
uy)
  where lx :: ValueBound tp
lx = ValueRange tp -> ValueBound tp
forall tp. ValueRange tp -> ValueBound tp
rangeLowBound ValueRange tp
x
        ux :: ValueBound tp
ux = ValueRange tp -> ValueBound tp
forall tp. ValueRange tp -> ValueBound tp
rangeHiBound ValueRange tp
x
        ly :: ValueBound tp
ly = ValueRange tp -> ValueBound tp
forall tp. ValueRange tp -> ValueBound tp
rangeLowBound ValueRange tp
y
        uy :: ValueBound tp
uy = ValueRange tp -> ValueBound tp
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 :: ValueRange tp -> ValueRange tp -> Bool
rangeOverlap ValueRange tp
x ValueRange tp
y
   -- first range is before second.
  | Inclusive tp
ux <- ValueRange tp -> ValueBound tp
forall tp. ValueRange tp -> ValueBound tp
rangeHiBound ValueRange tp
x
  , Inclusive tp
ly <- ValueRange tp -> ValueBound tp
forall tp. ValueRange tp -> ValueBound tp
rangeLowBound ValueRange tp
y
  , tp
ux tp -> tp -> Bool
forall a. Ord a => a -> a -> Bool
< tp
ly = Bool
False

  -- second range is before first.
  | Inclusive tp
lx <- ValueRange tp -> ValueBound tp
forall tp. ValueRange tp -> ValueBound tp
rangeLowBound ValueRange tp
x
  , Inclusive tp
uy <- ValueRange tp -> ValueBound tp
forall tp. ValueRange tp -> ValueBound tp
rangeHiBound ValueRange tp
y
  , tp
uy tp -> tp -> Bool
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 :: ValueRange tp -> ValueRange tp -> Maybe Bool
rangeCheckEq ValueRange tp
x ValueRange tp
y
    -- If ranges do not overlap return false.
  | Bool -> Bool
not (ValueRange tp -> ValueRange tp -> Bool
forall tp. Ord tp => ValueRange tp -> ValueRange tp -> Bool
rangeOverlap ValueRange tp
x ValueRange tp
y) = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
    -- If they are both single values, then result can be determined.
  | Just tp
cx <- ValueRange tp -> Maybe tp
forall tp. ValueRange tp -> Maybe tp
asSingleRange ValueRange tp
x
  , Just tp
cy <- ValueRange tp -> Maybe tp
forall tp. ValueRange tp -> Maybe tp
asSingleRange ValueRange tp
y
  = Bool -> Maybe Bool
forall a. a -> Maybe a
Just (tp
cx tp -> tp -> Bool
forall a. Eq a => a -> a -> Bool
== tp
cy)
    -- Otherwise result is indeterminant.
  | Bool
otherwise = Maybe Bool
forall a. Maybe a
Nothing


rangeCheckLe :: Ord tp => ValueRange tp -> ValueRange tp -> Maybe Bool
rangeCheckLe :: 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 <- ValueRange tp -> ValueBound tp
forall tp. ValueRange tp -> ValueBound tp
rangeHiBound ValueRange tp
x
  , Inclusive tp
ly <- ValueRange tp -> ValueBound tp
forall tp. ValueRange tp -> ValueBound tp
rangeLowBound ValueRange tp
y
  , tp
ux tp -> tp -> Bool
forall a. Ord a => a -> a -> Bool
<= tp
ly = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True

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

  | Bool
otherwise = Maybe Bool
forall a. Maybe a
Nothing

-- | Defines a unbounded value range.
unboundedRange :: ValueRange tp
unboundedRange :: ValueRange tp
unboundedRange = ValueBound tp -> ValueBound tp -> ValueRange tp
forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
MultiRange ValueBound tp
forall tp. ValueBound tp
Unbounded ValueBound tp
forall tp. ValueBound tp
Unbounded

-- | Defines a unbounded value range.
concreteRange :: Eq tp => tp -> tp -> ValueRange tp
concreteRange :: tp -> tp -> ValueRange tp
concreteRange tp
x tp
y
  | tp
x tp -> tp -> Bool
forall a. Eq a => a -> a -> Bool
== tp
y = tp -> ValueRange tp
forall tp. tp -> ValueRange tp
SingleRange tp
x
  | Bool
otherwise = ValueBound tp -> ValueBound tp -> ValueRange tp
forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
MultiRange (tp -> ValueBound tp
forall a. a -> ValueBound a
Inclusive tp
x) (tp -> ValueBound tp
forall a. a -> ValueBound a
Inclusive tp
y)

-- | Defines a value range containing a single element.
singleRange :: tp -> ValueRange tp
singleRange :: tp -> ValueRange tp
singleRange tp
v = tp -> ValueRange tp
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 :: ValueBound tp -> ValueBound tp -> ValueRange tp
valueRange (Inclusive tp
x) (Inclusive tp
y)
  | tp
x tp -> tp -> Bool
forall a. Eq a => a -> a -> Bool
== tp
y = tp -> ValueRange tp
forall tp. tp -> ValueRange tp
SingleRange tp
x
valueRange ValueBound tp
x ValueBound tp
y = ValueBound tp -> ValueBound tp -> ValueRange tp
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 :: ValueRange tp -> Maybe tp
asSingleRange (SingleRange tp
x) = tp -> Maybe tp
forall a. a -> Maybe a
Just tp
x
asSingleRange ValueRange tp
_ = Maybe tp
forall a. Maybe a
Nothing

mapRange :: (a -> b) -> ValueRange a -> ValueRange b
mapRange :: (a -> b) -> ValueRange a -> ValueRange b
mapRange a -> b
f (SingleRange a
x) = b -> ValueRange b
forall tp. tp -> ValueRange tp
SingleRange (a -> b
f a
x)
mapRange a -> b
f (MultiRange ValueBound a
l ValueBound a
u) = ValueBound b -> ValueBound b -> ValueRange b
forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
MultiRange (a -> b
f (a -> b) -> ValueBound a -> ValueBound b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueBound a
l) (a -> b
f (a -> b) -> ValueBound a -> ValueBound b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueBound a
u)

------------------------------------------------------------------------
-- 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 ValueRange Rational
forall tp. ValueRange tp
unboundedRange Maybe Bool
forall a. Maybe a
Nothing)

ravSingle :: Rational -> RealAbstractValue
ravSingle :: Rational -> RealAbstractValue
ravSingle Rational
x = ValueRange Rational -> Maybe Bool -> RealAbstractValue
RAV (Rational -> ValueRange Rational
forall tp. tp -> ValueRange tp
singleRange Rational
x) (Bool -> Maybe Bool
forall a. a -> Maybe a
Just (Bool -> Maybe Bool) -> Bool -> Maybe Bool
forall a b. (a -> b) -> a -> b
$! Rational -> Integer
forall a. Ratio a -> a
denominator Rational
x Integer -> Integer -> Bool
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 (Rational -> Rational -> ValueRange Rational
forall tp. Eq tp => tp -> tp -> ValueRange tp
concreteRange Rational
l Rational
h) (Bool -> Maybe Bool
forall a. a -> Maybe a
Just (Bool -> Maybe Bool) -> Bool -> Maybe Bool
forall a b. (a -> b) -> a -> b
$! Bool
b)
  where -- Return true if this is a singleton.
        b :: Bool
b = Rational
l Rational -> Rational -> Bool
forall a. Eq a => a -> a -> Bool
== Rational
h Bool -> Bool -> Bool
&& Rational -> Integer
forall a. Ratio a -> a
denominator Rational
l Integer -> Integer -> Bool
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 = ValueRange Rational -> ValueRange Rational -> ValueRange Rational
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) (Maybe Bool, Maybe Bool) -> (Maybe Bool, Maybe Bool) -> Bool
forall a. Eq a => a -> a -> Bool
== (Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True, Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True) = Bool -> Maybe Bool
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 = Rational -> ValueRange Rational -> ValueRange Rational
forall tp. (Ord tp, Num tp) => tp -> ValueRange tp -> ValueRange tp
rangeScalarMul Rational
x ValueRange Rational
yr
        zi :: Maybe Bool
zi | Rational -> Integer
forall a. Ratio a -> a
denominator Rational
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1 Bool -> Bool -> Bool
&& Maybe Bool
yi Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True = Bool -> Maybe Bool
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 = ValueRange Rational -> ValueRange Rational -> ValueRange Rational
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) (Maybe Bool, Maybe Bool) -> (Maybe Bool, Maybe Bool) -> Bool
forall a. Eq a => a -> a -> Bool
== (Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True, Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True) = Bool -> Maybe Bool
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 (ValueRange Rational -> ValueRange Rational -> ValueRange Rational
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 Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe Bool
yi = Maybe Bool
xi
           | Bool
otherwise = Maybe Bool
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
_) = ValueRange Rational -> ValueRange Rational -> 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
_) = ValueRange Rational -> ValueRange Rational -> 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
_ = Bool -> 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) = Bool -> Maybe Bool
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 = Maybe Bool
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
_ = Bool -> 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)  = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
absOr Maybe Bool
Nothing Maybe Bool
Nothing = Maybe Bool
forall a. Maybe a
Nothing


rangeMax :: Ord a => ValueRange a -> ValueRange a -> ValueRange a
rangeMax :: ValueRange a -> ValueRange a -> ValueRange a
rangeMax ValueRange a
x ValueRange a
y = ValueBound a -> ValueBound a -> ValueRange a
forall tp. Eq tp => ValueBound tp -> ValueBound tp -> ValueRange tp
valueRange ValueBound a
lo ValueBound a
hi
 where
 lo :: ValueBound a
lo = case (ValueRange a -> ValueBound a
forall tp. ValueRange tp -> ValueBound tp
rangeLowBound ValueRange a
x, ValueRange a -> ValueBound a
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) -> a -> ValueBound a
forall a. a -> ValueBound a
Inclusive (a -> a -> a
forall a. Ord a => a -> a -> a
max a
a a
b)

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


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

 hi :: ValueBound a
hi = case (ValueRange a -> ValueBound a
forall tp. ValueRange tp -> ValueBound tp
rangeHiBound ValueRange a
x, ValueRange a -> ValueBound a
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) -> a -> ValueBound a
forall a. a -> ValueBound a
Inclusive (a -> a -> a
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 (ValueBound Integer -> ValueBound Integer -> ValueRange Integer
forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
MultiRange (Integer -> ValueBound Integer
forall a. a -> ValueBound a
Inclusive Integer
0) ValueBound Integer
forall tp. ValueBound tp
Unbounded)

stringAbsEmpty :: StringAbstractValue
stringAbsEmpty :: StringAbstractValue
stringAbsEmpty = ValueRange Integer -> StringAbstractValue
StringAbs (Integer -> ValueRange Integer
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 (ValueRange Integer -> ValueRange Integer -> ValueRange Integer
forall tp.
Ord tp =>
ValueRange tp -> ValueRange tp -> ValueRange tp
joinRange ValueRange Integer
lenx ValueRange Integer
leny)

stringAbsSingle :: StringLiteral si -> StringAbstractValue
stringAbsSingle :: StringLiteral si -> StringAbstractValue
stringAbsSingle StringLiteral si
lit = ValueRange Integer -> StringAbstractValue
StringAbs (Integer -> ValueRange Integer
forall tp. tp -> ValueRange tp
singleRange (Integer -> Integer
forall a. Integral a => a -> Integer
toInteger (StringLiteral si -> Integer
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) = ValueRange Integer -> ValueRange Integer -> Bool
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 <- ValueRange Integer -> Maybe Integer
forall tp. ValueRange tp -> Maybe tp
asSingleRange ValueRange Integer
lenx
  , Just Integer
0 <- ValueRange Integer -> Maybe Integer
forall tp. ValueRange tp -> Maybe tp
asSingleRange ValueRange Integer
leny
  = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True

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

  | Bool
otherwise
  = Maybe Bool
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 (ValueRange Integer -> ValueRange Integer -> ValueRange Integer
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 =
  ValueRange Integer -> StringAbstractValue
StringAbs (ValueRange Integer -> ValueRange Integer -> ValueRange Integer
forall tp.
Ord tp =>
ValueRange tp -> ValueRange tp -> ValueRange tp
rangeMin ValueRange Integer
len (ValueRange Integer -> ValueRange Integer -> ValueRange Integer
forall tp.
Ord tp =>
ValueRange tp -> ValueRange tp -> ValueRange tp
rangeMax (Integer -> ValueRange Integer
forall tp. tp -> ValueRange tp
singleRange Integer
0) (ValueRange Integer -> ValueRange Integer -> ValueRange Integer
forall tp.
Num tp =>
ValueRange tp -> ValueRange tp -> ValueRange tp
addRange ValueRange Integer
s (ValueRange Integer -> ValueRange Integer
forall tp. Num tp => ValueRange tp -> ValueRange tp
negateRange ValueRange Integer
off))))

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 = (StringAbstractValue -> StringAbstractValue -> Maybe Bool)
-> StringAbstractValue -> StringAbstractValue -> Maybe Bool
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 = (StringAbstractValue -> StringAbstractValue -> Maybe Bool)
-> StringAbstractValue -> StringAbstractValue -> Maybe Bool
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 <- ValueRange Integer -> ValueRange Integer -> Maybe Bool
forall tp. Ord tp => ValueRange tp -> ValueRange tp -> Maybe Bool
rangeCheckLe ValueRange Integer
leny ValueRange Integer
lenx = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
  | Bool
otherwise = Maybe Bool
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 <- ValueRange Integer -> ValueRange Integer -> Maybe Bool
forall tp. Ord tp => ValueRange tp -> ValueRange tp -> Maybe Bool
rangeCheckLe (ValueRange Integer -> ValueRange Integer -> ValueRange Integer
forall tp.
Num tp =>
ValueRange tp -> ValueRange tp -> ValueRange tp
addRange ValueRange Integer
leny ValueRange Integer
k) ValueRange Integer
lenx = Integer -> ValueRange Integer
forall tp. tp -> ValueRange tp
SingleRange (-Integer
1)
  | Bool
otherwise = ValueBound Integer -> ValueBound Integer -> ValueRange Integer
forall tp. ValueBound tp -> ValueBound tp -> ValueRange tp
MultiRange (Integer -> ValueBound Integer
forall a. a -> ValueBound a
Inclusive (-Integer
1)) (ValueRange Integer -> ValueBound Integer
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 = ValueRange Integer -> ValueRange Integer -> ValueRange Integer
forall tp.
Ord tp =>
ValueRange tp -> ValueRange tp -> ValueRange tp
rangeMax (Integer -> ValueRange Integer
forall tp. tp -> ValueRange tp
singleRange Integer
0) (ValueRange Integer -> ValueRange Integer -> ValueRange Integer
forall tp.
Num tp =>
ValueRange tp -> ValueRange tp -> ValueRange tp
addRange ValueRange Integer
lenx (ValueRange Integer -> ValueRange Integer
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 { 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 { ConcreteValueWrapper tp -> ConcreteValue tp
unwrapCV :: ConcreteValue tp }

-- | Create an abstract value that contains every concrete value.
avTop :: BaseTypeRepr tp -> AbstractValue tp
avTop :: BaseTypeRepr tp -> AbstractValue tp
avTop BaseTypeRepr tp
tp =
  case BaseTypeRepr tp
tp of
    BaseTypeRepr tp
BaseBoolRepr    -> AbstractValue tp
forall a. Maybe a
Nothing
    BaseTypeRepr tp
BaseIntegerRepr -> AbstractValue tp
forall tp. ValueRange tp
unboundedRange
    BaseTypeRepr tp
BaseRealRepr    -> AbstractValue tp
RealAbstractValue
ravUnbounded
    BaseTypeRepr tp
BaseComplexRepr -> RealAbstractValue
ravUnbounded RealAbstractValue -> RealAbstractValue -> Complex RealAbstractValue
forall a. a -> a -> Complex a
:+ RealAbstractValue
ravUnbounded
    BaseStringRepr StringInfoRepr si
_ -> AbstractValue tp
StringAbstractValue
stringAbsTop
    BaseBVRepr NatRepr w
w    -> NatRepr w -> BVDomain w
forall (w :: Nat). (1 <= w) => NatRepr w -> BVDomain w
BVD.any NatRepr w
w
    BaseFloatRepr{} -> ()
    BaseArrayRepr Assignment BaseTypeRepr (idx ::> tp)
_a BaseTypeRepr xs
b -> BaseTypeRepr xs -> AbstractValue xs
forall (tp :: BaseType). BaseTypeRepr tp -> AbstractValue tp
avTop BaseTypeRepr xs
b
    BaseStructRepr Assignment BaseTypeRepr ctx
flds -> (forall (x :: BaseType). BaseTypeRepr x -> AbstractValueWrapper x)
-> Assignment BaseTypeRepr ctx
-> Assignment AbstractValueWrapper ctx
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 -> AbstractValue x -> AbstractValueWrapper x
forall (tp :: BaseType).
AbstractValue tp -> AbstractValueWrapper tp
AbstractValueWrapper (BaseTypeRepr x -> AbstractValue x
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 :: BaseTypeRepr tp -> ConcreteValue tp -> AbstractValue tp
avSingle BaseTypeRepr tp
tp =
  case BaseTypeRepr tp
tp of
    BaseTypeRepr tp
BaseBoolRepr -> ConcreteValue tp -> AbstractValue tp
forall a. a -> Maybe a
Just
    BaseTypeRepr tp
BaseIntegerRepr -> ConcreteValue tp -> AbstractValue tp
forall tp. tp -> ValueRange tp
singleRange
    BaseTypeRepr tp
BaseRealRepr -> Rational -> RealAbstractValue
ConcreteValue tp -> AbstractValue tp
ravSingle
    BaseStringRepr StringInfoRepr si
_ -> ConcreteValue tp -> AbstractValue tp
forall (si :: StringInfo). StringLiteral si -> StringAbstractValue
stringAbsSingle
    BaseTypeRepr tp
BaseComplexRepr -> (Rational -> RealAbstractValue)
-> Complex Rational -> Complex RealAbstractValue
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Rational -> RealAbstractValue
ravSingle
    BaseBVRepr NatRepr w
w -> NatRepr w -> Integer -> BVDomain w
forall (w :: Nat).
(?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
_ -> BaseTypeRepr xs -> AbstractValue xs
forall (tp :: BaseType). BaseTypeRepr tp -> AbstractValue tp
avTop BaseTypeRepr xs
b
    BaseStructRepr Assignment BaseTypeRepr ctx
flds -> \ConcreteValue tp
vals ->
      (forall (x :: BaseType).
 BaseTypeRepr x -> ConcreteValueWrapper x -> AbstractValueWrapper x)
-> Assignment BaseTypeRepr ctx
-> Assignment ConcreteValueWrapper ctx
-> Assignment AbstractValueWrapper ctx
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 -> AbstractValue x -> AbstractValueWrapper x
forall (tp :: BaseType).
AbstractValue tp -> AbstractValueWrapper tp
AbstractValueWrapper (BaseTypeRepr x -> ConcreteValue x -> AbstractValue x
forall (tp :: BaseType).
BaseTypeRepr tp -> ConcreteValue tp -> AbstractValue tp
avSingle BaseTypeRepr x
ftp (ConcreteValueWrapper x -> ConcreteValue x
forall (tp :: BaseType).
ConcreteValueWrapper tp -> ConcreteValue tp
unwrapCV ConcreteValueWrapper x
v)))
        Assignment BaseTypeRepr ctx
flds
        Assignment ConcreteValueWrapper ctx
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' :: BaseTypeRepr tp
-> AbstractValueWrapper tp
-> AbstractValueWrapper tp
-> AbstractValueWrapper tp
avJoin' BaseTypeRepr tp
tp AbstractValueWrapper tp
x AbstractValueWrapper tp
y = BaseTypeRepr tp
-> (Abstractable tp => AbstractValueWrapper tp)
-> AbstractValueWrapper tp
forall (bt :: BaseType) a.
BaseTypeRepr bt -> (Abstractable bt => a) -> a
withAbstractable BaseTypeRepr tp
tp ((Abstractable tp => AbstractValueWrapper tp)
 -> AbstractValueWrapper tp)
-> (Abstractable tp => AbstractValueWrapper tp)
-> AbstractValueWrapper tp
forall a b. (a -> b) -> a -> b
$
  AbstractValue tp -> AbstractValueWrapper tp
forall (tp :: BaseType).
AbstractValue tp -> AbstractValueWrapper tp
AbstractValueWrapper (AbstractValue tp -> AbstractValueWrapper tp)
-> AbstractValue tp -> AbstractValueWrapper tp
forall a b. (a -> b) -> a -> b
$ BaseTypeRepr tp
-> AbstractValue tp -> AbstractValue tp -> AbstractValue tp
forall (tp :: BaseType).
Abstractable tp =>
BaseTypeRepr tp
-> AbstractValue tp -> AbstractValue tp -> AbstractValue tp
avJoin BaseTypeRepr tp
tp (AbstractValueWrapper tp -> AbstractValue tp
forall (tp :: BaseType).
AbstractValueWrapper tp -> AbstractValue tp
unwrapAV AbstractValueWrapper tp
x) (AbstractValueWrapper tp -> AbstractValue tp
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 | Maybe Bool
AbstractValue BaseBoolType
x Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe Bool
AbstractValue BaseBoolType
y = AbstractValue BaseBoolType
x
               | Bool
otherwise = AbstractValue BaseBoolType
forall a. Maybe a
Nothing

  avOverlap :: BaseTypeRepr BaseBoolType
-> AbstractValue BaseBoolType -> AbstractValue BaseBoolType -> Bool
avOverlap BaseTypeRepr BaseBoolType
_ (Just x) (Just y) | Bool
x Bool -> Bool -> Bool
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 x) (Just y) = Bool -> Maybe Bool
forall a. a -> Maybe a
Just (Bool
x Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
y)
  avCheckEq BaseTypeRepr BaseBoolType
_ AbstractValue BaseBoolType
_ AbstractValue BaseBoolType
_ = Maybe Bool
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)
_     = AbstractValue (BaseStringType si)
-> AbstractValue (BaseStringType si)
-> AbstractValue (BaseStringType si)
StringAbstractValue -> StringAbstractValue -> StringAbstractValue
stringAbsJoin
  avOverlap :: BaseTypeRepr (BaseStringType si)
-> AbstractValue (BaseStringType si)
-> AbstractValue (BaseStringType si)
-> Bool
avOverlap BaseTypeRepr (BaseStringType si)
_  = AbstractValue (BaseStringType si)
-> AbstractValue (BaseStringType si) -> Bool
StringAbstractValue -> StringAbstractValue -> Bool
stringAbsOverlap
  avCheckEq :: BaseTypeRepr (BaseStringType si)
-> AbstractValue (BaseStringType si)
-> AbstractValue (BaseStringType si)
-> Maybe Bool
avCheckEq BaseTypeRepr (BaseStringType si)
_  = AbstractValue (BaseStringType si)
-> AbstractValue (BaseStringType si) -> Maybe Bool
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
_ = AbstractValue BaseIntegerType
-> AbstractValue BaseIntegerType -> AbstractValue BaseIntegerType
forall tp.
Ord tp =>
ValueRange tp -> ValueRange tp -> ValueRange tp
joinRange
  avOverlap :: BaseTypeRepr BaseIntegerType
-> AbstractValue BaseIntegerType
-> AbstractValue BaseIntegerType
-> Bool
avOverlap BaseTypeRepr BaseIntegerType
_ = AbstractValue BaseIntegerType
-> AbstractValue BaseIntegerType -> Bool
forall tp. Ord tp => ValueRange tp -> ValueRange tp -> Bool
rangeOverlap
  avCheckEq :: BaseTypeRepr BaseIntegerType
-> AbstractValue BaseIntegerType
-> AbstractValue BaseIntegerType
-> Maybe Bool
avCheckEq BaseTypeRepr BaseIntegerType
_ = AbstractValue BaseIntegerType
-> AbstractValue BaseIntegerType -> Maybe Bool
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
_ = AbstractValue BaseRealType
-> AbstractValue BaseRealType -> AbstractValue BaseRealType
RealAbstractValue -> RealAbstractValue -> RealAbstractValue
ravJoin
  avOverlap :: BaseTypeRepr BaseRealType
-> AbstractValue BaseRealType -> AbstractValue BaseRealType -> Bool
avOverlap BaseTypeRepr BaseRealType
_ AbstractValue BaseRealType
x AbstractValue BaseRealType
y = ValueRange Rational -> ValueRange Rational -> Bool
forall tp. Ord tp => ValueRange tp -> ValueRange tp -> Bool
rangeOverlap (RealAbstractValue -> ValueRange Rational
ravRange AbstractValue BaseRealType
RealAbstractValue
x) (RealAbstractValue -> ValueRange Rational
ravRange AbstractValue BaseRealType
RealAbstractValue
y)
  avCheckEq :: BaseTypeRepr BaseRealType
-> AbstractValue BaseRealType
-> AbstractValue BaseRealType
-> Maybe Bool
avCheckEq BaseTypeRepr BaseRealType
_ = AbstractValue BaseRealType
-> AbstractValue BaseRealType -> Maybe Bool
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
_) = AbstractValue (BaseBVType w)
-> AbstractValue (BaseBVType w) -> AbstractValue (BaseBVType w)
forall (w :: Nat).
(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)
_ = AbstractValue (BaseBVType w)
-> AbstractValue (BaseBVType w) -> Bool
forall (w :: Nat). BVDomain w -> BVDomain w -> Bool
BVD.domainsOverlap
  avCheckEq :: BaseTypeRepr (BaseBVType w)
-> AbstractValue (BaseBVType w)
-> AbstractValue (BaseBVType w)
-> Maybe Bool
avCheckEq BaseTypeRepr (BaseBVType w)
_ = AbstractValue (BaseBVType w)
-> AbstractValue (BaseBVType w) -> Maybe Bool
forall (w :: Nat). 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)
_ = Maybe Bool
forall a. Maybe a
Nothing

instance Abstractable BaseComplexType where
  avJoin :: BaseTypeRepr BaseComplexType
-> AbstractValue BaseComplexType
-> AbstractValue BaseComplexType
-> AbstractValue BaseComplexType
avJoin BaseTypeRepr BaseComplexType
_ (r1 :+ i1) (r2 :+ i2) = (RealAbstractValue -> RealAbstractValue -> RealAbstractValue
ravJoin RealAbstractValue
r1 RealAbstractValue
r2) RealAbstractValue -> RealAbstractValue -> Complex RealAbstractValue
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
_ (r1 :+ i1) (r2 :+ i2) = ValueRange Rational -> ValueRange Rational -> Bool
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
&& ValueRange Rational -> ValueRange Rational -> 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
_ (r1 :+ i1) (r2 :+ i2)
    = Maybe Bool -> Maybe Bool -> Maybe Bool
combineEqCheck
        (ValueRange Rational -> ValueRange Rational -> Maybe Bool
forall tp. Ord tp => ValueRange tp -> ValueRange tp -> Maybe Bool
rangeCheckEq (RealAbstractValue -> ValueRange Rational
ravRange RealAbstractValue
r1) (RealAbstractValue -> ValueRange Rational
ravRange RealAbstractValue
r2))
        (ValueRange Rational -> ValueRange Rational -> Maybe Bool
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 = BaseTypeRepr xs
-> (Abstractable xs => AbstractValue b) -> AbstractValue b
forall (bt :: BaseType) a.
BaseTypeRepr bt -> (Abstractable bt => a) -> a
withAbstractable BaseTypeRepr xs
b ((Abstractable xs => AbstractValue b) -> AbstractValue b)
-> (Abstractable xs => AbstractValue b) -> AbstractValue b
forall a b. (a -> b) -> a -> b
$ BaseTypeRepr xs
-> AbstractValue xs -> AbstractValue xs -> AbstractValue xs
forall (tp :: BaseType).
Abstractable tp =>
BaseTypeRepr tp
-> AbstractValue tp -> AbstractValue tp -> AbstractValue tp
avJoin BaseTypeRepr xs
b AbstractValue xs
AbstractValue (BaseArrayType idx b)
x AbstractValue xs
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 = BaseTypeRepr xs -> (Abstractable xs => Bool) -> Bool
forall (bt :: BaseType) a.
BaseTypeRepr bt -> (Abstractable bt => a) -> a
withAbstractable BaseTypeRepr xs
b ((Abstractable xs => Bool) -> Bool)
-> (Abstractable xs => Bool) -> Bool
forall a b. (a -> b) -> a -> b
$ BaseTypeRepr xs -> AbstractValue xs -> AbstractValue xs -> Bool
forall (tp :: BaseType).
Abstractable tp =>
BaseTypeRepr tp -> AbstractValue tp -> AbstractValue tp -> Bool
avOverlap BaseTypeRepr xs
b AbstractValue xs
AbstractValue (BaseArrayType idx b)
x AbstractValue xs
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 = BaseTypeRepr xs -> (Abstractable xs => Maybe Bool) -> Maybe Bool
forall (bt :: BaseType) a.
BaseTypeRepr bt -> (Abstractable bt => a) -> a
withAbstractable BaseTypeRepr xs
b ((Abstractable xs => Maybe Bool) -> Maybe Bool)
-> (Abstractable xs => Maybe Bool) -> Maybe Bool
forall a b. (a -> b) -> a -> b
$ BaseTypeRepr xs
-> AbstractValue xs -> AbstractValue xs -> Maybe Bool
forall (tp :: BaseType).
Abstractable tp =>
BaseTypeRepr tp
-> AbstractValue tp -> AbstractValue tp -> Maybe Bool
avCheckEq BaseTypeRepr xs
b AbstractValue xs
AbstractValue (BaseArrayType idx b)
x AbstractValue xs
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
_ = Bool -> 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) = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
combineEqCheck Maybe Bool
x (Just Bool
True)  = Maybe Bool
x
combineEqCheck Maybe Bool
_ 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 (x :: BaseType).
 BaseTypeRepr x
 -> AbstractValueWrapper x
 -> AbstractValueWrapper x
 -> AbstractValueWrapper x)
-> Assignment BaseTypeRepr ctx
-> Assignment AbstractValueWrapper ctx
-> Assignment AbstractValueWrapper ctx
-> Assignment AbstractValueWrapper ctx
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 :: BaseType).
BaseTypeRepr x
-> AbstractValueWrapper x
-> AbstractValueWrapper x
-> AbstractValueWrapper x
avJoin' Assignment BaseTypeRepr ctx
flds Assignment AbstractValueWrapper ctx
AbstractValue (BaseStructType ctx)
x Assignment AbstractValueWrapper ctx
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 = Size ctx
-> (forall (tp :: BaseType). Bool -> Index ctx tp -> Bool)
-> Bool
-> Bool
forall k (ctx :: Ctx k) r.
Size ctx -> (forall (tp :: k). r -> Index ctx tp -> r) -> r -> r
Ctx.forIndex (Assignment BaseTypeRepr ctx -> Size ctx
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
forall (tp :: BaseType). Bool -> Index ctx tp -> Bool
f Bool
True
    where f :: Bool -> Ctx.Index ctx tp -> Bool
          f :: Bool -> Index ctx tp -> Bool
f Bool
b Index ctx tp
i = BaseTypeRepr tp -> (Abstractable tp => Bool) -> Bool
forall (bt :: BaseType) a.
BaseTypeRepr bt -> (Abstractable bt => a) -> a
withAbstractable BaseTypeRepr tp
tp (BaseTypeRepr tp -> AbstractValue tp -> AbstractValue tp -> Bool
forall (tp :: BaseType).
Abstractable tp =>
BaseTypeRepr tp -> AbstractValue tp -> AbstractValue tp -> Bool
avOverlap BaseTypeRepr tp
tp (AbstractValueWrapper tp -> AbstractValue tp
forall (tp :: BaseType).
AbstractValueWrapper tp -> AbstractValue tp
unwrapAV AbstractValueWrapper tp
u) (AbstractValueWrapper tp -> AbstractValue tp
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 Assignment BaseTypeRepr ctx -> Index ctx tp -> BaseTypeRepr tp
forall k (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index ctx tp
Index ctx tp
i
                  u :: AbstractValueWrapper tp
u  = Assignment AbstractValueWrapper ctx
AbstractValue (BaseStructType ctx)
x Assignment AbstractValueWrapper ctx
-> Index ctx tp -> AbstractValueWrapper tp
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  = Assignment AbstractValueWrapper ctx
AbstractValue (BaseStructType ctx)
y Assignment AbstractValueWrapper ctx
-> Index ctx tp -> AbstractValueWrapper tp
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 = Size ctx
-> (forall (tp :: BaseType).
    Maybe Bool -> Index ctx tp -> Maybe Bool)
-> Maybe Bool
-> Maybe Bool
forall k (ctx :: Ctx k) r.
Size ctx -> (forall (tp :: k). r -> Index ctx tp -> r) -> r -> r
Ctx.forIndex (Assignment BaseTypeRepr ctx -> Size ctx
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
forall (tp :: BaseType). Maybe Bool -> Index ctx tp -> Maybe Bool
f (Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True)
    where f :: Maybe Bool -> Ctx.Index ctx tp -> Maybe Bool
          f :: 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 (BaseTypeRepr tp -> (Abstractable tp => Maybe Bool) -> Maybe Bool
forall (bt :: BaseType) a.
BaseTypeRepr bt -> (Abstractable bt => a) -> a
withAbstractable BaseTypeRepr tp
tp (BaseTypeRepr tp
-> AbstractValue tp -> AbstractValue tp -> Maybe Bool
forall (tp :: BaseType).
Abstractable tp =>
BaseTypeRepr tp
-> AbstractValue tp -> AbstractValue tp -> Maybe Bool
avCheckEq BaseTypeRepr tp
tp (AbstractValueWrapper tp -> AbstractValue tp
forall (tp :: BaseType).
AbstractValueWrapper tp -> AbstractValue tp
unwrapAV AbstractValueWrapper tp
u) (AbstractValueWrapper tp -> AbstractValue tp
forall (tp :: BaseType).
AbstractValueWrapper tp -> AbstractValue tp
unwrapAV AbstractValueWrapper tp
v)))
            where tp :: BaseTypeRepr tp
tp = Assignment BaseTypeRepr ctx
flds Assignment BaseTypeRepr ctx -> Index ctx tp -> BaseTypeRepr tp
forall k (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index ctx tp
Index ctx tp
i
                  u :: AbstractValueWrapper tp
u  = Assignment AbstractValueWrapper ctx
AbstractValue (BaseStructType ctx)
x Assignment AbstractValueWrapper ctx
-> Index ctx tp -> AbstractValueWrapper tp
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  = Assignment AbstractValueWrapper ctx
AbstractValue (BaseStructType ctx)
y Assignment AbstractValueWrapper ctx
-> Index ctx tp -> AbstractValueWrapper tp
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 :: BaseTypeRepr bt -> (Abstractable bt => a) -> a
withAbstractable BaseTypeRepr bt
bt Abstractable bt => a
k =
  case BaseTypeRepr bt
bt of
    BaseTypeRepr bt
BaseBoolRepr -> a
Abstractable bt => a
k
    BaseBVRepr NatRepr w
_w -> a
Abstractable bt => a
k
    BaseTypeRepr bt
BaseIntegerRepr -> a
Abstractable bt => a
k
    BaseStringRepr StringInfoRepr si
_ -> a
Abstractable bt => a
k
    BaseTypeRepr bt
BaseRealRepr -> a
Abstractable bt => a
k
    BaseTypeRepr bt
BaseComplexRepr -> a
Abstractable bt => a
k
    BaseArrayRepr Assignment BaseTypeRepr (idx ::> tp)
_a BaseTypeRepr xs
_b -> a
Abstractable bt => a
k
    BaseStructRepr Assignment BaseTypeRepr ctx
_flds -> a
Abstractable bt => a
k
    BaseFloatRepr FloatPrecisionRepr fpp
_fpp -> a
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 :: BaseTypeRepr tp -> ConcreteValue tp -> AbstractValue tp -> Bool
avContains BaseTypeRepr tp
tp = BaseTypeRepr tp
-> (Abstractable tp =>
    ConcreteValue tp -> AbstractValue tp -> Bool)
-> ConcreteValue tp
-> AbstractValue tp
-> Bool
forall (bt :: BaseType) a.
BaseTypeRepr bt -> (Abstractable bt => a) -> a
withAbstractable BaseTypeRepr tp
tp ((Abstractable tp => ConcreteValue tp -> AbstractValue tp -> Bool)
 -> ConcreteValue tp -> AbstractValue tp -> Bool)
-> (Abstractable tp =>
    ConcreteValue tp -> AbstractValue tp -> Bool)
-> ConcreteValue tp
-> AbstractValue tp
-> Bool
forall a b. (a -> b) -> a -> b
$ \ConcreteValue tp
x AbstractValue tp
y -> BaseTypeRepr tp -> AbstractValue tp -> AbstractValue tp -> Bool
forall (tp :: BaseType).
Abstractable tp =>
BaseTypeRepr tp -> AbstractValue tp -> AbstractValue tp -> Bool
avOverlap BaseTypeRepr tp
tp (BaseTypeRepr tp -> ConcreteValue tp -> AbstractValue tp
forall (tp :: BaseType).
BaseTypeRepr tp -> ConcreteValue tp -> AbstractValue tp
avSingle BaseTypeRepr tp
tp ConcreteValue tp
x) AbstractValue tp
y