GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/base/output.h Lines: 104 128 81.3 %
Date: 2021-03-22 Branches: 141 884 16.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file output.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Morgan Deters, Andres Noetzli, Dejan Jovanovic
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 Output utility classes and functions
13
 **
14
 ** Output utility classes and functions.
15
 **/
16
17
#include "cvc4_private_library.h"
18
19
#ifndef CVC4__OUTPUT_H
20
#define CVC4__OUTPUT_H
21
22
#include <cstdio>
23
#include <ios>
24
#include <iostream>
25
#include <set>
26
#include <string>
27
#include <utility>
28
29
#include "cvc4_export.h"
30
31
namespace CVC4 {
32
33
template <class T, class U>
34
std::ostream& operator<<(std::ostream& out,
35
                         const std::pair<T, U>& p) CVC4_EXPORT;
36
37
template <class T, class U>
38
std::ostream& operator<<(std::ostream& out, const std::pair<T, U>& p) {
39
  return out << "[" << p.first << "," << p.second << "]";
40
}
41
42
/**
43
 * A utility class to provide (essentially) a "/dev/null" streambuf.
44
 * If debugging support is compiled in, but debugging for
45
 * e.g. "parser" is off, then Debug("parser") returns a stream
46
 * attached to a null_streambuf instance so that output is directed to
47
 * the bit bucket.
48
 */
49
17784
class null_streambuf : public std::streambuf
50
{
51
 public:
52
  /* Overriding overflow() just ensures that EOF isn't returned on the
53
   * stream.  Perhaps this is not so critical, but recommended; this
54
   * way the output stream looks like it's functioning, in a non-error
55
   * state. */
56
10770849
 int overflow(int c) override { return c; }
57
}; /* class null_streambuf */
58
59
/** A null stream-buffer singleton */
60
extern null_streambuf null_sb;
61
/** A null output stream singleton */
62
extern std::ostream null_os CVC4_EXPORT;
63
64
class CVC4_EXPORT CVC4ostream
65
{
66
  static const std::string s_tab;
67
  static const int s_indentIosIndex;
68
69
  /** The underlying ostream */
70
  std::ostream* d_os;
71
  /** Are we in the first column? */
72
  bool d_firstColumn;
73
74
  /** The endl manipulator (why do we need to keep this?) */
75
  std::ostream& (*const d_endl)(std::ostream&);
76
77
  // do not allow use
78
  CVC4ostream& operator=(const CVC4ostream&);
79
80
public:
81
8854888133
  CVC4ostream() :
82
    d_os(NULL),
83
    d_firstColumn(false),
84
8854888133
    d_endl(&std::endl) {
85
8854888133
  }
86
229
  explicit CVC4ostream(std::ostream* os) :
87
    d_os(os),
88
    d_firstColumn(true),
89
229
    d_endl(&std::endl) {
90
229
  }
91
92
17231679
  void pushIndent() {
93
17231679
    if(d_os != NULL) {
94
      ++d_os->iword(s_indentIosIndex);
95
    }
96
17231679
  }
97
16555523
  void popIndent() {
98
16555523
    if(d_os != NULL) {
99
      long& indent = d_os->iword(s_indentIosIndex);
100
      if(indent > 0) {
101
        --indent;
102
      }
103
    }
104
16555523
  }
105
106
  CVC4ostream& flush() {
107
    if(d_os != NULL) {
108
      d_os->flush();
109
    }
110
    return *this;
111
  }
112
113
41002
  bool isConnected() const { return d_os != NULL; }
114
41002
  operator std::ostream&() const { return isConnected() ? *d_os : null_os; }
115
116
  std::ostream* getStreamPointer() const { return d_os; }
117
118
  template <class T>
119
  CVC4ostream& operator<<(T const& t) CVC4_EXPORT;
120
121
  // support manipulators, endl, etc..
122
7079093148
  CVC4ostream& operator<<(std::ostream& (*pf)(std::ostream&)) {
123
7079093148
    if(d_os != NULL) {
124
217
      d_os = &(*d_os << pf);
125
126
217
      if(pf == d_endl) {
127
217
        d_firstColumn = true;
128
      }
129
    }
130
7079093148
    return *this;
131
  }
132
  CVC4ostream& operator<<(std::ios& (*pf)(std::ios&)) {
133
    if(d_os != NULL) {
134
      d_os = &(*d_os << pf);
135
    }
136
    return *this;
137
  }
138
  CVC4ostream& operator<<(std::ios_base& (*pf)(std::ios_base&)) {
139
    if(d_os != NULL) {
140
      d_os = &(*d_os << pf);
141
    }
142
    return *this;
143
  }
144
33787202
  CVC4ostream& operator<<(CVC4ostream& (*pf)(CVC4ostream&)) {
145
33787202
    return pf(*this);
146
  }
147
}; /* class CVC4ostream */
148
149
17231679
inline CVC4ostream& push(CVC4ostream& stream) {
150
17231679
  stream.pushIndent();
151
17231679
  return stream;
152
}
153
154
16555523
inline CVC4ostream& pop(CVC4ostream& stream) {
155
16555523
  stream.popIndent();
156
16555523
  return stream;
157
}
158
159
template <class T>
160
45330359439
CVC4ostream& CVC4ostream::operator<<(T const& t) {
161
45330359439
  if(d_os != NULL) {
162
925
    if(d_firstColumn) {
163
249
      d_firstColumn = false;
164
249
      long indent = d_os->iword(s_indentIosIndex);
165
249
      for(long i = 0; i < indent; ++i) {
166
        d_os = &(*d_os << s_tab);
167
      }
168
    }
169
925
    d_os = &(*d_os << t);
170
  }
171
45330359439
  return *this;
172
}
173
174
/**
175
 * Does nothing; designed for compilation of non-debug/non-trace
176
 * builds.  None of these should ever be called in such builds, but we
177
 * offer this to the compiler so it doesn't complain.
178
 */
179
class NullC
180
{
181
 public:
182
19594
  operator bool() const { return false; }
183
390224
  operator CVC4ostream() const { return CVC4ostream(); }
184
76
  operator std::ostream&() const { return null_os; }
185
}; /* class NullC */
186
187
extern NullC nullCvc4Stream CVC4_EXPORT;
188
189
/** The debug output class */
190
8892
class DebugC
191
{
192
  std::set<std::string> d_tags;
193
  std::ostream* d_os;
194
195
public:
196
8892
  explicit DebugC(std::ostream* os) : d_os(os) {}
197
198
7480536499
  CVC4ostream operator()(const std::string& tag) const
199
  {
200
7480536499
    if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) {
201
62
      return CVC4ostream(d_os);
202
    } else {
203
7480536437
      return CVC4ostream();
204
    }
205
  }
206
207
48
  bool on(const std::string& tag)
208
  {
209
48
    d_tags.insert(tag);
210
48
    return true;
211
  }
212
6
  bool off(const std::string& tag)
213
  {
214
6
    d_tags.erase(tag);
215
6
    return false;
216
  }
217
  bool off()                { d_tags.clear(); return false; }
218
219
307913228
  bool isOn(const std::string& tag) const
220
  {
221
307913228
    return d_tags.find(tag) != d_tags.end();
222
  }
223
224
6
  std::ostream& setStream(std::ostream* os) { d_os = os; return *os; }
225
33
  std::ostream& getStream() const { return *d_os; }
226
9599
  std::ostream* getStreamPointer() const { return d_os; }
227
}; /* class DebugC */
228
229
/** The warning output class */
230
8892
class WarningC
231
{
232
  std::set<std::pair<std::string, size_t> > d_alreadyWarned;
233
  std::ostream* d_os;
234
235
public:
236
8892
  explicit WarningC(std::ostream* os) : d_os(os) {}
237
238
112
  CVC4ostream operator()() const { return CVC4ostream(d_os); }
239
240
187
  std::ostream& setStream(std::ostream* os) { d_os = os; return *d_os; }
241
28
  std::ostream& getStream() const { return *d_os; }
242
9399
  std::ostream* getStreamPointer() const { return d_os; }
243
244
10071
  bool isOn() const { return d_os != &null_os; }
245
246
  // This function supports the WarningOnce() macro, which allows you
247
  // to easily indicate that a warning should be emitted, but only
248
  // once for a given run of CVC4.
249
  bool warnOnce(const std::string& file, size_t line)
250
  {
251
    std::pair<std::string, size_t> pr = std::make_pair(file, line);
252
    if(d_alreadyWarned.find(pr) != d_alreadyWarned.end()) {
253
      // signal caller not to warn again
254
      return false;
255
    }
256
257
    // okay warn this time, but don't do it again
258
    d_alreadyWarned.insert(pr);
259
    return true;
260
  }
261
262
}; /* class WarningC */
263
264
/** The message output class */
265
class MessageC
266
{
267
  std::ostream* d_os;
268
269
public:
270
8892
  explicit MessageC(std::ostream* os) : d_os(os) {}
271
272
4
  CVC4ostream operator()() const { return CVC4ostream(d_os); }
273
274
187
  std::ostream& setStream(std::ostream* os) { d_os = os; return *d_os; }
275
28
  std::ostream& getStream() const { return *d_os; }
276
9399
  std::ostream* getStreamPointer() const { return d_os; }
277
278
9638
  bool isOn() const { return d_os != &null_os; }
279
}; /* class MessageC */
280
281
/** The notice output class */
282
class NoticeC
283
{
284
  std::ostream* d_os;
285
286
public:
287
8892
  explicit NoticeC(std::ostream* os) : d_os(os) {}
288
289
11
  CVC4ostream operator()() const { return CVC4ostream(d_os); }
290
291
187
  std::ostream& setStream(std::ostream* os) { d_os = os; return *d_os; }
292
  std::ostream& getStream() const { return *d_os; }
293
2
  std::ostream* getStreamPointer() const { return d_os; }
294
295
133400
  bool isOn() const { return d_os != &null_os; }
296
}; /* class NoticeC */
297
298
/** The chat output class */
299
class ChatC
300
{
301
  std::ostream* d_os;
302
303
public:
304
8892
  explicit ChatC(std::ostream* os) : d_os(os) {}
305
306
34
  CVC4ostream operator()() const { return CVC4ostream(d_os); }
307
308
187
  std::ostream& setStream(std::ostream* os) { d_os = os; return *d_os; }
309
  std::ostream& getStream() const { return *d_os; }
310
2
  std::ostream* getStreamPointer() const { return d_os; }
311
312
275766
  bool isOn() const { return d_os != &null_os; }
313
}; /* class ChatC */
314
315
/** The trace output class */
316
8892
class TraceC
317
{
318
  std::ostream* d_os;
319
  std::set<std::string> d_tags;
320
321
public:
322
8892
  explicit TraceC(std::ostream* os) : d_os(os) {}
323
324
1373961478
  CVC4ostream operator()(std::string tag) const
325
  {
326
1373961478
    if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) {
327
6
      return CVC4ostream(d_os);
328
    } else {
329
1373961472
      return CVC4ostream();
330
    }
331
  }
