{-|
Module      : What4.Expr.UnaryBV
Description : A "unary" bitvector representation
Copyright   : (c) Galois, Inc 2015-2020
License     : BSD3
Maintainer  : Joe Hendrix <jhendrix@galois.com>

This module defines a data structure for representing a symbolic bitvector
using a form of "unary" representation.

The idea behind this representation is that we associate a predicate to
each possible value of the bitvector that is true if the symbolic value
is less than or equal to the possible value.

As an example, if we had the unary term 'x' equal to
"{ 0 -> false, 1 -> p, 2 -> q, 3 -> t }", then 'x' cannot be '0', has the
value '1' if 'p' is true, the value '2' if 'q & not p' is true, and '3' if
'not q' is true.  By construction, we should have that 'p => q'.
-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DoAndIfThenElse #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
#if MIN_VERSION_base(4,9,0)
{-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
#endif
module What4.Expr.UnaryBV
  ( UnaryBV
  , width
  , size
  , traversePreds
  , constant
  , asConstant
  , unsignedEntries
  , unsignedRanges
  , evaluate
  , sym_evaluate
  , instantiate
  , domain
    -- * Operations
  , add
  , neg
  , mux
  , eq
  , slt
  , ult
  , uext
  , sext
  , trunc
  ) where

import           Control.Exception (assert)
import           Control.Lens
import           Control.Monad
import           Data.Bits
import           Data.Hashable
import           Data.Parameterized.Classes
import           Data.Parameterized.NatRepr
import qualified GHC.TypeNats as Type

import           What4.BaseTypes
import           What4.Interface
import           What4.Utils.BVDomain (BVDomain)
import qualified What4.Utils.BVDomain as BVD

import qualified Data.Map.Strict as Map

type IntMap = Map.Map Integer

-- | @splitLeq k m@ returns a pair @(l,h)@ where @l@ contains
-- all the bindings with a key less than or equal to @k@, and
-- @h@ contains the ones greater than @k@.
splitLeq :: Integer -> IntMap a -> (IntMap a, IntMap a)
splitLeq :: forall a. Integer -> IntMap a -> (IntMap a, IntMap a)
splitLeq Integer
k IntMap a
m =
  case forall k a. Ord k => k -> Map k a -> (Map k a, Maybe a, Map k a)
Map.splitLookup Integer
k IntMap a
m of
    (IntMap a
l, Maybe a
Nothing, IntMap a
h) -> (IntMap a
l,IntMap a
h)
    (IntMap a
l, Just a
v, IntMap a
h) -> (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Integer
k a
v IntMap a
l, IntMap a
h)

-- | Split a map into a lower bound, midpoint, and upperbound if non-empty.
splitEntry :: IntMap a -> Maybe (IntMap a, (Integer, a), IntMap a)
splitEntry :: forall a. IntMap a -> Maybe (IntMap a, (Integer, a), IntMap a)
splitEntry IntMap a
m0 = forall {k} {a}.
Ord k =>
[Map k a] -> Maybe (Map k a, (k, a), Map k a)
go (forall k b. Map k b -> [Map k b]
Map.splitRoot IntMap a
m0)
  where go :: [Map k a] -> Maybe (Map k a, (k, a), Map k a)
go [] = forall a. Maybe a
Nothing
        go [Map k a
m] =
          case forall k a. Map k a -> Maybe ((k, a), Map k a)
Map.minViewWithKey Map k a
m of
            Maybe ((k, a), Map k a)
Nothing -> forall a. Maybe a
Nothing
            Just ((k, a)
p, Map k a
h) -> forall a. a -> Maybe a
Just (forall k a. Map k a
Map.empty, (k, a)
p, Map k a
h)
        go (Map k a
l:Map k a
m:[Map k a]
h) =
          case forall k a. Map k a -> Maybe ((k, a), Map k a)
Map.minViewWithKey Map k a
m of
            Maybe ((k, a), Map k a)
Nothing -> [Map k a] -> Maybe (Map k a, (k, a), Map k a)
go (Map k a
lforall a. a -> [a] -> [a]
:[Map k a]
h)
            Just ((k, a)
p, Map k a
m') | forall k a. Map k a -> Bool
Map.null Map k a
m' -> forall a. a -> Maybe a
Just (Map k a
l, (k, a)
p, forall (f :: Type -> Type) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
Map.unions [Map k a]
h)
                         | Bool
otherwise   -> forall a. a -> Maybe a
Just (Map k a
l, (k, a)
p, forall (f :: Type -> Type) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
Map.unions (Map k a
m'forall a. a -> [a] -> [a]
:[Map k a]
h))

-- | This function eliminates entries where the predicate has the same
-- value.
stripDuplicatePreds :: Eq p => [(Integer,p)] -> [(Integer,p)]
stripDuplicatePreds :: forall p. Eq p => [(Integer, p)] -> [(Integer, p)]
stripDuplicatePreds ((Integer
l,p
p):(Integer
h,p
q):[(Integer, p)]
r)
  | p
p forall a. Eq a => a -> a -> Bool
== p
q = forall p. Eq p => [(Integer, p)] -> [(Integer, p)]
stripDuplicatePreds ((Integer
l,p
p)forall a. a -> [a] -> [a]
:[(Integer, p)]
r)
  | Bool
otherwise = (Integer
l,p
p)forall a. a -> [a] -> [a]
:forall p. Eq p => [(Integer, p)] -> [(Integer, p)]
stripDuplicatePreds ((Integer
h,p
q)forall a. a -> [a] -> [a]
:[(Integer, p)]
r)
stripDuplicatePreds [(Integer, p)
p] = [(Integer, p)
p]
stripDuplicatePreds [] = []

------------------------------------------------------------------------
-- UnaryBV

-- | A unary bitvector encoding where the map contains predicates
-- such as @u^.unaryBVMap^.at i@ holds iff the value represented by @u@
-- is less than or equal to @i@.
--
-- The map stored in the representation should always have a single element,
-- and the largest integer stored in the map should be associated with a
-- predicate representing "true".  This means that if the map contains only
-- a single binding, then it represents a constant.
data UnaryBV p (n::Type.Nat)
   = UnaryBV { forall p (n :: Nat). UnaryBV p n -> NatRepr n
width :: !(NatRepr n)
             , forall p (n :: Nat). UnaryBV p n -> IntMap p
unaryBVMap :: !(IntMap p)
             }

-- | Returns the number of distinct values that this could be.
size :: UnaryBV p n -> Int
size :: forall p (n :: Nat). UnaryBV p n -> Int
size UnaryBV p n
x = forall k a. Map k a -> Int
Map.size (forall p (n :: Nat). UnaryBV p n -> IntMap p
unaryBVMap UnaryBV p n
x)

traversePreds :: Traversal (UnaryBV p n) (UnaryBV q n) p q
traversePreds :: forall p (n :: Nat) q. Traversal (UnaryBV p n) (UnaryBV q n) p q
traversePreds p -> f q
f (UnaryBV NatRepr n
w IntMap p
m) = forall p (n :: Nat). NatRepr n -> IntMap p -> UnaryBV p n
UnaryBV NatRepr n
w forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse p -> f q
f IntMap p
m

instance Eq p => TestEquality (UnaryBV p) where
  testEquality :: forall (a :: Nat) (b :: Nat).
UnaryBV p a -> UnaryBV p b -> Maybe (a :~: b)
testEquality UnaryBV p a
x UnaryBV p b
y = do
    a :~: b
Refl <- forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (forall p (n :: Nat). UnaryBV p n -> NatRepr n
width UnaryBV p a
x) (forall p (n :: Nat). UnaryBV p n -> NatRepr n
width UnaryBV p b
y)
    if forall p (n :: Nat). UnaryBV p n -> IntMap p
unaryBVMap UnaryBV p a
x forall a. Eq a => a -> a -> Bool
== forall p (n :: Nat). UnaryBV p n -> IntMap p
unaryBVMap UnaryBV p b
y then
      forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
    else
      forall a. Maybe a
Nothing
instance Eq p => Eq (UnaryBV p n) where
  UnaryBV p n
x == :: UnaryBV p n -> UnaryBV p n -> Bool
== UnaryBV p n
y = forall a. Maybe a -> Bool
isJust (forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality UnaryBV p n
x UnaryBV p n
y)

instance Hashable p => Hashable (UnaryBV p n) where
  hashWithSalt :: Int -> UnaryBV p n -> Int
hashWithSalt Int
s0 UnaryBV p n
u = forall a k b. (a -> k -> b -> a) -> a -> Map k b -> a
Map.foldlWithKey' forall {a} {a}. (Hashable a, Hashable a) => Int -> a -> a -> Int
go Int
s0 (forall p (n :: Nat). UnaryBV p n -> IntMap p
unaryBVMap UnaryBV p n
u)
    where go :: Int -> a -> a -> Int
go Int
s a
k a
e = forall a. Hashable a => Int -> a -> Int
hashWithSalt (forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s a
k) a
e

-- | Create a unary bitvector term from a constant.
constant :: IsExprBuilder sym
          => sym
          -> NatRepr n
          -> Integer
          -> UnaryBV (Pred sym) n
constant :: forall sym (n :: Nat).
IsExprBuilder sym =>
sym -> NatRepr n -> Integer -> UnaryBV (Pred sym) n
constant sym
sym NatRepr n
w Integer
v = forall p (n :: Nat). NatRepr n -> IntMap p -> UnaryBV p n
UnaryBV NatRepr n
w (forall k a. k -> a -> Map k a
Map.singleton Integer
v' (forall sym. IsExprBuilder sym => sym -> Pred sym
truePred sym
sym))
  where v' :: Integer
v' = forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
w Integer
v

-- | Create a unary bitvector term from a constant.
asConstant :: IsExpr p => UnaryBV (p BaseBoolType) w -> Maybe Integer
asConstant :: forall (p :: BaseType -> Type) (w :: Nat).
IsExpr p =>
UnaryBV (p BaseBoolType) w -> Maybe Integer
asConstant UnaryBV (p BaseBoolType) w
x
  | forall p (n :: Nat). UnaryBV p n -> Int
size UnaryBV (p BaseBoolType) w
x forall a. Eq a => a -> a -> Bool
== Int
1, [(Integer
v,p BaseBoolType
_)] <- forall k a. Map k a -> [(k, a)]
Map.toList (forall p (n :: Nat). UnaryBV p n -> IntMap p
unaryBVMap UnaryBV (p BaseBoolType) w
x) = forall a. a -> Maybe a
Just Integer
v
  | Bool
otherwise = forall a. Maybe a
Nothing

-- | @unsignedRanges v@ returns a set of predicates and ranges
-- where we know that for each entry @(p,l,h)@ and each value
-- @i : l <= i & i <= h@:
--   @p@ iff. @v <= i@
unsignedRanges :: UnaryBV p n
               -> [(p, Integer, Integer)]
unsignedRanges :: forall p (n :: Nat). UnaryBV p n -> [(p, Integer, Integer)]
unsignedRanges UnaryBV p n
v =
    case forall k a. Map k a -> [(k, a)]
Map.toList (forall p (n :: Nat). UnaryBV p n -> IntMap p
unaryBVMap UnaryBV p n
v) of
      [] -> forall a. HasCallStack => [Char] -> a
error [Char]
"internal: unsignedRanges given illegal UnaryBV"
      [(Integer, p)]
l -> forall p. [(Integer, p)] -> [(p, Integer, Integer)]
go [(Integer, p)]
l
  where w :: Integer
        w :: Integer
w = forall (w :: Nat). NatRepr w -> Integer
maxUnsigned (forall p (n :: Nat). UnaryBV p n -> NatRepr n
width UnaryBV p n
v)

        next :: [(Integer,p)] -> Integer
        next :: forall p. [(Integer, p)] -> Integer
next ((Integer
h,p
_):[(Integer, p)]
_) = Integer
hforall a. Num a => a -> a -> a
-Integer
1
        next [] = Integer
w

        go :: [(Integer, p)] -> [(p, Integer, Integer)]
        go :: forall p. [(Integer, p)] -> [(p, Integer, Integer)]
go [] = []
        go ((Integer
l,p
p):[(Integer, p)]
rest) = (p
p,Integer
l,forall p. [(Integer, p)] -> Integer
next [(Integer, p)]
rest) forall a. a -> [a] -> [a]
: forall p. [(Integer, p)] -> [(p, Integer, Integer)]
go [(Integer, p)]
rest

unsignedEntries :: (1 <= n)
                => UnaryBV p n
                -> [(Integer, p)]
unsignedEntries :: forall (n :: Nat) p. (1 <= n) => UnaryBV p n -> [(Integer, p)]
unsignedEntries UnaryBV p n
b = forall k a. Map k a -> [(k, a)]
Map.toList (forall p (n :: Nat). UnaryBV p n -> IntMap p
unaryBVMap UnaryBV p n
b)

-- | Evaluate a unary bitvector as an integer given an evaluation function.
evaluate :: Monad m => (p -> m Bool) -> UnaryBV p n -> m Integer
evaluate :: forall (m :: Type -> Type) p (n :: Nat).
Monad m =>
(p -> m Bool) -> UnaryBV p n -> m Integer
evaluate p -> m Bool
f0 UnaryBV p n
u = forall (m :: Type -> Type) p.
Monad m =>
(p -> m Bool) -> IntMap p -> Integer -> m Integer
go p -> m Bool
f0 (forall p (n :: Nat). UnaryBV p n -> IntMap p
unaryBVMap UnaryBV p n
u) (forall (w :: Nat). NatRepr w -> Integer
maxUnsigned (forall p (n :: Nat). UnaryBV p n -> NatRepr n
width UnaryBV p n
u))
  where go :: Monad m => (p -> m Bool) -> IntMap p -> Integer -> m Integer
        go :: forall (m :: Type -> Type) p.
Monad m =>
(p -> m Bool) -> IntMap p -> Integer -> m Integer
go p -> m Bool
f IntMap p
m Integer
bnd =
          case forall a. IntMap a -> Maybe (IntMap a, (Integer, a), IntMap a)
splitEntry IntMap p
m of
            Maybe (IntMap p, (Integer, p), IntMap p)
Nothing -> forall (m :: Type -> Type) a. Monad m => a -> m a
return Integer
bnd
            Just (IntMap p
l,(Integer
k,p
v),IntMap p
h) -> do
              Bool
b <- p -> m Bool
f p
v
              case Bool
b of
                -- value <= k
                Bool
True -> forall (m :: Type -> Type) p.
Monad m =>
(p -> m Bool) -> IntMap p -> Integer -> m Integer
go p -> m Bool
f IntMap p
l Integer
k
                -- value > k
                Bool
False -> forall (m :: Type -> Type) p.
Monad m =>
(p -> m Bool) -> IntMap p -> Integer -> m Integer
go p -> m Bool
f IntMap p
h Integer
bnd

-- | Evaluate a unary bitvector given an evaluation function.
--
-- This function is used to convert a unary bitvector into some other representation
-- such as a binary bitvector or vector of bits.
--
-- It is polymorphic over the result type 'r', and requires functions for manipulating
-- values of type 'r' to construct it.
sym_evaluate :: (Applicative m, Monad m)
             => (Integer -> m r)
                -- ^ Function for mapping an integer to its bitvector
                -- representation.
             -> (p -> r -> r -> m r)
                -- ^ Function for performing an 'ite' expression on 'r'.
             -> UnaryBV p n
                -- ^ Unary bitvector to evaluate.
             -> m r
sym_evaluate :: forall (m :: Type -> Type) r p (n :: Nat).
(Applicative m, Monad m) =>
(Integer -> m r) -> (p -> r -> r -> m r) -> UnaryBV p n -> m r
sym_evaluate Integer -> m r
cns0 p -> r -> r -> m r
ite0 UnaryBV p n
u = forall (m :: Type -> Type) r p.
(Applicative m, Monad m) =>
(Integer -> m r)
-> (p -> r -> r -> m r) -> IntMap p -> Integer -> m r
go Integer -> m r
cns0 p -> r -> r -> m r
ite0 (forall p (n :: Nat). UnaryBV p n -> IntMap p
unaryBVMap UnaryBV p n
u) (forall (w :: Nat). NatRepr w -> Integer
maxUnsigned (forall p (n :: Nat). UnaryBV p n -> NatRepr n
width UnaryBV p n
u))
  where go :: (Applicative m, Monad m)
           => (Integer -> m r)
           -> (p -> r -> r -> m r)
           -> IntMap p
           -> Integer
           -> m r
        go :: forall (m :: Type -> Type) r p.
(Applicative m, Monad m) =>
(Integer -> m r)
-> (p -> r -> r -> m r) -> IntMap p -> Integer -> m r
go Integer -> m r
cns p -> r -> r -> m r
ite IntMap p
m Integer
bnd =
          case forall a. IntMap a -> Maybe (IntMap a, (Integer, a), IntMap a)
splitEntry IntMap p
m of
            Maybe (IntMap p, (Integer, p), IntMap p)
Nothing -> Integer -> m r
cns Integer
bnd
            Just (IntMap p
l,(Integer
k,p
v),IntMap p
h) -> do
              forall (m :: Type -> Type) a. Monad m => m (m a) -> m a
join forall a b. (a -> b) -> a -> b
$ p -> r -> r -> m r
ite p
v forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: Type -> Type) r p.
(Applicative m, Monad m) =>
(Integer -> m r)
-> (p -> r -> r -> m r) -> IntMap p -> Integer -> m r
go Integer -> m r
cns p -> r -> r -> m r
ite IntMap p
l Integer
k forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall (m :: Type -> Type) r p.
(Applicative m, Monad m) =>
(Integer -> m r)
-> (p -> r -> r -> m r) -> IntMap p -> Integer -> m r
go Integer -> m r
cns p -> r -> r -> m r
ite IntMap p
h Integer
bnd

-- | This function instantiates the predicates in a unary predicate with new predicates.
--
-- The mapping 'f' should be monotonic, that is for all predicates 'p' and 'q,
-- such that 'p |- q', 'f' should satisfy the constraint that 'f p |- f q'.
instantiate :: (Applicative m, Eq q) => (p -> m q) -> UnaryBV p w -> m (UnaryBV q w)
instantiate :: forall (m :: Type -> Type) q p (w :: Nat).
(Applicative m, Eq q) =>
(p -> m q) -> UnaryBV p w -> m (UnaryBV q w)
instantiate p -> m q
f UnaryBV p w
u = Map Integer q -> UnaryBV q w
fin forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse p -> m q
f (forall p (n :: Nat). UnaryBV p n -> IntMap p
unaryBVMap UnaryBV p w
u)
  where fin :: Map Integer q -> UnaryBV q w
fin Map Integer q
m = UnaryBV { width :: NatRepr w
width = forall p (n :: Nat). UnaryBV p n -> NatRepr n
width UnaryBV p w
u
                        , unaryBVMap :: Map Integer q
unaryBVMap = forall k a. [(k, a)] -> Map k a
Map.fromDistinctAscList [(Integer, q)]
l
                        }
          where l :: [(Integer, q)]
l = forall p. Eq p => [(Integer, p)] -> [(Integer, p)]
stripDuplicatePreds (forall k a. Map k a -> [(k, a)]
Map.toList Map Integer q
m)

-- | Return potential values for abstract domain.
domain :: forall p n
        . (1 <= n)
       => (p -> Maybe Bool)
       -> UnaryBV p n
       -> BVDomain n
domain :: forall p (n :: Nat).
(1 <= n) =>
(p -> Maybe Bool) -> UnaryBV p n -> BVDomain n
domain p -> Maybe Bool
f UnaryBV p n
u = forall (w :: Nat). (1 <= w) => NatRepr w -> [Integer] -> BVDomain w
BVD.fromAscEltList (forall p (n :: Nat). UnaryBV p n -> NatRepr n
width UnaryBV p n
u) (IntMap p -> [Integer]
go (forall p (n :: Nat). UnaryBV p n -> IntMap p
unaryBVMap UnaryBV p n
u))
  where go :: IntMap p -> [Integer]
        go :: IntMap p -> [Integer]
go IntMap p
m =
          case forall a. IntMap a -> Maybe (IntMap a, (Integer, a), IntMap a)
splitEntry IntMap p
m of
            Maybe (IntMap p, (Integer, p), IntMap p)
Nothing -> []
            Just (IntMap p
l,(Integer
k,p
v),IntMap p
h) -> do
              case p -> Maybe Bool
f p
v of
                -- value <= k
                Just Bool
True -> Integer
kforall a. a -> [a] -> [a]
:IntMap p -> [Integer]
go IntMap p
l
                -- value > k
                Just Bool
False -> IntMap p -> [Integer]
go IntMap p
h
                Maybe Bool
Nothing -> IntMap p -> [Integer]
go IntMap p
l forall a. [a] -> [a] -> [a]
++ (Integer
kforall a. a -> [a] -> [a]
:IntMap p -> [Integer]
go IntMap p
h)

------------------------------------------------------------------------
-- Operations

-- | This merges two maps used for a unary bitvector int a single map that
-- combines them.
--
-- 'mergeWithKey sym cfn x y' should return a map 'z' such that for all constants
-- 'c', 'z = c' iff 'cfn (x = c) (y = c)'.
mergeWithKey :: forall sym
              . IsExprBuilder sym
             => sym
             -> (Pred sym -> Pred sym -> IO (Pred sym))
             -> IntMap (Pred sym)
             -> IntMap (Pred sym)
             -> IO (IntMap (Pred sym))
mergeWithKey :: forall sym.
IsExprBuilder sym =>
sym
-> (Pred sym -> Pred sym -> IO (Pred sym))
-> IntMap (Pred sym)
-> IntMap (Pred sym)
-> IO (IntMap (Pred sym))
mergeWithKey sym
sym Pred sym -> Pred sym -> IO (Pred sym)
f IntMap (Pred sym)
x IntMap (Pred sym)
y =
    IntMap (Pred sym)
-> Pred sym
-> [(Integer, Pred sym)]
-> Pred sym
-> [(Integer, Pred sym)]
-> IO (IntMap (Pred sym))
go forall k a. Map k a
Map.empty (forall sym. IsExprBuilder sym => sym -> Pred sym
falsePred sym
sym) (forall k a. Map k a -> [(k, a)]
Map.toList IntMap (Pred sym)
x)
                 (forall sym. IsExprBuilder sym => sym -> Pred sym
falsePred sym
sym) (forall k a. Map k a -> [(k, a)]
Map.toList IntMap (Pred sym)
y)
  where go :: IntMap (Pred sym)
           -> Pred sym
           -> [(Integer, Pred sym)]
           -> Pred sym
           -> [(Integer, Pred sym)]
           -> IO (IntMap (Pred sym))
        -- Force "m" to be evaluated"
        go :: IntMap (Pred sym)
-> Pred sym
-> [(Integer, Pred sym)]
-> Pred sym
-> [(Integer, Pred sym)]
-> IO (IntMap (Pred sym))
go IntMap (Pred sym)
m Pred sym
_ [(Integer, Pred sym)]
_ Pred sym
_ [(Integer, Pred sym)]
_ | seq :: forall a b. a -> b -> b
seq IntMap (Pred sym)
m forall a b. (a -> b) -> a -> b
$ Bool
False = forall a. HasCallStack => [Char] -> a
error [Char]
"go bad"
        go IntMap (Pred sym)
m Pred sym
x_prev x_a :: [(Integer, Pred sym)]
x_a@((Integer
x_k,Pred sym
x_p):[(Integer, Pred sym)]
x_r) Pred sym
y_prev y_a :: [(Integer, Pred sym)]
y_a@((Integer
y_k,Pred sym
y_p):[(Integer, Pred sym)]
y_r) =
          case forall a. Ord a => a -> a -> Ordering
compare Integer
x_k Integer
y_k of
            Ordering
LT -> do
              Pred sym
p <- Pred sym -> Pred sym -> IO (Pred sym)
f Pred sym
x_p Pred sym
y_prev
              IntMap (Pred sym)
-> Pred sym
-> [(Integer, Pred sym)]
-> Pred sym
-> [(Integer, Pred sym)]
-> IO (IntMap (Pred sym))
go (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Integer
x_k Pred sym
p IntMap (Pred sym)
m) Pred sym
x_p [(Integer, Pred sym)]
x_r Pred sym
y_prev [(Integer, Pred sym)]
y_a
            Ordering
GT -> do
              Pred sym
p <- Pred sym -> Pred sym -> IO (Pred sym)
f Pred sym
x_prev Pred sym
y_p
              IntMap (Pred sym)
-> Pred sym
-> [(Integer, Pred sym)]
-> Pred sym
-> [(Integer, Pred sym)]
-> IO (IntMap (Pred sym))
go (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Integer
y_k Pred sym
p IntMap (Pred sym)
m) Pred sym
x_prev [(Integer, Pred sym)]
x_a Pred sym
y_p [(Integer, Pred sym)]
y_r
            Ordering
EQ -> do
              Pred sym
p <- Pred sym -> Pred sym -> IO (Pred sym)
f Pred sym
x_p Pred sym
y_p
              IntMap (Pred sym)
-> Pred sym
-> [(Integer, Pred sym)]
-> Pred sym
-> [(Integer, Pred sym)]
-> IO (IntMap (Pred sym))
go (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Integer
x_k Pred sym
p IntMap (Pred sym)
m) Pred sym
x_p [(Integer, Pred sym)]
x_r Pred sym
y_p [(Integer, Pred sym)]
y_r
        go IntMap (Pred sym)
m Pred sym
_ [] Pred sym
_ [(Integer, Pred sym)]
y_a = do
          forall {m :: Type -> Type} {k} {a} {t}.
(Monad m, Ord k) =>
Map k a -> (t -> m a) -> [(k, t)] -> m (Map k a)
go1 IntMap (Pred sym)
m (forall sym. IsExprBuilder sym => sym -> Pred sym
truePred sym
sym Pred sym -> Pred sym -> IO (Pred sym)
`f`) [(Integer, Pred sym)]
y_a
        go IntMap (Pred sym)
m Pred sym
_ [(Integer, Pred sym)]
x_a Pred sym
_ [] = do
          forall {m :: Type -> Type} {k} {a} {t}.
(Monad m, Ord k) =>
Map k a -> (t -> m a) -> [(k, t)] -> m (Map k a)
go1 IntMap (Pred sym)
m (Pred sym -> Pred sym -> IO (Pred sym)
`f` forall sym. IsExprBuilder sym => sym -> Pred sym
truePred sym
sym) [(Integer, Pred sym)]
x_a

        go1 :: Map k a -> (t -> m a) -> [(k, t)] -> m (Map k a)
go1 Map k a
m t -> m a
fn ((k
y_k,t
y_p):[(k, t)]
y_r) = do
          a
p <- t -> m a
fn t
y_p
          Map k a -> (t -> m a) -> [(k, t)] -> m (Map k a)
go1 (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert k
y_k a
p Map k a
m) t -> m a
fn [(k, t)]
y_r
        go1 Map k a
m t -> m a
_ [] =
          forall (m :: Type -> Type) a. Monad m => a -> m a
return Map k a
m

-- | @mux sym c x y@ returns value equal to if @c@ then @x@ else @y@.
-- The number of entries in the return value is at most @size x@
-- + @size y@.
mux :: forall sym n
     . (1 <= n, IsExprBuilder sym)
    => sym
    -> Pred sym
    -> UnaryBV (Pred sym) n
    -> UnaryBV (Pred sym) n
    -> IO (UnaryBV (Pred sym) n)
mux :: forall sym (n :: Nat).
(1 <= n, IsExprBuilder sym) =>
sym
-> Pred sym
-> UnaryBV (Pred sym) n
-> UnaryBV (Pred sym) n
-> IO (UnaryBV (Pred sym) n)
mux sym
sym Pred sym
c UnaryBV (Pred sym) n
x UnaryBV (Pred sym) n
y = forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall p (n :: Nat). NatRepr n -> IntMap p -> UnaryBV p n
UnaryBV (forall p (n :: Nat). UnaryBV p n -> NatRepr n
width UnaryBV (Pred sym) n
x)) forall a b. (a -> b) -> a -> b
$
  forall sym.
