Z3 memory manager stores actual data along with its size, which causes the memory to be 8-byte aligned. Use malloc non-portable functions to obtain memory region size instead. https://github.com/Z3Prover/z3/issues/6015 --- src/util/memory_manager.cpp.orig 2022-05-05 00:16:30 UTC +++ src/util/memory_manager.cpp @@ -13,6 +13,7 @@ --*/ #include "util/error_codes.h" #include "util/debug.h" #include "util/scoped_timer.h" +#include // The following two function are automatically generated by the mk_make.py script. // The script collects ADD_INITIALIZER and ADD_FINALIZER commands in the .h files. // For example, rational.h contains @@ -258,52 +259,43 @@ void memory::deallocate(void * p) { } void memory::deallocate(void * p) { - size_t * sz_p = reinterpret_cast(p) - 1; - size_t sz = *sz_p; - void * real_p = reinterpret_cast(sz_p); - g_memory_thread_alloc_size -= sz; - free(real_p); + g_memory_thread_alloc_size -= malloc_usable_size(p); + if (g_memory_thread_alloc_size < 0) g_memory_thread_alloc_size = 0; + free(p); if (g_memory_thread_alloc_size < -SYNCH_THRESHOLD) { synchronize_counters(false); } } void * memory::allocate(size_t s) { - s = s + sizeof(size_t); // we allocate an extra field! void * r = malloc(s); if (r == 0) { throw_out_of_memory(); return nullptr; } - *(static_cast(r)) = s; g_memory_thread_alloc_size += s; g_memory_thread_alloc_count += 1; if (g_memory_thread_alloc_size > SYNCH_THRESHOLD) { synchronize_counters(true); } - return static_cast(r) + 1; // we return a pointer to the location after the extra field + return r; // 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(p)-1; - size_t sz = *sz_p; - void *real_p = reinterpret_cast(sz_p); - s = s + sizeof(size_t); // we allocate an extra field! - - g_memory_thread_alloc_size += s - sz; + g_memory_thread_alloc_size += s - malloc_usable_size(p); + if (g_memory_thread_alloc_size < 0) g_memory_thread_alloc_size = 0; g_memory_thread_alloc_count += 1; if (g_memory_thread_alloc_size > SYNCH_THRESHOLD) { synchronize_counters(true); } - void *r = realloc(real_p, s); + void *r = realloc(p, s); if (r == 0) { throw_out_of_memory(); return nullptr; } - *(static_cast(r)) = s; - return static_cast(r) + 1; // we return a pointer to the location after the extra field + return r; } #else