diff --git a/cabal.project.freeze b/cabal.project.freeze index 2fccf97608..a451ab6bcd 100644 --- a/cabal.project.freeze +++ b/cabal.project.freeze @@ -131,7 +131,7 @@ constraints: any.Cabal ==3.6.3.0, any.json-rpc ==1.0.4, any.junit-xml ==0.1.0.2, any.kan-extensions ==5.2.5, - kore -threaded, + kore +threaded, any.lens ==5.1.1, lens -benchmark-uniplate -dump-splices +inlining -j +test-hunit +test-properties +test-templates +trustworthy, any.libyaml ==0.1.2, diff --git a/kore-rpc-types/src/Kore/JsonRpc/Server.hs b/kore-rpc-types/src/Kore/JsonRpc/Server.hs index 262f03c6e2..4fc291d963 100644 --- a/kore-rpc-types/src/Kore/JsonRpc/Server.hs +++ b/kore-rpc-types/src/Kore/JsonRpc/Server.hs @@ -14,10 +14,10 @@ module Kore.JsonRpc.Server ( JsonRpcHandler (..), ) where -import Control.Concurrent (forkIO, throwTo) +import Control.Concurrent (forkIO, newMVar, readMVar, swapMVar, throwTo) import Control.Concurrent.STM.TChan (newTChan, readTChan, writeTChan) import Control.Exception (Exception (fromException), catch, mask, throw) -import Control.Monad (forM_, forever) +import Control.Monad (forM_, forever, (>=>)) import Control.Monad.IO.Class (MonadIO (liftIO)) import Control.Monad.Logger (MonadLoggerIO) import Control.Monad.Logger qualified as Log @@ -79,11 +79,13 @@ jsonRpcServer :: (MonadLoggerIO m, MonadUnliftIO m, FromRequestCancellable q, ToJSON r) => -- | Connection settings ServerSettings -> + -- | Init session state + state -> -- | Action to perform on connecting client thread - (Request -> Respond q (Log.LoggingT IO) r) -> + (Request -> state -> Respond q (Log.LoggingT IO) (r, Maybe state)) -> [JsonRpcHandler] -> m a -jsonRpcServer serverSettings respond handlers = +jsonRpcServer serverSettings initState respond handlers = runGeneralTCPServer serverSettings $ \cl -> runJSONRPCT -- we have to ensure that the returned messages contain no newlines @@ -93,17 +95,19 @@ jsonRpcServer serverSettings respond handlers = False (appSink cl) (appSource cl) - (srv respond handlers) + (srv initState respond handlers) data JsonRpcHandler = forall e. Exception e => JsonRpcHandler (e -> Log.LoggingT IO ErrorObj) srv :: - forall m q r. + forall m q r state. (MonadLoggerIO m, FromRequestCancellable q, ToJSON r) => - (Request -> Respond q (Log.LoggingT IO) r) -> + state -> + (Request -> state -> Respond q (Log.LoggingT IO) (r, Maybe state)) -> [JsonRpcHandler] -> JSONRPCT m () -srv respond handlers = do +srv initState respond handlers = do + state <- liftIO $ newMVar initState reqQueue <- liftIO $ atomically newTChan let mainLoop tid = let loop = @@ -121,7 +125,7 @@ srv respond handlers = do liftIO $ atomically $ writeTChan reqQueue req loop in loop - spawnWorker reqQueue >>= mainLoop + spawnWorker state reqQueue >>= mainLoop where isRequest = \case Request{} -> True @@ -138,7 +142,7 @@ srv respond handlers = do cancelError = ErrorObj "Request cancelled" (-32000) Null - spawnWorker reqQueue = do + spawnWorker stateMVar reqQueue = do rpcSession <- ask logger <- Log.askLoggerIO let withLog :: Log.LoggingT IO a -> IO a @@ -148,7 +152,20 @@ srv respond handlers = do sendResponses r = flip runReaderT rpcSession $ sendBatchResponse r respondTo :: Request -> Log.LoggingT IO (Maybe Response) - respondTo req = buildResponse (respond req) req + respondTo req = do + state <- liftIO $ readMVar stateMVar + buildResponse + ( respond req state + >=> ( \case + Left err -> pure $ Left err + Right (res, Nothing) -> pure $ Right res + Right (res, Just newState) -> + do + _ <- liftIO $ swapMVar stateMVar newState + pure $ Right res + ) + ) + req cancelReq :: ErrorObj -> BatchRequest -> Log.LoggingT IO () cancelReq err = \case diff --git a/kore/app/rpc/Main.hs b/kore/app/rpc/Main.hs index 401601b0da..17008cf6a0 100644 --- a/kore/app/rpc/Main.hs +++ b/kore/app/rpc/Main.hs @@ -2,7 +2,6 @@ module Main (main) where -import Control.Concurrent.MVar as MVar import Control.Exception (AsyncException (..)) import Control.Monad.Catch ( bracket, @@ -175,18 +174,16 @@ koreRpcServerRun GlobalMain.LocalOptions{execOptions} = do lift $ writeIORef globalInternedTextCache internedTextCache loadedDefinition <- GlobalMain.loadDefinitions [definitionFileName] - serverState <- - lift $ - MVar.newMVar - ServerState - { serializedModules = Map.singleton mainModuleName sd - , loadedDefinition - } + let initServerState = + ServerState + { serializedModules = Map.singleton mainModuleName sd + , loadedDefinition + } GlobalMain.clockSomethingIO "Executing" $ -- wrap the call to runServer in the logger monad Log.LoggerT $ ReaderT $ - \loggerEnv -> runServer port serverState mainModuleName (runSMT loggerEnv) loggerEnv + \loggerEnv -> runServer port initServerState mainModuleName (runSMT loggerEnv) loggerEnv pure ExitSuccess where diff --git a/kore/src/Kore/JsonRpc.hs b/kore/src/Kore/JsonRpc.hs index 7ec1d34d67..eb1e30cc21 100644 --- a/kore/src/Kore/JsonRpc.hs +++ b/kore/src/Kore/JsonRpc.hs @@ -8,7 +8,6 @@ module Kore.JsonRpc ( module Kore.JsonRpc, ) where -import Control.Concurrent.MVar qualified as MVar import Control.Monad.Except (runExceptT) import Control.Monad.Logger (runLoggingT) import Data.Aeson.Types (ToJSON (..)) @@ -105,7 +104,7 @@ import System.Clock (Clock (Monotonic), diffTimeSpec, getTime, toNanoSecs) respond :: forall m. MonadIO m => - MVar.MVar ServerState -> + ServerState -> ModuleName -> ( forall a. SmtMetadataTools StepperAttributes -> @@ -113,7 +112,7 @@ respond :: SMT.SMT a -> IO a ) -> - Respond (API 'Req) m (API 'Res) + Respond (API 'Req) m (API 'Res, Maybe ServerState) respond serverState moduleName runSMT = \case Execute @@ -158,7 +157,7 @@ respond serverState moduleName runSMT = Just $ fromIntegral (toNanoSecs (diffTimeSpec stop start)) / 1e9 else Nothing - pure $ buildResult duration (TermLike.termLikeSort verifiedPattern) traversalResult + pure $ (,Nothing) <$> buildResult duration (TermLike.termLikeSort verifiedPattern) traversalResult where toStopLabels :: Maybe [Text] -> Maybe [Text] -> Exec.StopLabels toStopLabels cpRs tRs = @@ -376,7 +375,7 @@ respond serverState moduleName runSMT = if (fromMaybe False logTiming) then maybe (Just [timeLog]) (Just . (timeLog :)) simplLogs else simplLogs - pure $ buildResult allLogs sort result + pure $ (,Nothing) <$> buildResult allLogs sort result where verify = do antVerified <- @@ -446,8 +445,8 @@ respond serverState moduleName runSMT = then maybe (Just [timeLog]) (Just . (timeLog :)) simplLogs else simplLogs pure $ - Right $ - Simplify + Right + ( Simplify SimplifyResult { state = PatternJson.fromTermLike $ @@ -455,13 +454,15 @@ respond serverState moduleName runSMT = OrPattern.toTermLike sort result , logs = allLogs } + , Nothing + ) AddModule AddModuleRequest{_module} -> case parseKoreModule "" _module of Left err -> pure $ Left $ backendError CouldNotParsePattern err Right parsedModule@Module{moduleName = name} -> do - LoadedDefinition{indexedModules, definedNames, kFileLocations} <- - liftIO $ loadedDefinition <$> MVar.readMVar serverState - let verified = + let LoadedDefinition{indexedModules, definedNames, kFileLocations} = + loadedDefinition serverState + verified = verifyAndIndexDefinitionWithBase (indexedModules, definedNames) Builtin.koreVerifiers @@ -480,29 +481,28 @@ respond serverState moduleName runSMT = $ Exec.makeSerializedModule mainModule internedTextCache <- liftIO $ readIORef globalInternedTextCache - liftIO . MVar.modifyMVar_ serverState $ - \ServerState{serializedModules} -> do - let serializedDefinition = - SerializedDefinition - { serializedModule = serializedModule' - , locations = kFileLocations - , internedTextCache - , lemmas - } - loadedDefinition = - LoadedDefinition - { indexedModules = indexedModules' - , definedNames = definedNames' - , kFileLocations - } - pure - ServerState - { serializedModules = - Map.insert (coerce name) serializedDefinition serializedModules - , loadedDefinition - } + let ServerState{serializedModules} = serverState + serializedDefinition = + SerializedDefinition + { serializedModule = serializedModule' + , locations = kFileLocations + , internedTextCache + , lemmas + } + loadedDefinition = + LoadedDefinition + { indexedModules = indexedModules' + , definedNames = definedNames' + , kFileLocations + } + newServerState = + ServerState + { serializedModules = + Map.insert (coerce name) serializedDefinition serializedModules + , loadedDefinition + } - pure . Right . AddModule $ AddModuleResult (getModuleName name) + pure $ Right (AddModule $ AddModuleResult (getModuleName name), Just newServerState) GetModel GetModelRequest{state, _module} -> withMainModule (coerce _module) $ \serializedModule lemmas -> case verifyIn serializedModule state of @@ -525,7 +525,7 @@ respond serverState moduleName runSMT = . SMT.Evaluator.getModelFor tools $ NonEmpty.fromList preds - pure . Right . GetModel $ + pure . Right . (,Nothing) . GetModel $ case result of Left False -> GetModelResult @@ -550,7 +550,7 @@ respond serverState moduleName runSMT = where withMainModule module' act = do let mainModule = fromMaybe moduleName module' - ServerState{serializedModules} <- liftIO $ MVar.readMVar serverState + ServerState{serializedModules} = serverState case Map.lookup mainModule serializedModules of Nothing -> pure $ Left $ backendError CouldNotFindModule mainModule Just (SerializedDefinition{serializedModule, lemmas}) -> @@ -622,7 +622,7 @@ data ServerState = ServerState runServer :: Int -> - MVar.MVar ServerState -> + ServerState -> ModuleName -> ( forall a. SmtMetadataTools StepperAttributes -> @@ -632,11 +632,12 @@ runServer :: ) -> Log.LoggerEnv IO -> IO () -runServer port serverState mainModule runSMT Log.LoggerEnv{logAction} = do +runServer port initServerState mainModule runSMT Log.LoggerEnv{logAction} = do flip runLoggingT logFun $ jsonRpcServer srvSettings - ( \req parsed -> + initServerState + ( \req serverState parsed -> log (InfoJsonRpcProcessRequest (getReqId req) parsed) >> respond serverState mainModule runSMT parsed )