diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,13 +1,45 @@ -# v0.2 -split `smtlib-backends`'s `Process` module into its own library -## `Config` datatype -- move the logger function into it -- make it an instance of the `Default` typeclass -## logging -- move the logger function into the `Config` datatype +# Changelog + +All notable changes to the smtlib-backends-process library will be documented in +this file. + +## v0.3 _(2023-02-03)_ + +### Added +- add tests for documenting edge cases of the backends + - check that we can pile up procedures for exiting a process + - what happens when sending an empty command + - what happens when sending a command not producing any output +- add `Process.defaultConfig` +- add `std_err` field in `Config`: the user may now specifiy how to create the + handle for the error channel + +### Changed +- make the test-suite compatible with `smtlib-backends-0.3` +- **(breaking change)** use `process` instead of `typed-process` to manage the underlying process + - change the definition of the `Process.Handle` datatype accordingly + - remove `Process.wait` + - there is now a single example in the test-suite showing how to + manage the underlying process and its I/O channels +- improve error messages inside `Process.toBackend` + +### Removed +- removed `Process.wait` +- **(breaking change)** removed logging capabilities, this is now on the user to + implement (see also the `underlyingProcess` example) + - remove `Config`'s `reportError` field + - remove `Handle`'s `errorReader` field +- **(breaking change)** removed `Data.Default` instance of `Config` + +## v0.2 _(2022-12-16)_ + +### Added +- made `Config` an instance of the `Default` typeclass +- add usage examples in the test-suite + +### Changed +- split `smtlib-backends`'s `Process` module into its own library +- move the logger function inside the `Config` datatype - don't prefix error messages with `[stderr]` -## test-suite -- add usage examples - make compatible with `smtlib-backends-0.2` -## miscellaneous - improve documentation diff --git a/smtlib-backends-process.cabal b/smtlib-backends-process.cabal --- a/smtlib-backends-process.cabal +++ b/smtlib-backends-process.cabal @@ -1,9 +1,9 @@ name: smtlib-backends-process -version: 0.2 +version: 0.3 synopsis: An SMT-LIB backend running solvers as external processes. description: - This library implements an SMT-LIB backend (in the sense of the smtlib-backends - package) using by running solvers as external processes. + This library implements an SMT-LIB backend (in the sense of the + smtlib-backends package) which runs solvers as external processes. license: MIT license-file: LICENSE @@ -22,7 +22,7 @@ source-repository this type: git location: https://github.com/tweag/smtlib-backends - tag: 0.2 + tag: 0.3 subdir: smtlib-backends-process library @@ -31,12 +31,10 @@ exposed-modules: SMTLIB.Backends.Process other-extensions: Safe build-depends: - async >=2.2.4 && <2.3 - , base >=4.14 && <4.17.0 - , bytestring >=0.10.12 && <0.11 - , data-default >=0.7.1 && <0.8 - , smtlib-backends >=0.2 && <0.3 - , typed-process >=0.2.10 && <0.3 + base >=4.14 && <4.18 + , bytestring >=0.10.12 && <0.12 + , process >=1.6 && <1.7 + , smtlib-backends >=0.3 && <0.4 default-language: Haskell2010 @@ -44,17 +42,20 @@ type: exitcode-stdio-1.0 hs-source-dirs: tests main-is: Main.hs - other-modules: Examples + other-modules: + EdgeCases + Examples + ghc-options: -threaded -Wall -Wunused-packages build-depends: - base + async + , base , bytestring - , data-default + , process , smtlib-backends , smtlib-backends-process , smtlib-backends-tests , tasty , tasty-hunit - , typed-process default-language: Haskell2010 diff --git a/src/SMTLIB/Backends/Process.hs b/src/SMTLIB/Backends/Process.hs --- a/src/SMTLIB/Backends/Process.hs +++ b/src/SMTLIB/Backends/Process.hs @@ -1,24 +1,23 @@ {-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE PatternGuards #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE ViewPatterns #-} -- | A module providing a backend that launches solvers as external processes. module SMTLIB.Backends.Process ( Config (..), Handle (..), + defaultConfig, new, - wait, close, with, toBackend, + P.StdStream (..), ) where -import Control.Concurrent.Async (Async, async, cancel) import qualified Control.Exception as X -import Control.Monad (forever) import Data.ByteString.Builder ( Builder, byteString, @@ -26,104 +25,73 @@ toLazyByteString, ) import qualified Data.ByteString.Char8 as BS -import qualified Data.ByteString.Lazy.Char8 as LBS -import Data.Default (Default, def) +import GHC.IO.Exception (IOException (ioe_description)) import SMTLIB.Backends (Backend (..)) -import System.Exit (ExitCode) import qualified System.IO as IO -import System.Process.Typed - ( Process, - getStderr, - getStdin, - getStdout, - mkPipeStreamSpec, - setStderr, - setStdin, - setStdout, - startProcess, - stopProcess, - waitExitCode, - ) -import qualified System.Process.Typed as P (proc) +import qualified System.Process as P data Config = Config { -- | The command to call to run the solver. exe :: String, -- | Arguments to pass to the solver's command. args :: [String], - -- | A function for logging the solver process' messages on stderr and file - -- handle exceptions. - -- If you want line breaks between each log message, you need to implement - -- it yourself, e.g use @'LBS.putStr' . (<> "\n")@. - reportError :: LBS.ByteString -> IO () + -- | How to handle std_err of the solver. + std_err :: P.StdStream } --- | By default, use Z3 as an external process and ignore log messages. -instance Default Config where - -- if you change this, make sure to also update the comment two lines above - -- as well as the one in @smtlib-backends-process/tests/Examples.hs@ - def = Config "z3" ["-in"] $ const $ return () +-- | By default, use Z3 as an external process and ignores log messages. +defaultConfig :: Config +-- if you change this, make sure to also update the comment two lines above +-- as well as the one in @smtlib-backends-process/tests/Examples.hs@ +defaultConfig = Config "z3" ["-in"] P.CreatePipe data Handle = Handle { -- | The process running the solver. - process :: Process IO.Handle IO.Handle IO.Handle, - -- | A process reading the solver's error messages and logging them. - errorReader :: Async () + process :: P.ProcessHandle, + -- | The input channel of the process. + hIn :: IO.Handle, + -- | The output channel of the process. + hOut :: IO.Handle, + -- | The error channel of the process. + hMaybeErr :: Maybe IO.Handle } -- | Run a solver as a process. --- Failures relative to terminating the process are logged and discarded. new :: -- | The solver process' configuration. Config -> IO Handle -new config = do - solverProcess <- - startProcess $ - setStdin createLoggedPipe $ - setStdout createLoggedPipe $ - setStderr createLoggedPipe $ - P.proc (exe config) (args config) +new Config {..} = decorateIOError "creating the solver process" $ do + (Just hIn, Just hOut, hMaybeErr, process) <- + P.createProcess + (P.proc exe args) + { P.std_in = P.CreatePipe, + P.std_out = P.CreatePipe, + P.std_err = std_err + } + mapM_ setupHandle [hIn, hOut] -- log error messages created by the backend - solverErrorReader <- - async $ - forever - ( do - errs <- BS.hGetLine $ getStderr solverProcess - reportError' errs - ) - `X.catch` \X.SomeException {} -> - return () - return $ Handle solverProcess solverErrorReader + return $ Handle process hIn hOut hMaybeErr where - createLoggedPipe = - mkPipeStreamSpec $ \_ h -> do - IO.hSetBinaryMode h True - IO.hSetBuffering h $ IO.BlockBuffering Nothing - return - ( h, - IO.hClose h `X.catch` \ex -> - reportError' $ BS.pack $ show (ex :: X.IOException) - ) - reportError' = (reportError config) . LBS.fromStrict + setupHandle h = do + IO.hSetBinaryMode h True + IO.hSetBuffering h $ IO.BlockBuffering Nothing --- | 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 = + decorateIOError msg $ do + hPutBuilder hIn $ cmd <> "\n" + IO.hFlush hIn + where + msg = "sending command " ++ show (toLazyByteString cmd) ++ " to the solver" --- | 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. +-- | Cleanup the process' resources, terminate it and wait for it to actually exit. close :: Handle -> IO () -close handle = do - cancel $ errorReader handle - stopProcess $ process handle +close Handle {..} = decorateIOError "closing the solver process" $ do + P.cleanupProcess (Just hIn, Just hOut, hMaybeErr, process) --- | 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 -> `bracket` (`new` config) `wait`@ instead. +-- | Create a solver process, use it to make a computation and close it. with :: -- | The solver process' configuration. Config -> @@ -139,12 +107,16 @@ -- | Make the solver process into an SMT-LIB backend. toBackend :: Handle -> Backend -toBackend handle = - Backend $ \cmd -> do - hPutBuilder (getStdin $ process handle) $ cmd <> "\n" - IO.hFlush $ getStdin $ process handle - toLazyByteString <$> continueNextLine (scanParen 0) mempty +toBackend handle = Backend backendSend backendSend_ where + backendSend_ = write handle + backendSend cmd = do + -- exceptions are decorated inside the body of 'write' + write handle cmd + decorateIOError "reading solver's response" $ + toLazyByteString + <$> continueNextLine (scanParen 0) mempty + -- scanParen read lines from the handle's output channel until it has detected -- a complete s-expression, i.e. a well-parenthesized word that may contain -- strings, quoted symbols, and comments @@ -184,5 +156,27 @@ continueNextLine :: (Builder -> BS.ByteString -> IO a) -> Builder -> IO a continueNextLine f acc = do - next <- BS.hGetLine $ getStdout $ process handle + next <- + BS.hGetLine (hOut handle) `X.catch` \ex -> + X.throwIO + ( ex + { ioe_description = + ioe_description ex + ++ ": " + ++ show (toLazyByteString acc) + } + ) f (acc <> byteString next) next + +decorateIOError :: String -> IO a -> IO a +decorateIOError contextDescription = + X.handle $ \ex -> + X.throwIO + ( ex + { ioe_description = + "[smtlib-backends-process] while " + ++ contextDescription + ++ ": " + ++ ioe_description ex + } + ) diff --git a/tests/EdgeCases.hs b/tests/EdgeCases.hs new file mode 100644 --- /dev/null +++ b/tests/EdgeCases.hs @@ -0,0 +1,47 @@ +{-# LANGUAGE OverloadedStrings #-} + +module EdgeCases (edgeCases) where + +import Data.ByteString.Builder (Builder) +import Data.ByteString.Lazy.Char8 as LBS +import SMTLIB.Backends as SMT +import qualified SMTLIB.Backends.Process as Process +import System.Process (terminateProcess, waitForProcess) +import Test.Tasty +import Test.Tasty.HUnit + +edgeCases :: [TestTree] +edgeCases = + [ testCase "Piling up stopping procedures" pileUpStops, + testCase "Sending an empty command" emptyCommand, + testCase "Sending a command expecting no response" commandNoResponse + ] + +-- | It's possible to accumulate procedures that stop the backend without +-- hanging or crashing the program. +pileUpStops :: IO () +pileUpStops = Process.with Process.defaultConfig $ \handle -> do + let backend = Process.toBackend handle + process = Process.process handle + SMT.send_ backend "(exit)" + _ <- waitForProcess process + terminateProcess process + +-- | Upon processing an empty command, the backend will not respond. +emptyCommand :: IO () +emptyCommand = checkNoResponse "" + +-- | Upon processing a command producing no output, the backend will not +-- respond, not even with an empty line. +commandNoResponse :: IO () +commandNoResponse = checkNoResponse "(set-option :print-success false)" + +checkNoResponse :: Builder -> IO () +checkNoResponse cmd = do + Just response <- Process.with Process.defaultConfig $ \handle -> do + let backend = Process.toBackend handle + -- using 'SMT.send' instead would hang the program + SMT.send_ backend cmd + -- (check-sat) will produce "sat" + LBS.stripSuffix "sat" <$> SMT.send backend "(check-sat)" + assertEqual "expected no response" "" response diff --git a/tests/Examples.hs b/tests/Examples.hs --- a/tests/Examples.hs +++ b/tests/Examples.hs @@ -1,14 +1,16 @@ {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RecordWildCards #-} module Examples (examples) where +import Control.Concurrent.Async (async) +import Control.Exception (SomeException (SomeException), catch) +import Control.Monad (forever) import qualified Data.ByteString.Lazy.Char8 as LBS -import Data.Default (def) -import SMTLIB.Backends (command, command_, initSolver) +import SMTLIB.Backends (QueuingFlag (..), command, command_, flushQueue, 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 System.IO (BufferMode (LineBuffering), hClose, hGetLine, hSetBuffering) +import System.Process (waitForProcess) import Test.Tasty import Test.Tasty.HUnit @@ -18,7 +20,8 @@ examples = [ testCase "basic use" basicUse, testCase "setting options" setOptions, - testCase "exiting manually" manualExit + testCase "managing the underlying process" underlyingProcess, + testCase "flushing the queue" flushing ] -- | Basic use of the 'Process' backend. @@ -26,20 +29,20 @@ basicUse = -- 'Process.with' runs a computation using the 'Process' backend Process.with - -- the configuration type 'Process.Config' is an instance of the 'Default' class - -- we can thus use a default configuration for the backend with the 'def' method - -- this default configuration uses Z3 as an external process and disables logging - def + -- the default configuration uses Z3 as an external process and disables logging + Process.defaultConfig $ \handle -> do -- first, we make the process handle into an actual backend let backend = Process.toBackend handle -- then, we create a solver out of the backend -- we enable queuing (it's faster !) - solver <- initSolver backend True + solver <- initSolver Queuing backend -- we send a basic command to the solver and ignore the response -- 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. @@ -47,39 +50,57 @@ setOptions = -- here we use a custom-made configuration let myConfig = - Process.Config + Process.defaultConfig { Process.exe = "z3", - Process.args = ["-in", "solver.timeout=10000"], - Process.reportError = LBS.putStr . (`LBS.snoc` '\n') + Process.args = ["-in", "solver.timeout=10000"] } in Process.with myConfig $ \handle -> do - -- since the 'Process' module exposes its 'Handle' datatype entirely, we can also - -- change the settings of the underlying process - -- you probably won't need to do this as the library already choose these - -- settings to ensure the communication with the solvers is as fast as - -- possible - let p = Process.process handle - stdin = getStdin p - -- for instance here we change the buffering mode of the process' input channel - hSetBuffering stdin LineBuffering - -- we can then use the backend as before - let backend = Process.toBackend handle - solver <- initSolver backend True + solver <- initSolver Queuing $ Process.toBackend handle _ <- command solver "(get-info :name)" return () --- | An example of how to close the 'Process' backend's underlying process manually, --- instead of relying on 'Process.with' or 'Process.close'. -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 backend False - 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 +-- | An example of how to get the backend's underlying process and manage it +-- manually, for instance when you want to monitor the process' error channel. +underlyingProcess :: IO () +underlyingProcess = do + -- since the 'Process' module exposes its 'Handle' datatype entirely, we have + -- direct access to the process and its I/O channels + -- this can in particular be useful if you want to monitor the process' errors + -- that it prints on its error channel + -- otherwise, it's unlikely you'll need this as the library already provides + -- enough bindings for common needs and chooses the process' settings to + -- ensure the communication with solvers is as fast as possible + -- + -- we'll close the process manually so we just launch it with 'Process.new' + -- instead of using `Process.with` + Process.Handle {hMaybeErr = Just hErr, ..} <- Process.new Process.defaultConfig + -- the main use of accessing the internals of the 'Process.Handle' is to monitor + -- the process' error channel + _ <- async $ forever (hGetLine hErr >>= putStrLn) `catch` \SomeException {} -> return () + -- we can also change the settings of the underlying process + -- for instance here we change the buffering mode of the process' input channel + hSetBuffering hIn LineBuffering + -- the default way to close the process is to use 'Process.close', which sends + -- it a SIGTERM + -- if you don't like this, you can always send it an @(exit)@ command and wait + -- for it to end, but make sure you also release its other resources + LBS.hPutStrLn hIn "(exit)" + mapM_ hClose [hIn, hOut, hErr] + _ <- waitForProcess process + return () + +-- | An example on how to force the content of the queue to be evaluated. +flushing :: IO () +flushing = do + -- sometimes you want to use 'Queuing' mode but still force some commands not + -- producing any output to be evaluated + -- in that case, using 'command' would lead to your program hanging as it waits + -- for a response from the solver that never comes + -- the solution is to use the 'command_' function and then to flush the queue + Process.with Process.defaultConfig $ \handle -> do + -- this example only makes sense in queuing mode + solver <- initSolver Queuing $ Process.toBackend handle + -- add a command to the queue + command_ solver "(assert true)" + -- force the queue to be evaluated + flushQueue solver diff --git a/tests/Main.hs b/tests/Main.hs --- a/tests/Main.hs +++ b/tests/Main.hs @@ -1,4 +1,6 @@ -import Data.Default (def) +{-# LANGUAGE OverloadedStrings #-} + +import EdgeCases (edgeCases) import Examples (examples) import qualified SMTLIB.Backends.Process as Process import SMTLIB.Backends.Tests (sources, testBackend) @@ -10,6 +12,7 @@ testGroup "Tests" [ testBackend "Basic examples" sources $ \todo -> - Process.with def $ todo . Process.toBackend, - testGroup "API usage examples" examples + Process.with Process.defaultConfig $ todo . Process.toBackend, + testGroup "API usage examples" examples, + testGroup "Edge cases" edgeCases ]