diff options
| -rw-r--r-- | Makefile.am | 6 | ||||
| -rw-r--r-- | Makefile.builds.in | 4 | ||||
| -rw-r--r-- | configure.ac | 2 | ||||
| -rw-r--r-- | src/util/stats.h | 215 | ||||
| -rw-r--r-- | test/Makefile.am | 8 | ||||
| -rw-r--r-- | test/regress/Makefile.am | 4 | ||||
| -rw-r--r-- | test/system/Makefile.am | 10 | ||||
| -rw-r--r-- | test/unit/Makefile.am | 15 | ||||
| -rw-r--r-- | test/unit/util/stats_black.h | 103 |
9 files changed, 298 insertions, 69 deletions
diff --git a/Makefile.am b/Makefile.am index 35744e381..aa2d5fdcf 100644 --- a/Makefile.am +++ b/Makefile.am @@ -7,8 +7,10 @@ ACLOCAL_AMFLAGS = -I config SUBDIRS = src test contrib -.PHONY: regress0 regress1 regress2 regress3 -regress0 regress1 regress2 regress3: all +.PHONY: units regress regress0 regress1 regress2 regress3 +regress regress0 regress1 regress2 regress3: all + (cd test && $(MAKE) $(AM_MAKEFLAGS) $@) || exit 1 +units: all (cd test && $(MAKE) $(AM_MAKEFLAGS) $@) || exit 1 LCOV = lcov diff --git a/Makefile.builds.in b/Makefile.builds.in index 5e5beb960..3f5b93b03 100644 --- a/Makefile.builds.in +++ b/Makefile.builds.in @@ -86,7 +86,9 @@ endif test -e lib || ln -sfv ".$(libdir)" lib test -e bin || ln -sfv ".$(bindir)" bin -check regress regress0 regress1 regress2 regress3: all +check test units regress: all + (cd $(CURRENT_BUILD)/test && $(MAKE) $@) +regress%: all (cd $(CURRENT_BUILD)/test && $(MAKE) $@) # any other target than the default doesn't do the extra stuff above diff --git a/configure.ac b/configure.ac index 939ad53a2..d369cbde5 100644 --- a/configure.ac +++ b/configure.ac @@ -636,6 +636,8 @@ fi AC_CHECK_LIB(z, gzread, , [AC_MSG_ERROR([zlib required, install your distro's zlib-dev package or see www.zlib.net])]) AC_CHECK_HEADER(zlib.h, , [AC_MSG_ERROR([zlib required, install your distro's zlib-dev package or see www.zlib.net])]) +AC_CHECK_LIB(rt, clock_gettime, , [AC_MSG_ERROR([can't find clock_gettime() in librt])]) + # Check for antlr C++ runtime (defined in config/antlr.m4) AC_LIB_ANTLR diff --git a/src/util/stats.h b/src/util/stats.h index f917e8b52..74afb5792 100644 --- a/src/util/stats.h +++ b/src/util/stats.h @@ -24,16 +24,19 @@ #include <string> #include <ostream> +#include <iomanip> #include <set> +#include <ctime> + #include "util/Assert.h" namespace CVC4 { #ifdef CVC4_STATISTICS_ON -# define USE_STATISTICS true +# define __CVC4_USE_STATISTICS true #else -# define USE_STATISTICS false +# define __CVC4_USE_STATISTICS false #endif class CVC4_PUBLIC Stat; @@ -48,8 +51,8 @@ private: public: static void flushStatistics(std::ostream& out); - static inline void registerStat(Stat* s) throw (AssertionException); - static inline void unregisterStat(Stat* s) throw (AssertionException); + static inline void registerStat(Stat* s) throw(AssertionException); + static inline void unregisterStat(Stat* s) throw(AssertionException); };/* class StatisticsRegistry */ @@ -61,9 +64,9 @@ private: public: - Stat(const std::string& s) throw (CVC4::AssertionException) : d_name(s) + Stat(const std::string& s) throw(CVC4::AssertionException) : d_name(s) { - if(USE_STATISTICS){ + if(__CVC4_USE_STATISTICS) { AlwaysAssert(d_name.find(s_delim) == std::string::npos); } } @@ -71,8 +74,8 @@ public: virtual void flushInformation(std::ostream& out) const = 0; - void flushStat(std::ostream& out) const{ - if(USE_STATISTICS){ + void flushStat(std::ostream& out) const { + if(__CVC4_USE_STATISTICS) { out << d_name << s_delim; flushInformation(out); } @@ -81,27 +84,31 @@ public: const std::string& getName() const { return d_name; } -}; +};/* class Stat */ + struct StatisticsRegistry::StatCmp { bool operator()(const Stat* s1, const Stat* s2) const { return (s1->getName()) < (s2->getName()); } -}; +};/* class StatCmp */ + -inline void StatisticsRegistry::registerStat(Stat* s) throw (AssertionException){ - if(USE_STATISTICS){ +inline void StatisticsRegistry::registerStat(Stat* s) throw(AssertionException) { + if(__CVC4_USE_STATISTICS) { AlwaysAssert(d_registeredStats.find(s) == d_registeredStats.end()); d_registeredStats.insert(s); } -} -inline void StatisticsRegistry::unregisterStat(Stat* s) throw (AssertionException){ - if(USE_STATISTICS){ +}/* StatisticsRegistry::registerStat */ + + +inline void StatisticsRegistry::unregisterStat(Stat* s) throw(AssertionException) { + if(__CVC4_USE_STATISTICS) { AlwaysAssert(d_registeredStats.find(s) != d_registeredStats.end()); d_registeredStats.erase(s); } -} +}/* StatisticsRegistry::unregisterStat */ @@ -109,24 +116,25 @@ inline void StatisticsRegistry::unregisterStat(Stat* s) throw (AssertionExceptio * class T must have stream insertion operation defined. * std::ostream& operator<<(std::ostream&, const T&); */ -template<class T> -class DataStat : public Stat{ +template <class T> +class DataStat : public Stat { public: DataStat(const std::string& s) : Stat(s) {} virtual const T& getData() const = 0; virtual void setData(const T&) = 0; - void flushInformation(std::ostream& out) const{ - if(USE_STATISTICS){ + void flushInformation(std::ostream& out) const { + if(__CVC4_USE_STATISTICS) { out << getData(); } } -}; +};/* class DataStat */ + /** T must have an assignment operator=(). */ template <class T> -class ReferenceStat: public DataStat<T>{ +class ReferenceStat : public DataStat<T> { private: const T* d_data; @@ -136,28 +144,29 @@ public: {} ReferenceStat(const std::string& s, const T& data): - DataStat<T>(s),d_data(NULL) + DataStat<T>(s), d_data(NULL) { setData(data); } - void setData(const T& t){ - if(USE_STATISTICS){ + void setData(const T& t) { + if(__CVC4_USE_STATISTICS) { d_data = &t; } } - const T& getData() const{ - if(USE_STATISTICS){ + const T& getData() const { + if(__CVC4_USE_STATISTICS) { return *d_data; - }else{ + } else { Unreachable(); } } -}; +};/* class ReferenceStat */ + /** T must have an operator=() and a copy constructor. */ template <class T> -class BackedStat: public DataStat<T>{ +class BackedStat : public DataStat<T> { protected: T d_data; @@ -167,65 +176,171 @@ public: {} void setData(const T& t) { - if(USE_STATISTICS){ + if(__CVC4_USE_STATISTICS) { d_data = t; } } - BackedStat<T>& operator=(const T& t){ - if(USE_STATISTICS){ + BackedStat<T>& operator=(const T& t) { + if(__CVC4_USE_STATISTICS) { d_data = t; } return *this; } - const T& getData() const{ - if(USE_STATISTICS){ + const T& getData() const { + if(__CVC4_USE_STATISTICS) { return d_data; - }else{ + } else { Unreachable(); } } -}; +};/* class BackedStat */ + -class IntStat : public BackedStat<int64_t>{ +class IntStat : public BackedStat<int64_t> { public: IntStat(const std::string& s, int64_t init): BackedStat<int64_t>(s, init) {} - IntStat& operator++(){ - if(USE_STATISTICS){ + IntStat& operator++() { + if(__CVC4_USE_STATISTICS) { ++d_data; } return *this; } - IntStat& operator+=(int64_t val){ - if(USE_STATISTICS){ + IntStat& operator+=(int64_t val) { + if(__CVC4_USE_STATISTICS) { d_data+= val; } return *this; } - void maxAssign(int64_t val){ - if(USE_STATISTICS){ - if(d_data < val){ + void maxAssign(int64_t val) { + if(__CVC4_USE_STATISTICS) { + if(d_data < val) { d_data = val; } } } - void minAssign(int64_t val){ - if(USE_STATISTICS){ - if(d_data > val){ + void minAssign(int64_t val) { + if(__CVC4_USE_STATISTICS) { + if(d_data > val) { d_data = val; } } } -}; +};/* class IntStat */ + + +// some utility functions for ::timespec +inline ::timespec& operator+=(::timespec& a, const ::timespec& b) { + // assumes a.tv_nsec and b.tv_nsec are in range + const long nsec_per_sec = 1000000000L; // one thousand million + a.tv_sec += b.tv_sec; + long nsec = a.tv_nsec + b.tv_nsec; + while(nsec < 0) { + nsec += nsec_per_sec; + ++a.tv_sec; + } + while(nsec >= nsec_per_sec) { + nsec -= nsec_per_sec; + --a.tv_sec; + } + a.tv_nsec = nsec; + return a; +} +inline ::timespec& operator-=(::timespec& a, const ::timespec& b) { + // assumes a.tv_nsec and b.tv_nsec are in range + const long nsec_per_sec = 1000000000L; // one thousand million + a.tv_sec -= b.tv_sec; + long nsec = a.tv_nsec - b.tv_nsec; + while(nsec < 0) { + nsec += nsec_per_sec; + ++a.tv_sec; + } + while(nsec >= nsec_per_sec) { + nsec -= nsec_per_sec; + --a.tv_sec; + } + a.tv_nsec = nsec; + return a; +} +inline ::timespec operator+(const ::timespec& a, const ::timespec& b) { + ::timespec result = a; + return result += b; +} +inline ::timespec operator-(const ::timespec& a, const ::timespec& b) { + ::timespec result = a; + return result -= b; +} +inline bool operator==(const ::timespec& a, const ::timespec& b) { + // assumes a.tv_nsec and b.tv_nsec are in range + return a.tv_sec == b.tv_sec && a.tv_nsec == b.tv_nsec; +} +inline bool operator!=(const ::timespec& a, const ::timespec& b) { + // assumes a.tv_nsec and b.tv_nsec are in range + return !(a == b); +} +inline bool operator<(const ::timespec& a, const ::timespec& b) { + // assumes a.tv_nsec and b.tv_nsec are in range + return a.tv_sec < b.tv_sec || + (a.tv_sec == b.tv_sec && a.tv_nsec < b.tv_nsec); +} +inline bool operator>(const ::timespec& a, const ::timespec& b) { + // assumes a.tv_nsec and b.tv_nsec are in range + return a.tv_sec > b.tv_sec || + (a.tv_sec == b.tv_sec && a.tv_nsec > b.tv_nsec); +} +inline bool operator<=(const ::timespec& a, const ::timespec& b) { + // assumes a.tv_nsec and b.tv_nsec are in range + return !(a > b); +} +inline bool operator>=(const ::timespec& a, const ::timespec& b) { + // assumes a.tv_nsec and b.tv_nsec are in range + return !(a < b); +} +inline std::ostream& operator<<(std::ostream& os, const ::timespec& t) { + // assumes t.tv_nsec is in range + return os << t.tv_sec << "." + << std::setfill('0') << std::setw(8) << std::right << t.tv_nsec; +} + + +class TimerStat : public BackedStat< ::timespec > { + // strange: timespec isn't placed in 'std' namespace ?! + ::timespec d_start; + bool d_running; + +public: + + TimerStat(const std::string& s) : + BackedStat< ::timespec >(s, ::timespec()), + d_running(false) { + } + + void start() { + if(__CVC4_USE_STATISTICS) { + AlwaysAssert(!d_running); + clock_gettime(CLOCK_REALTIME, &d_start); + } + } + + void stop() { + if(__CVC4_USE_STATISTICS) { + AlwaysAssert(d_running); + ::timespec end; + clock_gettime(CLOCK_REALTIME, &end); + d_data += end - d_start; + } + } +};/* class TimerStat */ + -#undef USE_STATISTICS +#undef __CVC4_USE_STATISTICS }/* CVC4 namespace */ diff --git a/test/Makefile.am b/test/Makefile.am index 501f85090..045599bc1 100644 --- a/test/Makefile.am +++ b/test/Makefile.am @@ -2,8 +2,8 @@ SUBDIRS = unit system regress . MAKEFLAGS = -k -.PHONY: regress0 regress1 regress2 regress3 -regress0 regress1 regress2 regress3: +.PHONY: units regress regress0 regress1 regress2 regress3 +units regress regress0 regress1 regress2 regress3: @$(MAKE) check-pre; \ for dir in $(SUBDIRS); do \ test $$dir = . || (cd $$dir && $(MAKE) $(AM_MAKEFLAGS) $@); \ @@ -11,8 +11,8 @@ regress0 regress1 regress2 regress3: $(MAKE) check-local # synonyms for "check" -.PHONY: regress test -regress test: check +.PHONY: test +test: check am__tty_colors = \ red=; grn=; lgn=; blu=; std=; \ diff --git a/test/regress/Makefile.am b/test/regress/Makefile.am index 80e8da387..3867ee860 100644 --- a/test/regress/Makefile.am +++ b/test/regress/Makefile.am @@ -16,6 +16,10 @@ regress0 regress1 regress2 regress3: .PHONY: regress test regress test: check +# no-ops here +.PHONY: units +units: + EXTRA_DIST = \ run_regression \ README diff --git a/test/system/Makefile.am b/test/system/Makefile.am index 219a26355..954798e6c 100644 --- a/test/system/Makefile.am +++ b/test/system/Makefile.am @@ -39,9 +39,9 @@ $(TESTS):: $(TEST_DEPS) export VERBOSE = 1 # synonyms for "check" -.PHONY: regress test -regress test: check +.PHONY: test +test: check -# in system test dir, regressN are also synonyms for check -.PHONY: regress0 regress1 regress2 regress3 -regress0 regress1 regress2 regress3: check +# no-ops here +.PHONY: units regress regress0 regress1 regress2 regress3s +units regress regress0 regress1 regress2 regress3: diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index eb920e6c5..1272be069 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -35,7 +35,8 @@ UNIT_TESTS = \ util/integer_black \ util/integer_white \ util/rational_black \ - util/rational_white + util/rational_white \ + util/stats_black export VERBOSE = 1 @@ -52,7 +53,7 @@ AM_CPPFLAGS = \ "-I@top_srcdir@/src" "-I@top_builddir@/src" \ "-I@top_srcdir@/src/prop/minisat" \ -D __STDC_LIMIT_MACROS \ - -D __STDC_FORMAT_MACROS \ + -D __STDC_FORMAT_MACROS \ $(ANTLR_INCLUDES) $(TEST_CPPFLAGS) AM_CXXFLAGS = -Wall -Wno-unknown-pragmas -Wno-parentheses $(TEST_CXXFLAGS) AM_LDFLAGS = $(TEST_LDFLAGS) @@ -158,12 +159,12 @@ libdummy_la_LIBADD = @abs_top_builddir@/src/libcvc4.la endif # synonyms for "check" -.PHONY: regress test -regress test: check +.PHONY: units test +units test: check -# in unit test dir, regressN are also synonyms for check -.PHONY: regress0 regress1 regress2 regress3 -regress0 regress1 regress2 regress3: check +# no-ops here +.PHONY: regress regress0 regress1 regress2 regress3 +regress regress0 regress1 regress2 regress3: if HAVE_CXXTESTGEN # all is fine with the world diff --git a/test/unit/util/stats_black.h b/test/unit/util/stats_black.h new file mode 100644 index 000000000..032efc37a --- /dev/null +++ b/test/unit/util/stats_black.h @@ -0,0 +1,103 @@ +/********************* */ +/*! \file stats_black.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Black box testing of CVC4::Stat and associated classes + ** + ** Black box testing of CVC4::Stat and associated classes. + **/ + +#include <cxxtest/TestSuite.h> +#include <sstream> +#include <string> +#include <ctime> + +#include "util/stats.h" + +using namespace CVC4; +using namespace std; + +class StatsBlack : public CxxTest::TestSuite { +public: + + void testStats() { + + // StatisticsRegistry + //static void flushStatistics(std::ostream& out); + + //static inline void registerStat(Stat* s) throw (AssertionException); + //static inline void unregisterStat(Stat* s) throw (AssertionException); + + string empty, bar = "bar", baz = "baz"; + ReferenceStat<string> refStr("stat #1", empty); + ReferenceStat<string> refStr2("refStr2", bar); + // setData + // getData + + // flushInformation + // flushStat + + BackedStat<string> backedStr("backed", baz); + // setData + // getData + // operator= + + IntStat sInt("my int", 10); + TimerStat sTimer("a timer ! for measuring time"); + + TS_ASSERT_EQUALS(refStr.getName(), "stat #1"); + TS_ASSERT_EQUALS(refStr2.getName(), "refStr2"); + TS_ASSERT_EQUALS(backedStr.getName(), "backed"); + TS_ASSERT_EQUALS(sInt.getName(), "my int"); + TS_ASSERT_EQUALS(sTimer.getName(), "a timer ! for measuring time"); + + TS_ASSERT_EQUALS(refStr.getData(), empty); + TS_ASSERT_EQUALS(refStr2.getData(), bar); + empty = "a different string"; + bar += " and with an addition"; + TS_ASSERT_EQUALS(refStr.getData(), empty); + TS_ASSERT_EQUALS(refStr2.getData(), bar); + + TS_ASSERT_EQUALS(backedStr.getData(), "baz"); + baz = "something else"; + TS_ASSERT_EQUALS(backedStr.getData(), "baz"); + + TS_ASSERT_EQUALS(sInt.getData(), 10); + sInt.setData(100); + TS_ASSERT_EQUALS(sInt.getData(), 100); + + TS_ASSERT_EQUALS(sTimer.getData(), timespec()); + + stringstream sstr; + + refStr.flushInformation(sstr); + TS_ASSERT_EQUALS(sstr.str(), empty); + sstr.str(""); + refStr2.flushInformation(sstr); + TS_ASSERT_EQUALS(sstr.str(), bar); + sstr.str(""); + backedStr.flushInformation(sstr); + TS_ASSERT_EQUALS(sstr.str(), "baz"); + sstr.str(""); + sInt.flushInformation(sstr); + TS_ASSERT_EQUALS(sstr.str(), "100"); + sstr.str(""); + sTimer.flushInformation(sstr); + TS_ASSERT_EQUALS(sstr.str(), "0.00000000"); + + sTimer.start(); + TS_ASSERT_EQUALS(timespec(), sTimer.getData()); + sTimer.stop(); + TS_ASSERT_LESS_THAN(timespec(), sTimer.getData()); + } + +}; |