From 5107403d24f871902d80bc08f781faf8f2235b83 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 1 May 2020 16:47:52 +0200 Subject: [PATCH] feat: detect stack overflows on all platforms and threads --- src/runtime/stack_overflow.cpp | 102 +++++++++++------- src/runtime/stack_overflow.h | 13 +++ src/runtime/thread.cpp | 2 + tests/compiler/StackOverflow.lean | 3 + .../compiler/StackOverflow.lean.expected.out | 2 + .../compiler/StackOverflow.lean.expected.ret | 0 .../StackOverflow.lean.no_interpreter | 0 tests/compiler/StackOverflowTask.lean | 3 + .../StackOverflowTask.lean.expected.out | 2 + .../StackOverflowTask.lean.expected.ret | 0 .../StackOverflowTask.lean.no_interpreter | 0 11 files changed, 88 insertions(+), 39 deletions(-) create mode 100644 tests/compiler/StackOverflow.lean create mode 100644 tests/compiler/StackOverflow.lean.expected.out create mode 100644 tests/compiler/StackOverflow.lean.expected.ret create mode 100644 tests/compiler/StackOverflow.lean.no_interpreter create mode 100644 tests/compiler/StackOverflowTask.lean create mode 100644 tests/compiler/StackOverflowTask.lean.expected.out create mode 100644 tests/compiler/StackOverflowTask.lean.expected.ret create mode 100644 tests/compiler/StackOverflowTask.lean.no_interpreter diff --git a/src/runtime/stack_overflow.cpp b/src/runtime/stack_overflow.cpp index 9cec107d03..61cb201f00 100644 --- a/src/runtime/stack_overflow.cpp +++ b/src/runtime/stack_overflow.cpp @@ -4,38 +4,66 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Sebastian Ullrich -Install a segfault signal handler and abort with custom message if address is within stack guard. -Inspired by https://github.com/rust-lang/rust/blob/master/src/libstd/sys/unix/stack_overflow.rs +Print a nicer error message on stack overflow. +Port of the corresponding Rust code (see links below). */ -#if !defined(LEAN_WINDOWS) && !defined(__APPLE__) +#ifdef LEAN_WINDOWS +#include +#else #include +#include +#include +#endif #include #include #include -#include -#include +#include "runtime/stack_overflow.h" namespace lean { -// signal stack of the main thread -static stack_t g_signal_stack; +// stack guard of the main thread +static stack_guard * g_stack_guard; + +#ifdef LEAN_WINDOWS +// https://github.com/rust-lang/rust/blob/master/src/libstd/sys/windows/stack_overflow.rs + +LONG WINAPI stack_overflow_handler(struct _EXCEPTION_POINTERS * info) { + if (info->ExceptionRecord->ExceptionCode == EXCEPTION_STACK_OVERFLOW) { + fprintf(stderr, "\nStack overflow detected. Aborting.\n"); + abort(); + } else { + return EXCEPTION_CONTINUE_SEARCH; + } +} + +stack_guard::stack_guard() { + // reserve some stack space for the handler + ULONG sz = 0x5000; + SetThreadStackGuarantee(&sz); +} + +stack_guard::~stack_guard() {} +#else +// Install a segfault signal handler and abort with custom message if address is within stack guard. +// https://github.com/rust-lang/rust/blob/master/src/libstd/sys/unix/stack_overflow.rs + // https://github.com/rust-lang/rust/blob/7c8dbd969dd0ef2af6d8bab9e03ba7ce6cac41a2/src/libstd/sys/unix/thread.rs#L293 bool is_within_stack_guard(void * addr) { + char * stackaddr; +#ifdef __APPLE__ + stackaddr = static_cast(pthread_get_stackaddr_np(pthread_self())) - pthread_get_stacksize_np(pthread_self()); +#else pthread_attr_t attr; if (pthread_attr_init(&attr) != 0) return false; pthread_getattr_np(pthread_self(), &attr); - void * stackaddr; - size_t stacksize, guardsize; - pthread_attr_getstack(&attr, &stackaddr, &stacksize); - pthread_attr_getguardsize(&attr, &guardsize); + size_t stacksize; + pthread_attr_getstack(&attr, reinterpret_cast(&stackaddr), &stacksize); pthread_attr_destroy(&attr); - if (guardsize == 0) { - // probably the main thread, make an educated guess - // https://github.com/rust-lang/rust/blob/7c8dbd969dd0ef2af6d8bab9e03ba7ce6cac41a2/src/libstd/sys/unix/thread.rs#L343-L347 - guardsize = static_cast(sysconf(_SC_PAGESIZE)); - } +#endif + // close enough; the actual guard might be bigger, but it's unlikely a Lean function will have stack frames that big + size_t guardsize = static_cast(sysconf(_SC_PAGESIZE)); // the stack guard is *below* the stack - return stackaddr > addr && addr >= static_cast(stackaddr) - guardsize; + return stackaddr - guardsize <= addr && addr < stackaddr; } extern "C" void segv_handler(int signum, siginfo_t * info, void *) { @@ -51,40 +79,36 @@ extern "C" void segv_handler(int signum, siginfo_t * info, void *) { } } -// We need a separate signal stack since we can't use the overflowed stack -void setup_signal_stack(stack_t & stack) { - stack.ss_sp = malloc(SIGSTKSZ); - if (stack.ss_sp == nullptr) return; - stack.ss_size = SIGSTKSZ; - stack.ss_flags = 0; - sigaltstack(&stack, nullptr); +stack_guard::stack_guard() { + m_signal_stack.ss_sp = malloc(SIGSTKSZ); + if (m_signal_stack.ss_sp == nullptr) return; + m_signal_stack.ss_size = SIGSTKSZ; + m_signal_stack.ss_flags = 0; + sigaltstack(&m_signal_stack, nullptr); } -void free_signal_stack(stack_t & stack) { - if (!stack.ss_sp) { - return; - } - stack.ss_flags = SS_DISABLE; - sigaltstack(&stack, nullptr); - free(stack.ss_sp); +stack_guard::~stack_guard() { + if (!m_signal_stack.ss_sp) return; + m_signal_stack.ss_flags = SS_DISABLE; + sigaltstack(&m_signal_stack, nullptr); + free(m_signal_stack.ss_sp); } +#endif void initialize_stack_overflow() { - setup_signal_stack(g_signal_stack); + g_stack_guard = new stack_guard(); +#ifdef LEAN_WINDOWS + AddVectoredExceptionHandler(0, stack_overflow_handler); +#else struct sigaction action; memset(&action, 0, sizeof(struct sigaction)); action.sa_flags = SA_SIGINFO | SA_ONSTACK; action.sa_sigaction = segv_handler; sigaction(SIGSEGV, &action, nullptr); +#endif } void finalize_stack_overflow() { - free_signal_stack(g_signal_stack); + delete g_stack_guard; } } -#else -namespace lean { -void initialize_stack_overflow() {} -void finalize_stack_overflow() {} -} -#endif diff --git a/src/runtime/stack_overflow.h b/src/runtime/stack_overflow.h index 1447233a53..1d09d6a80e 100644 --- a/src/runtime/stack_overflow.h +++ b/src/runtime/stack_overflow.h @@ -5,8 +5,21 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Sebastian Ullrich */ #pragma once +#ifndef LEAN_WINDOWS +#include +#endif namespace lean { +class stack_guard { +#ifndef LEAN_WINDOWS + // We need a separate signal stack since we can't use the overflowed stack + stack_t m_signal_stack; +#endif +public: + stack_guard(); + ~stack_guard(); +}; + void initialize_stack_overflow(); void finalize_stack_overflow(); } diff --git a/src/runtime/thread.cpp b/src/runtime/thread.cpp index 33202cfa31..23dffb6dac 100644 --- a/src/runtime/thread.cpp +++ b/src/runtime/thread.cpp @@ -17,6 +17,7 @@ Author: Leonardo de Moura #include "runtime/interrupt.h" #include "runtime/exception.h" #include "runtime/alloc.h" +#include "runtime/stack_overflow.h" #ifndef LEAN_DEFAULT_THREAD_STACK_SIZE #define LEAN_DEFAULT_THREAD_STACK_SIZE 8*1024*1024 // 8Mb @@ -108,6 +109,7 @@ struct lthread::imp { bool m_joined = false; static void * _main(void * p) { + stack_guard guard; thread_main(p); return nullptr; } diff --git a/tests/compiler/StackOverflow.lean b/tests/compiler/StackOverflow.lean new file mode 100644 index 0000000000..e495adbe68 --- /dev/null +++ b/tests/compiler/StackOverflow.lean @@ -0,0 +1,3 @@ +partial def foo : Nat → Nat | n => foo n + 1 +@[neverExtract] +def main : IO Unit := IO.println $ foo 0 diff --git a/tests/compiler/StackOverflow.lean.expected.out b/tests/compiler/StackOverflow.lean.expected.out new file mode 100644 index 0000000000..af0b90964f --- /dev/null +++ b/tests/compiler/StackOverflow.lean.expected.out @@ -0,0 +1,2 @@ + +Stack overflow detected. Aborting. diff --git a/tests/compiler/StackOverflow.lean.expected.ret b/tests/compiler/StackOverflow.lean.expected.ret new file mode 100644 index 0000000000..e69de29bb2 diff --git a/tests/compiler/StackOverflow.lean.no_interpreter b/tests/compiler/StackOverflow.lean.no_interpreter new file mode 100644 index 0000000000..e69de29bb2 diff --git a/tests/compiler/StackOverflowTask.lean b/tests/compiler/StackOverflowTask.lean new file mode 100644 index 0000000000..2006c37ac3 --- /dev/null +++ b/tests/compiler/StackOverflowTask.lean @@ -0,0 +1,3 @@ +partial def foo : Nat → Nat | n => foo n + 1 +@[neverExtract] +def main : IO Unit := IO.println $ Task.get $ Task.mk $ fun _ => foo 0 diff --git a/tests/compiler/StackOverflowTask.lean.expected.out b/tests/compiler/StackOverflowTask.lean.expected.out new file mode 100644 index 0000000000..af0b90964f --- /dev/null +++ b/tests/compiler/StackOverflowTask.lean.expected.out @@ -0,0 +1,2 @@ + +Stack overflow detected. Aborting. diff --git a/tests/compiler/StackOverflowTask.lean.expected.ret b/tests/compiler/StackOverflowTask.lean.expected.ret new file mode 100644 index 0000000000..e69de29bb2 diff --git a/tests/compiler/StackOverflowTask.lean.no_interpreter b/tests/compiler/StackOverflowTask.lean.no_interpreter new file mode 100644 index 0000000000..e69de29bb2