-- |
-- Module      :  Cryptol.Backend.SBV
-- Copyright   :  (c) 2013-2016 Galois, Inc.
-- License     :  BSD3
-- Maintainer  :  cryptol@galois.com
-- Stability   :  provisional
-- Portability :  portable

{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE ViewPatterns #-}
module Cryptol.Backend.SBV
  ( SBV(..), SBVEval(..), SBVResult(..)
  , literalSWord
  , freshSBool_
  , freshBV_
  , freshSInteger_
  , addDefEqn
  , ashr
  , lshr
  , shl
  , evalPanic
  , svFromInteger
  , svToInteger
  ) where

import qualified Control.Exception as X
import           Control.Concurrent.MVar
import           Control.Monad.IO.Class (MonadIO(..))
import           Data.Bits (bit, complement)
import           Data.List (foldl')

import qualified GHC.Integer.GMP.Internals as Integer

import Data.SBV.Dynamic as SBV
import qualified Data.SBV.Internals as SBV

import Cryptol.Backend
import Cryptol.Backend.Concrete ( integerToChar )
import Cryptol.Backend.Monad
  ( Eval(..), blackhole, delayFill, evalSpark
  , EvalError(..), EvalErrorEx(..), Unsupported(..)
  , modifyCallStack, getCallStack
  )

import Cryptol.Utils.Panic (panic)

data SBV =
  SBV
  { SBV -> MVar State
sbvStateVar     :: MVar (SBV.State)
  , SBV -> MVar SVal
sbvDefRelations :: MVar SVal
  }

-- Utility operations -------------------------------------------------------------

fromBitsLE :: [SBit SBV] -> SWord SBV
fromBitsLE :: [SBit SBV] -> SWord SBV
fromBitsLE [SBit SBV]
bs = (SVal -> SVal -> SVal) -> SVal -> [SVal] -> SVal
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' SVal -> SVal -> SVal
f (Int -> Integer -> SWord SBV
literalSWord Int
0 Integer
0) [SVal]
[SBit SBV]
bs
  where f :: SVal -> SVal -> SVal
f SVal
w SVal
b = SVal -> SVal -> SVal
svJoin (SVal -> SVal
svToWord1 SVal
b) SVal
w

packSBV :: [SBit SBV] -> SWord SBV
packSBV :: [SBit SBV] -> SWord SBV
packSBV [SBit SBV]
bs = [SBit SBV] -> SWord SBV
fromBitsLE ([SVal] -> [SVal]
forall a. [a] -> [a]
reverse [SVal]
[SBit SBV]
bs)

unpackSBV :: SWord SBV -> [SBit SBV]
unpackSBV :: SWord SBV -> [SBit SBV]
unpackSBV SWord SBV
x = [ SVal -> Int -> SVal
svTestBit SVal
SWord SBV
x Int
i | Int
i <- [Int] -> [Int]
forall a. [a] -> [a]
reverse [Int
0 .. SVal -> Int
forall a. HasKind a => a -> Int
intSizeOf SVal
SWord SBV
x Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1] ]

literalSWord :: Int -> Integer -> SWord SBV
literalSWord :: Int -> Integer -> SWord SBV
literalSWord Int
w Integer
i = Kind -> Integer -> SVal
svInteger (Bool -> Int -> Kind
KBounded Bool
False Int
w) Integer
i

svMkSymVar_ :: Maybe Quantifier -> Kind -> Maybe String -> SBV.State -> IO SVal
#if MIN_VERSION_sbv(8,8,0)
svMkSymVar_ :: Maybe Quantifier -> Kind -> Maybe String -> State -> IO SVal
svMkSymVar_ = VarContext -> Kind -> Maybe String -> State -> IO SVal
svMkSymVar (VarContext -> Kind -> Maybe String -> State -> IO SVal)
-> (Maybe Quantifier -> VarContext)
-> Maybe Quantifier
-> Kind
-> Maybe String
-> State
-> IO SVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Quantifier -> VarContext
SBV.NonQueryVar
#else
svMkSymVar_ = svMkSymVar
#endif

freshBV_ :: SBV -> Int -> IO (SWord SBV)
freshBV_ :: SBV -> Int -> IO (SWord SBV)
freshBV_ (SBV MVar State
stateVar MVar SVal
_) Int
w =
  MVar State -> (State -> IO SVal) -> IO SVal
forall a b. MVar a -> (a -> IO b) -> IO b
withMVar MVar State
stateVar (Maybe Quantifier -> Kind -> Maybe String -> State -> IO SVal
svMkSymVar_ Maybe Quantifier
forall a. Maybe a
Nothing (Bool -> Int -> Kind
KBounded Bool
False Int
w) Maybe String
forall a. Maybe a
Nothing)

freshSBool_ :: SBV -> IO (SBit SBV)
freshSBool_ :: SBV -> IO (SBit SBV)
freshSBool_ (SBV MVar State
stateVar MVar SVal
_) =
  MVar State -> (State -> IO SVal) -> IO SVal
forall a b. MVar a -> (a -> IO b) -> IO b
withMVar MVar State
stateVar (Maybe Quantifier -> Kind -> Maybe String -> State -> IO SVal
svMkSymVar_ Maybe Quantifier
forall a. Maybe a
Nothing Kind
KBool Maybe String
forall a. Maybe a
Nothing)

freshSInteger_ :: SBV -> IO (SInteger SBV)
freshSInteger_ :: SBV -> IO (SInteger SBV)
freshSInteger_ (SBV MVar State
stateVar MVar SVal
_) =
  MVar State -> (State -> IO SVal) -> IO SVal
forall a b. MVar a -> (a -> IO b) -> IO b
withMVar MVar State
stateVar (Maybe Quantifier -> Kind -> Maybe String -> State -> IO SVal
svMkSymVar_ Maybe Quantifier
forall a. Maybe a
Nothing Kind
KUnbounded Maybe String
forall a. Maybe a
Nothing)


-- SBV Evaluation monad -------------------------------------------------------

data SBVResult a
  = SBVError !EvalErrorEx
  | SBVResult !SVal !a -- safety predicate and result

instance Functor SBVResult where
  fmap :: (a -> b) -> SBVResult a -> SBVResult b
fmap a -> b
_ (SBVError EvalErrorEx
err) = EvalErrorEx -> SBVResult b
forall a. EvalErrorEx -> SBVResult a
SBVError EvalErrorEx
err
  fmap a -> b
f (SBVResult SVal
p a
x) = SVal -> b -> SBVResult b
forall a. SVal -> a -> SBVResult a
SBVResult SVal
p (a -> b
f a
x)

instance Applicative SBVResult where
  pure :: a -> SBVResult a
pure = SVal -> a -> SBVResult a
forall a. SVal -> a -> SBVResult a
SBVResult SVal
svTrue
  SBVError EvalErrorEx
err <*> :: SBVResult (a -> b) -> SBVResult a -> SBVResult b
<*> SBVResult a
_ = EvalErrorEx -> SBVResult b
forall a. EvalErrorEx -> SBVResult a
SBVError EvalErrorEx
err
  SBVResult (a -> b)
_ <*> SBVError EvalErrorEx
err = EvalErrorEx -> SBVResult b
forall a. EvalErrorEx -> SBVResult a
SBVError EvalErrorEx
err
  SBVResult SVal
p1 a -> b
f <*> SBVResult SVal
p2 a
x = SVal -> b -> SBVResult b
forall a. SVal -> a -> SBVResult a
SBVResult (SVal -> SVal -> SVal
svAnd SVal
p1 SVal
p2) (a -> b
f a
x)

instance Monad SBVResult where
  return :: a -> SBVResult a
return = a -> SBVResult a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
  SBVError EvalErrorEx
err >>= :: SBVResult a -> (a -> SBVResult b) -> SBVResult b
>>= a -> SBVResult b
_ = EvalErrorEx -> SBVResult b
forall a. EvalErrorEx -> SBVResult a
SBVError EvalErrorEx
err
  SBVResult SVal
px a
x >>= a -> SBVResult b
m =
    case a -> SBVResult b
m a
x of
      SBVError EvalErrorEx
err   -> EvalErrorEx -> SBVResult b
forall a. EvalErrorEx -> SBVResult a
SBVError EvalErrorEx
err
      SBVResult SVal
pm b
z -> SVal -> b -> SBVResult b
forall a. SVal -> a -> SBVResult a
SBVResult (SVal -> SVal -> SVal
svAnd SVal
px SVal
pm) b
z

newtype SBVEval a = SBVEval{ SBVEval a -> Eval (SBVResult a)
sbvEval :: Eval (SBVResult a) }
  deriving (a -> SBVEval b -> SBVEval a
(a -> b) -> SBVEval a -> SBVEval b
(forall a b. (a -> b) -> SBVEval a -> SBVEval b)
-> (forall a b. a -> SBVEval b -> SBVEval a) -> Functor SBVEval
forall a b. a -> SBVEval b -> SBVEval a
forall a b. (a -> b) -> SBVEval a -> SBVEval b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> SBVEval b -> SBVEval a
$c<$ :: forall a b. a -> SBVEval b -> SBVEval a
fmap :: (a -> b) -> SBVEval a -> SBVEval b
$cfmap :: forall a b. (a -> b) -> SBVEval a -> SBVEval b
Functor)

instance Applicative SBVEval where
  pure :: a -> SBVEval a
pure = Eval (SBVResult a) -> SBVEval a
forall a. Eval (SBVResult a) -> SBVEval a
SBVEval (Eval (SBVResult a) -> SBVEval a)
-> (a -> Eval (SBVResult a)) -> a -> SBVEval a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SBVResult a -> Eval (SBVResult a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SBVResult a -> Eval (SBVResult a))
-> (a -> SBVResult a) -> a -> Eval (SBVResult a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> SBVResult a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
  SBVEval (a -> b)
f <*> :: SBVEval (a -> b) -> SBVEval a -> SBVEval b
<*> SBVEval a
x = Eval (SBVResult b) -> SBVEval b
forall a. Eval (SBVResult a) -> SBVEval a
SBVEval (Eval (SBVResult b) -> SBVEval b)
-> Eval (SBVResult b) -> SBVEval b
forall a b. (a -> b) -> a -> b
$
    do SBVResult (a -> b)
f' <- SBVEval (a -> b) -> Eval (SBVResult (a -> b))
forall a. SBVEval a -> Eval (SBVResult a)
sbvEval SBVEval (a -> b)
f
       SBVResult a
x' <- SBVEval a -> Eval (SBVResult a)
forall a. SBVEval a -> Eval (SBVResult a)
sbvEval SBVEval a
x
       SBVResult b -> Eval (SBVResult b)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SBVResult (a -> b)
f' SBVResult (a -> b) -> SBVResult a -> SBVResult b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SBVResult a
x')

instance Monad SBVEval where
  return :: a -> SBVEval a
return = a -> SBVEval a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
  SBVEval a
x >>= :: SBVEval a -> (a -> SBVEval b) -> SBVEval b
>>= a -> SBVEval b
f = Eval (SBVResult b) -> SBVEval b
forall a. Eval (SBVResult a) -> SBVEval a
SBVEval (Eval (SBVResult b) -> SBVEval b)
-> Eval (SBVResult b) -> SBVEval b
forall a b. (a -> b) -> a -> b
$
    SBVEval a -> Eval (SBVResult a)
forall a. SBVEval a -> Eval (SBVResult a)
sbvEval SBVEval a
x Eval (SBVResult a)
-> (SBVResult a -> Eval (SBVResult b)) -> Eval (SBVResult b)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      SBVError EvalErrorEx
err -> SBVResult b -> Eval (SBVResult b)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (EvalErrorEx -> SBVResult b
forall a. EvalErrorEx -> SBVResult a
SBVError EvalErrorEx
err)
      SBVResult SVal
px a
x' ->
        SBVEval b -> Eval (SBVResult b)
forall a. SBVEval a -> Eval (SBVResult a)
sbvEval (a -> SBVEval b
f a
x') Eval (SBVResult b)
-> (SBVResult b -> Eval (SBVResult b)) -> Eval (SBVResult b)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          SBVError EvalErrorEx
err -> SBVResult b -> Eval (SBVResult b)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (EvalErrorEx -> SBVResult b
forall a. EvalErrorEx -> SBVResult a
SBVError EvalErrorEx
err)
          SBVResult SVal
pz b
z -> SBVResult b -> Eval (SBVResult b)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> b -> SBVResult b
forall a. SVal -> a -> SBVResult a
SBVResult (SVal -> SVal -> SVal
svAnd SVal
px SVal
pz) b
z)

instance MonadIO SBVEval where
  liftIO :: IO a -> SBVEval a
liftIO IO a
m = Eval (SBVResult a) -> SBVEval a
forall a. Eval (SBVResult a) -> SBVEval a
SBVEval (Eval (SBVResult a) -> SBVEval a)
-> Eval (SBVResult a) -> SBVEval a
forall a b. (a -> b) -> a -> b
$ (a -> SBVResult a) -> Eval a -> Eval (SBVResult a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> SBVResult a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (IO a -> Eval a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO a
m)


addDefEqn :: SBV -> SVal -> IO ()
addDefEqn :: SBV -> SVal -> IO ()
addDefEqn (SBV MVar State
_ MVar SVal
relsVar) SVal
b = MVar SVal -> (SVal -> IO SVal) -> IO ()
forall a. MVar a -> (a -> IO a) -> IO ()
modifyMVar_ MVar SVal
relsVar (SVal -> IO SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> IO SVal) -> (SVal -> SVal) -> SVal -> IO SVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SVal -> SVal -> SVal
svAnd SVal
b)

-- Symbolic Big-endian Words -------------------------------------------------------

instance Backend SBV where
  type SBit SBV = SVal
  type SWord SBV = SVal
  type SInteger SBV = SVal
  type SFloat SBV = ()        -- XXX: not implemented
  type SEval SBV = SBVEval

  raiseError :: SBV -> EvalError -> SEval SBV a
raiseError SBV
_ EvalError
err = Eval (SBVResult a) -> SBVEval a
forall a. Eval (SBVResult a) -> SBVEval a
SBVEval (Eval (SBVResult a) -> SBVEval a)
-> Eval (SBVResult a) -> SBVEval a
forall a b. (a -> b) -> a -> b
$
    do CallStack
stk <- Eval CallStack
getCallStack
       SBVResult a -> Eval (SBVResult a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (EvalErrorEx -> SBVResult a
forall a. EvalErrorEx -> SBVResult a
SBVError (CallStack -> EvalError -> EvalErrorEx
EvalErrorEx CallStack
stk EvalError
err))

  assertSideCondition :: SBV -> SBit SBV -> EvalError -> SEval SBV ()
assertSideCondition SBV
sym SBit SBV
cond EvalError
err
    | Just Bool
False <- SVal -> Maybe Bool
svAsBool SVal
SBit SBV
cond = SBV -> EvalError -> SEval SBV ()
forall sym a. Backend sym => sym -> EvalError -> SEval sym a
raiseError SBV
sym EvalError
err
    | Bool
otherwise = Eval (SBVResult ()) -> SBVEval ()
forall a. Eval (SBVResult a) -> SBVEval a
SBVEval (SBVResult () -> Eval (SBVResult ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> () -> SBVResult ()
forall a. SVal -> a -> SBVResult a
SBVResult SVal
SBit SBV
cond ()))

  isReady :: SBV -> SEval SBV a -> Bool
isReady SBV
_ (SBVEval (Ready _)) = Bool
True
  isReady SBV
_ SEval SBV a
_ = Bool
False

  sDelayFill :: SBV
-> SEval SBV a
-> Maybe (SEval SBV a)
-> String
-> SEval SBV (SEval SBV a)
sDelayFill SBV
_ SEval SBV a
m Maybe (SEval SBV a)
retry String
msg = Eval (SBVResult (SBVEval a)) -> SBVEval (SBVEval a)
forall a. Eval (SBVResult a) -> SBVEval a
SBVEval (Eval (SBVResult (SBVEval a)) -> SBVEval (SBVEval a))
-> Eval (SBVResult (SBVEval a)) -> SBVEval (SBVEval a)
forall a b. (a -> b) -> a -> b
$
    do Eval (SBVResult a)
m' <- Eval (SBVResult a)
-> Maybe (Eval (SBVResult a))
-> String
-> Eval (Eval (SBVResult a))
forall a. Eval a -> Maybe (Eval a) -> String -> Eval (Eval a)
delayFill (SBVEval a -> Eval (SBVResult a)
forall a. SBVEval a -> Eval (SBVResult a)
sbvEval SEval SBV a
SBVEval a
m) (SBVEval a -> Eval (SBVResult a)
forall a. SBVEval a -> Eval (SBVResult a)
sbvEval (SBVEval a -> Eval (SBVResult a))
-> Maybe (SBVEval a) -> Maybe (Eval (SBVResult a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (SEval SBV a)
Maybe (SBVEval a)
retry) String
msg
       SBVResult (SBVEval a) -> Eval (SBVResult (SBVEval a))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SBVEval a -> SBVResult (SBVEval a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Eval (SBVResult a) -> SBVEval a
forall a. Eval (SBVResult a) -> SBVEval a
SBVEval Eval (SBVResult a)
m'))

  sSpark :: SBV -> SEval SBV a -> SEval SBV (SEval SBV a)
sSpark SBV
_ SEval SBV a
m = Eval (SBVResult (SBVEval a)) -> SBVEval (SBVEval a)
forall a. Eval (SBVResult a) -> SBVEval a
SBVEval (Eval (SBVResult (SBVEval a)) -> SBVEval (SBVEval a))
-> Eval (SBVResult (SBVEval a)) -> SBVEval (SBVEval a)
forall a b. (a -> b) -> a -> b
$
    do Eval (SBVResult a)
m' <- Eval (SBVResult a) -> Eval (Eval (SBVResult a))
forall a. Eval a -> Eval (Eval a)
evalSpark (SBVEval a -> Eval (SBVResult a)
forall a. SBVEval a -> Eval (SBVResult a)
sbvEval SEval SBV a
SBVEval a
m)
       SBVResult (SBVEval a) -> Eval (SBVResult (SBVEval a))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SBVEval a -> SBVResult (SBVEval a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Eval (SBVResult a) -> SBVEval a
forall a. Eval (SBVResult a) -> SBVEval a
SBVEval Eval (SBVResult a)
m'))

  sDeclareHole :: SBV
-> String -> SEval SBV (SEval SBV a, SEval SBV a -> SEval SBV ())
sDeclareHole SBV
_ String
msg = Eval (SBVResult (SBVEval a, SBVEval a -> SBVEval ()))
-> SBVEval (SBVEval a, SBVEval a -> SBVEval ())
forall a. Eval (SBVResult a) -> SBVEval a
SBVEval (Eval (SBVResult (SBVEval a, SBVEval a -> SBVEval ()))
 -> SBVEval (SBVEval a, SBVEval a -> SBVEval ()))
-> Eval (SBVResult (SBVEval a, SBVEval a -> SBVEval ()))
-> SBVEval (SBVEval a, SBVEval a -> SBVEval ())
forall a b. (a -> b) -> a -> b
$
    do (Eval (SBVResult a)
hole, Eval (SBVResult a) -> Eval ()
fill) <- String -> Eval (Eval (SBVResult a), Eval (SBVResult a) -> Eval ())
forall a. String -> Eval (Eval a, Eval a -> Eval ())
blackhole String
msg
       SBVResult (SBVEval a, SBVEval a -> SBVEval ())
-> Eval (SBVResult (SBVEval a, SBVEval a -> SBVEval ()))
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((SBVEval a, SBVEval a -> SBVEval ())
-> SBVResult (SBVEval a, SBVEval a -> SBVEval ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Eval (SBVResult a) -> SBVEval a
forall a. Eval (SBVResult a) -> SBVEval a
SBVEval Eval (SBVResult a)
hole, \SBVEval a
m -> Eval (SBVResult ()) -> SBVEval ()
forall a. Eval (SBVResult a) -> SBVEval a
SBVEval ((() -> SBVResult ()) -> Eval () -> Eval (SBVResult ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap () -> SBVResult ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Eval () -> Eval (SBVResult ())) -> Eval () -> Eval (SBVResult ())
forall a b. (a -> b) -> a -> b
$ Eval (SBVResult a) -> Eval ()
fill (SBVEval a -> Eval (SBVResult a)
forall a. SBVEval a -> Eval (SBVResult a)
sbvEval SBVEval a
m))))

  sModifyCallStack :: SBV -> (CallStack -> CallStack) -> SEval SBV a -> SEval SBV a
sModifyCallStack SBV
_ CallStack -> CallStack
f (SBVEval m) = Eval (SBVResult a) -> SBVEval a
forall a. Eval (SBVResult a) -> SBVEval a
SBVEval (Eval (SBVResult a) -> SBVEval a)
-> Eval (SBVResult a) -> SBVEval a
forall a b. (a -> b) -> a -> b
$
    (CallStack -> CallStack)
-> Eval (SBVResult a) -> Eval (SBVResult a)
forall a. (CallStack -> CallStack) -> Eval a -> Eval a
modifyCallStack CallStack -> CallStack
f Eval (SBVResult a)
m

  sGetCallStack :: SBV -> SEval SBV CallStack
sGetCallStack SBV
_ = Eval (SBVResult CallStack) -> SBVEval CallStack
forall a. Eval (SBVResult a) -> SBVEval a
SBVEval (CallStack -> SBVResult CallStack
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CallStack -> SBVResult CallStack)
-> Eval CallStack -> Eval (SBVResult CallStack)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Eval CallStack
getCallStack)

  mergeEval :: SBV
-> (SBit SBV -> a -> a -> SEval SBV a)
-> SBit SBV
-> SEval SBV a
-> SEval SBV a
-> SEval SBV a
mergeEval SBV
_sym SBit SBV -> a -> a -> SEval SBV a
f SBit SBV
c SEval SBV a
mx SEval SBV a
my = Eval (SBVResult a) -> SBVEval a
forall a. Eval (SBVResult a) -> SBVEval a
SBVEval (Eval (SBVResult a) -> SBVEval a)
-> Eval (SBVResult a) -> SBVEval a
forall a b. (a -> b) -> a -> b
$
    do SBVResult a
rx <- SBVEval a -> Eval (SBVResult a)
forall a. SBVEval a -> Eval (SBVResult a)
sbvEval SEval SBV a
SBVEval a
mx
       SBVResult a
ry <- SBVEval a -> Eval (SBVResult a)
forall a. SBVEval a -> Eval (SBVResult a)
sbvEval SEval SBV a
SBVEval a
my
       case (SBVResult a
rx, SBVResult a
ry) of
         (SBVError EvalErrorEx
err, SBVError EvalErrorEx
_) ->
           SBVResult a -> Eval (SBVResult a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SBVResult a -> Eval (SBVResult a))
-> SBVResult a -> Eval (SBVResult a)
forall a b. (a -> b) -> a -> b
$ EvalErrorEx -> SBVResult a
forall a. EvalErrorEx -> SBVResult a
SBVError EvalErrorEx
err -- arbitrarily choose left error to report
         (SBVError EvalErrorEx
_, SBVResult SVal
p a
y) ->
           SBVResult a -> Eval (SBVResult a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SBVResult a -> Eval (SBVResult a))
-> SBVResult a -> Eval (SBVResult a)
forall a b. (a -> b) -> a -> b
$ SVal -> a -> SBVResult a
forall a. SVal -> a -> SBVResult a
SBVResult (SVal -> SVal -> SVal
svAnd (SVal -> SVal
svNot SVal
SBit SBV
c) SVal
p) a
y
         (SBVResult SVal
p a
x, SBVError EvalErrorEx
_) ->
           SBVResult a -> Eval (SBVResult a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SBVResult a -> Eval (SBVResult a))
-> SBVResult a -> Eval (SBVResult a)
forall a b. (a -> b) -> a -> b
$ SVal -> a -> SBVResult a
forall a. SVal -> a -> SBVResult a
SBVResult (SVal -> SVal -> SVal
svAnd SVal
SBit SBV
c SVal
p) a
x
         (SBVResult SVal
px a
x, SBVResult SVal
py a
y) ->
           do SBVResult a
zr <- SBVEval a -> Eval (SBVResult a)
forall a. SBVEval a -> Eval (SBVResult a)
sbvEval (SBit SBV -> a -> a -> SEval SBV a
f SBit SBV
c a
x a
y)
              case SBVResult a
zr of
                SBVError EvalErrorEx
err -> SBVResult a -> Eval (SBVResult a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SBVResult a -> Eval (SBVResult a))
-> SBVResult a -> Eval (SBVResult a)
forall a b. (a -> b) -> a -> b
$ EvalErrorEx -> SBVResult a
forall a. EvalErrorEx -> SBVResult a
SBVError EvalErrorEx
err
                SBVResult SVal
pz a
z ->
                  SBVResult a -> Eval (SBVResult a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SBVResult a -> Eval (SBVResult a))
-> SBVResult a -> Eval (SBVResult a)
forall a b. (a -> b) -> a -> b
$ SVal -> a -> SBVResult a
forall a. SVal -> a -> SBVResult a
SBVResult (SVal -> SVal -> SVal
svAnd (SVal -> SVal -> SVal -> SVal
svIte SVal
SBit SBV
c SVal
px SVal
py) SVal
pz) a
z

  wordLen :: SBV -> SWord SBV -> Integer
wordLen SBV
_ SWord SBV
v = Int -> Integer
forall a. Integral a => a -> Integer
toInteger (SVal -> Int
forall a. HasKind a => a -> Int
intSizeOf SVal
SWord SBV
v)
  wordAsChar :: SBV -> SWord SBV -> Maybe Char
wordAsChar SBV
_ SWord SBV
v = Integer -> Char
integerToChar (Integer -> Char) -> Maybe Integer -> Maybe Char
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SVal -> Maybe Integer
svAsInteger SVal
SWord SBV
v

  iteBit :: SBV -> SBit SBV -> SBit SBV -> SBit SBV -> SEval SBV (SBit SBV)
iteBit SBV
_ SBit SBV
b SBit SBV
x SBit SBV
y = SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
forall a b. (a -> b) -> a -> b
$! Kind -> Bool -> SVal -> SVal -> SVal -> SVal
svSymbolicMerge Kind
KBool Bool
True SVal
SBit SBV
b SVal
SBit SBV
x SVal
SBit SBV
y
  iteWord :: SBV -> SBit SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV)
iteWord SBV
_ SBit SBV
b SWord SBV
x SWord SBV
y = SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
forall a b. (a -> b) -> a -> b
$! Kind -> Bool -> SVal -> SVal -> SVal -> SVal
svSymbolicMerge (SVal -> Kind
forall a. HasKind a => a -> Kind
kindOf SVal
SWord SBV
x) Bool
True SVal
SBit SBV
b SVal
SWord SBV
x SVal
SWord SBV
y
  iteInteger :: SBV
-> SBit SBV
-> SInteger SBV
-> SInteger SBV
-> SEval SBV (SInteger SBV)
iteInteger SBV
_ SBit SBV
b SInteger SBV
x SInteger SBV
y = SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
forall a b. (a -> b) -> a -> b
$! Kind -> Bool -> SVal -> SVal -> SVal -> SVal
svSymbolicMerge Kind
KUnbounded Bool
True SVal
SBit SBV
b SVal
SInteger SBV
x SVal
SInteger SBV
y

  bitAsLit :: SBV -> SBit SBV -> Maybe Bool
bitAsLit SBV
_ SBit SBV
b = SVal -> Maybe Bool
svAsBool SVal
SBit SBV
b
  wordAsLit :: SBV -> SWord SBV -> Maybe (Integer, Integer)
wordAsLit SBV
_ SWord SBV
w =
    case SVal -> Maybe Integer
svAsInteger SVal
SWord SBV
w of
      Just Integer
x -> (Integer, Integer) -> Maybe (Integer, Integer)
forall a. a -> Maybe a
Just (Int -> Integer
forall a. Integral a => a -> Integer
toInteger (SVal -> Int
forall a. HasKind a => a -> Int
intSizeOf SVal
SWord SBV
w), Integer
x)
      Maybe Integer
Nothing -> Maybe (Integer, Integer)
forall a. Maybe a
Nothing
  integerAsLit :: SBV -> SInteger SBV -> Maybe Integer
integerAsLit SBV
_ SInteger SBV
v = SVal -> Maybe Integer
svAsInteger SVal
SInteger SBV
v

  bitLit :: SBV -> Bool -> SBit SBV
bitLit SBV
_ Bool
b     = Bool -> SVal
svBool Bool
b
  wordLit :: SBV -> Integer -> Integer -> SEval SBV (SWord SBV)
wordLit SBV
_ Integer
n Integer
x  = SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
forall a b. (a -> b) -> a -> b
$! Int -> Integer -> SWord SBV
literalSWord (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
n) Integer
x
  integerLit :: SBV -> Integer -> SEval SBV (SInteger SBV)
integerLit SBV
_ Integer
x = SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
forall a b. (a -> b) -> a -> b
$! Kind -> Integer -> SVal
svInteger Kind
KUnbounded Integer
x

  bitEq :: SBV -> SBit SBV -> SBit SBV -> SEval SBV (SBit SBV)
bitEq  SBV
_ SBit SBV
x SBit SBV
y = SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
forall a b. (a -> b) -> a -> b
$! SVal -> SVal -> SVal
svEqual SVal
SBit SBV
x SVal
SBit SBV
y
  bitOr :: SBV -> SBit SBV -> SBit SBV -> SEval SBV (SBit SBV)
bitOr  SBV
_ SBit SBV
x SBit SBV
y = SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
forall a b. (a -> b) -> a -> b
$! SVal -> SVal -> SVal
svOr SVal
SBit SBV
x SVal
SBit SBV
y
  bitAnd :: SBV -> SBit SBV -> SBit SBV -> SEval SBV (SBit SBV)
bitAnd SBV
_ SBit SBV
x SBit SBV
y = SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
forall a b. (a -> b) -> a -> b
$! SVal -> SVal -> SVal
svAnd SVal
SBit SBV
x SVal
SBit SBV
y
  bitXor :: SBV -> SBit SBV -> SBit SBV -> SEval SBV (SBit SBV)
bitXor SBV
_ SBit SBV
x SBit SBV
y = SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
forall a b. (a -> b) -> a -> b
$! SVal -> SVal -> SVal
svXOr SVal
SBit SBV
x SVal
SBit SBV
y
  bitComplement :: SBV -> SBit SBV -> SEval SBV (SBit SBV)
bitComplement SBV
_ SBit SBV
x = SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
forall a b. (a -> b) -> a -> b
$! SVal -> SVal
svNot SVal
SBit SBV
x

  wordBit :: SBV -> SWord SBV -> Integer -> SEval SBV (SBit SBV)
wordBit SBV
_ SWord SBV
x Integer
idx = SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
forall a b. (a -> b) -> a -> b
$! SVal -> Int -> SVal
svTestBit SVal
SWord SBV
x (SVal -> Int
forall a. HasKind a => a -> Int
intSizeOf SVal
SWord SBV
x Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
idx)

  wordUpdate :: SBV -> SWord SBV -> Integer -> SBit SBV -> SEval SBV (SWord SBV)
wordUpdate SBV
_ SWord SBV
x Integer
idx SBit SBV
b = SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
forall a b. (a -> b) -> a -> b
$! Kind -> Bool -> SVal -> SVal -> SVal -> SVal
svSymbolicMerge (SVal -> Kind
forall a. HasKind a => a -> Kind
kindOf SVal
SWord SBV
x) Bool
False SVal
SBit SBV
b SVal
wtrue SVal
wfalse
    where
     i' :: Int
i' = SVal -> Int
forall a. HasKind a => a -> Int
intSizeOf SVal
SWord SBV
x Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
idx
     wtrue :: SVal
wtrue  = SVal
SWord SBV
x SVal -> SVal -> SVal
`svOr`  Kind -> Integer -> SVal
svInteger (SVal -> Kind
forall a. HasKind a => a -> Kind
kindOf SVal
SWord SBV
x) (Int -> Integer
forall a. Bits a => Int -> a
bit Int
i' :: Integer)
     wfalse :: SVal
wfalse = SVal
SWord SBV
x SVal -> SVal -> SVal
`svAnd` Kind -> Integer -> SVal
svInteger (SVal -> Kind
forall a. HasKind a => a -> Kind
kindOf SVal
SWord SBV
x) (Integer -> Integer
forall a. Bits a => a -> a
complement (Int -> Integer
forall a. Bits a => Int -> a
bit Int
i' :: Integer))

  packWord :: SBV -> [SBit SBV] -> SEval SBV (SWord SBV)
packWord SBV
_ [SBit SBV]
bs  = SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
forall a b. (a -> b) -> a -> b
$! [SBit SBV] -> SWord SBV
packSBV [SBit SBV]
bs
  unpackWord :: SBV -> SWord SBV -> SEval SBV [SBit SBV]
unpackWord SBV
_ SWord SBV
x = [SVal] -> SBVEval [SVal]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([SVal] -> SBVEval [SVal]) -> [SVal] -> SBVEval [SVal]
forall a b. (a -> b) -> a -> b
$! SWord SBV -> [SBit SBV]
unpackSBV SWord SBV
x

  wordEq :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SBit SBV)
wordEq SBV
_ SWord SBV
x SWord SBV
y = SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
forall a b. (a -> b) -> a -> b
$! SVal -> SVal -> SVal
svEqual SVal
SWord SBV
x SVal
SWord SBV
y
  wordLessThan :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SBit SBV)
wordLessThan SBV
_ SWord SBV
x SWord SBV
y = SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
forall a b. (a -> b) -> a -> b
$! SVal -> SVal -> SVal
svLessThan SVal
SWord SBV
x SVal
SWord SBV
y
  wordGreaterThan :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SBit SBV)
wordGreaterThan SBV
_ SWord SBV
x SWord SBV
y = SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
forall a b. (a -> b) -> a -> b
$! SVal -> SVal -> SVal
svGreaterThan SVal
SWord SBV
x SVal
SWord SBV
y

  wordSignedLessThan :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SBit SBV)
wordSignedLessThan SBV
_ SWord SBV
x SWord SBV
y = SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
forall a b. (a -> b) -> a -> b
$! SVal -> SVal -> SVal
svLessThan SVal
sx SVal
sy
    where sx :: SVal
sx = SVal -> SVal
svSign SVal
SWord SBV
x
          sy :: SVal
sy = SVal -> SVal
svSign SVal
SWord SBV
y

  joinWord :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV)
joinWord SBV
_ SWord SBV
x SWord SBV
y = SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
forall a b. (a -> b) -> a -> b
$! SVal -> SVal -> SVal
svJoin SVal
SWord SBV
x SVal
SWord SBV
y

  splitWord :: SBV
-> Integer
-> Integer
-> SWord SBV
-> SEval SBV (SWord SBV, SWord SBV)
splitWord SBV
_ Integer
_leftW Integer
rightW SWord SBV
w = (SVal, SVal) -> SBVEval (SVal, SVal)
forall (f :: * -> *) a. Applicative f => a -> f a
pure
    ( Int -> Int -> SVal -> SVal
svExtract (SVal -> Int
forall a. HasKind a => a -> Int
intSizeOf SVal
SWord SBV
w Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
rightW) SVal
SWord SBV
w
    , Int -> Int -> SVal -> SVal
svExtract (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
rightW Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Int
0 SVal
SWord SBV
w
    )

  extractWord :: SBV -> Integer -> Integer -> SWord SBV -> SEval SBV (SWord SBV)
extractWord SBV
_ Integer
len Integer
start SWord SBV
w =
    SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
forall a b. (a -> b) -> a -> b
$! Int -> Int -> SVal -> SVal
svExtract (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
start Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
len Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
start) SVal
SWord SBV
w

  wordAnd :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV)
wordAnd SBV
_ SWord SBV
a SWord SBV
b = SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
forall a b. (a -> b) -> a -> b
$! SVal -> SVal -> SVal
svAnd SVal
SWord SBV
a SVal
SWord SBV
b
  wordOr :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV)
wordOr  SBV
_ SWord SBV
a SWord SBV
b = SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
forall a b. (a -> b) -> a -> b
$! SVal -> SVal -> SVal
svOr SVal
SWord SBV
a SVal
SWord SBV
b
  wordXor :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV)
wordXor SBV
_ SWord SBV
a SWord SBV
b = SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
forall a b. (a -> b) -> a -> b
$! SVal -> SVal -> SVal
svXOr SVal
SWord SBV
a SVal
SWord SBV
b
  wordComplement :: SBV -> SWord SBV -> SEval SBV (SWord SBV)
wordComplement SBV
_ SWord SBV
a = SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
forall a b. (a -> b) -> a -> b
$! SVal -> SVal
svNot SVal
SWord SBV
a

  wordPlus :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV)
wordPlus  SBV
_ SWord SBV
a SWord SBV
b = SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
forall a b. (a -> b) -> a -> b
$! SVal -> SVal -> SVal
svPlus SVal
SWord SBV
a SVal
SWord SBV
b
  wordMinus :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV)
