summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/expr/expr_manager_template.cpp4
-rw-r--r--src/expr/expr_manager_template.h8
-rw-r--r--src/main/command_executor.h9
-rw-r--r--src/main/driver_unified.cpp12
-rw-r--r--src/main/util.cpp191
-rw-r--r--src/smt/smt_engine.cpp4
-rw-r--r--src/smt/smt_engine.h5
-rw-r--r--src/util/Makefile.am2
-rw-r--r--src/util/safe_print.cpp215
-rw-r--r--src/util/safe_print.h99
-rw-r--r--src/util/statistics.cpp15
-rw-r--r--src/util/statistics.h6
-rw-r--r--src/util/statistics_registry.cpp6
-rw-r--r--src/util/statistics_registry.h106
-rw-r--r--test/unit/util/stats_black.h76
15 files changed, 631 insertions, 127 deletions
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 82cabbd3e..cb8ad710f 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -1039,6 +1039,10 @@ SExpr ExprManager::getStatistic(const std::string& name) const throw() {
return d_nodeManager->getStatisticsRegistry()->getStatistic(name);
}
+void ExprManager::safeFlushStatistics(int fd) const {
+ d_nodeManager->getStatisticsRegistry()->safeFlushInformation(fd);
+}
+
namespace expr {
Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap);
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 9e962d970..07ace173c 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -545,7 +545,7 @@ public:
* @param type the type for the new bound variable
*/
Expr mkBoundVar(Type type);
-
+
/**
* Create unique variable of type
*/
@@ -557,6 +557,12 @@ public:
/** Get a reference to the statistics registry for this ExprManager */
SExpr getStatistic(const std::string& name) const throw();
+ /**
+ * Flushes statistics for this ExprManager to a file descriptor. Safe to use
+ * in a signal handler.
+ */
+ void safeFlushStatistics(int fd) const;
+
/** Export an expr to a different ExprManager */
//static Expr exportExpr(const Expr& e, ExprManager* em);
/** Export a type to a different ExprManager */
diff --git a/src/main/command_executor.h b/src/main/command_executor.h
index 4018aeda1..7a33e1db7 100644
--- a/src/main/command_executor.h
+++ b/src/main/command_executor.h
@@ -69,6 +69,15 @@ public:
d_stats.flushInformation(out);
}
+ /**
+ * Flushes statistics to a file descriptor. Safe to use in a signal handler.
+ */
+ void safeFlushStatistics(int fd) const {
+ d_exprMgr.safeFlushStatistics(fd);
+ d_smtEngine->safeFlushStatistics(fd);
+ d_stats.safeFlushInformation(fd);
+ }
+
static void printStatsFilterZeros(std::ostream& out,
const std::string& statsString);
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index efa4f5bd2..6de4f9ff4 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -146,14 +146,20 @@ int runCvc4(int argc, char* argv[], Options& opts) {
}
// Auto-detect input language by filename extension
- const char* filename = inputFromStdin ? "<stdin>" : filenames[0].c_str();
+ std::string filenameStr("<stdin>");
+ if (!inputFromStdin) {
+ // Use swap to avoid copying the string
+ // TODO: use std::move() when switching to c++11
+ filenameStr.swap(filenames[0]);
+ }
+ const char* filename = filenameStr.c_str();
if(opts.getInputLanguage() == language::input::LANG_AUTO) {
if( inputFromStdin ) {
// We can't do any fancy detection on stdin
opts.setInputLanguage(language::input::LANG_CVC4);
} else {
- unsigned len = strlen(filename);
+ unsigned len = filenameStr.size();
if(len >= 5 && !strcmp(".smt2", filename + len - 5)) {
opts.setInputLanguage(language::input::LANG_SMTLIB_V2_5);
} else if(len >= 4 && !strcmp(".smt", filename + len - 4)) {
@@ -264,7 +270,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
pTotalTime);
// Filename statistics
- ReferenceStat< const char* > s_statFilename("filename", filename);
+ ReferenceStat<std::string> s_statFilename("filename", filenameStr);
RegisterStatistic statFilenameReg(&pExecutor->getStatisticsRegistry(),
&s_statFilename);
diff --git a/src/main/util.cpp b/src/main/util.cpp
index d4c00cad2..744122cc8 100644
--- a/src/main/util.cpp
+++ b/src/main/util.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Tim King, Kshitij Bansal
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
** in the top-level source directory) and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
@@ -12,13 +12,17 @@
** \brief Utilities for the main driver.
**
** Utilities for the main driver.
+ **
+ ** It is important to only call async-signal-safe functions from signal
+ ** handlers. See: http://man7.org/linux/man-pages/man7/signal-safety.7.html for
+ ** a list of async-signal-safe POSIX.1 functions.
**/
+#include <string.h>
+#include <cerrno>
#include <cstdio>
#include <cstdlib>
-#include <cerrno>
#include <exception>
-#include <string.h>
#ifndef __WIN32__
@@ -35,6 +39,7 @@
#include "main/main.h"
#include "options/options.h"
#include "smt/smt_engine.h"
+#include "util/safe_print.h"
#include "util/statistics.h"
using CVC4::Exception;
@@ -55,23 +60,26 @@ bool segvSpin = false;
size_t cvc4StackSize;
void* cvc4StackBase;
+void print_statistics() {
+ if (pOptions != NULL && pOptions->getStatistics() && pExecutor != NULL) {
+ if (pTotalTime != NULL && pTotalTime->running()) {
+ pTotalTime->stop();
+ }
+ pExecutor->safeFlushStatistics(STDERR_FILENO);
+ }
+}
+
/** Handler for SIGXCPU, i.e., timeout. */
void timeout_handler(int sig, siginfo_t* info, void*) {
- fprintf(stderr, "CVC4 interrupted by timeout.\n");
- if(pOptions->getStatistics() && pExecutor != NULL) {
- pTotalTime->stop();
- pExecutor->flushStatistics(cerr);
- }
+ safe_print(STDERR_FILENO, "CVC4 interrupted by timeout.\n");
+ print_statistics();
abort();
}
/** Handler for SIGINT, i.e., when the user hits control C. */
void sigint_handler(int sig, siginfo_t* info, void*) {
- fprintf(stderr, "CVC4 interrupted by user.\n");
- if(pOptions->getStatistics() && pExecutor != NULL) {
- pTotalTime->stop();
- pExecutor->flushStatistics(cerr);
- }
+ safe_print(STDERR_FILENO, "CVC4 interrupted by user.\n");
+ print_statistics();
abort();
}
@@ -80,45 +88,58 @@ void segv_handler(int sig, siginfo_t* info, void* c) {
uintptr_t extent = reinterpret_cast<uintptr_t>(cvc4StackBase) - cvc4StackSize;
uintptr_t addr = reinterpret_cast<uintptr_t>(info->si_addr);
#ifdef CVC4_DEBUG
- fprintf(stderr, "CVC4 suffered a segfault in DEBUG mode.\n");
- cerr << "Offending address is " << info->si_addr << endl;
+ safe_print(STDERR_FILENO, "CVC4 suffered a segfault in DEBUG mode.\n");
+ safe_print(STDERR_FILENO, "Offending address is ");
+ safe_print(STDERR_FILENO, info->si_addr);
+ safe_print(STDERR_FILENO, "\n");
//cerr << "base is " << (void*)cvc4StackBase << endl;
//cerr << "size is " << cvc4StackSize << endl;
//cerr << "extent is " << (void*)extent << endl;
if(addr >= extent && addr <= extent + 10*1024) {
- cerr << "Looks like this is likely due to stack overflow." << endl
- << "You might consider increasing the limit with `ulimit -s' or equivalent." << endl;
+ safe_print(STDERR_FILENO,
+ "Looks like this is likely due to stack overflow.\n");
+ safe_print(STDERR_FILENO,
+ "You might consider increasing the limit with `ulimit -s' or "
+ "equivalent.\n");
} else if(addr < 10*1024) {
- cerr << "Looks like a NULL pointer was dereferenced." << endl;
+ safe_print(STDERR_FILENO, "Looks like a NULL pointer was dereferenced.\n");
}
if(!segvSpin) {
- if(pOptions->getStatistics() && pExecutor != NULL) {
- pTotalTime->stop();
- pExecutor->flushStatistics(cerr);
- }
+ print_statistics();
abort();
} else {
- fprintf(stderr, "Spinning so that a debugger can be connected.\n");
- cerr << "Try: gdb " << progName << " " << getpid() << endl
- << " or: gdb --pid=" << getpid() << " " << progName << endl;
+ safe_print(STDERR_FILENO,
+ "Spinning so that a debugger can be connected.\n");
+ safe_print(STDERR_FILENO, "Try: gdb ");
+ safe_print(STDERR_FILENO, progName);
+ safe_print(STDERR_FILENO, " ");
+ safe_print<int64_t>(STDERR_FILENO, getpid());
+ safe_print(STDERR_FILENO, "\n");
+ safe_print(STDERR_FILENO, " or: gdb --pid=");
+ safe_print<int64_t>(STDERR_FILENO, getpid());
+ safe_print(STDERR_FILENO, " ");
+ safe_print(STDERR_FILENO, progName);
+ safe_print(STDERR_FILENO, "\n");
for(;;) {
sleep(60);
}
}
#else /* CVC4_DEBUG */
- fprintf(stderr, "CVC4 suffered a segfault.\n");
- cerr << "Offending address is " << info->si_addr << endl;
+ safe_print(STDERR_FILENO, "CVC4 suffered a segfault.\n");
+ safe_print(STDERR_FILENO, "Offending address is ");
+ safe_print(STDERR_FILENO, info->si_addr);
+ safe_print(STDERR_FILENO, "\n");
if(addr >= extent && addr <= extent + 10*1024) {
- cerr << "Looks like this is likely due to stack overflow." << endl
- << "You might consider increasing the limit with `ulimit -s' or equivalent." << endl;
+ safe_print(STDERR_FILENO,
+ "Looks like this is likely due to stack overflow.\n");
+ safe_print(STDERR_FILENO,
+ "You might consider increasing the limit with `ulimit -s' or "
+ "equivalent.\n");
} else if(addr < 10*1024) {
- cerr << "Looks like a NULL pointer was dereferenced." << endl;
- }
- if(pOptions->getStatistics() && pExecutor != NULL) {
- pTotalTime->stop();
- pExecutor->flushStatistics(cerr);
+ safe_print(STDERR_FILENO, "Looks like a NULL pointer was dereferenced.\n");
}
+ print_statistics();
abort();
#endif /* CVC4_DEBUG */
}
@@ -126,27 +147,31 @@ void segv_handler(int sig, siginfo_t* info, void* c) {
/** Handler for SIGILL (illegal instruction). */
void ill_handler(int sig, siginfo_t* info, void*) {
#ifdef CVC4_DEBUG
- fprintf(stderr, "CVC4 executed an illegal instruction in DEBUG mode.\n");
+ safe_print(STDERR_FILENO,
+ "CVC4 executed an illegal instruction in DEBUG mode.\n");
if(!segvSpin) {
- if(pOptions->getStatistics() && pExecutor != NULL) {
- pTotalTime->stop();
- pExecutor->flushStatistics(cerr);
- }
+ print_statistics();
abort();
} else {
- fprintf(stderr, "Spinning so that a debugger can be connected.\n");
- fprintf(stderr, "Try: gdb %s %u\n", progName, getpid());
- fprintf(stderr, " or: gdb --pid=%u %s\n", getpid(), progName);
+ safe_print(STDERR_FILENO,
+ "Spinning so that a debugger can be connected.\n");
+ safe_print(STDERR_FILENO, "Try: gdb ");
+ safe_print(STDERR_FILENO, progName);
+ safe_print(STDERR_FILENO, " ");
+ safe_print<int64_t>(STDERR_FILENO, getpid());
+ safe_print(STDERR_FILENO, "\n");
+ safe_print(STDERR_FILENO, " or: gdb --pid=");
+ safe_print<int64_t>(STDERR_FILENO, getpid());
+ safe_print(STDERR_FILENO, " ");
+ safe_print(STDERR_FILENO, progName);
+ safe_print(STDERR_FILENO, "\n");
for(;;) {
sleep(60);
}
}
#else /* CVC4_DEBUG */
- fprintf(stderr, "CVC4 executed an illegal instruction.\n");
- if(pOptions->getStatistics() && pExecutor != NULL) {
- pTotalTime->stop();
- pExecutor->flushStatistics(cerr);
- }
+ safe_print(STDERR_FILENO, "CVC4 executed an illegal instruction.\n");
+ print_statistics();
abort();
#endif /* CVC4_DEBUG */
}
@@ -157,39 +182,46 @@ static terminate_handler default_terminator;
void cvc4unexpected() {
#if defined(CVC4_DEBUG) && !defined(__WIN32__)
- fprintf(stderr, "\n"
- "CVC4 threw an \"unexpected\" exception (one that wasn't properly "
- "specified\nin the throws() specifier for the throwing function)."
- "\n\n");
+ safe_print(STDERR_FILENO,
+ "\n"
+ "CVC4 threw an \"unexpected\" exception (one that wasn't properly "
+ "specified\nin the throws() specifier for the throwing function)."
+ "\n\n");
const char* lastContents = LastExceptionBuffer::currentContents();
if(lastContents == NULL) {
- fprintf(stderr,
- "The exception is unknown (maybe it's not a CVC4::Exception).\n\n");
+ safe_print(
+ STDERR_FILENO,
+ "The exception is unknown (maybe it's not a CVC4::Exception).\n\n");
} else {
- fprintf(stderr, "The exception is:\n%s\n\n", lastContents);
+ safe_print(STDERR_FILENO, "The exception is:\n");
+ safe_print(STDERR_FILENO, lastContents);
+ safe_print(STDERR_FILENO, "\n\n");
}
if(!segvSpin) {
- if(pOptions->getStatistics() && pExecutor != NULL) {
- pTotalTime->stop();
- pExecutor->flushStatistics(cerr);
- }
+ print_statistics();
set_terminate(default_terminator);
} else {
- fprintf(stderr, "Spinning so that a debugger can be connected.\n");
- fprintf(stderr, "Try: gdb %s %u\n", progName, getpid());
- fprintf(stderr, " or: gdb --pid=%u %s\n", getpid(), progName);
+ safe_print(STDERR_FILENO,
+ "Spinning so that a debugger can be connected.\n");
+ safe_print(STDERR_FILENO, "Try: gdb ");
+ safe_print(STDERR_FILENO, progName);
+ safe_print(STDERR_FILENO, " ");
+ safe_print<int64_t>(STDERR_FILENO, getpid());
+ safe_print(STDERR_FILENO, "\n");
+ safe_print(STDERR_FILENO, " or: gdb --pid=");
+ safe_print<int64_t>(STDERR_FILENO, getpid());
+ safe_print(STDERR_FILENO, " ");
+ safe_print(STDERR_FILENO, progName);
+ safe_print(STDERR_FILENO, "\n");
for(;;) {
sleep(60);
}
}
#else /* CVC4_DEBUG */
- fprintf(stderr, "CVC4 threw an \"unexpected\" exception.\n");
- if(pOptions->getStatistics() && pExecutor != NULL) {
- pTotalTime->stop();
- pExecutor->flushStatistics(cerr);
- }
+ safe_print(STDERR_FILENO, "CVC4 threw an \"unexpected\" exception.\n");
+ print_statistics();
set_terminate(default_terminator);
#endif /* CVC4_DEBUG */
}
@@ -198,26 +230,21 @@ void cvc4terminate() {
set_terminate(default_terminator);
#ifdef CVC4_DEBUG
LastExceptionBuffer* current = LastExceptionBuffer::getCurrent();
- LastExceptionBuffer::setCurrent(NULL);
+ LastExceptionBuffer::setCurrent(NULL);
delete current;
- fprintf(stderr, "\n"
- "CVC4 was terminated by the C++ runtime.\n"
- "Perhaps an exception was thrown during stack unwinding. "
- "(Don't do that.)\n");
- if(pOptions->getStatistics() && pExecutor != NULL) {
- pTotalTime->stop();
- pExecutor->flushStatistics(cerr);
- }
+ safe_print(STDERR_FILENO,
+ "\n"
+ "CVC4 was terminated by the C++ runtime.\n"
+ "Perhaps an exception was thrown during stack unwinding. "
+ "(Don't do that.)\n");
+ print_statistics();
default_terminator();
#else /* CVC4_DEBUG */
- fprintf(stderr,
- "CVC4 was terminated by the C++ runtime.\n"
- "Perhaps an exception was thrown during stack unwinding.\n");
- if(pOptions->getStatistics() && pExecutor != NULL) {
- pTotalTime->stop();
- pExecutor->flushStatistics(cerr);
- }
+ safe_print(STDERR_FILENO,
+ "CVC4 was terminated by the C++ runtime.\n"
+ "Perhaps an exception was thrown during stack unwinding.\n");
+ print_statistics();
default_terminator();
#endif /* CVC4_DEBUG */
}
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 4e75a7937..b5fbecf7d 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -5573,6 +5573,10 @@ SExpr SmtEngine::getStatistic(std::string name) const throw() {
return d_statisticsRegistry->getStatistic(name);
}
+void SmtEngine::safeFlushStatistics(int fd) const {
+ d_statisticsRegistry->safeFlushInformation(fd);
+}
+
void SmtEngine::setUserAttribute(const std::string& attr, Expr expr, std::vector<Expr> expr_values, std::string str_value) {
SmtScope smts(this);
std::vector<Node> node_values;
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index c3cb54685..a27259ff4 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -722,6 +722,11 @@ public:
SExpr getStatistic(std::string name) const throw();
/**
+ * Flush statistic from this SmtEngine. Safe to use in a signal handler.
+ */
+ void safeFlushStatistics(int fd) const;
+
+ /**
* Returns the most recent result of checkSat/query or (set-info :status).
*/
Result getStatusOfLastCommand() const throw() {
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index a8e37c93c..cd6f0e11c 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -44,6 +44,8 @@ libutil_la_SOURCES = \
resource_manager.h \
result.cpp \
result.h \
+ safe_print.cpp \
+ safe_print.h \
sexpr.cpp \
sexpr.h \
smt2_quote_string.cpp \
diff --git a/src/util/safe_print.cpp b/src/util/safe_print.cpp
new file mode 100644
index 000000000..ff5a7aa7e
--- /dev/null
+++ b/src/util/safe_print.cpp
@@ -0,0 +1,215 @@
+/********************* */
+/*! \file safe_print.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Definition of print functions that are safe to use in a signal
+ ** handler.
+ **
+ ** Signal handlers only allow a very limited set of operations, e.g. dynamic
+ ** memory allocation is not possible. This set of functions can be used to
+ ** print information from a signal handler. All output is written to file
+ ** descriptors using the async-signal-safe write() function.
+ **/
+
+#include "safe_print.h"
+
+#include <unistd.h>
+
+/* Size of buffers used */
+#define BUFFER_SIZE 20
+
+namespace CVC4 {
+
+template <>
+void safe_print(int fd, const std::string& msg) {
+ // Print characters one by one instead of using
+ // string::data()/string::c_str() to avoid allocations (pre-c++11)
+ for (size_t i = 0; i < msg.length(); i++) {
+ if (write(fd, &(msg[i]), 1) != 1) {
+ abort();
+ }
+ }
+}
+
+template <>
+void safe_print(int fd, const int64_t& _i) {
+ char buf[BUFFER_SIZE];
+ int64_t i = _i;
+
+ if (i == 0) {
+ safe_print(fd, "0");
+ return;
+ } else if (i < 0) {
+ safe_print(fd, "-");
+ i *= -1;
+ }
+
+ // This loop fills the buffer from the end. The number of elements in the
+ // buffer is BUFER_SIZE - idx - 1 and they start at position idx + 1.
+ ssize_t idx = BUFFER_SIZE - 1;
+ while (i != 0 && idx >= 0) {
+ buf[idx] = '0' + i % 10;
+ i /= 10;
+ idx--;
+ }
+
+ ssize_t nbyte = BUFFER_SIZE - idx - 1;
+ if (write(fd, buf + idx + 1, nbyte) != nbyte) {
+ abort();
+ }
+}
+
+template <>
+void safe_print(int fd, const int32_t& i) {
+ safe_print<int64_t>(fd, i);
+}
+
+template <>
+void safe_print(int fd, const uint64_t& _i) {
+ char buf[BUFFER_SIZE];
+ uint64_t i = _i;
+
+ if (i == 0) {
+ safe_print(fd, "0");
+ return;
+ }
+
+ // This loop fills the buffer from the end. The number of elements in the
+ // buffer is BUFER_SIZE - idx - 1 and they start at position idx + 1.
+ ssize_t idx = BUFFER_SIZE - 1;
+ while (i != 0 && idx >= 0) {
+ buf[idx] = '0' + i % 10;
+ i /= 10;
+ idx--;
+ }
+
+ ssize_t nbyte = BUFFER_SIZE - idx - 1;
+ if (write(fd, buf + idx + 1, nbyte) != nbyte) {
+ abort();
+ }
+}
+
+template <>
+void safe_print(int fd, const uint32_t& i) {
+ safe_print<uint64_t>(fd, i);
+}
+
+template <>
+void safe_print(int fd, const double& _d) {
+ // Note: this print function for floating-point values is optimized for
+ // simplicity, not correctness or performance.
+ char buf[BUFFER_SIZE];
+ double d = _d;
+
+ ssize_t i = 0;
+ int64_t v = static_cast<int64_t>(d);
+ d -= v;
+
+ if (d < 0.0) {
+ d *= -1.0;
+ }
+
+ safe_print<int64_t>(fd, v);
+ safe_print(fd, ".");
+
+ // Print decimal digits as long as the remaining value is larger than zero
+ // and print at least one digit.
+ while (i == 0 || (d > 0.0 && i < BUFFER_SIZE)) {
+ d *= 10.0;
+ char c = static_cast<char>(d);
+ buf[i] = '0' + c;
+ d -= c;
+ i++;
+ }
+ if (i == 0) {
+ safe_print(fd, "0");
+ } else if (write(fd, buf, i) != i) {
+ abort();
+ }
+}
+
+template <>
+void safe_print(int fd, const float& f) {
+ safe_print<double>(fd, (double)f);
+}
+
+template <>
+void safe_print(int fd, const bool& b) {
+ if (b) {
+ safe_print(fd, "true");
+ } else {
+ safe_print(fd, "false");
+ }
+}
+
+template <>
+void safe_print(int fd, void* const& addr) {
+ safe_print_hex(fd, (uint64_t)addr);
+}
+
+template <>
+void safe_print(int fd, const timespec& t) {
+ safe_print<uint64_t>(fd, t.tv_sec);
+ safe_print(fd, ".");
+ safe_print_right_aligned(fd, t.tv_nsec, 9);
+}
+
+void safe_print_hex(int fd, uint64_t i) {
+ char buf[BUFFER_SIZE];
+
+ safe_print(fd, "0x");
+ if (i == 0) {
+ safe_print(fd, "0");
+ return;
+ }
+
+ // This loop fills the buffer from the end. The number of elements in the
+ // buffer is BUFER_SIZE - idx - 1 and they start at position idx + 1.
+ size_t idx = BUFFER_SIZE - 1;
+ while (i != 0 && idx >= 0) {
+ char current = i % 16;
+ if (current <= 9) {
+ buf[idx] = '0' + current;
+ } else {
+ buf[idx] = 'a' + current - 10;
+ }
+ i /= 16;
+ idx--;
+ }
+
+ ssize_t nbyte = BUFFER_SIZE - idx - 1;
+ if (write(fd, buf + idx + 1, nbyte) != nbyte) {
+ abort();
+ }
+}
+
+void safe_print_right_aligned(int fd, uint64_t i, ssize_t width) {
+ char buf[BUFFER_SIZE];
+
+ // Make sure that the result fits in the buffer
+ width = (width < BUFFER_SIZE) ? width : BUFFER_SIZE;
+
+ for (ssize_t j = 0; j < width; j++) {
+ buf[j] = '0';
+ }
+
+ ssize_t idx = width - 1;
+ while (i != 0 && idx >= 0) {
+ buf[idx] = '0' + i % 10;
+ i /= 10;
+ idx--;
+ }
+
+ if (write(fd, buf, width) != width) {
+ abort();
+ }
+}
+
+} /* CVC4 namespace */
diff --git a/src/util/safe_print.h b/src/util/safe_print.h
new file mode 100644
index 000000000..637d00d00
--- /dev/null
+++ b/src/util/safe_print.h
@@ -0,0 +1,99 @@
+/********************* */
+/*! \file safe_print.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Print functions that are safe to use in a signal handler.
+ **
+ ** Signal handlers only allow a very limited set of operations, e.g. dynamic
+ ** memory allocation is not possible. This set of functions can be used to
+ ** print information from a signal handler.
+ **
+ ** The safe_print function takes a template parameter T and prints an argument
+ ** of type const T& to avoid copying, e.g. when printing std::strings. For
+ ** consistency, we also pass primitive types by reference (otherwise, functions
+ ** in statistics_registry.h would require specialization or we would have to
+ ** use function overloading).
+ **
+ ** This header is a "cvc4_private_library.h" header because it is private but
+ ** the safe_print functions are used in the driver. See also the description
+ ** of "statistics_registry.h" for more information on
+ ** "cvc4_private_library.h".
+ **/
+
+#include "cvc4_private_library.h"
+
+#ifndef __CVC4__SAFE_PRINT_H
+#define __CVC4__SAFE_PRINT_H
+
+#if __cplusplus >= 201103L
+// For c++11 and newer
+#include <cstdint>
+#else
+#include <stdint.h>
+#endif
+
+#include <unistd.h>
+
+#include "lib/clock_gettime.h"
+#include "util/result.h"
+
+namespace CVC4 {
+
+/**
+ * Prints arrays of chars (e.g. string literals) of length N. Safe to use in a
+ * signal handler.
+ */
+template <size_t N>
+void CVC4_PUBLIC safe_print(int fd, const char (&msg)[N]) {
+ ssize_t nb = N - 1;
+ if (write(fd, msg, nb) != nb) {
+ abort();
+ }
+}
+
+/** Prints a variable of type T. Safe to use in a signal handler. */
+template <typename T>
+void CVC4_PUBLIC safe_print(int fd, const T& msg) {
+ safe_print(fd, "<unsupported>");
+}
+
+template <>
+void CVC4_PUBLIC safe_print(int fd, const std::string& msg);
+template <>
+void CVC4_PUBLIC safe_print(int fd, const int64_t& _i);
+template <>
+void CVC4_PUBLIC safe_print(int fd, const int32_t& i);
+template <>
+void CVC4_PUBLIC safe_print(int fd, const uint64_t& _i);
+template <>
+void CVC4_PUBLIC safe_print(int fd, const uint32_t& i);
+template <>
+void CVC4_PUBLIC safe_print(int fd, const double& _d);
+template <>
+void CVC4_PUBLIC safe_print(int fd, const float& f);
+template <>
+void CVC4_PUBLIC safe_print(int fd, const bool& b);
+template <>
+void CVC4_PUBLIC safe_print(int fd, void* const& addr);
+template <>
+void CVC4_PUBLIC safe_print(int fd, const timespec& t);
+
+/** Prints an integer in hexadecimal. Safe to use in a signal handler. */
+void safe_print_hex(int fd, uint64_t i);
+
+/**
+ * Prints a right aligned number. Fills up remaining space with zeros. Safe to
+ * use in a signal handler.
+ */
+void safe_print_right_aligned(int fd, uint64_t i, ssize_t width);
+
+} /* CVC4 namespace */
+
+#endif /* __CVC4__SAFE_PRINT_H */
diff --git a/src/util/statistics.cpp b/src/util/statistics.cpp
index 368335f7e..73ea5b1b1 100644
--- a/src/util/statistics.cpp
+++ b/src/util/statistics.cpp
@@ -19,6 +19,7 @@
#include <typeinfo>
+#include "util/safe_print.h"
#include "util/statistics_registry.h" // for details about class Stat
@@ -116,6 +117,20 @@ void StatisticsBase::flushInformation(std::ostream &out) const {
#endif /* CVC4_STATISTICS_ON */
}
+void StatisticsBase::safeFlushInformation(int fd) const {
+#ifdef CVC4_STATISTICS_ON
+ for (StatSet::iterator i = d_stats.begin(); i != d_stats.end(); ++i) {
+ Stat* s = *i;
+ if (d_prefix.size() != 0) {
+ safe_print(fd, d_prefix.c_str());
+ safe_print(fd, s_regDelim.c_str());
+ }
+ s->safeFlushStat(fd);
+ safe_print(fd, "\n");
+ }
+#endif /* CVC4_STATISTICS_ON */
+}
+
SExpr StatisticsBase::getStatistic(std::string name) const {
SExpr value;
IntStat s(name, 0);
diff --git a/src/util/statistics.h b/src/util/statistics.h
index 663d2071b..bdc8ad6a2 100644
--- a/src/util/statistics.h
+++ b/src/util/statistics.h
@@ -84,6 +84,12 @@ public:
/** Flush all statistics to the given output stream. */
void flushInformation(std::ostream& out) const;
+ /**
+ * Flush all statistics to the given file descriptor. Safe to use in a signal
+ * handler.
+ */
+ void safeFlushInformation(int fd) const;
+
/** Get the value of a named statistic. */
SExpr getStatistic(std::string name) const;
diff --git a/src/util/statistics_registry.cpp b/src/util/statistics_registry.cpp
index cb8e1ce90..4b0626048 100644
--- a/src/util/statistics_registry.cpp
+++ b/src/util/statistics_registry.cpp
@@ -182,6 +182,12 @@ void StatisticsRegistry::flushInformation(std::ostream &out) const {
#endif /* CVC4_STATISTICS_ON */
}
+void StatisticsRegistry::safeFlushInformation(int fd) const {
+#ifdef CVC4_STATISTICS_ON
+ this->StatisticsBase::safeFlushInformation(fd);
+#endif /* CVC4_STATISTICS_ON */
+}
+
void TimerStat::start() {
if(__CVC4_USE_STATISTICS) {
PrettyCheckArgument(!d_running, *this, "timer already running");
diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h
index 4f2c356e8..1206a3e4a 100644
--- a/src/util/statistics_registry.h
+++ b/src/util/statistics_registry.h
@@ -47,6 +47,7 @@
#include "base/exception.h"
#include "lib/clock_gettime.h"
+#include "util/safe_print.h"
#include "util/statistics.h"
namespace CVC4 {
@@ -109,6 +110,13 @@ public:
virtual void flushInformation(std::ostream& out) const = 0;
/**
+ * Flush the value of this statistic to a file descriptor. Should finish the
+ * output with an end-of-line character. Should be safe to use in a signal
+ * handler.
+ */
+ virtual void safeFlushInformation(int fd) const = 0;
+
+ /**
* Flush the name,value pair of this statistic to an output stream.
* Uses the statistic delimiter string between name and value.
*
@@ -121,6 +129,20 @@ public:
}
}
+ /**
+ * Flush the name,value pair of this statistic to a file descriptor. Uses the
+ * statistic delimiter string between name and value.
+ *
+ * May be redefined by a child class
+ */
+ virtual void safeFlushStat(int fd) const {
+ if (__CVC4_USE_STATISTICS) {
+ safe_print(fd, d_name.c_str());
+ safe_print(fd, ", ");
+ safeFlushInformation(fd);
+ }
+ }
+
/** Get the name of this statistic. */
const std::string& getName() const {
return d_name;
@@ -210,6 +232,12 @@ public:
}
}
+ virtual void safeFlushInformation(int fd) const {
+ if (__CVC4_USE_STATISTICS) {
+ safe_print<T>(fd, getData());
+ }
+ }
+
SExpr getValue() const {
return mkSExpr(getData());
}
@@ -298,7 +326,6 @@ public:
};/* class ReferenceStat<T> */
-
/**
* A data statistic that keeps a T and sets it with setData().
*
@@ -340,7 +367,6 @@ public:
};/* class BackedStat<T> */
-
/**
* A wrapper Stat for another Stat.
*
@@ -455,6 +481,10 @@ public:
out << d_sized.size();
}
+ void safeFlushInformation(int fd) const {
+ safe_print<uint64_t>(fd, d_sized.size());
+ }
+
SExpr getValue() const {
return SExpr(Integer(d_sized.size()));
}
@@ -522,6 +552,12 @@ public:
out << d_data << std::endl;
}
+ virtual void safeFlushInformation(int fd) const {
+ // SExprStat is only used in statistics.cpp in copyFrom, which we cannot
+ // do in a signal handler anyway.
+ safe_print(fd, "<unsupported>");
+ }
+
SExpr getValue() const {
return d_data;
}
@@ -529,44 +565,6 @@ public:
};/* class SExprStat */
template <class T>
-class ListStat : public Stat {
-private:
- typedef std::vector<T> List;
- List d_list;
-public:
-
- /**
- * Construct an integer-valued statistic with the given name and
- * initial value.
- */
- ListStat(const std::string& name) : Stat(name) {}
- ~ListStat() {}
-
- void flushInformation(std::ostream& out) const{
- if(__CVC4_USE_STATISTICS) {
- typename List::const_iterator i = d_list.begin(), end = d_list.end();
- out << "[";
- if(i != end){
- out << *i;
- ++i;
- for(; i != end; ++i){
- out << ", " << *i;
- }
- }
- out << "]";
- }
- }
-
- ListStat& operator<<(const T& val){
- if(__CVC4_USE_STATISTICS) {
- d_list.push_back(val);
- }
- return (*this);
- }
-
-};/* class ListStat */
-
-template <class T>
class HistogramStat : public Stat {
private:
typedef std::map<T, unsigned int> Histogram;
@@ -595,6 +593,28 @@ public:
}
}
+ virtual void safeFlushInformation(int fd) const {
+ if (__CVC4_USE_STATISTICS) {
+ typename Histogram::const_iterator i = d_hist.begin();
+ typename Histogram::const_iterator end = d_hist.end();
+ safe_print(fd, "[");
+ while (i != end) {
+ const T& key = (*i).first;
+ unsigned int count = (*i).second;
+ safe_print(fd, "(");
+ safe_print<T>(fd, key);
+ safe_print(fd, " : ");
+ safe_print<uint64_t>(fd, count);
+ safe_print(fd, ")");
+ ++i;
+ if (i != end) {
+ safe_print(fd, ", ");
+ }
+ }
+ safe_print(fd, "]");
+ }
+ }
+
HistogramStat& operator<<(const T& val){
if(__CVC4_USE_STATISTICS) {
if(d_hist.find(val) == d_hist.end()){
@@ -643,6 +663,8 @@ public:
virtual void flushInformation(std::ostream& out) const;
+ virtual void safeFlushInformation(int fd) const;
+
SExpr getValue() const {
std::vector<SExpr> v;
for(StatSet::iterator i = d_stats.begin(); i != d_stats.end(); ++i) {
@@ -708,6 +730,10 @@ public:
timespec getData() const;
+ virtual void safeFlushInformation(int fd) const {
+ safe_print<timespec>(fd, d_data);
+ }
+
SExpr getValue() const;
};/* class TimerStat */
diff --git a/test/unit/util/stats_black.h b/test/unit/util/stats_black.h
index c5b0d46bb..9f06b469f 100644
--- a/test/unit/util/stats_black.h
+++ b/test/unit/util/stats_black.h
@@ -15,9 +15,10 @@
**/
#include <cxxtest/TestSuite.h>
+#include <fcntl.h>
+#include <ctime>
#include <sstream>
#include <string>
-#include <ctime>
#include "lib/clock_gettime.h"
#include "util/statistics_registry.h"
@@ -62,6 +63,22 @@ public:
// getData
// operator=
+ BackedStat<double> backedDouble("backedDouble", 16.5);
+ BackedStat<double> backedNegDouble("backedNegDouble", -16.5);
+ BackedStat<double> backedDoubleNoDec("backedDoubleNoDec", 2.0);
+ BackedStat<bool> backedBool("backedBool", true);
+ BackedStat<void*> backedAddr("backedDouble", (void*)0xDEADBEEF);
+ HistogramStat<int64_t> histStat("hist");
+ histStat << 5;
+ histStat << 6;
+ histStat << 5;
+ histStat << 10;
+ histStat << 10;
+ histStat << 0;
+
+ // A statistic with no safe_print support
+ BackedStat<string*> backedUnsupported("backedUnsupported", &bar);
+
IntStat sInt("my int", 10);
TimerStat sTimer("a timer ! for measuring time");
@@ -104,6 +121,63 @@ public:
sstr.str("");
sTimer.flushInformation(sstr);
TS_ASSERT_EQUALS(sstr.str(), "0.000000000");
+
+ // Test safeFlushInformation (and safe_print functions)
+ char tmp_filename[] = "testXXXXXX";
+ int fd = mkstemp(tmp_filename);
+ TS_ASSERT_DIFFERS(fd, -1);
+ refStr.safeFlushInformation(fd);
+ safe_print(fd, "\n");
+ refStr2.safeFlushInformation(fd);
+ safe_print(fd, "\n");
+ backedStr.safeFlushInformation(fd);
+ safe_print(fd, "\n");
+ sInt.safeFlushInformation(fd);
+ safe_print(fd, "\n");
+ sTimer.safeFlushInformation(fd);
+ safe_print(fd, "\n");
+ backedDouble.safeFlushInformation(fd);
+ safe_print(fd, "\n");
+ backedNegDouble.safeFlushInformation(fd);
+ safe_print(fd, "\n");
+ backedDoubleNoDec.safeFlushInformation(fd);
+ safe_print(fd, "\n");
+ backedAddr.safeFlushInformation(fd);
+ safe_print(fd, "\n");
+ backedBool.safeFlushInformation(fd);
+ safe_print(fd, "\n");
+ histStat.safeFlushInformation(fd);
+ safe_print(fd, "\n");
+ backedUnsupported.safeFlushInformation(fd);
+ off_t file_size = lseek(fd, 0, SEEK_CUR);
+ close(fd);
+
+ char* buf = new char[file_size];
+ fd = open(tmp_filename, O_RDONLY);
+ TS_ASSERT_DIFFERS(fd, -1);
+ ssize_t n_read = pread(fd, buf, file_size, 0);
+ TS_ASSERT_EQUALS(n_read, file_size);
+ close(fd);
+
+ const char* expected =
+ "a different string\n"
+ "bar and with an addition\n"
+ "baz\n"
+ "100\n"
+ "0.000000000\n"
+ "16.5\n"
+ "-16.5\n"
+ "2.0\n"
+ "0xdeadbeef\n"
+ "true\n"
+ "[(0 : 1), (5 : 2), (6 : 1), (10 : 2)]\n"
+ "<unsupported>";
+ std::cout << buf << std::endl;
+ TS_ASSERT(strncmp(expected, buf, file_size) == 0);
+ delete[] buf;
+
+ int ret = remove(tmp_filename);
+ TS_ASSERT_EQUALS(ret, 0);
#endif /* CVC4_STATISTICS_ON */
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback