Fix reporting of processing time (tamarin-prover#517)

Fixes a regression introduced in tamarin-prover#484 where the processing time was incorrectly measured due to the missing full evaluation of the IO action. Additionally, the precission of the reported time is now set to 2.

lib/utils/src/System/Timing.hs

@@ -1,27 +1,34 @@
 -- |
--- Copyright   : (c) 2011 Simon Meier
+-- Copyright   : (c) 2011 Simon Meier, 2022 Kevin Morio
 -- License     : GPL v3 (see LICENSE)
 --
 -- Maintainer  : Simon Meier <iridcode@gmail.com>
 -- Portability : GHC only
 --
--- A simple module for timing IO action.
+-- A simple module for timing IO actions and evaluation of values.
 module System.Timing (
-    timed
-  , timed_
+    timedIO
+  , timed
 ) where
 
-import           Control.Monad
-import           Data.Time.Clock
+import Data.Time.Clock ( diffUTCTime, getCurrentTime, NominalDiffTime )
+import GHC.IO (unsafePerformIO)
+import Control.DeepSeq ( NFData, deepseq )
 
--- | Execute an IO action and return its result plus the time it took to execute it.
-timed :: IO a -> IO (a, NominalDiffTime)
-timed io = do
-  t0 <- getCurrentTime
-  x <- io
-  t1 <- getCurrentTime
-  return (x, diffUTCTime t1 t0)
+-- | Fully evaluate an IO action and measure its execution time.
+timedIO :: NFData a => IO a -> IO (a, NominalDiffTime)
+timedIO mx = do
+    t0 <- getCurrentTime
+    val <- mx
+    t1 <- val `deepseq` getCurrentTime
+    let measure = t1 `diffUTCTime` t0
+    return (val, measure)
 
--- | Execute an IO action and return the time it took to execute it.
-timed_ :: IO a -> IO NominalDiffTime
-timed_ = (snd `liftM`) . timed
+-- | Fully evaluate a value and measure its execution time.
+timed :: NFData a => a -> (a, NominalDiffTime)
+timed x =
+    let measure = unsafePerformIO $ do
+                    t0 <- getCurrentTime
+                    t1 <- x `deepseq` getCurrentTime
+                    return (t1 `diffUTCTime` t0)
+    in (x, measure)

src/Main/Mode/Batch.hs

@@ -16,7 +16,7 @@ import           Data.List
 import           Data.Bitraversable              (bisequence)
 import           System.Console.CmdArgs.Explicit as CmdArgs
 import           System.FilePath
-import           System.Timing                   (timed)
+import           System.Timing                   (timedIO)
 import           Extension.Data.Label
 
 import qualified Text.PrettyPrint.Class          as Pretty
@@ -35,6 +35,7 @@ import           Theory.Module
 import           Control.Monad.Except (MonadIO(liftIO), runExceptT)
 import           System.Exit (die)
 import Theory.Tools.Wellformedness (prettyWfErrorReport)
+import           Text.Printf                     (printf)
 
 
 -- | Batch processing mode.
@@ -89,9 +90,8 @@ run thisMode as
       putStrLn ""
   | otherwise = do
       versionData <- ensureMaudeAndGetVersion as
-      res <- mapM (timed . processThy versionData) inFiles
-      let (thys, times) = unzip res
-      let (docs, reps) = unzip thys
+      resTimed <- mapM (timedIO . processThy versionData) inFiles
+      let (docs, reps, times) = unzip3 $ fmap (\((d, r), t) -> (d, r, t)) resTimed
 
       if writeOutput then do
         let maybeOutFiles = sequence $ mkOutPath <$> inFiles
@@ -125,7 +125,7 @@ run thisMode as
                   , Pretty.text $ ""
                   , Pretty.nest 2 $ Pretty.vcat [
                       maybe Pretty.emptyDoc (\o -> Pretty.text $ "output:          " ++ o) outFile
-                    , Pretty.text $ "processing time: " ++ show time
+                    , Pretty.text $ printf "processing time: %.2fs" (realToFrac time :: Double)
                     , Pretty.text $ ""
                     , summary ] ]