GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/util/statistics_value.h Lines: 40 88 45.5 %
Date: 2021-09-07 Branches: 37 129 28.7 %

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
 * Statistic data classes.
14
 *
15
 * The statistic data classes that actually hold the data for the statistics.
16
 *
17
 * Conceptually, every statistic consists of a data object and a proxy object.
18
 * The data objects (statistic values) are derived from `StatisticBaseValue`
19
 * and live in the `StatisticsRegistry`.
20
 * They are solely exported to the proxy objects, which should be the sole
21
 * way to manipulate the data of a data object.
22
 * The data objects themselves need to implement printing (normal and safe) and
23
 * conversion to the API type `Stat`.
24
 */
25
26
#include "cvc5_private_library.h"
27
28
#ifndef CVC5__UTIL__STATISTICS_VALUE_H
29
#define CVC5__UTIL__STATISTICS_VALUE_H
30
31
#include <chrono>
32
#include <iomanip>
33
#include <map>
34
#include <optional>
35
#include <sstream>
36
#include <variant>
37
#include <vector>
38
39
#include "util/safe_print.h"
40
41
namespace cvc5 {
42
43
class StatisticsRegistry;
44
45
using StatExportData =
46
    std::variant<int64_t, double, std::string, std::map<std::string, uint64_t>>;
47
namespace detail {
48
  std::ostream& print(std::ostream& out, const StatExportData& sed);
49
}
50
51
/**
52
 * Base class for all statistic values.
53
 */
54
5082287
struct StatisticBaseValue
55
{
56
  virtual ~StatisticBaseValue();
57
  /** Checks whether the data holds the default value. */
58
  virtual bool isDefault() const = 0;
59
  /**
60
   * Converts the internal data to an instance of `StatExportData` that is
61
   * suitable for printing and exporting to the API.
62
   */
63
  virtual StatExportData getViewer() const = 0;
64
  /**
65
   * Safely writes the data to a file descriptor. Is suitable to be used
66
   * within a signal handler.
67
   */
68
  virtual void printSafe(int fd) const = 0;
69
70
  bool d_expert = true;
71
};
72
/** Writes the data to an output stream */
73
std::ostream& operator<<(std::ostream& out, const StatisticBaseValue& sbv);
74
75
/** Holds the data for an running average statistic */
76
119100
struct StatisticAverageValue : StatisticBaseValue
77
{
78
  StatExportData getViewer() const override;
79
  bool isDefault() const override;
80
  void printSafe(int fd) const override;
81
  double get() const;
82
83
  /** Sum of added values */
84
  double d_sum;
85
  /** Number of added values */
86
  uint64_t d_count;
87
};
88
89
/**
90
 * Holds some value of type `T`.
91
 *
92
 * To convert to the API representation in `getViewer`, `T` can only be one
93
 * of the types listed in `Stat::d_data` (or be implicitly converted to
94
 * one of them).
95
 */
96
template <typename T>
97
9242676
struct StatisticBackedValue : StatisticBaseValue
98
{
99
16
  StatExportData getViewer() const override { return d_value; }
100
  bool isDefault() const override { return d_value == T(); }
101
  void printSafe(int fd) const override { safe_print<T>(fd, d_value); }
102
103
  T d_value;
104
};
105
106
/**
107
 * Holds the data for a histogram. We assume the type to be (convertible to)
108
 * integral, and we can thus use a std::vector<uint64_t> for fast storage.
109
 * The core idea is to track the minimum and maximum values `[a,b]` that have
110
 * been added to the histogram and maintain a vector with `b-a+1` values.
111
 * The vector is resized on demand to grow as necessary and supports negative
112
 * values as well.
113
 * Note that the template type needs to have a streaming operator to convert it
114
 * to a string in `getViewer`.
115
 */
116
template <typename Integral>
117
1841097
struct StatisticHistogramValue : StatisticBaseValue
118
{
119
  static_assert(std::is_integral<Integral>::value
120
                    || std::is_enum<Integral>::value,
121
                "Type should be a fundamental integral type.");
122
123
  /**
124
   * Convert the internal representation to a `std::map<std::string, uint64_t>`
125
   */
126
48
  StatExportData getViewer() const override
127
  {
128
96
    std::map<std::string, uint64_t> res;
129
59
    for (size_t i = 0, n = d_hist.size(); i < n; ++i)
130
    {
131
11
      if (d_hist[i] > 0)
132
      {
133
22
        std::stringstream ss;
134
11
        ss << static_cast<Integral>(i + d_offset);
135
11
        res.emplace(ss.str(), d_hist[i]);
136
      }
137
    }
138
96
    return res;
139
  }
140
  bool isDefault() const override { return d_hist.size() == 0; }
141
  void printSafe(int fd) const override
142
  {
143
    safe_print(fd, "{ ");
144
    bool first = true;
145
    for (size_t i = 0, n = d_hist.size(); i < n; ++i)
146
    {
147
      if (d_hist[i] > 0)
148
      {
149
        if (first)
150
        {
151
          first = false;
152
        }
153
        else
154
        {
155
          safe_print(fd, ", ");
156
        }
157
        safe_print<Integral>(fd, static_cast<Integral>(i + d_offset));
158
        safe_print(fd, ": ");
159
        safe_print<uint64_t>(fd, d_hist[i]);
160
      }
161
    }
162
    safe_print(fd, " }");
163
  }
164
165
  /**
166
   * Add `val` to the histogram. Casts `val` to `int64_t`, then resizes and
167
   * moves the vector entries as necessary.
168
   */
169
101236123
  void add(Integral val)
170
  {
171
101236123
    int64_t v = static_cast<int64_t>(val);
172
101236123
    if (d_hist.empty())
173
    {
174
52620
      d_offset = v;
175
    }
176
101236123
    if (v < d_offset)
177
    {
178
42446
      d_hist.insert(d_hist.begin(), d_offset - v, 0);
179
42446
      d_offset = v;
180
    }
181
101236123
    if (static_cast<size_t>(v - d_offset) >= d_hist.size())
182
    {
183
113034
      d_hist.resize(v - d_offset + 1);
184
    }
185
101236123
    d_hist[v - d_offset]++;
186
101236123
  }
187
188
  /** Actual data */
189
  std::vector<uint64_t> d_hist;
190
  /** Offset of the entries. d_hist[i] corresponds to Interval(d_offset + i) */
191
  int64_t d_offset;
192
};
193
194
/**
195
 * Holds the data for a `ReferenceStat`.
196
 * When the `ReferenceStat` is destroyed the current value is copied into
197
 * `d_committed`. Once `d_committed` is set, this value is returned, even if
198
 * the reference is still valid.
199
 */
200
template <typename T>
201
391638
struct StatisticReferenceValue : StatisticBaseValue
202
{
203
5
  StatExportData getViewer() const override
204
  {
205
5
    if (d_committed)
206
    {
207
      if constexpr (std::is_integral_v<T>)
208
      {
209
        return static_cast<int64_t>(*d_committed);
210
      }
211
      else
212
      {
213
        // this else branch is required to ensure compilation.
214
        // if T is unsigned int, this return statement triggers a compiler error
215
        return *d_committed;
216
      }
217
    }
218
5
    else if (d_value != nullptr)
219
    {
220
      if constexpr (std::is_integral_v<T>)
221
      {
222
1
        return static_cast<int64_t>(*d_value);
223
      }
224
      else
225
      {
226
        // this else branch is required to ensure compilation.
227
        // if T is unsigned int, this return statement triggers a compiler error
228
4
        return *d_value;
229
      }
230
    }
231
    if constexpr (std::is_integral_v<T>)
232
    {
233
      return static_cast<int64_t>(0);
234
    }
235
    else
236
    {
237
      // this else branch is required to ensure compilation.
238
      // if T is unsigned int, this return statement triggers a compiler error
239
      return T();
240
    }
241
  }
242
  bool isDefault() const override
243
  {
244
    if (d_committed)
245
    {
246
      return *d_committed == T();
247
    }
248
    return d_value == nullptr || *d_value == T();
249
  }
250
  void printSafe(int fd) const override
251
  {
252
    if (d_committed)
253
    {
254
      safe_print<T>(fd, *d_committed);
255
    }
256
    else if (d_value != nullptr)
257
    {
258
      safe_print<T>(fd, *d_value);
259
    }
260
    else
261
    {
262
      safe_print<T>(fd, T());
263
    }
264
  }
265
220187
  void commit()
266
  {
267
220187
    if (d_value != nullptr)
268
    {
269
130257
      d_committed = *d_value;
270
    }
271
220187
  }
272
  const T& get() const { return d_committed ? *d_committed : *d_value; }
273
274
  const T* d_value = nullptr;
275
  std::optional<T> d_committed;
276
};
277
278
/**
279
 * Holds the data for a `SizeStat`.
280
 * When the `SizeStat` is destroyed the current size is copied into
281
 * `d_committed`. Once `d_committed` is set, this value is returned, even if
282
 * the reference is still valid.
283
 */
284
template <typename T>
285
29778
struct StatisticSizeValue : StatisticBaseValue
286
{
287
  StatExportData getViewer() const override
288
  {
289
    if (d_committed)
290
    {
291
      return static_cast<int64_t>(*d_committed);
292
    }
293
    else if (d_value != nullptr)
294
    {
295
      return static_cast<int64_t>(d_value->size());
296
    }
297
    return static_cast<int64_t>(0);
298
  }
299
  bool isDefault() const override
300
  {
301
    if (d_committed)
302
    {
303
      return *d_committed == 0;
304
    }
305
    return d_value == nullptr || d_value->size() == 0;
306
  }
307
  void printSafe(int fd) const override
308
  {
309
    if (d_committed)
310
    {
311
      safe_print(fd, *d_committed);
312
    }
313
    else if (d_value != nullptr)
314
    {
315
      safe_print(fd, d_value->size());
316
    }
317
    else
318
    {
319
      safe_print(fd, 0);
320
    }
321
  }
322
9925
  void commit()
323
  {
324
9925
    if (d_value != nullptr)
325
    {
326
9925
      d_committed = d_value->size();
327
    }
328
9925
  }
329
  size_t get() const { return d_committed ? *d_committed : d_value->size(); }
330
331
  const T* d_value = nullptr;
332
  std::optional<std::size_t> d_committed;
333
};
334
335
/**
336
 * Holds the data for a `TimerStat`.
337
 * Uses `std::chrono` to obtain the current time, store a time point and sum up
338
 * the total durations.
339
 */
340
3313716
struct StatisticTimerValue : StatisticBaseValue
341
{
342
  using clock = std::chrono::steady_clock;
343
  using time_point = clock::time_point;
344
  struct duration : public std::chrono::nanoseconds
345
  {
346
  };
347
  /** Returns the number of milliseconds */
348
  StatExportData getViewer() const override;
349
  bool isDefault() const override;
350
  /** Prints seconds in fixed-point format */
351
  void printSafe(int fd) const override;
352
  /**
353
   * Returns the elapsed time in milliseconds.
354
   * Make sure that we include the time of a currently running timer
355
   */
356
  uint64_t get() const;
357
358
  /**
359
   * The cumulative duration of the timer so far.
360
   * Does not include a currently running timer, but `get()` takes care of this.
361
   */
362
  duration d_duration;
363
  /**
364
   * The start time of a currently running timer.
365
   * May not be reset when the timer is stopped.
366
   */
367
  time_point d_start;
368
  /** Whether a timer is running right now. */
369
  bool d_running;
370
};
371
372
}  // namespace cvc5
373
374
#endif