From 87354761d2e615a7f2cbc8e7d18fc6e0b67cbbb4 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Wed, 26 Jul 2023 11:00:45 +1000 Subject: [PATCH] 207 consume pyk rpc bug reports (#241) Extend `rpc-client` to run all requests from a tarball (from the directory `rpc_*` inside it) Also refactored program option data type(s) to accommodate the new run mode. --------- Co-authored-by: Georgy Lukyanov --- cabal.project.freeze | 5 + library/Booster/JsonRpc/Utils.hs | 44 +- package.yaml | 4 + .../add-module.error.response | 1 + ...rror.response@depth-limit.execute.response | 3 + ...limit.spaghetti-formatted.execute.response | 3 + ...ror.response@foundry-proof.implies.request | 3 + ...or.response@foundry-proof.simplify.request | 3 + ...r.response@foundry-proof2.simplify.request | 3 + .../add-module.error.response@not-json.error | 3 + ...d-module.error.response@params.random.json | 3 + ...dd-module.error.response@state-a.kore.json | 3 + ...onse@state-a.spaghetti-formatted.kore.json | 3 + ...sponse@state-a.unformatted.execute.request | 3 + ...e.error.response@terminal.execute.response | 3 + ...or.response@with-logging.simplify.response | 3 + ...execute.response@add-module.error.response | 3 + ...execute.response@add-module.error.response | 3 + ....implies.request@add-module.error.response | 3 + ...simplify.request@add-module.error.response | 3 + ...simplify.request@add-module.error.response | 3 + .../not-json.error@add-module.error.response | 3 + ...rams.random.json@add-module.error.response | 3 + ...tate-a.kore.json@add-module.error.response | 3 + ...matted.kore.json@add-module.error.response | 3 + ....execute.request@add-module.error.response | 3 + ...execute.response@add-module.error.response | 3 + ...implify.response@add-module.error.response | 3 + tools/kore-json-differ/Main.hs | 8 +- tools/rpc-client/RpcClient.hs | 376 ++++++++++++++---- unit-tests/Test/Booster/JsonRpc/DiffTest.hs | 2 +- 31 files changed, 402 insertions(+), 110 deletions(-) create mode 100644 test/jsonrpc-examples/add-module.error.response create mode 100644 test/jsonrpc-examples/expected/add-module.error.response@depth-limit.execute.response create mode 100644 test/jsonrpc-examples/expected/add-module.error.response@depth-limit.spaghetti-formatted.execute.response create mode 100644 test/jsonrpc-examples/expected/add-module.error.response@foundry-proof.implies.request create mode 100644 test/jsonrpc-examples/expected/add-module.error.response@foundry-proof.simplify.request create mode 100644 test/jsonrpc-examples/expected/add-module.error.response@foundry-proof2.simplify.request create mode 100644 test/jsonrpc-examples/expected/add-module.error.response@not-json.error create mode 100644 test/jsonrpc-examples/expected/add-module.error.response@params.random.json create mode 100644 test/jsonrpc-examples/expected/add-module.error.response@state-a.kore.json create mode 100644 test/jsonrpc-examples/expected/add-module.error.response@state-a.spaghetti-formatted.kore.json create mode 100644 test/jsonrpc-examples/expected/add-module.error.response@state-a.unformatted.execute.request create mode 100644 test/jsonrpc-examples/expected/add-module.error.response@terminal.execute.response create mode 100644 test/jsonrpc-examples/expected/add-module.error.response@with-logging.simplify.response create mode 100644 test/jsonrpc-examples/expected/depth-limit.execute.response@add-module.error.response create mode 100644 test/jsonrpc-examples/expected/depth-limit.spaghetti-formatted.execute.response@add-module.error.response create mode 100644 test/jsonrpc-examples/expected/foundry-proof.implies.request@add-module.error.response create mode 100644 test/jsonrpc-examples/expected/foundry-proof.simplify.request@add-module.error.response create mode 100644 test/jsonrpc-examples/expected/foundry-proof2.simplify.request@add-module.error.response create mode 100644 test/jsonrpc-examples/expected/not-json.error@add-module.error.response create mode 100644 test/jsonrpc-examples/expected/params.random.json@add-module.error.response create mode 100644 test/jsonrpc-examples/expected/state-a.kore.json@add-module.error.response create mode 100644 test/jsonrpc-examples/expected/state-a.spaghetti-formatted.kore.json@add-module.error.response create mode 100644 test/jsonrpc-examples/expected/state-a.unformatted.execute.request@add-module.error.response create mode 100644 test/jsonrpc-examples/expected/terminal.execute.response@add-module.error.response create mode 100644 test/jsonrpc-examples/expected/with-logging.simplify.response@add-module.error.response diff --git a/cabal.project.freeze b/cabal.project.freeze index e3b962698..7bb359753 100644 --- a/cabal.project.freeze +++ b/cabal.project.freeze @@ -1,5 +1,6 @@ active-repositories: hackage.haskell.org:merge constraints: any.Cabal ==3.6.3.0, + any.Diff ==0.4.1, any.Glob ==0.10.2, any.HUnit ==1.6.2.0, any.OneTuple ==0.3.1, @@ -45,6 +46,10 @@ constraints: any.Cabal ==3.6.3.0, byteslice +avoid-rawmemchr, any.bytesmith ==0.3.9.1, any.bytestring ==0.11.4.0, + any.bz2 ==1.0.1.0, + bz2 -cross +with-bzlib, + any.c2hs ==0.28.8, + c2hs +base3 -regression, any.cabal-doctest ==1.0.9, any.call-stack ==0.4.0, any.case-insensitive ==1.2.1.0, diff --git a/library/Booster/JsonRpc/Utils.hs b/library/Booster/JsonRpc/Utils.hs index fe90488f4..e8bfe3f0b 100644 --- a/library/Booster/JsonRpc/Utils.hs +++ b/library/Booster/JsonRpc/Utils.hs @@ -28,15 +28,10 @@ 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 - (_, _) +diffJson :: BS.ByteString -> BS.ByteString -> DiffResult +diffJson file1 file2 = + case (decodeKoreRpc file1, decodeKoreRpc file2) of + (contents1, contents2) | contents1 == contents2 -> Identical $ rpcTypeOf contents1 (NotRpcJson lines1, NotRpcJson lines2) -> do @@ -96,22 +91,25 @@ decodeKoreRpc input = req <- Json.decode @Request input parser <- parseParams req.getReqMethod parseMaybe parser req.getReqParams - rpcResponse = fmap RpcResponse $ do + 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 - ] + case resp of + ResponseError{} -> extractError resp.getError + OrphanError{} -> extractError resp.getError + Response{} -> + fmap RpcResponse . try $ + [ 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" + Json.decode @ErrorObj input >>= extractError + extractError = \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 = diff --git a/package.yaml b/package.yaml index 9052580f6..96db4a415 100644 --- a/package.yaml +++ b/package.yaml @@ -125,16 +125,20 @@ executables: - aeson-pretty - base - bytestring + - bz2 - clock - directory - extra + - filepath - hs-backend-booster - network - network-run - optparse-applicative - process + - tar - text - vector + - zlib ghc-options: - -rtsopts parsetest: diff --git a/test/jsonrpc-examples/add-module.error.response b/test/jsonrpc-examples/add-module.error.response new file mode 100644 index 000000000..07f017f54 --- /dev/null +++ b/test/jsonrpc-examples/add-module.error.response @@ -0,0 +1 @@ +{"jsonrpc":"2.0","id":4,"error":{"code":2,"data":{"context":null,"error":"FOUNDRY-MAIN-DEPENDS-MODULE: Duplicate module"},"message":"Could not verify pattern"}} diff --git a/test/jsonrpc-examples/expected/add-module.error.response@depth-limit.execute.response b/test/jsonrpc-examples/expected/add-module.error.response@depth-limit.execute.response new file mode 100644 index 000000000..18f798cea --- /dev/null +++ b/test/jsonrpc-examples/expected/add-module.error.response@depth-limit.execute.response @@ -0,0 +1,3 @@ +Json data in files is of different type + * File test/jsonrpc-examples/add-module.error.response: error response + * File test/jsonrpc-examples/depth-limit.execute.response: ExecuteM response diff --git a/test/jsonrpc-examples/expected/add-module.error.response@depth-limit.spaghetti-formatted.execute.response b/test/jsonrpc-examples/expected/add-module.error.response@depth-limit.spaghetti-formatted.execute.response new file mode 100644 index 000000000..6d5a2ce70 --- /dev/null +++ b/test/jsonrpc-examples/expected/add-module.error.response@depth-limit.spaghetti-formatted.execute.response @@ -0,0 +1,3 @@ +Json data in files is of different type + * File test/jsonrpc-examples/add-module.error.response: error response + * File test/jsonrpc-examples/depth-limit.spaghetti-formatted.execute.response: ExecuteM response diff --git a/test/jsonrpc-examples/expected/add-module.error.response@foundry-proof.implies.request b/test/jsonrpc-examples/expected/add-module.error.response@foundry-proof.implies.request new file mode 100644 index 000000000..7f0e536b9 --- /dev/null +++ b/test/jsonrpc-examples/expected/add-module.error.response@foundry-proof.implies.request @@ -0,0 +1,3 @@ +Json data in files is of different type + * File test/jsonrpc-examples/add-module.error.response: error response + * File test/jsonrpc-examples/foundry-proof.implies.request: ImpliesM request diff --git a/test/jsonrpc-examples/expected/add-module.error.response@foundry-proof.simplify.request b/test/jsonrpc-examples/expected/add-module.error.response@foundry-proof.simplify.request new file mode 100644 index 000000000..571c0deb6 --- /dev/null +++ b/test/jsonrpc-examples/expected/add-module.error.response@foundry-proof.simplify.request @@ -0,0 +1,3 @@ +Json data in files is of different type + * File test/jsonrpc-examples/add-module.error.response: error response + * File test/jsonrpc-examples/foundry-proof.simplify.request: SimplifyM request diff --git a/test/jsonrpc-examples/expected/add-module.error.response@foundry-proof2.simplify.request b/test/jsonrpc-examples/expected/add-module.error.response@foundry-proof2.simplify.request new file mode 100644 index 000000000..efdd79434 --- /dev/null +++ b/test/jsonrpc-examples/expected/add-module.error.response@foundry-proof2.simplify.request @@ -0,0 +1,3 @@ +Json data in files is of different type + * File test/jsonrpc-examples/add-module.error.response: error response + * File test/jsonrpc-examples/foundry-proof2.simplify.request: SimplifyM request diff --git a/test/jsonrpc-examples/expected/add-module.error.response@not-json.error b/test/jsonrpc-examples/expected/add-module.error.response@not-json.error new file mode 100644 index 000000000..669b9fe95 --- /dev/null +++ b/test/jsonrpc-examples/expected/add-module.error.response@not-json.error @@ -0,0 +1,3 @@ +Json data in files is of different type + * File test/jsonrpc-examples/add-module.error.response: error response + * File test/jsonrpc-examples/not-json.error: non-JSON file diff --git a/test/jsonrpc-examples/expected/add-module.error.response@params.random.json b/test/jsonrpc-examples/expected/add-module.error.response@params.random.json new file mode 100644 index 000000000..d3adc5c72 --- /dev/null +++ b/test/jsonrpc-examples/expected/add-module.error.response@params.random.json @@ -0,0 +1,3 @@ +Json data in files is of different type + * File test/jsonrpc-examples/add-module.error.response: error response + * File test/jsonrpc-examples/params.random.json: unknown object diff --git a/test/jsonrpc-examples/expected/add-module.error.response@state-a.kore.json b/test/jsonrpc-examples/expected/add-module.error.response@state-a.kore.json new file mode 100644 index 000000000..48651fac2 --- /dev/null +++ b/test/jsonrpc-examples/expected/add-module.error.response@state-a.kore.json @@ -0,0 +1,3 @@ +Json data in files is of different type + * File test/jsonrpc-examples/add-module.error.response: error response + * File test/jsonrpc-examples/state-a.kore.json: Kore term diff --git a/test/jsonrpc-examples/expected/add-module.error.response@state-a.spaghetti-formatted.kore.json b/test/jsonrpc-examples/expected/add-module.error.response@state-a.spaghetti-formatted.kore.json new file mode 100644 index 000000000..d72fc9b2e --- /dev/null +++ b/test/jsonrpc-examples/expected/add-module.error.response@state-a.spaghetti-formatted.kore.json @@ -0,0 +1,3 @@ +Json data in files is of different type + * File test/jsonrpc-examples/add-module.error.response: error response + * File test/jsonrpc-examples/state-a.spaghetti-formatted.kore.json: Kore term diff --git a/test/jsonrpc-examples/expected/add-module.error.response@state-a.unformatted.execute.request b/test/jsonrpc-examples/expected/add-module.error.response@state-a.unformatted.execute.request new file mode 100644 index 000000000..fb372946a --- /dev/null +++ b/test/jsonrpc-examples/expected/add-module.error.response@state-a.unformatted.execute.request @@ -0,0 +1,3 @@ +Json data in files is of different type + * File test/jsonrpc-examples/add-module.error.response: error response + * File test/jsonrpc-examples/state-a.unformatted.execute.request: ExecuteM request diff --git a/test/jsonrpc-examples/expected/add-module.error.response@terminal.execute.response b/test/jsonrpc-examples/expected/add-module.error.response@terminal.execute.response new file mode 100644 index 000000000..b04e6c8b8 --- /dev/null +++ b/test/jsonrpc-examples/expected/add-module.error.response@terminal.execute.response @@ -0,0 +1,3 @@ +Json data in files is of different type + * File test/jsonrpc-examples/add-module.error.response: error response + * File test/jsonrpc-examples/terminal.execute.response: ExecuteM response diff --git a/test/jsonrpc-examples/expected/add-module.error.response@with-logging.simplify.response b/test/jsonrpc-examples/expected/add-module.error.response@with-logging.simplify.response new file mode 100644 index 000000000..a81d6b28e --- /dev/null +++ b/test/jsonrpc-examples/expected/add-module.error.response@with-logging.simplify.response @@ -0,0 +1,3 @@ +Json data in files is of different type + * File test/jsonrpc-examples/add-module.error.response: error response + * File test/jsonrpc-examples/with-logging.simplify.response: SimplifyM response diff --git a/test/jsonrpc-examples/expected/depth-limit.execute.response@add-module.error.response b/test/jsonrpc-examples/expected/depth-limit.execute.response@add-module.error.response new file mode 100644 index 000000000..5b075c563 --- /dev/null +++ b/test/jsonrpc-examples/expected/depth-limit.execute.response@add-module.error.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/add-module.error.response: error response diff --git a/test/jsonrpc-examples/expected/depth-limit.spaghetti-formatted.execute.response@add-module.error.response b/test/jsonrpc-examples/expected/depth-limit.spaghetti-formatted.execute.response@add-module.error.response new file mode 100644 index 000000000..2ccbafb9c --- /dev/null +++ b/test/jsonrpc-examples/expected/depth-limit.spaghetti-formatted.execute.response@add-module.error.response @@ -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/add-module.error.response: error response diff --git a/test/jsonrpc-examples/expected/foundry-proof.implies.request@add-module.error.response b/test/jsonrpc-examples/expected/foundry-proof.implies.request@add-module.error.response new file mode 100644 index 000000000..c78231602 --- /dev/null +++ b/test/jsonrpc-examples/expected/foundry-proof.implies.request@add-module.error.response @@ -0,0 +1,3 @@ +Json data in files is of different type + * File test/jsonrpc-examples/foundry-proof.implies.request: ImpliesM request + * File test/jsonrpc-examples/add-module.error.response: error response diff --git a/test/jsonrpc-examples/expected/foundry-proof.simplify.request@add-module.error.response b/test/jsonrpc-examples/expected/foundry-proof.simplify.request@add-module.error.response new file mode 100644 index 000000000..2ec697a5a --- /dev/null +++ b/test/jsonrpc-examples/expected/foundry-proof.simplify.request@add-module.error.response @@ -0,0 +1,3 @@ +Json data in files is of different type + * File test/jsonrpc-examples/foundry-proof.simplify.request: SimplifyM request + * File test/jsonrpc-examples/add-module.error.response: error response diff --git a/test/jsonrpc-examples/expected/foundry-proof2.simplify.request@add-module.error.response b/test/jsonrpc-examples/expected/foundry-proof2.simplify.request@add-module.error.response new file mode 100644 index 000000000..813de868a --- /dev/null +++ b/test/jsonrpc-examples/expected/foundry-proof2.simplify.request@add-module.error.response @@ -0,0 +1,3 @@ +Json data in files is of different type + * File test/jsonrpc-examples/foundry-proof2.simplify.request: SimplifyM request + * File test/jsonrpc-examples/add-module.error.response: error response diff --git a/test/jsonrpc-examples/expected/not-json.error@add-module.error.response b/test/jsonrpc-examples/expected/not-json.error@add-module.error.response new file mode 100644 index 000000000..61d877d30 --- /dev/null +++ b/test/jsonrpc-examples/expected/not-json.error@add-module.error.response @@ -0,0 +1,3 @@ +Json data in files is of different type + * File test/jsonrpc-examples/not-json.error: non-JSON file + * File test/jsonrpc-examples/add-module.error.response: error response diff --git a/test/jsonrpc-examples/expected/params.random.json@add-module.error.response b/test/jsonrpc-examples/expected/params.random.json@add-module.error.response new file mode 100644 index 000000000..c495837a8 --- /dev/null +++ b/test/jsonrpc-examples/expected/params.random.json@add-module.error.response @@ -0,0 +1,3 @@ +Json data in files is of different type + * File test/jsonrpc-examples/params.random.json: unknown object + * File test/jsonrpc-examples/add-module.error.response: error response diff --git a/test/jsonrpc-examples/expected/state-a.kore.json@add-module.error.response b/test/jsonrpc-examples/expected/state-a.kore.json@add-module.error.response new file mode 100644 index 000000000..c793ffc1c --- /dev/null +++ b/test/jsonrpc-examples/expected/state-a.kore.json@add-module.error.response @@ -0,0 +1,3 @@ +Json data in files is of different type + * File test/jsonrpc-examples/state-a.kore.json: Kore term + * File test/jsonrpc-examples/add-module.error.response: error response diff --git a/test/jsonrpc-examples/expected/state-a.spaghetti-formatted.kore.json@add-module.error.response b/test/jsonrpc-examples/expected/state-a.spaghetti-formatted.kore.json@add-module.error.response new file mode 100644 index 000000000..e4616434f --- /dev/null +++ b/test/jsonrpc-examples/expected/state-a.spaghetti-formatted.kore.json@add-module.error.response @@ -0,0 +1,3 @@ +Json data in files is of different type + * File test/jsonrpc-examples/state-a.spaghetti-formatted.kore.json: Kore term + * File test/jsonrpc-examples/add-module.error.response: error response diff --git a/test/jsonrpc-examples/expected/state-a.unformatted.execute.request@add-module.error.response b/test/jsonrpc-examples/expected/state-a.unformatted.execute.request@add-module.error.response new file mode 100644 index 000000000..6cfa6a413 --- /dev/null +++ b/test/jsonrpc-examples/expected/state-a.unformatted.execute.request@add-module.error.response @@ -0,0 +1,3 @@ +Json data in files is of different type + * File test/jsonrpc-examples/state-a.unformatted.execute.request: ExecuteM request + * File test/jsonrpc-examples/add-module.error.response: error response diff --git a/test/jsonrpc-examples/expected/terminal.execute.response@add-module.error.response b/test/jsonrpc-examples/expected/terminal.execute.response@add-module.error.response new file mode 100644 index 000000000..0f6af828d --- /dev/null +++ b/test/jsonrpc-examples/expected/terminal.execute.response@add-module.error.response @@ -0,0 +1,3 @@ +Json data in files is of different type + * File test/jsonrpc-examples/terminal.execute.response: ExecuteM response + * File test/jsonrpc-examples/add-module.error.response: error response diff --git a/test/jsonrpc-examples/expected/with-logging.simplify.response@add-module.error.response b/test/jsonrpc-examples/expected/with-logging.simplify.response@add-module.error.response new file mode 100644 index 000000000..6b006c18e --- /dev/null +++ b/test/jsonrpc-examples/expected/with-logging.simplify.response@add-module.error.response @@ -0,0 +1,3 @@ +Json data in files is of different type + * File test/jsonrpc-examples/with-logging.simplify.response: SimplifyM response + * File test/jsonrpc-examples/add-module.error.response: error response diff --git a/tools/kore-json-differ/Main.hs b/tools/kore-json-differ/Main.hs index df3b8ddaf..4d050fbac 100644 --- a/tools/kore-json-differ/Main.hs +++ b/tools/kore-json-differ/Main.hs @@ -31,9 +31,11 @@ main = do _ | "--help" `elem` args -> putStrLn usage - [x, y] -> do - result <- diffJson x y - BS.putStrLn $ renderResult x y result + [file1, file2] -> do + x <- BS.readFile file1 + y <- BS.readFile file2 + let result = diffJson x y + BS.putStrLn $ renderResult file1 file2 result exitWith $ if isIdentical result then ExitSuccess else ExitFailure 1 _other -> do putStrLn $ "ERROR: program requires exactly two arguments.\n\n" <> usage diff --git a/tools/rpc-client/RpcClient.hs b/tools/rpc-client/RpcClient.hs index d5af90b12..0251ca5fb 100644 --- a/tools/rpc-client/RpcClient.hs +++ b/tools/rpc-client/RpcClient.hs @@ -14,6 +14,11 @@ module RpcClient ( main, ) where +import Codec.Archive.Tar qualified as Tar +import Codec.Archive.Tar.Check qualified as Tar +import Codec.Compression.BZip qualified as BZ2 +import Codec.Compression.GZip qualified as GZip +import Control.Exception import Control.Monad import Data.Aeson qualified as Json import Data.Aeson.Encode.Pretty qualified as Json @@ -22,10 +27,12 @@ import Data.Aeson.KeyMap qualified as JsonKeyMap import Data.Bifunctor import Data.ByteString.Lazy.Char8 qualified as BS import Data.Char (isDigit) +import Data.Int (Int64) import Data.List.Extra -import Data.Maybe (isNothing) +import Data.Maybe (isNothing, mapMaybe) import Data.Text qualified as Text import Data.Vector as Array (fromList) +import GHC.IO.Exception (IOErrorType (..), IOException (..)) import Network.Run.TCP import Network.Socket import Network.Socket.ByteString.Lazy @@ -33,70 +40,112 @@ import Options.Applicative import System.Clock import System.Directory import System.Exit +import System.FilePath import System.IO +import System.IO.Extra import System.Process import Booster.JsonRpc (rpcJsonConfig) +import Booster.JsonRpc.Utils (diffJson, isIdentical, renderResult) import Booster.Syntax.Json qualified as Syntax import Debug.Trace main :: IO () main = do - Options{host, port, mode, optionFile, options, postProcessing, prettify, time, dryRun} <- - execParser parseOptions - request <- - trace "[Info] Preparing request data" $ - prepareRequestData mode optionFile options - when dryRun $ do - traceM "[Info] Dry-run mode, just showing request instead of sending" - let write - | Just (Expect True file) <- postProcessing = - trace ("[Info] Writing request to file " <> file) (BS.writeFile file) - | otherwise = BS.putStrLn - reformat = Json.encodePretty' rpcJsonConfig . Json.decode @Json.Value - write $ if not prettify then request else reformat request - exitSuccess - runTCPClient host (show port) $ \s -> do - start <- getTime Monotonic - trace "[Info] Sending request..." $ - sendAll s request - response <- readResponse s 8192 - end <- getTime Monotonic - let modeFile = getModeFile mode - timeStr = timeSpecs start end - hPutStrLn stderr $ "[info] Round trip time for request '" <> modeFile <> "' was " <> timeStr - when time $ do - hPutStrLn stderr $ "[Info] Saving timing for " <> modeFile - writeFile (modeFile <> ".time") timeStr - - trace "[Info] Response received." $ - postProcess prettify postProcessing response - shutdown s ShutdownReceive + Options{common, runOptions} <- execParser parseOptions + case runOptions of + RunTarball tarFile keepGoing -> + runTarball common.host common.port tarFile keepGoing + RunSingle mode optionFile options processingOptions -> do + let ProcessingOptions{postProcessing, prettify, time, dryRun} = processingOptions + + request <- + trace "[Info] Preparing request data" $ + prepareRequestData mode optionFile options + if dryRun + then do + traceM "[Info] Dry-run mode, just showing request instead of sending" + let write + | Just (Expect True file) <- postProcessing = + trace ("[Info] Writing request to file " <> file) (BS.writeFile file) + | otherwise = BS.putStrLn + reformat = Json.encodePretty' rpcJsonConfig . Json.decode @Json.Value + write $ if not prettify then request else reformat request + exitSuccess + else runTCPClient common.host (show common.port) $ \s -> do + makeRequest + time + (getModeFile mode) + s + 8192 + request + (postProcess prettify postProcessing) + shutdown s ShutdownReceive + +makeRequest :: + Bool -> String -> Socket -> Int64 -> BS.ByteString -> (BS.ByteString -> IO a) -> IO a +makeRequest time name s bufSize request handleResponse = do + start <- getTime Monotonic + trace ("[Info] Sending request " <> name <> "...") $ + sendAll s request + response <- readResponse + end <- getTime Monotonic + let timeStr = timeSpecs start end + traceM $ "[Info] Round trip time for request '" <> name <> "' was " <> timeStr + when time $ + trace ("[Info] Saving timing for " <> name) $ + writeFile (name <> ".time") timeStr + + trace "[Info] Response received." $ + handleResponse response where - readResponse s bufSize = do + readResponse :: IO BS.ByteString + readResponse = do part <- recv s bufSize if BS.length part < bufSize then pure part else do - more <- readResponse s bufSize + more <- readResponse pure $ part <> more data Options = Options + { common :: CommonOptions + , runOptions :: RunOptions + } + deriving stock (Show) + +data CommonOptions = CommonOptions { host :: String , port :: Int - , mode :: Mode -- what to do - , optionFile :: Maybe FilePath -- file with options (different for each endpoint - , options :: [(String, String)] -- verbatim options (name, value) to add to json - , postProcessing :: Maybe PostProcessing + } + deriving stock (Show) + +data RunOptions + = -- | run a single request + RunSingle + Mode -- what kind of request + (Maybe FilePath) -- json file with options + [(String, String)] -- verbatim options (name, value) to add to json + ProcessingOptions + | -- | run all requests contained in a tarball (using some conventions) + RunTarball + FilePath -- tar file + Bool -- do not stop on first diff if set to true + deriving stock (Show) + +data ProcessingOptions = ProcessingOptions + { postProcessing :: Maybe PostProcessing , prettify :: Bool , time :: Bool , dryRun :: Bool } deriving stock (Show) -{- | Defines what to do. Either one of the endpoints (with state in a - file), or raw data (entire input in a file). +{- | Defines details for a single requests. Either assemble a request + from the state in a file and given options in a file or on the + command line, or raw data (entire input in a file) without additional + options. -} data Mode = Exec FilePath @@ -126,6 +175,27 @@ data PostProcessing = Expect } deriving stock (Show) +parseCommonOptions :: Parser CommonOptions +parseCommonOptions = + CommonOptions + <$> strOption + ( long "host" + <> short 'h' + <> metavar "HOST" + <> value "localhost" + <> help "server host to connect to" + <> showDefault + ) + <*> option + auto + ( long "port" + <> short 'p' + <> metavar "PORT" + <> value 31337 + <> help "server port to connect to" + <> showDefault + ) + parseOptions :: ParserInfo Options parseOptions = info @@ -136,46 +206,18 @@ parseOptions = where parseOptions' = Options - <$> hostOpt - <*> portOpt + <$> parseCommonOptions <*> parseMode - <*> paramFileOpt - <*> many paramOpt - <*> optional parsePostProcessing - <*> prettifyOpt - <*> timeOpt - <*> dryRunOpt - hostOpt = - strOption $ - long "host" - <> short 'h' - <> metavar "HOST" - <> value "localhost" - <> help "server host to connect to" - <> showDefault - portOpt = - option auto $ - long "port" - <> short 'p' - <> metavar "PORT" - <> value 31337 - <> help "server port to connect to" - <> showDefault - paramFileOpt = - optional $ - strOption $ - long "param-file" - <> metavar "PARAMFILE" - <> help "file with parameters (json object), optional" - paramOpt = - option readPair $ - short 'O' - <> metavar "NAME=VALUE" - <> help "parameters to use (name=value)" - readPair = - maybeReader $ \s -> case split (== '=') s of [k, v] -> Just (k, v); _ -> Nothing - flagOpt name desc = flag False True $ long name <> help desc +parseProcessingOptions :: Parser ProcessingOptions +parseProcessingOptions = + ProcessingOptions + <$> optional parsePostProcessing + <*> prettifyOpt + <*> timeOpt + <*> dryRunOpt + where + flagOpt name desc = switch $ long name <> help desc prettifyOpt = flagOpt "prettify" "format JSON before printing" timeOpt = flagOpt "time" "record the timing information between sending a request and receiving a response" dryRunOpt = flagOpt "dry-run" "Do not send anything, just output the request" @@ -202,38 +244,206 @@ parsePostProcessing = ) ) -parseMode :: Parser Mode +parseMode :: Parser RunOptions parseMode = subparser ( command "send" - ( info (SendRaw <$> strArgument (metavar "FILENAME")) (progDesc "send the raw file contents directly") + ( info + ( RunSingle + <$> (SendRaw <$> strArgument (metavar "FILENAME")) + <*> pure Nothing -- no param file + <*> pure [] -- no params + <*> parseProcessingOptions + <**> helper + ) + (progDesc "send the raw file contents directly") ) <> command "execute" ( info - (Exec <$> strArgument (metavar "FILENAME")) + ( RunSingle + <$> (Exec <$> strArgument (metavar "FILENAME")) + <*> paramFileOpt + <*> many paramOpt + <*> parseProcessingOptions + <**> helper + ) (progDesc "execute (rewrite) the state in the file") ) <> command "simplify" ( info - (Simpl <$> strArgument (metavar "FILENAME")) + ( RunSingle + <$> (Simpl <$> strArgument (metavar "FILENAME")) + <*> paramFileOpt + <*> many paramOpt + <*> parseProcessingOptions + <**> helper + ) (progDesc "simplify the state or condition in the file") ) <> command "add-module" ( info - (AddModule <$> strArgument (metavar "FILENAME")) + ( RunSingle + <$> (AddModule <$> strArgument (metavar "FILENAME")) + <*> paramFileOpt + <*> many paramOpt + <*> parseProcessingOptions + <**> helper + ) (progDesc "add the module in the given kore file") ) <> command "get-model" ( info - (GetModel <$> strArgument (metavar "FILENAME")) + ( RunSingle + <$> (GetModel <$> strArgument (metavar "FILENAME")) + <*> paramFileOpt + <*> many paramOpt + <*> parseProcessingOptions + <**> helper + ) (progDesc "check satisfiability/provide model for the state in the file") ) + <> command + "run-tarball" + ( info + ( RunTarball + <$> strArgument (metavar "FILENAME") + <*> switch (long "keep-going" <> help "do not stop on unexpected output") + <**> helper + ) + (progDesc "Run all requests and compare responses from a bug report tarball") + ) ) + where + paramFileOpt = + optional $ + strOption $ + long "param-file" + <> metavar "PARAMFILE" + <> help "file with parameters (json object), optional" + paramOpt = + option readPair $ + short 'O' + <> metavar "NAME=VALUE" + <> help "parameters to use (name=value)" + readPair = + maybeReader $ \s -> case split (== '=') s of [k, v] -> Just (k, v); _ -> Nothing + +---------------------------------------- +-- Running all requests contained in the `rpc_*` directory of a tarball + +runTarball :: String -> Int -> FilePath -> Bool -> IO () +runTarball host port tarFile keepGoing = do + -- unpack tar files, determining type from extension(s) + let unpackTar + | ".tar" == takeExtension tarFile = Tar.read + | ".tgz" == takeExtension tarFile = Tar.read . GZip.decompress + | ".tar.gz" `isSuffixOf` takeExtensions tarFile = Tar.read . GZip.decompress + | ".tar.bz2" `isSuffixOf` takeExtensions tarFile = Tar.read . BZ2.decompress + | otherwise = Tar.read + + containedFiles <- unpackTar <$> BS.readFile tarFile + let checked = Tar.checkSecurity containedFiles + -- probe server connection before doing anything, display + -- instructions unless server was found. + runTCPClient host (show port) (runAllRequests checked) + `catch` noServerError + where + runAllRequests checked skt = do + -- unpack relevant tar files (rpc_* directory only) + withTempDir $ \tmp -> do + jsonFiles <- + trace (unwords ["[Info] unpacking json files from tarball", tarFile, "into", tmp]) $ + Tar.foldEntries (unpackIfRpc tmp) (pure []) throwAnyError checked + traceM $ "[Info] RPC data:" <> show jsonFiles + + let requests = mapMaybe (stripSuffix "_request.json") jsonFiles + results <- + forM requests $ \r -> do + mbError <- runRequest skt tmp jsonFiles r + case mbError of + Just err -> + trace ("[Error] Request " <> r <> " failed: " <> BS.unpack err) $ + unless keepGoing $ do + shutdown skt ShutdownReceive + exitWith (ExitFailure 2) + Nothing -> + hPutStrLn stderr "[Info] Response matched with expected" + pure mbError + shutdown skt ShutdownReceive + exitWith (if all isNothing results then ExitSuccess else ExitFailure 2) + + -- complain on any errors in the tarball + throwAnyError :: Either Tar.FormatError Tar.FileNameError -> IO a + throwAnyError = either throwIO throwIO + + -- unpack all rpc_*/*.json files into dir and return their names + unpackIfRpc :: FilePath -> Tar.Entry -> IO [FilePath] -> IO [FilePath] + unpackIfRpc tmpDir entry acc = do + case splitFileName (Tar.entryPath entry) of + -- assume single directory "rpc_" containing "*.json" files + (_, "") -- skip all directories + | Tar.Directory <- Tar.entryContent entry -> + acc + (dir, file) -- unpack json files into tmp directory + | "rpc_" `isPrefixOf` dir + , ".json" `isSuffixOf` file + , Tar.NormalFile bs _size <- Tar.entryContent entry -> do + BS.writeFile (tmpDir file) bs + (file :) <$> acc + _other -> + -- skip anything else + acc + + noServerError :: IOException -> IO () + noServerError e@IOError{ioe_type = NoSuchThing} = do + -- show instructions how to run the server + hPutStrLn stderr $ "[Error] Could not connect to RPC server on port " <> show port + hPutStrLn stderr $ "[Error] " <> show e + hPutStrLn stderr $ + unlines + [ "" + , "To run the required RPC server, you need to" + , "1) extract `definition.kore` and `server_instance.json` from the tarball;" + , "2) look up the module name `` in `server_instance.json`;" + , "3) and then run the server using" + , " $ kore-rpc definition.kore --module --server-port " <> show port + , "" + , "If you want to use `kore-rpc-booster, you should also compile an LLVM backend library" + , "by 1) extracting the `llvm_definition/` directory from the tarball;" + , " 2) running the llvm backend compiler on the unpacked files:" + , " $ llvm-kompile llvm_definition/definition.kore llvm_definition/dt c -- -o interpreter`" + , "This will generate `interpreter.[so|dylib]` and you can run" + , " `kore-rpc-booster definition.kore --main-module --llvm-backend-library interpreter.so`" + ] + exitWith (ExitFailure 1) + noServerError otherError = do + hPutStrLn stderr $ "[Error] " <> show otherError + exitWith (ExitFailure 1) + + -- Runs one request, checking that a response is available for + -- comparison. Returns Nothing if successful (identical + -- response), or rendered diff or error message if failing + runRequest :: Socket -> FilePath -> [FilePath] -> String -> IO (Maybe BS.ByteString) + runRequest skt tmpDir jsonFiles basename + | not . (`elem` jsonFiles) $ basename <> "_response.json" = + pure . Just . BS.pack $ "Response file " <> basename <> "_response.json is missing." + | not . (`elem` jsonFiles) $ basename <> "_request.json" = + pure . Just . BS.pack $ "Request file " <> basename <> "_request.json is missing." + | otherwise = do + request <- BS.readFile $ tmpDir basename <> "_request.json" + expected <- BS.readFile $ tmpDir basename <> "_response.json" + + actual <- makeRequest False basename skt 8192 request pure + + let diff = diffJson expected actual + if isIdentical diff + then pure Nothing + else pure . Just $ renderResult "expected response" "actual response" diff ---------------------------------------- prepareRequestData :: Mode -> Maybe FilePath -> [(String, String)] -> IO BS.ByteString diff --git a/unit-tests/Test/Booster/JsonRpc/DiffTest.hs b/unit-tests/Test/Booster/JsonRpc/DiffTest.hs index ee064f2f4..e786941c3 100644 --- a/unit-tests/Test/Booster/JsonRpc/DiffTest.hs +++ b/unit-tests/Test/Booster/JsonRpc/DiffTest.hs @@ -77,7 +77,7 @@ test_jsonDiff = do compareTest f1 f2 = do let expectedName = testDataDir "expected" takeFileName f1 <> "@" <> takeFileName f2 - renderedDiff = renderResult f1 f2 <$> diffJson f1 f2 + renderedDiff = fmap (renderResult f1 f2) $ diffJson <$> BS.readFile f1 <*> BS.readFile f2 testName = takeFileName f1 <> " vs " <> takeFileName f2 testGoldenVsString testName expectedName renderedDiff