/*****************************************************************************/
/*!
* \file debug.h
* \brief Description: Collection of debugging macros and functions.
*
* Author: Sergey Berezin
*
* Created: Thu Dec 5 13:12:59 2002
*
* <hr>
*
* License to use, copy, modify, sell and/or distribute this software
* and its documentation for any purpose is hereby granted without
* royalty, subject to the terms and conditions defined in the \ref
* LICENSE file provided with this distribution.
*
* <hr>
*
*/
/*****************************************************************************/
#ifndef _cvc3__debug_h
#define _cvc3__debug_h
#include <string>
#include <iostream>
#include <sstream>
#include <vector>
#include "os.h"
#include "exception.h"
/*! @brief If something goes horribly wrong, print a message and abort
immediately with exit(1). */
/*! This macro stays even in the non-debug build, so the end users can
send us meaningful bug reports. */
#define FatalAssert(cond, msg) if(!(cond)) \
CVC3::fatalError(__FILE__, __LINE__, #cond, msg)
namespace CVC3 {
//! Function for fatal exit.
/*! It just exits with code 1, but is provided here for the debugger
to set a breakpoint to. For this reason, it is not inlined. */
extern void fatalError(const std::string& file, int line,
const std::string& cond, const std::string& msg);
}
#ifdef DEBUG
#include "compat_hash_map.h"
#include "compat_hash_set.h"
//! Any debugging code must be within IF_DEBUG(...)
#define IF_DEBUG(code) code
//! Print a value conditionally.
/*! If 'cond' is true, print 'pre', then 'v', then 'post'. The type
of v must have overloaded operator<<. It expects a ';' after it. */
#define DBG_PRINT(cond, pre, v, post) if(cond) CVC3::debugger.getOS() \
<< (pre) << (v) << (post) << std::endl
//! Print a message conditionally
#define DBG_PRINT_MSG(cond, msg) \
if(cond) CVC3::debugger.getOS() << (msg) << std::endl
/*! @brief Same as DBG_PRINT, only takes a flag name instead of a
general condition */
#define TRACE(flag, pre, v, post) \
DBG_PRINT(CVC3::debugger.trace(flag), pre, v, post)
//! Same as TRACE, but for a simple message
#define TRACE_MSG(flag, msg) \
DBG_PRINT_MSG(CVC3::debugger.trace(flag), msg)
//! Sanity check for debug build. It disappears in the production code.
#define DebugAssert(cond, str) if(!(cond)) \
CVC3::debugError(__FILE__, __LINE__, #cond, str)
namespace CVC3 {
/*! @brief A class which sets a boolean value to true when created,
* and resets to false when deleted.
*
* Useful for tracking when the control is within a certain method or
* not. For example, TheoryCore::addFact() uses d_inAddFact to check
* that certain other methods are only called from within addFact().
* However, when an exception is thrown, this variable is not reset.
* The watcher class will reset the variable even in those cases.
*/
class ScopeWatcher {
private:
bool *d_flag;
public:
ScopeWatcher(bool *flag): d_flag(flag) { *d_flag = true; }
~ScopeWatcher() { *d_flag = false; }
};
class Expr;
//! Our exception to throw
class DebugException: public Exception {
public:
// Constructor
DebugException(const std::string& msg): Exception(msg) { }
// Printing
virtual std::string toString() const {
return "Assertion violation " + d_msg;
}
}; // end of class DebugException
//! Similar to fatalError to raise an exception when DebugAssert fires.
/*! This does not necessarily cause the program to quit. */
extern void debugError(const std::string& file, int line,
const std::string& cond, const std::string& msg);
// First, wrapper classes for flags, counters, and timers. Later,
// we overload some operators like '=', '++', etc. for those
// classes.
//! Boolean flag (can only be true or false)
class DebugFlag {
private:
bool* d_flag; // We don't own the pointer
public:
// Constructor: takes the pointer to the actual flag, normally
// stored in class Debug below.
DebugFlag(bool& flag) : d_flag(&flag) { }
// Destructor
~DebugFlag() { }
// Auto-cast to boolean
operator bool() { return *d_flag; }
// Setting and resetting by ++ and --
// Prefix versions:
bool operator--() { *d_flag = false; return false; }
bool operator++() { *d_flag = true; return true; }
// Postfix versions:
bool operator--(int) { bool x=*d_flag; *d_flag=false; return x; }
bool operator++(int) { bool x=*d_flag; *d_flag=true; return x; }
// Can be assigned only a boolean value
DebugFlag& operator=(bool x) { *d_flag=(x!=false); return *this; }
// Comparisons
friend bool operator==(const DebugFlag& f1, const DebugFlag& f2);
friend bool operator!=(const DebugFlag& f1, const DebugFlag& f2);
// Printing
friend std::ostream& operator<<(std::ostream& os, const DebugFlag& f);
}; // end of class DebugFlag
//! Checks if the *values* of the flags are equal
inline bool operator==(const DebugFlag& f1, const DebugFlag& f2) {
return (*f1.d_flag) == (*f2.d_flag);
}
//! Checks if the *values* of the flags are disequal
inline bool operator!=(const DebugFlag& f1, const DebugFlag& f2) {
return (*f1.d_flag) != (*f2.d_flag);
}
//! Printing flags
inline std::ostream& operator<<(std::ostream& os, const DebugFlag& f) {
if(*f.d_flag) return(os << "true");
else return(os << "false");
}
//! Integer counter for debugging purposes.
/*! Intended use is to count events (e.g. number of function calls),
but can be used to store any integer value (e.g. size of some data
structure) */
class DebugCounter {
private:
int* d_counter; //!< We don't own the pointer
public:
//! Constructor
/*! Takes the pointer to the actual counter, normally stored in
class Debug below. */
DebugCounter(int& c) : d_counter(&c) { }
//! Destructor
~DebugCounter() { }
//! Auto-cast to int.
/*! In particular, arithmetic comparisons like <, >, <=, >= will
work because of this. */
operator int() { return *d_counter; }
// Auto-increment operators
//! Prefix auto-decrement
int operator--() { return --(*d_counter); }
//! Prefix auto-increment
int operator++() { return ++(*d_counter); }
//! Postfix auto-decrement
int operator--(int) { return (*d_counter)--; }
//! Postfix auto-increment
int operator++(int) { return (*d_counter)++; }
//! Value assignment.
DebugCounter& operator=(int x) { *d_counter=x; return *this; }
DebugCounter& operator+=(int x) { *d_counter+=x; return *this; }
DebugCounter& operator-=(int x) { *d_counter-=x; return *this; }
//! Assignment from another counter.
/*! It copies the value, not the pointer */
DebugCounter& operator=(const DebugCounter& x)
{ *d_counter=*x.d_counter; return *this; }
/*! It copies the value, not the pointer */
DebugCounter& operator-=(const DebugCounter& x)
{ *d_counter-=*x.d_counter; return *this; }
/*! It copies the value, not the pointer */
DebugCounter& operator+=(const DebugCounter& x)
{ *d_counter+=*x.d_counter; return *this; }
// Comparisons to integers and other DebugCounters
friend bool operator==(const DebugCounter& c1, const DebugCounter& c2);
friend bool operator!=(const DebugCounter& c1, const DebugCounter& c2);
friend bool operator==(int c1, const DebugCounter& c2);
friend bool operator!=(int c1, const DebugCounter& c2);
friend bool operator==(const DebugCounter& c1, int c2);
friend bool operator!=(const DebugCounter& c1, int c2);
//! Printing counters
friend std::ostream& operator<<(std::ostream& os, const DebugCounter& f);
}; // end of class DebugCounter
inline bool operator==(const DebugCounter& c1, const DebugCounter& c2) {
return (*c1.d_counter) == (*c2.d_counter);
}
inline bool operator!=(const DebugCounter& c1, const DebugCounter& c2) {
return (*c1.d_counter) != (*c2.d_counter);
}
inline bool operator==(int c1, const DebugCounter& c2) {
return c1 == (*c2.d_counter);
}
inline bool operator!=(int c1, const DebugCounter& c2) {
return c1 != (*c2.d_counter);
}
inline bool operator==(const DebugCounter& c1, int c2) {
return (*c1.d_counter) == c2;
}
inline bool operator!=(const DebugCounter& c1, int c2) {
return (*c1.d_counter) != c2;
}
inline std::ostream& operator<<(std::ostream& os, const DebugCounter& c) {
return (os << *c.d_counter);
}
//! A class holding the time value.
/*! What exactly is time is not exposed. It can be the system's
struct timeval, or it can be the (subset of the) user/system/real
time tuple. */
class DebugTime;
//! Time counter.
/*! Intended use is to store time intervals or accumulated time for
multiple events (e.g. time spent to execute certain lines of code,
or accumulated time spent in a particular function). */
class DebugTimer {
private:
DebugTime* d_time; //!< The time value
bool d_clean_time; //!< Set if we own *d_time
public:
//! Constructor: takes the pointer to the actual time value.
/*! It is either stored in class Debug below (then the timer is
"public"), or we own it, making the timer "private". */
DebugTimer(DebugTime* time, bool take_time = false)
: d_time(time), d_clean_time(take_time) { }
/*! @brief Copy constructor: copy the *pointer* from public
timers, and *value* from private. */
/*! The reason for different behavior for public and private time
is the following. When you modify a public timer, you want the
changes to show in the central database and everywhere else,
whereas private timers are used as independent temporary
variables holding intermediate time values. */
DebugTimer(const DebugTimer& timer);
//! Assignment: same logistics as for the copy constructor
DebugTimer& operator=(const DebugTimer& timer);
//! Destructor
~DebugTimer();
// Operators
//! Set time to zero
void reset();
DebugTimer& operator+=(const DebugTimer& timer);
DebugTimer& operator-=(const DebugTimer& timer);
//! Produces new "private" timer
DebugTimer operator+(const DebugTimer& timer);
//! Produces new "private" timer
DebugTimer operator-(const DebugTimer& timer);
// Our friends
friend class Debug;
// Comparisons
friend bool operator==(const DebugTimer& t1, const DebugTimer& t2);
friend bool operator!=(const DebugTimer& t1, const DebugTimer& t2);
friend bool operator<(const DebugTimer& t1, const DebugTimer& t2);
friend bool operator>(const DebugTimer& t1, const DebugTimer& t2);
friend bool operator<=(const DebugTimer& t1, const DebugTimer& t2);
friend bool operator>=(const DebugTimer& t1, const DebugTimer& t2);
//! Print the timer's value
friend std::ostream& operator<<(std::ostream& os, const DebugTimer& timer);
}; // end of class DebugTimer
//! The heart of the Bug Extermination Kingdom.
/*! This class exposes many important components of the entire
CVC-lite system for use in debugging, keeps all the flags,
counters, and timers in the central database, and provides timing
and printing functions. */
class Debug {
private:
//! Command line options for tracing; these override the TRACE command
const std::vector<std::pair<std::string,bool> >* d_traceOptions;
//! name of dump file
const std::string* d_dumpName;
// Output control
std::ostream* d_os;
// Stream for dumping trace to file ("dump-trace" option)
std::ostream* d_osDumpTrace;
//! Private hasher class for strings
class stringHash {
public:
size_t operator()(const std::string& s) const {
std::hash<char*> h;
return h(s.c_str());
}
}; // end of stringHash
// Hash tables for storing flags, counters, and timers
typedef std::hash_map<std::string, bool, stringHash> FlagMap;
typedef std::hash_map<std::string, int, stringHash> CounterMap;
typedef std::hash_map<std::string, DebugTime*, stringHash> TimerMap;
FlagMap d_flags; //!< Set of flags
FlagMap d_traceFlags; //!< Set of trace flags
CounterMap d_counters; //!< Set of counters
/*! Note, that the d_timers map does *not* own the pointers; so
the objects in d_timers must be destroyed explicitly in our
destructor. */
TimerMap d_timers; //!< Set of timers
public:
//! Constructor
Debug(): d_traceOptions(NULL), d_os(&std::cerr), d_osDumpTrace(NULL) { }
//! Destructor (must destroy objects it d_timers)
~Debug();
//! Must be called before Debug class can be safely used
void init(const std::vector<std::pair<std::string,bool> >* traceOptions,
const std::string* dumpName);
//! Accessing flags by name.
/*! If a flag doesn't exist, it is created and initialized to
false. */
DebugFlag flag(const std::string& name)
{ return DebugFlag(d_flags[name]); }
//! Accessing tracing flags by name.
/*! If a flag doesn't exist, it is created and initialized to
false. */
DebugFlag traceFlag(const std::string& name)
{ return DebugFlag(d_traceFlags[name]); }
//! Accessing tracing flag by char* name (mostly for GDB)
DebugFlag traceFlag(char* name);
//! Set tracing of everything on (1) and off (0) [for use in GDB]
void traceAll(bool enable = true);
//! Accessing counters by name.
/*! If a counter doesn't exist, it is created and initialized to 0. */
DebugCounter counter(const std::string& name)
{ return DebugCounter(d_counters[name]); }
//! Accessing timers by name.
/*! If a timer doesn't exist, it is created and initialized to 0. */
DebugTimer timer(const std::string& name);
//! Check whether to print trace info for a particular flag.
/*! Trace flags are the same DebugFlag objects, but live in a
different namespace from the normal debug flags */
bool trace(const std::string& name);
// Timer functions
//! Create a new "private" timer, initially set to 0.
/*! The new timer will not be added to the set of timers, will not
have a name, and will not be printed by 'printAll()'. It is
intended to be used to measure time intervals which are later
added or assigned to the named timers. */
static DebugTimer newTimer();
//! Set the timer to the current time (whatever that means)
void setCurrentTime(DebugTimer& timer);
void setCurrentTime(const std::string& name) {
DebugTimer t(timer(name));
setCurrentTime(t);
}
/*! @brief Set the timer to the difference between current time
and the time stored in the timer: timer = currentTime -
timer. */
/*! Intended to obtain the time interval since the last call to
setCurrentTime() with that timer. */
void setElapsed(DebugTimer& timer);
//! Return the ostream used for debugging output
std::ostream& getOS() { return *d_os; }
//! Return the ostream for dumping trace
std::ostream& getOSDumpTrace();
//! Print an entry to the dump file
void dumpTrace(const std::string& title,
const std::vector<std::pair<std::string,std::string> >&
fields);
//! Set the debugging ostream
void setOS(std::ostream& os) { d_os = &os; }
//! Print all the collected data if "DEBUG" flag is set to 'os'
void printAll(std::ostream& os);
/*! @brief Print all the collected data if "DEBUG" flag is set to
the default debug stream */
void printAll() { printAll(*d_os); }
// Generally useful functions
//! Get the current scope level
int scopeLevel();
}; // end of class Debug
extern Debug debugger;
} // end of namespace CVC3
#else // if DEBUG is not defined
// All debugging macros are empty here
#define IF_DEBUG(code)
#define DebugAssert(cond, str)
#define DBG_PRINT(cond, pre, v, post)
#define TRACE(cond, pre, v, post)
#define DBG_PRINT_MSG(cond, msg)
#define TRACE_MSG(flag, msg)
// to make the CLI wrapper happy
namespace CVC3 {
class DebugException: public Exception { };
}
#endif // DEBUG
#include "cvc_util.h"
#endif // _cvc3__debug_h
syntax highlighted by Code2HTML, v. 0.9.1