IsExprBuilder sym =>
sym
-> (Pred sym -> Pred sym -> IO (Pred sym))
-> IntMap (Pred sym)
-> IntMap (Pred sym)
-> IO (IntMap (Pred sym))
mergeWithKey sym
sym
               (forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> Pred sym -> IO (Pred sym)
itePred sym
sym Pred sym
c)
               (forall p (n :: Nat). UnaryBV p n -> IntMap p
unaryBVMap UnaryBV (Pred sym) n
x)
               (forall p (n :: Nat). UnaryBV p n -> IntMap p
unaryBVMap UnaryBV (Pred sym) n
y)

-- | Return predicate that holds if bitvectors are equal.
eq :: (1 <= n, IsExprBuilder sym)
   => sym
   -> UnaryBV (Pred sym) n
   -> UnaryBV (Pred sym) n
   -> IO (Pred sym)
eq :: forall (n :: Nat) sym.
(1 <= n, IsExprBuilder sym) =>
sym
-> UnaryBV (Pred sym) n -> UnaryBV (Pred sym) n -> IO (Pred sym)
eq sym
sym0 UnaryBV (Pred sym) n
x0 UnaryBV (Pred sym) n
y0 =
    let (Integer
x_k, Pred sym
x_p) = forall k a. Map k a -> (k, a)
Map.findMin (forall p (n :: Nat). UnaryBV p n -> IntMap p
unaryBVMap UnaryBV (Pred sym) n
x0)
     in forall sym.
