From 00136e1b1e90bc185eceb3d069216688cb219df3 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Tue, 9 Jun 2020 14:26:45 -0500 Subject: [PATCH 1/8] hlint: Forbid importing System.FilePath.Posix --- .hlint.yaml | 1 + kore/src/Kore/Log.hs | 2 +- kore/src/Kore/Repl/Interpreter.hs | 2 +- 3 files changed, 3 insertions(+), 2 deletions(-) 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/src/Kore/Log.hs b/kore/src/Kore/Log.hs index 3d09b39655..0305832f4f 100644 --- a/kore/src/Kore/Log.hs +++ b/kore/src/Kore/Log.hs @@ -96,7 +96,7 @@ import Log import System.Directory ( listDirectory ) -import System.FilePath.Posix +import System.FilePath ( (<.>) , () ) 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 , (<.>) ) From 30552de475cb036373fa247a220b2f944bf37ddb Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Tue, 9 Jun 2020 14:45:34 -0500 Subject: [PATCH 2/8] Extract common functions to Kore.BugReport --- kore/app/exec/Main.hs | 48 ++++++------------ kore/app/repl/Main.hs | 101 ++++++++++++++++++------------------- kore/src/Kore/BugReport.hs | 83 ++++++++++++++++++++++++++++++ kore/src/Kore/Log.hs | 21 -------- 4 files changed, 148 insertions(+), 105 deletions(-) diff --git a/kore/app/exec/Main.hs b/kore/app/exec/Main.hs index a31db9e12b..a4f0f4ff3d 100644 --- a/kore/app/exec/Main.hs +++ b/kore/app/exec/Main.hs @@ -6,7 +6,6 @@ import Control.Monad.Catch ( MonadCatch , SomeException , displayException - , finally , handle , throwM ) @@ -73,6 +72,9 @@ import System.Exit ( ExitCode (..) , exitWith ) +import System.FilePath + ( () + ) import System.IO ( IOMode (WriteMode) , withFile @@ -81,9 +83,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 +116,6 @@ import Kore.Log , LogMessage , SomeEntry (..) , WithLog - , archiveDirectoryReport , logEntry , parseKoreLogOptions , runKoreLog @@ -178,12 +176,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 @@ -559,23 +553,18 @@ main = do 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 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 +610,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..065e840bc0 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 @@ -205,60 +205,59 @@ mainWithOptions , outputFile , koreLogOptions } - = - Temp.withSystemTempDirectory - "report" - $ \tempDirectory -> - withLogger tempDirectory koreLogOptions $ \actualLogAction -> do - mvarLogAction <- newMVar actualLogAction - let swapLogAction = swappableLogger mvarLogAction - flip runLoggerT swapLogAction $ do - definition <- loadDefinitions [definitionFileName, specFile] - indexedModule <- loadModule mainModuleName definition - specDefIndexedModule <- loadModule specModule definition + = do + exitCode <- withBugReport (BugReport Nothing) $ \tempDirectory -> + withLogger tempDirectory koreLogOptions $ \actualLogAction -> do + mvarLogAction <- newMVar actualLogAction + let swapLogAction = swappableLogger mvarLogAction + flip runLoggerT swapLogAction $ do + definition <- loadDefinitions [definitionFileName, specFile] + indexedModule <- loadModule mainModuleName definition + specDefIndexedModule <- loadModule specModule definition - let - smtConfig = - SMT.defaultConfig - { SMT.timeOut = smtTimeOut - , SMT.preludeFile = smtPrelude - } + let + smtConfig = + SMT.defaultConfig + { SMT.timeOut = smtTimeOut + , SMT.preludeFile = smtPrelude + } - when - ( replMode == RunScript - && isNothing (unReplScript replScript) - ) - $ lift $ do - putStrLn - "You must supply the path to the repl script\ - \ in order to run the repl in run-script mode." - exitFailure + when + ( replMode == RunScript + && isNothing (unReplScript replScript) + ) + $ lift $ do + putStrLn + "You must supply the path to the repl script\ + \ in order to run the repl in run-script mode." + exitFailure - when - ( replMode == Interactive - && scriptModeOutput == EnableOutput - ) - $ lift $ do - putStrLn - "The --save-run-output flag is only available\ - \ when running the repl in run-script mode." - exitFailure + when + ( replMode == Interactive + && scriptModeOutput == EnableOutput + ) + $ lift $ do + putStrLn + "The --save-run-output flag is only available\ + \ when running the repl in run-script mode." + exitFailure - SMT.runSMT smtConfig $ do - give (MetadataTools.build indexedModule) - $ declareSMTLemmas indexedModule - proveWithRepl - indexedModule - specDefIndexedModule - Nothing - mvarLogAction - replScript - replMode - scriptModeOutput - outputFile - mainModuleName - archiveDirectoryReport tempDirectory tempDirectory + SMT.runSMT smtConfig $ do + give (MetadataTools.build indexedModule) + $ declareSMTLemmas indexedModule + proveWithRepl + indexedModule + specDefIndexedModule + Nothing + mvarLogAction + replScript + replMode + scriptModeOutput + outputFile + mainModuleName + 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..9ed583e179 100644 --- a/kore/src/Kore/BugReport.hs +++ b/kore/src/Kore/BugReport.hs @@ -7,11 +7,43 @@ 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 + , handleAll + ) +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 + ) newtype BugReport = BugReport { toReport :: Maybe FilePath } deriving Show @@ -26,3 +58,54 @@ 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 :: BugReport -> (FilePath -> IO ExitCode) -> IO ExitCode +withBugReport bugReport act = + do + (exitCode, _) <- + generalBracket + acquireTempDirectory + releaseTempDirectory + act + pure exitCode + & handleAll (\_ -> pure (ExitFailure 1)) + where + acquireTempDirectory = do + tmp <- getCanonicalTemporaryDirectory + createTempDirectory tmp "kore-exec" + releaseTempDirectory tmpDir exitCase = do + case exitCase of + ExitCaseSuccess _ -> optionalWriteBugReport tmpDir + ExitCaseException someException -> do + writeFile + (tmpDir "error" <.> "log") + (displayException someException) + alwaysWriteBugReport tmpDir + ExitCaseAbort -> alwaysWriteBugReport tmpDir + removePathForcibly tmpDir + alwaysWriteBugReport tmpDir = + writeBugReportArchive tmpDir + (fromMaybe "kore-exec" $ 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 0305832f4f..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 ( (<.>) , () ) -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" From 43767ddbce41146f3d4846f644d64bedd90fd8bb Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Wed, 10 Jun 2020 08:47:55 -0500 Subject: [PATCH 3/8] withBugReport: Re-throw exceptions --- kore/src/Kore/BugReport.hs | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/kore/src/Kore/BugReport.hs b/kore/src/Kore/BugReport.hs index 9ed583e179..11906b9314 100644 --- a/kore/src/Kore/BugReport.hs +++ b/kore/src/Kore/BugReport.hs @@ -21,6 +21,7 @@ import Control.Monad.Catch , displayException , generalBracket , handleAll + , throwM ) import qualified Data.ByteString.Lazy as ByteString.Lazy import qualified Data.Foldable as Foldable @@ -96,10 +97,10 @@ withBugReport bugReport act = case exitCase of ExitCaseSuccess _ -> optionalWriteBugReport tmpDir ExitCaseException someException -> do - writeFile - (tmpDir "error" <.> "log") - (displayException someException) + let message = displayException someException + writeFile (tmpDir "error" <.> "log") message alwaysWriteBugReport tmpDir + throwM someException ExitCaseAbort -> alwaysWriteBugReport tmpDir removePathForcibly tmpDir alwaysWriteBugReport tmpDir = From 2a1f372730ff371b1286e15aa2962dfea4990464 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Wed, 10 Jun 2020 08:48:12 -0500 Subject: [PATCH 4/8] test/include.mk: Print KORE_EXEC_OPTS --- test/include.mk | 2 ++ 1 file changed, 2 insertions(+) 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 From 237081b599db61f337e364b9d7610a5379fec43a Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Wed, 10 Jun 2020 08:55:34 -0500 Subject: [PATCH 5/8] kore-exec: Only write saved proofs file if given as input --- kore/app/exec/Main.hs | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) diff --git a/kore/app/exec/Main.hs b/kore/app/exec/Main.hs index a4f0f4ff3d..01dc437793 100644 --- a/kore/app/exec/Main.hs +++ b/kore/app/exec/Main.hs @@ -9,9 +9,7 @@ import Control.Monad.Catch , handle , throwM ) -import Control.Monad.Trans - ( lift - ) +import Control.Monad.Extra as Monad import qualified Data.Char as Char import Data.Default ( def @@ -498,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 From 6cc10eb67ca3ff15ddc765ead71e314718cf1131 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Wed, 10 Jun 2020 08:56:02 -0500 Subject: [PATCH 6/8] gitignore: kore-exec.tar.gz --- .gitignore | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 From c8839a976b765012928494148f1c99b4d6ae168c Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Wed, 10 Jun 2020 10:59:45 -0500 Subject: [PATCH 7/8] withBugReport: Re-throw exceptions --- kore/src/Kore/BugReport.hs | 4 ---- 1 file changed, 4 deletions(-) diff --git a/kore/src/Kore/BugReport.hs b/kore/src/Kore/BugReport.hs index 11906b9314..1571b3c8b4 100644 --- a/kore/src/Kore/BugReport.hs +++ b/kore/src/Kore/BugReport.hs @@ -20,8 +20,6 @@ import Control.Monad.Catch ( ExitCase (..) , displayException , generalBracket - , handleAll - , throwM ) import qualified Data.ByteString.Lazy as ByteString.Lazy import qualified Data.Foldable as Foldable @@ -88,7 +86,6 @@ withBugReport bugReport act = releaseTempDirectory act pure exitCode - & handleAll (\_ -> pure (ExitFailure 1)) where acquireTempDirectory = do tmp <- getCanonicalTemporaryDirectory @@ -100,7 +97,6 @@ withBugReport bugReport act = let message = displayException someException writeFile (tmpDir "error" <.> "log") message alwaysWriteBugReport tmpDir - throwM someException ExitCaseAbort -> alwaysWriteBugReport tmpDir removePathForcibly tmpDir alwaysWriteBugReport tmpDir = From 3c53967b6c67395dc58ce355bfa97c01dbe2266d Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Wed, 10 Jun 2020 10:59:56 -0500 Subject: [PATCH 8/8] withBugReport: ExeName argument --- kore/app/exec/Main.hs | 8 +-- kore/app/repl/Main.hs | 99 ++++++++++++++++++++------------------ kore/src/Kore/BugReport.hs | 29 ++++++----- 3 files changed, 74 insertions(+), 62 deletions(-) diff --git a/kore/app/exec/Main.hs b/kore/app/exec/Main.hs index 01dc437793..d2a65546e3 100644 --- a/kore/app/exec/Main.hs +++ b/kore/app/exec/Main.hs @@ -545,19 +545,21 @@ 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 exitCode <- - withBugReport bugReport $ \tmpDir -> do + withBugReport Main.exeName bugReport $ \tmpDir -> do writeOptionsAndKoreFiles tmpDir execOptions go & handle handleWithConfiguration diff --git a/kore/app/repl/Main.hs b/kore/app/repl/Main.hs index 065e840bc0..143dd22f32 100644 --- a/kore/app/repl/Main.hs +++ b/kore/app/repl/Main.hs @@ -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 @@ -206,57 +208,58 @@ mainWithOptions , koreLogOptions } = do - exitCode <- withBugReport (BugReport Nothing) $ \tempDirectory -> - withLogger tempDirectory koreLogOptions $ \actualLogAction -> do - mvarLogAction <- newMVar actualLogAction - let swapLogAction = swappableLogger mvarLogAction - flip runLoggerT swapLogAction $ do - definition <- loadDefinitions [definitionFileName, specFile] - indexedModule <- loadModule mainModuleName definition - specDefIndexedModule <- loadModule specModule definition + exitCode <- + withBugReport Main.exeName (BugReport Nothing) $ \tempDirectory -> + withLogger tempDirectory koreLogOptions $ \actualLogAction -> do + mvarLogAction <- newMVar actualLogAction + let swapLogAction = swappableLogger mvarLogAction + flip runLoggerT swapLogAction $ do + definition <- loadDefinitions [definitionFileName, specFile] + indexedModule <- loadModule mainModuleName definition + specDefIndexedModule <- loadModule specModule definition - let - smtConfig = - SMT.defaultConfig - { SMT.timeOut = smtTimeOut - , SMT.preludeFile = smtPrelude - } + let + smtConfig = + SMT.defaultConfig + { SMT.timeOut = smtTimeOut + , SMT.preludeFile = smtPrelude + } - when - ( replMode == RunScript - && isNothing (unReplScript replScript) - ) - $ lift $ do - putStrLn - "You must supply the path to the repl script\ - \ in order to run the repl in run-script mode." - exitFailure + when + ( replMode == RunScript + && isNothing (unReplScript replScript) + ) + $ lift $ do + putStrLn + "You must supply the path to the repl script\ + \ in order to run the repl in run-script mode." + exitFailure - when - ( replMode == Interactive - && scriptModeOutput == EnableOutput - ) - $ lift $ do - putStrLn - "The --save-run-output flag is only available\ - \ when running the repl in run-script mode." - exitFailure + when + ( replMode == Interactive + && scriptModeOutput == EnableOutput + ) + $ lift $ do + putStrLn + "The --save-run-output flag is only available\ + \ when running the repl in run-script mode." + exitFailure - SMT.runSMT smtConfig $ do - give (MetadataTools.build indexedModule) - $ declareSMTLemmas indexedModule - proveWithRepl - indexedModule - specDefIndexedModule - Nothing - mvarLogAction - replScript - replMode - scriptModeOutput - outputFile - mainModuleName + SMT.runSMT smtConfig $ do + give (MetadataTools.build indexedModule) + $ declareSMTLemmas indexedModule + proveWithRepl + indexedModule + specDefIndexedModule + Nothing + mvarLogAction + replScript + replMode + scriptModeOutput + outputFile + mainModuleName - pure ExitSuccess + pure ExitSuccess exitWith exitCode where mainModuleName :: ModuleName diff --git a/kore/src/Kore/BugReport.hs b/kore/src/Kore/BugReport.hs index 1571b3c8b4..eff8448062 100644 --- a/kore/src/Kore/BugReport.hs +++ b/kore/src/Kore/BugReport.hs @@ -44,6 +44,10 @@ import System.IO.Temp , getCanonicalTemporaryDirectory ) +import Kore.Log.KoreLogOptions + ( ExeName (..) + ) + newtype BugReport = BugReport { toReport :: Maybe FilePath } deriving Show @@ -77,19 +81,22 @@ 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 :: BugReport -> (FilePath -> IO ExitCode) -> IO ExitCode -withBugReport bugReport act = - do - (exitCode, _) <- - generalBracket - acquireTempDirectory - releaseTempDirectory - act - pure exitCode +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 "kore-exec" + createTempDirectory tmp (getExeName exeName) releaseTempDirectory tmpDir exitCase = do case exitCase of ExitCaseSuccess _ -> optionalWriteBugReport tmpDir @@ -101,7 +108,7 @@ withBugReport bugReport act = removePathForcibly tmpDir alwaysWriteBugReport tmpDir = writeBugReportArchive tmpDir - (fromMaybe "kore-exec" $ toReport bugReport) + (fromMaybe (getExeName exeName) (toReport bugReport)) optionalWriteBugReport tmpDir = Foldable.traverse_ (writeBugReportArchive tmpDir)