-- |
-- Module           : Lang.Crucible.LLVM.Intrinsics.Cast
-- Description      : Casting to and from the Crucible-LLVM ABI
-- Copyright        : (c) Galois, Inc 2026
-- License          : BSD3
-- Maintainer       : Langston Barrett <langston@galois.com>
-- Stability        : provisional
--
-- In Crucible-LLVM, LLVM pointers and integers are translated to terms
-- of type 'Lang.Crucible.LLVM.MemModel.Pointer.LLVMPointerType'. When
-- writing overrides, it can be convenient to take arguments or return
-- values of 'Lang.Crucible.Types.BVType'. This is done frequently in
-- the built-in overrides in "Lang.Crucible.LLVM.Intrinsics.Libc" and
-- "Lang.Crucible.LLVM.Intrinsics.LLVM". This module contains helpers for
-- \"lowering\" signatures using Crucible bitvectors to ones that use LLVM
-- pointers.
------------------------------------------------------------------------

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

module Lang.Crucible.LLVM.Intrinsics.Cast
  ( -- * There
    CtxToLLVMType
  , ToLLVMType
  , ctxToLLVMType
  , toLLVMType
  , regValuesToLLVM
  , regValueToLLVM
    -- * Back again
  , regValuesFromLLVM
  , regValueFromLLVM
  , regEntriesFromLLVM
  , regMapFromLLVM
    -- * Lowering overrides
  , lowerLLVMOverride
  , lowerMakeOverride
  , lowerOverrideTemplate
  ) where

import           Control.Monad.IO.Class (liftIO)
import           Data.Coerce (coerce)
import qualified Data.Text as Text
import           Data.Type.Equality ((:~:)(Refl), testEquality)

import qualified Data.Parameterized.Context as Ctx
import qualified Data.Parameterized.TraversableFC as TFC

import qualified What4.FunctionName as WFN

import qualified Lang.Crucible.Backend as CB
import           Lang.Crucible.Panic (panic)
import qualified Lang.Crucible.Simulator.OverrideSim as CSO
import qualified Lang.Crucible.Simulator.RegMap as CRM
import qualified Lang.Crucible.Simulator.RegValue as CRV
import qualified Lang.Crucible.Simulator.SimError as CSE
import qualified Lang.Crucible.Types as CT

import qualified Lang.Crucible.LLVM.Intrinsics.Common as IC
import qualified Lang.Crucible.LLVM.Intrinsics.Declare as Decl
import           Lang.Crucible.LLVM.MemModel.Partial (HasLLVMAnn, ptrToBv)
import           Lang.Crucible.LLVM.MemModel.Pointer (LLVMPointerType)
import qualified Lang.Crucible.LLVM.MemModel.Pointer as Ptr

---------------------------------------------------------------------
-- * There

-- | Convert bitvectors to 'LLVMPointer's.
type CtxToLLVMType :: Ctx.Ctx CT.CrucibleType -> Ctx.Ctx CT.CrucibleType
type family CtxToLLVMType t where
  CtxToLLVMType Ctx.EmptyCtx = Ctx.EmptyCtx
  CtxToLLVMType (ctx Ctx.::> tp) = CtxToLLVMType ctx Ctx.::> ToLLVMType tp

-- | Convert bitvectors to 'LLVMPointer's.
type ToLLVMType :: CT.CrucibleType -> CT.CrucibleType
type family ToLLVMType t where
  ToLLVMType (CT.BVType w) = LLVMPointerType w

  -- recursive cases
  ToLLVMType (CT.VectorType tp) = CT.VectorType (ToLLVMType tp)
  ToLLVMType (CT.StructType ctx) = CT.StructType (CtxToLLVMType ctx)

  -- no-ops
  ToLLVMType CT.AnyType = CT.AnyType
  ToLLVMType CT.UnitType = CT.UnitType
  ToLLVMType CT.BoolType = CT.BoolType
  ToLLVMType CT.NatType = CT.NatType
  ToLLVMType CT.IntegerType = CT.IntegerType
  ToLLVMType CT.RealValType = CT.RealValType
  ToLLVMType (CT.FloatType flt) = CT.FloatType flt
  ToLLVMType (CT.IEEEFloatType ps) = CT.IEEEFloatType ps
  ToLLVMType CT.CharType = CT.CharType
  ToLLVMType (CT.StringType si) = CT.StringType si
  ToLLVMType (CT.ComplexRealType) = CT.ComplexRealType
  ToLLVMType (CT.IntrinsicType nm ctx) = CT.IntrinsicType nm ctx

  -- these shouldn't appear in override signaures, so don't worry about them
  ToLLVMType (CT.FunctionHandleType ctx ret) = CT.FunctionHandleType ctx ret
  ToLLVMType (CT.RecursiveType nm ctx) = CT.RecursiveType nm ctx
  ToLLVMType (CT.MaybeType tp) = CT.MaybeType tp
  ToLLVMType (CT.ReferenceType t) = CT.ReferenceType t
  ToLLVMType (CT.SequenceType tp) = CT.SequenceType tp
  ToLLVMType (CT.VariantType ctx) = CT.VariantType ctx
  ToLLVMType (CT.WordMapType n tp) = CT.WordMapType n tp
  ToLLVMType (CT.StringMapType tp) = CT.StringMapType tp
  ToLLVMType (CT.SymbolicArrayType idx t) = CT.SymbolicArrayType idx t
  ToLLVMType (CT.SymbolicStructType ctx) = CT.SymbolicStructType ctx

-- | Value-level analogue of 'CtxToLLVMType'
ctxToLLVMType ::
  Ctx.Assignment CT.TypeRepr ctx ->
  Ctx.Assignment CT.TypeRepr (CtxToLLVMType ctx)
ctxToLLVMType :: forall (ctx :: Ctx CrucibleType).
Assignment TypeRepr ctx -> Assignment TypeRepr (CtxToLLVMType ctx)
ctxToLLVMType =
  \case
    Assignment TypeRepr ctx
Ctx.Empty -> Assignment TypeRepr EmptyCtx
Assignment TypeRepr (CtxToLLVMType ctx)
forall {k} (f :: k -> Type). Assignment f EmptyCtx
Ctx.empty
    Assignment TypeRepr ctx
ctx Ctx.:> TypeRepr tp
t -> Assignment TypeRepr ctx -> Assignment TypeRepr (CtxToLLVMType ctx)
forall (ctx :: Ctx CrucibleType).
Assignment TypeRepr ctx -> Assignment TypeRepr (CtxToLLVMType ctx)
ctxToLLVMType Assignment TypeRepr ctx
ctx Assignment TypeRepr (CtxToLLVMType ctx)
-> TypeRepr (ToLLVMType tp)
-> Assignment TypeRepr (CtxToLLVMType ctx ::> ToLLVMType tp)
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 -> TypeRepr (ToLLVMType tp)
forall (t :: CrucibleType). TypeRepr t -> TypeRepr (ToLLVMType t)
toLLVMType TypeRepr tp
t

