-- |
-- 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 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.Integer.GMP.Internals as Integer

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

import qualified Cryptol.Backend.What4.SFloat as FP

import Cryptol.Backend
import Cryptol.Backend.Concrete( BV(..), ppBV )
import Cryptol.Backend.FloatHelpers
import Cryptol.Backend.Monad
   ( Eval(..), EvalError(..), Unsupported(..)
   , delayFill, blackhole, evalSpark
   )
import Cryptol.Utils.Panic
import Cryptol.Utils.PP


data What4 sym =
  What4
  { What4 sym -> sym
w4  :: sym
  , What4 sym -> MVar (Pred sym)
w4defs :: MVar (W4.Pred sym)
  , What4 sym -> MVar (What4FunCache sym)
w4funs :: MVar (What4FunCache 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 { 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 { W4Conn sym a -> sym -> Eval a
evalConn :: sym -> Eval a }

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

  | W4Result !(W4.Pred sym) !a
    -- ^ safety predicate and result: the result only makes sense when
    -- the predicate holds.


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

w4Eval :: W4Eval sym a -> sym -> Eval (W4Result sym a)
w4Eval :: 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 :: Eval (W4Result sym a) -> W4Eval sym a
w4Thunk Eval (W4Result sym a)
m = W4Conn sym (W4Result sym a) -> W4Eval sym a
forall sym a. W4Conn sym (W4Result sym a) -> W4Eval sym a
W4Eval ((sym -> Eval (W4Result sym a)) -> W4Conn sym (W4Result sym a)
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 :: Eval a -> W4Conn sym a
doEval Eval a
m = (sym -> Eval a) -> W4Conn sym a
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 :: W4Conn sym a -> W4Eval sym a
total W4Conn sym a
m = W4Conn sym (W4Result sym a) -> W4Eval sym a
forall sym a. W4Conn sym (W4Result sym a) -> W4Eval sym a
W4Eval
  do sym
sym <- W4Conn sym sym
forall sym. W4Conn sym sym
getSym
     Pred sym -> a -> W4Result sym a
forall sym a. Pred sym -> a -> W4Result sym a
W4Result (sym -> Bool -> Pred sym
forall sym. IsExprBuilder sym => sym -> Bool -> Pred sym
W4.backendPred sym
sym Bool
True) (a -> W4Result sym a)
-> W4Conn sym a -> W4Conn sym (W4Result sym a)
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 :: (a -> b) -> W4Conn sym a -> W4Conn sym b
fmap = (a -> b) -> W4Conn sym a -> W4Conn sym b
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM

instance W4.IsSymExprBuilder sym => Applicative (W4Conn sym) where
  pure :: a -> W4Conn sym a
pure   = Eval a -> W4Conn sym a
forall sym a. IsSymExprBuilder sym => Eval a -> W4Conn sym a
doEval (Eval a -> W4Conn sym a) -> (a -> Eval a) -> a -> W4Conn sym a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Eval a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
  <*> :: W4Conn sym (a -> b) -> W4Conn sym a -> W4Conn sym 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 >>= :: W4Conn sym a -> (a -> W4Conn sym b) -> W4Conn sym b
>>= a -> W4Conn sym b
f = (sym -> Eval b) -> W4Conn sym b
forall sym a. (sym -> Eval a) -> W4Conn sym a
W4Conn \sym
sym ->
    do a
res1 <- W4Conn sym a -> sym -> Eval a
forall sym a. W4Conn sym a -> sym -> Eval a
evalConn W4Conn sym a
m1 sym
sym
       W4Conn sym b -> sym -> Eval b
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 :: IO a -> W4Conn sym a
liftIO = Eval a -> W4Conn sym a
forall sym a. IsSymExprBuilder sym => Eval a -> W4Conn sym a
doEval (Eval a -> W4Conn sym a)
-> (IO a -> Eval a) -> IO a -> W4Conn sym a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IO a -> Eval a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO

-- | Access the symbolic back-end
getSym :: W4Conn sym sym
getSym :: W4Conn sym sym
getSym = (sym -> Eval sym) -> W4Conn sym sym
forall sym a. (sym -> Eval a) -> W4Conn sym a
W4Conn \sym
sym -> sym -> Eval 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 :: Pred sym -> Pred sym -> W4Conn sym (Pred sym)
w4And Pred sym
p Pred sym
q =
  do sym
sym <- W4Conn sym sym
forall sym. W4Conn sym sym
getSym
     IO (Pred sym) -> W4Conn sym (Pred sym)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (sym -> Pred sym -> Pred sym -> IO (Pred sym)
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 :: Pred sym -> W4Conn sym (Pred sym)
w4Not Pred sym
p =
  do sym
sym <- W4Conn sym sym
forall sym. W4Conn sym sym
getSym
     IO (Pred sym) -> W4Conn sym (Pred sym)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (sym -> Pred sym -> IO (Pred sym)
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 :: Pred sym -> Pred sym -> Pred sym -> W4Conn sym (Pred sym)
w4ITE Pred sym
ifP Pred sym
ifThen Pred sym
ifElse =
  do sym
sym <- W4Conn sym sym
forall sym. W4Conn sym sym
getSym
     IO (Pred sym) -> W4Conn sym (Pred sym)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (sym -> Pred sym -> Pred sym -> Pred sym -> IO (Pred sym)
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 :: (a -> b) -> W4Eval sym a -> W4Eval sym b
fmap = (a -> b) -> W4Eval sym a -> W4Eval sym b
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM

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

instance W4.IsSymExprBuilder sym => MonadIO (W4Eval sym) where
  liftIO :: IO a -> W4Eval sym a
liftIO = W4Conn sym a -> W4Eval sym a
forall sym a. IsSymExprBuilder sym => W4Conn sym a -> W4Eval sym a
total (W4Conn sym a -> W4Eval sym a)
-> (IO a -> W4Conn sym a) -> IO a -> W4Eval sym a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IO a -> W4Conn sym a
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 :: What4 sym -> Pred sym -> W4Eval sym ()
addDefEqn What4 sym
sym Pred sym
p =
  IO () -> W4Eval sym ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (MVar (Pred sym) -> (Pred sym -> IO (Pred sym)) -> IO ()
forall a. MVar a -> (a -> IO a) -> IO ()
modifyMVar_ (What4 sym -> MVar (Pred sym)
forall sym. What4 sym -> MVar (Pred sym)
w4defs What4 sym
sym) (sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
W4.andPred (What4 sym -> sym
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 :: Pred sym -> W4Eval sym ()
addSafety Pred sym
p = W4Conn sym (W4Result sym ()) -> W4Eval sym ()
forall sym a. W4Conn sym (W4Result sym a) -> W4Eval sym a
W4Eval (W4Result sym () -> W4Conn sym (W4Result sym ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pred sym -> () -> W4Result sym ()
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 :: EvalError -> W4Eval sym a
evalError EvalError
err = W4Conn sym (W4Result sym a) -> W4Eval sym a
forall sym a. W4Conn sym (W4Result sym a) -> W4Eval sym a
W4Eval (W4Result sym a -> W4Conn sym (W4Result sym a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (EvalError -> W4Result sym a
forall sym a. EvalError -> W4Result sym a
W4Error EvalError
err))

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


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

assertIntDivisor ::
  W4.IsSymExprBuilder sym => What4 sym -> W4.SymInteger sym -> W4Eval sym ()
assertIntDivisor :: What4 sym -> SymInteger sym -> W4Eval sym ()
assertIntDivisor What4 sym
sym SymInteger sym
x =
  do SymExpr sym BaseBoolType
p <- IO (SymExpr sym BaseBoolType)
-> W4Eval sym (SymExpr sym BaseBoolType)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (sym -> SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType)
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
W4.notPred (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) (SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType))
-> IO (SymExpr sym BaseBoolType) -> IO (SymExpr sym BaseBoolType)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym
-> SymInteger sym
-> SymInteger sym
-> IO (SymExpr sym BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
W4.intEq (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SymInteger sym
x (SymInteger sym -> IO (SymExpr sym BaseBoolType))
-> IO (SymInteger sym) -> IO (SymExpr sym BaseBoolType)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> Integer -> IO (SymInteger sym)
forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
W4.intLit (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) Integer
0)
     What4 sym -> SBit (What4 sym) -> EvalError -> SEval (What4 sym) ()
forall sym.
Backend sym =>
sym -> SBit sym -> EvalError -> SEval sym ()
assertSideCondition What4 sym
sym SymExpr sym BaseBoolType
SBit (What4 sym)
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 :: What4 sym -> EvalError -> SEval (What4 sym) a
raiseError What4 sym
_ = EvalError -> SEval (What4 sym) a
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 <- SymExpr sym BaseBoolType -> Maybe Bool
forall (e :: BaseType -> *).
IsExpr e =>
e BaseBoolType -> Maybe Bool
W4.asConstantPred SymExpr sym BaseBoolType
SBit (What4 sym)
cond = EvalError -> W4Eval sym ()
forall sym a. IsSymExprBuilder sym => EvalError -> W4Eval sym a
evalError EvalError
err
    | Bool
otherwise = SymExpr sym BaseBoolType -> W4Eval sym ()
forall sym. IsSymExprBuilder sym => Pred sym -> W4Eval sym ()
addSafety SymExpr sym BaseBoolType
SBit (What4 sym)
cond

  isReady :: What4 sym -> SEval (What4 sym) a -> Bool
isReady What4 sym
sym SEval (What4 sym) a
m =
    case W4Eval sym a -> sym -> Eval (W4Result sym a)
forall sym a. W4Eval sym a -> sym -> Eval (W4Result sym a)
w4Eval SEval (What4 sym) a
W4Eval sym a
m (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) of
      Ready W4Result sym a
_ -> Bool
True
      Eval (W4Result sym a)
_ -> Bool
False

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

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


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

  mergeEval :: 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 = W4Conn sym (W4Result sym a) -> W4Eval sym a
forall sym a. W4Conn sym (W4Result sym a) -> W4Eval sym a
W4Eval
    do W4Result sym a
rx <- W4Eval sym a -> W4Conn sym (W4Result sym a)
forall sym a. W4Eval sym a -> W4Conn sym (W4Result sym a)
evalPartial SEval (What4 sym) a
W4Eval sym a
mx
       W4Result sym a
ry <- W4Eval sym a -> W4Conn sym (W4Result sym a)
forall sym a. W4Eval sym a -> W4Conn sym (W4Result sym a)
evalPartial SEval (What4 sym) a
W4Eval sym a
my
       case (W4Result sym a
rx, W4Result sym a
ry) of

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

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

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

         (W4Result SymExpr sym BaseBoolType
px a
x, W4Result SymExpr sym BaseBoolType
py a
y) ->
           do W4Result sym a
zr <- W4Eval sym a -> W4Conn sym (W4Result sym a)
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 EvalError
err -> W4Result sym a -> W4Conn sym (W4Result sym a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (W4Result sym a -> W4Conn sym (W4Result sym a))
-> W4Result sym a -> W4Conn sym (W4Result sym a)
forall a b. (a -> b) -> a -> b
$ EvalError -> W4Result sym a
forall sym a. EvalError -> W4Result sym a
W4Error EvalError
err
                W4Result SymExpr sym BaseBoolType
pz a
z ->
                  do SymExpr sym BaseBoolType
p' <- SymExpr sym BaseBoolType
-> SymExpr sym BaseBoolType
-> W4Conn sym (SymExpr sym BaseBoolType)
forall sym.
IsSymExprBuilder sym =>
Pred sym -> Pred sym -> W4Conn sym (Pred sym)
w4And SymExpr sym BaseBoolType
pz (SymExpr sym BaseBoolType -> W4Conn sym (SymExpr sym BaseBoolType))
-> W4Conn sym (SymExpr sym BaseBoolType)
-> W4Conn sym (SymExpr sym BaseBoolType)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SymExpr sym BaseBoolType
-> SymExpr sym BaseBoolType
-> SymExpr sym BaseBoolType
-> W4Conn sym (SymExpr sym BaseBoolType)
forall sym.
IsSymExprBuilder sym =>
Pred sym -> Pred sym -> Pred sym -> W4Conn sym (Pred sym)
w4ITE SymExpr sym BaseBoolType
SBit (What4 sym)
c SymExpr sym BaseBoolType
px SymExpr sym BaseBoolType
py
                     W4Result sym a -> W4Conn sym (W4Result sym a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SymExpr sym BaseBoolType -> a -> W4Result sym a
forall sym a. Pred sym -> a -> W4Result sym a
W4Result SymExpr sym BaseBoolType
p' a
z)

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

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

  bitLit :: What4 sym -> Bool -> SBit (What4 sym)
bitLit What4 sym
sym Bool
b = sym -> Bool -> SymExpr sym BaseBoolType
forall sym. IsExprBuilder sym => sym -> Bool -> Pred sym
W4.backendPred (What4 sym -> sym
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 = SymExpr sym BaseBoolType -> Maybe Bool
forall (e :: BaseType -> *).
IsExpr e =>
e BaseBoolType -> Maybe Bool
W4.asConstantPred SymExpr sym BaseBoolType
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) <- Integer -> Maybe (Some NatRepr)
forall a. Integral a => a -> Maybe (Some NatRepr)
someNat Integer
intw
    = case NatRepr x -> Maybe (LeqProof 1 x)
forall (n :: Nat). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr x
w of
        Maybe (LeqProof 1 x)
Nothing -> SWord sym -> W4Eval sym (SWord sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SWord sym -> W4Eval sym (SWord sym))
-> SWord sym -> W4Eval sym (SWord sym)
forall a b. (a -> b) -> a -> b
$ SWord sym
forall sym. SWord sym
SW.ZBV
        Just LeqProof 1 x
LeqProof -> SymExpr sym ('BaseBVType x) -> SWord sym
forall sym (w :: Nat).
(IsExpr (SymExpr sym), 1 <= w) =>
SymBV sym w -> SWord sym
SW.DBV (SymExpr sym ('BaseBVType x) -> SWord sym)
-> W4Eval sym (SymExpr sym ('BaseBVType x))
-> W4Eval sym (SWord sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO (SymExpr sym ('BaseBVType x))
-> W4Eval sym (SymExpr sym ('BaseBVType x))
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (sym -> NatRepr x -> BV x -> IO (SymExpr sym ('BaseBVType x))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
W4.bvLit (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) NatRepr x
w (NatRepr x -> Integer -> BV x
forall (w :: Nat). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr x
w Integer
i))
    | Bool
otherwise = String -> [String] -> W4Eval sym (SWord sym)
forall a. HasCallStack => String -> [String] -> a
panic String
"what4: wordLit" [String
"invalid bit width:", Integer -> String
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 <- SWord sym -> Maybe Integer
forall sym. IsExprBuilder sym => SWord sym -> Maybe Integer
SW.bvAsUnsignedInteger SWord sym
SWord (What4 sym)
v = (Integer, Integer) -> Maybe (Integer, Integer)
forall a. a -> Maybe a
Just (SWord sym -> Integer
forall sym. SWord sym -> Integer
SW.bvWidth SWord sym
SWord (What4 sym)
v, Integer
x)
    | Bool
otherwise = Maybe (Integer, Integer)
forall a. Maybe a
Nothing

  integerLit :: What4 sym -> Integer -> SEval (What4 sym) (SInteger (What4 sym))
integerLit What4 sym
sym Integer
i = IO (SymExpr sym BaseIntegerType)
-> W4Eval sym (SymExpr sym BaseIntegerType)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (sym -> Integer -> IO (SymExpr sym BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
W4.intLit (What4 sym -> sym
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 = SymExpr sym BaseIntegerType -> Maybe Integer
forall (e :: BaseType -> *).
IsExpr e =>
e BaseIntegerType -> Maybe Integer
W4.asInteger SymExpr sym BaseIntegerType
SInteger (What4 sym)
v

  ppBit :: What4 sym -> SBit (What4 sym) -> Doc
ppBit What4 sym
_ SBit (What4 sym)
v
    | Just Bool
b <- SymExpr sym BaseBoolType -> Maybe Bool
forall (e :: BaseType -> *).
IsExpr e =>
e BaseBoolType -> Maybe Bool
W4.asConstantPred SymExpr sym BaseBoolType
SBit (What4 sym)
v = String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$! if Bool
b then String
"True" else String
"False"
    | Bool
otherwise                     = String -> Doc
text String
"?"

  ppWord :: What4 sym -> PPOpts -> SWord (What4 sym) -> Doc
ppWord What4 sym
_ PPOpts
opts SWord (What4 sym)
v
    | Just Integer
x <- SWord sym -> Maybe Integer
forall sym. IsExprBuilder sym => SWord sym -> Maybe Integer
SW.bvAsUnsignedInteger SWord sym
SWord (What4 sym)
v
    = PPOpts -> BV -> Doc
ppBV PPOpts
opts (Integer -> Integer -> BV
BV (SWord sym -> Integer
forall sym. SWord sym -> Integer
SW.bvWidth SWord sym
SWord (What4 sym)
v) Integer
x)

    | Bool
otherwise = String -> Doc
text String
"[?]"

  ppInteger :: What4 sym -> PPOpts -> SInteger (What4 sym) -> Doc
ppInteger What4 sym
_ PPOpts
_opts SInteger (What4 sym)
v
    | Just Integer
x <- SymExpr sym BaseIntegerType -> Maybe Integer
forall (e :: BaseType -> *).
IsExpr e =>
e BaseIntegerType -> Maybe Integer
W4.asInteger SymExpr sym BaseIntegerType
SInteger (What4 sym)
v = Integer -> Doc
integer Integer
x
    | Bool
otherwise = String -> Doc
text String
"[?]"

  ppFloat :: What4 sym -> PPOpts -> SFloat (What4 sym) -> Doc
ppFloat What4 sym
_ PPOpts
_opts SFloat (What4 sym)
_ = String -> Doc
text String
"[?]"

  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 = IO (SymExpr sym BaseBoolType)
-> W4Eval sym (SymExpr sym BaseBoolType)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (sym
-> SymExpr sym BaseBoolType
-> SymExpr sym BaseBoolType
-> SymExpr sym BaseBoolType
-> IO (SymExpr sym BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> Pred sym -> IO (Pred sym)
W4.itePred (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym BaseBoolType
SBit (What4 sym)
c SymExpr sym BaseBoolType
SBit (What4 sym)
x SymExpr sym BaseBoolType
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 = IO (SWord sym) -> W4Eval sym (SWord sym)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (sym
-> SymExpr sym BaseBoolType
-> SWord sym
-> SWord sym
-> IO (SWord sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> SWord sym -> SWord sym -> IO (SWord sym)
SW.bvIte (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym BaseBoolType
SBit (What4 sym)
c SWord sym
SWord (What4 sym)
x SWord sym
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 = IO (SymExpr sym BaseIntegerType)
-> W4Eval sym (SymExpr sym BaseIntegerType)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (sym
-> SymExpr sym BaseBoolType
-> SymExpr sym BaseIntegerType
-> SymExpr sym BaseIntegerType
-> IO (SymExpr sym BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym
-> Pred sym
-> SymInteger sym
-> SymInteger sym
-> IO (SymInteger sym)
W4.intIte (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym BaseBoolType
SBit (What4 sym)
c SymExpr sym BaseIntegerType
SInteger (What4 sym)
x SymExpr sym BaseIntegerType
SInteger (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 = IO (SymExpr sym BaseBoolType)
-> W4Eval sym (SymExpr sym BaseBoolType)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (sym
-> SymExpr sym BaseBoolType
-> SymExpr sym BaseBoolType
-> IO (SymExpr sym BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
W4.eqPred (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym BaseBoolType
SBit (What4 sym)
x SymExpr sym BaseBoolType
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 = IO (SymExpr sym BaseBoolType)
-> W4Eval sym (SymExpr sym BaseBoolType)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (sym
-> SymExpr sym BaseBoolType
-> SymExpr sym BaseBoolType
-> IO (SymExpr sym BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
W4.andPred (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym BaseBoolType
SBit (What4 sym)
x SymExpr sym BaseBoolType
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 = IO (SymExpr sym BaseBoolType)
-> W4Eval sym (SymExpr sym BaseBoolType)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (sym
-> SymExpr sym BaseBoolType
-> SymExpr sym BaseBoolType
-> IO (SymExpr sym BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
W4.orPred (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym BaseBoolType
SBit (What4 sym)
x SymExpr sym BaseBoolType
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 = IO (SymExpr sym BaseBoolType)
-> W4Eval sym (SymExpr sym BaseBoolType)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (sym
-> SymExpr sym BaseBoolType
-> SymExpr sym BaseBoolType
-> IO (SymExpr sym BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
W4.xorPred (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym BaseBoolType
SBit (What4 sym)
x SymExpr sym BaseBoolType
SBit (What4 sym)
y)
  bitComplement :: What4 sym
-> SBit (What4 sym) -> SEval (What4 sym) (SBit (What4 sym))
bitComplement What4 sym
sym SBit (What4 sym)
x = IO (SymExpr sym BaseBoolType)
-> W4Eval sym (SymExpr sym BaseBoolType)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (sym -> SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType)
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
W4.notPred (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym BaseBoolType
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 = IO (SymExpr sym BaseBoolType)
-> W4Eval sym (SymExpr sym BaseBoolType)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (sym -> SWord sym -> Integer -> IO (SymExpr sym BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> Integer -> IO (Pred sym)
SW.bvAtBE (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SWord 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 = IO (SWord sym) -> W4Eval sym (SWord sym)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (sym
-> SWord sym
-> Integer
-> SymExpr sym BaseBoolType
-> IO (SWord sym)
forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> Integer -> Pred sym -> IO (SWord sym)
SW.bvSetBE (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SWord sym
SWord (What4 sym)
bv Integer
idx SymExpr sym BaseBoolType
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 <- What4 sym
-> Integer -> Integer -> SEval (What4 sym) (SWord (What4 sym))
forall sym.
Backend sym =>
sym -> Integer -> Integer -> SEval sym (SWord sym)
wordLit What4 sym
sym ([SymExpr sym BaseBoolType] -> Integer
forall i a. Num i => [a] -> i
genericLength [SymExpr sym BaseBoolType]
[SBit (What4 sym)]
bs) Integer
0
       let f :: SWord sym
-> (Integer, SymExpr sym BaseBoolType)
-> SEval (What4 sym) (SWord (What4 sym))
f SWord sym
w (Integer
idx,SymExpr sym BaseBoolType
b) = What4 sym
-> SWord (What4 sym)
-> Integer
-> SBit (What4 sym)
-> SEval (What4 sym) (SWord (What4 sym))
forall sym.
Backend sym =>
sym -> SWord sym -> Integer -> SBit sym -> SEval sym (SWord sym)
wordUpdate What4 sym
sym SWord sym
SWord (What4 sym)
w Integer
idx SymExpr sym BaseBoolType
SBit (What4 sym)
b
       (SWord sym
 -> (Integer, SymExpr sym BaseBoolType) -> W4Eval sym (SWord sym))
-> SWord sym
-> [(Integer, SymExpr sym BaseBoolType)]
-> W4Eval sym (SWord sym)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM SWord sym
-> (Integer, SymExpr sym BaseBoolType)
-> SEval (What4 sym) (SWord (What4 sym))
SWord sym
-> (Integer, SymExpr sym BaseBoolType) -> W4Eval sym (SWord sym)
f SWord sym
z ([Integer]
-> [SymExpr sym BaseBoolType]
-> [(Integer, SymExpr sym BaseBoolType)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Integer
0..] [SymExpr sym BaseBoolType]
[SBit (What4 sym)]
bs)

  unpackWord :: What4 sym
-> SWord (What4 sym) -> SEval (What4 sym) [SBit (What4 sym)]
unpackWord What4 sym
sym SWord (What4 sym)
bv = IO [SymExpr sym BaseBoolType]
-> W4Eval sym [SymExpr sym BaseBoolType]
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO [SymExpr sym BaseBoolType]
 -> W4Eval sym [SymExpr sym BaseBoolType])
-> IO [SymExpr sym BaseBoolType]
-> W4Eval sym [SymExpr sym BaseBoolType]
forall a b. (a -> b) -> a -> b
$
    (Integer -> IO (SymExpr sym BaseBoolType))
-> [Integer] -> IO [SymExpr sym BaseBoolType]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (sym -> SWord sym -> Integer -> IO (SymExpr sym BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> Integer -> IO (Pred sym)
SW.bvAtBE (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SWord sym
SWord (What4 sym)
bv) [Integer
0 .. SWord sym -> Integer
forall sym. SWord sym -> Integer
SW.bvWidth SWord sym
SWord (What4 sym)
bvInteger -> Integer -> Integer
forall 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 = IO (SWord sym) -> W4Eval sym (SWord sym)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SWord sym) -> W4Eval sym (SWord sym))
-> IO (SWord sym) -> W4Eval sym (SWord sym)
forall a b. (a -> b) -> a -> b
$ sym -> SWord sym -> SWord sym -> IO (SWord sym)
forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> SWord sym -> IO (SWord sym)
SW.bvJoin (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SWord sym
SWord (What4 sym)
x SWord sym
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 = (SWord sym, SWord sym) -> W4Eval sym (SWord sym, SWord sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SWord sym
forall sym. SWord sym
SW.ZBV, SWord sym
SWord (What4 sym)
bv)
  splitWord What4 sym
_sym Integer
_ Integer
0 SWord (What4 sym)
bv = (SWord sym, SWord sym) -> W4Eval sym (SWord sym, SWord sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SWord sym
SWord (What4 sym)
bv, SWord sym
forall sym. SWord sym
SW.ZBV)
  splitWord What4 sym
sym Integer
lw Integer
rw SWord (What4 sym)
bv = IO (SWord sym, SWord sym) -> W4Eval sym (SWord sym, SWord sym)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SWord sym, SWord sym) -> W4Eval sym (SWord sym, SWord sym))
-> IO (SWord sym, SWord sym) -> W4Eval sym (SWord sym, SWord sym)
forall a b. (a -> b) -> a -> b
$
    do SWord sym
l <- sym -> Integer -> Integer -> SWord sym -> IO (SWord sym)
forall sym.
IsExprBuilder sym =>
sym -> Integer -> Integer -> SWord sym -> IO (SWord sym)
SW.bvSliceBE (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) Integer
0 Integer
lw SWord sym
SWord (What4 sym)
bv
       SWord sym
r <- sym -> Integer -> Integer -> SWord sym -> IO (SWord sym)
forall sym.
IsExprBuilder sym =>
sym -> Integer -> Integer -> SWord sym -> IO (SWord sym)
SW.bvSliceBE (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) Integer
lw Integer
rw SWord sym
SWord (What4 sym)
bv
       (SWord sym, SWord sym) -> IO (SWord sym, SWord sym)
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 =
    IO (SWord sym) -> W4Eval sym (SWord sym)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SWord sym) -> W4Eval sym (SWord sym))
-> IO (SWord sym) -> W4Eval sym (SWord sym)
forall a b. (a -> b) -> a -> b
$ sym -> Integer -> Integer -> SWord sym -> IO (SWord sym)
forall sym.
IsExprBuilder sym =>
sym -> Integer -> Integer -> SWord sym -> IO (SWord sym)
SW.bvSliceLE (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) Integer
idx Integer
bits SWord sym
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 = IO (SymExpr sym BaseBoolType)
-> W4Eval sym (SymExpr sym BaseBoolType)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (sym -> SWord sym -> SWord sym -> IO (SymExpr sym BaseBoolType)
PredBin
SW.bvEq  (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SWord sym
SWord (What4 sym)
x SWord sym
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 = IO (SymExpr sym BaseBoolType)
-> W4Eval sym (SymExpr sym BaseBoolType)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (sym -> SWord sym -> SWord sym -> IO (SymExpr sym BaseBoolType)
PredBin
SW.bvult (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SWord sym
SWord (What4 sym)
x SWord sym
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 = IO (SymExpr sym BaseBoolType)
-> W4Eval sym (SymExpr sym BaseBoolType)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (sym -> SWord sym -> SWord sym -> IO (SymExpr sym BaseBoolType)
PredBin
SW.bvugt (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SWord sym
SWord (What4 sym)
x SWord sym
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 = IO (SymExpr sym BaseBoolType)
-> W4Eval sym (SymExpr sym BaseBoolType)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (sym -> SWord sym -> SWord sym -> IO (SymExpr sym BaseBoolType)
PredBin
SW.bvslt (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SWord sym
SWord (What4 sym)
x SWord sym
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 = IO (SWord sym) -> W4Eval sym (SWord sym)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (sym -> SWord sym -> SWord sym -> IO (SWord sym)
forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> SWord sym -> IO (SWord sym)
SW.bvOr  (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SWord sym
SWord (What4 sym)
x SWord sym
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 = IO (SWord sym) -> W4Eval sym (SWord sym)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (sym -> SWord sym -> SWord sym -> IO (SWord sym)
forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> SWord sym -> IO (SWord sym)
SW.bvAnd (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SWord sym
SWord (What4 sym)
x SWord sym
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 = IO (SWord sym) -> W4Eval sym (SWord sym)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (sym -> SWord sym -> SWord sym -> IO (SWord sym)
forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> SWord sym -> IO (SWord sym)
SW.bvXor (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SWord sym
SWord (What4 sym)
x SWord sym
SWord (What4 sym)
y)
  wordComplement :: What4 sym
-> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym))
wordComplement What4 sym
sym SWord (What4 sym)
x = IO (SWord sym) -> W4Eval sym (SWord sym)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (sym -> SWord sym -> IO (SWord sym)
SWordUn
SW.bvNot (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SWord 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 = IO (SWord sym) -> W4Eval sym (SWord sym)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (sym -> SWord sym -> SWord sym -> IO (SWord sym)
forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> SWord sym -> IO (SWord sym)
SW.bvAdd (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SWord sym
SWord (What4 sym)
x SWord sym
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 = IO (SWord sym) -> W4Eval sym (SWord sym)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (sym -> SWord sym -> SWord sym -> IO (SWord sym)
forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> SWord sym -> IO (SWord sym)
SW.bvSub (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SWord sym
SWord (What4 sym)
x SWord sym
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 = IO (SWord sym) -> W4Eval sym (SWord sym)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (sym -> SWord sym -> SWord sym -> IO (SWord sym)
forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> SWord sym -> IO (SWord sym)
SW.bvMul (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SWord sym
SWord (What4 sym)
x SWord sym
SWord (What4 sym)
y)
  wordNegate :: What4 sym
-> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym))
wordNegate What4 sym
sym SWord (What4 sym)
x   = IO (SWord sym) -> W4Eval sym (SWord sym)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (sym -> SWord sym -> IO (SWord sym)
SWordUn
SW.bvNeg (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SWord 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   = sym -> SWord sym -> SEval (What4 sym) (SWord sym)
forall sym.
IsSymExprBuilder sym =>
sym -> SWord sym -> SEval (What4 sym) (SWord sym)
sLg2 (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SWord sym
SWord (What4 sym)
x
 
  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 What4 sym -> SWord sym -> W4Eval sym ()
forall sym.
IsSymExprBuilder sym =>
What4 sym -> SWord sym -> W4Eval sym ()
assertBVDivisor What4 sym
sym SWord sym
SWord (What4 sym)
y
        IO (SWord sym) -> W4Eval sym (SWord sym)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (sym -> SWord sym -> SWord sym -> IO (SWord sym)
forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> SWord sym -> IO (SWord sym)
SW.bvUDiv (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SWord sym
SWord (What4 sym)
x SWord sym
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 What4 sym -> SWord sym -> W4Eval sym ()
forall sym.
IsSymExprBuilder sym =>
What4 sym -> SWord sym -> W4Eval sym ()
assertBVDivisor What4 sym
sym SWord sym
SWord (What4 sym)
y
        IO (SWord sym) -> W4Eval sym (SWord sym)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (sym -> SWord sym -> SWord sym -> IO (SWord sym)
forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> SWord sym -> IO (SWord sym)
SW.bvURem (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SWord sym
SWord (What4 sym)
x SWord sym
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 What4 sym -> SWord sym -> W4Eval sym ()
forall sym.
IsSymExprBuilder sym =>
What4 sym -> SWord sym -> W4Eval sym ()
assertBVDivisor What4 sym
sym SWord sym
SWord (What4 sym)
y
        IO (SWord sym) -> W4Eval sym (SWord sym)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (sym -> SWord sym -> SWord sym -> IO (SWord sym)
forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> SWord sym -> IO (SWord sym)
SW.bvSDiv (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SWord sym
SWord (What4 sym)
x SWord sym
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 What4 sym -> SWord sym -> W4Eval sym ()
forall sym.
IsSymExprBuilder sym =>
What4 sym -> SWord sym -> W4Eval sym ()
assertBVDivisor What4 sym
sym SWord sym
SWord (What4 sym)
y
        IO (SWord sym) -> W4Eval sym (SWord sym)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (sym -> SWord sym -> SWord sym -> IO (SWord sym)
forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> SWord sym -> IO (SWord sym)
SW.bvSRem (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SWord sym
SWord (What4 sym)
x SWord sym
SWord (What4 sym)
y)

  wordToInt :: What4 sym
-> SWord (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym))
wordToInt What4 sym
sym SWord (What4 sym)
x = IO (SymExpr sym BaseIntegerType)
-> W4Eval sym (SymExpr sym BaseIntegerType)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (sym -> SWord sym -> IO (SymExpr sym BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> IO (SymInteger sym)
SW.bvToInteger (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SWord 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 = IO (SWord sym) -> W4Eval sym (SWord sym)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (sym -> SymExpr sym BaseIntegerType -> Integer -> IO (SWord sym)
forall sym width.
(Show width, Integral width, IsExprBuilder sym) =>
sym -> SymInteger sym -> width -> IO (SWord sym)
SW.integerToBV (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym BaseIntegerType
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  = IO (SymExpr sym BaseIntegerType)
-> W4Eval sym (SymExpr sym BaseIntegerType)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym BaseIntegerType)
 -> W4Eval sym (SymExpr sym BaseIntegerType))
-> IO (SymExpr sym BaseIntegerType)
-> W4Eval sym (SymExpr sym BaseIntegerType)
forall a b. (a -> b) -> a -> b
$ sym
-> SymExpr sym BaseIntegerType
-> SymExpr sym BaseIntegerType
-> IO (SymExpr sym BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
W4.intAdd (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym BaseIntegerType
SInteger (What4 sym)
x SymExpr sym BaseIntegerType
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  = IO (SymExpr sym BaseIntegerType)
-> W4Eval sym (SymExpr sym BaseIntegerType)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym BaseIntegerType)
 -> W4Eval sym (SymExpr sym BaseIntegerType))
-> IO (SymExpr sym BaseIntegerType)
-> W4Eval sym (SymExpr sym BaseIntegerType)
forall a b. (a -> b) -> a -> b
$ sym
-> SymExpr sym BaseIntegerType
-> SymExpr sym BaseIntegerType
-> IO (SymExpr sym BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
W4.intSub (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym BaseIntegerType
SInteger (What4 sym)
x SymExpr sym BaseIntegerType
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  = IO (SymExpr sym BaseIntegerType)
-> W4Eval sym (SymExpr sym BaseIntegerType)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym BaseIntegerType)
 -> W4Eval sym (SymExpr sym BaseIntegerType))
-> IO (SymExpr sym BaseIntegerType)
-> W4Eval sym (SymExpr sym BaseIntegerType)
forall a b. (a -> b) -> a -> b
$ sym
-> SymExpr sym BaseIntegerType
-> SymExpr sym BaseIntegerType
-> IO (SymExpr sym BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
W4.intMul (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym BaseIntegerType
SInteger (What4 sym)
x SymExpr sym BaseIntegerType
SInteger (What4 sym)
y
  intNegate :: What4 sym
-> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym))
intNegate What4 sym
sym SInteger (What4 sym)
x    = IO (SymExpr sym BaseIntegerType)
-> W4Eval sym (SymExpr sym BaseIntegerType)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym BaseIntegerType)
 -> W4Eval sym (SymExpr sym BaseIntegerType))
-> IO (SymExpr sym BaseIntegerType)
-> W4Eval sym (SymExpr sym BaseIntegerType)
forall a b. (a -> b) -> a -> b
$ sym
-> SymExpr sym BaseIntegerType -> IO (SymExpr sym BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymInteger sym)
W4.intNeg (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym BaseIntegerType
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 What4 sym -> SymExpr sym BaseIntegerType -> W4Eval sym ()
forall sym.
IsSymExprBuilder sym =>
What4 sym -> SymInteger sym -> W4Eval sym ()
assertIntDivisor What4 sym
sym SymExpr sym BaseIntegerType
SInteger (What4 sym)
y
       IO (SymExpr sym BaseIntegerType)
-> W4Eval sym (SymExpr sym BaseIntegerType)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym BaseIntegerType)
 -> W4Eval sym (SymExpr sym BaseIntegerType))
-> IO (SymExpr sym BaseIntegerType)
-> W4Eval sym (SymExpr sym BaseIntegerType)
forall a b. (a -> b) -> a -> b
$ do
         SymExpr sym BaseBoolType
neg <- IO (SymExpr sym BaseBoolType) -> IO (SymExpr sym BaseBoolType)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (sym
-> SymExpr sym BaseIntegerType
-> SymExpr sym BaseIntegerType
-> IO (SymExpr sym BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
W4.intLt (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym BaseIntegerType
SInteger (What4 sym)
y (SymExpr sym BaseIntegerType -> IO (SymExpr sym BaseBoolType))
-> IO (SymExpr sym BaseIntegerType)
-> IO (SymExpr sym BaseBoolType)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> Integer -> IO (SymExpr sym BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
W4.intLit (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) Integer
0)
         case SymExpr sym BaseBoolType -> Maybe Bool
forall (e :: BaseType -> *).
IsExpr e =>
e BaseBoolType -> Maybe Bool
W4.asConstantPred SymExpr sym BaseBoolType
neg of
           Just Bool
False -> sym
-> SymExpr sym BaseIntegerType
-> SymExpr sym BaseIntegerType
-> IO (SymExpr sym BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
W4.intDiv (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym BaseIntegerType
SInteger (What4 sym)
x SymExpr sym BaseIntegerType
SInteger (What4 sym)
y
           Just Bool
True  ->
              do SymExpr sym BaseIntegerType
xneg <- sym
-> SymExpr sym BaseIntegerType -> IO (SymExpr sym BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymInteger sym)
W4.intNeg (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym BaseIntegerType
SInteger (What4 sym)
x
                 SymExpr sym BaseIntegerType
yneg <- sym
-> SymExpr sym BaseIntegerType -> IO (SymExpr sym BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymInteger sym)
W4.intNeg (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym BaseIntegerType
SInteger (What4 sym)
y
                 sym
-> SymExpr sym BaseIntegerType
-> SymExpr sym BaseIntegerType
-> IO (SymExpr sym BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
W4.intDiv (What4 sym -> sym
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 <- sym
-> SymExpr sym BaseIntegerType -> IO (SymExpr sym BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymInteger sym)
W4.intNeg (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym BaseIntegerType
SInteger (What4 sym)
x
                 SymExpr sym BaseIntegerType
yneg <- sym
-> SymExpr sym BaseIntegerType -> IO (SymExpr sym BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymInteger sym)
W4.intNeg (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym BaseIntegerType
SInteger (What4 sym)
y
                 SymExpr sym BaseIntegerType
zneg <- sym
-> SymExpr sym BaseIntegerType
-> SymExpr sym BaseIntegerType
-> IO (SymExpr sym BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
W4.intDiv (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym BaseIntegerType
xneg SymExpr sym BaseIntegerType
yneg
                 SymExpr sym BaseIntegerType
z    <- sym
-> SymExpr sym BaseIntegerType
-> SymExpr sym BaseIntegerType
-> IO (SymExpr sym BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
W4.intDiv (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym BaseIntegerType
SInteger (What4 sym)
x SymExpr sym BaseIntegerType
SInteger (What4 sym)
y
                 sym
-> SymExpr sym BaseBoolType
-> SymExpr sym BaseIntegerType
-> SymExpr sym BaseIntegerType
-> IO (SymExpr sym BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym
-> Pred sym
-> SymInteger sym
-> SymInteger sym
-> IO (SymInteger sym)
W4.intIte (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym BaseBoolType
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 What4 sym -> SymExpr sym BaseIntegerType -> W4Eval sym ()
forall sym.
IsSymExprBuilder sym =>
What4 sym -> SymInteger sym -> W4Eval sym ()
assertIntDivisor What4 sym
sym SymExpr sym BaseIntegerType
SInteger (What4 sym)
y
       IO (SymExpr sym BaseIntegerType)
-> W4Eval sym (SymExpr sym BaseIntegerType)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym BaseIntegerType)
 -> W4Eval sym (SymExpr sym BaseIntegerType))
-> IO (SymExpr sym BaseIntegerType)
-> W4Eval sym (SymExpr sym BaseIntegerType)
forall a b. (a -> b) -> a -> b
$ do
         SymExpr sym BaseBoolType
neg <- IO (SymExpr sym BaseBoolType) -> IO (SymExpr sym BaseBoolType)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (sym
-> SymExpr sym BaseIntegerType
-> SymExpr sym BaseIntegerType
-> IO (SymExpr sym BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
W4.intLt (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym BaseIntegerType
SInteger (What4 sym)
y (SymExpr sym BaseIntegerType -> IO (SymExpr sym BaseBoolType))
-> IO (SymExpr sym BaseIntegerType)
-> IO (SymExpr sym BaseBoolType)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> Integer -> IO (SymExpr sym BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
W4.intLit (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) Integer
0)
         case SymExpr sym BaseBoolType -> Maybe Bool
forall (e :: BaseType -> *).
IsExpr e =>
e BaseBoolType -> Maybe Bool
W4.asConstantPred SymExpr sym BaseBoolType
neg of
           Just Bool
False -> sym
-> SymExpr sym BaseIntegerType
-> SymExpr sym BaseIntegerType
-> IO (SymExpr sym BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
W4.intMod (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym BaseIntegerType
SInteger (What4 sym)
x SymExpr sym BaseIntegerType
SInteger (What4 sym)
y
           Just Bool
True  ->
              do SymExpr sym BaseIntegerType
xneg <- sym
-> SymExpr sym BaseIntegerType -> IO (SymExpr sym BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymInteger sym)
W4.intNeg (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym BaseIntegerType
SInteger (What4 sym)
x
                 SymExpr sym BaseIntegerType
yneg <- sym
-> SymExpr sym BaseIntegerType -> IO (SymExpr sym BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymInteger sym)
W4.intNeg (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym BaseIntegerType
SInteger (What4 sym)
y
                 sym
-> SymExpr sym BaseIntegerType -> IO (SymExpr sym BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymInteger sym)
W4.intNeg (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) (SymExpr sym BaseIntegerType -> IO (SymExpr sym BaseIntegerType))
-> IO (SymExpr sym BaseIntegerType)
-> IO (SymExpr sym BaseIntegerType)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym
-> SymExpr sym BaseIntegerType
-> SymExpr sym BaseIntegerType
-> IO (SymExpr sym BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
W4.intMod (What4 sym -> sym
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 <- sym
-> SymExpr sym BaseIntegerType -> IO (SymExpr sym BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymInteger sym)
W4.intNeg (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym BaseIntegerType
SInteger (What4 sym)
x
                 SymExpr sym BaseIntegerType
yneg <- sym
-> SymExpr sym BaseIntegerType -> IO (SymExpr sym BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymInteger sym)
W4.intNeg (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym BaseIntegerType
SInteger (What4 sym)
y
                 SymExpr sym BaseIntegerType
z    <- sym
-> SymExpr sym BaseIntegerType
-> SymExpr sym BaseIntegerType
-> IO (SymExpr sym BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
W4.intMod (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym BaseIntegerType
SInteger (What4 sym)
x SymExpr sym BaseIntegerType
SInteger (What4 sym)
y
                 SymExpr sym BaseIntegerType
zneg <- sym
-> SymExpr sym BaseIntegerType -> IO (SymExpr sym BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymInteger sym)
W4.intNeg (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) (SymExpr sym BaseIntegerType -> IO (SymExpr sym BaseIntegerType))
-> IO (SymExpr sym BaseIntegerType)
-> IO (SymExpr sym BaseIntegerType)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym
-> SymExpr sym BaseIntegerType
-> SymExpr sym BaseIntegerType
-> IO (SymExpr sym BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
W4.intMod (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym BaseIntegerType
xneg SymExpr sym BaseIntegerType
yneg
                 sym
-> SymExpr sym BaseBoolType
-> SymExpr sym BaseIntegerType
-> SymExpr sym BaseIntegerType
-> IO (SymExpr sym BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym
-> Pred sym
-> SymInteger sym
-> SymInteger sym
-> IO (SymInteger sym)
W4.intIte (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym BaseBoolType
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 = IO (SymExpr sym BaseBoolType)
-> W4Eval sym (SymExpr sym BaseBoolType)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym BaseBoolType)
 -> W4Eval sym (SymExpr sym BaseBoolType))
-> IO (SymExpr sym BaseBoolType)
-> W4Eval sym (SymExpr sym BaseBoolType)
forall a b. (a -> b) -> a -> b
$ sym
-> SymExpr sym BaseIntegerType
-> SymExpr sym BaseIntegerType
-> IO (SymExpr sym BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
W4.intEq (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym BaseIntegerType
SInteger (What4 sym)
x SymExpr sym BaseIntegerType
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 = IO (SymExpr sym BaseBoolType)
-> W4Eval sym (SymExpr sym BaseBoolType)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym BaseBoolType)
 -> W4Eval sym (SymExpr sym BaseBoolType))
-> IO (SymExpr sym BaseBoolType)
-> W4Eval sym (SymExpr sym BaseBoolType)
forall a b. (a -> b) -> a -> b
$ sym
-> SymExpr sym BaseIntegerType
-> SymExpr sym BaseIntegerType
-> IO (SymExpr sym BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
W4.intLt (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym BaseIntegerType
SInteger (What4 sym)
x SymExpr sym BaseIntegerType
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 = IO (SymExpr sym BaseBoolType)
-> W4Eval sym (SymExpr sym BaseBoolType)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym BaseBoolType)
 -> W4Eval sym (SymExpr sym BaseBoolType))
-> IO (SymExpr sym BaseBoolType)
-> W4Eval sym (SymExpr sym BaseBoolType)
forall a b. (a -> b) -> a -> b
$ sym
-> SymExpr sym BaseIntegerType
-> SymExpr sym BaseIntegerType
-> IO (SymExpr sym BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
W4.intLt (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym BaseIntegerType
SInteger (What4 sym)
y SymExpr sym BaseIntegerType
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 <- SymExpr sym BaseIntegerType -> Maybe Integer
forall (e :: BaseType -> *).
IsExpr e =>
e BaseIntegerType -> Maybe Integer
W4.asInteger SymExpr sym BaseIntegerType
SInteger (What4 sym)
x
    = IO (SymExpr sym BaseIntegerType)
-> W4Eval sym (SymExpr sym BaseIntegerType)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym BaseIntegerType)
 -> W4Eval sym (SymExpr sym BaseIntegerType))
-> IO (SymExpr sym BaseIntegerType)
-> W4Eval sym (SymExpr sym BaseIntegerType)
forall a b. (a -> b) -> a -> b
$ sym -> Integer -> IO (SymExpr sym BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
W4.intLit (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) (Integer
xi Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
m)

    | Bool
otherwise
    = SymExpr sym BaseIntegerType
-> W4Eval sym (SymExpr sym BaseIntegerType)
forall (f :: * -> *) a. Applicative f => a -> f a
pure SymExpr sym BaseIntegerType
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)
_ = String -> [String] -> W4Eval sym (SymExpr sym BaseIntegerType)
forall a. String -> [String] -> a
evalPanic String
"znToInt" [String
"0 modulus not allowed"]
  znToInt What4 sym
sym Integer
m SInteger (What4 sym)
x = IO (SymExpr sym BaseIntegerType)
-> W4Eval sym (SymExpr sym BaseIntegerType)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (sym
-> SymExpr sym BaseIntegerType
-> SymExpr sym BaseIntegerType
-> IO (SymExpr sym BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
W4.intMod (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym BaseIntegerType
SInteger (What4 sym)
x (SymExpr sym BaseIntegerType -> IO (SymExpr sym BaseIntegerType))
-> IO (SymExpr sym BaseIntegerType)
-> IO (SymExpr sym BaseIntegerType)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> Integer -> IO (SymExpr sym BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
W4.intLit (What4 sym -> sym
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)
_ = String -> [String] -> W4Eval sym (SymExpr sym BaseBoolType)
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 = IO (SymExpr sym BaseBoolType)
-> W4Eval sym (SymExpr sym BaseBoolType)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym BaseBoolType)
 -> W4Eval sym (SymExpr sym BaseBoolType))
-> IO (SymExpr sym BaseBoolType)
-> W4Eval sym (SymExpr sym BaseBoolType)
forall a b. (a -> b) -> a -> b
$
     do SymExpr sym BaseIntegerType
diff <- sym
-> SymExpr sym BaseIntegerType
-> SymExpr sym BaseIntegerType
-> IO (SymExpr sym BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
W4.intSub (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym BaseIntegerType
SInteger (What4 sym)
x SymExpr sym BaseIntegerType
SInteger (What4 sym)
y
        sym
-> SymExpr sym BaseIntegerType
-> Natural
-> IO (SymExpr sym BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> Natural -> IO (Pred sym)
W4.intDivisible (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym BaseIntegerType
diff (Integer -> Natural
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 = IO (SymExpr sym BaseIntegerType)
-> W4Eval sym (SymExpr sym BaseIntegerType)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym BaseIntegerType)
 -> W4Eval sym (SymExpr sym BaseIntegerType))
-> IO (SymExpr sym BaseIntegerType)
-> W4Eval sym (SymExpr sym BaseIntegerType)
forall a b. (a -> b) -> a -> b
$ sym
-> Integer
-> SymExpr sym BaseIntegerType
-> SymExpr sym BaseIntegerType
-> IO (SymExpr sym BaseIntegerType)
forall sym.
IsSymExprBuilder sym =>
sym
-> Integer
-> SymInteger sym
-> SymInteger sym
-> IO (SymInteger sym)
sModAdd (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) Integer
m SymExpr sym BaseIntegerType
SInteger (What4 sym)
x SymExpr sym BaseIntegerType
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 = IO (SymExpr sym BaseIntegerType)
-> W4Eval sym (SymExpr sym BaseIntegerType)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym BaseIntegerType)
 -> W4Eval sym (SymExpr sym BaseIntegerType))
-> IO (SymExpr sym BaseIntegerType)
-> W4Eval sym (SymExpr sym BaseIntegerType)
forall a b. (a -> b) -> a -> b
$ sym
-> Integer
-> SymExpr sym BaseIntegerType
-> SymExpr sym BaseIntegerType
-> IO (SymExpr sym BaseIntegerType)
forall sym.
IsSymExprBuilder sym =>
sym
-> Integer
-> SymInteger sym
-> SymInteger sym
-> IO (SymInteger sym)
sModSub (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) Integer
m SymExpr sym BaseIntegerType
SInteger (What4 sym)
x SymExpr sym BaseIntegerType
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 = IO (SymExpr sym BaseIntegerType)
-> W4Eval sym (SymExpr sym BaseIntegerType)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym BaseIntegerType)
 -> W4Eval sym (SymExpr sym BaseIntegerType))
-> IO (SymExpr sym BaseIntegerType)
-> W4Eval sym (SymExpr sym BaseIntegerType)
forall a b. (a -> b) -> a -> b
$ sym
-> Integer
-> SymExpr sym BaseIntegerType
-> SymExpr sym BaseIntegerType
-> IO (SymExpr sym BaseIntegerType)
forall sym.
IsSymExprBuilder sym =>
sym
-> Integer
-> SymInteger sym
-> SymInteger sym
-> IO (SymInteger sym)
sModMult (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) Integer
m SymExpr sym BaseIntegerType
SInteger (What4 sym)
x SymExpr sym BaseIntegerType
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   = IO (SymExpr sym BaseIntegerType)
-> W4Eval sym (SymExpr sym BaseIntegerType)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym BaseIntegerType)
 -> W4Eval sym (SymExpr sym BaseIntegerType))
-> IO (SymExpr sym BaseIntegerType)
-> W4Eval sym (SymExpr sym BaseIntegerType)
forall a b. (a -> b) -> a -> b
$ sym
-> Integer
-> SymExpr sym BaseIntegerType
-> IO (SymExpr sym BaseIntegerType)
forall sym.
IsSymExprBuilder sym =>
sym -> Integer -> SymInteger sym -> IO (SymInteger sym)
sModNegate (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) Integer
m SymExpr sym BaseIntegerType
SInteger (What4 sym)
x
  znRecip :: What4 sym
-> Integer
-> SInteger (What4 sym)
-> SEval (What4 sym) (SInteger (What4 sym))
znRecip = What4 sym
-> Integer
-> SInteger (What4 sym)
-> SEval (What4 sym) (SInteger (What4 sym))
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 = IO (SFloat sym) -> W4Eval sym (SFloat sym)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SFloat sym) -> W4Eval sym (SFloat sym))
-> IO (SFloat sym) -> W4Eval sym (SFloat sym)
forall a b. (a -> b) -> a -> b
$ sym -> Integer -> Integer -> Rational -> IO (SFloat sym)
forall sym.
IsExprBuilder sym =>
sym -> Integer -> Integer -> Rational -> IO (SFloat sym)
FP.fpFromRationalLit (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) Integer
e Integer
p Rational
r

  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 } =
    IO (SFloat sym) -> W4Eval sym (SFloat sym)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (sym -> Integer -> Integer -> SWord sym -> IO (SFloat sym)
forall sym.
IsExprBuilder sym =>
sym -> Integer -> Integer -> SWord sym -> IO (SFloat sym)
FP.fpFromBinary (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) Integer
e Integer
p (SWord sym -> IO (SFloat sym)) -> IO (SWord sym) -> IO (SFloat sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> Integer -> Integer -> IO (SWord sym)
forall sym.
IsExprBuilder sym =>
sym -> Integer -> Integer -> IO (SWord sym)
SW.bvLit (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) (Integer
eInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
p) (Integer -> Integer -> BigFloat -> Integer
floatToBits Integer
e Integer
p BigFloat
bf))

  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 = IO (SymExpr sym BaseBoolType)
-> W4Eval sym (SymExpr sym BaseBoolType)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym BaseBoolType)
 -> W4Eval sym (SymExpr sym BaseBoolType))
-> IO (SymExpr sym BaseBoolType)
-> W4Eval sym (SymExpr sym BaseBoolType)
forall a b. (a -> b) -> a -> b
$ SFloatRel sym
forall sym. IsExprBuilder sym => SFloatRel sym
FP.fpEqIEEE (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SFloat sym
SFloat (What4 sym)
x SFloat sym
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 = IO (SymExpr sym BaseBoolType)
-> W4Eval sym (SymExpr sym BaseBoolType)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym BaseBoolType)
 -> W4Eval sym (SymExpr sym BaseBoolType))
-> IO (SymExpr sym BaseBoolType)
-> W4Eval sym (SymExpr sym BaseBoolType)
forall a b. (a -> b) -> a -> b
$ SFloatRel sym
forall sym. IsExprBuilder sym => SFloatRel sym
FP.fpLtIEEE (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SFloat sym
SFloat (What4 sym)
x SFloat sym
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 = IO (SymExpr sym BaseBoolType)
-> W4Eval sym (SymExpr sym BaseBoolType)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym BaseBoolType)
 -> W4Eval sym (SymExpr sym BaseBoolType))
-> IO (SymExpr sym BaseBoolType)
-> W4Eval sym (SymExpr sym BaseBoolType)
forall a b. (a -> b) -> a -> b
$ SFloatRel sym
forall sym. IsExprBuilder sym => SFloatRel sym
FP.fpGtIEEE (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SFloat sym
SFloat (What4 sym)
x SFloat sym
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 = IO (SymExpr sym BaseBoolType)
-> W4Eval sym (SymExpr sym BaseBoolType)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym BaseBoolType)
 -> W4Eval sym (SymExpr sym BaseBoolType))
-> IO (SymExpr sym BaseBoolType)
-> W4Eval sym (SymExpr sym BaseBoolType)
forall a b. (a -> b) -> a -> b
$ SFloatRel sym
forall sym. IsExprBuilder sym => SFloatRel sym
FP.fpEq (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SFloat sym
SFloat (What4 sym)
x SFloat sym
SFloat (What4 sym)
y

  fpPlus :: FPArith2 (What4 sym)
fpPlus  = SFloatBinArith sym -> FPArith2 (What4 sym)
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
forall sym. IsExprBuilder sym => SFloatBinArith sym
FP.fpAdd
  fpMinus :: FPArith2 (What4 sym)
fpMinus = SFloatBinArith sym -> FPArith2 (What4 sym)
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
forall sym. IsExprBuilder sym => SFloatBinArith sym
FP.fpSub
  fpMult :: FPArith2 (What4 sym)
fpMult  = SFloatBinArith sym -> FPArith2 (What4 sym)
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
forall sym. IsExprBuilder sym => SFloatBinArith sym
FP.fpMul
  fpDiv :: FPArith2 (What4 sym)
fpDiv   = SFloatBinArith sym -> FPArith2 (What4 sym)
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
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 = IO (SFloat sym) -> W4Eval sym (SFloat sym)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SFloat sym) -> W4Eval sym (SFloat sym))
-> IO (SFloat sym) -> W4Eval sym (SFloat sym)
forall a b. (a -> b) -> a -> b
$ sym -> SFloat sym -> IO (SFloat sym)
forall sym.
IsExprBuilder sym =>
sym -> SFloat sym -> IO (SFloat sym)
FP.fpNeg (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SFloat 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 <- What4 sym -> SWord (What4 sym) -> SEval (What4 sym) RoundingMode
forall sym.
IsSymExprBuilder sym =>
What4 sym -> SWord (What4 sym) -> SEval (What4 sym) RoundingMode
fpRoundingMode What4 sym
sym SWord (What4 sym)
r
       IO (SFloat sym) -> W4Eval sym (SFloat sym)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SFloat sym) -> W4Eval sym (SFloat sym))
-> IO (SFloat sym) -> W4Eval sym (SFloat sym)
forall a b. (a -> b) -> a -> b
$ sym
-> Integer
-> Integer
-> RoundingMode
-> SymExpr sym BaseIntegerType
-> IO (SFloat sym)
forall sym.
IsExprBuilder sym =>
sym
-> Integer
-> Integer
-> RoundingMode
-> SymInteger sym
-> IO (SFloat sym)
FP.fpFromInteger (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) Integer
e Integer
p RoundingMode
rm SymExpr sym BaseIntegerType
SInteger (What4 sym)
x

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

sModAdd :: W4.IsSymExprBuilder sym =>
  sym -> Integer -> W4.SymInteger sym -> W4.SymInteger sym -> IO (W4.SymInteger sym)
sModAdd :: sym
-> Integer
-> SymInteger sym
-> SymInteger sym
-> IO (SymInteger sym)
sModAdd sym
_sym Integer
0 SymInteger sym
_ SymInteger sym
_ = String -> [String] -> IO (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 <- SymInteger sym -> Maybe Integer
forall (e :: BaseType -> *).
IsExpr e =>
e BaseIntegerType -> Maybe Integer
W4.asInteger SymInteger sym
x
  , Just Integer
yi <- SymInteger sym -> Maybe Integer
forall (e :: BaseType -> *).
IsExpr e =>
e BaseIntegerType -> Maybe Integer
W4.asInteger SymInteger sym
y
  = sym -> Integer -> IO (SymInteger sym)
forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
W4.intLit sym
sym ((Integer
xiInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
yi) Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
m)

  | Bool
otherwise
  = sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
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 :: sym
-> Integer
-> SymInteger sym
-> SymInteger sym
-> IO (SymInteger sym)
sModSub sym
_sym Integer
0 SymInteger sym
_ SymInteger sym
_ = String -> [String] -> IO (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 <- SymInteger sym -> Maybe Integer
forall (e :: BaseType -> *).
IsExpr e =>
e BaseIntegerType -> Maybe Integer
W4.asInteger SymInteger sym
x
  , Just Integer
yi <- SymInteger sym -> Maybe Integer
forall (e :: BaseType -> *).
IsExpr e =>
e BaseIntegerType -> Maybe Integer
W4.asInteger SymInteger sym
y
  = sym -> Integer -> IO (SymInteger sym)
forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
W4.intLit sym
sym ((Integer
xiInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
yi) Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
m)

  | Bool
otherwise
  = sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
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 :: sym
-> Integer
-> SymInteger sym
-> SymInteger sym
-> IO (SymInteger sym)
sModMult sym
_sym Integer
0 SymInteger sym
_ SymInteger sym
_ = String -> [String] -> IO (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 <- SymInteger sym -> Maybe Integer
forall (e :: BaseType -> *).
IsExpr e =>
e BaseIntegerType -> Maybe Integer
W4.asInteger SymInteger sym
x
  , Just Integer
yi <- SymInteger sym -> Maybe Integer
forall (e :: BaseType -> *).
IsExpr e =>
e BaseIntegerType -> Maybe Integer
W4.asInteger SymInteger sym
y
  = sym -> Integer -> IO (SymInteger sym)
forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
W4.intLit sym
sym ((Integer
xiInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
*Integer
yi) Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
m)

  | Bool
otherwise
  = sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
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 :: sym -> Integer -> SymInteger sym -> IO (SymInteger sym)
sModNegate sym
_sym Integer
0 SymInteger sym
_ = String -> [String] -> IO (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 <- SymInteger sym -> Maybe Integer
forall (e :: BaseType -> *).
IsExpr e =>
e BaseIntegerType -> Maybe Integer
W4.asInteger SymInteger sym
x
  = sym -> Integer -> IO (SymInteger sym)
forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
W4.intLit sym
sym ((Integer -> Integer
forall a. Num a => a -> a
negate Integer
xi) Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
m)

  | Bool
otherwise
  = sym -> SymInteger sym -> IO (SymInteger sym)
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 :: sym -> SWord sym -> SEval (What4 sym) (SWord sym)
sLg2 sym
sym SWord sym
x = IO (SWord sym) -> W4Eval sym (SWord sym)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SWord sym) -> W4Eval sym (SWord sym))
-> IO (SWord sym) -> W4Eval sym (SWord sym)
forall a b. (a -> b) -> a -> b
$ Int -> IO (SWord sym)
go Int
0
  where
  w :: Integer
w = SWord sym -> Integer
forall sym. SWord sym -> Integer
SW.bvWidth SWord sym
x
  lit :: Int -> IO (SWord sym)
lit Int
n = sym -> Integer -> Integer -> IO (SWord sym)
forall sym.
IsExprBuilder sym =>
sym -> Integer -> Integer -> IO (SWord sym)
SW.bvLit sym
sym Integer
w (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
n)

  go :: Int -> IO (SWord sym)
go Int
i | Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
w =
       do SymExpr sym BaseBoolType
p <- sym -> SWord sym -> SWord sym -> IO (SymExpr sym BaseBoolType)
PredBin
SW.bvule sym
sym SWord sym
x (SWord sym -> IO (SymExpr sym BaseBoolType))
-> IO (SWord sym) -> IO (SymExpr sym BaseBoolType)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Int -> IO (SWord sym)
lit (Int -> Int
forall a. Bits a => Int -> a
bit Int
i)
          (SymExpr sym BaseBoolType
 -> SWord sym -> SWord sym -> IO (SWord sym))
-> SymExpr sym BaseBoolType
-> IO (SWord sym)
-> IO (SWord sym)
-> IO (SWord sym)
forall (p :: BaseType -> *) (m :: * -> *) a.
(IsExpr p, Monad m) =>
(p BaseBoolType -> a -> a -> m a)
-> p BaseBoolType -> m a -> m a -> m a
lazyIte (sym
-> SymExpr sym BaseBoolType
-> SWord sym
-> SWord sym
-> IO (SWord sym)
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
iInt -> Int -> Int
forall 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 :: String -> [String] -> a
evalPanic String
cxt = String -> [String] -> a
forall a. HasCallStack => String -> [String] -> a
panic (String
"[What4] " String -> String -> String
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 :: (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 <- p BaseBoolType -> Maybe Bool
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 :: sym -> SWord sym -> SWord sym -> W4Eval sym (SWord sym)
w4bvShl sym
sym SWord sym
x SWord sym
y = IO (SWord sym) -> W4Eval sym (SWord sym)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SWord sym) -> W4Eval sym (SWord sym))
-> IO (SWord sym) -> W4Eval sym (SWord sym)
forall a b. (a -> b) -> a -> b
$ sym -> SWord sym -> SWord sym -> IO (SWord sym)
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 :: sym -> SWord sym -> SWord sym -> W4Eval sym (SWord sym)
w4bvLshr sym
sym SWord sym
x SWord sym
y = IO (SWord sym) -> W4Eval sym (SWord sym)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SWord sym) -> W4Eval sym (SWord sym))
-> IO (SWord sym) -> W4Eval sym (SWord sym)
forall a b. (a -> b) -> a -> b
$ sym -> SWord sym -> SWord sym -> IO (SWord sym)
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 :: sym -> SWord sym -> SWord sym -> W4Eval sym (SWord sym)
w4bvAshr sym
sym SWord sym
x SWord sym
y = IO (SWord sym) -> W4Eval sym (SWord sym)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SWord sym) -> W4Eval sym (SWord sym))
-> IO (SWord sym) -> W4Eval sym (SWord sym)
forall a b. (a -> b) -> a -> b
$ sym -> SWord sym -> SWord sym -> IO (SWord sym)
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 :: sym -> SWord sym -> SWord sym -> W4Eval sym (SWord sym)
w4bvRol sym
sym SWord sym
x SWord sym
y = IO (SWord sym) -> W4Eval sym (SWord sym)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SWord sym) -> W4Eval sym (SWord sym))
-> IO (SWord sym) -> W4Eval sym (SWord sym)
forall a b. (a -> b) -> a -> b
$ sym -> SWord sym -> SWord sym -> IO (SWord sym)
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 :: sym -> SWord sym -> SWord sym -> W4Eval sym (SWord sym)
w4bvRor sym
sym SWord sym
x SWord sym
y = IO (SWord sym) -> W4Eval sym (SWord sym)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SWord sym) -> W4Eval sym (SWord sym))
-> IO (SWord sym) -> W4Eval sym (SWord sym)
forall a b. (a -> b) -> a -> b
$ sym -> SWord sym -> SWord sym -> IO (SWord sym)
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 :: What4 sym -> SWord (What4 sym) -> SEval (What4 sym) RoundingMode
fpRoundingMode What4 sym
sym SWord (What4 sym)
v =
  case What4 sym -> SWord (What4 sym) -> Maybe (Integer, Integer)
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 -> RoundingMode -> W4Eval sym RoundingMode
forall (f :: * -> *) a. Applicative f => a -> f a
pure RoundingMode
W4.RNE
        Integer
1 -> RoundingMode -> W4Eval sym RoundingMode
forall (f :: * -> *) a. Applicative f => a -> f a
pure RoundingMode
W4.RNA
        Integer
2 -> RoundingMode -> W4Eval sym RoundingMode
forall (f :: * -> *) a. Applicative f => a -> f a
pure RoundingMode
W4.RTP
        Integer
3 -> RoundingMode -> W4Eval sym RoundingMode
forall (f :: * -> *) a. Applicative f => a -> f a
pure RoundingMode
W4.RTN
        Integer
4 -> RoundingMode -> W4Eval sym RoundingMode
forall (f :: * -> *) a. Applicative f => a -> f a
pure RoundingMode
W4.RTZ
        Integer
x -> What4 sym -> EvalError -> SEval (What4 sym) RoundingMode
forall sym a. Backend sym => sym -> EvalError -> SEval sym a
raiseError What4 sym
sym (Integer -> EvalError
BadRoundingMode Integer
x)
    Maybe (Integer, Integer)
_ -> IO RoundingMode -> W4Eval sym RoundingMode
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO RoundingMode -> W4Eval sym RoundingMode)
-> IO RoundingMode -> W4Eval sym RoundingMode
forall a b. (a -> b) -> a -> b
$ Unsupported -> IO RoundingMode
forall e a. Exception e => e -> IO a
X.throwIO (Unsupported -> IO RoundingMode) -> Unsupported -> IO RoundingMode
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 :: 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 <- What4 sym -> SWord (What4 sym) -> SEval (What4 sym) RoundingMode
forall sym.
IsSymExprBuilder sym =>
What4 sym -> SWord (What4 sym) -> SEval (What4 sym) RoundingMode
fpRoundingMode What4 sym
sym SWord (What4 sym)
r
     IO (SFloat sym) -> W4Eval sym (SFloat sym)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (SFloatBinArith sym
fun (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) RoundingMode
m SFloat sym
SFloat (What4 sym)
x SFloat sym
SFloat (What4 sym)
y)


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


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

fpCvtFromRational ::
  (W4.IsSymExprBuilder sy, sym ~ What4 sy) =>
  sym -> Integer -> Integer -> SWord sym ->
  SRational sym -> SEval sym (SFloat sym)
fpCvtFromRational :: 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 <- What4 sy -> SWord (What4 sy) -> SEval (What4 sy) RoundingMode
forall sym.
IsSymExprBuilder sym =>
What4 sym -> SWord (What4 sym) -> SEval (What4 sym) RoundingMode
fpRoundingMode sym
What4 sy
sym SWord sym
SWord (What4 sy)
r
     IO (SFloat sy) -> W4Eval sy (SFloat sy)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (sy
-> Integer
-> Integer
-> RoundingMode
-> SymInteger sy
-> SymInteger sy
-> IO (SFloat sy)
forall sym.
IsExprBuilder sym =>
sym
-> Integer
-> Integer
-> RoundingMode
-> SymInteger sym
-> SymInteger sym
-> IO (SFloat sym)
FP.fpFromRational (What4 sy -> sy
forall sym. What4 sym -> sym
w4 sym
What4 sy
sym) Integer
e Integer
p RoundingMode
rnd (SRational sym -> SInteger sym
forall sym. SRational sym -> SInteger sym
sNum SRational sym
rat) (SRational sym -> SInteger sym
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 :: What4 sym
-> Integer -> SymInteger sym -> W4Eval sym (SymInteger sym)
sModRecip What4 sym
_sym Integer
0 SymInteger sym
_ = String -> [String] -> W4Eval sym (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 <- SymInteger sym -> Maybe Integer
forall (e :: BaseType -> *).
IsExpr e =>
e BaseIntegerType -> Maybe Integer
W4.asInteger SymInteger sym
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 What4 sym -> EvalError -> SEval (What4 sym) (SymInteger sym)
forall sym a. Backend sym => sym -> EvalError -> SEval sym a
raiseError What4 sym
sym EvalError
DivideByZero else What4 sym -> Integer -> SEval (What4 sym) (SInteger (What4 sym))
forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit What4 sym
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 SymExpr sym BaseBoolType
divZero <- IO (SymExpr sym BaseBoolType)
-> W4Eval sym (SymExpr sym BaseBoolType)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (sym -> SymInteger sym -> Natural -> IO (SymExpr sym BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> Natural -> IO (Pred sym)
W4.intDivisible (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SymInteger sym
x (Integer -> Natural
forall a. Num a => Integer -> a
fromInteger Integer
m))
       SymExpr sym BaseBoolType
ok <- IO (SymExpr sym BaseBoolType)
-> W4Eval sym (SymExpr sym BaseBoolType)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (sym -> SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType)
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
W4.notPred (What4 sym -> sym
forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym BaseBoolType
divZero)
       What4 sym -> SBit (What4 sym) -> EvalError -> SEval (What4 sym) ()
forall sym.
Backend sym =>
sym -> SBit sym -> EvalError -> SEval sym ()
assertSideCondition What4 sym
sym SymExpr sym BaseBoolType
SBit (What4 sym)
ok EvalError
DivideByZero

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

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