CVC3  2.4.1
debug.cpp
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file debug.cpp
4  * \brief Description: Implementation of debugging facilities.
5  *
6  * Author: Sergey Berezin
7  *
8  * Created: Fri Jan 31 11:48:37 2003
9  *
10  * <hr>
11  *
12  * License to use, copy, modify, sell and/or distribute this software
13  * and its documentation for any purpose is hereby granted without
14  * royalty, subject to the terms and conditions defined in the \ref
15  * LICENSE file provided with this distribution.
16  *
17  * <hr>
18  *
19  */
20 /*****************************************************************************/
21 
22 #include <cstdlib>
23 #include <fstream>
24 #include <stdlib.h>
25 
26 #include "debug.h"
27 
28 using namespace std;
29 
30 namespace CVC3 {
31 
32 // Function for fatal exit. It just exits with code 1, but is
33 // provided here for the debugger to set a breakpoint to. For this
34 // reason, it is not inlined.
35 CVC_DLL void fatalError(const std::string& file, int line,
36  const std::string& cond, const std::string& msg) {
37  cerr << "\n**** Fatal error in " << file << ":" << line
38  << " (" << cond << ")\n" << msg << endl << flush;
39  exit(1);
40 }
41 
42 } // end of namespace CVC3
43 
44 #ifdef _CVC3_DEBUG_MODE
45 
46 #include <ctime>
47 #include <iomanip>
48 
49 namespace CVC3 {
50 // Similar to fatalError to raise an exception when DebugAssert fires.
51 // This does not necessarily cause the program to quit.
52 CVC_DLL void debugError(const std::string& file, int line,
53  const std::string& cond, const std::string& msg) {
54  ostringstream ss;
55  ss << "in " << file << ":" << line << " (" << cond << ")\n" << msg;
56  throw DebugException(ss.str());
57 }
58 
59 
60 class DebugTime {
61 public:
62  clock_t d_clock;
63 
64  // Constructors
65  DebugTime() {
66  d_clock = 0;
67  }
68  DebugTime(const clock_t& clock): d_clock(clock) { }
69 
70  // Set time to zero
71  void reset() {
72  d_clock = 0;
73  }
74 
75  // Incremental assignments
76  DebugTime& operator+=(const DebugTime& t) {
77  d_clock += t.d_clock;
78  return *this;
79  }
80  DebugTime& operator-=(const DebugTime& t) {
81  d_clock -= t.d_clock;
82  return *this;
83  }
84 
85  friend bool operator==(const DebugTime& t1, const DebugTime& t2);
86  friend bool operator!=(const DebugTime& t1, const DebugTime& t2);
87 
88  friend bool operator<(const DebugTime& t1, const DebugTime& t2);
89  friend bool operator>(const DebugTime& t1, const DebugTime& t2);
90  friend bool operator<=(const DebugTime& t1, const DebugTime& t2);
91  friend bool operator>=(const DebugTime& t1, const DebugTime& t2);
92 
93  friend ostream& operator<<(ostream& os, const DebugTime& t);
94 };
95 
96 DebugTime operator+(const DebugTime& t1, const DebugTime& t2) {
97  DebugTime res(t1);
98  res += t2;
99  return res;
100 }
101 DebugTime operator-(const DebugTime& t1, const DebugTime& t2) {
102  DebugTime res(t1);
103  res -= t2;
104  return res;
105 }
106 
107 bool operator==(const DebugTime& t1, const DebugTime& t2) {
108  return t1.d_clock == t2.d_clock;
109 }
110 
111 bool operator!=(const DebugTime& t1, const DebugTime& t2) {
112  return !(t1 == t2);
113 }
114 
115 bool operator<(const DebugTime& t1, const DebugTime& t2) {
116  return t1.d_clock < t2.d_clock;
117 }
118 
119 bool operator>(const DebugTime& t1, const DebugTime& t2) {
120  return t1.d_clock > t2.d_clock;
121 }
122 
123 bool operator<=(const DebugTime& t1, const DebugTime& t2) {
124  return t1.d_clock <= t2.d_clock;
125 }
126 
127 bool operator>=(const DebugTime& t1, const DebugTime& t2) {
128  return t1.d_clock >= t2.d_clock;
129 }
130 
131 ////////////////////////////////////////////////////////////////////////
132 // Class DebugTimer
133 ////////////////////////////////////////////////////////////////////////
134 
135 // Destructor
136 DebugTimer::~DebugTimer() {
137  if(d_clean_time)
138  delete d_time;
139 }
140 
141 void Debug::init(const std::vector<std::pair<std::string,bool> >* traceOptions,
142  const std::string* dumpName)
143 {
144  d_traceOptions = traceOptions;
145  d_dumpName = dumpName;
146 }
147 
148 void Debug::finalize()
149 {
150  d_traceOptions = NULL;
151  d_dumpName = NULL;
152 }
153 
154 DebugFlag
155 Debug::traceFlag(const char* name) { return traceFlag(std::string(name)); }
156 
157 void
158 Debug::traceAll(bool enable) { traceFlag("ALL") = enable; }
159 
160 // Copy constructor: copy the *pointer* from public timers, and
161 // value from private. The reason is, when you modify a public
162 // timer, you want the changes to show in the central database and
163 // everywhere else, whereas private timers are used as independent
164 // temporary variables holding intermediate time values.
165 DebugTimer::DebugTimer(const DebugTimer& timer) {
166  d_clean_time = timer.d_clean_time;
167  if(d_clean_time) {
168  // We are copying a private timer; make our own copy
169  d_time = new DebugTime(*timer.d_time);
170  d_clean_time = true;
171  } else {
172  // This is a public timer; just grab the pointer
173  d_time = timer.d_time;
174  }
175 }
176 // Assignment: same logistics as for the copy constructor, but need
177 // to take care of our own pointer
178 DebugTimer& DebugTimer::operator=(const DebugTimer& timer) {
179  // Check for self-assignment
180  if(&timer == this) return *this;
181 
182  if(timer.d_clean_time) {
183  // We are copying a private timer
184  if(d_clean_time) // We already have a private pointer, reuse it
185  *d_time = *timer.d_time;
186  else { // Create a new storage
187  d_time = new DebugTime(*timer.d_time);
188  d_clean_time = true;
189  }
190  } else {
191  // This is a public timer
192  if(d_clean_time) // We own our pointer, clean it up first
193  delete d_time;
194  d_time = timer.d_time;
195  d_clean_time = false;
196  }
197  return *this;
198 }
199 
200 void DebugTimer::reset() {
201  d_time->reset();
202 }
203 
204 DebugTimer& DebugTimer::operator+=(const DebugTimer& timer) {
205  (*d_time) += *(timer.d_time);
206  return *this;
207 }
208 
209 DebugTimer& DebugTimer::operator-=(const DebugTimer& timer) {
210  (*d_time) -= *(timer.d_time);
211  return *this;
212 }
213 
214 // These will produce new "private" timers
215 DebugTimer DebugTimer::operator+(const DebugTimer& timer) {
216  return DebugTimer(new DebugTime((*d_time) + (*timer.d_time)),
217  true /* take the new DebugTime */);
218 }
219 
220 DebugTimer DebugTimer::operator-(const DebugTimer& timer) {
221  return DebugTimer(new DebugTime((*d_time) - (*timer.d_time)),
222  true /* take the new DebugTime */);
223 }
224 
225 // Comparisons
226 bool operator==(const DebugTimer& t1, const DebugTimer& t2) {
227  return(*t1.d_time == *t2.d_time);
228 }
229 bool operator!=(const DebugTimer& t1, const DebugTimer& t2) {
230  return(*t1.d_time != *t2.d_time);
231 }
232 bool operator<(const DebugTimer& t1, const DebugTimer& t2) {
233  return *t1.d_time < *t2.d_time;
234 }
235 bool operator>(const DebugTimer& t1, const DebugTimer& t2) {
236  return *t1.d_time > *t2.d_time;
237 }
238 bool operator<=(const DebugTimer& t1, const DebugTimer& t2) {
239  return *t1.d_time <= *t2.d_time;
240 }
241 bool operator>=(const DebugTimer& t1, const DebugTimer& t2) {
242  return *t1.d_time >= *t2.d_time;
243 }
244 
245 // Print the time and timer's values
246 ostream& operator<<(ostream& os, const DebugTime& t) {
247  int seconds = (int)(t.d_clock / CLOCKS_PER_SEC);
248  int milliseconds = 1000 * int((((double)(t.d_clock % CLOCKS_PER_SEC)) / CLOCKS_PER_SEC));
249  os << seconds << "." << setfill('0') << setw(6) << milliseconds;
250  return os;
251 }
252 ostream& operator<<(ostream& os, const DebugTimer& timer) {
253  return(os << *timer.d_time);
254 }
255 
256 ////////////////////////////////////////////////////////////////////////
257 // Class Debug
258 ////////////////////////////////////////////////////////////////////////
259 
260 // Destructor: destroy all the pointers in d_timers
261 Debug::~Debug() {
262  TimerMap::iterator i, iend;
263  for(i = d_timers.begin(), iend = d_timers.end(); i != iend; ++i)
264  delete (*i).second;
265  if(d_osDumpTrace != NULL)
266  delete d_osDumpTrace;
267 }
268 
269 bool
270 Debug::trace(const string& name) {
271  // First, check if this flag was set in the command line. Walk the
272  // vector backwards, so that the last +/-trace takes effect.
273  if(d_traceOptions != NULL) {
274  vector<pair<string,bool> >::const_reverse_iterator i, iend;
275  for(i=d_traceOptions->rbegin(), iend=d_traceOptions->rend(); i!=iend; ++i)
276  if((*i).first == name || (*i).first == "ALL") return (*i).second;
277  }
278  return traceFlag(name) || traceFlag("ALL");
279 }
280 
281 
282 DebugTimer Debug::timer(const string& name) {
283  // See if we already have the timer
284  if(d_timers.count(name) > 0) return(DebugTimer(d_timers[name]));
285  else {
286  // Create a new timer
287  DebugTime *t = new DebugTime();
288  d_timers[name] = t;
289  return DebugTimer(t);
290  }
291 }
292 
293 DebugTimer Debug::newTimer() {
294  return DebugTimer(new DebugTime(), true /* take the pointer */);
295 }
296 
297 void Debug::setCurrentTime(DebugTimer& timer) {
298  *timer.d_time = clock();
299 }
300 
301 // Set the timer to the difference between current time and the
302 // time stored in the timer: timer = currentTime - timer.
303 // Intended to obtain the time interval since the last call to
304 // setCurrentTime() with that timer.
305 void Debug::setElapsed(DebugTimer& timer) {
306  *timer.d_time -= DebugTime(clock());
307 }
308 
309 /*! If the stream is not initialized, open the file
310  * If the filename is empty or "-", then return
311  * cout (but do not initialize the stream in this case).
312  */
313 
314 ostream& Debug::getOSDumpTrace() {
315  if(d_osDumpTrace != NULL) return *d_osDumpTrace;
316  // Check if the flag has a file name in it
317  if(*d_dumpName == "" || *d_dumpName == "-") return cout;
318  d_osDumpTrace = new ofstream(d_dumpName->c_str());
319  return *d_osDumpTrace;
320 }
321 
322 
323 // Print an entry to the dump-sat file: free-form message
324 void Debug::dumpTrace(const std::string& title,
325  const std::vector<std::pair<std::string,std::string> >& fields) {
326  ostream& os = getOSDumpTrace();
327  os << "[" << title << "]\n";
328  for(size_t i=0, iend=fields.size(); i<iend; ++i)
329  os << fields[i].first << " = " << fields[i].second << "\n";
330  os << endl;
331 }
332 
333 
334 // Print all the collected data if "DEBUG" flag is set
335 void Debug::printAll(ostream& os) {
336  if(!trace("DEBUG")) return;
337  // Flags
338  os << endl
339  << "********************************" << endl
340  << "******* Debugging Info *********" << endl
341  << "********************************" << endl;
342 
343  if(d_flags.size() > 0) {
344  os << endl << "************ Flags *************" << endl << endl;
345  for(FlagMap::iterator
346  i = d_flags.begin(), iend = d_flags.end(); i != iend; ++i)
347  os << (*i).first << " = " << (*i).second << endl;
348  }
349 
350  if(d_counters.size() > 0) {
351  os << endl << "*********** Counters ***********" << endl << endl;
352  for(CounterMap::iterator
353  i = d_counters.begin(), iend = d_counters.end(); i != iend; ++i)
354  os << (*i).first << " = " << (*i).second << endl;
355  }
356 
357  if(d_timers.size() > 0) {
358  os << endl << "************ Timers ************" << endl << endl;
359  for(TimerMap::iterator
360  i = d_timers.begin(), iend = d_timers.end(); i != iend; ++i)
361  os << (*i).first << " = " << *((*i).second) << endl;
362  }
363 
364  os << endl
365  << "********************************" << endl
366  << "**** End of Debugging Info *****" << endl
367  << "********************************" << endl;
368 }
369 
370 // Global debugger. It must be initialized in main() through its
371 // init() method.
372 CVC_DLL Debug debugger;
373 
374 } // end of namespace CVC3
375 
376 #endif