GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/context/cdhashmap.h Lines: 125 128 97.7 %
Date: 2021-03-22 Branches: 489 1304 37.5 %

Line Exec Source
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-2021 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.
77
 **     CDOhash_map::~CDOhash_map() calls destroy(), which restores as much as
78
 **     possible.
79
 **/
80
81
#include "cvc4_private.h"
82
83
#ifndef CVC4__CONTEXT__CDHASHMAP_H
84
#define CVC4__CONTEXT__CDHASHMAP_H
85
86
#include <functional>
87
#include <iterator>
88
#include <unordered_map>
89
90
#include "base/check.h"
91
#include "context/cdhashmap_forward.h"
92
#include "context/context.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.
121
58052013
  Key& mutable_key() { return const_cast<Key&>(d_value.first); }
122
  // See documentation of value_type for why this is needed.
123
184736426
  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
131
58052229
  ContextObj* save(ContextMemoryManager* pCMM) override
132
  {
133
58052229
    return new(pCMM) CDOhash_map(*this);
134
  }
135
136
58052013
  void restore(ContextObj* data) override
137
  {
138
58052013
    CDOhash_map* p = static_cast<CDOhash_map*>(data);
139
58052013
    if(d_map != NULL) {
140
58000600
      if(p->d_map == NULL) {
141
56823891
        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
56823891
        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
56823891
        if(d_map->d_first == this) {
150
396087
          Debug("gc") << "remove first-elem " << this << " from map " << d_map << " with next-elem " << d_next << std::endl;
151
396087
          if(d_next == this) {
152
396069
            Assert(d_prev == this);
153
396069
            d_map->d_first = NULL;
154
          } else {
155
18
            d_map->d_first = d_next;
156
          }
157
        } else {
158
56427804
          Debug("gc") << "remove nonfirst-elem " << this << " from map " << d_map << std::endl;
159
        }
160
56823891
        d_next->d_prev = d_prev;
161
56823891
        d_prev->d_next = d_next;
162
163
56823891
        Debug("gc") << "CDHashMap<> trash push_back " << this << std::endl;
164
        // this->deleteSelf();
165
56823891
        enqueueToGarbageCollect();
166
      } else {
167
1176709
        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
58052013
    p->mutable_key().~Key();
173
58052013
    p->mutable_data().~Data();
174
58052013
  }
175
176
  /** ensure copy ctor is only called by us */
177
58052229
  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
58052229
        d_map(other.d_map),
183
        d_prev(NULL),
184
116104458
        d_next(NULL)
185
  {
186
58052229
  }
187
  CDOhash_map& operator=(const CDOhash_map&) = delete;
188
189
 public:
190
63410215
  CDOhash_map(Context* context,
191
              CDHashMap<Key, Data, HashFcn>* map,
192
              const Key& key,
193
              const Data& data,
194
              bool atLevelZero = false)
195
63410215
      : ContextObj(false, context), d_value(key, data), d_map(NULL)
196
  {
197
63410215
    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
32055
      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
63378160
      set(data);
211
    }
212
63410215
    d_map = map;
213
214
63410215
    CDOhash_map*& first = d_map->d_first;
215
63410215
    if(first == NULL) {
216
1233134
      first = d_next = d_prev = this;
217
1233134
      Debug("gc") << "add first-elem " << this << " to map " << d_map << std::endl;
218
    } else {
219
62177081
      Debug("gc") << "add nonfirst-elem " << this << " to map " << d_map << " with first-elem " << first << "[" << first->d_prev << " " << first->d_next << std::endl;
220
62177081
      d_prev = first->d_prev;
221
62177081
      d_next = first;
222
62177081
      d_prev->d_next = this;
223
62177081
      first->d_prev = this;
224
    }
225
63410215
  }
226
227
63409873
  ~CDOhash_map() {
228
63409873
    destroy();
229
126819746
  }
230
231
125475649
  void set(const Data& data) {
232
125475649
    makeCurrent();
233
125475649
    mutable_data() = data;
234
125475649
  }
235
236
170471673
  const Key& getKey() const { return d_value.first; }
237
238
13988571
  const Data& get() const { return d_value.second; }
239
240
132947617
  const value_type& getValue() const { return d_value; }
241
242
7944941
  operator Data() {
243
7944941
    return get();
244
  }
245
246
61290054
  const Data& operator=(const Data& data) {
247
61290054
    set(data);
248
61290054
    return data;
249
  }
250
251
1284425
  CDOhash_map* next() const {
252
1284425
    if(d_next == d_map->d_first) {
253
117800
      return NULL;
254
    } else {
255
1166625
      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
280
  ContextObj* save(ContextMemoryManager* pCMM) override
281
  {
282
    Unreachable();
283
    SuppressWrongNoReturnWarning;
284
  }
285
286
  // Similarly, nothing to restore
287
  void restore(ContextObj* data) override { Unreachable(); }
288
289
  // no copy or assignment
290
  CDHashMap(const CDHashMap&) = delete;
291
  CDHashMap& operator=(const CDHashMap&) = delete;
292
293
public:
294
2394559
  CDHashMap(Context* context)
295
2394559
    : ContextObj(context), d_map(), d_first(NULL), d_context(context) {}
296
297
2394137
  ~CDHashMap() {
298
2394137
    Debug("gc") << "cdhashmap" << this << " disappearing, destroying..."
299
                << std::endl;
300
2394137
    destroy();
301
2394137
    Debug("gc") << "cdhashmap" << this << " disappearing, done destroying"
302
                << std::endl;
303
2394137
    clear();
304
4788274
  }
305
306
2394137
  void clear() {
307
2394137
    Debug("gc") << "clearing cdhashmap" << this << ", emptying trash"
308
                << std::endl;
309
2394137
    Debug("gc") << "done emptying trash for " << this << std::endl;
310
311
8980119
    for (auto& key_element_pair : d_map) {
312
      // mark it as being a destruction (short-circuit restore())
313
6585982
      Element* element = key_element_pair.second;
314
6585982
      element->d_map = nullptr;
315
6585982
      element->deleteSelf();
316
    }
317
2394137
    d_map.clear();
318
2394137
    d_first = nullptr;
319
2394137
  }
320
321
  // The usual operators of map
322
323
138993
  size_t size() const {
324
138993
    return d_map.size();
325
  }
326
327
3104241
  bool empty() const {
328
3104241
    return d_map.empty();
329
  }
330
331
  size_t count(const Key& k) const {
332
    return d_map.count(k);
333
  }
334
335
  // If a key is not present, a new object is created and inserted
336
74136221
  Element& operator[](const Key& k) {
337
74136221
    typename table_type::iterator i = d_map.find(k);
338
339
    Element* obj;
340
74136221
    if(i == d_map.end()) {// create new object
341
53807164
      obj = new(true) Element(d_context, this, k, Data());
342
69450193
      d_map.insert(std::make_pair(k, obj));
343
    } else {
344
20329057
      obj = (*i).second;
345
    }
346
74136221
    return *obj;
347
  }
348
349
10359638
  bool insert(const Key& k, const Data& d) {
350
10359638
    typename table_type::iterator i = d_map.find(k);
351
352
10359638
    if(i == d_map.end()) {// create new object
353
9570996
      Element* obj = new(true) Element(d_context, this, k, d);
354
10136999
      d_map.insert(std::make_pair(k, obj));
355
9570996
      return true;
356
    } else {
357
788642
      (*i).second->set(d);
358
788642
      return false;
359
    }
360
  }
361
362
  /**
363
   * Version of insert() for CDHashMap<> that inserts data value d at
364
   * context level zero.  This is a special escape hatch for inserting
365
   * "initializing" data into the map.  Imagine something happens at a
366
   * deep context level L that causes insertion into a map, such that
367
   * the object should have an "initializing" value v1 below context
368
   * level L, and a "current" value v2 at context level L.  Then you
369
   * can (assuming key k):
370
   *
371
   *   map.insertAtContextLevelZero(k, v1);
372
   *   map.insert(k, v2);
373
   *
374
   * The justification for this "escape hatch" has to do with
375
   * variables and assignments in theories (e.g., in arithmetic).
376
   * Let's say you introduce a new variable x at some deep decision
377
   * level (thanks to lazy registration, or a splitting lemma, or
378
   * whatever).  x might be mapped to something, but for theory
379
   * implementation simplicity shouldn't disappear from the map on
380
   * backjump; rather, it can take another (legal) value, or a special
381
   * value to indicate it needs to be recomputed.
382
   *
383
   * It is an error (checked via AlwaysAssert()) to
384
   * insertAtContextLevelZero() a key that already is in the map.
385
   */
386
32055
  void insertAtContextLevelZero(const Key& k, const Data& d) {
387
32055
    AlwaysAssert(d_map.find(k) == d_map.end());
388
389
32055
    Element* obj = new(true) Element(d_context, this, k, d,
390
                                     true /* atLevelZero */);
391
32055
    d_map.insert(std::make_pair(k, obj));
392
32055
  }
393
394
  // FIXME: no erase(), too much hassle to implement efficiently...
395
396
  using value_type = typename CDOhash_map<Key, Data, HashFcn>::value_type;
397
398
  class iterator {
399
    const Element* d_it;
400
401
   public:
402
    using iterator_category = std::input_iterator_tag;
403
    using value_type = typename CDOhash_map<Key, Data, HashFcn>::value_type;
404
    using difference_type = ptrdiff_t;
405
    using pointer = typename CDOhash_map<Key, Data, HashFcn>::value_type*;
406
    using reference = typename CDOhash_map<Key, Data, HashFcn>::value_type&;
407
408
638611183
    iterator(const Element* p) : d_it(p) {}
409
104
    iterator(const iterator& i) : d_it(i.d_it) {}
410
411
    // Default constructor
412
122483
    iterator() : d_it(nullptr) {}
413
414
    // (Dis)equality
415
85824648
    bool operator==(const iterator& i) const { return d_it == i.d_it; }
416
228073669
    bool operator!=(const iterator& i) const { return d_it != i.d_it; }
417
418
    // Dereference operators.
419
124827235
    const value_type& operator*() const { return d_it->getValue(); }
420
8120382
    const value_type* operator->() const { return &d_it->getValue(); }
421
422
    // Prefix increment
423
1284425
    iterator& operator++()
424
    {
425
1284425
      d_it = d_it->next();
426
1284425
      return *this;
427
    }
428
429
    // Postfix increment is not yet supported.
430
  };/* class CDHashMap<>::iterator */
431
432
  typedef iterator const_iterator;
433
434
362836
  iterator begin() const {
435
362836
    return iterator(d_first);
436
  }
437
438
450662973
  iterator end() const {
439
450662973
    return iterator(NULL);
440
  }
441
442
324522450
  iterator find(const Key& k) const {
443
324522450
    typename table_type::const_iterator i = d_map.find(k);
444
445
324522450
    if(i == d_map.end()) {
446
136937076
      return end();
447
    } else {
448
187585374
      return iterator((*i).second);
449
    }
450
  }
451
452
453
};/* class CDHashMap<> */
454
455
}/* CVC4::context namespace */
456
}/* CVC4 namespace */
457
458
#endif /* CVC4__CONTEXT__CDHASHMAP_H */