debug.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file debug.h
00004  * \brief Description: Collection of debugging macros and functions. 
00005  * 
00006  * Author: Sergey Berezin
00007  * 
00008  * Created: Thu Dec  5 13:12:59 2002
00009  *
00010  * <hr>
00011  *
00012  * License to use, copy, modify, sell and/or distribute this software
00013  * and its documentation for any purpose is hereby granted without
00014  * royalty, subject to the terms and conditions defined in the \ref
00015  * LICENSE file provided with this distribution.
00016  * 
00017  * <hr>
00018  * 
00019  */
00020 /*****************************************************************************/
00021 
00022 #ifndef _cvc3__debug_h
00023 #define _cvc3__debug_h
00024 
00025 #include <string>
00026 #include <iostream>
00027 #include <sstream>
00028 #include <vector>
00029 #include "os.h"
00030 #include "exception.h"
00031 
00032 /*! @brief If something goes horribly wrong, print a message and abort
00033   immediately with exit(1). */
00034 /*! This macro stays even in the non-debug build, so the end users can
00035   send us meaningful bug reports. */
00036 
00037 #define FatalAssert(cond, msg) if(!(cond)) \
00038  CVC3::fatalError(__FILE__, __LINE__, #cond, msg)
00039 
00040 namespace CVC3 {
00041   //! Function for fatal exit.
00042   /*! It just exits with code 1, but is provided here for the debugger
00043    to set a breakpoint to.  For this reason, it is not inlined. */
00044   extern void fatalError(const std::string& file, int line,
00045        const std::string& cond, const std::string& msg);
00046 }
00047 
00048 #ifdef DEBUG
00049 
00050 #include "compat_hash_map.h"
00051 #include "compat_hash_set.h"
00052 
00053 //! Any debugging code must be within IF_DEBUG(...)
00054 #define IF_DEBUG(code) code
00055 
00056 //! Print a value conditionally.
00057 /*!  If 'cond' is true, print 'pre', then 'v', then 'post'.  The type
00058  of v must have overloaded operator<<.  It expects a ';' after it. */
00059 #define DBG_PRINT(cond, pre, v, post) if(cond) CVC3::debugger.getOS() \
00060   << (pre) << (v) << (post) << std::endl
00061 
00062 //! Print a message conditionally
00063 #define DBG_PRINT_MSG(cond, msg) \
00064   if(cond) CVC3::debugger.getOS() << (msg) << std::endl
00065 
00066 /*! @brief Same as DBG_PRINT, only takes a flag name instead of a
00067   general condition */
00068 #define TRACE(flag, pre, v, post) \
00069   DBG_PRINT(CVC3::debugger.trace(flag), pre, v, post)
00070 
00071 //! Same as TRACE, but for a simple message
00072 #define TRACE_MSG(flag, msg) \
00073   DBG_PRINT_MSG(CVC3::debugger.trace(flag), msg)
00074 
00075 //! Sanity check for debug build.  It disappears in the production code.
00076 #define DebugAssert(cond, str) if(!(cond)) \
00077  CVC3::debugError(__FILE__, __LINE__, #cond, str)
00078 
00079 
00080 namespace CVC3 {
00081 
00082 /*! @brief A class which sets a boolean value to true when created,
00083  * and resets to false when deleted.
00084  *
00085  * Useful for tracking when the control is within a certain method or
00086  * not.  For example, TheoryCore::addFact() uses d_inAddFact to check
00087  * that certain other methods are only called from within addFact().
00088  * However, when an exception is thrown, this variable is not reset.
00089  * The watcher class will reset the variable even in those cases.
00090  */
00091 class ScopeWatcher {
00092  private:
00093   bool *d_flag;
00094 public:
00095   ScopeWatcher(bool *flag): d_flag(flag) { *d_flag = true; }
00096   ~ScopeWatcher() { *d_flag = false; }
00097 };
00098 
00099   class Expr;
00100   //! Our exception to throw
00101   class DebugException: public Exception {
00102   public:
00103     // Constructor
00104     DebugException(const std::string& msg): Exception(msg) { }
00105     // Printing
00106     virtual std::string toString() const {
00107       return "Assertion violation " + d_msg;
00108     }
00109   }; // end of class DebugException
00110 
00111   //! Similar to fatalError to raise an exception when DebugAssert fires.
00112   /*! This does not necessarily cause the program to quit. */
00113   extern void debugError(const std::string& file, int line,
00114        const std::string& cond, const std::string& msg);
00115 
00116   // First, wrapper classes for flags, counters, and timers.  Later,
00117   // we overload some operators like '=', '++', etc. for those
00118   // classes.
00119   //! Boolean flag (can only be true or false)
00120   class DebugFlag {
00121   private:
00122     bool* d_flag; // We don't own the pointer
00123   public:
00124     // Constructor: takes the pointer to the actual flag, normally
00125     // stored in class Debug below.
00126     DebugFlag(bool& flag) : d_flag(&flag) { }
00127     // Destructor
00128     ~DebugFlag() { }
00129     // Auto-cast to boolean
00130     operator bool() { return *d_flag; }
00131 
00132     // Setting and resetting by ++ and --
00133     // Prefix versions:
00134     bool operator--() { *d_flag = false; return false; }
00135     bool operator++() { *d_flag = true; return true; }
00136     // Postfix versions:
00137     bool operator--(int) { bool x=*d_flag; *d_flag=false; return x; }
00138     bool operator++(int) { bool x=*d_flag; *d_flag=true; return x; }
00139     // Can be assigned only a boolean value
00140     DebugFlag& operator=(bool x) { *d_flag=(x!=false); return *this; }
00141     // Comparisons
00142     friend bool operator==(const DebugFlag& f1, const DebugFlag& f2);
00143     friend bool operator!=(const DebugFlag& f1, const DebugFlag& f2);
00144     // Printing
00145     friend std::ostream& operator<<(std::ostream& os, const DebugFlag& f);
00146   }; // end of class DebugFlag
00147 
00148   //! Checks if the *values* of the flags are equal
00149   inline bool operator==(const DebugFlag& f1, const DebugFlag& f2) {
00150     return (*f1.d_flag) == (*f2.d_flag);
00151   }
00152   //! Checks if the *values* of the flags are disequal
00153   inline bool operator!=(const DebugFlag& f1, const DebugFlag& f2) {
00154     return (*f1.d_flag) != (*f2.d_flag);
00155   }
00156   //! Printing flags
00157   inline std::ostream& operator<<(std::ostream& os, const DebugFlag& f) {
00158     if(*f.d_flag) return(os << "true");
00159     else return(os << "false");
00160   }
00161 
00162   //! Integer counter for debugging purposes.
00163   /*! Intended use is to count events (e.g. number of function calls),
00164     but can be used to store any integer value (e.g. size of some data
00165     structure) */
00166   class DebugCounter {
00167   private:
00168     int* d_counter; //!< We don't own the pointer
00169   public:
00170     //! Constructor
00171     /*!  Takes the pointer to the actual counter, normally stored in
00172       class Debug below. */
00173     DebugCounter(int& c) : d_counter(&c) { }
00174     //! Destructor
00175     ~DebugCounter() { }
00176     //! Auto-cast to int.
00177     /*! In particular, arithmetic comparisons like <, >, <=, >= will
00178       work because of this. */
00179     operator int() { return *d_counter; }
00180 
00181     // Auto-increment operators
00182 
00183     //! Prefix auto-decrement
00184     int operator--() { return --(*d_counter); }
00185     //! Prefix auto-increment
00186     int operator++() { return ++(*d_counter); }
00187     //! Postfix auto-decrement
00188     int operator--(int) { return (*d_counter)--; }
00189     //! Postfix auto-increment
00190     int operator++(int) { return (*d_counter)++; }
00191     //! Value assignment.
00192     DebugCounter& operator=(int x) { *d_counter=x; return *this; }
00193     DebugCounter& operator+=(int x) { *d_counter+=x; return *this; }
00194     DebugCounter& operator-=(int x) { *d_counter-=x; return *this; }
00195     //! Assignment from another counter.
00196     /*! It copies the value, not the pointer */
00197     DebugCounter& operator=(const DebugCounter& x)
00198       { *d_counter=*x.d_counter; return *this; }
00199     /*! It copies the value, not the pointer */
00200     DebugCounter& operator-=(const DebugCounter& x)
00201       { *d_counter-=*x.d_counter; return *this; }
00202     /*! It copies the value, not the pointer */
00203     DebugCounter& operator+=(const DebugCounter& x)
00204       { *d_counter+=*x.d_counter; return *this; }
00205     // Comparisons to integers and other DebugCounters
00206     friend bool operator==(const DebugCounter& c1, const DebugCounter& c2);
00207     friend bool operator!=(const DebugCounter& c1, const DebugCounter& c2);
00208     friend bool operator==(int c1, const DebugCounter& c2);
00209     friend bool operator!=(int c1, const DebugCounter& c2);
00210     friend bool operator==(const DebugCounter& c1, int c2);
00211     friend bool operator!=(const DebugCounter& c1, int c2);
00212     //! Printing counters
00213     friend std::ostream& operator<<(std::ostream& os, const DebugCounter& f);
00214   }; // end of class DebugCounter
00215 
00216   inline bool operator==(const DebugCounter& c1, const DebugCounter& c2) {
00217     return (*c1.d_counter) == (*c2.d_counter);
00218   }
00219   inline bool operator!=(const DebugCounter& c1, const DebugCounter& c2) {
00220     return (*c1.d_counter) != (*c2.d_counter);
00221   }
00222   inline bool operator==(int c1, const DebugCounter& c2) {
00223     return c1 == (*c2.d_counter);
00224   }
00225   inline bool operator!=(int c1, const DebugCounter& c2) {
00226     return c1 != (*c2.d_counter);
00227   }
00228   inline bool operator==(const DebugCounter& c1, int c2) {
00229     return (*c1.d_counter) == c2;
00230   }
00231   inline bool operator!=(const DebugCounter& c1, int c2) {
00232     return (*c1.d_counter) != c2;
00233   }
00234   inline std::ostream& operator<<(std::ostream& os, const DebugCounter& c) {
00235     return (os << *c.d_counter);
00236   }
00237 
00238   //! A class holding the time value.
00239   /*! What exactly is time is not exposed.  It can be the system's
00240     struct timeval, or it can be the (subset of the) user/system/real
00241     time tuple. */
00242   class DebugTime;
00243 
00244   //! Time counter.
00245   /*! Intended use is to store time intervals or accumulated time for
00246     multiple events (e.g. time spent to execute certain lines of code,
00247     or accumulated time spent in a particular function). */
00248   class DebugTimer {
00249   private:
00250     DebugTime* d_time; //!< The time value
00251     bool d_clean_time; //!< Set if we own *d_time
00252   public:
00253     //! Constructor: takes the pointer to the actual time value.
00254     /*! It is either stored in class Debug below (then the timer is
00255       "public"), or we own it, making the timer "private". */
00256     DebugTimer(DebugTime* time, bool take_time = false)
00257       : d_time(time), d_clean_time(take_time) { }
00258     /*! @brief Copy constructor: copy the *pointer* from public
00259       timers, and *value* from private.  */
00260     /*! The reason for different behavior for public and private time
00261       is the following.  When you modify a public timer, you want the
00262       changes to show in the central database and everywhere else,
00263       whereas private timers are used as independent temporary
00264       variables holding intermediate time values. */
00265     DebugTimer(const DebugTimer& timer);
00266     //! Assignment: same logistics as for the copy constructor
00267     DebugTimer& operator=(const DebugTimer& timer);
00268 
00269     //! Destructor
00270     ~DebugTimer();
00271 
00272     // Operators
00273     //! Set time to zero
00274     void reset();
00275     DebugTimer& operator+=(const DebugTimer& timer);
00276     DebugTimer& operator-=(const DebugTimer& timer);
00277     //! Produces new "private" timer
00278     DebugTimer operator+(const DebugTimer& timer);
00279     //! Produces new "private" timer
00280     DebugTimer operator-(const DebugTimer& timer);
00281 
00282     // Our friends
00283     friend class Debug;
00284     // Comparisons
00285     friend bool operator==(const DebugTimer& t1, const DebugTimer& t2);
00286     friend bool operator!=(const DebugTimer& t1, const DebugTimer& t2);
00287     friend bool operator<(const DebugTimer& t1, const DebugTimer& t2);
00288     friend bool operator>(const DebugTimer& t1, const DebugTimer& t2);
00289     friend bool operator<=(const DebugTimer& t1, const DebugTimer& t2);
00290     friend bool operator>=(const DebugTimer& t1, const DebugTimer& t2);
00291 
00292     //! Print the timer's value
00293     friend std::ostream& operator<<(std::ostream& os, const DebugTimer& timer);
00294   }; // end of class DebugTimer
00295 
00296   //! The heart of the Bug Extermination Kingdom.
00297   /*! This class exposes many important components of the entire
00298     CVC-lite system for use in debugging, keeps all the flags,
00299     counters, and timers in the central database, and provides timing
00300     and printing functions. */
00301 
00302   class Debug {
00303   private:
00304     //! Command line options for tracing; these override the TRACE command
00305     const std::vector<std::pair<std::string,bool> >* d_traceOptions;
00306     //! name of dump file
00307     const std::string* d_dumpName;
00308     // Output control
00309     std::ostream* d_os;
00310     // Stream for dumping trace to file ("dump-trace" option)
00311     std::ostream* d_osDumpTrace;
00312     //! Private hasher class for strings
00313     class stringHash {
00314     public:
00315       size_t operator()(const std::string& s) const {
00316   std::hash<char*> h;
00317   return h(s.c_str());
00318       }
00319     }; // end of stringHash
00320     // Hash tables for storing flags, counters, and timers
00321     typedef std::hash_map<std::string, bool, stringHash> FlagMap;
00322     typedef std::hash_map<std::string, int, stringHash> CounterMap;
00323     typedef std::hash_map<std::string, DebugTime*, stringHash> TimerMap;
00324     FlagMap d_flags;       //!< Set of flags
00325     FlagMap d_traceFlags;  //!< Set of trace flags
00326     CounterMap d_counters; //!< Set of counters
00327     /*! Note, that the d_timers map does *not* own the pointers; so
00328       the objects in d_timers must be destroyed explicitly in our
00329       destructor. */
00330     TimerMap d_timers;     //!< Set of timers
00331 
00332   public:
00333     //! Constructor
00334     Debug(): d_traceOptions(NULL), d_os(&std::cerr), d_osDumpTrace(NULL) { }
00335     //! Destructor (must destroy objects it d_timers)
00336     ~Debug();
00337     //! Must be called before Debug class can be safely used
00338     void init(const std::vector<std::pair<std::string,bool> >* traceOptions,
00339               const std::string* dumpName);
00340     //! Accessing flags by name.
00341     /*! If a flag doesn't exist, it is created and initialized to
00342       false. */
00343     DebugFlag flag(const std::string& name)
00344       { return DebugFlag(d_flags[name]); }
00345     //! Accessing tracing flags by name.
00346     /*! If a flag doesn't exist, it is created and initialized to
00347       false. */
00348     DebugFlag traceFlag(const std::string& name)
00349       { return DebugFlag(d_traceFlags[name]); }
00350     //! Accessing tracing flag by char* name (mostly for GDB)
00351     DebugFlag traceFlag(char* name);
00352     //! Set tracing of everything on (1) and off (0) [for use in GDB]
00353     void traceAll(bool enable = true);
00354     //! Accessing counters by name.
00355     /*! If a counter doesn't exist, it is created and initialized to 0. */
00356     DebugCounter counter(const std::string& name)
00357       { return DebugCounter(d_counters[name]); }
00358     //! Accessing timers by name.
00359     /*! If a timer doesn't exist, it is created and initialized to 0. */
00360     DebugTimer timer(const std::string& name);
00361 
00362     //! Check whether to print trace info for a particular flag.
00363     /*! Trace flags are the same DebugFlag objects, but live in a
00364       different namespace from the normal debug flags */
00365     bool trace(const std::string& name);
00366 
00367     // Timer functions
00368 
00369     //! Create a new "private" timer, initially set to 0. 
00370     /*! The new timer will not be added to the set of timers, will not
00371      have a name, and will not be printed by 'printAll()'.  It is
00372      intended to be used to measure time intervals which are later
00373      added or assigned to the named timers. */
00374     static DebugTimer newTimer();
00375 
00376     //! Set the timer to the current time (whatever that means)
00377     void setCurrentTime(DebugTimer& timer);
00378     void setCurrentTime(const std::string& name) {
00379       DebugTimer t(timer(name));
00380       setCurrentTime(t);
00381     }
00382     /*! @brief Set the timer to the difference between current time
00383       and the time stored in the timer: timer = currentTime -
00384       timer. */
00385     /*! Intended to obtain the time interval since the last call to
00386       setCurrentTime() with that timer. */
00387     void setElapsed(DebugTimer& timer);
00388     
00389     //! Return the ostream used for debugging output
00390     std::ostream& getOS() { return *d_os; }
00391     //! Return the ostream for dumping trace
00392     std::ostream& getOSDumpTrace();
00393 
00394     //! Print an entry to the dump file
00395     void dumpTrace(const std::string& title,
00396        const std::vector<std::pair<std::string,std::string> >&
00397        fields);
00398     //! Set the debugging ostream
00399     void setOS(std::ostream& os) { d_os = &os; }
00400 
00401     //! Print all the collected data if "DEBUG" flag is set to 'os'
00402     void printAll(std::ostream& os);
00403     /*! @brief Print all the collected data if "DEBUG" flag is set to
00404       the default debug stream */
00405     void printAll() { printAll(*d_os); }
00406 
00407     // Generally useful functions
00408     //! Get the current scope level
00409     int scopeLevel();
00410 
00411   }; // end of class Debug
00412 
00413   extern Debug debugger;
00414 
00415 } // end of namespace CVC3
00416 
00417 #else  // if DEBUG is not defined
00418 
00419 // All debugging macros are empty here
00420 
00421 #define IF_DEBUG(code)
00422 
00423 #define DebugAssert(cond, str)
00424 
00425 #define DBG_PRINT(cond, pre, v, post)
00426 #define TRACE(cond, pre, v, post)
00427 
00428 #define DBG_PRINT_MSG(cond, msg)
00429 #define TRACE_MSG(flag, msg)
00430 
00431 // to make the CLI wrapper happy
00432 namespace CVC3 {
00433 class DebugException: public Exception { };
00434 }
00435 
00436 #endif // DEBUG
00437 
00438 #include "cvc_util.h"
00439 
00440 #endif // _cvc3__debug_h

Generated on Tue Jul 3 14:33:36 2007 for CVC3 by  doxygen 1.5.1