mirror of
https://github.com/Z3Prover/z3
synced 2025-06-14 09:56:15 +00:00
Use glibc's malloc_usable_size when available (#6321)
This commit is contained in:
parent
6a61efbf99
commit
9717dadd9f
1 changed files with 83 additions and 37 deletions
|
@ -13,6 +13,11 @@ Copyright (c) 2015 Microsoft Corporation
|
||||||
#include "util/error_codes.h"
|
#include "util/error_codes.h"
|
||||||
#include "util/debug.h"
|
#include "util/debug.h"
|
||||||
#include "util/scoped_timer.h"
|
#include "util/scoped_timer.h"
|
||||||
|
#ifdef __GLIBC__
|
||||||
|
# include <malloc.h>
|
||||||
|
# define HAS_MALLOC_USABLE_SIZE
|
||||||
|
#endif
|
||||||
|
|
||||||
// The following two function are automatically generated by the mk_make.py script.
|
// 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.
|
// The script collects ADD_INITIALIZER and ADD_FINALIZER commands in the .h files.
|
||||||
// For example, rational.h contains
|
// For example, rational.h contains
|
||||||
|
@ -215,7 +220,7 @@ void * memory::allocate(char const* file, int line, char const* obj, size_t s) {
|
||||||
}
|
}
|
||||||
#endif
|
#endif
|
||||||
|
|
||||||
#if !defined(SINGLE_THREAD)
|
#ifndef SINGLE_THREAD
|
||||||
// ==================================
|
// ==================================
|
||||||
// ==================================
|
// ==================================
|
||||||
// THREAD LOCAL VERSION
|
// THREAD LOCAL VERSION
|
||||||
|
@ -258,9 +263,14 @@ static void synchronize_counters(bool allocating) {
|
||||||
}
|
}
|
||||||
|
|
||||||
void memory::deallocate(void * p) {
|
void memory::deallocate(void * p) {
|
||||||
|
#ifdef HAS_MALLOC_USABLE_SIZE
|
||||||
|
size_t sz = malloc_usable_size(p);
|
||||||
|
void * real_p = p;
|
||||||
|
#else
|
||||||
size_t * sz_p = reinterpret_cast<size_t*>(p) - 1;
|
size_t * sz_p = reinterpret_cast<size_t*>(p) - 1;
|
||||||
size_t sz = *sz_p;
|
size_t sz = *sz_p;
|
||||||
void * real_p = reinterpret_cast<void*>(sz_p);
|
void * real_p = reinterpret_cast<void*>(sz_p);
|
||||||
|
#endif
|
||||||
g_memory_thread_alloc_size -= sz;
|
g_memory_thread_alloc_size -= sz;
|
||||||
free(real_p);
|
free(real_p);
|
||||||
if (g_memory_thread_alloc_size < -SYNCH_THRESHOLD) {
|
if (g_memory_thread_alloc_size < -SYNCH_THRESHOLD) {
|
||||||
|
@ -269,28 +279,41 @@ void memory::deallocate(void * p) {
|
||||||
}
|
}
|
||||||
|
|
||||||
void * memory::allocate(size_t s) {
|
void * memory::allocate(size_t s) {
|
||||||
|
#ifndef HAS_MALLOC_USABLE_SIZE
|
||||||
s = s + sizeof(size_t); // we allocate an extra field!
|
s = s + sizeof(size_t); // we allocate an extra field!
|
||||||
void * r = malloc(s);
|
#endif
|
||||||
if (r == nullptr) {
|
|
||||||
throw_out_of_memory();
|
|
||||||
return nullptr;
|
|
||||||
}
|
|
||||||
*(static_cast<size_t*>(r)) = s;
|
|
||||||
g_memory_thread_alloc_size += s;
|
g_memory_thread_alloc_size += s;
|
||||||
g_memory_thread_alloc_count += 1;
|
g_memory_thread_alloc_count += 1;
|
||||||
if (g_memory_thread_alloc_size > SYNCH_THRESHOLD) {
|
if (g_memory_thread_alloc_size > SYNCH_THRESHOLD) {
|
||||||
synchronize_counters(true);
|
synchronize_counters(true);
|
||||||
}
|
}
|
||||||
|
void * r = malloc(s);
|
||||||
|
if (r == nullptr) {
|
||||||
|
throw_out_of_memory();
|
||||||
|
return nullptr;
|
||||||
|
}
|
||||||
|
#ifdef HAS_MALLOC_USABLE_SIZE
|
||||||
|
g_memory_thread_alloc_size += malloc_usable_size(r) - s;
|
||||||
|
return r;
|
||||||
|
#else
|
||||||
|
*(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
|
||||||
|
#endif
|
||||||
}
|
}
|
||||||
|
|
||||||
void* memory::reallocate(void *p, size_t s) {
|
void* memory::reallocate(void *p, size_t s) {
|
||||||
|
#ifdef HAS_MALLOC_USABLE_SIZE
|
||||||
|
size_t sz = malloc_usable_size(p);
|
||||||
|
void * real_p = p;
|
||||||
|
// We may be lucky and malloc gave us enough space
|
||||||
|
if (sz >= s)
|
||||||
|
return p;
|
||||||
|
#else
|
||||||
size_t *sz_p = reinterpret_cast<size_t*>(p)-1;
|
size_t *sz_p = reinterpret_cast<size_t*>(p)-1;
|
||||||
size_t sz = *sz_p;
|
size_t sz = *sz_p;
|
||||||
void *real_p = reinterpret_cast<void*>(sz_p);
|
void *real_p = reinterpret_cast<void*>(sz_p);
|
||||||
s = s + sizeof(size_t); // we allocate an extra field!
|
s = s + sizeof(size_t); // we allocate an extra field!
|
||||||
|
#endif
|
||||||
g_memory_thread_alloc_size += s - sz;
|
g_memory_thread_alloc_size += s - sz;
|
||||||
g_memory_thread_alloc_count += 1;
|
g_memory_thread_alloc_count += 1;
|
||||||
if (g_memory_thread_alloc_size > SYNCH_THRESHOLD) {
|
if (g_memory_thread_alloc_size > SYNCH_THRESHOLD) {
|
||||||
|
@ -302,74 +325,97 @@ void* memory::reallocate(void *p, size_t s) {
|
||||||
throw_out_of_memory();
|
throw_out_of_memory();
|
||||||
return nullptr;
|
return nullptr;
|
||||||
}
|
}
|
||||||
|
#ifdef HAS_MALLOC_USABLE_SIZE
|
||||||
|
g_memory_thread_alloc_size += malloc_usable_size(r) - s;
|
||||||
|
return r;
|
||||||
|
#else
|
||||||
*(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
|
||||||
|
#endif
|
||||||
}
|
}
|
||||||
|
|
||||||
#else
|
#else
|
||||||
// ==================================
|
// ==================================
|
||||||
// ==================================
|
// ==================================
|
||||||
// NO THREAD LOCAL VERSION
|
// SINGLE-THREAD MODE
|
||||||
// ==================================
|
// ==================================
|
||||||
// ==================================
|
// ==================================
|
||||||
// allocate & deallocate without using thread local storage
|
// allocate & deallocate without locking
|
||||||
|
|
||||||
void memory::deallocate(void * p) {
|
void memory::deallocate(void * p) {
|
||||||
|
#ifdef HAS_MALLOC_USABLE_SIZE
|
||||||
|
size_t sz = malloc_usable_size(p);
|
||||||
|
void * real_p = p;
|
||||||
|
#else
|
||||||
size_t * sz_p = reinterpret_cast<size_t*>(p) - 1;
|
size_t * sz_p = reinterpret_cast<size_t*>(p) - 1;
|
||||||
size_t sz = *sz_p;
|
size_t sz = *sz_p;
|
||||||
void * real_p = reinterpret_cast<void*>(sz_p);
|
void * real_p = reinterpret_cast<void*>(sz_p);
|
||||||
{
|
#endif
|
||||||
lock_guard lock(*g_memory_mux);
|
g_memory_alloc_size -= sz;
|
||||||
g_memory_alloc_size -= sz;
|
|
||||||
}
|
|
||||||
free(real_p);
|
free(real_p);
|
||||||
}
|
}
|
||||||
|
|
||||||
void * memory::allocate(size_t s) {
|
void * memory::allocate(size_t s) {
|
||||||
|
#ifndef HAS_MALLOC_USABLE_SIZE
|
||||||
s = s + sizeof(size_t); // we allocate an extra field!
|
s = s + sizeof(size_t); // we allocate an extra field!
|
||||||
{
|
#endif
|
||||||
lock_guard lock(*g_memory_mux);
|
g_memory_alloc_size += s;
|
||||||
g_memory_alloc_size += s;
|
g_memory_alloc_count += 1;
|
||||||
g_memory_alloc_count += 1;
|
if (g_memory_alloc_size > g_memory_max_used_size)
|
||||||
if (g_memory_alloc_size > g_memory_max_used_size)
|
g_memory_max_used_size = g_memory_alloc_size;
|
||||||
g_memory_max_used_size = g_memory_alloc_size;
|
if (g_memory_max_size != 0 && g_memory_alloc_size > g_memory_max_size)
|
||||||
if (g_memory_max_size != 0 && g_memory_alloc_size > g_memory_max_size)
|
throw_out_of_memory();
|
||||||
throw_out_of_memory();
|
if (g_memory_max_alloc_count != 0 && g_memory_alloc_count > g_memory_max_alloc_count)
|
||||||
if (g_memory_max_alloc_count != 0 && g_memory_alloc_count > g_memory_max_alloc_count)
|
throw_alloc_counts_exceeded();
|
||||||
throw_alloc_counts_exceeded();
|
|
||||||
}
|
|
||||||
void * r = malloc(s);
|
void * r = malloc(s);
|
||||||
if (r == nullptr) {
|
if (r == nullptr) {
|
||||||
throw_out_of_memory();
|
throw_out_of_memory();
|
||||||
return nullptr;
|
return nullptr;
|
||||||
}
|
}
|
||||||
|
#ifdef HAS_MALLOC_USABLE_SIZE
|
||||||
|
g_memory_alloc_size += malloc_usable_size(r) - s;
|
||||||
|
return r;
|
||||||
|
#else
|
||||||
*(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
|
||||||
|
#endif
|
||||||
}
|
}
|
||||||
|
|
||||||
void* memory::reallocate(void *p, size_t s) {
|
void* memory::reallocate(void *p, size_t s) {
|
||||||
|
#ifdef HAS_MALLOC_USABLE_SIZE
|
||||||
|
size_t sz = malloc_usable_size(p);
|
||||||
|
void * real_p = p;
|
||||||
|
// We may be lucky and malloc gave us enough space
|
||||||
|
if (sz >= s)
|
||||||
|
return p;
|
||||||
|
#else
|
||||||
size_t * sz_p = reinterpret_cast<size_t*>(p) - 1;
|
size_t * sz_p = reinterpret_cast<size_t*>(p) - 1;
|
||||||
size_t sz = *sz_p;
|
size_t sz = *sz_p;
|
||||||
void * real_p = reinterpret_cast<void*>(sz_p);
|
void * real_p = reinterpret_cast<void*>(sz_p);
|
||||||
s = s + sizeof(size_t); // we allocate an extra field!
|
s = s + sizeof(size_t); // we allocate an extra field!
|
||||||
{
|
#endif
|
||||||
lock_guard lock(*g_memory_mux);
|
g_memory_alloc_size += s - sz;
|
||||||
g_memory_alloc_size += s - sz;
|
g_memory_alloc_count += 1;
|
||||||
g_memory_alloc_count += 1;
|
if (g_memory_alloc_size > g_memory_max_used_size)
|
||||||
if (g_memory_alloc_size > g_memory_max_used_size)
|
g_memory_max_used_size = g_memory_alloc_size;
|
||||||
g_memory_max_used_size = g_memory_alloc_size;
|
if (g_memory_max_size != 0 && g_memory_alloc_size > g_memory_max_size)
|
||||||
if (g_memory_max_size != 0 && g_memory_alloc_size > g_memory_max_size)
|
throw_out_of_memory();
|
||||||
throw_out_of_memory();
|
if (g_memory_max_alloc_count != 0 && g_memory_alloc_count > g_memory_max_alloc_count)
|
||||||
if (g_memory_max_alloc_count != 0 && g_memory_alloc_count > g_memory_max_alloc_count)
|
throw_alloc_counts_exceeded();
|
||||||
throw_alloc_counts_exceeded();
|
|
||||||
}
|
|
||||||
void *r = realloc(real_p, s);
|
void *r = realloc(real_p, s);
|
||||||
if (r == nullptr) {
|
if (r == nullptr) {
|
||||||
throw_out_of_memory();
|
throw_out_of_memory();
|
||||||
return nullptr;
|
return nullptr;
|
||||||
}
|
}
|
||||||
|
#ifdef HAS_MALLOC_USABLE_SIZE
|
||||||
|
g_memory_alloc_size += malloc_usable_size(r) - s;
|
||||||
|
return r;
|
||||||
|
#else
|
||||||
*(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
|
||||||
|
#endif
|
||||||
}
|
}
|
||||||
|
|
||||||
#endif
|
#endif
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue