From a44e1edaa302539fc1a53bf099c77b8085ed4d79 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sat, 3 Mar 2018 14:50:40 +0100 Subject: [PATCH] Terminate running SMT solver when smtbmc is terminated Signed-off-by: Clifford Wolf --- backends/smt2/smtio.py | 32 +++++++++++++++++++++++++++++++- 1 file changed, 31 insertions(+), 1 deletion(-) diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 5bc43acae..34e8cf604 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -16,7 +16,7 @@ # OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. # -import sys, re, os +import sys, re, os, signal import resource, subprocess from copy import deepcopy from select import select @@ -35,6 +35,25 @@ if resource.getrlimit(resource.RLIMIT_STACK)[0] < smtio_stacksize: resource.setrlimit(resource.RLIMIT_STACK, (smtio_stacksize, -1)) +# currently running solvers (so we can kill them) +running_solvers = dict() +got_term_signal = False +solvers_index = 0 + +def sig_handler(signum, frame): + global got_term_signal + if not got_term_signal: + print("<%s>" % signal.Signals(signum).name) + got_term_signal = True + for p in running_solvers.values(): + os.killpg(os.getpgid(p.pid), signal.SIGTERM) + sys.exit(0) + +signal.signal(signal.SIGINT, sig_handler) +signal.signal(signal.SIGHUP, sig_handler) +signal.signal(signal.SIGTERM, sig_handler) + + hex_dict = { "0": "0000", "1": "0001", "2": "0010", "3": "0011", "4": "0100", "5": "0101", "6": "0110", "7": "0111", @@ -66,6 +85,8 @@ class SmtModInfo: class SmtIo: def __init__(self, opts=None): + global solvers_index + self.logic = None self.logic_qf = True self.logic_ax = True @@ -76,6 +97,8 @@ class SmtIo: self.produce_models = True self.smt2cache = [list()] self.p = None + self.p_index = solvers_index + solvers_index += 1 if opts is not None: self.logic = opts.logic @@ -109,6 +132,11 @@ class SmtIo: self.topmod = None self.setup_done = False + def __del__(self): + if self.p is not None: + os.killpg(os.getpgid(self.p.pid), signal.SIGTERM) + del running_solvers[self.p_index] + def setup(self): assert not self.setup_done @@ -241,6 +269,7 @@ class SmtIo: def p_open(self): assert self.p is None self.p = subprocess.Popen(self.popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT) + running_solvers[self.p_index] = self.p self.p_running = True self.p_next = None self.p_queue = Queue() @@ -277,6 +306,7 @@ class SmtIo: self.p.stdin.close() self.p_thread.join() assert not self.p_running + del running_solvers[self.p_index] self.p = None self.p_next = None self.p_queue = None -- 2.30.2