return module ids for add-module

runtimeverification · Dec 12, 2023 · 01a5876 · 01a5876
1 parent a584730
commit 01a5876
Show file tree

Hide file tree

Showing 4 changed files with 111 additions and 51 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
@@ -37,6 +37,7 @@ data JsonRpcBackendError
     = CouldNotParsePattern
     | CouldNotVerifyPattern
     | CouldNotFindModule
+    | DuplicateModule
     | ImplicationCheckError
     | SmtSolverError
     | Aborted

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,9 @@ 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 Crypto.Hash (SHA256 (..), hashWith)
 import Data.Aeson.Types (ToJSON (..))
 import Data.Coerce (coerce)
 import Data.Conduit.Network (serverSettings)
@@ -23,7 +24,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 +458,109 @@ 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
+            LoadedDefinition{indexedModules, definedNames, kFileLocations} <-
+                liftIO $ loadedDefinition <$> MVar.readMVar serverState
+            let moduleHash = ModuleName . fromString . ('m' :) . show . hashWith SHA256 $ encodeUtf8 _module
+            liftIO $ print moduleHash
+
+            when (nameAsId && isJust (Map.lookup (coerce name) indexedModules)) $
+                throwError $
+                    backendError DuplicateModule name
+
+            (newIndexedModulesHash, newDefinedNamesHash) <-
+                withExceptT (backendError CouldNotVerifyPattern) $
+                    liftEither $
+                        verifyAndIndexDefinitionWithBase
+                            (indexedModules, definedNames)
+                            Builtin.koreVerifiers
+                            (Definition (def @Attributes) [parsedModule{moduleName = moduleHash}])
+
+            mainModuleHash <-
+                liftEither $
+                    maybe (Left $ backendError CouldNotFindModule moduleHash) Right $
+                        Map.lookup (coerce moduleHash) newIndexedModulesHash
+
+            let metadataToolsHash = MetadataTools.build mainModuleHash
+                lemmasHash = getSMTLemmas mainModuleHash
+            serializedModuleHash <-
+                liftIO
+                    . runSMT metadataToolsHash lemmasHash
+                    $ Exec.makeSerializedModule mainModuleHash
+            internedTextCacheHash <- liftIO $ readIORef globalInternedTextCache
+
+            let serializedDefinitionHash =
+                    SerializedDefinition
+                        { serializedModule = serializedModuleHash
+                        , locations = kFileLocations
+                        , internedTextCache = internedTextCacheHash
+                        , lemmas = lemmasHash
+                        }
+
+            (newIndexedModules, newDefinedNames, newSerializedModules) <-
+                if nameAsId
+                    then do
+                        (newIndexedModulesName, newDefinedNamesName) <-
+                            withExceptT (backendError CouldNotVerifyPattern) $
+                                liftEither $
+                                    verifyAndIndexDefinitionWithBase
+                                        (newIndexedModulesHash, newDefinedNamesHash)
+                                        Builtin.koreVerifiers
+                                        (Definition (def @Attributes) [parsedModule])
+
+                        mainModule <-
+                            liftEither $
+                                maybe (Left $ backendError CouldNotFindModule name) Right $
+                                    Map.lookup (coerce name) newIndexedModulesName
+
+                        let metadataTools = MetadataTools.build mainModule
+                            lemmas = getSMTLemmas mainModule
+                        serializedModule' <-
+                            liftIO
+                                . runSMT metadataTools lemmas
+                                $ Exec.makeSerializedModule mainModule
+                        internedTextCache <- liftIO $ readIORef globalInternedTextCache
+
+                        let serializedDefinition =
+                                SerializedDefinition
+                                    { serializedModule = serializedModule'
+                                    , locations = kFileLocations
+                                    , internedTextCache
+                                    , lemmas
+                                    }
+                        pure
+                            ( newIndexedModulesName
+                            , newDefinedNamesName
+                            , Map.fromList [(coerce moduleHash, serializedDefinitionHash), (coerce name, serializedDefinition)]
+                            )
+                    else
+                        pure
+                            ( newIndexedModulesHash
+                            , newDefinedNamesHash
+                            , Map.fromList [(coerce moduleHash, serializedDefinitionHash)]
+                            )
+
+            liftIO . MVar.modifyMVar_ serverState $
+                \ServerState{serializedModules} -> do
+                    let loadedDefinition =
+                            LoadedDefinition
+                                { indexedModules = newIndexedModules
+                                , definedNames = newDefinedNames
+                                , kFileLocations
+                                }
+                    pure
+                        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