Revert "Concurrent kore-rpc server (#3704)" (#3707)

Reverts #3704. We would like to update the `haskell-backend` version used in [hs-backend-booster](https://github.com/runtimeverification/hs-backend-booster/) in order to merge runtimeverification/hs-backend-booster#421. We cannot have #3704 (concurrent `kore-rpc`), because we will need to merge runtimeverification/hs-backend-booster#427 (concurrent `kore-rpc-booster`). We do not want to merge the concurrent `kore-rpc-booster` PR before the Holiday break, since it is a braking change for `pyk`. The reverted PR will need to be reopened. I think it is best to merge it in sync with runtimeverification/hs-backend-booster#427, preparing a relevant change to `pyk` in advance.
runtimeverification · Dec 20, 2023 · ca05f14 · ca05f14
1 parent 0f46665
commit ca05f14
Show file tree

Hide file tree

Showing 10 changed files with 53 additions and 1,553 deletions.
diff --git 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/Error.hs b/kore-rpc-types/src/Kore/JsonRpc/Error.hs
@@ -41,7 +41,6 @@ data JsonRpcBackendError
     | SmtSolverError
     | Aborted
     | MultipleStates
-    | DuplicateModule
     deriving stock (Enum, Show)
 
 backendError :: ToJSON a => JsonRpcBackendError -> a -> ErrorObj

diff --git a/kore-rpc-types/src/Kore/JsonRpc/Types.hs b/kore-rpc-types/src/Kore/JsonRpc/Types.hs
@@ -76,12 +76,11 @@ data SimplifyRequest = SimplifyRequest
 
 data AddModuleRequest = AddModuleRequest
     { _module :: Text
-    , nameAsId :: !(Maybe Bool)
     }
     deriving stock (Generic, Show, Eq)
     deriving
         (FromJSON, ToJSON)
-        via CustomJSON '[FieldLabelModifier '[CamelToKebab, StripPrefix "_"]] AddModuleRequest
+        via CustomJSON '[FieldLabelModifier '[StripPrefix "_"]] AddModuleRequest
 
 data GetModelRequest = GetModelRequest
     { state :: KoreJson

diff --git a/kore/src/Kore/JsonRpc.hs b/kore/src/Kore/JsonRpc.hs
@@ -9,10 +9,8 @@ module Kore.JsonRpc (
 ) where
 
 import Control.Concurrent.MVar qualified as MVar
-import Control.Monad.Except (MonadError (throwError), liftEither, runExceptT, withExceptT)
+import Control.Monad.Except (runExceptT)
 import Control.Monad.Logger (runLoggingT)
-import Control.Monad.Trans.Except (catchE)
-import Crypto.Hash (SHA256 (..), hashWith)
 import Data.Aeson.Types (ToJSON (..))
 import Data.Coerce (coerce)
 import Data.Conduit.Network (serverSettings)
@@ -25,9 +23,7 @@ import Data.List.NonEmpty qualified as NonEmpty
 import Data.Map.Strict qualified as Map
 import Data.Sequence as Seq (Seq, empty)
 import Data.Set qualified as Set
-import Data.String (fromString)
 import Data.Text (Text)
-import Data.Text.Encoding (encodeUtf8)
 import GlobalMain (
     LoadedDefinition (..),
     SerializedDefinition (..),
@@ -465,85 +461,54 @@ respond serverState moduleName runSMT =
                                                 OrPattern.toTermLike sort result
                                     , logs = allLogs
                                     }
-        AddModule AddModuleRequest{_module, nameAsId = nameAsId'} -> runExceptT $ do
-            let nameAsId = fromMaybe False nameAsId'
-            parsedModule@Module{moduleName = name} <-
-                withExceptT (backendError CouldNotParsePattern) $
-                    liftEither $
-                        parseKoreModule "<add-module>" _module
-            st@ServerState
-                { serializedModules
-                , loadedDefinition = LoadedDefinition{indexedModules, definedNames, kFileLocations}
-                } <-
-                liftIO $ MVar.takeMVar serverState
-            let moduleHash = ModuleName . fromString . ('m' :) . show . hashWith SHA256 $ encodeUtf8 _module
-
-            -- put the original state back if we fail at any point
-            flip catchE (\e -> liftIO (MVar.putMVar serverState st) >> throwError e) $ do
-                when
-                    ( nameAsId
-                        && isJust (Map.lookup (coerce name) indexedModules)
-                        && isNothing (Map.lookup (coerce moduleHash) indexedModules)
-                    )
-                    $
-                    -- if a module with the same name already exists, but it's contents are different to the current module, throw an error
-                    throwError
-                    $ backendError DuplicateModule name
-
-                case Map.lookup (coerce moduleHash) indexedModules of
-                    Just{} -> do
-                        -- the module already exists so we don't need to add it again
-                        liftIO $ MVar.putMVar serverState st
-                        pure . AddModule $ AddModuleResult (getModuleName moduleHash)
-                    Nothing -> do
-                        (newIndexedModules, newDefinedNames) <-
-                            withExceptT (backendError CouldNotVerifyPattern) $
-                                liftEither $
-                                    verifyAndIndexDefinitionWithBase
-                                        (indexedModules, definedNames)
-                                        Builtin.koreVerifiers
-                                        (Definition (def @Attributes) [parsedModule{moduleName = moduleHash}])
-
-                        newModule <-
-                            liftEither $
-                                maybe (Left $ backendError CouldNotFindModule moduleHash) Right $
-                                    Map.lookup (coerce moduleHash) newIndexedModules
-
-                        let metadataTools = MetadataTools.build newModule
-                            lemmas = getSMTLemmas newModule
-                        serializedModule <-
-                            liftIO
-                                . runSMT metadataTools lemmas
-                                $ Exec.makeSerializedModule newModule
-                        internedTextCacheHash <- liftIO $ readIORef globalInternedTextCache
-
-                        let serializedDefinition =
-                                SerializedDefinition
-                                    { serializedModule = serializedModule
-                                    , locations = kFileLocations
-                                    , internedTextCache = internedTextCacheHash
-                                    , lemmas = lemmas
-                                    }
-                            newSerializedModules =
-                                Map.fromList $
-                                    if nameAsId
-                                        then [(coerce moduleHash, serializedDefinition), (coerce name, serializedDefinition)]
-                                        else [(coerce moduleHash, serializedDefinition)]
-                            loadedDefinition =
-                                LoadedDefinition
-                                    { indexedModules = (if nameAsId then Map.insert (coerce name) newModule else id) newIndexedModules
-                                    , definedNames = newDefinedNames
-                                    , kFileLocations
-                                    }
-
-                        liftIO . MVar.putMVar serverState $
-                            ServerState
-                                { serializedModules =
-                                    serializedModules `Map.union` newSerializedModules
-                                , loadedDefinition
-                                }
-
-                        pure . AddModule $ AddModuleResult (getModuleName moduleHash)
+        AddModule AddModuleRequest{_module} ->
+            case parseKoreModule "<add-module>" _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 =
+                            verifyAndIndexDefinitionWithBase
+                                (indexedModules, definedNames)
+                                Builtin.koreVerifiers
+                                (Definition (def @Attributes) [parsedModule])
+                    case verified of
+                        Left err -> pure $ Left $ backendError CouldNotVerifyPattern err
+                        Right (indexedModules', definedNames') ->
+                            case Map.lookup (coerce name) indexedModules' of
+                                Nothing -> pure $ Left $ backendError CouldNotFindModule name
+                                Just mainModule -> do
+                                    let metadataTools = MetadataTools.build mainModule
+                                        lemmas = getSMTLemmas mainModule
+                                    serializedModule' <-
+                                        liftIO
+                                            . runSMT metadataTools lemmas
+                                            $ 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
+                                                    }
+
+                                    pure . Right . AddModule $ AddModuleResult (getModuleName name)
         GetModel GetModelRequest{state, _module} ->
             withMainModule (coerce _module) $ \serializedModule lemmas ->
                 case verifyIn serializedModule state of

diff --git a/test/rpc-server/add-module/add-again/README.md b/test/rpc-server/add-module/add-again/README.md