CVC3

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 unsigned long Scope::getMemory(int verbosity)
00083 {
00084   unsigned long memSelf = 0; // scope is allocated in cmm
00085   unsigned long mem = 0;
00086 
00087   mem += getCMM()->getMemory(verbosity - 1);
00088   if (d_prevScope != NULL) {
00089     mem += d_prevScope->getMemory(verbosity - 1);
00090   }
00091 
00092   // TODO: d_restoreChain?
00093 
00094   if (verbosity > 0) {
00095     cout << "Scope " << d_level << ": " << memSelf << endl;
00096     cout << "  Children: " << mem << endl;
00097     cout << "  Total: " << mem+memSelf << endl;
00098   }
00099 
00100   return mem + memSelf;
00101 
00102 
00103 }
00104 
00105 
00106 ///////////////////////////////////////////////////////////////////////////////
00107 // ContextObjChain methods                                                   //
00108 ///////////////////////////////////////////////////////////////////////////////
00109 
00110 
00111 ContextObjChain* ContextObjChain::restore(void)
00112 {
00113   // Assign 'next' pointer only when the master object is restored,
00114   // since this may change our next pointer (master may have other
00115   // context objects removed).
00116   DebugAssert(d_master != NULL, "How did this happen");
00117   //  if (d_master == NULL) return d_restoreChainNext;
00118   ContextObjChain* next;
00119   DebugAssert(d_data != NULL, "Shouldn't happen");
00120 //   if (d_data == NULL) {
00121 //     d_master->setNull();
00122 //     d_master->d_scope = d_master->d_scope->prevScope();
00123 //     DebugAssert(d_restore==NULL,"Expected NULL");
00124 //     next = d_restoreChainNext;
00125 //     d_master->d_scope->addToChain(this);
00126 //   }
00127 //   else {
00128     d_master->restoreData(d_data);
00129     d_master->d_scope = d_data->d_scope;
00130     d_master->d_restore = d_restore;
00131     next = d_restoreChainNext;
00132     if (d_data != NULL) delete d_data;
00133     DebugAssert(d_master->d_restore != this, "points to self");
00134 //   }
00135   return next;
00136 }
00137 
00138 
00139 #ifdef _CVC3_DEBUG_MODE
00140 std::string ContextObjChain::name() const
00141 {
00142   DebugAssert(d_master != NULL, "NULL master");
00143   return d_master->name();
00144 }
00145 #endif
00146 
00147 
00148 ///////////////////////////////////////////////////////////////////////////////
00149 // ContextObj methods                                                        //
00150 ///////////////////////////////////////////////////////////////////////////////
00151 
00152 
00153 void ContextObj::update(int scope)
00154 {
00155   Scope* tmpScope = d_scope;
00156   DebugAssert(scope < 0 || d_scope->level() <= scope,
00157         "ContextObj::update(scope="+int2string(scope)
00158         +"): scope < d_scope->level() = "
00159         +int2string(d_scope->level()));
00160   d_scope = d_scope->topScope();
00161   if (scope >= 0) {
00162     // Fetch the specified scope
00163     for(int i=level(); i>scope; --i) {
00164       d_scope = d_scope->prevScope();
00165       DebugAssert(d_scope != NULL, "ContextObj::update["
00166       +name()+"]: d_scope == NULL");
00167     }
00168   }
00169   ContextObj* data = makeCopy(getCMM());
00170   data->d_scope = tmpScope;
00171   // The destructor of the copy should not destroy our older copies
00172   data->d_restore=NULL;
00173   IF_DEBUG(data->setName(name()+" [copy]");)
00174   d_restore = new(getCMM()) ContextObjChain(data, this, d_restore);
00175   d_scope->addToChain(d_restore);
00176 }
00177 
00178 
00179 ContextObj::~ContextObj()
00180 {
00181   // Delete our restore copies
00182   IF_DEBUG(FatalAssert(d_active, "~ContextObj["+name()+"]");)
00183   IF_DEBUG(d_active=false);;
00184   for(ContextObjChain* obj = d_restore; obj != NULL; ) {
00185     ContextObjChain* tmp = obj->d_restore;
00186     // Remove the object from the restore chain
00187     if(obj->d_restoreChainNext != NULL)
00188       obj->d_restoreChainNext->d_restoreChainPrev = obj->d_restoreChainPrev;
00189     *(obj->d_restoreChainPrev) = obj->d_restoreChainNext;
00190     //    if (obj->d_data != NULL) delete obj->d_data;
00191     obj->d_master = NULL;
00192     if (tmp == NULL) {
00193       delete obj;
00194       free(obj);
00195       break;
00196     }
00197     obj = tmp;
00198   }
00199   //  TRACE("context verbose", "~ContextObj()[", this, "] }");
00200 }
00201 
00202 
00203 ///////////////////////////////////////////////////////////////////////////////
00204 // Context methods                                                           //
00205 ///////////////////////////////////////////////////////////////////////////////
00206 
00207 
00208 Context::Context(ContextManager* cm, const string& name, int id)
00209   : d_cm(cm), d_name(name), d_id(id)
00210 {
00211   ContextMemoryManager* cmm = new ContextMemoryManager();
00212   d_topScope = new(cmm) Scope(this, cmm);
00213   d_bottomScope = d_topScope;
00214   TRACE("context", "*** [context] Creating new context: name = "
00215   + name + "id = ", id, "");
00216 }
00217 
00218 
00219 // Don't pop, just delete everything.  At this point, most of the
00220 // system is already destroyed, popping may be dangerous.
00221 Context::~Context()
00222 {
00223   // popto(0);
00224   Scope* top = d_topScope;
00225   while(top != NULL) {
00226     top = d_topScope->prevScope();
00227     d_topScope->finalize();
00228     delete d_topScope->getCMM();
00229     d_topScope = top;
00230   }
00231   while (!d_cmmStack.empty()) {
00232     delete d_cmmStack.back();
00233     d_cmmStack.pop_back();
00234   }
00235   ContextMemoryManager::garbageCollect();
00236   // Erase ourselves from the notify objects, so they don't call us
00237   for(vector<ContextNotifyObj*>::iterator i=d_notifyObjList.begin(),
00238   iend=d_notifyObjList.end(); i!=iend; ++i) {
00239     (*i)->d_context = NULL;
00240   }
00241 }
00242 
00243 
00244 void Context::push()
00245 {
00246   IF_DEBUG(
00247     string indentStr(level(), ' ');
00248     TRACE("pushpop", indentStr, "Push", " {");
00249   )
00250   ContextMemoryManager* cmm;
00251   if (!d_cmmStack.empty()) {
00252     cmm = d_cmmStack.back();
00253     d_cmmStack.pop_back();
00254   }
00255   else {
00256     cmm = new ContextMemoryManager();
00257   }
00258   cmm->push();
00259   d_topScope = new(cmm) Scope(this, cmm, d_topScope);
00260   //  TRACE("context", "*** [context] Pushing scope to level ", level(), " {");
00261   IF_DEBUG(DebugCounter maxLevel(debugger.counter("max scope level"));)
00262   IF_DEBUG(if(maxLevel<level()) maxLevel=level();)
00263 }
00264 
00265 
00266 void Context::pop()
00267 {
00268   Scope* top = d_topScope;
00269   //  TRACE("context", "*** [context] Popping scope from level ", level(), "...");
00270   DebugAssert(top->prevScope() != NULL,
00271         "Illegal to pop last scope off of stack.");
00272   // Notify before popping the scope
00273   for(vector<ContextNotifyObj*>::iterator i=d_notifyObjList.begin(),
00274   iend=d_notifyObjList.end(); i != iend; ++i)
00275     (*i)->notifyPre();
00276   // Pop the scope
00277   d_topScope = top->prevScope();
00278   top->restore();
00279   IF_DEBUG(top->check();)
00280   ContextMemoryManager* cmm = top->getCMM();
00281   cmm->pop();
00282   d_cmmStack.push_back(cmm);
00283 
00284   // Notify after the pop is done
00285   for(vector<ContextNotifyObj*>::iterator i=d_notifyObjList.begin(),
00286   iend=d_notifyObjList.end(); i != iend; ++i)
00287     (*i)->notify();
00288   //  TRACE("context", "*** [context] Popped scope to level ", level(), "}");
00289   IF_DEBUG(
00290     string indentStr(level(), ' ');
00291     TRACE("pushpop", indentStr, "}", " Pop");
00292   )
00293 }
00294 
00295 
00296 void Context::popto(int toLevel)
00297 {
00298   while (toLevel < topScope()->level()) pop();
00299 }
00300 
00301 
00302 void Context::deleteNotifyObj(ContextNotifyObj* obj) {
00303   size_t i(0), iend(d_notifyObjList.size());
00304   for(; i<iend && d_notifyObjList[i]!=obj; ++i);
00305   if(i<iend) { // Found obj; delete it from the vector
00306     d_notifyObjList[i]=d_notifyObjList.back();
00307     d_notifyObjList.pop_back();
00308   }
00309 }
00310 
00311 
00312 unsigned long Context::getMemory(int verbosity)
00313 {
00314   unsigned long memSelf = sizeof(Context);
00315   unsigned long mem = 0;
00316   mem += MemoryTracker::getString(verbosity - 1, d_name);
00317   mem += d_topScope->getMemory(verbosity - 1);
00318   mem += MemoryTracker::getVecAndDataP(verbosity - 1, d_notifyObjList);
00319   mem += MemoryTracker::getVecAndDataP(verbosity - 1, d_cmmStack);
00320   MemoryTracker::print("Context "+d_name, verbosity, memSelf, mem);
00321   return mem + memSelf;
00322 }
00323 
00324 
00325 ///////////////////////////////////////////////////////////////////////////////
00326 // ContextManager methods                                                    //
00327 ///////////////////////////////////////////////////////////////////////////////
00328 
00329 
00330 ContextManager::ContextManager()
00331 {
00332   d_curContext = createContext("default");
00333 }
00334 
00335 
00336 ContextManager::~ContextManager()
00337 {
00338   while (d_contexts.size()) {
00339     delete d_contexts.back();
00340     d_contexts.pop_back();
00341   }
00342 }
00343 
00344 
00345 Context* ContextManager::createContext(const string& name)
00346 {
00347   d_contexts.push_back(new Context(this, name, d_contexts.size()));
00348   return d_contexts.back();
00349 }
00350 
00351 
00352 Context* ContextManager::switchContext(Context* context)
00353 {
00354   FatalAssert(false, "Multiple contexts not yet implemented");
00355   Context* old = d_curContext;
00356   DebugAssert(context && context == d_contexts[context->id()],
00357         "Unknown context");
00358   d_curContext = context;
00359   // TODO: Fix up all Context Objects
00360   return old;
00361 }
00362 
00363 
00364 unsigned long ContextManager::getMemory(int verbosity)
00365 {
00366   unsigned long memSelf = sizeof(ContextManager);
00367   unsigned long mem = 0;
00368 
00369   // free pages in the context memory manager need to be counted somewhere
00370   // this seems as good a place as any
00371   mem += ContextMemoryManager::getStaticMemory(verbosity - 1);
00372 
00373   for (unsigned i = 0; i < d_contexts.size(); ++i) {
00374     mem += d_contexts[i]->getMemory(verbosity - 1);
00375   }
00376 
00377   MemoryTracker::print("ContextManager", verbosity, memSelf, mem);
00378 
00379   return mem + memSelf;
00380 }