From 698c1435edc485e4f719e53be50f34cce666e543 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Thu, 25 Jul 2024 08:43:22 +0200 Subject: [PATCH] Update `kore-rpc-client` to use `tar-0.6.3` (#3996) With https://github.com/runtimeverification/k/pull/4548, the bug reports will be generated in GNU format of tar files instead of the default POSIX.1-2001 pax format. This is necessary because: - the filenames in the bug reports are often longer than the format-portable restriction of 256 characters - the Haskell [library](https://hackage.haskell.org/package/tar-0.6.3.0) we use to work with tar does not support the pax format. However, it does support the GNU format which also allows long names. With this change, we get to process bug reports with long names. --- booster/tools/rpc-client/RpcClient.hs | 24 +- cabal.project.freeze | 12 +- dev-tools/package.yaml | 27 --- dev-tools/tarball-compare/Main.hs | 318 -------------------------- flake.nix | 4 +- stack.yaml | 1 + stack.yaml.lock | 7 + 7 files changed, 31 insertions(+), 362 deletions(-) delete mode 100644 dev-tools/tarball-compare/Main.hs diff --git a/booster/tools/rpc-client/RpcClient.hs b/booster/tools/rpc-client/RpcClient.hs index 83a48ddd2c..80544c2d45 100644 --- a/booster/tools/rpc-client/RpcClient.hs +++ b/booster/tools/rpc-client/RpcClient.hs @@ -15,7 +15,7 @@ module RpcClient ( ) where import Codec.Archive.Tar qualified as Tar -import Codec.Archive.Tar.Check qualified as Tar +import Codec.Archive.Tar.Entry qualified as Tar import Codec.Compression.BZip qualified as BZ2 import Codec.Compression.GZip qualified as GZip import Control.Exception @@ -505,20 +505,24 @@ runTarball common (Just sock) tarFile keepGoing runOnly compareDetails = do | ".tar.bz2" `isSuffixOf` takeExtensions tarFile = Tar.read . BZ2.decompress | otherwise = Tar.read - containedFiles <- unpackTar <$> BS.readFile tarFile - let checked = Tar.checkSecurity containedFiles + entries <- Tar.decodeLongNames . unpackTar <$> BS.readFile tarFile -- probe server connection before doing anything, display -- instructions unless server was found. - runAllRequests checked sock + runAllRequests entries sock where runAllRequests :: - Tar.Entries (Either Tar.FormatError Tar.FileNameError) -> Socket -> IO () + Tar.GenEntries + FilePath + a + (Either Tar.FormatError Tar.DecodeLongNamesError) -> + Socket -> + IO () runAllRequests checked skt = cancelIfInterrupted skt $ do withTempDir $ \tmp -> withLogLevel common.logLevel $ do -- unpack relevant tar files (rpc_* directories only) logInfo_ $ unwords ["unpacking json files from tarball", tarFile, "into", tmp] (jsonFiles, sequenceMap) <- - liftIO $ Tar.foldEntries (unpackIfRpc tmp) (pure mempty) throwAnyError checked + liftIO $ Tar.foldEntries (unpackIfRpc tmp) (pure mempty) (error . show) checked logInfo_ $ "RPC data:" <> show jsonFiles logInfo_ $ "Sequence data:" <> show sequenceMap @@ -543,10 +547,6 @@ runTarball common (Just sock) tarFile keepGoing runOnly compareDetails = do liftIO $ shutdown skt ShutdownReceive liftIO $ 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 - compareSequence :: Ord a => Ord b => Map.Map a b -> a -> a -> Ordering compareSequence seqMap a b = case (Map.lookup a seqMap, Map.lookup b seqMap) of (Nothing, Nothing) -> compare a b @@ -557,11 +557,11 @@ runTarball common (Just sock) tarFile keepGoing runOnly compareDetails = do -- unpack all */*.json files into dir and return their names unpackIfRpc :: FilePath -> - Tar.Entry -> + Tar.GenEntry FilePath a -> IO ([FilePath], Map.Map FilePath Int) -> IO ([FilePath], Map.Map FilePath Int) unpackIfRpc tmpDir entry acc = do - case splitFileName (Tar.entryPath entry) of + case splitFileName (Tar.entryTarPath entry) of -- unpack all directories "" containing "*.json" files (dir, "") -- directory | Tar.Directory <- Tar.entryContent entry -> do diff --git a/cabal.project.freeze b/cabal.project.freeze index 880df446e0..2c1bf4233f 100644 --- a/cabal.project.freeze +++ b/cabal.project.freeze @@ -37,7 +37,7 @@ constraints: any.Cabal ==3.10.3.0, any.bytesmith ==0.3.11.1, any.bytestring ==0.11.5.3, any.bz2 ==1.0.1.2, - any.cabal-doctest ==1.0.9, + any.cabal-doctest ==1.0.10, any.call-stack ==0.4.0, any.case-insensitive ==1.2.1.0, any.casing ==0.1.4.1, @@ -81,6 +81,7 @@ constraints: any.Cabal ==3.10.3.0, any.extra ==1.7.16, any.fast-logger ==3.2.3, any.fgl ==5.8.2.0, + any.file-embed ==0.0.11.2, any.filepath ==1.4.300.1, any.free ==5.2, any.generic-lens ==2.2.2.0, @@ -91,6 +92,7 @@ constraints: any.Cabal ==3.10.3.0, any.ghc-compact ==0.1.0.0, any.ghc-events ==0.19.0.1, any.ghc-prim ==0.10.0, + any.ghc-prof ==1.4.1.12, any.ghc-trace-events ==0.1.2.9, any.gitrev ==1.3.1, any.graphviz ==2999.20.2.0, @@ -117,6 +119,7 @@ constraints: any.Cabal ==3.10.3.0, any.integer-logarithms ==1.0.3.1, any.intern ==0.9.5, any.invariant ==0.6.3, + any.js-jquery ==3.3.1, any.json-rpc ==1.0.4, any.junit-xml ==0.1.0.3, any.kan-extensions ==5.2.6, @@ -148,6 +151,7 @@ constraints: any.Cabal ==3.10.3.0, any.old-locale ==1.0.0.7, any.old-time ==1.1.0.4, any.optparse-applicative ==0.18.1.0, + any.os-string ==2.0.2.2, any.parallel ==3.2.2.0, any.parsec ==3.1.16.1, any.parser-combinators ==1.3.0, @@ -162,6 +166,8 @@ constraints: any.Cabal ==3.10.3.0, any.primitive-offset ==0.2.0.1, any.primitive-unlifted ==2.1.0.0, any.process ==1.6.19.0, + any.profiteur ==0.4.7.0, + profiteur +embed-data-files, any.profunctors ==5.6.2, any.quickcheck-instances ==0.3.30, quickcheck-instances -bytestring-builder, @@ -198,7 +204,7 @@ constraints: any.Cabal ==3.10.3.0, any.string-conversions ==0.4.0.1, any.syb ==0.7.2.4, any.tagged ==0.8.8, - any.tar ==0.5.1.1, + any.tar ==0.6.3.0, any.tasty ==1.4.3, tasty +unix, any.tasty-discover ==5.0.0, @@ -254,4 +260,4 @@ constraints: any.Cabal ==3.10.3.0, any.yaml ==0.11.11.2, any.zigzag ==0.0.1.0, any.zlib ==0.6.3.0 -index-state: hackage.haskell.org 2024-05-24T09:11:31Z +index-state: hackage.haskell.org 2024-07-22T06:21:59Z diff --git a/dev-tools/package.yaml b/dev-tools/package.yaml index ce458bdab7..3ab1e66bc3 100644 --- a/dev-tools/package.yaml +++ b/dev-tools/package.yaml @@ -173,33 +173,6 @@ executables: - hs-backend-booster ghc-options: - -rtsopts - tarball-compare: - source-dirs: tarball-compare - main: Main - dependencies: - - aeson - - aeson-pretty - - base - - bytestring - - bz2 - - clock - - containers - - directory - - extra - - filepath - - hs-backend-booster - - kore-rpc-types - - monad-logger - - optparse-applicative - - prettyprinter - - recursion-schemes - - tar - - text - - transformers - - vector - - zlib - ghc-options: - - -rtsopts kore-rpc-dev: source-dirs: kore-rpc-dev main: Server.hs diff --git a/dev-tools/tarball-compare/Main.hs b/dev-tools/tarball-compare/Main.hs deleted file mode 100644 index 2565407090..0000000000 --- a/dev-tools/tarball-compare/Main.hs +++ /dev/null @@ -1,318 +0,0 @@ -{- | -Copyright : (c) Runtime Verification, 2022 -License : BSD-3-Clause - -Tool to compare two bug report tarballs (or directories containing an -unpacked bug report) for correspondence. The following comparisons are -performed: - -. compare number of request/response files in the tarball -. compare definition.kore file in the tarball (top-level) -Then, for each pair of requests or responses in the rpc_* directories: - . compare file contents and file size of json files - . compare the number of steps (depth) in responses to execute requests - . internalise states in response data (based on the definition.kore - file) and compare internal data (displaying diff if not equal) - -The tool can work on: - -. a single gzipped tarball containing other tarballs for many tests - (when given a single argument) -. two tarballs or directories of unpacked bug report data, assumed to - contain the same rpc_* directory names (two files as arguments) . - (when given two arguments, each one either a tar file or a directory) --} -module Main ( - module 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.Monad (forM, forM_, unless, when) -import Control.Monad.Trans.Writer -import Data.ByteString.Lazy.Char8 qualified as BS -import Data.List.Extra as List -import Data.Map (Map) -import Data.Map qualified as Map -import Data.Maybe (catMaybes, fromMaybe) -import Data.Text.Encoding qualified as Text -import System.Directory -import System.Directory.Extra -import System.Environment (getArgs) -import System.FilePath - -import Booster.JsonRpc.Utils -import Booster.Syntax.Json (sortOfJson) -import Booster.Syntax.ParsedKore (internalise, parseKoreDefinition) -import Kore.JsonRpc.Types -import Kore.Syntax.Json.Types hiding (Left, Right) - -data BugReportData = BugReportData - { requests :: Map FilePath BS.ByteString - , responses :: Map FilePath BS.ByteString - , definition :: BS.ByteString - } - deriving (Show) - -emptyBugReport :: BugReportData -emptyBugReport = BugReportData mempty mempty "INVALID" - -data BugReportDiff = BugReportDiff - { booster :: BugReportData - , koreRpc :: BugReportData - } - deriving (Show) - -emptyDiff :: BugReportDiff -emptyDiff = BugReportDiff emptyBugReport emptyBugReport - -main :: IO () -main = - getArgs >>= \case - [tarFile] -> do - contents <- readToTar tarFile - case unpackBugReports contents of - Left err -> either print print err - Right bugReports -> - forM_ (Map.toList bugReports) $ - mapM_ BS.putStrLn . uncurry checkDiff - [tar1, tar2] -> do - let dataFrom = - fmap (either (error . either show show) id . unpackBugReportDataFrom) - . readToTar - bugReportDiff <- - BugReportDiff - <$> dataFrom tar1 - <*> dataFrom tar2 - mapM_ BS.putStrLn $ checkDiff (tar1 <> "<->" <> tar2) bugReportDiff - _ -> putStrLn "incorrect args" - where - readToTar :: FilePath -> IO (Tar.Entries (Either Tar.FormatError Tar.FileNameError)) - readToTar file - | ".tar" == takeExtension file = - Tar.checkSecurity . Tar.read <$> BS.readFile file - | ".tgz" == takeExtension file || ".tar.gz" `isSuffixOf` takeExtensions file = - Tar.checkSecurity . Tar.read . GZip.decompress <$> BS.readFile file - | ".tar.bz2" `isSuffixOf` takeExtensions file = - Tar.checkSecurity . Tar.read . BZ2.decompress <$> BS.readFile file - | otherwise = do - isDir <- doesDirectoryExist file - if isDir - then withCurrentDirectory file $ do - -- create a Tar.Entries structure from the rpc_* - -- directories within the directory (ignore all other - -- files and subdirectories) - subdirs <- - filter (dirPrefix `isPrefixOf`) . map takeFileName <$> listDirectories "." - let hasCorrectSuffix f = - requestSuffix `isSuffixOf` f || responseSuffix `isSuffixOf` f - files <- - filter hasCorrectSuffix . concat <$> mapM listFiles subdirs - defFile <- - fromMaybe (error $ "No definition found in " <> file) - . find (== "./definition.kore") - <$> listFiles "." - - entries <- Tar.pack "." $ defFile : files - -- need to force the tar entries, withCurrentDirectory is not retained - mapM_ (`seq` pure ()) entries - pure $ foldr Tar.Next Tar.Done entries - else -- if a differently-named file was given. try to read a tarball - Tar.checkSecurity . Tar.read <$> BS.readFile file - -unpackBugReports :: - Tar.Entries (Either Tar.FormatError Tar.FileNameError) -> - Either (Either Tar.FormatError Tar.FileNameError) (Map FilePath BugReportDiff) -unpackBugReports = Tar.foldEntries unpackBugReportData (Right mempty) Left - where - unpackBugReportData :: - Tar.Entry -> - Either (Either Tar.FormatError Tar.FileNameError) (Map FilePath BugReportDiff) -> - Either (Either Tar.FormatError Tar.FileNameError) (Map FilePath BugReportDiff) - unpackBugReportData _ err@(Left _) = err - unpackBugReportData entry acc@(Right m) - | Tar.NormalFile bs _size <- Tar.entryContent entry - , ".tar" `isSuffixOf` file - , contents <- Tar.read bs = - case unpackBugReportDataFrom contents of - Left err -> Left $ Left err - Right bugReport -> Right $ Map.alter (insertBugReport bugReport) file m - | otherwise = acc - where - (dir, file) = splitFileName (Tar.entryPath entry) - insertBugReport b bDiff = - Just - $ ( \bugReportDiff -> - if "booster" `isInfixOf` dir - then bugReportDiff{booster = b} - else bugReportDiff{koreRpc = b} - ) - $ fromMaybe emptyDiff bDiff - -{- Unpack all files inside rpc_* directories in a tarball, into maps - of file prefixes (dir.name and number) to requests and resp. responses. - - There may be multiple rpc_* directories in a single tarball, therefore - the map keys have to contain the directory name. --} -unpackBugReportDataFrom :: - Tar.Entries err -> - Either err BugReportData -unpackBugReportDataFrom = Tar.foldEntries unpackRpc (Right emptyBugReport) Left - where - unpackRpc :: - Tar.Entry -> - Either err BugReportData -> - Either err BugReportData - unpackRpc _ err@(Left _) = err - unpackRpc entry acc@(Right bugReportData) - | Tar.NormalFile bs _size <- Tar.entryContent entry - , Just dir <- stripPrefix dirPrefix rpcDir - , ".json" `isSuffixOf` file = - let (isRequest, number, json) - | Just num <- stripSuffix requestSuffix file = - (True, num, bs) - | Just num <- stripSuffix responseSuffix file = - (False, num, bs) - | otherwise = error $ "Bad file in tarball: " <> show (rpcDir file) - in Right $ - if isRequest - then bugReportData{requests = Map.insert (dir <> number) json bugReportData.requests} - else bugReportData{responses = Map.insert (dir <> number) json bugReportData.responses} - | Tar.NormalFile bs _size <- Tar.entryContent entry - , rpcDir == "./" -- dir output of splitFileName for names without path - , file == "definition.kore" = - Right bugReportData{definition = bs} - | otherwise = acc - where - (rpcDir, file) = splitFileName (Tar.entryPath entry) - -dirPrefix, requestSuffix, responseSuffix :: FilePath -dirPrefix = "rpc_" -requestSuffix = "_request.json" -responseSuffix = "_response.json" - -checkDiff :: FilePath -> BugReportDiff -> [BS.ByteString] -checkDiff name BugReportDiff{booster, koreRpc} = - "------------- " <> BS.pack name <> " -------------" - : if null $ Map.keys booster.requests - then ["No Booster data... skipping..."] - else execWriter $ do - when (booster.definition /= koreRpc.definition) $ do - msg $ - "Definitions in bug reports differ " - <> compareSizes booster.definition koreRpc.definition - when - ( Map.keys koreRpc.requests /= Map.keys booster.requests - || Map.keys koreRpc.responses /= Map.keys booster.responses - ) - $ msg "Booster and kore-rpc have different requests/responses" - forM (Map.toList koreRpc.requests) $ \(koreRpcReqKey, koreRpcReqJson) -> do - let keyBS = BS.pack koreRpcReqKey - case Map.lookup koreRpcReqKey booster.requests of - Nothing -> - msg $ "Request " <> keyBS <> " does not exist in booster" - Just boosterReqJson -> do - let koreTp = requestType koreRpcReqJson - boosTp = requestType boosterReqJson - when (koreTp /= boosTp) $ - strMsg $ - "Requests have different type: " <> show (boosTp, koreTp) - compareJson - "Requests" - keyBS - koreRpcReqJson - boosterReqJson - comparePatternsIn "requests" keyBS boosterReqJson koreRpcReqJson - case (Map.lookup koreRpcReqKey koreRpc.responses, Map.lookup koreRpcReqKey booster.responses) of - (Just koreResp, Just boosterResp) -> do - compareJson - "Responses" - keyBS - koreResp - boosterResp - let koreDepth = responseDepth koreResp - boosDepth = responseDepth boosterResp - when (koreDepth /= boosDepth) $ - strMsg $ - "Execution depth differs: " - <> show boosDepth - <> " vs " - <> show koreDepth - comparePatternsIn "responses" keyBS boosterResp koreResp - (Just _, Nothing) -> - msg $ "Response " <> keyBS <> " missing in booster" - (Nothing, Just _) -> - msg $ "Response " <> keyBS <> " missing in kore-rpc" - (Nothing, Nothing) -> - msg $ "Response " <> keyBS <> " missing" - where - msg = tell . (: []) - strMsg = msg . BS.pack - - compareJson :: - BS.ByteString -> - BS.ByteString -> - BS.ByteString -> - BS.ByteString -> - Writer [BS.ByteString] () - compareJson prefix key koreJson boosterJson = - when (koreJson /= boosterJson) $ - msg $ - BS.unwords - [prefix, "for", key, "are different", compareSizes boosterJson koreJson] - - compareSizes bsBooster bsKore = - case compare (BS.length bsBooster) (BS.length bsKore) of - LT -> "(kore bigger)" - EQ -> "(same size)" - GT -> "(booster bigger)" - - requestType :: BS.ByteString -> KoreRpcType - requestType = rpcTypeOf . decodeKoreRpc - - responseDepth :: BS.ByteString -> Maybe Depth - responseDepth json = - case decodeKoreRpc json of - RpcResponse (Execute r) -> Just r.depth - _other -> Nothing - - bDef = - -- HACK: compare contents using the default module and booster def - either (error . show) id - . internalise Nothing - . either error id - . parseKoreDefinition (name <> "/definition.kore") - . Text.decodeUtf8 - $ BS.toStrict booster.definition - - patternsIn :: KoreRpcJson -> [KorePattern] - patternsIn (RpcRequest (Execute r)) = [r.state.term] - -- no need for patternsIn (RpcRequest (Implies r)) = map internalised [r.antecedent.term, r.consequent.term] - patternsIn (RpcRequest (Simplify r)) = [r.state.term] - patternsIn (RpcResponse (Execute r)) = fromState r.state : maybe [] (List.sortOn show . map fromState) r.nextStates - patternsIn (RpcResponse (Simplify r)) = [r.state.term] - -- no need for patternsIn (RpcResponse (Implies r)) = [internalised r.implication.term] - patternsIn (RpcKoreJson state) = [state.term] - patternsIn _other = [] - - fromState :: ExecuteState -> KorePattern - fromState exState = - case catMaybes [exState.substitution, exState.predicate] of - [] -> exState.term.term - ps@(p : _) -> - KJAnd - (fromMaybe (error "no sort") $ sortOfJson p.term) - (exState.term.term : map (.term) ps) - - comparePatternsIn tipe key bsBooster bsKore = do - let bPats = patternsIn $ decodeKoreRpc bsBooster - kPats = patternsIn $ decodeKoreRpc bsKore - diffs = catMaybes $ zipWith (diffBy bDef) bPats kPats - if length bPats /= length kPats - then msg "Different amount of patterns" - else unless (null diffs) $ do - msg ("Patterns in " <> tipe <> " " <> key <> " differ.") - mapM_ (msg . BS.pack) diffs diff --git a/flake.nix b/flake.nix index 6dd77b878e..9e9ba3440b 100644 --- a/flake.nix +++ b/flake.nix @@ -104,8 +104,8 @@ # this need to be bumped if changing the stack resolver all-cabal-hashes = final.fetchurl { url = - "https://github.com/commercialhaskell/all-cabal-hashes/archive/8b0d7c881466c603de7975596cb203e3fd4890ad.tar.gz"; - sha256 = "sha256-jTNSwG37bHY5vLMo5yqtk93sTUzlsp/jeYCfXJGaivU="; + "https://github.com/commercialhaskell/all-cabal-hashes/archive/ce857734d7d4c0fad3f6dda3a4db052836ed4619.tar.gz"; + sha256 = "sha256-Q7Zg32v5ubjVJMQXGiyyMmeFg08jTzVRKC18laiHCPE="; }; }; }; diff --git a/stack.yaml b/stack.yaml index b3b31ad2f1..b42775a83b 100644 --- a/stack.yaml +++ b/stack.yaml @@ -14,6 +14,7 @@ packages: # Dependency packages to be pulled from upstream that are not in the resolver extra-deps: + - tar-0.6.3.0 - hashable-1.4.2.0 - decision-diagrams-0.2.0.0 - smtlib-backends-0.3 diff --git a/stack.yaml.lock b/stack.yaml.lock index 73b1ba46c4..098f216431 100644 --- a/stack.yaml.lock +++ b/stack.yaml.lock @@ -4,6 +4,13 @@ # https://docs.haskellstack.org/en/stable/lock_files packages: +- completed: + hackage: tar-0.6.3.0@sha256:e9f151d9999be8953443e730524b2792e9c0a4fb5b1463097fa1a8230870fd8a,4634 + pantry-tree: + sha256: e59e0d0224352033c32356d517f90d4c6a41cee4fa0d386885df146302d1ba3b + size: 2241 + original: + hackage: tar-0.6.3.0 - completed: hackage: hashable-1.4.2.0@sha256:585792335d5541dba78fa8dfcb291a89cd5812a281825ff7a44afa296ab5d58a,4520 pantry-tree: