From 74dfdd02deb08542e16d74759799cfbb99f32743 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 1 Dec 2013 12:42:32 -0800 Subject: [PATCH] feat(util): add primitives for checking the amount of available stack space Recursive functions that may go very deep should invoke the function check_stack. It throws an exception if the amount of stack space is limited. The function check_system() is syntax sugar for check_interrupted(); check_stack(); Signed-off-by: Leonardo de Moura --- src/CMakeLists.txt | 5 +- src/kernel/normalizer.cpp | 2 +- src/kernel/type_checker.cpp | 2 +- src/library/type_inferer.cpp | 2 +- src/shell/lean.cpp | 2 + src/tests/frontends/lean/frontend.cpp | 1 + src/tests/frontends/lean/parser.cpp | 1 + src/tests/frontends/lean/pp.cpp | 1 + src/tests/frontends/lean/scanner.cpp | 1 + src/tests/kernel/CMakeLists.txt | 3 - src/tests/kernel/arith.cpp | 106 -------------------- src/tests/kernel/environment.cpp | 1 + src/tests/kernel/metavar.cpp | 1 + src/tests/kernel/normalizer.cpp | 1 + src/tests/kernel/threads.cpp | 3 +- src/tests/kernel/type_checker.cpp | 2 +- src/tests/library/arith.cpp | 102 ++++++++++++++++++- src/tests/library/elaborator/elaborator.cpp | 1 + src/tests/library/formatter.cpp | 1 + src/tests/library/rewriter/rewriter.cpp | 2 + src/tests/library/tactic/tactic.cpp | 1 + src/tests/library/type_inferer.cpp | 1 + src/tests/util/CMakeLists.txt | 3 + src/tests/util/lazy_list.cpp | 1 + src/tests/util/stackinfo.cpp | 30 ++++++ src/tests/util/thread.cpp | 1 + src/util/CMakeLists.txt | 2 +- src/util/exception.h | 12 ++- src/util/interrupt.h | 4 + src/util/lazy_list_fn.h | 16 +-- src/util/stackinfo.cpp | 58 +++++++++++ src/util/stackinfo.h | 17 ++++ src/util/test.h | 1 + 33 files changed, 253 insertions(+), 134 deletions(-) delete mode 100644 src/tests/kernel/arith.cpp create mode 100644 src/tests/util/stackinfo.cpp create mode 100644 src/util/stackinfo.cpp create mode 100644 src/util/stackinfo.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index ed99fb269..17aca5f79 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -20,9 +20,10 @@ set(LEAN_EXTRA_CXX_FLAGS "") # Windows does not support ulimit -s unlimited. So, we reserve a lot of stack space: 100Mb if((${CYGWIN} EQUAL "1") OR (${CMAKE_SYSTEM_NAME} MATCHES "Windows")) message(STATUS "Windows detected") - set(LEAN_EXTRA_LINKER_FLAGS "${LEAN_EXTRA_LINKER_FLAGS} -Wl,--stack,104857600") + set(LEAN_WIN_STACK_SIZE "104857600") + set(LEAN_EXTRA_LINKER_FLAGS "${LEAN_EXTRA_LINKER_FLAGS} -Wl,--stack,${LEAN_WIN_STACK_SIZE}") set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_DEFAULT_PP_UNICODE=false") - set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_WINDOWS") + set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_WINDOWS -D LEAN_WIN_STACK_SIZE=${LEAN_WIN_STACK_SIZE}") endif() if("${THREAD_SAFE}" MATCHES "OFF") diff --git a/src/kernel/normalizer.cpp b/src/kernel/normalizer.cpp index 5c11ecf6f..63537d0d9 100644 --- a/src/kernel/normalizer.cpp +++ b/src/kernel/normalizer.cpp @@ -179,7 +179,7 @@ class normalizer::imp { /** \brief Normalize the expression \c a in a context composed of stack \c s and \c k binders. */ svalue normalize(expr const & a, value_stack const & s, unsigned k) { flet l(m_depth, m_depth+1); - check_interrupted(); + check_system(); if (m_depth > m_max_depth) throw kernel_exception(env(), "normalizer maximum recursion depth exceeded"); bool shared = false; diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index b25eb2b1e..43e3750a6 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -85,7 +85,7 @@ class type_checker::imp { } expr infer_type_core(expr const & e, context const & ctx) { - check_interrupted(); + check_system(); bool shared = false; if (is_shared(e)) { shared = true; diff --git a/src/library/type_inferer.cpp b/src/library/type_inferer.cpp index 8cfb98411..8e9171662 100644 --- a/src/library/type_inferer.cpp +++ b/src/library/type_inferer.cpp @@ -144,7 +144,7 @@ class type_inferer::imp { break; // expensive cases } - check_interrupted(); + check_system(); bool shared = false; if (is_shared(e)) { shared = true; diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index 1d76d6760..528ef4f32 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include #include #include +#include "util/stackinfo.h" #include "util/debug.h" #include "util/interrupt.h" #include "util/script_state.h" @@ -68,6 +69,7 @@ static struct option g_long_options[] = { }; int main(int argc, char ** argv) { + lean::save_stack_info(); lean::register_modules(); input_kind default_k = input_kind::Lean; // default int optind = 1; diff --git a/src/tests/frontends/lean/frontend.cpp b/src/tests/frontends/lean/frontend.cpp index bcb8bd616..381a0aa35 100644 --- a/src/tests/frontends/lean/frontend.cpp +++ b/src/tests/frontends/lean/frontend.cpp @@ -205,6 +205,7 @@ static void tst11() { } int main() { + save_stack_info(); tst1(); tst2(); tst3(); diff --git a/src/tests/frontends/lean/parser.cpp b/src/tests/frontends/lean/parser.cpp index 826bef815..4f1daa8b0 100644 --- a/src/tests/frontends/lean/parser.cpp +++ b/src/tests/frontends/lean/parser.cpp @@ -106,6 +106,7 @@ static void tst3() { } int main() { + save_stack_info(); tst1(); tst2(); tst3(); diff --git a/src/tests/frontends/lean/pp.cpp b/src/tests/frontends/lean/pp.cpp index 018e64ac2..c1f66f51b 100644 --- a/src/tests/frontends/lean/pp.cpp +++ b/src/tests/frontends/lean/pp.cpp @@ -103,6 +103,7 @@ static void tst6() { } int main() { + save_stack_info(); tst1(); tst2(); tst3(); diff --git a/src/tests/frontends/lean/scanner.cpp b/src/tests/frontends/lean/scanner.cpp index d293f3259..24c1339c9 100644 --- a/src/tests/frontends/lean/scanner.cpp +++ b/src/tests/frontends/lean/scanner.cpp @@ -119,6 +119,7 @@ static void tst3() { } int main() { + save_stack_info(); tst1(); tst2(); tst3(); diff --git a/src/tests/kernel/CMakeLists.txt b/src/tests/kernel/CMakeLists.txt index a8635a454..967d077b3 100644 --- a/src/tests/kernel/CMakeLists.txt +++ b/src/tests/kernel/CMakeLists.txt @@ -19,9 +19,6 @@ add_test(replace ${CMAKE_CURRENT_BINARY_DIR}/replace) add_executable(type_checker type_checker.cpp) target_link_libraries(type_checker ${EXTRA_LIBS}) add_test(type_checker ${CMAKE_CURRENT_BINARY_DIR}/type_checker) -add_executable(arith arith.cpp) -target_link_libraries(arith ${EXTRA_LIBS}) -add_test(arith ${CMAKE_CURRENT_BINARY_DIR}/arith) add_executable(environment environment.cpp) target_link_libraries(environment ${EXTRA_LIBS}) add_test(environment ${CMAKE_CURRENT_BINARY_DIR}/environment) diff --git a/src/tests/kernel/arith.cpp b/src/tests/kernel/arith.cpp deleted file mode 100644 index baa380d12..000000000 --- a/src/tests/kernel/arith.cpp +++ /dev/null @@ -1,106 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include "util/test.h" -#include "kernel/environment.h" -#include "kernel/type_checker.h" -#include "kernel/builtin.h" -#include "kernel/normalizer.h" -#include "kernel/abstract.h" -#include "kernel/printer.h" -#include "library/arith/arith.h" -#include "library/all/all.h" -using namespace lean; - -static void tst1() { - environment env = mk_toplevel(); - expr e = mk_int_value(mpz(10)); - lean_assert(is_int_value(e)); - lean_assert(infer_type(e, env) == Int); - std::cout << "e: " << e << "\n"; -} - -static void tst2() { - environment env = mk_toplevel(); - expr e = iAdd(iVal(10), iVal(30)); - std::cout << e << "\n"; - std::cout << normalize(e, env) << "\n"; - lean_assert(normalize(e, env) == iVal(40)); - std::cout << infer_type(mk_int_add_fn(), env) << "\n"; - lean_assert(infer_type(e, env) == Int); - lean_assert(infer_type(mk_app(mk_int_add_fn(), iVal(10)), env) == (Int >> Int)); - lean_assert(is_int_value(normalize(e, env))); - expr e2 = Fun("a", Int, iAdd(Const("a"), iAdd(iVal(10), iVal(30)))); - std::cout << e2 << " --> " << normalize(e2, env) << "\n"; - lean_assert(infer_type(e2, env) == mk_arrow(Int, Int)); - lean_assert(normalize(e2, env) == Fun("a", Int, iAdd(Const("a"), iVal(40)))); -} - -static void tst3() { - environment env = mk_toplevel(); - expr e = iMul(iVal(10), iVal(30)); - std::cout << e << "\n"; - std::cout << normalize(e, env) << "\n"; - lean_assert(normalize(e, env) == iVal(300)); - std::cout << infer_type(mk_int_mul_fn(), env) << "\n"; - lean_assert(infer_type(e, env) == Int); - lean_assert(infer_type(mk_app(mk_int_mul_fn(), iVal(10)), env) == mk_arrow(Int, Int)); - lean_assert(is_int_value(normalize(e, env))); - expr e2 = Fun("a", Int, iMul(Const("a"), iMul(iVal(10), iVal(30)))); - std::cout << e2 << " --> " << normalize(e2, env) << "\n"; - lean_assert(infer_type(e2, env) == (Int >> Int)); - lean_assert(normalize(e2, env) == Fun("a", Int, iMul(Const("a"), iVal(300)))); -} - -static void tst4() { - environment env = mk_toplevel(); - expr e = iSub(iVal(10), iVal(30)); - std::cout << e << "\n"; - std::cout << normalize(e, env) << "\n"; - lean_assert(normalize(e, env) == iVal(-20)); - std::cout << infer_type(mk_int_sub_fn(), env) << "\n"; - lean_assert(infer_type(e, env) == Int); - lean_assert(infer_type(mk_app(mk_int_sub_fn(), iVal(10)), env) == mk_arrow(Int, Int)); - lean_assert(is_int_value(normalize(e, env))); - expr e2 = Fun("a", Int, iSub(Const("a"), iSub(iVal(10), iVal(30)))); - std::cout << e2 << " --> " << normalize(e2, env) << "\n"; - lean_assert(infer_type(e2, env) == (Int >> Int)); - lean_assert(normalize(e2, env) == Fun("a", Int, iAdd(Const("a"), iVal(20)))); -} - -static void tst5() { - environment env = mk_toplevel(); - env.add_var(name("a"), Int); - expr e = Eq(iVal(3), iVal(4)); - std::cout << e << " --> " << normalize(e, env) << "\n"; - lean_assert(normalize(e, env) == False); - lean_assert(normalize(Eq(Const("a"), iVal(3)), env) == Eq(Const("a"), iVal(3))); -} - -static void tst6() { - std::cout << "tst6\n"; - std::cout << mk_int_add_fn().raw() << "\n"; - std::cout << mk_int_add_fn().raw() << "\n"; - - #ifndef __APPLE__ - std::thread t1([](){ std::cout << "t1: " << mk_int_add_fn().raw() << "\n"; }); - t1.join(); - std::thread t2([](){ std::cout << "t2: " << mk_int_add_fn().raw() << "\n"; }); - t2.join(); - #endif - std::cout << mk_int_add_fn().raw() << "\n"; -} - -int main() { - tst1(); - tst2(); - tst3(); - tst4(); - tst5(); - tst6(); - return has_violations() ? 1 : 0; -} diff --git a/src/tests/kernel/environment.cpp b/src/tests/kernel/environment.cpp index 18a2e8ff1..851b403e3 100644 --- a/src/tests/kernel/environment.cpp +++ b/src/tests/kernel/environment.cpp @@ -283,6 +283,7 @@ static void tst13() { } int main() { + save_stack_info(); enable_trace("is_convertible"); tst1(); tst2(); diff --git a/src/tests/kernel/metavar.cpp b/src/tests/kernel/metavar.cpp index 309bc102b..49beab810 100644 --- a/src/tests/kernel/metavar.cpp +++ b/src/tests/kernel/metavar.cpp @@ -594,6 +594,7 @@ static void tst27() { } int main() { + save_stack_info(); tst1(); tst2(); tst3(); diff --git a/src/tests/kernel/normalizer.cpp b/src/tests/kernel/normalizer.cpp index 01af51631..ce999ffe9 100644 --- a/src/tests/kernel/normalizer.cpp +++ b/src/tests/kernel/normalizer.cpp @@ -250,6 +250,7 @@ static void tst6() { } int main() { + save_stack_info(); tst_church_numbers(); tst1(); tst2(); diff --git a/src/tests/kernel/threads.cpp b/src/tests/kernel/threads.cpp index b1bdfee22..d81188079 100644 --- a/src/tests/kernel/threads.cpp +++ b/src/tests/kernel/threads.cpp @@ -52,7 +52,7 @@ static void tst1() { #ifndef __APPLE__ for (unsigned i = 0; i < 8; i++) { - ts.push_back(std::thread([&](){ mk(a); })); + ts.push_back(std::thread([&](){ save_stack_info(); mk(a); })); } for (unsigned i = 0; i < 8; i++) { ts[i].join(); @@ -64,6 +64,7 @@ static void tst1() { } int main() { + save_stack_info(); tst1(); return 0; } diff --git a/src/tests/kernel/type_checker.cpp b/src/tests/kernel/type_checker.cpp index 84beee6f5..e94f5d279 100644 --- a/src/tests/kernel/type_checker.cpp +++ b/src/tests/kernel/type_checker.cpp @@ -325,7 +325,7 @@ static void tst16() { } int main() { - tst15(); return 0; + save_stack_info(); tst1(); tst2(); tst3(); diff --git a/src/tests/library/arith.cpp b/src/tests/library/arith.cpp index 0eb1eb2d0..dfffb1dbc 100644 --- a/src/tests/library/arith.cpp +++ b/src/tests/library/arith.cpp @@ -4,13 +4,17 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include #include "util/test.h" #include "kernel/builtin.h" #include "kernel/normalizer.h" +#include "kernel/type_checker.h" +#include "kernel/abstract.h" #include "library/arith/arith.h" +#include "library/all/all.h" using namespace lean; -static void tst1() { +static void tst0() { environment env; normalizer norm(env); import_basic(env); @@ -42,8 +46,98 @@ static void tst1() { lean_assert_eq(norm(iDiv(iVal(2), iVal(0))), iVal(0)); } -int main() { - tst1(); - return has_violations() ? 1 : 0; +static void tst1() { + environment env; + import_all(env); + expr e = mk_int_value(mpz(10)); + lean_assert(is_int_value(e)); + lean_assert(infer_type(e, env) == Int); + std::cout << "e: " << e << "\n"; } +static void tst2() { + environment env; + import_all(env); + expr e = iAdd(iVal(10), iVal(30)); + std::cout << e << "\n"; + std::cout << normalize(e, env) << "\n"; + lean_assert(normalize(e, env) == iVal(40)); + std::cout << infer_type(mk_int_add_fn(), env) << "\n"; + lean_assert(infer_type(e, env) == Int); + lean_assert(infer_type(mk_app(mk_int_add_fn(), iVal(10)), env) == (Int >> Int)); + lean_assert(is_int_value(normalize(e, env))); + expr e2 = Fun("a", Int, iAdd(Const("a"), iAdd(iVal(10), iVal(30)))); + std::cout << e2 << " --> " << normalize(e2, env) << "\n"; + lean_assert(infer_type(e2, env) == mk_arrow(Int, Int)); + lean_assert(normalize(e2, env) == Fun("a", Int, iAdd(Const("a"), iVal(40)))); +} + +static void tst3() { + environment env; + import_all(env); + expr e = iMul(iVal(10), iVal(30)); + std::cout << e << "\n"; + std::cout << normalize(e, env) << "\n"; + lean_assert(normalize(e, env) == iVal(300)); + std::cout << infer_type(mk_int_mul_fn(), env) << "\n"; + lean_assert(infer_type(e, env) == Int); + lean_assert(infer_type(mk_app(mk_int_mul_fn(), iVal(10)), env) == mk_arrow(Int, Int)); + lean_assert(is_int_value(normalize(e, env))); + expr e2 = Fun("a", Int, iMul(Const("a"), iMul(iVal(10), iVal(30)))); + std::cout << e2 << " --> " << normalize(e2, env) << "\n"; + lean_assert(infer_type(e2, env) == (Int >> Int)); + lean_assert(normalize(e2, env) == Fun("a", Int, iMul(Const("a"), iVal(300)))); +} + +static void tst4() { + environment env; + import_all(env); + expr e = iSub(iVal(10), iVal(30)); + std::cout << e << "\n"; + std::cout << normalize(e, env) << "\n"; + lean_assert(normalize(e, env) == iVal(-20)); + std::cout << infer_type(mk_int_sub_fn(), env) << "\n"; + lean_assert(infer_type(e, env) == Int); + lean_assert(infer_type(mk_app(mk_int_sub_fn(), iVal(10)), env) == mk_arrow(Int, Int)); + lean_assert(is_int_value(normalize(e, env))); + expr e2 = Fun("a", Int, iSub(Const("a"), iSub(iVal(10), iVal(30)))); + std::cout << e2 << " --> " << normalize(e2, env) << "\n"; + lean_assert(infer_type(e2, env) == (Int >> Int)); + lean_assert(normalize(e2, env) == Fun("a", Int, iAdd(Const("a"), iVal(20)))); +} + +static void tst5() { + environment env; + import_all(env); + env.add_var(name("a"), Int); + expr e = Eq(iVal(3), iVal(4)); + std::cout << e << " --> " << normalize(e, env) << "\n"; + lean_assert(normalize(e, env) == False); + lean_assert(normalize(Eq(Const("a"), iVal(3)), env) == Eq(Const("a"), iVal(3))); +} + +static void tst6() { + std::cout << "tst6\n"; + std::cout << mk_int_add_fn().raw() << "\n"; + std::cout << mk_int_add_fn().raw() << "\n"; + + #ifndef __APPLE__ + std::thread t1([](){ save_stack_info(); std::cout << "t1: " << mk_int_add_fn().raw() << "\n"; }); + t1.join(); + std::thread t2([](){ save_stack_info(); std::cout << "t2: " << mk_int_add_fn().raw() << "\n"; }); + t2.join(); + #endif + std::cout << mk_int_add_fn().raw() << "\n"; +} + +int main() { + save_stack_info(); + tst0(); + tst1(); + tst2(); + tst3(); + tst4(); + tst5(); + tst6(); + return has_violations() ? 1 : 0; +} diff --git a/src/tests/library/elaborator/elaborator.cpp b/src/tests/library/elaborator/elaborator.cpp index 6a0927259..899c29d52 100644 --- a/src/tests/library/elaborator/elaborator.cpp +++ b/src/tests/library/elaborator/elaborator.cpp @@ -874,6 +874,7 @@ void tst27() { } int main() { + save_stack_info(); tst1(); tst2(); tst3(); diff --git a/src/tests/library/formatter.cpp b/src/tests/library/formatter.cpp index 6dd87cdd6..9261d2075 100644 --- a/src/tests/library/formatter.cpp +++ b/src/tests/library/formatter.cpp @@ -42,6 +42,7 @@ static void tst1() { } int main() { + save_stack_info(); tst1(); return has_violations() ? 1 : 0; } diff --git a/src/tests/library/rewriter/rewriter.cpp b/src/tests/library/rewriter/rewriter.cpp index ce8d16a3b..c06d3abf9 100644 --- a/src/tests/library/rewriter/rewriter.cpp +++ b/src/tests/library/rewriter/rewriter.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Soonho Kong */ +#include "util/test.h" #include "util/trace.h" #include "kernel/abstract.h" #include "kernel/context.h" @@ -638,6 +639,7 @@ static void depth_rewriter1_tst() { } int main() { + save_stack_info(); theorem_rewriter1_tst(); theorem_rewriter2_tst(); then_rewriter1_tst(); diff --git a/src/tests/library/tactic/tactic.cpp b/src/tests/library/tactic/tactic.cpp index 7f00f6ac8..0cf56df46 100644 --- a/src/tests/library/tactic/tactic.cpp +++ b/src/tests/library/tactic/tactic.cpp @@ -144,6 +144,7 @@ static void tst2() { } int main() { + save_stack_info(); tst1(); tst2(); return has_violations() ? 1 : 0; diff --git a/src/tests/library/type_inferer.cpp b/src/tests/library/type_inferer.cpp index 2a26acc1e..ec53d3bed 100644 --- a/src/tests/library/type_inferer.cpp +++ b/src/tests/library/type_inferer.cpp @@ -138,6 +138,7 @@ static void tst4() { } int main() { + save_stack_info(); tst1(); tst2(); tst3(); diff --git a/src/tests/util/CMakeLists.txt b/src/tests/util/CMakeLists.txt index c42485039..7e4dcc74c 100644 --- a/src/tests/util/CMakeLists.txt +++ b/src/tests/util/CMakeLists.txt @@ -64,3 +64,6 @@ add_test(set ${CMAKE_CURRENT_BINARY_DIR}/set) add_executable(optional optional.cpp) target_link_libraries(optional ${EXTRA_LIBS}) add_test(optional ${CMAKE_CURRENT_BINARY_DIR}/optional) +add_executable(stackinfo stackinfo.cpp) +target_link_libraries(stackinfo ${EXTRA_LIBS}) +add_test(stackinfo ${CMAKE_CURRENT_BINARY_DIR}/stackinfo) diff --git a/src/tests/util/lazy_list.cpp b/src/tests/util/lazy_list.cpp index ab76ccc2d..78d845417 100644 --- a/src/tests/util/lazy_list.cpp +++ b/src/tests/util/lazy_list.cpp @@ -169,6 +169,7 @@ static void tst4() { } int main() { + save_stack_info(); tst1(); tst2(); tst3(); diff --git a/src/tests/util/stackinfo.cpp b/src/tests/util/stackinfo.cpp new file mode 100644 index 000000000..8c6bc2de8 --- /dev/null +++ b/src/tests/util/stackinfo.cpp @@ -0,0 +1,30 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include +#include "util/test.h" +#include "util/stackinfo.h" +using namespace lean; + +static char foo(int i) { + #define SZ 1000000 + char buffer[SZ]; + buffer[i] = i; + std::cout << get_available_stack_size() << "\n"; + return buffer[i]; +} + +static void tst1() { + std::cout << get_available_stack_size() << "\n"; + foo(10); + std::cout << get_available_stack_size() << "\n"; +} + +int main() { + save_stack_info(); + tst1(); + return has_violations() ? 1 : 0; +} diff --git a/src/tests/util/thread.cpp b/src/tests/util/thread.cpp index 9fe4b9d97..14bbe1b38 100644 --- a/src/tests/util/thread.cpp +++ b/src/tests/util/thread.cpp @@ -181,6 +181,7 @@ static void tst6() {} #endif int main() { + save_stack_info(); tst1(); tst2(); tst3(); diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index 3d09b4622..9996a53b6 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -2,6 +2,6 @@ add_library(util trace.cpp debug.cpp name.cpp name_set.cpp exception.cpp interrupt.cpp hash.cpp escaped.cpp bit_tricks.cpp safe_arith.cpp ascii.cpp memory.cpp shared_mutex.cpp realpath.cpp script_state.cpp script_exception.cpp splay_map.cpp lua.cpp - luaref.cpp) + luaref.cpp stackinfo.cpp) target_link_libraries(util ${LEAN_LIBS}) diff --git a/src/util/exception.h b/src/util/exception.h index 20dab89a2..0725b4df3 100644 --- a/src/util/exception.h +++ b/src/util/exception.h @@ -50,11 +50,13 @@ public: virtual exception * clone() const { return new interrupted(); } virtual void rethrow() const { throw *this; } }; -/** \brief Throw interrupted exception iff flag is true. */ -inline void check_interrupted(bool flag) { - if (flag) - throw interrupted(); -} +class stack_space_exception : public exception { +public: + stack_space_exception() {} + virtual char const * what() const noexcept { return "deep recursion was detected (potential solution: increase stack space in your system)"; } + virtual exception * clone() const { return new stack_space_exception(); } + virtual void rethrow() const { throw *this; } +}; int push_exception(lua_State * L, exception const & e); exception const & to_exception(lua_State * L, int i); bool is_exception(lua_State * L, int i); diff --git a/src/util/interrupt.h b/src/util/interrupt.h index 7e2adc280..c916b930b 100644 --- a/src/util/interrupt.h +++ b/src/util/interrupt.h @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include #include #include +#include "util/stackinfo.h" namespace lean { /** @@ -29,6 +30,8 @@ bool interrupt_requested(); */ void check_interrupted(); +inline void check_system() { check_stack(); check_interrupted(); } + constexpr unsigned g_small_sleep = 50; /** @@ -68,6 +71,7 @@ public: m_thread( [&](Function&& fun, Args&&... args) { m_flag_addr.store(get_flag_addr()); + save_stack_info(); fun(std::forward(args)...); m_flag_addr.store(&m_dummy_addr); // see comment before m_dummy_addr }, diff --git a/src/util/lazy_list_fn.h b/src/util/lazy_list_fn.h index c08c38fec..de5bdff3b 100644 --- a/src/util/lazy_list_fn.h +++ b/src/util/lazy_list_fn.h @@ -65,7 +65,7 @@ lazy_list append(lazy_list const & l1, lazy_list const & l2) { return mk_lazy_list([=]() { auto p = l1.pull(); if (!p) { - check_interrupted(); + check_system(); return l2.pull(); } else { return some(mk_pair(p->first, append(p->second, l2))); @@ -81,7 +81,7 @@ lazy_list orelse(lazy_list const & l1, lazy_list const & l2) { return mk_lazy_list([=]() { auto p = l1.pull(); if (!p) { - check_interrupted(); + check_system(); return l2.pull(); } else { return p; @@ -98,7 +98,7 @@ lazy_list interleave(lazy_list const & l1, lazy_list const & l2) { return mk_lazy_list([=]() { auto p = l1.pull(); if (!p) { - check_interrupted(); + check_system(); return l2.pull(); } else { return some(mk_pair(p->first, interleave(l2, p->second))); @@ -125,7 +125,7 @@ lazy_list map(lazy_list const & l, F && f) { \remark Lazy lists may be infinite, and none of them may satisfy \c pred. - \remark \c check_interrupted() is invoked whenever \c pred returns false. + \remark \c check_system() is invoked whenever \c pred returns false. */ template lazy_list filter(lazy_list const & l, P && pred) { @@ -136,7 +136,7 @@ lazy_list filter(lazy_list const & l, P && pred) { } else if (pred(p->first)) { return p; } else { - check_interrupted(); + check_system(); return filter(p->second, pred).pull(); } }); @@ -155,7 +155,7 @@ lazy_list map_append_aux(lazy_list const & h, lazy_list const & l, F && check_interrupted(); auto p2 = l.pull(); if (p2) { - check_interrupted(); + check_system(); return map_append_aux(f(p2->first), p2->second, f).pull(); } else { return typename lazy_list::maybe_pair(); @@ -180,7 +180,7 @@ lazy_list repeat(T const & v, F && f) { if (!p) { return some(mk_pair(v, lazy_list())); } else { - check_interrupted(); + check_system(); return append(repeat(p->first, f), map_append(p->second, [=](T const & v2) { return repeat(v2, f); })).pull(); } @@ -197,7 +197,7 @@ lazy_list repeat_at_most(T const & v, F && f, unsigned k) { if (!p) { return some(mk_pair(v, lazy_list())); } else { - check_interrupted(); + check_system(); return append(repeat_at_most(p->first, f, k - 1), map_append(p->second, [=](T const & v2) { return repeat_at_most(v2, f, k - 1); })).pull(); } diff --git a/src/util/stackinfo.cpp b/src/util/stackinfo.cpp new file mode 100644 index 000000000..fa998d2a6 --- /dev/null +++ b/src/util/stackinfo.cpp @@ -0,0 +1,58 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include +#include +#include +#include "util/exception.h" + +#define LEAN_MIN_STACK_SPACE 128*1024 // 128 Kb + +namespace lean { +#ifdef LEAN_WINDOWS +size_t get_stack_size() { + return LEAN_WIN_STACK_SIZE +} +#else +size_t get_stack_size() { + pthread_attr_t attr; + memset (&attr, 0, sizeof(attr)); + pthread_getattr_np (pthread_self(), &attr); + void * ptr; + size_t result; + pthread_attr_getstack (&attr, &ptr, &result); + return result; +} +#endif + +static thread_local size_t g_stack_size; +static thread_local size_t g_stack_base; + +void save_stack_info() { + g_stack_size = get_stack_size(); + char x; + g_stack_base = reinterpret_cast(&x); +} + +size_t get_used_stack_size() { + char y; + size_t curr_stack = reinterpret_cast(&y); + return g_stack_base - curr_stack; +} + +size_t get_available_stack_size() { + size_t sz = get_used_stack_size(); + if (sz > g_stack_size) + return 0; + else + return g_stack_size - sz; +} + +void check_stack() { + if (get_used_stack_size() + LEAN_MIN_STACK_SPACE > g_stack_size) + throw stack_space_exception(); +} +} diff --git a/src/util/stackinfo.h b/src/util/stackinfo.h new file mode 100644 index 000000000..2ccda5fd7 --- /dev/null +++ b/src/util/stackinfo.h @@ -0,0 +1,17 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +namespace lean { +size_t get_stack_size(); +void save_stack_info(); +size_t get_used_stack_size(); +size_t get_available_stack_size(); +/** + \brief Throw an exception if the amount of available stack space is low. +*/ +void check_stack(); +} diff --git a/src/util/test.h b/src/util/test.h index 5d0a59c3d..3f4a1c693 100644 --- a/src/util/test.h +++ b/src/util/test.h @@ -10,3 +10,4 @@ Author: Leonardo de Moura #define LEAN_DEBUG #endif #include "util/debug.h" +#include "util/stackinfo.h"