simple-smt 1.0 → 1.0.1
raw patch · 4 files changed
+163/−6 lines, 4 filesdep ~basePVP ok
version bump matches the API change (PVP)
Dependency ranges changed: base
API changes (from Hackage documentation)
Files
- CHANGES +2/−0
- SimpleSMT.hs +10/−5
- 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,7 +166,9 @@ import Text.Read(readMaybe) import Data.Ratio((%), numerator, denominator) import Numeric(showHex, readHex, showFFloat)-import System.Mem.Weak(addFinalizer)+import Foreign.Concurrent(newForeignPtr)+import Foreign.ForeignPtr(withForeignPtr)+import Foreign.Ptr(nullPtr) -- | Results of checking for satisfiability.@@ -337,13 +339,13 @@ -- Close `stdin` when the Haskell Solver object is GC-ed, so that -- we close `stdin` and the solver process exits.- addFinalizer responses (closeHandle hIn)+ finalizer <- newForeignPtr nullPtr (closeHandle hIn) let solver = Solver- { command = runCommand hIn responses- , stop = stopSolver hIn exitResult- , forceStop = forceStopSolver h exitResult+ { command = keepAlive finalizer . runCommand hIn responses+ , stop = keepAlive finalizer (stopSolver hIn exitResult)+ , forceStop = keepAlive finalizer (forceStopSolver h exitResult) } setOption solver ":print-success" "true"@@ -389,6 +391,9 @@ 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: 1.0+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