Merge pull request #38 from tweag/qa/exit_command

`Process` backend: add a function for sending `(exit)`

Author: qaristote

smtlib-backends-process/CHANGELOG.md

@@ -1,5 +1,15 @@
 # v0.3-alpha
 - make test-suite compatible with `smtlib-backends-0.3`
+- rename `Process.close` to `Process.kill`
+- rename `Process.wait` to `Process.close` and improve it
+  - ensure the process gets killed even if an error is caught
+  - send an `(exit)` command before waiting for the process to exit
+  - this means `Process.with` now closes the process with this new version of
+    `Process.close`, hence gracefully
+- add a `Process.write` function for writing commands without reading the
+  solver's response
+- add a test checking that we can pile up procedures for exiting a process
+  safely
 
 # v0.2
 split `smtlib-backends`'s `Process` module into its own library

smtlib-backends-process/src/SMTLIB/Backends/Process.hs

@@ -1,15 +1,17 @@
 {-# LANGUAGE DisambiguateRecordFields #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE ViewPatterns #-}
 
 -- | A module providing a backend that launches solvers as external processes.
 module SMTLIB.Backends.Process
   ( Config (..),
     Handle (..),
     new,
-    wait,
+    write,
     close,
+    kill,
     with,
     toBackend,
   )
@@ -28,7 +30,7 @@ import qualified Data.ByteString.Char8 as BS
 import qualified Data.ByteString.Lazy.Char8 as LBS
 import Data.Default (Default, def)
 import SMTLIB.Backends (Backend (..))
-import System.Exit (ExitCode)
+import System.Exit (ExitCode (ExitFailure))
 import qualified System.IO as IO
 import System.Process.Typed
   ( Process,
@@ -106,23 +108,37 @@ new config = do
           )
     reportError' = reportError config . LBS.fromStrict
 
--- | Wait for the process to exit and cleanup its resources.
-wait :: Handle -> IO ExitCode
-wait handle = do
-  cancel $ errorReader handle
-  waitExitCode $ process handle
+-- | Send a command to the process without reading its response.
+write :: Handle -> Builder -> IO ()
+write handle cmd = do
+  hPutBuilder (getStdin $ process handle) $ cmd <> "\n"
+  IO.hFlush $ getStdin $ process handle
 
--- | Terminate the process, wait for it to actually exit and cleanup its resources.
--- Don't use this if you're manually stopping the solver process by sending an
--- @(exit)@ command. Use `wait` instead.
-close :: Handle -> IO ()
+-- | Cleanup the process' resources.
+cleanup :: Handle -> IO ()
+cleanup = cancel . errorReader
+
+-- | Cleanup the process' resources, send it an @(exit)@ command and wait for it
+-- to exit.
+close :: Handle -> IO ExitCode
 close handle = do
-  cancel $ errorReader handle
+  cleanup handle
+  let p = process handle
+  ( do
+      write handle "(exit)"
+      waitExitCode p
+    )
+    `X.catch` \(_ :: X.IOException) -> do
+      stopProcess p
+      return $ ExitFailure 1
+
+-- | Cleanup the process' resources and kill it immediately.
+kill :: Handle -> IO ()
+kill handle = do
+  cleanup handle
   stopProcess $ process handle
 
--- | Create a solver process, use it to make a computation and stop it.
--- Don't use this if you're manually stopping the solver process by sending an
--- @(exit)@ command. Use @\\config -> `System.IO.bracket` (`new` config) `wait`@ instead.
+-- | Create a solver process, use it to make a computation and close it.
 with ::
   -- | The solver process' configuration.
   Config ->
@@ -140,8 +156,7 @@ pattern c :< rest <- (BS.uncons -> Just (c, rest))
 toBackend :: Handle -> Backend
 toBackend handle =
   Backend $ \cmd -> do
-    hPutBuilder (getStdin $ process handle) $ cmd <> "\n"
-    IO.hFlush $ getStdin $ process handle
+    write handle cmd
     toLazyByteString <$> continueNextLine (scanParen 0) mempty
   where
     -- scanParen read lines from the handle's output channel until it has detected

smtlib-backends-process/tests/Examples.hs

@@ -4,9 +4,8 @@ module Examples (examples) where
 
 import qualified Data.ByteString.Lazy.Char8 as LBS
 import Data.Default (def)
-import SMTLIB.Backends (QueuingFlag (..), command, command_, initSolver)
+import SMTLIB.Backends (QueuingFlag (..), command, initSolver)
 import qualified SMTLIB.Backends.Process as Process
-import System.Exit (ExitCode (ExitSuccess))
 import System.IO (BufferMode (LineBuffering), hSetBuffering)
 import System.Process.Typed (getStdin)
 import Test.Tasty
@@ -40,6 +39,8 @@ basicUse =
       -- we can write the command as a simple string because we have enabled the
       -- OverloadedStrings pragma
       _ <- command solver "(get-info :name)"
+      -- note how there is no need to send an @(exit)@ command, this is already
+      -- handled by the 'Process.with' function
       return ()
 
 -- | An example of how to change the default settings of the 'Process' backend.
@@ -74,12 +75,17 @@ manualExit :: IO ()
 manualExit = do
   -- launch a new process with 'Process.new'
   handle <- Process.new def
-  let backend = Process.toBackend handle
-  -- here we disable queuing so that we can use 'command_' to ensure the exit
-  -- command will be received successfully
-  solver <- initSolver NoQueuing backend
-  command_ solver "(exit)"
-  -- 'Process.wait' takes care of cleaning resources and waits for the process to
-  -- exit
-  exitCode <- Process.wait handle
-  assertBool "the solver process didn't exit properly" $ exitCode == ExitSuccess
+  -- do some stuff
+  doStuffWithHandle handle
+  -- kill the process with 'Process.kill'
+  -- other options include using 'Process.close' to ensure the process exits
+  -- gracefully
+  --
+  -- if this isn't enough for you, it is always possible to send an @(exit)@
+  -- command using 'Process.write', access the solver process using
+  -- 'Process.process' and kill it manually
+  -- if this is what you go with, don't forget to also cancel the
+  -- 'Process.errorReader' asynchronous process!
+  Process.kill handle
+  where
+    doStuffWithHandle _ = return ()

smtlib-backends-process/tests/Main.hs

@@ -1,8 +1,11 @@
+{-# LANGUAGE OverloadedStrings #-}
+
 import Data.Default (def)
 import Examples (examples)
 import qualified SMTLIB.Backends.Process as Process
 import SMTLIB.Backends.Tests (sources, testBackend)
 import Test.Tasty
+import Test.Tasty.HUnit
 
 main :: IO ()
 main = do
@@ -11,5 +14,9 @@ main = do
       "Tests"
       [ testBackend "Basic examples" sources $ \todo ->
           Process.with def $ todo . Process.toBackend,
-        testGroup "API usage examples" examples
+        testGroup "API usage examples" examples,
+        testCase "Piling up stopping procedures" $ Process.with def $ \handle -> do
+          Process.write handle "(exit)"
+          _ <- Process.close handle
+          Process.kill handle
       ]