wordMinus SBV
_ SWord SBV
a SWord SBV
b = SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
forall a b. (a -> b) -> a -> b
$! SVal -> SVal -> SVal
svMinus SVal
SWord SBV
a SVal
SWord SBV
b
  wordMult :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV)
wordMult  SBV
_ SWord SBV
a SWord SBV
b = SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
forall a b. (a -> b) -> a -> b
$! SVal -> SVal -> SVal
svTimes SVal
SWord SBV
a SVal
SWord SBV
b
  wordNegate :: SBV -> SWord SBV -> SEval SBV (SWord SBV)
wordNegate SBV
_ SWord SBV
a  = SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
forall a b. (a -> b) -> a -> b
$! SVal -> SVal
svUNeg SVal
SWord SBV
a

  wordDiv :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV)
wordDiv SBV
sym SWord SBV
a SWord SBV
b =
    do let z :: SWord SBV
z = Int -> Integer -> SWord SBV
literalSWord (SVal -> Int
forall a. HasKind a => a -> Int
intSizeOf SVal
SWord SBV
b) Integer
0
       SBV -> SBit SBV -> EvalError -> SEval SBV ()
forall sym.
Backend sym =>
sym -> SBit sym -> EvalError -> SEval sym ()
assertSideCondition SBV
sym (SVal -> SVal
svNot (SVal -> SVal -> SVal
svEqual SVal
SWord SBV
b SVal
SWord SBV
z)) EvalError
DivideByZero
       SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
forall a b. (a -> b) -> a -> b
$! SVal -> SVal -> SVal
svQuot SVal
SWord SBV
a SVal
SWord SBV
b

  wordMod :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV)
wordMod SBV
sym SWord SBV
a SWord SBV
b =
    do let z :: SWord SBV
z = Int -> Integer -> SWord SBV
literalSWord (SVal -> Int
forall a. HasKind a => a -> Int
intSizeOf SVal
SWord SBV
b) Integer
0
       SBV -> SBit SBV -> EvalError -> SEval SBV ()
forall sym.
Backend sym =>
sym -> SBit sym -> EvalError -> SEval sym ()
assertSideCondition SBV
sym (SVal -> SVal
svNot (SVal -> SVal -> SVal
svEqual SVal
SWord SBV
b SVal
SWord SBV
z)) EvalError
DivideByZero
       SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
forall a b. (a -> b) -> a -> b
$! SVal -> SVal -> SVal
svRem SVal
SWord SBV
a SVal
SWord SBV
b

  wordSignedDiv :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV)
wordSignedDiv SBV
sym SWord SBV
a SWord SBV
b =
    do let z :: SWord SBV
z = Int -> Integer -> SWord SBV
literalSWord (SVal -> Int
forall a. HasKind a => a -> Int
intSizeOf SVal
SWord SBV
b) Integer
0
       SBV -> SBit SBV -> EvalError -> SEval SBV ()
