00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
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
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
00043
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
00084
00085
00086
00087 ContextObjChain* ContextObjChain::restore(void)
00088 {
00089
00090
00091
00092 DebugAssert(d_master != NULL, "How did this happen");
00093
00094 ContextObjChain* next;
00095 DebugAssert(d_data != NULL, "Shouldn't happen");
00096
00097
00098
00099
00100
00101
00102
00103
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
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
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
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
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
00163 if(obj->d_restoreChainNext != NULL)
00164 obj->d_restoreChainNext->d_restoreChainPrev = obj->d_restoreChainPrev;
00165 *(obj->d_restoreChainPrev) = obj->d_restoreChainNext;
00166
00167 obj->d_master = NULL;
00168 if (tmp == NULL) {
00169 delete obj;
00170 free(obj);
00171 break;
00172 }
00173 obj = tmp;
00174 }
00175
00176 }
00177
00178
00179
00180
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
00196
00197 Context::~Context()
00198 {
00199
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
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
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
00246 DebugAssert(top->prevScope() != NULL,
00247 "Illegal to pop last scope off of stack.");
00248
00249 for(vector<ContextNotifyObj*>::iterator i=d_notifyObjList.begin(),
00250 iend=d_notifyObjList.end(); i != iend; ++i)
00251 (*i)->notifyPre();
00252
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
00261 for(vector<ContextNotifyObj*>::iterator i=d_notifyObjList.begin(),
00262 iend=d_notifyObjList.end(); i != iend; ++i)
00263 (*i)->notify();
00264
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) {
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
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
00344 return old;
00345 }
00346
00347
00348 unsigned long ContextManager::getMemory()
00349 {
00350 return d_curContext->getMemory();
00351 }