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 Context Memory Manager
      11                 :            :  */
      12                 :            : 
      13                 :            : #include <cstdlib>
      14                 :            : #include <deque>
      15                 :            : #include <limits>
      16                 :            : #include <new>
      17                 :            : #include <ostream>
      18                 :            : #include <vector>
      19                 :            : 
      20                 :            : #ifdef CVC5_VALGRIND
      21                 :            : #include <valgrind/memcheck.h>
      22                 :            : #endif /* CVC5_VALGRIND */
      23                 :            : 
      24                 :            : #include "base/check.h"
      25                 :            : #include "base/output.h"
      26                 :            : #include "context/context_mm.h"
      27                 :            : 
      28                 :            : namespace cvc5::context {
      29                 :            : 
      30                 :            : #ifndef CVC5_DEBUG_CONTEXT_MEMORY_MANAGER
      31                 :            : 
      32                 :    1228512 : void ContextMemoryManager::newChunk()
      33                 :            : {
      34                 :            :   // Increment index to chunk list
      35                 :    1228512 :   ++d_indexChunkList;
      36 [ -  + ][ -  + ]:    1228512 :   Assert(d_chunkList.size() == d_indexChunkList)
                 [ -  - ]
      37                 :          0 :       << "Index should be at the end of the list";
      38                 :            : 
      39                 :            :   // Create new chunk if no free chunk available
      40         [ +  + ]:    1228512 :   if (d_freeChunks.empty())
      41                 :            :   {
      42                 :     173548 :     d_chunkList.push_back((char*)malloc(chunkSizeBytes));
      43         [ -  + ]:     173548 :     if (d_chunkList.back() == nullptr)
      44                 :            :     {
      45                 :          0 :       throw std::bad_alloc();
      46                 :            :     }
      47                 :            : 
      48                 :            : #ifdef CVC5_VALGRIND
      49                 :            :     VALGRIND_MAKE_MEM_NOACCESS(d_chunkList.back(), chunkSizeBytes);
      50                 :            : #endif /* CVC5_VALGRIND */
      51                 :            :   }
      52                 :            :   // If there is a free chunk, use that
      53                 :            :   else
      54                 :            :   {
      55                 :    1054964 :     d_chunkList.push_back(d_freeChunks.back());
      56                 :    1054964 :     d_freeChunks.pop_back();
      57                 :            :   }
      58                 :            :   // Set up the current chunk pointers
      59                 :    1228512 :   d_nextFree = d_chunkList.back();
      60                 :    1228512 :   d_endChunk = d_nextFree + chunkSizeBytes;
      61                 :    1228512 : }
      62                 :            : 
      63                 :   16202226 : ContextMemoryManager::ContextMemoryManager() : d_indexChunkList(0)
      64                 :            : {
      65                 :            :   // Create initial chunk
      66                 :   16202226 :   d_chunkList.push_back((char*)malloc(chunkSizeBytes));
      67                 :   16202226 :   d_nextFree = d_chunkList.back();
      68         [ -  + ]:   16202226 :   if (d_nextFree == nullptr)
      69                 :            :   {
      70                 :          0 :     throw std::bad_alloc();
      71                 :            :   }
      72                 :   16202226 :   d_endChunk = d_nextFree + chunkSizeBytes;
      73                 :            : 
      74                 :            : #ifdef CVC5_VALGRIND
      75                 :            :   VALGRIND_CREATE_MEMPOOL(this, 0, false);
      76                 :            :   VALGRIND_MAKE_MEM_NOACCESS(d_nextFree, chunkSizeBytes);
      77                 :            :   d_allocations.push_back(std::vector<char*>());
      78                 :            : #endif /* CVC5_VALGRIND */
      79                 :   16202226 : }
      80                 :            : 
      81                 :   16179376 : ContextMemoryManager::~ContextMemoryManager()
      82                 :            : {
      83                 :            : #ifdef CVC5_VALGRIND
      84                 :            :   VALGRIND_DESTROY_MEMPOOL(this);
      85                 :            : #endif /* CVC5_VALGRIND */
      86                 :            : 
      87                 :            :   // Delete all chunks
      88         [ +  + ]:   32358752 :   while (!d_chunkList.empty())
      89                 :            :   {
      90                 :   16179376 :     free(d_chunkList.back());
      91                 :   16179376 :     d_chunkList.pop_back();
      92                 :            :   }
      93         [ +  + ]:   16306981 :   while (!d_freeChunks.empty())
      94                 :            :   {
      95                 :     127605 :     free(d_freeChunks.back());
      96                 :     127605 :     d_freeChunks.pop_back();
      97                 :            :   }
      98                 :   16179376 : }
      99                 :            : 
     100                 :  375836758 : void* ContextMemoryManager::newData(size_t size)
     101                 :            : {
     102                 :            :   // Use next available free location in current chunk
     103                 :  375836758 :   void* res = (void*)d_nextFree;
     104                 :  375836758 :   d_nextFree += size;
     105                 :            :   // Check if the request is too big for the chunk
     106         [ +  + ]:  375836758 :   if (d_nextFree > d_endChunk)
     107                 :            :   {
     108                 :    1228512 :     newChunk();
     109                 :    1228512 :     res = (void*)d_nextFree;
     110                 :    1228512 :     d_nextFree += size;
     111 [ -  + ][ -  + ]:    1228512 :     AlwaysAssert(d_nextFree <= d_endChunk)
                 [ -  - ]
     112                 :          0 :         << "Request is bigger than memory chunk size";
     113                 :            :   }
     114                 :            : 
     115                 :            : #ifdef CVC5_VALGRIND
     116                 :            :   VALGRIND_MEMPOOL_ALLOC(this, static_cast<char*>(res), size);
     117                 :            :   d_allocations.back().push_back(static_cast<char*>(res));
     118                 :            : #endif /* CVC5_VALGRIND */
     119                 :            : 
     120                 :  375836758 :   return res;
     121                 :            : }
     122                 :            : 
     123                 :   20888561 : void ContextMemoryManager::push()
     124                 :            : {
     125                 :            : #ifdef CVC5_VALGRIND
     126                 :            :   d_allocations.push_back(std::vector<char*>());
     127                 :            : #endif /* CVC5_VALGRIND */
     128                 :            : 
     129                 :            :   // Store current state on the stack
     130                 :   20888561 :   d_nextFreeStack.push_back(d_nextFree);
     131                 :   20888561 :   d_endChunkStack.push_back(d_endChunk);
     132                 :   20888561 :   d_indexChunkListStack.push_back(d_indexChunkList);
     133                 :   20888561 : }
     134                 :            : 
     135                 :   20887188 : void ContextMemoryManager::pop()
     136                 :            : {
     137                 :            : #ifdef CVC5_VALGRIND
     138                 :            :   for (auto allocation : d_allocations.back())
     139                 :            :   {
     140                 :            :     VALGRIND_MEMPOOL_FREE(this, allocation);
     141                 :            :   }
     142                 :            :   d_allocations.pop_back();
     143                 :            : #endif /* CVC5_VALGRIND */
     144                 :            : 
     145 [ +  - ][ +  - ]:   20887188 :   Assert(d_nextFreeStack.size() > 0 && d_endChunkStack.size() > 0);
         [ -  + ][ -  + ]
                 [ -  - ]
     146                 :            : 
     147                 :            :   // Restore state from stack
     148                 :   20887188 :   d_nextFree = d_nextFreeStack.back();
     149                 :   20887188 :   d_nextFreeStack.pop_back();
     150                 :   20887188 :   d_endChunk = d_endChunkStack.back();
     151                 :   20887188 :   d_endChunkStack.pop_back();
     152                 :            : 
     153                 :            :   // Free all the new chunks since the last push
     154         [ +  + ]:   22115686 :   while (d_indexChunkList > d_indexChunkListStack.back())
     155                 :            :   {
     156                 :    1228498 :     d_freeChunks.push_back(d_chunkList.back());
     157                 :            : #ifdef CVC5_VALGRIND
     158                 :            :     VALGRIND_MAKE_MEM_NOACCESS(d_chunkList.back(), chunkSizeBytes);
     159                 :            : #endif /* CVC5_VALGRIND */
     160                 :    1228498 :     d_chunkList.pop_back();
     161                 :    1228498 :     --d_indexChunkList;
     162                 :            :   }
     163                 :   20887188 :   d_indexChunkListStack.pop_back();
     164                 :            : 
     165                 :            :   // Delete excess free chunks
     166         [ +  + ]:   20933117 :   while (d_freeChunks.size() > maxFreeChunks)
     167                 :            :   {
     168                 :      45929 :     free(d_freeChunks.front());
     169                 :      45929 :     d_freeChunks.pop_front();
     170                 :            :   }
     171                 :   20887188 : }
     172                 :            : #else
     173                 :            : 
     174                 :            : unsigned ContextMemoryManager::getMaxAllocationSize()
     175                 :            : {
     176                 :            :   return std::numeric_limits<unsigned>::max();
     177                 :            : }
     178                 :            : 
     179                 :            : #endif /* CVC5_DEBUG_CONTEXT_MEMORY_MANAGER */
     180                 :            : 
     181                 :            : }  // namespace cvc5::context