forall sym.
Backend sym =>
sym -> SBit sym -> EvalError -> SEval sym ()
assertSideCondition SBV
sym (SVal -> SVal
svNot (SVal -> SVal -> SVal
svEqual SVal
SWord SBV
b SVal
SWord SBV
z)) EvalError
DivideByZero
       SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
forall a b. (a -> b) -> a -> b
$! SWord SBV -> SWord SBV -> SWord SBV
signedQuot SWord SBV
a SWord SBV
b

  wordSignedMod :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV)
wordSignedMod SBV
sym SWord SBV
a SWord SBV
b =
    do let z :: SWord SBV
z = Int -> Integer -> SWord SBV
literalSWord (SVal -> Int
forall a. HasKind a => a -> Int
intSizeOf SVal
SWord SBV
b) Integer
0
       SBV -> SBit SBV -> EvalError -> SEval SBV ()
forall sym.
Backend sym =>
sym -> SBit sym -> EvalError -> SEval sym ()
assertSideCondition SBV
sym (SVal -> SVal
svNot (SVal -> SVal -> SVal
svEqual SVal
SWord SBV
b SVal
SWord SBV
z)) EvalError
DivideByZero
       SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
forall a b. (a -> b) -> a -> b
$! SWord SBV -> SWord SBV -> SWord SBV
signedRem SWord SBV
a SWord SBV
b

  wordLg2 :: SBV -> SWord SBV -> SEval SBV (SWord SBV)
