From d249ccbf23d3260bdf5c01cae2a210231d464f10 Mon Sep 17 00:00:00 2001
From: Quentin Aristote <quentin@aristote.fr>
Date: Mon, 9 Jan 2023 17:09:43 +0100
Subject: [PATCH 1/5] Process: add exit function

---
 .../src/SMTLIB/Backends/Process.hs               | 16 ++++++++++++++--
 smtlib-backends-process/tests/Examples.hs        | 15 +++++++--------
 2 files changed, 21 insertions(+), 10 deletions(-)

diff --git a/smtlib-backends-process/src/SMTLIB/Backends/Process.hs b/smtlib-backends-process/src/SMTLIB/Backends/Process.hs
index f148d8c..e87cb5b 100644
--- a/smtlib-backends-process/src/SMTLIB/Backends/Process.hs
+++ b/smtlib-backends-process/src/SMTLIB/Backends/Process.hs
@@ -9,6 +9,7 @@ module SMTLIB.Backends.Process
   ( Config (..),
     Handle (..),
     new,
+    exit,
     wait,
     close,
     with,
@@ -107,6 +108,18 @@ new config = do
           )
     reportError' = (reportError config) . LBS.fromStrict
 
+-- | 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
+
+-- | Send the @(exit)@ command to the process.
+-- Note that using @'write' ('toBackend' handle) "(exit)"@ instead could hang
+-- the process as it would wait for a response.
+exit :: Handle -> IO ()
+exit = flip write "(exit)"
+
 -- | Wait for the process to exit and cleanup its resources.
 wait :: Handle -> IO ExitCode
 wait handle = do
@@ -141,8 +154,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
diff --git a/smtlib-backends-process/tests/Examples.hs b/smtlib-backends-process/tests/Examples.hs
index f25c22a..fc47508 100644
--- a/smtlib-backends-process/tests/Examples.hs
+++ b/smtlib-backends-process/tests/Examples.hs
@@ -4,7 +4,7 @@ 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)
@@ -74,12 +74,11 @@ 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
+  -- to stop the process, we first send an "(exit)" command and then use
+  -- 'Process.wait' which takes care of cleaning resources and waits for the
+  -- process to actually exit
+  -- when an exit code isn't needed and the process doesn't have to stop
+  -- gracefully, another simpler option is to just use 'Process.close'
+  Process.exit handle
   exitCode <- Process.wait handle
   assertBool "the solver process didn't exit properly" $ exitCode == ExitSuccess

From 5ead3eeacee4a2e15ce13a690eaf6c764508a653 Mon Sep 17 00:00:00 2001
From: Quentin Aristote <quentin@aristote.fr>
Date: Tue, 10 Jan 2023 12:36:45 +0100
Subject: [PATCH 2/5] Process: reimplement closing functions

---
 smtlib-backends-process/CHANGELOG.md          |  8 +++
 .../src/SMTLIB/Backends/Process.hs            | 49 ++++++++++---------
 smtlib-backends-process/tests/Examples.hs     | 25 ++++++----
 3 files changed, 50 insertions(+), 32 deletions(-)

diff --git a/smtlib-backends-process/CHANGELOG.md b/smtlib-backends-process/CHANGELOG.md
index 3359eaf..c21f509 100644
--- a/smtlib-backends-process/CHANGELOG.md
+++ b/smtlib-backends-process/CHANGELOG.md
@@ -1,5 +1,13 @@
 # v0.3-alpha
 - make test-suite compatible with `smtlib-backends-0.3`
+- rename `Process.close` to `Process.kill`
+- rename `Process.wait` to `Process.close`
+  - 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
 
 # v0.2
 split `smtlib-backends`'s `Process` module into its own library
