debug.cpp

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file debug.cpp
00004  * \brief Description: Implementation of debugging facilities.
00005  * 
00006  * Author: Sergey Berezin
00007  * 
00008  * Created: Fri Jan 31 11:48:37 2003
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 #include <fstream>
00023 
00024 #include "debug.h"
00025 
00026 using namespace std;
00027 
00028 namespace CVC3 {
00029   
00030 // Function for fatal exit.  It just exits with code 1, but is
00031 // provided here for the debugger to set a breakpoint to.  For this
00032 // reason, it is not inlined.
00033 void fatalError(const std::string& file, int line,
00034     const std::string& cond, const std::string& msg) {
00035   cerr <<  "\n**** Fatal error in " << file << ":" << line
00036        << " (" << cond << ")\n" << msg << endl << flush;
00037   exit(1);
00038 }
00039   
00040 } // end of namespace CVC3
00041 
00042 #ifdef DEBUG
00043 
00044 #include <ctime>
00045 #include <iomanip>
00046 
00047 namespace CVC3 {
00048 // Similar to fatalError to raise an exception when DebugAssert fires.
00049 // This does not necessarily cause the program to quit.
00050 void debugError(const std::string& file, int line,
00051     const std::string& cond, const std::string& msg) {
00052   ostringstream ss;
00053   ss << "in " << file << ":" << line << " (" << cond << ")\n" << msg;
00054   throw DebugException(ss.str());
00055 }
00056   
00057 
00058 class DebugTime {
00059 public:
00060   clock_t d_clock;
00061 
00062   // Constructors
00063   DebugTime() {
00064     d_clock = 0;
00065   }
00066   DebugTime(const clock_t& clock): d_clock(clock) { }
00067 
00068   // Set time to zero
00069   void reset() {
00070     d_clock = 0;
00071   }
00072     
00073   // Incremental assignments
00074   DebugTime& operator+=(const DebugTime& t) {
00075     d_clock += t.d_clock;
00076     return *this;
00077   }
00078   DebugTime& operator-=(const DebugTime& t) {
00079     d_clock -= t.d_clock;
00080     return *this;
00081   }
00082 
00083   friend bool operator==(const DebugTime& t1, const DebugTime& t2);
00084   friend bool operator!=(const DebugTime& t1, const DebugTime& t2);
00085 
00086   friend bool operator<(const DebugTime& t1, const DebugTime& t2);
00087   friend bool operator>(const DebugTime& t1, const DebugTime& t2);
00088   friend bool operator<=(const DebugTime& t1, const DebugTime& t2);
00089   friend bool operator>=(const DebugTime& t1, const DebugTime& t2);
00090 
00091   friend ostream& operator<<(ostream& os, const DebugTime& t);
00092 };
00093 
00094 DebugTime operator+(const DebugTime& t1, const DebugTime& t2) {
00095   DebugTime res(t1);
00096   res += t2;
00097   return res;
00098 }
00099 DebugTime operator-(const DebugTime& t1, const DebugTime& t2) {
00100   DebugTime res(t1);
00101   res -= t2;
00102   return res;
00103 }
00104 
00105 bool operator==(const DebugTime& t1, const DebugTime& t2) {
00106   return t1.d_clock == t2.d_clock;
00107 }
00108 
00109 bool operator!=(const DebugTime& t1, const DebugTime& t2) {
00110   return !(t1 == t2);
00111 }
00112 
00113 bool operator<(const DebugTime& t1, const DebugTime& t2) {
00114   return t1.d_clock < t2.d_clock;
00115 }
00116 
00117 bool operator>(const DebugTime& t1, const DebugTime& t2) {
00118   return t1.d_clock > t2.d_clock;
00119 }
00120 
00121 bool operator<=(const DebugTime& t1, const DebugTime& t2) {
00122   return t1.d_clock <= t2.d_clock;
00123 }
00124 
00125 bool operator>=(const DebugTime& t1, const DebugTime& t2) {
00126   return t1.d_clock >= t2.d_clock;
00127 }
00128 
00129 ////////////////////////////////////////////////////////////////////////
00130 // Class DebugTimer
00131 ////////////////////////////////////////////////////////////////////////
00132 
00133 // Destructor
00134 DebugTimer::~DebugTimer() {
00135   if(d_clean_time)
00136     delete d_time;
00137 }
00138 
00139 void Debug::init(const std::vector<std::pair<std::string,bool> >* traceOptions,
00140                  const std::string* dumpName)
00141 {
00142   d_traceOptions = traceOptions;
00143   d_dumpName = dumpName;
00144 }
00145 
00146 
00147 DebugFlag
00148 Debug::traceFlag(char* name) { return traceFlag(std::string(name)); }
00149 
00150 void
00151 Debug::traceAll(bool enable) { traceFlag("ALL") = enable; }
00152 
00153 // Copy constructor: copy the *pointer* from public timers, and
00154 // value from private.  The reason is, when you modify a public
00155 // timer, you want the changes to show in the central database and
00156 // everywhere else, whereas private timers are used as independent
00157 // temporary variables holding intermediate time values.
00158 DebugTimer::DebugTimer(const DebugTimer& timer) {
00159   d_clean_time = timer.d_clean_time;
00160   if(d_clean_time) {
00161     // We are copying a private timer; make our own copy
00162     d_time = new DebugTime(*timer.d_time);
00163     d_clean_time = true;
00164   } else {
00165     // This is a public timer; just grab the pointer
00166     d_time = timer.d_time;
00167   }
00168 }
00169 // Assignment: same logistics as for the copy constructor, but need
00170 // to take care of our own pointer
00171 DebugTimer& DebugTimer::operator=(const DebugTimer& timer) {
00172   // Check for self-assignment
00173   if(&timer == this) return *this;
00174 
00175   if(timer.d_clean_time) {
00176     // We are copying a private timer
00177     if(d_clean_time) // We already have a private pointer, reuse it
00178       *d_time = *timer.d_time;
00179     else { // Create a new storage
00180       d_time = new DebugTime(*timer.d_time);
00181       d_clean_time = true;
00182     }
00183   } else {
00184     // This is a public timer
00185     if(d_clean_time) // We own our pointer, clean it up first
00186       delete d_time;
00187     d_time = timer.d_time;
00188     d_clean_time = false; 
00189   }
00190   return *this;
00191 }
00192 
00193 void DebugTimer::reset() {
00194   d_time->reset();
00195 }
00196 
00197 DebugTimer& DebugTimer::operator+=(const DebugTimer& timer) {
00198   (*d_time) += *(timer.d_time);
00199   return *this;
00200 }
00201 
00202 DebugTimer& DebugTimer::operator-=(const DebugTimer& timer) {
00203   (*d_time) -= *(timer.d_time);
00204   return *this;
00205 }
00206 
00207 // These will produce new "private" timers
00208 DebugTimer DebugTimer::operator+(const DebugTimer& timer) {
00209   return DebugTimer(new DebugTime((*d_time) + (*timer.d_time)),
00210         true /* take the new DebugTime */);
00211 }
00212 
00213 DebugTimer DebugTimer::operator-(const DebugTimer& timer) {
00214   return DebugTimer(new DebugTime((*d_time) - (*timer.d_time)),
00215         true /* take the new DebugTime */);
00216 }
00217 
00218 // Comparisons
00219 bool operator==(const DebugTimer& t1, const DebugTimer& t2) {
00220   return(*t1.d_time == *t2.d_time);
00221 }
00222 bool operator!=(const DebugTimer& t1, const DebugTimer& t2) {
00223   return(*t1.d_time != *t2.d_time);
00224 }
00225 bool operator<(const DebugTimer& t1, const DebugTimer& t2) {
00226   return *t1.d_time < *t2.d_time;
00227 }
00228 bool operator>(const DebugTimer& t1, const DebugTimer& t2) {
00229   return *t1.d_time > *t2.d_time;
00230 }
00231 bool operator<=(const DebugTimer& t1, const DebugTimer& t2) {
00232   return *t1.d_time <= *t2.d_time;
00233 }
00234 bool operator>=(const DebugTimer& t1, const DebugTimer& t2) {
00235   return *t1.d_time >= *t2.d_time;
00236 }
00237 
00238 // Print the time and timer's values
00239 ostream& operator<<(ostream& os, const DebugTime& t) {
00240   int seconds = (int)(t.d_clock / CLOCKS_PER_SEC);
00241   int milliseconds = 1000 * int((((double)(t.d_clock % CLOCKS_PER_SEC)) / CLOCKS_PER_SEC));
00242   os << seconds << "." << setfill('0') << setw(6) << milliseconds;
00243   return os;
00244 }
00245 ostream& operator<<(ostream& os, const DebugTimer& timer) {
00246   return(os << *timer.d_time);
00247 }
00248   
00249 ////////////////////////////////////////////////////////////////////////
00250 // Class Debug
00251 ////////////////////////////////////////////////////////////////////////
00252 
00253 // Destructor: destroy all the pointers in d_timers
00254 Debug::~Debug() {
00255   TimerMap::iterator i, iend;
00256   for(i = d_timers.begin(), iend = d_timers.end(); i != iend; ++i)
00257     delete (*i).second;
00258   if(d_osDumpTrace != NULL)
00259     delete d_osDumpTrace;
00260 }
00261 
00262 bool
00263 Debug::trace(const string& name) {
00264   // First, check if this flag was set in the command line.  Walk the
00265   // vector backwards, so that the last +/-trace takes effect.
00266   if(d_traceOptions != NULL) {
00267     vector<pair<string,bool> >::const_reverse_iterator i, iend;
00268     for(i=d_traceOptions->rbegin(), iend=d_traceOptions->rend(); i!=iend; ++i)
00269       if((*i).first == name || (*i).first == "ALL") return (*i).second;
00270   }
00271   return traceFlag(name) || traceFlag("ALL");
00272 }
00273 
00274 
00275 DebugTimer Debug::timer(const string& name) {
00276   // See if we already have the timer 
00277   if(d_timers.count(name) > 0) return(DebugTimer(d_timers[name]));
00278   else {
00279     // Create a new timer
00280     DebugTime *t = new DebugTime();
00281     d_timers[name] = t;
00282     return DebugTimer(t);
00283   }
00284 }
00285 
00286 DebugTimer Debug::newTimer() {
00287   return DebugTimer(new DebugTime(), true /* take the pointer */);
00288 }
00289 
00290 void Debug::setCurrentTime(DebugTimer& timer) {
00291   *timer.d_time = clock();
00292 }
00293 
00294 // Set the timer to the difference between current time and the
00295 // time stored in the timer: timer = currentTime - timer.
00296 // Intended to obtain the time interval since the last call to
00297 // setCurrentTime() with that timer.
00298 void Debug::setElapsed(DebugTimer& timer) {
00299   *timer.d_time -= DebugTime(clock());
00300 }
00301 
00302 /*! If the stream is not initialized, open the file
00303  * If the filename is empty or "-", then return
00304  * cout (but do not initialize the stream in this case).
00305  */
00306   
00307 ostream& Debug::getOSDumpTrace() {
00308   if(d_osDumpTrace != NULL) return *d_osDumpTrace;
00309   // Check if the flag has a file name in it
00310   if(*d_dumpName == "" || *d_dumpName == "-") return cout;
00311   d_osDumpTrace = new ofstream(d_dumpName->c_str());
00312   return *d_osDumpTrace;
00313 }
00314 
00315 
00316 // Print an entry to the dump-sat file: free-form message
00317 void Debug::dumpTrace(const std::string& title, 
00318           const std::vector<std::pair<std::string,std::string> >& fields) {
00319   ostream& os = getOSDumpTrace();
00320   os << "[" << title << "]\n";
00321   for(size_t i=0, iend=fields.size(); i<iend; ++i)
00322     os << fields[i].first << " = " << fields[i].second << "\n";
00323   os << endl;
00324 }
00325 
00326 
00327 // Print all the collected data if "DEBUG" flag is set
00328 void Debug::printAll(ostream& os) {
00329   if(!trace("DEBUG")) return;
00330   // Flags
00331   os << endl
00332      << "********************************" << endl
00333      << "******* Debugging Info *********" << endl
00334      << "********************************" << endl;
00335 
00336   if(d_flags.size() > 0) {
00337     os << endl << "************ Flags *************" << endl << endl;
00338     for(FlagMap::iterator
00339     i = d_flags.begin(), iend = d_flags.end(); i != iend; ++i)
00340       os << (*i).first << " = " << (*i).second << endl;
00341   }
00342 
00343   if(d_counters.size() > 0) {
00344     os << endl << "*********** Counters ***********" << endl << endl;
00345     for(CounterMap::iterator
00346     i = d_counters.begin(), iend = d_counters.end(); i != iend; ++i)
00347       os << (*i).first << " = " << (*i).second << endl;
00348   }
00349 
00350   if(d_timers.size() > 0) {
00351     os << endl << "************ Timers ************" << endl << endl;
00352     for(TimerMap::iterator
00353     i = d_timers.begin(), iend = d_timers.end(); i != iend; ++i)
00354       os << (*i).first << " = " << *((*i).second) << endl;
00355   }
00356 
00357   os << endl
00358      << "********************************" << endl
00359      << "**** End of Debugging Info *****" << endl
00360      << "********************************" << endl;
00361 }
00362 
00363 // Global debugger.  It must be initialized in main() through its
00364 // init() method.
00365 Debug debugger;
00366 
00367 } // end of namespace CVC3
00368 
00369 #endif

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