mirror of
https://github.com/Z3Prover/z3
synced 2025-06-03 12:51:22 +00:00
add reallocate() function and use it in bit_vector and vector containers
give a speedup of 1-4% Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
This commit is contained in:
parent
55ca6ce44b
commit
44e647e72b
5 changed files with 51 additions and 18 deletions
|
@ -25,13 +25,11 @@ Revision History:
|
||||||
#define MK_MASK(_num_bits_) ((1U << _num_bits_) - 1)
|
#define MK_MASK(_num_bits_) ((1U << _num_bits_) - 1)
|
||||||
|
|
||||||
void bit_vector::expand_to(unsigned new_capacity) {
|
void bit_vector::expand_to(unsigned new_capacity) {
|
||||||
unsigned * new_data = alloc_svect(unsigned, new_capacity);
|
if (m_data) {
|
||||||
memset(new_data, 0, new_capacity * sizeof(unsigned));
|
m_data = (unsigned*)memory::reallocate(m_data, new_capacity * sizeof(unsigned));
|
||||||
if (m_capacity > 0) {
|
} else {
|
||||||
memcpy(new_data, m_data, m_capacity * sizeof(unsigned));
|
m_data = alloc_svect(unsigned, new_capacity);
|
||||||
dealloc_svect(m_data);
|
|
||||||
}
|
}
|
||||||
m_data = new_data;
|
|
||||||
m_capacity = new_capacity;
|
m_capacity = new_capacity;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
@ -87,9 +87,7 @@ public:
|
||||||
}
|
}
|
||||||
|
|
||||||
~bit_vector() {
|
~bit_vector() {
|
||||||
if (m_data) {
|
dealloc_svect(m_data);
|
||||||
dealloc_svect(m_data);
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
|
|
||||||
void reset() {
|
void reset() {
|
||||||
|
|
|
@ -252,6 +252,24 @@ void * memory::allocate(size_t s) {
|
||||||
return static_cast<size_t*>(r) + 1; // we return a pointer to the location after the extra field
|
return static_cast<size_t*>(r) + 1; // we return a pointer to the location after the extra field
|
||||||
}
|
}
|
||||||
|
|
||||||
|
void* memory::reallocate(void *p, size_t s) {
|
||||||
|
size_t *sz_p = reinterpret_cast<size_t*>(p)-1;
|
||||||
|
size_t sz = *sz_p;
|
||||||
|
void *real_p = reinterpret_cast<void*>(sz_p);
|
||||||
|
s = s + sizeof(size_t); // we allocate an extra field!
|
||||||
|
|
||||||
|
g_memory_thread_alloc_size += s - sz;
|
||||||
|
if (g_memory_thread_alloc_size > SYNCH_THRESHOLD) {
|
||||||
|
synchronize_counters(true);
|
||||||
|
}
|
||||||
|
|
||||||
|
void *r = realloc(real_p, s);
|
||||||
|
if (r == 0)
|
||||||
|
throw_out_of_memory();
|
||||||
|
*(static_cast<size_t*>(r)) = s;
|
||||||
|
return static_cast<size_t*>(r) + 1; // we return a pointer to the location after the extra field
|
||||||
|
}
|
||||||
|
|
||||||
#else
|
#else
|
||||||
// ==================================
|
// ==================================
|
||||||
// ==================================
|
// ==================================
|
||||||
|
@ -292,5 +310,29 @@ void * memory::allocate(size_t s) {
|
||||||
*(static_cast<size_t*>(r)) = s;
|
*(static_cast<size_t*>(r)) = s;
|
||||||
return static_cast<size_t*>(r) + 1; // we return a pointer to the location after the extra field
|
return static_cast<size_t*>(r) + 1; // we return a pointer to the location after the extra field
|
||||||
}
|
}
|
||||||
|
|
||||||
|
void* memory::reallocate(void *p, size_t s) {
|
||||||
|
size_t * sz_p = reinterpret_cast<size_t*>(p) - 1;
|
||||||
|
size_t sz = *sz_p;
|
||||||
|
void * real_p = reinterpret_cast<void*>(sz_p);
|
||||||
|
s = s + sizeof(size_t); // we allocate an extra field!
|
||||||
|
bool out_of_mem = false;
|
||||||
|
#pragma omp critical (z3_memory_manager)
|
||||||
|
{
|
||||||
|
g_memory_alloc_size += s - sz;
|
||||||
|
if (g_memory_alloc_size > g_memory_max_used_size)
|
||||||
|
g_memory_max_used_size = g_memory_alloc_size;
|
||||||
|
if (g_memory_max_size != 0 && g_memory_alloc_size > g_memory_max_size)
|
||||||
|
out_of_mem = true;
|
||||||
|
}
|
||||||
|
if (out_of_mem)
|
||||||
|
throw_out_of_memory();
|
||||||
|
|
||||||
|
void *r = realloc(real_p, s);
|
||||||
|
if (r == 0)
|
||||||
|
throw_out_of_memory();
|
||||||
|
*(static_cast<size_t*>(r)) = s;
|
||||||
|
return static_cast<size_t*>(r) + 1; // we return a pointer to the location after the extra field
|
||||||
|
}
|
||||||
|
|
||||||
#endif
|
#endif
|
||||||
|
|
|
@ -58,6 +58,7 @@ public:
|
||||||
static void display_i_max_usage(std::ostream& os);
|
static void display_i_max_usage(std::ostream& os);
|
||||||
static void deallocate(void* p);
|
static void deallocate(void* p);
|
||||||
static ALLOC_ATTR void* allocate(size_t s);
|
static ALLOC_ATTR void* allocate(size_t s);
|
||||||
|
static ALLOC_ATTR void* reallocate(void *p, size_t s);
|
||||||
#if _DEBUG
|
#if _DEBUG
|
||||||
static void deallocate(char const* file, int line, void* p);
|
static void deallocate(char const* file, int line, void* p);
|
||||||
static ALLOC_ATTR void* allocate(char const* file, int line, char const* obj, size_t s);
|
static ALLOC_ATTR void* allocate(char const* file, int line, char const* obj, size_t s);
|
||||||
|
|
|
@ -71,18 +71,12 @@ class vector {
|
||||||
SZ old_capacity_T = sizeof(T) * old_capacity + sizeof(SZ) * 2;
|
SZ old_capacity_T = sizeof(T) * old_capacity + sizeof(SZ) * 2;
|
||||||
SZ new_capacity = (3 * old_capacity + 1) >> 1;
|
SZ new_capacity = (3 * old_capacity + 1) >> 1;
|
||||||
SZ new_capacity_T = sizeof(T) * new_capacity + sizeof(SZ) * 2;
|
SZ new_capacity_T = sizeof(T) * new_capacity + sizeof(SZ) * 2;
|
||||||
SZ size = reinterpret_cast<SZ *>(m_data)[SIZE_IDX];
|
|
||||||
if (new_capacity <= old_capacity || new_capacity_T <= old_capacity_T) {
|
if (new_capacity <= old_capacity || new_capacity_T <= old_capacity_T) {
|
||||||
throw default_exception("Overflow encountered when expanding vector");
|
throw default_exception("Overflow encountered when expanding vector");
|
||||||
}
|
}
|
||||||
SZ * mem = reinterpret_cast<SZ*>(memory::allocate(new_capacity_T));
|
SZ *mem = (SZ*)memory::reallocate(reinterpret_cast<SZ*>(m_data)-2, new_capacity_T);
|
||||||
*mem = new_capacity;
|
*mem = new_capacity;
|
||||||
mem ++;
|
m_data = reinterpret_cast<T *>(mem + 2);
|
||||||
*mem = size;
|
|
||||||
mem++;
|
|
||||||
memcpy(mem, m_data, size * sizeof(T));
|
|
||||||
free_memory();
|
|
||||||
m_data = reinterpret_cast<T *>(mem);
|
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue