-- |
-- Module      :  Cryptol.Backend.What4
-- Copyright   :  (c) 2020 Galois, Inc.
-- License     :  BSD3
-- Maintainer  :  cryptol@galois.com

{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}
module Cryptol.Backend.What4 where


import qualified Control.Exception as X
import           Control.Concurrent.MVar
import           Control.Monad (foldM,ap,liftM)
import           Control.Monad.IO.Class
import           Data.Bits (bit)
import qualified Data.BitVector.Sized as BV
import           Data.List
import           Data.Map (Map)
import           Data.Set (Set)
import           Data.Text (Text)
import           Data.Parameterized.NatRepr
import           Data.Parameterized.Some

import qualified GHC.Num.Compat as Integer

import qualified What4.Interface as W4
import qualified What4.SWord as SW
import qualified What4.SFloat as FP

import Cryptol.Backend
import Cryptol.Backend.FloatHelpers
import Cryptol.Backend.Monad
   ( Eval(..), EvalError(..), EvalErrorEx(..)
   , Unsupported(..), delayFill, blackhole, evalSpark
   , modifyCallStack, getCallStack, maybeReady
   )
import Cryptol.Utils.Panic


data What4 sym =
  What4
  { forall sym. What4 sym -> sym
w4  :: sym
  , forall sym. What4 sym -> MVar (Pred sym)
w4defs :: MVar (W4.Pred sym)
  , forall sym. What4 sym -> MVar (What4FunCache sym)
w4funs :: MVar (What4FunCache sym)
  , forall sym. What4 sym -> MVar (Set Text)
w4uninterpWarns :: MVar (Set Text)
  }

type What4FunCache sym = Map Text (SomeSymFn sym)

data SomeSymFn sym =
  forall args ret. SomeSymFn (W4.SymFn sym args ret)

{- | This is the monad used for symbolic evaluation. It adds to
aspects to 'Eval'---'WConn' keeps track of the backend and collects
definitional predicates, and 'W4Eval` adds support for partially
defined values -}
newtype W4Eval sym a = W4Eval { forall sym a. W4Eval sym a -> W4Conn sym (W4Result sym a)
evalPartial :: W4Conn sym (W4Result sym a) }

{- | This layer has the symbolic back-end, and can keep track of definitional
predicates used when working with uninterpreted constants defined
via a property. -}
newtype W4Conn sym a = W4Conn { forall sym a. W4Conn sym a -> sym -> Eval a
evalConn :: sym -> Eval a }

-- | The symbolic value we computed.
data W4Result sym a
  = W4Error !EvalErrorEx
    -- ^ A malformed value

  | W4Result !(W4.Pred sym) !a
    -- ^ safety predicate and result: the result only makes sense when
    -- the predicate holds.
 deriving forall a b. a -> W4Result sym b -> W4Result sym a
forall a b. (a -> b) -> W4Result sym a -> W4Result sym b
forall sym a b. a -> W4Result sym b -> W4Result sym a
forall sym a b. (a -> b) -> W4Result sym a -> W4Result sym b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> W4Result sym b -> W4Result sym a
$c<$ :: forall sym a b. a -> W4Result sym b -> W4Result sym a
fmap :: forall a b. (a -> b) -> W4Result sym a -> W4Result sym b
$cfmap :: forall sym a b. (a -> b) -> W4Result sym a -> W4Result sym b
Functor

--------------------------------------------------------------------------------
-- Moving between the layers

w4Eval :: W4Eval sym a -> sym -> Eval (W4Result sym a)
w4Eval :: forall sym a. W4Eval sym a -> sym -> Eval (W4Result sym a)
w4Eval (W4Eval (W4Conn sym -> Eval (W4Result sym a)
m)) = sym -> Eval (W4Result sym a)
m

w4Thunk :: Eval (W4Result sym a) -> W4Eval sym a
w4Thunk :: forall sym a. Eval (W4Result sym a) -> W4Eval sym a
w4Thunk Eval (W4Result sym a)
m = forall sym a. W4Conn sym (W4Result sym a) -> W4Eval sym a
W4Eval (forall sym a. (sym -> Eval a) -> W4Conn sym a
W4Conn \sym
_ -> Eval (W4Result sym a)
m)

-- | A value with no context.
doEval :: W4.IsSymExprBuilder sym => Eval a -> W4Conn sym a
doEval :: forall sym a. IsSymExprBuilder sym => Eval a -> W4Conn sym a
doEval Eval a
m = forall sym a. (sym -> Eval a) -> W4Conn sym a
W4Conn \sym
_sym -> Eval a
m

-- | A total value.
total :: W4.IsSymExprBuilder sym => W4Conn sym a -> W4Eval sym a
total :: forall sym a. IsSymExprBuilder sym => W4Conn sym a -> W4Eval sym a
total W4Conn sym a
m = forall sym a. W4Conn sym (W4Result sym a) -> W4Eval sym a
W4Eval
  do sym
sym <- forall sym. W4Conn sym sym
getSym
     forall sym a. Pred sym -> a -> W4Result sym a
W4Result (forall sym. IsExprBuilder sym => sym -> Bool -> Pred sym
W4.backendPred sym
sym Bool
True) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> W4Conn sym a
m

--------------------------------------------------------------------------------
-- Operations in WConn

instance W4.IsSymExprBuilder sym => Functor (W4Conn sym) where
  fmap :: forall a b. (a -> b) -> W4Conn sym a -> W4Conn sym b
fmap = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM

instance W4.IsSymExprBuilder sym => Applicative (W4Conn sym) where
  pure :: forall a. a -> W4Conn sym a
pure   = forall sym a. IsSymExprBuilder sym => Eval a -> W4Conn sym a
doEval forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a. Applicative f => a -> f a
pure
  <*> :: forall a b. W4Conn sym (a -> b) -> W4Conn sym a -> W4Conn sym b
(<*>)  = forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance W4.IsSymExprBuilder sym => Monad (W4Conn sym) where
  W4Conn sym a
m1 >>= :: forall a b. W4Conn sym a -> (a -> W4Conn sym b) -> W4Conn sym b
>>= a -> W4Conn sym b
f = forall sym a. (sym -> Eval a) -> W4Conn sym a
W4Conn \sym
sym ->
    do a
res1 <- forall sym a. W4Conn sym a -> sym -> Eval a
evalConn W4Conn sym a
m1 sym
sym
       forall sym a. W4Conn sym a -> sym -> Eval a
evalConn (a -> W4Conn sym b
f a
res1) sym
sym

instance W4.IsSymExprBuilder sym => MonadIO (W4Conn sym) where
  liftIO :: forall a. IO a -> W4Conn sym a
liftIO = forall sym a. IsSymExprBuilder sym => Eval a -> W4Conn sym a
doEval forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO

-- | Access the symbolic back-end
getSym :: W4Conn sym sym
getSym :: forall sym. W4Conn sym sym
getSym = forall sym a. (sym -> Eval a) -> W4Conn sym a
W4Conn \sym
sym -> forall (f :: * -> *) a. Applicative f => a -> f a
pure sym
sym

-- | Record a definition.
--addDef :: W4.Pred sym -> W4Conn sym ()
--addDef p = W4Conn \_ -> pure W4Defs { w4Defs = p, w4Result = () }

-- | Compute conjunction.
w4And :: W4.IsSymExprBuilder sym =>
         W4.Pred sym -> W4.Pred sym -> W4Conn sym (W4.Pred sym)
w4And :: forall sym.
IsSymExprBuilder sym =>
Pred sym -> Pred sym -> W4Conn sym (Pred sym)
w4And Pred sym
p Pred sym
q =
  do sym
sym <- forall sym. W4Conn sym sym
getSym
     forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
W4.andPred sym
sym Pred sym
p Pred sym
q)

-- | Compute negation.
w4Not :: W4.IsSymExprBuilder sym => W4.Pred sym -> W4Conn sym (W4.Pred sym)
w4Not :: forall sym.
IsSymExprBuilder sym =>
Pred sym -> W4Conn sym (Pred sym)
w4Not Pred sym
p =
  do sym
sym <- forall sym. W4Conn sym sym
getSym
     forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
W4.notPred sym
sym Pred sym
p)

-- | Compute if-then-else.
w4ITE :: W4.IsSymExprBuilder sym =>
         W4.Pred sym -> W4.Pred sym -> W4.Pred sym -> W4Conn sym (W4.Pred sym)
w4ITE :: forall sym.
IsSymExprBuilder sym =>
Pred sym -> Pred sym -> Pred sym -> W4Conn sym (Pred sym)
w4ITE Pred sym
ifP Pred sym
ifThen Pred sym
ifElse =
  do sym
sym <- forall sym. W4Conn sym sym
getSym
     forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> Pred sym -> IO (Pred sym)
W4.itePred sym
sym Pred sym
ifP Pred sym
ifThen Pred sym
ifElse)



--------------------------------------------------------------------------------
-- Operations in W4Eval

instance W4.IsSymExprBuilder sym => Functor (W4Eval sym) where
  fmap :: forall a b. (a -> b) -> W4Eval sym a -> W4Eval sym b
fmap = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM

instance W4.IsSymExprBuilder sym => Applicative (W4Eval sym) where
  pure :: forall a. a -> W4Eval sym a
pure  = forall sym a. IsSymExprBuilder sym => W4Conn sym a -> W4Eval sym a
total forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a. Applicative f => a -> f a
pure
  <*> :: forall a b. W4Eval sym (a -> b) -> W4Eval sym a -> W4Eval sym b
(<*>) = forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance W4.IsSymExprBuilder sym => Monad (W4Eval sym) where
  W4Eval sym a
m1 >>= :: forall a b. W4Eval sym a -> (a -> W4Eval sym b) -> W4Eval sym b
>>= a -> W4Eval sym b
f = forall sym a. W4Conn sym (W4Result sym a) -> W4Eval sym a
W4Eval
    do W4Result sym a
res1 <- forall sym a. W4Eval sym a -> W4Conn sym (W4Result sym a)
evalPartial W4Eval sym a
m1
       case W4Result sym a
res1 of
         W4Error EvalErrorEx
err -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall sym a. EvalErrorEx -> W4Result sym a
W4Error EvalErrorEx
err)
         W4Result Pred sym
px a
x' ->
           do W4Result sym b
res2 <- forall sym a. W4Eval sym a -> W4Conn sym (W4Result sym a)
evalPartial (a -> W4Eval sym b
f a
x')
              case W4Result sym b
res2 of
                W4Result Pred sym
py b
y ->
                  do Pred sym
pz <- forall sym.
IsSymExprBuilder sym =>
Pred sym -> Pred sym -> W4Conn sym (Pred sym)
w4And Pred sym
px Pred sym
py
                     forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall sym a. Pred sym -> a -> W4Result sym a
W4Result Pred sym
pz b
y)
                W4Error EvalErrorEx
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure W4Result sym b
res2

instance W4.IsSymExprBuilder sym => MonadIO (W4Eval sym) where
  liftIO :: forall a. IO a -> W4Eval sym a
liftIO = forall sym a. IsSymExprBuilder sym => W4Conn sym a -> W4Eval sym a
total forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO


-- | Add a definitional equation.
-- This will always be asserted when we make queries to the solver.
addDefEqn :: W4.IsSymExprBuilder sym => What4 sym -> W4.Pred sym -> W4Eval sym ()
addDefEqn :: forall sym.
IsSymExprBuilder sym =>
What4 sym -> Pred sym -> W4Eval sym ()
addDefEqn What4 sym
sym Pred sym
p =
  forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall a. MVar a -> (a -> IO a) -> IO ()
modifyMVar_ (forall sym. What4 sym -> MVar (Pred sym)
w4defs What4 sym
sym) (forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
W4.andPred (forall sym. What4 sym -> sym
w4 What4 sym
sym) Pred sym
p))

-- | Add s safety condition.
addSafety :: W4.IsSymExprBuilder sym => W4.Pred sym -> W4Eval sym ()
addSafety :: forall sym. IsSymExprBuilder sym => Pred sym -> W4Eval sym ()
addSafety Pred sym
p = forall sym a. W4Conn sym (W4Result sym a) -> W4Eval sym a
W4Eval (forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall sym a. Pred sym -> a -> W4Result sym a
W4Result Pred sym
p ()))

