CVC3

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