wordLg2 SBV
_ SWord SBV
a = SWord SBV -> SEval SBV (SWord SBV)
sLg2 SWord SBV
a

  wordToInt :: SBV -> SWord SBV -> SEval SBV (SInteger SBV)
wordToInt SBV
_ SWord SBV
x = SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
forall a b. (a -> b) -> a -> b
$! SWord SBV -> SInteger SBV
svToInteger SWord SBV
x
  wordFromInt :: SBV -> Integer -> SInteger SBV -> SEval SBV (SWord SBV)
wordFromInt SBV
_ Integer
w SInteger SBV
i = SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
forall a b. (a -> b) -> a -> b
$! Integer -> SInteger SBV -> SWord SBV
svFromInteger Integer
w SInteger SBV
i

  intEq :: SBV -> SInteger SBV -> SInteger SBV -> SEval SBV (SBit SBV)
intEq SBV
_ SInteger SBV
a SInteger SBV
b = SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
forall a b. (a -> b) -> a -> b
$! SVal -> SVal -> SVal
svEqual SVal
SInteger SBV
a SVal
SInteger SBV
b
  intLessThan :: SBV -> SInteger SBV -> SInteger SBV -> SEval SBV (SBit SBV)
intLessThan SBV
_ SInteger SBV
a SInteger SBV
b = SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
forall a b. (a -> b) -> a -> b
$! SVal -> SVal -> SVal
svLessThan SVal
SInteger SBV
a SVal
SInteger SBV
b
  intGreaterThan :: SBV -> SInteger SBV -> SInteger SBV -> SEval SBV (SBit SBV)
intGreaterThan SBV
_ SInteger SBV
a SInteger SBV
b = SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
forall a b. (a -> b) -> a -> b
$! SVal -> SVal -> SVal
svGreaterThan SVal
SInteger SBV
a SVal
SInteger SBV
b

  intPlus :: SBV -> SInteger SBV -> SInteger SBV -> SEval SBV (SInteger SBV)
intPlus  SBV
_ SInteger SBV
a SInteger SBV
b = SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
forall a b. (a -> b) -> a -> b
$! SVal -> SVal -> SVal
svPlus SVal
SInteger SBV
a SVal
SInteger SBV
b
  intMinus :: SBV -> SInteger SBV -> SInteger SBV -> SEval SBV (SInteger SBV)
intMinus SBV
_ SInteger SBV
a SInteger SBV
b = SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
forall a b. (a -> b) -> a -> b
$! SVal -> SVal -> SVal
svMinus SVal
SInteger SBV
a SVal
SInteger SBV
b
  intMult :: SBV -> SInteger SBV -> SInteger SBV -> SEval SBV (SInteger SBV)
intMult  SBV
_ SInteger SBV
a SInteger SBV
b = SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
forall a b. (a -> b) -> a -> b
$! SVal -> SVal -> SVal
svTimes SVal
SInteger SBV
a SVal
SInteger SBV
b
  intNegate :: SBV -> SInteger SBV -> SEval SBV (SInteger SBV)
intNegate SBV
_ SInteger SBV
a  = SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
forall a b. (a -> b) -> a -> b
$! SVal -> SVal
SBV.svUNeg SVal
SInteger SBV
a

  intDiv :: SBV -> SInteger SBV -> SInteger SBV -> SEval SBV (SInteger SBV)
intDiv SBV
sym SInteger SBV
a SInteger SBV
b =
    do let z :: SVal
z = Kind -> Integer -> SVal
svInteger Kind
KUnbounded Integer
0
       SBV -> SBit SBV -> EvalError -> SEval SBV ()
forall sym.
Backend sym =>
sym -> SBit sym -> EvalError -> SEval sym ()
assertSideCondition SBV
sym (SVal -> SVal
svNot (SVal -> SVal -> SVal
svEqual SVal
SInteger SBV
b SVal
z)) EvalError
DivideByZero
       let p :: SVal
p = SVal -> SVal -> SVal
svLessThan SVal
z SVal
SInteger SBV
b
       SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
