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