diff --git a/.gitignore b/.gitignore index a8ccdd032f..38a23e80e7 100644 --- a/.gitignore +++ b/.gitignore @@ -47,4 +47,4 @@ cabal.project.local /shell.local.nix /TAGS /.TAGS* -report-*/ \ No newline at end of file +kore-exec.tar.gz diff --git a/.hlint.yaml b/.hlint.yaml index a846084914..cbd317d99c 100644 --- a/.hlint.yaml +++ b/.hlint.yaml @@ -31,6 +31,7 @@ - modules: - {name: [Data.Map], within: []} + - {name: [System.FilePath.Posix], within: []} - name: - Data.Text.Prettyprint.Doc - Data.Text.Prettyprint.Doc.Render.Text diff --git a/kore/app/exec/Main.hs b/kore/app/exec/Main.hs index a31db9e12b..d2a65546e3 100644 --- a/kore/app/exec/Main.hs +++ b/kore/app/exec/Main.hs @@ -6,13 +6,10 @@ import Control.Monad.Catch ( MonadCatch , SomeException , displayException - , finally , handle , throwM ) -import Control.Monad.Trans - ( lift - ) +import Control.Monad.Extra as Monad import qualified Data.Char as Char import Data.Default ( def @@ -73,6 +70,9 @@ import System.Exit ( ExitCode (..) , exitWith ) +import System.FilePath + ( () + ) import System.IO ( IOMode (WriteMode) , withFile @@ -81,9 +81,6 @@ import System.IO import qualified Data.Limit as Limit import Kore.Attribute.Symbol as Attribute import Kore.BugReport - ( BugReport (..) - , parseBugReport - ) import Kore.Exec import Kore.IndexedModule.IndexedModule ( VerifiedModule @@ -117,7 +114,6 @@ import Kore.Log , LogMessage , SomeEntry (..) , WithLog - , archiveDirectoryReport , logEntry , parseKoreLogOptions , runKoreLog @@ -178,12 +174,8 @@ import SMT ) import qualified SMT import Stats -import qualified System.IO.Temp as Temp import GlobalMain -import System.FilePath.Posix - ( () - ) {- Main module to run kore-exec @@ -504,9 +496,14 @@ writeKoreMergeFiles reportFile KoreMergeOptions { rulesFileName } = copyFile rulesFileName $ reportFile <> "/mergeRules.kore" writeKoreProveFiles :: FilePath -> KoreProveOptions -> IO () -writeKoreProveFiles reportFile KoreProveOptions { specFileName, saveProofs } = do - copyFile specFileName $ reportFile <> "/spec.kore" - Foldable.forM_ saveProofs $ flip copyFile (reportFile <> "/saveProofs.kore") +writeKoreProveFiles reportFile koreProveOptions = do + let KoreProveOptions { specFileName } = koreProveOptions + copyFile specFileName (reportFile "spec.kore") + let KoreProveOptions { saveProofs } = koreProveOptions + Foldable.forM_ saveProofs $ \filePath -> + Monad.whenM + (doesFileExist filePath) + (copyFile filePath (reportFile "save-proofs.kore")) writeOptionsAndKoreFiles :: FilePath -> KoreExecOptions -> IO () writeOptionsAndKoreFiles @@ -548,34 +545,31 @@ writeOptionsAndKoreFiles koreProveOptions (writeKoreProveFiles reportDirectory) +exeName :: ExeName +exeName = ExeName "kore-exec" + -- TODO(virgil): Maybe add a regression test for main. -- | Loads a kore definition file and uses it to execute kore programs main :: IO () main = do - options <- - mainGlobal (ExeName "kore-exec") parseKoreExecOptions parserInfoModifiers + options <- mainGlobal Main.exeName parseKoreExecOptions parserInfoModifiers Foldable.forM_ (localOptions options) mainWithOptions mainWithOptions :: KoreExecOptions -> IO () mainWithOptions execOptions = do let KoreExecOptions { koreLogOptions, bugReport } = execOptions - Temp.withSystemTempDirectory - (fromMaybe "report" $ toReport bugReport) - $ \tempDirectory -> do - traceM tempDirectory - exitCode <- - runKoreLog tempDirectory koreLogOptions - $ handle (handleSomeException tempDirectory) - $ handle handleSomeEntry - $ handle handleWithConfiguration go - let KoreExecOptions { rtsStatistics } = execOptions - Foldable.forM_ rtsStatistics $ \filePath -> - writeStats filePath =<< getStats - let reportPath = maybe tempDirectory ("./" <>) (toReport bugReport) - finally - (writeInReportDirectory tempDirectory) - (archiveDirectoryReport tempDirectory reportPath) - exitWith exitCode + exitCode <- + withBugReport Main.exeName bugReport $ \tmpDir -> do + writeOptionsAndKoreFiles tmpDir execOptions + go + & handle handleWithConfiguration + & handle handleSomeEntry + & handle (handleSomeException tmpDir) + & runKoreLog tmpDir koreLogOptions + let KoreExecOptions { rtsStatistics } = execOptions + Foldable.forM_ rtsStatistics $ \filePath -> + writeStats filePath =<< getStats + exitWith exitCode where KoreExecOptions { koreProveOptions } = execOptions KoreExecOptions { koreSearchOptions } = execOptions @@ -621,13 +615,6 @@ mainWithOptions execOptions = do | otherwise = koreRun execOptions - writeInReportDirectory :: FilePath -> IO () - writeInReportDirectory tempDirectory = do - when . isJust . toReport . bugReport - <*> writeOptionsAndKoreFiles tempDirectory $ execOptions - Foldable.forM_ (outputFileName execOptions) - $ flip copyFile (tempDirectory <> "/outputFile.kore") - koreSearch :: KoreExecOptions -> KoreSearchOptions -> Main ExitCode koreSearch execOptions searchOptions = do let KoreExecOptions { definitionFileName } = execOptions diff --git a/kore/app/repl/Main.hs b/kore/app/repl/Main.hs index 8d3bda281f..143dd22f32 100644 --- a/kore/app/repl/Main.hs +++ b/kore/app/repl/Main.hs @@ -34,11 +34,13 @@ import Options.Applicative ) import System.Exit ( exitFailure + , exitWith ) import Data.Limit ( Limit (..) ) +import Kore.BugReport import Kore.Exec ( proveWithRepl ) @@ -47,7 +49,6 @@ import qualified Kore.IndexedModule.MetadataToolsBuilder as MetadataTools ) import Kore.Log ( KoreLogOptions (..) - , archiveDirectoryReport , runLoggerT , swappableLogger , withLogger @@ -61,7 +62,6 @@ import Kore.Syntax.Module ( ModuleName (..) ) import qualified SMT -import qualified System.IO.Temp as Temp import GlobalMain @@ -185,10 +185,12 @@ parserInfoModifiers = <> progDesc "REPL debugger for proofs" <> header "kore-repl - a repl for Kore proofs" +exeName :: ExeName +exeName = ExeName "kore-repl" + main :: IO () main = do - options <- - mainGlobal (ExeName "kore-repl") parseKoreReplOptions parserInfoModifiers + options <- mainGlobal Main.exeName parseKoreReplOptions parserInfoModifiers case localOptions options of Nothing -> pure () Just koreReplOptions -> mainWithOptions koreReplOptions @@ -205,10 +207,9 @@ mainWithOptions , outputFile , koreLogOptions } - = - Temp.withSystemTempDirectory - "report" - $ \tempDirectory -> + = do + exitCode <- + withBugReport Main.exeName (BugReport Nothing) $ \tempDirectory -> withLogger tempDirectory koreLogOptions $ \actualLogAction -> do mvarLogAction <- newMVar actualLogAction let swapLogAction = swappableLogger mvarLogAction @@ -257,8 +258,9 @@ mainWithOptions scriptModeOutput outputFile mainModuleName - archiveDirectoryReport tempDirectory tempDirectory + pure ExitSuccess + exitWith exitCode where mainModuleName :: ModuleName mainModuleName = moduleName definitionModule diff --git a/kore/src/Kore/BugReport.hs b/kore/src/Kore/BugReport.hs index d748711851..eff8448062 100644 --- a/kore/src/Kore/BugReport.hs +++ b/kore/src/Kore/BugReport.hs @@ -7,11 +7,46 @@ License : NCSA module Kore.BugReport ( BugReport (..) , parseBugReport + , withBugReport + -- * Re-exports + , ExitCode (..) ) where import Prelude.Kore +import qualified Codec.Archive.Tar as Tar +import qualified Codec.Compression.GZip as GZip +import Control.Monad.Catch + ( ExitCase (..) + , displayException + , generalBracket + ) +import qualified Data.ByteString.Lazy as ByteString.Lazy +import qualified Data.Foldable as Foldable import Options.Applicative +import System.Directory + ( listDirectory + , removePathForcibly + ) +import System.Exit + ( ExitCode (..) + ) +import System.FilePath + ( (<.>) + , () + ) +import System.IO + ( hPutStrLn + , stderr + ) +import System.IO.Temp + ( createTempDirectory + , getCanonicalTemporaryDirectory + ) + +import Kore.Log.KoreLogOptions + ( ExeName (..) + ) newtype BugReport = BugReport { toReport :: Maybe FilePath } deriving Show @@ -26,3 +61,55 @@ parseBugReport = <> help "Whether to report a bug" ) ) + +{- | Create a @.tar.gz@ archive containing the bug report. + -} +writeBugReportArchive + :: FilePath -- ^ Directory to archive + -> FilePath -- ^ Name of the archive file, without extension. + -> IO () +writeBugReportArchive base tar = do + contents <- listDirectory base + let filename = tar <.> "tar" <.> "gz" + ByteString.Lazy.writeFile filename . GZip.compress . Tar.write + =<< Tar.pack base contents + (hPutStrLn stderr . unwords) ["Created bug report:", filename] + +{- | Run the inner action with a temporary directory holding the bug report. + +The bug report will be saved as an archive if that was requested by the user, or +if there is an error in the inner action. + + -} +withBugReport + :: ExeName + -> BugReport + -> (FilePath -> IO ExitCode) + -> IO ExitCode +withBugReport exeName bugReport act = do + (exitCode, _) <- + generalBracket + acquireTempDirectory + releaseTempDirectory + act + pure exitCode + where + acquireTempDirectory = do + tmp <- getCanonicalTemporaryDirectory + createTempDirectory tmp (getExeName exeName) + releaseTempDirectory tmpDir exitCase = do + case exitCase of + ExitCaseSuccess _ -> optionalWriteBugReport tmpDir + ExitCaseException someException -> do + let message = displayException someException + writeFile (tmpDir "error" <.> "log") message + alwaysWriteBugReport tmpDir + ExitCaseAbort -> alwaysWriteBugReport tmpDir + removePathForcibly tmpDir + alwaysWriteBugReport tmpDir = + writeBugReportArchive tmpDir + (fromMaybe (getExeName exeName) (toReport bugReport)) + optionalWriteBugReport tmpDir = + Foldable.traverse_ + (writeBugReportArchive tmpDir) + (toReport bugReport) diff --git a/kore/src/Kore/Log.hs b/kore/src/Kore/Log.hs index 3d09b39655..f0eb8eab18 100644 --- a/kore/src/Kore/Log.hs +++ b/kore/src/Kore/Log.hs @@ -15,15 +15,12 @@ module Kore.Log , Colog.logTextStderr , Colog.logTextHandle , runKoreLog - , archiveDirectoryReport , module Log , module KoreLogOptions ) where import Prelude.Kore -import qualified Codec.Archive.Tar as Tar -import qualified Codec.Compression.GZip as GZip import Colog ( LogAction (..) ) @@ -53,7 +50,6 @@ import Control.Monad.Cont ( ContT (..) , runContT ) -import qualified Data.ByteString.Lazy as BS import Data.Foldable ( toList ) @@ -93,17 +89,10 @@ import Kore.Log.Registry ) import Kore.Log.SQLite import Log -import System.Directory - ( listDirectory - ) -import System.FilePath.Posix +import System.FilePath ( (<.>) , () ) -import System.IO - ( hPutStrLn - , stderr - ) -- | Internal type used to add timestamps to a 'LogMessage'. data WithTimestamp = WithTimestamp ActualEntry LocalTime @@ -336,13 +325,3 @@ swappableLogger mvar = acquire = liftIO $ takeMVar mvar release = liftIO . putMVar mvar worker a logAction = Colog.unLogAction logAction a - -archiveDirectoryReport - :: FilePath -- ^ Path of the \".tar.gz\" file to write. - -> FilePath -- ^ Directory to archive - -> IO () -archiveDirectoryReport tar base = do - contents <- listDirectory base - BS.writeFile (tar <> ".tar.gz") . GZip.compress . Tar.write - =<< Tar.pack base contents - hPutStrLn stderr $ "\nCreated " <> tar <> ".tar.gz" diff --git a/kore/src/Kore/Repl/Interpreter.hs b/kore/src/Kore/Repl/Interpreter.hs index 65beaee813..036c7d726b 100644 --- a/kore/src/Kore/Repl/Interpreter.hs +++ b/kore/src/Kore/Repl/Interpreter.hs @@ -122,7 +122,7 @@ import System.Directory , findExecutable ) import System.Exit -import System.FilePath.Posix +import System.FilePath ( splitFileName , (<.>) ) diff --git a/test/include.mk b/test/include.mk index a50827ef8a..89ef06db34 100644 --- a/test/include.mk +++ b/test/include.mk @@ -66,6 +66,7 @@ $(DEF_KORE_DEFAULT): $(DEF_DIR)/$(DEF).k $(K) %.$(EXT).out: $(TEST_DIR)/%.$(EXT) $(TEST_DEPS) @echo ">>>" $(CURDIR) "krun" $< + @echo "KORE_EXEC_OPTS =" $(KORE_EXEC_OPTS) rm -f $@ $(KRUN) $(KRUN_OPTS) $< --output-file $@ 2>/dev/null $(DIFF) $@.golden $@ || $(FAILED) @@ -99,6 +100,7 @@ PATTERN_OPTS = --pattern "$$(cat $*.k)" %-spec.k.out: $(TEST_DIR)/%-spec.k $(TEST_DEPS) @echo ">>>" $(CURDIR) "kprove" $< + @echo "KORE_EXEC_OPTS =" $(KORE_EXEC_OPTS) rm -f $@ $(if $(STORE_PROOFS),rm -f $(STORE_PROOFS),$(if $(RECALL_PROOFS),cp $(RECALL_PROOFS) $(@:.out=.save-proofs.kore))) $(KPROVE) $(KPROVE_OPTS) $(KPROVE_SPEC) 2>/dev/null >$@ || true