diff options
Diffstat (limited to 'src/util/statistics_registry.h')
| -rw-r--r-- | src/util/statistics_registry.h | 273 |
1 files changed, 171 insertions, 102 deletions
diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h index 098d88c07..7a714012e 100644 --- a/src/util/statistics_registry.h +++ b/src/util/statistics_registry.h @@ -1,6 +1,6 @@ /****************************************************************************** * Top contributors (to current version): - * Morgan Deters, Gereon Kremer, Tim King + * Gereon Kremer * * This file is part of the cvc5 project. * @@ -10,26 +10,9 @@ * directory for licensing information. * **************************************************************************** * - * Statistics utility classes - * - * Statistics utility classes, including classes for holding (and referring - * to) statistics, the statistics registry, and some other associated - * classes. - * - * This file is somewhat unique in that it is a "cvc5_private_library.h" - * header. Because of this, most classes need to be marked as CVC4_EXPORT. - * This is because CVC4_EXPORT is connected to the visibility of the linkage - * in the object files for the class. It does not dictate what headers are - * installed. - * Because the StatisticsRegistry and associated classes are built into - * libutil, which is used by libcvc4, and then later used by the libmain - * without referring to libutil as well. Thus the without marking these as - * CVC4_EXPORT the symbols would be external in libutil, internal in libcvc4, - * and not be visible to libmain and linking would fail. - * You can debug this using "nm" on the .so and .o files in the builds/ - * directory. See - * http://eli.thegreenplace.net/2013/07/09/library-order-in-static-linking - * for a longer discussion on symbol visibility. + * Central statistics registry. + * + * The StatisticsRegistry that issues statistic proxy objects. */ /** @@ -85,117 +68,203 @@ #ifndef CVC5__STATISTICS_REGISTRY_H #define CVC5__STATISTICS_REGISTRY_H -#include <ctime> -#include <iomanip> +#include <iostream> #include <map> -#include <sstream> -#include <vector> - -#ifdef CVC5_STATISTICS_ON -#define CVC5_USE_STATISTICS true -#else -#define CVC5_USE_STATISTICS false -#endif +#include <memory> +#include <typeinfo> -#include "base/exception.h" -#include "cvc4_export.h" -#include "util/safe_print.h" -#include "util/statistics.h" -#include "util/stats_base.h" +#include "base/check.h" +#include "util/statistics_stats.h" +#include "util/statistics_value.h" namespace cvc5 { -/** A statistic that contains a SExpr. */ -class SExprStat : public Stat { -private: - SExpr d_data; +struct StatisticBaseValue; -public: +/** + * The central registry for statistics. + * Internally stores statistic data objects and issues corresponding proxy + * objects to modules that want to expose statistics. + * Provides registration methods (e.g. `registerAverage` or + * `registerHistogram<T>`) that return the proxy object. + * The different statistics are explained in more detail in statistics_stats.h + * + * Every statistic is identified by a name. If a statistic with the given + * name is already registered, the registry issues another proxy object + * for that name using the same data it already holds for this name. + * While this makes perfect sense for most statistic types, it may lead to + * unexpected (though not undefined) behaviour for others. For a reference + * statistic, for example, the internal data will simply point to the object + * registered last. + * Note that the type of the re-registered statistic must always match + * the type of the previously registered statistic with the same name. + * + * We generally distinguish between public (non-expert) and private (expert) + * statistics. By default, `--stats` only shows public statistics. Private + * ones are printed as well if `--all-statistics` is set. + * All registration methods have a trailing argument `expert`, defaulting to + * true. + * + * If statistics are disabled entirely (i.e. the cmake option + * `ENABLE_STATISTICS` is not set), the registry still issues proxy objects + * that can be used normally. + * However, no data is stored in the registry and the modification functions + * of the proxy objects do nothing. + */ +class StatisticsRegistry +{ + public: + friend std::ostream& operator<<(std::ostream& os, + const StatisticsRegistry& sr); + + using Snapshot = std::map<std::string, StatExportData>; /** - * Construct a SExpr-valued statistic with the given name and - * initial value. + * If `registerPublic` is true, all statistics that are public are + * pre-registered as such. This argument mostly exists so that unit tests + * can disable this pre-registration. */ - SExprStat(const std::string& name, const SExpr& init) : - Stat(name), d_data(init){} + StatisticsRegistry(bool registerPublic = true); - void flushInformation(std::ostream& out) const override + /** Register a new running average statistic for `name` */ + + AverageStat registerAverage(const std::string& name, bool expert = true); + /** Register a new histogram statistic for `name` */ + template <typename T> + HistogramStat<T> registerHistogram(const std::string& name, + bool expert = true) { - out << d_data; + return registerStat<HistogramStat<T>>(name, expert); } - void safeFlushInformation(int fd) const override + /** Register a new integer statistic for `name` */ + IntStat registerInt(const std::string& name, bool expert = true); + + /** Register a new reference statistic for `name` */ + template <typename T> + ReferenceStat<T> registerReference(const std::string& name, + bool expert = true) { - // SExprStat is only used in statistics.cpp in copyFrom, which we cannot - // do in a signal handler anyway. - safe_print(fd, "<unsupported>"); + return registerStat<ReferenceStat<T>>(name, expert); + } + /** + * Register a new reference statistic for `name` and initialize it to + * refer to `t`. + */ + template <typename T> + ReferenceStat<T> registerReference(const std::string& name, + const T& t, + bool expert = true) + { + ReferenceStat<T> res = registerStat<ReferenceStat<T>>(name, expert); + res.set(t); + return res; } - SExpr getValue() const override { return d_data; } - -};/* class SExprStat */ + /** + * Register a new container size statistic for `name` and initialize it + * to refer to `t`. + */ + template <typename T> + SizeStat<T> registerSize(const std::string& name, + const T& t, + bool expert = true) + { + SizeStat<T> res = registerStat<SizeStat<T>>(name, expert); + res.set(t); + return res; + } -/****************************************************************************/ -/* Statistics Registry */ -/****************************************************************************/ + /** Register a new timer statistic for `name` */ + TimerStat registerTimer(const std::string& name, bool expert = true); -/** - * The main statistics registry. This registry maintains the list of - * currently active statistics and is able to "flush" them all. - */ -class CVC4_EXPORT StatisticsRegistry : public StatisticsBase -{ - private: - /** Private copy constructor undefined (no copy permitted). */ - StatisticsRegistry(const StatisticsRegistry&) = delete; + /** Register a new value statistic for `name`. */ + template <typename T> + ValueStat<T> registerValue(const std::string& name, bool expert = true) + { + return registerStat<ValueStat<T>>(name, expert); + } -public: + /** Register a new value statistic for `name` and set it to `init`. */ + template <typename T> + ValueStat<T> registerValue(const std::string& name, + const T& init, + bool expert = true) + { + ValueStat<T> res = registerStat<ValueStat<T>>(name, expert); + res.set(init); + return res; + } - /** Construct an nameless statistics registry */ - StatisticsRegistry() {} + /** begin iteration */ + auto begin() const { return d_stats.begin(); } + /** end iteration */ + auto end() const { return d_stats.end(); } - void flushStat(std::ostream& out) const; + /** + * Obtain the current state of all statistics. + */ + void storeSnapshot(); - void flushInformation(std::ostream& out) const; + /** + * Obtain a single statistic by name. Returns nullptr if no statistic has + * been registered for this name. + */ + StatisticBaseValue* get(const std::string& name) const; - void safeFlushInformation(int fd) const; + /** + * Print all statistics to the given output stream. + */ + void print(std::ostream& os) const; + /** + * Print all statistics in a safe manner to the given file descriptor. + */ + void printSafe(int fd) const; + /** + * Print all statistics as a diff to the last stored snapshot. + */ + void printDiff(std::ostream& os) const; - SExpr getValue() const + private: + /** + * Helper method to register a new statistic. + * If the name was already used, a new proxy object is created. + * We check whether the type matches the type of the originally registered + * statistic using `typeid`. + */ + template <typename Stat> + Stat registerStat(const std::string& name, bool expert) { - std::vector<SExpr> v; - for(StatSet::iterator i = d_stats.begin(); i != d_stats.end(); ++i) { - std::vector<SExpr> w; - w.push_back(SExpr((*i)->getName())); - w.push_back((*i)->getValue()); - v.push_back(SExpr(w)); + if constexpr (Configuration::isStatisticsBuild()) + { + auto it = d_stats.find(name); + if (it == d_stats.end()) + { + it = d_stats.emplace(name, std::make_unique<typename Stat::stat_type>()) + .first; + it->second->d_expert = expert; + } + auto* ptr = it->second.get(); + Assert(typeid(*ptr) == typeid(typename Stat::stat_type)) + << "Statistic value " << name + << " was registered again with a different type."; + it->second->d_expert = it->second->d_expert && expert; + return Stat(static_cast<typename Stat::stat_type*>(ptr)); } - return SExpr(v); + return Stat(nullptr); } - /** Register a new statistic */ - void registerStat(Stat* s); - - /** Unregister a new statistic */ - void unregisterStat(Stat* s); - -}; /* class StatisticsRegistry */ - -/** - * Resource-acquisition-is-initialization idiom for statistics - * registry. Useful for stack-based statistics (like in the driver). - * This RAII class only does registration and unregistration. - */ -class CVC4_EXPORT RegisterStatistic -{ - public: - RegisterStatistic(StatisticsRegistry* reg, Stat* stat); - ~RegisterStatistic(); + /** + * Holds (and owns) all statistic values, indexed by the name they were + * registered for. + */ + std::map<std::string, std::unique_ptr<StatisticBaseValue>> d_stats; -private: - StatisticsRegistry* d_reg; - Stat* d_stat; + std::unique_ptr<Snapshot> d_lastSnapshot; +}; -}; /* class RegisterStatistic */ +/** Calls `sr.print(os)`. */ +std::ostream& operator<<(std::ostream& os, const StatisticsRegistry& sr); } // namespace cvc5 |