summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/context/cdlist.h25
-rw-r--r--src/context/cdmap.h47
-rw-r--r--src/context/context.h17
-rw-r--r--test/unit/context/cdmap_black.h144
4 files changed, 216 insertions, 17 deletions
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<Key, Data, HashFcn>* 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<Key, Data, HashFcn>* 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
@@ -380,6 +380,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
* all Scope lists. Note that this doesn't actually free the memory
@@ -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 <cxxtest/TestSuite.h>
#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<int, int> 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, CDList<myint>*, int_hasher> map(d_context);
+
+ CDList<myint> *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<myint>(true, d_context);
+ list2 = new(d_context->getCMM()) CDList<myint>(true, d_context);
+ list3 = new(d_context->getCMM()) CDList<myint>(true, d_context);
+ list4 = new(d_context->getCMM()) CDList<myint>(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; }
+ }
};
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback