Simplify obligation-proving timeouts by not catching exceptions

crucible-cli/src/Lang/Crucible/CLI.hs

@@ -195,8 +195,6 @@ simulateProgramWithExtension mkExt fn theInput outh profh opts hooks =
                            Prove.Unknown {} -> hPutStrLn outh "UNKNOWN"
                        case merr of
                          Left CTO.TimedOut -> hPutStrLn outh $ unlines ["TIMEOUT"]
-                         Left (CTO.Exception exn) ->
-                          hPutStrLn outh $ unlines ["EXCEPTION", show exn]
                          Right () -> pure ()
 
                   _ -> hPutStrLn outh "No suitable main function found"

crucible-symio/tests/TestMain.hs

@@ -153,7 +153,6 @@ runFSTest' bak (FSTest fsTest) = do
         T.assertFailure "Assertion Failure"
   case merr of
     Left CTO.TimedOut -> T.assertFailure "Timeout"
-    Left (CTO.Exception exn) -> T.assertFailure ("Exception: " ++ show exn)
     Right () -> pure ()
 
 showAbortedResult :: CS.AbortedResult c d -> String

crucible-syntax/src/Lang/Crucible/Syntax/Overrides.hs

@@ -61,7 +61,6 @@ proveObligations =
            CB.Unknown {} -> hPutStrLn h $ unlines ["Proof inconclusive!", show $ ppSimError $ (proofGoal o)^.labeledPredMsg]
        case merr of
          Left CTO.TimedOut -> hPutStrLn h $ unlines ["Proof timed out!"]
-         Left (CTO.Exception exn) -> hPutStrLn h $ unlines ["Exception during proof!", show exn]
          Right () -> pure ()
 
        clearProofObligations bak

crucible/src/Lang/Crucible/Backend/Prove.hs

@@ -84,7 +84,7 @@ import qualified What4.Solver.Adapter as WSA
 
 import qualified Lang.Crucible.Backend as CB
 import           Lang.Crucible.Backend.Assumptions (Assumptions)
-import           Lang.Crucible.Utils.Timeout (Timeout, TimeoutError)
+import           Lang.Crucible.Utils.Timeout (Timeout, TimedOut)
 import qualified Lang.Crucible.Utils.Timeout as CTO
 
 -- | Local helper
@@ -258,7 +258,7 @@ offlineProve sym ld adapter asmps goal k =
   liftIO (offlineProveIO sym ld adapter asmps goal k)
 
 offlineProveWithTimeout ::
-  MonadError TimeoutError m =>
+  MonadError TimedOut m =>
   MonadIO m =>
   (sym ~ WE.ExprBuilder t st fs) =>
   W4.IsSymExprBuilder sym =>
@@ -275,7 +275,7 @@ offlineProveWithTimeout to sym ld adapter asmps goal k = do
   liftEither r
 
 offlineProver ::
-  MonadError TimeoutError m =>
+  MonadError TimedOut m =>
   MonadIO m =>
   (sym ~ WE.ExprBuilder t st fs) =>
   Timeout ->

crucible/src/Lang/Crucible/Utils/Timeout.hs

@@ -1,12 +1,11 @@
 module Lang.Crucible.Utils.Timeout
   ( Timeout(..)
-  , TimeoutError(..)
+  , TimedOut(..)
   , withTimeout
   ) where
 
 import qualified Control.Concurrent as CC
 import qualified Control.Concurrent.Async as CCA
-import           Control.Exception.Base (SomeException)
 
 import qualified Lang.Crucible.Utils.Seconds as Secs
 
@@ -18,41 +17,22 @@ newtype Timeout = Timeout { getTimeout :: Secs.Seconds }
 timeoutToMicros :: Timeout -> Int
 timeoutToMicros = Secs.secondsToMicroseconds . getTimeout
 
--- Private, not exported
-data DidTimeOut = DidTimeOut
-
--- | An error resulting from 'withTimeout'.
-data TimeoutError
-  = -- | The task timed out
-    TimedOut
-    -- | Some other exception ocurred
-  | Exception SomeException
+-- | A task timed out.
+data TimedOut = TimedOut
   deriving Show
 
 -- | Execute a task with a timeout.
 --
--- Catches any exceptions that occur during the task, returning them as
--- @'Left' ('Exception' exn)@.
+-- Implemented via 'CCA.race', so re-throws exceptions that occur during the
+-- task (if it completes before the timeout).
 withTimeout ::
   -- | Timeout duration (seconds)
   Timeout ->
   -- | Task to attempt
   IO a ->
-  IO (Either TimeoutError a)
+  IO (Either TimedOut a)
 withTimeout to task = do
-  worker <- CCA.async task
-  timeout <- CCA.async $ do
-    CC.threadDelay (timeoutToMicros to)
-    CCA.cancel worker
-    return DidTimeOut
-  res <- CCA.waitEitherCatch timeout worker
-  case res of
-    Left (Right DidTimeOut) -> do
-      return (Left TimedOut)
-    Left (Left exn) -> do
-      return (Left (Exception exn))
-    Right (Left exn) -> do
-      return (Left (Exception exn))
-    Right (Right val) ->
-      return (Right val)
-
+  let timeout = do
+        CC.threadDelay (timeoutToMicros to)
+        pure TimedOut
+  CCA.race timeout task