1 /********************* */ 2 /*! \file cdhashmap.h 3 ** \verbatim 4 ** Top contributors (to current version): 5 ** Morgan Deters, Tim King, Dejan Jovanovic 6 ** This file is part of the CVC4 project. 7 ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS 8 ** in the top-level source directory) and their institutional affiliations. 9 ** All rights reserved. See the file COPYING in the top-level source 10 ** directory for licensing information.\endverbatim 11 ** 12 ** \brief Context-dependent map class. 13 ** 14 ** Context-dependent map class. Generic templated class for a map 15 ** which must be saved and restored as contexts are pushed and 16 ** popped. Requires that operator= be defined for the data class, 17 ** and operator== for the key class. For key types that don't have a 18 ** std::hash<>, you should provide an explicit HashFcn. 19 ** 20 ** See also: 21 ** CDInsertHashMap : An "insert-once" CD hash map. 22 ** CDTrailHashMap : A lightweight CD hash map with poor iteration 23 ** characteristics and some quirks in usage. 24 ** 25 ** Internal documentation: 26 ** 27 ** CDHashMap<> is something of a work in progress at present (26 May 28 ** 2010), due to some recent discoveries of problems with its 29 ** internal state. Here are some notes on the internal use of 30 ** CDOhash_maps that may be useful in figuring out this mess: 31 ** 32 ** So you have a CDHashMap<>. 33 ** 34 ** You insert some (key,value) pairs. Each allocates a CDOhash_map<> 35 ** and goes on a doubly-linked list headed by map.d_first and 36 ** threaded via CDOhash_map.{d_prev,d_next}. CDOhash_maps are constructed 37 ** with a NULL d_map pointer, but then immediately call 38 ** makeCurrent() and set the d_map pointer back to the map. At 39 ** context level 0, this doesn't lead to anything special. In 40 ** higher context levels, this stores away a CDOhash_map with a NULL 41 ** map pointer at level 0, and a non-NULL map pointer in the 42 ** current context level. (Remember that for later.) 43 ** 44 ** When a key is associated to a new value in a CDHashMap, its 45 ** associated CDOhash_map calls makeCurrent(), then sets the new 46 ** value. The save object is also a CDOhash_map (allocated in context 47 ** memory). 48 ** 49 ** Now, CDOhash_maps disappear in a variety of ways. 50 ** 51 ** First, you might pop beyond a "modification of the value" 52 ** scope level, requiring a re-association of the key to an old 53 ** value. This is easy. CDOhash_map::restore() does the work, and 54 ** the context memory of the save object is reclaimed as usual. 55 ** 56 ** Second, you might pop beyond a "insert the key" scope level, 57 ** requiring that the key be completely removed from the map and 58 ** its CDOhash_map object memory freed. Here, the CDOhash_map is restored 59 ** to a "NULL-map" state (see above), signaling it to remove 60 ** itself from the map completely and put itself on a "trash 61 ** list" for its scope. 62 ** 63 ** Third, you might delete the cdhashmap(calling CDHashMap::~CDHashMap()). 64 ** This first calls destroy(), as per ContextObj contract, but 65 ** cdhashmapdoesn't save/restore itself, so that does nothing at the 66 ** CDHashMap-level. Then, for each element in the map, it marks it as being 67 ** "part of a complete map destruction", which essentially short-circuits 68 ** CDOhash_map::restore() (see CDOhash_map::restore()), then deallocates 69 ** it. 70 ** 71 ** Fourth, you might clear() the CDHashMap. This does exactly the 72 ** same as CDHashMap::~CDHashMap(), except that it doesn't call destroy() 73 ** on itself. 74 ** 75 ** ContextObj::deleteSelf() calls the CDOhash_map destructor, then 76 ** frees the memory associated to the CDOhash_map. CDOhash_map::~CDOhash_map() 77 ** calls destroy(), which restores as much as possible. 78 **/ 79 80 #include "cvc4_private.h" 81 82 #ifndef __CVC4__CONTEXT__CDHASHMAP_H 83 #define __CVC4__CONTEXT__CDHASHMAP_H 84 85 #include <functional> 86 #include <iterator> 87 #include <unordered_map> 88 #include <vector> 89 90 #include "base/cvc4_assert.h" 91 #include "context/context.h" 92 #include "context/cdhashmap_forward.h" 93 94 namespace CVC4 { 95 namespace context { 96 97 // Auxiliary class: almost the same as CDO (see cdo.h) 98 99 template <class Key, class Data, class HashFcn = std::hash<Key> > 100 class CDOhash_map : public ContextObj { 101 friend class CDHashMap<Key, Data, HashFcn>; 102 103 public: 104 // The type of the <Key, Data> pair mapped by this class. 105 // 106 // Implementation: 107 // The data and key visible to users of CDHashMap are only visible through 108 // const references. Thus the type of dereferencing a 109 // CDHashMap<Key, Data>::iterator.second is intended to always be a 110 // `const Data&`. (Otherwise, to get a Data& safely, access operations 111 // would need to makeCurrent() to get the Data&, which is an unacceptable 112 // performance hit.) To allow for the desired updating in other scenarios, we 113 // store a std::pair<const Key, const Data> and break the const encapsulation 114 // when necessary. 115 using value_type = std::pair<const Key, const Data>; 116 117 private: 118 value_type d_value; 119 120 // See documentation of value_type for why this is needed. mutable_key()121 Key& mutable_key() { return const_cast<Key&>(d_value.first); } 122 // See documentation of value_type for why this is needed. mutable_data()123 Data& mutable_data() { return const_cast<Data&>(d_value.second); } 124 125 CDHashMap<Key, Data, HashFcn>* d_map; 126 127 // Doubly-linked list for keeping track of elements in order of insertion 128 CDOhash_map* d_prev; 129 CDOhash_map* d_next; 130 save(ContextMemoryManager * pCMM)131 ContextObj* save(ContextMemoryManager* pCMM) override 132 { 133 return new(pCMM) CDOhash_map(*this); 134 } 135 restore(ContextObj * data)136 void restore(ContextObj* data) override 137 { 138 CDOhash_map* p = static_cast<CDOhash_map*>(data); 139 if(d_map != NULL) { 140 if(p->d_map == NULL) { 141 Assert(d_map->d_map.find(getKey()) != d_map->d_map.end() 142 && (*d_map->d_map.find(getKey())).second == this); 143 // no longer in map (popped beyond first level in which it was) 144 d_map->d_map.erase(getKey()); 145 // If we call deleteSelf() here, it re-enters restore(). So, 146 // put it on a "trash heap" instead, for later deletion. 147 // 148 // FIXME multithreading 149 if(d_map->d_first == this) { 150 Debug("gc") << "remove first-elem " << this << " from map " << d_map << " with next-elem " << d_next << std::endl; 151 if(d_next == this) { 152 Assert(d_prev == this); 153 d_map->d_first = NULL; 154 } else { 155 d_map->d_first = d_next; 156 } 157 } else { 158 Debug("gc") << "remove nonfirst-elem " << this << " from map " << d_map << std::endl; 159 } 160 d_next->d_prev = d_prev; 161 d_prev->d_next = d_next; 162 163 Debug("gc") << "CDHashMap<> trash push_back " << this << std::endl; 164 // this->deleteSelf(); 165 enqueueToGarbageCollect(); 166 } else { 167 mutable_data() = p->get(); 168 } 169 } 170 // Explicitly call destructors for the key and the data as they will not 171 // otherwise get called. 172 p->mutable_key().~Key(); 173 p->mutable_data().~Data(); 174 } 175 176 /** ensure copy ctor is only called by us */ CDOhash_map(const CDOhash_map & other)177 CDOhash_map(const CDOhash_map& other) 178 : ContextObj(other), 179 // don't need to save the key---and if we do we can get 180 // refcounts for Node keys messed up and leak memory 181 d_value(Key(), other.d_value.second), 182 d_map(other.d_map), 183 d_prev(NULL), 184 d_next(NULL) 185 { 186 } 187 CDOhash_map& operator=(const CDOhash_map&) = delete; 188 189 public: 190 CDOhash_map(Context* context, 191 CDHashMap<Key, Data, HashFcn>* map, 192 const Key& key, 193 const Data& data, 194 bool atLevelZero = false) ContextObj(false,context)195 : ContextObj(false, context), d_value(key, data), d_map(NULL) 196 { 197 if(atLevelZero) { 198 // "Initializing" map insertion: this entry will never be 199 // removed from the map, it's inserted at level 0 as an 200 // "initializing" element. See 201 // CDHashMap<>::insertAtContextLevelZero(). 202 mutable_data() = data; 203 } else { 204 // Normal map insertion: first makeCurrent(), then set the data 205 // and then, later, the map. Order is important; we can't 206 // initialize d_map in the constructor init list above, because 207 // we want the restore of d_map to NULL to signal us to remove 208 // the element from the map. 209 210 set(data); 211 } 212 d_map = map; 213 214 CDOhash_map*& first = d_map->d_first; 215 if(first == NULL) { 216 first = d_next = d_prev = this; 217 Debug("gc") << "add first-elem " << this << " to map " << d_map << std::endl; 218 } else { 219 Debug("gc") << "add nonfirst-elem " << this << " to map " << d_map << " with first-elem " << first << "[" << first->d_prev << " " << first->d_next << std::endl; 220 d_prev = first->d_prev; 221 d_next = first; 222 d_prev->d_next = this; 223 first->d_prev = this; 224 } 225 } 226 ~CDOhash_map()227 ~CDOhash_map() { 228 destroy(); 229 } 230 set(const Data & data)231 void set(const Data& data) { 232 makeCurrent(); 233 mutable_data() = data; 234 } 235 getKey()236 const Key& getKey() const { return d_value.first; } 237 get()238 const Data& get() const { return d_value.second; } 239 getValue()240 const value_type& getValue() const { return d_value; } 241 Data()242 operator Data() { 243 return get(); 244 } 245 246 const Data& operator=(const Data& data) { 247 set(data); 248 return data; 249 } 250 next()251 CDOhash_map* next() const { 252 if(d_next == d_map->d_first) { 253 return NULL; 254 } else { 255 return d_next; 256 } 257 } 258 };/* class CDOhash_map<> */ 259 260 261 /** 262 * Generic templated class for a map which must be saved and restored 263 * as contexts are pushed and popped. Requires that operator= be 264 * defined for the data class, and operator== for the key class. 265 */ 266 template <class Key, class Data, class HashFcn> 267 class CDHashMap : public ContextObj { 268 269 typedef CDOhash_map<Key, Data, HashFcn> Element; 270 typedef std::unordered_map<Key, Element*, HashFcn> table_type; 271 272 friend class CDOhash_map<Key, Data, HashFcn>; 273 274 table_type d_map; 275 276 Element* d_first; 277 Context* d_context; 278 279 // Nothing to save; the elements take care of themselves save(ContextMemoryManager * pCMM)280 ContextObj* save(ContextMemoryManager* pCMM) override { Unreachable(); } 281 282 // Similarly, nothing to restore restore(ContextObj * data)283 void restore(ContextObj* data) override { Unreachable(); } 284 285 // no copy or assignment 286 CDHashMap(const CDHashMap&) = delete; 287 CDHashMap& operator=(const CDHashMap&) = delete; 288 289 public: CDHashMap(Context * context)290 CDHashMap(Context* context) 291 : ContextObj(context), d_map(), d_first(NULL), d_context(context) {} 292 ~CDHashMap()293 ~CDHashMap() { 294 Debug("gc") << "cdhashmap" << this << " disappearing, destroying..." 295 << std::endl; 296 destroy(); 297 Debug("gc") << "cdhashmap" << this << " disappearing, done destroying" 298 << std::endl; 299 clear(); 300 } 301 clear()302 void clear() { 303 Debug("gc") << "clearing cdhashmap" << this << ", emptying trash" 304 << std::endl; 305 Debug("gc") << "done emptying trash for " << this << std::endl; 306 307 for (auto& key_element_pair : d_map) { 308 // mark it as being a destruction (short-circuit restore()) 309 Element* element = key_element_pair.second; 310 element->d_map = nullptr; 311 element->deleteSelf(); 312 } 313 d_map.clear(); 314 d_first = nullptr; 315 } 316 317 // The usual operators of map 318 size()319 size_t size() const { 320 return d_map.size(); 321 } 322 empty()323 bool empty() const { 324 return d_map.empty(); 325 } 326 count(const Key & k)327 size_t count(const Key& k) const { 328 return d_map.count(k); 329 } 330 331 // If a key is not present, a new object is created and inserted 332 Element& operator[](const Key& k) { 333 typename table_type::iterator i = d_map.find(k); 334 335 Element* obj; 336 if(i == d_map.end()) {// create new object 337 obj = new(true) Element(d_context, this, k, Data()); 338 d_map.insert(std::make_pair(k, obj)); 339 } else { 340 obj = (*i).second; 341 } 342 return *obj; 343 } 344 insert(const Key & k,const Data & d)345 bool insert(const Key& k, const Data& d) { 346 typename table_type::iterator i = d_map.find(k); 347 348 if(i == d_map.end()) {// create new object 349 Element* obj = new(true) Element(d_context, this, k, d); 350 d_map.insert(std::make_pair(k, obj)); 351 return true; 352 } else { 353 (*i).second->set(d); 354 return false; 355 } 356 } 357 358 /** 359 * Version of insert() for CDHashMap<> that inserts data value d at 360 * context level zero. This is a special escape hatch for inserting 361 * "initializing" data into the map. Imagine something happens at a 362 * deep context level L that causes insertion into a map, such that 363 * the object should have an "initializing" value v1 below context 364 * level L, and a "current" value v2 at context level L. Then you 365 * can (assuming key k): 366 * 367 * map.insertAtContextLevelZero(k, v1); 368 * map.insert(k, v2); 369 * 370 * The justification for this "escape hatch" has to do with 371 * variables and assignments in theories (e.g., in arithmetic). 372 * Let's say you introduce a new variable x at some deep decision 373 * level (thanks to lazy registration, or a splitting lemma, or 374 * whatever). x might be mapped to something, but for theory 375 * implementation simplicity shouldn't disappear from the map on 376 * backjump; rather, it can take another (legal) value, or a special 377 * value to indicate it needs to be recomputed. 378 * 379 * It is an error (checked via AlwaysAssert()) to 380 * insertAtContextLevelZero() a key that already is in the map. 381 */ insertAtContextLevelZero(const Key & k,const Data & d)382 void insertAtContextLevelZero(const Key& k, const Data& d) { 383 AlwaysAssert(d_map.find(k) == d_map.end()); 384 385 Element* obj = new(true) Element(d_context, this, k, d, 386 true /* atLevelZero */); 387 d_map.insert(std::make_pair(k, obj)); 388 } 389 390 // FIXME: no erase(), too much hassle to implement efficiently... 391 392 using value_type = typename CDOhash_map<Key, Data, HashFcn>::value_type; 393 394 class iterator { 395 const Element* d_it; 396 397 public: 398 iterator(const Element * p)399 iterator(const Element* p) : d_it(p) {} iterator(const iterator & i)400 iterator(const iterator& i) : d_it(i.d_it) {} 401 402 // Default constructor iterator()403 iterator() : d_it(nullptr) {} 404 405 // (Dis)equality 406 bool operator==(const iterator& i) const { 407 return d_it == i.d_it; 408 } 409 bool operator!=(const iterator& i) const { 410 return d_it != i.d_it; 411 } 412 413 // Dereference operators. 414 const value_type& operator*() const { return d_it->getValue(); } 415 416 // Prefix increment 417 iterator& operator++() { 418 d_it = d_it->next(); 419 return *this; 420 } 421 422 // Postfix increment is not yet supported. 423 };/* class CDHashMap<>::iterator */ 424 425 typedef iterator const_iterator; 426 begin()427 iterator begin() const { 428 return iterator(d_first); 429 } 430 end()431 iterator end() const { 432 return iterator(NULL); 433 } 434 find(const Key & k)435 iterator find(const Key& k) const { 436 typename table_type::const_iterator i = d_map.find(k); 437 438 if(i == d_map.end()) { 439 return end(); 440 } else { 441 return iterator((*i).second); 442 } 443 } 444 445 446 };/* class CDHashMap<> */ 447 448 }/* CVC4::context namespace */ 449 }/* CVC4 namespace */ 450 451 #endif /* __CVC4__CONTEXT__CDHASHMAP_H */ 452