Concurrent kore-rpc-booster (#427)

Fixes #383 --------- Co-authored-by: devops <[email protected]> Co-authored-by: github-actions <[email protected]> Co-authored-by: Jost Berthold <[email protected]>
runtimeverification · Jan 24, 2024 · 0f11436 · 0f11436
1 parent 889e046
commit 0f11436
Show file tree

Hide file tree

Showing 16 changed files with 100 additions and 54 deletions.
diff --git a/cabal.project b/cabal.project
@@ -20,6 +20,6 @@ source-repository-package
 source-repository-package
     type: git
     location: https://github.com/runtimeverification/haskell-backend.git
-    tag: d9fa6aeb36407193b701059a54307b6368841632
+    tag: de63565944540344cba242343500f1a61ece45c5
     --sha256: 
     subdir: kore kore-rpc-types
diff --git a/deps/haskell-backend_release b/deps/haskell-backend_release
@@ -1 +1 @@
-d9fa6aeb36407193b701059a54307b6368841632
+de63565944540344cba242343500f1a61ece45c5
diff --git a/flake.lock b/flake.lock
diff --git a/flake.nix b/flake.nix
@@ -2,7 +2,7 @@
   description = "hs-backend-booster";
 
   inputs = {
-    haskell-backend.url = "github:runtimeverification/haskell-backend/d9fa6aeb36407193b701059a54307b6368841632";
+    haskell-backend.url = "github:runtimeverification/haskell-backend/de63565944540344cba242343500f1a61ece45c5";
     stacklock2nix.follows = "haskell-backend/stacklock2nix";
     nixpkgs.follows = "haskell-backend/nixpkgs";
   };

diff --git a/library/Booster/JsonRpc.hs b/library/Booster/JsonRpc.hs
@@ -22,7 +22,8 @@ import Control.Monad.Extra (whenJust)
 import Control.Monad.IO.Class
 import Control.Monad.Logger.CallStack (LogLevel (LevelError), MonadLoggerIO)
 import Control.Monad.Logger.CallStack qualified as Log
-import Control.Monad.Trans.Except (runExcept, throwE)
+import Control.Monad.Trans.Except (catchE, except, runExcept, runExceptT, throwE, withExceptT)
+import Crypto.Hash (SHA256 (..), hashWith)
 import Data.Bifunctor (second)
 import Data.Conduit.Network (serverSettings)
 import Data.Foldable
@@ -71,8 +72,10 @@ import Booster.Syntax.Json.Internalise (
     pattern DisallowAlias,
  )
 import Booster.Syntax.ParsedKore (parseKoreModule)
-import Booster.Syntax.ParsedKore.Base
-import Booster.Syntax.ParsedKore.Internalise (DefinitionError (..), addToDefinitions)
+import Booster.Syntax.ParsedKore.Base hiding (ParsedModule)
+import Booster.Syntax.ParsedKore.Base qualified as ParsedModule (ParsedModule (..))
+import Booster.Syntax.ParsedKore.Internalise (addToDefinitions)
+import Data.Aeson (ToJSON (toJSON))
 import Data.Set qualified as Set
 import Kore.JsonRpc.Error qualified as RpcError
 import Kore.JsonRpc.Server
@@ -142,35 +145,71 @@ respond stateVar =
                                         fromIntegral (toNanoSecs (diffTimeSpec stop start)) / 1e9
                                 else Nothing
                     pure $ execResponse duration req result substitution unsupported
-        RpcTypes.AddModule req -> do
+        RpcTypes.AddModule RpcTypes.AddModuleRequest{_module, nameAsId = nameAsId'} -> runExceptT $ do
             -- block other request executions while modifying the server state
             state <- liftIO $ takeMVar stateVar
-            let abortWith err = do
+            let nameAsId = fromMaybe False nameAsId'
+                moduleHash = Text.pack $ ('m' :) . show . hashWith SHA256 $ Text.encodeUtf8 _module
+                restoreStateAndRethrow (errTy, errMsg) = do
                     liftIO (putMVar stateVar state)
-                    pure $ Left err
+                    throwE $ RpcError.backendError errTy errMsg
                 listNames :: (HasField "name" a b, HasField "getId" b Text) => [a] -> Text
                 listNames = Text.intercalate ", " . map (.name.getId)
 
-            case parseKoreModule "rpc-request" req._module of
-                Left errMsg ->
-                    abortWith $ RpcError.backendError RpcError.CouldNotParsePattern errMsg
-                Right newModule ->
-                    -- constraints on add-module imposed by LLVM simplification library:
-                    let checkModule = do
-                            unless (null newModule.sorts) $
-                                throwE . AddModuleError $
-                                    "Module introduces new sorts: " <> listNames newModule.sorts
-                            unless (null newModule.symbols) $
-                                throwE . AddModuleError $
-                                    "Module introduces new symbols: " <> listNames newModule.symbols
-                     in case runExcept (checkModule >> addToDefinitions newModule state.definitions) of
-                            Left err ->
-                                abortWith $ RpcError.backendError RpcError.CouldNotVerifyPattern err
-                            Right newDefinitions -> do
-                                liftIO $ putMVar stateVar state{definitions = newDefinitions}
-                                Log.logInfo $
-                                    "Added a new module. Now in scope: " <> Text.intercalate ", " (Map.keys newDefinitions)
-                                pure $ Right $ RpcTypes.AddModule $ RpcTypes.AddModuleResult $ getId newModule.name
+            flip catchE restoreStateAndRethrow $ do
+                newModule <-
+                    withExceptT ((RpcError.InvalidModule,) . toJSON) $
+                        except $
+                            parseKoreModule "rpc-request" _module
+
+                unless (null newModule.sorts) $
+                    throwE
+                        ( RpcError.InvalidModule
+                        , toJSON $
+                            "Module introduces new sorts: " <> listNames newModule.sorts
+                        )
+                unless (null newModule.symbols) $
+                    throwE
+                        ( RpcError.InvalidModule
+                        , toJSON $
+                            "Module introduces new symbols: " <> listNames newModule.symbols
+                        )
+
+                when nameAsId $
+                    case (Map.lookup (getId $ newModule.name) state.definitions, Map.lookup moduleHash state.definitions) of
+                        (Just{}, Nothing) ->
+                            -- another module with the same name already exists
+                            throwE (RpcError.DuplicateModuleName, toJSON $ getId $ newModule.name)
+                        (Just nmMod, Just idMod)
+                            | nmMod /= idMod ->
+                                -- this module has previously been added and different
+                                -- module with the same name also already exists
+                                throwE (RpcError.DuplicateModuleName, toJSON $ getId $ newModule.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 ()
+
+                newDefinitions <-
+                    withExceptT ((RpcError.InvalidModule,) . toJSON) $
+                        except $
+                            runExcept $
+                                addToDefinitions newModule{ParsedModule.name = Id moduleHash} state.definitions
+
+                liftIO $
+                    putMVar
+                        stateVar
+                        state
+                            { definitions =
+                                if nameAsId
+                                    then Map.insert (getId $ newModule.name) (newDefinitions Map.! moduleHash) newDefinitions
+                                    else newDefinitions
+                            }
+                Log.logInfo $
+                    "Added a new module. Now in scope: " <> Text.intercalate ", " (Map.keys newDefinitions)
+                pure $ RpcTypes.AddModule $ RpcTypes.AddModuleResult moduleHash
         RpcTypes.Simplify req -> withContext req._module $ \(def, mLlvmLibrary, mSMTOptions) -> do
             start <- liftIO $ getTime Monotonic
             let internalised =

diff --git a/library/Booster/Syntax/ParsedKore/Internalise.hs b/library/Booster/Syntax/ParsedKore/Internalise.hs
@@ -1284,7 +1284,6 @@ data DefinitionError
     | DefinitionAliasError Text AliasError
     | DefinitionAxiomError AxiomError
     | DefinitionTermOrPredicateError SourceRef TermOrPredicateError
-    | AddModuleError Text
     | ElemSymbolMalformed Def.Symbol
     | ElemSymbolNotFound Def.SymbolName
     deriving stock (Eq, Show)
@@ -1318,8 +1317,6 @@ instance Pretty DefinitionError where
             "Bad rewrite rule " <> pretty err
         DefinitionTermOrPredicateError ref (PatternExpected p) ->
             "Expected a pattern in " <> pretty ref <> " but found a predicate: " <> pretty (show p)
-        AddModuleError msg ->
-            pretty $ "Add-module error: " <> msg
         ElemSymbolMalformed sym ->
             pretty $ "Element{} symbol is malformed: " <> show sym
         ElemSymbolNotFound sym ->

diff --git a/package.yaml b/package.yaml
@@ -70,6 +70,7 @@ library:
   - conduit
   - conduit-extra
   - containers
+  - cryptonite
   - deepseq
   - deriving-aeson
   - exceptions
@@ -158,6 +159,8 @@ executables:
       - transformers
     ghc-options:
     - -rtsopts
+    - -threaded
+    - -with-rtsopts=-N
 
 tests:
   unit-tests:

diff --git a/stack.yaml b/stack.yaml
@@ -14,7 +14,7 @@ extra-deps:
   - typerep-map-0.5.0.0
   - monad-validate-1.2.0.1
   - git: https://github.com/runtimeverification/haskell-backend.git
-    commit: d9fa6aeb36407193b701059a54307b6368841632
+    commit: de63565944540344cba242343500f1a61ece45c5
     subdirs:
       - kore
       - kore-rpc-types

diff --git a/stack.yaml.lock b/stack.yaml.lock
@@ -54,29 +54,29 @@ packages:
   original:
     hackage: monad-validate-1.2.0.1
 - completed:
-    commit: d9fa6aeb36407193b701059a54307b6368841632
+    commit: de63565944540344cba242343500f1a61ece45c5
     git: https://github.com/runtimeverification/haskell-backend.git
     name: kore
     pantry-tree:
-      sha256: 8d8922cd448afd3fcb11c9e45c06b092912d63916499d4afb403e12848092c98
+      sha256: 7de5e4dd59a46fe418006113e8e963d925cf1ad0e7580016491e8093fce01079
       size: 44685
     subdir: kore
     version: 0.60.0.0
   original:
-    commit: d9fa6aeb36407193b701059a54307b6368841632
+    commit: de63565944540344cba242343500f1a61ece45c5
     git: https://github.com/runtimeverification/haskell-backend.git
     subdir: kore
 - completed:
-    commit: d9fa6aeb36407193b701059a54307b6368841632
+    commit: de63565944540344cba242343500f1a61ece45c5
     git: https://github.com/runtimeverification/haskell-backend.git
     name: kore-rpc-types
     pantry-tree:
-      sha256: c9493d99798fa850782738ab91801b66b79b64a7f931b94d21d14a7144141516
+      sha256: 2ecba424c32e6e48618caf5154afc8007ee488170d449c1f457fa099a42de2cf
       size: 476
     subdir: kore-rpc-types
     version: 0.60.0.0
   original:
-    commit: d9fa6aeb36407193b701059a54307b6368841632
+    commit: de63565944540344cba242343500f1a61ece45c5
     git: https://github.com/runtimeverification/haskell-backend.git
     subdir: kore-rpc-types
 snapshots:

diff --git a/test/rpc-integration/test-foundry-bug-report/response-004.json b/test/rpc-integration/test-foundry-bug-report/response-004.json
@@ -1,5 +1,5 @@
 {
     "jsonrpc": "2.0",
     "id": 4,
-    "result": {"module": "FOUNDRY-MAIN-DEPENDS-MODULE"}
+    "result": {"module": "m3229868fc7c7f2ac5e45a3c1adc203ac623df4ffccd6f41f293bd5c2388d6e1e"}
 }
diff --git a/test/rpc-integration/test-foundry-bug-report/response-005.json b/test/rpc-integration/test-foundry-bug-report/response-005.json
@@ -1,5 +1,5 @@
 {
     "jsonrpc": "2.0",
     "id": 5,
-    "result": {"module": "FOUNDRY-MAIN-CIRCULARITIES-MODULE"}
+    "result": {"module": "m3324c39dcb583781d17e69e2f5ec25dd27494e9573ac2064ad0a9ea6b024f2c9"}
 }
diff --git a/test/rpc-integration/test-foundry-bug-report/state-004.send b/test/rpc-integration/test-foundry-bug-report/state-004.send
@@ -1 +1 @@
-{"jsonrpc": "2.0", "id": 4, "method": "add-module", "params": {"module": "module FOUNDRY-MAIN-DEPENDS-MODULE\n    import FOUNDRY-MAIN []\nendmodule []"}}
+{"jsonrpc": "2.0", "id": 4, "method": "add-module", "params": {"module": "module FOUNDRY-MAIN-DEPENDS-MODULE\n    import FOUNDRY-MAIN []\nendmodule []", "name-as-id": true}}
diff --git a/test/rpc-integration/test-foundry-bug-report/state-005.send b/test/rpc-integration/test-foundry-bug-report/state-005.send
@@ -1 +1 @@
-{"jsonrpc": "2.0", "id": 5, "method": "add-module", "params": {"module": "module FOUNDRY-MAIN-CIRCULARITIES-MODULE\n    import FOUNDRY-MAIN []\nendmodule []"}}
+{"jsonrpc": "2.0", "id": 5, "method": "add-module", "params": {"module": "module FOUNDRY-MAIN-CIRCULARITIES-MODULE\n    import FOUNDRY-MAIN []\nendmodule []", "name-as-id": true}}
diff --git a/test/rpc-integration/test-module-addition/params-03-add-new-module.json b/test/rpc-integration/test-module-addition/params-03-add-new-module.json
@@ -0,0 +1 @@
+{ "name-as-id": true }
diff --git a/test/rpc-integration/test-module-addition/response-03-add-new-module.json b/test/rpc-integration/test-module-addition/response-03-add-new-module.json
@@ -1,5 +1,5 @@
 {
     "jsonrpc": "2.0",
     "id": 1,
-    "result": {"module": "NEW"}
+    "result": {"module": "m0c5abd9a7aa1496431ec92d8002759f382a207f64deb5247e9c89c3ec3cc5cbc"}
 }
diff --git a/tools/rpc-client/RpcClient.hs b/tools/rpc-client/RpcClient.hs
@@ -49,6 +49,7 @@ import System.Time.Extra (Seconds, sleep)
 import Booster.JsonRpc (rpcJsonConfig)
 import Booster.JsonRpc.Utils (diffJson, isIdentical, renderResult)
 import Booster.Syntax.Json qualified as Syntax
+import Data.Text.IO qualified as Text
 
 main :: IO ()
 main = do
@@ -574,19 +575,24 @@ prepareRequestData (Exec file) mbOptFile opts =
 prepareRequestData (Simpl file) mbOptFile opts =
     liftIO $ prepareOneTermRequest "simplify" file mbOptFile opts
 prepareRequestData (AddModule file) mbOptFile opts = do
-    unless (isNothing mbOptFile) $
-        logWarn_ "Add-module mode, ignoring given option file"
-    unless (null opts) $
-        logWarn_ "Raw mode, ignoring given request options"
-    moduleText <- liftIO $ readFile file
+    moduleText <- liftIO $ Text.readFile file
+    paramsFromFile <-
+        liftIO $
+            maybe
+                (pure JsonKeyMap.empty)
+                ( BS.readFile
+                    >=> either error (pure . getObject) . Json.eitherDecode @Json.Value
+                )
+                mbOptFile
+    let params = paramsFromFile <> object opts
     pure . Json.encode $
         object
             [ "jsonrpc" ~> "2.0"
             , "id" ~> "1"
             , "method" ~> "add-module"
             ]
             +: "params"
-            ~> Json.Object (object ["module" ~> moduleText])
+            ~> Json.Object (params +: "module" ~> Json.String moduleText)
 prepareRequestData (GetModel file) mbOptFile opts =
     liftIO $ prepareOneTermRequest "get-model" file mbOptFile opts
 prepareRequestData (Check _file1 _file2) _mbOptFile _opts = do
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		d9fa6aeb36407193b701059a54307b6368841632
		de63565944540344cba242343500f1a61ece45c5
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		{"jsonrpc": "2.0", "id": 4, "method": "add-module", "params": {"module": "module FOUNDRY-MAIN-DEPENDS-MODULE\n import FOUNDRY-MAIN []\nendmodule []"}}
		{"jsonrpc": "2.0", "id": 4, "method": "add-module", "params": {"module": "module FOUNDRY-MAIN-DEPENDS-MODULE\n import FOUNDRY-MAIN []\nendmodule []", "name-as-id": true}}
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		{"jsonrpc": "2.0", "id": 5, "method": "add-module", "params": {"module": "module FOUNDRY-MAIN-CIRCULARITIES-MODULE\n import FOUNDRY-MAIN []\nendmodule []"}}
		{"jsonrpc": "2.0", "id": 5, "method": "add-module", "params": {"module": "module FOUNDRY-MAIN-CIRCULARITIES-MODULE\n import FOUNDRY-MAIN []\nendmodule []", "name-as-id": true}}