diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-03-02 20:38:23 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-03-02 20:38:23 +0000 |
commit | 068107e1d1f705eb9054b4309a26236230687d80 (patch) | |
tree | 4c422f3efd6a8319abe426c518f9d2feb7ab5a6d /src/context/cdhashmap.h | |
parent | 53176a3d39935bd77f1c057d0b806c380b346e23 (diff) |
CDMap -> CDHashMap
CDSet -> CDHashSet
Diffstat (limited to 'src/context/cdhashmap.h')
-rw-r--r-- | src/context/cdhashmap.h | 586 |
1 files changed, 586 insertions, 0 deletions
diff --git a/src/context/cdhashmap.h b/src/context/cdhashmap.h new file mode 100644 index 000000000..de21515c7 --- /dev/null +++ b/src/context/cdhashmap.h @@ -0,0 +1,586 @@ +/********************* */ +/*! \file cdmap.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): taking, dejan + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 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.\endverbatim + ** + ** \brief Context-dependent map class. + ** + ** Context-dependent map class. Generic templated class for a map + ** which must be saved and restored as contexts are pushed and + ** popped. Requires that operator= be defined for the data class, + ** and operator== for the key class. For key types that don't have a + ** __gnu_cxx::hash<>, you should provide an explicit HashFcn. + ** + ** Internal documentation: + ** + ** CDMap<> is something of a work in progress at present (26 May + ** 2010), due to some recent discoveries of problems with its + ** internal state. Here are some notes on the internal use of + ** CDOhash_maps that may be useful in figuring out this mess: + ** + ** So you have a CDMap<>. + ** + ** You insert some (key,value) pairs. Each allocates a CDOhash_map<> + ** and goes on a doubly-linked list headed by map.d_first and + ** threaded via CDOhash_map.{d_prev,d_next}. CDOhash_maps are constructed + ** with a NULL d_map pointer, but then immediately call + ** makeCurrent() and set the d_map pointer back to the map. At + ** context level 0, this doesn't lead to anything special. In + ** higher context levels, this stores away a CDOhash_map with a NULL + ** map pointer at level 0, and a non-NULL map pointer in the + ** current context level. (Remember that for later.) + ** + ** When a key is associated to a new value in a CDMap, its + ** associated CDOhash_map calls makeCurrent(), then sets the new + ** value. The save object is also a CDOhash_map (allocated in context + ** memory). + ** + ** Now, CDOhash_maps disappear in a variety of ways. + ** + ** First, you might pop beyond a "modification of the value" + ** scope level, requiring a re-association of the key to an old + ** value. This is easy. CDOhash_map::restore() does the work, and + ** the context memory of the save object is reclaimed as usual. + ** + ** Second, you might pop beyond a "insert the key" scope level, + ** requiring that the key be completely removed from the map and + ** its CDOhash_map object memory freed. Here, the CDOhash_map is restored + ** to a "NULL-map" state (see above), signaling it to remove + ** itself from the map completely and put itself on a "trash + ** list" for the map. + ** + ** Third, you might obliterate() the key. This calls the CDOhash_map + ** destructor, which calls destroy(), which does a successive + ** restore() until level 0. If the key was in the map since + ** level 0, the restore() won't remove it, so in that case + ** obliterate() removes it from the map and frees the CDOhash_map's + ** memory. + ** + ** Fourth, you might delete the cdhashmap(calling CDMap::~CDMap()). + ** This first calls destroy(), as per ContextObj contract, but + ** cdhashmapdoesn't save/restore itself, so that does nothing at the + ** CDMap-level. Then it empties the trash. Then, for each + ** element in the map, it marks it as being "part of a complete + ** map destruction", which essentially short-circuits + ** CDOhash_map::restore() (see CDOhash_map::restore()), then deallocates + ** it. Finally it asserts that the trash is empty (which it + ** should be, since restore() was short-circuited). + ** + ** Fifth, you might clear() the CDMap. This does exactly the + ** same as CDMap::~CDMap(), except that it doesn't call destroy() + ** on itself. + ** + ** CDMap::emptyTrash() simply goes through and calls + ** ->deleteSelf() on all elements in the trash. + ** ContextObj::deleteSelf() calls the CDOhash_map destructor, then + ** frees the memory associated to the CDOhash_map. CDOhash_map::~CDOhash_map() + ** calls destroy(), which restores as much as possible. (Note, + ** though, that since objects placed on the trash have already + ** restored to the fullest extent possible, it does nothing.) + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__CONTEXT__CDMAP_H +#define __CVC4__CONTEXT__CDMAP_H + +#include <vector> +#include <iterator> +#include <ext/hash_map> + +#include "context/context.h" +#include "util/Assert.h" +#include "context/cdhashmap_forward.h" + +namespace CVC4 { +namespace context { + +// Auxiliary class: almost the same as CDO (see cdo.h) + +template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> > +class CDOhash_map : public ContextObj { + friend class CDHashMap<Key, Data, HashFcn>; + + Key d_key; + Data d_data; + CDHashMap<Key, Data, HashFcn>* d_map; + + /** never put this cdhashmapelement on the trash */ + bool d_noTrash; + + // Doubly-linked list for keeping track of elements in order of insertion + CDOhash_map* d_prev; + CDOhash_map* d_next; + + virtual ContextObj* save(ContextMemoryManager* pCMM) { + return new(pCMM) CDOhash_map(*this); + } + + virtual void restore(ContextObj* data) { + if(d_map != NULL) { + CDOhash_map* p = static_cast<CDOhash_map*>(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) { + Debug("gc") << "remove first-elem " << this << " from map " << d_map << " with next-elem " << d_next << std::endl; + if(d_next == this) { + Assert(d_prev == this); + d_map->d_first = NULL; + } else { + d_map->d_first = d_next; + } + } else { + Debug("gc") << "remove nonfirst-elem " << this << " from map " << d_map << std::endl; + } + d_next->d_prev = d_prev; + d_prev->d_next = d_next; + 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; + } + } + } + + /** ensure copy ctor is only called by us */ + CDOhash_map(const CDOhash_map& other) : + ContextObj(other), + d_key(other.d_key), + d_data(other.d_data), + d_map(other.d_map), + d_prev(NULL), + d_next(NULL) { + } + +public: + + CDOhash_map(Context* context, + CDHashMap<Key, Data, HashFcn>* map, + const Key& key, + const Data& data, + bool atLevelZero = false, + bool allocatedInCMM = false) : + ContextObj(allocatedInCMM, context), + d_key(key), + d_map(NULL), + d_noTrash(allocatedInCMM) { + + // untested, probably unsafe. + Assert(!(atLevelZero && allocatedInCMM)); + + if(atLevelZero) { + // "Initializing" map insertion: this entry will never be + // removed from the map, it's inserted at level 0 as an + // "initializing" element. See + // CDMap<>::insertAtContextLevelZero(). + d_data = data; + } else { + // Normal map insertion: first makeCurrent(), then set the data + // and then, later, 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. + + 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; + + CDOhash_map*& first = d_map->d_first; + if(first == NULL) { + first = d_next = d_prev = this; + Debug("gc") << "add first-elem " << this << " to map " << d_map << std::endl; + } else { + Debug("gc") << "add nonfirst-elem " << this << " to map " << d_map << " with first-elem " << first << "[" << first->d_prev << " " << first->d_next << std::endl; + d_prev = first->d_prev; + d_next = first; + d_prev->d_next = this; + first->d_prev = this; + } + } + + ~CDOhash_map() throw(AssertionException) { + destroy(); + } + + void set(const Data& data) { + makeCurrent(); + d_data = data; + } + + const Key& getKey() const { + return d_key; + } + + const Data& get() const { + return d_data; + } + + operator Data() { + return get(); + } + + const Data& operator=(const Data& data) { + set(data); + return data; + } + + CDOhash_map* next() const { + if(d_next == d_map->d_first) { + return NULL; + } else { + return d_next; + } + } +};/* class CDOhash_map<> */ + + +/** + * Generic templated class for a map which must be saved and restored + * as contexts are pushed and popped. Requires that operator= be + * defined for the data class, and operator== for the key class. + */ +template <class Key, class Data, class HashFcn> +class CDHashMap : public ContextObj { + + typedef CDOhash_map<Key, Data, HashFcn> Element; + typedef __gnu_cxx::hash_map<Key, Element*, HashFcn> table_type; + + friend class CDOhash_map<Key, Data, HashFcn>; + + table_type d_map; + + Element* d_first; + Context* d_context; + + std::vector<Element*> d_trash; + + // Nothing to save; the elements take care of themselves + virtual ContextObj* save(ContextMemoryManager* pCMM) { + Unreachable(); + } + + // Similarly, nothing to restore + virtual void restore(ContextObj* data) { + Unreachable(); + } + + void emptyTrash() { + //FIXME multithreading + for(typename std::vector<Element*>::iterator i = d_trash.begin(); + i != d_trash.end(); + ++i) { + Debug("gc") << "emptyTrash(): " << *i << std::endl; + (*i)->deleteSelf(); + } + d_trash.clear(); + } + +public: + + CDHashMap(Context* context) : + ContextObj(context), + d_map(), + d_first(NULL), + d_context(context), + d_trash() { + } + + ~CDHashMap() throw(AssertionException) { + Debug("gc") << "cdhashmap" << this + << " disappearing, destroying..." << std::endl; + destroy(); + Debug("gc") << "cdhashmap" << this + << " disappearing, done destroying" << std::endl; + + Debug("gc") << "cdhashmap" << this << " gone, emptying trash" << std::endl; + emptyTrash(); + Debug("gc") << "done emptying trash for " << this << std::endl; + + for(typename table_type::iterator i = d_map.begin(); + i != d_map.end(); + ++i) { + // mark it as being a destruction (short-circuit restore()) + (*i).second->d_map = NULL; + if(!(*i).second->d_noTrash) { + (*i).second->deleteSelf(); + } + } + d_map.clear(); + d_first = NULL; + + Assert(d_trash.empty()); + } + + void clear() throw(AssertionException) { + Debug("gc") << "clearing cdhashmap" << this << ", emptying trash" << std::endl; + emptyTrash(); + Debug("gc") << "done emptying trash for " << this << std::endl; + + for(typename table_type::iterator i = d_map.begin(); + i != d_map.end(); + ++i) { + // mark it as being a destruction (short-circuit restore()) + (*i).second->d_map = NULL; + if(!(*i).second->d_noTrash) { + (*i).second->deleteSelf(); + } + } + d_map.clear(); + d_first = NULL; + + Assert(d_trash.empty()); + } + + // The usual operators of map + + size_t size() const { + return d_map.size(); + } + + bool empty() const { + return d_map.empty(); + } + + size_t count(const Key& k) const { + return d_map.count(k); + } + + // If a key is not present, a new object is created and inserted + Element& operator[](const Key& k) { + emptyTrash(); + + typename table_type::iterator i = d_map.find(k); + + Element* obj; + if(i == d_map.end()) {// create new object + obj = new(true) Element(d_context, this, k, Data()); + d_map[k] = obj; + } else { + obj = (*i).second; + } + return *obj; + } + + bool insert(const Key& k, const Data& d) { + emptyTrash(); + + typename table_type::iterator i = d_map.find(k); + + if(i == d_map.end()) {// create new object + Element* obj = new(true) Element(d_context, this, k, d); + d_map[k] = obj; + return true; + } else { + (*i).second->set(d); + return false; + } + } + + // 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 + * "initializing" data into the map. Imagine something happens at a + * deep context level L that causes insertion into a map, such that + * the object should have an "initializing" value v1 below context + * level L, and a "current" value v2 at context level L. Then you + * can (assuming key k): + * + * map.insertAtContextLevelZero(k, v1); + * map.insert(k, v2); + * + * The justification for this "escape hatch" has to do with + * variables and assignments in theories (e.g., in arithmetic). + * Let's say you introduce a new variable x at some deep decision + * level (thanks to lazy registration, or a splitting lemma, or + * whatever). x might be mapped to something, but for theory + * implementation simplicity shouldn't disappear from the map on + * backjump; rather, it can take another (legal) value, or a special + * value to indicate it needs to be recomputed. + * + * It is an error (checked via AlwaysAssert()) to + * insertAtContextLevelZero() a key that already is in the map. + */ + void insertAtContextLevelZero(const Key& k, const Data& d) { + emptyTrash(); + + AlwaysAssert(d_map.find(k) == d_map.end()); + + Element* obj = new(true) Element(d_context, this, k, d, + true /* atLevelZero */); + d_map[k] = obj; + } + + // 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 CDOhash_map::destroy(), which + // restore()'s, which puts the CDOhash_map on the trash, which causes + // a double-delete. + (*i).second->~Element(); + // Writing ...->~CDOhash_map() in the above is legal (?) but breaks + // g++ 4.1, though later versions have no problem. + + 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; + if(d_first == elt) { + if(elt->d_next == elt) { + Assert(elt->d_prev == elt); + d_first = NULL; + } else { + d_first = elt->d_next; + } + } else { + elt->d_prev->d_next = elt->d_next; + elt->d_next->d_prev = elt->d_prev; + } + d_map.erase(j);//FIXME multithreading + Debug("gc") << "key " << k << " obliterated zero-scope: " << elt << std::endl; + // was already destructed, so don't call ->deleteSelf() + if(!elt->d_noTrash) { + ::operator delete(elt); + } + } + } + } + + class iterator { + const Element* d_it; + + public: + + iterator(const Element* p) : d_it(p) {} + iterator(const iterator& i) : d_it(i.d_it) {} + + // Default constructor + iterator() {} + + // (Dis)equality + bool operator==(const iterator& i) const { + return d_it == i.d_it; + } + bool operator!=(const iterator& i) const { + return d_it != i.d_it; + } + + // Dereference operators. + std::pair<const Key, const Data> operator*() const { + return std::pair<const Key, const Data>(d_it->getKey(), d_it->get()); + } + + // Prefix increment + iterator& operator++() { + d_it = d_it->next(); + return *this; + } + + // Postfix increment: requires a Proxy object to hold the + // intermediate value for dereferencing + class Proxy { + const std::pair<const Key, Data>* d_pair; + + public: + + Proxy(const std::pair<const Key, Data>& p) : d_pair(&p) {} + + const std::pair<const Key, Data>& operator*() const { + return *d_pair; + } + };/* class CDMap<>::iterator::Proxy */ + + // Actual postfix increment: returns Proxy with the old value. + // Now, an expression like *i++ will return the current *i, and + // then advance the iterator. However, don't try to use + // Proxy for anything else. + const Proxy operator++(int) { + Proxy e(*(*this)); + ++(*this); + return e; + } + };/* class CDMap<>::iterator */ + + typedef iterator const_iterator; + + iterator begin() const { + return iterator(d_first); + } + + iterator end() const { + return iterator(NULL); + } + + iterator find(const Key& k) const { + typename table_type::const_iterator i = d_map.find(k); + + if(i == d_map.end()) { + return end(); + } else { + return iterator((*i).second); + } + } + + iterator find(const Key& k) { + emptyTrash(); + return const_cast<const CDHashMap*>(this)->find(k); + } + +};/* class CDMap<> */ + +}/* CVC4::context namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__CONTEXT__CDMAP_H */ |