1 /********************* */
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
14 ** \brief Context-dependent map class.
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.
22 ** Internal documentation:
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:
29 ** So you have a CDMap<>.
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.)
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
46 ** Now, CDOmaps disappear in a variety of ways.
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.
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
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
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).
77 ** Fifth, you might clear() the CDMap. This does exactly the
78 ** same as CDMap::~CDMap(), except that it doesn't call destroy()
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.)
90 #include "cvc4_private.h"
92 #ifndef __CVC4__CONTEXT__CDMAP_H
93 #define __CVC4__CONTEXT__CDMAP_H
95 #include "context/context.h"
96 #include "util/Assert.h"
100 #include <ext/hash_map>
105 // Auxiliary class: almost the same as CDO (see cdo.h)
107 template <class Key
, class Data
, class HashFcn
= __gnu_cxx::hash
<Key
> > class CDMap
;
109 template <class Key
, class Data
, class HashFcn
= __gnu_cxx::hash
<Key
> >
110 class CDOmap
: public ContextObj
{
111 friend class CDMap
<Key
, Data
, HashFcn
>;
115 CDMap
<Key
, Data
, HashFcn
>* d_map
;
117 /** never put this cdmap element on the trash */
120 // Doubly-linked list for keeping track of elements in order of insertion
124 virtual ContextObj
* save(ContextMemoryManager
* pCMM
) {
125 return new(pCMM
) CDOmap(*this);
128 virtual void restore(ContextObj
* data
) {
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.
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
;
143 Assert(d_prev
== this);
144 d_map
->d_first
= NULL
;
146 d_map
->d_first
= d_next
;
149 Debug("gc") << "remove nonfirst-elem " << this << " from map " << d_map
<< std::endl
;
151 d_next
->d_prev
= d_prev
;
152 d_prev
->d_next
= d_next
;
154 Debug("gc") << "CDMap<> no-trash " << this << std::endl
;
156 Debug("gc") << "CDMap<> trash push_back " << this << std::endl
;
157 //this->deleteSelf();
158 d_map
->d_trash
.push_back(this);
166 /** ensure copy ctor is only called by us */
167 CDOmap(const CDOmap
& other
) :
170 d_data(other
.d_data
),
178 CDOmap(Context
* context
,
179 CDMap
<Key
, Data
, HashFcn
>* map
,
182 bool atLevelZero
= false,
183 bool allocatedInCMM
= false) :
184 ContextObj(allocatedInCMM
, context
),
187 d_noTrash(allocatedInCMM
) {
189 // untested, probably unsafe.
190 Assert(!(atLevelZero
&& allocatedInCMM
));
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().
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.
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();
216 CDOmap
*& first
= d_map
->d_first
;
218 first
= d_next
= d_prev
= this;
219 Debug("gc") << "add first-elem " << this << " to map " << d_map
<< std::endl
;
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
;
224 d_prev
->d_next
= this;
225 first
->d_prev
= this;
229 ~CDOmap() throw(AssertionException
) {
233 void set(const Data
& data
) {
238 const Key
& getKey() const {
242 const Data
& get() const {
250 const Data
& operator=(const Data
& data
) {
255 CDOmap
* next() const {
256 if(d_next
== d_map
->d_first
) {
262 };/* class CDOmap<> */
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.
270 template <class Key
, class Data
, class HashFcn
>
271 class CDMap
: public ContextObj
{
273 typedef CDOmap
<Key
, Data
, HashFcn
> Element
;
274 typedef __gnu_cxx::hash_map
<Key
, Element
*, HashFcn
> table_type
;
276 friend class CDOmap
<Key
, Data
, HashFcn
>;
283 std::vector
<Element
*> d_trash
;
285 // Nothing to save; the elements take care of themselves
286 virtual ContextObj
* save(ContextMemoryManager
* pCMM
) {
290 // Similarly, nothing to restore
291 virtual void restore(ContextObj
* data
) {
296 //FIXME multithreading
297 for(typename
std::vector
<Element
*>::iterator i
= d_trash
.begin();
300 Debug("gc") << "emptyTrash(): " << *i
<< std::endl
;
308 CDMap(Context
* context
) :
316 ~CDMap() throw(AssertionException
) {
317 Debug("gc") << "cdmap " << this
318 << " disappearing, destroying..." << std::endl
;
320 Debug("gc") << "cdmap " << this
321 << " disappearing, done destroying" << std::endl
;
323 Debug("gc") << "cdmap " << this << " gone, emptying trash" << std::endl
;
325 Debug("gc") << "done emptying trash for " << this << std::endl
;
327 for(typename
table_type::iterator i
= d_map
.begin();
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();
339 Assert(d_trash
.empty());
342 void clear() throw(AssertionException
) {
343 Debug("gc") << "clearing cdmap " << this << ", emptying trash" << std::endl
;
345 Debug("gc") << "done emptying trash for " << this << std::endl
;
347 for(typename
table_type::iterator i
= d_map
.begin();
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();
359 Assert(d_trash
.empty());
362 // The usual operators of map
364 size_t size() const {
368 size_t count(const Key
& k
) const {
369 return d_map
.count(k
);
372 // If a key is not present, a new object is created and inserted
373 Element
& operator[](const Key
& k
) {
376 typename
table_type::iterator i
= d_map
.find(k
);
379 if(i
== d_map
.end()) {// create new object
380 obj
= new(true) Element(d_context
, this, k
, Data());
388 bool insert(const Key
& k
, const Data
& d
) {
391 typename
table_type::iterator i
= d_map
.find(k
);
393 if(i
== d_map
.end()) {// create new object
394 Element
* obj
= new(true) Element(d_context
, this, k
, d
);
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
) {
409 AlwaysAssert(d_map
.find(k
) == d_map
.end());
411 Element
* obj
= new(d_context
->getCMM()) Element(d_context
, this, k
, d
,
412 false /* atLevelZero */,
413 true /* allocatedInCMM */);
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):
427 * map.insertAtContextLevelZero(k, v1);
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.
439 * It is an error (checked via AlwaysAssert()) to
440 * insertAtContextLevelZero() a key that already is in the map.
442 void insertAtContextLevelZero(const Key
& k
, const Data
& d
) {
445 AlwaysAssert(d_map
.find(k
) == d_map
.end());
447 Element
* obj
= new(true) Element(d_context
, this, k
, d
,
448 true /* atLevelZero */);
452 // FIXME: no erase(), too much hassle to implement efficiently...
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.)
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
467 (*i
).second
->~Element();
468 // Writing ...->~CDOmap() in the above is legal (?) but breaks
469 // g++ 4.1, though later versions have no problem.
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
;
478 if(elt
->d_next
== elt
) {
479 Assert(elt
->d_prev
== elt
);
482 d_first
= elt
->d_next
;
485 elt
->d_prev
->d_next
= elt
->d_next
;
486 elt
->d_next
->d_prev
= elt
->d_prev
;
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
);
503 iterator(const Element
* p
) : d_it(p
) {}
504 iterator(const iterator
& i
) : d_it(i
.d_it
) {}
506 // Default constructor
510 bool operator==(const iterator
& i
) const {
511 return d_it
== i
.d_it
;
513 bool operator!=(const iterator
& i
) const {
514 return d_it
!= i
.d_it
;
517 // Dereference operators.
518 std::pair
<const Key
, Data
> operator*() const {
519 return std::pair
<const Key
, Data
>(d_it
->getKey(), d_it
->get());
523 iterator
& operator++() {
528 // Postfix increment: requires a Proxy object to hold the
529 // intermediate value for dereferencing
531 const std::pair
<const Key
, Data
>* d_pair
;
535 Proxy(const std::pair
<const Key
, Data
>& p
) : d_pair(&p
) {}
537 const std::pair
<const Key
, Data
>& operator*() const {
540 };/* class CDMap<>::iterator::Proxy */
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) {
551 };/* class CDMap<>::iterator */
553 typedef iterator const_iterator
;
555 iterator
begin() const {
556 return iterator(d_first
);
559 iterator
end() const {
560 return iterator(NULL
);
563 iterator
find(const Key
& k
) const {
564 typename
table_type::const_iterator i
= d_map
.find(k
);
566 if(i
== d_map
.end()) {
569 return iterator((*i
).second
);
573 iterator
find(const Key
& k
) {
575 return const_cast<const CDMap
*>(this)->find(k
);
578 };/* class CDMap<> */
580 }/* CVC4::context namespace */
581 }/* CVC4 namespace */
583 #endif /* __CVC4__CONTEXT__CDMAP_H */