00001 /*****************************************************************************/ 00002 /*! 00003 *\file memory_manager_context.h 00004 *\brief Stack-based memory manager 00005 * 00006 * Author: Clark Barrett 00007 * 00008 * Created: Thu Aug 3 21:39:07 2006 00009 * 00010 * <hr> 00011 * 00012 * License to use, copy, modify, sell and/or distribute this software 00013 * and its documentation for any purpose is hereby granted without 00014 * royalty, subject to the terms and conditions defined in the \ref 00015 * LICENSE file provided with this distribution. 00016 * 00017 * <hr> 00018 */ 00019 /*****************************************************************************/ 00020 00021 #ifndef _cvc3__include__memory_manager_context_h 00022 #define _cvc3__include__memory_manager_context_h 00023 00024 #include <vector> 00025 #include "memory_manager.h" 00026 00027 namespace CVC3 { 00028 00029 /*****************************************************************************/ 00030 /*! 00031 *\class ContextMemoryManager 00032 *\brief ContextMemoryManager 00033 * 00034 * Author: Clark Barrett 00035 * 00036 * Created: Thu Aug 3 16:41:35 2006 00037 * 00038 * Stack-based memory manager 00039 */ 00040 /*****************************************************************************/ 00041 class ContextMemoryManager :public MemoryManager { 00042 private: 00043 unsigned d_chunkSizeBytes; // #bytes in each chunk 00044 00045 static std::vector<char*> s_freePages; 00046 std::vector<char*> d_chunkList; // Pointers to the beginning of each chunk 00047 00048 // Pointers to the next free block of memory in the current chunk 00049 char* d_nextFree; 00050 // Pointer to end of current chunk (1 byte off the end) 00051 char* d_endChunk; 00052 // Index into chunk vector 00053 unsigned d_indexChunkList; 00054 00055 // Stack of pointers to the next free block of memory in the current chunk 00056 std::vector<char*> d_nextFreeStack; 00057 // Stack of pointers to end of current chunk (1 byte off the end) 00058 std::vector<char*> d_endChunkStack; 00059 // Stack of indices into chunk vector 00060 std::vector<unsigned> d_indexChunkListStack; 00061 00062 // Private methods 00063 void newChunk() { // Allocate new chunk 00064 DebugAssert(d_chunkList.size() > 0, "expected unempty list"); 00065 ++d_indexChunkList; 00066 DebugAssert(d_chunkList.size() == d_indexChunkList, "invariant violated"); 00067 if (s_freePages.empty()) { 00068 d_chunkList.push_back((char*)malloc(d_chunkSizeBytes)); 00069 } 00070 else { 00071 d_chunkList.push_back(s_freePages.back()); 00072 s_freePages.pop_back(); 00073 } 00074 d_nextFree = d_chunkList.back(); 00075 FatalAssert(d_nextFree != NULL, "Out of memory"); 00076 d_endChunk = d_nextFree + d_chunkSizeBytes; 00077 } 00078 00079 public: 00080 // Constructor 00081 ContextMemoryManager(unsigned chunkSize = 16384) 00082 : d_chunkSizeBytes(chunkSize), d_indexChunkList(0) 00083 { 00084 if (s_freePages.empty()) { 00085 d_chunkList.push_back((char*)malloc(d_chunkSizeBytes)); 00086 } 00087 else { 00088 d_chunkList.push_back(s_freePages.back()); 00089 s_freePages.pop_back(); 00090 } 00091 d_nextFree = d_chunkList.back(); 00092 FatalAssert(d_nextFree != NULL, "Out of memory"); 00093 d_endChunk = d_nextFree + d_chunkSizeBytes; 00094 } 00095 00096 // Destructor 00097 ~ContextMemoryManager() { 00098 while(!d_chunkList.empty()) { 00099 s_freePages.push_back(d_chunkList.back()); 00100 d_chunkList.pop_back(); 00101 } 00102 } 00103 00104 void* newData(size_t size) { 00105 void* res = (void*)d_nextFree; 00106 d_nextFree += size; 00107 if (d_nextFree > d_endChunk) { 00108 newChunk(); 00109 res = (void*)d_nextFree; 00110 d_nextFree += size; 00111 DebugAssert(d_nextFree <= d_endChunk, "chunk not big enough"); 00112 } 00113 return res; 00114 } 00115 00116 void deleteData(void* d) { } 00117 00118 void push() { 00119 d_nextFreeStack.push_back(d_nextFree); 00120 d_endChunkStack.push_back(d_endChunk); 00121 d_indexChunkListStack.push_back(d_indexChunkList); 00122 } 00123 00124 void pop() { 00125 d_nextFree = d_nextFreeStack.back(); 00126 d_nextFreeStack.pop_back(); 00127 d_endChunk = d_endChunkStack.back(); 00128 d_endChunkStack.pop_back(); 00129 while (d_indexChunkList > d_indexChunkListStack.back()) { 00130 s_freePages.push_back(d_chunkList.back()); 00131 d_chunkList.pop_back(); 00132 --d_indexChunkList; 00133 } 00134 d_indexChunkListStack.pop_back(); 00135 } 00136 00137 static void garbageCollect(void) { 00138 while (!s_freePages.empty()) { 00139 free(s_freePages.back()); 00140 s_freePages.pop_back(); 00141 } 00142 } 00143 00144 unsigned getMemory() { 00145 return d_chunkList.size() * d_chunkSizeBytes; 00146 } 00147 00148 static unsigned getStaticMemory() { 00149 return s_freePages.size() * 16384; 00150 } 00151 00152 }; // end of class ContextMemoryManager 00153 00154 } 00155 00156 #endif