From 7c83d004874a46efe36d58717f7a4d72553b3693 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Wed, 14 Apr 2010 06:21:26 +0000 Subject: [PATCH] * Better dependency tracking for unit test building and linking, and auto-generated headers (metakind.h etc.), so they don't have to be recompiled every time. This drastically improves build time when only small updates are made. * Added "memory.h" unit test header for checking out-of-memory conditions. cdlist_black uses it. * Added helpful output when you "make lcov" in a non-coverage-enabled build. * Removed strict aliasing warning when compiling metakind.h header with optimization on. * Removed const version of NodeBuilder::operator Node()---it was poorly performing, better to not permit it---and fixed the convenience builders to use the non-const version (re: code review #63) * Color-coded test output on capable terminals. * Fixed some warnings in unit tests. --- Makefile.am | 28 ++- configure.ac | 7 +- src/expr/Makefile.am | 39 +++-- src/expr/mkmetakind | 9 + src/expr/node_builder.h | 288 ++++--------------------------- src/theory/Makefile.am | 8 +- src/theory/Makefile.subdirs | 6 + test/unit/Makefile.am | 76 +++++--- test/unit/context/cdlist_black.h | 21 ++- test/unit/expr/attribute_black.h | 24 +-- test/unit/memory.h | 69 ++++++++ 11 files changed, 255 insertions(+), 320 deletions(-) create mode 100644 src/theory/Makefile.subdirs create mode 100644 test/unit/memory.h diff --git a/Makefile.am b/Makefile.am index 57e9e3af2..8488c4dec 100644 --- a/Makefile.am +++ b/Makefile.am @@ -19,10 +19,12 @@ LCOV_EXCLUDES = \ "/usr/include/*" \ "$(abs_top_builddir)/test/*" +.PHONY: lcov lcov-all lcov18 +if COVERAGE_ENABLED + # lcov 1.7 has some bugs that we have to work around (can't do # baseline measurement, merge between different test-names doesn't # work...) -.PHONY: lcov lcov: all $(LCOV) -z -d . $(MAKE) check -C test/unit @@ -34,10 +36,20 @@ lcov: all @find "@top_srcdir@/html" -name '*.func.html' | \ xargs perl -pi -e 's#()(.*)()#$$_=`c++filt "$$2"`;chomp;print "$$1$$_$$3\n";#e' +lcov-all: all + $(LCOV) -z -d . + $(MAKE) check -C test + $(LCOV) -c -d . -t cvc4_units -o cvc4-coverage-full.info + $(LCOV) -o cvc4-coverage.info -r cvc4-coverage-full.info $(LCOV_EXCLUDES) + mkdir -p "@top_srcdir@/html" + $(GENHTML) -o "@top_srcdir@/html" cvc4-coverage.info + @echo "De-mangling C++ symbols..." + @find "@top_srcdir@/html" -name '*.func.html' | \ + xargs perl -pi -e 's#()(.*)()#$$_=`c++filt "$$2"`;chomp;print "$$1$$_$$3\n";#e' + # when we get a working lcov, we can do better stats for # modules/test-types; unfortunately lcov 1.8 directory paths # are broken(?) or at least different than 1.7 -.PHONY: lcov18 lcov18: all @for testtype in public black white; do \ echo; echo "=== Collecting coverage data from $$testtype unit tests ==="; \ @@ -56,3 +68,15 @@ lcov18: all @echo "De-mangling C++ symbols..." @find "@top_srcdir@/html" -name '*.func.html' | \ xargs perl -ni -e 's,()(.*)(.*),$$_=`c++filt "$$2"`;chomp;print "$$1$$_$$3\n";,e || print' + +else + +lcov lcov-all lcov18: + @echo + @echo "Coverage is not enabled in this build." >&2 + @echo "Please run configure with --enable-coverage." >&2 + @echo + @false + +endif + diff --git a/configure.ac b/configure.ac index a44dc4b66..93f8f2ee5 100644 --- a/configure.ac +++ b/configure.ac @@ -165,7 +165,7 @@ elif test -e src/include/cvc4_public.h; then exitval=$? cd ../../.. if test $exitval -eq 0; then - cat >config.status <config.reconfig </dev/null || true + $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true $(AM_V_GEN)(@srcdir@/mkkind \ $< \ @srcdir@/builtin_kinds \ - `grep '^SUBDIRS = ' @top_srcdir@/src/theory/Makefile.in | cut -d' ' -f3- | tr ' ' "\n" | xargs -i__D__ echo @top_srcdir@/src/theory/__D__/kinds` \ + `cat @top_srcdir@/src/theory/.subdirs` \ > $@) || (rm -f $@ && exit 1) -@srcdir@/metakind.h: metakind_template.h mkmetakind builtin_kinds @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds +@srcdir@/metakind.h: metakind_template.h mkmetakind builtin_kinds @top_srcdir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds $(AM_V_at)chmod +x @srcdir@/mkmetakind - $(AM_V_at)mv -f $@ $@~ 2>/dev/null || true + $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true $(AM_V_GEN)(@srcdir@/mkmetakind \ $< \ @srcdir@/builtin_kinds \ - `grep '^SUBDIRS = ' @top_srcdir@/src/theory/Makefile.in | cut -d' ' -f3- | tr ' ' "\n" | xargs -i__D__ echo @top_srcdir@/src/theory/__D__/kinds` \ + `cat @top_srcdir@/src/theory/.subdirs` \ > $@) || (rm -f $@ && exit 1) -@srcdir@/expr.h: expr_template.h mkexpr builtin_kinds @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds +@srcdir@/expr.h: expr_template.h mkexpr builtin_kinds @top_srcdir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds $(AM_V_at)chmod +x @srcdir@/mkexpr - $(AM_V_at)mv -f $@ $@~ 2>/dev/null || true + $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true $(AM_V_GEN)(@srcdir@/mkexpr \ $< \ @srcdir@/builtin_kinds \ - `grep '^SUBDIRS = ' @top_srcdir@/src/theory/Makefile.in | cut -d' ' -f3- | tr ' ' "\n" | xargs -i__D__ echo @top_srcdir@/src/theory/__D__/kinds` \ + `cat @top_srcdir@/src/theory/.subdirs` \ > $@) || (rm -f $@ && exit 1) -@srcdir@/expr.cpp: expr_template.cpp mkexpr builtin_kinds @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds +@srcdir@/expr.cpp: expr_template.cpp mkexpr builtin_kinds @top_srcdir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds $(AM_V_at)chmod +x @srcdir@/mkexpr - $(AM_V_at)mv -f $@ $@~ 2>/dev/null || true + $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true $(AM_V_GEN)(@srcdir@/mkexpr \ $< \ @srcdir@/builtin_kinds \ - `grep '^SUBDIRS = ' @top_srcdir@/src/theory/Makefile.in | cut -d' ' -f3- | tr ' ' "\n" | xargs -i__D__ echo @top_srcdir@/src/theory/__D__/kinds` \ + `cat @top_srcdir@/src/theory/.subdirs` \ > $@) || (rm -f $@ && exit 1) -@srcdir@/expr_manager.h: expr_manager_template.h mkexpr builtin_kinds @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds +@srcdir@/expr_manager.h: expr_manager_template.h mkexpr builtin_kinds @top_srcdir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds $(AM_V_at)chmod +x @srcdir@/mkexpr - $(AM_V_at)mv -f $@ $@~ 2>/dev/null || true + $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true $(AM_V_GEN)(@srcdir@/mkexpr \ $< \ @srcdir@/builtin_kinds \ - `grep '^SUBDIRS = ' @top_srcdir@/src/theory/Makefile.in | cut -d' ' -f3- | tr ' ' "\n" | xargs -i__D__ echo @top_srcdir@/src/theory/__D__/kinds` \ + `cat @top_srcdir@/src/theory/.subdirs` \ > $@) || (rm -f $@ && exit 1) -@srcdir@/expr_manager.cpp: expr_manager_template.cpp mkexpr builtin_kinds @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds +@srcdir@/expr_manager.cpp: expr_manager_template.cpp mkexpr builtin_kinds @top_srcdir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds $(AM_V_at)chmod +x @srcdir@/mkexpr - $(AM_V_at)mv -f $@ $@~ 2>/dev/null || true + $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true $(AM_V_GEN)(@srcdir@/mkexpr \ $< \ @srcdir@/builtin_kinds \ - `grep '^SUBDIRS = ' @top_srcdir@/src/theory/Makefile.in | cut -d' ' -f3- | tr ' ' "\n" | xargs -i__D__ echo @top_srcdir@/src/theory/__D__/kinds` \ + `cat @top_srcdir@/src/theory/.subdirs` \ > $@) || (rm -f $@ && exit 1) BUILT_SOURCES = \ diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind index b8dbc2dd6..84d18e218 100755 --- a/src/expr/mkmetakind +++ b/src/expr/mkmetakind @@ -148,6 +148,12 @@ function constant { namespace expr { +// The reinterpret_cast of d_children to \"$2 const*\" +// flags a \"strict aliasing\" warning; it's okay, because we never access +// the embedded constant as a NodeValue* child, and never access an embedded +// NodeValue* child as a constant. +#pragma GCC diagnostic ignored \"-Wstrict-aliasing\" + template <> inline $2 const& NodeValue::getConst< $2 >() const { AssertArgument(getKind() == ::CVC4::kind::$1, *this, @@ -160,6 +166,9 @@ inline $2 const& NodeValue::getConst< $2 >() const { : *reinterpret_cast< $2 const* >(d_children[0]); } +// re-enable the warning +#pragma GCC diagnostic warning \"-Wstrict-aliasing\" + }/* CVC4::expr namespace */ namespace kind { diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index 5c0cfb987..c854b6b80 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -58,12 +58,11 @@ ** (b) The Node under construction is NOT already in the ** NodeManager's pool. ** - ** When a Node is extracted (see the non-const version of - ** NodeBuilderBase<>::operator Node()), we convert the NodeBuilder to - ** a Node and make sure the reference counts are properly maintained. - ** That means we must ensure there are no reference-counting errors - ** among the node's children, that the children aren't re-decremented - ** on clear() or NodeBuilder destruction, and that the returned Node + ** When a Node is extracted, we convert the NodeBuilder to a Node and + ** make sure the reference counts are properly maintained. That + ** means we must ensure there are no reference-counting errors among + ** the node's children, that the children aren't re-decremented on + ** clear() or NodeBuilder destruction, and that the returned Node ** wraps a NodeValue with a reference count of 1. ** ** 0. If a VARIABLE, treat similarly to 1(b), except that we @@ -109,37 +108,6 @@ ** decremented, which makes it eligible for collection before the ** builder has even returned it! So this is a no-no. ** - ** For the _const_ version of NodeBuilderBase<>::operator Node(), no - ** reference-count modifications or anything else can take place! - ** Therefore, we have a slightly more expensive version: - ** - ** 0. If a VARIABLE, treat similarly to 1(b), except that we - ** know there are no children, and we don't keep - ** VARIABLE-kinded Nodes in the NodeManager pool. - ** - ** 1(a). The existing NodeManager pool entry is returned; we leave - ** child reference counts alone and get them at NodeBuilder - ** destruction time. - ** - ** 1(b). A new heap-allocated NodeValue must be constructed and all - ** settings and children from d_inlineNv copied into it. - ** This new NodeValue is put into the NodeManager's pool. - ** The NodeBuilder cannot be marked as "used", so we - ** increment all child reference counts (which will be - ** decremented to match on destruction of the NodeBuilder). - ** We return a Node wrapper for this new NodeValue, which - ** increments its reference count. - ** - ** 2(a). The existing NodeManager pool entry is returned; we leave - ** child reference counts alone and get them at NodeBuilder - ** destruction time. - ** - ** 2(b). The heap-allocated d_nv cannot be "cropped" to the correct - ** size; we create a copy, increment child reference counts, - ** place this copy into the NodeManager pool, and return a - ** Node wrapper around it. The child reference counts will - ** be decremented to match at NodeBuilder destruction time. - ** ** There are also two cases when the NodeBuilder is clear()'ed: ** ** 1. d_nv == &d_inlineNv (NodeBuilder using the user-supplied @@ -285,9 +253,8 @@ protected: /** * Returns whether or not this NodeBuilder has been "used"---i.e., - * whether a Node has been extracted with [the non-const version of] - * operator Node(). Internally, this state is represented by d_nv - * pointing to NULL. + * whether a Node has been extracted with operator Node(). + * Internally, this state is represented by d_nv pointing to NULL. */ inline bool isUsed() const { return EXPECT_FALSE( d_nv == NULL ); @@ -570,10 +537,7 @@ public: return static_cast(*this); } - // two versions, so we can support extraction from (const) - // NodeBuilders which are temporaries appearing as rvalues operator Node(); - operator Node() const; inline void toStream(std::ostream& out, int depth = -1) const { Assert(!isUsed(), "NodeBuilder is one-shot only; " @@ -890,19 +854,19 @@ inline OrNodeBuilder AndNodeBuilder::operator||(const NodeTemplate& n) { inline AndNodeBuilder& operator&&(AndNodeBuilder& a, const AndNodeBuilder& b) { - return a && Node(b.d_eb); + return a && Node(const_cast&>(b.d_eb)); } inline AndNodeBuilder& operator&&(AndNodeBuilder& a, const OrNodeBuilder& b) { - return a && Node(b.d_eb); + return a && Node(const_cast&>(b.d_eb)); } inline OrNodeBuilder operator||(AndNodeBuilder& a, const AndNodeBuilder& b) { - return a || Node(b.d_eb); + return a || Node(const_cast&>(b.d_eb)); } inline OrNodeBuilder operator||(AndNodeBuilder& a, const OrNodeBuilder& b) { - return a || Node(b.d_eb); + return a || Node(const_cast&>(b.d_eb)); } template @@ -918,19 +882,19 @@ inline OrNodeBuilder& OrNodeBuilder::operator||(const NodeTemplate& n) { inline AndNodeBuilder operator&&(OrNodeBuilder& a, const AndNodeBuilder& b) { - return a && Node(b.d_eb); + return a && Node(const_cast&>(b.d_eb)); } inline AndNodeBuilder operator&&(OrNodeBuilder& a, const OrNodeBuilder& b) { - return a && Node(b.d_eb); + return a && Node(const_cast&>(b.d_eb)); } inline OrNodeBuilder& operator||(OrNodeBuilder& a, const AndNodeBuilder& b) { - return a || Node(b.d_eb); + return a || Node(const_cast&>(b.d_eb)); } inline OrNodeBuilder& operator||(OrNodeBuilder& a, const OrNodeBuilder& b) { - return a || Node(b.d_eb); + return a || Node(const_cast&>(b.d_eb)); } template @@ -952,27 +916,27 @@ inline MultNodeBuilder PlusNodeBuilder::operator*(const NodeTemplate& n) { inline PlusNodeBuilder& operator+(PlusNodeBuilder& a, const PlusNodeBuilder& b) { - return a + Node(b.d_eb); + return a + Node(const_cast&>(b.d_eb)); } inline PlusNodeBuilder& operator+(PlusNodeBuilder& a, const MultNodeBuilder& b) { - return a + Node(b.d_eb); + return a + Node(const_cast&>(b.d_eb)); } inline PlusNodeBuilder& operator-(PlusNodeBuilder&a, const PlusNodeBuilder& b) { - return a - Node(b.d_eb); + return a - Node(const_cast&>(b.d_eb)); } inline PlusNodeBuilder& operator-(PlusNodeBuilder& a, const MultNodeBuilder& b) { - return a - Node(b.d_eb); + return a - Node(const_cast&>(b.d_eb)); } inline MultNodeBuilder operator*(PlusNodeBuilder& a, const PlusNodeBuilder& b) { - return a * Node(b.d_eb); + return a * Node(const_cast&>(b.d_eb)); } inline MultNodeBuilder operator*(PlusNodeBuilder& a, const MultNodeBuilder& b) { - return a * Node(b.d_eb); + return a * Node(const_cast&>(b.d_eb)); } template @@ -994,27 +958,27 @@ inline MultNodeBuilder& MultNodeBuilder::operator*(const NodeTemplate& n) { inline PlusNodeBuilder operator+(MultNodeBuilder& a, const PlusNodeBuilder& b) { - return a + Node(b.d_eb); + return a + Node(const_cast&>(b.d_eb)); } inline PlusNodeBuilder operator+(MultNodeBuilder& a, const MultNodeBuilder& b) { - return a + Node(b.d_eb); + return a + Node(const_cast&>(b.d_eb)); } inline PlusNodeBuilder operator-(MultNodeBuilder& a, const PlusNodeBuilder& b) { - return a - Node(b.d_eb); + return a - Node(const_cast&>(b.d_eb)); } inline PlusNodeBuilder operator-(MultNodeBuilder& a, const MultNodeBuilder& b) { - return a - Node(b.d_eb); + return a - Node(const_cast&>(b.d_eb)); } inline MultNodeBuilder& operator*(MultNodeBuilder& a, const PlusNodeBuilder& b) { - return a * Node(b.d_eb); + return a * Node(const_cast&>(b.d_eb)); } inline MultNodeBuilder& operator*(MultNodeBuilder& a, const MultNodeBuilder& b) { - return a * Node(b.d_eb); + return a * Node(const_cast&>(b.d_eb)); } template @@ -1050,61 +1014,61 @@ inline MultNodeBuilder operator*(const NodeTemplate& a, template inline AndNodeBuilder operator&&(const NodeTemplate& a, const AndNodeBuilder& b) { - return a && Node(b.d_eb); + return a && Node(const_cast&>(b.d_eb)); } template inline AndNodeBuilder operator&&(const NodeTemplate& a, const OrNodeBuilder& b) { - return a && Node(b.d_eb); + return a && Node(const_cast&>(b.d_eb)); } template inline OrNodeBuilder operator||(const NodeTemplate& a, const AndNodeBuilder& b) { - return a || Node(b.d_eb); + return a || Node(const_cast&>(b.d_eb)); } template inline OrNodeBuilder operator||(const NodeTemplate& a, const OrNodeBuilder& b) { - return a || Node(b.d_eb); + return a || Node(const_cast&>(b.d_eb)); } template inline PlusNodeBuilder operator+(const NodeTemplate& a, const PlusNodeBuilder& b) { - return a + Node(b.d_eb); + return a + Node(const_cast&>(b.d_eb)); } template inline PlusNodeBuilder operator+(const NodeTemplate& a, const MultNodeBuilder& b) { - return a + Node(b.d_eb); + return a + Node(const_cast&>(b.d_eb)); } template inline PlusNodeBuilder operator-(const NodeTemplate& a, const PlusNodeBuilder& b) { - return a - Node(b.d_eb); + return a - Node(const_cast&>(b.d_eb)); } template inline PlusNodeBuilder operator-(const NodeTemplate& a, const MultNodeBuilder& b) { - return a - Node(b.d_eb); + return a - Node(const_cast&>(b.d_eb)); } template inline MultNodeBuilder operator*(const NodeTemplate& a, const PlusNodeBuilder& b) { - return a * Node(b.d_eb); + return a * Node(const_cast&>(b.d_eb)); } template inline MultNodeBuilder operator*(const NodeTemplate& a, const MultNodeBuilder& b) { - return a * Node(b.d_eb); + return a * Node(const_cast&>(b.d_eb)); } template @@ -1262,7 +1226,6 @@ void NodeBuilderBase::decrRefCounts() { d_inlineNv.d_nchildren = 0; } -// NON-CONST VERSION OF NODE EXTRACTOR template NodeBuilderBase::operator Node() { Assert(!isUsed(), "NodeBuilder is one-shot only; " @@ -1434,183 +1397,6 @@ NodeBuilderBase::operator Node() { } } -// CONST VERSION OF NODE EXTRACTOR -template -NodeBuilderBase::operator Node() const { - Assert(!isUsed(), "NodeBuilder is one-shot only; " - "attempt to access it after conversion"); - Assert(getKind() != kind::UNDEFINED_KIND, - "Can't make an expression of an undefined kind!"); - - // NOTE: The comments in this function refer to the cases in the - // file comments at the top of this file. - - // Case 0: If a VARIABLE - if(getMetaKind() == kind::metakind::VARIABLE) { - /* 0. If a VARIABLE, treat similarly to 1(b), except that we know - * there are no children (no reference counts to reason about), - * and we don't keep VARIABLE-kinded Nodes in the NodeManager - * pool. */ - - Assert( ! nvIsAllocated(), - "internal NodeBuilder error: " - "VARIABLE-kinded NodeBuilder is heap-allocated !?" ); - Assert( d_inlineNv.d_nchildren == 0, - "improperly-formed VARIABLE-kinded NodeBuilder: " - "no children permitted" ); - - // we have to copy the inline NodeValue out - expr::NodeValue* nv = (expr::NodeValue*) - std::malloc(sizeof(expr::NodeValue)); - if(nv == NULL) { - throw std::bad_alloc(); - } - // there are no children, so we don't have to worry about - // reference counts in this case. - nv->d_nchildren = 0; - nv->d_kind = d_nv->d_kind; - nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading - nv->d_rc = 0; - Debug("gc") << "creating node value " << nv - << " [" << nv->d_id << "]: " << *nv << "\n"; - return Node(nv); - } - - // check that there are the right # of children for this kind - Assert(getMetaKind() != kind::metakind::CONSTANT, - "Cannot make Nodes with NodeBuilder that have CONSTANT-kinded kinds"); - Assert(d_nv->d_nchildren >= kind::metakind::getLowerBoundForKind(getKind()), - "Nodes with kind %s must have at least %u children (the one under " - "construction has %u)", - kind::kindToString(getKind()).c_str(), - kind::metakind::getLowerBoundForKind(getKind()), - getNumChildren()); - Assert(d_nv->d_nchildren <= kind::metakind::getUpperBoundForKind(getKind()), - "Nodes with kind %s must have at most %u children (the one under " - "construction has %u)", - kind::kindToString(getKind()).c_str(), - kind::metakind::getUpperBoundForKind(getKind()), - getNumChildren()); - - // Implementation differs depending on whether the NodeValue was - // malloc'ed or not and whether or not it's in the already-been-seen - // NodeManager pool of Nodes. See implementation notes at the top - // of this file. - - if(EXPECT_TRUE( ! nvIsAllocated() )) { - /** Case 1. d_nv points to d_inlineNv: it is the backing store - ** supplied by the user (or derived class) **/ - - // Lookup the expression value in the pool we already have - expr::NodeValue* poolNv = d_nm->poolLookup(&d_inlineNv); - // If something else is there, we reuse it - if(poolNv != NULL) { - /* Subcase (a): The Node under construction already exists in - * the NodeManager's pool. */ - - /* 1(a). The existing NodeManager pool entry is returned; we - * leave child reference counts alone and get them at - * NodeBuilder destruction time. */ - - return Node(poolNv); - } else { - /* Subcase (b): The Node under construction is NOT already in - * the NodeManager's pool. */ - - /* 1(b). A new heap-allocated NodeValue must be constructed and - * all settings and children from d_inlineNv copied into it. - * This new NodeValue is put into the NodeManager's pool. The - * NodeBuilder cannot be marked as "used", so we increment all - * child reference counts (which will be decremented to match on - * destruction of the NodeBuilder). We return a Node wrapper - * for this new NodeValue, which increments its reference - * count. */ - - // create the canonical expression value for this node - expr::NodeValue* nv = (expr::NodeValue*) - std::malloc(sizeof(expr::NodeValue) + - ( sizeof(expr::NodeValue*) * d_inlineNv.d_nchildren )); - if(nv == NULL) { - throw std::bad_alloc(); - } - nv->d_nchildren = d_inlineNv.d_nchildren; - nv->d_kind = d_inlineNv.d_kind; - nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading - nv->d_rc = 0; - - std::copy(d_inlineNv.d_children, - d_inlineNv.d_children + d_inlineNv.d_nchildren, - nv->d_children); - - for(expr::NodeValue::nv_iterator i = nv->nv_begin(); - i != nv->nv_end(); - ++i) { - (*i)->inc(); - } - - //poolNv = nv; - d_nm->poolInsert(nv); - Debug("gc") << "creating node value " << nv - << " [" << nv->d_id << "]: " << *nv << "\n"; - return Node(nv); - } - } else { - /** Case 2. d_nv does NOT point to d_inlineNv: it is a new, larger - ** buffer that was heap-allocated by this NodeBuilder. **/ - - // Lookup the expression value in the pool we already have (with insert) - expr::NodeValue* poolNv = d_nm->poolLookup(d_nv); - // If something else is there, we reuse it - if(poolNv != NULL) { - /* Subcase (a): The Node under construction already exists in - * the NodeManager's pool. */ - - /* 2(a). The existing NodeManager pool entry is returned; we - * leave child reference counts alone and get them at - * NodeBuilder destruction time. */ - - return Node(poolNv); - } else { - /* Subcase (b) The Node under construction is NOT already in the - * NodeManager's pool. */ - - /* 2(b). The heap-allocated d_nv cannot be "cropped" to the - * correct size; we create a copy, increment child reference - * counts, place this copy into the NodeManager pool, and return - * a Node wrapper around it. The child reference counts will be - * decremented to match at NodeBuilder destruction time. */ - - // create the canonical expression value for this node - expr::NodeValue* nv = (expr::NodeValue*) - std::malloc(sizeof(expr::NodeValue) + - ( sizeof(expr::NodeValue*) * d_nv->d_nchildren )); - if(nv == NULL) { - throw std::bad_alloc(); - } - nv->d_nchildren = d_nv->d_nchildren; - nv->d_kind = d_nv->d_kind; - nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading - nv->d_rc = 0; - - std::copy(d_nv->d_children, - d_nv->d_children + d_nv->d_nchildren, - nv->d_children); - - for(expr::NodeValue::nv_iterator i = nv->nv_begin(); - i != nv->nv_end(); - ++i) { - (*i)->inc(); - } - - //poolNv = nv; - d_nm->poolInsert(nv); - Debug("gc") << "creating node value " << nv - << " [" << nv->d_id << "]: " << *nv << "\n"; - return Node(nv); - } - } -} - template template void NodeBuilder::internalCopy(const NodeBuilder& nb) { diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am index 6b1854bfc..07896271a 100644 --- a/src/theory/Makefile.am +++ b/src/theory/Makefile.am @@ -23,12 +23,14 @@ EXTRA_DIST = \ @srcdir@/theoryof_table.h \ theoryof_table_template.h -@srcdir@/theoryof_table.h: theoryof_table_template.h mktheoryof @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds +include @top_srcdir@/src/theory/Makefile.subdirs + +@srcdir@/theoryof_table.h: theoryof_table_template.h mktheoryof @top_srcdir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds $(AM_V_at)chmod +x @srcdir@/mktheoryof - $(AM_V_at)mv -f $@ $@~ 2>/dev/null || true + $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true $(AM_V_GEN)(@srcdir@/mktheoryof \ $< \ - `grep '^SUBDIRS = ' @top_srcdir@/src/theory/Makefile.in | cut -d' ' -f3- | tr ' ' "\n" | xargs -i__D__ echo @top_srcdir@/src/theory/__D__/kinds` \ + `cat @top_srcdir@/src/theory/.subdirs` \ > $@) || (rm -f $@ && exit 1) BUILT_SOURCES = @srcdir@/theoryof_table.h diff --git a/src/theory/Makefile.subdirs b/src/theory/Makefile.subdirs new file mode 100644 index 000000000..bcc7db1c5 --- /dev/null +++ b/src/theory/Makefile.subdirs @@ -0,0 +1,6 @@ +$(top_srcdir)/src/theory/.subdirs: $(top_srcdir)/src/theory/Makefile.am + $(AM_V_at)grep '^SUBDIRS = ' $(top_srcdir)/src/theory/Makefile.am | cut -d' ' -f3- | tr ' ' "\n" | xargs -i__D__ echo $(top_srcdir)/src/theory/__D__/kinds >$(top_srcdir)/src/theory/.subdirs.tmp + @if ! diff -q $(top_srcdir)/src/theory/.subdirs $(top_srcdir)/src/theory/.subdirs.tmp &>/dev/null; then \ + echo " GEN " $@; \ + $(am__mv) $(top_srcdir)/src/theory/.subdirs.tmp $(top_srcdir)/src/theory/.subdirs; \ + fi diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index a190152d3..1f56434c9 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -30,21 +30,8 @@ UNIT_TESTS = \ # Things that aren't tests but that tests rely on and need to # go into the distribution -TEST_DEPS_DIST = - -# Make-level dependencies; these don't go in the source distribution -# but should trigger a re-compile of all unit tests. Libraries are -# included here because (1) if static-linking, the tests must be -# relinked, and (2) if they've changed that means the sources changed, -# and that means we should ensure the tests compile against any -# changes made in the header files. -TEST_DEPS_NODIST = \ - $(abs_top_builddir)/src/libcvc4.la \ - $(abs_top_builddir)/src/parser/libcvc4parser.la - -TEST_DEPS = \ - $(TEST_DEPS_DIST) \ - $(TEST_DEPS_NODIST) +TEST_DEPS_DIST = \ + memory.h if HAVE_CXXTESTGEN @@ -57,13 +44,16 @@ AM_LDFLAGS = $(TEST_LDFLAGS) AM_CXXFLAGS_WHITE = -fno-access-control -D__BUILDING_CVC4LIB_UNIT_TEST -D__BUILDING_CVC4PARSERLIB_UNIT_TEST AM_CXXFLAGS_BLACK = -D__BUILDING_CVC4LIB_UNIT_TEST -D__BUILDING_CVC4PARSERLIB_UNIT_TEST AM_CXXFLAGS_PUBLIC = -AM_LDFLAGS_WHITE = \ +AM_LDFLAGS_WHITE = +AM_LDFLAGS_BLACK = +AM_LDFLAGS_PUBLIC = +AM_LIBADD_WHITE = \ @abs_top_builddir@/src/parser/libcvc4parser_noinst.la \ @abs_top_builddir@/src/libcvc4_noinst.la -AM_LDFLAGS_BLACK = \ +AM_LIBADD_BLACK = \ @abs_top_builddir@/src/parser/libcvc4parser_noinst.la \ @abs_top_builddir@/src/libcvc4_noinst.la -AM_LDFLAGS_PUBLIC = \ +AM_LIBADD_PUBLIC = \ @abs_top_builddir@/src/libcvc4.la EXTRA_DIST = \ @@ -84,18 +74,48 @@ else unit_LINK = $(CXXLINK) endif +@AMDEP_TRUE@@am__include@ $(UNIT_TESTS:%=@am__quote@./$(DEPDIR)/%.Plo@am__quote@) + +$(UNIT_TESTS:%=@am__quote@./$(DEPDIR)/%.Plo@am__quote@): %.Plo: + $(AM_V_at)$(MKDIR_P) `dirname "$@"` + $(AM_V_GEN)test -e "$@" || touch "$@" + $(UNIT_TESTS:%=%.cpp): %.cpp: %.h - $(AM_V_at)mkdir -p `dirname "$@"` + $(AM_V_at)$(MKDIR_P) `dirname "$@"` $(AM_V_GEN)$(CXXTESTGEN) --have-eh --have-std --error-printer -o "$@" "$<" -$(WHITE_TESTS): %_white: %_white.cpp $(TEST_DEPS) - $(AM_V_CXX)$(LTCXXCOMPILE) $(AM_CXXFLAGS_WHITE) -c -o $@.lo @abs_builddir@/$< - $(AM_V_CXXLD)$(unit_LINK) $(AM_LDFLAGS_WHITE) $@.lo -$(BLACK_TESTS): %_black: %_black.cpp $(TEST_DEPS) - $(AM_V_CXX)$(LTCXXCOMPILE) $(AM_CXXFLAGS_BLACK) -c -o $@.lo @abs_builddir@/$< - $(AM_V_CXXLD)$(unit_LINK) $(AM_LDFLAGS_BLACK) $@.lo -$(PUBLIC_TESTS): %_public: %_public.cpp $(TEST_DEPS) - $(AM_V_CXX)$(LTCXXCOMPILE) $(AM_CXXFLAGS_PUBLIC) -c -o $@.lo @abs_builddir@/$< - $(AM_V_CXXLD)$(unit_LINK) $(AM_LDFLAGS_PUBLIC) $@.lo + +$(WHITE_TESTS:%=%.lo): %_white.lo: %_white.cpp +@am__fastdepCXX_TRUE@ $(AM_V_CXX)$(LTCXXCOMPILE) $(AM_CXXFLAGS_WHITE) -MT $@ -MD -MP -MF $(DEPDIR)/$(@:%.lo=%).Tpo -c -o $@ $< +@am__fastdepCXX_TRUE@ $(AM_V_at)$(am__mv) $(DEPDIR)/$(@:%.lo=%).Tpo $(DEPDIR)/$(@:%.lo=%).Plo +@am__fastdepCXX_FALSE@ $(AM_V_CXX) @AM_BACKSLASH@ +@AMDEP_TRUE@@am__fastdepCXX_FALSE@ source='$<' object='$@' libtool=yes @AMDEPBACKSLASH@ +@AMDEP_TRUE@@am__fastdepCXX_FALSE@ DEPDIR=$(DEPDIR) $(CXXDEPMODE) $(depcomp) @AMDEPBACKSLASH@ +@am__fastdepCXX_FALSE@ $(LTCXXCOMPILE) $(AM_CXXFLAGS_WHITE) -c -o $@ $< + +$(WHITE_TESTS): %_white: %_white.lo $(AM_LIBADD_WHITE) + $(AM_V_CXXLD)$(unit_LINK) $(AM_LIBADD_WHITE) $(AM_LDFLAGS_WHITE) $< + +$(BLACK_TESTS:%=%.lo): %_black.lo: %_black.cpp +@am__fastdepCXX_TRUE@ $(AM_V_CXX)$(LTCXXCOMPILE) $(AM_CXXFLAGS_BLACK) -MT $@ -MD -MP -MF $(DEPDIR)/$(@:%.lo=%).Tpo -c -o $@ $< +@am__fastdepCXX_TRUE@ $(AM_V_at)$(am__mv) $(DEPDIR)/$(@:%.lo=%).Tpo $(DEPDIR)/$(@:%.lo=%).Plo +@am__fastdepCXX_FALSE@ $(AM_V_CXX) @AM_BACKSLASH@ +@AMDEP_TRUE@@am__fastdepCXX_FALSE@ source='$<' object='$@' libtool=yes @AMDEPBACKSLASH@ +@AMDEP_TRUE@@am__fastdepCXX_FALSE@ DEPDIR=$(DEPDIR) $(CXXDEPMODE) $(depcomp) @AMDEPBACKSLASH@ +@am__fastdepCXX_FALSE@ $(LTCXXCOMPILE) $(AM_CXXFLAGS_BLACK) -c -o $@ $< + +$(BLACK_TESTS): %_black: %_black.lo $(AM_LIBADD_BLACK) + $(AM_V_CXXLD)$(unit_LINK) $(AM_LIBADD_BLACK) $(AM_LDFLAGS_BLACK) $< + +$(PUBLIC_TESTS:%=%.lo): %_public.lo: %_public.cpp +@am__fastdepCXX_TRUE@ $(AM_V_CXX)$(LTCXXCOMPILE) $(AM_CXXFLAGS_PUBLIC) -MT $@ -MD -MP -MF $(DEPDIR)/$(@:%.lo=%).Tpo -c -o $@ $< +@am__fastdepCXX_TRUE@ $(AM_V_at)$(am__mv) $(DEPDIR)/$(@:%.lo=%).Tpo $(DEPDIR)/$(@:%.lo=%).Plo +@am__fastdepCXX_FALSE@ $(AM_V_CXX) @AM_BACKSLASH@ +@AMDEP_TRUE@@am__fastdepCXX_FALSE@ source='$<' object='$@' libtool=yes @AMDEPBACKSLASH@ +@AMDEP_TRUE@@am__fastdepCXX_FALSE@ DEPDIR=$(DEPDIR) $(CXXDEPMODE) $(depcomp) @AMDEPBACKSLASH@ +@am__fastdepCXX_FALSE@ $(LTCXXCOMPILE) $(AM_CXXFLAGS_PUBLIC) -c -o $@ $< + +$(PUBLIC_TESTS): %_public: %_public.lo $(AM_LIBADD_PUBLIC) + $(AM_V_CXXLD)$(unit_LINK) $(AM_LIBADD_PUBLIC) $(AM_LDFLAGS_PUBLIC) $< else diff --git a/test/unit/context/cdlist_black.h b/test/unit/context/cdlist_black.h index 418357630..bcc95b470 100644 --- a/test/unit/context/cdlist_black.h +++ b/test/unit/context/cdlist_black.h @@ -17,12 +17,17 @@ #include #include + +#include + +#include "memory.h" + #include "context/context.h" #include "context/cdlist.h" using namespace std; using namespace CVC4::context; - +using namespace CVC4::test; struct DtorSensitiveObject { bool& d_dtorCalled; @@ -30,7 +35,6 @@ struct DtorSensitiveObject { ~DtorSensitiveObject() { d_dtorCalled = true; } }; - class CDListBlack : public CxxTest::TestSuite { private: @@ -125,4 +129,17 @@ public: TS_ASSERT_EQUALS(shouldAlsoRemainFalse, false); TS_ASSERT_EQUALS(aThirdFalse, false); } + + void testOutOfMemory() { + CDList list(d_context); + WithLimitedMemory wlm(0); + + TS_ASSERT_THROWS({ + // We cap it at UINT_MAX, preferring to terminate with a + // failure than run indefinitely. + for(unsigned i = 0; i < UINT_MAX; ++i) { + list.push_back(i); + } + }, bad_alloc); + } }; diff --git a/test/unit/expr/attribute_black.h b/test/unit/expr/attribute_black.h index 92aacf509..5ae644193 100644 --- a/test/unit/expr/attribute_black.h +++ b/test/unit/expr/attribute_black.h @@ -91,8 +91,8 @@ public: Type* booleanType = d_nodeManager->booleanType(); Node* node = new Node(d_nodeManager->mkVar(booleanType)); const uint64_t val = 63489; - uint64_t data0; - uint64_t data1; + uint64_t data0 = 0; + uint64_t data1 = 0; PrimitiveIntAttribute attr; TS_ASSERT(!node->getAttribute(attr, data0)); @@ -100,8 +100,8 @@ public: TS_ASSERT(node->getAttribute(attr, data1)); TS_ASSERT_EQUALS(data1, val); - uint64_t data2; - uint64_t data3; + uint64_t data2 = 0; + uint64_t data3 = 0; CDPrimitiveIntAttribute cdattr; TS_ASSERT(!node->getAttribute(cdattr, data2)); node->setAttribute(cdattr, val); @@ -155,8 +155,8 @@ public: Node* node = new Node(d_nodeManager->mkVar(booleanType)); Foo* val = new Foo(63489); - Foo* data0; - Foo* data1; + Foo* data0 = NULL; + Foo* data1 = NULL; PtrAttribute attr; TS_ASSERT(!node->getAttribute(attr, data0)); @@ -164,8 +164,8 @@ public: TS_ASSERT(node->getAttribute(attr, data1)); TS_ASSERT_EQUALS(data1, val); - Foo* data2; - Foo* data3; + Foo* data2 = NULL; + Foo* data3 = NULL; CDPtrAttribute cdattr; TS_ASSERT(!node->getAttribute(cdattr, data2)); node->setAttribute(cdattr, val); @@ -186,8 +186,8 @@ public: Node* node = new Node(d_nodeManager->mkVar(booleanType)); const Foo* val = new Foo(63489); - const Foo* data0; - const Foo* data1; + const Foo* data0 = NULL; + const Foo* data1 = NULL; ConstPtrAttribute attr; TS_ASSERT(!node->getAttribute(attr, data0)); @@ -195,8 +195,8 @@ public: TS_ASSERT(node->getAttribute(attr, data1)); TS_ASSERT_EQUALS(data1, val); - const Foo* data2; - const Foo* data3; + const Foo* data2 = NULL; + const Foo* data3 = NULL; CDConstPtrAttribute cdattr; TS_ASSERT(!node->getAttribute(cdattr, data2)); node->setAttribute(cdattr, val); diff --git a/test/unit/memory.h b/test/unit/memory.h new file mode 100644 index 000000000..38ac63e65 --- /dev/null +++ b/test/unit/memory.h @@ -0,0 +1,69 @@ +/********************* */ +/** memory.h + ** 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. + ** + ** Utility class to help testing out-of-memory conditions. + ** + ** Use it like this (for example): + ** + ** CVC4::test::WithLimitedMemory wlm(amount); + ** TS_ASSERT_THROWS( foo(), bad_alloc ); + ** + ** The WithLimitedMemory destructor will re-establish the previous limit. + **/ + +#include + +#ifndef __CVC4__TEST__MEMORY_H +#define __CVC4__TEST__MEMORY_H + +#include +#include + +namespace CVC4 { +namespace test { + +class WithLimitedMemory { + rlim_t d_prevAmount; + + void remember() { + struct rlimit rlim; + TS_ASSERT_EQUALS(getrlimit(RLIMIT_AS, &rlim), 0); + d_prevAmount = rlim.rlim_cur; + } + +public: + + WithLimitedMemory() { + remember(); + } + + WithLimitedMemory(rlim_t amount) { + remember(); + set(amount); + } + + ~WithLimitedMemory() { + set(d_prevAmount); + } + + void set(rlim_t amount) { + struct rlimit rlim; + rlim.rlim_cur = amount; + rlim.rlim_max = RLIM_INFINITY; + TS_ASSERT_EQUALS(setrlimit(RLIMIT_AS, &rlim), 0); + } +}; + +}/* CVC4::test namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__TEST__MEMORY_H */ -- 2.30.2