CVC3
|
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