Clean up --bug-report option (#1876)

* hlint: Forbid importing System.FilePath.Posix

* Extract common functions to Kore.BugReport

* withBugReport: Re-throw exceptions

* test/include.mk: Print KORE_EXEC_OPTS

* kore-exec: Only write saved proofs file if given as input

* gitignore: kore-exec.tar.gz

* withBugReport: Re-throw exceptions

* withBugReport: ExeName argument

Author: ttuegel

.gitignore

@@ -47,4 +47,4 @@ cabal.project.local
 /shell.local.nix
 /TAGS
 /.TAGS*
-report-*/
+kore-exec.tar.gz

.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

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

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

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)

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"

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
     , (<.>)
     )