Concretize.hs

-----------------------------------------------------------------------
-- |
-- Module           : Lang.Crucible.Concretize
-- Description      : Get feasible concrete values from a model
-- Copyright        : (c) Galois, Inc 2024
-- License          : BSD3
-- Maintainer       : Langston Barrett <langston@galois.com>
-- Stability        : provisional
--
-- This module defines 'concRegValue', a function that takes a 'RegValue' (i.e.,
-- a symbolic value), and a model from the SMT solver ('W4GE.GroundEvalFn'), and
-- returns the concrete value that the symbolic value takes in the model.
--
-- This can be used to report specific values that lead to violations of
-- assertions, including safety assertions.
------------------------------------------------------------------------

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

module Lang.Crucible.Concretize
  ( ConcRegValue
  , ConcRV'(..)
  , ConcAnyValue(..)
  , ConcIntrinsic
  , IntrinsicConcFn(..)
  , ConcCtx(..)
  , concRegValue
  , concRegEntry
  , concRegMap
    -- * There and back again
  , IntrinsicConcToSymFn(..)
  , concToSym
  ) where

import qualified Data.Foldable as F
import           Data.Kind (Type)
import           Data.List.NonEmpty (NonEmpty)
import qualified Data.List.NonEmpty as NE
import           Data.Map (Map)
import qualified Data.Map as Map
import           Data.Sequence (Seq)
import           Data.Text (Text)
import qualified Data.Text as Text
import qualified Data.Vector as V
import           Data.Word (Word16)

import qualified Data.Parameterized.Context as Ctx
import           Data.Parameterized.Map (MapF)
import qualified Data.Parameterized.Map as MapF
import           Data.Parameterized.TraversableFC (traverseFC)

import           What4.Expr (Expr, ExprBuilder, Flags, FloatModeRepr(..))
import qualified What4.Expr.GroundEval as W4GE
import           What4.Interface (SymExpr)
import qualified What4.Interface as W4I
import qualified What4.Partial as W4P

import           Lang.Crucible.FunctionHandle (FnHandle, RefCell)
import           Lang.Crucible.Simulator.Intrinsics (Intrinsic)
import           Lang.Crucible.Simulator.RegMap (RegEntry, RegMap)
import qualified Lang.Crucible.Simulator.RegMap as RM
import           Lang.Crucible.Simulator.RegValue (RegValue, FnVal)
import qualified Lang.Crucible.Simulator.RegValue as RV
import qualified Lang.Crucible.Simulator.SymSequence as SymSeq
import qualified Lang.Crucible.Utils.MuxTree as MuxTree
import           Lang.Crucible.Types
import           Lang.Crucible.Panic (panic)

