summaryrefslogtreecommitdiff
path: root/src/util
diff options
context:
space:
mode:
Diffstat (limited to 'src/util')
-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
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback