207 kore rpc json differ (#238)

Part of #207 

* LIbrary module to classify json files into the types used for
`kore-rpc-types` and compute differences between files of identical type
* Small executable to load two files and determine the differences
between them
* Some tests with exemplary json files have been added (comparing
pair-wise, with golden files for expected output)

Also in this PR:

*  Add dry-run mode to `rpc-client`
* A new switch `--dry-run` makes `rpc-client` print the request instead
of sending it
   * The option can be combined with `--output/-o` and `--prettify`

flake.nix

@@ -42,6 +42,7 @@
                 /test/parser
                 /test/internalisation
                 /test/rpc-integration
+                /test/jsonrpc-examples
                 /scripts
                 /.github
               ''

library/Booster/JsonRpc/Utils.hs

@@ -0,0 +1,202 @@
+{- |
+Copyright   : (c) Runtime Verification, 2023
+License     : BSD-3-Clause
+-}
+module Booster.JsonRpc.Utils (
+    diffJson,
+    DiffResult (..),
+    isIdentical,
+    renderResult,
+    KoreRpcJson (..),
+    decodeKoreRpc,
+    KoreRpcType (..),
+    rpcTypeOf,
+    typeString,
+) where
+
+import Control.Applicative ((<|>))
+import Data.Aeson as Json
+import Data.Aeson.Encode.Pretty (encodePretty')
+import Data.Aeson.Types (parseMaybe)
+import Data.Algorithm.Diff
+import Data.Algorithm.DiffOutput (ppDiff)
+import Data.ByteString.Lazy.Char8 qualified as BS
+import Data.Function (on)
+import Data.Maybe (fromMaybe)
+import Network.JSONRPC
+
+import Kore.JsonRpc.Types
+import Kore.Syntax.Json.Types hiding (Left, Right)
+
+diffJson :: FilePath -> FilePath -> IO DiffResult
+diffJson korefile1 korefile2 = do
+    contents1 <-
+        decodeKoreRpc <$> BS.readFile korefile1
+    contents2 <-
+        decodeKoreRpc <$> BS.readFile korefile2
+
+    pure $ case (contents1, contents2) of
+        (_, _)
+            | contents1 == contents2 ->
+                Identical $ rpcTypeOf contents1
+        (NotRpcJson lines1, NotRpcJson lines2) -> do
+            TextDiff $ getGroupedDiff lines1 lines2
+        (other1, other2)
+            | rpcTypeOf other1 /= rpcTypeOf other2 ->
+                DifferentType (rpcTypeOf other1) (rpcTypeOf other2)
+            | otherwise -> do
+                JsonDiff (rpcTypeOf other1) $ computeJsonDiff other1 other2
+  where
+    computeJsonDiff =
+        getGroupedDiff `on` (BS.lines . encodePretty' rpcJsonConfig)
+
+data DiffResult
+    = Identical KoreRpcType
+    | DifferentType KoreRpcType KoreRpcType
+    | JsonDiff KoreRpcType [Diff [BS.ByteString]]
+    | TextDiff [Diff [BS.ByteString]]
+    deriving (Eq, Show)
+
+isIdentical :: DiffResult -> Bool
+isIdentical Identical{} = True
+isIdentical _ = False
+
+renderResult :: FilePath -> FilePath -> DiffResult -> BS.ByteString
+renderResult korefile1 korefile2 = \case
+    Identical rpcType ->
+        BS.unwords
+            ["Files", file1, "and", file2, "are identical", typeString rpcType <> "s"]
+    DifferentType type1 type2 ->
+        BS.unlines
+            [ "Json data in files is of different type"
+            , "  * File " <> file1 <> ": " <> typeString type1
+            , "  * File " <> file2 <> ": " <> typeString type2
+            ]
+    JsonDiff rpcType diffs ->
+        BS.unlines
+            [ BS.unwords ["Files", file1, "and", file2, "are different", typeString rpcType <> "s"]
+            , renderDiff diffs
+            ]
+    TextDiff diffs ->
+        BS.unlines
+            [ BS.unwords ["Files", file1, "and", file2, "are different non-json files"]
+            , renderDiff diffs
+            ]
+  where
+    file1 = BS.pack korefile1
+    file2 = BS.pack korefile2
+
+decodeKoreRpc :: BS.ByteString -> KoreRpcJson
+decodeKoreRpc input =
+    fromMaybe (NotRpcJson splitInput) $
+        try [rpcRequest, rpcResponse, rpcError, koreJson, unknown]
+  where
+    try = foldl1 (<|>)
+    rpcRequest = fmap RpcRequest $ do
+        req <- Json.decode @Request input
+        parser <- parseParams req.getReqMethod
+        parseMaybe parser req.getReqParams
+    rpcResponse = fmap RpcResponse $ do
+        resp <- Json.decode @Response input
+        foldl1
+            (<|>)
+            [ Execute <$> parseMaybe (Json.parseJSON @ExecuteResult) resp.getResult
+            , Implies <$> parseMaybe (Json.parseJSON @ImpliesResult) resp.getResult
+            , Simplify <$> parseMaybe (Json.parseJSON @SimplifyResult) resp.getResult
+            , AddModule <$> parseMaybe (Json.parseJSON @()) resp.getResult
+            , GetModel <$> parseMaybe (Json.parseJSON @GetModelResult) resp.getResult
+            ]
+    rpcError =
+        Json.decode @ErrorObj input
+            >>= \case
+                ErrorObj msg code mbData ->
+                    pure $ RpcError msg code mbData
+                ErrorVal{} -> fail "arbitrary json can be an ErrorVal"
+    koreJson =
+        RpcKoreJson <$> Json.decode @KoreJson input
+    unknown =
+        RpcJson <$> Json.decode @Object input
+    -- last resort: break the bytestring into lines at json-relevant
+    -- characters (ignoring quoting)
+    splitInput = BS.splitWith (`elem` [':', ',', '{', '}']) input
+
+-- | helper type enumerating all Kore-RPC json requests and responses
+data KoreRpcJson
+    = RpcRequest (API 'Req)
+    | RpcResponse (API 'Res)
+    | RpcError String Int Value
+    | RpcKoreJson KoreJson
+    | RpcJson Object
+    | NotRpcJson [BS.ByteString]
+    deriving stock (Eq, Show)
+
+instance ToJSON KoreRpcJson where
+    toJSON = \case
+        RpcRequest req ->
+            case req of -- missing instance ToJSON (API 'Req), inlined
+                Execute r -> toJSON r
+                Implies r -> toJSON r
+                Simplify r -> toJSON r
+                AddModule r -> toJSON r
+                GetModel r -> toJSON r
+                Cancel -> toJSON ()
+        RpcResponse r -> toJSON r
+        RpcError msg code v -> toJSON (msg, code, v)
+        RpcKoreJson t -> toJSON t
+        RpcJson v -> toJSON v
+        NotRpcJson bs -> toJSON $ map BS.unpack bs
+
+-- | Information about the kind of object in 'KoreRpcJson' (without payload)
+data KoreRpcType
+    = RpcReq APIMethod
+    | RpcResp APIMethod
+    | RpcErr
+    | RpcKore
+    | RpcJs
+    | NotRpcJs
+    deriving (Eq, Ord)
+
+instance Show KoreRpcType where
+    show = \case
+        RpcReq method -> show method <> " request"
+        RpcResp method -> show method <> " response"
+        RpcErr -> "error response"
+        RpcKore -> "Kore term"
+        RpcJs -> "unknown object"
+        NotRpcJs -> "non-JSON file"
+
+typeString :: KoreRpcType -> BS.ByteString
+typeString = BS.pack . show
+
+rpcTypeOf :: KoreRpcJson -> KoreRpcType
+rpcTypeOf = \case
+    RpcRequest req -> RpcReq $ methodOf req
+    RpcResponse r -> RpcResp $ methodOf r
+    RpcError{} -> RpcErr
+    RpcKoreJson{} -> RpcKore
+    RpcJson{} -> RpcJs
+    NotRpcJson{} -> NotRpcJs
+  where
+    methodOf = \case
+        Execute _ -> ExecuteM
+        Implies _ -> ImpliesM
+        Simplify _ -> SimplifyM
+        AddModule _ -> AddModuleM
+        GetModel _ -> GetModelM
+        Cancel -> error "Cancel"
+
+-------------------------------------------------------------------
+-- pretty diff output
+-- Currently using a String-based module from the Diff package but
+-- which should be rewritten to handle Text and Char8.ByteString
+
+renderDiff :: [Diff [BS.ByteString]] -> BS.ByteString
+renderDiff = BS.pack . ppDiff . map (convert (map BS.unpack))
+
+-- Should we defined `Functor Diff`? But then again `type Diff a = PolyDiff a a`
+-- and we should define `Bifunctor PolyDiff` and assimilate the `Diff` package.
+convert :: (a -> b) -> Diff a -> Diff b
+convert f = \case
+    First a -> First $ f a
+    Second b -> Second $ f b
+    Both a b -> Both (f a) (f b)

package.yaml

@@ -70,6 +70,7 @@ library:
   - containers
   - deepseq
   - deriving-aeson
+  - Diff
   - exceptions
   - extra
   - filepath
@@ -184,6 +185,14 @@ executables:
       - unordered-containers
     ghc-options:
     - -rtsopts
+  kore-json-differ:
+    source-dirs: tools/kore-json-differ
+    main: Main.hs
+    dependencies:
+      - base
+      - bytestring
+      - containers
+      - hs-backend-booster
 
   kore-rpc-booster:
     source-dirs: tools/booster

stack.yaml.lock

@@ -40,20 +40,20 @@ packages:
   original:
     hackage: monad-validate-1.2.0.1
 - completed:
-    commit: a6230144a37ee9ebf0f6dffc849faf5ce10df380
+    commit: 3ac2c87da44ed9e8fe4ba4583fb5860a4680d821
     git: https://github.com/runtimeverification/haskell-backend.git
     name: kore
     pantry-tree:
-      sha256: c8c0f36a0c1a949317f6062ab3320fc4f831ed85f3922b455f19743da9ca360f
+      sha256: dc1263850bb4fa01ba62eabe6716ac0d6e82f5a6eea0c9d0037d711883498496
       size: 44548
     subdir: kore
     version: 0.60.0.0
   original:
-    commit: a6230144a37ee9ebf0f6dffc849faf5ce10df380
+    commit: 3ac2c87da44ed9e8fe4ba4583fb5860a4680d821
     git: https://github.com/runtimeverification/haskell-backend.git
     subdir: kore
 - completed:
-    commit: a6230144a37ee9ebf0f6dffc849faf5ce10df380
+    commit: 3ac2c87da44ed9e8fe4ba4583fb5860a4680d821
     git: https://github.com/runtimeverification/haskell-backend.git
     name: kore-rpc-types
     pantry-tree:
@@ -62,7 +62,7 @@ packages:
     subdir: kore-rpc-types
     version: 0.60.0.0
   original:
-    commit: a6230144a37ee9ebf0f6dffc849faf5ce10df380
+    commit: 3ac2c87da44ed9e8fe4ba4583fb5860a4680d821
     git: https://github.com/runtimeverification/haskell-backend.git
     subdir: kore-rpc-types
 snapshots:

test/jsonrpc-examples/README.md

@@ -0,0 +1,33 @@
+## Integration tests for JSON classification and comparison tool
+
+This directory contains input files for tests in
+`Test.Booster.JsonRpc.DiffTest`.
+
+### File Classification
+
+Files in this directory are named according to their expected
+classification by `decodeKoreJson`, with suffixes indicating the
+expected `KoreRpcType`:
+
+| Suffix               | `KoreRpcType`        |                                     |
+|----------------------|----------------------|-------------------------------------|
+| `.<method>.request`  | `RpcReq <Method-M>`  | Request with given method           |
+| `.<method>.response` | `RpcResp <Method-M>` | Response for given method           |
+| `.error.response`    | `RpcErr`             | Error response {msg, code, details} |
+| `.kore.json`         | `RpcKore`            | JSON-encoded Kore term              |
+| `.random.json`       | `RpcJs`              | Valid JSON of unknown type          |
+| `.error`             | `NotRpcJs`           | Not valid as JSON                   |
+
+The test reads and classifies the file, comparing against the expected
+type given by the suffix.
+
+### File comparisons
+
+The files in this directory are compared _pairwise_ with each
+other. The comparison results are rendered as file differences or type
+differences.
+
+The output of the comparison is compared to expected outputs stored in
+files in subdirectory `expected/`.
+The expected output of comparing `<file1>` and `<file2>` is stored in
+`<basename file1>@<basename file2`

test/jsonrpc-examples/depth-limit.execute.response

@@ -0,0 +1 @@
+../rpc-integration/test-a-to-f/response-depth-limit.json

test/jsonrpc-examples/depth-limit.spaghetti-formatted.execute.response

@@ -0,0 +1 @@
+{"jsonrpc":"2.0","id":1,"result":{"reason":"depth-bound","depth":2,"state":{"term":{"format":"KORE","version":1,"term":{"tag":"App","name":"Lbl'-LT-'generatedTop'-GT-'","sorts":[],"args":[{"tag":"App","name":"Lbl'-LT-'k'-GT-'","sorts":[],"args":[{"tag":"App","name":"kseq","sorts":[],"args":[{"tag":"App","name":"inj","sorts":[{"tag":"SortApp","name":"SortState","args":[]},{"tag":"SortApp","name":"SortKItem","args":[]}],"args":[{"tag":"DV","sort":{"tag":"SortApp","name":"SortState","args":[]},"value":"e"}]},{"tag":"App","name":"dotk","sorts":[],"args":[]}]}]},{"tag":"App","name":"Lbl'-LT-'generatedCounter'-GT-'","sorts":[],"args":[{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"0"}]}]}}}}}

test/jsonrpc-examples/expected/depth-limit.execute.response@depth-limit.spaghetti-formatted.execute.response

@@ -0,0 +1 @@
+Files test/jsonrpc-examples/depth-limit.execute.response and test/jsonrpc-examples/depth-limit.spaghetti-formatted.execute.response are identical ExecuteM responses

test/jsonrpc-examples/expected/depth-limit.execute.response@foundry-proof.implies.request

@@ -0,0 +1,3 @@
+Json data in files is of different type
+  * File test/jsonrpc-examples/depth-limit.execute.response: ExecuteM response
+  * File test/jsonrpc-examples/foundry-proof.implies.request: ImpliesM request

test/jsonrpc-examples/expected/depth-limit.execute.response@foundry-proof.simplify.request

@@ -0,0 +1,3 @@
+Json data in files is of different type
+  * File test/jsonrpc-examples/depth-limit.execute.response: ExecuteM response
+  * File test/jsonrpc-examples/foundry-proof.simplify.request: SimplifyM request

test/jsonrpc-examples/expected/depth-limit.execute.response@foundry-proof2.simplify.request

@@ -0,0 +1,3 @@
+Json data in files is of different type
+  * File test/jsonrpc-examples/depth-limit.execute.response: ExecuteM response
+  * File test/jsonrpc-examples/foundry-proof2.simplify.request: SimplifyM request

test/jsonrpc-examples/expected/depth-limit.execute.response@not-json.error

@@ -0,0 +1,3 @@
+Json data in files is of different type
+  * File test/jsonrpc-examples/depth-limit.execute.response: ExecuteM response
+  * File test/jsonrpc-examples/not-json.error: non-JSON file

test/jsonrpc-examples/expected/depth-limit.execute.response@params.random.json

@@ -0,0 +1,3 @@
+Json data in files is of different type
+  * File test/jsonrpc-examples/depth-limit.execute.response: ExecuteM response
+  * File test/jsonrpc-examples/params.random.json: unknown object

test/jsonrpc-examples/expected/depth-limit.execute.response@state-a.kore.json

@@ -0,0 +1,3 @@
+Json data in files is of different type
+  * File test/jsonrpc-examples/depth-limit.execute.response: ExecuteM response
+  * File test/jsonrpc-examples/state-a.kore.json: Kore term

test/jsonrpc-examples/expected/depth-limit.execute.response@state-a.spaghetti-formatted.kore.json

@@ -0,0 +1,3 @@
+Json data in files is of different type
+  * File test/jsonrpc-examples/depth-limit.execute.response: ExecuteM response
+  * File test/jsonrpc-examples/state-a.spaghetti-formatted.kore.json: Kore term

test/jsonrpc-examples/expected/depth-limit.execute.response@state-a.unformatted.execute.request

@@ -0,0 +1,3 @@
+Json data in files is of different type
+  * File test/jsonrpc-examples/depth-limit.execute.response: ExecuteM response
+  * File test/jsonrpc-examples/state-a.unformatted.execute.request: ExecuteM request

test/jsonrpc-examples/expected/depth-limit.execute.response@terminal.execute.response

@@ -0,0 +1,8 @@
+Files test/jsonrpc-examples/depth-limit.execute.response and test/jsonrpc-examples/terminal.execute.response are different ExecuteM responses
+2c2
+<     "reason": "depth-bound",
+---
+>     "reason": "terminal-rule",
+3a4
+>     "rule": "TEST.DE",
+

test/jsonrpc-examples/expected/depth-limit.execute.response@with-logging.simplify.response

@@ -0,0 +1,3 @@
+Json data in files is of different type
+  * File test/jsonrpc-examples/depth-limit.execute.response: ExecuteM response
+  * File test/jsonrpc-examples/with-logging.simplify.response: SimplifyM response

test/jsonrpc-examples/expected/depth-limit.spaghetti-formatted.execute.response@depth-limit.execute.response

@@ -0,0 +1 @@
+Files test/jsonrpc-examples/depth-limit.spaghetti-formatted.execute.response and test/jsonrpc-examples/depth-limit.execute.response are identical ExecuteM responses

test/jsonrpc-examples/expected/depth-limit.spaghetti-formatted.execute.response@foundry-proof.implies.request

@@ -0,0 +1,3 @@
+Json data in files is of different type
+  * File test/jsonrpc-examples/depth-limit.spaghetti-formatted.execute.response: ExecuteM response
+  * File test/jsonrpc-examples/foundry-proof.implies.request: ImpliesM request

test/jsonrpc-examples/expected/depth-limit.spaghetti-formatted.execute.response@foundry-proof.simplify.request

@@ -0,0 +1,3 @@
+Json data in files is of different type
+  * File test/jsonrpc-examples/depth-limit.spaghetti-formatted.execute.response: ExecuteM response
+  * File test/jsonrpc-examples/foundry-proof.simplify.request: SimplifyM request

test/jsonrpc-examples/expected/depth-limit.spaghetti-formatted.execute.response@foundry-proof2.simplify.request

@@ -0,0 +1,3 @@
+Json data in files is of different type
+  * File test/jsonrpc-examples/depth-limit.spaghetti-formatted.execute.response: ExecuteM response
+  * File test/jsonrpc-examples/foundry-proof2.simplify.request: SimplifyM request

test/jsonrpc-examples/expected/depth-limit.spaghetti-formatted.execute.response@not-json.error

@@ -0,0 +1,3 @@
+Json data in files is of different type
+  * File test/jsonrpc-examples/depth-limit.spaghetti-formatted.execute.response: ExecuteM response
+  * File test/jsonrpc-examples/not-json.error: non-JSON file

test/jsonrpc-examples/expected/depth-limit.spaghetti-formatted.execute.response@params.random.json

@@ -0,0 +1,3 @@
+Json data in files is of different type
+  * File test/jsonrpc-examples/depth-limit.spaghetti-formatted.execute.response: ExecuteM response
+  * File test/jsonrpc-examples/params.random.json: unknown object

test/jsonrpc-examples/expected/depth-limit.spaghetti-formatted.execute.response@state-a.kore.json

@@ -0,0 +1,3 @@
+Json data in files is of different type
+  * File test/jsonrpc-examples/depth-limit.spaghetti-formatted.execute.response: ExecuteM response
+  * File test/jsonrpc-examples/state-a.kore.json: Kore term

test/jsonrpc-examples/expected/depth-limit.spaghetti-formatted.execute.response@state-a.spaghetti-formatted.kore.json

@@ -0,0 +1,3 @@
+Json data in files is of different type
+  * File test/jsonrpc-examples/depth-limit.spaghetti-formatted.execute.response: ExecuteM response
+  * File test/jsonrpc-examples/state-a.spaghetti-formatted.kore.json: Kore term

test/jsonrpc-examples/expected/depth-limit.spaghetti-formatted.execute.response@state-a.unformatted.execute.request

@@ -0,0 +1,3 @@
+Json data in files is of different type
+  * File test/jsonrpc-examples/depth-limit.spaghetti-formatted.execute.response: ExecuteM response
+  * File test/jsonrpc-examples/state-a.unformatted.execute.request: ExecuteM request

test/jsonrpc-examples/expected/depth-limit.spaghetti-formatted.execute.response@terminal.execute.response

@@ -0,0 +1,8 @@
+Files test/jsonrpc-examples/depth-limit.spaghetti-formatted.execute.response and test/jsonrpc-examples/terminal.execute.response are different ExecuteM responses
+2c2
+<     "reason": "depth-bound",
+---
+>     "reason": "terminal-rule",
+3a4
+>     "rule": "TEST.DE",
+