From 31681c7ff2a1469f5efc325fc1b3a406e3a85949 Mon Sep 17 00:00:00 2001 From: Andres Notzli Date: Fri, 31 Mar 2017 14:27:05 -0700 Subject: Make signal handlers safer As reported in bug 769, the signal handlers currently use unsafe functions such as dynamic memory allocations and fprintf. This commit fixes the issue by introducing functions for printing statistics in signal handlers (functions with the `safe` prefix). It also avoids copying statistics, which further avoids dynamic memory allocation. The safe printing of statistics has some limitations (it does not support SExprStats or printing CVC4::Result), which should not matter much in practice. Printing statistics in a non-signal handler is not affected by these changes as that uses a separate code path (the functions without the `safe` prefix). Additional changes: - Remove ListStat as it is not used anywhere - Add unit test for safe printing statistics --- src/util/statistics_registry.cpp | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'src/util/statistics_registry.cpp') 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"); -- cgit v1.2.3