perf: use C23's free_sized when available (#6598)

See https://www.open-std.org/jtc1/sc22/wg14/www/docs/n2699.htm for an explanation of this feature. --------- Co-authored-by: Chris Kennelly <[email protected]>
leanprover · Jan 28, 2025 · 6aa6407 · 6aa6407
1 parent 9247206
commit 6aa6407
Show file tree

Hide file tree

Showing 5 changed files with 20 additions and 5 deletions.
diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h
@@ -380,11 +380,16 @@ static inline unsigned lean_small_object_size(lean_object * o) {
 void free(void *);  // avoid including big `stdlib.h`
 #endif
 
+#if !defined(__STDC_VERSION_STDLIB_H__) || __STDC_VERSION_STDLIB_H__ < 202311L
+void free_sized(void* ptr, size_t);
+#endif
+
 static inline void lean_free_small_object(lean_object * o) {
 #ifdef LEAN_SMALL_ALLOCATOR
     lean_free_small(o);
 #else
-    free((size_t*)o - 1);
+    size_t* ptr = (size_t*)o - 1;
+    free_sized(ptr, *ptr + sizeof(size_t));
 #endif
 }
 

diff --git a/src/library/module.cpp b/src/library/module.cpp
@@ -213,7 +213,7 @@ extern "C" LEAN_EXPORT object * lean_read_module_data(object * fname, object *)
 #endif
             buffer = static_cast<char *>(malloc(size - sizeof(olean_header)));
             free_data = [=]() {
-                free(buffer);
+                free_sized(buffer, size - sizeof(olean_header));
             };
             in.read(buffer, size - sizeof(olean_header));
             if (!in) {

diff --git a/src/runtime/alloc.cpp b/src/runtime/alloc.cpp
@@ -437,7 +437,7 @@ void dealloc(void * o, size_t sz) {
     LEAN_RUNTIME_STAT_CODE(g_num_dealloc++);
     sz = lean_align(sz, LEAN_OBJECT_SIZE_DELTA);
     if (LEAN_UNLIKELY(sz > LEAN_MAX_SMALL_OBJECT_SIZE)) {
-        return free(o);
+        return free_sized(o, sz);
     }
     dealloc_small_core(o);
 }

diff --git a/src/runtime/buffer.h b/src/runtime/buffer.h
@@ -27,7 +27,11 @@ class buffer {
 
     void free_memory() {
         if (m_buffer != reinterpret_cast<T*>(m_initial_buffer))
-            delete[] reinterpret_cast<char*>(m_buffer);
+            #if __cpp_sized_deallocation >= 201309L
+                operator delete[](reinterpret_cast<char*>(m_buffer), sizeof(T) * m_capacity);
+            #else
+                delete[] reinterpret_cast<char*>(m_buffer);
+            #endif
     }
 
     void set_capacity(size_t new_capacity) {

diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp
@@ -41,6 +41,12 @@ Author: Leonardo de Moura
 #define isinf(x) std::isinf(x)
 #endif
 
+#if !defined(__STDC_VERSION_STDLIB_H__) || __STDC_VERSION_STDLIB_H__ < 202311L
+extern "C" __attribute__((weak)) void free_sized(void *ptr, size_t) {
+    free(ptr);
+}
+#endif
+
 // see `Task.Priority.max`
 #define LEAN_MAX_PRIO 8
 
@@ -198,7 +204,7 @@ static inline void lean_dealloc(lean_object * o, size_t sz) {
 #ifdef LEAN_SMALL_ALLOCATOR
     dealloc(o, sz);
 #else
-    free(o);
+    free_sized(o, sz);
 #endif
 }