blob: e7b234a95dcf7ce476704dbfbb7265c2d610c2f6 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
|
/********************* */
/*! \file context_mm.cpp
** \verbatim
** Original author: Clark Barrett
** Major contributors: Morgan Deters
** Minor contributors (to current version): none
** This file is part of the CVC4 project.
** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
** \brief Implementation of Context Memory Manager.
**
** Implementation of Context Memory Manager
**/
#include <cstdlib>
#include <vector>
#include <deque>
#include <new>
#include "context/context_mm.h"
#include "util/cvc4_assert.h"
#include "util/output.h"
namespace CVC4 {
namespace context {
void ContextMemoryManager::newChunk() {
// Increment index to chunk list
++d_indexChunkList;
Assert(d_chunkList.size() == d_indexChunkList,
"Index should be at the end of the list");
// Create new chunk if no free chunk available
if(d_freeChunks.empty()) {
d_chunkList.push_back((char*)malloc(chunkSizeBytes));
if(d_chunkList.back() == NULL) {
throw std::bad_alloc();
}
}
// If there is a free chunk, use that
else {
d_chunkList.push_back(d_freeChunks.back());
d_freeChunks.pop_back();
}
// Set up the current chunk pointers
d_nextFree = d_chunkList.back();
d_endChunk = d_nextFree + chunkSizeBytes;
}
ContextMemoryManager::ContextMemoryManager() : d_indexChunkList(0) {
// Create initial chunk
d_chunkList.push_back((char*)malloc(chunkSizeBytes));
d_nextFree = d_chunkList.back();
if(d_nextFree == NULL) {
throw std::bad_alloc();
}
d_endChunk = d_nextFree + chunkSizeBytes;
}
ContextMemoryManager::~ContextMemoryManager() throw() {
// Delete all chunks
while(!d_chunkList.empty()) {
free(d_chunkList.back());
d_chunkList.pop_back();
}
while(!d_freeChunks.empty()) {
free(d_freeChunks.back());
d_freeChunks.pop_back();
}
}
void* ContextMemoryManager::newData(size_t size) {
// Use next available free location in current chunk
void* res = (void*)d_nextFree;
d_nextFree += size;
// Check if the request is too big for the chunk
if(d_nextFree > d_endChunk) {
newChunk();
res = (void*)d_nextFree;
d_nextFree += size;
AlwaysAssert(d_nextFree <= d_endChunk,
"Request is bigger than memory chunk size");
}
Debug("context") << "ContextMemoryManager::newData(" << size
<< ") returning " << res << " at level "
<< d_chunkList.size() << std::endl;
return res;
}
void ContextMemoryManager::push() {
// Store current state on the stack
d_nextFreeStack.push_back(d_nextFree);
d_endChunkStack.push_back(d_endChunk);
d_indexChunkListStack.push_back(d_indexChunkList);
}
void ContextMemoryManager::pop() {
// Restore state from stack
d_nextFree = d_nextFreeStack.back();
d_nextFreeStack.pop_back();
d_endChunk = d_endChunkStack.back();
d_endChunkStack.pop_back();
// Free all the new chunks since the last push
while(d_indexChunkList > d_indexChunkListStack.back()) {
d_freeChunks.push_back(d_chunkList.back());
d_chunkList.pop_back();
--d_indexChunkList;
}
d_indexChunkListStack.pop_back();
// Delete excess free chunks
while(d_freeChunks.size() > maxFreeChunks) {
free(d_freeChunks.front());
d_freeChunks.pop_front();
}
}
} /* CVC4::context namespace */
} /* CVC4 namespace */
|
