[crucible] Add deadman timeout for online solver actions

Fixes #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

@@ -27,6 +27,7 @@ flag unsafe-operations
 
 library
   build-depends:
+    async,
     base >= 4.8 && < 4.15,
     bimap,
     bv-sized >= 1.0.0 && < 1.1,

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