Use an IORef to hold a reference to the solver/solverClose (#3977)

Fixes (hopefully) #3959 by making the `solver`/`solverClose` handles
into an `IORef`. This way, we can be (reasonably) sure that when we
write the new handles into the `IORef`, there will be no other
references held to the old ones elsewhere, which was previously
preventing the old z3 instance from terminating, leaving a zombie
process.

---------

Co-authored-by: github-actions <[email protected]>

Author: goodlyrottenapple

booster/library/Booster/SMT/Interface.hs

@@ -28,6 +28,7 @@ import Data.Coerce
 import Data.Data (Proxy)
 import Data.Either (isLeft)
 import Data.Either.Extra (fromLeft', fromRight')
+import Data.IORef
 import Data.Map (Map)
 import Data.Map qualified as Map
 import Data.Set (Set)
@@ -111,11 +112,14 @@ swapSmtOptions smtOptions = do
 -- | Stop the solver, initialise a new one and put in the @SMTContext@
 hardResetSolver :: forall io. Log.LoggerMIO io => SMTOptions -> SMT io ()
 hardResetSolver smtOptions = do
-    Log.logMessage ("Starting new SMT solver" :: Text)
+    Log.logMessage ("Restarting SMT solver" :: Text)
     ctxt <- SMT get
-    liftIO ctxt.solverClose
+    liftIO $ join $ readIORef ctxt.solverClose
     (solver, handle) <- connectToSolver
-    SMT $ put ctxt{solver, solverClose = Backend.close handle}
+    liftIO $ do
+        writeIORef ctxt.solver solver
+        writeIORef ctxt.solverClose $ Backend.close handle
+
     checkPrelude
     swapSmtOptions smtOptions
 

booster/library/Booster/SMT/Runner.hs

@@ -29,6 +29,7 @@ import Control.Monad.Logger
 import Control.Monad.Trans.State
 import Data.ByteString.Builder qualified as BS
 import Data.ByteString.Char8 qualified as BS
+import Data.IORef
 import Data.Text (Text, pack)
 import SMTLIB.Backends qualified as Backend
 import SMTLIB.Backends.Process qualified as Backend
@@ -72,8 +73,10 @@ defaultSMTOptions =
 
 data SMTContext = SMTContext
     { options :: SMTOptions
-    , solver :: Backend.Solver
-    , solverClose :: IO ()
+    , -- use IORef here to ensure we only ever retain one pointer to the solver,
+      -- otherwise the solverClose action does not actually terminate the solver instance
+      solver :: IORef Backend.Solver
+    , solverClose :: IORef (IO ())
     , mbTranscriptHandle :: Maybe Handle
     , prelude :: [DeclareCommand]
     }
@@ -93,7 +96,9 @@ mkContext ::
     io SMTContext
 mkContext opts prelude = do
     logMessage ("Starting SMT solver" :: Text)
-    (solver, handle) <- connectToSolver
+    (solver', handle) <- connectToSolver
+    solver <- liftIO $ newIORef solver'
+    solverClose <- liftIO $ newIORef $ Backend.close handle
     mbTranscriptHandle <- forM opts.transcript $ \path -> do
         logMessage $ "Transcript in file " <> pack path
         liftIO $ do
@@ -107,7 +112,7 @@ mkContext opts prelude = do
     pure
         SMTContext
             { solver
-            , solverClose = Backend.close handle
+            , solverClose
             , mbTranscriptHandle
             , prelude
             , options = opts
@@ -122,7 +127,7 @@ closeContext ctxt = do
     logMessage ("Stopping SMT solver" :: Text)
     whenJust ctxt.mbTranscriptHandle $ \h -> liftIO $ do
         BS.hPutStrLn h "; stopping solver\n;;;;;;;;;;;;;;;;;;;;;;;"
-    liftIO ctxt.solverClose
+    liftIO $ join $ readIORef ctxt.solverClose
 
 {- | Close the connection to the SMT solver process and all other resources in  @SMTContext@.
  Using this function means completely stopping the solver with no intention of using it any more.
@@ -133,7 +138,7 @@ destroyContext ctxt = do
     whenJust ctxt.mbTranscriptHandle $ \h -> liftIO $ do
         BS.hPutStrLn h "; permanently stopping solver\n;;;;;;;;;;;;;;;;;;;;;;;"
         hClose h
-    liftIO ctxt.solverClose
+    liftIO $ join $ readIORef ctxt.solverClose
 
 connectToSolver :: LoggerMIO io => io (Backend.Solver, Backend.Handle)
 connectToSolver = do
@@ -179,7 +184,7 @@ runCmd cmd = do
         whenJust (comment cmd) $ \c ->
             liftIO (BS.hPutBuilder h c)
         liftIO (BS.hPutBuilder h $ cmdBS <> "\n")
-    output <- run_ cmd ctxt.solver cmdBS
+    output <- (liftIO $ readIORef ctxt.solver) >>= \solver -> run_ cmd solver cmdBS
     let result = readResponse output
     whenJust ctxt.mbTranscriptHandle $
         liftIO . flip BS.hPutStrLn (BS.pack $ "; " <> show output <> ", parsed as " <> show result <> "\n")