kore-rpc-client: Add an --omit-details flag for run-tarball mode (#3961)

When running fall-back analysis, it is usually not interesting whether
all response terms match exactly with the expectations. (For instance,
one might change the definition and expect fewer fall-backs, but also
cause slightly changed output)

The new flag `--omit-details` for `kore-rpc-client run-tarball` only
checks that the response _type_ matches (i.e., no unexpected errors have
happened).

Author: jberthold

booster/tools/rpc-client/RpcClient.hs

@@ -52,12 +52,14 @@ import Text.Read (readMaybe)
 
 import Booster.JsonRpc (rpcJsonConfig)
 import Booster.JsonRpc.Utils (
+    DiffResult (DifferentType),
     KoreRpcJson (RpcRequest),
     decodeKoreRpc,
     diffJson,
     isIdentical,
     methodOfRpcCall,
     renderResult,
+    rpcTypeOf,
  )
 import Booster.Prettyprinter (renderDefault)
 import Booster.Syntax.Json qualified as Syntax
@@ -85,8 +87,8 @@ handleRunOptions common@CommonOptions{dryRun} s = \case
     [] -> case s of
         Just sock -> shutdown sock ShutdownReceive
         Nothing -> pure ()
-    (RunTarball tarFile keepGoing runOnly : xs) -> do
-        runTarball common s tarFile keepGoing runOnly
+    (RunTarball tarFile keepGoing runOnly noDetails : xs) -> do
+        runTarball common s tarFile keepGoing runOnly (not noDetails)
         handleRunOptions common s xs
     (RunSingle mode optionFile options processingOptions : xs) -> do
         let ProcessingOptions{postProcessing, prettify, time} = processingOptions
@@ -246,7 +248,8 @@ data RunOptions
       RunTarball
         FilePath -- tar file
         Bool -- do not stop on first diff if set to true
-        [Kore.JsonRpc.Types.APIMethod] -- only run specified types of requests. run all if empty
+        [Kore.JsonRpc.Types.APIMethod] -- only run specified types of requests. Run all if empty.
+        Bool -- omit detailed comparison with expected output
     deriving stock (Show)
 
 data ProcessingOptions = ProcessingOptions
@@ -448,6 +451,10 @@ parseMode =
                             ( long "run-only"
                                 <> help "Only run the specified request(s), e.g. --run-only \"add-module implies\""
                             )
+                        <*> switch
+                            ( long "omit-details"
+                                <> help "only compare response types, not contents"
+                            )
                         <**> helper
                     )
                     (progDesc "Run all requests and compare responses from a bug report tarball")
@@ -479,9 +486,15 @@ parseMode =
 -- Running all requests contained in the `rpc_*` directory of a tarball
 
 runTarball ::
-    CommonOptions -> Maybe Socket -> FilePath -> Bool -> [Kore.JsonRpc.Types.APIMethod] -> IO ()
-runTarball _ Nothing _ _ _ = pure ()
-runTarball common (Just sock) tarFile keepGoing runOnly = do
+    CommonOptions ->
+    Maybe Socket ->
+    FilePath ->
+    Bool ->
+    [Kore.JsonRpc.Types.APIMethod] ->
+    Bool ->
+    IO ()
+runTarball _ Nothing _ _ _ _ = pure ()
+runTarball common (Just sock) tarFile keepGoing runOnly compareDetails = do
     -- unpack tar files, determining type from extension(s)
     let unpackTar
             | ".tar" == takeExtension tarFile = Tar.read
@@ -509,6 +522,7 @@ runTarball common (Just sock) tarFile keepGoing runOnly = do
             -- we should not rely on the requests being returned in a sorted order and
             -- should therefore sort them explicitly
             let requests = sort $ mapMaybe (stripSuffix "_request.json") jsonFiles
+                successMsg = if compareDetails then "matches expected" else "has expected type"
             results <-
                 forM requests $ \r -> do
                     mbError <- runRequest skt tmp jsonFiles r
@@ -519,7 +533,7 @@ runTarball common (Just sock) tarFile keepGoing runOnly = do
                                 liftIO $
                                     shutdown skt ShutdownReceive >> exitWith (ExitFailure 2)
                         Nothing ->
-                            logInfo_ $ "Response to " <> r <> " matched with expected"
+                            logInfo_ $ unwords ["Response to", r, successMsg]
                     pure mbError
             liftIO $ shutdown skt ShutdownReceive
             liftIO $ exitWith (if all isNothing results then ExitSuccess else ExitFailure 2)
@@ -569,13 +583,22 @@ runTarball common (Just sock) tarFile keepGoing runOnly = do
             request <- liftIO . BS.readFile $ tmpDir </> basename <> "_request.json"
             expected <- liftIO . BS.readFile $ tmpDir </> basename <> "_response.json"
 
+            let showResult =
+                    renderResult "expected response" "actual response"
             makeRequest False basename (Just skt) request pure runOnly >>= \case
                 Nothing -> pure Nothing -- should not be reachable
-                Just actual -> do
-                    let diff = diffJson expected actual
-                    if isIdentical diff
-                        then pure Nothing
-                        else pure . Just $ renderResult "expected response" "actual response" diff
+                Just actual
+                    | compareDetails -> do
+                        let diff = diffJson expected actual
+                        if isIdentical diff
+                            then pure Nothing
+                            else pure . Just $ showResult diff
+                    | otherwise -> do
+                        let expectedType = rpcTypeOf (decodeKoreRpc expected)
+                            actualType = rpcTypeOf (decodeKoreRpc actual)
+                        if expectedType == actualType
+                            then pure Nothing
+                            else pure . Just $ showResult (DifferentType expectedType actualType)
 
 noServerError :: MonadLoggerIO m => CommonOptions -> IOException -> m ()
 noServerError common e@IOError{ioe_type = NoSuchThing} = do

scripts/booster-analysis.sh

@@ -46,7 +46,7 @@ export PLUGIN_DIR=$(nix build github:runtimeverification/blockchain-k-plugin/$PL
 
 run_tarball(){
   echo "######## $1 ########";
-  $SCRIPT_DIR/run-with-tarball.sh "$1" -l Aborts --log-format json --log-file "$LOG_DIR/$(basename "$1").json.log" --print-stats ${SERVER_OPTS} 2>&1 | tee "$LOG_DIR/$(basename "$1").out";
+  $SCRIPT_DIR/run-with-tarball.sh "$1" -l Aborts --log-format json --log-file "$LOG_DIR/$(basename "$1").json.log" -l Timing ${SERVER_OPTS} 2>&1 | tee "$LOG_DIR/$(basename "$1").out";
 }
 
 export -f run_tarball

scripts/run-with-tarball.sh

@@ -135,7 +135,7 @@ server_port=$($LSOF -a -p${server_pid} -sTCP:LISTEN -iTCP | grep ${server_pid} |
 echo "Server listening on port ${server_port}"
 
 
-echo "Running requests from $tarball against the server: $client run-tarball '$tarball' --keep-going -p ${server_port} -h 127.0.0.1"
-$client run-tarball "$tarball" --keep-going -p ${server_port} -h 127.0.0.1
+echo "Running requests from $tarball against the server: $client run-tarball '$tarball' --keep-going --omit-details -p ${server_port} -h 127.0.0.1"
+$client run-tarball "$tarball" --keep-going --omit-details -p ${server_port} -h 127.0.0.1
 
 echo "Done with '$tarball'"