Concurrent kore-rpc strikes back

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,

docs/2022-07-18-JSON-RPC-Server-API.md

@@ -469,6 +469,11 @@ Same as for execute
 
 ## Add-module
 
+* Allows extending the current rule-set of the RPC server by sending textual KORE definition of a module to the server.
+* The server computes the SHA256 hash of the unparsed module string and saves the internalised module under this key, returning this ID in the response
+* The optional `name-as-id` parameter allows the user to refer to the module by the name as well as the hashed ID.
+* 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. 
+
 ### Request
 
 ```json
@@ -477,12 +482,14 @@ Same as for execute
   "id": 1,
   "method": "add-module",
   "params": {
-    "module": "module MODULE-NAME endmodule []"
+    "module": "module MODULE-NAME endmodule []",
+    "name-as-id": true
   }
 }
 ```
 
-* `module` is a module represented in textual KORE format. The module may import modules that have been loaded or added earlier.
+* `module` is a module represented in textual KORE format. The module may import modules that have been loaded or added earlier
+* `name-as-id` is an optional argument which adds the module to the module map under the module name as well as the its ID. 
 
 ### Error Response:
 
@@ -501,6 +508,23 @@ If the textual KORE in `module` is syntactically wrong, the response will use th
 }
 ```
 
+If two dfferent modules with the same name and `name-as-id: true` are sent, the second request will fail with a `Duplicate module name` error
+
+```json
+{
+  "jsonrpc": "2.0",
+  "id": 1,
+  "error": {
+    "code": 8,
+    "message": "Duplicate module name"
+  }
+}
+```
+
+However, if the modules are sent twice with `name-as-id: false` or without `name-as-id`, the second request will succeed. 
+THe request will also succeed in case the same module is sent multiple times, irrespective of the value of `name-as-id`.
+
+
 Other errors, for instance, using an unknown sort or symbol, will be reported with the error code
 `Could not verify pattern` and a more specific error message in the `data` field.
 
@@ -513,12 +537,12 @@ Responds with the name of the added module if successful.
   "jsonrpc": "2.0",
   "id": 1,
   "result": {
-    "module": "MODULE-NAME"
+    "module": "`m<sha256_of_given_module>"
   }
 }
 ```
 
-Module `MODULE-NAME` can now be used in subsequent requests to the server by passing `"module": "MODULE-NAME"`.
+The module ID `m<sha256_of_given_module>` can now be used in subsequent requests to the server by passing `"module": "m<sha256_of_given_module>"`.
 
 ## Get-model
 
@@ -715,3 +739,11 @@ Error returned when the SMT solver crashes or is unable to discharge a goal.
 ## 7 Multiple states
 
 The two errors above indicate that the execute endpoint ended up in an erroneous/inconsistent state and the returned error message is should be included in the bug report.
+
+# 8 Invalid module
+
+The module could not be parsed or is invalid (e.g. contains new symbols)
+
+# 9 Duplicate module name
+
+A module with the same name is already loaded on the server

kore-rpc-types/src/Kore/JsonRpc/Error.hs

@@ -41,6 +41,8 @@ data JsonRpcBackendError
     | SmtSolverError
     | Aborted
     | MultipleStates
+    | InvalidModule
+    | DuplicateModuleName
     deriving stock (Enum, Show)
 
 backendError :: ToJSON a => JsonRpcBackendError -> a -> ErrorObj

kore-rpc-types/src/Kore/JsonRpc/Types.hs

@@ -76,11 +76,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

kore/src/Kore/IndexedModule/IndexedModule.hs

@@ -133,7 +133,7 @@ data IndexedModuleSyntax pat declAtts = IndexedModuleSyntax
         !(Set.Set Id)
     -- ^ set of hooked identifiers
     }
-    deriving stock (Generic, Show, Functor, Foldable, Traversable)
+    deriving stock (Generic, Show, Eq, Functor, Foldable, Traversable)
 
 -- TODO (thomas.tuegel): Consider splitting IndexedModule into separate sort,
 -- symbol, and axiom indices.
@@ -157,7 +157,7 @@ data IndexedModule pat declAtts axiomAtts = IndexedModule
     -- ^ map from builtin domain (symbol and sort) identifiers to the hooked
     -- identifiers
     }
-    deriving stock (Generic, Show, Functor, Foldable, Traversable)
+    deriving stock (Generic, Show, Eq, Functor, Foldable, Traversable)
 
 recursiveIndexedModuleSortDescriptions ::
     forall pat declAtts axiomAtts.

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 (..),
@@ -461,54 +465,107 @@ 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
+        AddModule AddModuleRequest{_module, nameAsId = nameAsId'} -> runExceptT $ do
+            let nameAsId = fromMaybe False nameAsId'
+            parsedModule@Module{moduleName = name} <-
+                withExceptT (backendError InvalidModule) $
+                    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 $
+                    case (Map.lookup (coerce name) indexedModules, Map.lookup (coerce moduleHash) indexedModules) of
+                        (Just{}, Nothing) ->
+                            -- another module with the same name already exists
+                            throwError $ backendError DuplicateModuleName name
+                        (Just nmMod, Just idMod)
+                            | nmMod /= idMod ->
+                                -- this module has previously been added and different
+                                -- module with the same name also already exists
+                                throwError $ backendError DuplicateModuleName name
+                            | otherwise ->
+                                -- this module has previously been added with name-as-id: true
+                                -- we can allow this, since the contents of the named module
+                                -- are the same
+                                pure ()
+                        _ -> pure ()
+
+                case (Map.lookup (coerce moduleHash) indexedModules, Map.lookup (coerce moduleHash) serializedModules) of
+                    (Just foundIdxModule, Just foundSerModule) -> do
+                        liftIO $
+                            MVar.putMVar serverState $
+                                if nameAsId
+                                    then -- the module already exists, but re-adding with name because name-as-id is true
+
+                                        ServerState
+                                            { serializedModules =
+                                                Map.insert (coerce name) foundSerModule serializedModules
+                                            , loadedDefinition =
+                                                LoadedDefinition
+                                                    { indexedModules = Map.insert (coerce name) foundIdxModule indexedModules
+                                                    , definedNames
+                                                    , kFileLocations
                                                     }
+                                            }
+                                    else -- the module already exists so we don't need to add it again
+                                        st
+                        pure . AddModule $ AddModuleResult (getModuleName moduleHash)
+                    _ -> do
+                        (newIndexedModules, newDefinedNames) <-
+                            withExceptT (backendError InvalidModule) $
+                                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 . Right . AddModule $ AddModuleResult (getModuleName name)
+                        pure . AddModule $ AddModuleResult (getModuleName moduleHash)
         GetModel GetModelRequest{state, _module} ->
             withMainModule (coerce _module) $ \serializedModule lemmas ->
                 case verifyIn serializedModule state of