CVC3

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 CVC_DLL void fatalError(const std::string& file, int line,
00045        const std::string& cond, const std::string& msg);
00046 }
00047 
00048 #ifdef _CVC3_DEBUG_MODE
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   class Expr;
00083   //! Our exception to throw
00084   class DebugException: public Exception {
00085   public:
00086     // Constructor
00087     DebugException(const std::string& msg): Exception(msg) { }
00088     // Printing
00089     virtual std::string toString() const {
00090       return "Assertion violation " + d_msg;
00091     }
00092   }; // end of class DebugException
00093 
00094   //! Similar to fatalError to raise an exception when DebugAssert fires.
00095   /*! This does not necessarily cause the program to quit. */
00096   extern CVC_DLL void debugError(const std::string& file, int line,
00097        const std::string& cond, const std::string& msg);
00098 
00099   // First, wrapper classes for flags, counters, and timers.  Later,
00100   // we overload some operators like '=', '++', etc. for those
00101   // classes.
00102   //! Boolean flag (can only be true or false)
00103   class DebugFlag {
00104   private:
00105     bool* d_flag; // We don't own the pointer
00106   public:
00107     // Constructor: takes the pointer to the actual flag, normally
00108     // stored in class Debug below.
00109     DebugFlag(bool& flag) : d_flag(&flag) { }
00110     // Destructor
00111     ~DebugFlag() { }
00112     // Auto-cast to boolean
00113     operator bool() { return *d_flag; }
00114 
00115     // Setting and resetting by ++ and --
00116     // Prefix versions:
00117     bool operator--() { *d_flag = false; return false; }
00118     bool operator++() { *d_flag = true; return true; }
00119     // Postfix versions:
00120     bool operator--(int) { bool x=*d_flag; *d_flag=false; return x; }
00121     bool operator++(int) { bool x=*d_flag; *d_flag=true; return x; }
00122     // Can be assigned only a boolean value
00123     DebugFlag& operator=(bool x) { *d_flag=(x!=false); return *this; }
00124     // Comparisons
00125     friend bool operator==(const DebugFlag& f1, const DebugFlag& f2);
00126     friend bool operator!=(const DebugFlag& f1, const DebugFlag& f2);
00127     // Printing
00128     friend std::ostream& operator<<(std::ostream& os, const DebugFlag& f);
00129   }; // end of class DebugFlag
00130 
00131   //! Checks if the *values* of the flags are equal
00132   inline bool operator==(const DebugFlag& f1, const DebugFlag& f2) {
00133     return (*f1.d_flag) == (*f2.d_flag);
00134   }
00135   //! Checks if the *values* of the flags are disequal
00136   inline bool operator!=(const DebugFlag& f1, const DebugFlag& f2) {
00137     return (*f1.d_flag) != (*f2.d_flag);
00138   }
00139   //! Printing flags
00140   inline std::ostream& operator<<(std::ostream& os, const DebugFlag& f) {
00141     if(*f.d_flag) return(os << "true");
00142     else return(os << "false");
00143   }
00144 
00145   //! Integer counter for debugging purposes.
00146   /*! Intended use is to count events (e.g. number of function calls),
00147     but can be used to store any integer value (e.g. size of some data
00148     structure) */
00149   class DebugCounter {
00150   private:
00151     int* d_counter; //!< We don't own the pointer
00152   public:
00153     //! Constructor
00154     /*!  Takes the pointer to the actual counter, normally stored in
00155       class Debug below. */
00156     DebugCounter(int& c) : d_counter(&c) { }
00157     //! Destructor
00158     ~DebugCounter() { }
00159     //! Auto-cast to int.
00160     /*! In particular, arithmetic comparisons like <, >, <=, >= will
00161       work because of this. */
00162     operator int() { return *d_counter; }
00163 
00164     // Auto-increment operators
00165 
00166     //! Prefix auto-decrement
00167     int operator--() { return --(*d_counter); }
00168     //! Prefix auto-increment
00169     int operator++() { return ++(*d_counter); }
00170     //! Postfix auto-decrement
00171     int operator--(int) { return (*d_counter)--; }
00172     //! Postfix auto-increment
00173     int operator++(int) { return (*d_counter)++; }
00174     //! Value assignment.
00175     DebugCounter& operator=(int x) { *d_counter=x; return *this; }
00176     DebugCounter& operator+=(int x) { *d_counter+=x; return *this; }
00177     DebugCounter& operator-=(int x) { *d_counter-=x; return *this; }
00178     //! Assignment from another counter.
00179     /*! It copies the value, not the pointer */
00180     DebugCounter& operator=(const DebugCounter& x)
00181       { *d_counter=*x.d_counter; return *this; }
00182     /*! It copies the value, not the pointer */
00183     DebugCounter& operator-=(const DebugCounter& x)
00184       { *d_counter-=*x.d_counter; return *this; }
00185     /*! It copies the value, not the pointer */
00186     DebugCounter& operator+=(const DebugCounter& x)
00187       { *d_counter+=*x.d_counter; return *this; }
00188     // Comparisons to integers and other DebugCounters
00189     friend bool operator==(const DebugCounter& c1, const DebugCounter& c2);
00190     friend bool operator!=(const DebugCounter& c1, const DebugCounter& c2);
00191     friend bool operator==(int c1, const DebugCounter& c2);
00192     friend bool operator!=(int c1, const DebugCounter& c2);
00193     friend bool operator==(const DebugCounter& c1, int c2);
00194     friend bool operator!=(const DebugCounter& c1, int c2);
00195     //! Printing counters
00196     friend std::ostream& operator<<(std::ostream& os, const DebugCounter& f);
00197   }; // end of class DebugCounter
00198 
00199   inline bool operator==(const DebugCounter& c1, const DebugCounter& c2) {
00200     return (*c1.d_counter) == (*c2.d_counter);
00201   }
00202   inline bool operator!=(const DebugCounter& c1, const DebugCounter& c2) {
00203     return (*c1.d_counter) != (*c2.d_counter);
00204   }
00205   inline bool operator==(int c1, const DebugCounter& c2) {
00206     return c1 == (*c2.d_counter);
00207   }
00208   inline bool operator!=(int c1, const DebugCounter& c2) {
00209     return c1 != (*c2.d_counter);
00210   }
00211   inline bool operator==(const DebugCounter& c1, int c2) {
00212     return (*c1.d_counter) == c2;
00213   }
00214   inline bool operator!=(const DebugCounter& c1, int c2) {
00215     return (*c1.d_counter) != c2;
00216   }
00217   inline std::ostream& operator<<(std::ostream& os, const DebugCounter& c) {
00218     return (os << *c.d_counter);
00219   }
00220 
00221   //! A class holding the time value.
00222   /*! What exactly is time is not exposed.  It can be the system's
00223     struct timeval, or it can be the (subset of the) user/system/real
00224     time tuple. */
00225   class DebugTime;
00226 
00227   //! Time counter.
00228   /*! Intended use is to store time intervals or accumulated time for
00229     multiple events (e.g. time spent to execute certain lines of code,
00230     or accumulated time spent in a particular function). */
00231   class CVC_DLL DebugTimer {
00232   private:
00233     DebugTime* d_time; //!< The time value
00234     bool d_clean_time; //!< Set if we own *d_time
00235   public:
00236     //! Constructor: takes the pointer to the actual time value.
00237     /*! It is either stored in class Debug below (then the timer is
00238       "public"), or we own it, making the timer "private". */
00239     DebugTimer(DebugTime* time, bool take_time = false)
00240       : d_time(time), d_clean_time(take_time) { }
00241     /*! @brief Copy constructor: copy the *pointer* from public
00242       timers, and *value* from private.  */
00243     /*! The reason for different behavior for public and private time
00244       is the following.  When you modify a public timer, you want the
00245       changes to show in the central database and everywhere else,
00246       whereas private timers are used as independent temporary
00247       variables holding intermediate time values. */
00248     DebugTimer(const DebugTimer& timer);
00249     //! Assignment: same logistics as for the copy constructor
00250     DebugTimer& operator=(const DebugTimer& timer);
00251 
00252     //! Destructor
00253     ~DebugTimer();
00254 
00255     // Operators
00256     //! Set time to zero
00257     void reset();
00258     DebugTimer& operator+=(const DebugTimer& timer);
00259     DebugTimer& operator-=(const DebugTimer& timer);
00260     //! Produces new "private" timer
00261     DebugTimer operator+(const DebugTimer& timer);
00262     //! Produces new "private" timer
00263     DebugTimer operator-(const DebugTimer& timer);
00264 
00265     // Our friends
00266     friend class Debug;
00267     // Comparisons
00268     friend bool operator==(const DebugTimer& t1, const DebugTimer& t2);
00269     friend bool operator!=(const DebugTimer& t1, const DebugTimer& t2);
00270     friend bool operator<(const DebugTimer& t1, const DebugTimer& t2);
00271     friend bool operator>(const DebugTimer& t1, const DebugTimer& t2);
00272     friend bool operator<=(const DebugTimer& t1, const DebugTimer& t2);
00273     friend bool operator>=(const DebugTimer& t1, const DebugTimer& t2);
00274 
00275     //! Print the timer's value
00276     friend std::ostream& operator<<(std::ostream& os, const DebugTimer& timer);
00277   }; // end of class DebugTimer
00278 
00279   //! The heart of the Bug Extermination Kingdom.
00280   /*! This class exposes many important components of the entire
00281     CVC-lite system for use in debugging, keeps all the flags,
00282     counters, and timers in the central database, and provides timing
00283     and printing functions. */
00284 
00285   class CVC_DLL Debug {
00286   private:
00287     //! Command line options for tracing; these override the TRACE command
00288     const std::vector<std::pair<std::string,bool> >* d_traceOptions;
00289     //! name of dump file
00290     const std::string* d_dumpName;
00291     // Output control
00292     std::ostream* d_os;
00293     // Stream for dumping trace to file ("dump-trace" option)
00294     std::ostream* d_osDumpTrace;
00295     //! Private hasher class for strings
00296     class stringHash {
00297     public:
00298       size_t operator()(const std::string& s) const {
00299   std::hash<char*> h;
00300   return h(s.c_str());
00301       }
00302     }; // end of stringHash
00303     // Hash tables for storing flags, counters, and timers
00304     typedef std::hash_map<std::string, bool, stringHash> FlagMap;
00305     typedef std::hash_map<std::string, int, stringHash> CounterMap;
00306     typedef std::hash_map<std::string, DebugTime*, stringHash> TimerMap;
00307     FlagMap d_flags;       //!< Set of flags
00308     FlagMap d_traceFlags;  //!< Set of trace flags
00309     CounterMap d_counters; //!< Set of counters
00310     /*! Note, that the d_timers map does *not* own the pointers; so
00311       the objects in d_timers must be destroyed explicitly in our
00312       destructor. */
00313     TimerMap d_timers;     //!< Set of timers
00314 
00315   public:
00316     //! Constructor
00317     Debug(): d_traceOptions(NULL), d_os(&std::cerr), d_osDumpTrace(NULL) { }
00318     //! Destructor (must destroy objects it d_timers)
00319     ~Debug();
00320     //! Must be called before Debug class can be safely used
00321     void init(const std::vector<std::pair<std::string,bool> >* traceOptions,
00322               const std::string* dumpName);
00323     //! Must be called before arguments supplied to init are deallocated
00324     void finalize();
00325     //! Accessing flags by name.
00326     /*! If a flag doesn't exist, it is created and initialized to
00327       false. */
00328     DebugFlag flag(const std::string& name)
00329       { return DebugFlag(d_flags[name]); }
00330     //! Accessing tracing flags by name.
00331     /*! If a flag doesn't exist, it is created and initialized to
00332       false. */
00333     DebugFlag traceFlag(const std::string& name)
00334       { return DebugFlag(d_traceFlags[name]); }
00335     //! Accessing tracing flag by char* name (mostly for GDB)
00336     DebugFlag traceFlag(const char* name);
00337     //! Set tracing of everything on (1) and off (0) [for use in GDB]
00338     void traceAll(bool enable = true);
00339     //! Accessing counters by name.
00340     /*! If a counter doesn't exist, it is created and initialized to 0. */
00341     DebugCounter counter(const std::string& name)
00342       { return DebugCounter(d_counters[name]); }
00343     //! Accessing timers by name.
00344     /*! If a timer doesn't exist, it is created and initialized to 0. */
00345     DebugTimer timer(const std::string& name);
00346 
00347     //! Check whether to print trace info for a particular flag.
00348     /*! Trace flags are the same DebugFlag objects, but live in a
00349       different namespace from the normal debug flags */
00350     bool trace(const std::string& name);
00351 
00352     // Timer functions
00353 
00354     //! Create a new "private" timer, initially set to 0.
00355     /*! The new timer will not be added to the set of timers, will not
00356      have a name, and will not be printed by 'printAll()'.  It is
00357      intended to be used to measure time intervals which are later
00358      added or assigned to the named timers. */
00359     static DebugTimer newTimer();
00360 
00361     //! Set the timer to the current time (whatever that means)
00362     void setCurrentTime(DebugTimer& timer);
00363     void setCurrentTime(const std::string& name) {
00364       DebugTimer t(timer(name));
00365       setCurrentTime(t);
00366     }
00367     /*! @brief Set the timer to the difference between current time
00368       and the time stored in the timer: timer = currentTime -
00369       timer. */
00370     /*! Intended to obtain the time interval since the last call to
00371       setCurrentTime() with that timer. */
00372     void setElapsed(DebugTimer& timer);
00373 
00374     //! Return the ostream used for debugging output
00375     std::ostream& getOS() { return *d_os; }
00376     //! Return the ostream for dumping trace
00377     std::ostream& getOSDumpTrace();
00378 
00379     //! Print an entry to the dump file
00380     void dumpTrace(const std::string& title,
00381        const std::vector<std::pair<std::string,std::string> >&
00382        fields);
00383     //! Set the debugging ostream
00384     void setOS(std::ostream& os) { d_os = &os; }
00385 
00386     //! Print all the collected data if "DEBUG" flag is set to 'os'
00387     void printAll(std::ostream& os);
00388     /*! @brief Print all the collected data if "DEBUG" flag is set to
00389       the default debug stream */
00390     void printAll() { printAll(*d_os); }
00391 
00392     // Generally useful functions
00393     //! Get the current scope level
00394     int scopeLevel();
00395 
00396   }; // end of class Debug
00397 
00398   extern CVC_DLL Debug debugger;
00399 
00400 } // end of namespace CVC3
00401 
00402 #else  // if _CVC3_DEBUG_MODE is not defined
00403 
00404 // All debugging macros are empty here
00405 
00406 #define IF_DEBUG(code)
00407 
00408 #define DebugAssert(cond, str)
00409 
00410 #define DBG_PRINT(cond, pre, v, post)
00411 #define TRACE(cond, pre, v, post)
00412 
00413 #define DBG_PRINT_MSG(cond, msg)
00414 #define TRACE_MSG(flag, msg)
00415 
00416 // to make the CLI wrapper happy
00417 namespace CVC3 {
00418 class DebugException: public Exception { };
00419 }
00420 
00421 #endif // _CVC3_DEBUG_MODE
00422 
00423 #include "cvc_util.h"
00424 
00425 #endif // _cvc3__debug_h