-- |
-- Module           : Lang.Crucible.LLVM.Intrinsics.Common
-- Description      : Types used in override definitions
-- Copyright        : (c) Galois, Inc 2015-2019
-- License          : BSD3
-- Maintainer       : Rob Dockins <rdockins@galois.com>
-- Stability        : provisional
------------------------------------------------------------------------

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}

module Lang.Crucible.LLVM.Intrinsics.Common
  ( LLVMOverride(..)
  , SomeLLVMOverride(..)
  , RegOverrideM
  , llvmSizeT
  , llvmSSizeT
  , OverrideTemplate(..)
  , TemplateMatcher(..)
  , callStackFromMemVar'
    -- ** register_llvm_override
  , basic_llvm_override
  , polymorphic1_llvm_override

  , build_llvm_override
  , register_llvm_override
  , register_1arg_polymorphic_override
  , bind_llvm_handle
  , bind_llvm_func
  , do_register_llvm_override
  , alloc_and_register_override
  ) where

import qualified Text.LLVM.AST as L

import           Control.Applicative (empty)
import           Control.Monad (when)
import           Control.Monad.IO.Class (liftIO)
import           Control.Lens
import           Control.Monad.Reader (ReaderT, ask, lift)
import           Control.Monad.Trans.Maybe (MaybeT)
import qualified Data.List as List
import qualified Data.Text as Text
import           Numeric (readDec)

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

