-- |
-- Module           : Lang.Crucible.LLVM.Functions
-- Description      : Register functions (CFGs and overrides)
-- Copyright        : (c) Galois, Inc 2024
-- License          : BSD3
-- Maintainer       : Langston Barrett <langston@galois.com>
-- Stability        : provisional
--
-- Registering functions to be used with the LLVM memory model is somewhat more
-- complex than for other Crucible frontends, as LLVM has a notion of function
-- pointers. Each function to be registered has to go through a few steps (the
-- first two are common to all Crucible frontends):
--
-- * Create a 'FnHandle' and a 'FnState' (a translated CFG or an override)
-- * Bind the 'FnHandle' to the 'FnState' ('OverrideSim.bindFnHandle')
-- * Create a (global, immutable, zero-sized) allocation corresponding to the
--   function in the 'MemImpl' ('allocFunPtr')
-- * Register the correspondence between the function\'s name (and any aliases)
--   and its global allocation ('registerGlobal', or via 'registerFunPtr')
-- * Register the correspondence between the function\'s allocation and its
--   handle ('doInstallHandle', or via 'bindLLVMHandle', 'bindLLVMCFG', or
--   'bindLLVMFunc')
--
-- This module provides helpers to accomplish all of this. They\'re ordered
-- roughly low-level/customizable to high-level/automated.
--
-- Perhaps surprisingly, there\'s no function that does all of the above at
-- once. This is because there are two main places where binding functions
-- happens:
--
-- * "Lang.Crucible.LLVM" registers translated CFGs, but does so lazily. In
--   particular, this means that it initially binds the handle and allocation to
--   a \"stub\" that, when called, will translate the actual CFG and then
--   re-bind the handle and allocation to it.
-- * "Lang.Crucible.LLVM.Intrinsics.Common" registers overrides, which generally
--   apply to functions that are @declare@d but not @define@d. Thus, they
--   already have corresponding allocations, which just need to be associated
--   with the override.
--
-- Prior to these, function allocation happens in
-- 'Lang.Crucible.LLVM.Globals.initializeMemory'.
------------------------------------------------------------------------

