diff options
Diffstat (limited to 'src/context/context.cpp')
-rw-r--r-- | src/context/context.cpp | 209 |
1 files changed, 209 insertions, 0 deletions
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 */ |