feat(*): add component name to check_stack and check_system

I also reduced the stack size to 8 Mb in the tests at tests/lean and tests/lean/slow. The idea is to simulate stackoverflow conditions.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/frontends/lean/pp.cpp

@@ -1071,7 +1071,7 @@ class pp_fn {
     }
 
     result pp(expr const & e, unsigned depth, bool main = false) {
-        check_interrupted();
+        check_system("pretty printer");
         if (!is_atomic(e) && (m_num_steps > m_max_steps || depth > m_max_depth)) {
             return pp_ellipsis();
         } else {

src/kernel/expr_eq.h

@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include <memory>
+#include "util/interrupt.h"
 #include "kernel/expr.h"
 #include "kernel/expr_sets.h"
 
@@ -29,6 +30,7 @@ class expr_eq_fn {
     N                                   m_norm;
 
     bool apply(expr const & a0, expr const & b0) {
+        check_system("expression equality test");
         if (is_eqp(a0, b0))                    return true;
         if (!a0 || !b0)                        return false;
         if (UseHash && a0.hash() != b0.hash()) return false;

src/kernel/normalizer.cpp

@@ -133,6 +133,7 @@ class normalizer::imp {
 
     /** \brief Convert the value \c v back into an expression in a context that contains \c k binders. */
     expr reify(svalue const & v, unsigned k) {
+        check_system("normalizer");
         switch (v.kind()) {
         case svalue_kind::Expr:       return to_expr(v);
         case svalue_kind::BoundedVar: return mk_var(k - to_bvar(v) - 1);
@@ -179,7 +180,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_system();
+        check_system("normalizer");
         if (m_depth > m_max_depth)
             throw kernel_exception(env(), "normalizer maximum recursion depth exceeded");
         bool shared = false;

src/kernel/replace_fn.h

@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #pragma once
 #include <tuple>
 #include "util/buffer.h"
+#include "util/interrupt.h"
 #include "kernel/expr.h"
 #include "kernel/expr_maps.h"
 
@@ -47,6 +48,7 @@ class replace_fn {
     P                          m_post;
 
     expr apply(expr const & e, unsigned offset) {
+        check_system("expression replacer");
         if (!e)
             return e;
         bool sh = false;

src/kernel/replace_visitor.cpp

@@ -63,7 +63,7 @@ expr replace_visitor::visit_let(expr const & e, context const & ctx) {
         });
 }
 expr replace_visitor::visit(expr const & e, context const & ctx) {
-    check_system();
+    check_system("expression replacer");
     bool shared = false;
     if (is_shared(e)) {
         shared = true;

src/kernel/type_checker.cpp

@@ -85,7 +85,7 @@ class type_checker::imp {
     }
 
     expr infer_type_core(expr const & e, context const & ctx) {
-        check_system();
+        check_system("type checker");
         bool shared = false;
         if (is_shared(e)) {
             shared = true;

src/library/tactic/tactic.cpp

@@ -213,13 +213,13 @@ tactic then(tactic const & t1, tactic const & t2) {
             return map_append(t1(env, io, s1), [=](proof_state const & s2) {
                     check_interrupted();
                     return t2(env, io, s2);
-                });
+                }, "THEN tactical");
         });
 }
 
 tactic orelse(tactic const & t1, tactic const & t2) {
     return mk_tactic([=](environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq {
-            return orelse(t1(env, io, s), t2(env, io, s));
+            return orelse(t1(env, io, s), t2(env, io, s), "ORELSE tactical");
         });
 }
 
@@ -239,13 +239,13 @@ tactic try_for(tactic const & t, unsigned ms, unsigned check_ms) {
 
 tactic append(tactic const & t1, tactic const & t2) {
     return mk_tactic([=](environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq {
-            return append(t1(env, io, s), t2(env, io, s));
+            return append(t1(env, io, s), t2(env, io, s), "APPEND tactical");
         });
 }
 
 tactic interleave(tactic const & t1, tactic const & t2) {
     return mk_tactic([=](environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq {
-            return interleave(t1(env, io, s), t2(env, io, s));
+            return interleave(t1(env, io, s), t2(env, io, s), "INTERLEAVE tactical");
         });
 }
 
@@ -259,7 +259,7 @@ tactic repeat(tactic const & t) {
     return mk_tactic([=](environment const & env, io_state const & io, proof_state const & s1) -> proof_state_seq {
             return repeat(s1, [=](proof_state const & s2) {
                     return t(env, io, s2);
-                });
+                }, "REPEAT tactical");
         });
 }
 
@@ -267,7 +267,7 @@ tactic repeat_at_most(tactic const & t, unsigned k) {
     return mk_tactic([=](environment const & env, io_state const & io, proof_state const & s1) -> proof_state_seq {
             return repeat_at_most(s1, [=](proof_state const & s2) {
                     return t(env, io, s2);
-                }, k);
+                }, k, "REPEAT_AT_MOST tactical");
         });
 }
 

src/library/type_inferer.cpp

@@ -144,7 +144,7 @@ class type_inferer::imp {
             break; // expensive cases
         }
 
-        check_system();
+        check_system("type inference");
         bool shared = false;
         if (is_shared(e)) {
             shared = true;

src/tests/kernel/expr.cpp

@@ -354,6 +354,7 @@ static void tst18() {
 }
 
 int main() {
+    save_stack_info();
     std::cout << "sizeof(expr):      " << sizeof(expr) << "\n";
     std::cout << "sizeof(expr_app):  " << sizeof(expr_app) << "\n";
     std::cout << "sizeof(expr_cell): " << sizeof(expr_cell) << "\n";

src/tests/kernel/free_vars.cpp

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

src/tests/kernel/instantiate.cpp

@@ -45,9 +45,8 @@ static void tst2() {
 }
 
 int main() {
+    save_stack_info();
     tst1();
     tst2();
     return has_violations() ? 1 : 0;
 }
-
-

src/tests/kernel/level.cpp

@@ -108,6 +108,7 @@ static void tst5() {
 }
 
 int main() {
+    save_stack_info();
     tst0();
     tst1();
     tst2();

src/tests/kernel/occurs.cpp

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

src/tests/kernel/replace.cpp

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

src/tests/library/deep_copy.cpp

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

src/tests/library/expr_lt.cpp

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

src/tests/library/max_sharing.cpp

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

src/tests/library/rewriter/fo_match.cpp

@@ -433,6 +433,7 @@ static void match_metavar_tst3() {
 }
 
 int main() {
+    save_stack_info();
     match_var_tst1();
     match_var_tst2();
     match_var_tst3();

src/tests/library/update_expr.cpp

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

src/tests/util/format.cpp

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

src/tests/util/options.cpp

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

src/tests/util/sexpr.cpp

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

src/util/exception.cpp

@@ -33,6 +33,14 @@ char const * parser_exception::what() const noexcept {
     }
 }
 
+char const * stack_space_exception::what() const noexcept {
+    static thread_local std::string buffer;
+    std::ostringstream s;
+    s << "deep recursion was detected at '" << m_component_name << "' (potential solution: increase stack space in your system)";
+    buffer = s.str();
+    return buffer.c_str();
+}
+
 constexpr char const * exception_mt = "exception_mt";
 exception const & to_exception(lua_State * L, int i) {
     return *(*static_cast<exception**>(luaL_checkudata(L, i, exception_mt)));

src/util/exception.h

@@ -51,10 +51,11 @@ public:
     virtual void rethrow() const { throw *this; }
 };
 class stack_space_exception : public exception {
+    std::string m_component_name;
 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(); }
+    stack_space_exception(char const * component_name):m_component_name(component_name) {}
+    virtual char const * what() const noexcept;
+    virtual exception * clone() const { return new stack_space_exception(m_component_name.c_str()); }
     virtual void rethrow() const { throw *this; }
 };
 int push_exception(lua_State * L, exception const & e);

src/util/interrupt.h

@@ -31,7 +31,7 @@ bool interrupt_requested();
 */
 void check_interrupted();
 
-inline void check_system() { check_stack(); check_interrupted(); }
+inline void check_system(char const * component_name) { check_stack(component_name); check_interrupted(); }
 
 constexpr unsigned g_small_sleep = 50;
 

src/util/lazy_list_fn.h

@@ -61,14 +61,14 @@ lazy_list<T> to_lazy(list<T> l) {
    \brief Appends the given lazy lists.
 */
 template<typename T>
-lazy_list<T> append(lazy_list<T> const & l1, lazy_list<T> const & l2) {
+lazy_list<T> append(lazy_list<T> const & l1, lazy_list<T> const & l2, char const * cname = "lazy list") {
     return mk_lazy_list<T>([=]() {
             auto p = l1.pull();
             if (!p) {
-                check_system();
+                check_system(cname);
                 return l2.pull();
             } else {
-                return some(mk_pair(p->first, append(p->second, l2)));
+                return some(mk_pair(p->first, append(p->second, l2, cname)));
             }
         });
 }
@@ -77,11 +77,11 @@ lazy_list<T> append(lazy_list<T> const & l1, lazy_list<T> const & l2) {
    \brief Return \c l1 if l1 is not empty, and \c l2 otherwise.
 */
 template<typename T>
-lazy_list<T> orelse(lazy_list<T> const & l1, lazy_list<T> const & l2) {
+lazy_list<T> orelse(lazy_list<T> const & l1, lazy_list<T> const & l2, char const * cname = "lazy list") {
     return mk_lazy_list<T>([=]() {
             auto p = l1.pull();
             if (!p) {
-                check_system();
+                check_system(cname);
                 return l2.pull();
             } else {
                 return p;
@@ -94,14 +94,14 @@ lazy_list<T> orelse(lazy_list<T> const & l1, lazy_list<T> const & l2) {
    are interleaved.
 */
 template<typename T>
-lazy_list<T> interleave(lazy_list<T> const & l1, lazy_list<T> const & l2) {
+lazy_list<T> interleave(lazy_list<T> const & l1, lazy_list<T> const & l2, char const * cname = "lazy list") {
     return mk_lazy_list<T>([=]() {
             auto p = l1.pull();
             if (!p) {
-                check_system();
+                check_system(cname);
                 return l2.pull();
             } else {
-                return some(mk_pair(p->first, interleave(l2, p->second)));
+                return some(mk_pair(p->first, interleave(l2, p->second, cname)));
             }
         });
 }
@@ -110,13 +110,15 @@ lazy_list<T> interleave(lazy_list<T> const & l1, lazy_list<T> const & l2) {
    \brief Create a lazy list by applying \c f to the elements of \c l.
 */
 template<typename T, typename F>
-lazy_list<T> map(lazy_list<T> const & l, F && f) {
+lazy_list<T> map(lazy_list<T> const & l, F && f, char const * cname = "lazy list") {
     return mk_lazy_list<T>([=]() {
             auto p = l.pull();
-            if (!p)
+            if (!p) {
                 return p;
-            else
-                return some(mk_pair(f(p->first), map(p->second, f)));
+            } else {
+                check_system(cname);
+                return some(mk_pair(f(p->first), map(p->second, f, cname)));
+            }
         });
 }
 
@@ -128,7 +130,7 @@ lazy_list<T> map(lazy_list<T> const & l, F && f) {
    \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) {
+lazy_list<T> filter(lazy_list<T> const & l, P && pred, char const * cname = "lazy list") {
     return mk_lazy_list<T>([=]() {
             auto p = l.pull();
             if (!p) {
@@ -136,8 +138,8 @@ lazy_list<T> filter(lazy_list<T> const & l, P && pred) {
             } else if (pred(p->first)) {
                 return p;
             } else {
-                check_system();
-                return filter(p->second, pred).pull();
+                check_system(cname);
+                return filter(p->second, pred, cname).pull();
             }
         });
 }
@@ -146,17 +148,17 @@ lazy_list<T> filter(lazy_list<T> const & l, P && pred) {
    \brief Auxiliary template for \c map_append.
 */
 template<typename T, typename F>
-lazy_list<T> map_append_aux(lazy_list<T> const & h, lazy_list<T> const & l, F && f) {
+lazy_list<T> map_append_aux(lazy_list<T> const & h, lazy_list<T> const & l, F && f, char const * cname) {
     return mk_lazy_list<T>([=]() {
             auto p1 = h.pull();
             if (p1) {
-                return some(mk_pair(p1->first, map_append_aux(p1->second, l, f)));
+                return some(mk_pair(p1->first, map_append_aux(p1->second, l, f, cname)));
             } else {
                 check_interrupted();
                 auto p2 = l.pull();
                 if (p2) {
-                    check_system();
-                    return map_append_aux(f(p2->first), p2->second, f).pull();
+                    check_system(cname);
+                    return map_append_aux(f(p2->first), p2->second, f, cname).pull();
                 } else {
                     return typename lazy_list<T>::maybe_pair();
                 }
@@ -169,26 +171,26 @@ lazy_list<T> map_append_aux(lazy_list<T> const & h, lazy_list<T> const & l, F &&
    All lazy_lists are appended together.
 */
 template<typename T, typename F>
-lazy_list<T> map_append(lazy_list<T> const & l, F && f) {
-    return map_append_aux(lazy_list<T>(), l, f);
+lazy_list<T> map_append(lazy_list<T> const & l, F && f, char const * cname = "lazy list") {
+    return map_append_aux(lazy_list<T>(), l, f, cname);
 }
 
 template<typename T, typename F>
-lazy_list<T> repeat(T const & v, F && f) {
+lazy_list<T> repeat(T const & v, F && f, char const * cname = "lazy list") {
     return mk_lazy_list<T>([=]() {
             auto p = f(v).pull();
             if (!p) {
                 return some(mk_pair(v, lazy_list<T>()));
             } else {
-                check_system();
-                return append(repeat(p->first, f),
-                              map_append(p->second, [=](T const & v2) { return repeat(v2, f); })).pull();
+                check_system(cname);
+                return append(repeat(p->first, f, cname),
+                              map_append(p->second, [=](T const & v2) { return repeat(v2, f, cname); }, cname), cname).pull();
             }
         });
 }
 
 template<typename T, typename F>
-lazy_list<T> repeat_at_most(T const & v, F && f, unsigned k) {
+lazy_list<T> repeat_at_most(T const & v, F && f, unsigned k, char const * cname = "lazy list") {
     return mk_lazy_list<T>([=]() {
             if (k == 0) {
                 return some(mk_pair(v, lazy_list<T>()));
@@ -197,9 +199,10 @@ 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_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();
+                    check_system(cname);
+                    return append(repeat_at_most(p->first, f, k - 1, cname),
+                                  map_append(p->second, [=](T const & v2) { return repeat_at_most(v2, f, k - 1, cname); }, cname),
+                                  cname).pull();
                 }
             }
         });

src/util/sexpr/format.cpp

@@ -10,6 +10,7 @@
 #include <utility>
 #include "util/sstream.h"
 #include "util/escaped.h"
+#include "util/interrupt.h"
 #include "util/numerics/mpz.h"
 #include "util/numerics/mpq.h"
 #include "util/sexpr/sexpr.h"
@@ -310,6 +311,7 @@ int format::space_upto_line_break(sexpr const & s, int available, bool & found_n
 }
 
 sexpr format::be(unsigned w, unsigned k, sexpr const & s) {
+    check_system("formatter");
     /* s = (i, v) :: z, where h has the type int x format */
     /* ret = list of format */
 

src/util/stackinfo.cpp

@@ -85,8 +85,8 @@ size_t get_available_stack_size() {
         return g_stack_size - sz;
 }
 
-void check_stack() {
+void check_stack(char const * component_name) {
     if (get_used_stack_size() + LEAN_MIN_STACK_SPACE > g_stack_size)
-        throw stack_space_exception();
+        throw stack_space_exception(component_name);
 }
 }

src/util/stackinfo.h

@@ -12,6 +12,9 @@ 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.
+
+   \remark The optional argument \c component_name is used to inform the
+   user which module is the potential offender.
 */
-void check_stack();
+void check_stack(char const * component_name);
 }

tests/lean/slow/tactic1.lean

@@ -0,0 +1,32 @@
+Definition double {A : Type} (f : A -> A) : A -> A := fun x, f (f x).
+Definition big {A : Type} (f : A -> A) : A -> A := (double (double (double (double (double (double (double f))))))).
+
+(**
+
+ -- Tactic for trying to prove goal using Reflexivity, Congruence and available assumptions
+local congr_tac = REPEAT(ORELSE(apply_tac("Refl"), apply_tac("Congr"), assumption_tac))
+
+-- Create an eager tactic that only tries to prove goal after unfolding everything
+eager_tac = THEN(-- unfold homogeneous equality
+                 TRY(unfold_tac("eq")),
+                 -- keep unfolding defintions above and beta-reducing
+                 REPEAT(unfold_tac .. REPEAT(beta_tac)),
+                 congr_tac)
+
+-- The 'lazy' version tries first to prove without unfolding anything
+lazy_tac = ORELSE(THEN(TRY(unfold_tac("eq")), congr_tac, now_tac),
+                  eager_tac)
+
+**)
+
+Theorem T1 (a b : Int) (f : Int -> Int) (H : a = b) : (big f a) = (big f b).
+        apply eager_tac.
+        done.
+
+Theorem T2 (a b : Int) (f : Int -> Int) (H : a = b) : (big f a) = (big f b).
+        apply lazy_tac.
+        done.
+
+Theorem T3 (a b : Int) (f : Int -> Int) (H : a = b) : (big f a) = ((double (double (double (double (double (double (double f))))))) b).
+        apply lazy_tac.
+        done.

tests/lean/slow/tactic1.lean.expected.out

@@ -0,0 +1,7 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Defined: double
+  Defined: big
+  Proved: T1
+  Proved: T2
+  Proved: T3

tests/lean/slow/tactic2.lean

@@ -0,0 +1,3 @@
+Theorem T (a : Bool) : a.
+    apply (** REPEAT(id_tac) **).
+    done.

tests/lean/slow/tactic2.lean.expected.out

@@ -0,0 +1,7 @@
+  Set: pp::colors
+  Set: pp::unicode
+Error (line: 2, pos: 32) deep recursion was detected at 'REPEAT tactical' (potential solution: increase stack space in your system)
+Error (line: 3, pos: 4) invalid 'done' command, proof cannot be produced from this state
+Proof state:
+a : Bool ⊢ a
+Error (line: 4, pos: 0) invalid tactic command, unexpected end of file

tests/lean/test.sh

@@ -3,7 +3,7 @@ if [ $# -ne 2 -a $# -ne 1 ]; then
     echo "Usage: test.sh [lean-executable-path] [yes/no]?"
     exit 1
 fi
-ulimit -s unlimited
+ulimit -s 8192
 LEAN=$1
 if [ $# -ne 2 ]; then
     INTERACTIVE=no

tests/lean/test_single.sh

@@ -3,7 +3,7 @@ if [ $# -ne 3 -a $# -ne 2 ]; then
     echo "Usage: test.sh [lean-executable-path] [file] [yes/no]?"
     exit 1
 fi
-ulimit -s unlimited
+ulimit -s 8192
 LEAN=$1
 if [ $# -ne 3 ]; then
     INTERACTIVE=no