forall a b. (a -> b) -> a -> b
$! Kind -> Bool -> SVal -> SVal -> SVal -> SVal
svSymbolicMerge Kind
KUnbounded Bool
True SVal
p (SVal -> SVal -> SVal
svQuot SVal
SInteger SBV
a SVal
SInteger SBV
b) (SVal -> SVal -> SVal
svQuot (SVal -> SVal
svUNeg SVal
SInteger SBV
a) (SVal -> SVal
svUNeg SVal
SInteger SBV
b))
  intMod :: SBV -> SInteger SBV -> SInteger SBV -> SEval SBV (SInteger SBV)
intMod SBV
sym SInteger SBV
a SInteger SBV
b =
    do let z :: SVal
z = Kind -> Integer -> SVal
svInteger Kind
KUnbounded Integer
0
       SBV -> SBit SBV -> EvalError -> SEval SBV ()
forall sym.
Backend sym =>
sym -> SBit sym -> EvalError -> SEval sym ()
assertSideCondition SBV
sym (SVal -> SVal
svNot (SVal -> SVal -> SVal
svEqual SVal
SInteger SBV
b SVal
z)) EvalError
DivideByZero
       let p :: SVal
p = SVal -> SVal -> SVal
svLessThan SVal
z SVal
SInteger SBV
b
       SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
forall a b. (a -> b) -> a -> b
$! Kind -> Bool -> SVal -> SVal -> SVal -> SVal
svSymbolicMerge Kind
KUnbounded Bool
True SVal
p (SVal -> SVal -> SVal
svRem SVal
SInteger SBV
a SVal
SInteger SBV
b) (SVal -> SVal
svUNeg (SVal -> SVal -> SVal
svRem (SVal -> SVal
svUNeg SVal
SInteger SBV
a) (SVal -> SVal
svUNeg SVal
SInteger SBV
b)))

  -- NB, we don't do reduction here
  intToZn :: SBV -> Integer -> SInteger SBV -> SEval SBV (SInteger SBV)
intToZn SBV
_ Integer
_m SInteger SBV
a = SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure SVal
SInteger SBV
a

  znToInt :: SBV -> Integer -> SInteger SBV -> SEval SBV (SInteger SBV)
znToInt SBV
_ Integer
0 SInteger SBV
_ = String -> [String] -> SBVEval SVal
forall a. String -> [String] -> a
evalPanic String
"znToInt" [String
"0 modulus not allowed"]
  znToInt SBV
_ Integer
m SInteger SBV
a =
    do let m' :: SVal
m' = Kind -> Integer -> SVal
svInteger Kind
KUnbounded Integer
m
       SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
forall a b. (a -> b) -> a -> b
$! SVal -> SVal -> SVal
svRem SVal
SInteger SBV
a SVal
m'

  znEq :: SBV
-> Integer -> SInteger SBV -> SInteger SBV -> SEval SBV (SBit SBV)
znEq SBV
_ Integer
0 SInteger SBV
_ SInteger SBV
_ = String -> [String] -> SBVEval SVal
forall a. String -> [String] -> a
evalPanic String
"znEq" [String
"0 modulus not allowed"]
  znEq SBV
sym Integer
m SInteger SBV
a SInteger SBV
b = SBV -> Integer -> SInteger SBV -> SEval SBV (SBit SBV)
svDivisible SBV
sym Integer
m (SVal -> SVal -> SVal
SBV.svMinus SVal
SInteger SBV
a SVal
SInteger SBV
b)

  znPlus :: SBV
-> Integer
-> SInteger SBV
-> SInteger SBV
-> SEval SBV (SInteger SBV)
znPlus  SBV
sym Integer
m SInteger SBV
a SInteger SBV
b = SBV
-> Integer
-> SInteger SBV
-> SInteger SBV
-> SEval SBV (SInteger SBV)
sModAdd SBV
sym Integer
m SInteger SBV
a SInteger SBV
b
  znMinus :: SBV
-> Integer
-> SInteger SBV
-> SInteger SBV
-> SEval SBV (SInteger SBV)
znMinus SBV
sym Integer
m SInteger SBV
a SInteger SBV
b = SBV
-> Integer
-> SInteger SBV
-> SInteger SBV
-> SEval SBV (SInteger SBV)
sModSub SBV
sym Integer
m SInteger SBV
a SInteger SBV
b
  znMult :: SBV
-> Integer
-> SInteger SBV
-> SInteger SBV
-> SEval SBV (SInteger SBV)
znMult  SBV
sym Integer
m SInteger SBV
a SInteger SBV
b = SBV
-> Integer
-> SInteger SBV
-> SInteger SBV
-> SEval SBV (SInteger SBV)
sModMult SBV
sym Integer
m SInteger SBV
a SInteger SBV
b
  znNegate :: SBV -> Integer -> SInteger SBV -> SEval SBV (SInteger SBV)
znNegate SBV
sym Integer
m SInteger SBV
a  = SBV -> Integer -> SInteger SBV -> SEval SBV (SInteger SBV)
sModNegate SBV
sym Integer
m SInteger SBV
a
  znRecip :: SBV -> Integer -> SInteger SBV -> SEval SBV (SInteger SBV)
znRecip = SBV -> Integer -> SInteger SBV -> SEval SBV (SInteger SBV)
sModRecip

  fpAsLit :: SBV -> SFloat SBV -> Maybe BF
fpAsLit SBV
_ SFloat SBV
_               = Maybe BF
forall a. Maybe a
Nothing
  iteFloat :: SBV
-> SBit SBV -> SFloat SBV -> SFloat SBV -> SEval SBV (SFloat SBV)
iteFloat SBV
_ SBit SBV
_ SFloat SBV
_ SFloat SBV
_          = String -> SEval SBV ()
forall a. String -> SEval SBV a
unsupported String
"iteFloat"
  fpNaN :: SBV -> Integer -> Integer -> SEval SBV (SFloat SBV)
fpNaN SBV
_ Integer
_ Integer
_               = String -> SEval SBV ()
forall a. String -> SEval SBV a
unsupported String
"fpNaN"
  fpPosInf :: SBV -> Integer -> Integer -> SEval SBV (SFloat SBV)
fpPosInf SBV
_ Integer
_ Integer
_            = String -> SEval SBV ()
forall a. String -> SEval SBV a
unsupported String
"fpPosInf"
  fpExactLit :: SBV -> BF -> SEval SBV (SFloat SBV)
fpExactLit SBV
_ BF
_            = String -> SEval SBV ()
forall a. String -> SEval SBV a
unsupported String
"fpExactLit"
  fpLit :: SBV -> Integer -> Integer -> Rational -> SEval SBV (SFloat SBV)
fpLit SBV
_ Integer
_ Integer
_ Rational
_             = String -> SEval SBV ()
forall a. String -> SEval SBV a
unsupported String
"fpLit"
  fpLogicalEq :: SBV -> SFloat SBV -> SFloat SBV -> SEval SBV (SBit SBV)
fpLogicalEq SBV
_ SFloat SBV
_ SFloat SBV
_         = String -> SEval SBV SVal
forall a. String -> SEval SBV a
unsupported String
"fpLogicalEq"
  fpEq :: SBV -> SFloat SBV -> SFloat SBV -> SEval SBV (SBit SBV)
fpEq SBV
_ SFloat SBV
_ SFloat SBV
_                = String -> SEval SBV SVal
forall a. String -> SEval SBV a
unsupported String
"fpEq"
  fpLessThan :: SBV -> SFloat SBV -> SFloat SBV -> SEval SBV (SBit SBV)
fpLessThan SBV
_ SFloat SBV
_ SFloat SBV
_          = String -> SEval SBV SVal
forall a. String -> SEval SBV a
unsupported String
"fpLessThan"
  fpGreaterThan :: SBV -> SFloat SBV -> SFloat SBV -> SEval SBV (SBit SBV)
fpGreaterThan SBV
_ SFloat SBV
_ SFloat SBV
_       = String -> SEval SBV SVal
forall a. String -> SEval SBV a
unsupported String
"fpGreaterThan"
  fpPlus :: FPArith2 SBV
fpPlus SBV
_ SWord SBV
_ SFloat SBV
_ SFloat SBV
_            = String -> SEval SBV ()
forall a. String -> SEval SBV a
unsupported String
"fpPlus"
  fpMinus :: FPArith2 SBV
fpMinus SBV
_ SWord SBV
_ SFloat SBV
_ SFloat SBV
_           = String -> SEval SBV ()
forall a. String -> SEval SBV a
unsupported String
"fpMinus"
  fpMult :: FPArith2 SBV
fpMult SBV
_ SWord SBV
_ SFloat SBV
_ SFloat SBV
_            = String -> SEval SBV ()
forall a. String -> SEval SBV a
unsupported String
"fpMult"
  fpDiv :: FPArith2 SBV
fpDiv SBV
_ SWord SBV
_ SFloat SBV
_ SFloat SBV
_             = String -> SEval SBV ()
forall a. String -> SEval SBV a
unsupported String
"fpDiv"
  fpAbs :: SBV -> SFloat SBV -> SEval SBV (SFloat SBV)
fpAbs SBV
_ SFloat SBV
_                 = String -> SEval SBV ()
forall a. String -> SEval SBV a
unsupported String
"fpAbs"
  fpSqrt :: SBV -> SWord SBV -> SFloat SBV -> SEval SBV (SFloat SBV)
