GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/util/statistics_registry.h Lines: 2 12 16.7 %
Date: 2021-03-22 Branches: 0 2 0.0 %

Line Exec Source
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 CVC4 {
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
38930
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
22246
  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
}/* CVC4 namespace */
200
201
#endif /* CVC4__STATISTICS_REGISTRY_H */