332
333
8
  bool on(const std::string& tag)
334
  {
335
8
    d_tags.insert(tag);
336
8
    return true;
337
  }
338
6
  bool off(const std::string& tag)
339
  {
340
6
    d_tags.erase(tag);
341
6
    return false;
342
  }
343
  bool off()                { d_tags.clear(); return false; }
344
345
146698902
  bool isOn(const std::string& tag) const
346
  {
347
146698902
    return d_tags.find(tag) != d_tags.end();
348
  }
349
350
6
  std::ostream& setStream(std::ostream* os) { d_os = os; return *d_os; }
351
33
  std::ostream& getStream() const { return *d_os; }
352
9599
  std::ostream* getStreamPointer() const { return d_os; }
353
354
}; /* class TraceC */
355
356
/** The dump output class */
357
8892
class DumpOutC
358
{
359
  std::set<std::string> d_tags;
360
  std::ostream* d_os;
361
362
public:
363
  /**
364
   * A copy of cout for use by the dumper.  This is important because
365
   * it has different settings (e.g., the expr printing depth is always
366
   * unlimited). */
367
  static std::ostream dump_cout;
368
369
8892
  explicit DumpOutC(std::ostream* os) : d_os(os) {}
370
371
  CVC4ostream operator()(std::string tag) {
372
    if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) {
373
      return CVC4ostream(d_os);
374
    } else {
375
      return CVC4ostream();
376
    }
377
  }
