GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/context/context.cpp Lines: 170 198 85.9 %
Date: 2021-03-23 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
1300809
Context::Context() : d_pCNOpre(NULL), d_pCNOpost(NULL) {
30
  // Create new memory manager
31
1300809
  d_pCMM = new ContextMemoryManager();
32
33
  // Create initial Scope
34
1300809
  d_scopeList.push_back(new(d_pCMM) Scope(this, d_pCMM, 0));
35
1300809
}
36
37
38
2601306
Context::~Context() {
39
  // Delete all Scopes
40
1300653
  popto(0);
41
42
  // Delete the memory manager
43
1300653
  delete d_pCMM;
44
45
  // Clear ContextNotifyObj lists so there are no dangling pointers
46
  ContextNotifyObj* pCNO;
47
1300657
  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
1300657
  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
1300653
}
60
61
62
2849091
void Context::push() {
63
5698182
  Trace("pushpop") << std::string(2 * getLevel(), ' ') << "Push [to "
64
2849091
                   << getLevel() + 1 << "] { " << this << std::endl;
65
66
  // Create a new memory region
67
2849091
  d_pCMM->push();
68
69
  // Create a new top Scope
70
2849091
  d_scopeList.push_back(new(d_pCMM) Scope(this, d_pCMM, getLevel()+1));
71
2849091
}
72
73
74
2849030
void Context::pop() {
75
2849030
  Assert(getLevel() > 0) << "Cannot pop below level 0";
76
77
  // Notify the (pre-pop) ContextNotifyObj objects
78
2849030
  ContextNotifyObj* pCNO = d_pCNOpre;
79
2849046
  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
2849030
  Scope* pScope = d_scopeList.back();
88
89
  // Restore the previous Scope
90
2849030
  d_scopeList.pop_back();
91
92
  // Restore all objects in the top Scope
93
2849030
  delete pScope;
94
95
  // Pop the memory region
96
2849030
  d_pCMM->pop();
97
98
  // Notify the (post-pop) ContextNotifyObj objects
99
2849030
  pCNO = d_pCNOpost;
100
95409602
  while(pCNO != NULL) {
101
    // pre-store the "next" pointer in case pCNO deletes itself on notify()
102
46280286
    ContextNotifyObj* next = pCNO->d_pCNOnext;
103
46280286
    pCNO->contextNotifyPop();
104
46280286
    pCNO = next;
105
  }
106
107
5698060
  Trace("pushpop") << std::string(2 * getLevel(), ' ') << "} Pop [to "
108
2849030
                   << getLevel() << "] " << this << std::endl;
109
2849030
}
110
111
112
1319919
void Context::popto(int toLevel) {
113
  // Pop scopes until there are none left or toLevel is reached
114
1319919
  if(toLevel < 0) toLevel = 0;
115
1338968
  while(toLevel < getLevel()) pop();
116
1319919
}
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
291415
void Context::addNotifyObjPost(ContextNotifyObj* pCNO) {
130
  // Insert pCNO at *front* of list
131
291415
  if(d_pCNOpost != NULL)
132
245150
    d_pCNOpost->prev() = &(pCNO->next());
133
291415
  pCNO->next() = d_pCNOpost;
134
291415
  pCNO->prev() = &d_pCNOpost;
135
291415
  d_pCNOpost = pCNO;
136
291415
}
137
138
103529816
void ContextObj::update()
139
{
140
207059632
  Debug("context") << "before update(" << this << "):" << std::endl
141
207059632
                   << "context is " << getContext() << std::endl
142
103529816
                   << *getContext() << std::endl;
143
144
  // Call save() to save the information in the current object
145
103529816
  ContextObj* pContextObjSaved = save(d_pScope->getCMM());
146
147
207059632
  Debug("context") << "in update(" << this << ") with restore "
148
103529816
                   << pContextObjSaved << ": waypoint 1" << std::endl
149
103529816
                   << *getContext() << std::endl;
150
151
  // Check that base class data was saved
152
103529816
  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
207059632
  Debug("context") << "in update(" << this
161
103529816
                   << "): next() == " << next() << std::endl;
162
103529816
  if(next() != NULL) {
163
201810882
    Debug("context") << "in update(" << this
164
100905441
                     << "): next()->prev() == " << next()->prev() << std::endl;
165
100905441
    next()->prev() = &pContextObjSaved->next();
166
201810882
    Debug("context") << "in update(" << this
167
100905441
                     << "): next()->prev() is now "
168
100905441
                     << next()->prev() << std::endl;
169
  }
170
207059632
  Debug("context") << "in update(" << this
171
103529816
                   << "): prev() == " << prev() << std::endl;
172
207059632
  Debug("context") << "in update(" << this
173
103529816
                   << "): *prev() == " << *prev() << std::endl;
174
103529816
  *prev() = pContextObjSaved;
175
207059632
  Debug("context") << "in update(" << this
176
103529816
                   << "): *prev() is now " << *prev() << std::endl;
177
178
207059632
  Debug("context") << "in update(" << this << ") with restore "
179
103529816
                   << pContextObjSaved << ": waypoint 3" << std::endl
180
103529816
                   << *getContext() << std::endl;
181
182
  // Update Scope pointer to current top Scope
183
103529816
  d_pScope = d_pScope->getContext()->getTopScope();
184
185
  // Store the saved copy in the restore pointer
186
103529816
  d_pContextObjRestore = pContextObjSaved;
187
188
  // Insert object into the list of objects that need to be restored when this
189
  // Scope is popped.
190
103529816
  d_pScope->addToChain(this);
191
192
207059632
  Debug("context") << "after update(" << this << ") with restore "
193
103529816
                   << pContextObjSaved << ":" << std::endl
194
103529816
                   << *getContext() << std::endl;
195
103529816
}
196
197
103529573
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
103529573
  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
