From f40617d8dd49296b637df2126de4d229ffcfe54d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 28 Aug 2019 15:35:46 -0300 Subject: [PATCH] feat(CMakeLists, runtime): add `CHECK_RC_OVERFLOW` cmake option --- src/CMakeLists.txt | 5 +++++ src/config.h.in | 1 + src/runtime/lean.h | 45 ++++++++++++++++++++++++++++++++++++++++-- src/runtime/object.cpp | 4 ++++ 4 files changed, 53 insertions(+), 2 deletions(-) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 9e9441f896..deec3ab695 100644 --- a/src/CMakeLists.txt +++ b/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") diff --git a/src/config.h.in b/src/config.h.in index 08bd0e0667..d9f524afd8 100644 --- a/src/config.h.in +++ b/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@ diff --git a/src/runtime/lean.h b/src/runtime/lean.h index 687e3214cb..c48df6f9e4 100644 --- a/src/runtime/lean.h +++ b/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; diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp index 0da3f4c734..43775628b1 100644 --- a/src/runtime/object.cpp +++ b/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.