GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/context/context_mm.cpp Lines: 58 62 93.5 %
Date: 2021-03-23 Branches: 36 100 36.0 %

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