tweak type of CouldNotVerifyPattern to fit the booster (#3752)

runtimeverification · Mar 25, 2024 · 8f97e95 · 8f97e95
1 parent c62d2a8
commit 8f97e95
Show file tree

Hide file tree

Showing 4 changed files with 23 additions and 17 deletions.
diff --git a/docs/2022-07-18-JSON-RPC-Server-API.md b/docs/2022-07-18-JSON-RPC-Server-API.md
@@ -83,14 +83,16 @@ If the verification of the `state` pattern fails, the following error is returne
   "jsonrpc": "2.0",
   "id": 1,
   "error": {
-    "data": {
-      "context": [
-          "symbol or alias \'Lbl\'-LT-\'generatedTop\'-GT-\'\' (<unknown location>)","symbol or alias \'Lbl\'-LT-\'k\'-GT-\'\' (<unknown location>)","symbol or alias \'kseq\' (<unknown location>)","symbol or alias \'inj\' (<unknown location>)","symbol or alias \'Lbl\'UndsUndsUnds\'TESTFOO-SYNTAX\'Unds\'Stmt\'Unds\'Stmt\'Unds\'Stmt\' (<unknown location>)"
-      ],
-      "error": "Head \'Lbl\'UndsUndsUnds\'TESTFOO-SYNTAX\'Unds\'Stmt\'Unds\'Stmt\'Unds\'Stmt\' not defined."
-    },
+    "data": [
+      {
+        "context": [
+            "symbol or alias \'Lbl\'-LT-\'generatedTop\'-GT-\'\' (<unknown location>)","symbol or alias \'Lbl\'-LT-\'k\'-GT-\'\' (<unknown location>)","symbol or alias \'kseq\' (<unknown location>)","symbol or alias \'inj\' (<unknown location>)","symbol or alias \'Lbl\'UndsUndsUnds\'TESTFOO-SYNTAX\'Unds\'Stmt\'Unds\'Stmt\'Unds\'Stmt\' (<unknown location>)"
+        ],
+        "error": "Head \'Lbl\'UndsUndsUnds\'TESTFOO-SYNTAX\'Unds\'Stmt\'Unds\'Stmt\'Unds\'Stmt\' not defined."
+      }
+    ],
     "code": 2,
-    "message": "Could not verify KORE pattern"
+    "message": "Could not verify pattern"
   }
 }
 ```

diff --git a/kore-rpc-types/src/Kore/JsonRpc/Error.hs b/kore-rpc-types/src/Kore/JsonRpc/Error.hs
@@ -72,7 +72,7 @@ pattern ErrorOnly error = ErrorWithTermAndContext error Nothing Nothing
 -}
 data JsonRpcBackendError
     = CouldNotParsePattern ErrorWithTermAndContext
-    | CouldNotVerifyPattern ErrorWithTermAndContext
+    | CouldNotVerifyPattern [ErrorWithTermAndContext]
     | CouldNotFindModule Text.Text
     | ImplicationCheckError ErrorWithTermAndContext
     | SmtSolverError ErrorWithTermAndContext

diff --git a/kore/src/Kore/JsonRpc.hs b/kore/src/Kore/JsonRpc.hs
@@ -151,9 +151,10 @@ respond serverState moduleName runSMT =
                         pure $
                             Left $
                                 backendError $
-                                    CouldNotVerifyPattern $
-                                        ErrorWithContext (pack errorError) $
+                                    CouldNotVerifyPattern
+                                        [ ErrorWithContext (pack errorError) $
                                             map pack errorContext
+                                        ]
                     Right verifiedPattern -> do
                         let tracingEnabled =
                                 fromMaybe False logSuccessfulRewrites || fromMaybe False logSuccessfulSimplifications
@@ -420,9 +421,10 @@ respond serverState moduleName runSMT =
                     pure $
                         Left $
                             backendError $
-                                CouldNotVerifyPattern $
-                                    ErrorWithContext (pack errorError) $
+                                CouldNotVerifyPattern
+                                    [ ErrorWithContext (pack errorError) $
                                         map pack errorContext
+                                    ]
                 Right (antVerified, consVerified) -> do
                     let leftPatt =
                             mkRewritingPattern $ Pattern.parsePatternFromTermLike antVerified
@@ -506,9 +508,10 @@ respond serverState moduleName runSMT =
                     pure $
                         Left $
                             backendError $
-                                CouldNotVerifyPattern $
-                                    ErrorWithContext (pack errorError) $
+                                CouldNotVerifyPattern
+                                    [ ErrorWithContext (pack errorError) $
                                         map pack errorContext
+                                    ]
                 Right stateVerified -> do
                     let patt =
                             mkRewritingPattern $ Pattern.parsePatternFromTermLike stateVerified
@@ -653,9 +656,10 @@ respond serverState moduleName runSMT =
                         pure $
                             Left $
                                 backendError $
-                                    CouldNotVerifyPattern $
-                                        ErrorWithContext (pack errorError) $
+                                    CouldNotVerifyPattern
+                                        [ ErrorWithContext (pack errorError) $
                                             map pack errorContext
+                                        ]
                     Right stateVerified -> do
                         let sort = TermLike.termLikeSort stateVerified
                             patt =

diff --git a/test/rpc-server/implies/refuse-macro-and-alias/response.golden b/test/rpc-server/implies/refuse-macro-and-alias/response.golden
@@ -1 +1 @@
-{"jsonrpc":"2.0","id":1,"error":{"code":2,"data":{"context":["\\and (<unknown location>)","\\and (<unknown location>)","\\equals (<unknown location>)","symbol or alias 'Lbl'Hash'rangeAddress'LParUndsRParUnds'WORD'Unds'Bool'Unds'Int' (<unknown location>)"],"error":"A symbol cannot be an alias or a macro"},"message":"Could not verify pattern"}}
+{"jsonrpc":"2.0","id":1,"error":{"code":2,"data":[{"context":["\\and (<unknown location>)","\\and (<unknown location>)","\\equals (<unknown location>)","symbol or alias 'Lbl'Hash'rangeAddress'LParUndsRParUnds'WORD'Unds'Bool'Unds'Int' (<unknown location>)"],"error":"A symbol cannot be an alias or a macro"}],"message":"Could not verify pattern"}}