fpSqrt SBV
_ SWord SBV
_ SFloat SBV
_              = String -> SEval SBV ()
forall a. String -> SEval SBV a
unsupported String
"fpSqrt"
  fpFMA :: SBV
-> SWord SBV
-> SFloat SBV
-> SFloat SBV
-> SFloat SBV
-> SEval SBV (SFloat SBV)
fpFMA SBV
_ SWord SBV
_ SFloat SBV
_ SFloat SBV
_ SFloat SBV
_           = String -> SEval SBV ()
forall a. String -> SEval SBV a
unsupported String
"fpFMA"
  fpNeg :: SBV -> SFloat SBV -> SEval SBV (SFloat SBV)
fpNeg SBV
_ SFloat SBV
_                 = String -> SEval SBV ()
forall a. String -> SEval SBV a
unsupported String
"fpNeg"
  fpFromInteger :: SBV
-> Integer
-> Integer
-> SWord SBV
-> SInteger SBV
-> SEval SBV (SFloat SBV)
fpFromInteger SBV
_ Integer
_ Integer
_ SWord SBV
_ SInteger SBV
_   = String -> SEval SBV ()
forall a. String -> SEval SBV a
unsupported String
"fpFromInteger"
  fpToInteger :: SBV
-> String -> SWord SBV -> SFloat SBV -> SEval SBV (SInteger SBV)
fpToInteger SBV
_ String
_ SWord SBV
_ SFloat SBV
_       = String -> SEval SBV SVal
forall a. String -> SEval SBV a
unsupported String
"fpToInteger"
  fpIsZero :: SBV -> SFloat SBV -> SEval SBV (SBit SBV)
fpIsZero SBV
_ SFloat SBV
_              = String -> SEval SBV SVal
forall a. String -> SEval SBV a
unsupported String
"fpIsZero"
  fpIsInf :: SBV -> SFloat SBV -> SEval SBV (SBit SBV)
fpIsInf SBV
_ SFloat SBV
_               = String -> SEval SBV SVal
forall a. String -> SEval SBV a
unsupported String
"fpIsInf"
  fpIsNeg :: SBV -> SFloat SBV -> SEval SBV (SBit SBV)
fpIsNeg SBV
_ SFloat SBV
_               = String -> SEval SBV SVal
forall a. String -> SEval SBV a
unsupported String
"fpIsNeg"
  fpIsNaN :: SBV -> SFloat SBV -> SEval SBV (SBit SBV)
fpIsNaN SBV
_ SFloat SBV
_               = String -> SEval SBV SVal
forall a. String -> SEval SBV a
unsupported String
"fpIsNaN"
  fpIsNorm :: SBV -> SFloat SBV -> SEval SBV (SBit SBV)
fpIsNorm SBV
_ SFloat SBV
_              = String -> SEval SBV SVal
forall a. String -> SEval SBV a
unsupported String
"fpIsNorm"
  fpIsSubnorm :: SBV -> SFloat SBV -> SEval SBV (SBit SBV)
fpIsSubnorm SBV
_ SFloat SBV
_           = String -> SEval SBV SVal
forall a. String -> SEval SBV a
unsupported String
"fpIsSubnorm"
  fpToBits :: SBV -> SFloat SBV -> SEval SBV (SWord SBV)
fpToBits SBV
_ SFloat SBV
_              = String -> SEval SBV SVal
forall a. String -> SEval SBV a
unsupported String
"fpToBits"
  fpFromBits :: SBV -> Integer -> Integer -> SWord SBV -> SEval SBV (SFloat SBV)
fpFromBits SBV
_ Integer
_ Integer
_ SWord SBV
_        = String -> SEval SBV ()
forall a. String -> SEval SBV a
unsupported String
"fpFromBits"
  fpToRational :: SBV -> SFloat SBV -> SEval SBV (SRational SBV)
fpToRational SBV
_ SFloat SBV
_          = String -> SEval SBV (SRational SBV)
forall a. String -> SEval SBV a
unsupported String
"fpToRational"
  fpFromRational :: SBV
-> Integer
-> Integer
-> SWord SBV
-> SRational SBV
-> SEval SBV (SFloat SBV)
fpFromRational SBV
_ Integer
_ Integer
_ SWord SBV
_ SRational SBV
_  = String -> SEval SBV ()
forall a. String -> SEval SBV a
unsupported String
"fpFromRational"


unsupported :: String -> SEval SBV a
unsupported :: String -> SEval SBV a
unsupported String
x = IO a -> SBVEval a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (Unsupported -> IO a
forall a e. Exception e => e -> a
X.throw (String -> Unsupported
UnsupportedSymbolicOp String
x))


svToInteger :: SWord SBV -> SInteger SBV
svToInteger :: SWord SBV -> SInteger SBV
svToInteger SWord SBV
w =
  case SVal -> Maybe Integer
svAsInteger SVal
SWord SBV
w of
    Maybe Integer
Nothing -> Kind -> SVal -> SVal
svFromIntegral Kind
KUnbounded SVal
SWord SBV
w
    Just Integer
x  -> Kind -> Integer -> SVal
svInteger Kind
KUnbounded Integer
x

svFromInteger :: Integer -> SInteger SBV -> SWord SBV
svFromInteger :: Integer -> SInteger SBV -> SWord SBV
svFromInteger Integer
0 SInteger SBV
_ = Int -> Integer -> SWord SBV
literalSWord Int
0 Integer
0
svFromInteger Integer
n SInteger SBV
i =
  case SVal -> Maybe Integer
svAsInteger SVal
SInteger SBV
i of
    Maybe Integer
Nothing -> Kind -> SVal -> SVal
svFromIntegral (Bool -> Int -> Kind
KBounded Bool
False (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
n)) SVal
SInteger SBV
i
    Just Integer
x  -> Int -> Integer -> SWord SBV
literalSWord (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
n) Integer
x

-- Errors ----------------------------------------------------------------------

evalPanic :: String -> [String] -> a
evalPanic :: String -> [String] -> a
evalPanic String
cxt = String -> [String] -> a
forall a. HasCallStack => String -> [String] -> a
panic (String
"[SBV] " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
cxt)


sModAdd :: SBV -> Integer -> SInteger SBV -> SInteger SBV -> SEval SBV (SInteger SBV)
sModAdd :: SBV
-> Integer
-> SInteger SBV
-> SInteger SBV
-> SEval SBV (SInteger SBV)
sModAdd SBV
_ Integer
0 SInteger SBV
_ SInteger SBV
_ = String -> [String] -> SBVEval SVal
forall a. String -> [String] -> a
evalPanic String
"sModAdd" [String
"0 modulus not allowed"]
sModAdd SBV
sym Integer
modulus SInteger SBV
x SInteger SBV
y =
  case (SVal -> Maybe Integer
SBV.svAsInteger SVal
SInteger SBV
x, SVal -> Maybe Integer
SBV.svAsInteger SVal
SInteger SBV
y) of
    (Just Integer
i, Just Integer
j) -> SBV -> Integer -> SEval SBV (SInteger SBV)
forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit SBV
sym ((Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
j) Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
modulus)
    (Maybe Integer, Maybe Integer)
_                -> SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
forall a b. (a -> b) -> a -> b
$ SVal -> SVal -> SVal
SBV.svPlus SVal
SInteger SBV
x SVal
SInteger SBV
y

sModSub :: SBV -> Integer -> SInteger SBV -> SInteger SBV -> SEval SBV (SInteger SBV)
sModSub :: SBV
-> Integer
-> SInteger SBV
-> SInteger SBV
-> SEval SBV (SInteger SBV)
sModSub SBV
_ Integer
0 SInteger SBV
_ SInteger SBV
_ = String -> [String] -> SBVEval SVal
forall a. String -> [String] -> a
evalPanic String
"sModSub" [String
"0 modulus not allowed"]
sModSub SBV
sym Integer
modulus SInteger SBV
x SInteger SBV
y =
  case (SVal -> Maybe Integer
SBV.svAsInteger SVal
SInteger SBV
x, SVal -> Maybe Integer
SBV.svAsInteger SVal
SInteger SBV
y) of
    (Just Integer
i, Just Integer
j) -> SBV -> Integer -> SEval SBV (SInteger SBV)
forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit SBV
sym ((Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
j) Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
modulus)
    (Maybe Integer, Maybe Integer)
_                -> SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
forall a b. (a -> b) -> a -> b
$ SVal -> SVal -> SVal
SBV.svMinus SVal
SInteger SBV
x SVal
SInteger SBV
y

sModNegate :: SBV -> Integer -> SInteger SBV -> SEval SBV (SInteger SBV)
sModNegate :: SBV -> Integer -> SInteger SBV -> SEval SBV (SInteger SBV)
sModNegate SBV
_ Integer
0 SInteger SBV
_ = String -> [String] -> SBVEval SVal
forall a. String -> [String] -> a
evalPanic String
"sModNegate" [String
"0 modulus not allowed"]
sModNegate SBV
sym Integer
modulus SInteger SBV
x =
  case SVal -> Maybe Integer
SBV.svAsInteger SVal
SInteger SBV
x of
    Just Integer
i -> SBV -> Integer -> SEval SBV (SInteger SBV)
forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit SBV
sym ((Integer -> Integer
forall a. Num a => a -> a
negate Integer
i) Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
modulus)
    Maybe Integer
