context.cpp

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file context.cpp
00004  * 
00005  * Author: Clark Barrett
00006  * 
00007  * Created: Fri Jan 17 14:30:37 2003
00008  *
00009  * <hr>
00010  *
00011  * License to use, copy, modify, sell and/or distribute this software
00012  * and its documentation for any purpose is hereby granted without
00013  * royalty, subject to the terms and conditions defined in the \ref
00014  * LICENSE file provided with this distribution.
00015  * 
00016  * <hr>
00017  * 
00018  */
00019 /*****************************************************************************/
00020 
00021 
00022 #include "context.h"
00023 
00024 
00025 using namespace CVC3;
00026 using namespace std;
00027 
00028 
00029 vector<char*> ContextMemoryManager::s_freePages;
00030 
00031 
00032 ///////////////////////////////////////////////////////////////////////////////
00033 // Scope methods                                                             //
00034 ///////////////////////////////////////////////////////////////////////////////
00035 
00036 
00037 void Scope::finalize(void)
00038 {
00039   ContextObjChain* obj = d_restoreChain;
00040   while (obj != NULL) {
00041     ContextObjChain* tmp = obj->d_restoreChainNext;
00042     // When called from ~ContextManager(), the master objects may
00043     // still point to this scope.  Disconnect them here.
00044     if (obj->d_master != NULL) {
00045       if (obj->d_master->d_scope == this)
00046         obj->d_master->d_scope = NULL;
00047       if (obj->d_master->d_restore == obj)
00048         obj->d_master->d_restore = NULL;
00049     }
00050     obj = tmp;
00051   }
00052 }
00053 
00054 
00055 void Scope::check(void)
00056 {
00057   IF_DEBUG(
00058   ContextObjChain* obj = d_restoreChain;
00059   if (debugger.trace("memory") && obj != NULL) {
00060     ostream& os = debugger.getOS();
00061     int n(0);
00062     ContextObjChain* tmp = obj;
00063     while(tmp != NULL) {
00064       tmp = tmp->d_restoreChainNext;
00065       n++;
00066     }
00067     os << "*** Warning: ~Scope(): found "<< n << " leaked objects "
00068        << "in scope " << d_level << ":" << endl;
00069     if (debugger.flag("memory leaks")) {
00070       tmp = obj;
00071       while(tmp != NULL) {
00072         os << tmp->name() << "\n";
00073         tmp = tmp->d_restoreChainNext;
00074       }
00075     }
00076     os << flush;
00077   }
00078   )
00079 }
00080 
00081 
00082 ///////////////////////////////////////////////////////////////////////////////
00083 // ContextObjChain methods                                                   //
00084 ///////////////////////////////////////////////////////////////////////////////
00085 
00086 
00087 ContextObjChain* ContextObjChain::restore(void)
00088 {
00089   // Assign 'next' pointer only when the master object is restored,
00090   // since this may change our next pointer (master may have other
00091   // context objects removed).
00092   DebugAssert(d_master != NULL, "How did this happen");
00093   //  if (d_master == NULL) return d_restoreChainNext;
00094   ContextObjChain* next;
00095   DebugAssert(d_data != NULL, "Shouldn't happen");
00096 //   if (d_data == NULL) {
00097 //     d_master->setNull();
00098 //     d_master->d_scope = d_master->d_scope->prevScope();
00099 //     DebugAssert(d_restore==NULL,"Expected NULL");
00100 //     next = d_restoreChainNext;
00101 //     d_master->d_scope->addToChain(this);
00102 //   }
00103 //   else {
00104     d_master->restoreData(d_data);
00105     d_master->d_scope = d_data->d_scope;
00106     d_master->d_restore = d_restore;
00107     next = d_restoreChainNext;
00108     if (d_data != NULL) delete d_data;
00109     DebugAssert(d_master->d_restore != this, "points to self");
00110 //   }
00111   return next;
00112 }
00113 
00114 
00115 #ifdef DEBUG
00116 std::string ContextObjChain::name() const
00117 {
00118   DebugAssert(d_master != NULL, "NULL master");
00119   return d_master->name();
00120 }
00121 #endif
00122 
00123 
00124 ///////////////////////////////////////////////////////////////////////////////
00125 // ContextObj methods                                                        //
00126 ///////////////////////////////////////////////////////////////////////////////
00127 
00128 
00129 void ContextObj::update(int scope)
00130 {
00131   Scope* tmpScope = d_scope;
00132   DebugAssert(scope < 0 || d_scope->level() <= scope,
00133         "ContextObj::update(scope="+int2string(scope)
00134         +"): scope < d_scope->level() = "
00135         +int2string(d_scope->level()));
00136   d_scope = d_scope->topScope();
00137   if (scope >= 0) {
00138     // Fetch the specified scope
00139     for(int i=level(); i>scope; --i) {
00140       d_scope = d_scope->prevScope();
00141       DebugAssert(d_scope != NULL, "ContextObj::update["
00142       +name()+"]: d_scope == NULL");
00143     }
00144   }
00145   ContextObj* data = makeCopy(getCMM());
00146   data->d_scope = tmpScope;
00147   // The destructor of the copy should not destroy our older copies
00148   data->d_restore=NULL;
00149   IF_DEBUG(data->setName(name()+" [copy]"));
00150   d_restore = new(getCMM()) ContextObjChain(data, this, d_restore);
00151   d_scope->addToChain(d_restore);
00152 }
00153 
00154 
00155 ContextObj::~ContextObj()
00156 {
00157   // Delete our restore copies
00158   IF_DEBUG(FatalAssert(d_active, "~ContextObj["+name()+"]"));
00159   IF_DEBUG(d_active=false); 
00160   for(ContextObjChain* obj = d_restore; obj != NULL; ) {
00161     ContextObjChain* tmp = obj->d_restore;
00162     // Remove the object from the restore chain
00163     if(obj->d_restoreChainNext != NULL)
00164       obj->d_restoreChainNext->d_restoreChainPrev = obj->d_restoreChainPrev;
00165     *(obj->d_restoreChainPrev) = obj->d_restoreChainNext;
00166     //    if (obj->d_data != NULL) delete obj->d_data;
00167     obj->d_master = NULL;
00168     if (tmp == NULL) {
00169       delete obj;
00170       free(obj);
00171       break;
00172     }
00173     obj = tmp;
00174   }
00175   //  TRACE("context verbose", "~ContextObj()[", this, "] }");
00176 }
00177 
00178 
00179 ///////////////////////////////////////////////////////////////////////////////
00180 // Context methods                                                           //
00181 ///////////////////////////////////////////////////////////////////////////////
00182 
00183 
00184 Context::Context(ContextManager* cm, const string& name, int id)
00185   : d_cm(cm), d_name(name), d_id(id)
00186 {
00187   ContextMemoryManager* cmm = new ContextMemoryManager();
00188   d_topScope = new(cmm) Scope(this, cmm);
00189   d_bottomScope = d_topScope;
00190   TRACE("context", "*** [context] Creating new context: name = "
00191   + name + "id = ", id, "");
00192 }
00193 
00194 
00195 // Don't pop, just delete everything.  At this point, most of the
00196 // system is already destroyed, popping may be dangerous.
00197 Context::~Context()
00198 {
00199   // popto(0);
00200   Scope* top = d_topScope;
00201   while(top != NULL) {
00202     top = d_topScope->prevScope();
00203     d_topScope->finalize();
00204     delete d_topScope->getCMM();
00205     d_topScope = top;
00206   }
00207   while (!d_cmmStack.empty()) {
00208     delete d_cmmStack.back();
00209     d_cmmStack.pop_back();
00210   }
00211   ContextMemoryManager::garbageCollect();
00212   // Erase ourselves from the notify objects, so they don't call us
00213   for(vector<ContextNotifyObj*>::iterator i=d_notifyObjList.begin(),
00214   iend=d_notifyObjList.end(); i!=iend; ++i) {
00215     (*i)->d_context = NULL;
00216   }
00217 }
00218 
00219 
00220 void Context::push()
00221 {
00222   IF_DEBUG(
00223     string indentStr(level(), ' ');
00224     TRACE("pushpop", indentStr, "Push", " {");
00225   )
00226   ContextMemoryManager* cmm;
00227   if (!d_cmmStack.empty()) {
00228     cmm = d_cmmStack.back();
00229     d_cmmStack.pop_back();
00230   }
00231   else {
00232     cmm = new ContextMemoryManager();
00233   }
00234   cmm->push();
00235   d_topScope = new(cmm) Scope(this, cmm, d_topScope);
00236   //  TRACE("context", "*** [context] Pushing scope to level ", level(), " {");
00237   IF_DEBUG(DebugCounter maxLevel(debugger.counter("max scope level")));
00238   IF_DEBUG(if(maxLevel<level()) maxLevel=level());
00239 }
00240 
00241 
00242 void Context::pop()
00243 {
00244   Scope* top = d_topScope;
00245   //  TRACE("context", "*** [context] Popping scope from level ", level(), "...");
00246   DebugAssert(top->prevScope() != NULL,
00247         "Illegal to pop last scope off of stack.");
00248   // Notify before popping the scope
00249   for(vector<ContextNotifyObj*>::iterator i=d_notifyObjList.begin(),
00250   iend=d_notifyObjList.end(); i != iend; ++i)
00251     (*i)->notifyPre();
00252   // Pop the scope
00253   d_topScope = top->prevScope();
00254   top->restore();
00255   IF_DEBUG(top->check());
00256   ContextMemoryManager* cmm = top->getCMM();
00257   cmm->pop();
00258   d_cmmStack.push_back(cmm);
00259 
00260   // Notify after the pop is done
00261   for(vector<ContextNotifyObj*>::iterator i=d_notifyObjList.begin(),
00262   iend=d_notifyObjList.end(); i != iend; ++i)
00263     (*i)->notify();
00264   //  TRACE("context", "*** [context] Popped scope to level ", level(), "}");
00265   IF_DEBUG(
00266     string indentStr(level(), ' ');
00267     TRACE("pushpop", indentStr, "}", " Pop");
00268   )
00269 }
00270 
00271 
00272 void Context::popto(int toLevel)
00273 {
00274   while (toLevel < topScope()->level()) pop();
00275 }
00276 
00277 
00278 void Context::deleteNotifyObj(ContextNotifyObj* obj) {
00279   size_t i(0), iend(d_notifyObjList.size());
00280   for(; i<iend && d_notifyObjList[i]!=obj; ++i);
00281   if(i<iend) { // Found obj; delete it from the vector
00282     d_notifyObjList[i]=d_notifyObjList.back();
00283     d_notifyObjList.pop_back();
00284   }
00285 }
00286 
00287 
00288 unsigned long Context::getMemory()
00289 {
00290   Scope* scope = d_topScope;
00291   unsigned long memory = ContextMemoryManager::getStaticMemory();
00292   unsigned long mem = 0;
00293   cout << "Static: " << memory << endl;
00294   while (scope != NULL) {
00295     mem = scope->getCMM()->getMemory();
00296     cout << "Scope " << scope->level() << ": " << mem << endl;
00297     memory += mem;
00298     scope = scope->prevScope();
00299   }
00300   mem = 0;
00301   for (unsigned long i = 0; i < d_cmmStack.size(); ++i) {
00302     mem += d_cmmStack[i]->getMemory();
00303   }
00304   cout << "Stack: " << mem << endl;
00305   return memory + mem;
00306 }
00307 
00308 
00309 ///////////////////////////////////////////////////////////////////////////////
00310 // ContextManager methods                                                    //
00311 ///////////////////////////////////////////////////////////////////////////////
00312 
00313 
00314 ContextManager::ContextManager()
00315 {
00316   d_curContext = createContext("default");
00317 }
00318 
00319 
00320 ContextManager::~ContextManager()
00321 {
00322   while (d_contexts.size()) {
00323     delete d_contexts.back();
00324     d_contexts.pop_back();
00325   }
00326 }
00327 
00328 
00329 Context* ContextManager::createContext(const string& name)
00330 {
00331   d_contexts.push_back(new Context(this, name, d_contexts.size()));
00332   return d_contexts.back();
00333 }
00334 
00335 
00336 Context* ContextManager::switchContext(Context* context)
00337 {
00338   FatalAssert(false, "Multiple contexts not yet implemented");
00339   Context* old = d_curContext;
00340   DebugAssert(context && context == d_contexts[context->id()],
00341         "Unknown context");
00342   d_curContext = context;
00343   // TODO: Fix up all Context Objects
00344   return old;
00345 }
00346 
00347 
00348 unsigned long ContextManager::getMemory()
00349 {
00350   return d_curContext->getMemory();
00351 }

Generated on Tue Jul 3 14:33:36 2007 for CVC3 by  doxygen 1.5.1