-- | A fully undefined symbolic value
evalError :: W4.IsSymExprBuilder sym => EvalError -> W4Eval sym a
evalError :: forall sym a. IsSymExprBuilder sym => EvalError -> W4Eval sym a
evalError EvalError
err = forall sym a. W4Conn sym (W4Result sym a) -> W4Eval sym a
W4Eval forall a b. (a -> b) -> a -> b
$ forall sym a. (sym -> Eval a) -> W4Conn sym a
W4Conn forall a b. (a -> b) -> a -> b
$ \sym
_sym ->
  do CallStack
stk <- Eval CallStack
getCallStack
     forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall sym a. EvalErrorEx -> W4Result sym a
W4Error (CallStack -> EvalError -> EvalErrorEx
EvalErrorEx CallStack
stk EvalError
err))

--------------------------------------------------------------------------------


assertBVDivisor :: W4.IsSymExprBuilder sym => What4 sym -> SW.SWord sym -> W4Eval sym ()
assertBVDivisor :: forall sym.
IsSymExprBuilder sym =>
What4 sym -> SWord sym -> W4Eval sym ()
assertBVDivisor What4 sym
sym SWord sym
x =
  do SymExpr sym BaseBoolType
p <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym. IsExprBuilder sym => sym -> SWord sym -> IO (Pred sym)
SW.bvIsNonzero (forall sym. What4 sym -> sym
w4 What4 sym
sym) SWord sym
x)
     forall sym.
Backend sym =>
sym -> SBit sym -> EvalError -> SEval sym ()
assertSideCondition What4 sym
sym SymExpr sym BaseBoolType
p EvalError
DivideByZero

assertIntDivisor ::
  W4.IsSymExprBuilder sym => What4 sym -> W4.SymInteger sym -> W4Eval sym ()
assertIntDivisor :: forall sym.
IsSymExprBuilder sym =>
What4 sym -> SymInteger sym -> W4Eval sym ()
assertIntDivisor What4 sym
sym SymInteger sym
x =
  do SymExpr sym BaseBoolType
p <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
W4.notPred (forall sym. What4 sym -> sym
w4 What4 sym
sym) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
W4.intEq (forall sym. What4 sym -> sym
w4 What4 sym
sym) SymInteger sym
x forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
W4.intLit (forall sym. What4 sym -> sym
w4 What4 sym
sym) Integer
0)
     forall sym.
Backend sym =>
sym -> SBit sym -> EvalError -> SEval sym ()
assertSideCondition What4 sym
sym SymExpr sym BaseBoolType
p EvalError
DivideByZero

instance W4.IsSymExprBuilder sym => Backend (What4 sym) where
  type SBit (What4 sym)     = W4.Pred sym
  type SWord (What4 sym)    = SW.SWord sym
  type SInteger (What4 sym) = W4.SymInteger sym
  type SFloat (What4 sym)   = FP.SFloat sym
  type SEval (What4 sym)    = W4Eval sym

  raiseError :: forall a. What4 sym -> EvalError -> SEval (What4 sym) a
raiseError What4 sym
_ = forall sym a. IsSymExprBuilder sym => EvalError -> W4Eval sym a
evalError

  assertSideCondition :: What4 sym -> SBit (What4 sym) -> EvalError -> SEval (What4 sym) ()
assertSideCondition What4 sym
_ SBit (What4 sym)
cond EvalError
err
    | Just Bool
False <- forall (e :: BaseType -> *).
IsExpr e =>
e BaseBoolType -> Maybe Bool
W4.asConstantPred SBit (What4 sym)
cond = forall sym a. IsSymExprBuilder sym => EvalError -> W4Eval sym a
evalError EvalError
err
    | Bool
otherwise = forall sym. IsSymExprBuilder sym => Pred sym -> W4Eval sym ()
addSafety SBit (What4 sym)
cond

  isReady :: forall a.
What4 sym -> SEval (What4 sym) a -> SEval (What4 sym) (Maybe a)
isReady What4 sym
sym SEval (What4 sym) a
m = forall sym a. W4Conn sym (W4Result sym a) -> W4Eval sym a
W4Eval forall a b. (a -> b) -> a -> b
$ forall sym a. (sym -> Eval a) -> W4Conn sym a
W4Conn forall a b. (a -> b) -> a -> b
$ \sym
_ ->
    forall a. Eval a -> Eval (Maybe a)
maybeReady (forall sym a. W4Eval sym a -> sym -> Eval (W4Result sym a)
w4Eval SEval (What4 sym) a
m (forall sym. What4 sym -> sym
w4 What4 sym
sym)) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Just W4Result sym a
x  -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> W4Result sym a
x)
      Maybe (W4Result sym a)
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall sym a. Pred sym -> a -> W4Result sym a
W4Result (forall sym. IsExprBuilder sym => sym -> Bool -> Pred sym
W4.backendPred (forall sym. What4 sym -> sym
w4 What4 sym
sym) Bool
True) forall a. Maybe a
Nothing)

  sDelayFill :: forall a.
What4 sym
-> SEval (What4 sym) a
-> Maybe (SEval (What4 sym) a)
-> String
-> SEval (What4 sym) (SEval (What4 sym) a)
sDelayFill What4 sym
_ SEval (What4 sym) a
m Maybe (SEval (What4 sym) a)
retry String
msg =
    forall sym a. IsSymExprBuilder sym => W4Conn sym a -> W4Eval sym a
total
    do sym
sym <- forall sym. W4Conn sym sym
getSym
       forall sym a. IsSymExprBuilder sym => Eval a -> W4Conn sym a
doEval (forall sym a. Eval (W4Result sym a) -> W4Eval sym a
w4Thunk forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Eval a -> Maybe (Eval a) -> String -> Eval (Eval a)
delayFill (forall sym a. W4Eval sym a -> sym -> Eval (W4Result sym a)
w4Eval SEval (What4 sym) a
m sym
sym) (forall sym a. W4Eval sym a -> sym -> Eval (W4Result sym a)
w4Eval forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (SEval (What4 sym) a)
retry forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure sym
sym) String
msg)

  sSpark :: forall a.
What4 sym
-> SEval (What4 sym) a -> SEval (What4 sym) (SEval (What4 sym) a)
sSpark What4 sym
_ SEval (What4 sym) a
m =
    forall sym a. IsSymExprBuilder sym => W4Conn sym a -> W4Eval sym a
total
    do sym
sym   <- forall sym. W4Conn sym sym
getSym
       forall sym a. IsSymExprBuilder sym => Eval a -> W4Conn sym a
doEval (forall sym a. Eval (W4Result sym a) -> W4Eval sym a
w4Thunk forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Eval a -> Eval (Eval a)
evalSpark (forall sym a. W4Eval sym a -> sym -> Eval (W4Result sym a)
w4Eval SEval (What4 sym) a
m sym
sym))

  sModifyCallStack :: forall a.
What4 sym
-> (CallStack -> CallStack)
-> SEval (What4 sym) a
-> SEval (What4 sym) a
sModifyCallStack What4 sym
_ CallStack -> CallStack
f (W4Eval (W4Conn sym -> Eval (W4Result sym a)
m)) =
    forall sym a. W4Conn sym (W4Result sym a) -> W4Eval sym a
W4Eval (forall sym a. (sym -> Eval a) -> W4Conn sym a
W4Conn \sym
sym -> forall a. (CallStack -> CallStack) -> Eval a -> Eval a
modifyCallStack CallStack -> CallStack
f (sym -> Eval (W4Result sym a)
m sym
sym))

  sGetCallStack :: What4 sym -> SEval (What4 sym) CallStack
sGetCallStack What4 sym
_ = forall sym a. IsSymExprBuilder sym => W4Conn sym a -> W4Eval sym a
total (forall sym a. IsSymExprBuilder sym => Eval a -> W4Conn sym a
doEval Eval CallStack
getCallStack)

  sDeclareHole :: forall a.
What4 sym
-> String
-> SEval
     (What4 sym)
     (SEval (What4 sym) a, SEval (What4 sym) a -> SEval (What4 sym) ())
sDeclareHole What4 sym
_ String
msg =
    forall sym a. IsSymExprBuilder sym => W4Conn sym a -> W4Eval sym a
total
    do (Eval (W4Result sym a)
hole, Eval (W4Result sym a) -> Eval ()
fill) <- forall sym a. IsSymExprBuilder sym => Eval a -> W4Conn sym a
doEval (forall a. String -> Eval (Eval a, Eval a -> Eval ())
blackhole String
msg)
       forall (f :: * -> *) a. Applicative f => a -> f a
pure ( forall sym a. Eval (W4Result sym a) -> W4Eval sym a
w4Thunk Eval (W4Result sym a)
hole
            , \W4Eval sym a
m -> forall sym a. IsSymExprBuilder sym => W4Conn sym a -> W4Eval sym a
total
                    do sym
sym <- forall sym. W4Conn sym sym
getSym
                       forall sym a. IsSymExprBuilder sym => Eval a -> W4Conn sym a
doEval (Eval (W4Result sym a) -> Eval ()
fill (forall sym a. W4Eval sym a -> sym -> Eval (W4Result sym a)
w4Eval W4Eval sym a
m sym
sym))
            )

  mergeEval :: forall a.
What4 sym
-> (SBit (What4 sym) -> a -> a -> SEval (What4 sym) a)
-> SBit (What4 sym)
-> SEval (What4 sym) a
-> SEval (What4 sym) a
-> SEval (What4 sym) a
mergeEval What4 sym
_sym SBit (What4 sym) -> a -> a -> SEval (What4 sym) a
f SBit (What4 sym)
c SEval (What4 sym) a
mx SEval (What4 sym) a
my = forall sym a. W4Conn sym (W4Result sym a) -> W4Eval sym a
W4Eval
    do W4Result sym a
rx <- forall sym a. W4Eval sym a -> W4Conn sym (W4Result sym a)
evalPartial SEval (What4 sym) a
mx
       W4Result sym a
ry <- forall sym a. W4Eval sym a -> W4Conn sym (W4Result sym a)
evalPartial SEval (What4 sym) a
my
       case (W4Result sym a
rx, W4Result sym a
ry) of

         (W4Error EvalErrorEx
err, W4Error EvalErrorEx
_) ->
           forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall sym a. EvalErrorEx -> W4Result sym a
W4Error EvalErrorEx
err) -- arbitrarily choose left error to report

         (W4Error EvalErrorEx
_, W4Result Pred sym
p a
y) ->
           do Pred sym
p' <- forall sym.
IsSymExprBuilder sym =>
Pred sym -> Pred sym -> W4Conn sym (Pred sym)
w4And Pred sym
p forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsSymExprBuilder sym =>
Pred sym -> W4Conn sym (Pred sym)
w4Not SBit (What4 sym)
c
              forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall sym a. Pred sym -> a -> W4Result sym a
W4Result Pred sym
p' a
y)

         (W4Result Pred sym
p a
x, W4Error EvalErrorEx
_) ->
           do Pred sym
p' <- forall sym.
IsSymExprBuilder sym =>
Pred sym -> Pred sym -> W4Conn sym (Pred sym)
w4And Pred sym
p SBit (What4 sym)
c
              forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall sym a. Pred sym -> a -> W4Result sym a
W4Result Pred sym
p' a
x)

         (W4Result Pred sym
px a
x, W4Result Pred sym
py a
y) ->
           do W4Result sym a
zr <- forall sym a. W4Eval sym a -> W4Conn sym (W4Result sym a)
evalPartial (SBit (What4 sym) -> a -> a -> SEval (What4 sym) a
f SBit (What4 sym)
c a
x a
y)
              case W4Result sym a
zr of
                W4Error EvalErrorEx
err -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall sym a. EvalErrorEx -> W4Result sym a
W4Error EvalErrorEx
err
                W4Result Pred sym
pz a
z ->
                  do Pred sym
p' <- forall sym.
IsSymExprBuilder sym =>
Pred sym -> Pred sym -> W4Conn sym (Pred sym)
w4And Pred sym
pz forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsSymExprBuilder sym =>
Pred sym -> Pred sym -> Pred sym -> W4Conn sym (Pred sym)
w4ITE SBit (What4 sym)
c Pred sym
px Pred sym
py
                     forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall sym a. Pred sym -> a -> W4Result sym a
W4Result Pred sym
p' a
z)

  wordAsChar :: What4 sym -> SWord (What4 sym) -> Maybe Char
wordAsChar What4 sym
_ SWord (What4 sym)
bv
    | forall sym. SWord sym -> Integer
