From e3b1ae514bddfc3c290b730a817cc33a30f630eb Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 18 Aug 2020 18:43:49 -0700 Subject: [PATCH] fix: nontermination This issue was reported by Simon Winwood at Zulip. Here is the message The following code doesn't terminate (in a reasonable amount of time) ``` def large_nat : Nat := (9223372036854775807 : Nat) ``` $ time lean --o=large-nat.olean large-nat.lean --- src/runtime/compact.cpp | 7 ++++++- stage0/src/runtime/compact.cpp | 7 ++++++- 2 files changed, 12 insertions(+), 2 deletions(-) diff --git a/src/runtime/compact.cpp b/src/runtime/compact.cpp index 1469a69bd4..4b2f210235 100644 --- a/src/runtime/compact.cpp +++ b/src/runtime/compact.cpp @@ -73,7 +73,12 @@ object_compactor::~object_compactor() { free(m_begin); } -object_offset g_null_offset = reinterpret_cast(static_cast(-1)); +/* + Remark: g_null_offset must NOT be a valid Lean scalar value (e.g., static_cast(-1)). + Recall that Lean scalar are odd size_t values. So, we use (static_cast(-1) - 1) which is an even number. + In the past we used `static_cast(-1)`, and it caused nontermination in the object compactor. +*/ +object_offset g_null_offset = reinterpret_cast(static_cast(-1) - 1); void * object_compactor::alloc(size_t sz) { size_t rem = sz % sizeof(void*); diff --git a/stage0/src/runtime/compact.cpp b/stage0/src/runtime/compact.cpp index 1469a69bd4..4b2f210235 100644 --- a/stage0/src/runtime/compact.cpp +++ b/stage0/src/runtime/compact.cpp @@ -73,7 +73,12 @@ object_compactor::~object_compactor() { free(m_begin); } -object_offset g_null_offset = reinterpret_cast(static_cast(-1)); +/* + Remark: g_null_offset must NOT be a valid Lean scalar value (e.g., static_cast(-1)). + Recall that Lean scalar are odd size_t values. So, we use (static_cast(-1) - 1) which is an even number. + In the past we used `static_cast(-1)`, and it caused nontermination in the object compactor. +*/ +object_offset g_null_offset = reinterpret_cast(static_cast(-1) - 1); void * object_compactor::alloc(size_t sz) { size_t rem = sz % sizeof(void*);