Add timeouts to obligation proving

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

@@ -21,7 +21,7 @@ module Lang.Crucible.CLI
   ) where
 
 import Control.Monad
-
+import Control.Monad.Except (runExceptT)
 import Data.Foldable
 import Data.Map (Map)
 import Data.Text (Text)
@@ -54,6 +54,8 @@ import Lang.Crucible.Backend.Simple
 import Lang.Crucible.FunctionHandle
 import Lang.Crucible.Simulator
 import Lang.Crucible.Simulator.Profiling
+import qualified Lang.Crucible.Utils.Seconds as Sec
+import qualified Lang.Crucible.Utils.Timeout as CTO
 
 import What4.Config
 import What4.Interface (getConfiguration)
@@ -181,14 +183,21 @@ simulateProgramWithExtension mkExt fn theInput outh profh opts hooks =
                        getProofObligations bak >>= \case
                          Nothing -> hPutStrLn outh "==== No proof obligations ===="
                          Just {} -> hPutStrLn outh "==== Proof obligations ===="
-                       let prover = Prove.offlineProver sym defaultLogData z3Adapter
+                       -- TODO: Make this timeout configurable via the CLI
+                       let timeout = CTO.Timeout (Sec.secondsFromInt 5)
+                       let prover = Prove.offlineProver timeout sym defaultLogData z3Adapter
                        let strat = Prove.ProofStrategy prover Prove.keepGoing
-                       Prove.proveCurrentObligations bak strat $ Prove.ProofConsumer $ \goal res -> do
+                       merr <- runExceptT $ Prove.proveCurrentObligations bak strat $ Prove.ProofConsumer $ \goal res -> do
                          hPrint outh =<< ppProofObligation sym goal
                          case res of
                            Prove.Proved {} -> hPutStrLn outh "PROVED"
                            Prove.Disproved {} -> hPutStrLn outh "COUNTEREXAMPLE"
                            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

@@ -27,6 +27,7 @@ import           GHC.TypeNats
 import           Control.Lens ( (^.) )
 
 import           Control.Monad (foldM )
+import           Control.Monad.Except (runExceptT)
 import           Control.Monad.IO.Class (liftIO)
 import qualified Data.Map as Map
 import qualified Data.Parameterized.Context as Ctx
@@ -51,6 +52,8 @@ import qualified Lang.Crucible.Simulator as CS
 import qualified Lang.Crucible.Simulator.OverrideSim as CSO
 import qualified Lang.Crucible.FunctionHandle as CFH
 import qualified Lang.Crucible.Simulator.GlobalState as CGS
+import qualified Lang.Crucible.Utils.Seconds as Sec
+import qualified Lang.Crucible.Utils.Timeout as CTO
 
 import qualified What4.Interface as W4
 import qualified What4.Expr as WE
@@ -134,9 +137,10 @@ runFSTest' bak (FSTest fsTest) = do
           putStrLn $ showF p
           T.assertFailure "Partial Result"
 
-  let prover = CB.offlineProver sym WSA.defaultLogData W4Y.yicesAdapter
+  let timeout = CTO.Timeout (Sec.secondsFromInt 5)
+  let prover = CB.offlineProver timeout sym WSA.defaultLogData W4Y.yicesAdapter
   let strat = CB.ProofStrategy prover CB.failFast
-  CB.proveCurrentObligations bak strat $ CB.ProofConsumer $ \obligation ->
+  merr <- runExceptT $ CB.proveCurrentObligations bak strat $ CB.ProofConsumer $ \obligation ->
     \case
       CB.Proved {} -> return ()
       CB.Unknown {} -> T.assertFailure "Inconclusive"
@@ -147,6 +151,10 @@ runFSTest' bak (FSTest fsTest) = do
         putStrLn (showF asmsPred)
         putStrLn (showF goalPred)
         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
 showAbortedResult ar = case ar of

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

@@ -10,6 +10,7 @@ module Lang.Crucible.Syntax.Overrides
   ) where
 
 import Control.Lens hiding ((:>), Empty)
+import Control.Monad.Except (runExceptT)
 import Control.Monad.IO.Class
 import System.IO
 
@@ -25,6 +26,8 @@ import qualified Lang.Crucible.Backend.Prove as CB
 import Lang.Crucible.Types
 import Lang.Crucible.FunctionHandle
 import Lang.Crucible.Simulator
+import qualified Lang.Crucible.Utils.Seconds as Sec
+import qualified Lang.Crucible.Utils.Timeout as CTO
 
 
 setupOverrides ::
@@ -48,12 +51,17 @@ proveObligations =
 
        let logData = defaultLogData { logCallbackVerbose = \_ -> hPutStrLn h
                                     , logReason = "assertion proof" }
-       let prover = CB.offlineProver sym logData z3Adapter
+       let timeout = CTO.Timeout (Sec.secondsFromInt 5)
+       let prover = CB.offlineProver timeout sym logData z3Adapter
        let strat = CB.ProofStrategy prover CB.keepGoing
-       CB.proveCurrentObligations bak strat $ CB.ProofConsumer $ \o ->
+       merr <- runExceptT $ CB.proveCurrentObligations bak strat $ CB.ProofConsumer $ \o ->
          \case
            CB.Proved {}  -> hPutStrLn h $ unlines ["Proof Succeeded!", show $ ppSimError $ (proofGoal o)^.labeledPredMsg]
            CB.Disproved {} -> hPutStrLn h $ unlines ["Proof failed!", show $ ppSimError $ (proofGoal o)^.labeledPredMsg]
            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/crucible.cabal

@@ -44,6 +44,7 @@ common bldflags
 library
   import: bldflags
   build-depends:
