simple-smt 0.9.9 → 1.0.1
raw patch · 4 files changed
Files
- CHANGES +2/−0
- SimpleSMT.hs +60/−42
- simple-smt.cabal +9/−1
- test/Finalizer.hs +142/−0
CHANGES view
@@ -1,3 +1,5 @@+1.0.1: Fix premature solver finalization in optimized code+1.0: Stop the external solver when the Solver object is garbage collected 0.9.7: `newSolverNotify` has a callback when solver quits 0.9.6: Suport for quoated symbols and recursive functions 0.9.5: Expose `loadString`
SimpleSMT.hs view
@@ -166,6 +166,9 @@ import Text.Read(readMaybe) import Data.Ratio((%), numerator, denominator) import Numeric(showHex, readHex, showFFloat)+import Foreign.Concurrent(newForeignPtr)+import Foreign.ForeignPtr(withForeignPtr)+import Foreign.Ptr(nullPtr) -- | Results of checking for satisfiability.@@ -319,63 +322,78 @@ }) = do (hIn, hOut, hErr, h) <- runInteractiveProcess exe opts Nothing Nothing + -- Drain stderr _ <- forkIO $ forever (do errs <- hGetLine hErr solverLogStdErr log errs) `X.catch` \X.SomeException {} -> return () - getResponse <-- do txt <- hGetContents hOut -- Read *all* output- ref <- newIORef (unfoldr readSExpr txt) -- Parse, and store result- return $ atomicModifyIORef ref $ \xs ->- case xs of- [] -> (xs, Nothing)- y : ys -> (ys, Just y)+ -- Parse responses (lazy)+ txt <- hGetContents hOut -- Read *all* output+ responses <- newIORef (unfoldr readSExpr txt) -- Parse, and store result - let cmd c = do let txt = showsSExpr c ""- solverLogSend log c- hPutStrLn hIn txt- hFlush hIn+ -- Wait for the solver to exit+ exitResult <- newEmptyMVar+ _ <- forkFinally+ (observeExit h hIn hOut hErr)+ (putMVar exitResult) - command c =- do cmd c- mb <- getResponse- case mb of- Just res -> do solverLogRecv log res- return res- Nothing -> fail "Missing response from solver"+ -- Close `stdin` when the Haskell Solver object is GC-ed, so that+ -- we close `stdin` and the solver process exits.+ finalizer <- newForeignPtr nullPtr (closeHandle hIn) - cleanup =- X.catch (do hClose hIn- hClose hOut- hClose hErr)- (solverLogExcn log)+ let solver =+ Solver+ { command = keepAlive finalizer . runCommand hIn responses+ , stop = keepAlive finalizer (stopSolver hIn exitResult)+ , forceStop = keepAlive finalizer (forceStopSolver h exitResult)+ } - observeExit =- do ec <- waitForProcess h- (case mbOnExit of- Nothing -> pure ()- Just this -> this ec)- `X.finally` cleanup- return ec+ setOption solver ":print-success" "true"+ setOption solver ":produce-models" "true" - exitResult <- newEmptyMVar- _ <- forkFinally observeExit (putMVar exitResult)+ return solver+ where+ send hIn c =+ do let txt = showsSExpr c ""+ solverLogSend log c+ hPutStrLn hIn txt+ hFlush hIn - let waitForExit = either X.throwIO pure =<< readMVar exitResult+ runCommand hIn responses c =+ do send hIn c+ mb <- atomicModifyIORef responses $ \xs ->+ case xs of+ [] -> (xs, Nothing)+ y : ys -> (ys, Just y)+ case mb of+ Just res -> do solverLogRecv log res+ return res+ Nothing -> fail "Missing response from solver" - forceStop = terminateProcess h *> waitForExit+ closeHandle handle =+ X.catch (hClose handle) (solverLogExcn log) - stop =- do cmd (List [Atom "exit"])- `X.catch` (\X.SomeException{} -> pure ())- waitForExit+ observeExit h hIn hOut hErr =+ do ec <- waitForProcess h+ (case mbOnExit of+ Nothing -> pure ()+ Just this -> this ec)+ `X.finally` mapM_ closeHandle [hIn, hOut, hErr]+ return ec - solver = Solver { .. }+ waitForExit exitResult =+ either X.throwIO pure =<< readMVar exitResult - setOption solver ":print-success" "true"- setOption solver ":produce-models" "true"+ forceStopSolver h exitResult =+ terminateProcess h *> waitForExit exitResult - return solver+ stopSolver hIn exitResult =+ do send hIn (List [Atom "exit"])+ `X.catch` (\X.SomeException{} -> pure ())+ waitForExit exitResult++ keepAlive finalizer action =+ withForeignPtr finalizer (\_ -> action) -- | Options for configuring how to start, stop, and interact with an SMT -- solver process.
simple-smt.cabal view
@@ -1,5 +1,5 @@ name: simple-smt-version: 0.9.9+version: 1.0.1 synopsis: A simple way to interact with an SMT solver process. description: A simple way to interact with an SMT solver process. license: BSD3@@ -24,6 +24,14 @@ main-is: DiffSEXp.hs hs-source-dirs: exe build-depends: base, containers, simple-smt, simple-get-opt++test-suite finalizer+ type: exitcode-stdio-1.0+ default-language: Haskell2010+ main-is: Finalizer.hs+ hs-source-dirs: test+ ghc-options: -threaded+ build-depends: base, simple-smt source-repository head type: git
+ test/Finalizer.hs view
@@ -0,0 +1,142 @@+{-# OPTIONS_GHC -O2 #-}++module Main (main) where++import Control.Concurrent.MVar+ ( MVar, newEmptyMVar, putMVar, takeMVar )+import Control.Exception (evaluate)+import Control.Monad (unless, when)+import System.Environment (getArgs, getExecutablePath)+import System.Exit (ExitCode)+import System.IO (hFlush, hPutStrLn, isEOF, stderr, stdout)+import System.Mem (performGC)+import System.Timeout (timeout)++import SimpleSMT+++eofMessage :: String+eofMessage = "fake solver: stdin closed"+++prematureFinalizerWindow :: Int+prematureFinalizerWindow = 50000+++operationTimeout :: Int+operationTimeout = 2000000+++main :: IO ()+main =+ do args <- getArgs+ case args of+ ["--solver"] -> fakeSolver+ _ -> testFinalizer+++testFinalizer :: IO ()+testFinalizer =+ do exe <- getExecutablePath++ -- Keeping projected Solver operations alive must keep the external+ -- process alive too.+ progress "Test 1: live solver operations prevent finalization"+ exited <- newEmptyMVar+ solver <- within "starting the first solver" $+ newSolverNotify exe ["--solver"] Nothing+ (Just (\ec ->+ do progress ("First solver exited: " ++ show ec)+ putMVar exited ec))+ run <- evaluate (command solver)+ finish <- evaluate (stop solver)++ progress " Forcing GC while projected operations are still live"+ performGC++ prematureExit <- timeout prematureFinalizerWindow (takeMVar exited)+ case prematureExit of+ Just _ -> fail "Solver finalizer ran while its operations were live"+ Nothing -> progress " Solver remained alive"++ progress " Sending check-sat after GC"+ result <- within "waiting for check-sat" $+ run (List [Atom "check-sat"])+ unless (result == Atom "sat") $+ fail ("Unexpected check-sat response: " ++ show result)+ progress " Stopping the first solver explicitly"+ _ <- within "stopping the first solver" finish++ -- Once the Solver and its operations are unreachable, its finalizer+ -- must close stdin and allow the external process to exit.+ progress "Test 2: unreachable solver is finalized"+ finalized <- newEmptyMVar+ sawEOF <- newEmptyMVar+ within "using the second solver" $+ useAndForgetSolver exe sawEOF finalized+ progress " Dropped the solver; forcing GC"+ performGC++ finalResult <- timeout operationTimeout $+ do takeMVar sawEOF+ takeMVar finalized+ case finalResult of+ Just _ -> progress " Solver observed EOF and exited"+ Nothing ->+ fail "Solver finalizer did not close stdin and terminate the process"++ progress "Finalizer tests passed"+++{-# NOINLINE useAndForgetSolver #-}+useAndForgetSolver :: FilePath -> MVar () -> MVar ExitCode -> IO ()+useAndForgetSolver exe sawEOF exited =+ do let logger =+ noSolverLogger+ { solverLogStdErr = \message ->+ when (message == eofMessage) $+ do progress " Fake solver observed EOF"+ putMVar sawEOF ()+ }+ config =+ (defaultConfig exe ["--solver"])+ { solverOnExit =+ Just (\ec ->+ do progress (" Second solver exited: " ++ show ec)+ putMVar exited ec)+ , solverLogger = logger+ }+ solver <- newSolverWithConfig config+ result <- command solver (List [Atom "check-sat"])+ unless (result == Atom "sat") $+ fail ("Unexpected check-sat response: " ++ show result)+++fakeSolver :: IO ()+fakeSolver =+ do eof <- isEOF+ if eof+ then hPutStrLn stderr eofMessage+ else do request <- getLine+ case request of+ "(exit)" -> pure ()+ "(check-sat)" -> respond "sat" >> fakeSolver+ _ -> respond "success" >> fakeSolver+ where+ respond response =+ do putStrLn response+ hFlush stdout+++within :: String -> IO a -> IO a+within description action =+ do result <- timeout operationTimeout action+ case result of+ Just value -> pure value+ Nothing -> fail ("Timed out " ++ description)+++progress :: String -> IO ()+progress message =+ do putStrLn message+ hFlush stdout