SW.bvWidth SWord (What4 sym)
bv forall a. Eq a => a -> a -> Bool
== Integer
8 = forall a. Enum a => Int -> a
toEnum forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Num a => Integer -> a
fromInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym. IsExprBuilder sym => SWord sym -> Maybe Integer
SW.bvAsUnsignedInteger SWord (What4 sym)
bv
    | Bool
otherwise = forall a. Maybe a
Nothing

  wordLen :: What4 sym -> SWord (What4 sym) -> Integer
wordLen What4 sym
_ SWord (What4 sym)
bv = forall sym. SWord sym -> Integer
SW.bvWidth SWord (What4 sym)
bv

  bitLit :: What4 sym -> Bool -> SBit (What4 sym)
bitLit What4 sym
sym Bool
b = forall sym. IsExprBuilder sym => sym -> Bool -> Pred sym
W4.backendPred (forall sym. What4 sym -> sym
w4 What4 sym
sym) Bool
b
  bitAsLit :: What4 sym -> SBit (What4 sym) -> Maybe Bool
bitAsLit What4 sym
_ SBit (What4 sym)
v = forall (e :: BaseType -> *).
IsExpr e =>
e BaseBoolType -> Maybe Bool
W4.asConstantPred SBit (What4 sym)
v

  wordLit :: What4 sym
-> Integer -> Integer -> SEval (What4 sym) (SWord (What4 sym))
wordLit What4 sym
sym Integer
intw Integer
i
    | Just (Some NatRepr x
w) <- forall a. Integral a => a -> Maybe (Some NatRepr)
someNat Integer
intw
    = case forall (n :: Nat). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr x
w of
        Maybe (LeqProof 1 x)
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall sym. SWord sym
SW.ZBV
        Just LeqProof 1 x
LeqProof -> forall sym (w :: Nat).
(IsExpr (SymExpr sym), 1 <= w) =>
SymBV sym w -> SWord sym
SW.DBV forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
W4.bvLit (forall sym. What4 sym -> sym
w4 What4 sym
sym) NatRepr x
w (forall (w :: Nat). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr x
w Integer
i))
    | Bool
otherwise = forall a. HasCallStack => String -> [String] -> a
panic String
"what4: wordLit" [String
"invalid bit width:", forall a. Show a => a -> String
show Integer
intw ]

  wordAsLit :: What4 sym -> SWord (What4 sym) -> Maybe (Integer, Integer)
wordAsLit What4 sym
_ SWord (What4 sym)
v
    | Just Integer
x <- forall sym. IsExprBuilder sym => SWord sym -> Maybe Integer
SW.bvAsUnsignedInteger SWord (What4 sym)
v = forall a. a -> Maybe a
Just (forall sym. SWord sym -> Integer
SW.bvWidth SWord (What4 sym)
v, Integer
x)
    | Bool
otherwise = forall a. Maybe a
Nothing

  integerLit :: What4 sym -> Integer -> SEval (What4 sym) (SInteger (What4 sym))
integerLit What4 sym
sym Integer
i = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
W4.intLit (forall sym. What4 sym -> sym
w4 What4 sym
sym) Integer
i)

  integerAsLit :: What4 sym -> SInteger (What4 sym) -> Maybe Integer
integerAsLit What4 sym
_ SInteger (What4 sym)
v = forall (e :: BaseType -> *).
IsExpr e =>
e BaseIntegerType -> Maybe Integer
W4.asInteger SInteger (What4 sym)
v

  iteBit :: What4 sym
-> SBit (What4 sym)
-> SBit (What4 sym)
-> SBit (What4 sym)
-> SEval (What4 sym) (SBit (What4 sym))
iteBit What4 sym
sym SBit (What4 sym)
c SBit (What4 sym)
x SBit (What4 sym)
y = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> Pred sym -> IO (Pred sym)
W4.itePred (forall sym. What4 sym -> sym
w4 What4 sym
sym) SBit (What4 sym)
c SBit (What4 sym)
x SBit (What4 sym)
y)
  iteWord :: What4 sym
-> SBit (What4 sym)
-> SWord (What4 sym)
-> SWord (What4 sym)
-> SEval (What4 sym) (SWord (What4 sym))
iteWord What4 sym
sym SBit (What4 sym)
c SWord (What4 sym)
x SWord (What4 sym)
y = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> SWord sym -> SWord sym -> IO (SWord sym)
SW.bvIte (forall sym. What4 sym -> sym
w4 What4 sym
sym) SBit (What4 sym)
c SWord (What4 sym)
x SWord (What4 sym)
y)
  iteInteger :: What4 sym
-> SBit (What4 sym)
-> SInteger (What4 sym)
-> SInteger (What4 sym)
-> SEval (What4 sym) (SInteger (What4 sym))
iteInteger What4 sym
sym SBit (What4 sym)
c SInteger (What4 sym)
x SInteger (What4 sym)
y = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym.
IsExprBuilder sym =>
sym
-> Pred sym
-> SymInteger sym
-> SymInteger sym
-> IO (SymInteger sym)
W4.intIte (forall sym. What4 sym -> sym
w4 What4 sym
sym) SBit (What4 sym)
c SInteger (What4 sym)
x SInteger (What4 sym)
y)
  iteFloat :: What4 sym
-> SBit (What4 sym)
-> SFloat (What4 sym)
-> SFloat (What4 sym)
-> SEval (What4 sym) (SFloat (What4 sym))
iteFloat What4 sym
sym SBit (What4 sym)
p SFloat (What4 sym)
x SFloat (What4 sym)
y = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> SFloat sym -> SFloat sym -> IO (SFloat sym)
FP.fpIte (forall sym. What4 sym -> sym
w4 What4 sym
sym) SBit (What4 sym)
p SFloat (What4 sym)
x SFloat (What4 sym)
y)

  bitEq :: What4 sym
-> SBit (What4 sym)
-> SBit (What4 sym)
-> SEval (What4 sym) (SBit (What4 sym))
bitEq  What4 sym
sym SBit (What4 sym)
x SBit (What4 sym)
y = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
W4.eqPred (forall sym. What4 sym -> sym
w4 What4 sym
sym) SBit (What4 sym)
x SBit (What4 sym)
y)
  bitAnd :: What4 sym
-> SBit (What4 sym)
-> SBit (What4 sym)
-> SEval (What4 sym) (SBit (What4 sym))
bitAnd What4 sym
sym SBit (What4 sym)
x SBit (What4 sym)
y = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
W4.andPred (forall sym. What4 sym -> sym
w4 What4 sym
sym) SBit (What4 sym)
x SBit (What4 sym)
y)
  bitOr :: What4 sym
-> SBit (What4 sym)
-> SBit (What4 sym)
-> SEval (What4 sym) (SBit (What4 sym))
bitOr  What4 sym
sym SBit (What4 sym)
x SBit (What4 sym)
y = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
W4.orPred (forall sym. What4 sym -> sym
w4 What4 sym
sym) SBit (What4 sym)
x SBit (What4 sym)
y)
  bitXor :: What4 sym
-> SBit (What4 sym)
-> SBit (What4 sym)
-> SEval (What4 sym) (SBit (What4 sym))
bitXor What4 sym
sym SBit (What4 sym)
x SBit (What4 sym)
y = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
W4.xorPred (forall sym. What4 sym -> sym
w4 What4 sym
sym) SBit (What4 sym)
x SBit (What4 sym)
y)
  bitComplement :: What4 sym
-> SBit (What4 sym) -> SEval (What4 sym) (SBit (What4 sym))
bitComplement What4 sym
sym SBit (What4 sym)
x = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
W4.notPred (forall sym. What4 sym -> sym
w4 What4 sym
sym) SBit (What4 sym)
x)

  wordBit :: What4 sym
-> SWord (What4 sym)
-> Integer
-> SEval (What4 sym) (SBit (What4 sym))
wordBit What4 sym
sym SWord (What4 sym)
bv Integer
idx = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> Integer -> IO (Pred sym)
SW.bvAtBE (forall sym. What4 sym -> sym
w4 What4 sym
sym) SWord (What4 sym)
bv Integer
idx)
  wordUpdate :: What4 sym
-> SWord (What4 sym)
-> Integer
-> SBit (What4 sym)
-> SEval (What4 sym) (SWord (What4 sym))
wordUpdate What4 sym
sym SWord (What4 sym)
bv Integer
idx SBit (What4 sym)
b = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> Integer -> Pred sym -> IO (SWord sym)
SW.bvSetBE (forall sym. What4 sym -> sym
w4 What4 sym
sym) SWord (What4 sym)
bv Integer
idx SBit (What4 sym)
b)

  packWord :: What4 sym
-> [SBit (What4 sym)] -> SEval (What4 sym) (SWord (What4 sym))
packWord What4 sym
sym [SBit (What4 sym)]
bs =
    do SWord sym
z <- forall sym.
Backend sym =>
sym -> Integer -> Integer -> SEval sym (SWord sym)
wordLit What4 sym
sym (forall i a. Num i => [a] -> i
genericLength [SBit (What4 sym)]
bs) Integer
0
       let f :: SWord sym
-> (Integer, Pred sym) -> SEval (What4 sym) (SWord (What4 sym))
f SWord sym
w (Integer
idx,Pred sym
b) = forall sym.
Backend sym =>
sym -> SWord sym -> Integer -> SBit sym -> SEval sym (SWord sym)
wordUpdate What4 sym
sym SWord sym
w Integer
idx Pred sym
b
       forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM SWord sym
-> (Integer, Pred sym) -> SEval (What4 sym) (SWord (What4 sym))
f SWord sym
z (forall a b. [a] -> [b] -> [(a, b)]
zip [Integer
0..] [SBit (What4 sym)]
bs)

  unpackWord :: What4 sym
-> SWord (What4 sym) -> SEval (What4 sym) [SBit (What4 sym)]
unpackWord What4 sym
sym SWord (What4 sym)
bv = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$
    forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> Integer -> IO (Pred sym)
SW.bvAtBE (forall sym. What4 sym -> sym
w4 What4 sym
sym) SWord (What4 sym)
bv) [Integer
0 .. forall sym. SWord sym -> Integer
SW.bvWidth SWord (What4 sym)
bvforall a. Num a => a -> a -> a
-Integer
1]

  joinWord :: What4 sym
-> SWord (What4 sym)
-> SWord (What4 sym)
-> SEval (What4 sym) (SWord (What4 sym))
joinWord What4 sym
sym SWord (What4 sym)
x SWord (What4 sym)
y = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> SWord sym -> IO (SWord sym)
SW.bvJoin (forall sym. What4 sym -> sym
w4 What4 sym
sym) SWord (What4 sym)
x SWord (What4 sym)
y

  splitWord :: What4 sym
-> Integer
-> Integer
-> SWord (What4 sym)
-> SEval (What4 sym) (SWord (What4 sym), SWord (What4 sym))
splitWord What4 sym
_sym Integer
0 Integer
_ SWord (What4 sym)
bv = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall sym. SWord sym
SW.ZBV, SWord (What4 sym)
bv)
  splitWord What4 sym
_sym Integer
_ Integer
0 SWord (What4 sym)
bv = forall (f :: * -> *) a. Applicative f => a -> f a
pure (SWord (What4 sym)
bv, forall sym. SWord sym
SW.ZBV)
  splitWord What4 sym
sym Integer
lw Integer
rw SWord (What4 sym)
bv = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$
    do SWord sym
l <- forall sym.
IsExprBuilder sym =>
sym -> Integer -> Integer -> SWord sym -> IO (SWord sym)
SW.bvSliceBE (forall sym. What4 sym -> sym
w4 What4 sym
sym) Integer
0 Integer
lw SWord (What4 sym)
bv
       SWord sym
r <- forall sym.
IsExprBuilder sym =>
sym -> Integer -> Integer -> SWord sym -> IO (SWord sym)
SW.bvSliceBE (forall sym. What4 sym -> sym
w4 What4 sym
sym) Integer
lw Integer
rw SWord (What4 sym)
bv
       forall (m :: * -> *) a. Monad m => a -> m a
return (SWord sym
l, SWord sym
r)

  extractWord :: What4 sym
-> Integer
-> Integer
-> SWord (What4 sym)
-> SEval (What4 sym) (SWord (What4 sym))
extractWord What4 sym
sym Integer
bits Integer
idx SWord (What4 sym)
bv =
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> Integer -> Integer -> SWord sym -> IO (SWord sym)
SW.bvSliceLE (forall sym. What4 sym -> sym
w4 What4 sym
sym) Integer
idx Integer
bits SWord (What4 sym)
bv

  wordEq :: What4 sym
