summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile.am28
-rw-r--r--configure.ac7
-rw-r--r--src/expr/Makefile.am39
-rwxr-xr-xsrc/expr/mkmetakind9
-rw-r--r--src/expr/node_builder.h288
-rw-r--r--src/theory/Makefile.am8
-rw-r--r--src/theory/Makefile.subdirs6
-rw-r--r--test/unit/Makefile.am76
-rw-r--r--test/unit/context/cdlist_black.h21
-rw-r--r--test/unit/expr/attribute_black.h24
-rw-r--r--test/unit/memory.h69
11 files changed, 255 insertions, 320 deletions
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#(<td class="coverFn"><a href=".*">)(.*)(</a></td>)#$$_=`c++filt "$$2"`;chomp;print "$$1<xmp>$$_</xmp>$$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#(<td class="coverFn"><a href=".*">)(.*)(</a></td>)#$$_=`c++filt "$$2"`;chomp;print "$$1<xmp>$$_</xmp>$$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,(<td class="coverFn"><a href=".*">)(.*)(</a></td>.*),$$_=`c++filt "$$2"`;chomp;print "$$1<xmp>$$_</xmp>$$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 <<EOF
+ cat >config.reconfig <<EOF
#!/bin/sh -ex
# Generated by configure, `date`
# This script part of CVC4.
@@ -176,7 +176,7 @@ build_type='$build_type'
cd "builds/$target/$build_type"
./config.status "\$@"
EOF
- chmod +x config.status
+ chmod +x config.reconfig
fi
exit $exitval
else
@@ -408,7 +408,7 @@ if test "$enable_profiling" = yes; then
CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }-pg"
fi
-AM_INIT_AUTOMAKE([1.11 no-define])
+AM_INIT_AUTOMAKE([1.11 no-define color-tests])
AC_CONFIG_HEADERS([cvc4autoconfig.h])
# Initialize libtool's configuration options.
@@ -516,6 +516,7 @@ AC_SUBST(BUILDING_SHARED)
AC_SUBST(BUILDING_STATIC)
AC_SUBST(STATIC_BINARY)
AM_CONDITIONAL([STATIC_BINARY], [test "$enable_static_binary" = yes])
+AM_CONDITIONAL([COVERAGE_ENABLED], [test "$enable_coverage" = yes])
AC_SUBST(CVC4_LIBRARY_VERSION)
AC_SUBST(CVC4_PARSER_LIBRARY_VERSION)
diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index 67970d453..a9480723f 100644
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -27,7 +27,6 @@ libexpr_la_SOURCES = \
command.cpp \
declaration_scope.h \
declaration_scope.cpp
-
EXTRA_DIST = \
@srcdir@/kind.h \
@@ -43,58 +42,60 @@ EXTRA_DIST = \
expr_template.h \
expr_template.cpp
-@srcdir@/kind.h: kind_template.h mkkind builtin_kinds @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds
+include @top_srcdir@/src/theory/Makefile.subdirs
+
+@srcdir@/kind.h: kind_template.h mkkind builtin_kinds @top_srcdir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
$(AM_V_at)chmod +x @srcdir@/mkkind
- $(AM_V_at)mv -f $@ $@~ 2>/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<Builder&>(*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<rc>& n) {
inline AndNodeBuilder& operator&&(AndNodeBuilder& a,
const AndNodeBuilder& b) {
- return a && Node(b.d_eb);
+ return a && Node(const_cast<NodeBuilder<>&>(b.d_eb));
}
inline AndNodeBuilder& operator&&(AndNodeBuilder& a,
const OrNodeBuilder& b) {
- return a && Node(b.d_eb);
+ return a && Node(const_cast<NodeBuilder<>&>(b.d_eb));
}
inline OrNodeBuilder operator||(AndNodeBuilder& a,
const AndNodeBuilder& b) {
- return a || Node(b.d_eb);
+ return a || Node(const_cast<NodeBuilder<>&>(b.d_eb));
}
inline OrNodeBuilder operator||(AndNodeBuilder& a,
const OrNodeBuilder& b) {
- return a || Node(b.d_eb);
+ return a || Node(const_cast<NodeBuilder<>&>(b.d_eb));
}
template <bool rc>
@@ -918,19 +882,19 @@ inline OrNodeBuilder& OrNodeBuilder::operator||(const NodeTemplate<rc>& n) {
inline AndNodeBuilder operator&&(OrNodeBuilder& a,
const AndNodeBuilder& b) {
- return a && Node(b.d_eb);
+ return a && Node(const_cast<NodeBuilder<>&>(b.d_eb));
}
inline AndNodeBuilder operator&&(OrNodeBuilder& a,
const OrNodeBuilder& b) {
- return a && Node(b.d_eb);
+ return a && Node(const_cast<NodeBuilder<>&>(b.d_eb));
}
inline OrNodeBuilder& operator||(OrNodeBuilder& a,
const AndNodeBuilder& b) {
- return a || Node(b.d_eb);
+ return a || Node(const_cast<NodeBuilder<>&>(b.d_eb));
}
inline OrNodeBuilder& operator||(OrNodeBuilder& a,
const OrNodeBuilder& b) {
- return a || Node(b.d_eb);
+ return a || Node(const_cast<NodeBuilder<>&>(b.d_eb));
}
template <bool rc>
@@ -952,27 +916,27 @@ inline MultNodeBuilder PlusNodeBuilder::operator*(const NodeTemplate<rc>& n) {
inline PlusNodeBuilder& operator+(PlusNodeBuilder& a,
const PlusNodeBuilder& b) {
- return a + Node(b.d_eb);
+ return a + Node(const_cast<NodeBuilder<>&>(b.d_eb));
}
inline PlusNodeBuilder& operator+(PlusNodeBuilder& a,
const MultNodeBuilder& b) {
- return a + Node(b.d_eb);
+ return a + Node(const_cast<NodeBuilder<>&>(b.d_eb));
}
inline PlusNodeBuilder& operator-(PlusNodeBuilder&a,
const PlusNodeBuilder& b) {
- return a - Node(b.d_eb);
+ return a - Node(const_cast<NodeBuilder<>&>(b.d_eb));
}
inline PlusNodeBuilder& operator-(PlusNodeBuilder& a,
const MultNodeBuilder& b) {
- return a - Node(b.d_eb);
+ return a - Node(const_cast<NodeBuilder<>&>(b.d_eb));
}
inline MultNodeBuilder operator*(PlusNodeBuilder& a,
const PlusNodeBuilder& b) {
- return a * Node(b.d_eb);
+ return a * Node(const_cast<NodeBuilder<>&>(b.d_eb));
}
inline MultNodeBuilder operator*(PlusNodeBuilder& a,
const MultNodeBuilder& b) {
- return a * Node(b.d_eb);
+ return a * Node(const_cast<NodeBuilder<>&>(b.d_eb));
}
template <bool rc>
@@ -994,27 +958,27 @@ inline MultNodeBuilder& MultNodeBuilder::operator*(const NodeTemplate<rc>& n) {
inline PlusNodeBuilder operator+(MultNodeBuilder& a,
const PlusNodeBuilder& b) {
- return a + Node(b.d_eb);
+ return a + Node(const_cast<NodeBuilder<>&>(b.d_eb));
}
inline PlusNodeBuilder operator+(MultNodeBuilder& a,
const MultNodeBuilder& b) {
- return a + Node(b.d_eb);
+ return a + Node(const_cast<NodeBuilder<>&>(b.d_eb));
}
inline PlusNodeBuilder operator-(MultNodeBuilder& a,
const PlusNodeBuilder& b) {
- return a - Node(b.d_eb);
+ return a - Node(const_cast<NodeBuilder<>&>(b.d_eb));
}
inline PlusNodeBuilder operator-(MultNodeBuilder& a,
const MultNodeBuilder& b) {
- return a - Node(b.d_eb);
+ return a - Node(const_cast<NodeBuilder<>&>(b.d_eb));
}
inline MultNodeBuilder& operator*(MultNodeBuilder& a,
const PlusNodeBuilder& b) {
- return a * Node(b.d_eb);
+ return a * Node(const_cast<NodeBuilder<>&>(b.d_eb));
}
inline MultNodeBuilder& operator*(MultNodeBuilder& a,
const MultNodeBuilder& b) {
- return a * Node(b.d_eb);
+ return a * Node(const_cast<NodeBuilder<>&>(b.d_eb));
}
template <bool rc1, bool rc2>
@@ -1050,61 +1014,61 @@ inline MultNodeBuilder operator*(const NodeTemplate<rc1>& a,
template <bool rc>
inline AndNodeBuilder operator&&(const NodeTemplate<rc>& a,
const AndNodeBuilder& b) {
- return a && Node(b.d_eb);
+ return a && Node(const_cast<NodeBuilder<>&>(b.d_eb));
}
template <bool rc>
inline AndNodeBuilder operator&&(const NodeTemplate<rc>& a,
const OrNodeBuilder& b) {
- return a && Node(b.d_eb);
+ return a && Node(const_cast<NodeBuilder<>&>(b.d_eb));
}
template <bool rc>
inline OrNodeBuilder operator||(const NodeTemplate<rc>& a,
const AndNodeBuilder& b) {
- return a || Node(b.d_eb);
+ return a || Node(const_cast<NodeBuilder<>&>(b.d_eb));
}
template <bool rc>
inline OrNodeBuilder operator||(const NodeTemplate<rc>& a,
const OrNodeBuilder& b) {
- return a || Node(b.d_eb);
+ return a || Node(const_cast<NodeBuilder<>&>(b.d_eb));
}
template <bool rc>
inline PlusNodeBuilder operator+(const NodeTemplate<rc>& a,
const PlusNodeBuilder& b) {
- return a + Node(b.d_eb);
+ return a + Node(const_cast<NodeBuilder<>&>(b.d_eb));
}
template <bool rc>
inline PlusNodeBuilder operator+(const NodeTemplate<rc>& a,
const MultNodeBuilder& b) {
- return a + Node(b.d_eb);
+ return a + Node(const_cast<NodeBuilder<>&>(b.d_eb));
}
template <bool rc>
inline PlusNodeBuilder operator-(const NodeTemplate<rc>& a,
const PlusNodeBuilder& b) {
- return a - Node(b.d_eb);
+ return a - Node(const_cast<NodeBuilder<>&>(b.d_eb));
}
template <bool rc>
inline PlusNodeBuilder operator-(const NodeTemplate<rc>& a,
const MultNodeBuilder& b) {
- return a - Node(b.d_eb);
+ return a - Node(const_cast<NodeBuilder<>&>(b.d_eb));
}
template <bool rc>
inline MultNodeBuilder operator*(const NodeTemplate<rc>& a,
const PlusNodeBuilder& b) {
- return a * Node(b.d_eb);
+ return a * Node(const_cast<NodeBuilder<>&>(b.d_eb));
}
template <bool rc>
inline MultNodeBuilder operator*(const NodeTemplate<rc>& a,
const MultNodeBuilder& b) {
- return a * Node(b.d_eb);
+ return a * Node(const_cast<NodeBuilder<>&>(b.d_eb));
}
template <bool rc>
@@ -1262,7 +1226,6 @@ void NodeBuilderBase<Builder>::decrRefCounts() {
d_inlineNv.d_nchildren = 0;
}
-// NON-CONST VERSION OF NODE EXTRACTOR
template <class Builder>
NodeBuilderBase<Builder>::operator Node() {
Assert(!isUsed(), "NodeBuilder is one-shot only; "
@@ -1434,183 +1397,6 @@ NodeBuilderBase<Builder>::operator Node() {
}
}
-// CONST VERSION OF NODE EXTRACTOR
-template <class Builder>
-NodeBuilderBase<Builder>::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 <unsigned nchild_thresh>
template <unsigned N>
void NodeBuilder<nchild_thresh>::internalCopy(const NodeBuilder<N>& 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 <vector>
#include <iostream>
+
+#include <limits.h>
+
+#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<unsigned> 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 <cxxtest/TestSuite.h>
+
+#ifndef __CVC4__TEST__MEMORY_H
+#define __CVC4__TEST__MEMORY_H
+
+#include <sys/time.h>
+#include <sys/resource.h>
+
+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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback