From: Morgan Deters Date: Tue, 30 Mar 2010 08:22:06 +0000 (+0000) Subject: I think this finishes off the CDMap<>/Attribute leaks X-Git-Tag: cvc5-1.0.0~9163 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=09d8860f19b928114460386fa17847a8ffb02244;p=cvc5.git I think this finishes off the CDMap<>/Attribute leaks --- diff --git a/src/context/cdmap.h b/src/context/cdmap.h index 1dc44d087..4adf90e4f 100644 --- a/src/context/cdmap.h +++ b/src/context/cdmap.h @@ -25,73 +25,76 @@ #include "context/context.h" #include "util/Assert.h" +#include #include #include namespace CVC4 { namespace context { -// Auxiliary class: almost the same as CDO (see cdo.h), but on -// setNull() call it erases itself from the map. +// Auxiliary class: almost the same as CDO (see cdo.h) template > class CDMap; +template +inline std::ostream& operator<<(std::ostream& out, const std::pair& p) { + return out << "[" << p.first << "," << p.second << "]"; +} + template > class CDOmap : public ContextObj { Key d_key; Data d_data; - bool d_inMap; // whether the data must be in the map - CDMap* d_cdmap; + CDMap* d_map; // Doubly-linked list for keeping track of elements in order of insertion - CDOmap* d_prev; - CDOmap* d_next; + CDOmap* d_prev; + CDOmap* d_next; virtual ContextObj* save(ContextMemoryManager* pCMM) { - return new(pCMM) CDOmap(*this); + return new(pCMM) CDOmap(*this); } virtual void restore(ContextObj* data) { - CDOmap* p((CDOmap*) data); - if(p->d_inMap) { - d_data = p->d_data; - d_inMap = true; - } else { - // Erase itself from the map and put itself into trash. We cannot - // "delete this" here, because it will break context operations in - // a non-trivial way. - if(d_cdmap->d_map.count(d_key) > 0) { - d_cdmap->d_map.erase(d_key); - d_cdmap->d_trash.push_back(this); + CDOmap* p = static_cast(data); + if(p->d_map == NULL) { + Assert(d_map->d_map.find(d_key) != d_map->d_map.end() && + (*d_map->d_map.find(d_key)).second == this); + // no longer in map (popped beyond first level in which it was) + d_map->d_map.erase(d_key); + // If we call deleteSelf() here, it re-enters restore(). So, + // put it on a "trash heap" instead, for later deletion. + // + // FIXME multithreading + if(d_map->d_first == this) { + d_map->d_first = d_next; } - - d_prev->d_next = d_next; d_next->d_prev = d_prev; - - if(d_cdmap->d_first == this) { - d_cdmap->d_first = d_next; - - if(d_next == this) { - d_cdmap->d_first = NULL; - } - } + d_prev->d_next = d_next; + d_map->d_trash.push_back(this); + } else { + d_data = p->d_data; } } public: CDOmap(Context* context, - CDMap* cdmap, + CDMap* map, const Key& key, const Data& data) : ContextObj(context), d_key(key), - d_inMap(false), - d_cdmap(cdmap) { + d_map(NULL) { + // makeCurrent(), then set the data and then the map. Order is + // important; we can't initialize d_map in the constructor init + // list above, because we want the restore of d_map to NULL to + // signal us to remove the element from the map. set(data); + d_map = map; - CDOmap*& first = d_cdmap->d_first; + CDOmap*& first = d_map->d_first; if(first == NULL) { first = d_next = d_prev = this; } else { @@ -101,12 +104,13 @@ public: } } - ~CDOmap() throw(AssertionException) { destroy(); } + ~CDOmap() throw(AssertionException) { + destroy(); + } void set(const Data& data) { makeCurrent(); d_data = data; - d_inMap = true; } const Key& getKey() const { @@ -121,19 +125,19 @@ public: return get(); } - CDOmap& operator=(const Data& data) { + CDOmap& operator=(const Data& data) { set(data); return *this; } - CDOmap* next() const { - if(d_next == d_cdmap->d_first) { + CDOmap* next() const { + if(d_next == d_map->d_first) { return NULL; } else { return d_next; } } -};/* class CDOmap */ +};/* class CDOmap<> */ // Dummy subclass of ContextObj to serve as our data class class CDMapData : public ContextObj { @@ -151,6 +155,7 @@ public: CDMapData(Context* context) : ContextObj(context) {} CDMapData(const ContextObj& co) : ContextObj(co) {} + ~CDMapData() { destroy(); } }; /** @@ -161,16 +166,18 @@ public: template class CDMap : public ContextObj { + typedef CDOmap Element; + typedef __gnu_cxx::hash_map table_type; + friend class CDOmap; - typedef __gnu_cxx::hash_map*, HashFcn> table_type; table_type d_map; - // The vector of CDOmap objects to be destroyed - std::vector*> d_trash; - CDOmap* d_first; + Element* d_first; Context* d_context; + std::vector d_trash; + // Nothing to save; the elements take care of themselves virtual ContextObj* save(ContextMemoryManager* pCMM) { return new(pCMM) CDMapData(*this); @@ -179,14 +186,12 @@ class CDMap : public ContextObj { // Similarly, nothing to restore virtual void restore(ContextObj* data) {} - // Destroy stale CDOmap objects from trash void emptyTrash() { - for(typename std::vector*>::iterator - i = d_trash.begin(), iend = d_trash.end(); i != iend; ++i) { - /* - delete *i; - free(*i); - */ + //FIXME multithreading + for(typename std::vector::iterator i = d_trash.begin(); + i != d_trash.end(); + ++i) { + (*i)->deleteSelf(); } d_trash.clear(); } @@ -196,19 +201,19 @@ public: CDMap(Context* context) : ContextObj(context), d_first(NULL), - d_context(context) { + d_context(context), + d_trash() { } ~CDMap() throw(AssertionException) { - // Delete all the elements and clear the map - /*for(typename table_type::iterator - i = d_map.begin(), iend = d_map.end(); i != iend; ++i) { - - delete (*i).second; - free((*i).second); - - }*/ - d_map.clear(); + destroy(); + for(typename table_type::iterator i = d_map.begin(); + i != d_map.end(); + ++i) { + (*i).second->deleteSelf(); + } + //d_map.clear(); + Debug("gc") << "cdmap gone, emptying trash" << std::endl; emptyTrash(); } @@ -222,17 +227,15 @@ public: return d_map.count(k); } - typedef CDOmap& ElementReference; - // If a key is not present, a new object is created and inserted - CDOmap& operator[](const Key& k) { + Element& operator[](const Key& k) { emptyTrash(); typename table_type::iterator i = d_map.find(k); - CDOmap* obj; + Element* obj; if(i == d_map.end()) {// create new object - obj = new(true) CDOmap(d_context, this, k, Data()); + obj = new(true) Element(d_context, this, k, Data()); d_map[k] = obj; } else { obj = (*i).second; @@ -246,8 +249,7 @@ public: typename table_type::iterator i = d_map.find(k); if(i == d_map.end()) {// create new object - CDOmap* - obj = new(true) CDOmap(d_context, this, k, d); + Element* obj = new(true) Element(d_context, this, k, d); d_map[k] = obj; } else { (*i).second->set(d); @@ -256,12 +258,40 @@ public: // FIXME: no erase(), too much hassle to implement efficiently... + /** + * "Obliterating" is kind of like erasing, except it's not + * backtrackable; the key is permanently removed from the map. + * (Naturally, it can be re-added as a new element.) + */ + void obliterate(const Key& k) { + typename table_type::iterator i = d_map.find(k); + if(i != d_map.end()) { + Debug("gc") << "key " << k << " obliterated" << std::endl; + // We can't call ->deleteSelf() here, because it calls the + // ContextObj destructor, which calls CDOmap::destroy(), which + // restore()'s, which puts the CDOmap on the trash, which causes + // a double-delete. + (*i).second->~CDOmap(); + + typename table_type::iterator j = d_map.find(k); + // This if() succeeds for objects inserted when in the + // zero-scope: they were never save()'d there, so restore() + // never gets a NULL map and so they leak. + if(j != d_map.end()) { + Element* elt = (*j).second; + d_map.erase(j);//FIXME multithreading + // was already destructed, so don't call ->deleteSelf() + ::operator delete(elt); + } + } + } + class iterator { - const CDOmap* d_it; + const Element* d_it; public: - iterator(const CDOmap* p) : d_it(p) {} + iterator(const Element* p) : d_it(p) {} iterator(const iterator& i) : d_it(i.d_it) {} // Default constructor @@ -302,7 +332,7 @@ public: // Actual postfix increment: returns Proxy with the old value. // Now, an expression like *i++ will return the current *i, and - // then advance the orderedIterator. However, don't try to use + // then advance the iterator. However, don't try to use // Proxy for anything else. const Proxy operator++(int) { Proxy e(*(*this)); @@ -323,6 +353,7 @@ public: iterator find(const Key& k) const { typename table_type::const_iterator i = d_map.find(k); + if(i == d_map.end()) { return end(); } else { @@ -330,6 +361,11 @@ public: } } + iterator find(const Key& k) { + emptyTrash(); + return const_cast(this)->find(k); + } + };/* class CDMap<> */ }/* CVC4::context namespace */ diff --git a/src/context/context.cpp b/src/context/context.cpp index d2e2bfa1b..05024430c 100644 --- a/src/context/context.cpp +++ b/src/context/context.cpp @@ -177,6 +177,10 @@ ContextObj* ContextObj::restoreAndContinue() { void ContextObj::destroy() throw(AssertionException) { for(;;) { + // If valgrind reports invalid writes on the next few lines, + // here's a hint: make sure all classes derived from ContextObj in + // the system properly call destroy() in their destructors. + // That's needed to maintain this linked list properly. if(next() != NULL) { next()->prev() = prev(); } diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp index be54a973e..26cb96646 100644 --- a/src/expr/attribute.cpp +++ b/src/expr/attribute.cpp @@ -56,23 +56,22 @@ void AttributeManager::deleteAllAttributes(NodeValue* nv) { deleteFromTable(d_ptrs, nv); // FIXME CD-bools in optimized table - /* for(unsigned id = 0; id < attr::LastAttributeId::s_id; ++id) { - d_cdbools.erase(std::make_pair(id, nv)); + Debug("gc") << "looking for " << id << " x " << nv << ":" << *nv << std::endl; + d_cdbools.obliterate(std::make_pair(id, nv)); } for(unsigned id = 0; id < attr::LastAttributeId::s_id; ++id) { - d_cdints.erase(std::make_pair(id, nv)); + d_cdints.obliterate(std::make_pair(id, nv)); } for(unsigned id = 0; id < attr::LastAttributeId::s_id; ++id) { - d_cdexprs.erase(std::make_pair(id, nv)); + d_cdexprs.obliterate(std::make_pair(id, nv)); } for(unsigned id = 0; id < attr::LastAttributeId::s_id; ++id) { - d_cdstrings.erase(std::make_pair(id, nv)); + d_cdstrings.obliterate(std::make_pair(id, nv)); } for(unsigned id = 0; id < attr::LastAttributeId::s_id; ++id) { - d_cdptrs.erase(std::make_pair(id, nv)); + d_cdptrs.obliterate(std::make_pair(id, nv)); } - */ } }/* CVC4::expr::attr namespace */ diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 6e24cce74..c51c7fb77 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -421,8 +421,8 @@ inline void NodeManager::setAttribute(TNode n, /** Make a function type from domain to range. * TODO: Function types should be unique for this manager. */ -FunctionType* NodeManager::mkFunctionType(Type* domain, - Type* range) const { +inline FunctionType* NodeManager::mkFunctionType(Type* domain, + Type* range) const { std::vector argTypes; argTypes.push_back(domain); return new FunctionType(argTypes, range); @@ -430,13 +430,14 @@ FunctionType* NodeManager::mkFunctionType(Type* domain, /** Make a function type with input types from argTypes. * TODO: Function types should be unique for this manager. */ -FunctionType* NodeManager::mkFunctionType(const std::vector& argTypes, - Type* range) const { +inline FunctionType* +NodeManager::mkFunctionType(const std::vector& argTypes, + Type* range) const { Assert( argTypes.size() > 0 ); return new FunctionType(argTypes, range); } -Type* NodeManager::mkSort(const std::string& name) const { +inline Type* NodeManager::mkSort(const std::string& name) const { return new SortType(name); } diff --git a/src/expr/type.cpp b/src/expr/type.cpp index 2549f02ca..2fa21c8a6 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -31,7 +31,8 @@ Type::Type() : } Type::Type(std::string name) : - d_name(name) { + d_name(name), + d_rc(0) { } std::string Type::getName() const { diff --git a/src/theory/uf/ecdata.h b/src/theory/uf/ecdata.h index 248e1e545..26d957c2e 100644 --- a/src/theory/uf/ecdata.h +++ b/src/theory/uf/ecdata.h @@ -175,7 +175,10 @@ public: */ ECData(context::Context* context, TNode n); - ~ECData() { Debug("ufgc") << "Calling ECData destructor" << std::endl;} + ~ECData() { + Debug("ufgc") << "Calling ECData destructor" << std::endl; + destroy(); + } /** * An ECData takes over the watch list of another ECData. diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index 214f2ac58..122d92cae 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -10,15 +10,17 @@ UNIT_TESTS = \ parser/parser_black \ context/context_black \ context/context_mm_black \ + context/cdo_black \ context/cdlist_black \ + context/cdmap_black \ theory/theory_black \ theory/theory_uf_white \ util/assert_white \ util/configuration_white \ - util/output_white \ - util/integer_black \ - util/integer_white \ - util/rational_white + util/output_white +# util/integer_black \ +# util/integer_white \ +# util/rational_white # Things that aren't tests but that tests rely on and need to # go into the distribution diff --git a/test/unit/context/cdmap_black.h b/test/unit/context/cdmap_black.h new file mode 100644 index 000000000..7040e4cc1 --- /dev/null +++ b/test/unit/context/cdmap_black.h @@ -0,0 +1,398 @@ +/********************* */ +/** cdmap_black.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. + ** + ** Black box testing of CVC4::context::CDMap<>. + **/ + +#include + +#include "context/cdmap.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::context; + +class CDMapBlack : public CxxTest::TestSuite { + + Context* d_context; + +public: + + void setUp() { + d_context = new Context; + //Debug.on("cdmap"); + } + + void tearDown() { + delete d_context; + } + + void testSimpleSequence() { + CDMap map(d_context); + + map.insert(3, 4); + + TS_ASSERT(map.find(3) != map.end()); + TS_ASSERT(map.find(5) == map.end()); + TS_ASSERT(map.find(9) == map.end()); + TS_ASSERT(map.find(1) == map.end()); + + { + d_context->push(); + + TS_ASSERT(map.find(3) != map.end()); + TS_ASSERT(map.find(5) == map.end()); + TS_ASSERT(map.find(9) == map.end()); + TS_ASSERT(map.find(1) == map.end()); + + map.insert(5, 6); + map.insert(9, 8); + + TS_ASSERT(map.find(3) != map.end()); + TS_ASSERT(map.find(5) != map.end()); + TS_ASSERT(map.find(9) != map.end()); + TS_ASSERT(map.find(1) == map.end()); + + { + d_context->push(); + + TS_ASSERT(map.find(3) != map.end()); + TS_ASSERT(map.find(5) != map.end()); + TS_ASSERT(map.find(9) != map.end()); + TS_ASSERT(map.find(1) == map.end()); + + map.insert(1, 2); + + TS_ASSERT(map.find(3) != map.end()); + TS_ASSERT(map.find(5) != map.end()); + TS_ASSERT(map.find(9) != map.end()); + TS_ASSERT(map.find(1) != map.end()); + + { + d_context->push(); + + TS_ASSERT(map.find(3) != map.end()); + TS_ASSERT(map.find(5) != map.end()); + TS_ASSERT(map.find(9) != map.end()); + TS_ASSERT(map.find(1) != map.end()); + + map.insert(1, 45); + + TS_ASSERT(map.find(3) != map.end()); + TS_ASSERT(map.find(5) != map.end()); + TS_ASSERT(map.find(9) != map.end()); + TS_ASSERT(map.find(1) != map.end()); + + d_context->pop(); + } + + TS_ASSERT(map.find(3) != map.end()); + TS_ASSERT(map.find(5) != map.end()); + TS_ASSERT(map.find(9) != map.end()); + TS_ASSERT(map.find(1) != map.end()); + + d_context->pop(); + } + + TS_ASSERT(map.find(3) != map.end()); + TS_ASSERT(map.find(5) != map.end()); + TS_ASSERT(map.find(9) != map.end()); + TS_ASSERT(map.find(1) == map.end()); + + d_context->pop(); + } + + TS_ASSERT(map.find(3) != map.end()); + TS_ASSERT(map.find(5) == map.end()); + TS_ASSERT(map.find(9) == map.end()); + TS_ASSERT(map.find(1) == map.end()); + } + + // no intervening find() in this one + // (under the theory that this could trigger a bug) + void testSimpleSequenceFewerFinds() { + CDMap map(d_context); + + map.insert(3, 4); + + { + d_context->push(); + + map.insert(5, 6); + map.insert(9, 8); + + { + d_context->push(); + + map.insert(1, 2); + + TS_ASSERT(map.find(1) != map.end()); + TS_ASSERT(map.find(9) != map.end()); + TS_ASSERT(map.find(5) != map.end()); + TS_ASSERT(map.find(7) == map.end()); + + { + d_context->push(); + + d_context->pop(); + } + + d_context->pop(); + } + + d_context->pop(); + } + } + + void testObliterate() { + CDMap map(d_context); + + map.insert(3, 4); + + TS_ASSERT(map.find(3) != map.end()); + TS_ASSERT(map.find(5) == map.end()); + TS_ASSERT(map.find(9) == map.end()); + TS_ASSERT(map.find(1) == map.end()); + + { + d_context->push(); + + TS_ASSERT(map.find(3) != map.end()); + TS_ASSERT(map.find(5) == map.end()); + TS_ASSERT(map.find(9) == map.end()); + TS_ASSERT(map.find(1) == map.end()); + + map.insert(5, 6); + map.insert(9, 8); + + TS_ASSERT(map.find(3) != map.end()); + TS_ASSERT(map.find(5) != map.end()); + TS_ASSERT(map.find(9) != map.end()); + TS_ASSERT(map.find(1) == map.end()); + + { + d_context->push(); + + TS_ASSERT(map.find(3) != map.end()); + TS_ASSERT(map.find(5) != map.end()); + TS_ASSERT(map.find(9) != map.end()); + TS_ASSERT(map.find(1) == map.end()); + + map.insert(1, 2); + + TS_ASSERT(map.find(3) != map.end()); + TS_ASSERT(map.find(5) != map.end()); + TS_ASSERT(map.find(9) != map.end()); + TS_ASSERT(map.find(1) != map.end()); + + map.obliterate(5); + + TS_ASSERT(map.find(3) != map.end()); + TS_ASSERT(map.find(5) == map.end()); + TS_ASSERT(map.find(9) != map.end()); + TS_ASSERT(map.find(1) != map.end()); + + { + d_context->push(); + + TS_ASSERT(map.find(3) != map.end()); + TS_ASSERT(map.find(5) == map.end()); + TS_ASSERT(map.find(9) != map.end()); + TS_ASSERT(map.find(1) != map.end()); + + d_context->pop(); + } + + TS_ASSERT(map.find(3) != map.end()); + TS_ASSERT(map.find(5) == map.end()); + TS_ASSERT(map.find(9) != map.end()); + TS_ASSERT(map.find(1) != map.end()); + + d_context->pop(); + } + + TS_ASSERT(map.find(3) != map.end()); + TS_ASSERT(map.find(5) == map.end()); + TS_ASSERT(map.find(9) != map.end()); + TS_ASSERT(map.find(1) == map.end()); + + d_context->pop(); + } + + TS_ASSERT(map.find(3) != map.end()); + TS_ASSERT(map.find(5) == map.end()); + TS_ASSERT(map.find(9) == map.end()); + TS_ASSERT(map.find(1) == map.end()); + } + + void testObliteratePrimordial() { + CDMap map(d_context); + + map.insert(3, 4); + + TS_ASSERT(map.find(3) != map.end()); + TS_ASSERT(map.find(5) == map.end()); + TS_ASSERT(map.find(9) == map.end()); + TS_ASSERT(map.find(1) == map.end()); + + { + d_context->push(); + + TS_ASSERT(map.find(3) != map.end()); + TS_ASSERT(map.find(5) == map.end()); + TS_ASSERT(map.find(9) == map.end()); + TS_ASSERT(map.find(1) == map.end()); + + map.insert(5, 6); + map.insert(9, 8); + + TS_ASSERT(map.find(3) != map.end()); + TS_ASSERT(map.find(5) != map.end()); + TS_ASSERT(map.find(9) != map.end()); + TS_ASSERT(map.find(1) == map.end()); + + { + d_context->push(); + + TS_ASSERT(map.find(3) != map.end()); + TS_ASSERT(map.find(5) != map.end()); + TS_ASSERT(map.find(9) != map.end()); + TS_ASSERT(map.find(1) == map.end()); + + map.insert(1, 2); + + TS_ASSERT(map.find(3) != map.end()); + TS_ASSERT(map.find(5) != map.end()); + TS_ASSERT(map.find(9) != map.end()); + TS_ASSERT(map.find(1) != map.end()); + + map.obliterate(3); + + TS_ASSERT(map.find(3) == map.end()); + TS_ASSERT(map.find(5) != map.end()); + TS_ASSERT(map.find(9) != map.end()); + TS_ASSERT(map.find(1) != map.end()); + + { + d_context->push(); + + TS_ASSERT(map.find(3) == map.end()); + TS_ASSERT(map.find(5) != map.end()); + TS_ASSERT(map.find(9) != map.end()); + TS_ASSERT(map.find(1) != map.end()); + + d_context->pop(); + } + + TS_ASSERT(map.find(3) == map.end()); + TS_ASSERT(map.find(5) != map.end()); + TS_ASSERT(map.find(9) != map.end()); + TS_ASSERT(map.find(1) != map.end()); + + d_context->pop(); + } + + TS_ASSERT(map.find(3) == map.end()); + TS_ASSERT(map.find(5) != map.end()); + TS_ASSERT(map.find(9) != map.end()); + TS_ASSERT(map.find(1) == map.end()); + + d_context->pop(); + } + + TS_ASSERT(map.find(3) == map.end()); + TS_ASSERT(map.find(5) == map.end()); + TS_ASSERT(map.find(9) == map.end()); + TS_ASSERT(map.find(1) == map.end()); + } + + void testObliterateCurrent() { + CDMap map(d_context); + + map.insert(3, 4); + + TS_ASSERT(map.find(3) != map.end()); + TS_ASSERT(map.find(5) == map.end()); + TS_ASSERT(map.find(9) == map.end()); + TS_ASSERT(map.find(1) == map.end()); + + { + d_context->push(); + + TS_ASSERT(map.find(3) != map.end()); + TS_ASSERT(map.find(5) == map.end()); + TS_ASSERT(map.find(9) == map.end()); + TS_ASSERT(map.find(1) == map.end()); + + map.insert(5, 6); + map.insert(9, 8); + + TS_ASSERT(map.find(3) != map.end()); + TS_ASSERT(map.find(5) != map.end()); + TS_ASSERT(map.find(9) != map.end()); + TS_ASSERT(map.find(1) == map.end()); + + { + d_context->push(); + + TS_ASSERT(map.find(3) != map.end()); + TS_ASSERT(map.find(5) != map.end()); + TS_ASSERT(map.find(9) != map.end()); + TS_ASSERT(map.find(1) == map.end()); + + map.insert(1, 2); + + TS_ASSERT(map.find(3) != map.end()); + TS_ASSERT(map.find(5) != map.end()); + TS_ASSERT(map.find(9) != map.end()); + TS_ASSERT(map.find(1) != map.end()); + + map.obliterate(1); + + TS_ASSERT(map.find(3) != map.end()); + TS_ASSERT(map.find(5) != map.end()); + TS_ASSERT(map.find(9) != map.end()); + TS_ASSERT(map.find(1) == map.end()); + + { + d_context->push(); + + TS_ASSERT(map.find(3) != map.end()); + TS_ASSERT(map.find(5) != map.end()); + TS_ASSERT(map.find(9) != map.end()); + TS_ASSERT(map.find(1) == map.end()); + + d_context->pop(); + } + + TS_ASSERT(map.find(3) != map.end()); + TS_ASSERT(map.find(5) != map.end()); + TS_ASSERT(map.find(9) != map.end()); + TS_ASSERT(map.find(1) == map.end()); + + d_context->pop(); + } + + TS_ASSERT(map.find(3) != map.end()); + TS_ASSERT(map.find(5) != map.end()); + TS_ASSERT(map.find(9) != map.end()); + TS_ASSERT(map.find(1) == map.end()); + + d_context->pop(); + } + + TS_ASSERT(map.find(3) != map.end()); + TS_ASSERT(map.find(5) == map.end()); + TS_ASSERT(map.find(9) == map.end()); + TS_ASSERT(map.find(1) == map.end()); + } +}; diff --git a/test/unit/context/cdo_black.h b/test/unit/context/cdo_black.h new file mode 100644 index 000000000..4cdb8f343 --- /dev/null +++ b/test/unit/context/cdo_black.h @@ -0,0 +1,57 @@ +/********************* */ +/** cdo_black.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. + ** + ** Black box testing of CVC4::context::CDO<>. + **/ + +#include + +#include +#include +#include "context/context.h" +#include "context/cdlist.h" +#include "context/cdo.h" +#include "util/Assert.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::context; + +class CDOBlack : public CxxTest::TestSuite { +private: + + Context* d_context; + +public: + + void setUp() { + d_context = new Context; + } + + void tearDown() { + delete d_context; + } + + void testIntCDO() { + // Test that push/pop maintains the original value + CDO a1(d_context); + a1 = 5; + TS_ASSERT(d_context->getLevel() == 0); + d_context->push(); + a1 = 10; + TS_ASSERT(d_context->getLevel() == 1); + TS_ASSERT(a1 == 10); + d_context->pop(); + TS_ASSERT(d_context->getLevel() == 0); + TS_ASSERT(a1 == 5); + } +}; diff --git a/test/unit/context/context_black.h b/test/unit/context/context_black.h index c9b47e400..338c09849 100644 --- a/test/unit/context/context_black.h +++ b/test/unit/context/context_black.h @@ -41,20 +41,6 @@ public: delete d_context; } - void testIntCDO() { - // Test that push/pop maintains the original value - CDO a1(d_context); - a1 = 5; - TS_ASSERT(d_context->getLevel() == 0); - d_context->push(); - a1 = 10; - TS_ASSERT(d_context->getLevel() == 1); - TS_ASSERT(a1 == 10); - d_context->pop(); - TS_ASSERT(d_context->getLevel() == 0); - TS_ASSERT(a1 == 5); - } - void testContextPushPop() { // Test what happens when the context is popped below 0 // the interface doesn't declare any exceptions