crucible-llvm: Helpers for binding function handles

crucible-llvm/src/Lang/Crucible/LLVM.hs

@@ -43,7 +43,7 @@ import           Lang.Crucible.LLVM.Extension (ArchWidth)
 import           Lang.Crucible.LLVM.Intrinsics
 import           Lang.Crucible.LLVM.MemModel
                    ( llvmStatementExec, HasPtrWidth, HasLLVMAnn, MemOptions, MemImpl
-                   , bindLLVMFunPtr, Mem
+                   , Mem
                    )
 import           Lang.Crucible.LLVM.Translation
 import           Lang.Crucible.Simulator (regValue, FnVal(..))
@@ -87,13 +87,8 @@ registerModuleFn handleWarning mtrans sym =
       let h = cfgHandle cfg
           s = UseCFG cfg (postdomInfo cfg)
       binds <- use (stateContext . functionBindings)
-      bindFnHandle h s
-      let llvm_ctx = mtrans ^. transContext
-      let mvar = llvmMemVar llvm_ctx
-      mem <- readGlobal mvar
-      mem' <- ovrWithBackend $ \bak ->
-                liftIO $ bindLLVMFunPtr bak decl h mem
-      writeGlobal mvar mem'
+      let llvmCtx = mtrans ^. transContext
+      bind_llvm_handle llvmCtx (L.decName decl) h s
 
       when (isJust $ lookupHandleMap h $ fnBindings binds) $
         do loc <- liftIO . getCurrentProgramLoc =<< getSymInterface
@@ -135,38 +130,34 @@ registerLazyModuleFn handleWarning mtrans sym =
      do -- Bind the function handle we just created to the following bootstrapping code,
         -- which actually translates the function on its first execution and patches up
         -- behind itself.
-        bindFnHandle h
-          $ UseOverride
-          $ mkOverride' (handleName h) (handleReturnType h)
-          $ -- This inner action defines what to do when this function is called for the
-            -- first time.  We actually translate the function and install it as the
-            -- implementation for the function handle, instead of this bootstrapping code.
-            liftIO (getTranslatedCFG mtrans sym) >>= \case
-              Nothing ->
-                panic "registerLazyModuleFn"
-                  [ "Could not find definition for function in bootstrapping code"
-                  , show sym
-                  ]
-              Just (_decl, AnyCFG cfg, warns) ->
-                case testEquality (handleType (cfgHandle cfg)) (handleType h) of
-                  Nothing -> panic "registerLazyModuleFn"
-                                  ["Translated CFG type does not match function handle type",
-                                   show (handleType h), show (handleType (cfgHandle cfg)) ]
-                  Just Refl ->
-                    do liftIO $ mapM_ handleWarning warns
-                       -- Here we rebind the function handle to use the translated CFG
-                       bindFnHandle h (UseCFG cfg (postdomInfo cfg))
-                       -- Now, make recursive call to ourself, which should invoke the
-                       -- newly-installed CFG
-                       regValue <$> (callFnVal (HandleFnVal h) =<< getOverrideArgs)
+        let s =
+              UseOverride
+              $ mkOverride' (handleName h) (handleReturnType h)
+              $ -- This inner action defines what to do when this function is called for the
+                -- first time.  We actually translate the function and install it as the
+                -- implementation for the function handle, instead of this bootstrapping code.
+                liftIO (getTranslatedCFG mtrans sym) >>= \case
+                  Nothing ->
+                    panic "registerLazyModuleFn"
+                      [ "Could not find definition for function in bootstrapping code"
+                      , show sym
+                      ]
+                  Just (_decl, AnyCFG cfg, warns) ->
+                    case testEquality (handleType (cfgHandle cfg)) (handleType h) of
+                      Nothing -> panic "registerLazyModuleFn"
+                                      ["Translated CFG type does not match function handle type",
+                                       show (handleType h), show (handleType (cfgHandle cfg)) ]
+                      Just Refl ->
+                        do liftIO $ mapM_ handleWarning warns
+                           -- Here we rebind the function handle to use the translated CFG
+                           bindFnHandle h (UseCFG cfg (postdomInfo cfg))
+                           -- Now, make recursive call to ourself, which should invoke the
+                           -- newly-installed CFG
+                           regValue <$> (callFnVal (HandleFnVal h) =<< getOverrideArgs)
 
         -- Bind the function handle to the appropriate global symbol.