+    async,
     base >= 4.13 && < 4.19,
     bimap,
     bv-sized >= 1.0.0 && < 1.1,
@@ -129,6 +130,8 @@ library
     Lang.Crucible.Utils.MuxTree
     Lang.Crucible.Utils.PrettyPrint
     Lang.Crucible.Utils.RegRewrite
+    Lang.Crucible.Utils.Seconds
+    Lang.Crucible.Utils.Timeout
     Lang.Crucible.Utils.StateContT
     Lang.Crucible.Utils.Structural
 

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

@@ -58,6 +58,7 @@ module Lang.Crucible.Backend.Prove
   , Prover(..)
     -- *** Offline
   , offlineProve
+  , offlineProveWithTimeout
   , offlineProver
     -- *** Online
   , onlineProve
@@ -70,6 +71,7 @@ module Lang.Crucible.Backend.Prove
 
 import           Control.Lens ((^.))
 import           Control.Monad.Catch (MonadMask)
+import           Control.Monad.Error.Class (MonadError, liftEither)
 import           Control.Monad.IO.Class (MonadIO(liftIO))
 import qualified Control.Monad.Reader as Reader
 
@@ -82,6 +84,8 @@ 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 qualified Lang.Crucible.Utils.Timeout as CTO
 
 -- | Local helper
 consumeGoals ::
@@ -216,8 +220,8 @@ data Prover sym m t r
 ---------------------------------------------------------------------
 -- *** Offline
 
-offlineProve ::
-  MonadIO m =>
+-- Not exported
+offlineProveIO ::
   (sym ~ WE.ExprBuilder t st fs) =>
   W4.IsSymExprBuilder sym =>
   sym ->
@@ -226,8 +230,8 @@ offlineProve ::
   Assumptions sym ->
   CB.Assertion sym ->
   ProofConsumer sym t r ->
-  m (SubgoalResult r)
-offlineProve sym ld adapter asmps goal (ProofConsumer k) = liftIO $ do
+  IO (SubgoalResult r)
+offlineProveIO sym ld adapter asmps goal (ProofConsumer k) = do
   let goalPred = goal ^. CB.labeledPred
   asmsPred <- CB.assumptionsPred sym asmps
   notGoal <- W4.notPred sym goalPred
@@ -239,17 +243,50 @@ offlineProve sym ld adapter asmps goal (ProofConsumer k) = liftIO $ do
             W4R.Unknown -> Unknown
     in SubgoalResult (isProved r') <$> k (CB.ProofGoal asmps goal) r'
 
+offlineProve ::
+  MonadIO m =>
+  (sym ~ WE.ExprBuilder t st fs) =>
+  W4.IsSymExprBuilder sym =>
+  sym ->
+  WSA.LogData ->
+  WSA.SolverAdapter st ->
+  Assumptions sym ->
+  CB.Assertion sym ->
+  ProofConsumer sym t r ->
+  m (SubgoalResult r)
+offlineProve sym ld adapter asmps goal k =
+  liftIO (offlineProveIO sym ld adapter asmps goal k)
+
+offlineProveWithTimeout ::
+  MonadError TimeoutError m =>
+  MonadIO m =>
+  (sym ~ WE.ExprBuilder t st fs) =>
+  W4.IsSymExprBuilder sym =>
+  Timeout ->
+  sym ->
+  WSA.LogData ->
+  WSA.SolverAdapter st ->
+  Assumptions sym ->
+  CB.Assertion sym ->
+  ProofConsumer sym t r ->
+  m (SubgoalResult r)
+offlineProveWithTimeout to sym ld adapter asmps goal k = do
+  r <- liftIO (CTO.withTimeout to (offlineProveIO sym ld adapter asmps goal k))
+  liftEither r
+
 offlineProver ::
+  MonadError TimeoutError m =>
   MonadIO m =>
   (sym ~ WE.ExprBuilder t st fs) =>
+  Timeout ->
   W4.IsSymExprBuilder sym =>
   sym ->
   WSA.LogData ->
   WSA.SolverAdapter st ->
   Prover sym m t r
-offlineProver sym ld adapter =
+offlineProver to sym ld adapter =
   Prover
-  { proverProve = offlineProve sym ld adapter
+  { proverProve = offlineProveWithTimeout to sym ld adapter
   , proverAssume = \_asmps a -> a
   }
 

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

@@ -0,0 +1,18 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+
+module Lang.Crucible.Utils.Seconds
+  ( Seconds
+  , secondsToInt
+  , secondsFromInt
+  , secondsToMicroseconds
+  ) where
+
+newtype Seconds = Seconds { secondsToInt :: Int }
+  deriving (Eq, Num, Ord, Show)
+
+-- | Inverse of 'secondsToInt'
+secondsFromInt :: Int -> Seconds
+secondsFromInt = Seconds
+
+secondsToMicroseconds :: Seconds -> Int
+secondsToMicroseconds = (* 1000000) . secondsToInt

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

@@ -0,0 +1,58 @@
+module Lang.Crucible.Utils.Timeout
+  ( Timeout(..)
+  , TimeoutError(..)
+  , 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
+
+-- | A timeout, in seconds.
+newtype Timeout = Timeout { getTimeout :: Secs.Seconds }
+  deriving (Eq, Ord, Show)
+
+-- Private, not exported
+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
+  deriving Show
+
+-- | Execute a task with a timeout.
+--
+-- Catches any exceptions that occur during the task, returning them as
+-- @'Left' ('Exception' exn)@.
+withTimeout ::
+  -- | Timeout duration (seconds)
+  Timeout ->
+  -- | Task to attempt
+  IO a ->
+  IO (Either TimeoutError 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)
+