packages feed

smtlib-backends-process (empty) → 0.2

raw patch · 7 files changed

+385/−0 lines, 7 filesdep +asyncdep +basedep +bytestringsetup-changed

Dependencies added: async, base, bytestring, data-default, smtlib-backends, smtlib-backends-process, smtlib-backends-tests, tasty, tasty-hunit, typed-process

Files

+ CHANGELOG.md view
@@ -0,0 +1,13 @@+# 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 +- don't prefix error messages with `[stderr]`+## test-suite+- add usage examples+- make compatible with `smtlib-backends-0.2`+## miscellaneous+- improve documentation
+ LICENSE view
@@ -0,0 +1,21 @@+MIT License++Copyright (c) Tweag I/O Limited.++Permission is hereby granted, free of charge, to any person obtaining a copy+of this software and associated documentation files (the "Software"), to deal+in the Software without restriction, including without limitation the rights+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell+copies of the Software, and to permit persons to whom the Software is+furnished to do so, subject to the following conditions:++The above copyright notice and this permission notice shall be included in all+copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE+SOFTWARE.
+ Setup.hs view
@@ -0,0 +1,3 @@+import Distribution.Simple++main = defaultMain
+ smtlib-backends-process.cabal view
@@ -0,0 +1,60 @@+name:               smtlib-backends-process+version:            0.2+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.++license:            MIT+license-file:       LICENSE+author:             Quentin Aristote+maintainer:         quentin.aristote@tweag.io+build-type:         Simple+category:           SMT+cabal-version:      >=1.10+extra-source-files: CHANGELOG.md++source-repository head+  type:     git+  location: https://github.com/tweag/smtlib-backends+  subdir:   smtlib-backends-process++source-repository this+  type:     git+  location: https://github.com/tweag/smtlib-backends+  tag:      0.2+  subdir:   smtlib-backends-process++library+  hs-source-dirs:   src+  ghc-options:      -Wall -Wunused-packages+  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++  default-language: Haskell2010++test-suite test+  type:             exitcode-stdio-1.0+  hs-source-dirs:   tests+  main-is:          Main.hs+  other-modules:    Examples+  ghc-options:      -threaded -Wall -Wunused-packages+  build-depends:+      base+    , bytestring+    , data-default+    , smtlib-backends+    , smtlib-backends-process+    , smtlib-backends-tests+    , tasty+    , tasty-hunit+    , typed-process++  default-language: Haskell2010
+ src/SMTLIB/Backends/Process.hs view
@@ -0,0 +1,188 @@+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE ViewPatterns #-}++-- | A module providing a backend that launches solvers as external processes.+module SMTLIB.Backends.Process+  ( Config (..),+    Handle (..),+    new,+    wait,+    close,+    with,+    toBackend,+  )+where++import Control.Concurrent.Async (Async, async, cancel)+import qualified Control.Exception as X+import Control.Monad (forever)+import Data.ByteString.Builder+  ( Builder,+    byteString,+    hPutBuilder,+    toLazyByteString,+  )+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 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)++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 ()+  }++-- | 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 ()++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 ()+  }++-- | 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)+  -- 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+  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++-- | 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 ()+close handle = do+  cancel $ errorReader 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 -> `bracket` (`new` config) `wait`@ instead.+with ::+  -- | The solver process' configuration.+  Config ->+  -- | The computation to run with the solver process+  (Handle -> IO a) ->+  IO a+with config = X.bracket (new config) close++infixr 5 :<++pattern (:<) :: Char -> BS.ByteString -> BS.ByteString+pattern c :< rest <- (BS.uncons -> Just (c, rest))++-- | 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+  where+    -- 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+    -- if we detect a ')' at depth 0 that is not enclosed in a string, a quoted+    -- symbol or a comment, we give up and return immediately+    -- see also the SMT-LIB standard v2.6+    -- https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf#part.2+    scanParen :: Int -> Builder -> BS.ByteString -> IO Builder+    scanParen depth acc ('(' :< more) = scanParen (depth + 1) acc more+    scanParen depth acc ('"' :< more) = do+      (acc', more') <- string acc more+      scanParen depth acc' more'+    scanParen depth acc ('|' :< more) = do+      (acc', more') <- quotedSymbol acc more+      scanParen depth acc' more'+    scanParen depth acc (';' :< _) = continueNextLine (scanParen depth) acc+    scanParen depth acc (')' :< more)+      | depth <= 1 = return acc+      | otherwise = scanParen (depth - 1) acc more+    scanParen depth acc (_ :< more) = scanParen depth acc more+    -- mempty case+    scanParen 0 acc _ = return acc+    scanParen depth acc _ = continueNextLine (scanParen depth) acc++    string :: Builder -> BS.ByteString -> IO (Builder, BS.ByteString)+    string acc ('"' :< '"' :< more) = string acc more+    string acc ('"' :< more) = return (acc, more)+    string acc (_ :< more) = string acc more+    -- mempty case+    string acc _ = continueNextLine string acc++    quotedSymbol :: Builder -> BS.ByteString -> IO (Builder, BS.ByteString)+    quotedSymbol acc ('|' :< more) = return (acc, more)+    quotedSymbol acc (_ :< more) = string acc more+    -- mempty case+    quotedSymbol acc _ = continueNextLine quotedSymbol acc++    continueNextLine :: (Builder -> BS.ByteString -> IO a) -> Builder -> IO a+    continueNextLine f acc = do+      next <- BS.hGetLine $ getStdout $ process handle+      f (acc <> byteString next) next
+ tests/Examples.hs view
@@ -0,0 +1,85 @@+{-# LANGUAGE OverloadedStrings #-}++module Examples (examples) where++import qualified Data.ByteString.Lazy.Char8 as LBS+import Data.Default (def)+import SMTLIB.Backends (command, 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+import Test.Tasty.HUnit++-- | The examples for the 'Process' backend (running solvers as external+-- processes).+examples :: [TestTree]+examples =+  [ testCase "basic use" basicUse,+    testCase "setting options" setOptions,+    testCase "exiting manually" manualExit+  ]++-- | Basic use of the 'Process' backend.+basicUse :: IO ()+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+    $ \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+      -- 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)"+      return ()++-- | An example of how to change the default settings of the 'Process' backend.+setOptions :: IO ()+setOptions =+  -- here we use a custom-made configuration+  let myConfig =+        Process.Config+          { Process.exe = "z3",+            Process.args = ["-in", "solver.timeout=10000"],+            Process.reportError = LBS.putStr . (`LBS.snoc` '\n')+          }+   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+        _ <- 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
+ tests/Main.hs view
@@ -0,0 +1,15 @@+import Data.Default (def)+import Examples (examples)+import qualified SMTLIB.Backends.Process as Process+import SMTLIB.Backends.Tests (sources, testBackend)+import Test.Tasty++main :: IO ()+main = do+  defaultMain $+    testGroup+      "Tests"+      [ testBackend "Basic examples" sources $ \todo ->+          Process.with def $ todo . Process.toBackend,+        testGroup "API usage examples" examples+      ]