GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/util/statistics_registry.h Lines: 31 32 96.9 %
Date: 2021-09-18 Branches: 54 189 28.6 %

Line Exec Source
1
/******************************************************************************
2
 * Top contributors (to current version):
3
 *   Gereon Kremer
4
 *
5
 * This file is part of the cvc5 project.
6
 *
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.
11
 * ****************************************************************************
12
 *
13
 * Central statistics registry.
14
 *
15
 * The StatisticsRegistry that issues statistic proxy objects.
16
 */
17
18
/**
19
 * On the design of the statistics:
20
 *
21
 * Stat is the abstract base class for all statistic values.
22
 * It stores the name and provides (fully virtual) methods
23
 * flushInformation() and safeFlushInformation().
24
 *
25
 * BackedStat is an abstract templated base class for statistic values
26
 * that store the data themselves. It takes care of printing them already
27
 * and derived classes usually only need to provide methods to set the
28
 * value.
29
 *
30
 * ReferenceStat holds a reference (conceptually, it is implemented as a
31
 * const pointer) to some data that is stored outside of the statistic.
32
 *
33
 * IntStat is a BackedStat<std::int64_t>.
34
 *
35
 * SizeStat holds a const reference to some container and provides the
36
 * size of this container.
37
 *
38
 * AverageStat is a BackedStat<double>.
39
 *
40
 * HistogramStat counts instances of some type T. It is implemented as a
41
 * std::map<T, std::uint64_t>.
42
 *
43
 * IntegralHistogramStat is a (conceptual) specialization of HistogramStat
44
 * for types that are (convertible to) integral. This allows to use a
45
 * std::vector<std::uint64_t> instead of a std::map.
46
 *
47
 * TimerStat uses std::chrono to collect timing information. It is
48
 * implemented as BackedStat<std::chrono::duration> and provides methods
49
 * start() and stop(), accumulating times it was activated. It provides
50
 * the convenience class CodeTimer to allow for RAII-style usage.
51
 *
52
 *
53
 * All statistic classes should protect their custom methods using
54
 *   if (CVC5_USE_STATISTICS) { ... }
55
 * Output methods (flushInformation() and safeFlushInformation()) are only
56
 * called when statistics are enabled and need no protection.
57
 *
58
 *
59
 * The statistic classes try to implement a consistent interface:
60
 * - if we store some generic data, we implement set()
61
 * - if we (conceptually) store a set of values, we implement operator<<()
62
 * - if there are standard operations for the stored data, we implement these
63
 *   (like operator++() or operator+=())
64
 */
