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 <leonardo@microsoft.com>

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")

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<unsigned> 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;

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;

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;

src/shell/lean.cpp

@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include <fstream>
 #include <signal.h>
 #include <getopt.h>
+#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;

src/tests/frontends/lean/frontend.cpp

@@ -205,6 +205,7 @@ static void tst11() {
 }
 
 int main() {
+    save_stack_info();
     tst1();
     tst2();
     tst3();

src/tests/frontends/lean/parser.cpp

@@ -106,6 +106,7 @@ static void tst3() {
 }
 
 int main() {
+    save_stack_info();
     tst1();
     tst2();
     tst3();

src/tests/frontends/lean/pp.cpp

@@ -103,6 +103,7 @@ static void tst6() {
 }
 
 int main() {
+    save_stack_info();
     tst1();
     tst2();
     tst3();

src/tests/frontends/lean/scanner.cpp

@@ -119,6 +119,7 @@ static void tst3() {
 }
 
 int main() {
+    save_stack_info();
     tst1();
     tst2();
     tst3();

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)

src/tests/kernel/arith.cpp

@@ -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 <thread>
-#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;
-}

src/tests/kernel/environment.cpp

@@ -283,6 +283,7 @@ static void tst13() {
 }
 
 int main() {
+    save_stack_info();
     enable_trace("is_convertible");
     tst1();
     tst2();

src/tests/kernel/metavar.cpp

@@ -594,6 +594,7 @@ static void tst27() {
 }
 
 int main() {
+    save_stack_info();
     tst1();
     tst2();
     tst3();

src/tests/kernel/normalizer.cpp

@@ -250,6 +250,7 @@ static void tst6() {
 }
 
 int main() {
+    save_stack_info();
     tst_church_numbers();
     tst1();
     tst2();

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;
 }

src/tests/kernel/type_checker.cpp

@@ -325,7 +325,7 @@ static void tst16() {
 }
 
 int main() {
-    tst15(); return 0;
+    save_stack_info();
     tst1();
     tst2();
     tst3();

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 <thread>
 #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;
+}

src/tests/library/elaborator/elaborator.cpp

@@ -874,6 +874,7 @@ void tst27() {
 }
 
 int main() {
+    save_stack_info();
     tst1();
     tst2();
     tst3();

src/tests/library/formatter.cpp

@@ -42,6 +42,7 @@ static void tst1() {
 }
 
 int main() {
+    save_stack_info();
     tst1();
     return has_violations() ? 1 : 0;
 }

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();

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;

src/tests/library/type_inferer.cpp

@@ -138,6 +138,7 @@ static void tst4() {
 }
 
 int main() {
+    save_stack_info();
     tst1();
     tst2();
     tst3();

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)

src/tests/util/lazy_list.cpp

@@ -169,6 +169,7 @@ static void tst4() {
 }
 
 int main() {
+    save_stack_info();
     tst1();
     tst2();
     tst3();

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 <iostream>
+#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;
+}

src/tests/util/thread.cpp

@@ -181,6 +181,7 @@ static void tst6() {}
 #endif
 
 int main() {
+    save_stack_info();
     tst1();
     tst2();
     tst3();

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})

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);

src/util/interrupt.h

@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include <atomic>
 #include <thread>
 #include <utility>
+#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>(args)...);
                 m_flag_addr.store(&m_dummy_addr); // see comment before m_dummy_addr
             },

src/util/lazy_list_fn.h

@@ -65,7 +65,7 @@ lazy_list<T> append(lazy_list<T> const & l1, lazy_list<T> const & l2) {
     return mk_lazy_list<T>([=]() {
             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<T> orelse(lazy_list<T> const & l1, lazy_list<T> const & l2) {
     return mk_lazy_list<T>([=]() {
             auto p = l1.pull();
             if (!p) {
-                check_interrupted();
+                check_system();
                 return l2.pull();
             } else {
                 return p;
@@ -98,7 +98,7 @@ lazy_list<T> interleave(lazy_list<T> const & l1, lazy_list<T> const & l2) {
     return mk_lazy_list<T>([=]() {
             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<T> map(lazy_list<T> 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<typename T, typename P>
 lazy_list<T> filter(lazy_list<T> const & l, P && pred) {
@@ -136,7 +136,7 @@ lazy_list<T> filter(lazy_list<T> 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<T> map_append_aux(lazy_list<T> const & h, lazy_list<T> 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<T>::maybe_pair();
@@ -180,7 +180,7 @@ lazy_list<T> repeat(T const & v, F && f) {
             if (!p) {
                 return some(mk_pair(v, lazy_list<T>()));
             } 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<T> repeat_at_most(T const & v, F && f, unsigned k) {
                 if (!p) {
                     return some(mk_pair(v, lazy_list<T>()));
                 } 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();
                 }

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 <pthread.h>
+#include <memory.h>
+#include <iostream>
+#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<size_t>(&x);
+}
+
+size_t get_used_stack_size() {
+    char y;
+    size_t curr_stack = reinterpret_cast<size_t>(&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();
+}
+}

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();
+}

src/util/test.h

@@ -10,3 +10,4 @@ Author: Leonardo de Moura
 #define LEAN_DEBUG
 #endif
 #include "util/debug.h"
+#include "util/stackinfo.h"