Concurrent kore-rpc server (#3704)

Implements the proposal from runtimeverification/hs-backend-booster#383 Namely: `add-module` ------------- * now returns the id of a given module, of the form `m<sha256_of_given_module>` * computes the SHA256 hash of the unparsed module string and saves the internalised module under this key * takes an optional `name-as-id: true` argument which implements the previous behaviour of `add-module` (still returns the new id), i.e. adds the module to the module map under the module name as well as the id. * if the same module is added twice with `name-as-id: true`, the second request will fail with a `Duplicate module` error * if the same module is sent twice with `name-as-id: false` or without `name-as-id`, the second request is idempotent and will succeed As discussed on the issue, the IDs and original names are not disjoint for ease of implementation. the `m` pre-pended to the hash is necessary to make the name a valid kore identifier. I have also not added the `modules` field to other methods as I'm unsure whether this should be replacing the current `module` parameter, which would be a backwards incompatible change to the API that would break a lot of our integration tests, or if it should be an additional field, @tothtamas28? --------- Co-authored-by: github-actions <[email protected]>
runtimeverification · Dec 14, 2023 · 4e9fb7a · 4e9fb7a
1 parent a584730
commit 4e9fb7a
Show file tree

Hide file tree

Showing 10 changed files with 1,553 additions and 53 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,6 +41,7 @@ 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
@@ -75,11 +75,12 @@ data SimplifyRequest = SimplifyRequest
 
 data AddModuleRequest = AddModuleRequest
     { _module :: Text
+    , nameAsId :: !(Maybe Bool)
     }
     deriving stock (Generic, Show, Eq)
     deriving
         (FromJSON, ToJSON)
-        via CustomJSON '[FieldLabelModifier '[StripPrefix "_"]] AddModuleRequest
+        via CustomJSON '[FieldLabelModifier '[CamelToKebab, StripPrefix "_"]] AddModuleRequest
 
 data GetModelRequest = GetModelRequest
     { state :: KoreJson

diff --git a/kore/src/Kore/JsonRpc.hs b/kore/src/Kore/JsonRpc.hs
@@ -9,8 +9,10 @@ module Kore.JsonRpc (
 ) where
 
 import Control.Concurrent.MVar qualified as MVar
-import Control.Monad.Except (runExceptT)
+import Control.Monad.Except (MonadError (throwError), liftEither, runExceptT, withExceptT)
 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)
@@ -23,7 +25,9 @@ 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 (..),
@@ -455,54 +459,85 @@ respond serverState moduleName runSMT =
                                                 OrPattern.toTermLike sort result
                                     , logs = allLogs
                                     }
-        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)
+        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)
         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
@@ -0,0 +1,32 @@
+# Add module with `add-module` endpoint again
+
+This test uses [a-to-f](../../resources/a-to-f/) [definition](../../resources/a-to-f/definition.kore) split into two parts:
+
+When the server starts, a `TEST` module is loaded which contains the following transitions:
+
+```
+      a
+     / \
+    V   V
+    b   c
+        |
+        V
+        d
+```
+
+Then a `NEW` module is added using the `add-module` endpoint [parameters](./params.json),
+adding the following transitions:
+
+
+```
+        d
+        |
+        V
+        e
+        |
+        V
+        f
+```
+
+Expected:
+* Module successfully added even though it has been added already, because the content is exactly the same.