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                 :    1222737 : void ContextMemoryManager::newChunk() {
      33                 :            : 
      34                 :            :   // Increment index to chunk list
      35                 :    1222737 :   ++d_indexChunkList;
      36 [ -  + ][ -  + ]:    1222737 :   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         [ +  + ]:    1222737 :   if(d_freeChunks.empty()) {
      41                 :     170125 :     d_chunkList.push_back((char*)malloc(chunkSizeBytes));
      42         [ -  + ]:     170125 :     if (d_chunkList.back() == nullptr)
      43                 :            :     {
      44                 :          0 :       throw std::bad_alloc();
      45                 :            :     }
      46                 :            : 
      47                 :            : #ifdef CVC5_VALGRIND
      48                 :            :     VALGRIND_MAKE_MEM_NOACCESS(d_chunkList.back(), chunkSizeBytes);
      49                 :            : #endif /* CVC5_VALGRIND */
      50                 :            :   }
      51                 :            :   // If there is a free chunk, use that
      52                 :            :   else {
      53                 :    1052612 :     d_chunkList.push_back(d_freeChunks.back());
      54                 :    1052612 :     d_freeChunks.pop_back();
      55                 :            :   }
      56                 :            :   // Set up the current chunk pointers
      57                 :    1222737 :   d_nextFree = d_chunkList.back();
      58                 :    1222737 :   d_endChunk = d_nextFree + chunkSizeBytes;
      59                 :    1222737 : }
      60                 :            : 
      61                 :            : 
      62                 :   16529937 : ContextMemoryManager::ContextMemoryManager() : d_indexChunkList(0) {
      63                 :            :   // Create initial chunk
      64                 :   16529937 :   d_chunkList.push_back((char*)malloc(chunkSizeBytes));
      65                 :   16529937 :   d_nextFree = d_chunkList.back();
      66         [ -  + ]:   16529937 :   if (d_nextFree == nullptr)
      67                 :            :   {
      68                 :          0 :     throw std::bad_alloc();
      69                 :            :   }
      70                 :   16529937 :   d_endChunk = d_nextFree + chunkSizeBytes;
      71                 :            : 
      72                 :            : #ifdef CVC5_VALGRIND
      73                 :            :   VALGRIND_CREATE_MEMPOOL(this, 0, false);
      74                 :            :   VALGRIND_MAKE_MEM_NOACCESS(d_nextFree, chunkSizeBytes);
      75                 :            :   d_allocations.push_back(std::vector<char*>());
      76                 :            : #endif /* CVC5_VALGRIND */
      77                 :   16529937 : }
      78                 :            : 
      79                 :            : 
      80                 :   16507624 : ContextMemoryManager::~ContextMemoryManager() {
      81                 :            : #ifdef CVC5_VALGRIND
      82                 :            :   VALGRIND_DESTROY_MEMPOOL(this);
      83                 :            : #endif /* CVC5_VALGRIND */
      84                 :            : 
      85                 :            :   // Delete all chunks
      86         [ +  + ]:   33015248 :   while(!d_chunkList.empty()) {
      87                 :   16507624 :     free(d_chunkList.back());
      88                 :   16507624 :     d_chunkList.pop_back();
      89                 :            :   }
      90         [ +  + ]:   16632588 :   while(!d_freeChunks.empty()) {
      91                 :     124964 :     free(d_freeChunks.back());
      92                 :     124964 :     d_freeChunks.pop_back();
      93                 :            :   }
      94                 :   16507624 : }
      95                 :            : 
      96                 :            : 
      97                 :  352717980 : void* ContextMemoryManager::newData(size_t size) {
      98                 :            :   // Use next available free location in current chunk
      99                 :  352717980 :   void* res = (void*)d_nextFree;
     100                 :  352717980 :   d_nextFree += size;
     101                 :            :   // Check if the request is too big for the chunk
     102         [ +  + ]:  352717980 :   if(d_nextFree > d_endChunk) {
     103                 :    1222737 :     newChunk();
     104                 :    1222737 :     res = (void*)d_nextFree;
     105                 :    1222737 :     d_nextFree += size;
     106 [ -  + ][ -  + ]:    1222737 :     AlwaysAssert(d_nextFree <= d_endChunk)
                 [ -  - ]
     107                 :          0 :         << "Request is bigger than memory chunk size";
     108                 :            :   }
     109                 :            : 
     110                 :            : #ifdef CVC5_VALGRIND
     111                 :            :   VALGRIND_MEMPOOL_ALLOC(this, static_cast<char*>(res), size);
     112                 :            :   d_allocations.back().push_back(static_cast<char*>(res));
     113                 :            : #endif /* CVC5_VALGRIND */
     114                 :            : 
     115                 :  352717980 :   return res;
     116                 :            : }
     117                 :            : 
     118                 :            : 
     119                 :   19524956 : void ContextMemoryManager::push() {
     120                 :            : #ifdef CVC5_VALGRIND
     121                 :            :   d_allocations.push_back(std::vector<char*>());
     122                 :            : #endif /* CVC5_VALGRIND */
     123                 :            : 
     124                 :            :   // Store current state on the stack
     125                 :   19524956 :   d_nextFreeStack.push_back(d_nextFree);
     126                 :   19524956 :   d_endChunkStack.push_back(d_endChunk);
     127                 :   19524956 :   d_indexChunkListStack.push_back(d_indexChunkList);
     128                 :   19524956 : }
     129                 :            : 
     130                 :            : 
     131                 :   19523595 : void ContextMemoryManager::pop() {
     132                 :            : #ifdef CVC5_VALGRIND
     133                 :            :   for (auto allocation : d_allocations.back())
     134                 :            :   {
     135                 :            :     VALGRIND_MEMPOOL_FREE(this, allocation);
     136                 :            :   }
     137                 :            :   d_allocations.pop_back();
     138                 :            : #endif /* CVC5_VALGRIND */
     139                 :            : 
     140 [ +  - ][ +  - ]:   19523595 :   Assert(d_nextFreeStack.size() > 0 && d_endChunkStack.size() > 0);
         [ -  + ][ -  + ]
                 [ -  - ]
     141                 :            : 
     142                 :            :   // Restore state from stack
     143                 :   19523595 :   d_nextFree = d_nextFreeStack.back();
     144                 :   19523595 :   d_nextFreeStack.pop_back();
     145                 :   19523595 :   d_endChunk = d_endChunkStack.back();
     146                 :   19523595 :   d_endChunkStack.pop_back();
     147                 :            : 
     148                 :            :   // Free all the new chunks since the last push
     149         [ +  + ]:   20746318 :   while(d_indexChunkList > d_indexChunkListStack.back()) {
     150                 :    1222723 :     d_freeChunks.push_back(d_chunkList.back());
     151                 :            : #ifdef CVC5_VALGRIND
     152                 :            :     VALGRIND_MAKE_MEM_NOACCESS(d_chunkList.back(), chunkSizeBytes);
     153                 :            : #endif /* CVC5_VALGRIND */
     154                 :    1222723 :     d_chunkList.pop_back();
     155                 :    1222723 :     --d_indexChunkList;
     156                 :            :   }
     157                 :   19523595 :   d_indexChunkListStack.pop_back();
     158                 :            : 
     159                 :            :   // Delete excess free chunks
     160         [ +  + ]:   19568742 :   while(d_freeChunks.size() > maxFreeChunks) {
     161                 :      45147 :     free(d_freeChunks.front());
     162                 :      45147 :     d_freeChunks.pop_front();
     163                 :            :   }
     164                 :   19523595 : }
     165                 :            : #else
     166                 :            : 
     167                 :            : unsigned ContextMemoryManager::getMaxAllocationSize()
     168                 :            : {
     169                 :            :   return std::numeric_limits<unsigned>::max();
     170                 :            : }
     171                 :            : 
     172                 :            : #endif /* CVC5_DEBUG_CONTEXT_MEMORY_MANAGER */
     173                 :            : 
     174                 :            : }  // namespace cvc5::context