packages feed

smtlib-backends-process 0.2 → 0.3

raw patch · 6 files changed

+248/−150 lines, 6 filesdep +processdep −data-defaultdep −typed-processdep ~asyncdep ~basedep ~bytestring

Dependencies added: process

Dependencies removed: data-default, typed-process

Dependency ranges changed: async, base, bytestring, smtlib-backends

Files

CHANGELOG.md view
@@ -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
smtlib-backends-process.cabal view
@@ -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
src/SMTLIB/Backends/Process.hs view
@@ -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+          }+      )
+ tests/EdgeCases.hs view
@@ -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
tests/Examples.hs view
@@ -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
tests/Main.hs view
@@ -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       ]