-- | Value-level analogue of 'ToLLVMType'
toLLVMType ::
  CT.TypeRepr t ->
  CT.TypeRepr (ToLLVMType t)
toLLVMType :: forall (t :: CrucibleType). TypeRepr t -> TypeRepr (ToLLVMType t)
toLLVMType =
  \case
    CT.BVRepr NatRepr n
w -> NatRepr n -> TypeRepr (LLVMPointerType n)
forall (ty :: CrucibleType) (w :: Natural).
(1 <= w, ty ~ LLVMPointerType w) =>
NatRepr w -> TypeRepr ty
Ptr.LLVMPointerRepr NatRepr n
w

    -- recursive cases
    CT.VectorRepr TypeRepr tp1
tp -> TypeRepr (ToLLVMType tp1)
-> TypeRepr ('VectorType (ToLLVMType tp1))
forall (tp1 :: CrucibleType).
TypeRepr tp1 -> TypeRepr ('VectorType tp1)
CT.VectorRepr (TypeRepr tp1 -> TypeRepr (ToLLVMType tp1)
forall (t :: CrucibleType). TypeRepr t -> TypeRepr (ToLLVMType t)
toLLVMType TypeRepr tp1
tp)
    CT.StructRepr CtxRepr ctx
ctx -> CtxRepr (CtxToLLVMType ctx)
-> TypeRepr ('StructType (CtxToLLVMType ctx))
forall (ctx :: Ctx CrucibleType).
CtxRepr ctx -> TypeRepr ('StructType ctx)
CT.StructRepr (CtxRepr ctx -> CtxRepr (CtxToLLVMType ctx)
forall (ctx :: Ctx CrucibleType).
Assignment TypeRepr ctx -> Assignment TypeRepr (CtxToLLVMType ctx)
ctxToLLVMType CtxRepr ctx
ctx)

    -- no-ops
    TypeRepr t
CT.AnyRepr -> TypeRepr 'AnyType
TypeRepr (ToLLVMType t)
CT.AnyRepr
    TypeRepr t
CT.UnitRepr -> TypeRepr 'UnitType
TypeRepr (ToLLVMType t)
CT.UnitRepr
    TypeRepr t
CT.BoolRepr -> TypeRepr ('BaseToType BaseBoolType)
TypeRepr (ToLLVMType t)
CT.BoolRepr
    TypeRepr t
CT.NatRepr -> TypeRepr 'NatType
TypeRepr (ToLLVMType t)
CT.NatRepr
    TypeRepr t
CT.IntegerRepr -> TypeRepr ('BaseToType BaseIntegerType)
TypeRepr (ToLLVMType t)
CT.IntegerRepr
    TypeRepr t
CT.RealValRepr -> TypeRepr ('BaseToType BaseRealType)
TypeRepr (ToLLVMType t)
CT.RealValRepr
    CT.FloatRepr FloatInfoRepr flt
flt -> FloatInfoRepr flt -> TypeRepr ('FloatType flt)
forall (flt :: FloatInfo).
FloatInfoRepr flt -> TypeRepr ('FloatType flt)
CT.FloatRepr FloatInfoRepr flt
flt
    CT.IEEEFloatRepr FloatPrecisionRepr ps
ps -> FloatPrecisionRepr ps -> TypeRepr ('BaseToType (BaseFloatType ps))
forall (ps :: FloatPrecision).
FloatPrecisionRepr ps -> TypeRepr ('BaseToType (BaseFloatType ps))
CT.IEEEFloatRepr FloatPrecisionRepr ps
ps
    TypeRepr t
CT.CharRepr -> TypeRepr 'CharType
TypeRepr (ToLLVMType t)
CT.CharRepr
    CT.StringRepr StringInfoRepr si
si -> StringInfoRepr si -> TypeRepr ('BaseToType (BaseStringType si))
forall (si :: StringInfo).
StringInfoRepr si -> TypeRepr ('BaseToType (BaseStringType si))
CT.StringRepr StringInfoRepr si
si
    TypeRepr t
CT.ComplexRealRepr -> TypeRepr ('BaseToType BaseComplexType)
TypeRepr (ToLLVMType t)
CT.ComplexRealRepr
    CT.IntrinsicRepr SymbolRepr nm
nm CtxRepr ctx
ctx -> SymbolRepr nm -> CtxRepr ctx -> TypeRepr ('IntrinsicType nm ctx)
forall (nm :: Symbol) (ctx :: Ctx CrucibleType).
SymbolRepr nm -> CtxRepr ctx -> TypeRepr ('IntrinsicType nm ctx)
CT.IntrinsicRepr SymbolRepr nm
nm CtxRepr ctx
ctx

    -- these shouldn't appear in override signaures, so don't worry about them
    t :: TypeRepr t
t@CT.FunctionHandleRepr {} -> TypeRepr t
TypeRepr (ToLLVMType t)
t
    t :: TypeRepr t
t@CT.RecursiveRepr {} -> TypeRepr t
TypeRepr (ToLLVMType t)
t
    t :: TypeRepr t
t@CT.MaybeRepr {} -> TypeRepr t
TypeRepr (ToLLVMType t)
t
    t :: TypeRepr t
t@CT.SequenceRepr {} -> TypeRepr t
TypeRepr (ToLLVMType t)
t
    t :: TypeRepr t
t@CT.ReferenceRepr {} -> TypeRepr t
TypeRepr (ToLLVMType t)
t
    t :: TypeRepr t
t@CT.VariantRepr {} -> TypeRepr t
TypeRepr (ToLLVMType t)
t
    t :: TypeRepr t
t@CT.WordMapRepr {} -> TypeRepr t
TypeRepr (ToLLVMType t)
t
    t :: TypeRepr t
t@CT.StringMapRepr {} -> TypeRepr t
TypeRepr (ToLLVMType t)
t
    t :: TypeRepr t
t@CT.SymbolicArrayRepr {} -> TypeRepr t
TypeRepr (ToLLVMType t)
t
    t :: TypeRepr t
t@CT.SymbolicStructRepr {} -> TypeRepr t
TypeRepr (ToLLVMType t)
t

-- | 'regValueToLLVM' over an 'Ctx.Assignment'
regValuesToLLVM ::
  CB.IsSymInterface sym =>
  sym ->
  Ctx.Assignment CT.TypeRepr tys ->
  Ctx.Assignment (CRV.RegValue' sym) tys ->
  IO (Ctx.Assignment  (CRV.RegValue' sym) (CtxToLLVMType tys))
regValuesToLLVM :: forall sym (tys :: Ctx CrucibleType).
IsSymInterface sym =>
sym
-> Assignment TypeRepr tys
-> Assignment (RegValue' sym) tys
-> IO (Assignment (RegValue' sym) (CtxToLLVMType tys))
regValuesToLLVM sym
sym Assignment TypeRepr tys
tys Assignment (RegValue' sym) tys
vals =
  case (Assignment TypeRepr tys
tys, Assignment (RegValue' sym) tys
vals) of
    (Assignment TypeRepr tys
Ctx.Empty, Assignment (RegValue' sym) tys
Ctx.Empty) -> Assignment (RegValue' sym) EmptyCtx
-> IO (Assignment (RegValue' sym) EmptyCtx)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Assignment (RegValue' sym) EmptyCtx
forall {k} (f :: k -> Type). Assignment f EmptyCtx
Ctx.empty
    (Assignment TypeRepr ctx
restTys Ctx.:> TypeRepr tp
ty, Assignment (RegValue' sym) ctx
restVals Ctx.:> CRV.RV RegValue sym tp
val) -> do
      Assignment (RegValue' sym) (CtxToLLVMType ctx)
rest <- sym
-> Assignment TypeRepr ctx
-> Assignment (RegValue' sym) ctx
-> IO (Assignment (RegValue' sym) (CtxToLLVMType ctx))
forall sym (tys :: Ctx CrucibleType).
IsSymInterface sym =>
sym
-> Assignment TypeRepr tys
-> Assignment (RegValue' sym) tys
-> IO (Assignment (RegValue' sym) (CtxToLLVMType tys))
regValuesToLLVM sym
sym Assignment TypeRepr ctx
restTys Assignment (RegValue' sym) ctx
Assignment (RegValue' sym) ctx
restVals
      RegValue sym (ToLLVMType tp)
val' <- sym
-> TypeRepr tp
-> RegValue sym tp
-> IO (RegValue sym (ToLLVMType tp))
forall sym (ty :: CrucibleType).
IsSymInterface sym =>
sym
-> TypeRepr ty
-> RegValue sym ty
-> IO (RegValue sym (ToLLVMType ty))
regValueToLLVM sym
sym TypeRepr tp
ty RegValue sym tp
RegValue sym tp
val
      Assignment (RegValue' sym) (CtxToLLVMType ctx ::> ToLLVMType tp)
-> IO
     (Assignment (RegValue' sym) (CtxToLLVMType ctx ::> ToLLVMType tp))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Assignment (RegValue' sym) (CtxToLLVMType ctx)
rest Assignment (RegValue' sym) (CtxToLLVMType ctx)
-> RegValue' sym (ToLLVMType tp)
-> Assignment (RegValue' sym) (CtxToLLVMType ctx ::> ToLLVMType tp)
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.:> RegValue sym (ToLLVMType tp) -> RegValue' sym (ToLLVMType tp)
forall sym (tp :: CrucibleType).
RegValue sym tp -> RegValue' sym tp
CRV.RV RegValue sym (ToLLVMType tp)
val')

-- | Convert a 'CRV.RegValue' to its corresponding LLVM type (replacing
-- bitvectors with LLVM pointers).
regValueToLLVM ::
  CB.IsSymInterface sym =>
  sym ->
  CT.TypeRepr ty ->
  CRV.RegValue sym ty ->
  IO (CRV.RegValue sym (ToLLVMType ty))
regValueToLLVM :: forall sym (ty :: CrucibleType).
IsSymInterface sym =>
sym
-> TypeRepr ty
-> RegValue sym ty
-> IO (RegValue sym (ToLLVMType ty))
regValueToLLVM sym
sym TypeRepr ty
ty RegValue sym ty
val =
  case TypeRepr ty
ty of
    CT.BVRepr {} -> sym -> SymBV sym n -> IO (LLVMPtr sym n)
forall sym (w :: Natural).
IsSymInterface sym =>
sym -> SymBV sym w -> IO (LLVMPtr sym w)
Ptr.llvmPointer_bv sym
sym RegValue sym ty
SymBV sym n
val

    -- recursive cases
    CT.VectorRepr TypeRepr tp1
elemTy -> (RegValue sym tp1 -> IO (RegValue sym (ToLLVMType tp1)))
-> Vector (RegValue sym tp1)
-> IO (Vector (RegValue sym (ToLLVMType 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 (sym
-> TypeRepr tp1
-> RegValue sym tp1
-> IO (RegValue sym (ToLLVMType tp1))
forall sym (ty :: CrucibleType).
IsSymInterface sym =>
sym
-> TypeRepr ty
-> RegValue sym ty
-> IO (RegValue sym (ToLLVMType ty))
regValueToLLVM sym
sym TypeRepr tp1
elemTy) Vector (RegValue sym tp1)
RegValue sym ty
val
    CT.StructRepr CtxRepr ctx
fieldTys -> sym
-> CtxRepr ctx
-> Assignment (RegValue' sym) ctx
-> IO (Assignment (RegValue' sym) (CtxToLLVMType ctx))
forall sym (tys :: Ctx CrucibleType).
IsSymInterface sym =>
sym
-> Assignment TypeRepr tys
-> Assignment (RegValue' sym) tys
-> IO (Assignment (RegValue' sym) (CtxToLLVMType tys))
regValuesToLLVM sym
sym CtxRepr ctx
fieldTys RegValue sym ty
Assignment (RegValue' sym) ctx
val

    -- no-ops
    TypeRepr ty
CT.AnyRepr -> AnyValue sym -> IO (AnyValue sym)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure AnyValue sym
RegValue sym ty
val
    TypeRepr ty
CT.UnitRepr -> () -> IO ()
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ()
RegValue sym ty
val
    TypeRepr ty
CT.BoolRepr -> SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure RegValue sym ty
SymExpr sym BaseBoolType
val
    TypeRepr ty
CT.NatRepr -> SymNat sym -> IO (SymNat sym)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure RegValue sym ty
SymNat sym
val
    TypeRepr ty
CT.IntegerRepr -> SymExpr sym BaseIntegerType -> IO (SymExpr sym BaseIntegerType)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure RegValue sym ty
SymExpr sym BaseIntegerType
val
    TypeRepr ty
CT.RealValRepr -> SymExpr sym BaseRealType -> IO (SymExpr sym BaseRealType)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure RegValue sym ty
SymExpr sym BaseRealType
val
    CT.FloatRepr {} -> SymExpr sym (SymInterpretedFloatType sym flt)
-> IO (SymExpr sym (SymInterpretedFloatType sym flt))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure RegValue sym ty
SymExpr sym (SymInterpretedFloatType sym flt)
val
    CT.IEEEFloatRepr {} -> SymExpr sym (BaseFloatType ps)
-> IO (SymExpr sym (BaseFloatType ps))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure RegValue sym ty
SymExpr sym (BaseFloatType ps)
val
    TypeRepr ty
CT.CharRepr -> Word16 -> IO Word16
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Word16
RegValue sym ty
val
    CT.StringRepr {} -> SymExpr sym (BaseStringType si)
-> IO (SymExpr sym (BaseStringType si))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure RegValue sym ty
SymExpr sym (BaseStringType si)
val
    TypeRepr ty
CT.ComplexRealRepr -> SymExpr sym BaseComplexType -> IO (SymExpr sym BaseComplexType)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure RegValue sym ty
SymExpr sym BaseComplexType
val
    CT.IntrinsicRepr {} -> Intrinsic sym nm ctx -> IO (Intrinsic sym nm ctx)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Intrinsic sym nm ctx
RegValue sym ty
val

    -- these shouldn't appear in override signaures, so don't worry about them
    CT.FunctionHandleRepr {} -> FnVal sym ctx ret -> IO (FnVal sym ctx ret)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure FnVal sym ctx ret
RegValue sym ty
val
    CT.MaybeRepr {} -> PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1)
-> IO (PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure RegValue sym ty
PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1)
val
    CT.SequenceRepr {} -> SymSequence sym (RegValue sym tp1)
-> IO (SymSequence sym (RegValue sym tp1))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure SymSequence sym (RegValue sym tp1)
RegValue sym ty
val
    CT.RecursiveRepr {} -> RolledType sym nm ctx -> IO (RolledType sym nm ctx)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure RolledType sym nm ctx
RegValue sym ty
val
    CT.ReferenceRepr {} -> MuxTree sym (RefCell a) -> IO (MuxTree sym (RefCell a))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure MuxTree sym (RefCell a)
RegValue sym ty
val
    CT.VariantRepr {} -> Assignment (VariantBranch sym) ctx
-> IO (Assignment (VariantBranch sym) ctx)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure RegValue sym ty
Assignment (VariantBranch sym) ctx
val
    CT.WordMapRepr {} -> WordMap sym n tp1 -> IO (WordMap sym n tp1)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure RegValue sym ty
WordMap sym n tp1
val
    CT.StringMapRepr {} -> Map Text (PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1))
-> IO
     (Map Text (PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1)))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Map Text (PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1))
RegValue sym ty
val
    CT.SymbolicArrayRepr {} -> SymExpr sym (BaseArrayType (idx ::> tp1) t)
-> IO (SymExpr sym (BaseArrayType (idx ::> tp1) t))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure RegValue sym ty
SymExpr sym (BaseArrayType (idx ::> tp1) t)
val
    CT.SymbolicStructRepr {} -> SymExpr sym (BaseStructType ctx)
-> IO (SymExpr sym (BaseStructType ctx))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure RegValue sym ty
SymExpr sym (BaseStructType ctx)
val

---------------------------------------------------------------------
-- * Back again

-- | Map 'regValueFromLLVM' over an 'Ctx.Assignment'.
regValuesFromLLVM ::
  CB.IsSymBackend sym bak =>
  bak ->
  -- | Only used in error messages
  WFN.FunctionName ->
  Ctx.Assignment CT.TypeRepr tys ->
  Ctx.Assignment CT.TypeRepr (CtxToLLVMType tys) ->
  Ctx.Assignment (CRV.RegValue' sym) (CtxToLLVMType tys) ->
  IO (Ctx.Assignment (CRV.RegValue' sym) tys)
regValuesFromLLVM :: forall sym bak (tys :: Ctx CrucibleType).
IsSymBackend sym bak =>
bak
-> FunctionName
-> Assignment TypeRepr tys
-> Assignment TypeRepr (CtxToLLVMType tys)
-> Assignment (RegValue' sym) (CtxToLLVMType tys)
-> IO (Assignment (RegValue' sym) tys)
regValuesFromLLVM bak
bak FunctionName
fNm Assignment TypeRepr tys
wanteds Assignment TypeRepr (CtxToLLVMType tys)
tys Assignment (RegValue' sym) (CtxToLLVMType tys)
vals =
  case (Assignment TypeRepr tys
wanteds, Assignment TypeRepr (CtxToLLVMType tys)
tys) of
    (Assignment TypeRepr tys
Ctx.Empty, Assignment TypeRepr EmptyCtx
Assignment TypeRepr (CtxToLLVMType tys)
Ctx.Empty) -> Assignment (RegValue' sym) tys
-> IO (Assignment (RegValue' sym) tys)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Assignment (RegValue' sym) tys
Assignment (RegValue' sym) (CtxToLLVMType tys)
vals
    (Assignment TypeRepr ctx
restWanted Ctx.:> TypeRepr tp
w, Assignment TypeRepr ctx
restTys Ctx.:> TypeRepr tp
t) -> do
      case Assignment (RegValue' sym) (CtxToLLVMType tys)
vals of
        Assignment (RegValue' sym) ctx
rest Ctx.:> CRV.RV RegValue sym tp
val -> do
          Assignment (RegValue' sym) ctx
rest' <- bak
-> FunctionName
-> Assignment TypeRepr ctx
-> Assignment TypeRepr (CtxToLLVMType ctx)
-> Assignment (RegValue' sym) (CtxToLLVMType ctx)
-> IO (Assignment (RegValue' sym) ctx)
forall sym bak (tys :: Ctx CrucibleType).
IsSymBackend sym bak =>
bak
-> FunctionName
-> Assignment TypeRepr tys
-> Assignment TypeRepr (CtxToLLVMType tys)
-> Assignment (RegValue' sym) (CtxToLLVMType tys)
-> IO (Assignment (RegValue' sym) tys)
regValuesFromLLVM bak
bak FunctionName
fNm Assignment TypeRepr ctx
restWanted Assignment TypeRepr ctx
Assignment TypeRepr (CtxToLLVMType ctx)
restTys Assignment (RegValue' sym) ctx
Assignment (RegValue' sym) (CtxToLLVMType ctx)
rest
          RegValue sym tp
val' <- bak
-> FunctionName
-> TypeRepr tp
-> TypeRepr (ToLLVMType tp)
-> RegValue sym (ToLLVMType tp)
-> IO (RegValue sym tp)
forall sym bak (ty :: CrucibleType).
IsSymBackend sym bak =>
bak
-> FunctionName
-> TypeRepr ty
-> TypeRepr (ToLLVMType ty)
-> RegValue sym (ToLLVMType ty)
-> IO (RegValue sym ty)
regValueFromLLVM bak
bak FunctionName
fNm TypeRepr tp
w TypeRepr tp
TypeRepr (ToLLVMType tp)
t RegValue sym tp
RegValue sym (ToLLVMType tp)
val
          Assignment (RegValue' sym) tys
-> IO (Assignment (RegValue' sym) tys)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Assignment (RegValue' sym) ctx
rest' Assignment (RegValue' sym) ctx
-> RegValue' sym tp -> Assignment (RegValue' sym) tys
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.:> RegValue sym tp -> RegValue' sym tp
forall sym (tp :: CrucibleType).
RegValue sym tp -> RegValue' sym tp
CRV.RV RegValue sym tp
val')

-- | Convert a 'CRV.RegValue' from its corresponding LLVM type (replacing LLVM
-- pointers with bitvectors where needed).
regValueFromLLVM ::
  forall sym bak ty.
  CB.IsSymBackend sym bak =>
  bak ->
  -- | Only used in error messages
  WFN.FunctionName ->
  CT.TypeRepr ty ->
  CT.TypeRepr (ToLLVMType ty) ->
  CRV.RegValue sym (ToLLVMType ty) ->
  IO (CRV.RegValue sym ty)
regValueFromLLVM :: forall sym bak (ty :: CrucibleType).
IsSymBackend sym bak =>
bak
-> FunctionName
-> TypeRepr ty
-> TypeRepr (ToLLVMType ty)
-> RegValue sym (ToLLVMType ty)
-> IO (RegValue sym ty)
regValueFromLLVM bak
bak FunctionName
fNm TypeRepr ty
wanted TypeRepr (ToLLVMType ty)
ty RegValue sym (ToLLVMType ty)
val = do
  case (TypeRepr ty
wanted, TypeRepr (ToLLVMType ty)
ty) of
    (CT.BVRepr NatRepr n
w, Ptr.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' -> do
        let err :: SimErrorReason
err = 
              String -> String -> SimErrorReason
CSE.AssertFailureSimError
               String
"Found a pointer where a bitvector was expected"
               (String
"In the arguments of "
                String -> String -> String
forall a. [a] -> [a] -> [a]
++ Text -> String
Text.unpack (FunctionName -> Text
WFN.functionName FunctionName
fNm))
        bak -> SimErrorReason -> LLVMPtr sym n -> IO (SymBV sym n)
forall sym bak (w :: Natural).
IsSymBackend sym bak =>
bak -> SimErrorReason -> LLVMPtr sym w -> IO (SymBV sym w)
ptrToBv bak
bak SimErrorReason
err LLVMPtr sym n
RegValue sym (ToLLVMType ty)
val
    (CT.BVRepr {}, TypeRepr (ToLLVMType ty)
_) ->
      String -> [String] -> IO (SymExpr sym (BaseBVType n))
forall a. HasCallStack => String -> [String] -> a
panic
        String
"regValueFromLLVM"
        [ String
"Pointer and bitvector of different sizes related by ToLLVMType!"
        , String
"This is impossible by the definition of ToLLVMType."
        ]

    -- recursive cases

    (CT.VectorRepr TypeRepr tp1
wantedElemTy, CT.VectorRepr TypeRepr tp1
elemTy) ->
      (RegValue sym tp1 -> IO (RegValue sym tp1))
-> Vector (RegValue sym tp1) -> IO (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 (bak
-> FunctionName
-> TypeRepr tp1
-> TypeRepr (ToLLVMType tp1)
-> RegValue sym (ToLLVMType tp1)
-> IO (RegValue sym tp1)
forall sym bak (ty :: CrucibleType).
IsSymBackend sym bak =>
bak
-> FunctionName
-> TypeRepr ty
-> TypeRepr (ToLLVMType ty)
-> RegValue sym (ToLLVMType ty)
-> IO (RegValue sym ty)
regValueFromLLVM bak
bak FunctionName
fNm TypeRepr tp1
wantedElemTy TypeRepr tp1
TypeRepr (ToLLVMType tp1)
elemTy) Vector (RegValue sym tp1)
RegValue sym (ToLLVMType ty)
val

    (CT.StructRepr CtxRepr ctx
wantedFieldTys, CT.StructRepr CtxRepr ctx
fieldTys) ->
      bak
-> FunctionName
-> CtxRepr ctx
-> Assignment TypeRepr (CtxToLLVMType ctx)
-> Assignment (RegValue' sym) (CtxToLLVMType ctx)
-> IO (Assignment (RegValue' sym) ctx)
forall sym bak (tys :: Ctx CrucibleType).
IsSymBackend sym bak =>
bak
-> FunctionName
-> Assignment TypeRepr tys
-> Assignment TypeRepr (CtxToLLVMType tys)
-> Assignment (RegValue' sym) (CtxToLLVMType tys)
-> IO (Assignment (RegValue' sym) tys)
regValuesFromLLVM bak
bak FunctionName
fNm CtxRepr ctx
wantedFieldTys CtxRepr ctx
Assignment TypeRepr (CtxToLLVMType ctx)
fieldTys RegValue sym (ToLLVMType ty)
Assignment (RegValue' sym) (CtxToLLVMType ctx)
val

    -- no-ops

    (TypeRepr ty
CT.AnyRepr, TypeRepr (ToLLVMType ty)
_) -> AnyValue sym -> IO (AnyValue sym)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure AnyValue sym
RegValue sym (ToLLVMType ty)
val
    (TypeRepr ty
CT.UnitRepr, TypeRepr (ToLLVMType ty)
_) ->  () -> IO ()
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ()
RegValue sym (ToLLVMType ty)
val
    (TypeRepr ty
CT.BoolRepr, TypeRepr (ToLLVMType ty)
_) ->  SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure RegValue sym (ToLLVMType ty)
SymExpr sym BaseBoolType
val
    (TypeRepr ty
CT.NatRepr, TypeRepr (ToLLVMType ty)
_) -> SymNat sym -> IO (SymNat sym)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure RegValue sym (ToLLVMType ty)
SymNat sym
val
    (TypeRepr ty
CT.IntegerRepr, TypeRepr (ToLLVMType ty)
_) -> SymExpr sym BaseIntegerType -> IO (SymExpr sym BaseIntegerType)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure RegValue sym (ToLLVMType ty)
SymExpr sym BaseIntegerType
val
    (TypeRepr ty
CT.RealValRepr, TypeRepr (ToLLVMType ty)
_) -> SymExpr sym BaseRealType -> IO (SymExpr sym BaseRealType)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure RegValue sym (ToLLVMType ty)
SymExpr sym BaseRealType
val
    (TypeRepr ty
CT.CharRepr, TypeRepr (ToLLVMType ty)
_) -> Word16 -> IO Word16
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Word16
RegValue sym (ToLLVMType ty)
val
    (TypeRepr ty
CT.ComplexRealRepr, TypeRepr (ToLLVMType ty)
_) -> SymExpr sym BaseComplexType -> IO (SymExpr sym BaseComplexType)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure RegValue sym (ToLLVMType ty)
SymExpr sym BaseComplexType
val
    (CT.FloatRepr {}, TypeRepr (ToLLVMType ty)
_) -> SymExpr sym (SymInterpretedFloatType sym flt)
-> IO (SymExpr sym (SymInterpretedFloatType sym flt))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure RegValue sym (ToLLVMType ty)
SymExpr sym (SymInterpretedFloatType sym flt)
val
    (CT.IEEEFloatRepr {}, TypeRepr (ToLLVMType ty)
_) -> SymExpr sym (BaseFloatType ps)
-> IO (SymExpr sym (BaseFloatType ps))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure RegValue sym (ToLLVMType ty)
SymExpr sym (BaseFloatType ps)
val
    (CT.StringRepr {}, TypeRepr (ToLLVMType ty)
_) -> SymExpr sym (BaseStringType si)
-> IO (SymExpr sym (BaseStringType si))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure RegValue sym (ToLLVMType ty)
SymExpr sym (BaseStringType si)
val
    (CT.IntrinsicRepr {}, TypeRepr (ToLLVMType ty)
_) -> Intrinsic sym nm ctx -> IO (Intrinsic sym nm ctx)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Intrinsic sym nm ctx
RegValue sym (ToLLVMType ty)
val

    -- these shouldn't appear in override signaures, so don't worry about them

    (CT.FunctionHandleRepr {}, TypeRepr (ToLLVMType ty)
_) -> FnVal sym ctx ret -> IO (FnVal sym ctx ret)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure FnVal sym ctx ret
RegValue sym (ToLLVMType ty)
val
    (CT.MaybeRepr {}, TypeRepr (ToLLVMType ty)
_) -> PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1)
-> IO (PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure RegValue sym (ToLLVMType ty)
PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1)
val
    (CT.SequenceRepr {}, TypeRepr (ToLLVMType ty)
_) -> SymSequence sym (RegValue sym tp1)
-> IO (SymSequence sym (RegValue sym tp1))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure SymSequence sym (RegValue sym tp1)
RegValue sym (ToLLVMType ty)
val
    (CT.RecursiveRepr {}, TypeRepr (ToLLVMType ty)
_) -> RolledType sym nm ctx -> IO (RolledType sym nm ctx)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure RolledType sym nm ctx
RegValue sym (ToLLVMType ty)
val
    (CT.ReferenceRepr {}, TypeRepr (ToLLVMType ty)
_) -> MuxTree sym (RefCell a) -> IO (MuxTree sym (RefCell a))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure MuxTree sym (RefCell a)
RegValue sym (ToLLVMType ty)
val
    (CT.VariantRepr {}, TypeRepr (ToLLVMType ty)
_) -> Assignment (VariantBranch sym) ctx
-> IO (Assignment (VariantBranch sym) ctx)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure RegValue sym (ToLLVMType ty)
Assignment (VariantBranch sym) ctx
val
    (CT.WordMapRepr {}, TypeRepr (ToLLVMType ty)
_) -> WordMap sym n tp1 -> IO (WordMap sym n tp1)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure RegValue sym (ToLLVMType ty)
WordMap sym n tp1
val
    (CT.StringMapRepr {}, TypeRepr (ToLLVMType ty)
_) -> Map Text (PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1))
-> IO
     (Map Text (PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1)))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Map Text (PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1))
RegValue sym (ToLLVMType ty)
val
    (CT.SymbolicArrayRepr {}, TypeRepr (ToLLVMType ty)
_) -> SymExpr sym (BaseArrayType (idx ::> tp1) t)
-> IO (SymExpr sym (BaseArrayType (idx ::> tp1) t))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure RegValue sym (ToLLVMType ty)
SymExpr sym (BaseArrayType (idx ::> tp1) t)
val
    (CT.SymbolicStructRepr {}, TypeRepr (ToLLVMType ty)
_) -> SymExpr sym (BaseStructType ctx)
-> IO (SymExpr sym (BaseStructType ctx))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure RegValue sym (ToLLVMType ty)
SymExpr sym (BaseStructType ctx)
val

-- | Map 'regValueFromLLVM' over an 'Ctx.Assignment' of 'CRM.RegEntry's.
regEntriesFromLLVM ::
  CB.IsSymBackend sym bak =>
  bak ->
  -- | Only used in error messages
  WFN.FunctionName ->
  Ctx.Assignment CT.TypeRepr tys ->
  Ctx.Assignment CT.TypeRepr (CtxToLLVMType tys) ->
  Ctx.Assignment (CRM.RegEntry sym) (CtxToLLVMType tys) ->
  IO (Ctx.Assignment (CRM.RegEntry sym) tys)
regEntriesFromLLVM :: forall sym bak (tys :: Ctx CrucibleType).
IsSymBackend sym bak =>
bak
-> FunctionName
-> Assignment TypeRepr tys
-> Assignment TypeRepr (CtxToLLVMType tys)
-> Assignment (RegEntry sym) (CtxToLLVMType tys)
-> IO (Assignment (RegEntry sym) tys)
regEntriesFromLLVM bak
bak FunctionName
fNm Assignment TypeRepr tys
wanteds Assignment TypeRepr (CtxToLLVMType tys)
tys Assignment (RegEntry sym) (CtxToLLVMType tys)
vals = do
  let cast :: Assignment (RegValue' sym) (CtxToLLVMType tys)
-> IO (Assignment (RegValue' sym) tys)
cast = bak
-> FunctionName
-> Assignment TypeRepr tys
-> Assignment TypeRepr (CtxToLLVMType tys)
-> Assignment (RegValue' sym) (CtxToLLVMType tys)
-> IO (Assignment (RegValue' sym) tys)
forall sym bak (tys :: Ctx CrucibleType).
IsSymBackend sym bak =>
bak
-> FunctionName
-> Assignment TypeRepr tys
-> Assignment TypeRepr (CtxToLLVMType tys)
-> Assignment (RegValue' sym) (CtxToLLVMType tys)
-> IO (Assignment (RegValue' sym) tys)
regValuesFromLLVM bak
bak FunctionName
fNm Assignment TypeRepr tys
wanteds Assignment TypeRepr (CtxToLLVMType tys)
tys
  (forall (x :: CrucibleType).
 TypeRepr x -> RegValue' sym x -> RegEntry sym x)
-> Assignment TypeRepr tys
-> Assignment (RegValue' sym) tys
-> Assignment (RegEntry sym) tys
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
ty (CRV.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
CRM.RegEntry TypeRepr x
ty RegValue sym x
v) Assignment TypeRepr tys
wanteds
    (Assignment (RegValue' sym) tys -> Assignment (RegEntry sym) tys)
-> IO (Assignment (RegValue' sym) tys)
-> IO (Assignment (RegEntry sym) tys)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Assignment (RegValue' sym) (CtxToLLVMType tys)
-> IO (Assignment (RegValue' sym) tys)
cast ((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
TFC.fmapFC (\(CRM.RegEntry TypeRepr x
_ty RegValue sym x
v) -> RegValue sym x -> RegValue' sym x
forall sym (tp :: CrucibleType).
RegValue sym tp -> RegValue' sym tp
CRM.RV RegValue sym x
v) Assignment (RegEntry sym) (CtxToLLVMType tys)
vals)

-- | Map 'regValueFromLLVM' over a 'CRM.RegMap'.
regMapFromLLVM ::
  forall sym bak tys.
  CB.IsSymBackend sym bak =>
  bak ->
  -- | Only used in error messages
  WFN.FunctionName ->
  Ctx.Assignment CT.TypeRepr tys ->
  Ctx.Assignment CT.TypeRepr (CtxToLLVMType tys) ->
  CRM.RegMap sym (CtxToLLVMType tys) ->
  IO (CRM.RegMap sym tys)
regMapFromLLVM :: forall sym bak (tys :: Ctx CrucibleType).
IsSymBackend sym bak =>
bak
-> FunctionName
-> Assignment TypeRepr tys
-> Assignment TypeRepr (CtxToLLVMType tys)
-> RegMap sym (CtxToLLVMType tys)
-> IO (RegMap sym tys)
regMapFromLLVM bak
bak FunctionName
fNm Assignment TypeRepr tys
wanteds Assignment TypeRepr (CtxToLLVMType tys)
tys =
  (Assignment (RegEntry sym) (CtxToLLVMType tys)
 -> IO (Assignment (RegEntry sym) tys))
-> RegMap sym (CtxToLLVMType tys) -> IO (RegMap sym tys)
forall a b. Coercible a b => a -> b
coerce (bak
-> FunctionName
-> Assignment TypeRepr tys
-> Assignment TypeRepr (CtxToLLVMType tys)
-> Assignment (RegEntry sym) (CtxToLLVMType tys)
-> IO (Assignment (RegEntry sym) tys)
forall sym bak (tys :: Ctx CrucibleType).
IsSymBackend sym bak =>
bak
-> FunctionName
-> Assignment TypeRepr tys
-> Assignment TypeRepr (CtxToLLVMType tys)
-> Assignment (RegEntry sym) (CtxToLLVMType tys)
-> IO (Assignment (RegEntry sym) tys)
regEntriesFromLLVM bak
bak FunctionName
fNm Assignment TypeRepr tys
wanteds Assignment TypeRepr (CtxToLLVMType tys)
tys)

---------------------------------------------------------------------
-- * Lowering overrides

-- | Lower an override to use the Crucible-LLVM ABI.
lowerLLVMOverride ::
  forall p sym ext args ret.
  HasLLVMAnn sym =>
  IC.LLVMOverride p sym ext args ret ->
  IC.LLVMOverride p sym ext (CtxToLLVMType args) (ToLLVMType ret)
lowerLLVMOverride :: forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
HasLLVMAnn sym =>
LLVMOverride p sym ext args ret
-> LLVMOverride p sym ext (CtxToLLVMType args) (ToLLVMType ret)
lowerLLVMOverride LLVMOverride p sym ext args ret
ov =
  IC.LLVMOverride
  { llvmOvDecl :: Declare (CtxToLLVMType args) (ToLLVMType ret)
IC.llvmOvDecl =
      Decl.Declare
      { decName :: Symbol
Decl.decName = LLVMOverride p sym ext args ret -> Symbol
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> Symbol
IC.llvmOvSymbol LLVMOverride p sym ext args ret
ov 
      , decArgs :: Assignment TypeRepr (CtxToLLVMType args)
Decl.decArgs = Assignment TypeRepr (CtxToLLVMType args)
argTys'
      , decRet :: TypeRepr (ToLLVMType ret)
Decl.decRet = TypeRepr (ToLLVMType ret)
retTy'
      }
  , llvmOvDefn :: IsSymInterface sym =>
GlobalVar Mem
-> Assignment (RegEntry sym) (CtxToLLVMType args)
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
   OverrideSim
     p sym ext rtp args' ret' (RegValue sym (ToLLVMType ret))
IC.llvmOvDefn =
    \GlobalVar Mem
mvar Assignment (RegEntry sym) (CtxToLLVMType args)
args ->
      (forall bak.
 IsSymBackend sym bak =>
 bak
 -> OverrideSim
      p sym ext rtp args' ret' (RegValue sym (ToLLVMType ret)))
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (ToLLVMType ret))
forall sym p ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
(forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym ext rtp args ret a)
-> OverrideSim p sym ext rtp args ret a
CSO.ovrWithBackend ((forall bak.
  IsSymBackend sym bak =>
  bak
  -> OverrideSim
       p sym ext rtp args' ret' (RegValue sym (ToLLVMType ret)))
 -> OverrideSim
      p sym ext rtp args' ret' (RegValue sym (ToLLVMType ret)))
-> (forall bak.
    IsSymBackend sym bak =>
    bak
    -> OverrideSim
         p sym ext rtp args' ret' (RegValue sym (ToLLVMType ret)))
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (ToLLVMType ret))
forall a b. (a -> b) -> a -> b
$ \bak
bak -> do
        let fNm :: FunctionName
fNm = LLVMOverride p sym ext args ret -> FunctionName
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> FunctionName
IC.llvmOvName LLVMOverride p sym ext args ret
ov
        Assignment (RegEntry sym) args
args' <- IO (Assignment (RegEntry sym) args)
-> OverrideSim
     p sym ext rtp args' ret' (Assignment (RegEntry sym) args)
forall a. IO a -> OverrideSim p sym ext rtp args' ret' a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (bak
-> FunctionName
-> Assignment TypeRepr args
-> Assignment TypeRepr (CtxToLLVMType args)
-> Assignment (RegEntry sym) (CtxToLLVMType args)
-> IO (Assignment (RegEntry sym) args)
forall sym bak (tys :: Ctx CrucibleType).
IsSymBackend sym bak =>
bak
-> FunctionName
-> Assignment TypeRepr tys
-> Assignment TypeRepr (CtxToLLVMType tys)
-> Assignment (RegEntry sym) (CtxToLLVMType tys)
-> IO (Assignment (RegEntry sym) tys)
regEntriesFromLLVM bak
bak FunctionName
fNm Assignment TypeRepr args
argTys Assignment TypeRepr (CtxToLLVMType args)
argTys' Assignment (RegEntry sym) (CtxToLLVMType args)
args)
        RegValue sym ret
ret <- LLVMOverride p sym ext args ret
-> IsSymInterface sym =>
   GlobalVar Mem
   -> Assignment (RegEntry sym) args
   -> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
      OverrideSim p sym ext rtp args' ret' (RegValue sym ret)
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret
-> IsSymInterface sym =>
   GlobalVar Mem
   -> Assignment (RegEntry sym) args
   -> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
      OverrideSim p sym ext rtp args' ret' (RegValue sym ret)
IC.llvmOvDefn LLVMOverride p sym ext args ret
ov GlobalVar Mem
mvar Assignment (RegEntry sym) args
args'
        IO (RegValue sym (ToLLVMType ret))
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (ToLLVMType ret))
forall a. IO a -> OverrideSim p sym ext rtp args' ret' a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (sym
-> TypeRepr ret
-> RegValue sym ret
-> IO (RegValue sym (ToLLVMType ret))
forall sym (ty :: CrucibleType).
IsSymInterface sym =>
sym
-> TypeRepr ty
-> RegValue sym ty
-> IO (RegValue sym (ToLLVMType ty))
regValueToLLVM (bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
CB.backendGetSym bak
bak) TypeRepr ret
retTy RegValue sym ret
ret)
  }
  where
    argTys :: Assignment TypeRepr args
argTys = LLVMOverride p sym ext args ret -> Assignment TypeRepr args
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> CtxRepr args
IC.llvmOvArgs LLVMOverride p sym ext args ret
ov
    argTys' :: Assignment TypeRepr (CtxToLLVMType args)
argTys' = Assignment TypeRepr args
-> Assignment TypeRepr (CtxToLLVMType args)
forall (ctx :: Ctx CrucibleType).
Assignment TypeRepr ctx -> Assignment TypeRepr (CtxToLLVMType ctx)
ctxToLLVMType Assignment TypeRepr args
argTys
    retTy :: TypeRepr ret
retTy = LLVMOverride p sym ext args ret -> TypeRepr ret
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> TypeRepr ret
IC.llvmOvRet LLVMOverride p sym ext args ret
ov
    retTy' :: TypeRepr (ToLLVMType ret)
retTy' = TypeRepr ret -> TypeRepr (ToLLVMType ret)
forall (t :: CrucibleType). TypeRepr t -> TypeRepr (ToLLVMType t)
toLLVMType TypeRepr ret
retTy

-- | Postcompose 'lowerLLVMOverride' with a 'IC.MakeOverride'
lowerMakeOverride ::
  HasLLVMAnn sym =>
  IC.MakeOverride p sym ext arch ->
  IC.MakeOverride p sym ext arch
lowerMakeOverride :: forall sym p ext (arch :: LLVMArch).
HasLLVMAnn sym =>
MakeOverride p sym ext arch -> MakeOverride p sym ext arch
lowerMakeOverride (IC.MakeOverride SomeDeclare
-> Maybe DecodedName
-> LLVMContext arch
-> Maybe (SomeLLVMOverride p sym ext)
f) =
  (SomeDeclare
 -> Maybe DecodedName
 -> LLVMContext arch
 -> Maybe (SomeLLVMOverride p sym ext))
-> MakeOverride p sym ext arch
forall p sym ext (arch :: LLVMArch).
(SomeDeclare
 -> Maybe DecodedName
 -> LLVMContext arch
 -> Maybe (SomeLLVMOverride p sym ext))
-> MakeOverride p sym ext arch
IC.MakeOverride ((SomeDeclare
  -> Maybe DecodedName
  -> LLVMContext arch
  -> Maybe (SomeLLVMOverride p sym ext))
 -> MakeOverride p sym ext arch)
-> (SomeDeclare
    -> Maybe DecodedName
    -> LLVMContext arch
    -> Maybe (SomeLLVMOverride p sym ext))
-> MakeOverride p sym ext arch
forall a b. (a -> b) -> a -> b
$ \SomeDeclare
decl Maybe DecodedName
nm LLVMContext arch
ctx -> do
    IC.SomeLLVMOverride LLVMOverride p sym ext args ret
ov <- SomeDeclare
-> Maybe DecodedName
-> LLVMContext arch
-> Maybe (SomeLLVMOverride p sym ext)
f SomeDeclare
decl Maybe DecodedName
nm LLVMContext arch
ctx
    SomeLLVMOverride p sym ext -> Maybe (SomeLLVMOverride p sym ext)
forall a. a -> Maybe a
Just (LLVMOverride p sym ext (CtxToLLVMType args) (ToLLVMType ret)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
IC.SomeLLVMOverride (LLVMOverride p sym ext args ret
-> LLVMOverride p sym ext (CtxToLLVMType args) (ToLLVMType ret)
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
HasLLVMAnn sym =>
LLVMOverride p sym ext args ret
-> LLVMOverride p sym ext (CtxToLLVMType args) (ToLLVMType ret)
lowerLLVMOverride LLVMOverride p sym ext args ret
ov))

-- | Call 'lowerLLVMOverride' on the override in a 'OverrideTemplate'
lowerOverrideTemplate ::
  HasLLVMAnn sym =>
  IC.OverrideTemplate p sym ext arch ->
  IC.OverrideTemplate p sym ext arch
lowerOverrideTemplate :: forall sym p ext (arch :: LLVMArch).
HasLLVMAnn sym =>
OverrideTemplate p sym ext arch -> OverrideTemplate p sym ext arch
lowerOverrideTemplate OverrideTemplate p sym ext arch
t =
  IC.OverrideTemplate
  { overrideTemplateMatcher :: TemplateMatcher
IC.overrideTemplateMatcher = OverrideTemplate p sym ext arch -> TemplateMatcher
forall p sym ext (arch :: LLVMArch).
OverrideTemplate p sym ext arch -> TemplateMatcher
IC.overrideTemplateMatcher OverrideTemplate p sym ext arch
t
  , overrideTemplateAction :: MakeOverride p sym ext arch
IC.overrideTemplateAction = MakeOverride p sym ext arch -> MakeOverride p sym ext arch
forall sym p ext (arch :: LLVMArch).
HasLLVMAnn sym =>
MakeOverride p sym ext arch -> MakeOverride p sym ext arch
lowerMakeOverride (OverrideTemplate p sym ext arch -> MakeOverride p sym ext arch
forall p sym ext (arch :: LLVMArch).
OverrideTemplate p sym ext arch -> MakeOverride p sym ext arch
IC.overrideTemplateAction OverrideTemplate p sym ext arch
t)
  }