From fa86342d9a0373287dcb164f7f9c15825f356542 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Wed, 26 May 2010 20:29:53 +0000 Subject: CDMap<> and CDOmap<> fixes to resolve bug 123 --- src/context/cdmap.h | 146 +++++++++++++++++++++++++++++++++++++++++----------- 1 file changed, 115 insertions(+), 31 deletions(-) (limited to 'src/context/cdmap.h') diff --git a/src/context/cdmap.h b/src/context/cdmap.h index d4e2e0d28..b0ffc91a4 100644 --- a/src/context/cdmap.h +++ b/src/context/cdmap.h @@ -15,6 +15,73 @@ ** 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 + ** CDOmaps that may be useful in figuring out this mess: + ** + ** So you have a CDMap<>. + ** + ** You insert some (key,value) pairs. Each allocates a CDOmap<> + ** and goes on a doubly-linked list headed by map.d_first and + ** threaded via cdomap.{d_prev,d_next}. CDOmaps 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 CDOmap 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 CDOmap calls makeCurrent(), then sets the new + ** value. The save object is also a CDOmap (allocated in context + ** memory). + ** + ** Now, CDOmaps 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. CDOmap::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 CDOmap object memory freed. Here, the CDOmap 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 CDOmap + ** 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 CDOmap's + ** memory. + ** + ** Fourth, you might delete the CDMap (calling CDMap::~CDMap()). + ** This first calls destroy(), as per ContextObj contract, but + ** CDMap doesn'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 + ** CDOmap::restore() (see CDOmap::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 CDOmap destructor, then + ** frees the memory associated to the CDOmap. CDOmap::~CDOmap() + ** 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" @@ -58,33 +125,36 @@ class CDOmap : public ContextObj { } virtual void restore(ContextObj* data) { - 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) { - 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; + if(d_map != NULL) { + 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) { + 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 { - d_map->d_first = d_next; + Debug("gc") << "remove nonfirst-elem " << this << " from map " << d_map << std::endl; } + 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); } else { - Debug("gc") << "remove nonfirst-elem " << this << " from map " << d_map << std::endl; + d_data = p->d_data; } - d_next->d_prev = d_prev; - d_prev->d_next = d_next; - Debug("gc") << "CDMap<> trash push_back " << this << std::endl; - d_map->d_trash.push_back(this); - } else { - d_data = p->d_data; } } @@ -211,29 +281,43 @@ public: destroy(); Debug("gc") << "cdmap " << this << " disappearing, done destroying" << std::endl; + + Debug("gc") << "cdmap " << 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; (*i).second->deleteSelf(); } - Debug("gc") << "cdmap " << this << " gone, emptying trash" << std::endl; - emptyTrash(); - Debug("gc") << "done emptying trash for " << this << std::endl; + d_map.clear(); + d_first = NULL; + + Assert(d_trash.empty()); } void clear() throw(AssertionException) { - Debug("gc") << "cdmap " << this - << " disappearing, destroying..." << std::endl; + Debug("gc") << "clearing cdmap " << this << std::endl; + + Debug("gc") << "cdmap " << this << " cleared, 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; (*i).second->deleteSelf(); } d_map.clear(); - emptyTrash(); - Debug("gc") << "done emptying trash for " << this << std::endl; - } + d_first = NULL; + Assert(d_trash.empty()); + } // The usual operators of map -- cgit v1.2.3