65
66
#include "cvc5_private_library.h"
67
68
#ifndef CVC5__STATISTICS_REGISTRY_H
69
#define CVC5__STATISTICS_REGISTRY_H
70
71
#include <iostream>
72
#include <map>
73
#include <memory>
74
#include <typeinfo>
75
76
#include "base/check.h"
77
#include "smt/env_obj.h"
78
#include "util/statistics_stats.h"
79
#include "util/statistics_value.h"
80
81
namespace cvc5 {
82
83
struct StatisticBaseValue;
84
85
/**
86
 * The central registry for statistics.
87
 * Internally stores statistic data objects and issues corresponding proxy
88
 * objects to modules that want to expose statistics.
89
 * Provides registration methods (e.g. `registerAverage` or
90
 * `registerHistogram<T>`) that return the proxy object.
91
 * The different statistics are explained in more detail in statistics_stats.h
92
 *
93
 * Every statistic is identified by a name. If a statistic with the given
94
 * name is already registered, the registry issues another proxy object
95
 * for that name using the same data it already holds for this name.
96
 * While this makes perfect sense for most statistic types, it may lead to
97
 * unexpected (though not undefined) behaviour for others. For a reference
98
 * statistic, for example, the internal data will simply point to the object
99
 * registered last.
100
 * Note that the type of the re-registered statistic must always match
101
 * the type of the previously registered statistic with the same name.
102
 *
103
 * We generally distinguish between public (non-expert) and private (expert)
104
 * statistics. By default, `--stats` only shows public statistics. Private
105
 * ones are printed as well if `--all-statistics` is set.
106
 * All registration methods have a trailing argument `expert`, defaulting to
107
 * true.
108
 *
109
 * If statistics are disabled entirely (i.e. the cmake option
110
 * `ENABLE_STATISTICS` is not set), the registry still issues proxy objects
111
 * that can be used normally.
112
 * However, no data is stored in the registry and the modification functions
113
 * of the proxy objects do nothing.
114
 */
115
21150
class StatisticsRegistry : protected EnvObj
116
{
117
 public:
118
  friend std::ostream& operator<<(std::ostream& os,
119
                                  const StatisticsRegistry& sr);
120
121
  using Snapshot = std::map<std::string, StatExportData>;
122
123
  /**
124
   * If `registerPublic` is true, all statistics that are public are
125
   * pre-registered as such. This argument mostly exists so that unit tests
126
   * can disable this pre-registration.
127
   */
128
  StatisticsRegistry(Env& env, bool registerPublic = true);
129
130
  /** Register a new running average statistic for `name` */
131
132
  AverageStat registerAverage(const std::string& name, bool expert = true);
133
  /** Register a new histogram statistic for `name` */
134
  template <typename T>
135
1079061
  HistogramStat<T> registerHistogram(const std::string& name,
136
                                     bool expert = true)
137
  {
138
1079061
    return registerStat<HistogramStat<T>>(name, expert);
139
  }
140
141
  /** Register a new integer statistic for `name` */
142
  IntStat registerInt(const std::string& name, bool expert = true);
143
144
  /** Register a new reference statistic for `name` */
145
  template <typename T>
146
103324
  ReferenceStat<T> registerReference(const std::string& name,
147
                                     bool expert = true)
148
  {
149
103324
    return registerStat<ReferenceStat<T>>(name, expert);
150
  }
151
  /**
152
   * Register a new reference statistic for `name` and initialize it to
153
   * refer to `t`.
154
   */
155
  template <typename T>
156
29824
  ReferenceStat<T> registerReference(const std::string& name,
157
                                     const T& t,
158
                                     bool expert = true)
159
  {
160
29824
    ReferenceStat<T> res = registerStat<ReferenceStat<T>>(name, expert);
161
29824
    res.set(t);
162
29824
    return res;
163
  }
164
165
  /**
166
   * Register a new container size statistic for `name` and initialize it
167
   * to refer to `t`.
168
   */
169
  template <typename T>
170
9944
  SizeStat<T> registerSize(const std::string& name,
171
                           const T& t,
172
                           bool expert = true)
173
  {
174
9944
    SizeStat<T> res = registerStat<SizeStat<T>>(name, expert);
175
9944
    res.set(t);
176
9944
    return res;
177
  }
178
179
  /** Register a new timer statistic for `name` */
180
  TimerStat registerTimer(const std::string& name, bool expert = true);
181
182
  /** Register a new value statistic for `name`. */
183
  template <typename T>
184
13221
  ValueStat<T> registerValue(const std::string& name, bool expert = true)
185
  {
186
13221
    return registerStat<ValueStat<T>>(name, expert);
187
  }
188
189
  /** Register a new value statistic for `name` and set it to `init`. */
190
  template <typename T>
191
6230
  ValueStat<T> registerValue(const std::string& name,
192
                             const T& init,
193
                             bool expert = true)
194
  {
195
6230
    ValueStat<T> res = registerStat<ValueStat<T>>(name, expert);
196
6230
    res.set(init);
197
6230
    return res;
198
  }
199
200
  /** begin iteration */
201
1
  auto begin() const { return d_stats.begin(); }
202
  /** end iteration */
203
1
  auto end() const { return d_stats.end(); }
204
205
  /**
206
   * Obtain the current state of all statistics.
207
   */
208
  void storeSnapshot();
209
210
  /**
211
   * Obtain a single statistic by name. Returns nullptr if no statistic has
212
   * been registered for this name.
213
   */
214
  StatisticBaseValue* get(const std::string& name) const;
215
216
  /**
217
   * Print all statistics to the given output stream.
218
   */
219
  void print(std::ostream& os) const;
220
  /**
221
   * Print all statistics in a safe manner to the given file descriptor.
222
   */
223
  void printSafe(int fd) const;
224
  /**
225
   * Print all statistics as a diff to the last stored snapshot.
226
   */
227
  void printDiff(std::ostream& os) const;
228
229
 private:
230
  /**
231
   * Helper method to register a new statistic.
232
   * If the name was already used, a new proxy object is created.
233
   * We check whether the type matches the type of the originally registered
234
   * statistic using `typeid`.
235
   */
236
  template <typename Stat>
237
5497431
  Stat registerStat(const std::string& name, bool expert)
238
  {
239
    if constexpr (Configuration::isStatisticsBuild())
240
    {
241
5497431
      auto it = d_stats.find(name);
242
5497431
      if (it == d_stats.end())
243
      {
244
5089970
        it = d_stats.emplace(name, std::make_unique<typename Stat::stat_type>())
245
10179940
                 .first;
246
5089970
        it->second->d_expert = expert;
247
      }
248
5497431
      auto* ptr = it->second.get();
249
5497431
      Assert(typeid(*ptr) == typeid(typename Stat::stat_type))
250
          << "Statistic value " << name
251
          << " was registered again with a different type.";
252
5497431
      it->second->d_expert = it->second->d_expert && expert;
253
5497431
      return Stat(static_cast<typename Stat::stat_type*>(ptr));
254
    }
255
    return Stat(nullptr);
256
  }
257
258
  /**
259
   * Holds (and owns) all statistic values, indexed by the name they were
260
   * registered for.
261
   */
262
  std::map<std::string, std::unique_ptr<StatisticBaseValue>> d_stats;
263
264
  std::unique_ptr<Snapshot> d_lastSnapshot;
265
};
266
267
/** Calls `sr.print(os)`. */
268
std::ostream& operator<<(std::ostream& os, const StatisticsRegistry& sr);
269
270
}  // namespace cvc5
271
272
#endif /* CVC5__STATISTICS_REGISTRY_H */