IsExprBuilder sym =>
sym
-> Pred sym
-> Integer
-> Pred sym
-> IntMap (Pred sym)
-> IntMap (Pred sym)
-> IO (Pred sym)
go sym
sym0 (forall sym. IsExprBuilder sym => sym -> Pred sym
falsePred sym
sym0) Integer
x_k Pred sym
x_p (forall p (n :: Nat). UnaryBV p n -> IntMap p
unaryBVMap UnaryBV (Pred sym) n
x0) (forall p (n :: Nat). UnaryBV p n -> IntMap p
unaryBVMap UnaryBV (Pred sym) n
y0)
  where go :: IsExprBuilder sym
            => sym
            -> Pred sym
            -> Integer
            -> Pred sym
            -> IntMap (Pred sym)
            -> IntMap (Pred sym)
            -> IO (Pred sym)
        go :: forall sym.
IsExprBuilder sym =>
sym
-> Pred sym
-> Integer
-> Pred sym
-> IntMap (Pred sym)
-> IntMap (Pred sym)
-> IO (Pred sym)
go sym
sym Pred sym
r Integer
x_k Pred sym
x_p IntMap (Pred sym)
x IntMap (Pred sym)
y
          | Just (Integer
y_k, Pred sym
y_p) <- forall k v. Ord k => k -> Map k v -> Maybe (k, v)
Map.lookupGE Integer
x_k IntMap (Pred sym)
y =
            case Integer
