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 d84656d533..befdb6f7f1 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: