Evaluation.hs

-----------------------------------------------------------------------
-- |
-- Module           : Lang.Crucible.Simulator.Evaluation
-- Description      : Evaluation functions for Crucible core expressions
-- Copyright        : (c) Galois, Inc 2014-2016
-- License          : BSD3
-- Maintainer       : Joe Hendrix <jhendrix@galois.com>
-- Stability        : provisional
--
-- This module provides operations evaluating Crucible expressions.
------------------------------------------------------------------------
{-# LANGUAGE DoAndIfThenElse #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}
module Lang.Crucible.Simulator.Evaluation
  ( EvalAppFunc
  , evalApp
  , selectedIndices
  , indexSymbolic
  , integerAsChar
  , complexRealAsChar
  , indexVectorWithSymNat
  , adjustVectorWithSymNat
  , updateVectorWithSymNat
  ) where

import           Prelude hiding (pred)

import qualified Control.Exception as Ex
import           Control.Lens
import           Control.Monad
import qualified Data.BitVector.Sized as BV
import qualified Data.Map.Strict as Map
import           Data.Maybe
import qualified Data.Text as Text
import qualified Data.Vector as V
import           Data.Word
import           Numeric ( showHex )
import           Numeric.Natural
import           GHC.Stack

import           Data.Parameterized.Classes
import           Data.Parameterized.Context as Ctx
import           Data.Parameterized.TraversableFC

import           What4.Interface
import           What4.InterpretedFloatingPoint
import           What4.Partial (pattern PE, pattern Unassigned, joinMaybePE)
import           What4.Utils.Complex
import           What4.WordMap

import           Lang.Crucible.Backend
import           Lang.Crucible.CFG.Expr
import           Lang.Crucible.Simulator.Intrinsics
import           Lang.Crucible.Simulator.RegMap
import           Lang.Crucible.Simulator.SimError
import           Lang.Crucible.Simulator.SymSequence
import           Lang.Crucible.Types

------------------------------------------------------------------------
-- Utilities


-- | Given a list of Booleans l, @selectedIndices@ returns the indices of
-- true values in @l@.
selectedIndices :: [Bool] -> [Natural]
selectedIndices l = catMaybes $ Prelude.zipWith selectIndex l [1..]
  where selectIndex True i  = Just i
        selectIndex False _ = Nothing

------------------------------------------------------------------------
-- Coercion functions

integerAsChar :: Integer -> Word16
integerAsChar i = fromInteger ((i `max` 0) `min` (2^(16::Int)-1))

complexRealAsChar :: (MonadFail m, IsExpr val)
                  => val BaseComplexType
                  -> m Word16
complexRealAsChar v = do
  case cplxExprAsRational v of
    -- Check number is printable.
    Just r | otherwise -> return (integerAsChar (floor r))
    Nothing -> fail "Symbolic value cannot be interpreted as a character."
    -- XXX: Should this be a panic?
    -- XXX: We should move this to crucible-matlab

------------------------------------------------------------------------
-- Evaluating expressions


-- | Helper method for implementing 'indexSymbolic'
indexSymbolic' :: IsSymBackend sym bak
               => bak
               -> (Pred sym -> a -> a -> IO a)
                  -- ^ Function for merging valeus
               -> ([Natural] -> IO a) -- ^ Concrete index function.
               -> [Natural] -- ^ Values of processed indices (in reverse order)
               -> [(Natural,Natural)] -- ^ Bounds on remaining indices.
               -> [SymNat sym] -- ^ Remaining indices.
               -> IO a
indexSymbolic' _ _ f p [] _ = f (reverse p)
indexSymbolic' _ _ f p _ [] = f (reverse p)
indexSymbolic' bak iteFn f p ((l,h):nl) (si:il) = do
  let subIndex idx = indexSymbolic' bak iteFn f (idx:p) nl il
  case asNat si of
    Just i
      | l <= i && i <= h -> subIndex i
      | otherwise ->
          addFailedAssertion bak (AssertFailureSimError msg details)
        where msg = "Index outside matrix dimensions." ++ show (l,i,h)
              details = unwords ["Index", show i, "is outside of range", show (l, h)]
    Nothing ->
      do let sym = backendGetSym bak
         ensureInRange bak l h si "Index outside matrix dimensions."
         let predFn i = natEq sym si =<< natLit sym i
         muxRange predFn iteFn subIndex l h


ensureInRange ::
  IsSymBackend sym bak =>
  bak ->
  Natural ->
  Natural ->
  SymNat sym ->
  String ->
  IO ()
ensureInRange bak l h si msg =
  do let sym = backendGetSym bak
     l_sym <- natLit sym l
     h_sym <- natLit sym h
     inRange <- join $ andPred sym <$> natLe sym l_sym si <*> natLe sym si h_sym
     assert bak inRange (AssertFailureSimError msg details)
  where details = unwords ["Range is", show (l, h)]



-- | Lookup a value in an array that may be at a symbolic offset.
--
-- This function takes a list of symbolic indices as natural numbers
-- along with a pair of lower and upper bounds for each index.
-- It assumes that the indices are all in range.
indexSymbolic :: IsSymBackend sym bak
              => bak
              -> (Pred sym -> a  -> a -> IO a)
                 -- ^ Function for combining results together.
              -> ([Natural] -> IO a) -- ^ Concrete index function.
              -> [(Natural,Natural)] -- ^ High and low bounds at the indices.
              -> [SymNat sym]
              -> IO a
indexSymbolic sym iteFn f = indexSymbolic' sym iteFn f []

-- | Evaluate an indexTermterm to an index value.
evalBase :: IsSymInterface sym =>
            sym
         -> (forall utp . f utp -> IO (RegValue sym utp))
         -> BaseTerm f vtp
         -> IO (SymExpr sym vtp)
evalBase _ evalSub (BaseTerm _tp e) = evalSub e

-- | Get value stored in vector at a symbolic index.
indexVectorWithSymNat :: IsSymBackend sym bak
                      => bak
                      -> (Pred sym -> a -> a -> IO a)
                         -- ^ Ite function
                      -> V.Vector a
                      -> SymNat sym
                      -> IO a
indexVectorWithSymNat bak iteFn v si =
  Ex.assert (n > 0) $
  case asNat si of
    Just i | 0 <= i && i < n -> return (v V.! fromIntegral i)
           | otherwise -> addFailedAssertion bak (AssertFailureSimError msg details)
    Nothing ->
      do let sym = backendGetSym bak
         let predFn i = natEq sym si =<< natLit sym i
         let getElt i = return (v V.! fromIntegral i)
         ensureInRange bak 0 (n - 1) si msg
         muxRange predFn iteFn getElt 0 (n - 1)
  where
  n   = fromIntegral (V.length v)
  msg = "Vector index out of range"
  details = unwords ["Range is", show (0 :: Natural, n)]



-- | Update a vector at a given natural number index.
updateVectorWithSymNat :: IsSymBackend sym bak
                       => bak
                          -- ^ Symbolic backend
                       -> (Pred sym -> a -> a -> IO a)
                          -- ^ Ite function
                       -> V.Vector a
                          -- ^ Vector to update
                       -> SymNat sym
                          -- ^ Index to update
                       -> a
                          -- ^ New value to assign
                       -> IO (V.Vector a)
updateVectorWithSymNat bak iteFn v si new_val = do
  adjustVectorWithSymNat bak iteFn v si (\_ -> return new_val)

-- | Update a vector at a given natural number index.
adjustVectorWithSymNat :: IsSymBackend sym bak
                       => bak
                          -- ^ Symbolic backend
                       -> (Pred sym -> a -> a -> IO a)
                          -- ^ Ite function
                       -> V.Vector a
                          -- ^ Vector to update
                       -> SymNat sym
                          -- ^ Index to update
                       -> (a -> IO a)
                          -- ^ Adjustment function to apply
                       -> IO (V.Vector a)
adjustVectorWithSymNat bak iteFn v si adj =
  case asNat si of
    Just i

      | i < fromIntegral n ->
        do new_val <- adj (v V.! fromIntegral i)
           return $ v V.// [(fromIntegral i, new_val)]

      | otherwise ->
        addFailedAssertion bak $ AssertFailureSimError msg (details i)

    Nothing ->
      do ensureInRange bak 0 (fromIntegral (n-1)) si msg
         V.generateM n setFn
      where
      setFn j =
        do  let sym = backendGetSym bak
            -- Compare si and j.
            c <- natEq sym si =<< natLit sym (fromIntegral j)
            -- Select old value or new value
            case asConstantPred c of
              Just True  -> adj (v V.! j)
              Just False -> return (v V.! j)
              Nothing ->
                do new_val <- adj (v V.! j)
                   iteFn c new_val (v V.! j)

  where
  n = V.length v
  msg = "Illegal vector index"
  details i = "Illegal index " ++ show i ++ "given to updateVectorWithSymNat"

type EvalAppFunc sym app = forall f.
  (forall tp. f tp -> IO (RegValue sym tp)) ->
  (forall tp. app f tp -> IO (RegValue sym tp))

{-# INLINE evalApp #-}
-- | Evaluate the application.
evalApp :: forall sym bak ext.
           IsSymBackend sym bak
        => bak
        -> IntrinsicTypes sym
        -> (Int -> String -> IO ())
           -- ^ Function for logging messages.
        -> EvalAppFunc sym (ExprExtension ext)
        -> EvalAppFunc sym (App ext)
evalApp bak itefns _logFn evalExt (evalSub :: forall tp. f tp -> IO (RegValue sym tp)) a0 = do
  let sym = backendGetSym bak
  case a0 of

    BaseIsEq tp xe ye -> do
      x <- evalBase sym evalSub (BaseTerm tp xe)
      y <- evalBase sym evalSub (BaseTerm tp ye)
      isEq sym x y

    BaseIte tp ce xe ye -> do
      c <- evalSub ce
      case asConstantPred c of
        Just True  -> evalSub xe
        Just False -> evalSub ye
        Nothing -> do
          x <- evalBase sym evalSub (BaseTerm tp xe)
          y <- evalBase sym evalSub (BaseTerm tp ye)
          baseTypeIte sym c x y

    ----------------------------------------------------------------------
    ExtensionApp x -> evalExt evalSub x

    ----------------------------------------------------------------------
    -- ()

    EmptyApp -> return ()

    ----------------------------------------------------------------------
    -- Any

    PackAny tp x -> do
      xv <- evalSub x
      return (AnyValue tp xv)

    UnpackAny tp x -> do
      xv <- evalSub x
      case xv of
        AnyValue tpv v
          | Just Refl <- testEquality tp tpv ->
               return $! PE (truePred sym) v
          | otherwise ->
               return Unassigned

    ----------------------------------------------------------------------
    -- Bool

    BoolLit b -> return $ backendPred sym b
    Not x -> do
      r <- evalSub x
      notPred sym r
    And x y -> do
      xv <- evalSub x
      yv <- evalSub y
      andPred sym xv yv
    Or x y -> do
      xv <- evalSub x
      yv <- evalSub y
      orPred sym xv yv
    BoolXor x y -> do
      xv <- evalSub x
      yv <- evalSub y
      xorPred sym xv yv

    ----------------------------------------------------------------------
    -- Nat

    NatLit n -> natLit sym n
    NatIte pe xe ye -> do
      p <- evalSub pe
      x <- evalSub xe
      y <- evalSub ye
      natIte sym p x y
    NatEq xe ye -> do
      x <- evalSub xe
      y <- evalSub ye
      natEq sym x y
    NatLt xe ye -> do
      x <- evalSub xe
      y <- evalSub ye
      natLt sym x y
    NatLe xe ye -> do
      x <- evalSub xe
      y <- evalSub ye
      natLe sym x y
    NatAdd xe ye -> do
      x <- evalSub xe
      y <- evalSub ye
      natAdd sym x y
    NatSub xe ye -> do
      x <- evalSub xe
      y <- evalSub ye
      natSub sym x y
    NatMul xe ye -> do
      x <- evalSub xe
      y <- evalSub ye
      natMul sym x y
    NatDiv xe ye -> do
      x <- evalSub xe
      y <- evalSub ye
      natDiv sym x y
    NatMod xe ye -> do
      x <- evalSub xe
      y <- evalSub ye
      natMod sym x y

    ----------------------------------------------------------------------
    -- Int

    IntLit n -> intLit sym n
    IntLe xe ye -> do
      x <- evalSub xe
      y <- evalSub ye
      intLe sym x y
    IntLt xe ye -> do
      x <- evalSub xe
      y <- evalSub ye
      intLt sym x y
    IntNeg xe -> do
      x <- evalSub xe
      intNeg sym x
    IntAbs xe -> do
      x <- evalSub xe
      intAbs sym x
    IntAdd xe ye -> do
      x <- evalSub xe
      y <- evalSub ye
      intAdd sym x y
    IntSub xe ye -> do
      x <- evalSub xe
      y <- evalSub ye
      intSub sym x y
    IntMul xe ye -> do
      x <- evalSub xe
      y <- evalSub ye
      intMul sym x y
    IntDiv xe ye -> do
      x <- evalSub xe
      y <- evalSub ye
      intDiv sym x y
    IntMod xe ye -> do
      x <- evalSub xe
      y <- evalSub ye
      intMod sym x y

    --------------------------------------------------------------------
    -- Maybe

    JustValue _ e -> do
      r <- evalSub e
      return $! PE (truePred sym) r
    NothingValue _ -> do
      return Unassigned
    FromJustValue _ maybe_expr msg_expr -> do
      maybe_val <- evalSub maybe_expr
      case maybe_val of
        -- Special case to avoid forcing evaluation of msg.
        PE (asConstantPred -> Just True) v -> return v
        _ -> do
          msg <- evalSub msg_expr
          case asString msg of
            Just (UnicodeLiteral msg') -> readPartExpr bak maybe_val (GenericSimError (Text.unpack msg'))
            Nothing ->
              addFailedAssertion bak $
                Unsupported callStack "Symbolic string in fromJustValue"

    ----------------------------------------------------------------------
    -- Recursive Types

    RollRecursive _ _ e   -> RolledType <$> evalSub e
    UnrollRecursive _ _ e -> unroll <$> evalSub e

    ----------------------------------------------------------------------
    -- Vector

    VectorLit _ v -> traverse evalSub v
    VectorReplicate _ n_expr e_expr -> do
      ne <- evalSub n_expr
      case asNat ne of
        Nothing -> addFailedAssertion bak $
                      Unsupported callStack "vectors with symbolic length"
        Just n -> do
          e <- evalSub e_expr
          return $ V.replicate (fromIntegral n) e
    VectorIsEmpty r -> do
      v <- evalSub r
      return $ backendPred sym (V.null v)
    VectorSize v_expr -> do
      v <- evalSub v_expr
      natLit sym (fromIntegral (V.length v))
    VectorGetEntry rtp v_expr i_expr -> do
      v <- evalSub v_expr
      i <- evalSub i_expr
      indexVectorWithSymNat bak (muxRegForType sym itefns rtp) v i
    VectorSetEntry rtp v_expr i_expr n_expr -> do
      v <- evalSub v_expr
      i <- evalSub i_expr
      n <- evalSub n_expr
      updateVectorWithSymNat bak (muxRegForType sym itefns rtp) v i n
    VectorCons _ e_expr v_expr -> do
      e <- evalSub e_expr
      v <- evalSub v_expr
      return $ V.cons e v

    --------------------------------------------------------------------
    -- Sequence

    SequenceNil _tpr -> nilSymSequence sym
    SequenceCons _tpr x xs ->
      join $ consSymSequence sym <$> evalSub x <*> evalSub xs
    SequenceAppend _tpr xs ys ->
      join $ appendSymSequence sym <$> evalSub xs <*> evalSub ys
    SequenceIsNil _tpr xs ->
      isNilSymSequence sym =<< evalSub xs
    SequenceLength _tpr xs ->
      lengthSymSequence sym =<< evalSub xs
    SequenceHead tpr xs ->
      headSymSequence sym (muxRegForType sym itefns tpr) =<< evalSub xs
    SequenceTail _tpr xs ->
      tailSymSequence sym =<< evalSub xs
    SequenceUncons tpr xs ->
      do xs' <- evalSub xs
         mu <- unconsSymSequence sym (muxRegForType sym itefns tpr) xs'
         traverse (\ (h,tl) -> pure (Ctx.Empty Ctx.:> RV h Ctx.:> RV tl)) mu

    --------------------------------------------------------------------
    -- Symbolic Arrays

    SymArrayLookup _ a i -> do
      join $ arrayLookup sym <$> evalSub a <*> traverseFC (evalBase sym evalSub) i

    SymArrayUpdate  _ a i v -> do
      join $ arrayUpdate sym
        <$> evalSub a
        <*> traverseFC (evalBase sym evalSub) i
        <*> evalSub v

    ----------------------------------------------------------------------
    -- Handle

    HandleLit h -> return (HandleFnVal h)

    Closure _ _ h_expr tp v_expr -> do
      h <- evalSub h_expr
      v <- evalSub v_expr
      return $! ClosureFnVal h tp v

    ----------------------------------------------------------------------
    -- RealVal

    RationalLit d -> realLit sym d
    RealNeg xe -> do
      x <- evalSub xe
      realNeg sym x
    RealAdd xe ye -> do
      x <- evalSub xe
      y <- evalSub ye
      realAdd sym x y
    RealSub xe ye -> do
      x <- evalSub xe
      y <- evalSub ye
      realSub sym x y
    RealMul xe ye -> do
      x <- evalSub xe
      y <- evalSub ye
      realMul sym x y
    RealDiv xe ye -> do
      x <- evalSub xe
      y <- evalSub ye
      realDiv sym x y
    RealMod xe ye -> do
      x <- evalSub xe
      y <- evalSub ye
      realMod sym x y
    RealLt x_expr y_expr -> do
      x <- evalSub x_expr
      y <- evalSub y_expr
      realLt sym x y
    RealLe x_expr y_expr -> do
      x <- evalSub x_expr
      y <- evalSub y_expr
      realLe sym x y
    RealIsInteger x_expr -> do
      x <- evalSub x_expr
      isInteger sym x

    ----------------------------------------------------------------------
    -- Float

    -- This is not necessarily considered correct, see crucible#366
    FloatUndef f -> freshConstant sym emptySymbol (iFloatBaseTypeRepr sym f)

    FloatLit f -> iFloatLitSingle sym f
    DoubleLit d -> iFloatLitDouble sym d
    X86_80Lit ld -> iFloatLitLongDouble sym ld
    FloatNaN fi -> iFloatNaN sym fi
    FloatPInf fi -> iFloatPInf sym fi
    FloatNInf fi -> iFloatNInf sym fi
    FloatPZero fi -> iFloatPZero sym fi
    FloatNZero fi -> iFloatNZero sym fi
    FloatNeg _ (x_expr :: f (FloatType fi)) ->
      iFloatNeg @_ @fi sym =<< evalSub x_expr
    FloatAbs _ (x_expr :: f (FloatType fi)) ->
      iFloatAbs @_ @fi sym =<< evalSub x_expr
    FloatSqrt _ rm (x_expr :: f (FloatType fi)) ->
      iFloatSqrt @_ @fi sym rm =<< evalSub x_expr
    FloatAdd _ rm (x_expr :: f (FloatType fi)) y_expr -> do
      x <- evalSub x_expr
      y <- evalSub y_expr
      iFloatAdd @_ @fi sym rm x y
    FloatSub _ rm (x_expr :: f (FloatType fi)) y_expr -> do
      x <- evalSub x_expr
      y <- evalSub y_expr
      iFloatSub @_ @fi sym rm x y
    FloatMul _ rm (x_expr :: f (FloatType fi)) y_expr -> do
      x <- evalSub x_expr
      y <- evalSub y_expr
      iFloatMul @_ @fi sym rm x y
    FloatDiv _ rm (x_expr :: f (FloatType fi)) y_expr -> do
      -- TODO: handle division by zero
      x <- evalSub x_expr
      y <- evalSub y_expr
      iFloatDiv @_ @fi sym rm x y
    FloatRem _ (x_expr :: f (FloatType fi)) y_expr -> do
      -- TODO: handle division by zero
      x <- evalSub x_expr
      y <- evalSub y_expr
      iFloatRem @_ @fi sym x y
    FloatMin _ (x_expr :: f (FloatType fi)) y_expr -> do
      x <- evalSub x_expr
      y <- evalSub y_expr
      iFloatMin @_ @fi sym x y
    FloatMax _ (x_expr :: f (FloatType fi)) y_expr -> do
      x <- evalSub x_expr
      y <- evalSub y_expr
      iFloatMax @_ @fi sym x y
    FloatFMA _ rm (x_expr :: f (FloatType fi)) y_expr z_expr -> do
      x <- evalSub x_expr
      y <- evalSub y_expr
      z <- evalSub z_expr
      iFloatFMA @_ @fi sym rm x y z
    FloatEq (x_expr :: f (FloatType fi)) y_expr -> do
      x <- evalSub x_expr
      y <- evalSub y_expr
      iFloatEq @_ @fi sym x y
    FloatFpEq (x_expr :: f (FloatType fi)) y_expr -> do
      x <- evalSub x_expr
      y <- evalSub y_expr
      iFloatFpEq @_ @fi sym x y
    FloatIte _ c_expr (x_expr :: f (FloatType fi)) y_expr -> do
      c <- evalSub c_expr
      x <- evalSub x_expr
      y <- evalSub y_expr
      iFloatIte @_ @fi sym c x y
    FloatLt (x_expr :: f (FloatType fi)) y_expr -> do
      x <- evalSub x_expr
      y <- evalSub y_expr
      iFloatLt @_ @fi sym x y
    FloatLe (x_expr :: f (FloatType fi)) y_expr -> do
      x <- evalSub x_expr
      y <- evalSub y_expr
      iFloatLe @_ @fi sym x y
    FloatGt (x_expr :: f (FloatType fi)) y_expr -> do
      x <- evalSub x_expr
      y <- evalSub y_expr
      iFloatGt @_ @fi sym x y
    FloatGe (x_expr :: f (FloatType fi)) y_expr -> do
      x <- evalSub x_expr
      y <- evalSub y_expr
      iFloatGe @_ @fi sym x y
    FloatNe (x_expr :: f (FloatType fi)) y_expr -> do
      x <- evalSub x_expr
      y <- evalSub y_expr
      iFloatNe @_ @fi sym x y
    FloatFpApart (x_expr :: f (FloatType fi)) y_expr -> do
      x <- evalSub x_expr
      y <- evalSub y_expr
      iFloatFpApart @_ @fi sym x y
    FloatCast fi rm (x_expr :: f (FloatType fi')) ->
      iFloatCast @_ @_ @fi' sym fi rm =<< evalSub x_expr
    FloatFromBinary fi x_expr -> iFloatFromBinary sym fi =<< evalSub x_expr
    FloatToBinary fi x_expr -> iFloatToBinary sym fi =<< evalSub x_expr
    FloatFromBV fi rm x_expr -> iBVToFloat sym fi rm =<< evalSub x_expr
    FloatFromSBV fi rm x_expr -> iSBVToFloat sym fi rm =<< evalSub x_expr
    FloatFromReal fi rm x_expr -> iRealToFloat sym fi rm =<< evalSub x_expr
    FloatToBV w rm (x_expr :: f (FloatType fi)) ->
      iFloatToBV @_ @_ @fi sym w rm =<< evalSub x_expr
    FloatToSBV w rm (x_expr :: f (FloatType fi)) ->
      iFloatToSBV @_ @_ @fi sym w rm =<< evalSub x_expr
    FloatToReal (x_expr :: f (FloatType fi)) ->
      iFloatToReal @_ @fi sym =<< evalSub x_expr
    FloatIsNaN (x_expr :: f (FloatType fi)) ->
      iFloatIsNaN @_ @fi sym =<< evalSub x_expr
    FloatIsInfinite (x_expr :: f (FloatType fi)) ->
      iFloatIsInf @_ @fi sym =<< evalSub x_expr
    FloatIsZero (x_expr :: f (FloatType fi)) ->
      iFloatIsZero @_ @fi sym =<< evalSub x_expr
    FloatIsPositive (x_expr :: f (FloatType fi)) ->
      iFloatIsPos @_ @fi sym =<< evalSub x_expr
    FloatIsNegative (x_expr :: f (FloatType fi)) ->
      iFloatIsNeg @_ @fi sym =<< evalSub x_expr
    FloatIsSubnormal (x_expr :: f (FloatType fi)) ->
      iFloatIsSubnorm @_ @fi sym =<< evalSub x_expr
    FloatIsNormal (x_expr :: f (FloatType fi)) ->
      iFloatIsNorm @_ @fi sym =<< evalSub x_expr

    ----------------------------------------------------------------------
    -- Conversions

    NatToInteger x_expr -> do
      x <- evalSub x_expr
      natToInteger sym x
    IntegerToReal x_expr -> do
      x <- evalSub x_expr
      integerToReal sym x
    RealToNat x_expr -> do
      x <- evalSub x_expr
      realToNat sym x
    BvToNat _ xe -> do
      bvToNat sym =<< evalSub xe
    BvToInteger _ xe -> do
      bvToInteger sym =<< evalSub xe
    SbvToInteger _ xe -> do
      sbvToInteger sym =<< evalSub xe
    RealFloor xe ->
      realFloor sym =<< evalSub xe
    RealCeil xe ->
      realCeil sym =<< evalSub xe
    RealRound xe ->
      realRound sym =<< evalSub xe
    IntegerToBV w xe -> do
      x <- evalSub xe
      integerToBV sym x w

    ----------------------------------------------------------------------
    -- ComplexReal

    Complex r_expr i_expr -> do
      r <- evalSub r_expr
      i <- evalSub i_expr
      mkComplex sym (r :+ i)
    RealPart c_expr -> getRealPart sym =<< evalSub c_expr
    ImagPart c_expr -> getImagPart sym =<< evalSub c_expr

    --------------------------------------------------------------------
    -- BVs

    -- This is not necessarily considered correct, see crucible#366
    BVUndef w ->
      freshConstant sym emptySymbol (BaseBVRepr w)

    BVLit w bv -> bvLit sym w bv

    BVConcat _ _ xe ye -> do
      x <- evalSub xe
      y <- evalSub ye
      bvConcat sym x y
    -- FIXME: there are probably some worthwhile special cases to exploit in "BVSelect"
    BVSelect idx n _ xe -> do
      x <- evalSub xe
      bvSelect sym idx n x
    BVTrunc w' _ xe -> do
      x <- evalSub xe
      bvTrunc sym w' x
    BVZext w' _ xe -> do
      x <- evalSub xe
      bvZext sym w' x
    BVSext w' _ xe -> do
      x <- evalSub xe
      bvSext sym w' x
    BVNot _ xe ->
      bvNotBits sym =<< evalSub xe
    BVAnd _ xe ye -> do
      x <- evalSub xe
      y <- evalSub ye
      bvAndBits sym x y
    BVOr _ xe ye -> do
      x <- evalSub xe
      y <- evalSub ye
      bvOrBits sym x y
    BVXor _ xe ye -> do
      x <- evalSub xe
      y <- evalSub ye
      bvXorBits sym x y
    BVAdd _ xe ye -> do
      x <- evalSub xe
      y <- evalSub ye
      bvAdd sym x y
    BVNeg _ xe -> do
      x <- evalSub xe
      bvNeg sym x
    BVSub _ xe ye -> do
      x <- evalSub xe
      y <- evalSub ye
      bvSub sym x y
    BVMul _ xe ye -> do
      x <- evalSub xe
      y <- evalSub ye
      bvMul sym x y
    BVUdiv _ xe ye -> do
      x <- evalSub xe
      y <- evalSub ye
      bvUdiv sym x y
    BVSdiv _ xe ye -> do
      x <- evalSub xe
      y <- evalSub ye
      bvSdiv sym x y
    BVUrem _ xe ye -> do
      x <- evalSub xe
      y <- evalSub ye
      bvUrem sym x y
    BVSrem _ xe ye -> do
      x <- evalSub xe
      y <- evalSub ye
      bvSrem sym x y

    BVUlt _ xe ye -> do
      x <- evalSub xe
      y <- evalSub ye
      bvUlt sym x y
    BVSlt _ xe ye -> do
      x <- evalSub xe
      y <- evalSub ye
      bvSlt sym x y
    BoolToBV w xe -> do
      x <- evalSub xe
      one <- bvLit sym w (BV.one w)
      zro <- bvLit sym w (BV.zero w)
      bvIte sym x one zro
    BVNonzero _ xe -> do
      x <- evalSub xe
      bvIsNonzero sym x
    BVShl _ xe ye -> do
      x <- evalSub xe
      y <- evalSub ye
      bvShl sym x y
    BVLshr _ xe ye -> do
      x <- evalSub xe
      y <- evalSub ye
      bvLshr sym x y
    BVAshr _ xe ye -> do
      x <- evalSub xe
      y <- evalSub ye
      bvAshr sym x y
    BVRol _ xe ye -> do
      x <- evalSub xe
      y <- evalSub ye
      bvRol sym x y
    BVRor _ xe ye -> do
      x <- evalSub xe
      y <- evalSub ye
      bvRor sym x y
    BVCountTrailingZeros _ xe -> do
      x <- evalSub xe
      bvCountTrailingZeros sym x
    BVCountLeadingZeros _ xe -> do
      x <- evalSub xe
      bvCountLeadingZeros sym x
    BVPopcount _ xe -> do
      x <- evalSub xe
      bvPopcount sym x
    BVCarry _ xe ye -> do
      x <- evalSub xe
      y <- evalSub ye
      fst <$> addUnsignedOF sym x y
    BVSCarry _ xe ye -> do
      x <- evalSub xe
      y <- evalSub ye
      fst <$> addSignedOF sym x y
    BVSBorrow _ xe ye -> do
      x <- evalSub xe
      y <- evalSub ye
      fst <$> subSignedOF sym x y
    BVUle _ xe ye -> do
      x <- evalSub xe
      y <- evalSub ye
      bvUle sym x y
    BVSle _ xe ye -> do
      x <- evalSub xe
      y <- evalSub ye
      bvSle sym x y
    BVUMin _ xe ye -> do
      x <- evalSub xe
      y <- evalSub ye
      c <- bvUle sym x y
      bvIte sym c x y
    BVUMax _ xe ye -> do
      x <- evalSub xe
      y <- evalSub ye
      c <- bvUgt sym x y
      bvIte sym c x y
    BVSMin _ xe ye -> do
      x <- evalSub xe
      y <- evalSub ye
      c <- bvSle sym x y
      bvIte sym c x y
    BVSMax _ xe ye -> do
      x <- evalSub xe
      y <- evalSub ye
      c <- bvSgt sym x y
      bvIte sym c x y

    --------------------------------------------------------------------
    -- Word Maps

    EmptyWordMap w tp -> do
      emptyWordMap sym w tp

    InsertWordMap w tp ie ve me -> do
      i <- evalSub ie
      v <- evalSub ve
      m <- evalSub me
      insertWordMap sym w tp i v m

    LookupWordMap tp ie me -> do
      i <- evalSub ie
      m <- evalSub me
      x <- lookupWordMap sym (bvWidth i) tp i m
      let msg = "WordMap: read an undefined index" ++
                case asBV i of
                   Nothing  -> ""
                   Just (BV.BV idx) -> " 0x" ++ showHex idx ""
      let ex = ReadBeforeWriteSimError msg
      readPartExpr bak x ex

    LookupWordMapWithDefault tp ie me de -> do
      i <- evalSub ie
      m <- evalSub me
      d <- evalSub de
      x <- lookupWordMap sym (bvWidth i) tp i m
      case x of
        Unassigned -> return d
        PE p v -> do
          muxRegForType sym itefns (baseToType tp) p v d

    ---------------------------------------------------------------------
    -- Struct

    MkStruct _ exprs -> traverseFC (\x -> RV <$> evalSub x) exprs

    GetStruct st idx _ -> do
      struct <- evalSub st
      return $ unRV $ struct Ctx.! idx

    SetStruct _ st idx x -> do
      struct <- evalSub st
      v <- evalSub x
      return $ struct & ixF idx .~ RV v

    ----------------------------------------------------------------------
    -- Variant

    InjectVariant ctx idx ve -> do
         v <- evalSub ve
         return $ injectVariant sym ctx idx v

    ProjectVariant _ctx idx ve -> do
         v <- evalSub ve
         return $ unVB $ v Ctx.! idx

    ----------------------------------------------------------------------
    -- IdentValueMap

    EmptyStringMap _ -> return Map.empty

    LookupStringMapEntry _ m_expr i_expr -> do
      i <- evalSub i_expr
      m <- evalSub m_expr
      case asString i of
        Just (UnicodeLiteral i') -> return $ joinMaybePE (Map.lookup i' m)
        Nothing -> addFailedAssertion bak $
                    Unsupported callStack "Symbolic string in lookupStringMapEntry"

    InsertStringMapEntry _ m_expr i_expr v_expr -> do
      m <- evalSub m_expr
      i <- evalSub i_expr
      v <- evalSub v_expr
      case asString i of
        Just (UnicodeLiteral i') -> return $ Map.insert i' v m
        Nothing -> addFailedAssertion bak $
                     Unsupported callStack "Symbolic string in insertStringMapEntry"

    --------------------------------------------------------------------
    -- Strings

    StringLit x -> stringLit sym x
    ShowValue _bt x_expr -> do
      x <- evalSub x_expr
      stringLit sym (UnicodeLiteral (Text.pack (show (printSymExpr x))))
    ShowFloat _fi x_expr -> do
      x <- evalSub x_expr
      stringLit sym (UnicodeLiteral (Text.pack (show (printSymExpr x))))
    StringConcat _si x y -> do
      x' <- evalSub x
      y' <- evalSub y
      stringConcat sym x' y'
    StringEmpty si ->
      stringEmpty sym si
    StringLength x -> do
      x' <- evalSub x
      stringLength sym x'
    StringContains x y -> do
      x' <- evalSub x
      y' <- evalSub y
      stringContains sym x' y'
    StringIsPrefixOf x y -> do
      x' <- evalSub x
      y' <- evalSub y
      stringIsPrefixOf sym x' y'
    StringIsSuffixOf x y -> do
      x' <- evalSub x
      y' <- evalSub y
      stringIsSuffixOf sym x' y'
    StringIndexOf x y k -> do
      x' <- evalSub x
      y' <- evalSub y
      k' <- evalSub k
      stringIndexOf sym x' y' k'
    StringSubstring _si x off len -> do
      x' <- evalSub x
      off' <- evalSub off
      len' <- evalSub len
      stringSubstring sym x' off' len'

    ---------------------------------------------------------------------
    -- Introspection

    IsConcrete _ v -> do
      x <- baseIsConcrete <$> evalSub v
      return $! if x then truePred sym else falsePred sym

    ---------------------------------------------------------------------
    -- References

    ReferenceEq _ ref1 ref2 -> do
      cell1 <- evalSub ref1
      cell2 <- evalSub ref2
      eqReference sym cell1 cell2