x_k forall a. Eq a => a -> a -> Bool
== Integer
y_k of
              Bool
False -> do
                forall sym.
IsExprBuilder sym =>
sym
-> Pred sym
-> Integer
-> Pred sym
-> IntMap (Pred sym)
-> IntMap (Pred sym)
-> IO (Pred sym)
go sym
sym Pred sym
r Integer
y_k Pred sym
y_p IntMap (Pred sym)
y IntMap (Pred sym)
x
              Bool
True -> do
                let x_lt :: Pred sym
x_lt = forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall sym. IsExprBuilder sym => sym -> Pred sym
falsePred sym
sym) forall a b. (a, b) -> b
snd (forall k v. Ord k => k -> Map k v -> Maybe (k, v)
Map.lookupLT Integer
x_k IntMap (Pred sym)
x)
                let y_lt :: Pred sym
y_lt = forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall sym. IsExprBuilder sym => sym -> Pred sym
falsePred sym
sym) forall a b. (a, b) -> b
snd (forall k v. Ord k => k -> Map k v -> Maybe (k, v)
Map.lookupLT Integer
x_k IntMap (Pred sym)
y)
                Pred sym
x_is_eq <- forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
x_p forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred sym
sym Pred sym
x_lt
                Pred sym
y_is_eq <- forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
y_p forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred sym
sym Pred sym
y_lt
                Pred sym
r' <- forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
orPred sym
sym Pred sym
r forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
x_is_eq Pred sym
y_is_eq
                case forall k v. Ord k => k -> Map k v -> Maybe (k, v)
Map.lookupGE (Integer
x_kforall a. Num a => a -> a -> a
+Integer
1) IntMap (Pred sym)
x of
                  Just (Integer
x_k', Pred sym
x_p') -> forall sym.
IsExprBuilder sym =>
sym
-> Pred sym
-> Integer
-> Pred sym
-> IntMap (Pred sym)
-> IntMap (Pred sym)
-> IO (Pred sym)
go sym
sym Pred sym
r' Integer
x_k' Pred sym
x_p' IntMap (Pred sym)
x IntMap (Pred sym)
y
                  Maybe (Integer, Pred sym)
Nothing -> forall (m :: Type -> Type) a. Monad m => a -> m a
return Pred sym
r'
        go sym
_ Pred sym
r Integer
_ Pred sym
_ IntMap (Pred sym)
_ IntMap (Pred sym)
_ = forall (m :: Type -> Type) a. Monad m => a -> m a
return Pred sym
r

-- | @compareLt sym x y@ returns predicate that holds
-- if for any @k@, @x < k & not (y <= k)@.
compareLt :: forall sym
           . IsExprBuilder sym
          => sym
          -> IntMap (Pred sym)
          -> IntMap (Pred sym)
          -> IO (Pred sym)
compareLt :: forall sym.
IsExprBuilder sym =>
sym -> IntMap (Pred sym) -> IntMap (Pred sym) -> IO (Pred sym)
compareLt sym
sym IntMap (Pred sym)
x IntMap (Pred sym)
y
    | forall k a. Map k a -> Bool
Map.null IntMap (Pred sym)
y = forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall sym. IsExprBuilder sym => sym -> Pred sym
falsePred sym
sym)
    | Bool
otherwise  = Pred sym -> Integer -> IO (Pred sym)
go (forall sym. IsExprBuilder sym => sym -> Pred sym
falsePred sym
sym) Integer
0
  where go :: Pred sym -- ^ Return predicate for cases where x is less than minimum.
           -> Integer  -- ^ Minimum value to consider for x.
           -> IO (Pred sym)
        go :: Pred sym -> Integer -> IO (Pred sym)
go Pred sym
r Integer
min_x
            -- Let x_k0 be min entry in x to consider next.
          | Just (Integer
x_k, Pred sym
_) <- forall k v. Ord k => k -> Map k v -> Maybe (k, v)
Map.lookupGE Integer
min_x IntMap (Pred sym)
x
            -- Get smallest entry in y that is larger than x_k.
          , Just (Integer
y_k, Pred sym
_) <- forall k v. Ord k => k -> Map k v -> Maybe (k, v)
Map.lookupGT Integer
x_k IntMap (Pred sym)
y
            -- Lookup largest predicate in x for value that is less then y_k.
          , Just (Integer
x_k_max, Pred sym
x_p) <- forall k v. Ord k => k -> Map k v -> Maybe (k, v)
Map.lookupLT Integer
y_k IntMap (Pred sym)
x = do

            -- We know the following:
            -- 1. min_x <= x_k <= x_k_max < y_k.
            -- 2. y > x_k => y >= y_k
            -- 3. x < y_k => x_p

            -- Get predicate asserting x < y_k && not (y <= x_k)
            -- Get predicate asserting x < y_k && y > x_k
            Pred sym
x_and_y_lt_x_k <-
              case forall k v. Ord k => k -> Map k v -> Maybe (k, v)
Map.lookupLT Integer
y_k IntMap (Pred sym)
y of
                Maybe (Integer, Pred sym)
Nothing -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Pred sym
x_p
                Just (Integer
_,Pred sym
y_lt_y_k) -> forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
x_p forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred sym
sym Pred sym
y_lt_y_k

            Pred sym
r' <- forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
orPred sym
sym Pred sym
r Pred sym
x_and_y_lt_x_k
            Pred sym -> Integer -> IO (Pred sym)
go Pred sym
r' (Integer
x_k_maxforall a. Num a => a -> a -> a
+Integer
1)

        go Pred sym
r Integer
_ = forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym (forall a b. (a, b) -> b
snd (forall k a. Map k a -> (k, a)
Map.findMax IntMap (Pred sym)
y)) Pred sym
r

-- | Return predicate that holds if first value is less than other.
ult :: (1 <= n, IsExprBuilder sym)
    => sym
    -> UnaryBV (Pred sym) n
    -> UnaryBV (Pred sym) n
    -> IO (Pred sym)
ult :: forall (n :: Nat) sym.
(1 <= n, IsExprBuilder sym) =>
sym
-> UnaryBV (Pred sym) n -> UnaryBV (Pred sym) n -> IO (Pred sym)
ult sym
sym UnaryBV (Pred sym) n
x UnaryBV (Pred sym) n
y = forall sym.
IsExprBuilder sym =>
sym -> IntMap (Pred sym) -> IntMap (Pred sym) -> IO (Pred sym)
compareLt sym
sym (forall p (n :: Nat). UnaryBV p n -> IntMap p
unaryBVMap UnaryBV (Pred sym) n
x) (forall p (n :: Nat). UnaryBV p n -> IntMap p
unaryBVMap UnaryBV (Pred sym) n
y)

