mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

simplify timeout mechanism and fix race conditions there

Browse source
This commit is contained in:
Nuno Lopes 2019-02-21 11:49:41 +00:00
parent f3cd7d646d
commit a76c0fbbfb
2 changed files with 15 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/shell/main.cpp
View file

@ -115,6 +115,7 @@ void display_usage() {
} }
void parse_cmd_line_args(int argc, char ** argv) { void parse_cmd_line_args(int argc, char ** argv) {
long timeout = 0;
int i = 1; int i = 1;
char * eq_pos = nullptr; char * eq_pos = nullptr;
while (i < argc) { while (i < argc) {
@ -216,8 +217,7 @@ void parse_cmd_line_args(int argc, char ** argv) {
else if (strcmp(opt_name, "T") == 0) { else if (strcmp(opt_name, "T") == 0) {
if (!opt_arg) if (!opt_arg)
error("option argument (-T:timeout) is missing."); error("option argument (-T:timeout) is missing.");
long tm = strtol(opt_arg, nullptr, 10); timeout = strtol(opt_arg, nullptr, 10);
set_timeout(tm * 1000);
} }
else if (strcmp(opt_name, "t") == 0) { else if (strcmp(opt_name, "t") == 0) {
if (!opt_arg) if (!opt_arg)
@ -292,6 +292,9 @@ void parse_cmd_line_args(int argc, char ** argv) {
} }
i++; i++;
} }
if (timeout)
set_timeout(timeout * 1000);
} }

26
src/util/timeout.cpp
View file

@ -19,7 +19,6 @@ Revision History:
--*/ --*/
#include<iostream> #include<iostream>
#include "util/z3_omp.h"
#include "util/util.h" #include "util/util.h"
#include "util/timeout.h" #include "util/timeout.h"
#include "util/error_codes.h" #include "util/error_codes.h"
@ -34,26 +33,21 @@ namespace {
class g_timeout_eh : public event_handler { class g_timeout_eh : public event_handler {
public: public:
void operator()(event_handler_caller_t caller_id) override { void operator()(event_handler_caller_t caller_id) override {
#pragma omp critical (g_timeout_cs) std::cout << "timeout\n";
{ m_caller_id = caller_id;
std::cout << "timeout\n"; if (g_on_timeout)
m_caller_id = caller_id; g_on_timeout();
if (g_on_timeout) throw z3_error(ERR_TIMEOUT);
g_on_timeout();
if (g_timeout)
delete g_timeout;
g_timeout = nullptr;
throw z3_error(ERR_TIMEOUT);
}
} }
}; };
} }
void set_timeout(long ms) { static g_timeout_eh eh;
if (g_timeout)
delete g_timeout;
g_timeout = new scoped_timer(ms, new g_timeout_eh()); void set_timeout(long ms) {
SASSERT(!g_timeout);
// this is leaked, but since it's only used in the shell, it's ok
g_timeout = new scoped_timer(ms, &eh);
} }
void register_on_timeout_proc(void (*proc)()) { void register_on_timeout_proc(void (*proc)()) {