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