GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/context/context.cpp Lines: 170 198 85.9 %
Date: 2021-03-22 Branches: 210 582 36.1 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file context.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Clark Barrett, Morgan Deters, Tim King
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief Implementation of base context operations.
13
 **
14
 ** Implementation of base context operations.
15
 **/
16
17
#include <iostream>
18
#include <string>
19
#include <vector>
20
21
#include "base/check.h"
22
#include "context/context.h"
23
24
25
namespace CVC4 {
26
namespace context {
27
28
29
1300775
Context::Context() : d_pCNOpre(NULL), d_pCNOpost(NULL) {
30
  // Create new memory manager
31
1300775
  d_pCMM = new ContextMemoryManager();
32
33
  // Create initial Scope
34
1300775
  d_scopeList.push_back(new(d_pCMM) Scope(this, d_pCMM, 0));
35
1300775
}
36
37
38
2601238
Context::~Context() {
39
  // Delete all Scopes
40
1300619
  popto(0);
41
42
  // Delete the memory manager
43
1300619
  delete d_pCMM;
44
45
  // Clear ContextNotifyObj lists so there are no dangling pointers
46
  ContextNotifyObj* pCNO;
47
1300623
  while(d_pCNOpre != NULL) {
48
2
    pCNO = d_pCNOpre;
49
2
    pCNO->d_ppCNOprev = NULL;
50
2
    d_pCNOpre = pCNO->d_pCNOnext;
51
2
    pCNO->d_pCNOnext = NULL;
52
  }
53
1300623
  while(d_pCNOpost != NULL) {
54
2
    pCNO = d_pCNOpost;
55
2
    pCNO->d_ppCNOprev = NULL;
56
2
    d_pCNOpost = pCNO->d_pCNOnext;
57
2
    pCNO->d_pCNOnext = NULL;
58
  }
59
1300619
}
60
61
62
2849006
void Context::push() {
63
5698012
  Trace("pushpop") << std::string(2 * getLevel(), ' ') << "Push [to "
64
2849006
                   << getLevel() + 1 << "] { " << this << std::endl;
65
66
  // Create a new memory region
67
2849006
  d_pCMM->push();
68
69
  // Create a new top Scope
70
2849006
  d_scopeList.push_back(new(d_pCMM) Scope(this, d_pCMM, getLevel()+1));
71
2849006
}
72
73
74
2848945
void Context::pop() {
75
2848945
  Assert(getLevel() > 0) << "Cannot pop below level 0";
76
77
  // Notify the (pre-pop) ContextNotifyObj objects
78
2848945
  ContextNotifyObj* pCNO = d_pCNOpre;
79
2848961
  while(pCNO != NULL) {
80
    // pre-store the "next" pointer in case pCNO deletes itself on notify()
81
8
    ContextNotifyObj* next = pCNO->d_pCNOnext;
82
8
    pCNO->contextNotifyPop();
83
8
    pCNO = next;
84
  }
85
86
  // Grab the top Scope
87
2848945
  Scope* pScope = d_scopeList.back();
88
89
  // Restore the previous Scope
90
2848945
  d_scopeList.pop_back();
91
92
  // Restore all objects in the top Scope
93
2848945
  delete pScope;
94
95
  // Pop the memory region
96
2848945
  d_pCMM->pop();
97
98
  // Notify the (post-pop) ContextNotifyObj objects
99
2848945
  pCNO = d_pCNOpost;
100
95407067
  while(pCNO != NULL) {
101
    // pre-store the "next" pointer in case pCNO deletes itself on notify()
102
46279061
    ContextNotifyObj* next = pCNO->d_pCNOnext;
103
46279061
    pCNO->contextNotifyPop();
104
46279061
    pCNO = next;
105
  }
106
107
5697890
  Trace("pushpop") << std::string(2 * getLevel(), ' ') << "} Pop [to "
108
2848945
                   << getLevel() << "] " << this << std::endl;
109
2848945
}
110
111
112
1319881
void Context::popto(int toLevel) {
113
  // Pop scopes until there are none left or toLevel is reached
114
1319881
  if(toLevel < 0) toLevel = 0;
115
1338926
  while(toLevel < getLevel()) pop();
116
1319881
}
117
118
119
4
void Context::addNotifyObjPre(ContextNotifyObj* pCNO) {
120
  // Insert pCNO at *front* of list
121
4
  if(d_pCNOpre != NULL)
122
2
    d_pCNOpre->prev() = &(pCNO->next());
123
4
  pCNO->next() = d_pCNOpre;
124
4
  pCNO->prev() = &d_pCNOpre;
125
4
  d_pCNOpre = pCNO;
126
4
}
127
128
129
291351
void Context::addNotifyObjPost(ContextNotifyObj* pCNO) {
130
  // Insert pCNO at *front* of list
131
291351
  if(d_pCNOpost != NULL)
132
245096
    d_pCNOpost->prev() = &(pCNO->next());
133
291351
  pCNO->next() = d_pCNOpost;
134
291351
  pCNO->prev() = &d_pCNOpost;
135
291351
  d_pCNOpost = pCNO;
136
291351
}
137
138
103523181
void ContextObj::update()
139
{
140
207046362
  Debug("context") << "before update(" << this << "):" << std::endl
141
207046362
                   << "context is " << getContext() << std::endl
142
103523181
                   << *getContext() << std::endl;
143
144
  // Call save() to save the information in the current object
145
103523181
  ContextObj* pContextObjSaved = save(d_pScope->getCMM());
146
147
207046362
  Debug("context") << "in update(" << this << ") with restore "
148
103523181
                   << pContextObjSaved << ": waypoint 1" << std::endl
149
103523181
                   << *getContext() << std::endl;
150
151
  // Check that base class data was saved
152
103523181
  Assert((pContextObjSaved->d_pContextObjNext == d_pContextObjNext
153
          && pContextObjSaved->d_ppContextObjPrev == d_ppContextObjPrev
154
          && pContextObjSaved->d_pContextObjRestore == d_pContextObjRestore
155
          && pContextObjSaved->d_pScope == d_pScope))
156
      << "save() did not properly copy information in base class";
157
158
  // Link the "saved" object in place of this ContextObj in the scope
159
  // we're moving it FROM.
160
207046362
  Debug("context") << "in update(" << this
161
103523181
                   << "): next() == " << next() << std::endl;
162
103523181
  if(next() != NULL) {
163
201797766
    Debug("context") << "in update(" << this
164
100898883
                     << "): next()->prev() == " << next()->prev() << std::endl;
165
100898883
    next()->prev() = &pContextObjSaved->next();
166
201797766
    Debug("context") << "in update(" << this
167
100898883
                     << "): next()->prev() is now "
168
100898883
                     << next()->prev() << std::endl;
169
  }
170
207046362
  Debug("context") << "in update(" << this
171
103523181
                   << "): prev() == " << prev() << std::endl;
172
207046362
  Debug("context") << "in update(" << this
173
103523181
                   << "): *prev() == " << *prev() << std::endl;
174
103523181
  *prev() = pContextObjSaved;
175
207046362
  Debug("context") << "in update(" << this
176
103523181
                   << "): *prev() is now " << *prev() << std::endl;
177
178
207046362
  Debug("context") << "in update(" << this << ") with restore "
179
103523181
                   << pContextObjSaved << ": waypoint 3" << std::endl
180
103523181
                   << *getContext() << std::endl;
181
182
  // Update Scope pointer to current top Scope
183
103523181
  d_pScope = d_pScope->getContext()->getTopScope();
184
185
  // Store the saved copy in the restore pointer
186
103523181
  d_pContextObjRestore = pContextObjSaved;
187
188
  // Insert object into the list of objects that need to be restored when this
189
  // Scope is popped.
190
103523181
  d_pScope->addToChain(this);
191
192
207046362
  Debug("context") << "after update(" << this << ") with restore "
193
103523181
                   << pContextObjSaved << ":" << std::endl
194
103523181
                   << *getContext() << std::endl;
195
103523181
}
196
197
103522938
ContextObj* ContextObj::restoreAndContinue()
198
{
199
  // Variable to hold next object in list
200
  ContextObj* pContextObjNext;
201
202
  // Check the restore pointer.  If NULL, this must be the bottom Scope
203
103522938
  if(d_pContextObjRestore == NULL) {
204
    // might not be bottom scope, since objects allocated in context
205
    // memory don't get linked to scope 0
206
    //
207
    // Assert(d_pScope == d_pScope->getContext()->getBottomScope()) <<
208
    //        "Expected bottom scope";
209
210
    Debug("context") << "NULL restore object! " << this << std::endl;
211
    pContextObjNext = d_pContextObjNext;
212
    d_pScope = nullptr;
213
214
    // Nothing else to do
215
  } else {
216
    // Call restore to update the subclass data
217
103522938
    restore(d_pContextObjRestore);
218
219
    // Remember the next object in the list
220
103522938
    pContextObjNext = d_pContextObjNext;
221
222
    // Restore the base class data
223
103522938
    d_pScope = d_pContextObjRestore->d_pScope;
224
103522938
    next() = d_pContextObjRestore->d_pContextObjNext;
225
103522938
    prev() = d_pContextObjRestore->d_ppContextObjPrev;
226
103522938
    d_pContextObjRestore = d_pContextObjRestore->d_pContextObjRestore;
227
228
    // Re-link this ContextObj to the list in this scope
229
103522938
    if(next() != NULL) {
230
100898045
      next()->prev() = &next();
231
    }
232
103522938
    *prev() = this;
233
  }
234
235
  // Return the next object in the list
236
103522938
  return pContextObjNext;
237
}
238
239
70279597
void ContextObj::destroy()
240
{
241
  /* The object to destroy must be valid, i.e., its current state must belong
242
   * to a scope. We remove the object and its previous versions from their
243
   * respective scopes below. If this assertion is failing, you may have
244
   * created an object at a non-zero level and let it outlive the destruction
245
   * of that level. */
246
70279597
  Assert(d_pScope != nullptr);
247
  /* Context can be big and complicated, so we only want to process this output
248
   * if we're really going to use it. (Same goes below.) */
249
140559194
  Debug("context") << "before destroy " << this << " (level " << getLevel()
250
70279597
                   << "):" << std::endl << *getContext() << std::endl;
251
252
  for (;;)
253
  {
254
    // If valgrind reports invalid writes on the next few lines,
255
    // here's a hint: make sure all classes derived from ContextObj in
256
    // the system properly call destroy() in their destructors.
257
    // That's needed to maintain this linked list properly.
258
70383055
    if (next() != nullptr)
259
    {
260
67437759
      next()->prev() = prev();
261
    }
262
70331326
    *prev() = next();
263
70331326
    if (d_pContextObjRestore == nullptr)
264
    {
265
70279597
      break;
266
    }
267
103458
    Debug("context") << "in destroy " << this << ", restore object is "
268
51729
                     << d_pContextObjRestore << " at level "
269
103458
                     << d_pContextObjRestore->getLevel() << ":" << std::endl
270
51729
                     << *getContext() << std::endl;
271
51729
    restoreAndContinue();
272
  }
273
140559194
  Debug("context") << "after destroy " << this << ":" << std::endl
274
70279597
                   << *getContext() << std::endl;
275
70279597
}
276
277
278
6859242
ContextObj::ContextObj(Context* pContext) :
279
  d_pScope(NULL),
280
  d_pContextObjRestore(NULL),
281
  d_pContextObjNext(NULL),
282
6859242
  d_ppContextObjPrev(NULL) {
283
6859242
  Assert(pContext != NULL) << "NULL context pointer";
284
285
6859242
  Debug("context") << "create new ContextObj(" << this << " inCMM=false)" << std::endl;
286
6859242
  d_pScope = pContext->getBottomScope();
287
6859242
  d_pScope->addToChain(this);
288
6859242
}
289
290
291
63422627
ContextObj::ContextObj(bool allocatedInCMM, Context* pContext) :
292
  d_pScope(NULL),
293
  d_pContextObjRestore(NULL),
294
  d_pContextObjNext(NULL),
295
63422627
  d_ppContextObjPrev(NULL) {
296
63422627
  Assert(pContext != NULL) << "NULL context pointer";
297
298
63422627
  Debug("context") << "create new ContextObj(" << this << " inCMM=" << allocatedInCMM << ")" << std::endl;
299
63422627
  if(allocatedInCMM) {
300
    d_pScope = pContext->getTopScope();
301
  } else {
302
63422627
    d_pScope = pContext->getBottomScope();
303
  }
304
63422627
  d_pScope->addToChain(this);
305
63422627
}
306
307
56823891
void ContextObj::enqueueToGarbageCollect() {
308
56823891
  Assert(d_pScope != NULL);
309
56823891
  d_pScope->enqueueToGarbageCollect(this);
310
56823891
}
311
312
291355
ContextNotifyObj::ContextNotifyObj(Context* pContext, bool preNotify) {
313
291355
  if(preNotify) {
314
4
    pContext->addNotifyObjPre(this);
315
  } else {
316
291351
    pContext->addNotifyObjPost(this);
317
  }
318
291355
}
319
320
321
582386
ContextNotifyObj::~ContextNotifyObj() {
322
291193
  if(d_pCNOnext != NULL) {
323
164141
    d_pCNOnext->d_ppCNOprev = d_ppCNOprev;
324
  }
325
291193
  if(d_ppCNOprev != NULL) {
326
291189
    *d_ppCNOprev = d_pCNOnext;
327
  }
328
291193
}
329
330
std::ostream& operator<<(std::ostream& out, const Context& context)
331
{
332
  static const std::string separator(79, '-');
333
334
  int level = context.d_scopeList.size() - 1;
335
  typedef std::vector<Scope*>::const_reverse_iterator const_reverse_iterator;
336
  for(const_reverse_iterator i = context.d_scopeList.rbegin();
337
      i != context.d_scopeList.rend();
338
      ++i, --level) {
339
    Scope* pScope = *i;
340
    Assert(pScope->getLevel() == level);
341
    Assert(pScope->getContext() == &context);
342
    out << separator << std::endl
343
        << *pScope << std::endl;
344
  }
345
  return out << separator << std::endl;
346
}
347
348
std::ostream& operator<<(std::ostream& out, const Scope& scope)
349
{
350
  out << "Scope " << scope.d_level << " [" << &scope << "]:";
351
  ContextObj* pContextObj = scope.d_pContextObjList;
352
  Assert(pContextObj == NULL
353
         || pContextObj->prev() == &scope.d_pContextObjList);
354
  while(pContextObj != NULL) {
355
    out << " <--> " << pContextObj;
356
    if(pContextObj->d_pScope != &scope) {
357
      out << " XXX bad scope" << std::endl;
358
    }
359
    Assert(pContextObj->d_pScope == &scope);
360
    Assert(pContextObj->next() == NULL
361
           || pContextObj->next()->prev() == &pContextObj->next());
362
    pContextObj = pContextObj->next();
363
  }
364
  return out << " --> NULL";
365
}
366
367
109169099
Scope::~Scope() {
368
  // Call restore() method on each ContextObj object in the list.
369
  // Note that it is the responsibility of restore() to return the
370
  // next item in the list.
371
209791363
  while (d_pContextObjList != NULL) {
372
103471209
    d_pContextObjList = d_pContextObjList->restoreAndContinue();
373
  }
374
375
2848945
  if (d_garbage) {
376
115911432
    while (!d_garbage->empty()) {
377
56823891
      ContextObj* obj = d_garbage->back();
378
56823891
      d_garbage->pop_back();
379
56823891
      obj->deleteSelf();
380
    }
381
  }
382
2848945
}
383
384
56823891
void Scope::enqueueToGarbageCollect(ContextObj* obj) {
385
56823891
  if (!d_garbage) {
386
2263650
    d_garbage.reset(new std::vector<ContextObj*>);
387
  }
388
56823891
  d_garbage->push_back(obj);
389
56823891
}
390
391
} /* CVC4::context namespace */
392
26676
} /* CVC4 namespace */