Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * Context-dependent map class.
11 : : *
12 : : * Generic templated class for a map which must be saved and restored as
13 : : * contexts are pushed and popped. Requires that operator= be defined for the
14 : : * data class, and operator== for the key class. For key types that don't have
15 : : * a std::hash<>, you should provide an explicit HashFcn.
16 : : *
17 : : * See also:
18 : : * CDInsertHashMap : An "insert-once" CD hash map.
19 : : * CDTrailHashMap : A lightweight CD hash map with poor iteration
20 : : * characteristics and some quirks in usage.
21 : : *
22 : : * Internal documentation:
23 : : *
24 : : * CDHashMap<> 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 : : * CDOhash_maps that may be useful in figuring out this mess:
28 : : *
29 : : * So you have a CDHashMap<>.
30 : : *
31 : : * You insert some (key,value) pairs. Each allocates a CDOhash_map<>
32 : : * and goes on a doubly-linked list headed by map.d_first and
33 : : * threaded via CDOhash_map.{d_prev,d_next}. CDOhash_maps 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 CDOhash_map 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 CDHashMap, its
42 : : * associated CDOhash_map calls makeCurrent(), then sets the new
43 : : * value. The save object is also a CDOhash_map (allocated in context
44 : : * memory).
45 : : *
46 : : * Now, CDOhash_maps 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. CDOhash_map::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 CDOhash_map object memory freed. Here, the CDOhash_map 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 its scope.
59 : : *
60 : : * Third, you might delete the cdhashmap(calling CDHashMap::~CDHashMap()).
61 : : * This first calls destroy(), as per ContextObj contract, but
62 : : * cdhashmapdoesn't save/restore itself, so that does nothing at the
63 : : * CDHashMap-level. Then, for each element in the map, it marks it as being
64 : : * "part of a complete map destruction", which essentially short-circuits
65 : : * CDOhash_map::restore() (see CDOhash_map::restore()), then deallocates
66 : : * it.
67 : : *
68 : : * Fourth, you might clear() the CDHashMap. This does exactly the
69 : : * same as CDHashMap::~CDHashMap(), except that it doesn't call destroy()
70 : : * on itself.
71 : : *
72 : : * ContextObj::deleteSelf() calls the CDOhash_map destructor, then
73 : : * frees the memory associated to the CDOhash_map.
74 : : * CDOhash_map::~CDOhash_map() calls destroy(), which restores as much as
75 : : * possible.
76 : : */
77 : :
78 : : #include "cvc5parser_public.h"
79 : :
80 : : #ifndef CVC5__CONTEXT__CDHASHMAP_H
81 : : #define CVC5__CONTEXT__CDHASHMAP_H
82 : :
83 : : #include <functional>
84 : : #include <iterator>
85 : : #include <unordered_map>
86 : :
87 : : #include "base/check.h"
88 : : #include "context/cdhashmap_forward.h"
89 : : #include "context/context.h"
90 : :
91 : : namespace cvc5::context {
92 : :
93 : : // Auxiliary class: almost the same as CDO (see cdo.h)
94 : :
95 : : template <class Key, class Data, class HashFcn = std::hash<Key> >
96 : : class CDOhash_map : public ContextObj
97 : : {
98 : : friend class CDHashMap<Key, Data, HashFcn>;
99 : :
100 : : public:
101 : : // The type of the <Key, Data> pair mapped by this class.
102 : : //
103 : : // Implementation:
104 : : // The data and key visible to users of CDHashMap are only visible through
105 : : // const references. Thus the type of dereferencing a
106 : : // CDHashMap<Key, Data>::iterator.second is intended to always be a
107 : : // `const Data&`. (Otherwise, to get a Data& safely, access operations
108 : : // would need to makeCurrent() to get the Data&, which is an unacceptable
109 : : // performance hit.) To allow for the desired updating in other scenarios, we
110 : : // store a std::pair<const Key, const Data> and break the const encapsulation
111 : : // when necessary.
112 : : using value_type = std::pair<const Key, const Data>;
113 : :
114 : : private:
115 : : value_type d_value;
116 : :
117 : : // See documentation of value_type for why this is needed.
118 : 139641146 : Key& mutable_key() { return const_cast<Key&>(d_value.first); }
119 : : // See documentation of value_type for why this is needed.
120 : 523163660 : Data& mutable_data() { return const_cast<Data&>(d_value.second); }
121 : :
122 : : CDHashMap<Key, Data, HashFcn>* d_map;
123 : :
124 : : // Doubly-linked list for keeping track of elements in order of insertion
125 : : CDOhash_map* d_prev;
126 : : CDOhash_map* d_next;
127 : :
128 : 139646577 : ContextObj* save(ContextMemoryManager* pCMM) override
129 : : {
130 : 139646577 : return new (pCMM) CDOhash_map(*this);
131 : : }
132 : :
133 : 139641146 : void restore(ContextObj* data) override
134 : : {
135 : 139641146 : CDOhash_map* p = static_cast<CDOhash_map*>(data);
136 [ + + ]: 139641146 : if (d_map != nullptr)
137 : : {
138 [ + + ]: 138701343 : if (p->d_map == nullptr)
139 : : {
140 [ + - ][ + - ]: 136465177 : Assert(d_map->d_map.find(getKey()) != d_map->d_map.end()
[ - + ][ - + ]
[ - - ]
141 : : && (*d_map->d_map.find(getKey())).second == this);
142 : : // no longer in map (popped beyond first level in which it was)
143 : 136465177 : d_map->d_map.erase(getKey());
144 : : // If we call deleteSelf() here, it re-enters restore(). So,
145 : : // put it on a "trash heap" instead, for later deletion.
146 : : //
147 [ + + ]: 136465177 : if (d_map->d_first == this)
148 : : {
149 [ + - ]: 3660360 : if (d_next == this)
150 : : {
151 [ - + ][ - + ]: 3660360 : Assert(d_prev == this);
[ - - ]
152 : 3660360 : d_map->d_first = nullptr;
153 : : }
154 : : else
155 : : {
156 : 0 : d_map->d_first = d_next;
157 : : }
158 : : }
159 : 136465177 : d_next->d_prev = d_prev;
160 : 136465177 : d_prev->d_next = d_next;
161 : :
162 : : // this->deleteSelf();
163 : 136465177 : enqueueToGarbageCollect();
164 : : }
165 : : else
166 : : {
167 : 2236166 : 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 : 139641146 : p->mutable_key().~Key();
173 : 139641146 : p->mutable_data().~Data();
174 : 139641146 : }
175 : :
176 : : /** ensure copy ctor is only called by us */
177 : 139646577 : 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 : 140541610 : d_value(Key(), other.d_value.second),
182 : 139646577 : d_map(other.d_map),
183 : 139646577 : d_prev(nullptr),
184 : 139646577 : d_next(nullptr)
185 : : {
186 : 139646577 : }
187 : : CDOhash_map& operator=(const CDOhash_map&) = delete;
188 : :
189 : : public:
190 : 199355985 : CDOhash_map(Context* context,
191 : : CDHashMap<Key, Data, HashFcn>* map,
192 : : const Key& key,
193 : : const Data& data)
194 : 199355985 : : ContextObj(context), d_value(key, data), d_map(nullptr)
195 : : {
196 : : // Normal map insertion: first makeCurrent(), then set the data
197 : : // and then, later, the map. Order is important; we can't
198 : : // initialize d_map in the constructor init list above, because
199 : : // we want the restore of d_map to NULL to signal us to remove
200 : : // the element from the map.
201 : :
202 : 199355985 : set(data);
203 : 199355985 : d_map = map;
204 : :
205 : 199355985 : CDOhash_map*& first = d_map->d_first;
206 [ + + ]: 199355985 : if (first == nullptr)
207 : : {
208 : 10673218 : first = d_next = d_prev = this;
209 : : }
210 : : else
211 : : {
212 : 188682767 : d_prev = first->d_prev;
213 : 188682767 : d_next = first;
214 : 188682767 : d_prev->d_next = this;
215 : 188682767 : first->d_prev = this;
216 : : }
217 : 199355985 : }
218 : :
219 : 199350189 : ~CDOhash_map() { destroy(); }
220 : :
221 : 381286348 : void set(const Data& data)
222 : : {
223 : 381286348 : makeCurrent();
224 : 381286348 : mutable_data() = data;
225 : 381286348 : }
226 : :
227 : 409395531 : const Key& getKey() const { return d_value.first; }
228 : :
229 : 59148429 : const Data& get() const { return d_value.second; }
230 : :
231 : 352122152 : const value_type& getValue() const { return d_value; }
232 : :
233 : 56893472 : operator Data() { return get(); }
234 : :
235 : 181439194 : const Data& operator=(const Data& data)
236 : : {
237 : 181439194 : set(data);
238 : 181439194 : return data;
239 : : }
240 : :
241 : 2977777 : CDOhash_map* next() const
242 : : {
243 [ + + ]: 2977777 : if (d_next == d_map->d_first)
244 : : {
245 : 292607 : return nullptr;
246 : : }
247 : : else
248 : : {
249 : 2685170 : return d_next;
250 : : }
251 : : }
252 : : }; /* class CDOhash_map<> */
253 : :
254 : : /**
255 : : * Generic templated class for a map which must be saved and restored
256 : : * as contexts are pushed and popped. Requires that operator= be
257 : : * defined for the data class, and operator== for the key class.
258 : : */
259 : : template <class Key, class Data, class HashFcn>
260 : : class CDHashMap : public ContextObj
261 : : {
262 : : typedef CDOhash_map<Key, Data, HashFcn> Element;
263 : : typedef std::unordered_map<Key, Element*, HashFcn> table_type;
264 : :
265 : : friend class CDOhash_map<Key, Data, HashFcn>;
266 : :
267 : : table_type d_map;
268 : :
269 : : Element* d_first;
270 : : Context* d_context;
271 : :
272 : : // Nothing to save; the elements take care of themselves
273 : 0 : ContextObj* save(CVC5_UNUSED ContextMemoryManager* pCMM) override
274 : : {
275 : 0 : Unreachable();
276 : : SuppressWrongNoReturnWarning;
277 : : }
278 : :
279 : : // Similarly, nothing to restore
280 : 0 : void restore(CVC5_UNUSED ContextObj* data) override { Unreachable(); }
281 : :
282 : : // no copy or assignment
283 : : CDHashMap(const CDHashMap&) = delete;
284 : : CDHashMap& operator=(const CDHashMap&) = delete;
285 : :
286 : : public:
287 : 27945685 : CDHashMap(Context* context)
288 : 27945685 : : ContextObj(context), d_map(), d_first(nullptr), d_context(context)
289 : : {
290 : 27945685 : }
291 : :
292 : 27900418 : ~CDHashMap()
293 : : {
294 : 27900418 : destroy();
295 : 27900418 : clear();
296 : 55800836 : }
297 : :
298 : 27900418 : void clear()
299 : : {
300 [ + + ]: 90785430 : for (auto& key_element_pair : d_map)
301 : : {
302 : : // mark it as being a destruction (short-circuit restore())
303 : 62885012 : Element* element = key_element_pair.second;
304 : 62885012 : element->d_map = nullptr;
305 : 62885012 : element->deleteSelf();
306 : : }
307 : 27900418 : d_map.clear();
308 : 27900418 : d_first = nullptr;
309 : 27900418 : }
310 : :
311 : : // The usual operators of map
312 : :
313 : 2528381 : size_t size() const { return d_map.size(); }
314 : :
315 : 24389898 : bool empty() const { return d_map.empty(); }
316 : :
317 : 892 : size_t count(const Key& k) const { return d_map.count(k); }
318 : :
319 : : // If a key is not present, a new object is created and inserted
320 : 238351457 : Element& operator[](const Key& k)
321 : : {
322 : 238351457 : const auto res = d_map.insert({k, nullptr});
323 [ + + ]: 238351457 : if (res.second)
324 : : { // create new object
325 : 133864701 : res.first->second = new (true) Element(d_context, this, k, Data());
326 : : }
327 : 238351457 : return *(res.first->second);
328 : : }
329 : :
330 : 65982453 : bool insert(const Key& k, const Data& d)
331 : : {
332 : 65982453 : const auto res = d_map.insert({k, nullptr});
333 [ + + ]: 65982453 : if (res.second)
334 : : { // create new object
335 : 65491284 : res.first->second = new (true) Element(d_context, this, k, d);
336 : : }
337 : : else
338 : : {
339 : 491169 : res.first->second->set(d);
340 : : }
341 : 65982453 : return res.second;
342 : : }
343 : :
344 : : // Note: no erase(), too much hassle to implement efficiently...
345 : :
346 : : using value_type = typename CDOhash_map<Key, Data, HashFcn>::value_type;
347 : :
348 : : class iterator
349 : : {
350 : : const Element* d_it;
351 : :
352 : : public:
353 : : using iterator_category = std::forward_iterator_tag;
354 : : using value_type = typename CDOhash_map<Key, Data, HashFcn>::value_type;
355 : : using difference_type = ptrdiff_t;
356 : : using pointer = typename CDOhash_map<Key, Data, HashFcn>::value_type*;
357 : : using reference = typename CDOhash_map<Key, Data, HashFcn>::value_type&;
358 : :
359 : 1614100113 : iterator(const Element* p) : d_it(p) {}
360 : :
361 : : // Default constructor
362 : 65168149 : iterator() : d_it(nullptr) {}
363 : :
364 : : // (Dis)equality
365 : 244482709 : bool operator==(const iterator& i) const { return d_it == i.d_it; }
366 : 549051204 : bool operator!=(const iterator& i) const { return d_it != i.d_it; }
367 : :
368 : : // Dereference operators.
369 : 323416454 : const value_type& operator*() const { return d_it->getValue(); }
370 : 28705698 : const value_type* operator->() const { return &d_it->getValue(); }
371 : :
372 : : // Prefix increment
373 : 2977777 : iterator& operator++()
374 : : {
375 : 2977777 : d_it = d_it->next();
376 : 2977777 : return *this;
377 : : }
378 : :
379 : : // Postfix increment is not yet supported.
380 : : }; /* class CDHashMap<>::iterator */
381 : :
382 : : typedef iterator const_iterator;
383 : :
384 : 906991 : iterator begin() const { return iterator(d_first); }
385 : :
386 : 1180433446 : iterator end() const { return iterator(nullptr); }
387 : :
388 : 819926904 : iterator find(const Key& k) const
389 : : {
390 : 819926904 : typename table_type::const_iterator i = d_map.find(k);
391 : :
392 [ + + ]: 819926904 : if (i == d_map.end())
393 : : {
394 : 387167228 : return end();
395 : : }
396 : : else
397 : : {
398 : 432759676 : return iterator((*i).second);
399 : : }
400 : : }
401 : :
402 : : }; /* class CDHashMap<> */
403 : :
404 : : } // namespace cvc5::context
405 : :
406 : : #endif /* CVC5__CONTEXT__CDHASHMAP_H */
|
