src/context/cdmap.h

   1 /*********************                                                        */
   2 /*! \file cdmap.h
   3  ** \verbatim
   4  ** Original author: mdeters
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): taking, dejan
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
   9  ** Courant Institute of Mathematical Sciences
  10  ** New York University
  11  ** See the file COPYING in the top-level source directory for licensing
  12  ** information.\endverbatim
  13  **
  14  ** \brief Context-dependent map class.
  15  **
  16  ** Context-dependent map class.  Generic templated class for a map
  17  ** which must be saved and restored as contexts are pushed and
  18  ** popped.  Requires that operator= be defined for the data class,
  19  ** and operator== for the key class.  For key types that don't have a
  20  ** __gnu_cxx::hash<>, you should provide an explicit HashFcn.
  21  **
  22  ** Internal documentation:
  23  **
  24  ** CDMap<> is something of a work in progress at present (26 May
  25  ** 2010), due to some recent discoveries of problems with its
  26  ** internal state.  Here are some notes on the internal use of
  27  ** CDOmaps that may be useful in figuring out this mess:
  28  **
  29  **     So you have a CDMap<>.
  30  **
  31  **     You insert some (key,value) pairs.  Each allocates a CDOmap<>
  32  **     and goes on a doubly-linked list headed by map.d_first and
  33  **     threaded via cdomap.{d_prev,d_next}.  CDOmaps are constructed
  34  **     with a NULL d_map pointer, but then immediately call
  35  **     makeCurrent() and set the d_map pointer back to the map.  At
  36  **     context level 0, this doesn't lead to anything special.  In
  37  **     higher context levels, this stores away a CDOmap with a NULL
  38  **     map pointer at level 0, and a non-NULL map pointer in the
  39  **     current context level.  (Remember that for later.)
  40  **
  41  **     When a key is associated to a new value in a CDMap, its
  42  **     associated CDOmap calls makeCurrent(), then sets the new
  43  **     value.  The save object is also a CDOmap (allocated in context
  44  **     memory).
  45  **
  46  **     Now, CDOmaps disappear in a variety of ways.
  47  **
  48  **     First, you might pop beyond a "modification of the value"
  49  **     scope level, requiring a re-association of the key to an old
  50  **     value.  This is easy.  CDOmap::restore() does the work, and
  51  **     the context memory of the save object is reclaimed as usual.
  52  **
  53  **     Second, you might pop beyond a "insert the key" scope level,
  54  **     requiring that the key be completely removed from the map and
  55  **     its CDOmap object memory freed.  Here, the CDOmap is restored
  56  **     to a "NULL-map" state (see above), signaling it to remove
  57  **     itself from the map completely and put itself on a "trash
  58  **     list" for the map.
  59  **
  60  **     Third, you might obliterate() the key.  This calls the CDOmap
  61  **     destructor, which calls destroy(), which does a successive
  62  **     restore() until level 0.  If the key was in the map since
  63  **     level 0, the restore() won't remove it, so in that case
  64  **     obliterate() removes it from the map and frees the CDOmap's
  65  **     memory.
  66  **
  67  **     Fourth, you might delete the CDMap (calling CDMap::~CDMap()).
  68  **     This first calls destroy(), as per ContextObj contract, but
  69  **     CDMap doesn't save/restore itself, so that does nothing at the
  70  **     CDMap-level.  Then it empties the trash.  Then, for each
  71  **     element in the map, it marks it as being "part of a complete
  72  **     map destruction", which essentially short-circuits
  73  **     CDOmap::restore() (see CDOmap::restore()), then deallocates
  74  **     it.  Finally it asserts that the trash is empty (which it
  75  **     should be, since restore() was short-circuited).
  76  **
  77  **     Fifth, you might clear() the CDMap.  This does exactly the
  78  **     same as CDMap::~CDMap(), except that it doesn't call destroy()
  79  **     on itself.
  80  **
  81  **     CDMap::emptyTrash() simply goes through and calls
  82  **     ->deleteSelf() on all elements in the trash.
  83  **     ContextObj::deleteSelf() calls the CDOmap destructor, then
  84  **     frees the memory associated to the CDOmap.  CDOmap::~CDOmap()
  85  **     calls destroy(), which restores as much as possible.  (Note,
  86  **     though, that since objects placed on the trash have already
  87  **     restored to the fullest extent possible, it does nothing.)
  88  **/
  89
  90 #include "cvc4_private.h"
  91
  92 #ifndef __CVC4__CONTEXT__CDMAP_H
  93 #define __CVC4__CONTEXT__CDMAP_H
  94
  95 #include "context/context.h"
  96 #include "util/Assert.h"
  97
  98 #include <vector>
  99 #include <iterator>
 100 #include <ext/hash_map>
 101
 102 namespace CVC4 {
 103 namespace context {
 104
 105 // Auxiliary class: almost the same as CDO (see cdo.h)
 106
 107 template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> > class CDMap;
 108
 109 template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> >
 110 class CDOmap : public ContextObj {
 111   friend class CDMap<Key, Data, HashFcn>;
 112
 113   Key d_key;
 114   Data d_data;
 115   CDMap<Key, Data, HashFcn>* d_map;
 116
 117   /** never put this cdmap element on the trash */
 118   bool d_noTrash;
 119
 120   // Doubly-linked list for keeping track of elements in order of insertion
 121   CDOmap* d_prev;
 122   CDOmap* d_next;
 123
 124   virtual ContextObj* save(ContextMemoryManager* pCMM) {
 125     return new(pCMM) CDOmap(*this);
 126   }
 127
 128   virtual void restore(ContextObj* data) {
 129     if(d_map != NULL) {
 130       CDOmap* p = static_cast<CDOmap*>(data);
 131       if(p->d_map == NULL) {
 132         Assert(d_map->d_map.find(d_key) != d_map->d_map.end() &&
 133                (*d_map->d_map.find(d_key)).second == this);
 134         // no longer in map (popped beyond first level in which it was)
 135         d_map->d_map.erase(d_key);
 136         // If we call deleteSelf() here, it re-enters restore().  So,
 137         // put it on a "trash heap" instead, for later deletion.
 138         //
 139         // FIXME multithreading
 140         if(d_map->d_first == this) {
 141           Debug("gc") << "remove first-elem " << this << " from map " << d_map << " with next-elem " << d_next << std::endl;
 142           if(d_next == this) {
 143             Assert(d_prev == this);
 144             d_map->d_first = NULL;
 145           } else {
 146             d_map->d_first = d_next;
 147           }
 148         } else {
 149           Debug("gc") << "remove nonfirst-elem " << this << " from map " << d_map << std::endl;
 150         }
 151         d_next->d_prev = d_prev;
 152         d_prev->d_next = d_next;
 153         if(d_noTrash) {
 154           Debug("gc") << "CDMap<> no-trash " << this << std::endl;
 155         } else {
 156           Debug("gc") << "CDMap<> trash push_back " << this << std::endl;
 157           //this->deleteSelf();
 158           d_map->d_trash.push_back(this);
 159         }
 160       } else {
 161         d_data = p->d_data;
 162       }
 163     }
 164   }
 165
 166   /** ensure copy ctor is only called by us */
 167   CDOmap(const CDOmap& other) :
 168     ContextObj(other),
 169     d_key(other.d_key),
 170     d_data(other.d_data),
 171     d_map(other.d_map),
 172     d_prev(NULL),
 173     d_next(NULL) {
 174   }
 175
 176 public:
 177
 178   CDOmap(Context* context,
 179          CDMap<Key, Data, HashFcn>* map,
 180          const Key& key,
 181          const Data& data,
 182          bool atLevelZero = false,
 183          bool allocatedInCMM = false) :
 184     ContextObj(allocatedInCMM, context),
 185     d_key(key),
 186     d_map(NULL),
 187     d_noTrash(allocatedInCMM) {
 188
 189     // untested, probably unsafe.
 190     Assert(!(atLevelZero && allocatedInCMM));
 191
 192     if(atLevelZero) {
 193       // "Initializing" map insertion: this entry will never be
 194       // removed from the map, it's inserted at level 0 as an
 195       // "initializing" element.  See
 196       // CDMap<>::insertAtContextLevelZero().
 197       d_data = data;
 198     } else {
 199       // Normal map insertion: first makeCurrent(), then set the data
 200       // and then, later, the map.  Order is important; we can't
 201       // initialize d_map in the constructor init list above, because
 202       // we want the restore of d_map to NULL to signal us to remove
 203       // the element from the map.
 204
 205       if(allocatedInCMM) {
 206         // Force a save/restore point, even though the object is
 207         // allocated here.  This is so that we can detect when the
 208         // object falls out of the map (otherwise we wouldn't get it).
 209         makeSaveRestorePoint();
 210       }
 211
 212       set(data);
 213     }
 214     d_map = map;
 215
 216     CDOmap*& first = d_map->d_first;
 217     if(first == NULL) {
 218       first = d_next = d_prev = this;
 219       Debug("gc") << "add first-elem " << this << " to map " << d_map << std::endl;
 220     } else {
 221       Debug("gc") << "add nonfirst-elem " << this << " to map " << d_map << " with first-elem " << first << "[" << first->d_prev << " " << first->d_next << std::endl;
 222       d_prev = first->d_prev;
 223       d_next = first;
 224       d_prev->d_next = this;
 225       first->d_prev = this;
 226     }
 227   }
 228
 229   ~CDOmap() throw(AssertionException) {
 230     destroy();
 231   }
 232
 233   void set(const Data& data) {
 234     makeCurrent();
 235     d_data = data;
 236   }
 237
 238   const Key& getKey() const {
 239     return d_key;
 240   }
 241
 242   const Data& get() const {
 243     return d_data;
 244   }
 245
 246   operator Data() {
 247     return get();
 248   }
 249
 250   const Data& operator=(const Data& data) {
 251     set(data);
 252     return data;
 253   }
 254
 255   CDOmap* next() const {
 256     if(d_next == d_map->d_first) {
 257       return NULL;
 258     } else {
 259       return d_next;
 260     }
 261   }
 262 };/* class CDOmap<> */
 263
 264
 265 /**
 266  * Generic templated class for a map which must be saved and restored
 267  * as contexts are pushed and popped.  Requires that operator= be
 268  * defined for the data class, and operator== for the key class.
 269  */
 270 template <class Key, class Data, class HashFcn>
 271 class CDMap : public ContextObj {
 272
 273   typedef CDOmap<Key, Data, HashFcn> Element;
 274   typedef __gnu_cxx::hash_map<Key, Element*, HashFcn> table_type;
 275
 276   friend class CDOmap<Key, Data, HashFcn>;
 277
 278   table_type d_map;
 279
 280   Element* d_first;
 281   Context* d_context;
 282
 283   std::vector<Element*> d_trash;
 284
 285   // Nothing to save; the elements take care of themselves
 286   virtual ContextObj* save(ContextMemoryManager* pCMM) {
 287     Unreachable();
 288   }
 289
 290   // Similarly, nothing to restore
 291   virtual void restore(ContextObj* data) {
 292     Unreachable();
 293   }
 294
 295   void emptyTrash() {
 296     //FIXME multithreading
 297     for(typename std::vector<Element*>::iterator i = d_trash.begin();
 298         i != d_trash.end();
 299         ++i) {
 300       Debug("gc") << "emptyTrash(): " << *i << std::endl;
 301       (*i)->deleteSelf();
 302     }
 303     d_trash.clear();
 304   }
 305
 306 public:
 307
 308   CDMap(Context* context) :
 309     ContextObj(context),
 310     d_map(),
 311     d_first(NULL),
 312     d_context(context),
 313     d_trash() {
 314   }
 315
 316   ~CDMap() throw(AssertionException) {
 317     Debug("gc") << "cdmap " << this
 318                 << " disappearing, destroying..." << std::endl;
 319     destroy();
 320     Debug("gc") << "cdmap " << this
 321                 << " disappearing, done destroying" << std::endl;
 322
 323     Debug("gc") << "cdmap " << this << " gone, emptying trash" << std::endl;
 324     emptyTrash();
 325     Debug("gc") << "done emptying trash for " << this << std::endl;
 326
 327     for(typename table_type::iterator i = d_map.begin();
 328         i != d_map.end();
 329         ++i) {
 330       // mark it as being a destruction (short-circuit restore())
 331       (*i).second->d_map = NULL;
 332       if(!(*i).second->d_noTrash) {
 333         (*i).second->deleteSelf();
 334       }
 335     }
 336     d_map.clear();
 337     d_first = NULL;
 338
 339     Assert(d_trash.empty());
 340   }
 341
 342   void clear() throw(AssertionException) {
 343     Debug("gc") << "clearing cdmap " << this << ", emptying trash" << std::endl;
 344     emptyTrash();
 345     Debug("gc") << "done emptying trash for " << this << std::endl;
 346
 347     for(typename table_type::iterator i = d_map.begin();
 348         i != d_map.end();
 349         ++i) {
 350       // mark it as being a destruction (short-circuit restore())
 351       (*i).second->d_map = NULL;
 352       if(!(*i).second->d_noTrash) {
 353         (*i).second->deleteSelf();
 354       }
 355     }
 356     d_map.clear();
 357     d_first = NULL;
 358
 359     Assert(d_trash.empty());
 360   }
 361
 362   // The usual operators of map
 363
 364   size_t size() const {
 365     return d_map.size();
 366   }
 367
 368   size_t count(const Key& k) const {
 369     return d_map.count(k);
 370   }
 371
 372   // If a key is not present, a new object is created and inserted
 373   Element& operator[](const Key& k) {
 374     emptyTrash();
 375
 376     typename table_type::iterator i = d_map.find(k);
 377
 378     Element* obj;
 379     if(i == d_map.end()) {// create new object
 380       obj = new(true) Element(d_context, this, k, Data());
 381       d_map[k] = obj;
 382     } else {
 383       obj = (*i).second;
 384     }
 385     return *obj;
 386   }
 387
 388   bool insert(const Key& k, const Data& d) {
 389     emptyTrash();
 390
 391     typename table_type::iterator i = d_map.find(k);
 392
 393     if(i == d_map.end()) {// create new object
 394       Element* obj = new(true) Element(d_context, this, k, d);
 395       d_map[k] = obj;
 396       return true;
 397     } else {
 398       (*i).second->set(d);
 399       return false;
 400     }
 401   }
 402
 403   // Use this for pointer data d allocated in context memory at this
 404   // level.  THIS IS HIGHLY EXPERIMENTAL.  It seems to work if ALL
 405   // your data objects are allocated from context memory.
 406   void insertDataFromContextMemory(const Key& k, const Data& d) {
 407     emptyTrash();
 408
 409     AlwaysAssert(d_map.find(k) == d_map.end());
 410
 411     Element* obj = new(d_context->getCMM()) Element(d_context, this, k, d,
 412                                                     false /* atLevelZero */,
 413                                                     true /* allocatedInCMM */);
 414
 415     d_map[k] = obj;
 416   }
 417
 418   /**
 419    * Version of insert() for CDMap<> that inserts data value d at
 420    * context level zero.  This is a special escape hatch for inserting
 421    * "initializing" data into the map.  Imagine something happens at a
 422    * deep context level L that causes insertion into a map, such that
 423    * the object should have an "initializing" value v1 below context
 424    * level L, and a "current" value v2 at context level L.  Then you
 425    * can (assuming key k):
 426    *
 427    *   map.insertAtContextLevelZero(k, v1);
 428    *   map.insert(k, v2);
 429    *
 430    * The justification for this "escape hatch" has to do with
 431    * variables and assignments in theories (e.g., in arithmetic).
 432    * Let's say you introduce a new variable x at some deep decision
 433    * level (thanks to lazy registration, or a splitting lemma, or
 434    * whatever).  x might be mapped to something, but for theory
 435    * implementation simplicity shouldn't disappear from the map on
 436    * backjump; rather, it can take another (legal) value, or a special
 437    * value to indicate it needs to be recomputed.
 438    *
 439    * It is an error (checked via AlwaysAssert()) to
 440    * insertAtContextLevelZero() a key that already is in the map.
 441    */
 442   void insertAtContextLevelZero(const Key& k, const Data& d) {
 443     emptyTrash();
 444
 445     AlwaysAssert(d_map.find(k) == d_map.end());
 446
 447     Element* obj = new(true) Element(d_context, this, k, d,
 448                                      true /* atLevelZero */);
 449     d_map[k] = obj;
 450   }
 451
 452   // FIXME: no erase(), too much hassle to implement efficiently...
 453
 454   /**
 455    * "Obliterating" is kind of like erasing, except it's not
 456    * backtrackable; the key is permanently removed from the map.
 457    * (Naturally, it can be re-added as a new element.)
 458    */
 459   void obliterate(const Key& k) {
 460     typename table_type::iterator i = d_map.find(k);
 461     if(i != d_map.end()) {
 462       Debug("gc") << "key " << k << " obliterated" << std::endl;
 463       // We can't call ->deleteSelf() here, because it calls the
 464       // ContextObj destructor, which calls CDOmap::destroy(), which
 465       // restore()'s, which puts the CDOmap on the trash, which causes
 466       // a double-delete.
 467       (*i).second->~Element();
 468       // Writing ...->~CDOmap() in the above is legal (?) but breaks
 469       // g++ 4.1, though later versions have no problem.
 470
 471       typename table_type::iterator j = d_map.find(k);
 472       // This if() succeeds for objects inserted when in the
 473       // zero-scope: they were never save()'d there, so restore()
 474       // never gets a NULL map and so they leak.
 475       if(j != d_map.end()) {
 476         Element* elt = (*j).second;
 477         if(d_first == elt) {
 478           if(elt->d_next == elt) {
 479             Assert(elt->d_prev == elt);
 480             d_first = NULL;
 481           } else {
 482             d_first = elt->d_next;
 483           }
 484         } else {
 485           elt->d_prev->d_next = elt->d_next;
 486           elt->d_next->d_prev = elt->d_prev;
 487         }
 488         d_map.erase(j);//FIXME multithreading
 489         Debug("gc") << "key " << k << " obliterated zero-scope: " << elt << std::endl;
 490         // was already destructed, so don't call ->deleteSelf()
 491         if(!elt->d_noTrash) {
 492           ::operator delete(elt);
 493         }
 494       }
 495     }
 496   }
 497
 498   class iterator {
 499     const Element* d_it;
 500
 501   public:
 502
 503     iterator(const Element* p) : d_it(p) {}
 504     iterator(const iterator& i) : d_it(i.d_it) {}
 505
 506     // Default constructor
 507     iterator() {}
 508
 509     // (Dis)equality
 510     bool operator==(const iterator& i) const {
 511       return d_it == i.d_it;
 512     }
 513     bool operator!=(const iterator& i) const {
 514       return d_it != i.d_it;
 515     }
 516
 517     // Dereference operators.
 518     std::pair<const Key, Data> operator*() const {
 519       return std::pair<const Key, Data>(d_it->getKey(), d_it->get());
 520     }
 521
 522     // Prefix increment
 523     iterator& operator++() {
 524       d_it = d_it->next();
 525       return *this;
 526     }
 527
 528     // Postfix increment: requires a Proxy object to hold the
 529     // intermediate value for dereferencing
 530     class Proxy {
 531       const std::pair<const Key, Data>* d_pair;
 532
 533     public:
 534
 535       Proxy(const std::pair<const Key, Data>& p) : d_pair(&p) {}
 536
 537       const std::pair<const Key, Data>& operator*() const {
 538         return *d_pair;
 539       }
 540     };/* class CDMap<>::iterator::Proxy */
 541
 542     // Actual postfix increment: returns Proxy with the old value.
 543     // Now, an expression like *i++ will return the current *i, and
 544     // then advance the iterator.  However, don't try to use
 545     // Proxy for anything else.
 546     const Proxy operator++(int) {
 547       Proxy e(*(*this));
 548       ++(*this);
 549       return e;
 550     }
 551   };/* class CDMap<>::iterator */
 552
 553   typedef iterator const_iterator;
 554
 555   iterator begin() const {
 556     return iterator(d_first);
 557   }
 558
 559   iterator end() const {
 560     return iterator(NULL);
 561   }
 562
 563   iterator find(const Key& k) const {
 564     typename table_type::const_iterator i = d_map.find(k);
 565
 566     if(i == d_map.end()) {
 567       return end();
 568     } else {
 569       return iterator((*i).second);
 570     }
 571   }
 572
 573   iterator find(const Key& k) {
 574     emptyTrash();
 575     return const_cast<const CDMap*>(this)->find(k);
 576   }
 577
 578 };/* class CDMap<> */
 579
 580 }/* CVC4::context namespace */
 581 }/* CVC4 namespace */
 582
 583 #endif /* __CVC4__CONTEXT__CDMAP_H */