Merge remote-tracking branch 'origin/master' into simplify-not-exists

runtimeverification · Feb 21, 2023 · 29f4de6 · 29f4de6
2 parents 0876515 + 50c9a8f
commit 29f4de6
Show file tree

Hide file tree

Showing 26 changed files with 628 additions and 148 deletions.
diff --git a/deps/k_release b/deps/k_release
@@ -1 +1 @@
-v5.5.75
+v5.5.99
diff --git a/design-decisions/2018-07-25 Attributes as patterns.md b/design-decisions/2018-07-25 Attributes as patterns.md
@@ -95,13 +95,15 @@ of a symbol to a list of parameters,
 the (name of the) symbol identifying the
 attribute and the list of parameters being the arguments of the attribute.
 Numbers will be encoded as string literals.
+Variables will appear as patterns with sort annotations.
 Therefore the following may be valid attributes:
 ```
 constructor{}()
 strict{}("1", "2")
 unit{}(epsilon{}())
 unit{}(epsilon{}(), zero{}())
 refersTo{}(plus{}())
+concrete{}(VarI1:SortInt{},VarI2:SortInt{})
 ```
 We will *not* check that this attributes are well-formed in the usual sense,
 e.g. we will not check whether the `plus` symbol in the example above has

diff --git a/docs/2022-07-18-JSON-RPC-Server-API.md b/docs/2022-07-18-JSON-RPC-Server-API.md
@@ -28,6 +28,7 @@ The server runs over sockets and can be interacted with by sending JSON RPC mess
     "terminal-rules": ["ruleFoo"],
     "moving-average-step-timeout": true,
     "step-timeout": 1234,
+    "module": "MODULE-NAME",
     "state": {
       "format": "KORE",
       "version": 1,
@@ -37,7 +38,7 @@ The server runs over sockets and can be interacted with by sending JSON RPC mess
 }
 ```
 
-Optional parameters: `max-depth`, `cut-point-rules`, `terminal-rules`, `moving-average-step-timeout`, `step-timeout` (timeout is in milliseconds)
+Optional parameters: `max-depth`, `cut-point-rules`, `terminal-rules`, `moving-average-step-timeout`, `step-timeout` (timeout is in milliseconds), `module` (main module name)
 
 _Note: `id` can be an int or a string and each message must have a new `id`. The response objects have the same id as the message._
 
@@ -204,11 +205,14 @@ If `"reason": "cut-point-rule"`, the `next-states` field contains the next state
   "method": "implies",
   "params": {
     "antecedent": {"format": "KORE", "version": 1, "term": {}},
-    "consequent": {"format": "KORE", "version": 1, "term": {}}
+    "consequent": {"format": "KORE", "version": 1, "term": {}},
+    "module": "MODULE-NAME"
   }
 }
 ```
 
+Optional parameters: `module` (main module name)
+
 ### Error Response:
 
 Errors in decoding the `antecedent` or `consequent` terms are reported similar as for execute.
@@ -275,6 +279,14 @@ If the implication cannot be shown to hold, `satisfiable` is false.
 
 In some cases, a unifier `condition` for the implication can still be provided, although the implication cannot be shown to be true.
 
+The endpoint implements the following specification:
+- `antecedent` is `\\bottom` (implication holds trivially) => `satisfiable = True` and `condition = \\bottom`
+- `consequent` is `\\bottom` and `antecedent` is not `\\bottom` => `satisfiable = False` and `condition = \\bottom`
+- implication holds (not trivial) => `satisfiable = True` and `condition /= \\bottom`
+- implication doesn't hold and the two terms do not unify,
+indicating that the program configuration can be rewritten further => `satisfiable = False` and `condition` is omitted
+- implication doesn't hold and the two terms unify, indicating that the configuration is stuck => `satisfiable = False` and `condition /= \\bottom`
+
 ## Simplify
 
 ### Request:
@@ -285,11 +297,14 @@ In some cases, a unifier `condition` for the implication can still be provided,
   "id": 1,
   "method": "simplify",
   "params": {
-    "state": {"format": "KORE", "version": 1, "term": {}}
+    "state": {"format": "KORE", "version": 1, "term": {}},
+    "module": "MODULE-NAME"
   }
 }
 ```
 
+Optional parameters: `module` (main module name)
+
 ### Error Response:
 
 Same as for execute
@@ -306,6 +321,37 @@ Same as for execute
 }
 ```
 
+## Add-module
+
+### Request
+
+```json
+{
+  "jsonrpc": "2.0",
+  "id": 1,
+  "method": "add-module",
+  "params": {
+    "name": "MODULE-NAME",
+    "module": "<plain text>"
+  }
+}
+```
+
+* `name` is the name of the main module.
+* `module` is module represented in KORE.
+
+### Correct Response:
+
+Responds with an empty array if successful.
+
+```json
+{
+  "jsonrpc": "2.0",
+  "id": 1,
+  "result": []
+}
+```
+
 ## Cancel
 
 ### Request:
