Add module fix (#3721)

Fixes a corner case tested for in runtimeverification/pyk#871 where * we send module `M1` with the name `"m<hash of M2>"` and `"name-as-id": true` * we send `M2` In this case, the server should reject `M2`, but currently both requests succeed, with `M1` being overridden by `M2` --------- Co-authored-by: github-actions <github-actions@github.com>
runtimeverification · Feb 19, 2024 · d943208 · d943208
1 parent e320d4b
commit d943208
Show file tree

Hide file tree

Showing 2 changed files with 19 additions and 14 deletions.
diff --git a/kore/app/rpc/Main.hs b/kore/app/rpc/Main.hs
@@ -181,6 +181,7 @@ koreRpcServerRun GlobalMain.LocalOptions{execOptions} = do
                 ServerState
                     { serializedModules = Map.singleton mainModuleName sd
                     , loadedDefinition
+                    , receivedModules = mempty
                     }
     GlobalMain.clockSomethingIO "Executing" $
         -- wrap the call to runServer in the logger monad

diff --git a/kore/src/Kore/JsonRpc.hs b/kore/src/Kore/JsonRpc.hs
@@ -527,30 +527,27 @@ respond serverState moduleName runSMT =
                         parseKoreModule "<add-module>" _module
             st@ServerState
                 { serializedModules
+                , receivedModules
                 , 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
+                -- check if we already received a module with this name
                 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 ()
+                    case Map.lookup (coerce name) receivedModules of
+                        -- if a different module was already added, throw error
+                        Just m | _module /= m -> throwError $ backendError DuplicateModuleName name
                         _ -> pure ()
 
+                -- Check for a corner case when we send module M1 with the name "m<hash of M2>"" and name-as-id: true
+                -- followed by adding M2. Should not happen in practice...
+                case Map.lookup (coerce moduleHash) receivedModules of
+                    Just m | _module /= m -> throwError $ backendError DuplicateModuleName moduleHash
+                    _ -> pure ()
+
                 case (Map.lookup (coerce moduleHash) indexedModules, Map.lookup (coerce moduleHash) serializedModules) of
                     (Just foundIdxModule, Just foundSerModule) -> do
                         liftIO $
@@ -561,6 +558,9 @@ respond serverState moduleName runSMT =
                                         ServerState
                                             { serializedModules =
                                                 Map.insert (coerce name) foundSerModule serializedModules
+                                            , receivedModules = case Map.lookup (coerce moduleHash) receivedModules of
+                                                Just recMod -> Map.insert (coerce name) recMod receivedModules
+                                                Nothing -> receivedModules
                                             , loadedDefinition =
                                                 LoadedDefinition
                                                     { indexedModules = Map.insert (coerce name) foundIdxModule indexedModules
@@ -617,6 +617,9 @@ respond serverState moduleName runSMT =
                                 { serializedModules =
                                     serializedModules `Map.union` newSerializedModules
                                 , loadedDefinition
+                                , receivedModules =
+                                    (if nameAsId then Map.insert (coerce name) _module else id) $
+                                        Map.insert (coerce moduleHash) _module receivedModules
                                 }
 
                         pure . AddModule $ AddModuleResult (getModuleName moduleHash)
@@ -734,6 +737,7 @@ respond serverState moduleName runSMT =
 
 data ServerState = ServerState
     { serializedModules :: Map.Map ModuleName SerializedDefinition
+    , receivedModules :: Map.Map ModuleName Text
     , loadedDefinition :: LoadedDefinition
     }