Merge remote-tracking branch 'origin/master' into release

runtimeverification · Dec 20, 2024 · ed19f22 · ed19f22
2 parents 7266e34 + 3021727
commit ed19f22
Show file tree

Hide file tree

Showing 6 changed files with 17 additions and 8 deletions.
diff --git a/booster/library/Booster/LLVM/TH.hs b/booster/library/Booster/LLVM/TH.hs
@@ -89,9 +89,9 @@ foreignImport name' ty' = do
     libHandle <- TH.newName "libHandle"
 
     pure
-        [ -- foreign import ccall "dynamic" <camel_name>Unwrap :: FunPtr <ty> -> <ty>
+        [ -- foreign import ccall unsafe "dynamic"  <camel_name>Unwrap :: FunPtr <ty> -> <ty>
           TH.ForeignD $
-            TH.ImportF TH.CCall TH.Safe "dynamic" nameUnwrap $
+            TH.ImportF TH.CCall TH.Unsafe "dynamic" nameUnwrap $
                 TH.AppT (TH.AppT TH.ArrowT $ TH.AppT (TH.ConT ''FunPtr) ty) ty
         , -- <camel_name>FunPtr :: ReaderT DL IO (FunPtr <ty>)
           TH.SigD

diff --git a/booster/tools/booster/Server.hs b/booster/tools/booster/Server.hs
@@ -334,6 +334,7 @@ main = do
                     server =
                         jsonRpcServer
                             srvSettings
+                            (isJust mLlvmLibrary) -- run with bound threads if LLVM API in use
                             ( \rawReq req ->
                                 let reqId = getReqId rawReq
                                  in runBoosterLogger $ do

diff --git a/dev-tools/booster-dev/Server.hs b/dev-tools/booster-dev/Server.hs
@@ -17,7 +17,7 @@ import Control.Monad.Trans.Reader (runReaderT)
 import Data.Conduit.Network (serverSettings)
 import Data.Map (Map)
 import Data.Map.Strict qualified as Map
-import Data.Maybe (fromMaybe, isNothing)
+import Data.Maybe (fromMaybe, isJust, isNothing)
 import Data.Text (Text, unpack)
 import Data.Text.Encoding qualified as Text
 import Options.Applicative
@@ -163,6 +163,7 @@ runServer port definitions defaultMain mLlvmLibrary rewriteOpts logFile mSMTOpti
                         }
             jsonRpcServer
                 (serverSettings port "*")
+                (isJust mLlvmLibrary) -- run in bound threads if LLVM library in use
                 ( \rawReq req ->
                     flip runReaderT (filteredBoosterContextLogger, toModifiersRep prettyPrintOptions)
                         . Booster.Log.unLoggerT

diff --git a/dev-tools/kore-rpc-dev/Server.hs b/dev-tools/kore-rpc-dev/Server.hs
@@ -240,6 +240,7 @@ main = do
                     server =
                         jsonRpcServer
                             srvSettings
+                            False -- no bound threads
                             (\rawReq -> runBoosterLogger . respond (koreRespond $ getReqId rawReq))
                             [Kore.handleDecidePredicateUnknown, handleErrorCall, handleSomeException]
                     interruptHandler _ = do

diff --git a/kore-rpc-types/src/Kore/JsonRpc/Server.hs b/kore-rpc-types/src/Kore/JsonRpc/Server.hs
@@ -14,7 +14,7 @@ module Kore.JsonRpc.Server (
     JsonRpcHandler (..),
 ) where
 
-import Control.Concurrent (forkIO, throwTo)
+import Control.Concurrent (forkIO, forkOS, throwTo)
 import Control.Concurrent.STM.TChan (newTChan, readTChan, writeTChan)
 import Control.Exception (Exception (fromException), catch, mask, throw)
 import Control.Monad (forever)
@@ -78,11 +78,14 @@ jsonRpcServer ::
     (MonadUnliftIO m, FromRequestCancellable q, ToJSON r) =>
     -- | Connection settings
     ServerSettings ->
+    -- | run workers in bound threads (required if worker below uses
+    -- foreign calls with thread-local state)
+    Bool ->
     -- | Action to perform on connecting client thread
     (Request -> Respond q IO r) ->
     [JsonRpcHandler] ->
     m a
-jsonRpcServer serverSettings respond handlers =
+jsonRpcServer serverSettings runBound respond handlers =
     runGeneralTCPServer serverSettings $ \cl ->
         Log.runNoLoggingT $
             runJSONRPCT
@@ -93,17 +96,18 @@ jsonRpcServer serverSettings respond handlers =
                 False
                 (appSink cl)
                 (appSource cl)
-                (srv respond handlers)
+                (srv runBound respond handlers)
 
 data JsonRpcHandler = forall e. Exception e => JsonRpcHandler (e -> IO ErrorObj)
 
 srv ::
     forall m q r.
     (MonadLoggerIO m, FromRequestCancellable q, ToJSON r) =>
+    Bool ->
     (Request -> Respond q IO r) ->
     [JsonRpcHandler] ->
     JSONRPCT m ()
-srv respond handlers = do
+srv runBound respond handlers = do
     reqQueue <- liftIO $ atomically newTChan
     let mainLoop tid =
             let loop =
@@ -170,7 +174,8 @@ srv respond handlers = do
                     restore (thing a) `catch` catchesHandler a
 
         liftIO $
-            forkIO $
+            -- workers should run in bound threads (to secure foreign calls) when flagged
+            (if runBound then forkOS else forkIO) $
                 forever $
                     bracketOnReqException
                         (atomically $ readTChan reqQueue)

diff --git a/kore/src/Kore/JsonRpc.hs b/kore/src/Kore/JsonRpc.hs
@@ -731,6 +731,7 @@ runServer port serverState mainModule runSMT Log.LoggerEnv{logAction} = do
     flip runLoggingT logFun $
         jsonRpcServer
             srvSettings
+            False -- no bound threads
             ( \req parsed ->
                 log (InfoJsonRpcProcessRequest (getReqId req) parsed)
                     >> respond (fromId $ getReqId req) serverState mainModule runSMT parsed