From 2ff4d642f916d3f9e9f5c5fb92bd551dd6d00577 Mon Sep 17 00:00:00 2001
From: Kevin Quick <kquick@galois.com>
Date: Sat, 16 Jan 2021 23:33:00 -0800
Subject: [PATCH] [crucible] Add deadman timeout for online solver actions

Fixes https://github.com/GaloisInc/crucible/issues/439 by implementing
a parallel timeout operation (at 1 second longer than the timeout
requested of the solver itself) whose expiration causes the solver
process to be killed.

This helps with issue 439 because Yices encounters some internal
divergence issue that is not stopped by the specified timeout
value (demonstrable by running the crux-llvm
test-data/golden/strlen_test2 with the Yices solver option).

This also helps provide timeout management for solvers that do not
provide a built-in timeout capability (like Boolector).
---
 crucible/crucible.cabal                      |  1 +
 crucible/src/Lang/Crucible/Backend/Online.hs | 52 +++++++++++++++-----
 2 files changed, 40 insertions(+), 13 deletions(-)

diff --git a/crucible/crucible.cabal b/crucible/crucible.cabal
index 1d036f0d6..92e14f341 100644
--- a/crucible/crucible.cabal
+++ b/crucible/crucible.cabal
@@ -27,6 +27,7 @@ flag unsafe-operations
 
 library
   build-depends:
+    async,
     base >= 4.8 && < 4.15,
     bimap,
     bv-sized >= 1.0.0 && < 1.1,
diff --git a/crucible/src/Lang/Crucible/Backend/Online.hs b/crucible/src/Lang/Crucible/Backend/Online.hs
index d80949205..79d4cc9a1 100644
--- a/crucible/src/Lang/Crucible/Backend/Online.hs
+++ b/crucible/src/Lang/Crucible/Backend/Online.hs
@@ -74,6 +74,9 @@ module Lang.Crucible.Backend.Online
   ) where
 
 
+import           Control.Concurrent ( threadDelay )
+import           Control.Concurrent.Async ( race )
+import           Control.Exception ( throwIO )
 import           Control.Lens
 import           Control.Monad
 import           Control.Monad.Catch
@@ -83,11 +86,11 @@ import           Data.Data (Data)
 import           Data.Foldable
 import           Data.IORef
 import           Data.Parameterized.Nonce
+import qualified Data.Text as Text
 import           Data.Typeable (Typeable)
 import           GHC.Generics (Generic)
-import           System.IO
-import qualified Data.Text as Text
 import qualified Prettyprinter as PP
+import           System.IO
 
 import           What4.Config
 import           What4.Concrete
@@ -422,17 +425,40 @@ withSolverProcess' getSolver sym def action = do
                     writeIORef (solverProc st) (SolverStarted p auxh)
                     return (p, auxh)
 
-        case solverErrorBehavior p of
-          ContinueOnError ->
-            action p
-          ImmediateExit ->
-            onException
-              (action p)
-              ((killSolver p)
-                `finally`
-               (maybe (return ()) hClose auxh)
-                `finally`
-               (writeIORef (solverProc st) SolverNotStarted))
+        let stopTheSolver =
+              (killSolver p)
+              `finally`
+              (maybe (return ()) hClose auxh)
+              `finally`
+              (writeIORef (solverProc st) SolverNotStarted)
+
+        let doAction =
+              case solverErrorBehavior p of
+                ContinueOnError ->
+                  action p
+                ImmediateExit ->
+                  onException (action p) stopTheSolver
+
+        if (getGoalTimeoutInSeconds $ solverGoalTimeout p) == 0
+          then doAction
+          else let deadmanTimeoutPeriod = (fromInteger $
+                                           getGoalTimeoutInMilliSeconds
+                                           (solverGoalTimeout p) + 1000) * 1000
+                   -- If the solver cannot voluntarily limit itself to
+                   -- the requested timeout period, an async process
+                   -- running slightly longer will forcibly terminate
+                   -- the solver process.
+                   deadmanTimeout = threadDelay deadmanTimeoutPeriod >> stopTheSolver
+               in race deadmanTimeout doAction >>=
+                  either (const $ throwIO RunawaySolverTimeout) return
+
+
+-- | The RunawaySolverTimeout is thrown when the solver cannot
+-- voluntarily limit itself to the requested solver-timeout period and
+-- has subsequently been forcibly stopped.
+data RunawaySolverTimeout = RunawaySolverTimeout deriving Show
+instance Exception RunawaySolverTimeout
+
 
 -- | Get the solver process, specialized to @OnlineBackend@.
 --   Starts the solver, if that hasn't