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;
}
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;
}
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
// 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;
}
}
+ // 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
*/
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
return d_pScope->isCurrent();
}
+public:
+
/**
* operator new using ContextMemoryManager (common case used by
* subclasses during save()). No delete is required for memory
*/
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
}
}
+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
#include <cxxtest/TestSuite.h>
#include "context/cdmap.h"
+#include "context/cdlist.h"
using namespace std;
using namespace CVC4;
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();
}
void testObliterateInsertedAtContextLevelZero() {
- cout << "\nobliteratCL0\n";
CDMap<int, int> map(d_context);
map.insert(3, 4);
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; }
+ }
};
projects / cvc5.git / commitdiff