-- |
-- Module           : Lang.Crucible.LLVM.Intrinsics.Cast
-- Description      : Cast between bitvectors and pointers in signatures
-- Copyright        : (c) Galois, Inc 2024
-- License          : BSD3
-- Maintainer       : Langston Barrett <langston@galois.com>
-- Stability        : provisional
--
-- The built-in overrides in "Lang.Crucible.LLVM.Intrinsics.Libc" and
-- "Lang.Crucible.LLVM.Intrinsics.LLVM" frequently take arguments of type
-- 'Lang.Crucible.Types.BVType', but at runtime everything is represented as an
-- 'Lang.Crucible.LLVM.MemModel.Pointer.LLVMPtr'. This module contains helpers
-- for \"casting\" between pointers and bitvectors.
------------------------------------------------------------------------

{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Lang.Crucible.LLVM.Intrinsics.Cast
  ( ValCastError
  , printValCastError
  , ArgCast(applyArgCast)
  , ValCast(applyValCast)
  , castLLVMArgs
  , castLLVMRet
  ) where

import           Control.Monad.IO.Class (liftIO)
import           Control.Lens
import qualified Data.Text as Text

import qualified Data.Parameterized.Context as Ctx
import           Data.Parameterized.Some (Some(Some))
import           Data.Parameterized.TraversableFC (fmapFC)

import           What4.FunctionName (FunctionName (functionName))

import           Lang.Crucible.Backend
import           Lang.Crucible.Simulator (SimErrorReason(AssertFailureSimError))
import           Lang.Crucible.Simulator.OverrideSim
import           Lang.Crucible.Simulator.RegMap
import           Lang.Crucible.Types

import           Lang.Crucible.LLVM.MemModel.Partial (ptrToBv)
import           Lang.Crucible.LLVM.MemModel.Pointer

data ValCastError
  = -- | Mismatched number of arguments ('castLLVMArgs') or struct fields
    -- ('castLLVMRet').
    MismatchedShape
    -- | Can\'t cast between these types
  | ValCastError (Some TypeRepr) (Some TypeRepr)

-- | Turn a 'ValCastError' into a human-readable message (lines).
printValCastError :: ValCastError -> [String]
printValCastError :: ValCastError -> [String]
printValCastError =
  \case
    ValCastError
MismatchedShape -> [String
"argument shape mismatch"]
    ValCastError (Some TypeRepr x
ret) (Some TypeRepr x
ret') ->
      [ String
"Cannot cast types"
      , String
"*** Source type: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ TypeRepr x -> String
forall a. Show a => a -> String
show TypeRepr x
ret
      , String
"*** Target type: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ TypeRepr x -> String
forall a. Show a => a -> String
show TypeRepr x
ret'
      ]

-- | A function to (infallibly) cast between 'Ctx.Assignment's of 'RegEntry's.
newtype ArgCast p sym ext args args' =
  ArgCast { forall p sym ext (args :: Ctx CrucibleType)
       (args' :: Ctx CrucibleType).
ArgCast p sym ext args args'
-> forall rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
   Assignment (RegEntry sym) args
   -> OverrideSim p sym ext rtp l a (Assignment (RegEntry sym) args')
applyArgCast :: (forall rtp l a.
    Ctx.Assignment (RegEntry sym) args ->
    OverrideSim p sym ext rtp l a (Ctx.Assignment (RegEntry sym) args')) }

-- | A function to (infallibly) cast a value of types @tp@ to @tp'@.
newtype ValCast p sym ext tp tp' =
  ValCast { forall p sym ext (tp :: CrucibleType) (tp' :: CrucibleType).
ValCast p sym ext tp tp'
-> forall rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
   RegValue sym tp -> OverrideSim p sym ext rtp l a (RegValue sym tp')
applyValCast :: (forall rtp l a.
    RegValue sym tp ->
    OverrideSim p sym ext rtp l a (RegValue sym tp')) }

-- | Attempt to construct a function to cast between 'Ctx.Assignment's of
-- 'RegEntry's.
castLLVMArgs :: forall p sym ext bak args args'.
  IsSymBackend sym bak =>
  -- | Only used in error messages
  FunctionName ->
  bak ->
  CtxRepr args' ->
  CtxRepr args ->
  Either ValCastError (ArgCast p sym ext args args')
castLLVMArgs :: forall p sym ext bak (args :: Ctx CrucibleType)
       (args' :: Ctx CrucibleType).
IsSymBackend sym bak =>
FunctionName
-> bak
-> CtxRepr args'
-> CtxRepr args
-> Either ValCastError (ArgCast p sym ext args args')
castLLVMArgs FunctionName
_fnm bak
_ Assignment TypeRepr args'
Ctx.Empty Assignment TypeRepr args
Ctx.Empty =
  ArgCast p sym ext args args'
-> Either ValCastError (ArgCast p sym ext args args')
forall a b. b -> Either a b
Right ((forall rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
 Assignment (RegEntry sym) args
 -> OverrideSim p sym ext rtp l a (Assignment (RegEntry sym) args'))
-> ArgCast p sym ext args args'
forall p sym ext (args :: Ctx CrucibleType)
       (args' :: Ctx CrucibleType).
(forall rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
 Assignment (RegEntry sym) args
 -> OverrideSim p sym ext rtp l a (Assignment (RegEntry sym) args'))
-> ArgCast p sym ext args args'
ArgCast (\Assignment (RegEntry sym) args
_ -> Assignment (RegEntry sym) args'
-> OverrideSim p sym ext rtp l a (Assignment (RegEntry sym) args')
forall a. a -> OverrideSim p sym ext rtp l a a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Assignment (RegEntry sym) args'
forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty))
castLLVMArgs FunctionName
fnm bak
bak (Assignment TypeRepr ctx
rest' Ctx.:> TypeRepr tp
tp') (Assignment TypeRepr ctx
rest Ctx.:> TypeRepr tp
tp) =
  do ValCast forall rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
RegValue sym tp -> OverrideSim p sym ext rtp l a (RegValue sym tp)
f  <- FunctionName
-> bak
-> TypeRepr tp
-> TypeRepr tp
-> Either ValCastError (ValCast p sym ext tp tp)
forall sym bak (ret :: CrucibleType) (ret' :: CrucibleType) p ext.
IsSymBackend sym bak =>
FunctionName
-> bak
-> TypeRepr ret
-> TypeRepr ret'
-> Either ValCastError (ValCast p sym ext ret ret')
castLLVMRet FunctionName
fnm bak
bak TypeRepr tp
tp TypeRepr tp
tp'
     ArgCast forall rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
Assignment (RegEntry sym) ctx
-> OverrideSim p sym ext rtp l a (Assignment (RegEntry sym) ctx)
fs <- FunctionName
-> bak
-> Assignment TypeRepr ctx
-> Assignment TypeRepr ctx
-> Either ValCastError (ArgCast p sym ext ctx ctx)
forall p sym ext bak (args :: Ctx CrucibleType)
       (args' :: Ctx CrucibleType).
IsSymBackend sym bak =>
FunctionName
-> bak
-> CtxRepr args'
-> CtxRepr args
-> Either ValCastError (ArgCast p sym ext args args')
castLLVMArgs FunctionName
fnm bak
bak Assignment TypeRepr ctx
rest' Assignment TypeRepr ctx
rest
     ArgCast p sym ext args args'
-> Either ValCastError (ArgCast p sym ext args args')
forall a b. b -> Either a b
Right ((forall rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
 Assignment (RegEntry sym) args
 -> OverrideSim p sym ext rtp l a (Assignment (RegEntry sym) args'))
-> ArgCast p sym ext args args'
forall p sym ext (args :: Ctx CrucibleType)
       (args' :: Ctx CrucibleType).
(forall rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
 Assignment (RegEntry sym) args
 -> OverrideSim p sym ext rtp l a (Assignment (RegEntry sym) args'))
-> ArgCast p sym ext args args'
ArgCast
              (\(Assignment (RegEntry sym) ctx
xs Ctx.:> RegEntry sym tp
x) -> do
                    Assignment (RegEntry sym) ctx
xs' <- Assignment (RegEntry sym) ctx
-> OverrideSim p sym ext rtp l a (Assignment (RegEntry sym) ctx)
forall rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
Assignment (RegEntry sym) ctx
-> OverrideSim p sym ext rtp l a (Assignment (RegEntry sym) ctx)
fs Assignment (RegEntry sym) ctx
Assignment (RegEntry sym) ctx
xs
                    RegValue sym tp
x'  <- RegValue sym tp -> OverrideSim p sym ext rtp l a (RegValue sym tp)
forall rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
RegValue sym tp -> OverrideSim p sym ext rtp l a (RegValue sym tp)
f (RegEntry sym tp -> RegValue sym tp
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue RegEntry sym tp
x)
                    Assignment (RegEntry sym) args'
-> OverrideSim p sym ext rtp l a (Assignment (RegEntry sym) args')
forall a. a -> OverrideSim p sym ext rtp l a a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Assignment (RegEntry sym) ctx
xs' Assignment (RegEntry sym) ctx
-> RegEntry sym tp -> Assignment (RegEntry sym) args'
forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
       (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
Ctx.:> TypeRepr tp -> RegValue sym tp -> RegEntry sym tp
forall sym (tp :: CrucibleType).
TypeRepr tp -> RegValue sym tp -> RegEntry sym tp
RegEntry TypeRepr tp
tp' RegValue sym tp
x')))
castLLVMArgs FunctionName
_ bak
_ Assignment TypeRepr args'
_ Assignment TypeRepr args
_ = ValCastError -> Either ValCastError (ArgCast p sym ext args args')
forall a b. a -> Either a b
Left ValCastError
MismatchedShape

-- | Attempt to construct a function to cast values of type @ret@ to type
-- @ret'@.
castLLVMRet ::
  IsSymBackend sym bak =>
  -- | Only used in error messages
  FunctionName ->
  bak ->
  TypeRepr ret  ->
  TypeRepr ret' ->
  Either ValCastError (ValCast p sym ext ret ret')
castLLVMRet :: forall sym bak (ret :: CrucibleType) (ret' :: CrucibleType) p ext.
IsSymBackend sym bak =>
FunctionName
-> bak
-> TypeRepr ret
-> TypeRepr ret'
-> Either ValCastError (ValCast p sym ext ret ret')
castLLVMRet FunctionName
_fnm bak
bak (BVRepr NatRepr n
w) (LLVMPointerRepr NatRepr w
w')
  | Just n :~: w
Refl <- NatRepr n -> NatRepr w -> Maybe (n :~: w)
forall (a :: Natural) (b :: Natural).
NatRepr a -> NatRepr b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality NatRepr n
w NatRepr w
w'
  = ValCast p sym ext ret ret'
-> Either ValCastError (ValCast p sym ext ret ret')
forall a b. b -> Either a b
Right ((forall rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
 RegValue sym ret
 -> OverrideSim p sym ext rtp l a (RegValue sym ret'))
-> ValCast p sym ext ret ret'
forall p sym ext (tp :: CrucibleType) (tp' :: CrucibleType).
(forall rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
 RegValue sym tp
 -> OverrideSim p sym ext rtp l a (RegValue sym tp'))
-> ValCast p sym ext tp tp'
ValCast (IO (LLVMPointer sym n)
-> OverrideSim p sym ext rtp l a (LLVMPointer sym n)
forall a. IO a -> OverrideSim p sym ext rtp l a a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (LLVMPointer sym n)
 -> OverrideSim p sym ext rtp l a (LLVMPointer sym n))
-> (SymExpr sym (BaseBVType n) -> IO (LLVMPointer sym n))
-> SymExpr sym (BaseBVType n)
-> OverrideSim p sym ext rtp l a (LLVMPointer sym n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. sym -> SymExpr sym (BaseBVType n) -> IO (LLVMPtr sym n)
forall sym (w :: Natural).
IsSymInterface sym =>
sym -> SymBV sym w -> IO (LLVMPtr sym w)
llvmPointer_bv (bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak)))
castLLVMRet FunctionName
fnm bak
bak (LLVMPointerRepr NatRepr w
w) (BVRepr NatRepr n
w')
  | Just w :~: n
Refl <- NatRepr w -> NatRepr n -> Maybe (w :~: n)
forall (a :: Natural) (b :: Natural).
NatRepr a -> NatRepr b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality NatRepr w
w NatRepr n
w'
  = let err :: SimErrorReason
err = 
          String -> String -> SimErrorReason
AssertFailureSimError
           String
"Found a pointer where a bitvector was expected"
           (String
"In the arguments or return value of " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Text -> String
Text.unpack (FunctionName -> Text
functionName FunctionName
fnm)) in
    ValCast p sym ext ret ret'
-> Either ValCastError (ValCast p sym ext ret ret')
forall a b. b -> Either a b
Right ((forall rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
 RegValue sym ret
 -> OverrideSim p sym ext rtp l a (RegValue sym ret'))
-> ValCast p sym ext ret ret'
forall p sym ext (tp :: CrucibleType) (tp' :: CrucibleType).
(forall rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
 RegValue sym tp
 -> OverrideSim p sym ext rtp l a (RegValue sym tp'))
-> ValCast p sym ext tp tp'
ValCast (IO (SymExpr sym ('BaseBVType w))
-> OverrideSim p sym ext rtp l a (SymExpr sym ('BaseBVType w))
forall a. IO a -> OverrideSim p sym ext rtp l a a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym ('BaseBVType w))
 -> OverrideSim p sym ext rtp l a (SymExpr sym ('BaseBVType w)))
-> (LLVMPointer sym w -> IO (SymExpr sym ('BaseBVType w)))
-> LLVMPointer sym w
-> OverrideSim p sym ext rtp l a (SymExpr sym ('BaseBVType w))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. bak
-> SimErrorReason
-> LLVMPtr sym w
-> IO (SymExpr sym ('BaseBVType w))
forall sym bak (w :: Natural).
IsSymBackend sym bak =>
bak -> SimErrorReason -> LLVMPtr sym w -> IO (SymBV sym w)
ptrToBv bak
bak SimErrorReason
err))
castLLVMRet FunctionName
fnm bak
bak (VectorRepr TypeRepr tp1
tp) (VectorRepr TypeRepr tp1
tp')
  = do ValCast forall rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
RegValue sym tp1
-> OverrideSim p sym ext rtp l a (RegValue sym tp1)
f <- FunctionName
-> bak
-> TypeRepr tp1
-> TypeRepr tp1
-> Either ValCastError (ValCast p sym ext tp1 tp1)
forall sym bak (ret :: CrucibleType) (ret' :: CrucibleType) p ext.
IsSymBackend sym bak =>
FunctionName
-> bak
-> TypeRepr ret
-> TypeRepr ret'
-> Either ValCastError (ValCast p sym ext ret ret')
castLLVMRet FunctionName
fnm bak
bak TypeRepr tp1
tp TypeRepr tp1
tp'
       ValCast p sym ext ret ret'
-> Either ValCastError (ValCast p sym ext ret ret')
forall a b. b -> Either a b
Right ((forall rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
 RegValue sym ret
 -> OverrideSim p sym ext rtp l a (RegValue sym ret'))
-> ValCast p sym ext ret ret'
forall p sym ext (tp :: CrucibleType) (tp' :: CrucibleType).
(forall rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
 RegValue sym tp
 -> OverrideSim p sym ext rtp l a (RegValue sym tp'))
-> ValCast p sym ext tp tp'
ValCast ((RegValue sym tp1
 -> OverrideSim p sym ext rtp l a (RegValue sym tp1))
-> Vector (RegValue sym tp1)
-> OverrideSim p sym ext rtp l a (Vector (RegValue sym tp1))
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Vector a -> f (Vector b)
traverse RegValue sym tp1
-> OverrideSim p sym ext rtp l a (RegValue sym tp1)
forall rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
RegValue sym tp1
-> OverrideSim p sym ext rtp l a (RegValue sym tp1)
f))
castLLVMRet FunctionName
fnm bak
bak (StructRepr CtxRepr ctx
ctx) (StructRepr CtxRepr ctx
ctx')
  = do ArgCast forall rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
Assignment (RegEntry sym) ctx
-> OverrideSim p sym ext rtp l a (Assignment (RegEntry sym) ctx)
tf <- FunctionName
-> bak
-> CtxRepr ctx
-> CtxRepr ctx
-> Either ValCastError (ArgCast p sym ext ctx ctx)
forall p sym ext bak (args :: Ctx CrucibleType)
       (args' :: Ctx CrucibleType).
IsSymBackend sym bak =>
FunctionName
-> bak
-> CtxRepr args'
-> CtxRepr args
-> Either ValCastError (ArgCast p sym ext args args')
castLLVMArgs FunctionName
fnm bak
bak CtxRepr ctx
ctx' CtxRepr ctx
ctx
       ValCast p sym ext ret ret'
-> Either ValCastError (ValCast p sym ext ret ret')
forall a b. b -> Either a b
Right ((forall rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
 RegValue sym ret
 -> OverrideSim p sym ext rtp l a (RegValue sym ret'))
-> ValCast p sym ext ret ret'
forall p sym ext (tp :: CrucibleType) (tp' :: CrucibleType).
(forall rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
 RegValue sym tp
 -> OverrideSim p sym ext rtp l a (RegValue sym tp'))
-> ValCast p sym ext tp tp'
ValCast (\RegValue sym ret
vals ->
          let vals' :: Assignment (RegEntry sym) ctx
vals' = (forall (x :: CrucibleType).
 TypeRepr x -> RegValue' sym x -> RegEntry sym x)
-> CtxRepr ctx
-> Assignment (RegValue' sym) ctx
-> Assignment (RegEntry sym) ctx
forall {k} (f :: k -> Type) (g :: k -> Type) (h :: k -> Type)
       (a :: Ctx k).
(forall (x :: k). f x -> g x -> h x)
-> Assignment f a -> Assignment g a -> Assignment h a
Ctx.zipWith (\TypeRepr x
tp (RV RegValue sym x
v) -> TypeRepr x -> RegValue sym x -> RegEntry sym x
forall sym (tp :: CrucibleType).
TypeRepr tp -> RegValue sym tp -> RegEntry sym tp
RegEntry TypeRepr x
tp RegValue sym x
v) CtxRepr ctx
ctx RegValue sym ret
Assignment (RegValue' sym) ctx
vals in
          (forall (x :: CrucibleType). RegEntry sym x -> RegValue' sym x)
-> forall (x :: Ctx CrucibleType).
   Assignment (RegEntry sym) x -> Assignment (RegValue' sym) x
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type).
FunctorFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
(forall (x :: CrucibleType). f x -> g x)
-> forall (x :: Ctx CrucibleType). Assignment f x -> Assignment g x
fmapFC (\RegEntry sym x
x -> RegValue sym x -> RegValue' sym x
forall sym (tp :: CrucibleType).
RegValue sym tp -> RegValue' sym tp
RV (RegEntry sym x -> RegValue sym x
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue RegEntry sym x
x)) (Assignment (RegEntry sym) ctx -> Assignment (RegValue' sym) ctx)
-> OverrideSim p sym ext rtp l a (Assignment (RegEntry sym) ctx)
-> OverrideSim p sym ext rtp l a (Assignment (RegValue' sym) ctx)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Assignment (RegEntry sym) ctx
-> OverrideSim p sym ext rtp l a (Assignment (RegEntry sym) ctx)
forall rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
Assignment (RegEntry sym) ctx
-> OverrideSim p sym ext rtp l a (Assignment (RegEntry sym) ctx)
tf Assignment (RegEntry sym) ctx
vals'))

castLLVMRet FunctionName
_fnm bak
_bak TypeRepr ret
ret TypeRepr ret'
ret'
  | Just ret :~: ret'
Refl <- TypeRepr ret -> TypeRepr ret' -> Maybe (ret :~: ret')
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: CrucibleType) (b :: CrucibleType).
TypeRepr a -> TypeRepr b -> Maybe (a :~: b)
testEquality TypeRepr ret
ret TypeRepr ret'
ret'
  = ValCast p sym ext ret ret'
-> Either ValCastError (ValCast p sym ext ret ret')
forall a b. b -> Either a b
Right ((forall rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
 RegValue sym ret
 -> OverrideSim p sym ext rtp l a (RegValue sym ret'))
-> ValCast p sym ext ret ret'
forall p sym ext (tp :: CrucibleType) (tp' :: CrucibleType).
(forall rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
 RegValue sym tp
 -> OverrideSim p sym ext rtp l a (RegValue sym tp'))
-> ValCast p sym ext tp tp'
ValCast RegValue sym ret
-> OverrideSim p sym ext rtp l a (RegValue sym ret)
RegValue sym ret
-> OverrideSim p sym ext rtp l a (RegValue sym ret')
forall a. a -> OverrideSim p sym ext rtp l a a
forall rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
RegValue sym ret
-> OverrideSim p sym ext rtp l a (RegValue sym ret')
forall (m :: Type -> Type) a. Monad m => a -> m a
return)
castLLVMRet FunctionName
_fnm bak
_bak TypeRepr ret
ret TypeRepr ret'
ret' = ValCastError -> Either ValCastError (ValCast p sym ext ret ret')
forall a b. a -> Either a b
Left (Some TypeRepr -> Some TypeRepr -> ValCastError
ValCastError (TypeRepr ret -> Some TypeRepr
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some TypeRepr ret
ret) (TypeRepr ret' -> Some TypeRepr
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some TypeRepr ret'
ret'))