diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-10-12 20:20:24 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-10-12 20:20:24 +0000 |
commit | 2bc4c351bbf89103577fa9f33ebb395f5d61826a (patch) | |
tree | 37345ddbee75fc7405868afd3de8b7c2ffdd0fdc /src/context | |
parent | ec320b78deaaf31bdae1b8b048f66cfb1b3a4197 (diff) |
Merge from cc-memout branch. Here are the main points
* Add ContextMemoryAllocator<T> allocator type, conforming to
STL allocator requirements.
* Extend the CDList<> template to take an allocator (defaults
to std::allocator<T>).
* Add a specialized version of the CDList<> template (in
src/context/cdlist_context_memory.h) that allocates a list
in segments, in context memory.
* Add "forward" headers -- cdlist_forward.h, cdmap_forward.h,
and cdset_forward.h. Use these in public headers, and other
places where you don't need the full header (just the
forward-declaration). These types justify their own header
(instead of just forward-declaring yourself), because they
are complex templated types, with default template parameters,
specializations, etc.
* theory_engine.h no longer depends on individual theory headers.
(Instead it forward-declares Theory implementations.) This is
especially important now that theory .cpp files depend on
TheoryEngine (to implement Theory::getValue()). Previously,
any modification to any theory header file required *all*
theories, and the engine, to be completely rebuilt.
* Support memory cleanup for nontrivial CONSTANT kinds. This
resolves an issue with arithmetic where memory leaked for
each distinct Rational or Integer that was wrapped in a Node.
Diffstat (limited to 'src/context')
-rw-r--r-- | src/context/Makefile.am | 4 | ||||
-rw-r--r-- | src/context/cdlist.h | 233 | ||||
-rw-r--r-- | src/context/cdlist_context_memory.h | 493 | ||||
-rw-r--r-- | src/context/cdlist_forward.h | 56 | ||||
-rw-r--r-- | src/context/context_mm.cpp | 1 | ||||
-rw-r--r-- | src/context/context_mm.h | 65 |
6 files changed, 780 insertions, 72 deletions
diff --git a/src/context/Makefile.am b/src/context/Makefile.am index 398de65a3..9e349a06b 100644 --- a/src/context/Makefile.am +++ b/src/context/Makefile.am @@ -12,6 +12,10 @@ libcontext_la_SOURCES = \ context_mm.h \ cdo.h \ cdlist.h \ + cdlist_context_memory.h \ + cdlist_forward.h \ cdmap.h \ + cdmap_forward.h \ cdset.h \ + cdset_forward.h \ cdvector.h diff --git a/src/context/cdlist.h b/src/context/cdlist.h index 02418d3df..7edef4121 100644 --- a/src/context/cdlist.h +++ b/src/context/cdlist.h @@ -22,23 +22,42 @@ #define __CVC4__CONTEXT__CDLIST_H #include <iterator> +#include <memory> +#include <string> +#include <sstream> #include "context/context.h" +#include "context/context_mm.h" +#include "context/cdlist_forward.h" #include "util/Assert.h" namespace CVC4 { namespace context { /** - * Generic context-dependent dynamic array. Note that for efficiency, this - * implementation makes the following assumptions: + * Generic context-dependent dynamic array. Note that for efficiency, + * this implementation makes the following assumptions: + * * 1. Over time, objects are only added to the list. Objects are only * removed when a pop restores the list to a previous state. + * * 2. T objects can safely be copied using their copy constructor, * operator=, and memcpy. */ -template <class T> +template <class T, class AllocatorT> class CDList : public ContextObj { +public: + + /** The value type with which this CDList<> was instantiated. */ + typedef T value_type; + /** The allocator type with which this CDList<> was instantiated. */ + typedef AllocatorT Allocator; + +protected: + + static const size_t INITIAL_SIZE = 10; + static const size_t GROWTH_FACTOR = 2; + /** * d_list is a dynamic array of objects of type T. */ @@ -54,55 +73,33 @@ class CDList : public ContextObj { /** * Number of objects in d_list */ - unsigned d_size; + size_t d_size; /** * Allocated size of d_list. */ - unsigned d_sizeAlloc; - -protected: + size_t d_sizeAlloc; /** - * Implementation of mandatory ContextObj method save: simply copies the - * current size to a copy using the copy constructor (the pointer and the - * allocated size are *not* copied as they are not restored on a pop). - * The saved information is allocated using the ContextMemoryManager. + * Our allocator. */ - ContextObj* save(ContextMemoryManager* pCMM) { - return new(pCMM) CDList<T>(*this); - } - - /** - * Implementation of mandatory ContextObj method restore: simply restores the - * previous size. Note that the list pointer and the allocated size are not - * changed. - */ - void restore(ContextObj* data) { - if(d_callDestructor) { - unsigned size = ((CDList<T>*)data)->d_size; - while(d_size != size) { - --d_size; - d_list[d_size].~T(); - } - } else { - d_size = ((CDList<T>*)data)->d_size; - } - } - -private: + Allocator d_allocator; /** - * Private copy constructor used only by save above. d_list and d_sizeAlloc - * are not copied: only the base class information and d_size are needed in - * restore. + * Private copy constructor used only by save(). d_list and + * d_sizeAlloc are not copied: only the base class information and + * d_size are needed in restore. */ - CDList(const CDList<T>& l) : + CDList(const CDList<T, Allocator>& l) : ContextObj(l), d_list(NULL), - d_callDestructor(l.d_callDestructor), + d_callDestructor(false), d_size(l.d_size), - d_sizeAlloc(0) { + d_sizeAlloc(0), + d_allocator(l.d_allocator) { + Debug("cdlist") << "copy ctor: " << this + << " from " << &l + << " size " << d_size << std::endl; } /** @@ -112,64 +109,133 @@ private: void grow() { if(d_list == NULL) { // Allocate an initial list if one does not yet exist - d_sizeAlloc = 10; - d_list = (T*) malloc(sizeof(T) * d_sizeAlloc); + d_sizeAlloc = INITIAL_SIZE; + Debug("cdlist") << "initial grow of cdlist " << this + << " level " << getContext()->getLevel() + << " to " << d_sizeAlloc << std::endl; + if(d_sizeAlloc > d_allocator.max_size()) { + d_sizeAlloc = d_allocator.max_size(); + } + d_list = d_allocator.allocate(d_sizeAlloc); if(d_list == NULL) { throw std::bad_alloc(); } } else { // Allocate a new array with double the size - d_sizeAlloc *= 2; - T* tmpList = (T*) realloc(d_list, sizeof(T) * d_sizeAlloc); - if(tmpList == NULL) { + size_t newSize = GROWTH_FACTOR * d_sizeAlloc; + if(newSize > d_allocator.max_size()) { + newSize = d_allocator.max_size(); + Assert(newSize > d_sizeAlloc, + "cannot request larger list due to allocator limits"); + } + T* newList = d_allocator.allocate(newSize); + Debug("cdlist") << "2x grow of cdlist " << this + << " level " << getContext()->getLevel() + << " to " << newSize + << " (from " << d_list + << " to " << newList << ")" << std::endl; + if(newList == NULL) { throw std::bad_alloc(); } - d_list = tmpList; + std::memcpy(newList, d_list, sizeof(T) * d_sizeAlloc); + d_allocator.deallocate(d_list, d_sizeAlloc); + d_list = newList; + d_sizeAlloc = newSize; + } + } + + /** + * Implementation of mandatory ContextObj method save: simply copies + * the current size to a copy using the copy constructor (the + * pointer and the allocated size are *not* copied as they are not + * restored on a pop). The saved information is allocated using the + * ContextMemoryManager. + */ + ContextObj* save(ContextMemoryManager* pCMM) { + ContextObj* data = new(pCMM) CDList<T, Allocator>(*this); + Debug("cdlist") << "save " << this + << " at level " << this->getContext()->getLevel() + << " size at " << this->d_size + << " sizeAlloc at " << this->d_sizeAlloc + << " d_list is " << this->d_list + << " data:" << data << std::endl; + return data; + } + + /** + * Implementation of mandatory ContextObj method restore: simply + * restores the previous size. Note that the list pointer and the + * allocated size are not changed. + */ + void restore(ContextObj* data) { + Debug("cdlist") << "restore " << this + << " level " << this->getContext()->getLevel() + << " data == " << data + << " call dtor == " << this->d_callDestructor + << " d_list == " << this->d_list << std::endl; + if(this->d_callDestructor) { + const size_t size = ((CDList<T, Allocator>*)data)->d_size; + while(this->d_size != size) { + --this->d_size; + this->d_allocator.destroy(&this->d_list[this->d_size]); + } + } else { + this->d_size = ((CDList<T, Allocator>*)data)->d_size; } + Debug("cdlist") << "restore " << this + << " level " << this->getContext()->getLevel() + << " size back to " << this->d_size + << " sizeAlloc at " << this->d_sizeAlloc << std::endl; } public: + /** * Main constructor: d_list starts as NULL, size is 0 */ - CDList(Context* context, bool callDestructor = true) : + CDList(Context* context, bool callDestructor = true, + const Allocator& alloc = Allocator()) : ContextObj(context), d_list(NULL), d_callDestructor(callDestructor), d_size(0), - d_sizeAlloc(0) { + d_sizeAlloc(0), + d_allocator(alloc) { } /** * Main constructor: d_list starts as NULL, size is 0 */ - CDList(bool allocatedInCMM, Context* context, bool callDestructor = true) : + CDList(bool allocatedInCMM, Context* context, bool callDestructor = true, + const Allocator& alloc = Allocator()) : ContextObj(allocatedInCMM, context), d_list(NULL), d_callDestructor(callDestructor), d_size(0), - d_sizeAlloc(0) { + d_sizeAlloc(0), + d_allocator(alloc) { } /** * Destructor: delete the list */ ~CDList() throw(AssertionException) { - destroy(); + this->destroy(); - if(d_callDestructor) { - for(unsigned i = 0; i < d_size; ++i) { - d_list[i].~T(); + if(this->d_callDestructor) { + for(size_t i = 0; i < this->d_size; ++i) { + this->d_allocator.destroy(&this->d_list[i]); } } - free(d_list); + this->d_allocator.deallocate(this->d_list, this->d_sizeAlloc); } /** - * Return the current size of (i.e. valid number of objects in) the list + * Return the current size of (i.e. valid number of objects in) the + * list. */ - unsigned size() const { + size_t size() const { return d_size; } @@ -184,20 +250,43 @@ public: * Add an item to the end of the list. */ void push_back(const T& data) { + Debug("cdlist") << "push_back " << this + << " " << getContext()->getLevel() + << ": make-current, " + << "d_list == " << d_list << std::endl; makeCurrent(); + Debug("cdlist") << "push_back " << this + << " " << getContext()->getLevel() + << ": grow? " << d_size + << " " << d_sizeAlloc << std::endl; if(d_size == d_sizeAlloc) { + Debug("cdlist") << "push_back " << this + << " " << getContext()->getLevel() + << ": grow!" << std::endl; grow(); } - - ::new((void*)(d_list + d_size)) T(data); + Assert(d_size < d_sizeAlloc); + + Debug("cdlist") << "push_back " << this + << " " << getContext()->getLevel() + << ": construct! at " << d_list + << "[" << d_size << "] == " << &d_list[d_size] + << std::endl; + d_allocator.construct(&d_list[d_size], data); + Debug("cdlist") << "push_back " << this + << " " << getContext()->getLevel() + << ": done..." << std::endl; ++d_size; + Debug("cdlist") << "push_back " << this + << " " << getContext()->getLevel() + << ": size now " << d_size << std::endl; } /** * Access to the ith item in the list. */ - const T& operator[](unsigned i) const { + const T& operator[](size_t i) const { Assert(i < d_size, "index out of bounds in CDList::operator[]"); return d_list[i]; } @@ -211,21 +300,24 @@ public: } /** - * Iterator for CDList class. It has to be const because we don't allow - * items in the list to be changed. It's a straightforward wrapper around a - * pointer. Note that for efficiency, we implement only prefix increment and - * decrement. Also note that it's OK to create an iterator from an empty, - * uninitialized list, as begin() and end() will have the same value (NULL). + * Iterator for CDList class. It has to be const because we don't + * allow items in the list to be changed. It's a straightforward + * wrapper around a pointer. Note that for efficiency, we implement + * only prefix increment and decrement. Also note that it's OK to + * create an iterator from an empty, uninitialized list, as begin() + * and end() will have the same value (NULL). */ class const_iterator { - T* d_it; + T const* d_it; - const_iterator(T* it) : d_it(it) {} + const_iterator(T const* it) : d_it(it) {} - friend class CDList<T>; + friend class CDList<T, Allocator>; public: + // FIXME we support operator--, but do we satisfy all the + // requirements of a bidirectional iterator ? typedef std::input_iterator_tag iterator_category; typedef T value_type; typedef ptrdiff_t difference_type; @@ -289,17 +381,16 @@ public: * Returns an iterator pointing to the first item in the list. */ const_iterator begin() const { - return const_iterator(d_list); + return const_iterator(static_cast<T const*>(d_list)); } /** * Returns an iterator pointing one past the last item in the list. */ const_iterator end() const { - return const_iterator(d_list + d_size); + return const_iterator(static_cast<T const*>(d_list) + d_size); } - -};/* class CDList */ +};/* class CDList<> */ }/* CVC4::context namespace */ }/* CVC4 namespace */ diff --git a/src/context/cdlist_context_memory.h b/src/context/cdlist_context_memory.h new file mode 100644 index 000000000..f85d3b79e --- /dev/null +++ b/src/context/cdlist_context_memory.h @@ -0,0 +1,493 @@ +/********************* */ +/*! \file cdlist_context_memory.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Context-dependent list class specialized for use with a + ** context memory allocator. + ** + ** Context-dependent list class specialized for use with a context + ** memory allocator. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__CONTEXT__CDLIST_CONTEXT_MEMORY_H +#define __CVC4__CONTEXT__CDLIST_CONTEXT_MEMORY_H + +#include <iterator> +#include <memory> + +#include "context/cdlist_forward.h" +#include "context/context.h" +#include "context/context_mm.h" +#include "util/Assert.h" + +namespace CVC4 { +namespace context { + +/** + * Generic context-dependent dynamic array. Like the usual CDList<>, + * but allocates all memory from context memory. Elements are kept in + * cascading "list segments." Access to elements is not O(1) but + * O(log n). As with CDList<>, update is not permitted, only + * appending to the end of the list. + */ +template <class T> +class CDList<T, ContextMemoryAllocator<T> > : public ContextObj { +public: + + /** The value type with which this CDList<> was instantiated. */ + typedef T value_type; + /** The allocator type with which this CDList<> was instantiated. */ + typedef ContextMemoryAllocator<T> Allocator; + +protected: + + static const size_t INITIAL_SEGMENT_SIZE = 10; + static const size_t INCREMENTAL_GROWTH_FACTOR = 2; + + /** + * ListSegment is itself allocated in Context memory, but it is + * never updated; it serves as information about the d_list segment + * pointer it contains only. + */ + class ListSegment { + ListSegment* d_nextSegment; + size_t d_segmentSize; + T* d_list; + public: + ListSegment() : + d_nextSegment(NULL), + d_segmentSize(0), + d_list(NULL) { + } + void initialize(T* list) { + Assert( d_nextSegment == NULL && + d_segmentSize == 0 && + d_list == NULL, + "Double-initialization of ListSegment not permitted" ); + d_list = list; + } + void linkTo(ListSegment* nextSegment) { + Assert( d_nextSegment == NULL, + "Double-linking of ListSegment not permitted" ); + d_nextSegment = nextSegment; + } + void cutLink() { + d_nextSegment = NULL; + } + ListSegment* getNextSegment() const { return d_nextSegment; } + size_t& size() { return d_segmentSize; } + size_t size() const { return d_segmentSize; } + const T* list() const { return d_list; } + T& operator[](size_t i) { return d_list[i]; } + const T& operator[](size_t i) const { return d_list[i]; } + };/* struct CDList<T, ContextMemoryAllocator<T> >::ListSegment */ + + /** + * The first segment of list memory. + */ + ListSegment d_headSegment; + + /** + * A pointer to the final segment of list memory. + */ + ListSegment* d_tailSegment; + + /** + * Whether to call the destructor when items are popped from the + * list. True by default, but can be set to false by setting the + * second argument in the constructor to false. + */ + bool d_callDestructor; + + /** + * Number of objects in list across all segments. + */ + size_t d_size; + + /** + * Total allocated size across all segments. + */ + size_t d_totalSizeAlloc; + + /** + * Our allocator. + */ + Allocator d_allocator; + + /** + * Lightweight save object for CDList<T, ContextMemoryAllocator<T> >. + */ + struct CDListSave : public ContextObj { + ListSegment* d_tail; + size_t d_tailSize, d_size, d_sizeAlloc; + CDListSave(const CDList<T, Allocator>& list, ListSegment* tail, + size_t size, size_t sizeAlloc) : + ContextObj(list), + d_tail(tail), + d_tailSize(tail->size()), + d_size(size), + d_sizeAlloc(sizeAlloc) { + } + ~CDListSave() { + this->destroy(); + } + ContextObj* save(ContextMemoryManager* pCMM) { + // This type of object _is_ the save/restore object. It isn't + // itself saved or restored. + Unreachable(); + } + void restore(ContextObj* data) { + // This type of object _is_ the save/restore object. It isn't + // itself saved or restored. + Unreachable(); + } + };/* struct CDList<T, ContextMemoryAllocator<T> >::CDListSave */ + + /** + * Private copy constructor undefined (no copy permitted). + */ + CDList(const CDList<T, Allocator>& l); + + /** + * Allocate the first list segment. + */ + void allocateHeadSegment() { + Assert(d_headSegment.list() == NULL); + Assert(d_totalSizeAlloc == 0 && d_size == 0); + + // Allocate an initial list if one does not yet exist + size_t newSize = INITIAL_SEGMENT_SIZE; + Debug("cdlist:cmm") << "initial grow of cdlist " << this + << " level " << getContext()->getLevel() + << " to " << newSize << std::endl; + if(newSize > d_allocator.max_size()) { + newSize = d_allocator.max_size(); + } + T* newList = d_allocator.allocate(newSize); + if(newList == NULL) { + throw std::bad_alloc(); + } + d_totalSizeAlloc = newSize; + d_headSegment.initialize(newList); + } + + /** + * Allocate a new segment with more space. + * Throws bad_alloc if memory allocation fails. + */ + void grow() { + Assert(d_totalSizeAlloc == d_size); + + // Allocate a new segment + typedef typename Allocator::template rebind<ListSegment>::other + SegmentAllocator; + ContextMemoryManager* cmm = d_allocator.getCMM(); + SegmentAllocator segAllocator = SegmentAllocator(cmm); + ListSegment* newSegment = segAllocator.allocate(1); + if(newSegment == NULL) { + throw std::bad_alloc(); + } + segAllocator.construct(newSegment, ListSegment()); + size_t newSize = INCREMENTAL_GROWTH_FACTOR * d_totalSizeAlloc; + if(newSize > d_allocator.max_size()) { + newSize = d_allocator.max_size(); + } + T* newList = d_allocator.allocate(newSize); + Debug("cdlist:cmm") << "new segment of cdlistcontext " << this + << " level " << getContext()->getLevel() + << " to " << newSize + << " (from " << d_tailSegment->list() + << " to " << newList << ")" << std::endl; + if(newList == NULL) { + throw std::bad_alloc(); + } + d_tailSegment->linkTo(newSegment); + d_tailSegment = newSegment; + d_tailSegment->initialize(newList); + d_totalSizeAlloc += newSize; + } + + /** + * Implementation of mandatory ContextObj method save: simply copies the + * current size to a copy using the copy constructor (the pointer and the + * allocated size are *not* copied as they are not restored on a pop). + * The saved information is allocated using the ContextMemoryManager. + */ + ContextObj* save(ContextMemoryManager* pCMM) { + ContextObj* data = new(pCMM) CDListSave(*this, d_tailSegment, + d_size, d_totalSizeAlloc); + Debug("cdlist:cmm") << "save " << this + << " at level " << this->getContext()->getLevel() + << " size at " << this->d_size + << " totalSizeAlloc at " << this->d_totalSizeAlloc + << " data:" << data << std::endl; + return data; + } + + /** + * Implementation of mandatory ContextObj method restore: simply restores the + * previous size. Note that the list pointer and the allocated size are not + * changed. + */ + void restore(ContextObj* data) { + CDListSave* save = static_cast<CDListSave*>(data); + Debug("cdlist:cmm") << "restore " << this + << " level " << this->getContext()->getLevel() + << " data == " << data + << " call dtor == " << this->d_callDestructor + << " d_tail == " << this->d_tailSegment << std::endl; + if(this->d_callDestructor) { + ListSegment* seg = &d_headSegment; + size_t i = save->d_size; + while(i >= seg->size()) { + i -= seg->size(); + seg = seg->getNextSegment(); + } + do { + while(i < seg->size()) { + this->d_allocator.destroy(&(*seg)[i++]); + } + i = 0; + } while((seg = seg->getNextSegment()) != NULL); + } + + this->d_size = save->d_size; + this->d_tailSegment = save->d_tail; + this->d_tailSegment->size() = save->d_tailSize; + this->d_tailSegment->cutLink(); + this->d_totalSizeAlloc = save->d_sizeAlloc; + Debug("cdlist:cmm") << "restore " << this + << " level " << this->getContext()->getLevel() + << " size back to " << this->d_size + << " totalSizeAlloc at " << this->d_totalSizeAlloc + << std::endl; + } + +public: + + CDList(Context* context, bool callDestructor, const Allocator& alloc) : + ContextObj(context), + d_headSegment(), + d_tailSegment(&d_headSegment), + d_callDestructor(callDestructor), + d_size(0), + d_totalSizeAlloc(0), + d_allocator(alloc) { + allocateHeadSegment(); + } + + CDList(Context* context, bool callDestructor = true) : + ContextObj(context), + d_headSegment(), + d_tailSegment(&d_headSegment), + d_callDestructor(callDestructor), + d_size(0), + d_totalSizeAlloc(0), + d_allocator(Allocator(context->getCMM())) { + allocateHeadSegment(); + } + + CDList(bool allocatedInCMM, Context* context, bool callDestructor, + const Allocator& alloc) : + ContextObj(allocatedInCMM, context), + d_headSegment(), + d_tailSegment(&d_headSegment), + d_callDestructor(callDestructor), + d_size(0), + d_totalSizeAlloc(0), + d_allocator(alloc) { + allocateHeadSegment(); + } + + CDList(bool allocatedInCMM, Context* context, bool callDestructor = true) : + ContextObj(allocatedInCMM, context), + d_headSegment(), + d_tailSegment(&d_headSegment), + d_callDestructor(callDestructor), + d_size(0), + d_totalSizeAlloc(0), + d_allocator(Allocator(context->getCMM())) { + allocateHeadSegment(); + } + + /** + * Destructor: delete the list + */ + ~CDList() throw(AssertionException) { + this->destroy(); + + if(this->d_callDestructor) { + for(ListSegment* segment = &d_headSegment; + segment != NULL; + segment = segment->getNextSegment()) { + for(size_t i = 0; i < segment->size(); ++i) { + this->d_allocator.destroy(&(*segment)[i]); + } + } + } + } + + /** + * Return the current size of (i.e. valid number of objects in) the + * list. + */ + size_t size() const { + return d_size; + } + + /** + * Return true iff there are no valid objects in the list. + */ + bool empty() const { + return d_size == 0; + } + + /** + * Add an item to the end of the list. + */ + void push_back(const T& data) { + Debug("cdlist:cmm") << "push_back " << this + << " level " << getContext()->getLevel() + << ": make-current, " + << "d_list == " << d_tailSegment->list() << std::endl; + makeCurrent(); + + Debug("cdlist:cmm") << "push_back " << this + << " level " << getContext()->getLevel() + << ": grow? " << d_size + << " size_alloc " << d_totalSizeAlloc + << std::endl; + + if(d_size == d_totalSizeAlloc) { + Debug("cdlist:cmm") << "push_back " << this + << " " << getContext()->getLevel() + << ": grow!\n"; + grow(); + } + Assert(d_size < d_totalSizeAlloc); + + Debug("cdlist:cmm") << "push_back " << this + << " " << getContext()->getLevel() + << ": construct! at [" << d_size << "] == " + << &(*d_tailSegment)[d_tailSegment->size()] + << std::endl; + d_allocator.construct(&(*d_tailSegment)[d_tailSegment->size()], data); + Debug("cdlist:cmm") << "push_back " << this + << " " << getContext()->getLevel() + << ": done..." << std::endl; + ++d_tailSegment->size(); + ++d_size; + Debug("cdlist:cmm") << "push_back " << this + << " " << getContext()->getLevel() + << ": size now " << d_size << std::endl; + } + + /** + * Access to the ith item in the list. + */ + const T& operator[](size_t i) const { + Assert(i < d_size, "index out of bounds in CDList::operator[]"); + const ListSegment* seg = &d_headSegment; + while(i >= seg->size()) { + i -= seg->size(); + seg = seg->getNextSegment(); + } + return (*seg)[i]; + } + + /** + * Returns the most recent item added to the list. + */ + const T& back() const { + Assert(d_size > 0, "CDList::back() called on empty list"); + return (*d_tailSegment)[d_tailSegment->size() - 1]; + } + + /** + * Iterator for CDList class. It has to be const because we don't + * allow items in the list to be changed. It's a straightforward + * wrapper around a pointer. Note that for efficiency, we implement + * only prefix increment and decrement. Also note that it's OK to + * create an iterator from an empty, uninitialized list, as begin() + * and end() will have the same value (NULL). + */ + class const_iterator { + const ListSegment* d_segment; + size_t d_index; + + const_iterator(const ListSegment* segment, size_t i) : + d_segment(segment), + d_index(i) { + } + + friend class CDList<T, Allocator>; + + public: + + typedef std::input_iterator_tag iterator_category; + typedef T value_type; + typedef ptrdiff_t difference_type; + typedef const T* pointer; + typedef const T& reference; + + const_iterator() : d_segment(NULL), d_index(0) {} + + inline bool operator==(const const_iterator& i) const { + return d_segment == i.d_segment && d_index == i.d_index; + } + + inline bool operator!=(const const_iterator& i) const { + return !(*this == i); + } + + inline const T& operator*() const { + return (*d_segment)[d_index]; + } + + /** Prefix increment */ + const_iterator& operator++() { + if(++d_index >= d_segment->size()) { + d_segment = d_segment->getNextSegment(); + d_index = 0; + } + return *this; + } + + /** Postfix increment: returns new iterator with the old value. */ + const_iterator operator++(int) { + const_iterator i = *this; + ++(*this); + return i; + } + };/* class CDList<>::const_iterator */ + + /** + * Returns an iterator pointing to the first item in the list. + */ + const_iterator begin() const { + return const_iterator(&d_headSegment, 0); + } + + /** + * Returns an iterator pointing one past the last item in the list. + */ + const_iterator end() const { + return const_iterator(NULL, 0); + } +};/* class CDList<T, ContextMemoryAllocator<T> > */ + +}/* CVC4::context namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__CONTEXT__CDLIST_CONTEXT_MEMORY_H */ diff --git a/src/context/cdlist_forward.h b/src/context/cdlist_forward.h new file mode 100644 index 000000000..82bc9cc15 --- /dev/null +++ b/src/context/cdlist_forward.h @@ -0,0 +1,56 @@ +/********************* */ +/*! \file cdlist_forward.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief This is a forward declaration header to declare the + ** CDList<> template + ** + ** This is a forward declaration header to declare the CDList<> + ** template. It's useful if you want to forward-declare CDList<> + ** without including the full cdlist.h or cdlist_context_memory.h + ** header, for example, in a public header context, or to keep + ** compile times low when only a forward declaration is needed. + ** + ** Note that all specializations of the template should be listed + ** here as well, since different specializations are defined in + ** different headers (cdlist.h and cdlist_context_memory.h). + ** Explicitly declaring both specializations here ensure that if you + ** define one, you'll get an error if you didn't include the correct + ** header (avoiding different, incompatible instantiations in + ** different compilation units). + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__CONTEXT__CDLIST_FORWARD_H +#define __CVC4__CONTEXT__CDLIST_FORWARD_H + +#include <memory> + +namespace __gnu_cxx { + template <class Key> class hash; +}/* __gnu_cxx namespace */ + +namespace CVC4 { + namespace context { + template <class T> + class ContextMemoryAllocator; + + template <class T, class Allocator = std::allocator<T> > + class CDList; + + template <class T> + class CDList<T, ContextMemoryAllocator<T> >; + }/* CVC4::context namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__CONTEXT__CDLIST_FORWARD_H */ diff --git a/src/context/context_mm.cpp b/src/context/context_mm.cpp index 5a1e52d66..fde69a149 100644 --- a/src/context/context_mm.cpp +++ b/src/context/context_mm.cpp @@ -23,6 +23,7 @@ #include <new> #include "context/context_mm.h" #include "util/Assert.h" +#include "util/output.h" namespace CVC4 { namespace context { diff --git a/src/context/context_mm.h b/src/context/context_mm.h index 1eb452113..71f7041c7 100644 --- a/src/context/context_mm.h +++ b/src/context/context_mm.h @@ -103,7 +103,14 @@ class ContextMemoryManager { */ void newChunk(); - public: +public: + + /** + * Get the maximum allocation size for this memory manager. + */ + static unsigned getMaxAllocationSize() { + return chunkSizeBytes; + } /** * Constructor - creates an initial region and an empty stack @@ -133,6 +140,62 @@ class ContextMemoryManager { };/* class ContextMemoryManager */ +/** + * An STL-like allocator class for allocating from context memory. + */ +template <class T> +class ContextMemoryAllocator { + ContextMemoryManager* d_mm; + +public: + + typedef size_t size_type; + typedef ptrdiff_t difference_type; + typedef T* pointer; + typedef T const* const_pointer; + typedef T& reference; + typedef T const& const_reference; + typedef T value_type; + template <class U> struct rebind { + typedef ContextMemoryAllocator<U> other; + }; + + ContextMemoryAllocator(ContextMemoryManager* mm) throw() : d_mm(mm) {} + ContextMemoryAllocator(const ContextMemoryAllocator& alloc) throw() : d_mm(alloc.d_mm) {} + ~ContextMemoryAllocator() throw() {} + + ContextMemoryManager* getCMM() { return d_mm; } + T* address(T& v) const { return &v; } + T const* address(T const& v) const { return &v; } + size_t max_size() const throw() { + return ContextMemoryManager::getMaxAllocationSize() / sizeof(T); + } + T* allocate(size_t n, const void* = 0) const { + return static_cast<T*>(d_mm->newData(n * sizeof(T))); + } + void deallocate(T* p, size_t n) const { + /* no explicit delete */ + } + void construct(T* p, T const& v) const { + ::new(reinterpret_cast<void*>(p)) T(v); + } + void destroy(T* p) const { + p->~T(); + } +};/* class ContextMemoryAllocator<T> */ + +template <class T> +inline bool operator==(const ContextMemoryAllocator<T>& a1, + const ContextMemoryAllocator<T>& a2) { + return a1.d_mm == a2.d_mm; +} + +template <class T> +inline bool operator!=(const ContextMemoryAllocator<T>& a1, + const ContextMemoryAllocator<T>& a2) { + return a1.d_mm != a2.d_mm; +} + }/* CVC4::context namespace */ }/* CVC4 namespace */ |