-- | Return predicate that holds if first value is less than other.
slt :: (1 <= n, IsExprBuilder sym)
    => sym
    -> UnaryBV (Pred sym) n
    -> UnaryBV (Pred sym) n
    -> IO (Pred sym)
slt :: forall (n :: Nat) sym.
(1 <= n, IsExprBuilder sym) =>
sym
-> UnaryBV (Pred sym) n -> UnaryBV (Pred sym) n -> IO (Pred sym)
slt sym
sym UnaryBV (Pred sym) n
x UnaryBV (Pred sym) n
y = do
  let mid :: Integer
mid = forall (w :: Nat). (1 <= w) => NatRepr w -> Integer
maxSigned (forall p (n :: Nat). UnaryBV p n -> NatRepr n
width UnaryBV (Pred sym) n
x)

  -- Split map so that we separate the values that will remain positive
  -- from the values that will be negative.
  let (IntMap (Pred sym)
x_pos,IntMap (Pred sym)
x_neg) = forall a. Integer -> IntMap a -> (IntMap a, IntMap a)
splitLeq Integer
mid (forall p (n :: Nat). UnaryBV p n -> IntMap p
unaryBVMap UnaryBV (Pred sym) n
x)

  -- Split map so that we separate the values that will remain positive
  -- from the values that will be negative.
  let (IntMap (Pred sym)
y_pos,IntMap (Pred sym)
y_neg) = forall a. Integer -> IntMap a -> (IntMap a, IntMap a)
splitLeq Integer
mid (forall p (n :: Nat). UnaryBV p n -> IntMap p
unaryBVMap UnaryBV (Pred sym) n
y)

  Pred sym
x_is_neg <-
    if forall k a. Map k a -> Bool
Map.null IntMap (Pred sym)
x_pos then
      forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall sym. IsExprBuilder sym => sym -> Pred sym
truePred sym
sym
    else
      forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred sym
sym (forall a b. (a, b) -> b
snd (forall k a. Map k a -> (k, a)
Map.findMax IntMap (Pred sym)
x_pos))

  Pred sym
pos_case <- forall sym.
IsExprBuilder sym =>
sym -> IntMap (Pred sym) -> IntMap (Pred sym) -> IO (Pred sym)
compareLt sym
sym IntMap (Pred sym)
x_pos IntMap (Pred sym)
y_pos
  Pred sym
neg_case <- forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
x_is_neg forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> IntMap (Pred sym) -> IntMap (Pred sym) -> IO (Pred sym)
compareLt sym
sym IntMap (Pred sym)
x_neg IntMap (Pred sym)
y_neg
  forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
orPred sym
sym Pred sym
pos_case Pred sym
neg_case

splitOnAddOverflow :: Integer -> UnaryBV p n -> (IntMap p, IntMap p)
splitOnAddOverflow :: forall p (n :: Nat). Integer -> UnaryBV p n -> (IntMap p, IntMap p)
splitOnAddOverflow Integer
v UnaryBV p n
x = forall a. HasCallStack => Bool -> a -> a
assert (Integer
0 forall a. Ord a => a -> a -> Bool
<= Integer
v Bool -> Bool -> Bool
&& Integer
v forall a. Ord a => a -> a -> Bool
<= Integer
limit) forall a b. (a -> b) -> a -> b
$
                           forall a. Integer -> IntMap a -> (IntMap a, IntMap a)
splitLeq Integer
overflow_limit (forall p (n :: Nat). UnaryBV p n -> IntMap p
unaryBVMap UnaryBV p n
x)
    where limit :: Integer
limit = forall (w :: Nat). NatRepr w -> Integer
maxUnsigned (forall p (n :: Nat). UnaryBV p n -> NatRepr n
width UnaryBV p n
x)
          overflow_limit :: Integer
overflow_limit = Integer
limit forall a. Num a => a -> a -> a
- Integer
v

completeList :: IsExprBuilder sym
             => sym
             -> IntMap (Pred sym) -- ^ Map to merge into
             -> (Integer -> Integer) -- ^ Monotonic function to update keys with
             -> (Pred sym -> IO (Pred sym)) -- ^ Function on predicate.
             -> IntMap (Pred sym)
             -> IO (IntMap (Pred sym))
completeList :: forall sym.
IsExprBuilder sym =>
sym
-> IntMap (Pred sym)
-> (Integer -> Integer)
-> (Pred sym -> IO (Pred sym))
-> IntMap (Pred sym)
-> IO (IntMap (Pred sym))
completeList sym
sym IntMap (Pred sym)
x Integer -> Integer
keyFn Pred sym -> IO (Pred sym)
predFn IntMap (Pred sym)
m0 = do
  let m1 :: IntMap (Pred sym)
