From: Clark Barrett Date: Fri, 29 Jan 2010 19:46:26 +0000 (+0000) Subject: Update of context module X-Git-Tag: cvc5-1.0.0~9330 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2ca8bf894a2e40e56b9379289e46b0a0d33cf272;p=cvc5.git Update of context module --- diff --git a/src/context/context.cpp b/src/context/context.cpp index 3635d0c07..5729c2283 100644 --- a/src/context/context.cpp +++ b/src/context/context.cpp @@ -12,5 +12,214 @@ ** **/ + #include "context/context.h" +#include "util/Assert.h" + + +namespace CVC4 { +namespace context { + + +Context::Context() : d_pContextNotifyObj(NULL) { + // Create new memory manager + d_pCMM = new ContextMemoryManager(); + + // Create initial Scope + d_pScopeTop = new(cmm) Scope(this, cmm); + d_pScopeBottom = d_pScopeTop; +} + + +Context::~Context() { + // Delete all Scopes + popto(-1); + + // Delete the memory manager + delete d_pCMM; + + // Clear ContextNotifyObj lists so there are no dangling pointers + ContextNotifyObj* pCNO; + while (d_pCNOpre != NULL) { + pCNO = d_pCNOpre; + pCNO->d_ppCNOprev = NULL; + d_pContextNotifyObj = pCNO->d_pCNOnext; + pCNO->d_pCNOnext = NULL; + } + while (d_pCNOpost != NULL) { + pCNO = d_pCNOpost; + pCNO->d_ppCNOprev = NULL; + d_pContextNotifyObj = pCNO->d_pCNOnext; + pCNO->d_pCNOnext = NULL; + } +} + + +void Context::push() { + // FIXME: TRACE("pushpop", indentStr, "Push", " {"); + + // Create a new memory region + d_pCMM->push(); + + // Create a new top Scope + d_pScopeTop = new(d_pCMM) Scope(this, d_pCMM, d_pScopeTop); +} + + +void Context::pop() { + // Notify the (pre-pop) ContextNotifyObj objects + ContextNotifyObj* pCNO = d_pCNOPre; + while (pCNO != NULL) { + pCNO->notify(); + pCNO = pCNO->d_pCNOnext; + } + + // Grab the top Scope + Scope* pScope = d_pScopeTop; + + // Restore the previous Scope + d_pScopeTop = pScope->getScopePrev(); + + // Restore all objects in the top Scope + delete(d_pCMM) pScope; + + // Pop the memory region + d_pCMM->pop(); + + // Notify the (post-pop) ContextNotifyObj objects + ContextNotifyObj* pCNO = d_pCNOPost; + while (pCNO != NULL) { + pCNO->notify(); + pCNO = pCNO->d_pCNOnext; + } + + //FIXME: TRACE("pushpop", indentStr, "}", " Pop"); +} + + +void Context::popto(int toLevel) { + // Pop scopes until there are none left or toLevel is reached + while (d_pScopeTop != NULL && toLevel < d_pScopeTop()->getLevel()) pop(); +} + + +void Context::addNotifyObjPre(ContextNotifyObj* pCNO) { + // Insert pCNO at *front* of list + if(d_pCNOpre != NULL) + d_pCNOpre->prev() = &(pCNO->next()); + pCNO->next() = d_pCNOpre; + pCNO->prev() = &d_pCNOpre; + d_pCNOpre = pCNO; +} + + +void Context::addNotifyObjPost(ContextNotifyObj* pCNO) { + // Insert pCNO at *front* of list + if(d_pCNOpost != NULL) + d_pCNOpost->prev() = &(pCNO->next()); + pCNO->next() = d_pCNOpost; + pCNO->prev() = &d_pCNOpost; + d_pCNOpost = pCNO; +} + + +void ContextObj::update() { + // Call save() to save the information in the current object + ContextObj* pContextObjSaved = save(d_pScope->getCMM()); + + // Check that base class data was saved + Assert(saved.d_pContextObjNext == d_pContextObjNext && + saved.d_ppContextObjPrev == d_ppContextObjPrev && + saved.d_pContextObjRestore == d_pContextObjRestore && + saved.d_pScope == d_pScope, + "save() did not properly copy information in base class"); + + // Update Scope pointer to current top Scope + d_pScope = d_pScope->getContext()->getTopScope(); + + // Store the saved copy in the restore pointer + d_pContextObjRestore = pContextObjSaved; + + // Insert object into the list of objects that need to be restored when this + // Scope is popped. + d_pScope->addToChain(this); +} + + +ContextObj* ContextObj::restoreAndContinue() +{ + // Variable to hold next object in list + ContextObj* pContextObjNext; + + // Check the restore pointer. If NULL, this must be the bottom Scope + if (d_pContextObjRestore == NULL) { + Assert(d_pScope == d_pScope->getContext()->getBottomScope(), + "Expected bottom scope"); + pContextObjNext = d_pContextObjNext; + // Nothing else to do + } + else { + // Call restore to update the subclass data + restore(d_pContextObjRestore); + + // Remember the next object in the list + pContextObjNext = d_pContextObjNext; + + // Restore the base class data + d_pScope = d_pContextObjRestore->d_pScope; + next() = d_pContextObjRestore->d_pContextObjNext; + prev() = d_pContextObjRestore->d_pContextObjPrev; + d_pContextObjRestore = d_pContextObjRestore->d_pContextObjRestore; + } + // Return the next object in the list + return pContextObjNext; +} + + +ContextObj::ContextObj(Context* pContext) + : d_pContextObjRestore(NULL) +{ + Assert(pContext != NULL, "NULL context pointer"); + d_pScope = pContext->getBottomScope(); + d_pScope->addToChain(this); +} + + +ContextObj::~ContextObj() +{ + for(;;) { + if (next() != NULL) { + next()->prev() = prev(); + } + *(prev()) = next(); + if (d_pContextObjRestore == NULL) break; + restoreAndContinue(); + } +} + + +ContextNotifyObj::ContextNotifyObj(Context* pContext, bool preNotify = false) { + if (preNotify) { + pContext->addNotifyObjPre(this); + } + else { + pContext->addNotifyObjPost(this); + } +} + + +ContextNotifyObj::~ContextNotifyObj() +{ + if (d_pCNOnext != NULL) { + d_pCNOnext->d_pCNOprev = d_pCNOprev; + } + if (d_pCNOprev != NULL) { + *(d_pCNOprev) = d_pCNOnext; + } +} + + +} /* CVC4::context namespace */ + +} /* CVC4 namespace */ diff --git a/src/context/context.h b/src/context/context.h index 68667c223..6c9f01acf 100644 --- a/src/context/context.h +++ b/src/context/context.h @@ -20,18 +20,414 @@ namespace CVC4 { namespace context { class Context; +class Scope; +class ContextObj; +class ContextNotifyObj; + + /** + * A Context encapsulates all of the dynamic state of the system. Its main + * methods are push() and pop(). A call to push() saves the current state, + * and a call to pop() restores the state saved by the most recent call to + * push(). + * + * Objects which want to participate in this global save and restore + * mechanism must inherit from ContextObj (see below). + * + * For more flexible context-dependent behavior, objects may implement the + * ContextNotifyObj interface and simply get a notification when a pop has + * occurred. + * + * Context also uses a helper class called Scope which stores information + * specific to the portion of the Context since the last call to push() (see + * below). + * + * Memory allocation in Contexts is done with the help of the + * ContextMemoryManager. A copy is stored in each Scope object for quick + * access. + * + */ +class Context { + + /** + * Pointer to the ContextMemoryManager fot this Context. + */ + ContextMemoryManager* d_pCMM; + + /** + * Pointer to the current (top) Scope for this Context. + */ + Scope* d_pScopeTop; + + /** + * Pointer to the initial (bottom) Scope for this Context. + */ + Scope* d_pScopeBottom; + + /** + * Doubly-linked list of objects to notify before every pop. See + * ContextNotifyObj for sturcture of linked list. + */ + ContextNotifyObj* d_pCNOpre; + + /** + * Doubly-linked list of objects to notify after every pop. See + * ContextNotifyObj for sturcture of linked list. + */ + ContextNotifyObj* d_pCNOpost; -class ContextManager { public: - void switchContext(Context); - Context snapshot(); -};/* class ContextManager */ + /** + * Constructor: create ContextMemoryManager and initial Scope + */ + Context(); + + /** + * Destructor: pop all scopes, delete ContextMemoryManager + */ + ~Context(); + + /** + * Return the current (top) scope + */ + Scope* getTopScope() const { return d_pScopeTop; } + + /** + * Return the initial (bottom) scope + */ + Scope* getBottomScope() const { return d_pScopeBottom; } + + /** + * Return the current Scope level. Implemented as inline function following + * declaration of Scope class. + */ + int getLevel() const; + + /** + * Save the current state, create a new Scope + */ + void push(); + + /** + * Restore the previous state, delete the top Scope + */ + void pop(); + + /** + * Pop all the way back to given level + */ + void popto(int toLevel); + + /** + * Add pCNO to the list of objects notified before every pop + */ + void addNotifyObjPre(ContextNotifyObj* pCNO); + + /** + * Add pCNO to the list of objects notified after every pop + */ + void addNotifyObjPost(ContextNotifyObj* pCNO); + +}; /* class Context */ + + /** + * Conceptually, a Scope encapsulates that portion of the context that + * changes after a call to push() and must be undone on a subsequent call to + * pop(). In particular, each call to push() creates a new Scope object . + * This new Scope object becomes the top scope and it points (via the + * d_pScopePrev member) to the previous top Scope. Each call to pop() + * deletes the current top scope and restores the previous one. The main + * purpose of a Scope is to maintain a linked list of ContexObj objects which + * change while the Scope is the top scope and which must be restored when + * the Scope is deleted. + * + * A Scope is also associated with a ContextMemoryManager. All memory + * allocated by the Scope is allocated in a single region using the + * ContextMemoryManager and released all at once when the Scope is popped. + */ +class Scope { + + /** + * Context that created this Scope + */ + Context* d_pContext; + + /** + * Memory manager for this Scope. Same as in Context, but stored here too + * for faster access by ContextObj objects. + */ + ContextMemoryManager* d_pCMM; + + /** + * Previous Scope in this context + */ + Scope* d_pScopePrev; + + /** + * Scope level (total number of outstanding push() calls when this Scope was + * created). + */ + int d_level; + + /** + * Linked list of objects which changed in this scope, + * and thus need to be restored when the scope is deleted. + */ + ContextObj* d_pContextObjList; -class ContextObject { public: - void snapshot(); - void restore(); -};/* class ContextObject */ + + /** + * Constructor: Create a new Scope; set the level and the previous Scope + * if any. + */ + Scope(Context* pContext, ContextMemoryManager* pCMM, + Scope* pScopePrev = NULL) + : d_pContext(context), d_pCMM(pCMM), d_pScopePrev(pScopePrev), + d_level(0), d_pContextObjList(NULL) + { if (pScopePrev != NULL) d_level = pScopePrev->getLevel() + 1; } + + /** + * Destructor: Restore all of the objects in CotextObjList. Defined inline + * below. + */ + ~Scope(); + + /** + * Get the Context for this Scope + */ + Context* getContext() const { return d_pContext; } + + /** + * Get the ContextMemoryManager for this Scope + */ + ContextMemoryManager* getCMM() const { return d_pCMM; } + + /** + * Get the pointer to the previous Scope (should be NULL if no previous + * scope). + */ + Scope* getScopePrev() const { return d_pScopePrev; } + + /** + * Get the level of the current Scope + */ + int getLevel(void) const { return d_level; } + + /** + * Return true iff this Scope is the current top Scope + */ + bool isCurrent(void) const { return this == d_pContext->getTopScope(); } + + /** + * When a ContextObj object is modified for the first time in this Scope, it + * should call this method to add itself to the list of objects that will + * need to be restored. Defined inline below. + */ + void addToChain(ContextObj* pContextObj); + + /** + * Overload operator new for use with ContextMemoryManager to allow creation + * of new Scope objects in the current memory region. + */ + void* operator new(size_t size, ContextMemoryManager* pCMM) + { return pCMM->newData(size); } + + /** + * Overload operator delete for Scope objects allocated using + * ContextMemoryManager. No need to do anything because memory is freed + * automatically when the ContextMemoryManager pop() method is called. + */ + void operator delete(void* pMem, ContextMemoryManager* pCMM) {} + + //FIXME: //! Check for memory leaks + // void check(void); + +}; /* class Scope */ + + /** + * This is an abstract base class from which all objects that are context-dependent + * should inherit. For any data structure that you want to have be + * automatically backtracked, do the following: + * 1. Create a class for the data structure that inherits from ContextObj + * 2. Implement save() + * The role of save() is to create a new ContexObj object that contains + * enough information to restore the object to its current state, even if + * it gets changed later. Note that save should call the (default) + * ContextObj Copy Constructor to copy the information in the base class. + * It is recommended that any memory allocated by save() should be done + * through the ContextMemoryManager. This way, it does not need to be + * explicitly freed when restore is called. However, it is only required + * that the ContextObj itself be allocated using the + * ContextMemoryManager. If other memory is allocated not using the + * ContextMemoryManager, it should be freed when restore() is called. + * 3. Implement restore() + * The role of restore() is, given the ContextObj returned by a previous + * call to save(), to restore the current object to the state it was in + * when save() was called. Note that the implementation of restore does + * *not* need to worry about restoring the base class data. This is done + * automatically. restore() should not have to free any memory as any + * memory allocated by save() should have been done using the + * ContextMemoryManager (see item 2 above). + * 4. In the subclass implementation, any time the state is about to be + * changed, first call to makeCurrent(). + */ +class ContextObj { + /** + * Pointer to Scope in which this object was last modified. + */ + Scope* d_pScope; + + /** + * Pointer to most recent version of same ContextObj in a previous Scope + */ + ContextObj* d_pContextObjRestore; + + /** + * Next link in ContextObjList list maintained by Scope class. + */ + ContextObj* d_pContextObjNext; + + /** + * Previous link in ContextObjList list maintained by Scope class. We use + * double-indirection here to make element deletion easy. + */ + ContextObj** d_ppContextObjPrev; + + /** + * Helper method for makeCurrent (see below). Separated out to allow common + * case to be inlined without making a function call. It calls save() and + * does the necessary bookkeeping to ensure that object can be restored to + * its current state when restore is called. + */ + void update(); + + // The rest of the private methods are for the benefit of the Scope. We make + // Scope our friend so it is the only one that can use them. + + friend class Scope; + + /** + * Return reference to next link in ContextObjList. Used by + * Scope::addToChain method. + */ + ContextObj*& next() { return d_pContextObjNext; } + + /** + * Return reference to prev link in ContextObjList. Used by + * Scope::addToChain method. + */ + ContextObj**& prev() { return d_ppContextObjPrev; } + + /** + * This method is called by Scope during a pop: it does the necessary work to + * restore the object from its saved copy and then returns the next object in + * the list that needs to be restored. + */ + ContextObj* restoreAndContinue(); + +protected: + /** + * This is a method that must be implemented by all classes inheriting from + * ContextObj. See the comment before the class declaration. + */ + virtual ContextObj* save(ContextMemoryManager* pCMM) = 0; + + /** + * This is a method that must be implemented by all classes inheriting from + * ContextObj. See the comment before the class declaration. + */ + virtual void restore(ContextObj* pContextObjRestore) = 0; + + /** + * This method checks if the object has been modified in this Scope yet. If + * not, it calls update(). + */ + void makeCurrent() { if (!(d_pScope->isCurrent())) update(); } + +public: + /** + * Create a new ContextObj. The initial scope is set to the bottom + * scope of the Context. + */ + ContextObj(Context* context); + + /** + * Destructor: Calls restore until restored to initial version. Also removes + * object from all Scope lists. Note that this doesn't actually free the + * memory allocated by the ContextMemoryManager for this object. This isn't + * done until the corresponding Scope is popped. + */ + virtual ~ContextObj(); + +}; /* class ContextObj */ + + /** + * For more flexible context-dependent behavior than that provided by + * ContextObj, objects may implement the ContextNotifyObj interface and + * simply get a notification when a pop has occurred. See Context class for + * how to register a ContextNotifyObj with the Context (you can choose to + * have notification come before or after the ContextObj objects have been + * restored). + */ +class ContextNotifyObj { + /** + * Context is our friend so that when the Context is deleted, any remaining + * ContextNotifyObj can be removed from the Context list. + */ + friend Context; + + /** + * Pointer to next ContextNotifyObject in this List + */ + ContextNotifyObj* d_pCNOnext; + + /** + * Pointer to previous ContextNotifyObject in this list + */ + ContextNotifyObj** d_ppCNOprev; + +public: + /** + * Constructor for ContextNotifyObj. Parameters are the context to which + * this notify object will be added, and a flag which, if true, tells the + * context to notify this object *before* the ContextObj objects are + * restored. Otherwise, the context notifies the object after the ContextObj + * objects are restored. The default is for notification after. + */ + ContextNotifyObj(Context* pContext, bool preNotify = false); + + /** + * Destructor: removes object from list + */ + virtual ~ContextNotifyObj(); + + /** + * This is the method called to notify the object of a pop. It must be + * implemented by the subclass. + */ + virtual void notify() = 0; +}; /* class ContextNotifyObj */ + +// Inline functions whose definitions had to be delayed: + +inline int Context::getLevel() const { return getTopScope()->getLevel(); } + +inline void Scope::~Scope() { + // Call restore() method on each ContextObj object in the list. + // Note that it is the responsibility of restore() to return the next item in + // the list. + while (d_pContextObjList != NULL) { + d_pContextObjList = d_pContextObjList->restoreAndContinue(); + } +} + +inline void Scope::addToChain(ContextObjChain* pContextObj) { + if(d_pContextObjList != NULL) + d_pContextObjList->prev() = &(pContextObj->next()); + pContextObj->next() = d_pContextObjList; + pContextObj->prev() = &d_pContextObjList; + d_pContextObjList = pContextObj; +} template class CDO; @@ -49,3 +445,4 @@ class CDSet; }/* CVC4 namespace */ #endif /* __CVC4__CONTEXT__CONTEXT_H */ + diff --git a/src/context/context_mm.cpp b/src/context/context_mm.cpp index d772b886f..f282df96d 100644 --- a/src/context/context_mm.cpp +++ b/src/context/context_mm.cpp @@ -119,5 +119,7 @@ void ContextMemoryManager::pop() { } -}/* CVC4::context namespace */ -}/* CVC4 namespace */ +} /* CVC4::context namespace */ + + +} /* CVC4 namespace */ diff --git a/src/context/context_mm.h b/src/context/context_mm.h index eeaa0a2c8..af524a51f 100644 --- a/src/context/context_mm.h +++ b/src/context/context_mm.h @@ -34,9 +34,9 @@ namespace context { class ContextMemoryManager { /** - * Memory in regions is allocated in chunks. This is the minimum chunk size + * Memory in regions is allocated in chunks. This is the chunk size */ - static const unsigned chunkSizeBytes = 16384; // #bytes in each chunk + static const unsigned chunkSizeBytes = 16384; /** * A list of free chunks is maintained. This is the maximum number of