diff --git a/autoverify/verifier/complete/abcrown/verifier.py b/autoverify/verifier/complete/abcrown/verifier.py index 5040919..3680b75 100644 --- a/autoverify/verifier/complete/abcrown/verifier.py +++ b/autoverify/verifier/complete/abcrown/verifier.py @@ -48,7 +48,6 @@ def contexts(self) -> list[ContextManager[None]]: # Ideally just keep track of PIDs rather than pkill name matching return [ cwd(self.tool_path / "complete_verifier"), - pkill_matches(["python abcrown.py"]), ] def _parse_result( diff --git a/autoverify/verifier/complete/nnenum/verifier.py b/autoverify/verifier/complete/nnenum/verifier.py index c31c2af..d87ff54 100644 --- a/autoverify/verifier/complete/nnenum/verifier.py +++ b/autoverify/verifier/complete/nnenum/verifier.py @@ -46,7 +46,6 @@ def contexts(self) -> list[ContextManager[None]]: return [ cwd(self.tool_path / "src"), environment(OPENBLAS_NUM_THREADS="1", OMP_NUM_THREADS="1"), - pkill_matches(["python -m nnenum.nnenum"]), ] def _parse_result( diff --git a/autoverify/verifier/complete/ovalbab/verifier.py b/autoverify/verifier/complete/ovalbab/verifier.py index 624e47c..ff76d69 100644 --- a/autoverify/verifier/complete/ovalbab/verifier.py +++ b/autoverify/verifier/complete/ovalbab/verifier.py @@ -52,7 +52,6 @@ def contexts(self) -> list[ContextManager[None]]: find_conda_lib(self.conda_env_name, "libcudart.so.11.0") ) ), - pkill_matches(["python tools/bab_tools/bab_from_vnnlib.py"]), ] def _parse_result( diff --git a/autoverify/verifier/verifier.py b/autoverify/verifier/verifier.py index b38dbe6..7a98b51 100644 --- a/autoverify/verifier/verifier.py +++ b/autoverify/verifier/verifier.py @@ -313,44 +313,24 @@ def _run_verification( for context in contexts: stack.enter_context(context) - process = subprocess.Popen( - run_cmd, - executable="/bin/bash", + before_t = time.time() + + process = subprocess.run( + run_cmd, + executable="/bin/bash", stdout=subprocess.PIPE, stderr=subprocess.STDOUT, shell=True, universal_newlines=True, - preexec_fn=os.setsid, - ) - - before_t = time.time() - self._timeout_event: threading.Event | None = threading.Event() - - def _terminate(timeout_sec): - assert self._timeout_event - on_time = self._timeout_event.wait(timeout_sec) - - if not on_time: - global result - result = "TIMEOUT" # type: ignore - - if pid_exists(process.pid): - os.killpg(os.getpgid(process.pid), signal.SIGTERM) - - t = threading.Thread(target=_terminate, args=[timeout]) - t.start() + preexec_fn=os.setsid) assert process.stdout - for line in iter(process.stdout.readline, ""): - output_lines.append(line) + output_str = process.stdout - process.stdout.close() - return_code = process.wait() + return_code = process.returncode took_t = time.time() - before_t - self._timeout_event.set() - output_str = "".join(output_lines) counter_example: str | None = None if result != "TIMEOUT": @@ -361,8 +341,6 @@ def _terminate(timeout_sec): output_str, result_file ) - self._timeout_event = None - return CompleteVerificationData( result, # type: ignore took_t,