m1 = forall k1 k2 a. (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeysMonotonic Integer -> Integer
keyFn IntMap (Pred sym)
m0
  IntMap (Pred sym)
m2 <- forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Pred sym -> IO (Pred sym)
predFn IntMap (Pred sym)
m1
  forall sym.
IsExprBuilder sym =>
sym
-> (Pred sym -> Pred sym -> IO (Pred sym))
-> IntMap (Pred sym)
-> IntMap (Pred sym)
-> IO (IntMap (Pred sym))
mergeWithKey sym
sym (forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
orPred sym
sym) IntMap (Pred sym)
x IntMap (Pred sym)
m2

addConstant :: forall sym n
             . (1 <= n, IsExprBuilder sym)
            => sym
            -> IntMap (Pred sym)
            -> Pred sym
            -> Integer
            -> Pred sym
            -> UnaryBV (Pred sym) n
            -> IO (IntMap (Pred sym))
addConstant :: forall sym (n :: Nat).
(1 <= n, IsExprBuilder sym) =>
sym
-> IntMap (Pred sym)
-> Pred sym
-> Integer
-> Pred sym
-> UnaryBV (Pred sym) n
-> IO (IntMap (Pred sym))
addConstant sym
sym IntMap (Pred sym)
m0 Pred sym
x_lt Integer
x_val Pred sym
x_leq UnaryBV (Pred sym) n
y = do
  let w :: NatRepr n
w = forall p (n :: Nat). UnaryBV p n -> NatRepr n
width UnaryBV (Pred sym) n
y

  let (IntMap (Pred sym)
y_low, IntMap (Pred sym)
y_high) = forall p (n :: Nat). Integer -> UnaryBV p n -> (IntMap p, IntMap p)
splitOnAddOverflow Integer
x_val UnaryBV (Pred sym) n
y

  IntMap (Pred sym)
m1 <- forall sym.
IsExprBuilder sym =>
sym
-> IntMap (Pred sym)
-> (Integer -> Integer)
-> (Pred sym -> IO (Pred sym))
-> IntMap (Pred sym)
-> IO (IntMap (Pred sym))
completeList sym
sym IntMap (Pred sym)
m0 (Integer
x_val forall a. Num a => a -> a -> a
+) (forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
x_leq) IntMap (Pred sym)
y_low

  -- Add entries when we don't overflow.
  -- If no overflow then continue
  case forall k a. Map k a -> Bool
Map.null IntMap (Pred sym)
y_high of
    Bool
True -> forall (m :: Type -> Type) a. Monad m => a -> m a
return IntMap (Pred sym)
m1
    Bool
False -> do
      -- See if there are any entries that do not overflow.
      -- Compute amount of offset to apply to y_val
      let x_off :: Integer
x_off = Integer
x_valforall a. Num a => a -> a -> a
-Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^forall (n :: Nat). NatRepr n -> Nat
natValue NatRepr n
w
      -- Generate predicate asserting that y overflows and x == x_val
      Pred sym
x_eq <- forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
x_leq forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred sym
sym Pred sym
x_lt
      Pred sym
p <-
        case forall k a. Map k a -> Bool
Map.null IntMap (Pred sym)
y_low of
          Bool
True -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Pred sym
x_eq
          Bool
False -> forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
x_eq forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred sym
sym (forall a b. (a, b) -> b
snd (forall k a. Map k a -> (k, a)
Map.findMax IntMap (Pred sym)
y_low))
      -- Complete next entries
      forall sym.
IsExprBuilder sym =>
sym
-> IntMap (Pred sym)
-> (Integer -> Integer)
-> (Pred sym -> IO (Pred sym))
-> IntMap (Pred sym)
-> IO (IntMap (Pred sym))
completeList sym
sym IntMap (Pred sym)
m1 (Integer
x_off forall a. Num a => a -> a -> a
+) (forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
p) IntMap (Pred sym)
y_high

-- | Add two bitvectors.
--
-- The number of integers in the result will be at most the product of the sizes
-- of the individual bitvectors.
add :: forall sym n
     . (1 <= n, IsExprBuilder sym)
    => sym
    -> UnaryBV (Pred sym) n
    -> UnaryBV (Pred sym) n
    -> IO (UnaryBV (Pred sym) n)
add :: forall sym (n :: Nat).
(1 <= n, IsExprBuilder sym) =>
sym
-> UnaryBV (Pred sym) n
-> UnaryBV (Pred sym) n
-> IO (UnaryBV (Pred sym) n)
add sym
sym UnaryBV (Pred sym) n
x UnaryBV (Pred sym) n
y = IntMap (Pred sym)
-> Pred sym -> [(Integer, Pred sym)] -> IO (UnaryBV (Pred sym) n)
go_x forall k a. Map k a
Map.empty (forall sym. IsExprBuilder sym => sym -> Pred sym
falsePred sym
sym) (forall (n :: Nat) p. (1 <= n) => UnaryBV p n -> [(Integer, p)]
unsignedEntries UnaryBV (Pred sym) n
x)
  where w :: NatRepr n
w = forall p (n :: Nat). UnaryBV p n -> NatRepr n
width UnaryBV (Pred sym) n
x
        go_x :: IntMap (Pred sym)
             -> Pred sym
             -> [(Integer, Pred sym)]
             -> IO (UnaryBV (Pred sym) n)
        go_x :: IntMap (Pred sym)
-> Pred sym -> [(Integer, Pred sym)] -> IO (UnaryBV (Pred sym) n)
go_x IntMap (Pred sym)
m0 Pred sym
_ [] = do
          forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! forall p (n :: Nat). NatRepr n -> IntMap p -> UnaryBV p n
UnaryBV NatRepr n
w IntMap (Pred sym)
m0
        go_x IntMap (Pred sym)
m0 Pred sym
x_lt ((Integer
x_val,Pred sym
x_leq):[(Integer, Pred sym)]
remaining) = do
          IntMap (Pred sym)
m2 <- forall sym (n :: Nat).
(1 <= n, IsExprBuilder sym) =>
sym
-> IntMap (Pred sym)
-> Pred sym
-> Integer
-> Pred sym
-> UnaryBV (Pred sym) n
-> IO (IntMap (Pred sym))
addConstant sym
sym IntMap (Pred sym)
m0 Pred sym
x_lt Integer
x_val Pred sym
x_leq UnaryBV (Pred sym) n
y
          IntMap (Pred sym)
-> Pred sym -> [(Integer, Pred sym)] -> IO (UnaryBV (Pred sym) n)
go_x IntMap (Pred sym)
m2 Pred sym
x_leq [(Integer, Pred sym)]
remaining

-- | Negate a bitvector.
-- The size of the result will be equal to the size of the input.
neg :: forall sym n
     . (1 <= n, IsExprBuilder sym)
    => sym
    -> UnaryBV (Pred sym) n
    -> IO (UnaryBV (Pred sym) n)
neg :: forall sym (n :: Nat).
(1 <= n, IsExprBuilder sym) =>
sym -> UnaryBV (Pred sym) n -> IO (UnaryBV (Pred sym) n)
neg sym
sym UnaryBV (Pred sym) n
x
  | forall k a. Map k a -> Bool
Map.null (forall p (n :: Nat). UnaryBV p n -> IntMap p
unaryBVMap UnaryBV (Pred sym) n
x) = forall a. HasCallStack => [Char] -> a
error [Char]
"Illegal unary value"
  | Bool
otherwise =
    case forall k a. Map k a -> ((k, a), Map k a)
Map.deleteFindMin (forall p (n :: Nat). UnaryBV p n -> IntMap p
unaryBVMap UnaryBV (Pred sym) n
x) of
      -- Special case for constant 0.
      ((Integer
0,Pred sym
_), Map Integer (Pred sym)
m) | forall k a. Map k a -> Bool
Map.null Map Integer (Pred sym)
m -> forall (m :: Type -> Type) a. Monad m => a -> m a
return UnaryBV (Pred sym) n
x
      -- Treat 0 case specially, then recurse on remaining elements.
      ((Integer
0,Pred sym
x_p), Map Integer (Pred sym)
m) -> [(Integer, Pred sym)]
-> Pred sym -> [(Integer, Pred sym)] -> IO (UnaryBV (Pred sym) n)
go [(Integer
0, Pred sym
x_p)] Pred sym
x_p             (forall k a. Map k a -> [(k, a)]
Map.toDescList Map Integer (Pred sym)
m)
      -- Value can't be 0, so just recurse on all ements.
      ((Integer, Pred sym), Map Integer (Pred sym))
_ ->            [(Integer, Pred sym)]
-> Pred sym -> [(Integer, Pred sym)] -> IO (UnaryBV (Pred sym) n)
go []         (forall sym. IsExprBuilder sym => sym -> Pred sym
falsePred sym
sym) (forall k a. Map k a -> [(k, a)]
Map.toDescList (forall p (n :: Nat). UnaryBV p n -> IntMap p
unaryBVMap UnaryBV (Pred sym) n
x))
  where w :: NatRepr n
w = forall p (n :: Nat). UnaryBV p n -> NatRepr n
width UnaryBV (Pred sym) n
x
        -- Iterate through remaining pairs in descending order.
        go :: [(Integer, Pred sym)]
              -- ^ Entries in descending order
           -> Pred sym -- ^ Predicate for first false.
           -> [(Integer, Pred sym)]
              -- ^ Remaining elements in descending order.
           -> IO (UnaryBV (Pred sym) n)
        go :: [(Integer, Pred sym)]
-> Pred sym -> [(Integer, Pred sym)] -> IO (UnaryBV (Pred sym) n)
go [(Integer, Pred sym)]
m Pred sym
p ((Integer
x_k,Pred sym
_) : r :: [(Integer, Pred sym)]
r@((Integer
_,Pred sym
y_p):[(Integer, Pred sym)]
_)) = seq :: forall a b. a -> b -> b
seq [(Integer, Pred sym)]
m forall a b. (a -> b) -> a -> b
$ do
          let z_k :: Integer
z_k = forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
w (forall a. Num a => a -> a
negate Integer
x_k)
          Pred sym
q <- forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
orPred sym
sym Pred sym
p forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred sym
sym Pred sym
y_p
          let pair :: (Integer, Pred sym)
pair = (Integer
z_k,Pred sym
q)
          let m' :: [(Integer, Pred sym)]
m' = (Integer, Pred sym)
pair forall a. a -> [a] -> [a]
: [(Integer, Pred sym)]
m
          seq :: forall a b. a -> b -> b
seq Integer
z_k forall a b. (a -> b) -> a -> b
$ seq :: forall a b. a -> b -> b
seq (Integer, Pred sym)
pair forall a b. (a -> b) -> a -> b
$ seq :: forall a b. a -> b -> b
seq [(Integer, Pred sym)]
m' forall a b. (a -> b) -> a -> b
$ do
          [(Integer, Pred sym)]
-> Pred sym -> [(Integer, Pred sym)] -> IO (UnaryBV (Pred sym) n)
go [(Integer, Pred sym)]
m' Pred sym
p [(Integer, Pred sym)]
r
        go [(Integer, Pred sym)]
m Pred sym
_ [(Integer
x_k,Pred sym
_)] = seq :: forall a b. a -> b -> b
seq [(Integer, Pred sym)]
m forall a b. (a -> b) -> a -> b
$ do
          let z_k :: Integer
z_k = forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
w (forall a. Num a => a -> a
negate Integer
x_k)
          let q :: Pred sym
q = forall sym. IsExprBuilder sym => sym -> Pred sym
truePred sym
sym
          forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! forall p (n :: Nat). NatRepr n -> IntMap p -> UnaryBV p n
UnaryBV NatRepr n
w (forall k a. [(k, a)] -> Map k a
Map.fromDistinctAscList (forall a. [a] -> [a]
reverse ((Integer
z_k,Pred sym
q) forall a. a -> [a] -> [a]
: [(Integer, Pred sym)]
m)))
        go [(Integer, Pred sym)]
_ Pred sym
_ [] = forall a. HasCallStack => [Char] -> a
error [Char]
"Illegal value return in UnaryBV.neg"

-- | Perform a unsigned extension
uext :: (1 <= u, u+1 <= r) => UnaryBV p u -> NatRepr r -> UnaryBV p r
uext :: forall (u :: Nat) (r :: Nat) p.
(1 <= u, (u + 1) <= r) =>
UnaryBV p u -> NatRepr r -> UnaryBV p r
uext UnaryBV p u
x NatRepr r
w' = forall p (n :: Nat). NatRepr n -> IntMap p -> UnaryBV p n
UnaryBV NatRepr r
w' (forall p (n :: Nat). UnaryBV p n -> IntMap p
unaryBVMap UnaryBV p u
x)