-> SWord (What4 sym)
-> SWord (What4 sym)
-> SEval (What4 sym) (SBit (What4 sym))
wordEq                What4 sym
sym SWord (What4 sym)
x SWord (What4 sym)
y = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (PredBin
SW.bvEq  (forall sym. What4 sym -> sym
w4 What4 sym
sym) SWord (What4 sym)
x SWord (What4 sym)
y)
  wordLessThan :: What4 sym
-> SWord (What4 sym)
-> SWord (What4 sym)
-> SEval (What4 sym) (SBit (What4 sym))
wordLessThan          What4 sym
sym SWord (What4 sym)
x SWord (What4 sym)
y = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (PredBin
SW.bvult (forall sym. What4 sym -> sym
w4 What4 sym
sym) SWord (What4 sym)
x SWord (What4 sym)
y)
  wordGreaterThan :: What4 sym
-> SWord (What4 sym)
-> SWord (What4 sym)
-> SEval (What4 sym) (SBit (What4 sym))
wordGreaterThan       What4 sym
sym SWord (What4 sym)
x SWord (What4 sym)
y = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (PredBin
SW.bvugt (forall sym. What4 sym -> sym
w4 What4 sym
sym) SWord (What4 sym)
x SWord (What4 sym)
y)
  wordSignedLessThan :: What4 sym
-> SWord (What4 sym)
-> SWord (What4 sym)
-> SEval (What4 sym) (SBit (What4 sym))
wordSignedLessThan    What4 sym
sym SWord (What4 sym)
x SWord (What4 sym)
y = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (PredBin
SW.bvslt (forall sym. What4 sym -> sym
w4 What4 sym
sym) SWord (What4 sym)
x SWord (What4 sym)
y)

  wordOr :: What4 sym
-> SWord (What4 sym)
-> SWord (What4 sym)
-> SEval (What4 sym) (SWord (What4 sym))
wordOr  What4 sym
sym SWord (What4 sym)
x SWord (What4 sym)
y = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> SWord sym -> IO (SWord sym)
SW.bvOr  (forall sym. What4 sym -> sym
w4 What4 sym
sym) SWord (What4 sym)
x SWord (What4 sym)
y)
  wordAnd :: What4 sym
-> SWord (What4 sym)
-> SWord (What4 sym)
-> SEval (What4 sym) (SWord (What4 sym))
wordAnd What4 sym
sym SWord (What4 sym)
x SWord (What4 sym)
y = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> SWord sym -> IO (SWord sym)
SW.bvAnd (forall sym. What4 sym -> sym
w4 What4 sym
sym) SWord (What4 sym)
x SWord (What4 sym)
y)
  wordXor :: What4 sym
-> SWord (What4 sym)
-> SWord (What4 sym)
-> SEval (What4 sym) (SWord (What4 sym))
wordXor What4 sym
sym SWord (What4 sym)
x SWord (What4 sym)
y = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> SWord sym -> IO (SWord sym)
SW.bvXor (forall sym. What4 sym -> sym
w4 What4 sym
sym) SWord (What4 sym)
x SWord (What4 sym)
y)
  wordComplement :: What4 sym
-> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym))
wordComplement What4 sym
sym SWord (What4 sym)
x = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (SWordUn
SW.bvNot (forall sym. What4 sym -> sym
w4 What4 sym
sym) SWord (What4 sym)
x)

  wordPlus :: What4 sym
-> SWord (What4 sym)
-> SWord (What4 sym)
-> SEval (What4 sym) (SWord (What4 sym))
wordPlus   What4 sym
sym SWord (What4 sym)
x SWord (What4 sym)
y = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> SWord sym -> IO (SWord sym)
SW.bvAdd (forall sym. What4 sym -> sym
w4 What4 sym
sym) SWord (What4 sym)
x SWord (What4 sym)
y)
  wordMinus :: What4 sym
-> SWord (What4 sym)
-> SWord (What4 sym)
-> SEval (What4 sym) (SWord (What4 sym))
wordMinus  What4 sym
sym SWord (What4 sym)
x SWord (What4 sym)
y = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> SWord sym -> IO (SWord sym)
SW.bvSub (forall sym. What4 sym -> sym
w4 What4 sym
sym) SWord (What4 sym)
x SWord (What4 sym)
y)
  wordMult :: What4 sym
-> SWord (What4 sym)
-> SWord (What4 sym)
-> SEval (What4 sym) (SWord (What4 sym))
wordMult   What4 sym
sym SWord (What4 sym)
x SWord (What4 sym)
y = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> SWord sym -> IO (SWord sym)
SW.bvMul (forall sym. What4 sym -> sym
w4 What4 sym
sym) SWord (What4 sym)
x SWord (What4 sym)
y)
  wordNegate :: What4 sym
-> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym))
wordNegate What4 sym
sym SWord (What4 sym)
x   = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (SWordUn
SW.bvNeg (forall sym. What4 sym -> sym
w4 What4 sym
sym) SWord (What4 sym)
x)
  wordLg2 :: What4 sym
-> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym))
wordLg2    What4 sym
sym SWord (What4 sym)
x   = forall sym.
IsSymExprBuilder sym =>
sym -> SWord sym -> SEval (What4 sym) (SWord sym)
sLg2 (forall sym. What4 sym -> sym
w4 What4 sym
sym) SWord (What4 sym)
x

  wordShiftLeft :: What4 sym
-> SWord (What4 sym)
-> SWord (What4 sym)
-> SEval (What4 sym) (SWord (What4 sym))
wordShiftLeft   What4 sym
sym SWord (What4 sym)
x SWord (What4 sym)
y = forall sym.
IsSymExprBuilder sym =>
sym -> SWord sym -> SWord sym -> W4Eval sym (SWord sym)
w4bvShl (forall sym. What4 sym -> sym
w4 What4 sym
sym) SWord (What4 sym)
x SWord (What4 sym)
y
  wordShiftRight :: What4 sym
-> SWord (What4 sym)
-> SWord (What4 sym)
-> SEval (What4 sym) (SWord (What4 sym))
wordShiftRight  What4 sym
sym SWord (What4 sym)
x SWord (What4 sym)
y = forall sym.
IsSymExprBuilder sym =>
sym -> SWord sym -> SWord sym -> W4Eval sym (SWord sym)
w4bvLshr (forall sym. What4 sym -> sym
w4 What4 sym
sym) SWord (What4 sym)
x SWord (What4 sym)
y
  wordRotateLeft :: What4 sym
-> SWord (What4 sym)
-> SWord (What4 sym)
-> SEval (What4 sym) (SWord (What4 sym))
wordRotateLeft  What4 sym
sym SWord (What4 sym)
x SWord (What4 sym)
y = forall sym.
IsSymExprBuilder sym =>
sym -> SWord sym -> SWord sym -> W4Eval sym (SWord sym)
w4bvRol (forall sym. What4 sym -> sym
w4 What4 sym
sym) SWord (What4 sym)
x SWord (What4 sym)
y
  wordRotateRight :: What4 sym
-> SWord (What4 sym)
-> SWord (What4 sym)
-> SEval (What4 sym) (SWord (What4 sym))
wordRotateRight What4 sym
sym SWord (What4 sym)
x SWord (What4 sym)
y = forall sym.
IsSymExprBuilder sym =>
sym -> SWord sym -> SWord sym -> W4Eval sym (SWord sym)
w4bvRor (forall sym. What4 sym -> sym
w4 What4 sym
sym) SWord (What4 sym)
x SWord (What4 sym)
y
  wordSignedShiftRight :: What4 sym
-> SWord (What4 sym)
-> SWord (What4 sym)
-> SEval (What4 sym) (SWord (What4 sym))
wordSignedShiftRight What4 sym
sym SWord (What4 sym)
x SWord (What4 sym)
y = forall sym.
IsSymExprBuilder sym =>
sym -> SWord sym -> SWord sym -> W4Eval sym (SWord sym)
w4bvAshr (forall sym. What4 sym -> sym
w4 What4 sym
sym) SWord (What4 sym)
x SWord (What4 sym)
y

  wordDiv :: What4 sym
-> SWord (What4 sym)
-> SWord (What4 sym)
-> SEval (What4 sym) (SWord (What4 sym))
wordDiv What4 sym
sym SWord (What4 sym)
x SWord (What4 sym)
y =
     do forall sym.
IsSymExprBuilder sym =>
What4 sym -> SWord sym -> W4Eval sym ()
assertBVDivisor What4 sym
sym SWord (What4 sym)
y
        forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> SWord sym -> IO (SWord sym)
SW.bvUDiv (forall sym. What4 sym -> sym
w4 What4 sym
sym) SWord (What4 sym)
x SWord (What4 sym)
y)
  wordMod :: What4 sym
-> SWord (What4 sym)
-> SWord (What4 sym)
-> SEval (What4 sym) (SWord (What4 sym))
wordMod What4 sym
sym SWord (What4 sym)
x SWord (What4 sym)
y =
     do forall sym.
IsSymExprBuilder sym =>
What4 sym -> SWord sym -> W4Eval sym ()
assertBVDivisor What4 sym
sym SWord (What4 sym)
y
        forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> SWord sym -> IO (SWord sym)
SW.bvURem (forall sym. What4 sym -> sym
w4 What4 sym
sym) SWord (What4 sym)
x SWord (What4 sym)
y)
  wordSignedDiv :: What4 sym
-> SWord (What4 sym)
-> SWord (What4 sym)
-> SEval (What4 sym) (SWord (What4 sym))
wordSignedDiv What4 sym
sym SWord (What4 sym)
x SWord (What4 sym)
y =
     do forall sym.
IsSymExprBuilder sym =>
What4 sym -> SWord sym -> W4Eval sym ()
assertBVDivisor What4 sym
sym SWord (What4 sym)
y
        forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> SWord sym -> IO (SWord sym)
SW.bvSDiv (forall sym. What4 sym -> sym
w4 What4 sym
sym) SWord (What4 sym)
x SWord (What4 sym)
y)
  wordSignedMod :: What4 sym
-> SWord (What4 sym)
-> SWord (What4 sym)
-> SEval (What4 sym) (SWord (What4 sym))
wordSignedMod What4 sym
sym SWord (What4 sym)
x SWord (What4 sym)
y =
     do forall sym.
IsSymExprBuilder sym =>
What4 sym -> SWord sym -> W4Eval sym ()
assertBVDivisor What4 sym
sym SWord (What4 sym)
y
        forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> SWord sym -> IO (SWord sym)
SW.bvSRem (forall sym. What4 sym -> sym
w4 What4 sym
sym) SWord (What4 sym)
x SWord (What4 sym)
y)

  wordToInt :: What4 sym
-> SWord (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym))
wordToInt What4 sym
sym SWord (What4 sym)
x = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> IO (SymInteger sym)
SW.bvToInteger (forall sym. What4 sym -> sym
w4 What4 sym
sym) SWord (What4 sym)
x)
  wordToSignedInt :: What4 sym
-> SWord (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym))
wordToSignedInt What4 sym
sym SWord (What4 sym)
x = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> IO (SymInteger sym)
SW.sbvToInteger (forall sym. What4 sym -> sym
w4 What4 sym
sym) SWord (What4 sym)
x)
  wordFromInt :: What4 sym
-> Integer
-> SInteger (What4 sym)
-> SEval (What4 sym) (SWord (What4 sym))
wordFromInt What4 sym
sym Integer
width SInteger (What4 sym)
i = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym width.
(Show width, Integral width, IsExprBuilder sym) =>
sym -> SymInteger sym -> width -> IO (SWord sym)
SW.integerToBV (forall sym. What4 sym -> sym
w4 What4 sym
sym) SInteger (What4 sym)
i Integer
width)

  intPlus :: What4 sym
-> SInteger (What4 sym)
-> SInteger (What4 sym)
-> SEval (What4 sym) (SInteger (What4 sym))
intPlus   What4 sym
sym SInteger (What4 sym)
x SInteger (What4 sym)
y  = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
W4.intAdd (forall sym. What4 sym -> sym
w4 What4 sym
sym) SInteger (What4 sym)
x SInteger (What4 sym)
y
  intMinus :: What4 sym
