Branch data     Line data    Source code

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