@@ -394,6 +440,37 @@ This error wraps an error message from the internal implication check routine, i
 }
 ```
 
+## -32004 Could not parse KORE pattern
+
+This error wraps the internal error thrown when parsing the received plain text module.
+
+```json
+{
+  "jsonrpc":"2.0",
+  "id":1,
+  "error":  {
+    "data":":21:286: unexpected token TokenIdent \\"hasDomainValues\\"\\n",
+    "code":-32004,
+    "message":"Could not parse KORE pattern"
+  }
+}
+```
+## -32005 Could not find module
+
+This error wraps the internal error thrown when a module with the given name can not be found.
+
+```json
+{
+  "jsonrpc":"2.0",
+  "id":1,
+  "error":  {
+    "data":"MODULE-NAME",
+    "code":-32005,
+    "message":"Could not find module"
+  }
+}
+```
+
 ## -32032 Internal server error
 
 This error indicates an internal problem with the server implementation. Its data is not expected to be processed by a client (other than including it in a bug report).
diff --git a/kore/app/rpc/Main.hs b/kore/app/rpc/Main.hs
@@ -2,6 +2,7 @@
 
 module Main (main) where
 
+import Control.Concurrent.MVar as MVar
 import Control.Monad.Catch (
     bracket,
     handle,
@@ -11,17 +12,21 @@ import Control.Monad.Reader (
  )
 import Data.IORef (writeIORef)
 import Data.InternedText (globalInternedTextCache)
+import Data.Map.Strict as Map
 import GlobalMain qualified
+import Kore.Attribute.Symbol (StepperAttributes)
 import Kore.BugReport (
     BugReportOption,
     ExitCode,
     parseBugReportOption,
     withBugReport,
  )
-import Kore.Exec (
-    SerializedModule (..),
+import Kore.IndexedModule.MetadataTools (SmtMetadataTools)
+import Kore.Internal.TermLike (TermLike)
+import Kore.JsonRpc (
+    ServerState (..),
+    runServer,
  )
-import Kore.JsonRpc (runServer)
 import Kore.Log (
     KoreLogOptions (..),
     parseKoreLogOptions,
@@ -31,9 +36,11 @@ import Kore.Log.ErrorException (
     handleSomeException,
  )
 import Kore.Rewrite.SMT.Lemma (declareSMTLemmas)
+import Kore.Syntax (VariableName)
 import Kore.Syntax.Definition (
     ModuleName (..),
  )
+import Kore.Syntax.Sentence (SentenceAxiom)
 import Log qualified
 import Options.Applicative (
     InfoMod,
@@ -143,30 +150,24 @@ koreRpcServerRun ::
     GlobalMain.LocalOptions KoreRpcServerOptions ->
     GlobalMain.Main ExitCode
 koreRpcServerRun GlobalMain.LocalOptions{execOptions} = do
-    GlobalMain.SerializedDefinition{serializedModule, lemmas, internedTextCache} <-
+    sd@GlobalMain.SerializedDefinition{internedTextCache} <-
         GlobalMain.deserializeDefinition
             koreSolverOptions
             definitionFileName
             mainModuleName
     lift $ writeIORef globalInternedTextCache internedTextCache
 
-    let SerializedModule{metadataTools} = serializedModule
-
-    -- initialize an SMT solver with user declared lemmas
-    let setupSolver smtSolverRef = do
-            let userInit = SMT.runWithSolver $ declareSMTLemmas metadataTools lemmas
-            let solverSetup = SMT.SolverSetup{userInit, refSolverHandle = smtSolverRef, config = smtConfig}
-            SMT.initSolver solverSetup
-            return solverSetup
-
-    -- launch the SMT solver, initialize it and then pass the SolverSetup object to the RPC server
+    loadedDefinition <- GlobalMain.loadDefinitions [definitionFileName]
+    serverState <-
+        lift $
+            MVar.newMVar
+                ServerState
+                    { serializedModules = Map.singleton mainModuleName sd
+                    , loadedDefinition
+                    }
     GlobalMain.clockSomethingIO "Executing" $
-        bracket
-            (SMT.newSolver smtConfig >>= setupSolver)
-            (SMT.stopSolver . SMT.refSolverHandle)
-            $ \solverSetup -> do
-                -- wrap the call to runServer in the logger monad
-                Log.LoggerT $ ReaderT $ \loggerEnv -> runServer port solverSetup loggerEnv serializedModule
+        -- wrap the call to runServer in the logger monad
+        Log.LoggerT $ ReaderT $ \loggerEnv -> runServer port serverState mainModuleName (runSMT loggerEnv) loggerEnv
 
     pure ExitSuccess
   where
@@ -179,3 +180,23 @@ koreRpcServerRun GlobalMain.LocalOptions{execOptions} = do
             , SMT.resetInterval = resetInterval
             , SMT.prelude = prelude
             }
+    -- SMT solver with user declared lemmas
+    runSMT ::
+        forall a.
+        Log.LoggerEnv IO ->
+        SmtMetadataTools StepperAttributes ->
+        [SentenceAxiom (TermLike VariableName)] ->
+        SMT.SMT a ->
+        IO a
+    runSMT Log.LoggerEnv{logAction} metadataTools lemmas m =
+        flip Log.runLoggerT logAction $
+            bracket (SMT.newSolver smtConfig) SMT.stopSolver $ \refSolverHandle -> do
+                let userInit = SMT.runWithSolver $ declareSMTLemmas metadataTools lemmas
+                    solverSetup =
+                        SMT.SolverSetup
+                            { userInit
+                            , refSolverHandle
+                            , config = smtConfig
+                            }
+                SMT.initSolver solverSetup
+                SMT.runWithSolver m solverSetup
diff --git a/kore/kore.cabal b/kore/kore.cabal
@@ -634,6 +634,7 @@ executable kore-rpc
   hs-source-dirs: app/rpc
   build-depends: kore
   build-depends: clock >=0.8
+  build-depends: containers >=0.5
   build-depends: directory >=1.3
   build-depends: exceptions >=0.10
   build-depends: mtl >=2.2