-> SInteger (What4 sym)
-> SInteger (What4 sym)
-> SEval (What4 sym) (SInteger (What4 sym))
intMinus  What4 sym
sym SInteger (What4 sym)
x SInteger (What4 sym)
y  = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
W4.intSub (forall sym. What4 sym -> sym
w4 What4 sym
sym) SInteger (What4 sym)
x SInteger (What4 sym)
y
  intMult :: What4 sym
-> SInteger (What4 sym)
-> SInteger (What4 sym)
-> SEval (What4 sym) (SInteger (What4 sym))
intMult   What4 sym
sym SInteger (What4 sym)
x SInteger (What4 sym)
y  = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
W4.intMul (forall sym. What4 sym -> sym
w4 What4 sym
sym) SInteger (What4 sym)
x SInteger (What4 sym)
y
  intNegate :: What4 sym
-> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym))
intNegate What4 sym
sym SInteger (What4 sym)
x    = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymInteger sym)
W4.intNeg (forall sym. What4 sym -> sym
w4 What4 sym
sym) SInteger (What4 sym)
x

  -- NB: What4's division operation provides SMTLib's euclidean division,
  -- which doesn't match the round-to-neg-infinity semantics of Cryptol,
  -- so we have to do some work to get the desired semantics.
  intDiv :: What4 sym
-> SInteger (What4 sym)
-> SInteger (What4 sym)
-> SEval (What4 sym) (SInteger (What4 sym))
intDiv What4 sym
sym SInteger (What4 sym)
x SInteger (What4 sym)
y =
    do forall sym.
IsSymExprBuilder sym =>
What4 sym -> SymInteger sym -> W4Eval sym ()
assertIntDivisor What4 sym
sym SInteger (What4 sym)
y
       forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ do
         Pred sym
neg <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
W4.intLt (forall sym. What4 sym -> sym
w4 What4 sym
sym) SInteger (What4 sym)
y forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
W4.intLit (forall sym. What4 sym -> sym
w4 What4 sym
sym) Integer
0)
         case forall (e :: BaseType -> *).
IsExpr e =>
e BaseBoolType -> Maybe Bool
W4.asConstantPred Pred sym
neg of
           Just Bool
False -> forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
W4.intDiv (forall sym. What4 sym -> sym
w4 What4 sym
sym) SInteger (What4 sym)
x SInteger (What4 sym)
y
           Just Bool
True  ->
              do SymExpr sym BaseIntegerType
xneg <- forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymInteger sym)
W4.intNeg (forall sym. What4 sym -> sym
w4 What4 sym
sym) SInteger (What4 sym)
x
                 SymExpr sym BaseIntegerType
yneg <- forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymInteger sym)
W4.intNeg (forall sym. What4 sym -> sym
w4 What4 sym
sym) SInteger (What4 sym)
y
                 forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
W4.intDiv (forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym BaseIntegerType
xneg SymExpr sym BaseIntegerType
yneg
           Maybe Bool
Nothing ->
              do SymExpr sym BaseIntegerType
xneg <- forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymInteger sym)
W4.intNeg (forall sym. What4 sym -> sym
w4 What4 sym
sym) SInteger (What4 sym)
x
                 SymExpr sym BaseIntegerType
yneg <- forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymInteger sym)
W4.intNeg (forall sym. What4 sym -> sym
w4 What4 sym
sym) SInteger (What4 sym)
y
                 SymExpr sym BaseIntegerType
zneg <- forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
W4.intDiv (forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym BaseIntegerType
xneg SymExpr sym BaseIntegerType
yneg
                 SymExpr sym BaseIntegerType
z    <- forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
W4.intDiv (forall sym. What4 sym -> sym
w4 What4 sym
sym) SInteger (What4 sym)
x SInteger (What4 sym)
y
                 forall sym.
IsExprBuilder sym =>
sym
-> Pred sym
-> SymInteger sym
-> SymInteger sym
-> IO (SymInteger sym)
W4.intIte (forall sym. What4 sym -> sym
w4 What4 sym
sym) Pred sym
neg SymExpr sym BaseIntegerType
zneg SymExpr sym BaseIntegerType
z

  -- NB: What4's division operation provides SMTLib's euclidean division,
  -- which doesn't match the round-to-neg-infinity semantics of Cryptol,
  -- so we have to do some work to get the desired semantics.
  intMod :: What4 sym
-> SInteger (What4 sym)
-> SInteger (What4 sym)
-> SEval (What4 sym) (SInteger (What4 sym))
intMod What4 sym
sym SInteger (What4 sym)
x SInteger (What4 sym)
y =
    do forall sym.
IsSymExprBuilder sym =>
What4 sym -> SymInteger sym -> W4Eval sym ()
assertIntDivisor What4 sym
sym SInteger (What4 sym)
y
       forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ do
         Pred sym
neg <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
W4.intLt (forall sym. What4 sym -> sym
w4 What4 sym
sym) SInteger (What4 sym)
y forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
W4.intLit (forall sym. What4 sym -> sym
w4 What4 sym
sym) Integer
0)
         case forall (e :: BaseType -> *).
IsExpr e =>
e BaseBoolType -> Maybe Bool
W4.asConstantPred Pred sym
neg of
           Just Bool
False -> forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
W4.intMod (forall sym. What4 sym -> sym
w4 What4 sym
sym) SInteger (What4 sym)
x SInteger (What4 sym)
y
           Just Bool
True  ->
              do SymExpr sym BaseIntegerType
xneg <- forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymInteger sym)
W4.intNeg (forall sym. What4 sym -> sym
w4 What4 sym
sym) SInteger (What4 sym)
x
                 SymExpr sym BaseIntegerType
yneg <- forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymInteger sym)
W4.intNeg (forall sym. What4 sym -> sym
w4 What4 sym
sym) SInteger (What4 sym)
y
                 forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymInteger sym)
W4.intNeg (forall sym. What4 sym -> sym
w4 What4 sym
sym) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
W4.intMod (forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym BaseIntegerType
xneg SymExpr sym BaseIntegerType
yneg
           Maybe Bool
Nothing ->
              do SymExpr sym BaseIntegerType
xneg <- forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymInteger sym)
W4.intNeg (forall sym. What4 sym -> sym
w4 What4 sym
sym) SInteger (What4 sym)
x
                 SymExpr sym BaseIntegerType
yneg <- forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymInteger sym)
W4.intNeg (forall sym. What4 sym -> sym
w4 What4 sym
sym) SInteger (What4 sym)
y
                 SymExpr sym BaseIntegerType
z    <- forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
W4.intMod (forall sym. What4 sym -> sym
w4 What4 sym
sym) SInteger (What4 sym)
x SInteger (What4 sym)
y
                 SymExpr sym BaseIntegerType
zneg <- forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymInteger sym)
W4.intNeg (forall sym. What4 sym -> sym
w4 What4 sym
sym) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
W4.intMod (forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym BaseIntegerType
xneg SymExpr sym BaseIntegerType
yneg
                 forall sym.
IsExprBuilder sym =>
sym
-> Pred sym
-> SymInteger sym
-> SymInteger sym
-> IO (SymInteger sym)
W4.intIte (forall sym. What4 sym -> sym
w4 What4 sym
sym) Pred sym
neg SymExpr sym BaseIntegerType
zneg SymExpr sym BaseIntegerType
z

  intEq :: What4 sym
-> SInteger (What4 sym)
-> SInteger (What4 sym)
-> SEval (What4 sym) (SBit (What4 sym))
intEq What4 sym
sym SInteger (What4 sym)
x SInteger (What4 sym)
y = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
W4.intEq (forall sym. What4 sym -> sym
w4 What4 sym
sym) SInteger (What4 sym)
x SInteger (What4 sym)
y
  intLessThan :: What4 sym
-> SInteger (What4 sym)
-> SInteger (What4 sym)
-> SEval (What4 sym) (SBit (What4 sym))
intLessThan What4 sym
sym SInteger (What4 sym)
x SInteger (What4 sym)
y = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
W4.intLt (forall sym. What4 sym -> sym
w4 What4 sym
sym) SInteger (What4 sym)
x SInteger (What4 sym)
y
  intGreaterThan :: What4 sym
-> SInteger (What4 sym)
-> SInteger (What4 sym)
-> SEval (What4 sym) (SBit (What4 sym))
intGreaterThan What4 sym
sym SInteger (What4 sym)
x SInteger (What4 sym)
y = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
W4.intLt (forall sym. What4 sym -> sym
w4 What4 sym
sym) SInteger (What4 sym)
y SInteger (What4 sym)
x

  -- NB, we don't do reduction here on symbolic values
  intToZn :: What4 sym
-> Integer
-> SInteger (What4 sym)
-> SEval (What4 sym) (SInteger (What4 sym))
intToZn What4 sym
sym Integer
m SInteger (What4 sym)
x
    | Just Integer
xi <- forall (e :: BaseType -> *).
IsExpr e =>
e BaseIntegerType -> Maybe Integer
W4.asInteger SInteger (What4 sym)
x
    = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
W4.intLit (forall sym. What4 sym -> sym
w4 What4 sym
sym) (Integer
xi forall a. Integral a => a -> a -> a
`mod` Integer
m)

    | Bool
otherwise
    = forall (f :: * -> *) a. Applicative f => a -> f a
pure SInteger (What4 sym)
x

  znToInt :: What4 sym
-> Integer
-> SInteger (What4 sym)
-> SEval (What4 sym) (SInteger (What4 sym))
znToInt What4 sym
_ Integer
0 SInteger (What4 sym)
_ = forall a. String -> [String] -> a
evalPanic String
"znToInt" [String
"0 modulus not allowed"]
  znToInt What4 sym
sym Integer
m SInteger (What4 sym)
x = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
W4.intMod (forall sym. What4 sym -> sym
w4 What4 sym
sym) SInteger (What4 sym)
x forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
W4.intLit (forall sym. What4 sym -> sym
w4 What4 sym
sym) Integer
m)

  znEq :: What4 sym
-> Integer
-> SInteger (What4 sym)
-> SInteger (What4 sym)
-> SEval (What4 sym) (SBit (What4 sym))
znEq What4 sym
_ Integer
0 SInteger (What4 sym)
_ SInteger (What4 sym)
_ = forall a. String -> [String] -> a
evalPanic String
"znEq" [String
"0 modulus not allowed"]
  znEq What4 sym
sym Integer
m SInteger (What4 sym)
x SInteger (What4 sym)
y = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$
     do SymExpr sym BaseIntegerType
diff <- forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
W4.intSub (forall sym. What4 sym -> sym
w4 What4 sym
sym) SInteger (What4 sym)
x SInteger (What4 sym)
y
        forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> Nat -> IO (Pred sym)
