chore: revert "perf: use C23's free_sized when available" (#6841)

Reverts leanprover/lean4#6598, which broke Windows CI
leanprover · Jan 29, 2025 · a35bf7e · a35bf7e
1 parent bc234f9
commit a35bf7e
Show file tree

Hide file tree

Showing 5 changed files with 5 additions and 20 deletions.
diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h
@@ -380,16 +380,11 @@ 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
-    size_t* ptr = (size_t*)o - 1;
-    free_sized(ptr, *ptr + sizeof(size_t));
+    free((size_t*)o - 1);
 #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_sized(buffer, size - sizeof(olean_header));
+                free(buffer);
             };
             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_sized(o, sz);
+        return free(o);
     }
     dealloc_small_core(o);
 }

diff --git a/src/runtime/buffer.h b/src/runtime/buffer.h
@@ -27,11 +27,7 @@ class buffer {
 
     void free_memory() {
         if (m_buffer != reinterpret_cast<T*>(m_initial_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
+            delete[] reinterpret_cast<char*>(m_buffer);
     }
 
     void set_capacity(size_t new_capacity) {

diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp
@@ -41,12 +41,6 @@ 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
 
@@ -204,7 +198,7 @@ static inline void lean_dealloc(lean_object * o, size_t sz) {
 #ifdef LEAN_SMALL_ALLOCATOR
     dealloc(o, sz);
 #else
-    free_sized(o, sz);
+    free(o);
 #endif
 }