Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Clark Barrett, Morgan Deters, Tim King
       4                 :            :  *
       5                 :            :  * This file is part of the cvc5 project.
       6                 :            :  *
       7                 :            :  * Copyright (c) 2009-2025 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.
      11                 :            :  * ****************************************************************************
      12                 :            :  *
      13                 :            :  * Implementation of base context operations.
      14                 :            :  */
      15                 :            : 
      16                 :            : #include <iostream>
      17                 :            : #include <string>
      18                 :            : #include <vector>
      19                 :            : 
      20                 :            : #include "base/check.h"
      21                 :            : #include "context/context.h"
      22                 :            : 
      23                 :            : namespace cvc5::context {
      24                 :            : 
      25                 :   15253700 : Context::Context() : d_pCNOpre(NULL), d_pCNOpost(NULL) {
      26                 :            :   // Create new memory manager
      27                 :   15253700 :   d_pCMM = new ContextMemoryManager();
      28                 :            : 
      29                 :            :   // Create initial Scope
      30                 :   15253700 :   d_scopeList.push_back(new(d_pCMM) Scope(this, d_pCMM, 0));
      31                 :   15253700 : }
      32                 :            : 
      33                 :            : 
      34                 :   15231600 : Context::~Context() {
      35                 :            :   // Delete all Scopes
      36                 :   15231600 :   popto(0);
      37                 :            : 
      38                 :            :   // Delete the memory manager
      39         [ +  - ]:   15231600 :   delete d_pCMM;
      40                 :            : 
      41                 :            :   // Clear ContextNotifyObj lists so there are no dangling pointers
      42                 :            :   ContextNotifyObj* pCNO;
      43         [ +  + ]:   15231600 :   while(d_pCNOpre != NULL) {
      44                 :          1 :     pCNO = d_pCNOpre;
      45                 :          1 :     pCNO->d_ppCNOprev = NULL;
      46                 :          1 :     d_pCNOpre = pCNO->d_pCNOnext;
      47                 :          1 :     pCNO->d_pCNOnext = NULL;
      48                 :            :   }
      49         [ +  + ]:   15231600 :   while(d_pCNOpost != NULL) {
      50                 :          1 :     pCNO = d_pCNOpost;
      51                 :          1 :     pCNO->d_ppCNOprev = NULL;
      52                 :          1 :     d_pCNOpost = pCNO->d_pCNOnext;
      53                 :          1 :     pCNO->d_pCNOnext = NULL;
      54                 :            :   }
      55                 :   15231600 : }
      56                 :            : 
      57                 :  114759000 : uint32_t Context::getLevel() const
      58                 :            : {
      59 [ -  + ][ -  + ]:  114759000 :   Assert(d_scopeList.size() > 0);
                 [ -  - ]
      60                 :  114759000 :   return d_scopeList.size() - 1;
      61                 :            : }
      62                 :            : 
      63                 :   19008400 : void Context::push() {
      64                 :   38016900 :   Trace("pushpop") << std::string(2 * getLevel(), ' ') << "Push [to "
      65         [ -  + ]:   19008400 :                    << getLevel() + 1 << "] { " << this << std::endl;
      66                 :            : 
      67                 :            :   // Create a new memory region
      68                 :   19008400 :   d_pCMM->push();
      69                 :            : 
      70                 :            :   // Create a new top Scope
      71                 :   19008400 :   d_scopeList.push_back(new(d_pCMM) Scope(this, d_pCMM, getLevel()+1));
      72                 :   19008400 : }
      73                 :            : 
      74                 :            : 
      75                 :   19007100 : void Context::pop() {
      76 [ -  + ][ -  + ]:   19007100 :   Assert(getLevel() > 0) << "Cannot pop below level 0";
                 [ -  - ]
      77                 :            : 
      78                 :            :   // Notify the (pre-pop) ContextNotifyObj objects
      79                 :   19007100 :   ContextNotifyObj* pCNO = d_pCNOpre;
      80         [ +  + ]:   19007100 :   while(pCNO != NULL) {
      81                 :            :     // pre-store the "next" pointer in case pCNO deletes itself on notify()
      82                 :          5 :     ContextNotifyObj* next = pCNO->d_pCNOnext;
      83                 :          5 :     pCNO->contextNotifyPop();
      84                 :          5 :     pCNO = next;
      85                 :            :   }
      86                 :            : 
      87                 :            :   // Grab the top Scope
      88                 :   19007100 :   Scope* pScope = d_scopeList.back();
      89                 :            : 
      90                 :            :   // Restore the previous Scope
      91                 :   19007100 :   d_scopeList.pop_back();
      92                 :            : 
      93                 :            :   // Restore all objects in the top Scope
      94         [ +  - ]:   19007100 :   delete pScope;
      95                 :            : 
      96                 :            :   // Pop the memory region
      97                 :   19007100 :   d_pCMM->pop();
      98                 :            : 
      99                 :            :   // Notify the (post-pop) ContextNotifyObj objects
     100                 :   19007100 :   pCNO = d_pCNOpost;
     101         [ +  + ]:  159058000 :   while(pCNO != NULL) {
     102                 :            :     // pre-store the "next" pointer in case pCNO deletes itself on notify()
     103                 :  140051000 :     ContextNotifyObj* next = pCNO->d_pCNOnext;
     104                 :  140051000 :     pCNO->contextNotifyPop();
     105                 :  140051000 :     pCNO = next;
     106                 :            :   }
     107                 :            : 
     108                 :   38014200 :   Trace("pushpop") << std::string(2 * getLevel(), ' ') << "} Pop [to "
     109         [ -  + ]:   19007100 :                    << getLevel() << "] " << this << std::endl;
     110                 :   19007100 : }
     111                 :            : 
     112                 :   16090600 : void Context::popto(uint32_t toLevel)
     113                 :            : {
     114                 :            :   // Pop scopes until there are none left or toLevel is reached
     115         [ +  + ]:   16090600 :   while (toLevel < getLevel()) pop();
     116                 :   15639400 : }
     117                 :            : 
     118                 :          3 : void Context::addNotifyObjPre(ContextNotifyObj* pCNO) {
     119                 :            :   // Insert pCNO at *front* of list
     120         [ +  + ]:          3 :   if(d_pCNOpre != NULL)
     121                 :          1 :     d_pCNOpre->prev() = &(pCNO->next());
     122                 :          3 :   pCNO->next() = d_pCNOpre;
     123                 :          3 :   pCNO->prev() = &d_pCNOpre;
     124                 :          3 :   d_pCNOpre = pCNO;
     125                 :          3 : }
     126                 :            : 
     127                 :            : 
     128                 :    1723380 : void Context::addNotifyObjPost(ContextNotifyObj* pCNO) {
     129                 :            :   // Insert pCNO at *front* of list
     130         [ +  + ]:    1723380 :   if(d_pCNOpost != NULL)
     131                 :    1408420 :     d_pCNOpost->prev() = &(pCNO->next());
     132                 :    1723380 :   pCNO->next() = d_pCNOpost;
     133                 :    1723380 :   pCNO->prev() = &d_pCNOpost;
     134                 :    1723380 :   d_pCNOpost = pCNO;
     135                 :    1723380 : }
     136                 :            : 
     137                 :  304782000 : void ContextObj::update()
     138                 :            : {
     139                 :            :   // Call save() to save the information in the current object
     140                 :  304782000 :   ContextObj* pContextObjSaved = save(d_pScope->getCMM());
     141                 :            : 
     142                 :            :   // Check that base class data was saved
     143 [ +  - ][ +  - ]:  609564000 :   Assert((pContextObjSaved->d_pContextObjNext == d_pContextObjNext
         [ +  - ][ +  - ]
         [ -  + ][ -  - ]
     144                 :            :           && pContextObjSaved->d_ppContextObjPrev == d_ppContextObjPrev
     145                 :            :           && pContextObjSaved->d_pContextObjRestore == d_pContextObjRestore
     146                 :            :           && pContextObjSaved->d_pScope == d_pScope))
     147                 :          0 :       << "save() did not properly copy information in base class";
     148                 :            : 
     149                 :            :   // Link the "saved" object in place of this ContextObj in the scope
     150                 :            :   // we're moving it FROM.
     151         [ +  + ]:  304782000 :   if(next() != NULL) {
     152                 :  297536000 :     next()->prev() = &pContextObjSaved->next();
     153                 :            :   }
     154                 :  304782000 :   *prev() = pContextObjSaved;
     155                 :            : 
     156                 :            :   // Update Scope pointer to current top Scope
     157                 :  304782000 :   d_pScope = d_pScope->getContext()->getTopScope();
     158                 :            : 
     159                 :            :   // Store the saved copy in the restore pointer
     160                 :  304782000 :   d_pContextObjRestore = pContextObjSaved;
     161                 :            : 
     162                 :            :   // Insert object into the list of objects that need to be restored when this
     163                 :            :   // Scope is popped.
     164                 :  304782000 :   d_pScope->addToChain(this);
     165                 :  304782000 : }
     166                 :            : 
     167                 :  304766000 : ContextObj* ContextObj::restoreAndContinue()
     168                 :            : {
     169                 :            :   // Variable to hold next object in list
     170                 :            :   ContextObj* pContextObjNext;
     171                 :            : 
     172                 :            :   // Check the restore pointer.  If NULL, this must be the bottom Scope
     173         [ -  + ]:  304766000 :   if(d_pContextObjRestore == NULL) {
     174                 :            :     // might not be bottom scope, since objects allocated in context
     175                 :            :     // memory don't get linked to scope 0
     176                 :            :     //
     177                 :            :     // Assert(d_pScope == d_pScope->getContext()->getBottomScope()) <<
     178                 :            :     //        "Expected bottom scope";
     179                 :            : 
     180         [ -  - ]:          0 :     Trace("context") << "NULL restore object! " << this << std::endl;
     181                 :          0 :     pContextObjNext = d_pContextObjNext;
     182                 :          0 :     d_pScope = nullptr;
     183                 :            : 
     184                 :            :     // Nothing else to do
     185                 :            :   } else {
     186                 :            :     // Call restore to update the subclass data
     187                 :  304766000 :     restore(d_pContextObjRestore);
     188                 :            : 
     189                 :            :     // Remember the next object in the list
     190                 :  304766000 :     pContextObjNext = d_pContextObjNext;
     191                 :            : 
     192                 :            :     // Restore the base class data
     193                 :  304766000 :     d_pScope = d_pContextObjRestore->d_pScope;
     194                 :  304766000 :     next() = d_pContextObjRestore->d_pContextObjNext;
     195                 :  304766000 :     prev() = d_pContextObjRestore->d_ppContextObjPrev;
     196                 :  304766000 :     d_pContextObjRestore = d_pContextObjRestore->d_pContextObjRestore;
     197                 :            : 
     198                 :            :     // Re-link this ContextObj to the list in this scope
     199         [ +  + ]:  304766000 :     if(next() != NULL) {
     200                 :  297519000 :       next()->prev() = &next();
     201                 :            :     }
     202                 :  304766000 :     *prev() = this;
     203                 :            :   }
     204                 :            : 
     205                 :            :   // Return the next object in the list
     206                 :  304766000 :   return pContextObjNext;
     207                 :            : }
     208                 :            : 
     209                 :  255174000 : void ContextObj::destroy()
     210                 :            : {
     211                 :            :   /* The object to destroy must be valid, i.e., its current state must belong
     212                 :            :    * to a scope. We remove the object and its previous versions from their
     213                 :            :    * respective scopes below. If this assertion is failing, you may have
     214                 :            :    * created an object at a non-zero level and let it outlive the destruction
     215                 :            :    * of that level. */
     216 [ -  + ][ -  + ]:  255174000 :   Assert(d_pScope != nullptr);
                 [ -  - ]
     217                 :            :   /* Context can be big and complicated, so we only want to process this output
     218                 :            :    * if we're really going to use it. (Same goes below.) */
     219         [ +  - ]:  510348000 :   Trace("context") << "before destroy " << this << " (level " << getLevel()
     220                 :  255174000 :                    << "):" << std::endl << *getContext() << std::endl;
     221                 :            : 
     222                 :            :   for (;;)
     223                 :            :   {
     224                 :            :     // If valgrind reports invalid writes on the next few lines,
     225                 :            :     // here's a hint: make sure all classes derived from ContextObj in
     226                 :            :     // the system properly call destroy() in their destructors.
     227                 :            :     // That's needed to maintain this linked list properly.
     228         [ +  + ]:  256453000 :     if (next() != nullptr)
     229                 :            :     {
     230                 :  232250000 :       next()->prev() = prev();
     231                 :            :     }
     232                 :  256453000 :     *prev() = next();
     233         [ +  + ]:  256453000 :     if (d_pContextObjRestore == nullptr)
     234                 :            :     {
     235                 :  255174000 :       break;
     236                 :            :     }
     237                 :    1278710 :     restoreAndContinue();
     238                 :            :   }
     239         [ +  - ]:  510348000 :   Trace("context") << "after destroy " << this << ":" << std::endl
     240                 :  255174000 :                    << *getContext() << std::endl;
     241                 :  255174000 : }
     242                 :            : 
     243                 :            : 
     244                 :  255444000 : ContextObj::ContextObj(Context* pContext) :
     245                 :            :   d_pScope(NULL),
     246                 :            :   d_pContextObjRestore(NULL),
     247                 :            :   d_pContextObjNext(NULL),
     248                 :  255444000 :   d_ppContextObjPrev(NULL) {
     249 [ -  + ][ -  + ]:  255444000 :   Assert(pContext != NULL) << "NULL context pointer";
                 [ -  - ]
     250                 :            : 
     251         [ +  - ]:  255444000 :   Trace("context") << "create new ContextObj(" << this << " inCMM=false)" << std::endl;
     252                 :  255444000 :   d_pScope = pContext->getBottomScope();
     253                 :  255444000 :   d_pScope->addToChain(this);
     254                 :  255444000 : }
     255                 :            : 
     256                 :  129271000 : void ContextObj::enqueueToGarbageCollect() {
     257 [ -  + ][ -  + ]:  129271000 :   Assert(d_pScope != NULL);
                 [ -  - ]
     258                 :  129271000 :   d_pScope->enqueueToGarbageCollect(this);
     259                 :  129271000 : }
     260                 :            : 
     261                 :    1723380 : ContextNotifyObj::ContextNotifyObj(Context* pContext, bool preNotify) {
     262         [ +  + ]:    1723380 :   if(preNotify) {
     263                 :          3 :     pContext->addNotifyObjPre(this);
     264                 :            :   } else {
     265                 :    1723380 :     pContext->addNotifyObjPost(this);
     266                 :            :   }
     267                 :    1723380 : }
     268                 :            : 
     269                 :            : 
     270                 :    3398340 : ContextNotifyObj::~ContextNotifyObj() {
     271         [ +  + ]:    1699170 :   if(d_pCNOnext != NULL) {
     272                 :    1197240 :     d_pCNOnext->d_ppCNOprev = d_ppCNOprev;
     273                 :            :   }
     274         [ +  + ]:    1699170 :   if(d_ppCNOprev != NULL) {
     275                 :    1699170 :     *d_ppCNOprev = d_pCNOnext;
     276                 :            :   }
     277                 :    1699170 : }
     278                 :            : 
     279                 :          0 : std::ostream& operator<<(std::ostream& out, const Context& context)
     280                 :            : {
     281                 :          0 :   static const std::string separator(79, '-');
     282                 :            : 
     283                 :          0 :   uint32_t level = context.d_scopeList.size() - 1;
     284                 :            :   typedef std::vector<Scope*>::const_reverse_iterator const_reverse_iterator;
     285                 :          0 :   for(const_reverse_iterator i = context.d_scopeList.rbegin();
     286         [ -  - ]:          0 :       i != context.d_scopeList.rend();
     287                 :          0 :       ++i, --level) {
     288                 :          0 :     Scope* pScope = *i;
     289                 :          0 :     Assert(pScope->getLevel() == level);
     290                 :          0 :     Assert(pScope->getContext() == &context);
     291                 :          0 :     out << separator << std::endl
     292                 :          0 :         << *pScope << std::endl;
     293                 :            :   }
     294                 :          0 :   return out << separator << std::endl;
     295                 :            : }
     296                 :            : 
     297                 :          0 : std::ostream& operator<<(std::ostream& out, const Scope& scope)
     298                 :            : {
     299                 :          0 :   out << "Scope " << scope.d_level << " [" << &scope << "]:";
     300                 :          0 :   ContextObj* pContextObj = scope.d_pContextObjList;
     301                 :          0 :   Assert(pContextObj == NULL
     302                 :            :          || pContextObj->prev() == &scope.d_pContextObjList);
     303         [ -  - ]:          0 :   while(pContextObj != NULL) {
     304                 :          0 :     out << " <--> " << pContextObj;
     305         [ -  - ]:          0 :     if(pContextObj->d_pScope != &scope) {
     306                 :          0 :       out << " XXX bad scope" << std::endl;
     307                 :            :     }
     308                 :          0 :     Assert(pContextObj->d_pScope == &scope);
     309                 :          0 :     Assert(pContextObj->next() == NULL
     310                 :            :            || pContextObj->next()->prev() == &pContextObj->next());
     311                 :          0 :     pContextObj = pContextObj->next();
     312                 :            :   }
     313                 :          0 :   return out << " --> NULL";
     314                 :            : }
     315                 :            : 
     316                 :   19007100 : Scope::~Scope() {
     317                 :            :   // Call restore() method on each ContextObj object in the list.
     318                 :            :   // Note that it is the responsibility of restore() to return the
     319                 :            :   // next item in the list.
     320         [ +  + ]:  322494000 :   while (d_pContextObjList != NULL) {
     321                 :  303487000 :     d_pContextObjList = d_pContextObjList->restoreAndContinue();
     322                 :            :   }
     323                 :            : 
     324         [ +  + ]:  148278000 :   for (ContextObj* obj : d_garbage)
     325                 :            :   {
     326                 :  129271000 :     obj->deleteSelf();
     327                 :            :   }
     328                 :   19007100 : }
     329                 :            : 
     330                 :  129271000 : void Scope::enqueueToGarbageCollect(ContextObj* obj) {
     331                 :  129271000 :   d_garbage.push_back(obj);
     332                 :  129271000 : }
     333                 :            : 
     334                 :            : }  // namespace cvc5::context