CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
include
memory_manager_context.h
Go to the documentation of this file.
1
/*****************************************************************************/
2
/*!
3
*\file memory_manager_context.h
4
*\brief Stack-based memory manager
5
*
6
* Author: Clark Barrett
7
*
8
* Created: Thu Aug 3 21:39:07 2006
9
*
10
* <hr>
11
*
12
* License to use, copy, modify, sell and/or distribute this software
13
* and its documentation for any purpose is hereby granted without
14
* royalty, subject to the terms and conditions defined in the \ref
15
* LICENSE file provided with this distribution.
16
*
17
* <hr>
18
*/
19
/*****************************************************************************/
20
21
#ifndef _cvc3__include__memory_manager_context_h
22
#define _cvc3__include__memory_manager_context_h
23
24
#include <cstdlib>
25
#include <vector>
26
#include "
memory_manager.h
"
27
28
namespace
CVC3 {
29
30
const
unsigned
chunkSizeBytes
= 16384;
// #bytes in each chunk
31
32
/*****************************************************************************/
33
/*!
34
*\class ContextMemoryManager
35
*\brief ContextMemoryManager
36
*
37
* Author: Clark Barrett
38
*
39
* Created: Thu Aug 3 16:41:35 2006
40
*
41
* Stack-based memory manager
42
*/
43
/*****************************************************************************/
44
class
ContextMemoryManager
:
public
MemoryManager
{
45
static
std::vector<char*>
s_freePages
;
46
std::vector<char*>
d_chunkList
;
// Pointers to the beginning of each chunk
47
48
// Pointers to the next free block of memory in the current chunk
49
char
*
d_nextFree
;
50
// Pointer to end of current chunk (1 byte off the end)
51
char
*
d_endChunk
;
52
// Index into chunk vector
53
unsigned
d_indexChunkList
;
54
55
// Stack of pointers to the next free block of memory in the current chunk
56
std::vector<char*>
d_nextFreeStack
;
57
// Stack of pointers to end of current chunk (1 byte off the end)
58
std::vector<char*>
d_endChunkStack
;
59
// Stack of indices into chunk vector
60
std::vector<unsigned>
d_indexChunkListStack
;
61
62
// Private methods
63
void
newChunk
() {
// Allocate new chunk
64
DebugAssert
(
d_chunkList
.size() > 0,
"expected unempty list"
);
65
++
d_indexChunkList
;
66
DebugAssert
(
d_chunkList
.size() ==
d_indexChunkList
,
"invariant violated"
);
67
if
(
s_freePages
.empty()) {
68
d_chunkList
.push_back((
char
*)malloc(
chunkSizeBytes
));
69
}
70
else
{
71
d_chunkList
.push_back(
s_freePages
.back());
72
s_freePages
.pop_back();
73
}
74
d_nextFree
=
d_chunkList
.back();
75
FatalAssert
(
d_nextFree
!= NULL,
"Out of memory"
);
76
d_endChunk
=
d_nextFree
+
chunkSizeBytes
;
77
}
78
79
public
:
80
// Constructor
81
ContextMemoryManager
()
82
:
d_indexChunkList
(0)
83
{
84
if
(
s_freePages
.empty()) {
85
d_chunkList
.push_back((
char
*)malloc(
chunkSizeBytes
));
86
}
87
else
{
88
d_chunkList
.push_back(
s_freePages
.back());
89
s_freePages
.pop_back();
90
}
91
d_nextFree
=
d_chunkList
.back();
92
FatalAssert
(
d_nextFree
!= NULL,
"Out of memory"
);
93
d_endChunk
=
d_nextFree
+
chunkSizeBytes
;
94
}
95
96
// Destructor
97
~ContextMemoryManager
() {
98
while
(!
d_chunkList
.empty()) {
99
s_freePages
.push_back(
d_chunkList
.back());
100
d_chunkList
.pop_back();
101
}
102
}
103
104
void
*
newData
(
size_t
size) {
105
void
* res = (
void
*)
d_nextFree
;
106
d_nextFree
+= size;
107
if
(
d_nextFree
>
d_endChunk
) {
108
newChunk
();
109
res = (
void
*)
d_nextFree
;
110
d_nextFree
+= size;
111
DebugAssert
(
d_nextFree
<=
d_endChunk
,
"chunk not big enough"
);
112
}
113
return
res;
114
}
115
116
void
deleteData
(
void
* d) { }
117
118
void
push
() {
119
d_nextFreeStack
.push_back(
d_nextFree
);
120
d_endChunkStack
.push_back(
d_endChunk
);
121
d_indexChunkListStack
.push_back(
d_indexChunkList
);
122
}
123
124
void
pop
() {
125
d_nextFree
=
d_nextFreeStack
.back();
126
d_nextFreeStack
.pop_back();
127
d_endChunk
=
d_endChunkStack
.back();
128
d_endChunkStack
.pop_back();
129
while
(
d_indexChunkList
>
d_indexChunkListStack
.back()) {
130
s_freePages
.push_back(
d_chunkList
.back());
131
d_chunkList
.pop_back();
132
--
d_indexChunkList
;
133
}
134
d_indexChunkListStack
.pop_back();
135
}
136
137
static
void
garbageCollect
(
void
) {
138
while
(!
s_freePages
.empty()) {
139
free(
s_freePages
.back());
140
s_freePages
.pop_back();
141
}
142
}
143
144
unsigned
getMemory
(
int
verbosity) {
145
unsigned
long
memSelf =
sizeof
(
ContextMemoryManager
);
146
unsigned
long
mem = 0;
147
148
mem +=
MemoryTracker::getVec
(verbosity - 1,
d_chunkList
);
149
mem +=
MemoryTracker::getVec
(verbosity - 1,
d_nextFreeStack
);
150
mem +=
MemoryTracker::getVec
(verbosity - 1,
d_endChunkStack
);
151
mem +=
MemoryTracker::getVec
(verbosity - 1,
d_indexChunkListStack
);
152
153
mem +=
d_chunkList
.size() *
chunkSizeBytes
;
154
155
MemoryTracker::print
(
"ContextMemoryManager"
, verbosity, memSelf, mem);
156
157
return
mem + memSelf;
158
}
159
160
static
unsigned
getStaticMemory
(
int
verbosity) {
161
unsigned
mem = 0;
162
mem +=
MemoryTracker::getVec
(verbosity - 1,
s_freePages
);
163
mem +=
s_freePages
.size() *
chunkSizeBytes
;
164
MemoryTracker::print
(
"ContextMemoryManager Static"
, verbosity, 0, mem);
165
return
mem;
166
}
167
168
};
// end of class ContextMemoryManager
169
170
}
171
172
#endif
Generated on Tue May 14 2013 14:44:52 for CVC3 by
1.8.3.1