Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * Context class and context manager.
11 : : */
12 : :
13 : : #include "cvc5parser_public.h"
14 : :
15 : : #ifndef CVC5__CONTEXT__CONTEXT_H
16 : : #define CVC5__CONTEXT__CONTEXT_H
17 : :
18 : : #include <cstdlib>
19 : : #include <iostream>
20 : : #include <memory>
21 : : #include <typeinfo>
22 : : #include <vector>
23 : :
24 : : #include "base/check.h"
25 : : #include "base/output.h"
26 : : #include "context/context_mm.h"
27 : :
28 : : namespace cvc5::context {
29 : :
30 : : class Context;
31 : : class Scope;
32 : : class ContextObj;
33 : : class ContextNotifyObj;
34 : :
35 : : /** Pretty-printing of Contexts (for debugging) */
36 : : std::ostream& operator<<(std::ostream&, const Context&);
37 : :
38 : : /** Pretty-printing of Scopes (for debugging) */
39 : : std::ostream& operator<<(std::ostream&, const Scope&);
40 : :
41 : : /**
42 : : * A Context encapsulates all of the dynamic state of the system. Its main
43 : : * methods are push() and pop(). A call to push() saves the current state,
44 : : * and a call to pop() restores the state saved by the most recent call to
45 : : * push().
46 : : *
47 : : * Objects which want to participate in this global save and restore
48 : : * mechanism must inherit from ContextObj (see below).
49 : : *
50 : : * For more flexible context-dependent behavior, objects may implement the
51 : : * ContextNotifyObj interface and simply get a notification when a pop has
52 : : * occurred.
53 : : *
54 : : * Context also uses a helper class called Scope which stores information
55 : : * specific to the portion of the Context since the last call to push() (see
56 : : * below).
57 : : *
58 : : * Memory allocation in Contexts is done with the help of the
59 : : * ContextMemoryManager. A copy is stored in each Scope object for quick
60 : : * access.
61 : : */
62 : : class CVC5_EXPORT Context
63 : : {
64 : : /**
65 : : * Pointer to the ContextMemoryManager for this Context.
66 : : */
67 : : ContextMemoryManager* d_pCMM;
68 : :
69 : : /**
70 : : * List of all scopes for this context.
71 : : */
72 : : std::vector<Scope*> d_scopeList;
73 : :
74 : : /**
75 : : * Doubly-linked list of objects to notify before every pop. See
76 : : * ContextNotifyObj for structure of linked list.
77 : : */
78 : : ContextNotifyObj* d_pCNOpre;
79 : :
80 : : /**
81 : : * Doubly-linked list of objects to notify after every pop. See
82 : : * ContextNotifyObj for structure of linked list.
83 : : */
84 : : ContextNotifyObj* d_pCNOpost;
85 : :
86 : : friend std::ostream& operator<<(std::ostream&, const Context&);
87 : :
88 : : // disable copy, assignment
89 : : Context(const Context&) = delete;
90 : : Context& operator=(const Context&) = delete;
91 : :
92 : : public:
93 : : /**
94 : : * A mechanism by which a "scoped" bit of contextual speculation can
95 : : * be applied. One might create a Context::ScopedPush in a function
96 : : * (as a local variable on the stack), then manipulate some
97 : : * context-dependent data structures in some fashion, speculatively.
98 : : * When the ScopedPush goes out of scope and is destructed, the
99 : : * context-dependent data structures will return to their original
100 : : * state.
101 : : *
102 : : * When such speculation occurs in a lexically-scoped manner, like
103 : : * described above, it is FAR preferable to use ScopedPush than to
104 : : * call ->push() and ->pop() on the Context directly. If you do the
105 : : * latter, it's extremely easy to forget to pop() on exceptional
106 : : * exit of the function, or if a short-circuited "early" return is
107 : : * later added to the function, etc. Further, ScopedPush includes
108 : : * an assertion that the Context at the end looks like the Context
109 : : * at the beginning (the topmost Scope pointer should be the same).
110 : : * This assertion is only an approximate check for correct behavior,
111 : : * but should catch egregious mismatches of ->push() and ->pop()
112 : : * while the ScopedPush is being applied---egregious mismatches that
113 : : * could exist, for example, if a Theory does some speculative
114 : : * reasoning but accidently gives control back to some other mechanism
115 : : * which does some speculation which isn't properly scoped inside the
116 : : * first.
117 : : */
118 : : class ScopedPush
119 : : {
120 : : Context* const d_context;
121 : : const Scope* const d_scope;
122 : :
123 : : public:
124 : 2818 : ScopedPush(Context* ctxt)
125 : 2818 : : d_context(ctxt), d_scope(d_context->getTopScope())
126 : : {
127 : 2818 : d_context->push();
128 : 2818 : }
129 : 2818 : ~ScopedPush() noexcept(false)
130 : : {
131 : 2818 : d_context->pop();
132 [ - + ][ - + ]: 2818 : AlwaysAssert(d_context->getTopScope() == d_scope)
[ - - ]
133 : : << "Context::ScopedPush observed an uneven Context (at pop, "
134 : : "top scope doesn't match what it was at the time the "
135 : 0 : "ScopedPush was applied)";
136 : 2818 : }
137 : : }; /* Context::ScopedPush */
138 : :
139 : : /**
140 : : * Constructor: create ContextMemoryManager and initial Scope
141 : : */
142 : : Context();
143 : :
144 : : /**
145 : : * Destructor: pop all scopes, delete ContextMemoryManager
146 : : */
147 : : ~Context();
148 : :
149 : : /**
150 : : * Return the current (top) scope
151 : : */
152 : 1861571385 : Scope* getTopScope() const { return d_scopeList.back(); }
153 : :
154 : : /**
155 : : * Return the initial (bottom) scope
156 : : */
157 : 268756335 : Scope* getBottomScope() const { return d_scopeList[0]; }
158 : :
159 : : /**
160 : : * Return the current Scope level.
161 : : */
162 : : uint32_t getLevel() const;
163 : :
164 : : /**
165 : : * Return the ContextMemoryManager associated with the context.
166 : : */
167 : 0 : ContextMemoryManager* getCMM() { return d_pCMM; }
168 : :
169 : : /**
170 : : * Save the current state, create a new Scope
171 : : */
172 : : void push();
173 : :
174 : : /**
175 : : * Restore the previous state, delete the top Scope
176 : : */
177 : : void pop();
178 : :
179 : : /**
180 : : * Pop all the way back to given level
181 : : */
182 : : void popto(uint32_t toLevel);
183 : :
184 : : /**
185 : : * Add pCNO to the list of objects notified before every pop
186 : : */
187 : : void addNotifyObjPre(ContextNotifyObj* pCNO);
188 : :
189 : : /**
190 : : * Add pCNO to the list of objects notified after every pop
191 : : */
192 : : void addNotifyObjPost(ContextNotifyObj* pCNO);
193 : :
194 : : }; /* class Context */
195 : :
196 : : /**
197 : : * A UserContext is different from a Context only because it's used for
198 : : * different purposes---so separating the two types gives type errors where
199 : : * appropriate.
200 : : */
201 : : class UserContext : public Context
202 : : {
203 : : private:
204 : : // disable copy, assignment
205 : : UserContext(const UserContext&) = delete;
206 : : UserContext& operator=(const UserContext&) = delete;
207 : :
208 : : public:
209 : 75684 : UserContext() {}
210 : : }; /* class UserContext */
211 : :
212 : : /**
213 : : * Conceptually, a Scope encapsulates that portion of the context that
214 : : * changes after a call to push() and must be undone on a subsequent call to
215 : : * pop(). In particular, each call to push() creates a new Scope object .
216 : : * This new Scope object becomes the top scope and it points (via the
217 : : * d_pScopePrev member) to the previous top Scope. Each call to pop()
218 : : * deletes the current top scope and restores the previous one. The main
219 : : * purpose of a Scope is to maintain a linked list of ContexObj objects which
220 : : * change while the Scope is the top scope and which must be restored when
221 : : * the Scope is deleted.
222 : : *
223 : : * A Scope is also associated with a ContextMemoryManager. All memory
224 : : * allocated by the Scope is allocated in a single region using the
225 : : * ContextMemoryManager and released all at once when the Scope is popped.
226 : : */
227 : : class Scope
228 : : {
229 : : /**
230 : : * Context that created this Scope
231 : : */
232 : : Context* d_pContext;
233 : :
234 : : /**
235 : : * Memory manager for this Scope. Same as in Context, but stored here too
236 : : * for faster access by ContextObj objects.
237 : : */
238 : : ContextMemoryManager* d_pCMM;
239 : :
240 : : /**
241 : : * Scope level (total number of outstanding push() calls when this Scope was
242 : : * created).
243 : : */
244 : : uint32_t d_level;
245 : :
246 : : /**
247 : : * Linked list of objects which changed in this scope,
248 : : * and thus need to be restored when the scope is deleted.
249 : : */
250 : : ContextObj* d_pContextObjList;
251 : :
252 : : /**
253 : : * A list of ContextObj to be garbage collected before the destruction of this
254 : : * scope. deleteSelf() will be called on each element during ~Scope().
255 : : *
256 : : * This is either nullptr or list owned by this scope.
257 : : */
258 : : std::vector<ContextObj*> d_garbage;
259 : :
260 : : friend std::ostream& operator<<(std::ostream&, const Scope&);
261 : :
262 : : public:
263 : : /**
264 : : * Constructor: Create a new Scope; set the level and the previous Scope
265 : : * if any.
266 : : */
267 : 36601045 : Scope(Context* pContext, ContextMemoryManager* pCMM, uint32_t level)
268 : 36601045 : : d_pContext(pContext),
269 : 36601045 : d_pCMM(pCMM),
270 : 36601045 : d_level(level),
271 : 36601045 : d_pContextObjList(nullptr),
272 : 36601045 : d_garbage()
273 : : {
274 : 36601045 : }
275 : :
276 : : /**
277 : : * Destructor: Clears out all of the garbage and restore all of the objects
278 : : * in ContextObjList.
279 : : */
280 : : ~Scope();
281 : :
282 : : /**
283 : : * Get the Context for this Scope
284 : : */
285 : 321095734 : Context* getContext() const { return d_pContext; }
286 : :
287 : : /**
288 : : * Get the ContextMemoryManager for this Scope
289 : : */
290 : 321095734 : ContextMemoryManager* getCMM() const { return d_pCMM; }
291 : :
292 : : /**
293 : : * Get the level of the current Scope
294 : : */
295 : 0 : uint32_t getLevel() const { return d_level; }
296 : :
297 : : /**
298 : : * Return true iff this Scope is the current top Scope
299 : : */
300 : 1540470012 : bool isCurrent() const { return this == d_pContext->getTopScope(); }
301 : :
302 : : /**
303 : : * When a ContextObj object is modified for the first time in this
304 : : * Scope, it should call this method to add itself to the list of
305 : : * objects that will need to be restored. Defined inline below.
306 : : */
307 : : void addToChain(ContextObj* pContextObj);
308 : :
309 : : /**
310 : : * Overload operator new for use with ContextMemoryManager to allow
311 : : * creation of new Scope objects in the current memory region.
312 : : */
313 : 36601045 : static void* operator new(size_t size, ContextMemoryManager* pCMM)
314 : : {
315 : 36601045 : return pCMM->newData(size);
316 : : }
317 : :
318 : : /**
319 : : * Enqueues a ContextObj to be garbage collected via a call to deleteSelf()
320 : : * during the destruction of this scope.
321 : : */
322 : : void enqueueToGarbageCollect(ContextObj* obj);
323 : :
324 : : /**
325 : : * Overload operator delete for Scope objects allocated using
326 : : * ContextMemoryManager. No need to do anything because memory is
327 : : * freed automatically when the ContextMemoryManager pop() method is
328 : : * called. Include both placement and standard delete for
329 : : * completeness.
330 : : */
331 : : static void operator delete(CVC5_UNUSED void* pMem,
332 : : CVC5_UNUSED ContextMemoryManager* pCMM)
333 : : {
334 : : }
335 : 20063349 : static void operator delete(CVC5_UNUSED void* pMem) {}
336 : :
337 : : // FIXME: //! Check for memory leaks
338 : : // void check();
339 : :
340 : : }; /* class Scope */
341 : :
342 : : /**
343 : : * This is an abstract base class from which all objects that are
344 : : * context-dependent should inherit. For any data structure that you
345 : : * want to have be automatically backtracked, do the following:
346 : : *
347 : : * 1. Create a class for the data structure that inherits from ContextObj
348 : : *
349 : : * 2. Implement save()
350 : : * The role of save() is to create a new ContexObj object that contains
351 : : * enough information to restore the object to its current state, even if
352 : : * it gets changed later. Note that save should call the (default)
353 : : * ContextObj Copy Constructor to copy the information in the base class.
354 : : * It is recommended that any memory allocated by save() should be done
355 : : * through the ContextMemoryManager. This way, it does not need to be
356 : : * explicitly freed when restore is called. However, it is only required
357 : : * that the ContextObj itself be allocated using the
358 : : * ContextMemoryManager. If other memory is allocated not using the
359 : : * ContextMemoryManager, it should be freed when restore() is called. In
360 : : * fact, any clean-up work on a saved object must be done by restore().
361 : : * This is because the destructor is never called explicitly on saved
362 : : * objects.
363 : : *
364 : : * 3. Implement restore()
365 : : * The role of restore() is, given the ContextObj returned by a previous
366 : : * call to save(), to restore the current object to the state it was in
367 : : * when save() was called. Note that the implementation of restore does
368 : : * *not* need to worry about restoring the base class data. This is done
369 : : * automatically. Ideally, restore() should not have to free any memory
370 : : * as any memory allocated by save() should have been done using the
371 : : * ContextMemoryManager (see item 2 above).
372 : : *
373 : : * 4. In the subclass implementation, any time the state is about to be
374 : : * changed, first call makeCurrent().
375 : : *
376 : : * 5. In the subclass implementation, the destructor should call destroy(),
377 : : * which repeatedly calls restore() until the object is restored to context
378 : : * level 0. Note, however, that if there is additional cleanup required at
379 : : * level 0, destroy() does not do this. It has to be implemented in the
380 : : * destructor of the subclass. The reason the destroy() functionality
381 : : * cannot be in the ContextObj destructor is that it needs to call the
382 : : * subclass-specific restore() method in order to properly clean up saved
383 : : * copies.
384 : : *
385 : : * GOTCHAS WHEN ALLOCATING CONTEXTUAL OBJECTS WITH NON-STANDARD ALLOCATORS
386 : : *
387 : : * Be careful if you intend to allocate ContextObj in (for example)
388 : : * ContextMemoryManager memory. ContextMemoryManager doesn't call the
389 : : * destructors of contained objects, which means the objects aren't
390 : : * properly unregistered from the Context (as in point #5, above).
391 : : * This can be remedied by allocating the ContextObj in the "top
392 : : * scope" rather than the "bottom scope" (which is what the
393 : : * "allocatedInCMM" flag to the special constructor in ContextObj
394 : : * does).
395 : : *
396 : : * But why allocate in CMM if it's so complicated? There's a big
397 : : * advantage: you don't have to track the lifetime of the ContextObj.
398 : : * The object simply ceases to exist when the Context is popped. Thus
399 : : * you can create an object in context memory, and if you stow
400 : : * pointers to it only in context memory as well, all is cleaned up
401 : : * for you when the scope pops. Here's a list of gotchas:
402 : : *
403 : : * 1. For data structures intended solely to be allocated in context
404 : : * memory, privately declare (but don't define) an operator
405 : : * new(size_t) and destructor (as currently in the Link class, in
406 : : * src/theory/uf/ecdata.h).
407 : : *
408 : : * 2. For data structures that may or may not be allocated in context
409 : : * memory, and are designed to be that way (esp. if they contain
410 : : * ContextObj instances), they should be heavily documented --
411 : : * especially the destructor, since it _may_or_may_not_be_called_.
412 : : *
413 : : * 3. There's also an issue for generic code -- some class Foo<T>
414 : : * might be allocated in context memory, and that might normally be
415 : : * fine, but if T is a ContextObj this requires certain care.
416 : : *
417 : : * 4. Note that certain care is required for ContextObj inside of data
418 : : * structures. If the (enclosing) data structure can be allocated
419 : : * in CMM, that means the (enclosed) ContextObj can be, even if it
420 : : * was not designed to be allocated in that way. In many
421 : : * instances, it may be required that data structures enclosing
422 : : * ContextObj be parameterized with a similar "bool allocatedInCMM"
423 : : * argument as the special constructor in this class (and pass it
424 : : * on to all ContextObj instances).
425 : : */
426 : : class CVC5_EXPORT ContextObj
427 : : {
428 : : /**
429 : : * Pointer to Scope in which this object was last modified.
430 : : */
431 : : Scope* d_pScope;
432 : :
433 : : /**
434 : : * Pointer to most recent version of same ContextObj in a previous Scope
435 : : */
436 : : ContextObj* d_pContextObjRestore;
437 : :
438 : : /**
439 : : * Next link in ContextObjList list maintained by Scope class.
440 : : */
441 : : ContextObj* d_pContextObjNext;
442 : :
443 : : /**
444 : : * Previous link in ContextObjList list maintained by Scope class. We use
445 : : * double-indirection here to make element deletion easy.
446 : : */
447 : : ContextObj** d_ppContextObjPrev;
448 : :
449 : : /**
450 : : * Helper method for makeCurrent (see below). Separated out to allow common
451 : : * case to be inlined without making a function call. It calls save() and
452 : : * does the necessary bookkeeping to ensure that object can be restored to
453 : : * its current state when restore is called.
454 : : */
455 : : void update();
456 : :
457 : : // The rest of the private methods are for the benefit of the Scope. We make
458 : : // Scope our friend so it is the only one that can use them.
459 : :
460 : : friend class Scope;
461 : :
462 : : friend std::ostream& operator<<(std::ostream&, const Scope&);
463 : :
464 : : /**
465 : : * Return reference to next link in ContextObjList. Used by
466 : : * Scope::addToChain method.
467 : : */
468 : 4152676152 : ContextObj*& next() { return d_pContextObjNext; }
469 : :
470 : : /**
471 : : * Return reference to prev link in ContextObjList. Used by
472 : : * Scope::addToChain method.
473 : : */
474 : 3499526503 : ContextObj**& prev() { return d_ppContextObjPrev; }
475 : :
476 : : /**
477 : : * This method is called by Scope during a pop: it does the necessary work to
478 : : * restore the object from its saved copy and then returns the next object in
479 : : * the list that needs to be restored.
480 : : */
481 : : ContextObj* restoreAndContinue();
482 : :
483 : : protected:
484 : : /**
485 : : * This is a method that must be implemented by all classes inheriting from
486 : : * ContextObj. See the comment before the class declaration.
487 : : */
488 : : virtual ContextObj* save(ContextMemoryManager* pCMM) = 0;
489 : :
490 : : /**
491 : : * This is a method that must be implemented by all classes inheriting from
492 : : * ContextObj. See the comment before the class declaration.
493 : : */
494 : : virtual void restore(ContextObj* pContextObjRestore) = 0;
495 : :
496 : : /**
497 : : * This method checks if the object has been modified in this Scope
498 : : * yet. If not, it calls update().
499 : : */
500 : : inline void makeCurrent();
501 : :
502 : : /**
503 : : * Just calls update(), but given a different name for the derived
504 : : * class-facing interface. This is a "forced" makeCurrent(), useful
505 : : * for ContextObjs allocated in CMM that need a special "bottom"
506 : : * case when they disappear out of existence (kind of a destructor).
507 : : * See CDOhash_map (in cdhashmap.h) for an example.
508 : : */
509 : : inline void makeSaveRestorePoint();
510 : :
511 : : /**
512 : : * Should be called from sub-class destructor: calls restore until restored
513 : : * to initial version (version at context level 0). Also removes object from
514 : : * all Scope lists. Note that this doesn't actually free the memory
515 : : * allocated by the ContextMemoryManager for this object. This isn't done
516 : : * until the corresponding Scope is popped.
517 : : */
518 : : void destroy();
519 : :
520 : : /////
521 : : //
522 : : // These next four accessors return properties of the Scope to
523 : : // derived classes without giving them the Scope object directly.
524 : : //
525 : : /////
526 : :
527 : : /**
528 : : * Get the Context with which this ContextObj was created. This is
529 : : * part of the protected interface, intended for derived classes to
530 : : * use if necessary.
531 : : */
532 : 0 : Context* getContext() const { return d_pScope->getContext(); }
533 : :
534 : : /**
535 : : * Get the ContextMemoryManager with which this ContextObj was
536 : : * created. This is part of the protected interface, intended for
537 : : * derived classes to use if necessary. If a ContextObj-derived
538 : : * class needs to allocate memory somewhere other than the save()
539 : : * member function (where it is explicitly given a
540 : : * ContextMemoryManager), it can use this accessor to get the memory
541 : : * manager.
542 : : */
543 : : ContextMemoryManager* getCMM() const { return d_pScope->getCMM(); }
544 : :
545 : : /**
546 : : * Get the level associated to this ContextObj. Useful if a
547 : : * ContextObj-derived class needs to compare the level of its last
548 : : * update with another ContextObj.
549 : : */
550 : 0 : uint32_t getLevel() const { return d_pScope->getLevel(); }
551 : :
552 : : /**
553 : : * Returns true if the object is "current"-- that is, updated in the
554 : : * topmost contextual scope. Useful if a ContextObj-derived class
555 : : * needs to determine if it has been modified in the current scope.
556 : : * Note that it is always safe to call makeCurrent() without first
557 : : * checking if the object is current, so this function need not be
558 : : * used under normal circumstances.
559 : : */
560 : : bool isCurrent() const { return d_pScope->isCurrent(); }
561 : :
562 : : public:
563 : : /**
564 : : * Disable delete: objects allocated with new(ContextMemorymanager) should
565 : : * never be deleted. Objects allocated with new(bool) should be deleted by
566 : : * calling deleteSelf().
567 : : */
568 : 0 : static void operator delete(CVC5_UNUSED void* pMem)
569 : : {
570 : 0 : AlwaysAssert(false) << "It is not allowed to delete a ContextObj this way!";
571 : : }
572 : :
573 : : /**
574 : : * operator new using ContextMemoryManager (common case used by
575 : : * subclasses during save()). No delete is required for memory
576 : : * allocated this way, since it is automatically released when the
577 : : * context is popped. Also note that allocations using this
578 : : * operator never have their destructor called, so any clean-up has
579 : : * to be done using the restore method.
580 : : */
581 : 321095734 : static void* operator new(size_t size, ContextMemoryManager* pCMM)
582 : : {
583 : 321095734 : return pCMM->newData(size);
584 : : }
585 : :
586 : : /**
587 : : * Corresponding placement delete. Note that this is provided just
588 : : * to satisfy the requirement that a placement delete should be
589 : : * provided for every placement new. It would only be called if a
590 : : * ContextObj constructor throws an exception after a successful
591 : : * call to the above new operator.
592 : : */
593 : 0 : static void operator delete(CVC5_UNUSED void* pMem,
594 : : CVC5_UNUSED ContextMemoryManager* pCMM)
595 : : {
596 : 0 : }
597 : :
598 : : /**
599 : : * Create a new ContextObj. The initial scope is set to the bottom
600 : : * scope of the Context. Note that in the common case, the copy
601 : : * constructor is called to create new ContextObj objects. The
602 : : * default copy constructor does the right thing, so we do not
603 : : * explicitly define it.
604 : : */
605 : : ContextObj(Context* context);
606 : :
607 : : /**
608 : : * Destructor does nothing: subclass must explicitly call destroy() instead.
609 : : */
610 : 268486170 : virtual ~ContextObj() {}
611 : :
612 : : /**
613 : : * If you want to allocate a ContextObj object on the heap, use this
614 : : * special new operator. To free this memory, instead of
615 : : * "delete p", use "p->deleteSelf()".
616 : : */
617 : 200277155 : static void* operator new(size_t size, bool) { return ::operator new(size); }
618 : :
619 : : /**
620 : : * Corresponding placement delete. Note that this is provided for
621 : : * the compiler in case the ContextObj constructor throws an
622 : : * exception. The client can't call it.
623 : : */
624 : 0 : static void operator delete(void* pMem, bool) { ::operator delete(pMem); }
625 : :
626 : : /**
627 : : * Use this instead of delete to delete memory allocated using the special
628 : : * new function provided above that takes a bool argument. Do not call this
629 : : * function on memory allocated using the new that takes a
630 : : * ContextMemoryManager as an argument.
631 : : */
632 : 200269585 : void deleteSelf()
633 : : {
634 : 200269585 : this->~ContextObj();
635 : 200269585 : ::operator delete(this);
636 : 200269585 : }
637 : :
638 : : /**
639 : : * Use this to enqueue calling deleteSelf() at the time of the destruction of
640 : : * the enclosing Scope.
641 : : */
642 : : void enqueueToGarbageCollect();
643 : :
644 : : }; /* class ContextObj */
645 : :
646 : : /**
647 : : * For more flexible context-dependent behavior than that provided by
648 : : * ContextObj, objects may implement the ContextNotifyObj interface
649 : : * and simply get a notification when a pop has occurred. See
650 : : * Context class for how to register a ContextNotifyObj with the
651 : : * Context (you can choose to have notification come before or after
652 : : * the ContextObj objects have been restored).
653 : : */
654 : : class ContextNotifyObj
655 : : {
656 : : /**
657 : : * Context is our friend so that when the Context is deleted, any
658 : : * remaining ContextNotifyObj can be removed from the Context list.
659 : : */
660 : : friend class Context;
661 : :
662 : : /**
663 : : * Pointer to next ContextNotifyObject in this List
664 : : */
665 : : ContextNotifyObj* d_pCNOnext;
666 : :
667 : : /**
668 : : * Pointer to previous ContextNotifyObject in this list
669 : : */
670 : : ContextNotifyObj** d_ppCNOprev;
671 : :
672 : : /**
673 : : * Return reference to next link in ContextNotifyObj list. Used by
674 : : * Context::addNotifyObj methods.
675 : : */
676 : 3170467 : ContextNotifyObj*& next() { return d_pCNOnext; }
677 : :
678 : : /**
679 : : * Return reference to prev link in ContextNotifyObj list. Used by
680 : : * Context::addNotifyObj methods.
681 : : */
682 : 3170467 : ContextNotifyObj**& prev() { return d_ppCNOprev; }
683 : :
684 : : protected:
685 : : /**
686 : : * This is the method called to notify the object of a pop. It must be
687 : : * implemented by the subclass. It is protected since context is out
688 : : * friend.
689 : : */
690 : : virtual void contextNotifyPop() = 0;
691 : :
692 : : public:
693 : : /**
694 : : * Constructor for ContextNotifyObj. Parameters are the context to
695 : : * which this notify object will be added, and a flag which, if
696 : : * true, tells the context to notify this object *before* the
697 : : * ContextObj objects are restored. Otherwise, the context notifies
698 : : * the object after the ContextObj objects are restored. The
699 : : * default is for notification after.
700 : : */
701 : : ContextNotifyObj(Context* pContext, bool preNotify = false);
702 : :
703 : : /**
704 : : * Destructor: removes object from list
705 : : */
706 : : virtual ~ContextNotifyObj();
707 : :
708 : : }; /* class ContextNotifyObj */
709 : :
710 : 1540470012 : inline void ContextObj::makeCurrent()
711 : : {
712 [ + + ]: 1540470012 : if (!(d_pScope->isCurrent()))
713 : : {
714 : 321095734 : update();
715 : : }
716 : 1540470012 : }
717 : :
718 : : inline void ContextObj::makeSaveRestorePoint() { update(); }
719 : :
720 : 589852067 : inline void Scope::addToChain(ContextObj* pContextObj)
721 : : {
722 [ + + ]: 589852067 : if (d_pContextObjList != nullptr)
723 : : {
724 : 562260719 : d_pContextObjList->prev() = &pContextObj->next();
725 : : }
726 : :
727 : 589852067 : pContextObj->next() = d_pContextObjList;
728 : 589852067 : pContextObj->prev() = &d_pContextObjList;
729 : 589852067 : d_pContextObjList = pContextObj;
730 : 589852067 : }
731 : :
732 : : } // namespace cvc5::context
733 : :
734 : : #endif /* CVC5__CONTEXT__CONTEXT_H */
|
