CVC3  2.4.1
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 /*****************************************************************************/
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");
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");
77  }
78 
79  public:
80  // Constructor
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");
94  }
95 
96  // Destructor
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);
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();
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