W4.intDivisible (forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym BaseIntegerType
diff (forall a. Num a => Integer -> a
fromInteger Integer
m)

  znPlus :: What4 sym
-> Integer
-> SInteger (What4 sym)
-> SInteger (What4 sym)
-> SEval (What4 sym) (SInteger (What4 sym))
znPlus   What4 sym
sym Integer
m SInteger (What4 sym)
x SInteger (What4 sym)
y = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym.
IsSymExprBuilder sym =>
sym
-> Integer
-> SymInteger sym
-> SymInteger sym
-> IO (SymInteger sym)
sModAdd (forall sym. What4 sym -> sym
w4 What4 sym
sym) Integer
m SInteger (What4 sym)
x SInteger (What4 sym)
y
  znMinus :: What4 sym
-> Integer
-> SInteger (What4 sym)
-> SInteger (What4 sym)
-> SEval (What4 sym) (SInteger (What4 sym))
znMinus  What4 sym
sym Integer
m SInteger (What4 sym)
x SInteger (What4 sym)
y = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym.
IsSymExprBuilder sym =>
sym
-> Integer
-> SymInteger sym
-> SymInteger sym
-> IO (SymInteger sym)
sModSub (forall sym. What4 sym -> sym
w4 What4 sym
sym) Integer
m SInteger (What4 sym)
x SInteger (What4 sym)
y
  znMult :: What4 sym
-> Integer
-> SInteger (What4 sym)
-> SInteger (What4 sym)
-> SEval (What4 sym) (SInteger (What4 sym))
znMult   What4 sym
sym Integer
m SInteger (What4 sym)
x SInteger (What4 sym)
y = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym.
IsSymExprBuilder sym =>
sym
-> Integer
-> SymInteger sym
-> SymInteger sym
-> IO (SymInteger sym)
sModMult (forall sym. What4 sym -> sym
w4 What4 sym
sym) Integer
m SInteger (What4 sym)
x SInteger (What4 sym)
y
  znNegate :: What4 sym
-> Integer
-> SInteger (What4 sym)
-> SEval (What4 sym) (SInteger (What4 sym))
znNegate What4 sym
sym Integer
m SInteger (What4 sym)
x   = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym.
IsSymExprBuilder sym =>
sym -> Integer -> SymInteger sym -> IO (SymInteger sym)
sModNegate (forall sym. What4 sym -> sym
w4 What4 sym
sym) Integer
m SInteger (What4 sym)
x
  znRecip :: What4 sym
-> Integer
-> SInteger (What4 sym)
-> SEval (What4 sym) (SInteger (What4 sym))
znRecip = forall sym.
IsSymExprBuilder sym =>
What4 sym
-> Integer -> SymInteger sym -> W4Eval sym (SymInteger sym)
sModRecip

  --------------------------------------------------------------

  fpLit :: What4 sym
-> Integer
-> Integer
-> Rational
-> SEval (What4 sym) (SFloat (What4 sym))
fpLit What4 sym
sym Integer
e Integer
p Rational
r = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> Integer -> Integer -> Rational -> IO (SFloat sym)
FP.fpFromRationalLit (forall sym. What4 sym -> sym
w4 What4 sym
sym) Integer
e Integer
p Rational
r
  fpAsLit :: What4 sym -> SFloat (What4 sym) -> Maybe BF
fpAsLit What4 sym
_ SFloat (What4 sym)
f = Integer -> Integer -> BigFloat -> BF
BF Integer
e Integer
p forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym. SFloat sym -> Maybe BigFloat
FP.fpAsLit SFloat (What4 sym)
f
    where (Integer
e,Integer
p) = forall sym. SFloat sym -> (Integer, Integer)
FP.fpSize SFloat (What4 sym)
f

  fpExactLit :: What4 sym -> BF -> SEval (What4 sym) (SFloat (What4 sym))
fpExactLit What4 sym
sym BF{ bfExpWidth :: BF -> Integer
bfExpWidth = Integer
e, bfPrecWidth :: BF -> Integer
bfPrecWidth = Integer
p, bfValue :: BF -> BigFloat
bfValue = BigFloat
bf } =
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym.
IsExprBuilder sym =>
sym -> Integer -> Integer -> SWord sym -> IO (SFloat sym)
FP.fpFromBinary (forall sym. What4 sym -> sym
w4 What4 sym
sym) Integer
e Integer
p forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> Integer -> Integer -> IO (SWord sym)
SW.bvLit (forall sym. What4 sym -> sym
w4 What4 sym
sym) (Integer
eforall a. Num a => a -> a -> a
+Integer
p) (Integer -> Integer -> BigFloat -> Integer
floatToBits Integer
e Integer
p BigFloat
bf))

  fpNaN :: What4 sym
-> Integer -> Integer -> SEval (What4 sym) (SFloat (What4 sym))
fpNaN What4 sym
sym Integer
e Integer
p = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym.
IsExprBuilder sym =>
sym -> Integer -> Integer -> IO (SFloat sym)
FP.fpNaN (forall sym. What4 sym -> sym
w4 What4 sym
sym) Integer
e Integer
p)
  fpPosInf :: What4 sym
-> Integer -> Integer -> SEval (What4 sym) (SFloat (What4 sym))
fpPosInf What4 sym
sym Integer
e Integer
p = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym.
IsExprBuilder sym =>
sym -> Integer -> Integer -> IO (SFloat sym)
FP.fpPosInf (forall sym. What4 sym -> sym
w4 What4 sym
sym) Integer
e Integer
p)

  fpToBits :: What4 sym
-> SFloat (What4 sym) -> SEval (What4 sym) (SWord (What4 sym))
fpToBits What4 sym
sym SFloat (What4 sym)
f = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym.
IsExprBuilder sym =>
sym -> SFloat sym -> IO (SWord sym)
FP.fpToBinary (forall sym. What4 sym -> sym
w4 What4 sym
sym) SFloat (What4 sym)
f)
  fpFromBits :: What4 sym
-> Integer
-> Integer
-> SWord (What4 sym)
-> SEval (What4 sym) (SFloat (What4 sym))
fpFromBits What4 sym
sym Integer
e Integer
p SWord (What4 sym)
w = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym.
IsExprBuilder sym =>
sym -> Integer -> Integer -> SWord sym -> IO (SFloat sym)
FP.fpFromBinary (forall sym. What4 sym -> sym
w4 What4 sym
sym) Integer
e Integer
p SWord (What4 sym)
w)

  fpEq :: What4 sym
-> SFloat (What4 sym)
-> SFloat (What4 sym)
-> SEval (What4 sym) (SBit (What4 sym))
fpEq          What4 sym
sym SFloat (What4 sym)
x SFloat (What4 sym)
y = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym. IsExprBuilder sym => SFloatRel sym
FP.fpEqIEEE (forall sym. What4 sym -> sym
w4 What4 sym
sym) SFloat (What4 sym)
x SFloat (What4 sym)
y
  fpLessThan :: What4 sym
-> SFloat (What4 sym)
-> SFloat (What4 sym)
-> SEval (What4 sym) (SBit (What4 sym))
fpLessThan    What4 sym
sym SFloat (What4 sym)
x SFloat (What4 sym)
y = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym. IsExprBuilder sym => SFloatRel sym
FP.fpLtIEEE (forall sym. What4 sym -> sym
w4 What4 sym
sym) SFloat (What4 sym)
x SFloat (What4 sym)
y
  fpGreaterThan :: What4 sym
-> SFloat (What4 sym)
-> SFloat (What4 sym)
-> SEval (What4 sym) (SBit (What4 sym))
fpGreaterThan What4 sym
sym SFloat (What4 sym)
x SFloat (What4 sym)
y = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym. IsExprBuilder sym => SFloatRel sym
FP.fpGtIEEE (forall sym. What4 sym -> sym
w4 What4 sym
sym) SFloat (What4 sym)
x SFloat (What4 sym)
y
  fpLogicalEq :: What4 sym
-> SFloat (What4 sym)
-> SFloat (What4 sym)
-> SEval (What4 sym) (SBit (What4 sym))
fpLogicalEq   What4 sym
sym SFloat (What4 sym)
x SFloat (What4 sym)
y = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym. IsExprBuilder sym => SFloatRel sym
FP.fpEq (forall sym. What4 sym -> sym
w4 What4 sym
sym) SFloat (What4 sym)
x SFloat (What4 sym)
y

  fpPlus :: FPArith2 (What4 sym)
fpPlus  = forall sym.
IsSymExprBuilder sym =>
SFloatBinArith sym
-> What4 sym
-> SWord (What4 sym)
-> SFloat (What4 sym)
-> SFloat (What4 sym)
-> SEval (What4 sym) (SFloat (What4 sym))
fpBinArith forall sym. IsExprBuilder sym => SFloatBinArith sym
FP.fpAdd
  fpMinus :: FPArith2 (What4 sym)
fpMinus = forall sym.
IsSymExprBuilder sym =>
SFloatBinArith sym
-> What4 sym
-> SWord (What4 sym)
-> SFloat (What4 sym)
-> SFloat (What4 sym)
-> SEval (What4 sym) (SFloat (What4 sym))
fpBinArith forall sym. IsExprBuilder sym => SFloatBinArith sym
FP.fpSub
  fpMult :: FPArith2 (What4 sym)
fpMult  = forall sym.
IsSymExprBuilder sym =>
SFloatBinArith sym
-> What4 sym
-> SWord (What4 sym)
-> SFloat (What4 sym)
-> SFloat (What4 sym)
-> SEval (What4 sym) (SFloat (What4 sym))
fpBinArith forall sym. IsExprBuilder sym => SFloatBinArith sym
FP.fpMul
  fpDiv :: FPArith2 (What4 sym)
fpDiv   = forall sym.
IsSymExprBuilder sym =>
SFloatBinArith sym
-> What4 sym
-> SWord (What4 sym)
-> SFloat (What4 sym)
-> SFloat (What4 sym)
-> SEval (What4 sym) (SFloat (What4 sym))
fpBinArith forall sym. IsExprBuilder sym => SFloatBinArith sym
FP.fpDiv

  fpNeg :: What4 sym
-> SFloat (What4 sym) -> SEval (What4 sym) (SFloat (What4 sym))
fpNeg What4 sym
sym SFloat (What4 sym)
x = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> SFloat sym -> IO (SFloat sym)
FP.fpNeg (forall sym. What4 sym -> sym
w4 What4 sym
sym) SFloat (What4 sym)
x
  fpAbs :: What4 sym
-> SFloat (What4 sym) -> SEval (What4 sym) (SFloat (What4 sym))
fpAbs What4 sym
sym SFloat (What4 sym)
x = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> SFloat sym -> IO (SFloat sym)
FP.fpAbs (forall sym. What4 sym -> sym
w4 What4 sym
sym) SFloat (What4 sym)
x
  fpSqrt :: What4 sym
-> SWord (What4 sym)
-> SFloat (What4 sym)
-> SEval (What4 sym) (SFloat (What4 sym))
fpSqrt What4 sym
sym SWord (What4 sym)
r SFloat (What4 sym)
x =
    do RoundingMode
rm <- forall sym.
IsSymExprBuilder sym =>
What4 sym -> SWord (What4 sym) -> SEval (What4 sym) RoundingMode
fpRoundingMode What4 sym
sym SWord (What4 sym)
r
       forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> RoundingMode -> SFloat sym -> IO (SFloat sym)
FP.fpSqrt (forall sym. What4 sym -> sym
w4 What4 sym
sym) RoundingMode
rm SFloat (What4 sym)
x

  fpFMA :: What4 sym
-> SWord (What4 sym)
-> SFloat (What4 sym)
-> SFloat (What4 sym)
-> SFloat (What4 sym)
-> SEval (What4 sym) (SFloat (What4 sym))
fpFMA What4 sym
sym SWord (What4 sym)
r SFloat (What4 sym)
x SFloat (What4 sym)
y SFloat (What4 sym)
z =
    do RoundingMode
rm <- forall sym.
IsSymExprBuilder sym =>
What4 sym -> SWord (What4 sym) -> SEval (What4 sym) RoundingMode
fpRoundingMode What4 sym
sym SWord (What4 sym)
r
       forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym
-> RoundingMode
-> SFloat sym
-> SFloat sym
-> SFloat sym
-> IO (SFloat sym)
FP.fpFMA (forall sym. What4 sym -> sym
w4 What4 sym
sym) RoundingMode
rm SFloat (What4 sym)
x SFloat (What4 sym)
y SFloat (What4 sym)
z

  fpIsZero :: What4 sym
-> SFloat (What4 sym) -> SEval (What4 sym) (SBit (What4 sym))
fpIsZero What4 sym
sym SFloat (What4 sym)
x = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym. IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
FP.fpIsZero (forall sym. What4 sym -> sym
w4 What4 sym
sym) SFloat (What4 sym)
x
  fpIsNeg :: What4 sym
-> SFloat (What4 sym) -> SEval (What4 sym) (SBit (What4 sym))
fpIsNeg What4 sym
sym SFloat (What4 sym)
x = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym. IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
FP.fpIsNeg (forall sym. What4 sym -> sym
w4 What4 sym
sym) SFloat (What4 sym)
x
  fpIsNaN :: What4 sym
-> SFloat (What4 sym) -> SEval (What4 sym) (SBit (What4 sym))
fpIsNaN What4 sym
sym SFloat (What4 sym)
x = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym. IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
FP.fpIsNaN (forall sym. What4 sym -> sym
w4 What4 sym
sym) SFloat (What4 sym)
x
  fpIsInf :: What4 sym
-> SFloat (What4 sym) -> SEval (What4 sym) (SBit (What4 sym))
fpIsInf What4 sym
sym SFloat (What4 sym)
x = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym. IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
FP.fpIsInf (forall sym. What4 sym -> sym
w4 What4 sym
sym) SFloat (What4 sym)
x
  fpIsNorm :: What4 sym
-> SFloat (What4 sym) -> SEval (What4 sym) (SBit (What4 sym))
fpIsNorm What4 sym
sym SFloat (What4 sym)
x = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym. IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
FP.fpIsNorm (forall sym. What4 sym -> sym
w4 What4 sym
sym) SFloat (What4 sym)
x
  fpIsSubnorm :: What4 sym
