From: Morgan Deters Date: Thu, 8 Jul 2010 04:33:10 +0000 (+0000) Subject: context work to support cdmaps with elements allocated in context memory X-Git-Tag: cvc5-1.0.0~8916 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8a0dcb9cb4bbf83f03b31343eaa6437ae829f1c9;p=cvc5.git context work to support cdmaps with elements allocated in context memory --- diff --git a/src/context/cdlist.h b/src/context/cdlist.h index e3bf4d56b..7e382697c 100644 --- a/src/context/cdlist.h +++ b/src/context/cdlist.h @@ -130,13 +130,24 @@ public: /** * Main constructor: d_list starts as NULL, size is 0 */ - CDList(Context* context, bool callDestructor = true) : - ContextObj(context), - d_list(NULL), - d_callDestructor(callDestructor), - d_size(0), - d_sizeAlloc(0) { - } + CDList(Context* context, bool callDestructor = true) : + ContextObj(context), + d_list(NULL), + d_callDestructor(callDestructor), + d_size(0), + d_sizeAlloc(0) { + } + + /** + * Main constructor: d_list starts as NULL, size is 0 + */ + CDList(bool allocatedInCMM, Context* context, bool callDestructor = true) : + ContextObj(allocatedInCMM, context), + d_list(NULL), + d_callDestructor(callDestructor), + d_size(0), + d_sizeAlloc(0) { + } /** * Destructor: delete the list diff --git a/src/context/cdmap.h b/src/context/cdmap.h index 5e5a07f2f..66f897818 100644 --- a/src/context/cdmap.h +++ b/src/context/cdmap.h @@ -114,6 +114,9 @@ class CDOmap : public ContextObj { Data d_data; CDMap* d_map; + /** never put this cdmap element on the trash */ + bool d_noTrash; + // Doubly-linked list for keeping track of elements in order of insertion CDOmap* d_prev; CDOmap* d_next; @@ -147,9 +150,13 @@ class CDOmap : public ContextObj { } d_next->d_prev = d_prev; d_prev->d_next = d_next; - Debug("gc") << "CDMap<> trash push_back " << this << std::endl; - //this->deleteSelf(); - d_map->d_trash.push_back(this); + if(d_noTrash) { + Debug("gc") << "CDMap<> no-trash " << this << std::endl; + } else { + Debug("gc") << "CDMap<> trash push_back " << this << std::endl; + //this->deleteSelf(); + d_map->d_trash.push_back(this); + } } else { d_data = p->d_data; } @@ -172,10 +179,15 @@ public: CDMap* map, const Key& key, const Data& data, - bool atLevelZero = false) : - ContextObj(context), + bool atLevelZero = false, + bool allocatedInCMM = false) : + ContextObj(allocatedInCMM, context), d_key(key), - d_map(NULL) { + d_map(NULL), + d_noTrash(allocatedInCMM) { + + // untested, probably unsafe. + Assert(!(atLevelZero && allocatedInCMM)); if(atLevelZero) { // "Initializing" map insertion: this entry will never be @@ -189,6 +201,14 @@ public: // 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. + + if(allocatedInCMM) { + // Force a save/restore point, even though the object is + // allocated here. This is so that we can detect when the + // object falls out of the map (otherwise we wouldn't get it). + makeSaveRestorePoint(); + } + set(data); } d_map = map; @@ -378,6 +398,21 @@ public: } } + // Use this for pointer data d allocated in context memory at this + // level. THIS IS HIGHLY EXPERIMENTAL. It seems to work if ALL + // your data objects are allocated from context memory. + void insertDataFromContextMemory(const Key& k, const Data& d) { + emptyTrash(); + + AlwaysAssert(d_map.find(k) == d_map.end()); + + Element* obj = new(d_context->getCMM()) Element(d_context, this, k, d, + false /* atLevelZero */, + true /* allocatedInCMM */); + + d_map[k] = obj; + } + /** * Version of insert() for CDMap<> that inserts data value d at * context level zero. This is a special escape hatch for inserting diff --git a/src/context/context.h b/src/context/context.h index 1aa5fe44d..20e84d7e5 100644 --- a/src/context/context.h +++ b/src/context/context.h @@ -379,6 +379,15 @@ protected: */ inline void makeCurrent() throw(AssertionException); + /** + * Just calls update(), but given a different name for the derived + * class-facing interface. This is a "forced" makeCurrent(), useful + * for ContextObjs allocated in CMM that need a special "bottom" + * case when they disappear out of existence (kind of a destructor). + * See CDOmap (in cdmap.h) for an example. + */ + inline void makeSaveRestorePoint() throw(AssertionException); + /** * Should be called from sub-class destructor: calls restore until restored * to initial version (version at context level 0). Also removes object from @@ -438,6 +447,8 @@ protected: return d_pScope->isCurrent(); } +public: + /** * operator new using ContextMemoryManager (common case used by * subclasses during save()). No delete is required for memory @@ -459,8 +470,6 @@ protected: */ static void operator delete(void* pMem, ContextMemoryManager* pCMM) {} -public: - /** * Create a new ContextObj. The initial scope is set to the bottom * scope of the Context. Note that in the common case, the copy @@ -592,6 +601,10 @@ inline void ContextObj::makeCurrent() throw(AssertionException) { } } +inline void ContextObj::makeSaveRestorePoint() throw(AssertionException) { + update(); +} + inline Scope::~Scope() throw(AssertionException) { // Call restore() method on each ContextObj object in the list. // Note that it is the responsibility of restore() to return the diff --git a/test/unit/context/cdmap_black.h b/test/unit/context/cdmap_black.h index b4370e93c..7b8953dc0 100644 --- a/test/unit/context/cdmap_black.h +++ b/test/unit/context/cdmap_black.h @@ -19,6 +19,7 @@ #include #include "context/cdmap.h" +#include "context/cdlist.h" using namespace std; using namespace CVC4; @@ -693,7 +694,6 @@ public: TS_ASSERT(map[5] == 6); TS_ASSERT(map[9] == 8); TS_ASSERT(map[1] == 2); - std::cout << "map[23] is " << map[23] << std::endl; TS_ASSERT(map[23] == 472); d_context->pop(); @@ -739,7 +739,6 @@ public: } void testObliterateInsertedAtContextLevelZero() { - cout << "\nobliteratCL0\n"; CDMap map(d_context); map.insert(3, 4); @@ -917,4 +916,145 @@ public: TS_ASSERT(map.find(23) == map.end()); TS_ASSERT(map[3] == 4); } + + struct int_hasher { + size_t operator()(int i) const { return i; } + }; + + struct myint { + int x; + myint(int i) : x(i) {} + ~myint() { std::cout << "dtor " << x << std::endl; } + myint& operator=(int i) { x = i; return *this; } + bool operator==(int i) const { return x == i; } + }; + + void testMapOfLists() { + try{ + //Debug.on("gc"); + //Debug.on("context"); + + CDMap*, int_hasher> map(d_context); + + CDList *list1, *list2, *list3, *list4; + + TS_ASSERT(map.find(1) == map.end()); + TS_ASSERT(map.find(2) == map.end()); + TS_ASSERT(map.find(3) == map.end()); + TS_ASSERT(map.find(4) == map.end()); + + { + d_context->push(); + + int* x = (int*) d_context->getCMM()->newData(sizeof(int)); + + list1 = new(d_context->getCMM()) CDList(true, d_context); + list2 = new(d_context->getCMM()) CDList(true, d_context); + list3 = new(d_context->getCMM()) CDList(true, d_context); + list4 = new(d_context->getCMM()) CDList(true, d_context); + + list1->push_back(1); + list2->push_back(2); + list3->push_back(3); + list4->push_back(4); + + map.insertDataFromContextMemory(1, list1); + map.insertDataFromContextMemory(2, list2); + + { + d_context->push(); + + list1->push_back(10); + list2->push_back(20); + list3->push_back(30); + list4->push_back(40); + + map.insertDataFromContextMemory(3, list3); + map.insertDataFromContextMemory(4, list4); + + x = (int*) d_context->getCMM()->newData(sizeof(int)); + + TS_ASSERT(map.find(1) != map.end()); + TS_ASSERT(map.find(2) != map.end()); + TS_ASSERT(map.find(3) != map.end()); + TS_ASSERT(map.find(4) != map.end()); + + TS_ASSERT(map[1] == list1); + TS_ASSERT(map[2] == list2); + TS_ASSERT(map[3] == list3); + TS_ASSERT(map[4] == list4); + + TS_ASSERT((*list1)[0] == 1); + TS_ASSERT((*list2)[0] == 2); + TS_ASSERT((*list3)[0] == 3); + TS_ASSERT((*list4)[0] == 4); + + TS_ASSERT((*list1)[1] == 10); + TS_ASSERT((*list2)[1] == 20); + TS_ASSERT((*list3)[1] == 30); + TS_ASSERT((*list4)[1] == 40); + + TS_ASSERT(list1->size() == 2); + TS_ASSERT(list2->size() == 2); + TS_ASSERT(list3->size() == 2); + TS_ASSERT(list4->size() == 2); + + d_context->pop(); + } + + TS_ASSERT(map.find(1) != map.end()); + TS_ASSERT(map.find(2) != map.end()); + TS_ASSERT(map.find(3) == map.end()); + TS_ASSERT(map.find(4) == map.end()); + + TS_ASSERT(map[1] == list1); + TS_ASSERT(map[2] == list2); + + TS_ASSERT((*list1)[0] == 1); + TS_ASSERT((*list2)[0] == 2); + TS_ASSERT((*list3)[0] == 3); + TS_ASSERT((*list4)[0] == 4); + + TS_ASSERT(list1->size() == 1); + TS_ASSERT(list2->size() == 1); + TS_ASSERT(list3->size() == 1); + TS_ASSERT(list4->size() == 1); + + d_context->pop(); + } + + { + d_context->push(); + + // This re-uses context memory used above. the map.clear() + // triggers an emptyTrash() which fails if the CDOmaps are put + // in the trash. (We use insertDataFromContextMemory() above to + // keep them out of the trash.) + cout << "allocating\n"; + int* x = (int*) d_context->getCMM()->newData(sizeof(int)); + cout << "x == " << x << std::endl; + for(int i = 0; i < 1000; ++i) { + *(int*)d_context->getCMM()->newData(sizeof(int)) = 512; + } + x = (int*) d_context->getCMM()->newData(sizeof(int)); + cout << "x == " << x << std::endl; + + TS_ASSERT(map.find(1) == map.end()); + TS_ASSERT(map.find(2) == map.end()); + TS_ASSERT(map.find(3) == map.end()); + TS_ASSERT(map.find(4) == map.end()); + + map.clear(); + + TS_ASSERT(map.find(1) == map.end()); + TS_ASSERT(map.find(2) == map.end()); + TS_ASSERT(map.find(3) == map.end()); + TS_ASSERT(map.find(4) == map.end()); + + d_context->pop(); + } + + TS_ASSERT(d_context->getLevel() == 0); + } catch(Exception& e) { cout << e << std::endl; throw e; } + } };