**
**/
+
#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 */
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 T>
class CDO;
}/* CVC4 namespace */
#endif /* __CVC4__CONTEXT__CONTEXT_H */
+
projects / cvc5.git / commitdiff