CVC3  2.4.1
debug.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file debug.h
4  * \brief Description: Collection of debugging macros and functions.
5  *
6  * Author: Sergey Berezin
7  *
8  * Created: Thu Dec 5 13:12:59 2002
9  *
10  * <hr>
11  *
12  * License to use, copy, modify, sell and/or distribute this software
13  * and its documentation for any purpose is hereby granted without
14  * royalty, subject to the terms and conditions defined in the \ref
15  * LICENSE file provided with this distribution.
16  *
17  * <hr>
18  *
19  */
20 /*****************************************************************************/
21 
22 #ifndef _cvc3__debug_h
23 #define _cvc3__debug_h
24 
25 #include <string>
26 #include <iostream>
27 #include <sstream>
28 #include <vector>
29 #include "os.h"
30 #include "exception.h"
31 
32 /*! @brief If something goes horribly wrong, print a message and abort
33  immediately with exit(1). */
34 /*! This macro stays even in the non-debug build, so the end users can
35  send us meaningful bug reports. */
36 
37 #define FatalAssert(cond, msg) if(!(cond)) \
38  CVC3::fatalError(__FILE__, __LINE__, #cond, msg)
39 
40 namespace CVC3 {
41  //! Function for fatal exit.
42  /*! It just exits with code 1, but is provided here for the debugger
43  to set a breakpoint to. For this reason, it is not inlined. */
44  extern CVC_DLL void fatalError(const std::string& file, int line,
45  const std::string& cond, const std::string& msg);
46 }
47 
48 #ifdef _CVC3_DEBUG_MODE
49 
50 #include "compat_hash_map.h"
51 #include "compat_hash_set.h"
52 
53 //! Any debugging code must be within IF_DEBUG(...)
54 #define IF_DEBUG(code) code
55 
56 //! Print a value conditionally.
57 /*! If 'cond' is true, print 'pre', then 'v', then 'post'. The type
58  of v must have overloaded operator<<. It expects a ';' after it. */
59 #define DBG_PRINT(cond, pre, v, post) if(cond) CVC3::debugger.getOS() \
60  << (pre) << (v) << (post) << std::endl
61 
62 //! Print a message conditionally
63 #define DBG_PRINT_MSG(cond, msg) \
64  if(cond) CVC3::debugger.getOS() << (msg) << std::endl
65 
66 /*! @brief Same as DBG_PRINT, only takes a flag name instead of a
67  general condition */
68 #define TRACE(flag, pre, v, post) \
69  DBG_PRINT(CVC3::debugger.trace(flag), pre, v, post)
70 
71 //! Same as TRACE, but for a simple message
72 #define TRACE_MSG(flag, msg) \
73  DBG_PRINT_MSG(CVC3::debugger.trace(flag), msg)
74 
75 //! Sanity check for debug build. It disappears in the production code.
76 #define DebugAssert(cond, str) if(!(cond)) \
77  CVC3::debugError(__FILE__, __LINE__, #cond, str)
78 
79 
80 namespace CVC3 {
81 
82  class Expr;
83  //! Our exception to throw
84  class DebugException: public Exception {
85  public:
86  // Constructor
87  DebugException(const std::string& msg): Exception(msg) { }
88  // Printing
89  virtual std::string toString() const {
90  return "Assertion violation " + d_msg;
91  }
92  }; // end of class DebugException
93 
94  //! Similar to fatalError to raise an exception when DebugAssert fires.
95  /*! This does not necessarily cause the program to quit. */
96  extern CVC_DLL void debugError(const std::string& file, int line,
97  const std::string& cond, const std::string& msg);
98 
99  // First, wrapper classes for flags, counters, and timers. Later,
100  // we overload some operators like '=', '++', etc. for those
101  // classes.
102  //! Boolean flag (can only be true or false)
103  class DebugFlag {
104  private:
105  bool* d_flag; // We don't own the pointer
106  public:
107  // Constructor: takes the pointer to the actual flag, normally
108  // stored in class Debug below.
109  DebugFlag(bool& flag) : d_flag(&flag) { }
110  // Destructor
111  ~DebugFlag() { }
112  // Auto-cast to boolean
113  operator bool() { return *d_flag; }
114 
115  // Setting and resetting by ++ and --
116  // Prefix versions:
117  bool operator--() { *d_flag = false; return false; }
118  bool operator++() { *d_flag = true; return true; }
119  // Postfix versions:
120  bool operator--(int) { bool x=*d_flag; *d_flag=false; return x; }
121  bool operator++(int) { bool x=*d_flag; *d_flag=true; return x; }
122  // Can be assigned only a boolean value
123  DebugFlag& operator=(bool x) { *d_flag=(x!=false); return *this; }
124  // Comparisons
125  friend bool operator==(const DebugFlag& f1, const DebugFlag& f2);
126  friend bool operator!=(const DebugFlag& f1, const DebugFlag& f2);
127  // Printing
128  friend std::ostream& operator<<(std::ostream& os, const DebugFlag& f);
129  }; // end of class DebugFlag
130 
131  //! Checks if the *values* of the flags are equal
132  inline bool operator==(const DebugFlag& f1, const DebugFlag& f2) {
133  return (*f1.d_flag) == (*f2.d_flag);
134  }
135  //! Checks if the *values* of the flags are disequal
136  inline bool operator!=(const DebugFlag& f1, const DebugFlag& f2) {
137  return (*f1.d_flag) != (*f2.d_flag);
138  }
139  //! Printing flags
140  inline std::ostream& operator<<(std::ostream& os, const DebugFlag& f) {
141  if(*f.d_flag) return(os << "true");
142  else return(os << "false");
143  }
144 
145  //! Integer counter for debugging purposes.
146  /*! Intended use is to count events (e.g. number of function calls),
147  but can be used to store any integer value (e.g. size of some data
148  structure) */
149  class DebugCounter {
150  private:
151  int* d_counter; //!< We don't own the pointer
152  public:
153  //! Constructor
154  /*! Takes the pointer to the actual counter, normally stored in
155  class Debug below. */
156  DebugCounter(int& c) : d_counter(&c) { }
157  //! Destructor
158  ~DebugCounter() { }
159  //! Auto-cast to int.
160  /*! In particular, arithmetic comparisons like <, >, <=, >= will
161  work because of this. */
162  operator int() { return *d_counter; }
163 
164  // Auto-increment operators
165 
166  //! Prefix auto-decrement
167  int operator--() { return --(*d_counter); }
168  //! Prefix auto-increment
169  int operator++() { return ++(*d_counter); }
170  //! Postfix auto-decrement
171  int operator--(int) { return (*d_counter)--; }
172  //! Postfix auto-increment
173  int operator++(int) { return (*d_counter)++; }
174  //! Value assignment.
175  DebugCounter& operator=(int x) { *d_counter=x; return *this; }
176  DebugCounter& operator+=(int x) { *d_counter+=x; return *this; }
177  DebugCounter& operator-=(int x) { *d_counter-=x; return *this; }
178  //! Assignment from another counter.
179  /*! It copies the value, not the pointer */
180  DebugCounter& operator=(const DebugCounter& x)
181  { *d_counter=*x.d_counter; return *this; }
182  /*! It copies the value, not the pointer */
183  DebugCounter& operator-=(const DebugCounter& x)
184  { *d_counter-=*x.d_counter; return *this; }
185  /*! It copies the value, not the pointer */
186  DebugCounter& operator+=(const DebugCounter& x)
187  { *d_counter+=*x.d_counter; return *this; }
188  // Comparisons to integers and other DebugCounters
189  friend bool operator==(const DebugCounter& c1, const DebugCounter& c2);
190  friend bool operator!=(const DebugCounter& c1, const DebugCounter& c2);
191  friend bool operator==(int c1, const DebugCounter& c2);
192  friend bool operator!=(int c1, const DebugCounter& c2);
193  friend bool operator==(const DebugCounter& c1, int c2);
194  friend bool operator!=(const DebugCounter& c1, int c2);
195  //! Printing counters
196  friend std::ostream& operator<<(std::ostream& os, const DebugCounter& f);
197  }; // end of class DebugCounter
198 
199  inline bool operator==(const DebugCounter& c1, const DebugCounter& c2) {
200  return (*c1.d_counter) == (*c2.d_counter);
201  }
202  inline bool operator!=(const DebugCounter& c1, const DebugCounter& c2) {
203  return (*c1.d_counter) != (*c2.d_counter);
204  }
205  inline bool operator==(int c1, const DebugCounter& c2) {
206  return c1 == (*c2.d_counter);
207  }
208  inline bool operator!=(int c1, const DebugCounter& c2) {
209  return c1 != (*c2.d_counter);
210  }
211  inline bool operator==(const DebugCounter& c1, int c2) {
212  return (*c1.d_counter) == c2;
213  }
214  inline bool operator!=(const DebugCounter& c1, int c2) {
215  return (*c1.d_counter) != c2;
216  }
217  inline std::ostream& operator<<(std::ostream& os, const DebugCounter& c) {
218  return (os << *c.d_counter);
219  }
220 
221  //! A class holding the time value.
222  /*! What exactly is time is not exposed. It can be the system's
223  struct timeval, or it can be the (subset of the) user/system/real
224  time tuple. */
225  class DebugTime;
226 
227  //! Time counter.
228  /*! Intended use is to store time intervals or accumulated time for
229  multiple events (e.g. time spent to execute certain lines of code,
230  or accumulated time spent in a particular function). */
231  class CVC_DLL DebugTimer {
232  private:
233  DebugTime* d_time; //!< The time value
234  bool d_clean_time; //!< Set if we own *d_time
235  public:
236  //! Constructor: takes the pointer to the actual time value.
237  /*! It is either stored in class Debug below (then the timer is
238  "public"), or we own it, making the timer "private". */
239  DebugTimer(DebugTime* time, bool take_time = false)
240  : d_time(time), d_clean_time(take_time) { }
241  /*! @brief Copy constructor: copy the *pointer* from public
242  timers, and *value* from private. */
243  /*! The reason for different behavior for public and private time
244  is the following. When you modify a public timer, you want the
245  changes to show in the central database and everywhere else,
246  whereas private timers are used as independent temporary
247  variables holding intermediate time values. */
248  DebugTimer(const DebugTimer& timer);
249  //! Assignment: same logistics as for the copy constructor
250  DebugTimer& operator=(const DebugTimer& timer);
251 
252  //! Destructor
253  ~DebugTimer();
254 
255  // Operators
256  //! Set time to zero
257  void reset();
258  DebugTimer& operator+=(const DebugTimer& timer);
259  DebugTimer& operator-=(const DebugTimer& timer);
260  //! Produces new "private" timer
261  DebugTimer operator+(const DebugTimer& timer);
262  //! Produces new "private" timer
263  DebugTimer operator-(const DebugTimer& timer);
264 
265  // Our friends
266  friend class Debug;
267  // Comparisons
268  friend bool operator==(const DebugTimer& t1, const DebugTimer& t2);
269  friend bool operator!=(const DebugTimer& t1, const DebugTimer& t2);
270  friend bool operator<(const DebugTimer& t1, const DebugTimer& t2);
271  friend bool operator>(const DebugTimer& t1, const DebugTimer& t2);
272  friend bool operator<=(const DebugTimer& t1, const DebugTimer& t2);
273  friend bool operator>=(const DebugTimer& t1, const DebugTimer& t2);
274 
275  //! Print the timer's value
276  friend std::ostream& operator<<(std::ostream& os, const DebugTimer& timer);
277  }; // end of class DebugTimer
278 
279  //! The heart of the Bug Extermination Kingdom.
280  /*! This class exposes many important components of the entire
281  CVC-lite system for use in debugging, keeps all the flags,
282  counters, and timers in the central database, and provides timing
283  and printing functions. */
284 
285  class CVC_DLL Debug {
286  private:
287  //! Command line options for tracing; these override the TRACE command
288  const std::vector<std::pair<std::string,bool> >* d_traceOptions;
289  //! name of dump file
290  const std::string* d_dumpName;
291  // Output control
292  std::ostream* d_os;
293  // Stream for dumping trace to file ("dump-trace" option)
294  std::ostream* d_osDumpTrace;
295  //! Private hasher class for strings
296  class stringHash {
297  public:
298  size_t operator()(const std::string& s) const {
300  return h(s.c_str());
301  }
302  }; // end of stringHash
303  // Hash tables for storing flags, counters, and timers
307  FlagMap d_flags; //!< Set of flags
308  FlagMap d_traceFlags; //!< Set of trace flags
309  CounterMap d_counters; //!< Set of counters
310  /*! Note, that the d_timers map does *not* own the pointers; so
311  the objects in d_timers must be destroyed explicitly in our
312  destructor. */
313  TimerMap d_timers; //!< Set of timers
314 
315  public:
316  //! Constructor
317  Debug(): d_traceOptions(NULL), d_os(&std::cerr), d_osDumpTrace(NULL) { }
318  //! Destructor (must destroy objects it d_timers)
319  ~Debug();
320  //! Must be called before Debug class can be safely used
321  void init(const std::vector<std::pair<std::string,bool> >* traceOptions,
322  const std::string* dumpName);
323  //! Must be called before arguments supplied to init are deallocated
324  void finalize();
325  //! Accessing flags by name.
326  /*! If a flag doesn't exist, it is created and initialized to
327  false. */
328  DebugFlag flag(const std::string& name)
329  { return DebugFlag(d_flags[name]); }
330  //! Accessing tracing flags by name.
331  /*! If a flag doesn't exist, it is created and initialized to
332  false. */
333  DebugFlag traceFlag(const std::string& name)
334  { return DebugFlag(d_traceFlags[name]); }
335  //! Accessing tracing flag by char* name (mostly for GDB)
336  DebugFlag traceFlag(const char* name);
337  //! Set tracing of everything on (1) and off (0) [for use in GDB]
338  void traceAll(bool enable = true);
339  //! Accessing counters by name.
340  /*! If a counter doesn't exist, it is created and initialized to 0. */
341  DebugCounter counter(const std::string& name)
342  { return DebugCounter(d_counters[name]); }
343  //! Accessing timers by name.
344  /*! If a timer doesn't exist, it is created and initialized to 0. */
345  DebugTimer timer(const std::string& name);
346 
347  //! Check whether to print trace info for a particular flag.
348  /*! Trace flags are the same DebugFlag objects, but live in a
349  different namespace from the normal debug flags */
350  bool trace(const std::string& name);
351 
352  // Timer functions
353 
354  //! Create a new "private" timer, initially set to 0.
355  /*! The new timer will not be added to the set of timers, will not
356  have a name, and will not be printed by 'printAll()'. It is
357  intended to be used to measure time intervals which are later
358  added or assigned to the named timers. */
359  static DebugTimer newTimer();
360 
361  //! Set the timer to the current time (whatever that means)
362  void setCurrentTime(DebugTimer& timer);
363  void setCurrentTime(const std::string& name) {
364  DebugTimer t(timer(name));
365  setCurrentTime(t);
366  }
367  /*! @brief Set the timer to the difference between current time
368  and the time stored in the timer: timer = currentTime -
369  timer. */
370  /*! Intended to obtain the time interval since the last call to
371  setCurrentTime() with that timer. */
372  void setElapsed(DebugTimer& timer);
373 
374  //! Return the ostream used for debugging output
375  std::ostream& getOS() { return *d_os; }
376  //! Return the ostream for dumping trace
377  std::ostream& getOSDumpTrace();
378 
379  //! Print an entry to the dump file
380  void dumpTrace(const std::string& title,
381  const std::vector<std::pair<std::string,std::string> >&
382  fields);
383  //! Set the debugging ostream
384  void setOS(std::ostream& os) { d_os = &os; }
385 
386  //! Print all the collected data if "DEBUG" flag is set to 'os'
387  void printAll(std::ostream& os);
388  /*! @brief Print all the collected data if "DEBUG" flag is set to
389  the default debug stream */
390  void printAll() { printAll(*d_os); }
391 
392  // Generally useful functions
393  //! Get the current scope level
394  int scopeLevel();
395 
396  }; // end of class Debug
397 
398  extern CVC_DLL Debug debugger;
399 
400 } // end of namespace CVC3
401 
402 #else // if _CVC3_DEBUG_MODE is not defined
403 
404 // All debugging macros are empty here
405 
406 #define IF_DEBUG(code)
407 
408 #define DebugAssert(cond, str)
409 
410 #define DBG_PRINT(cond, pre, v, post)
411 #define TRACE(cond, pre, v, post)
412 
413 #define DBG_PRINT_MSG(cond, msg)
414 #define TRACE_MSG(flag, msg)
415 
416 // to make the CLI wrapper happy
417 namespace CVC3 {
418 class DebugException: public Exception { };
419 }
420 
421 #endif // _CVC3_DEBUG_MODE
422 
423 #include "cvc_util.h"
424 
425 #endif // _cvc3__debug_h
CVC_DLL void fatalError(const std::string &file, int line, const std::string &cond, const std::string &msg)
Function for fatal exit.
Definition: debug.cpp:35
basic helper utilities
#define CVC_DLL
Definition: type.h:43
ExprStream & reset(ExprStream &os)
Reset the indentation to the default at this level.
bool operator<=(const Expr &e1, const Expr &e2)
Definition: expr.h:1612
ostream & operator<<(ostream &os, const Expr &e)
Definition: expr.cpp:621
Expr operator+(const Expr &left, const Expr &right)
Definition: theory_arith.h:232
STL namespace.
bool operator==(const Expr &e1, const Expr &e2)
Definition: expr.h:1600
bool operator>(const Expr &e1, const Expr &e2)
Definition: expr.h:1614
Expr operator-(const Expr &child)
Definition: theory_arith.h:230
std::string d_msg
Definition: exception.h:33
virtual std::string toString() const
Definition: exception.h:46
Abstraction over different operating systems.
bool operator<(const Expr &e1, const Expr &e2)
Definition: expr.h:1610
bool operator>=(const Expr &e1, const Expr &e2)
Definition: expr.h:1616
bool operator!=(const Expr &e1, const Expr &e2)
Definition: expr.h:1605
Definition: expr.cpp:35