-> SFloat (What4 sym) -> SEval (What4 sym) (SBit (What4 sym))
fpIsSubnorm What4 sym
sym SFloat (What4 sym)
x = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym. IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
FP.fpIsSubnorm (forall sym. What4 sym -> sym
w4 What4 sym
sym) SFloat (What4 sym)
x

  fpFromInteger :: What4 sym
-> Integer
-> Integer
-> SWord (What4 sym)
-> SInteger (What4 sym)
-> SEval (What4 sym) (SFloat (What4 sym))
fpFromInteger What4 sym
sym Integer
e Integer
p SWord (What4 sym)
r SInteger (What4 sym)
x =
    do RoundingMode
rm <- forall sym.
IsSymExprBuilder sym =>
What4 sym -> SWord (What4 sym) -> SEval (What4 sym) RoundingMode
fpRoundingMode What4 sym
sym SWord (What4 sym)
r
       forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym
-> Integer
-> Integer
-> RoundingMode
-> SymInteger sym
-> IO (SFloat sym)
FP.fpFromInteger (forall sym. What4 sym -> sym
w4 What4 sym
sym) Integer
e Integer
p RoundingMode
rm SInteger (What4 sym)
x

  fpToInteger :: What4 sym
-> String
-> SWord (What4 sym)
-> SFloat (What4 sym)
-> SEval (What4 sym) (SInteger (What4 sym))
fpToInteger = forall sy sym.
(IsSymExprBuilder sy, sym ~ What4 sy) =>
sym
-> String -> SWord sym -> SFloat sym -> SEval sym (SInteger sym)
fpCvtToInteger

  fpFromRational :: What4 sym
-> Integer
-> Integer
-> SWord (What4 sym)
-> SRational (What4 sym)
-> SEval (What4 sym) (SFloat (What4 sym))
fpFromRational = forall sy sym.
(IsSymExprBuilder sy, sym ~ What4 sy) =>
sym
-> Integer
-> Integer
-> SWord sym
-> SRational sym
-> SEval sym (SFloat sym)
fpCvtFromRational
  fpToRational :: What4 sym
-> SFloat (What4 sym) -> SEval (What4 sym) (SRational (What4 sym))
fpToRational = forall sy sym.
(IsSymExprBuilder sy, sym ~ What4 sy) =>
sym -> SFloat sym -> SEval sym (SRational sym)
fpCvtToRational

sModAdd :: W4.IsSymExprBuilder sym =>
  sym -> Integer -> W4.SymInteger sym -> W4.SymInteger sym -> IO (W4.SymInteger sym)
sModAdd :: forall sym.
IsSymExprBuilder sym =>
sym
-> Integer
-> SymInteger sym
-> SymInteger sym
-> IO (SymInteger sym)
sModAdd sym
_sym Integer
0 SymInteger sym
_ SymInteger sym
_ = forall a. String -> [String] -> a
evalPanic String
"sModAdd" [String
"0 modulus not allowed"]
sModAdd sym
sym Integer
m SymInteger sym
x SymInteger sym
y
  | Just Integer
xi <- forall (e :: BaseType -> *).
IsExpr e =>
e BaseIntegerType -> Maybe Integer
W4.asInteger SymInteger sym
x
  , Just Integer
yi <- forall (e :: BaseType -> *).
IsExpr e =>
e BaseIntegerType -> Maybe Integer
W4.asInteger SymInteger sym
y
  = forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
W4.intLit sym
sym ((Integer
xiforall a. Num a => a -> a -> a
+Integer
yi) forall a. Integral a => a -> a -> a
`mod` Integer
m)

  | Bool
otherwise
  = forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
W4.intAdd sym
sym SymInteger sym
x SymInteger sym
y

sModSub :: W4.IsSymExprBuilder sym =>
  sym -> Integer -> W4.SymInteger sym -> W4.SymInteger sym -> IO (W4.SymInteger sym)
sModSub :: forall sym.
IsSymExprBuilder sym =>
sym
-> Integer
-> SymInteger sym
-> SymInteger sym
-> IO (SymInteger sym)
sModSub sym
_sym Integer
0 SymInteger sym
_ SymInteger sym
_ = forall a. String -> [String] -> a
evalPanic String
"sModSub" [String
"0 modulus not allowed"]
sModSub sym
sym Integer
m SymInteger sym
x SymInteger sym
y
  | Just Integer
xi <- forall (e :: BaseType -> *).
IsExpr e =>
e BaseIntegerType -> Maybe Integer
W4.asInteger SymInteger sym
x
  , Just Integer
yi <- forall (e :: BaseType -> *).
IsExpr e =>
e BaseIntegerType -> Maybe Integer
W4.asInteger SymInteger sym
y
  = forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
W4.intLit sym
sym ((Integer
xiforall a. Num a => a -> a -> a
-Integer
yi) forall a. Integral a => a -> a -> a
`mod` Integer
m)

  | Bool
otherwise
  = forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
W4.intSub sym
sym SymInteger sym
x SymInteger sym
y


sModMult :: W4.IsSymExprBuilder sym =>
  sym -> Integer -> W4.SymInteger sym -> W4.SymInteger sym -> IO (W4.SymInteger sym)
sModMult :: forall sym.
IsSymExprBuilder sym =>
sym
-> Integer
-> SymInteger sym
-> SymInteger sym
-> IO (SymInteger sym)
sModMult sym
_sym Integer
0 SymInteger sym
_ SymInteger sym
_ = forall a. String -> [String] -> a
evalPanic String
"sModMult" [String
"0 modulus not allowed"]
sModMult sym
sym Integer
m SymInteger sym
x SymInteger sym
y
  | Just Integer
xi <- forall (e :: BaseType -> *).
IsExpr e =>
e BaseIntegerType -> Maybe Integer
W4.asInteger SymInteger sym
x
  , Just Integer
yi <- forall (e :: BaseType -> *).
IsExpr e =>
e BaseIntegerType -> Maybe Integer
W4.asInteger SymInteger sym
y
  = forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
W4.intLit sym
sym ((Integer
xiforall a. Num a => a -> a -> a
*Integer
yi) forall a. Integral a => a -> a -> a
`mod` Integer
m)

  | Bool
otherwise
  = forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
W4.intMul sym
sym SymInteger sym
x SymInteger sym
y

sModNegate :: W4.IsSymExprBuilder sym =>
  sym -> Integer -> W4.SymInteger sym -> IO (W4.SymInteger sym)
sModNegate :: forall sym.
IsSymExprBuilder sym =>
sym -> Integer -> SymInteger sym -> IO (SymInteger sym)
sModNegate sym
_sym Integer
0 SymInteger sym
_ = forall a. String -> [String] -> a
evalPanic String
"sModMult" [String
"0 modulus not allowed"]
sModNegate sym
sym Integer
m SymInteger sym
x
  | Just Integer
xi <- forall (e :: BaseType -> *).
IsExpr e =>
e BaseIntegerType -> Maybe Integer
W4.asInteger SymInteger sym
x
  = forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
W4.intLit sym
sym ((forall a. Num a => a -> a
negate Integer
xi) forall a. Integral a => a -> a -> a
`mod` Integer
m)

  | Bool
otherwise
  = forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymInteger sym)
W4.intNeg sym
sym SymInteger sym
x


-- | Try successive powers of 2 to find the first that dominates the input.
--   We could perhaps reduce to using CLZ instead...
sLg2 :: W4.IsSymExprBuilder sym => sym -> SW.SWord sym -> SEval (What4 sym) (SW.SWord sym)
sLg2 :: forall sym.
IsSymExprBuilder sym =>
sym -> SWord sym -> SEval (What4 sym) (SWord sym)
sLg2 sym
sym SWord sym
x = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ Int -> IO (SWord sym)
go Int
0
  where
  w :: Integer
w = forall sym. SWord sym -> Integer
SW.bvWidth SWord sym
x
  lit :: Int -> IO (SWord sym)
lit Int
n = forall sym.
IsExprBuilder sym =>
sym -> Integer -> Integer -> IO (SWord sym)
SW.bvLit sym
sym Integer
w (forall a. Integral a => a -> Integer
toInteger Int
n)

  go :: Int -> IO (SWord sym)
go Int
i | forall a. Integral a => a -> Integer
toInteger Int
i forall a. Ord a => a -> a -> Bool
< Integer
w =
       do SymExpr sym BaseBoolType
p <- PredBin
SW.bvule sym
sym SWord sym
x forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Int -> IO (SWord sym)
lit (forall a. Bits a => Int -> a
bit Int
i)
          forall (p :: BaseType -> *) (m :: * -> *) a.
(IsExpr p, Monad m) =>
(p BaseBoolType -> a -> a -> m a)
-> p BaseBoolType -> m a -> m a -> m a
lazyIte (forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> SWord sym -> SWord sym -> IO (SWord sym)
SW.bvIte sym
sym) SymExpr sym BaseBoolType
p (Int -> IO (SWord sym)
lit Int
i) (Int -> IO (SWord sym)
go (Int
iforall a. Num a => a -> a -> a
+Int
1))

  -- base case, should only happen when i = w
  go Int
i = Int -> IO (SWord sym)
lit Int
i



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

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

lazyIte ::
  (W4.IsExpr p, Monad m) =>
  (p W4.BaseBoolType -> a -> a -> m a) ->
  p W4.BaseBoolType ->
  m a ->
  m a ->
  m a
lazyIte :: forall (p :: BaseType -> *) (m :: * -> *) a.
(IsExpr p, Monad m) =>
(p BaseBoolType -> a -> a -> m a)
-> p BaseBoolType -> m a -> m a -> m a
lazyIte p BaseBoolType -> a -> a -> m a
f p BaseBoolType
c m a
mx m a
my
  | Just Bool
b <- forall (e :: BaseType -> *).
IsExpr e =>
e BaseBoolType -> Maybe Bool
W4.asConstantPred p BaseBoolType
c = if Bool
b then m a
mx else m a
my
  | Bool
otherwise =
      do a
x <- m a
mx
         a
y <- m a
my
         p BaseBoolType -> a -> a -> m a
f p BaseBoolType
c a
x a
y

w4bvShl  :: W4.IsSymExprBuilder sym => sym -> SW.SWord sym -> SW.SWord sym -> W4Eval sym (SW.SWord sym)
w4bvShl :: forall sym.
IsSymExprBuilder sym =>
sym -> SWord sym -> SWord sym -> W4Eval sym (SWord sym)
w4bvShl sym
sym SWord sym
x SWord sym
y = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> SWord sym -> IO (SWord sym)
SW.bvShl sym
sym SWord sym
x SWord sym
y

w4bvLshr  :: W4.IsSymExprBuilder sym => sym -> SW.SWord sym -> SW.SWord sym -> W4Eval sym (SW.SWord sym)
w4bvLshr :: forall sym.
IsSymExprBuilder sym =>
sym -> SWord sym -> SWord sym -> W4Eval sym (SWord sym)
w4bvLshr sym
sym SWord sym
x SWord sym
y = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> SWord sym -> IO (SWord sym)
SW.bvLshr sym
sym SWord sym
x SWord sym
y

w4bvAshr :: W4.IsSymExprBuilder sym => sym -> SW.SWord sym -> SW.SWord sym -> W4Eval sym (SW.SWord sym)
w4bvAshr :: forall sym.
IsSymExprBuilder sym =>
sym -> SWord sym -> SWord sym -> W4Eval sym (SWord sym)
w4bvAshr sym
sym SWord sym
x SWord sym
y = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> SWord sym -> IO (SWord sym)
SW.bvAshr sym
sym SWord sym
x SWord sym
y

w4bvRol  :: W4.IsSymExprBuilder sym => sym -> SW.SWord sym -> SW.SWord sym -> W4Eval sym (SW.SWord sym)
w4bvRol :: forall sym.
IsSymExprBuilder sym =>
sym -> SWord sym -> SWord sym -> W4Eval sym (SWord sym)
w4bvRol sym
sym SWord sym
x SWord sym
y = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> SWord sym -> IO (SWord sym)
SW.bvRol sym
sym SWord sym
x SWord sym
y

