fix(util/lua): deadlock

Errors in the Lua library produce longjmps.
The longjmp will not unwind the C++ stack.
In the new test, the lock was not being released, and the system was deadlocking in the next call that tried to lock the environment

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

src/util/lua.cpp

@@ -9,9 +9,11 @@ Author: Leonardo de Moura
 #include <sstream>
 #include <vector>
 #include <memory>
+#include <cstring>
 #include "util/lua.h"
 #include "util/script_exception.h"
 #include "util/debug.h"
+#include "util/sstream.h"
 
 namespace lean {
 /**
@@ -131,6 +133,16 @@ bool resume(lua_State * L, int nargs) {
     return true;
 }
 
+void throw_bad_arg_error(lua_State * L, int i, char const * expected_type) {
+    lua_Debug ar;
+    if (!lua_getstack(L, 0, &ar))  /* no stack frame? */
+        throw exception(sstream() << "bad argument #" << i << " (" << expected_type << " expected)");
+    lua_getinfo(L, "n", &ar);
+    if (strcmp(ar.namewhat, "method") == 0 || ar.name == nullptr)
+        throw exception(sstream() << "bad argument #" << i << " (" << expected_type << " expected)");
+    throw exception(sstream() << "bad argument #" << i << " to '" << ar.name << "' (" << expected_type << " expected)");
+}
+
 /**
    \brief Wrapper for "customers" that are only using a subset
    of Lean libraries.

src/util/lua.h

@@ -71,6 +71,8 @@ static int T ## _pred(lua_State * L) {                                  \
     return 1;                                                           \
 }
 
+void throw_bad_arg_error(lua_State * L, int i, char const * expected_type);
+
 /**
    \brief Create basic declarations for adding a new kind of userdata in Lua
    T is a Lean object type.
@@ -87,8 +89,8 @@ static int T ## _pred(lua_State * L) {                                  \
 */
 #define DECL_UDATA(T)                                                   \
 constexpr char const * T ## _mt = #T;                                   \
-T & to_ ## T(lua_State * L, int i) { return *static_cast<T*>(luaL_checkudata(L, i, T ## _mt)); } \
 DECL_PRED(T)                                                            \
+T & to_ ## T(lua_State * L, int i) { if (!is_ ## T(L, i)) throw_bad_arg_error(L, i, T ## _mt); return *static_cast<T*>(luaL_checkudata(L, i, T ## _mt)); } \
 DECL_GC(T)                                                              \
 DECL_PUSH(T)
 

tests/lean/loop3.lean

@@ -0,0 +1,37 @@
+variable vec    : Nat → Type
+variable concat {n m : Nat} (v : vec n) (w : vec m) : vec (n + m)
+infixl   65 ; : concat
+axiom    concat_assoc {n1 n2 n3 : Nat} (v1 : vec n1) (v2 : vec n2) (v3 : vec n3) :
+             (v1 ; v2) ; v3 = cast (congr2 vec (symm (Nat::add_assoc n1 n2 n3)))
+                              (v1 ; (v2 ; v3))
+variable empty : vec 0
+axiom    concat_empty {n : Nat} (v : vec n) :
+             v ; empty = cast (congr2 vec (symm (Nat::add_zeror n)))
+                         v
+
+rewrite_set simple
+add_rewrite Nat::add_assoc Nat::add_zeror eq_id : simple
+add_rewrite concat_assoc concat_empty Nat::add_assoc Nat::add_zeror : simple
+
+(*
+local opts = options({"simplifier", "heq"}, true)
+local t = parse_lean('∀ (n : Nat) (v : vec (n + 0)) (w : vec n), v = w ; empty')
+print(t)
+local t2, pr = simplify(t, "simple", heq)
+print("====>")
+print(t2)
+get_environment():type_check(pr)
+*)
+
+print "STEP 1"
+print "STEP 2"
+
+(*
+local opts = options({"simplifier", "heq"}, true)
+local t = parse_lean('λ n : Nat, ∃ (v : vec (n + 0)) (w : vec n), v ≠ w ; empty')
+print(t)
+local t2, pr = simplify(t, "simple", opts)
+print("====>")
+print(t2)
+get_environment():type_check(pr)
+*)

tests/lean/loop3.lean.expected.out

@@ -0,0 +1,15 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: vec
+  Assumed: concat
+  Assumed: concat_assoc
+  Assumed: empty
+  Assumed: concat_empty
+∀ (n : ℕ) (v : vec (n + 0)) (w : vec n), v = w ; empty
+loop3.lean:20: error: executing script
+error: bad argument #3 to 'simplify' (options expected)
+STEP 1
+STEP 2
+λ n : ℕ, ∃ (v : vec (n + 0)) (w : vec n), v ≠ w ; empty
+====>
+λ n : ℕ, ∃ v x : vec n, v ≠ x