378
379
  bool on(const std::string& tag)
380
  {
381
    d_tags.insert(tag);
382
    return true;
383
  }
384
  bool off(const std::string& tag)
385
  {
386
    d_tags.erase(tag);
387
    return false;
388
  }
389
  bool off()                { d_tags.clear(); return false; }
390
391
  bool isOn(std::string tag) const { return d_tags.find(tag) != d_tags.end(); }
392
393
  std::ostream& setStream(std::ostream* os) { d_os = os; return *d_os; }
394
2711
  std::ostream& getStream() const { return *d_os; }
395
9599
  std::ostream* getStreamPointer() const { return d_os; }
396
}; /* class DumpOutC */
397
398
/** The debug output singleton */
399
extern DebugC DebugChannel CVC4_EXPORT;
400
/** The warning output singleton */
401
extern WarningC WarningChannel CVC4_EXPORT;
402
/** The message output singleton */
403
extern MessageC MessageChannel CVC4_EXPORT;
404
/** The notice output singleton */
405
extern NoticeC NoticeChannel CVC4_EXPORT;
406
/** The chat output singleton */
407
extern ChatC ChatChannel CVC4_EXPORT;
408
/** The trace output singleton */
409
extern TraceC TraceChannel CVC4_EXPORT;
410
/** The dump output singleton */
411
extern DumpOutC DumpOutChannel CVC4_EXPORT;
412
413
#ifdef CVC4_MUZZLE
414
415
#  define Debug ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::DebugChannel
416
#  define Warning ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::WarningChannel
417
#  define WarningOnce ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::WarningChannel
418
#define CVC4Message \
419
  ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::MessageChannel