-        let llvm_ctx = mtrans ^. transContext
-        let mvar = llvmMemVar llvm_ctx
-        mem <- readGlobal mvar
-        mem' <- ovrWithBackend $ \bak ->
-                  liftIO $ bindLLVMFunPtr bak decl h mem
-        writeGlobal mvar mem'
+        let llvmCtx = mtrans ^. transContext
+        bind_llvm_handle llvmCtx (L.decName decl) h s
 
 
 llvmGlobalsToCtx

crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Common.hs

@@ -33,6 +33,8 @@ module Lang.Crucible.LLVM.Intrinsics.Common
   , 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
@@ -57,7 +59,7 @@ 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 ( mkHandle' )
+import           Lang.Crucible.FunctionHandle (FnHandle, mkHandle')
 import           Lang.Crucible.Panic (panic)
 import           Lang.Crucible.Simulator (stateContext, simHandleAllocator)
 import           Lang.Crucible.Simulator.OverrideSim
@@ -294,14 +296,52 @@ register_llvm_override llvmOverride = do
        empty
   else lift (lift (do_register_llvm_override llvmctx llvmOverride))
 
--- | Low-level function to regsiter LLVM overrides.
+-- | 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 llvmCtx nm hdl impl = do
+  let mvar = llvmMemVar llvmCtx
+  bindFnHandle hdl impl
+  mem <- readGlobal mvar
+  mem' <- ovrWithBackend $ \bak -> liftIO $ bindLLVMFunPtr bak nm hdl mem
+  writeGlobal mvar 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 llvmCtx nm args ret impl = do
+  let L.Symbol strNm = nm
+  let fnm  = functionNameFromText (Text.pack strNm)
+  ctx <- use stateContext
+  let ha = simHandleAllocator ctx
+  h <- liftIO $ mkHandle' ha fnm args ret
+  bind_llvm_handle llvmCtx nm h 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'.
---
--- Creates and binds a function handle, and also binds the function to the
--- global function allocation in the LLVM memory.
 do_register_llvm_override :: forall p args ret sym arch wptr l a rtp.
   (IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym) =>
   LLVMContext arch ->
@@ -321,15 +361,7 @@ do_register_llvm_override llvmctx llvmOverride = do
   llvmDeclToFunHandleRepr' decl $ \args ret -> do
     o <- build_llvm_override fnm overrideArgs overrideRet args ret
            (\bak asgn -> llvmOverride_def llvmOverride mvar bak asgn)
-    ctx <- use stateContext
-    let ha = simHandleAllocator ctx
-    h <- liftIO $ mkHandle' ha fnm args ret
-
-    bindFnHandle h (UseOverride o)
-    mem <- readGlobal mvar
-    mem' <- ovrWithBackend $ \bak ->
-              liftIO $ bindLLVMFunPtr bak decl h mem
-    writeGlobal mvar mem'
+    bind_llvm_func llvmctx (L.decName decl) args ret (UseOverride o)
 
 -- | Create an allocation for an override and register it.
 --

crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs

@@ -725,19 +725,18 @@ doMallocSize sz bak allocType mut loc mem alignment = do
 bindLLVMFunPtr ::
   (IsSymBackend sym bak, HasPtrWidth wptr) =>
   bak ->
-  L.Declare ->
+  L.Symbol ->
   FnHandle args ret ->
   MemImpl sym ->
   IO (MemImpl sym)
-bindLLVMFunPtr bak dec h mem
-  | L.decVarArgs dec
-  , (_ Ctx.:> VectorRepr AnyRepr) <- handleArgTypes h
+bindLLVMFunPtr bak nm h mem
+  | (_ Ctx.:> VectorRepr AnyRepr) <- handleArgTypes h
 
-  = do ptr <- doResolveGlobal bak mem (L.decName dec)
+  = do ptr <- doResolveGlobal bak mem nm
        doInstallHandle bak ptr (VarargsFnHandle h) mem
 
   | otherwise
-  = do ptr <- doResolveGlobal bak mem (L.decName dec)
+  = do ptr <- doResolveGlobal bak mem nm
        doInstallHandle bak ptr (SomeFnHandle h) mem
 
 doInstallHandle