diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/expr/expr_manager_template.cpp | 4 | ||||
-rw-r--r-- | src/expr/expr_manager_template.h | 8 | ||||
-rw-r--r-- | src/main/command_executor.h | 9 | ||||
-rw-r--r-- | src/main/driver_unified.cpp | 12 | ||||
-rw-r--r-- | src/main/util.cpp | 191 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 4 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 5 | ||||
-rw-r--r-- | src/util/Makefile.am | 2 | ||||
-rw-r--r-- | src/util/safe_print.cpp | 215 | ||||
-rw-r--r-- | src/util/safe_print.h | 99 | ||||
-rw-r--r-- | src/util/statistics.cpp | 15 | ||||
-rw-r--r-- | src/util/statistics.h | 6 | ||||
-rw-r--r-- | src/util/statistics_registry.cpp | 6 | ||||
-rw-r--r-- | src/util/statistics_registry.h | 106 |
14 files changed, 556 insertions, 126 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 */ |