-- |
-- 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
  { w4  :: sym
  , w4defs :: MVar (W4.Pred sym)
  , w4funs :: MVar (What4FunCache sym)
  , 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 { 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 { 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 (W4Conn m)) = m

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

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

-- | A total value.
total :: W4.IsSymExprBuilder sym => W4Conn sym a -> W4Eval sym a
total m = W4Eval
  do sym <- getSym
     W4Result (W4.backendPred sym True) <$> m

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

instance W4.IsSymExprBuilder sym => Functor (W4Conn sym) where
  fmap = liftM

instance W4.IsSymExprBuilder sym => Applicative (W4Conn sym) where
  pure   = doEval . pure
  (<*>)  = ap

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

instance W4.IsSymExprBuilder sym => MonadIO (W4Conn sym) where
  liftIO = doEval . liftIO

-- | Access the symbolic back-end
getSym :: W4Conn sym sym
getSym = W4Conn \sym -> pure 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 p q =
  do sym <- getSym
     liftIO (W4.andPred sym p q)

-- | Compute negation.
w4Not :: W4.IsSymExprBuilder sym => W4.Pred sym -> W4Conn sym (W4.Pred sym)
w4Not p =
  do sym <- getSym
     liftIO (W4.notPred 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 ifP ifThen ifElse =
  do sym <- getSym
     liftIO (W4.itePred sym ifP ifThen ifElse)



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

instance W4.IsSymExprBuilder sym => Functor (W4Eval sym) where
  fmap = liftM

instance W4.IsSymExprBuilder sym => Applicative (W4Eval sym) where
  pure  = total . pure
  (<*>) = ap

instance W4.IsSymExprBuilder sym => Monad (W4Eval sym) where
  m1 >>= f = W4Eval
    do res1 <- evalPartial m1
       case res1 of
         W4Error err -> pure (W4Error err)
         W4Result px x' ->
           do res2 <- evalPartial (f x')
              case res2 of
                W4Result py y ->
                  do pz <- w4And px py
                     pure (W4Result pz y)
                W4Error _ -> pure res2

instance W4.IsSymExprBuilder sym => MonadIO (W4Eval sym) where
  liftIO = total . 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 sym p =
  liftIO (modifyMVar_ (w4defs sym) (W4.andPred (w4 sym) p))

-- | Add s safety condition.
addSafety :: W4.IsSymExprBuilder sym => W4.Pred sym -> W4Eval sym ()
addSafety p = W4Eval (pure (W4Result p ()))

-- | A fully undefined symbolic value
evalError :: W4.IsSymExprBuilder sym => EvalError -> W4Eval sym a
evalError err = W4Eval (pure (W4Error err))

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


assertBVDivisor :: W4.IsSymExprBuilder sym => What4 sym -> SW.SWord sym -> W4Eval sym ()
assertBVDivisor sym x =
  do p <- liftIO (SW.bvIsNonzero (w4 sym) x)
     assertSideCondition sym p DivideByZero

assertIntDivisor ::
  W4.IsSymExprBuilder sym => What4 sym -> W4.SymInteger sym -> W4Eval sym ()
assertIntDivisor sym x =
  do p <- liftIO (W4.notPred (w4 sym) =<< W4.intEq (w4 sym) x =<< W4.intLit (w4 sym) 0)
     assertSideCondition sym p 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 _ = evalError

  assertSideCondition _ cond err
    | Just False <- W4.asConstantPred cond = evalError err
    | otherwise = addSafety cond

  isReady sym m =
    case w4Eval m (w4 sym) of
      Ready _ -> True
      _ -> False

  sDelayFill _ m retry =
    total
    do sym <- getSym
       doEval (w4Thunk <$> delayFill (w4Eval m sym) (w4Eval retry sym))

  sSpark _ m =
    total
    do sym   <- getSym
       doEval (w4Thunk <$> evalSpark (w4Eval m sym))


  sDeclareHole _ msg =
    total
    do (hole, fill) <- doEval (blackhole msg)
       pure ( w4Thunk hole
            , \m -> total
                    do sym <- getSym
                       doEval (fill (w4Eval m sym))
            )

  mergeEval _sym f c mx my = W4Eval
    do rx <- evalPartial mx
       ry <- evalPartial my
       case (rx, ry) of

         (W4Error err, W4Error _) ->
           pure (W4Error err) -- arbitrarily choose left error to report

         (W4Error _, W4Result p y) ->
           do p' <- w4And p =<< w4Not c
              pure (W4Result p' y)

         (W4Result p x, W4Error _) ->
           do p' <- w4And p c
              pure (W4Result p' x)

         (W4Result px x, W4Result py y) ->
           do zr <- evalPartial (f c x y)
              case zr of
                W4Error err -> pure $ W4Error err
                W4Result pz z ->
                  do p' <- w4And pz =<< w4ITE c px py
                     pure (W4Result p' z)

  wordAsChar _ bv
    | SW.bvWidth bv == 8 = toEnum . fromInteger <$> SW.bvAsUnsignedInteger bv
    | otherwise = Nothing

  wordLen _ bv = SW.bvWidth bv

  bitLit sym b = W4.backendPred (w4 sym) b
  bitAsLit _ v = W4.asConstantPred v

  wordLit sym intw i
    | Just (Some w) <- someNat intw
    = case isPosNat w of
        Nothing -> pure $ SW.ZBV
        Just LeqProof -> SW.DBV <$> liftIO (W4.bvLit (w4 sym) w (BV.mkBV w i))
    | otherwise = panic "what4: wordLit" ["invalid bit width:", show intw ]

  wordAsLit _ v
    | Just x <- SW.bvAsUnsignedInteger v = Just (SW.bvWidth v, x)
    | otherwise = Nothing

  integerLit sym i = liftIO (W4.intLit (w4 sym) i)

  integerAsLit _ v = W4.asInteger v

  ppBit _ v
    | Just b <- W4.asConstantPred v = text $! if b then "True" else "False"
    | otherwise                     = text "?"

  ppWord _ opts v
    | Just x <- SW.bvAsUnsignedInteger v
    = ppBV opts (BV (SW.bvWidth v) x)

    | otherwise = text "[?]"

  ppInteger _ _opts v
    | Just x <- W4.asInteger v = integer x
    | otherwise = text "[?]"

  ppFloat _ _opts _ = text "[?]"

  iteBit sym c x y = liftIO (W4.itePred (w4 sym) c x y)
  iteWord sym c x y = liftIO (SW.bvIte (w4 sym) c x y)
  iteInteger sym c x y = liftIO (W4.intIte (w4 sym) c x y)

  bitEq  sym x y = liftIO (W4.eqPred (w4 sym) x y)
  bitAnd sym x y = liftIO (W4.andPred (w4 sym) x y)
  bitOr  sym x y = liftIO (W4.orPred (w4 sym) x y)
  bitXor sym x y = liftIO (W4.xorPred (w4 sym) x y)
  bitComplement sym x = liftIO (W4.notPred (w4 sym) x)

  wordBit sym bv idx = liftIO (SW.bvAtBE (w4 sym) bv idx)
  wordUpdate sym bv idx b = liftIO (SW.bvSetBE (w4 sym) bv idx b)

  packWord sym bs =
    do z <- wordLit sym (genericLength bs) 0
       let f w (idx,b) = wordUpdate sym w idx b
       foldM f z (zip [0..] bs)

  unpackWord sym bv = liftIO $
    mapM (SW.bvAtBE (w4 sym) bv) [0 .. SW.bvWidth bv-1]

  joinWord sym x y = liftIO $ SW.bvJoin (w4 sym) x y

  splitWord _sym 0 _ bv = pure (SW.ZBV, bv)
  splitWord _sym _ 0 bv = pure (bv, SW.ZBV)
  splitWord sym lw rw bv = liftIO $
    do l <- SW.bvSliceBE (w4 sym) 0 lw bv
       r <- SW.bvSliceBE (w4 sym) lw rw bv
       return (l, r)

  extractWord sym bits idx bv =
    liftIO $ SW.bvSliceLE (w4 sym) idx bits bv

  wordEq                sym x y = liftIO (SW.bvEq  (w4 sym) x y)
  wordLessThan          sym x y = liftIO (SW.bvult (w4 sym) x y)
  wordGreaterThan       sym x y = liftIO (SW.bvugt (w4 sym) x y)
  wordSignedLessThan    sym x y = liftIO (SW.bvslt (w4 sym) x y)

  wordOr  sym x y = liftIO (SW.bvOr  (w4 sym) x y)
  wordAnd sym x y = liftIO (SW.bvAnd (w4 sym) x y)
  wordXor sym x y = liftIO (SW.bvXor (w4 sym) x y)
  wordComplement sym x = liftIO (SW.bvNot (w4 sym) x)

  wordPlus   sym x y = liftIO (SW.bvAdd (w4 sym) x y)
  wordMinus  sym x y = liftIO (SW.bvSub (w4 sym) x y)
  wordMult   sym x y = liftIO (SW.bvMul (w4 sym) x y)
  wordNegate sym x   = liftIO (SW.bvNeg (w4 sym) x)
  wordLg2    sym x   = sLg2 (w4 sym) x
 
  wordDiv sym x y =
     do assertBVDivisor sym y
        liftIO (SW.bvUDiv (w4 sym) x y)
  wordMod sym x y =
     do assertBVDivisor sym y
        liftIO (SW.bvURem (w4 sym) x y)
  wordSignedDiv sym x y =
     do assertBVDivisor sym y
        liftIO (SW.bvSDiv (w4 sym) x y)
  wordSignedMod sym x y =
     do assertBVDivisor sym y
        liftIO (SW.bvSRem (w4 sym) x y)

  wordToInt sym x = liftIO (SW.bvToInteger (w4 sym) x)
  wordFromInt sym width i = liftIO (SW.integerToBV (w4 sym) i width)

  intPlus   sym x y  = liftIO $ W4.intAdd (w4 sym) x y
  intMinus  sym x y  = liftIO $ W4.intSub (w4 sym) x y
  intMult   sym x y  = liftIO $ W4.intMul (w4 sym) x y
  intNegate sym x    = liftIO $ W4.intNeg (w4 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 sym x y =
    do assertIntDivisor sym y
       liftIO $ do
         neg <- liftIO (W4.intLt (w4 sym) y =<< W4.intLit (w4 sym) 0)
         case W4.asConstantPred neg of
           Just False -> W4.intDiv (w4 sym) x y
           Just True  ->
              do xneg <- W4.intNeg (w4 sym) x
                 yneg <- W4.intNeg (w4 sym) y
                 W4.intDiv (w4 sym) xneg yneg
           Nothing ->
              do xneg <- W4.intNeg (w4 sym) x
                 yneg <- W4.intNeg (w4 sym) y
                 zneg <- W4.intDiv (w4 sym) xneg yneg
                 z    <- W4.intDiv (w4 sym) x y
                 W4.intIte (w4 sym) neg zneg 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 sym x y =
    do assertIntDivisor sym y
       liftIO $ do
         neg <- liftIO (W4.intLt (w4 sym) y =<< W4.intLit (w4 sym) 0)
         case W4.asConstantPred neg of
           Just False -> W4.intMod (w4 sym) x y
           Just True  ->
              do xneg <- W4.intNeg (w4 sym) x
                 yneg <- W4.intNeg (w4 sym) y
                 W4.intNeg (w4 sym) =<< W4.intMod (w4 sym) xneg yneg
           Nothing ->
              do xneg <- W4.intNeg (w4 sym) x
                 yneg <- W4.intNeg (w4 sym) y
                 z    <- W4.intMod (w4 sym) x y
                 zneg <- W4.intNeg (w4 sym) =<< W4.intMod (w4 sym) xneg yneg
                 W4.intIte (w4 sym) neg zneg z

  intEq sym x y = liftIO $ W4.intEq (w4 sym) x y
  intLessThan sym x y = liftIO $ W4.intLt (w4 sym) x y
  intGreaterThan sym x y = liftIO $ W4.intLt (w4 sym) y x

  -- NB, we don't do reduction here on symbolic values
  intToZn sym m x
    | Just xi <- W4.asInteger x
    = liftIO $ W4.intLit (w4 sym) (xi `mod` m)

    | otherwise
    = pure x

  znToInt _ 0 _ = evalPanic "znToInt" ["0 modulus not allowed"]
  znToInt sym m x = liftIO (W4.intMod (w4 sym) x =<< W4.intLit (w4 sym) m)

  znEq _ 0 _ _ = evalPanic "znEq" ["0 modulus not allowed"]
  znEq sym m x y = liftIO $
     do diff <- W4.intSub (w4 sym) x y
        W4.intDivisible (w4 sym) diff (fromInteger m)

  znPlus   sym m x y = liftIO $ sModAdd (w4 sym) m x y
  znMinus  sym m x y = liftIO $ sModSub (w4 sym) m x y
  znMult   sym m x y = liftIO $ sModMult (w4 sym) m x y
  znNegate sym m x   = liftIO $ sModNegate (w4 sym) m x
  znRecip = sModRecip

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

  fpLit sym e p r = liftIO $ FP.fpFromRationalLit (w4 sym) e p r

  fpExactLit sym BF{ bfExpWidth = e, bfPrecWidth = p, bfValue = bf } =
    liftIO (FP.fpFromBinary (w4 sym) e p =<< SW.bvLit (w4 sym) (e+p) (floatToBits e p bf))

  fpEq          sym x y = liftIO $ FP.fpEqIEEE (w4 sym) x y
  fpLessThan    sym x y = liftIO $ FP.fpLtIEEE (w4 sym) x y
  fpGreaterThan sym x y = liftIO $ FP.fpGtIEEE (w4 sym) x y
  fpLogicalEq   sym x y = liftIO $ FP.fpEq (w4 sym) x y

  fpPlus  = fpBinArith FP.fpAdd
  fpMinus = fpBinArith FP.fpSub
  fpMult  = fpBinArith FP.fpMul
  fpDiv   = fpBinArith FP.fpDiv

  fpNeg sym x = liftIO $ FP.fpNeg (w4 sym) x

  fpFromInteger sym e p r x =
    do rm <- fpRoundingMode sym r
       liftIO $ FP.fpFromInteger (w4 sym) e p rm x

  fpToInteger = fpCvtToInteger

sModAdd :: W4.IsSymExprBuilder sym =>
  sym -> Integer -> W4.SymInteger sym -> W4.SymInteger sym -> IO (W4.SymInteger sym)
sModAdd _sym 0 _ _ = evalPanic "sModAdd" ["0 modulus not allowed"]
sModAdd sym m x y
  | Just xi <- W4.asInteger x
  , Just yi <- W4.asInteger y
  = W4.intLit sym ((xi+yi) `mod` m)

  | otherwise
  = W4.intAdd sym x y

sModSub :: W4.IsSymExprBuilder sym =>
  sym -> Integer -> W4.SymInteger sym -> W4.SymInteger sym -> IO (W4.SymInteger sym)
sModSub _sym 0 _ _ = evalPanic "sModSub" ["0 modulus not allowed"]
sModSub sym m x y
  | Just xi <- W4.asInteger x
  , Just yi <- W4.asInteger y
  = W4.intLit sym ((xi-yi) `mod` m)

  | otherwise
  = W4.intSub sym x y


sModMult :: W4.IsSymExprBuilder sym =>
  sym -> Integer -> W4.SymInteger sym -> W4.SymInteger sym -> IO (W4.SymInteger sym)
sModMult _sym 0 _ _ = evalPanic "sModMult" ["0 modulus not allowed"]
sModMult sym m x y
  | Just xi <- W4.asInteger x
  , Just yi <- W4.asInteger y
  = W4.intLit sym ((xi*yi) `mod` m)

  | otherwise
  = W4.intMul sym x y

sModNegate :: W4.IsSymExprBuilder sym =>
  sym -> Integer -> W4.SymInteger sym -> IO (W4.SymInteger sym)
sModNegate _sym 0 _ = evalPanic "sModMult" ["0 modulus not allowed"]
sModNegate sym m x
  | Just xi <- W4.asInteger x
  = W4.intLit sym ((negate xi) `mod` m)

  | otherwise
  = W4.intNeg 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 x = liftIO $ go 0
  where
  w = SW.bvWidth x
  lit n = SW.bvLit sym w (toInteger n)

  go i | toInteger i < w =
       do p <- SW.bvule sym x =<< lit (bit i)
          lazyIte (SW.bvIte sym) p (lit i) (go (i+1))

  -- base case, should only happen when i = w
  go i = lit i



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

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

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

w4bvShl  :: W4.IsSymExprBuilder sym => sym -> SW.SWord sym -> SW.SWord sym -> W4Eval sym (SW.SWord sym)
w4bvShl sym x y = liftIO $ SW.bvShl sym x y

w4bvLshr  :: W4.IsSymExprBuilder sym => sym -> SW.SWord sym -> SW.SWord sym -> W4Eval sym (SW.SWord sym)
w4bvLshr sym x y = liftIO $ SW.bvLshr sym x y

w4bvAshr :: W4.IsSymExprBuilder sym => sym -> SW.SWord sym -> SW.SWord sym -> W4Eval sym (SW.SWord sym)
w4bvAshr sym x y = liftIO $ SW.bvAshr sym x y

w4bvRol  :: W4.IsSymExprBuilder sym => sym -> SW.SWord sym -> SW.SWord sym -> W4Eval sym (SW.SWord sym)
w4bvRol sym x y = liftIO $ SW.bvRol sym x y

w4bvRor  :: W4.IsSymExprBuilder sym => sym -> SW.SWord sym -> SW.SWord sym -> W4Eval sym (SW.SWord sym)
w4bvRor sym x y = liftIO $ SW.bvRor sym x y



fpRoundingMode ::
  W4.IsSymExprBuilder sym =>
  What4 sym -> SWord (What4 sym) -> SEval (What4 sym) W4.RoundingMode
fpRoundingMode sym v =
  case wordAsLit sym v of
    Just (_w,i) ->
      case i of
        0 -> pure W4.RNE
        1 -> pure W4.RNA
        2 -> pure W4.RTP
        3 -> pure W4.RTN
        4 -> pure W4.RTZ
        x -> raiseError sym (BadRoundingMode x)
    _ -> liftIO $ X.throwIO $ UnsupportedSymbolicOp "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 fun = \sym r x y ->
  do m <- fpRoundingMode sym r
     liftIO (fun (w4 sym) m x y)


fpCvtToInteger ::
  (W4.IsSymExprBuilder sy, sym ~ What4 sy) =>
  sym -> String -> SWord sym -> SFloat sym -> SEval sym (SInteger sym)
fpCvtToInteger sym fun r x =
  do grd <- liftIO
              do bad1 <- FP.fpIsInf (w4 sym) x
                 bad2 <- FP.fpIsNaN (w4 sym) x
                 W4.notPred (w4 sym) =<< W4.orPred (w4 sym) bad1 bad2
     assertSideCondition sym grd (BadValue fun)
     rnd  <- fpRoundingMode sym r
     liftIO
       do y <- FP.fpToReal (w4 sym) x
          case rnd of
            W4.RNE -> W4.realRoundEven (w4 sym) y
            W4.RNA -> W4.realRound (w4 sym) y
            W4.RTP -> W4.realCeil (w4 sym) y
            W4.RTN -> W4.realFloor (w4 sym) y
            W4.RTZ -> W4.realTrunc (w4 sym) y


fpCvtToRational ::
  (W4.IsSymExprBuilder sy, sym ~ What4 sy) =>
  sym -> SFloat sym -> SEval sym (SRational sym)
fpCvtToRational sym fp =
  do grd <- liftIO
            do bad1 <- FP.fpIsInf (w4 sym) fp
               bad2 <- FP.fpIsNaN (w4 sym) fp
               W4.notPred (w4 sym) =<< W4.orPred (w4 sym) bad1 bad2
     assertSideCondition sym grd (BadValue "fpToRational")
     (rel,x,y) <- liftIO (FP.fpToRational (w4 sym) fp)
     addDefEqn sym =<< liftIO (W4.impliesPred (w4 sym) grd rel)
     ratio sym x y

fpCvtFromRational ::
  (W4.IsSymExprBuilder sy, sym ~ What4 sy) =>
  sym -> Integer -> Integer -> SWord sym ->
  SRational sym -> SEval sym (SFloat sym)
fpCvtFromRational sym e p r rat =
  do rnd <- fpRoundingMode sym r
     liftIO (FP.fpFromRational (w4 sym) e p rnd (sNum rat) (sDenom 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 _sym 0 _ = panic "sModRecip" ["0 modulus not allowed"]
sModRecip sym m x
  -- If the input is concrete, evaluate the answer
  | Just xi <- W4.asInteger x
  = let r = Integer.recipModInteger xi m
     in if r == 0 then raiseError sym DivideByZero else integerLit sym 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.
  | otherwise
  = do divZero <- liftIO (W4.intDivisible (w4 sym) x (fromInteger m))
       ok <- liftIO (W4.notPred (w4 sym) divZero)
       assertSideCondition sym ok DivideByZero

       z <- liftIO (W4.freshBoundedInt (w4 sym) W4.emptySymbol (Just 1) (Just (m-1)))
       xz <- liftIO (W4.intMul (w4 sym) x z)
       rel <- znEq sym m xz =<< liftIO (W4.intLit (w4 sym) 1)
       addDefEqn sym =<< liftIO (W4.orPred (w4 sym) divZero rel)

       return z