feat(CMakeLists, runtime): add CHECK_RC_OVERFLOW cmake option

src/CMakeLists.txt

@@ -36,6 +36,7 @@ option(JSON               "JSON"               ON)
 option(LLVM               "LLVM"               OFF)
 option(COMPRESSED_OBJECT_HEADER "Use compressed object headers in 64-bit machines, this option is ignored in 32-bit machines, and assumes the 64-bit OS can only address 2^48 bytes" ON)
 option(SMALL_RC "Use only 32-bits for RC, this option is only relevant when COMPRESSED_OBJECT_HEARDER is ON" ON)
+option(CHECK_RC_OVERFLOW "Check for RC overflows when SMALL_RC is ON" OFF)
 
 # When cross-compiling, we do not compile the standard library since
 # the executable will not work on the host machine
@@ -144,6 +145,10 @@ if ("${COMPRESSED_OBJECT_HEADER}" MATCHES "ON")
     if ("${SMALL_RC}" MATCHES "ON")
         set(LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC "#define LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC")
         message(STATUS "Using compressed object headers and only 32-bits for reference counter, this feature assume the OS only uses memory addresses < 2^48")
+        if ("${CHECK_RC_OVERFLOW}" MATCHES "ON")
+           set(LEAN_CHECK_RC_OVERFLOW "#define LEAN_CHECK_RC_OVERFLOW")
+           message(STATUS "RC overflow checks are enabled")
+        endif()
     else()
         set(LEAN_COMPRESSED_OBJECT_HEADER "#define LEAN_COMPRESSED_OBJECT_HEADER")
         message(STATUS "Using compressed object headers, this feature assume the OS only uses memory addresses < 2^48")

src/config.h.in

@@ -9,3 +9,4 @@ Author: Leonardo de Moura
 @LEAN_LAZY_RC@
 @LEAN_COMPRESSED_OBJECT_HEADER@
 @LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC@
+@LEAN_CHECK_RC_OVERFLOW@

src/runtime/lean.h

@@ -245,6 +245,7 @@ static inline size_t lean_unbox(lean_object * o) { return (size_t)(o) >> 1; }
 __attribute__((noreturn)) void lean_panic(char const * msg);
 __attribute__((noreturn)) void lean_panic_out_of_memory();
 __attribute__((noreturn)) void lean_panic_unreachable();
+__attribute__((noreturn)) void lean_panic_rc_overflow();
 
 static inline size_t lean_align(size_t v, size_t a) {
     return (v / a)*a + a * (v % a != 0);
@@ -359,13 +360,33 @@ static inline _Atomic(size_t) * lean_get_rc_mt_addr(lean_object* o) {
 }
 
 static inline void lean_inc_ref(lean_object * o) {
-#if defined(LEAN_COMPRESSED_OBJECT_HEADER) || defined(LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC)
+#if defined(LEAN_COMPRESSED_OBJECT_HEADER)
     if (LEAN_LIKELY(lean_is_st(o))) {
         o->m_header++;
     } else if (lean_is_mt(o)) {
         LEAN_USING_STD;
         atomic_fetch_add_explicit(lean_get_rc_mt_addr(o), (size_t)1, memory_order_relaxed);
     }
+#elif defined(LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC)
+    if (LEAN_LIKELY(lean_is_st(o))) {
+        o->m_header++;
+        #ifdef LEAN_CHECK_RC_OVERFLOW
+        if (LEAN_UNLIKELY(((uint32_t)o->m_header) == 0)) {
+            lean_panic_rc_overflow();
+        }
+        #endif
+    } else if (lean_is_mt(o)) {
+        LEAN_USING_STD;
+        #ifdef LEAN_CHECK_RC_OVERFLOW
+        uint32_t old_rc = (uint32_t)
+        #endif
+        atomic_fetch_add_explicit(lean_get_rc_mt_addr(o), (size_t)1, memory_order_relaxed);
+        #ifdef LEAN_CHECK_RC_OVERFLOW
+        if (LEAN_UNLIKELY(old_rc + 1 == 0)) {
+            lean_panic_rc_overflow();
+        }
+        #endif
+    }
 #else
     if (LEAN_LIKELY(lean_is_st(o))) {
         o->m_rc++;
@@ -377,13 +398,33 @@ static inline void lean_inc_ref(lean_object * o) {
 }
 
 static inline void lean_inc_ref_n(lean_object * o, size_t n) {
-#if defined(LEAN_COMPRESSED_OBJECT_HEADER) || defined(LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC)
+#if defined(LEAN_COMPRESSED_OBJECT_HEADER)
     if (LEAN_LIKELY(lean_is_st(o))) {
         o->m_header += n;
     } else if (lean_is_mt(o)) {
         LEAN_USING_STD;
         atomic_fetch_add_explicit(lean_get_rc_mt_addr(o), n, memory_order_relaxed);
     }
+#elif defined(LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC)
+    if (LEAN_LIKELY(lean_is_st(o))) {
+        o->m_header += n;
+        #ifdef LEAN_CHECK_RC_OVERFLOW
+        if (LEAN_UNLIKELY(((uint32_t)o->m_header) < n)) {
+            lean_panic_rc_overflow();
+        }
+        #endif
+    } else if (lean_is_mt(o)) {
+        LEAN_USING_STD;
+        #ifdef LEAN_CHECK_RC_OVERFLOW
+        uint32_t old_rc = (uint32_t)
+        #endif
+        atomic_fetch_add_explicit(lean_get_rc_mt_addr(o), n, memory_order_relaxed);
+        #ifdef LEAN_CHECK_RC_OVERFLOW
+        if (LEAN_UNLIKELY(old_rc + n < n)) {
+            lean_panic_rc_overflow();
+        }
+        #endif
+    }
 #else
     if (LEAN_LIKELY(lean_is_st(o))) {
         o->m_rc += n;

src/runtime/object.cpp

@@ -34,6 +34,10 @@ extern "C" void lean_panic_unreachable() {
     lean_panic("unreachable code has been reached");
 }
 
+extern "C" void lean_panic_rc_overflow() {
+    lean_panic("reference counter overflowed");
+}
+
 extern "C" size_t lean_object_byte_size(lean_object * o) {
     if (lean_is_mt(o) || lean_is_st(o) || lean_is_persistent(o)) {
         /* Recall that multi-threaded, single-threaded and persistent objects are stored in the heap.