diff --git a/osek-verification.cabal b/osek-verification.cabal index ffba188149df1d0abe646cf89459d1a253ecf96f..097b2ab9265bd240c76004d196a5fc8904ee0521 100644 --- a/osek-verification.cabal +++ b/osek-verification.cabal @@ -50,6 +50,7 @@ library , microlens-th >= 0.4 && < 0.5 , unordered-containers >= 0.2 && <0.3 , hashable >= 1.2 && < 1.3 + , unix >= 2.7 && <2.8 default-language: Haskell2010 ghc-options: -Wall -fno-warn-name-shadowing diff --git a/src/Search/Search.hs b/src/Search/Search.hs index e058af209b6be0f929e6186e850d536fc0738f80..56510e7f6db6850097b6328a7e13c40ae8d2088e 100644 --- a/src/Search/Search.hs +++ b/src/Search/Search.hs @@ -18,6 +18,8 @@ import qualified Data.Text.IO as T import System.Exit import System.IO import System.Process +import System.Process.Internals (withProcessHandle, ProcessHandle__(..)) +import System.Posix.Signals (signalProcess, sigKILL) import Data.Aeson import qualified Data.Graph.Inductive as G @@ -130,6 +132,12 @@ driver' elimEpsis dumpJSON debug prog startVertex = do loop +killProcess :: ProcessHandle -> IO () +killProcess handle = withProcessHandle handle $ \ph -> + case ph of + OpenHandle pid -> signalProcess sigKILL pid + _ -> return () + oneProgRun :: FilePath -> DebugOutput -> IORef State -> Maybe [Bool] -> IO () oneProgRun prog debug state trace = do (Just pstdin, Just pstdout, _, handle) <- createProcess (proc prog []) { std_in = CreatePipe, std_out = CreatePipe } @@ -144,7 +152,7 @@ oneProgRun prog debug state trace = do let (next, s') = handleDecision x (s^.curTrace) s writeIORef state s' case next of - Restart -> terminateProcess handle >> mapM_ hClose [pstdin, pstdout] + Restart -> killProcess handle >> mapM_ hClose [pstdin, pstdout] Continue x' -> do makeDecision pstdin state x' loop @@ -152,7 +160,7 @@ oneProgRun prog debug state trace = do EOF -> do getProcessExitCode handle >>= \case Nothing -> -- process still running, send SIGTERM - terminateProcess handle + killProcess handle Just ExitSuccess -> return () -- do nothing Just (ExitFailure code) -> do