src/util/statistics_registry.h

   1 /*********************                                                        */
   2 /*! \file statistics_registry.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Morgan Deters, Tim King, Gereon Kremer
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Statistics utility classes
  13  **
  14  ** Statistics utility classes, including classes for holding (and referring
  15  ** to) statistics, the statistics registry, and some other associated
  16  ** classes.
  17  **
  18  ** This file is somewhat unique in that it is a "cvc4_private_library.h"
  19  ** header. Because of this, most classes need to be marked as CVC4_EXPORT.
  20  ** This is because CVC4_EXPORT is connected to the visibility of the linkage
  21  ** in the object files for the class. It does not dictate what headers are
  22  ** installed.
  23  ** Because the StatisticsRegistry and associated classes are built into
  24  ** libutil, which is used by libcvc4, and then later used by the libmain
  25  ** without referring to libutil as well. Thus the without marking these as
  26  ** CVC4_EXPORT the symbols would be external in libutil, internal in libcvc4,
  27  ** and not be visible to libmain and linking would fail.
  28  ** You can debug this using "nm" on the .so and .o files in the builds/
  29  ** directory. See
  30  ** http://eli.thegreenplace.net/2013/07/09/library-order-in-static-linking
  31  ** for a longer discussion on symbol visibility.
  32  **/
  33
  34 /**
  35  * On the design of the statistics:
  36  *
  37  * Stat is the abstract base class for all statistic values.
  38  * It stores the name and provides (fully virtual) methods
  39  * flushInformation() and safeFlushInformation().
  40  *
  41  * BackedStat is an abstract templated base class for statistic values
  42  * that store the data themselves. It takes care of printing them already
  43  * and derived classes usually only need to provide methods to set the
  44  * value.
  45  *
  46  * ReferenceStat holds a reference (conceptually, it is implemented as a
  47  * const pointer) to some data that is stored outside of the statistic.
  48  *
  49  * IntStat is a BackedStat<std::int64_t>.
  50  *
  51  * SizeStat holds a const reference to some container and provides the
  52  * size of this container.
  53  *
  54  * AverageStat is a BackedStat<double>.
  55  *
  56  * HistogramStat counts instances of some type T. It is implemented as a
  57  * std::map<T, std::uint64_t>.
  58  *
  59  * IntegralHistogramStat is a (conceptual) specialization of HistogramStat
  60  * for types that are (convertible to) integral. This allows to use a
  61  * std::vector<std::uint64_t> instead of a std::map.
  62  *
  63  * TimerStat uses std::chrono to collect timing information. It is
  64  * implemented as BackedStat<std::chrono::duration> and provides methods
  65  * start() and stop(), accumulating times it was activated. It provides
  66  * the convenience class CodeTimer to allow for RAII-style usage.
  67  *
  68  *
  69  * All statistic classes should protect their custom methods using
  70  *   if (CVC4_USE_STATISTICS) { ... }
  71  * Output methods (flushInformation() and safeFlushInformation()) are only
  72  * called when statistics are enabled and need no protection.
  73  *
  74  *
  75  * The statistic classes try to implement a consistent interface:
  76  * - if we store some generic data, we implement set()
  77  * - if we (conceptually) store a set of values, we implement operator<<()
  78  * - if there are standard operations for the stored data, we implement these
  79  *   (like operator++() or operator+=())
  80  */
  81
  82 #include "cvc4_private_library.h"
  83
  84 #ifndef CVC4__STATISTICS_REGISTRY_H
  85 #define CVC4__STATISTICS_REGISTRY_H
  86
  87 #include <ctime>
  88 #include <iomanip>
  89 #include <map>
  90 #include <sstream>
  91 #include <vector>
  92
  93 #ifdef CVC4_STATISTICS_ON
  94 #  define CVC4_USE_STATISTICS true
  95 #else
  96 #  define CVC4_USE_STATISTICS false
  97 #endif
  98
  99 #include "base/exception.h"
 100 #include "cvc4_export.h"
 101 #include "util/safe_print.h"
 102 #include "util/statistics.h"
 103 #include "util/stats_base.h"
 104
 105 namespace cvc5 {
 106
 107 /** A statistic that contains a SExpr. */
 108 class SExprStat : public Stat {
 109 private:
 110   SExpr d_data;
 111
 112 public:
 113
 114   /**
 115    * Construct a SExpr-valued statistic with the given name and
 116    * initial value.
 117    */
 118   SExprStat(const std::string& name, const SExpr& init) :
 119     Stat(name), d_data(init){}
 120
 121   void flushInformation(std::ostream& out) const override
 122   {
 123     out << d_data;
 124   }
 125
 126   void safeFlushInformation(int fd) const override
 127   {
 128     // SExprStat is only used in statistics.cpp in copyFrom, which we cannot
 129     // do in a signal handler anyway.
 130     safe_print(fd, "<unsupported>");
 131   }
 132
 133   SExpr getValue() const override { return d_data; }
 134
 135 };/* class SExprStat */
 136
 137 /****************************************************************************/
 138 /* Statistics Registry                                                      */
 139 /****************************************************************************/
 140
 141 /**
 142  * The main statistics registry.  This registry maintains the list of
 143  * currently active statistics and is able to "flush" them all.
 144  */
 145 class CVC4_EXPORT StatisticsRegistry : public StatisticsBase
 146 {
 147  private:
 148   /** Private copy constructor undefined (no copy permitted). */
 149   StatisticsRegistry(const StatisticsRegistry&) = delete;
 150
 151 public:
 152
 153   /** Construct an nameless statistics registry */
 154   StatisticsRegistry() {}
 155
 156   void flushStat(std::ostream& out) const;
 157
 158   void flushInformation(std::ostream& out) const;
 159
 160   void safeFlushInformation(int fd) const;
 161
 162   SExpr getValue() const
 163   {
 164     std::vector<SExpr> v;
 165     for(StatSet::iterator i = d_stats.begin(); i != d_stats.end(); ++i) {
 166       std::vector<SExpr> w;
 167       w.push_back(SExpr((*i)->getName()));
 168       w.push_back((*i)->getValue());
 169       v.push_back(SExpr(w));
 170     }
 171     return SExpr(v);
 172   }
 173
 174   /** Register a new statistic */
 175   void registerStat(Stat* s);
 176
 177   /** Unregister a new statistic */
 178   void unregisterStat(Stat* s);
 179
 180 }; /* class StatisticsRegistry */
 181
 182 /**
 183  * Resource-acquisition-is-initialization idiom for statistics
 184  * registry.  Useful for stack-based statistics (like in the driver).
 185  * This RAII class only does registration and unregistration.
 186  */
 187 class CVC4_EXPORT RegisterStatistic
 188 {
 189  public:
 190   RegisterStatistic(StatisticsRegistry* reg, Stat* stat);
 191   ~RegisterStatistic();
 192
 193 private:
 194   StatisticsRegistry* d_reg;
 195   Stat* d_stat;
 196
 197 }; /* class RegisterStatistic */
 198
 199 }  // namespace cvc5
 200
 201 #endif /* CVC4__STATISTICS_REGISTRY_H */