{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImplicitParams #-}

module Lang.Crucible.LLVM.Functions
  ( allocFunPtr
  , allocLLVMFunPtr
  , allocLLVMFunPtrs
  , registerFunPtr
  , bindLLVMFunPtr
  , bindLLVMHandle
  , bindLLVMCFG
  , bindLLVMFunc
  ) where

import           Control.Lens (use)
import           Control.Monad (foldM)
import           Control.Monad.IO.Class (liftIO)
import qualified Data.Map as Map
import qualified Data.Set as Set
import           qualified Data.Text as Text

import qualified Text.LLVM.AST as L

import qualified Data.Parameterized.Context as Ctx

import           What4.FunctionName (functionNameFromText)
import qualified What4.Interface as W4

import           Lang.Crucible.Analysis.Postdom (postdomInfo)
import           Lang.Crucible.Backend
import           Lang.Crucible.CFG.Common (GlobalVar)
import           Lang.Crucible.CFG.Core (CFG)
import           Lang.Crucible.CFG.Core (TypeRepr(..), cfgHandle)
import           Lang.Crucible.FunctionHandle (FnHandle(handleArgTypes), mkHandle')
import           Lang.Crucible.Simulator.ExecutionTree (stateContext)
import           Lang.Crucible.Simulator (FnState(..), SimContext(..))
import           Lang.Crucible.Simulator.OverrideSim (OverrideSim)
import qualified Lang.Crucible.Simulator.OverrideSim as OverrideSim

import           Lang.Crucible.LLVM.DataLayout
import           Lang.Crucible.LLVM.MemModel
import qualified Lang.Crucible.LLVM.MemModel as G
import           Lang.Crucible.LLVM.Translation.Monad
import           Lang.Crucible.LLVM.Extension (LLVM)

-- | Create a global allocation to be assocated with a function.
--
-- The returned allocation is global ('G.GlobalAlloc'), immutable
-- ('G.Immutable'), and has a size and alignment of zero.
allocFunPtr ::
  ( IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym
  , ?memOpts :: MemOptions ) =>
  bak ->
  MemImpl sym ->
  -- | Function Name
  String ->
  IO (LLVMPtr sym wptr, MemImpl sym)
allocFunPtr :: forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak -> MemImpl sym -> String -> IO (LLVMPtr sym wptr, MemImpl sym)
allocFunPtr bak
bak MemImpl sym
mem String
nm = do
  let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak
  SymExpr sym (BaseBVType wptr)
z <- sym -> NatRepr wptr -> IO (SymExpr sym (BaseBVType wptr))
forall (w :: Natural) sym.
(1 <= w, IsExprBuilder sym) =>
sym -> NatRepr w -> IO (SymBV sym w)
W4.bvZero sym
sym ?ptrWidth::NatRepr wptr
NatRepr wptr
?ptrWidth
  bak
-> AllocType
-> Mutability
-> String
-> MemImpl sym
-> SymExpr sym (BaseBVType wptr)
-> Alignment
-> IO (LLVMPtr sym wptr, MemImpl sym)
forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> AllocType
-> Mutability
-> String
-> MemImpl sym
-> SymBV sym wptr
-> Alignment
-> IO (LLVMPtr sym wptr, MemImpl sym)
doMalloc bak
bak AllocType
G.GlobalAlloc Mutability
G.Immutable String
nm MemImpl sym
mem SymExpr sym (BaseBVType wptr)
z Alignment
noAlignment

-- | Create a global allocation assocated with a function (see 'allocFunPtr'),
-- and register the function\'s primary symbol and its aliases as associated
-- with that allocation.
registerFunPtr ::
  ( IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym
  , ?memOpts :: MemOptions ) =>
  bak ->
  MemImpl sym ->
  -- | Display name
  String ->
  -- | Function name
  L.Symbol ->
  -- | Aliases
  [L.Symbol] ->
  IO (LLVMPtr sym wptr, MemImpl sym)
registerFunPtr :: 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
displayName Symbol
nm [Symbol]
aliases = do
  (LLVMPointer sym wptr
ptr, MemImpl sym
mem') <- bak -> MemImpl sym -> String -> IO (LLVMPtr sym wptr, MemImpl sym)
forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak -> MemImpl sym -> String -> IO (LLVMPtr sym wptr, MemImpl sym)
allocFunPtr bak
bak MemImpl sym
mem String
displayName
  (LLVMPointer sym wptr, MemImpl sym)
-> IO (LLVMPointer sym wptr, MemImpl sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ((LLVMPointer sym wptr, MemImpl sym)
 -> IO (LLVMPointer sym wptr, MemImpl sym))
-> (LLVMPointer sym wptr, MemImpl sym)
-> IO (LLVMPointer sym wptr, MemImpl sym)
forall a b. (a -> b) -> a -> b
$ (LLVMPointer sym wptr
ptr, MemImpl sym -> [Symbol] -> LLVMPtr sym wptr -> MemImpl sym
forall sym (wptr :: Natural).
(IsExprBuilder sym, 1 <= wptr) =>
MemImpl sym -> [Symbol] -> LLVMPtr sym wptr -> MemImpl sym
registerGlobal MemImpl sym
mem' (Symbol
nmSymbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
:[Symbol]
aliases) LLVMPtr sym wptr
LLVMPointer sym wptr
ptr)

-- Not exported
funAliases ::
  LLVMContext arch ->
  L.Symbol ->
  [L.Symbol]
funAliases :: forall (arch :: LLVMArch). LLVMContext arch -> Symbol -> [Symbol]
funAliases LLVMContext arch
llvmCtx Symbol
symbol =
  let aliases :: Map Symbol (Set GlobalAlias)
aliases = LLVMContext arch -> Map Symbol (Set GlobalAlias)
forall (arch :: LLVMArch).
LLVMContext arch -> Map Symbol (Set GlobalAlias)
llvmFunctionAliases LLVMContext arch
llvmCtx
  in (GlobalAlias -> Symbol) -> [GlobalAlias] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map GlobalAlias -> Symbol
L.aliasName ([GlobalAlias] -> [Symbol]) -> [GlobalAlias] -> [Symbol]
forall a b. (a -> b) -> a -> b
$ [GlobalAlias]
-> (Set GlobalAlias -> [GlobalAlias])
-> Maybe (Set GlobalAlias)
-> [GlobalAlias]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] Set GlobalAlias -> [GlobalAlias]
forall a. Set a -> [a]
Set.toList (Maybe (Set GlobalAlias) -> [GlobalAlias])
-> Maybe (Set GlobalAlias) -> [GlobalAlias]
forall a b. (a -> b) -> a -> b
$ Symbol -> Map Symbol (Set GlobalAlias) -> Maybe (Set GlobalAlias)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Symbol
symbol Map Symbol (Set GlobalAlias)
aliases

-- | Create a global allocation assocated with a function (see 'allocFunPtr'),
-- register the function\'s primary symbol and its aliases as associated with
-- that allocation (see 'registerFunPtr'), looking up the aliases from the
-- 'LLVMContext'.
allocLLVMFunPtr ::
  ( IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym
  , ?memOpts :: MemOptions ) =>
  bak ->
  LLVMContext arch ->
  MemImpl sym ->
  Either L.Declare L.Define ->
  IO (LLVMPtr sym wptr, MemImpl sym)
allocLLVMFunPtr :: forall sym bak (wptr :: Natural) (arch :: LLVMArch).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> LLVMContext arch
-> MemImpl sym
-> Either Declare Define
-> IO (LLVMPtr sym wptr, MemImpl sym)
allocLLVMFunPtr bak
bak LLVMContext arch
llvm_ctx MemImpl sym
mem Either Declare Define
decl = do
  let (Symbol
symbol, String
displayString) =
        case Either Declare Define
decl of
          Left Declare
d ->
            let s :: Symbol
s@(L.Symbol String
nm) = Declare -> Symbol
L.decName Declare
d
             in ( Symbol
s, String
"[external function] " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm )
          Right Define
d ->
            let s :: Symbol
s@(L.Symbol String
nm) = Define -> Symbol
L.defName Define
d
             in ( Symbol
s, String
"[defined function ] " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm)
  let aliases :: [Symbol]
aliases = LLVMContext arch -> Symbol -> [Symbol]
forall (arch :: LLVMArch). LLVMContext arch -> Symbol -> [Symbol]
funAliases LLVMContext arch
llvm_ctx Symbol
symbol
  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
displayString Symbol
symbol [Symbol]
aliases

-- | Create global allocations associated with each function in a module (see
-- 'allocLLVMFunPtr').
allocLLVMFunPtrs ::
  ( IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym
  , ?memOpts :: MemOptions ) =>
  bak ->
  LLVMContext arch ->
  MemImpl sym ->
  L.Module ->
  IO (MemImpl sym)
allocLLVMFunPtrs :: forall sym bak (wptr :: Natural) (arch :: LLVMArch).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> LLVMContext arch -> MemImpl sym -> Module -> IO (MemImpl sym)
allocLLVMFunPtrs bak
bak LLVMContext arch
llvmCtx MemImpl sym
mem0 Module
llvmMod = do
   -- allocate pointers values for function symbols, but do not
   -- yet bind them to function handles
   let decls :: [Either Declare Define]
decls = (Declare -> Either Declare Define)
-> [Declare] -> [Either Declare Define]
forall a b. (a -> b) -> [a] -> [b]
map Declare -> Either Declare Define
forall a b. a -> Either a b
Left (Module -> [Declare]
L.modDeclares Module
llvmMod) [Either Declare Define]
-> [Either Declare Define] -> [Either Declare Define]
forall a. [a] -> [a] -> [a]
++ (Define -> Either Declare Define)
-> [Define] -> [Either Declare Define]
forall a b. (a -> b) -> [a] -> [b]
map Define -> Either Declare Define
forall a b. b -> Either a b
Right (Module -> [Define]
L.modDefines Module
llvmMod)

   let allocLLVMFunPtr' :: bak
-> LLVMContext arch
-> MemImpl sym
-> Either Declare Define
-> IO (MemImpl sym)
allocLLVMFunPtr' bak
bak' LLVMContext arch
lctx MemImpl sym
mem Either Declare Define
decl = (LLVMPointer sym wptr, MemImpl sym) -> MemImpl sym
forall a b. (a, b) -> b
snd ((LLVMPointer sym wptr, MemImpl sym) -> MemImpl sym)
-> IO (LLVMPointer sym wptr, MemImpl sym) -> IO (MemImpl sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> bak
-> LLVMContext arch
-> MemImpl sym
-> Either Declare Define
-> IO (LLVMPtr sym wptr, MemImpl sym)
forall sym bak (wptr :: Natural) (arch :: LLVMArch).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> LLVMContext arch
-> MemImpl sym
-> Either Declare Define
-> IO (LLVMPtr sym wptr, MemImpl sym)
allocLLVMFunPtr bak
bak' LLVMContext arch
lctx MemImpl sym
mem Either Declare Define
decl
   (MemImpl sym -> Either Declare Define -> IO (MemImpl sym))
-> MemImpl sym -> [Either Declare Define] -> IO (MemImpl sym)
forall (t :: Type -> Type) (m :: Type -> Type) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (bak
-> LLVMContext arch
-> MemImpl sym
-> Either Declare Define
-> IO (MemImpl sym)
forall {wptr :: Natural} {sym} {bak} {arch :: LLVMArch}.
(Assert
   (OrdCond (CmpNat 1 wptr) 'True 'True 'False) (TypeError ...),
 Assert
   (OrdCond (CmpNat 16 wptr) 'True 'True 'False) (TypeError ...),
 IsSymBackend sym bak, ?ptrWidth::NatRepr wptr,
 ?memOpts::MemOptions,
 ?recordLLVMAnnotation::CallStack
                        -> BoolAnn sym -> BadBehavior sym -> IO ()) =>
bak
-> LLVMContext arch
-> MemImpl sym
-> Either Declare Define
-> IO (MemImpl sym)
allocLLVMFunPtr' bak
bak LLVMContext arch
llvmCtx) MemImpl sym
mem0 [Either Declare Define]
decls

-- Not exported
someFnHandle :: FnHandle args ret -> SomeFnHandle
someFnHandle :: forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> SomeFnHandle
someFnHandle FnHandle args ret
h =
  case FnHandle args ret -> CtxRepr args
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> CtxRepr args
handleArgTypes FnHandle args ret
h of
    (Assignment TypeRepr ctx
_ Ctx.:> VectorRepr TypeRepr tp1
AnyRepr) -> FnHandle (ctx ::> VectorType 'AnyType) ret -> SomeFnHandle
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle (args ::> VectorType 'AnyType) ret -> SomeFnHandle
VarargsFnHandle FnHandle args ret
FnHandle (ctx ::> VectorType 'AnyType) ret
h
    CtxRepr args
_ -> FnHandle args ret -> SomeFnHandle
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> SomeFnHandle
SomeFnHandle FnHandle args ret
h

-- | Look up an existing global function allocation by name and bind a handle
-- to it.
--
-- This can overwrite existing allocation/handle associations, and is used to do
-- so when registering lazily-translated CFGs.
--
-- For a stateful version in 'OverrideSim', see 'bindLLVMHandle'.
bindLLVMFunPtr ::
  (IsSymBackend sym bak, HasPtrWidth wptr) =>
  bak ->
  -- | Function name
  L.Symbol ->
  -- | Function implementation (CFG or override)
  FnHandle args ret ->
  -- | LLVM memory
  MemImpl sym ->
  IO (MemImpl sym)
bindLLVMFunPtr :: 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
h MemImpl sym
mem = do
  LLVMPointer sym wptr
ptr <- bak -> MemImpl sym -> Symbol -> IO (LLVMPtr sym wptr)
forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasCallStack) =>
bak -> MemImpl sym -> Symbol -> IO (LLVMPtr sym wptr)
doResolveGlobal bak
bak MemImpl sym
mem Symbol
nm
  bak
-> LLVMPtr sym wptr
-> SomeFnHandle
-> MemImpl sym
-> IO (MemImpl sym)
forall a sym bak (wptr :: Natural).
(Typeable a, IsSymBackend sym bak) =>
bak -> LLVMPtr sym wptr -> a -> MemImpl sym -> IO (MemImpl sym)
doInstallHandle bak
bak LLVMPtr sym wptr
LLVMPointer sym wptr
ptr (FnHandle args ret -> SomeFnHandle
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> SomeFnHandle
someFnHandle FnHandle args ret
h) MemImpl sym
mem

-- | Look up an existing global function allocation by name and bind a handle
-- to it.
--
-- This can overwrite existing allocation/handle associations, and is used to do
-- so when registering lazily-translated CFGs.
--
-- For a less stateful version in 'IO', see 'bindLLVMHandle'.
bindLLVMHandle ::
  (IsSymInterface sym, HasPtrWidth wptr) =>
  GlobalVar Mem ->
  -- | Function name
  L.Symbol ->
  -- | Function handle
  FnHandle args ret ->
  -- | Function implementation (CFG or override)
  FnState p sym ext args ret ->
  OverrideSim p sym ext rtp l a ()
bindLLVMHandle :: forall sym (wptr :: Natural) (args :: Ctx CrucibleType)
       (ret :: CrucibleType) p ext rtp (l :: Ctx CrucibleType)
       (a :: CrucibleType).
(IsSymInterface sym, HasPtrWidth wptr) =>
GlobalVar Mem
-> Symbol
-> FnHandle args ret
-> FnState p sym ext args ret
-> OverrideSim p sym ext rtp l a ()
bindLLVMHandle GlobalVar Mem
mvar Symbol
nm FnHandle args ret
hdl FnState p sym ext args ret
impl = do
  FnHandle args ret
-> FnState p sym ext args ret -> OverrideSim p sym ext 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 ()
OverrideSim.bindFnHandle FnHandle args ret
hdl FnState p sym ext args ret
impl
  MemImpl sym
mem <- GlobalVar Mem -> OverrideSim p sym ext 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)
OverrideSim.readGlobal GlobalVar Mem
mvar
  MemImpl sym
mem' <- (forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym ext rtp l a (MemImpl sym))
-> OverrideSim p sym ext 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
OverrideSim.ovrWithBackend ((forall bak.
  IsSymBackend sym bak =>
  bak -> OverrideSim p sym ext rtp l a (MemImpl sym))
 -> OverrideSim p sym ext rtp l a (MemImpl sym))
-> (forall bak.
    IsSymBackend sym bak =>
    bak -> OverrideSim p sym ext rtp l a (MemImpl sym))
-> OverrideSim p sym ext rtp l a (MemImpl sym)
forall a b. (a -> b) -> a -> b
$ \bak
bak ->
    IO (MemImpl sym) -> OverrideSim p sym ext rtp l a (MemImpl sym)
forall a. IO a -> OverrideSim p sym ext rtp l a a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (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 ext 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 ()
OverrideSim.writeGlobal GlobalVar Mem
mvar RegValue sym Mem
MemImpl sym
mem'

-- | Look up an existing global function allocation by name and bind a CFG to
-- it.
--
-- This can overwrite existing allocation/handle associations, and is used to do
-- so when registering lazily-translated CFGs.
bindLLVMCFG ::
  (IsSymInterface sym, HasPtrWidth wptr) =>
  GlobalVar Mem ->
  -- | Function name
  L.Symbol ->
  -- | Function CFG
  CFG LLVM blocks init ret ->
  OverrideSim p sym LLVM rtp l a ()
bindLLVMCFG :: forall sym (wptr :: Natural) (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType) p rtp
       (l :: Ctx CrucibleType) (a :: CrucibleType).
(IsSymInterface sym, HasPtrWidth wptr) =>
GlobalVar Mem
-> Symbol
-> CFG LLVM blocks init ret
-> OverrideSim p sym LLVM rtp l a ()
bindLLVMCFG GlobalVar Mem
mvar Symbol
name CFG LLVM blocks init ret
cfg = do
  let h :: FnHandle init ret
h = CFG LLVM blocks init ret -> FnHandle init ret
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> FnHandle init ret
cfgHandle CFG LLVM blocks init ret
cfg
      s :: FnState p sym LLVM init ret
s = CFG LLVM blocks init ret
-> CFGPostdom blocks -> FnState p sym LLVM init ret
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)).
CFG ext blocks args ret
-> CFGPostdom blocks -> FnState p sym ext args ret
UseCFG CFG LLVM blocks init ret
cfg (CFG LLVM blocks init ret -> CFGPostdom blocks
forall ext (b :: Ctx (Ctx CrucibleType)) (i :: Ctx CrucibleType)
       (r :: CrucibleType).
CFG ext b i r -> CFGPostdom b
postdomInfo CFG LLVM blocks init ret
cfg)
  GlobalVar Mem
-> Symbol
-> FnHandle init ret
-> FnState p sym LLVM init ret
-> OverrideSim p sym LLVM rtp l a ()
forall sym (wptr :: Natural) (args :: Ctx CrucibleType)
       (ret :: CrucibleType) p ext rtp (l :: Ctx CrucibleType)
       (a :: CrucibleType).
(IsSymInterface sym, HasPtrWidth wptr) =>
GlobalVar Mem
-> Symbol
-> FnHandle args ret
-> FnState p sym ext args ret
-> OverrideSim p sym ext rtp l a ()
bindLLVMHandle GlobalVar Mem
mvar Symbol
name FnHandle init ret
h FnState p sym LLVM init ret
s

-- Private helper to make function handles
mkHandle ::
  -- | Function name
  L.Symbol ->
  -- | Argument types
  Ctx.Assignment TypeRepr args ->
  -- | Return type
  TypeRepr ret ->
  OverrideSim p sym ext rtp l a (FnHandle args ret)
mkHandle :: forall (args :: Ctx CrucibleType) (ret :: CrucibleType) p sym ext
       rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
Symbol
-> Assignment TypeRepr args
-> TypeRepr ret
-> OverrideSim p sym ext rtp l a (FnHandle args ret)
mkHandle Symbol
nm Assignment TypeRepr args
args TypeRepr ret
ret = do
  let L.Symbol String
strNm = Symbol
nm
  let fnm :: FunctionName
fnm  = Text -> FunctionName
functionNameFromText (String -> Text
Text.pack String
strNm)
  SimContext p sym ext
ctx <- Getting
  (SimContext p sym ext)
  (SimState p sym ext rtp (OverrideLang a) ('Just l))
  (SimContext p sym ext)
-> OverrideSim p sym ext rtp l a (SimContext p sym ext)
forall s (m :: Type -> Type) a.
MonadState s m =>
Getting a s a -> m a
use Getting
  (SimContext p sym ext)
  (SimState p sym ext rtp (OverrideLang a) ('Just l))
  (SimContext p sym ext)
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 ext -> HandleAllocator
forall personality sym ext.
SimContext personality sym ext -> HandleAllocator
simHandleAllocator SimContext p sym ext
ctx
  IO (FnHandle args ret)
-> OverrideSim p sym ext rtp l a (FnHandle args ret)
forall a. IO a -> OverrideSim p sym ext rtp l a a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (FnHandle args ret)
 -> OverrideSim p sym ext rtp l a (FnHandle args ret))
-> IO (FnHandle args ret)
-> OverrideSim p sym ext 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

-- | Create a function handle, then call 'bindLLVMHandle' on it.
bindLLVMFunc ::
  (IsSymInterface sym, HasPtrWidth wptr) =>
  GlobalVar Mem ->
  -- | Function name
  L.Symbol ->
  -- | Argument types
  Ctx.Assignment TypeRepr args ->
  -- | Return type
  TypeRepr ret ->
  -- | Function implementation (CFG or override)
  FnState p sym ext args ret ->
  OverrideSim p sym ext rtp l a ()
bindLLVMFunc :: forall sym (wptr :: Natural) (args :: Ctx CrucibleType)
       (ret :: CrucibleType) p ext rtp (l :: Ctx CrucibleType)
       (a :: CrucibleType).
(IsSymInterface sym, HasPtrWidth wptr) =>
GlobalVar Mem
-> Symbol
-> Assignment TypeRepr args
-> TypeRepr ret
-> FnState p sym ext args ret
-> OverrideSim p sym ext rtp l a ()
bindLLVMFunc GlobalVar Mem
mvar Symbol
nm Assignment TypeRepr args
args TypeRepr ret
ret FnState p sym ext args ret
impl = do
  FnHandle args ret
hdl <- Symbol
-> Assignment TypeRepr args
-> TypeRepr ret
-> OverrideSim p sym ext rtp l a (FnHandle args ret)
forall (args :: Ctx CrucibleType) (ret :: CrucibleType) p sym ext
       rtp (l :: Ctx CrucibleType) (a :: CrucibleType).
Symbol
-> Assignment TypeRepr args
-> TypeRepr ret
-> OverrideSim p sym ext rtp l a (FnHandle args ret)
mkHandle Symbol
nm Assignment TypeRepr args
args TypeRepr ret
ret
  GlobalVar Mem
-> Symbol
-> FnHandle args ret
-> FnState p sym ext args ret
-> OverrideSim p sym ext rtp l a ()
forall sym (wptr :: Natural) (args :: Ctx CrucibleType)
       (ret :: CrucibleType) p ext rtp (l :: Ctx CrucibleType)
       (a :: CrucibleType).
(IsSymInterface sym, HasPtrWidth wptr) =>
GlobalVar Mem
-> Symbol
-> FnHandle args ret
-> FnState p sym ext args ret
-> OverrideSim p sym ext rtp l a ()
bindLLVMHandle GlobalVar Mem
mvar Symbol
nm FnHandle args ret
hdl FnState p sym ext args ret
impl