103529573
    restore(d_pContextObjRestore);
218
219
    // Remember the next object in the list
220
103529573
    pContextObjNext = d_pContextObjNext;
221
222
    // Restore the base class data
223
103529573
    d_pScope = d_pContextObjRestore->d_pScope;
224
103529573
    next() = d_pContextObjRestore->d_pContextObjNext;
225
103529573
    prev() = d_pContextObjRestore->d_ppContextObjPrev;
226
103529573
    d_pContextObjRestore = d_pContextObjRestore->d_pContextObjRestore;
227
228
    // Re-link this ContextObj to the list in this scope
229
103529573
    if(next() != NULL) {
230
100904603
      next()->prev() = &next();
231
    }
232
103529573
    *prev() = this;
233
  }
234
235
  // Return the next object in the list
236
103529573
  return pContextObjNext;
237
}
238
239
70294338
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
70294338
  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
140588676
  Debug("context") << "before destroy " << this << " (level " << getLevel()
250
70294338
                   << "):" << 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
70397800
    if (next() != nullptr)
259
    {
260
67452592
      next()->prev() = prev();
261
    }
262
70346069
    *prev() = next();
263
70346069
    if (d_pContextObjRestore == nullptr)
264
    {
265
70294338
      break;
266
    }
267
103462
    Debug("context") << "in destroy " << this << ", restore object is "
268
51731
                     << d_pContextObjRestore << " at level "
269
103462
                     << d_pContextObjRestore->getLevel() << ":" << std::endl
270
51731
                     << *getContext() << std::endl;
271
51731
    restoreAndContinue();
272
  }
273
140588676
  Debug("context") << "after destroy " << this << ":" << std::endl
274
70294338
                   << *getContext() << std::endl;
275
70294338
}
276
277
278
6869518
ContextObj::ContextObj(Context* pContext) :
279
  d_pScope(NULL),
280
  d_pContextObjRestore(NULL),
281
  d_pContextObjNext(NULL),
282
6869518
  d_ppContextObjPrev(NULL) {
283
6869518
  Assert(pContext != NULL) << "NULL context pointer";
284
285
6869518
  Debug("context") << "create new ContextObj(" << this << " inCMM=false)" << std::endl;
286
6869518
  d_pScope = pContext->getBottomScope();
287
6869518
  d_pScope->addToChain(this);
288
6869518
}
289
290
291
63427095
ContextObj::ContextObj(bool allocatedInCMM, Context* pContext) :
292
  d_pScope(NULL),
293
  d_pContextObjRestore(NULL),
294
  d_pContextObjNext(NULL),
295
63427095
  d_ppContextObjPrev(NULL) {
296
63427095
  Assert(pContext != NULL) << "NULL context pointer";
297
298
63427095
  Debug("context") << "create new ContextObj(" << this << " inCMM=" << allocatedInCMM << ")" << std::endl;
299
63427095
  if(allocatedInCMM) {
300
    d_pScope = pContext->getTopScope();
301
  } else {
302
63427095
    d_pScope = pContext->getBottomScope();
303
  }
304
63427095
  d_pScope->addToChain(this);
305
63427095
}
306
307
56828268
void ContextObj::enqueueToGarbageCollect() {
308
56828268
  Assert(d_pScope != NULL);
309
56828268
  d_pScope->enqueueToGarbageCollect(this);
310
56828268
}
311
312
291419
ContextNotifyObj::ContextNotifyObj(Context* pContext, bool preNotify) {
313
291419
  if(preNotify) {
314
4
    pContext->addNotifyObjPre(this);
315
  } else {
316
291415
    pContext->addNotifyObjPost(this);
317
  }
318
291419
}
319
320
321
582514
ContextNotifyObj::~ContextNotifyObj() {
322
291257
  if(d_pCNOnext != NULL) {
323
164177
    d_pCNOnext->d_ppCNOprev = d_ppCNOprev;
324
  }
325
291257
  if(d_ppCNOprev != NULL) {
326
291253
    *d_ppCNOprev = d_pCNOnext;
327
  }
328
291257
}
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
109175902
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
209804714
  while (d_pContextObjList != NULL) {
372
103477842
    d_pContextObjList = d_pContextObjList->restoreAndContinue();
373
  }
374
375
2849030
  if (d_garbage) {
376
115920241
    while (!d_garbage->empty()) {
377
56828268
      ContextObj* obj = d_garbage->back();
378
56828268
      d_garbage->pop_back();
379
56828268
      obj->deleteSelf();
380
    }
381
  }
382
2849030
}
383
384
56828268
void Scope::enqueueToGarbageCollect(ContextObj* obj) {
385
56828268
  if (!d_garbage) {
386
2263705
    d_garbage.reset(new std::vector<ContextObj*>);
387
  }
388
56828268
  d_garbage->push_back(obj);
389
56828268
}
390
391
} /* CVC4::context namespace */
392
26685
} /* CVC4 namespace */