CVC3  2.4.1
context.cpp
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file context.cpp
4  *
5  * Author: Clark Barrett
6  *
7  * Created: Fri Jan 17 14:30:37 2003
8  *
9  * <hr>
10  *
11  * License to use, copy, modify, sell and/or distribute this software
12  * and its documentation for any purpose is hereby granted without
13  * royalty, subject to the terms and conditions defined in the \ref
14  * LICENSE file provided with this distribution.
15  *
16  * <hr>
17  *
18  */
19 /*****************************************************************************/
20 
21 
22 #include "context.h"
23 
24 
25 using namespace CVC3;
26 using namespace std;
27 
28 
30 
31 
32 ///////////////////////////////////////////////////////////////////////////////
33 // Scope methods //
34 ///////////////////////////////////////////////////////////////////////////////
35 
36 
37 void Scope::finalize(void)
38 {
39  ContextObjChain* obj = d_restoreChain;
40  while (obj != NULL) {
42  // When called from ~ContextManager(), the master objects may
43  // still point to this scope. Disconnect them here.
44  if (obj->d_master != NULL) {
45  if (obj->d_master->d_scope == this)
46  obj->d_master->d_scope = NULL;
47  if (obj->d_master->d_restore == obj)
48  obj->d_master->d_restore = NULL;
49  }
50  obj = tmp;
51  }
52 }
53 
54 
55 void Scope::check(void)
56 {
57  IF_DEBUG(
58  ContextObjChain* obj = d_restoreChain;
59  if (debugger.trace("memory") && obj != NULL) {
60  ostream& os = debugger.getOS();
61  int n(0);
62  ContextObjChain* tmp = obj;
63  while(tmp != NULL) {
64  tmp = tmp->d_restoreChainNext;
65  n++;
66  }
67  os << "*** Warning: ~Scope(): found "<< n << " leaked objects "
68  << "in scope " << d_level << ":" << endl;
69  if (debugger.flag("memory leaks")) {
70  tmp = obj;
71  while(tmp != NULL) {
72  os << tmp->name() << "\n";
73  tmp = tmp->d_restoreChainNext;
74  }
75  }
76  os << flush;
77  }
78  )
79 }
80 
81 
82 unsigned long Scope::getMemory(int verbosity)
83 {
84  unsigned long memSelf = 0; // scope is allocated in cmm
85  unsigned long mem = 0;
86 
87  mem += getCMM()->getMemory(verbosity - 1);
88  if (d_prevScope != NULL) {
89  mem += d_prevScope->getMemory(verbosity - 1);
90  }
91 
92  // TODO: d_restoreChain?
93 
94  if (verbosity > 0) {
95  cout << "Scope " << d_level << ": " << memSelf << endl;
96  cout << " Children: " << mem << endl;
97  cout << " Total: " << mem+memSelf << endl;
98  }
99 
100  return mem + memSelf;
101 
102 
103 }
104 
105 
106 ///////////////////////////////////////////////////////////////////////////////
107 // ContextObjChain methods //
108 ///////////////////////////////////////////////////////////////////////////////
109 
110 
112 {
113  // Assign 'next' pointer only when the master object is restored,
114  // since this may change our next pointer (master may have other
115  // context objects removed).
116  DebugAssert(d_master != NULL, "How did this happen");
117  // if (d_master == NULL) return d_restoreChainNext;
118  ContextObjChain* next;
119  DebugAssert(d_data != NULL, "Shouldn't happen");
120 // if (d_data == NULL) {
121 // d_master->setNull();
122 // d_master->d_scope = d_master->d_scope->prevScope();
123 // DebugAssert(d_restore==NULL,"Expected NULL");
124 // next = d_restoreChainNext;
125 // d_master->d_scope->addToChain(this);
126 // }
127 // else {
128  d_master->restoreData(d_data);
129  d_master->d_scope = d_data->d_scope;
130  d_master->d_restore = d_restore;
131  next = d_restoreChainNext;
132  if (d_data != NULL) delete d_data;
133  DebugAssert(d_master->d_restore != this, "points to self");
134 // }
135  return next;
136 }
137 
138 
139 #ifdef _CVC3_DEBUG_MODE
140 std::string ContextObjChain::name() const
141 {
142  DebugAssert(d_master != NULL, "NULL master");
143  return d_master->name();
144 }
145 #endif
146 
147 
148 ///////////////////////////////////////////////////////////////////////////////
149 // ContextObj methods //
150 ///////////////////////////////////////////////////////////////////////////////
151 
152 
153 void ContextObj::update(int scope)
154 {
155  Scope* tmpScope = d_scope;
156  DebugAssert(scope < 0 || d_scope->level() <= scope,
157  "ContextObj::update(scope="+int2string(scope)
158  +"): scope < d_scope->level() = "
159  +int2string(d_scope->level()));
160  d_scope = d_scope->topScope();
161  if (scope >= 0) {
162  // Fetch the specified scope
163  for(int i=level(); i>scope; --i) {
164  d_scope = d_scope->prevScope();
165  DebugAssert(d_scope != NULL, "ContextObj::update["
166  +name()+"]: d_scope == NULL");
167  }
168  }
169  ContextObj* data = makeCopy(getCMM());
170  data->d_scope = tmpScope;
171  // The destructor of the copy should not destroy our older copies
172  data->d_restore=NULL;
173  IF_DEBUG(data->setName(name()+" [copy]");)
174  d_restore = new(getCMM()) ContextObjChain(data, this, d_restore);
175  d_scope->addToChain(d_restore);
176 }
177 
178 
180 {
181  // Delete our restore copies
182  IF_DEBUG(FatalAssert(d_active, "~ContextObj["+name()+"]");)
183  IF_DEBUG(d_active=false);;
184  for(ContextObjChain* obj = d_restore; obj != NULL; ) {
185  ContextObjChain* tmp = obj->d_restore;
186  // Remove the object from the restore chain
187  if(obj->d_restoreChainNext != NULL)
189  *(obj->d_restoreChainPrev) = obj->d_restoreChainNext;
190  // if (obj->d_data != NULL) delete obj->d_data;
191  obj->d_master = NULL;
192  if (tmp == NULL) {
193  delete obj;
194  free(obj);
195  break;
196  }
197  obj = tmp;
198  }
199  // TRACE("context verbose", "~ContextObj()[", this, "] }");
200 }
201 
202 
203 ///////////////////////////////////////////////////////////////////////////////
204 // Context methods //
205 ///////////////////////////////////////////////////////////////////////////////
206 
207 
208 Context::Context(ContextManager* cm, const string& name, int id)
209  : d_cm(cm), d_name(name), d_id(id)
210 {
212  d_topScope = new(cmm) Scope(this, cmm);
214  TRACE("context", "*** [context] Creating new context: name = "
215  + name + "id = ", id, "");
216 }
217 
218 
219 // Don't pop, just delete everything. At this point, most of the
220 // system is already destroyed, popping may be dangerous.
222 {
223  // popto(0);
224  Scope* top = d_topScope;
225  while(top != NULL) {
226  top = d_topScope->prevScope();
227  d_topScope->finalize();
228  delete d_topScope->getCMM();
229  d_topScope = top;
230  }
231  while (!d_cmmStack.empty()) {
232  delete d_cmmStack.back();
233  d_cmmStack.pop_back();
234  }
236  // Erase ourselves from the notify objects, so they don't call us
237  for(vector<ContextNotifyObj*>::iterator i=d_notifyObjList.begin(),
238  iend=d_notifyObjList.end(); i!=iend; ++i) {
239  (*i)->d_context = NULL;
240  }
241 }
242 
243 
245 {
246  IF_DEBUG(
247  string indentStr(level(), ' ');
248  TRACE("pushpop", indentStr, "Push", " {");
249  )
251  if (!d_cmmStack.empty()) {
252  cmm = d_cmmStack.back();
253  d_cmmStack.pop_back();
254  }
255  else {
256  cmm = new ContextMemoryManager();
257  }
258  cmm->push();
259  d_topScope = new(cmm) Scope(this, cmm, d_topScope);
260  // TRACE("context", "*** [context] Pushing scope to level ", level(), " {");
261  IF_DEBUG(DebugCounter maxLevel(debugger.counter("max scope level"));)
262  IF_DEBUG(if(maxLevel<level()) maxLevel=level();)
263 }
264 
265 
267 {
268  Scope* top = d_topScope;
269  // TRACE("context", "*** [context] Popping scope from level ", level(), "...");
270  DebugAssert(top->prevScope() != NULL,
271  "Illegal to pop last scope off of stack.");
272  // Notify before popping the scope
273  for(vector<ContextNotifyObj*>::iterator i=d_notifyObjList.begin(),
274  iend=d_notifyObjList.end(); i != iend; ++i)
275  (*i)->notifyPre();
276  // Pop the scope
277  d_topScope = top->prevScope();
278  top->restore();
279  IF_DEBUG(top->check();)
280  ContextMemoryManager* cmm = top->getCMM();
281  cmm->pop();
282  d_cmmStack.push_back(cmm);
283 
284  // Notify after the pop is done
285  for(vector<ContextNotifyObj*>::iterator i=d_notifyObjList.begin(),
286  iend=d_notifyObjList.end(); i != iend; ++i)
287  (*i)->notify();
288  // TRACE("context", "*** [context] Popped scope to level ", level(), "}");
289  IF_DEBUG(
290  string indentStr(level(), ' ');
291  TRACE("pushpop", indentStr, "}", " Pop");
292  )
293 }
294 
295 
296 void Context::popto(int toLevel)
297 {
298  while (toLevel < topScope()->level()) pop();
299 }
300 
301 
303  size_t i(0), iend(d_notifyObjList.size());
304  for(; i<iend && d_notifyObjList[i]!=obj; ++i);
305  if(i<iend) { // Found obj; delete it from the vector
307  d_notifyObjList.pop_back();
308  }
309 }
310 
311 
312 unsigned long Context::getMemory(int verbosity)
313 {
314  unsigned long memSelf = sizeof(Context);
315  unsigned long mem = 0;
316  mem += MemoryTracker::getString(verbosity - 1, d_name);
317  mem += d_topScope->getMemory(verbosity - 1);
318  mem += MemoryTracker::getVecAndDataP(verbosity - 1, d_notifyObjList);
319  mem += MemoryTracker::getVecAndDataP(verbosity - 1, d_cmmStack);
320  MemoryTracker::print("Context "+d_name, verbosity, memSelf, mem);
321  return mem + memSelf;
322 }
323 
324 
325 ///////////////////////////////////////////////////////////////////////////////
326 // ContextManager methods //
327 ///////////////////////////////////////////////////////////////////////////////
328 
329 
331 {
332  d_curContext = createContext("default");
333 }
334 
335 
337 {
338  while (d_contexts.size()) {
339  delete d_contexts.back();
340  d_contexts.pop_back();
341  }
342 }
343 
344 
346 {
347  d_contexts.push_back(new Context(this, name, d_contexts.size()));
348  return d_contexts.back();
349 }
350 
351 
353 {
354  FatalAssert(false, "Multiple contexts not yet implemented");
355  Context* old = d_curContext;
356  DebugAssert(context && context == d_contexts[context->id()],
357  "Unknown context");
358  d_curContext = context;
359  // TODO: Fix up all Context Objects
360  return old;
361 }
362 
363 
364 unsigned long ContextManager::getMemory(int verbosity)
365 {
366  unsigned long memSelf = sizeof(ContextManager);
367  unsigned long mem = 0;
368 
369  // free pages in the context memory manager need to be counted somewhere
370  // this seems as good a place as any
371  mem += ContextMemoryManager::getStaticMemory(verbosity - 1);
372 
373  for (unsigned i = 0; i < d_contexts.size(); ++i) {
374  mem += d_contexts[i]->getMemory(verbosity - 1);
375  }
376 
377  MemoryTracker::print("ContextManager", verbosity, memSelf, mem);
378 
379  return mem + memSelf;
380 }
ContextObjChain ** d_restoreChainPrev
Pointer to the pointer of the previous object which points to us. This makes a doubly-linked list for...
Definition: context.h:144
Context * createContext(const std::string &name="")
Definition: context.cpp:345
int level() const
Definition: context.h:336
ContextObjChain * d_restore
The list of values on previous scopes; our destructor should clean up those.
Definition: context.h:210
static unsigned long getVecAndDataP(int verbosity, const std::vector< T > &v)
Definition: cvc_util.h:152
void push()
Definition: context.cpp:244
static unsigned getStaticMemory(int verbosity)
std::string d_name
Name of context.
Definition: context.h:311
int id() const
Definition: context.h:333
ContextObjChain * d_restore
Pointer to the previous copy which belongs to the same master.
Definition: context.h:147
static unsigned long getString(int verbosity, const std::string &s)
Definition: cvc_util.h:163
ContextObjChain * d_restoreChainNext
Next link in chain.
Definition: context.h:139
void update(int scope=-1)
Update on the given scope, on the current scope if 'scope' == -1.
Definition: context.cpp:153
void pop()
Definition: context.cpp:266
unsigned long getMemory(int verbosity)
Definition: context.cpp:312
std::vector< ContextMemoryManager * > d_cmmStack
Stack of free ContextMemoryManager's.
Definition: context.h:324
#define DebugAssert(cond, str)
Definition: debug.h:408
void deleteNotifyObj(ContextNotifyObj *obj)
Definition: context.cpp:302
Scope * topScope() const
Definition: context.h:334
unsigned long getMemory(int verbosity)
Compute memory used.
Definition: context.cpp:82
Context * switchContext(Context *context)
Definition: context.cpp:352
CVC3::ExprStream & endl(CVC3::ExprStream &os)
Print the end-of-line.
void popto(int toLevel)
Definition: context.cpp:296
ContextMemoryManager * getCMM() const
Definition: context.h:99
#define FatalAssert(cond, msg)
If something goes horribly wrong, print a message and abort immediately with exit(1).
Definition: debug.h:37
Scope * d_topScope
Pointer to top and bottom scopes of context.
Definition: context.h:317
unsigned long getMemory(int verbosity)
Definition: context.cpp:364
void restore(void)
Restore all the values.
Definition: context.h:360
std::vector< ContextNotifyObj * > d_notifyObjList
List of objects to notify with every pop.
Definition: context.h:321
std::string int2string(int n)
Definition: cvc_util.h:46
ContextObjChain * restore(void)
Restore from d_data to d_master.
Definition: context.cpp:111
#define IF_DEBUG(code)
Definition: debug.h:406
static void print(std::string name, int verbosity, unsigned long memSelf, unsigned long mem)
Definition: cvc_util.h:120
void finalize(void)
Called by ~ContextManager.
Definition: context.cpp:37
Scope * d_scope
Last scope in which this object was modified.
Definition: context.h:206
ContextObj * d_master
Pointer to the master object.
Definition: context.h:153
Scope * prevScope() const
Access functions.
Definition: context.h:94
Scope * d_bottomScope
Definition: context.h:318
static std::vector< char * > s_freePages
virtual ~ContextObj()
Definition: context.cpp:179
int level(void) const
Definition: context.h:95
Manager for multiple contexts. Also holds current context.
Definition: context.h:393
Definition: kinds.h:99
Context(ContextManager *cm, const std::string &name, int id)
Definition: context.cpp:208
const std::string & name() const
Definition: context.h:332
void check(void)
Check for memory leaks.
Definition: context.cpp:55