import           Lang.Crucible.Backend
import           Lang.Crucible.CFG.Common (GlobalVar)
import           Lang.Crucible.Simulator.ExecutionTree (FnState(UseOverride))
import           Lang.Crucible.FunctionHandle (FnHandle, mkHandle')
import           Lang.Crucible.Panic (panic)
import           Lang.Crucible.Simulator (stateContext, simHandleAllocator)
import           Lang.Crucible.Simulator.OverrideSim
import           Lang.Crucible.Utils.MonadVerbosity (getLogFunction)
import           Lang.Crucible.Simulator.RegMap
import           Lang.Crucible.Types

import           What4.FunctionName

import           Lang.Crucible.LLVM.Extension
import           Lang.Crucible.LLVM.Eval (callStackFromMemVar)
import           Lang.Crucible.LLVM.Globals (registerFunPtr)
import           Lang.Crucible.LLVM.MemModel
import           Lang.Crucible.LLVM.MemModel.CallStack (CallStack)
import           Lang.Crucible.LLVM.Translation.Monad
import           Lang.Crucible.LLVM.Translation.Types

-- | This type represents an implementation of an LLVM intrinsic function in
-- Crucible.
data LLVMOverride p sym args ret =
  LLVMOverride
  { forall p sym (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym args ret -> Declare
llvmOverride_declare :: L.Declare    -- ^ An LLVM name and signature for this intrinsic
  , forall p sym (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym args ret -> CtxRepr args
llvmOverride_args    :: CtxRepr args -- ^ A representation of the argument types
  , forall p sym (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym args ret -> TypeRepr ret
llvmOverride_ret     :: TypeRepr ret -- ^ A representation of the return type
  , forall p sym (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym args ret
-> forall bak.
   IsSymBackend sym bak =>
   GlobalVar Mem
   -> bak
   -> Assignment (RegEntry sym) args
   -> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
      OverrideSim p sym LLVM rtp args' ret' (RegValue sym ret)
llvmOverride_def ::
       forall bak.
         IsSymBackend sym bak =>
         GlobalVar Mem ->
         bak ->
         Ctx.Assignment (RegEntry sym) args ->
         forall rtp args' ret'.
         OverrideSim p sym LLVM rtp args' ret' (RegValue sym ret)
    -- ^ The implementation of the intrinsic in the simulator monad
    -- (@OverrideSim@).
  }

data SomeLLVMOverride p sym =
  forall args ret. SomeLLVMOverride (LLVMOverride p sym args ret)

-- | Convenient LLVM representation of the @size_t@ type.
llvmSizeT :: HasPtrWidth wptr => L.Type
llvmSizeT :: forall (wptr :: Natural). HasPtrWidth wptr => Type
llvmSizeT = PrimType -> Type
forall ident. PrimType -> Type' ident
L.PrimType (PrimType -> Type) -> PrimType -> Type
forall a b. (a -> b) -> a -> b
$ Word32 -> PrimType
L.Integer (Word32 -> PrimType) -> Word32 -> PrimType
forall a b. (a -> b) -> a -> b
$ Natural -> Word32
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Word32) -> Natural -> Word32
forall a b. (a -> b) -> a -> b
$ NatRepr wptr -> Natural
forall (n :: Natural). NatRepr n -> Natural
natValue (NatRepr wptr -> Natural) -> NatRepr wptr -> Natural
forall a b. (a -> b) -> a -> b
$ NatRepr wptr
forall (w :: Natural) (w' :: Natural).
(HasPtrWidth w, w ~ w') =>
NatRepr w'
PtrWidth

-- | Convenient LLVM representation of the @ssize_t@ type.
llvmSSizeT :: HasPtrWidth wptr => L.Type
llvmSSizeT :: forall (wptr :: Natural). HasPtrWidth wptr => Type
llvmSSizeT = PrimType -> Type
forall ident. PrimType -> Type' ident
L.PrimType (PrimType -> Type) -> PrimType -> Type
forall a b. (a -> b) -> a -> b
$ Word32 -> PrimType
L.Integer (Word32 -> PrimType) -> Word32 -> PrimType
forall a b. (a -> b) -> a -> b
$ Natural -> Word32
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Word32) -> Natural -> Word32
forall a b. (a -> b) -> a -> b
$ NatRepr wptr -> Natural
forall (n :: Natural). NatRepr n -> Natural
natValue (NatRepr wptr -> Natural) -> NatRepr wptr -> Natural
forall a b. (a -> b) -> a -> b
$ NatRepr wptr
forall (w :: Natural) (w' :: Natural).
(HasPtrWidth w, w ~ w') =>
NatRepr w'
PtrWidth

data OverrideTemplate p sym arch rtp l a =
  OverrideTemplate
  { forall p sym (arch :: LLVMArch) rtp (l :: Ctx CrucibleType)
       (a :: CrucibleType).
OverrideTemplate p sym arch rtp l a -> TemplateMatcher
overrideTemplateMatcher :: TemplateMatcher
  , forall p sym (arch :: LLVMArch) rtp (l :: Ctx CrucibleType)
       (a :: CrucibleType).
OverrideTemplate p sym arch rtp l a
-> RegOverrideM p sym arch rtp l a ()
overrideTemplateAction :: RegOverrideM p sym arch rtp l a ()
  }

-- | This type controls whether an override is installed for a given name found in a module.
--  See 'filterTemplates'.
data TemplateMatcher
  = ExactMatch String
  | PrefixMatch String
  | SubstringsMatch [String]

type RegOverrideM p sym arch rtp l a =
  ReaderT (L.Declare, Maybe ABI.DecodedName, LLVMContext arch)
    (MaybeT (OverrideSim p sym LLVM rtp l a))

callStackFromMemVar' ::
  GlobalVar Mem ->
  OverrideSim p sym ext r args ret CallStack
callStackFromMemVar' :: forall p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
GlobalVar Mem -> OverrideSim p sym ext r args ret CallStack
callStackFromMemVar' GlobalVar Mem
mvar = Getting
  CallStack
  (SimState p sym ext r (OverrideLang ret) ('Just args))
  CallStack
-> OverrideSim p sym ext r args ret CallStack
forall s (m :: Type -> Type) a.
MonadState s m =>
Getting a s a -> m a
use ((SimState p sym ext r (OverrideLang ret) ('Just args) -> CallStack)
-> Getting
     CallStack
     (SimState p sym ext r (OverrideLang ret) ('Just args))
     CallStack
forall (p :: Type -> Type -> Type) (f :: Type -> Type) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to ((SimState p sym ext r (OverrideLang ret) ('Just args)
 -> GlobalVar Mem -> CallStack)
-> GlobalVar Mem
-> SimState p sym ext r (OverrideLang ret) ('Just args)
-> CallStack
forall a b c. (a -> b -> c) -> b -> a -> c
flip SimState p sym ext r (OverrideLang ret) ('Just args)
-> GlobalVar Mem -> CallStack
forall p sym ext rtp lang (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext rtp lang args -> GlobalVar Mem -> CallStack
callStackFromMemVar GlobalVar Mem
mvar))

------------------------------------------------------------------------
-- ** register_llvm_override

newtype ArgTransformer p sym args args' =
  ArgTransformer { forall p sym (args :: Ctx CrucibleType)
       (args' :: Ctx CrucibleType).
ArgTransformer p sym args args'
-> forall rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
   Assignment (RegEntry sym) args
   -> OverrideSim p sym LLVM rtp l a (Assignment (RegEntry sym) args')
applyArgTransformer :: (forall rtp l a.
    Ctx.Assignment (RegEntry sym) args ->
    OverrideSim p sym LLVM rtp l a (Ctx.Assignment (RegEntry sym) args')) }

newtype ValTransformer p sym tp tp' =
  ValTransformer { forall p sym (tp :: CrucibleType) (tp' :: CrucibleType).
ValTransformer p sym tp tp'
-> forall rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
   RegValue sym tp
   -> OverrideSim p sym LLVM rtp l a (RegValue sym tp')
applyValTransformer :: (forall rtp l a.
    RegValue sym tp ->
    OverrideSim p sym LLVM rtp l a (RegValue sym tp')) }

transformLLVMArgs :: forall m p sym bak args args'.
  (IsSymBackend sym bak, Monad m, HasLLVMAnn sym) =>
  -- | This function name is only used in panic messages.
  FunctionName ->
  bak ->
  CtxRepr args' ->
  CtxRepr args ->
  m (ArgTransformer p sym args args')
transformLLVMArgs :: forall (m :: Type -> Type) p sym bak (args :: Ctx CrucibleType)
       (args' :: Ctx CrucibleType).
(IsSymBackend sym bak, Monad m, HasLLVMAnn sym) =>
FunctionName
-> bak
-> CtxRepr args'
-> CtxRepr args
-> m (ArgTransformer p sym args args')
transformLLVMArgs FunctionName
_fnName bak
_ Assignment TypeRepr args'
Ctx.Empty Assignment TypeRepr args
Ctx.Empty =
  ArgTransformer p sym args args'
-> m (ArgTransformer p sym args args')
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ((forall rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
 Assignment (RegEntry sym) args
 -> OverrideSim
      p sym LLVM rtp l a (Assignment (RegEntry sym) args'))
-> ArgTransformer p sym args args'
forall p sym (args :: Ctx CrucibleType)
       (args' :: Ctx CrucibleType).
(forall rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
 Assignment (RegEntry sym) args
 -> OverrideSim
      p sym LLVM rtp l a (Assignment (RegEntry sym) args'))
-> ArgTransformer p sym args args'
ArgTransformer (\Assignment (RegEntry sym) args
_ -> Assignment (RegEntry sym) args'
-> OverrideSim p sym LLVM rtp l a (Assignment (RegEntry sym) args')
forall a. a -> OverrideSim p sym LLVM 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))
transformLLVMArgs FunctionName
fnName bak
bak (Assignment TypeRepr ctx
rest' Ctx.:> TypeRepr tp
tp') (Assignment TypeRepr ctx
rest Ctx.:> TypeRepr tp
tp) = do
  ArgTransformer p sym args args'
-> m (ArgTransformer p sym args args')
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ((forall rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
 Assignment (RegEntry sym) args
 -> OverrideSim
      p sym LLVM rtp l a (Assignment (RegEntry sym) args'))
-> ArgTransformer p sym args args'
forall p sym (args :: Ctx CrucibleType)
       (args' :: Ctx CrucibleType).
(forall rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
 Assignment (RegEntry sym) args
 -> OverrideSim
      p sym LLVM rtp l a (Assignment (RegEntry sym) args'))
-> ArgTransformer p sym args args'
ArgTransformer
           (\(Assignment (RegEntry sym) ctx
xs Ctx.:> RegEntry sym tp
x) ->
              do (ValTransformer forall rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
RegValue sym tp -> OverrideSim p sym LLVM rtp l a (RegValue sym tp)
f)  <- FunctionName
-> bak
-> TypeRepr tp
-> TypeRepr tp
-> OverrideSim p sym LLVM rtp l a (ValTransformer p sym tp tp)
forall sym bak (m :: Type -> Type) (ret :: CrucibleType)
       (ret' :: CrucibleType) p.
(IsSymBackend sym bak, Monad m, HasLLVMAnn sym) =>
FunctionName
-> bak
-> TypeRepr ret
-> TypeRepr ret'
-> m (ValTransformer p sym ret ret')
transformLLVMRet FunctionName
fnName bak
bak TypeRepr tp
tp TypeRepr tp
tp'
                 (ArgTransformer forall rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
Assignment (RegEntry sym) ctx
-> OverrideSim p sym LLVM rtp l a (Assignment (RegEntry sym) ctx)
fs) <- FunctionName
-> bak
-> Assignment TypeRepr ctx
-> Assignment TypeRepr ctx
-> OverrideSim p sym LLVM rtp l a (ArgTransformer p sym ctx ctx)
forall (m :: Type -> Type) p sym bak (args :: Ctx CrucibleType)
       (args' :: Ctx CrucibleType).
(IsSymBackend sym bak, Monad m, HasLLVMAnn sym) =>
FunctionName
-> bak
-> CtxRepr args'
-> CtxRepr args
-> m (ArgTransformer p sym args args')
transformLLVMArgs FunctionName
fnName bak
bak Assignment TypeRepr ctx
rest' Assignment TypeRepr ctx
rest
                 Assignment (RegEntry sym) ctx
xs' <- Assignment (RegEntry sym) ctx
-> OverrideSim p sym LLVM rtp l a (Assignment (RegEntry sym) ctx)
forall rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
Assignment (RegEntry sym) ctx
-> OverrideSim p sym LLVM rtp l a (Assignment (RegEntry sym) ctx)
fs Assignment (RegEntry sym) ctx
Assignment (RegEntry sym) ctx
xs
                 RegEntry sym tp
x'  <- 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 -> RegEntry sym tp)
-> OverrideSim p sym LLVM rtp l a (RegValue sym tp)
-> OverrideSim p sym LLVM rtp l a (RegEntry sym tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> RegValue sym tp -> OverrideSim p sym LLVM rtp l a (RegValue sym tp)
forall rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
RegValue sym tp -> OverrideSim p sym LLVM 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 LLVM rtp l a (Assignment (RegEntry sym) args')
forall a. a -> OverrideSim p sym LLVM 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.:> RegEntry sym tp
x')))
transformLLVMArgs FunctionName
fnName bak
_ Assignment TypeRepr args'
_ Assignment TypeRepr args
_ =
  String -> [String] -> m (ArgTransformer p sym args args')
forall a. HasCallStack => String -> [String] -> a
panic String
"Intrinsics.transformLLVMArgs"
    [ String
"transformLLVMArgs: argument shape mismatch!"
    , String
"in function: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Text -> String
Text.unpack (FunctionName -> Text
functionName FunctionName
fnName)
    ]

transformLLVMRet ::
  (IsSymBackend sym bak, Monad m, HasLLVMAnn sym) =>
  -- | This function name is only used in panic messages.
  FunctionName ->
  bak ->
  TypeRepr ret  ->
  TypeRepr ret' ->
  m (ValTransformer p sym ret ret')
transformLLVMRet :: forall sym bak (m :: Type -> Type) (ret :: CrucibleType)
       (ret' :: CrucibleType) p.
(IsSymBackend sym bak, Monad m, HasLLVMAnn sym) =>
FunctionName
-> bak
-> TypeRepr ret
-> TypeRepr ret'
-> m (ValTransformer p sym ret ret')
transformLLVMRet FunctionName
_fnName 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'
  = ValTransformer p sym ret ret' -> m (ValTransformer p sym ret ret')
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ((forall rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
 RegValue sym ret
 -> OverrideSim p sym LLVM rtp l a (RegValue sym ret'))
-> ValTransformer p sym ret ret'
forall p sym (tp :: CrucibleType) (tp' :: CrucibleType).
(forall rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
 RegValue sym tp
 -> OverrideSim p sym LLVM rtp l a (RegValue sym tp'))
-> ValTransformer p sym tp tp'
ValTransformer (IO (LLVMPointer sym n)
-> OverrideSim p sym LLVM rtp l a (LLVMPointer sym n)
forall a. IO a -> OverrideSim p sym LLVM rtp l a a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (LLVMPointer sym n)
 -> OverrideSim p sym LLVM rtp l a (LLVMPointer sym n))
-> (SymExpr sym (BaseBVType n) -> IO (LLVMPointer sym n))
-> SymExpr sym (BaseBVType n)
-> OverrideSim p sym LLVM 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)))
transformLLVMRet FunctionName
_fnName 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'
  = ValTransformer p sym ret ret' -> m (ValTransformer p sym ret ret')
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ((forall rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
 RegValue sym ret
 -> OverrideSim p sym LLVM rtp l a (RegValue sym ret'))
-> ValTransformer p sym ret ret'
forall p sym (tp :: CrucibleType) (tp' :: CrucibleType).
(forall rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
 RegValue sym tp
 -> OverrideSim p sym LLVM rtp l a (RegValue sym tp'))
-> ValTransformer p sym tp tp'
ValTransformer (IO (SymExpr sym ('BaseBVType w))
-> OverrideSim p sym LLVM rtp l a (SymExpr sym ('BaseBVType w))
forall a. IO a -> OverrideSim p sym LLVM rtp l a a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym ('BaseBVType w))
 -> OverrideSim p sym LLVM rtp l a (SymExpr sym ('BaseBVType w)))
-> (LLVMPointer sym w -> IO (SymExpr sym ('BaseBVType w)))
-> LLVMPointer sym w
-> OverrideSim p sym LLVM rtp l a (SymExpr sym ('BaseBVType w))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. bak -> LLVMPtr sym w -> IO (SymExpr sym ('BaseBVType w))
forall sym bak (w :: Natural).
IsSymBackend sym bak =>
bak -> LLVMPtr sym w -> IO (SymBV sym w)
projectLLVM_bv bak
bak))
transformLLVMRet FunctionName
fnName bak
bak (VectorRepr TypeRepr tp1
tp) (VectorRepr TypeRepr tp1
tp')
  = do ValTransformer forall rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
RegValue sym tp1
-> OverrideSim p sym LLVM rtp l a (RegValue sym tp1)
f <- FunctionName
-> bak
-> TypeRepr tp1
-> TypeRepr tp1
-> m (ValTransformer p sym tp1 tp1)
forall sym bak (m :: Type -> Type) (ret :: CrucibleType)
       (ret' :: CrucibleType) p.
(IsSymBackend sym bak, Monad m, HasLLVMAnn sym) =>
FunctionName
-> bak
-> TypeRepr ret
-> TypeRepr ret'
-> m (ValTransformer p sym ret ret')
transformLLVMRet FunctionName
fnName bak
bak TypeRepr tp1
tp TypeRepr tp1
tp'
       ValTransformer p sym ret ret' -> m (ValTransformer p sym ret ret')
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ((forall rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
 RegValue sym ret
 -> OverrideSim p sym LLVM rtp l a (RegValue sym ret'))
-> ValTransformer p sym ret ret'
forall p sym (tp :: CrucibleType) (tp' :: CrucibleType).
(forall rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
 RegValue sym tp
 -> OverrideSim p sym LLVM rtp l a (RegValue sym tp'))
-> ValTransformer p sym tp tp'
ValTransformer ((RegValue sym tp1
 -> OverrideSim p sym LLVM rtp l a (RegValue sym tp1))
-> Vector (RegValue sym tp1)
-> OverrideSim p sym LLVM 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 LLVM rtp l a (RegValue sym tp1)
forall rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
RegValue sym tp1
-> OverrideSim p sym LLVM rtp l a (RegValue sym tp1)
f))
transformLLVMRet FunctionName
fnName bak
bak (StructRepr CtxRepr ctx
ctx) (StructRepr CtxRepr ctx
ctx')
  = do ArgTransformer forall rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
Assignment (RegEntry sym) ctx
-> OverrideSim p sym LLVM rtp l a (Assignment (RegEntry sym) ctx)
tf <- FunctionName
-> bak
-> CtxRepr ctx
-> CtxRepr ctx
-> m (ArgTransformer p sym ctx ctx)
forall (m :: Type -> Type) p sym bak (args :: Ctx CrucibleType)
       (args' :: Ctx CrucibleType).
(IsSymBackend sym bak, Monad m, HasLLVMAnn sym) =>
FunctionName
-> bak
-> CtxRepr args'
-> CtxRepr args
-> m (ArgTransformer p sym args args')
transformLLVMArgs FunctionName
fnName bak
bak CtxRepr ctx
ctx' CtxRepr ctx
ctx
       ValTransformer p sym ret ret' -> m (ValTransformer p sym ret ret')
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ((forall rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
 RegValue sym ret
 -> OverrideSim p sym LLVM rtp l a (RegValue sym ret'))
-> ValTransformer p sym ret ret'
forall p sym (tp :: CrucibleType) (tp' :: CrucibleType).
(forall rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
 RegValue sym tp
 -> OverrideSim p sym LLVM rtp l a (RegValue sym tp'))
-> ValTransformer p sym tp tp'
ValTransformer (\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 LLVM rtp l a (Assignment (RegEntry sym) ctx)
-> OverrideSim p sym LLVM 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 LLVM rtp l a (Assignment (RegEntry sym) ctx)
forall rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
Assignment (RegEntry sym) ctx
-> OverrideSim p sym LLVM rtp l a (Assignment (RegEntry sym) ctx)
tf Assignment (RegEntry sym) ctx
vals'))

transformLLVMRet FunctionName
_fnName 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'
  = ValTransformer p sym ret ret' -> m (ValTransformer p sym ret ret')
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ((forall rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
 RegValue sym ret
 -> OverrideSim p sym LLVM rtp l a (RegValue sym ret'))
-> ValTransformer p sym ret ret'
forall p sym (tp :: CrucibleType) (tp' :: CrucibleType).
(forall rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
 RegValue sym tp
 -> OverrideSim p sym LLVM rtp l a (RegValue sym tp'))
-> ValTransformer p sym tp tp'
ValTransformer RegValue sym ret
-> OverrideSim p sym LLVM rtp l a (RegValue sym ret)
RegValue sym ret
-> OverrideSim p sym LLVM rtp l a (RegValue sym ret')
forall a. a -> OverrideSim p sym LLVM rtp l a a
forall rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
RegValue sym ret
-> OverrideSim p sym LLVM rtp l a (RegValue sym ret')
forall (m :: Type -> Type) a. Monad m => a -> m a
return)
transformLLVMRet FunctionName
fnName bak
_bak TypeRepr ret
ret TypeRepr ret'
ret'
  = String -> [String] -> m (ValTransformer p sym ret ret')
forall a. HasCallStack => String -> [String] -> a
panic String
"Intrinsics.transformLLVMRet"
      [ String
"Cannot transform types"
      , String
"*** Source type: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ TypeRepr ret -> String
forall a. Show a => a -> String
show TypeRepr ret
ret
      , String
"*** Target type: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ TypeRepr ret' -> String
forall a. Show a => a -> String
show TypeRepr ret'
ret'
      , String
"in function: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Text -> String
Text.unpack (FunctionName -> Text
functionName FunctionName
fnName)
      ]

-- | Do some pipe-fitting to match a Crucible override function into the shape
--   expected by the LLVM calling convention.  This basically just coerces
--   between values of @BVType w@ and values of @LLVMPointerType w@.
build_llvm_override ::
  HasLLVMAnn sym =>
  FunctionName ->
  CtxRepr args ->
  TypeRepr ret ->
  CtxRepr args' ->
  TypeRepr ret' ->
  (forall bak rtp' l' a'. IsSymBackend sym bak =>
   bak ->
   Ctx.Assignment (RegEntry sym) args ->
   OverrideSim p sym LLVM rtp' l' a' (RegValue sym ret)) ->
  OverrideSim p sym LLVM rtp l a (Override p sym LLVM args' ret')
build_llvm_override :: forall sym (args :: Ctx CrucibleType) (ret :: CrucibleType)
       (args' :: Ctx CrucibleType) (ret' :: CrucibleType) p rtp
       (l :: Ctx CrucibleType) (a :: CrucibleType).
HasLLVMAnn sym =>
FunctionName
-> CtxRepr args
-> TypeRepr ret
-> CtxRepr args'
-> TypeRepr ret'
-> (forall bak rtp' (l' :: Ctx CrucibleType) (a' :: CrucibleType).
    IsSymBackend sym bak =>
    bak
    -> Assignment (RegEntry sym) args
    -> OverrideSim p sym LLVM rtp' l' a' (RegValue sym ret))
-> OverrideSim p sym LLVM rtp l a (Override p sym LLVM args' ret')
build_llvm_override FunctionName
fnm CtxRepr args
args TypeRepr ret
ret CtxRepr args'
args' TypeRepr ret'
ret' forall bak rtp' (l' :: Ctx CrucibleType) (a' :: CrucibleType).
IsSymBackend sym bak =>
bak
-> Assignment (RegEntry sym) args
-> OverrideSim p sym LLVM rtp' l' a' (RegValue sym ret)
llvmOverride =
  (forall bak.
 IsSymBackend sym bak =>
 bak
 -> OverrideSim p sym LLVM rtp l a (Override p sym LLVM args' ret'))
-> OverrideSim p sym LLVM rtp l a (Override p sym LLVM args' 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
ovrWithBackend ((forall bak.
  IsSymBackend sym bak =>
  bak
  -> OverrideSim p sym LLVM rtp l a (Override p sym LLVM args' ret'))
 -> OverrideSim p sym LLVM rtp l a (Override p sym LLVM args' ret'))
-> (forall bak.
    IsSymBackend sym bak =>
    bak
    -> OverrideSim p sym LLVM rtp l a (Override p sym LLVM args' ret'))
-> OverrideSim p sym LLVM rtp l a (Override p sym LLVM args' ret')
forall a b. (a -> b) -> a -> b
$ \bak
bak ->
  do ArgTransformer p sym args' args
fargs <- FunctionName
-> bak
-> CtxRepr args
-> CtxRepr args'
-> OverrideSim p sym LLVM rtp l a (ArgTransformer p sym args' args)
forall (m :: Type -> Type) p sym bak (args :: Ctx CrucibleType)
       (args' :: Ctx CrucibleType).
(IsSymBackend sym bak, Monad m, HasLLVMAnn sym) =>
FunctionName
-> bak
-> CtxRepr args'
-> CtxRepr args
-> m (ArgTransformer p sym args args')
transformLLVMArgs FunctionName
fnm bak
bak CtxRepr args
args CtxRepr args'
args'
     ValTransformer p sym ret ret'
fret  <- FunctionName
-> bak
-> TypeRepr ret
-> TypeRepr ret'
-> OverrideSim p sym LLVM rtp l a (ValTransformer p sym ret ret')
forall sym bak (m :: Type -> Type) (ret :: CrucibleType)
       (ret' :: CrucibleType) p.
(IsSymBackend sym bak, Monad m, HasLLVMAnn sym) =>
FunctionName
-> bak
-> TypeRepr ret
-> TypeRepr ret'
-> m (ValTransformer p sym ret ret')
transformLLVMRet FunctionName
fnm bak
bak TypeRepr ret
ret  TypeRepr ret'
ret'
     Override p sym LLVM args' ret'
-> OverrideSim p sym LLVM rtp l a (Override p sym LLVM args' ret')
forall a. a -> OverrideSim p sym LLVM rtp l a a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Override p sym LLVM args' ret'
 -> OverrideSim p sym LLVM rtp l a (Override p sym LLVM args' ret'))
-> Override p sym LLVM args' ret'
-> OverrideSim p sym LLVM rtp l a (Override p sym LLVM args' ret')
forall a b. (a -> b) -> a -> b
$ FunctionName
-> TypeRepr ret'
-> (forall {r}.
    OverrideSim p sym LLVM r args' ret' (RegValue sym ret'))
-> Override p sym LLVM args' ret'
forall (ret :: CrucibleType) p sym ext (args :: Ctx CrucibleType).
FunctionName
-> TypeRepr ret
-> (forall r. OverrideSim p sym ext r args ret (RegValue sym ret))
-> Override p sym ext args ret
mkOverride' FunctionName
fnm TypeRepr ret'
ret' ((forall {r}.
  OverrideSim p sym LLVM r args' ret' (RegValue sym ret'))
 -> Override p sym LLVM args' ret')
-> (forall {r}.
    OverrideSim p sym LLVM r args' ret' (RegValue sym ret'))
-> Override p sym LLVM args' ret'
forall a b. (a -> b) -> a -> b
$
            do RegMap Assignment (RegEntry sym) args'
xs <- OverrideSim p sym LLVM r args' ret' (RegMap sym args')
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
OverrideSim p sym ext rtp args ret (RegMap sym args)
getOverrideArgs
               (forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym LLVM r args' ret' (RegValue sym ret'))
-> OverrideSim p sym LLVM r args' ret' (RegValue sym 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
ovrWithBackend ((forall bak.
  IsSymBackend sym bak =>
  bak -> OverrideSim p sym LLVM r args' ret' (RegValue sym ret'))
 -> OverrideSim p sym LLVM r args' ret' (RegValue sym ret'))
-> (forall bak.
    IsSymBackend sym bak =>
    bak -> OverrideSim p sym LLVM r args' ret' (RegValue sym ret'))
-> OverrideSim p sym LLVM r args' ret' (RegValue sym ret')
forall a b. (a -> b) -> a -> b
$ \bak
bak' ->
                 ValTransformer p sym ret ret'
-> forall rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
   RegValue sym ret
   -> OverrideSim p sym LLVM rtp l a (RegValue sym ret')
forall p sym (tp :: CrucibleType) (tp' :: CrucibleType).
ValTransformer p sym tp tp'
-> forall rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
   RegValue sym tp
   -> OverrideSim p sym LLVM rtp l a (RegValue sym tp')
applyValTransformer ValTransformer p sym ret ret'
fret (RegValue sym ret
 -> OverrideSim p sym LLVM r args' ret' (RegValue sym ret'))
-> OverrideSim p sym LLVM r args' ret' (RegValue sym ret)
-> OverrideSim p sym LLVM r args' ret' (RegValue sym ret')
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< bak
-> Assignment (RegEntry sym) args
-> OverrideSim p sym LLVM r args' ret' (RegValue sym ret)
forall bak rtp' (l' :: Ctx CrucibleType) (a' :: CrucibleType).
IsSymBackend sym bak =>
bak
-> Assignment (RegEntry sym) args
-> OverrideSim p sym LLVM rtp' l' a' (RegValue sym ret)
llvmOverride bak
bak' (Assignment (RegEntry sym) args
 -> OverrideSim p sym LLVM r args' ret' (RegValue sym ret))
-> OverrideSim
     p sym LLVM r args' ret' (Assignment (RegEntry sym) args)
-> OverrideSim p sym LLVM r args' ret' (RegValue sym ret)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< ArgTransformer p sym args' args
-> forall rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
   Assignment (RegEntry sym) args'
   -> OverrideSim p sym LLVM rtp l a (Assignment (RegEntry sym) args)
forall p sym (args :: Ctx CrucibleType)
       (args' :: Ctx CrucibleType).
ArgTransformer p sym args args'
-> forall rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
   Assignment (RegEntry sym) args
   -> OverrideSim p sym LLVM rtp l a (Assignment (RegEntry sym) args')
applyArgTransformer ArgTransformer p sym args' args
fargs Assignment (RegEntry sym) args'
xs

polymorphic1_llvm_override :: forall p sym arch wptr l a rtp.
  (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
  String ->
  (forall w. (1 <= w) => NatRepr w -> SomeLLVMOverride p sym) ->
  OverrideTemplate p sym arch rtp l a
polymorphic1_llvm_override :: forall p sym (arch :: LLVMArch) (wptr :: Natural)
       (l :: Ctx CrucibleType) (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
String
-> (forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> SomeLLVMOverride p sym)
-> OverrideTemplate p sym arch rtp l a
polymorphic1_llvm_override String
prefix forall (w :: Natural).
(1 <= w) =>
NatRepr w -> SomeLLVMOverride p sym
fn =
  TemplateMatcher
-> RegOverrideM p sym arch rtp l a ()
-> OverrideTemplate p sym arch rtp l a
forall p sym (arch :: LLVMArch) rtp (l :: Ctx CrucibleType)
       (a :: CrucibleType).
TemplateMatcher
-> RegOverrideM p sym arch rtp l a ()
-> OverrideTemplate p sym arch rtp l a
OverrideTemplate (String -> TemplateMatcher
PrefixMatch String
prefix) (String
-> (forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> SomeLLVMOverride p sym)
-> RegOverrideM p sym arch rtp l a ()
forall p sym (arch :: LLVMArch) (wptr :: Natural)
       (l :: Ctx CrucibleType) (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
String
-> (forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> SomeLLVMOverride p sym)
-> RegOverrideM p sym arch rtp l a ()
register_1arg_polymorphic_override String
prefix NatRepr w -> SomeLLVMOverride p sym
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> SomeLLVMOverride p sym
fn)

register_1arg_polymorphic_override :: forall p sym arch wptr l a rtp.
  (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
  String ->
  (forall w. (1 <= w) => NatRepr w -> SomeLLVMOverride p sym) ->
  RegOverrideM p sym arch rtp l a ()
register_1arg_polymorphic_override :: forall p sym (arch :: LLVMArch) (wptr :: Natural)
       (l :: Ctx CrucibleType) (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
String
-> (forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> SomeLLVMOverride p sym)
-> RegOverrideM p sym arch rtp l a ()
register_1arg_polymorphic_override String
prefix forall (w :: Natural).
(1 <= w) =>
NatRepr w -> SomeLLVMOverride p sym
overrideFn =
  do (L.Declare{ decName :: Declare -> Symbol
L.decName = L.Symbol String
nm },Maybe DecodedName
_,LLVMContext arch
_) <- ReaderT
  (Declare, Maybe DecodedName, LLVMContext arch)
  (MaybeT (OverrideSim p sym LLVM rtp l a))
  (Declare, Maybe DecodedName, LLVMContext arch)
forall r (m :: Type -> Type). MonadReader r m => m r
ask
     case String -> String -> Maybe String
forall a. Eq a => [a] -> [a] -> Maybe [a]
List.stripPrefix String
prefix String
nm of
       Just (Char
'.':Char
'i': (ReadS Natural
forall a. (Eq a, Num a) => ReadS a
readDec -> (Natural
sz,[]):[(Natural, String)]
_))
         | Some NatRepr x
w <- Natural -> Some NatRepr
mkNatRepr Natural
sz
         , Just LeqProof 1 x
LeqProof <- NatRepr x -> Maybe (LeqProof 1 x)
forall (n :: Natural). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr x
w
         -> case NatRepr x -> SomeLLVMOverride p sym
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> SomeLLVMOverride p sym
overrideFn NatRepr x
w of SomeLLVMOverride LLVMOverride p sym args ret
ovr -> LLVMOverride p sym args ret -> RegOverrideM p sym arch rtp l a ()
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym) =>
LLVMOverride p sym args ret -> RegOverrideM p sym arch rtp l a ()
register_llvm_override LLVMOverride p sym args ret
ovr
       Maybe String
_ -> RegOverrideM p sym arch rtp l a ()
forall a.
ReaderT
  (Declare, Maybe DecodedName, LLVMContext arch)
  (MaybeT (OverrideSim p sym LLVM rtp l a))
  a
forall (f :: Type -> Type) a. Alternative f => f a
empty

basic_llvm_override :: forall p args ret sym arch wptr l a rtp.
  (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
  LLVMOverride p sym args ret ->
  OverrideTemplate p sym arch rtp l a
basic_llvm_override :: forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym args ret -> OverrideTemplate p sym arch rtp l a
basic_llvm_override LLVMOverride p sym args ret
ovr = TemplateMatcher
-> RegOverrideM p sym arch rtp l a ()
-> OverrideTemplate p sym arch rtp l a
forall p sym (arch :: LLVMArch) rtp (l :: Ctx CrucibleType)
       (a :: CrucibleType).
TemplateMatcher
-> RegOverrideM p sym arch rtp l a ()
-> OverrideTemplate p sym arch rtp l a
OverrideTemplate (String -> TemplateMatcher
ExactMatch String
nm) (LLVMOverride p sym args ret -> RegOverrideM p sym arch rtp l a ()
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym) =>
LLVMOverride p sym args ret -> RegOverrideM p sym arch rtp l a ()
register_llvm_override LLVMOverride p sym args ret
ovr)
 where L.Symbol String
nm = Declare -> Symbol
L.decName (LLVMOverride p sym args ret -> Declare
forall p sym (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym args ret -> Declare
llvmOverride_declare LLVMOverride p sym args ret
ovr)


-- | Check that the requested declaration matches the provided declaration. In
-- this context, \"matching\" means that both declarations have identical names,
-- as well as equal argument and result types. When checking types for equality,
-- we consider opaque pointer types to be equal to non-opaque pointer types so
-- that we do not have to define quite so many overrides with different
-- combinations of pointer types.
isMatchingDeclaration ::
  L.Declare {- ^ Requested declaration -} ->
  L.Declare {- ^ Provided declaration for intrinsic -} ->
  Bool
isMatchingDeclaration :: Declare -> Declare -> Bool
isMatchingDeclaration Declare
requested Declare
provided = [Bool] -> Bool
forall (t :: Type -> Type). Foldable t => t Bool -> Bool
and
  [ Declare -> Symbol
L.decName Declare
requested Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Declare -> Symbol
L.decName Declare
provided
  , [Type] -> [Type] -> Bool
matchingArgList (Declare -> [Type]
L.decArgs Declare
requested) (Declare -> [Type]
L.decArgs Declare
provided)
  , Declare -> Type
L.decRetType Declare
requested Type -> Type -> Bool
forall ident. Eq ident => Type' ident -> Type' ident -> Bool
`L.eqTypeModuloOpaquePtrs` Declare -> Type
L.decRetType Declare
provided
  -- TODO? do we need to pay attention to various attributes?
  ]

 where
 matchingArgList :: [Type] -> [Type] -> Bool
matchingArgList [] [] = Bool
True
 matchingArgList [] [Type]
_  = Declare -> Bool
L.decVarArgs Declare
requested
 matchingArgList [Type]
_  [] = Declare -> Bool
L.decVarArgs Declare
provided
 matchingArgList (Type
x:[Type]
xs) (Type
y:[Type]
ys) = Type
x Type -> Type -> Bool
forall ident. Eq ident => Type' ident -> Type' ident -> Bool
`L.eqTypeModuloOpaquePtrs` Type
y Bool -> Bool -> Bool
&& [Type] -> [Type] -> Bool
matchingArgList [Type]
xs [Type]
ys

register_llvm_override :: forall p args ret sym arch wptr l a rtp.
  (IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym) =>
  LLVMOverride p sym args ret ->
  RegOverrideM p sym arch rtp l a ()
register_llvm_override :: forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym) =>
LLVMOverride p sym args ret -> RegOverrideM p sym arch rtp l a ()
register_llvm_override LLVMOverride p sym args ret
llvmOverride = do
  (Declare
requestedDecl,Maybe DecodedName
_,LLVMContext arch
llvmctx) <- ReaderT
  (Declare, Maybe DecodedName, LLVMContext arch)
  (MaybeT (OverrideSim p sym LLVM rtp l a))
  (Declare, Maybe DecodedName, LLVMContext arch)
forall r (m :: Type -> Type). MonadReader r m => m r
ask
  let decl :: Declare
decl = LLVMOverride p sym args ret -> Declare
forall p sym (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym args ret -> Declare
llvmOverride_declare LLVMOverride p sym args ret
llvmOverride
  if Bool -> Bool
not (Declare -> Declare -> Bool
isMatchingDeclaration Declare
requestedDecl Declare
decl) then
    do Bool
-> RegOverrideM p sym arch rtp l a ()
-> RegOverrideM p sym arch rtp l a ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (Declare -> Symbol
L.decName Declare
requestedDecl Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Declare -> Symbol
L.decName Declare
decl) (RegOverrideM p sym arch rtp l a ()
 -> RegOverrideM p sym arch rtp l a ())
-> RegOverrideM p sym arch rtp l a ()
-> RegOverrideM p sym arch rtp l a ()
forall a b. (a -> b) -> a -> b
$
         do Int -> String -> IO ()
logFn <- MaybeT (OverrideSim p sym LLVM rtp l a) (Int -> String -> IO ())
-> ReaderT
     (Declare, Maybe DecodedName, LLVMContext arch)
     (MaybeT (OverrideSim p sym LLVM rtp l a))
     (Int -> String -> IO ())
forall (m :: Type -> Type) a.
Monad m =>
m a -> ReaderT (Declare, Maybe DecodedName, LLVMContext arch) m a
forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (MaybeT (OverrideSim p sym LLVM rtp l a) (Int -> String -> IO ())
 -> ReaderT
      (Declare, Maybe DecodedName, LLVMContext arch)
      (MaybeT (OverrideSim p sym LLVM rtp l a))
      (Int -> String -> IO ()))
-> MaybeT (OverrideSim p sym LLVM rtp l a) (Int -> String -> IO ())
-> ReaderT
     (Declare, Maybe DecodedName, LLVMContext arch)
     (MaybeT (OverrideSim p sym LLVM rtp l a))
     (Int -> String -> IO ())
forall a b. (a -> b) -> a -> b
$ OverrideSim p sym LLVM rtp l a (Int -> String -> IO ())
-> MaybeT (OverrideSim p sym LLVM rtp l a) (Int -> String -> IO ())
forall (m :: Type -> Type) a. Monad m => m a -> MaybeT m a
forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (OverrideSim p sym LLVM rtp l a (Int -> String -> IO ())
 -> MaybeT
      (OverrideSim p sym LLVM rtp l a) (Int -> String -> IO ()))
-> OverrideSim p sym LLVM rtp l a (Int -> String -> IO ())
-> MaybeT (OverrideSim p sym LLVM rtp l a) (Int -> String -> IO ())
forall a b. (a -> b) -> a -> b
$ OverrideSim p sym LLVM rtp l a (Int -> String -> IO ())
forall (m :: Type -> Type).
MonadVerbosity m =>
m (Int -> String -> IO ())
getLogFunction
            IO () -> RegOverrideM p sym arch rtp l a ()
forall a.
IO a
-> ReaderT
     (Declare, Maybe DecodedName, LLVMContext arch)
     (MaybeT (OverrideSim p sym LLVM rtp l a))
     a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO () -> RegOverrideM p sym arch rtp l a ())
-> IO () -> RegOverrideM p sym arch rtp l a ()
forall a b. (a -> b) -> a -> b
$ Int -> String -> IO ()
logFn Int
3 (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines
              [ String
"Mismatched declaration signatures"
              , String
" *** requested: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Declare -> String
forall a. Show a => a -> String
show Declare
requestedDecl
              , String
" *** found: "     String -> String -> String
forall a. [a] -> [a] -> [a]
++ Declare -> String
forall a. Show a => a -> String
show Declare
decl
              , String
""
              ]
       RegOverrideM p sym arch rtp l a ()
forall a.
ReaderT
  (Declare, Maybe DecodedName, LLVMContext arch)
  (MaybeT (OverrideSim p sym LLVM rtp l a))
  a
forall (f :: Type -> Type) a. Alternative f => f a
empty
  else MaybeT (OverrideSim p sym LLVM rtp l a) ()
-> RegOverrideM p sym arch rtp l a ()
forall (m :: Type -> Type) a.
Monad m =>
m a -> ReaderT (Declare, Maybe DecodedName, LLVMContext arch) m a
forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (OverrideSim p sym LLVM rtp l a ()
-> MaybeT (OverrideSim p sym LLVM rtp l a) ()
forall (m :: Type -> Type) a. Monad m => m a -> MaybeT m a
forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (LLVMContext arch
-> LLVMOverride p sym args ret -> OverrideSim p sym LLVM rtp l a ()
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym) =>
LLVMContext arch
-> LLVMOverride p sym args ret -> OverrideSim p sym LLVM rtp l a ()
do_register_llvm_override LLVMContext arch
llvmctx LLVMOverride p sym args ret
llvmOverride))

-- | Bind a function handle, and also bind the function to the global function
-- allocation in the LLVM memory.
bind_llvm_handle ::
  (IsSymInterface sym, HasPtrWidth wptr) =>
  LLVMContext arch ->
  L.Symbol ->
  FnHandle args ret ->
  FnState p sym LLVM args ret ->
  OverrideSim p sym LLVM rtp l a ()
bind_llvm_handle :: forall sym (wptr :: Natural) (arch :: LLVMArch)
       (args :: Ctx CrucibleType) (ret :: CrucibleType) p rtp
       (l :: Ctx CrucibleType) (a :: CrucibleType).
(IsSymInterface sym, HasPtrWidth wptr) =>
LLVMContext arch
-> Symbol
-> FnHandle args ret
-> FnState p sym LLVM args ret
-> OverrideSim p sym LLVM rtp l a ()
bind_llvm_handle LLVMContext arch
llvmCtx Symbol
nm FnHandle args ret
hdl FnState p sym LLVM args ret
impl = do
  let mvar :: GlobalVar Mem
mvar = LLVMContext arch -> GlobalVar Mem
forall (arch :: LLVMArch). LLVMContext arch -> GlobalVar Mem
llvmMemVar LLVMContext arch
llvmCtx
  FnHandle args ret
-> FnState p sym LLVM args ret -> OverrideSim p sym LLVM rtp l a ()
forall (args :: Ctx CrucibleType) (ret :: CrucibleType) p sym ext
       rtp (a :: Ctx CrucibleType) (r :: CrucibleType).
FnHandle args ret
-> FnState p sym ext args ret -> OverrideSim p sym ext rtp a r ()
bindFnHandle FnHandle args ret
hdl FnState p sym LLVM args ret
impl
  MemImpl sym
mem <- GlobalVar Mem -> OverrideSim p sym LLVM rtp l a (RegValue sym Mem)
forall sym (tp :: CrucibleType) p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
IsSymInterface sym =>
GlobalVar tp
-> OverrideSim p sym ext rtp args ret (RegValue sym tp)
readGlobal GlobalVar Mem
mvar
  MemImpl sym
mem' <- (forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym LLVM rtp l a (MemImpl sym))
-> OverrideSim p sym LLVM rtp l a (MemImpl sym)
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
ovrWithBackend ((forall bak.
  IsSymBackend sym bak =>
  bak -> OverrideSim p sym LLVM rtp l a (MemImpl sym))
 -> OverrideSim p sym LLVM rtp l a (MemImpl sym))
-> (forall bak.
    IsSymBackend sym bak =>
    bak -> OverrideSim p sym LLVM rtp l a (MemImpl sym))
-> OverrideSim p sym LLVM rtp l a (MemImpl sym)
forall a b. (a -> b) -> a -> b
$ \bak
bak -> IO (MemImpl sym) -> OverrideSim p sym LLVM rtp l a (MemImpl sym)
forall a. IO a -> OverrideSim p sym LLVM rtp l a a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (MemImpl sym) -> OverrideSim p sym LLVM rtp l a (MemImpl sym))
-> IO (MemImpl sym) -> OverrideSim p sym LLVM rtp l a (MemImpl sym)
forall a b. (a -> b) -> a -> b
$ bak
-> Symbol -> FnHandle args ret -> MemImpl sym -> IO (MemImpl sym)
forall sym bak (wptr :: Natural) (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymBackend sym bak, HasPtrWidth wptr) =>
bak
-> Symbol -> FnHandle args ret -> MemImpl sym -> IO (MemImpl sym)
bindLLVMFunPtr bak
bak Symbol
nm FnHandle args ret
hdl MemImpl sym
mem
  GlobalVar Mem
-> RegValue sym Mem -> OverrideSim p sym LLVM rtp l a ()
forall (tp :: CrucibleType) sym p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
GlobalVar tp
-> RegValue sym tp -> OverrideSim p sym ext rtp args ret ()
writeGlobal GlobalVar Mem
mvar RegValue sym Mem
MemImpl sym
mem'

-- | Low-level function to register LLVM functions.
--
-- Creates and binds a function handle, and also binds the function to the
-- global function allocation in the LLVM memory.
bind_llvm_func ::
  (IsSymInterface sym, HasPtrWidth wptr) =>
  LLVMContext arch ->
  L.Symbol ->
  Ctx.Assignment TypeRepr args ->
  TypeRepr ret ->
  FnState p sym LLVM args ret ->
  OverrideSim p sym LLVM rtp l a ()
bind_llvm_func :: forall sym (wptr :: Natural) (arch :: LLVMArch)
       (args :: Ctx CrucibleType) (ret :: CrucibleType) p rtp
       (l :: Ctx CrucibleType) (a :: CrucibleType).
(IsSymInterface sym, HasPtrWidth wptr) =>
LLVMContext arch
-> Symbol
-> Assignment TypeRepr args
-> TypeRepr ret
-> FnState p sym LLVM args ret
-> OverrideSim p sym LLVM rtp l a ()
bind_llvm_func LLVMContext arch
llvmCtx Symbol
nm Assignment TypeRepr args
args TypeRepr ret
ret FnState p sym LLVM args ret
impl = do
  let L.Symbol String
strNm = Symbol
nm
  let fnm :: FunctionName
fnm  = Text -> FunctionName
functionNameFromText (String -> Text
Text.pack String
strNm)
  SimContext p sym LLVM
ctx <- Getting
  (SimContext p sym LLVM)
  (SimState p sym LLVM rtp (OverrideLang a) ('Just l))
  (SimContext p sym LLVM)
-> OverrideSim p sym LLVM rtp l a (SimContext p sym LLVM)
forall s (m :: Type -> Type) a.
MonadState s m =>
Getting a s a -> m a
use Getting
  (SimContext p sym LLVM)
  (SimState p sym LLVM rtp (OverrideLang a) ('Just l))
  (SimContext p sym LLVM)
forall p sym ext r f1 (a :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
Functor f2 =>
(SimContext p sym ext -> f2 (SimContext p sym ext))
-> SimState p sym ext r f1 a -> f2 (SimState p sym ext r f1 a)
stateContext
  let ha :: HandleAllocator
ha = SimContext p sym LLVM -> HandleAllocator
forall personality sym ext.
SimContext personality sym ext -> HandleAllocator
simHandleAllocator SimContext p sym LLVM
ctx
  FnHandle args ret
h <- IO (FnHandle args ret)
-> OverrideSim p sym LLVM rtp l a (FnHandle args ret)
forall a. IO a -> OverrideSim p sym LLVM rtp l a a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (FnHandle args ret)
 -> OverrideSim p sym LLVM rtp l a (FnHandle args ret))
-> IO (FnHandle args ret)
-> OverrideSim p sym LLVM rtp l a (FnHandle args ret)
forall a b. (a -> b) -> a -> b
$ HandleAllocator
-> FunctionName
-> Assignment TypeRepr args
-> TypeRepr ret
-> IO (FnHandle args ret)
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
HandleAllocator
-> FunctionName
-> Assignment TypeRepr args
-> TypeRepr ret
-> IO (FnHandle args ret)
mkHandle' HandleAllocator
ha FunctionName
fnm Assignment TypeRepr args
args TypeRepr ret
ret
  LLVMContext arch
-> Symbol
-> FnHandle args ret
-> FnState p sym LLVM args ret
-> OverrideSim p sym LLVM rtp l a ()
forall sym (wptr :: Natural) (arch :: LLVMArch)
       (args :: Ctx CrucibleType) (ret :: CrucibleType) p rtp
       (l :: Ctx CrucibleType) (a :: CrucibleType).
(IsSymInterface sym, HasPtrWidth wptr) =>
LLVMContext arch
-> Symbol
-> FnHandle args ret
-> FnState p sym LLVM args ret
-> OverrideSim p sym LLVM rtp l a ()
bind_llvm_handle LLVMContext arch
llvmCtx Symbol
nm FnHandle args ret
h FnState p sym LLVM args ret
impl

-- | Low-level function to register LLVM overrides.
--
-- Type-checks the LLVM override against the 'L.Declare' it contains, adapting
-- its arguments and return values as necessary. Then creates and binds
-- a function handle, and also binds the function to the global function
-- allocation in the LLVM memory.
--
-- Useful when you don\'t have access to a full LLVM AST, e.g., when parsing
-- Crucible CFGs written in crucible-syntax. For more usual cases, use
-- 'Lang.Crucible.LLVM.Intrinsics.register_llvm_overrides'.
do_register_llvm_override :: forall p args ret sym arch wptr l a rtp.
  (IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym) =>
  LLVMContext arch ->
  LLVMOverride p sym args ret ->
  OverrideSim p sym LLVM rtp l a ()
do_register_llvm_override :: forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym) =>
LLVMContext arch
-> LLVMOverride p sym args ret -> OverrideSim p sym LLVM rtp l a ()
do_register_llvm_override LLVMContext arch
llvmctx LLVMOverride p sym args ret
llvmOverride = do
  let decl :: Declare
decl = LLVMOverride p sym args ret -> Declare
forall p sym (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym args ret -> Declare
llvmOverride_declare LLVMOverride p sym args ret
llvmOverride
  let (L.Symbol String
str_nm) = Declare -> Symbol
L.decName Declare
decl
  let fnm :: FunctionName
fnm  = Text -> FunctionName
functionNameFromText (String -> Text
Text.pack String
str_nm)

  let mvar :: GlobalVar Mem
mvar = LLVMContext arch -> GlobalVar Mem
forall (arch :: LLVMArch). LLVMContext arch -> GlobalVar Mem
llvmMemVar LLVMContext arch
llvmctx
  let overrideArgs :: CtxRepr args
overrideArgs = LLVMOverride p sym args ret -> CtxRepr args
forall p sym (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym args ret -> CtxRepr args
llvmOverride_args LLVMOverride p sym args ret
llvmOverride
  let overrideRet :: TypeRepr ret
overrideRet  = LLVMOverride p sym args ret -> TypeRepr ret
forall p sym (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym args ret -> TypeRepr ret
llvmOverride_ret LLVMOverride p sym args ret
llvmOverride

  let ?lc = LLVMContext arch
llvmctxLLVMContext arch
-> Getting TypeContext (LLVMContext arch) TypeContext
-> TypeContext
forall s a. s -> Getting a s a -> a
^.Getting TypeContext (LLVMContext arch) TypeContext
forall (arch :: LLVMArch) (f :: Type -> Type).
Functor f =>
(TypeContext -> f TypeContext)
-> LLVMContext arch -> f (LLVMContext arch)
llvmTypeCtx

  Declare
-> (forall {args :: Ctx CrucibleType} {ret :: CrucibleType}.
    CtxRepr args -> TypeRepr ret -> OverrideSim p sym LLVM rtp l a ())
-> OverrideSim p sym LLVM rtp l a ()
forall (wptr :: Natural) (m :: Type -> Type) a.
(?lc::TypeContext, HasPtrWidth wptr, MonadFail m) =>
Declare
-> (forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
    CtxRepr args -> TypeRepr ret -> m a)
-> m a
llvmDeclToFunHandleRepr' Declare
decl ((forall {args :: Ctx CrucibleType} {ret :: CrucibleType}.
  CtxRepr args -> TypeRepr ret -> OverrideSim p sym LLVM rtp l a ())
 -> OverrideSim p sym LLVM rtp l a ())
-> (forall {args :: Ctx CrucibleType} {ret :: CrucibleType}.
    CtxRepr args -> TypeRepr ret -> OverrideSim p sym LLVM rtp l a ())
-> OverrideSim p sym LLVM rtp l a ()
forall a b. (a -> b) -> a -> b
$ \CtxRepr args
args TypeRepr ret
ret -> do
    Override p sym LLVM args ret
o <- FunctionName
-> CtxRepr args
-> TypeRepr ret
-> CtxRepr args
-> TypeRepr ret
-> (forall bak rtp' (l' :: Ctx CrucibleType) (a' :: CrucibleType).
    IsSymBackend sym bak =>
    bak
    -> Assignment (RegEntry sym) args
    -> OverrideSim p sym LLVM rtp' l' a' (RegValue sym ret))
-> OverrideSim p sym LLVM rtp l a (Override p sym LLVM args ret)
forall sym (args :: Ctx CrucibleType) (ret :: CrucibleType)
       (args' :: Ctx CrucibleType) (ret' :: CrucibleType) p rtp
       (l :: Ctx CrucibleType) (a :: CrucibleType).
HasLLVMAnn sym =>
FunctionName
-> CtxRepr args
-> TypeRepr ret
-> CtxRepr args'
-> TypeRepr ret'
-> (forall bak rtp' (l' :: Ctx CrucibleType) (a' :: CrucibleType).
    IsSymBackend sym bak =>
    bak
    -> Assignment (RegEntry sym) args
    -> OverrideSim p sym LLVM rtp' l' a' (RegValue sym ret))
-> OverrideSim p sym LLVM rtp l a (Override p sym LLVM args' ret')
build_llvm_override FunctionName
fnm CtxRepr args
overrideArgs TypeRepr ret
overrideRet CtxRepr args
args TypeRepr ret
ret
           (\bak
bak Assignment (RegEntry sym) args
asgn -> LLVMOverride p sym args ret
-> forall bak.
   IsSymBackend sym bak =>
   GlobalVar Mem
   -> bak
   -> Assignment (RegEntry sym) args
   -> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
      OverrideSim p sym LLVM rtp args' ret' (RegValue sym ret)
forall p sym (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym args ret
-> forall bak.
   IsSymBackend sym bak =>
   GlobalVar Mem
   -> bak
   -> Assignment (RegEntry sym) args
   -> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
      OverrideSim p sym LLVM rtp args' ret' (RegValue sym ret)
llvmOverride_def LLVMOverride p sym args ret
llvmOverride GlobalVar Mem
mvar bak
bak Assignment (RegEntry sym) args
asgn)
    LLVMContext arch
-> Symbol
-> CtxRepr args
-> TypeRepr ret
-> FnState p sym LLVM args ret
-> OverrideSim p sym LLVM rtp l a ()
forall sym (wptr :: Natural) (arch :: LLVMArch)
       (args :: Ctx CrucibleType) (ret :: CrucibleType) p rtp
       (l :: Ctx CrucibleType) (a :: CrucibleType).
(IsSymInterface sym, HasPtrWidth wptr) =>
LLVMContext arch
-> Symbol
-> Assignment TypeRepr args
-> TypeRepr ret
-> FnState p sym LLVM args ret
-> OverrideSim p sym LLVM rtp l a ()
bind_llvm_func LLVMContext arch
llvmctx (Declare -> Symbol
L.decName Declare
decl) CtxRepr args
args TypeRepr ret
ret (Override p sym LLVM args ret -> FnState p sym LLVM args ret
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
Override p sym ext args ret -> FnState p sym ext args ret
UseOverride Override p sym LLVM args ret
o)

-- | Create an allocation for an override and register it.
--
-- Useful when registering an override for a function in an LLVM memory that
-- wasn't initialized with the functions in "Lang.Crucible.LLVM.Globals", e.g.,
-- when parsing Crucible CFGs written in crucible-syntax. For more usual cases,
-- use 'Lang.Crucible.LLVM.Intrinsics.register_llvm_overrides'.
--
-- c.f. 'Lang.Crucible.LLVM.Globals.allocLLVMFunPtr'
alloc_and_register_override ::
  (IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions) =>
  bak ->
  LLVMContext arch ->
  LLVMOverride p sym args ret ->
  -- | Aliases
  [L.Symbol] ->
  OverrideSim p sym LLVM rtp l a ()
alloc_and_register_override :: forall sym bak (wptr :: Natural) (arch :: LLVMArch) p
       (args :: Ctx CrucibleType) (ret :: CrucibleType) rtp
       (l :: Ctx CrucibleType) (a :: CrucibleType).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> LLVMContext arch
-> LLVMOverride p sym args ret
-> [Symbol]
-> OverrideSim p sym LLVM rtp l a ()
alloc_and_register_override bak
bak LLVMContext arch
llvmctx LLVMOverride p sym args ret
llvmOverride [Symbol]
aliases = do
  let L.Declare { decName :: Declare -> Symbol
L.decName = symb :: Symbol
symb@(L.Symbol String
nm) } = LLVMOverride p sym args ret -> Declare
forall p sym (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym args ret -> Declare
llvmOverride_declare LLVMOverride p sym args ret
llvmOverride
  let mvar :: GlobalVar Mem
mvar = LLVMContext arch -> GlobalVar Mem
forall (arch :: LLVMArch). LLVMContext arch -> GlobalVar Mem
llvmMemVar LLVMContext arch
llvmctx
  MemImpl sym
mem <- GlobalVar Mem -> OverrideSim p sym LLVM rtp l a (RegValue sym Mem)
forall sym (tp :: CrucibleType) p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
IsSymInterface sym =>
GlobalVar tp
-> OverrideSim p sym ext rtp args ret (RegValue sym tp)
readGlobal GlobalVar Mem
mvar
  (LLVMPointer sym wptr
_ptr, MemImpl sym
mem') <- IO (LLVMPointer sym wptr, MemImpl sym)
-> OverrideSim
     p sym LLVM rtp l a (LLVMPointer sym wptr, MemImpl sym)
forall a. IO a -> OverrideSim p sym LLVM rtp l a a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (bak
-> MemImpl sym
-> String
-> Symbol
-> [Symbol]
-> IO (LLVMPtr sym wptr, MemImpl sym)
forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> MemImpl sym
-> String
-> Symbol
-> [Symbol]
-> IO (LLVMPtr sym wptr, MemImpl sym)
registerFunPtr bak
bak MemImpl sym
mem String
nm Symbol
symb [Symbol]
aliases)
  GlobalVar Mem
-> RegValue sym Mem -> OverrideSim p sym LLVM rtp l a ()
forall (tp :: CrucibleType) sym p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
GlobalVar tp
-> RegValue sym tp -> OverrideSim p sym ext rtp args ret ()
writeGlobal GlobalVar Mem
mvar RegValue sym Mem
MemImpl sym
mem'
  LLVMContext arch
-> LLVMOverride p sym args ret -> OverrideSim p sym LLVM rtp l a ()
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym) =>
LLVMContext arch
-> LLVMOverride p sym args ret -> OverrideSim p sym LLVM rtp l a ()
do_register_llvm_override LLVMContext arch
llvmctx LLVMOverride p sym args ret
llvmOverride