-- | Newtype to allow partial application of 'ConcRegValue'.
--
-- Type families cannot appear partially applied.
type ConcRV' :: Type -> CrucibleType -> Type
newtype ConcRV' sym tp = ConcRV' { unConcRV' :: ConcRegValue sym tp }

-- | Defines the \"concrete\" interpretations of 'CrucibleType' (as opposed
-- to the \"symbolic\" interpretations, which are defined by 'RegValue'), as
-- returned by 'concRegValue'.
--
-- Unlike What4\'s 'W4GE.GroundValue', this type family is parameterized
-- by @sym@, the symbolic backend. This is because Crucible makes use of
-- \"interpreted\" floating point numbers ('SymInterpretedFloatType'). What4\'s
-- @SymFloat@ always uses an IEEE-754 interpretation of symbolic floats, whereas
-- 'SymInterpretedFloatType' can use IEEE-754, real numbers, or uninterpreted
-- functions depending on how the symbolic backend is configured.
type ConcRegValue :: Type -> CrucibleType -> Type
type family ConcRegValue sym tp where
  ConcRegValue sym (BaseToType bt) = W4GE.GroundValue bt
  ConcRegValue sym (FloatType fi) = W4GE.GroundValue (SymInterpretedFloatType sym fi)
  ConcRegValue sym AnyType = ConcAnyValue sym
  ConcRegValue sym UnitType = ()
  ConcRegValue sym NatType = Integer
  ConcRegValue sym CharType = Word16
  ConcRegValue sym (FunctionHandleType a r) = ConcFnVal sym a r
  ConcRegValue sym (MaybeType tp) = Maybe (ConcRegValue sym tp)
  ConcRegValue sym (VectorType tp) = V.Vector (ConcRV' sym tp)
  ConcRegValue sym (SequenceType tp) = Seq (ConcRV' sym tp)
  ConcRegValue sym (StructType ctx) = Ctx.Assignment (ConcRV' sym) ctx
  ConcRegValue sym (VariantType ctx) = Ctx.Assignment (ConcVariantBranch sym) ctx
  ConcRegValue sym (ReferenceType tp) = NonEmpty (RefCell tp)
  ConcRegValue sym (WordMapType w tp) = ()  -- TODO: possible to do something meaningful?
  ConcRegValue sym (RecursiveType nm ctx) = ConcRegValue sym (UnrollType nm ctx)
  ConcRegValue sym (IntrinsicType nm ctx) = ConcIntrinsic nm ctx
  ConcRegValue sym (StringMapType tp) = Map Text (ConcRV' sym tp)

---------------------------------------------------------------------
-- * ConcCtx

-- | Context needed for 'concRegValue'
--
-- The @t@ parameter matches that on 'W4GE.GroundEvalFn' and 'Expr', namely, it
-- is a phantom type brand used to relate nonces to a specific nonce generator
-- (similar to the @s@ parameter of the @ST@ monad). It also appears as the
-- first argument to 'ExprBuilder'.
data ConcCtx sym t
  = ConcCtx
  { -- | Model returned from SMT solver
    model :: W4GE.GroundEvalFn t
    -- | How to ground intrinsics
  , intrinsicConcFuns :: MapF SymbolRepr (IntrinsicConcFn t)
  }

-- | Helper, not exported
ground ::
  ConcCtx sym t ->
  Expr t tp ->
  IO (ConcRegValue sym (BaseToType tp))
ground (ConcCtx (W4GE.GroundEvalFn ge) _) = ge

---------------------------------------------------------------------
-- * Helpers

-- | Helper, not exported
ite ::
  (SymExpr sym ~ Expr t) =>
  ConcCtx sym t ->
  W4I.Pred sym ->
  a ->
  a ->
  IO a
ite ctx p t f = do
  b <- ground ctx p
  pure (if b then t else f)

-- | Helper, not exported
iteIO ::
  (SymExpr sym ~ Expr t) =>
  ConcCtx sym t ->
  W4I.Pred sym ->
  IO a ->
  IO a ->
  IO a
iteIO ctx p t f = do
  b <- ground ctx p
  if b then t else f

-- | Helper, not exported
concPartial ::
  (SymExpr sym ~ Expr t) =>
  W4I.IsExprBuilder sym =>
  ConcCtx sym t ->
  TypeRepr tp ->
  W4P.Partial (W4I.Pred sym) (RegValue sym tp) ->
  IO (Maybe (ConcRegValue sym tp))
concPartial ctx tp (W4P.Partial p v) =
  iteIO ctx p (Just <$> concRegValue ctx tp v) (pure Nothing)

-- | Helper, not exported
concPartialWithErr ::
  (SymExpr sym ~ Expr t) =>
  W4I.IsExprBuilder sym =>
  ConcCtx sym t ->
  TypeRepr tp ->
  W4P.PartialWithErr e (W4I.Pred sym) (RegValue sym tp) ->
  IO (Maybe (ConcRegValue sym tp))
concPartialWithErr ctx tp =
  \case
    W4P.Err _ -> pure Nothing
    W4P.NoErr pv -> concPartial ctx tp pv

---------------------------------------------------------------------
-- * Intrinsics

-- | Open type family for defining how intrinsics are concretized
type ConcIntrinsic :: Symbol -> Ctx CrucibleType -> Type
type family ConcIntrinsic nm ctx

-- | Function for concretizing an intrinsic type
type IntrinsicConcFn :: Type -> Symbol -> Type
newtype IntrinsicConcFn t nm
  = IntrinsicConcFn
    (forall sym ctx.
      SymExpr sym ~ Expr t =>
      W4I.IsExprBuilder sym =>
      ConcCtx sym t ->
      Ctx.Assignment TypeRepr ctx ->
      Intrinsic sym nm ctx ->
      IO (ConcRegValue sym (IntrinsicType nm ctx)))

-- | Helper, not exported
tryConcIntrinsic ::
  forall sym nm ctx t.
  SymExpr sym ~ Expr t =>
  W4I.IsExprBuilder sym =>
  ConcCtx sym t ->
  SymbolRepr nm ->
  Ctx.Assignment TypeRepr ctx ->
  RegValue sym (IntrinsicType nm ctx) ->
  Maybe (IO (ConcRegValue sym (IntrinsicType nm ctx)))
tryConcIntrinsic ctx nm tyCtx v = do
    case MapF.lookup nm (intrinsicConcFuns ctx) of
      Nothing -> Nothing
      Just (IntrinsicConcFn f) -> Just (f @sym @ctx ctx tyCtx v)

---------------------------------------------------------------------
-- * Any

-- | An 'AnyValue' concretized by 'concRegValue'
data ConcAnyValue sym = forall tp. ConcAnyValue (TypeRepr tp) (ConcRV' sym tp)

---------------------------------------------------------------------
-- * FnVal

-- | A 'FnVal' concretized by 'concRegValue'
data ConcFnVal (sym :: Type) (args :: Ctx CrucibleType) (res :: CrucibleType) where
  ConcClosureFnVal ::
    !(ConcFnVal sym (args ::> tp) ret) ->
    !(TypeRepr tp) ->
    !(ConcRV' sym tp) ->
    ConcFnVal sym args ret

  ConcVarargsFnVal ::
    !(FnHandle (args ::> VectorType AnyType) ret) ->
    !(CtxRepr addlArgs) ->
    ConcFnVal sym (args <+> addlArgs) ret

  ConcHandleFnVal ::
    !(FnHandle a r) ->
    ConcFnVal sym a r

-- | Helper, not exported
concFnVal ::
  (SymExpr sym ~ Expr t) =>
  W4I.IsExprBuilder sym =>
  ConcCtx sym t ->
  CtxRepr args ->
  TypeRepr ret ->
  FnVal sym args ret ->
  IO (ConcFnVal sym args ret)
concFnVal ctx args ret =
  \case
    RV.ClosureFnVal fv t v -> do
      concV <- concFnVal ctx (args Ctx.:> t) ret fv
      v' <- concRegValue ctx t v
      pure (ConcClosureFnVal concV t (ConcRV' v'))
    RV.VarargsFnVal hdl extra ->
      pure (ConcVarargsFnVal hdl extra)
    RV.HandleFnVal hdl ->
      pure (ConcHandleFnVal hdl)

---------------------------------------------------------------------
-- * Reference

-- | Helper, not exported
concMux ::
  (SymExpr sym ~ Expr t) =>
  W4I.IsExprBuilder sym =>
  ConcCtx sym t ->
  MuxTree.MuxTree sym a ->
  IO (NonEmpty a)
concMux ctx mt = do
  l <- go (MuxTree.viewMuxTree mt)
  case NE.nonEmpty l of
    -- This is impossible because the only way to make a MuxTree is with
    -- `toMuxTree`, which uses `truePred`.
    Nothing ->
      panic "Lang.Crucible.Concretize.concMux"
        [ "Impossible: Mux tree had no feasible branches?" ]
    Just ne -> pure ne
  where
    go [] = pure []
    go ((val, p):xs) = do
      f <- ite ctx p (val:) id
      f <$> go xs

---------------------------------------------------------------------
-- * Sequence

-- | Helper, not exported
concSymSequence ::
  (SymExpr sym ~ Expr t) =>
  W4I.IsExprBuilder sym =>
  ConcCtx sym t ->
  TypeRepr tp ->
  SymSeq.SymSequence sym (RegValue sym tp) ->
  IO (Seq (ConcRV' sym tp))
concSymSequence ctx tp =
  SymSeq.concretizeSymSequence
    (ground ctx)
    (fmap ConcRV' . concRegValue ctx tp)

---------------------------------------------------------------------
-- * StringMap

-- | Helper, not exported
concStringMap ::
  (SymExpr sym ~ Expr t) =>
  W4I.IsExprBuilder sym =>
  ConcCtx sym t ->
  TypeRepr tp ->
  RegValue sym (StringMapType tp) ->
  IO (Map Text (ConcRV' sym tp))
concStringMap ctx tp v = Map.fromList <$> go (Map.toList v)
  where
    go [] = pure []
    go ((t, v'):xs) =
      concPartialWithErr ctx tp v' >>=
        \case
          Nothing -> go xs
          Just v'' -> ((t, ConcRV' v''):) <$> go xs

---------------------------------------------------------------------
-- * Variant

-- | Note that we do not attempt to \"normalize\" variants in 'concRegValue'
-- in any way. If the model reports that multiple branches of a variant are
-- plausible, then multiple branches might be included as 'Just's.
newtype ConcVariantBranch sym tp
  = ConcVariantBranch (Maybe (ConcRV' sym tp))

-- | Helper, not exported
concVariant ::
  forall sym variants t.
  (SymExpr sym ~ Expr t) =>
  W4I.IsExprBuilder sym =>
  ConcCtx sym t ->
  Ctx.Assignment TypeRepr variants ->
  RegValue sym (VariantType variants) ->
  IO (ConcRegValue sym (VariantType variants))
concVariant ctx tps vs = Ctx.zipWithM concBranch tps vs
  where
    concBranch :: forall tp. TypeRepr tp -> RV.VariantBranch sym tp -> IO (ConcVariantBranch sym tp)
    concBranch tp (RV.VB v) = do
      v' <- concPartialWithErr ctx tp v
      case v' of
        Just v'' -> pure (ConcVariantBranch (Just (ConcRV' v'')))
        Nothing -> pure (ConcVariantBranch Nothing)

---------------------------------------------------------------------
-- * 'concRegValue'

-- | Pick a feasible concrete value from the model
--
-- This function does not attempt to \"normalize\" variants nor mux trees in any
-- way. If the model reports that multiple branches of a variant or mux tree are
-- plausible, then multiple branches might be included in the result.
concRegValue ::
  (SymExpr sym ~ Expr t) =>
  W4I.IsExprBuilder sym =>
  ConcCtx sym t ->
  TypeRepr tp ->
  RegValue sym tp ->
  IO (ConcRegValue sym tp)
concRegValue ctx tp v =
  case (tp, v) of
    -- Base types
    (BoolRepr, _) -> ground ctx v
    (BVRepr _width, _) -> ground ctx v
    (ComplexRealRepr, _) -> ground ctx v
    (FloatRepr _fpp, _) -> ground ctx v
    (IEEEFloatRepr _fpp, _) -> ground ctx v
    (IntegerRepr, _) -> ground ctx v
    (NatRepr, _) -> ground ctx (W4I.natToIntegerPure v)
    (RealValRepr, _) -> ground ctx v
    (StringRepr _, _) -> ground ctx v
    (SymbolicArrayRepr _idxs _tp', _) -> ground ctx v
    (SymbolicStructRepr _tys, _) -> ground ctx v

    -- Trivial cases
    (UnitRepr, ()) -> pure ()
    (CharRepr, _) -> pure v

    -- Simple recursive cases
    (AnyRepr, RV.AnyValue tp' v') ->
      ConcAnyValue tp' . ConcRV' <$> concRegValue ctx tp' v'
    (RecursiveRepr symb tyCtx, RV.RolledType v') ->
      concRegValue ctx (unrollType symb tyCtx) v'
    (StructRepr tps, _) ->
      Ctx.zipWithM (\tp' (RV.RV v') -> ConcRV' <$> concRegValue ctx tp' v') tps v
    (VectorRepr tp', _) ->
      traverse (fmap ConcRV' . concRegValue ctx tp') v

    -- Cases with helper functions
    (MaybeRepr tp', _) ->
      concPartialWithErr ctx tp' v
    (FunctionHandleRepr args ret, _) ->
      concFnVal ctx args ret v
    (IntrinsicRepr nm tyCtx, _) ->
      case tryConcIntrinsic ctx nm tyCtx v of
        Nothing ->
          let strNm = Text.unpack (symbolRepr nm) in
          fail ("Missing concretization function for intrinsic: " ++ strNm)
        Just r -> r
    (ReferenceRepr _, _) ->
      concMux ctx v
    (SequenceRepr tp', _) ->
      concSymSequence ctx tp' v
    (StringMapRepr tp', _) ->
      concStringMap ctx tp' v
    (VariantRepr tps, _) ->
      concVariant ctx tps v

    -- Incomplete cases
    (WordMapRepr _ _, _) -> pure ()

-- | Like 'concRegValue', but for 'RegEntry'
concRegEntry ::
  (SymExpr sym ~ Expr t) =>
  W4I.IsExprBuilder sym =>
  ConcCtx sym t ->
  RegEntry sym tp ->
  IO (ConcRegValue sym tp)
concRegEntry ctx e = concRegValue ctx (RM.regType e) (RM.regValue e)

-- | Like 'concRegEntry', but for a whole 'RegMap'
concRegMap ::
  (SymExpr sym ~ Expr t) =>
  W4I.IsExprBuilder sym =>
  ConcCtx sym t ->
  RegMap sym tps ->
  IO (Ctx.Assignment (ConcRV' sym) tps)
concRegMap ctx (RM.RegMap m) = traverseFC (fmap ConcRV' . concRegEntry ctx) m

---------------------------------------------------------------------
-- * concToSym

-- | Function for re-symbolizing an intrinsic type
type IntrinsicConcToSymFn :: Symbol -> Type
newtype IntrinsicConcToSymFn nm
  = IntrinsicConcToSymFn
    (forall sym ctx.
      W4I.IsExprBuilder sym =>
      sym ->
      Ctx.Assignment TypeRepr ctx ->
      ConcIntrinsic nm ctx ->
      IO (RegValue sym (IntrinsicType nm ctx)))

-- | Helper, not exported
concToSymAny ::
  (sym ~ ExprBuilder scope st (Flags fm)) =>
  sym ->
  MapF SymbolRepr IntrinsicConcToSymFn ->
  FloatModeRepr fm ->
  ConcRegValue sym AnyType ->
  IO (RegValue sym AnyType)
concToSymAny sym iFns fm (ConcAnyValue tp' (ConcRV' v')) =
  RV.AnyValue tp' <$> concToSym sym iFns fm tp' v'

-- | Helper, not exported
concToSymFn ::
  (sym ~ ExprBuilder scope st (Flags fm)) =>
  sym ->
  MapF SymbolRepr IntrinsicConcToSymFn ->
  FloatModeRepr fm ->
  Ctx.Assignment (TypeRepr) as ->
  TypeRepr r ->
  ConcRegValue sym (FunctionHandleType as r) ->
  IO (RegValue sym (FunctionHandleType as r))
concToSymFn sym iFns fm as r f =
  case f of
    ConcClosureFnVal clos vtp (ConcRV' v) -> do
      v' <- concToSym sym iFns fm vtp v
      clos' <- concToSymFn sym iFns fm (as Ctx.:> vtp) r clos
      pure (RV.ClosureFnVal clos' vtp v')

    ConcVarargsFnVal hdl extra ->
      pure (RV.VarargsFnVal hdl extra)

    ConcHandleFnVal hdl ->
      pure (RV.HandleFnVal hdl)

-- | Helper, not exported
concToSymIntrinsic ::
  W4I.IsExprBuilder sym =>
  sym ->
  MapF SymbolRepr IntrinsicConcToSymFn ->
  SymbolRepr nm ->
  CtxRepr ctx ->
  ConcRegValue sym (IntrinsicType nm ctx) ->
  IO (RegValue sym (IntrinsicType nm ctx))
concToSymIntrinsic sym iFns nm tyCtx v =
  case MapF.lookup nm iFns of
    Nothing ->
      let strNm = Text.unpack (symbolRepr nm) in
      fail ("Missing concretization function for intrinsic: " ++ strNm)
    Just (IntrinsicConcToSymFn f) -> f sym tyCtx v

-- | Helper, not exported
concToSymMaybe ::
  (sym ~ ExprBuilder scope st (Flags fm)) =>
  sym ->
  MapF SymbolRepr IntrinsicConcToSymFn ->
  FloatModeRepr fm ->
  TypeRepr tp ->
  ConcRegValue sym (MaybeType tp) ->
  IO (RegValue sym (MaybeType tp))
concToSymMaybe sym iFns fm tp =
  \case
    Nothing -> pure (W4P.Err ())
    Just v ->
      W4P.justPartExpr sym <$> concToSym sym iFns fm tp v

-- | Helper, not exported
concToSymRef ::
  W4I.IsExprBuilder sym =>
  sym ->
  ConcRegValue sym (ReferenceType tp) ->
  IO (RegValue sym (ReferenceType tp))
concToSymRef sym (v NE.:| _) = pure (MuxTree.toMuxTree sym v)

-- | Helper, not exported
concToSymVariant ::
  forall sym tps scope st fm.
  (sym ~ ExprBuilder scope st (Flags fm)) =>
  sym ->
  MapF SymbolRepr IntrinsicConcToSymFn ->
  FloatModeRepr fm ->
  CtxRepr tps ->
  ConcRegValue sym (VariantType tps) ->
  IO (RegValue sym (VariantType tps))
concToSymVariant sym iFns fm tps v = Ctx.zipWithM go tps v
  where
    go :: forall tp. TypeRepr tp -> ConcVariantBranch sym tp -> IO (RV.VariantBranch sym tp)
    go tp (ConcVariantBranch b) =
      case b of
        Nothing -> pure (RV.VB (W4P.Err ()))
        Just (ConcRV' v') ->
          RV.VB . W4P.justPartExpr sym <$> concToSym sym iFns fm tp v'

-- | Inject a 'ConcRegValue' back into a 'RegValue'.
concToSym ::
  (sym ~ ExprBuilder scope st (Flags fm)) =>
  sym ->
  MapF SymbolRepr IntrinsicConcToSymFn ->
  FloatModeRepr fm ->
  TypeRepr tp ->
  ConcRegValue sym tp ->
  IO (RegValue sym tp)
concToSym sym iFns fm tp v =
  case tp of
    -- Base types
    BoolRepr -> W4GE.groundToSym sym BaseBoolRepr v
    BVRepr width -> W4GE.groundToSym sym (BaseBVRepr width) v
    ComplexRealRepr -> W4GE.groundToSym sym BaseComplexRepr v
    FloatRepr fi ->
      case fm of
        FloatIEEERepr ->
          W4I.floatLit sym (floatInfoToPrecisionRepr fi) v
        FloatUninterpretedRepr -> do
          sv <- W4GE.groundToSym sym (floatInfoToBVTypeRepr fi) v
          iFloatFromBinary sym fi sv
        FloatRealRepr ->
          iFloatLitRational sym fi v
    IEEEFloatRepr fpp -> W4GE.groundToSym sym (BaseFloatRepr fpp) v
    IntegerRepr -> W4GE.groundToSym sym BaseIntegerRepr v
    NatRepr -> W4I.integerToNat sym =<< W4GE.groundToSym sym BaseIntegerRepr v
    RealValRepr -> W4GE.groundToSym sym BaseRealRepr v
    StringRepr si -> W4GE.groundToSym sym (BaseStringRepr si) v
    SymbolicArrayRepr idxs tp' -> W4GE.groundToSym sym (BaseArrayRepr idxs tp') v
    SymbolicStructRepr tys -> W4GE.groundToSym sym (BaseStructRepr tys) v

    -- Trivial cases
    UnitRepr -> pure ()
    CharRepr -> pure v

    -- Simple recursive cases
    RecursiveRepr symb tyCtx ->
      RV.RolledType <$> concToSym sym iFns fm (unrollType symb tyCtx) v
    SequenceRepr tp' -> do
      l <- traverse (concToSym sym iFns fm tp' . unConcRV') (F.toList v)
      SymSeq.fromListSymSequence sym l
    StringMapRepr tp' ->
      traverse (fmap (W4P.justPartExpr sym) . concToSym sym iFns fm tp' . unConcRV') v
    StructRepr tps ->
      Ctx.zipWithM (\tp' (ConcRV' v') -> RV.RV <$> concToSym sym iFns fm tp' v') tps v
    VectorRepr tp' ->
      traverse (concToSym sym iFns fm tp' . unConcRV') v

    -- Cases with helper functions
    AnyRepr -> concToSymAny sym iFns fm v
    MaybeRepr tp' -> concToSymMaybe sym iFns fm tp' v
    FunctionHandleRepr args ret -> concToSymFn sym iFns fm args ret v
    IntrinsicRepr nm tyCtx -> concToSymIntrinsic sym iFns nm tyCtx v
    ReferenceRepr _tp' -> concToSymRef sym v
    VariantRepr tps -> concToSymVariant sym iFns fm tps v

    -- Incomplete cases
    WordMapRepr _ _ -> fail "concToSym does not yet support WordMap"