-- | Perform a signed extension
sext :: (1 <= u, u+1 <= r) => UnaryBV p u -> NatRepr r -> UnaryBV p r
sext :: forall (u :: Nat) (r :: Nat) p.
(1 <= u, (u + 1) <= r) =>
UnaryBV p u -> NatRepr r -> UnaryBV p r
sext UnaryBV p u
x NatRepr r
w' = forall p (n :: Nat). NatRepr n -> IntMap p -> UnaryBV p n
UnaryBV NatRepr r
w' (forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map Integer p
neg_entries Map Integer p
l)
  where w :: NatRepr u
w = forall p (n :: Nat). UnaryBV p n -> NatRepr n
width UnaryBV p u
x
        mid :: Integer
mid = forall (w :: Nat). (1 <= w) => NatRepr w -> Integer
maxSigned NatRepr u
w
        (Map Integer p
l,Map Integer p
h) = forall a. Integer -> IntMap a -> (IntMap a, IntMap a)
splitLeq Integer
mid (forall p (n :: Nat). UnaryBV p n -> IntMap p
unaryBVMap UnaryBV p u
x)

        diff :: Integer
diff = Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^forall (n :: Nat). NatRepr n -> Nat
natValue NatRepr r
w' forall a. Num a => a -> a -> a
- Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^forall (n :: Nat). NatRepr n -> Nat
natValue NatRepr u
w
        neg_entries :: Map Integer p
neg_entries = forall k1 k2 a. (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeysMonotonic (forall a. Num a => a -> a -> a
+ Integer
diff) Map Integer p
h

-- | Perform a struncation.
trunc :: forall sym u r
       . (IsExprBuilder sym, 1 <= u, u <= r)
      => sym
      -> UnaryBV (Pred sym) r
      -> NatRepr u
      -> IO (UnaryBV (Pred sym) u)
trunc :: forall sym (u :: Nat) (r :: Nat).
(IsExprBuilder sym, 1 <= u, u <= r) =>
sym
-> UnaryBV (Pred sym) r -> NatRepr u -> IO (UnaryBV (Pred sym) u)
trunc sym
sym UnaryBV (Pred sym) r
x NatRepr u
w
  | Just u :~: r
Refl <- forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality NatRepr u
w (forall p (n :: Nat). UnaryBV p n -> NatRepr n
width UnaryBV (Pred sym) r
x) = forall (m :: Type -> Type) a. Monad m => a -> m a
return UnaryBV (Pred sym) r
x
  | Bool
otherwise = IntMap (Pred sym)
-> Pred sym -> IntMap (Pred sym) -> IO (UnaryBV (Pred sym) u)
go forall k a. Map k a
Map.empty (forall sym. IsExprBuilder sym => sym -> Pred sym
truePred sym
sym) (forall p (n :: Nat). UnaryBV p n -> IntMap p
unaryBVMap UnaryBV (Pred sym) r
x)
  where go :: IntMap (Pred sym)
           -> Pred sym
           -> IntMap (Pred sym)
           -> IO (UnaryBV (Pred sym) u)
        go :: IntMap (Pred sym)
-> Pred sym -> IntMap (Pred sym) -> IO (UnaryBV (Pred sym) u)
go IntMap (Pred sym)
result Pred sym
toRemove IntMap (Pred sym)
remaining
          | forall k a. Map k a -> Bool
Map.null IntMap (Pred sym)
remaining =
            forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! forall p (n :: Nat). NatRepr n -> IntMap p -> UnaryBV p n
UnaryBV NatRepr u
w IntMap (Pred sym)
result
          | Bool
otherwise = do
            let (Integer
k,Pred sym
_) = forall k a. Map k a -> (k, a)
Map.findMin IntMap (Pred sym)
remaining
            -- Get base offset
            let base :: Integer
base = Integer
k forall a. Bits a => a -> a -> a
`xor` (forall (w :: Nat). NatRepr w -> Integer
maxUnsigned NatRepr u
w)
            let next :: Integer
next = Integer
base forall a. Num a => a -> a -> a
+ forall (w :: Nat). NatRepr w -> Integer
maxUnsigned NatRepr u
w
            let (IntMap (Pred sym)
l,IntMap (Pred sym)
h) = forall a. Integer -> IntMap a -> (IntMap a, IntMap a)
splitLeq Integer
next IntMap (Pred sym)
remaining

            forall a. HasCallStack => Bool -> a -> a
assert (Bool -> Bool
not (forall k a. Map k a -> Bool
Map.null IntMap (Pred sym)
l)) forall a b. (a -> b) -> a -> b
$ do
            -- Get entries to add.
            IntMap (Pred sym)
result' <- forall sym.
IsExprBuilder sym =>
sym
-> IntMap (Pred sym)
-> (Integer -> Integer)
-> (Pred sym -> IO (Pred sym))
-> IntMap (Pred sym)
-> IO (IntMap (Pred sym))
completeList sym
sym IntMap (Pred sym)
result (forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr u
w) (forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
toRemove) IntMap (Pred sym)
l

            let (Integer
_,Pred sym
p) = forall k a. Map k a -> (k, a)
Map.findMax IntMap (Pred sym)
l
            Pred sym
toRemove' <- forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred sym
sym Pred sym
p
            IntMap (Pred sym)
-> Pred sym -> IntMap (Pred sym) -> IO (UnaryBV (Pred sym) u)
go IntMap (Pred sym)
result' Pred sym
toRemove' IntMap (Pred sym)
h