From 2a7266f121548064d8e78643a3d9f7cef13f1e8e Mon Sep 17 00:00:00 2001
From: Hans-Peter Deifel <hpd@hpdeifel.de>
Date: Wed, 10 May 2017 13:39:17 +0200
Subject: [PATCH] Kill child process instead of sending SIGTERM
If the child is currently between DisableInterrupts and
EnableInterrupts and we decide to terminate it, it will not respond to
sigterm.
---
osek-verification.cabal | 1 +
src/Search/Search.hs | 12 ++++++++++--
2 files changed, 11 insertions(+), 2 deletions(-)
diff --git a/osek-verification.cabal b/osek-verification.cabal
index ffba188..097b2ab 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 e058af2..56510e7 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
--
GitLab