diff options
Diffstat (limited to 'src/util')
-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 |
7 files changed, 409 insertions, 40 deletions
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 */ |