diff --git a/smtlib-backends-process/src/SMTLIB/Backends/Process.hs b/smtlib-backends-process/src/SMTLIB/Backends/Process.hs
index e87cb5b..28cdf26 100644
--- a/smtlib-backends-process/src/SMTLIB/Backends/Process.hs
+++ b/smtlib-backends-process/src/SMTLIB/Backends/Process.hs
@@ -2,6 +2,7 @@
 {-# LANGUAGE PatternGuards #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE ViewPatterns #-}
 
 -- | A module providing a backend that launches solvers as external processes.
@@ -9,9 +10,9 @@ module SMTLIB.Backends.Process
   ( Config (..),
     Handle (..),
     new,
-    exit,
-    wait,
+    write,
     close,
+    kill,
     with,
     toBackend,
   )
@@ -30,7 +31,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,
@@ -114,29 +115,31 @@ write handle cmd = do
   hPutBuilder (getStdin $ process handle) $ cmd <> "\n"
   IO.hFlush $ getStdin $ process handle
 
--- | Send the @(exit)@ command to the process.
--- Note that using @'write' ('toBackend' handle) "(exit)"@ instead could hang
--- the process as it would wait for a response.
-exit :: Handle -> IO ()
-exit = flip write "(exit)"
-
--- | Wait for the process to exit and cleanup its resources.
-wait :: Handle -> IO ExitCode
-wait handle = do
-  cancel $ errorReader handle
-  waitExitCode $ 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 ->
diff --git a/smtlib-backends-process/tests/Examples.hs b/smtlib-backends-process/tests/Examples.hs
index fc47508..aff370c 100644
--- a/smtlib-backends-process/tests/Examples.hs
+++ b/smtlib-backends-process/tests/Examples.hs
@@ -6,7 +6,6 @@ import qualified Data.ByteString.Lazy.Char8 as LBS
 import Data.Default (def)
 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,11 +75,17 @@ manualExit :: IO ()
 manualExit = do
   -- launch a new process with 'Process.new'
   handle <- Process.new def
-  -- to stop the process, we first send an "(exit)" command and then use
-  -- 'Process.wait' which takes care of cleaning resources and waits for the
-  -- process to actually exit
-  -- when an exit code isn't needed and the process doesn't have to stop
-  -- gracefully, another simpler option is to just use 'Process.close'
-  Process.exit handle
-  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 ()

From 82da6e19e1f10ffcf1647196964d4d59dbcdceab Mon Sep 17 00:00:00 2001
From: Quentin Aristote <quentin@aristote.fr>
Date: Tue, 10 Jan 2023 12:46:40 +0100
Subject: [PATCH 3/5] Process: tests: check that we can safely pile up exiting
 procedures

---
 smtlib-backends-process/tests/Main.hs | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/smtlib-backends-process/tests/Main.hs b/smtlib-backends-process/tests/Main.hs
index a22dd15..92f0c5e 100644
--- a/smtlib-backends-process/tests/Main.hs
+++ b/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
       ]

From 98782d62fa68adbf6b03d4e1d519aab83f4e86a7 Mon Sep 17 00:00:00 2001
From: Quentin Aristote <quentin@aristote.fr>
Date: Tue, 10 Jan 2023 13:12:46 +0100
Subject: [PATCH 4/5] Process: tests: mention new test in changelog

---
 smtlib-backends-process/CHANGELOG.md | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/smtlib-backends-process/CHANGELOG.md b/smtlib-backends-process/CHANGELOG.md
index c21f509..7eeaf7b 100644
--- a/smtlib-backends-process/CHANGELOG.md
+++ b/smtlib-backends-process/CHANGELOG.md
@@ -8,6 +8,8 @@
     `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

From 847f4379e66158a41c5b0be9ba3d80e0376f8d88 Mon Sep 17 00:00:00 2001
From: Quentin Aristote <quentin@aristote.fr>
Date: Tue, 10 Jan 2023 13:22:26 +0100
Subject: [PATCH 5/5] Process: improve changelog

---
 smtlib-backends-process/CHANGELOG.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/smtlib-backends-process/CHANGELOG.md b/smtlib-backends-process/CHANGELOG.md
index 7eeaf7b..3163ec5 100644
--- a/smtlib-backends-process/CHANGELOG.md
+++ b/smtlib-backends-process/CHANGELOG.md
@@ -1,7 +1,7 @@
 # v0.3-alpha
 - make test-suite compatible with `smtlib-backends-0.3`
 - rename `Process.close` to `Process.kill`
-- rename `Process.wait` to `Process.close`
+- 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