420
#  define Notice ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::NoticeChannel
421
#  define Chat ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::ChatChannel
422
#  define Trace ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::TraceChannel
423
#  define DumpOut ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::DumpOutChannel
424
425
#else /* CVC4_MUZZLE */
426
427
#  if defined(CVC4_DEBUG) && defined(CVC4_TRACING)
428
#    define Debug ::CVC4::DebugChannel
429
#  else /* CVC4_DEBUG && CVC4_TRACING */
430
#    define Debug ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::DebugChannel
431
#  endif /* CVC4_DEBUG && CVC4_TRACING */
432
#  define Warning (! ::CVC4::WarningChannel.isOn()) ? ::CVC4::nullCvc4Stream : ::CVC4::WarningChannel
433
#  define WarningOnce (! ::CVC4::WarningChannel.isOn() || ! ::CVC4::WarningChannel.warnOnce(__FILE__,__LINE__)) ? ::CVC4::nullCvc4Stream : ::CVC4::WarningChannel
434
#define CVC4Message                                         \
435
  (!::CVC4::MessageChannel.isOn()) ? ::CVC4::nullCvc4Stream \
436
                                   : ::CVC4::MessageChannel
437
#  define Notice (! ::CVC4::NoticeChannel.isOn()) ? ::CVC4::nullCvc4Stream : ::CVC4::NoticeChannel
438
#  define Chat (! ::CVC4::ChatChannel.isOn()) ? ::CVC4::nullCvc4Stream : ::CVC4::ChatChannel
439
#  ifdef CVC4_TRACING
440
#    define Trace ::CVC4::TraceChannel
441
#  else /* CVC4_TRACING */
442
#    define Trace ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::TraceChannel
443
#  endif /* CVC4_TRACING */
444
#  ifdef CVC4_DUMPING
445
#    define DumpOut ::CVC4::DumpOutChannel
446
#  else /* CVC4_DUMPING */
447
#    define DumpOut ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::DumpOutChannel
448
#  endif /* CVC4_DUMPING */
449
450
#endif /* CVC4_MUZZLE */
451
452
// Disallow e.g. !Debug("foo").isOn() forms
453
// because the ! will apply before the ? .
454
// If a compiler error has directed you here,
455
// just parenthesize it e.g. !(Debug("foo").isOn())
456
class __cvc4_true {
457
  void operator!() CVC4_UNUSED;
458
  void operator~() CVC4_UNUSED;
459
  void operator-() CVC4_UNUSED;
460
  void operator+() CVC4_UNUSED;
461
public:
462
  inline operator bool() { return true; }
463
};/* __cvc4_true */
464
465
#if defined(CVC4_DEBUG) && defined(CVC4_TRACING)
466
467
class ScopedDebug
468
{
469
  std::string d_tag;
470
  bool d_oldSetting;
471
472
public:
473
474
  ScopedDebug(std::string tag, bool newSetting = true) :
475
    d_tag(tag) {
476
    d_oldSetting = Debug.isOn(d_tag);
477
    if(newSetting) {
478
      Debug.on(d_tag);
479
    } else {
480
      Debug.off(d_tag);
481
    }
482
  }
483
484
  ~ScopedDebug() {
485
    if(d_oldSetting) {
486
      Debug.on(d_tag);
487
    } else {
488
      Debug.off(d_tag);
489
    }
490
  }
491
}; /* class ScopedDebug */
492
493
#else /* CVC4_DEBUG && CVC4_TRACING */
494
495
class ScopedDebug
496
{
497
 public:
498
  ScopedDebug(std::string tag, bool newSetting = true) {}
499
}; /* class ScopedDebug */
500
501
#endif /* CVC4_DEBUG && CVC4_TRACING */
502
503
#ifdef CVC4_TRACING
504
505
class ScopedTrace
506
{
507
  std::string d_tag;
508
  bool d_oldSetting;
509
510
public:
511
512
  ScopedTrace(std::string tag, bool newSetting = true) :
513
    d_tag(tag) {
514
    d_oldSetting = Trace.isOn(d_tag);
515
    if(newSetting) {
516
      Trace.on(d_tag);
517
    } else {
518
      Trace.off(d_tag);
519
    }
520
  }
521
522
  ~ScopedTrace() {
523
    if(d_oldSetting) {
524
      Trace.on(d_tag);
525
    } else {
526
      Trace.off(d_tag);
527
    }
528
  }
529
}; /* class ScopedTrace */
530
531
#else /* CVC4_TRACING */
532
533
class ScopedTrace
534
{
535
 public:
536
  ScopedTrace(std::string tag, bool newSetting = true) {}
537
}; /* class ScopedTrace */
538
539
#endif /* CVC4_TRACING */
540
541
/**
542
 * Pushes an indentation level on construction, pop on destruction.
543
 * Useful for tracing recursive functions especially, but also can be
544
 * used for clearly separating different phases of an algorithm,
545
 * or iterations of a loop, or... etc.
546
 */
547
class IndentedScope
548
{
549
  CVC4ostream d_out;
550
public:
551
  inline IndentedScope(CVC4ostream out);
552
  inline ~IndentedScope();
553
}; /* class IndentedScope */
554
555
#if defined(CVC4_DEBUG) && defined(CVC4_TRACING)
556
44970
inline IndentedScope::IndentedScope(CVC4ostream out) : d_out(out) { d_out << push; }
557
44970
inline IndentedScope::~IndentedScope() { d_out << pop; }
558
#else /* CVC4_DEBUG && CVC4_TRACING */
559
inline IndentedScope::IndentedScope(CVC4ostream out) {}
560
inline IndentedScope::~IndentedScope() {}
561
#endif /* CVC4_DEBUG && CVC4_TRACING */
562
563
}/* CVC4 namespace */
564
565
#endif /* CVC4__OUTPUT_H */