Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Morgan Deters, Mikolas Janota, Tim King
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 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.
11 : : * ****************************************************************************
12 : : *
13 : : * Context-dependent map class.
14 : : *
15 : : * Generic templated class for a map which must be saved and restored as
16 : : * contexts are pushed and popped. Requires that operator= be defined for the
17 : : * data class, and operator== for the key class. For key types that don't have
18 : : * a 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 "cvc5parser_public.h"
82 : :
83 : : #ifndef CVC5__CONTEXT__CDHASHMAP_H
84 : : #define CVC5__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 cvc5::context {
95 : :
96 : : // Auxiliary class: almost the same as CDO (see cdo.h)
97 : :
98 : : template <class Key, class Data, class HashFcn = std::hash<Key> >
99 : : class CDOhash_map : public ContextObj
100 : : {
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 : 123862373 : Key& mutable_key() { return const_cast<Key&>(d_value.first); }
122 : : // See documentation of value_type for why this is needed.
123 : 493914890 : 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 : 123866282 : ContextObj* save(ContextMemoryManager* pCMM) override
132 : : {
133 : 123866282 : return new (pCMM) CDOhash_map(*this);
134 : : }
135 : :
136 : 123862373 : void restore(ContextObj* data) override
137 : : {
138 : 123862373 : CDOhash_map* p = static_cast<CDOhash_map*>(data);
139 [ + + ]: 123862373 : if (d_map != NULL)
140 : : {
141 [ + + ]: 122757657 : if (p->d_map == NULL)
142 : : {
143 [ + - ][ + - ]: 241429144 : Assert(d_map->d_map.find(getKey()) != d_map->d_map.end()
[ - + ][ - - ]
144 : : && (*d_map->d_map.find(getKey())).second == this);
145 : : // no longer in map (popped beyond first level in which it was)
146 : 120714595 : d_map->d_map.erase(getKey());
147 : : // If we call deleteSelf() here, it re-enters restore(). So,
148 : : // put it on a "trash heap" instead, for later deletion.
149 : : //
150 : : // FIXME multithreading
151 [ + + ]: 120714595 : if (d_map->d_first == this)
152 : : {
153 [ + - ]: 3222343 : if (d_next == this)
154 : : {
155 [ - + ][ - + ]: 3222343 : Assert(d_prev == this);
[ - - ]
156 : 3222343 : d_map->d_first = NULL;
157 : : }
158 : : else
159 : : {
160 : 0 : d_map->d_first = d_next;
161 : : }
162 : : }
163 : 120714595 : d_next->d_prev = d_prev;
164 : 120714595 : d_prev->d_next = d_next;
165 : :
166 : : // this->deleteSelf();
167 : 120714595 : enqueueToGarbageCollect();
168 : : }
169 : : else
170 : : {
171 : 2043026 : mutable_data() = p->get();
172 : : }
173 : : }
174 : : // Explicitly call destructors for the key and the data as they will not
175 : : // otherwise get called.
176 : 123862373 : p->mutable_key().~Key();
177 : 123862373 : p->mutable_data().~Data();
178 : 123862373 : }
179 : :
180 : : /** ensure copy ctor is only called by us */
181 : 123866282 : CDOhash_map(const CDOhash_map& other)
182 : : : ContextObj(other),
183 : : // don't need to save the key---and if we do we can get
184 : : // refcounts for Node keys messed up and leak memory
185 : 123866282 : d_value(Key(), other.d_value.second),
186 : 123866282 : d_map(other.d_map),
187 : : d_prev(NULL),
188 : 123866282 : d_next(NULL)
189 : : {
190 : 123866282 : }
191 : : CDOhash_map& operator=(const CDOhash_map&) = delete;
192 : :
193 : : public:
194 : 191599669 : CDOhash_map(Context* context,
195 : : CDHashMap<Key, Data, HashFcn>* map,
196 : : const Key& key,
197 : : const Data& data)
198 : 191599669 : : ContextObj(context), d_value(key, data), d_map(NULL)
199 : : {
200 : : // Normal map insertion: first makeCurrent(), then set the data
201 : : // and then, later, the map. Order is important; we can't
202 : : // initialize d_map in the constructor init list above, because
203 : : // we want the restore of d_map to NULL to signal us to remove
204 : : // the element from the map.
205 : :
206 : 191599669 : set(data);
207 : 191599669 : d_map = map;
208 : :
209 : 191599669 : CDOhash_map*& first = d_map->d_first;
210 [ + + ]: 191599669 : if (first == NULL)
211 : : {
212 : 9193553 : first = d_next = d_prev = this;
213 : : }
214 : : else
215 : : {
216 : 182405913 : d_prev = first->d_prev;
217 : 182405913 : d_next = first;
218 : 182405913 : d_prev->d_next = this;
219 : 182405913 : first->d_prev = this;
220 : : }
221 : 191599669 : }
222 : :
223 : 191594851 : ~CDOhash_map() { destroy(); }
224 : :
225 : 368009766 : void set(const Data& data)
226 : : {
227 : 368009766 : makeCurrent();
228 : 368009766 : mutable_data() = data;
229 : 368009766 : }
230 : :
231 : 362143232 : const Key& getKey() const { return d_value.first; }
232 : :
233 : 56733823 : const Data& get() const { return d_value.second; }
234 : :
235 : 386536208 : const value_type& getValue() const { return d_value; }
236 : :
237 : 54674583 : operator Data() { return get(); }
238 : :
239 : 176278927 : const Data& operator=(const Data& data)
240 : : {
241 : 176278927 : set(data);
242 : 176278927 : return data;
243 : : }
244 : :
245 : 2644707 : CDOhash_map* next() const
246 : : {
247 [ + + ]: 2644707 : if (d_next == d_map->d_first)
248 : : {
249 : 267786 : return NULL;
250 : : }
251 : : else
252 : : {
253 : 2376921 : return d_next;
254 : : }
255 : : }
256 : : }; /* class CDOhash_map<> */
257 : :
258 : : /**
259 : : * Generic templated class for a map which must be saved and restored
260 : : * as contexts are pushed and popped. Requires that operator= be
261 : : * defined for the data class, and operator== for the key class.
262 : : */
263 : : template <class Key, class Data, class HashFcn>
264 : : class CDHashMap : public ContextObj
265 : : {
266 : : typedef CDOhash_map<Key, Data, HashFcn> Element;
267 : : typedef std::unordered_map<Key, Element*, HashFcn> table_type;
268 : :
269 : : friend class CDOhash_map<Key, Data, HashFcn>;
270 : :
271 : : table_type d_map;
272 : :
273 : : Element* d_first;
274 : : Context* d_context;
275 : :
276 : : // Nothing to save; the elements take care of themselves
277 : 0 : ContextObj* save(ContextMemoryManager* pCMM) override
278 : : {
279 : 0 : Unreachable();
280 : : SuppressWrongNoReturnWarning;
281 : : }
282 : :
283 : : // Similarly, nothing to restore
284 : 0 : void restore(ContextObj* data) override { Unreachable(); }
285 : :
286 : : // no copy or assignment
287 : : CDHashMap(const CDHashMap&) = delete;
288 : : CDHashMap& operator=(const CDHashMap&) = delete;
289 : :
290 : : public:
291 : 24137435 : CDHashMap(Context* context)
292 : 24137435 : : ContextObj(context), d_map(), d_first(NULL), d_context(context)
293 : : {
294 : 24137435 : }
295 : :
296 : 24103359 : ~CDHashMap()
297 : : {
298 : 24103359 : destroy();
299 : 24103359 : clear();
300 : 48206648 : }
301 : :
302 : 24103359 : void clear()
303 : : {
304 [ + + ]: 94983438 : for (auto& key_element_pair : d_map)
305 : : {
306 : : // mark it as being a destruction (short-circuit restore())
307 : 70880096 : Element* element = key_element_pair.second;
308 : 70880096 : element->d_map = nullptr;
309 : 70880096 : element->deleteSelf();
310 : : }
311 : 24103359 : d_map.clear();
312 : 24103359 : d_first = nullptr;
313 : 24103359 : }
314 : :
315 : : // The usual operators of map
316 : :
317 : 2285243 : size_t size() const { return d_map.size(); }
318 : :
319 : 23387361 : bool empty() const { return d_map.empty(); }
320 : :
321 : 656 : size_t count(const Key& k) const { return d_map.count(k); }
322 : :
323 : : // If a key is not present, a new object is created and inserted
324 : 230969880 : Element& operator[](const Key& k)
325 : : {
326 : 230969880 : const auto res = d_map.insert({k, nullptr});
327 [ + + ]: 230969880 : if (res.second)
328 : : { // create new object
329 : 125632667 : res.first->second = new (true) Element(d_context, this, k, Data());
330 : : }
331 : 230969880 : return *(res.first->second);
332 : : }
333 : :
334 : 66098011 : bool insert(const Key& k, const Data& d)
335 : : {
336 : 66098011 : const auto res = d_map.insert({k, nullptr});
337 [ + + ]: 66098011 : if (res.second)
338 : : { // create new object
339 : 65966951 : res.first->second = new (true) Element(d_context, this, k, d);
340 : : }
341 : : else
342 : : {
343 : 131096 : res.first->second->set(d);
344 : : }
345 : 66098011 : return res.second;
346 : : }
347 : :
348 : : // FIXME: no erase(), too much hassle to implement efficiently...
349 : :
350 : : using value_type = typename CDOhash_map<Key, Data, HashFcn>::value_type;
351 : :
352 : : class iterator
353 : : {
354 : : const Element* d_it;
355 : :
356 : : public:
357 : : using iterator_category = std::forward_iterator_tag;
358 : : using value_type = typename CDOhash_map<Key, Data, HashFcn>::value_type;
359 : : using difference_type = ptrdiff_t;
360 : : using pointer = typename CDOhash_map<Key, Data, HashFcn>::value_type*;
361 : : using reference = typename CDOhash_map<Key, Data, HashFcn>::value_type&;
362 : :
363 : 1622495668 : iterator(const Element* p) : d_it(p) {}
364 : 52 : iterator(const iterator& i) : d_it(i.d_it) {}
365 : :
366 : : // Default constructor
367 : 62447452 : iterator() : d_it(nullptr) {}
368 : :
369 : : // (Dis)equality
370 : 303894994 : bool operator==(const iterator& i) const { return d_it == i.d_it; }
371 : 493692417 : bool operator!=(const iterator& i) const { return d_it != i.d_it; }
372 : :
373 : : // Dereference operators.
374 : 358390616 : const value_type& operator*() const { return d_it->getValue(); }
375 : 28145616 : const value_type* operator->() const { return &d_it->getValue(); }
376 : :
377 : : // Prefix increment
378 : 2644707 : iterator& operator++()
379 : : {
380 : 2644707 : d_it = d_it->next();
381 : 2644707 : return *this;
382 : : }
383 : :
384 : : // Postfix increment is not yet supported.
385 : : }; /* class CDHashMap<>::iterator */
386 : :
387 : : typedef iterator const_iterator;
388 : :
389 : 830386 : iterator begin() const { return iterator(d_first); }
390 : :
391 : 1160922367 : iterator end() const { return iterator(NULL); }
392 : :
393 : 824365780 : iterator find(const Key& k) const
394 : : {
395 : 824365780 : typename table_type::const_iterator i = d_map.find(k);
396 : :
397 [ + + ]: 824365780 : if (i == d_map.end())
398 : : {
399 : 363623376 : return end();
400 : : }
401 : : else
402 : : {
403 : 460742537 : return iterator((*i).second);
404 : : }
405 : : }
406 : :
407 : : }; /* class CDHashMap<> */
408 : :
409 : : } // namespace cvc5::context
410 : :
411 : : #endif /* CVC5__CONTEXT__CDHASHMAP_H */
|