_      -> SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
forall a b. (a -> b) -> a -> b
$ SVal -> SVal
SBV.svUNeg SVal
SInteger SBV
x

sModMult :: SBV -> Integer -> SInteger SBV -> SInteger SBV -> SEval SBV (SInteger SBV)
sModMult :: SBV
-> Integer
-> SInteger SBV
-> SInteger SBV
-> SEval SBV (SInteger SBV)
sModMult SBV
_ Integer
0 SInteger SBV
_ SInteger SBV
_ = String -> [String] -> SBVEval SVal
forall a. String -> [String] -> a
evalPanic String
"sModMult" [String
"0 modulus not allowed"]
sModMult SBV
sym Integer
modulus SInteger SBV
x SInteger SBV
y =
  case (SVal -> Maybe Integer
SBV.svAsInteger SVal
SInteger SBV
x, SVal -> Maybe Integer
SBV.svAsInteger SVal
SInteger SBV
y) of
    (Just Integer
i, Just Integer
j) -> SBV -> Integer -> SEval SBV (SInteger SBV)
forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit SBV
sym ((Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
j) Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
modulus)
    (Maybe Integer, Maybe Integer)
_                -> SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
forall a b. (a -> b) -> a -> b
$ SVal -> SVal -> SVal
SBV.svTimes SVal
SInteger SBV
x SVal
SInteger SBV
y

-- Create a fresh constant and assert that it is the
-- multiplicitive inverse of x; return the constant.
-- Such an inverse must exist under the precondition
-- that the modulus is prime and the input is nonzero.
sModRecip ::
  SBV ->
  Integer {- ^ modulus: must be prime -} ->
  SInteger SBV ->
  SEval SBV (SInteger SBV)
sModRecip :: SBV -> Integer -> SInteger SBV -> SEval SBV (SInteger SBV)
sModRecip SBV
_sym Integer
0 SInteger SBV
_ = String -> [String] -> SBVEval SVal
forall a. HasCallStack => String -> [String] -> a
panic String
"sModRecip" [String
"0 modulus not allowed"]
sModRecip SBV
sym Integer
m SInteger SBV
x
  -- If the input is concrete, evaluate the answer
  | Just Integer
xi <- SVal -> Maybe Integer
svAsInteger SVal
SInteger SBV
x
  = let r :: Integer
r = Integer -> Integer -> Integer
Integer.recipModInteger Integer
xi Integer
m
     in if Integer
r Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 then SBV -> EvalError -> SEval SBV SVal
forall sym a. Backend sym => sym -> EvalError -> SEval sym a
raiseError SBV
sym EvalError
DivideByZero else SBV -> Integer -> SEval SBV (SInteger SBV)
forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit SBV
sym Integer
r

  -- If the input is symbolic, create a new symbolic constant
  -- and assert that it is the desired multiplicitive inverse.
  -- Such an inverse will exist under the precondition that
  -- the modulus is prime, and as long as the input is nonzero.
  | Bool
otherwise
  = do SVal
divZero <- SBV -> Integer -> SInteger SBV -> SEval SBV (SBit SBV)
svDivisible SBV
sym Integer
m SInteger SBV
x
       SBV -> SBit SBV -> EvalError -> SEval SBV ()
forall sym.
Backend sym =>
sym -> SBit sym -> EvalError -> SEval sym ()
assertSideCondition SBV
sym (SVal -> SVal
svNot SVal
divZero) EvalError
DivideByZero

       SVal
z <- IO SVal -> SBVEval SVal
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (SBV -> IO (SInteger SBV)
freshSInteger_ SBV
sym)
       let xz :: SVal
xz = SVal -> SVal -> SVal
svTimes SVal
SInteger SBV
x SVal
z
       SVal
rel <- SBV
-> Integer -> SInteger SBV -> SInteger SBV -> SEval SBV (SBit SBV)
forall sym.
Backend sym =>
sym
-> Integer -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
znEq SBV
sym Integer
m SVal
SInteger SBV
xz (Kind -> Integer -> SVal
svInteger Kind
KUnbounded Integer
1)
       let range :: SVal
range = SVal -> SVal -> SVal
svAnd (SVal -> SVal -> SVal
svLessThan (Kind -> Integer -> SVal
svInteger Kind
KUnbounded Integer
0) SVal
z)
                         (SVal -> SVal -> SVal
svLessThan SVal
z (Kind -> Integer -> SVal
svInteger Kind
KUnbounded Integer
m))
       IO () -> SBVEval ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (SBV -> SVal -> IO ()
addDefEqn SBV
sym (SVal -> SVal -> SVal
svAnd SVal
range (SVal -> SVal -> SVal
svOr SVal
divZero SVal
rel)))

       SVal -> SBVEval SVal
forall (m :: * -> *) a. Monad m => a -> m a
return SVal
z

-- | Ceiling (log_2 x)
sLg2 :: SWord SBV -> SEval SBV (SWord SBV)
sLg2 :: SWord SBV -> SEval SBV (SWord SBV)
sLg2 SWord SBV
x = SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
forall a b. (a -> b) -> a -> b
$ Int -> SVal
go Int
0
  where
    lit :: Integer -> SWord SBV
lit Integer
n = Int -> Integer -> SWord SBV
literalSWord (SVal -> Int
forall a. HasKind a => a -> Int
SBV.intSizeOf SVal
SWord SBV
x) Integer
n
    go :: Int -> SVal
go Int
i | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< SVal -> Int
forall a. HasKind a => a -> Int
SBV.intSizeOf SVal
SWord SBV
x = SVal -> SVal -> SVal -> SVal
SBV.svIte (SVal -> SVal -> SVal
SBV.svLessEq SVal
SWord SBV
x (Integer -> SWord SBV
lit (Integer
2Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^Int
i))) (Integer -> SWord SBV
lit (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
i)) (Int -> SVal
go (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1))
         | Bool
otherwise           = Integer -> SWord SBV
lit (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
i)

svDivisible :: SBV -> Integer -> SInteger SBV -> SEval SBV (SBit SBV)
svDivisible :: SBV -> Integer -> SInteger SBV -> SEval SBV (SBit SBV)
svDivisible SBV
sym Integer
m SInteger SBV
x =
  do SVal
m' <- SBV -> Integer -> SEval SBV (SInteger SBV)
forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit SBV
sym Integer
m
     SVal
z  <- SBV -> Integer -> SEval SBV (SInteger SBV)
forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit SBV
sym Integer
0
     SVal -> SBVEval SVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal -> SBVEval SVal) -> SVal -> SBVEval SVal
forall a b. (a -> b) -> a -> b
$ SVal -> SVal -> SVal
SBV.svEqual (SVal -> SVal -> SVal
SBV.svRem SVal
SInteger SBV
x SVal
m') SVal
z

signedQuot :: SWord SBV -> SWord SBV -> SWord SBV
signedQuot :: SWord SBV -> SWord SBV -> SWord SBV
signedQuot SWord SBV
x SWord SBV
y = SVal -> SVal
SBV.svUnsign (SVal -> SVal -> SVal
SBV.svQuot (SVal -> SVal
SBV.svSign SVal
SWord SBV
x) (SVal -> SVal
SBV.svSign SVal
SWord SBV
y))

signedRem :: SWord SBV -> SWord SBV -> SWord SBV
signedRem :: SWord SBV -> SWord SBV -> SWord SBV
signedRem SWord SBV
x SWord SBV
y = SVal -> SVal
SBV.svUnsign (SVal -> SVal -> SVal
SBV.svRem (SVal -> SVal
SBV.svSign SVal
SWord SBV
x) (SVal -> SVal
SBV.svSign SVal
SWord SBV
y))

ashr :: SVal -> SVal -> SVal
ashr :: SVal -> SVal -> SVal
ashr SVal
x SVal
idx =
  case SVal -> Maybe Integer
SBV.svAsInteger SVal
idx of
    Just Integer
i  -> SVal -> SVal
SBV.svUnsign (SVal -> Int -> SVal
SBV.svShr (SVal -> SVal
SBV.svSign SVal
x) (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
i))
    Maybe Integer
Nothing -> SVal -> SVal
SBV.svUnsign (SVal -> SVal -> SVal
SBV.svShiftRight (SVal -> SVal
SBV.svSign SVal
x) SVal
idx)

lshr :: SVal -> SVal -> SVal
lshr :: SVal -> SVal -> SVal
lshr SVal
x SVal
idx =
  case SVal -> Maybe Integer
SBV.svAsInteger SVal
idx of
    Just Integer
i -> SVal -> Int -> SVal
SBV.svShr SVal
x (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
i)
    Maybe Integer
Nothing -> SVal -> SVal -> SVal
SBV.svShiftRight SVal
x SVal
idx

shl :: SVal -> SVal -> SVal
shl :: SVal -> SVal -> SVal
shl SVal
x SVal
idx =
  case SVal -> Maybe Integer
SBV.svAsInteger SVal
idx of
    Just Integer
i  -> SVal -> Int -> SVal
SBV.svShl SVal
x (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
i)
    Maybe Integer
Nothing -> SVal -> SVal -> SVal
SBV.svShiftLeft SVal
x SVal
idx