w4bvRor  :: W4.IsSymExprBuilder sym => sym -> SW.SWord sym -> SW.SWord sym -> W4Eval sym (SW.SWord sym)
w4bvRor :: forall sym.
IsSymExprBuilder sym =>
sym -> SWord sym -> SWord sym -> W4Eval sym (SWord sym)
w4bvRor sym
sym SWord sym
x SWord sym
y = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> SWord sym -> IO (SWord sym)
SW.bvRor sym
sym SWord sym
x SWord sym
y



fpRoundingMode ::
  W4.IsSymExprBuilder sym =>
  What4 sym -> SWord (What4 sym) -> SEval (What4 sym) W4.RoundingMode
fpRoundingMode :: forall sym.
IsSymExprBuilder sym =>
What4 sym -> SWord (What4 sym) -> SEval (What4 sym) RoundingMode
fpRoundingMode What4 sym
sym SWord (What4 sym)
v =
  case forall sym.
Backend sym =>
sym -> SWord sym -> Maybe (Integer, Integer)
wordAsLit What4 sym
sym SWord (What4 sym)
v of
    Just (Integer
_w,Integer
i) ->
      case Integer
i of
        Integer
0 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure RoundingMode
W4.RNE
        Integer
1 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure RoundingMode
W4.RNA
        Integer
2 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure RoundingMode
W4.RTP
        Integer
3 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure RoundingMode
W4.RTN
        Integer
4 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure RoundingMode
W4.RTZ
        Integer
x -> forall sym a. Backend sym => sym -> EvalError -> SEval sym a
raiseError What4 sym
sym (Integer -> EvalError
BadRoundingMode Integer
x)
    Maybe (Integer, Integer)
_ -> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall e a. Exception e => e -> IO a
X.throwIO forall a b. (a -> b) -> a -> b
$ String -> Unsupported
UnsupportedSymbolicOp String
"rounding mode"

fpBinArith ::
  W4.IsSymExprBuilder sym =>
  FP.SFloatBinArith sym ->
  What4 sym ->
  SWord (What4 sym) ->
  SFloat (What4 sym) ->
  SFloat (What4 sym) ->
  SEval (What4 sym) (SFloat (What4 sym))
fpBinArith :: forall sym.
IsSymExprBuilder sym =>
SFloatBinArith sym
-> What4 sym
-> SWord (What4 sym)
-> SFloat (What4 sym)
-> SFloat (What4 sym)
-> SEval (What4 sym) (SFloat (What4 sym))
fpBinArith SFloatBinArith sym
fun = \What4 sym
sym SWord (What4 sym)
r SFloat (What4 sym)
x SFloat (What4 sym)
y ->
  do RoundingMode
m <- forall sym.
IsSymExprBuilder sym =>
What4 sym -> SWord (What4 sym) -> SEval (What4 sym) RoundingMode
fpRoundingMode What4 sym
sym SWord (What4 sym)
r
     forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (SFloatBinArith sym
fun (forall sym. What4 sym -> sym
w4 What4 sym
sym) RoundingMode
m SFloat (What4 sym)
x SFloat (What4 sym)
y)


fpCvtToInteger ::
  (W4.IsSymExprBuilder sy, sym ~ What4 sy) =>
  sym -> String -> SWord sym -> SFloat sym -> SEval sym (SInteger sym)
fpCvtToInteger :: forall sy sym.
(IsSymExprBuilder sy, sym ~ What4 sy) =>
sym
-> String -> SWord sym -> SFloat sym -> SEval sym (SInteger sym)
fpCvtToInteger sym
sym String
fun SWord sym
r SFloat sym
x =
  do SymExpr sy BaseBoolType
grd <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO
              do SymExpr sy BaseBoolType
bad1 <- forall sym. IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
FP.fpIsInf (forall sym. What4 sym -> sym
w4 sym
sym) SFloat sym
x
                 SymExpr sy BaseBoolType
bad2 <- forall sym. IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
FP.fpIsNaN (forall sym. What4 sym -> sym
w4 sym
sym) SFloat sym
x
                 forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
W4.notPred (forall sym. What4 sym -> sym
w4 sym
sym) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
W4.orPred (forall sym. What4 sym -> sym
w4 sym
sym) SymExpr sy BaseBoolType
bad1 SymExpr sy BaseBoolType
bad2
     forall sym.
Backend sym =>
sym -> SBit sym -> EvalError -> SEval sym ()
assertSideCondition sym
sym SymExpr sy BaseBoolType
grd (String -> EvalError
BadValue String
fun)
     RoundingMode
rnd  <- forall sym.
IsSymExprBuilder sym =>
What4 sym -> SWord (What4 sym) -> SEval (What4 sym) RoundingMode
fpRoundingMode sym
sym SWord sym
r
     forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO
       do SymExpr sy BaseRealType
y <- forall sym.
IsExprBuilder sym =>
sym -> SFloat sym -> IO (SymReal sym)
FP.fpToReal (forall sym. What4 sym -> sym
w4 sym
sym) SFloat sym
x
          case RoundingMode
rnd of
            RoundingMode
W4.RNE -> forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymInteger sym)
W4.realRoundEven (forall sym. What4 sym -> sym
w4 sym
sym) SymExpr sy BaseRealType
y
            RoundingMode
W4.RNA -> forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymInteger sym)
W4.realRound (forall sym. What4 sym -> sym
w4 sym
sym) SymExpr sy BaseRealType
y
            RoundingMode
W4.RTP -> forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymInteger sym)
W4.realCeil (forall sym. What4 sym -> sym
w4 sym
sym) SymExpr sy BaseRealType
y
            RoundingMode
W4.RTN -> forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymInteger sym)
W4.realFloor (forall sym. What4 sym -> sym
w4 sym
sym) SymExpr sy BaseRealType
y
            RoundingMode
W4.RTZ -> forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymInteger sym)
W4.realTrunc (forall sym. What4 sym -> sym
w4 sym
sym) SymExpr sy BaseRealType
y


fpCvtToRational ::
  (W4.IsSymExprBuilder sy, sym ~ What4 sy) =>
  sym -> SFloat sym -> SEval sym (SRational sym)
fpCvtToRational :: forall sy sym.
(IsSymExprBuilder sy, sym ~ What4 sy) =>
sym -> SFloat sym -> SEval sym (SRational sym)
fpCvtToRational sym
sym SFloat sym
fp =
  do SymExpr sy BaseBoolType
grd <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO
            do SymExpr sy BaseBoolType
bad1 <- forall sym. IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
FP.fpIsInf (forall sym. What4 sym -> sym
w4 sym
sym) SFloat sym
fp
               SymExpr sy BaseBoolType
bad2 <- forall sym. IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
FP.fpIsNaN (forall sym. What4 sym -> sym
w4 sym
sym) SFloat sym
fp
               forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
W4.notPred (forall sym. What4 sym -> sym
w4 sym
sym) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
W4.orPred (forall sym. What4 sym -> sym
w4 sym
sym) SymExpr sy BaseBoolType
bad1 SymExpr sy BaseBoolType
bad2
     forall sym.
Backend sym =>
sym -> SBit sym -> EvalError -> SEval sym ()
assertSideCondition sym
sym SymExpr sy BaseBoolType
grd (String -> EvalError
BadValue String
"fpToRational")
     (SymExpr sy BaseBoolType
rel,SymExpr sy BaseIntegerType
x,SymExpr sy BaseIntegerType
y) <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym.
IsSymExprBuilder sym =>
sym -> SFloat sym -> IO (Pred sym, SymInteger sym, SymInteger sym)
FP.fpToRational (forall sym. What4 sym -> sym
w4 sym
sym) SFloat sym
fp)
     forall sym.
IsSymExprBuilder sym =>
What4 sym -> Pred sym -> W4Eval sym ()
addDefEqn sym
sym forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
W4.impliesPred (forall sym. What4 sym -> sym
w4 sym
sym) SymExpr sy BaseBoolType
grd SymExpr sy BaseBoolType
rel)
     forall sym.
Backend sym =>
sym -> SInteger sym -> SInteger sym -> SEval sym (SRational sym)
ratio sym
sym SymExpr sy BaseIntegerType
x SymExpr sy BaseIntegerType
y

fpCvtFromRational ::
  (W4.IsSymExprBuilder sy, sym ~ What4 sy) =>
  sym -> Integer -> Integer -> SWord sym ->
  SRational sym -> SEval sym (SFloat sym)
fpCvtFromRational :: forall sy sym.
(IsSymExprBuilder sy, sym ~ What4 sy) =>
sym
-> Integer
-> Integer
-> SWord sym
-> SRational sym
-> SEval sym (SFloat sym)
fpCvtFromRational sym
sym Integer
e Integer
p SWord sym
r SRational sym
rat =
  do RoundingMode
rnd <- forall sym.
IsSymExprBuilder sym =>
What4 sym -> SWord (What4 sym) -> SEval (What4 sym) RoundingMode
fpRoundingMode sym
sym SWord sym
r
     forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym.
IsExprBuilder sym =>
sym
-> Integer
-> Integer
-> RoundingMode
-> SymInteger sym
-> SymInteger sym
-> IO (SFloat sym)
FP.fpFromRational (forall sym. What4 sym -> sym
w4 sym
sym) Integer
e Integer
p RoundingMode
rnd (forall sym. SRational sym -> SInteger sym
sNum SRational sym
rat) (forall sym. SRational sym -> SInteger sym
sDenom SRational sym
rat))

-- 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 ::
  W4.IsSymExprBuilder sym =>
  What4 sym ->
  Integer ->
  W4.SymInteger sym ->
  W4Eval sym (W4.SymInteger sym)
sModRecip :: forall sym.
IsSymExprBuilder sym =>
What4 sym
-> Integer -> SymInteger sym -> W4Eval sym (SymInteger sym)
sModRecip What4 sym
_sym Integer
0 SymInteger sym
_ = forall a. HasCallStack => String -> [String] -> a
panic String
"sModRecip" [String
"0 modulus not allowed"]
sModRecip What4 sym
sym Integer
m SymInteger sym
x
  -- If the input is concrete, evaluate the answer
  | Just Integer
xi <- forall (e :: BaseType -> *).
IsExpr e =>
e BaseIntegerType -> Maybe Integer
W4.asInteger SymInteger sym
x
  = case Integer -> Integer -> Maybe Integer
Integer.integerRecipMod Integer
xi Integer
m of
      Just Integer
r  -> forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit What4 sym
sym Integer
r
      Maybe Integer
Nothing -> forall sym a. Backend sym => sym -> EvalError -> SEval sym a
raiseError What4 sym
sym EvalError
DivideByZero

  -- 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 SymExpr sym BaseBoolType
divZero <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> Nat -> IO (Pred sym)
W4.intDivisible (forall sym. What4 sym -> sym
w4 What4 sym
sym) SymInteger sym
x (forall a. Num a => Integer -> a
fromInteger Integer
m))
       SymExpr sym BaseBoolType
ok <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
W4.notPred (forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym BaseBoolType
divZero)
       forall sym.
Backend sym =>
sym -> SBit sym -> EvalError -> SEval sym ()
assertSideCondition What4 sym
sym SymExpr sym BaseBoolType
ok EvalError
DivideByZero

       SymInteger sym
z <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym.
IsSymExprBuilder sym =>
sym
-> SolverSymbol
-> Maybe Integer
-> Maybe Integer
-> IO (SymInteger sym)
W4.freshBoundedInt (forall sym. What4 sym -> sym
w4 What4 sym
sym) SolverSymbol
W4.emptySymbol (forall a. a -> Maybe a
Just Integer
1) (forall a. a -> Maybe a
Just (Integer
mforall a. Num a => a -> a -> a
-Integer
1)))
       SymInteger sym
xz <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
W4.intMul (forall sym. What4 sym -> sym
w4 What4 sym
sym) SymInteger sym
x SymInteger sym
z)
       SymExpr sym BaseBoolType
rel <- forall sym.
Backend sym =>
sym
-> Integer -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
znEq What4 sym
sym Integer
m SymInteger sym
xz forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
W4.intLit (forall sym. What4 sym -> sym
w4 What4 sym
sym) Integer
1)
       forall sym.
IsSymExprBuilder sym =>
What4 sym -> Pred sym -> W4Eval sym ()
addDefEqn What4 sym
sym forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
W4.orPred (forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym BaseBoolType
divZero SymExpr sym BaseBoolType
rel)

       forall (m :: * -> *) a. Monad m => a -> m a
return SymInteger sym
z