michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(lua): memory leaks, we should not use luaL_error because it does not unwind C++ stack

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-11-11 21:44:10 -08:00
parent a30e02d862
commit d257156b88
11 changed files with 42 additions and 45 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/bindings/lua/context.cpp
View file

@ -114,7 +114,7 @@ static int context_pred(lua_State * L) {
static int context_extend(lua_State * L) {
int nargs = lua_gettop(L);
if (nargs != 3 && nargs != 4)
luaL_error(L, "extend expect 3 or 4 arguments");
throw exception("extend expect 3 or 4 arguments");
return mk_context(L);
}

2
src/bindings/lua/environment.cpp
View file

@ -173,7 +173,7 @@ int get_environment(lua_State * L) {
lua_pushlightuserdata(L, static_cast<void *>(&g_set_environment_key));
lua_gettable(L, LUA_REGISTRYINDEX);
if (!is_environment(L, -1))
luaL_error(L, "Lua registry does not contain a Lean environment");
throw exception("Lua registry does not contain a Lean environment");
return push_environment(L, to_environment(L, -1));
}

22
src/bindings/lua/expr.cpp
View file

@ -32,7 +32,7 @@ expr & to_expr(lua_State * L, int idx) {
expr & to_nonnull_expr(lua_State * L, int idx) {
expr & r = to_expr(L, idx);
if (!r)
luaL_error(L, "non-null Lean expression expected");
throw exception("non-null Lean expression expected");
return r;
}
@ -83,7 +83,7 @@ static int expr_mk_var(lua_State * L) {
static int expr_mk_app(lua_State * L) {
int nargs = lua_gettop(L);
if (nargs < 2)
luaL_error(L, "application must have at least two arguments");
throw exception("application must have at least two arguments");
buffer<expr> args;
for (int i = 1; i <= nargs; i++)
args.push_back(to_nonnull_expr(L, i));
@ -126,7 +126,7 @@ static std::pair<expr, expr> get_expr_pair_from_table(lua_State * L, int t, int
lua_pushinteger(L, i);
lua_gettable(L, -2); // now table {ai, bi} is on the top
if (!lua_istable(L, -1) || objlen(L, -1) != 2)
luaL_error(L, "arg #1 must be of the form '{{expr, expr}, ...}'");
throw exception("arg #1 must be of the form '{{expr, expr}, ...}'");
expr ai = get_expr_from_table(L, -1, 1);
expr bi = get_expr_from_table(L, -1, 2);
lua_pop(L, 2); // pop table {ai, bi} and t from stack
@ -137,16 +137,16 @@ typedef expr (*MkAbst1)(expr const & n, expr const & t, expr const & b);
typedef expr (*MkAbst2)(name const & n, expr const & t, expr const & b);
template<MkAbst1 F1, MkAbst2 F2>
int expr_abst(lua_State * L, char const * fname) {
int expr_abst(lua_State * L) {
int nargs = lua_gettop(L);
if (nargs < 2)
luaL_error(L, "Lean %s must have at least 2 arguments", fname);
throw exception("function must have at least 2 arguments");
if (nargs == 2) {
if (!lua_istable(L, 1))
luaL_error(L, "Lean %s expects arg #1 to be of the form '{{expr, expr}, ...}'", fname);
throw exception("function expects arg #1 to be of the form '{{expr, expr}, ...}'");
int len = objlen(L, 1);
if (len == 0)
luaL_error(L, "Lean %s expects arg #1 to be a non-empty table", fname);
throw exception("function expects arg #1 to be a non-empty table");
expr r = to_nonnull_expr(L, 2);
for (int i = len; i >= 1; i--) {
auto p = get_expr_pair_from_table(L, 1, i);
@ -155,7 +155,7 @@ int expr_abst(lua_State * L, char const * fname) {
return push_expr(L, r);
} else {
if (nargs % 2 == 0)
luaL_error(L, "Lean %s must have an odd number of arguments", fname);
throw exception("function must have an odd number of arguments");
expr r = to_nonnull_expr(L, nargs);
for (int i = nargs - 1; i >= 1; i-=2) {
if (is_expr(L, i - 1))
@ -167,9 +167,9 @@ int expr_abst(lua_State * L, char const * fname) {
}
}
static int expr_fun(lua_State * L) { return expr_abst<Fun, Fun>(L, "fun"); }
static int expr_pi(lua_State * L) { return expr_abst<Pi, Pi>(L, "Pi"); }
static int expr_let(lua_State * L) { return expr_abst<Let, Let>(L, "Let"); }
static int expr_fun(lua_State * L) { return expr_abst<Fun, Fun>(L); }
static int expr_pi(lua_State * L) { return expr_abst<Pi, Pi>(L); }
static int expr_let(lua_State * L) { return expr_abst<Let, Let>(L); }
static int expr_type(lua_State * L) {
int nargs = lua_gettop(L);

3
src/bindings/lua/format.cpp
View file

@ -8,6 +8,7 @@ Author: Leonardo de Moura
#include <lua.hpp>
#include <cstring>
#include "util/debug.h"
#include "util/sstream.h"
#include "util/sexpr/format.h"
#include "bindings/lua/util.h"
#include "bindings/lua/name.h"
@ -103,7 +104,7 @@ static int format_highlight(lua_State * L) {
} else if (strcmp(color_str, "grey") == 0) {
color = format::GREY;
} else {
return luaL_error(L, "unknown color '%s'", color_str);
throw exception(sstream() << "unknown color '" << color_str << "'");
}
return push_format(L, highlight(to_format(L, 1), color));
}

2
src/bindings/lua/leanlua_state.cpp
View file

@ -159,7 +159,7 @@ static int print(lua_State * L) {
lua_call(L, 1, 1);
s = lua_tolstring(L, -1, &l);
if (s == NULL)
return luaL_error(L, "'to_string' must return a string to 'print'");
throw exception("'to_string' must return a string to 'print'");
if (i > 1) {
std::cout << "\t";
}

10
src/bindings/lua/level.cpp
View file

@ -96,33 +96,33 @@ static int level_is_max(lua_State * L) {
static int level_name(lua_State * L) {
if (!is_uvar(to_level(L, 1)))
luaL_error(L, "arg #1 must be a Lean level universal variable");
throw exception("arg #1 must be a Lean level universal variable");
return push_name(L, uvar_name(to_level(L, 1)));
}
static int level_lift_of(lua_State * L) {
if (!is_lift(to_level(L, 1)))
luaL_error(L, "arg #1 must be a Lean level lift");
throw exception("arg #1 must be a Lean level lift");
return push_level(L, lift_of(to_level(L, 1)));
}
static int level_lift_offset(lua_State * L) {
if (!is_lift(to_level(L, 1)))
luaL_error(L, "arg #1 must be a Lean level lift");
throw exception("arg #1 must be a Lean level lift");
lua_pushinteger(L, lift_offset(to_level(L, 1)));
return 1;
}
static int level_max_size(lua_State * L) {
if (!is_max(to_level(L, 1)))
luaL_error(L, "arg #1 must be a Lean level max");
throw exception("arg #1 must be a Lean level max");
lua_pushinteger(L, max_size(to_level(L, 1)));
return 1;
}
static int level_max_level(lua_State * L) {
if (!is_max(to_level(L, 1)))
luaL_error(L, "arg #1 must be a Lean level max");
throw exception("arg #1 must be a Lean level max");
return push_level(L, max_level(to_level(L, 1), luaL_checkinteger(L, 2)));
}

4
src/bindings/lua/local_context.cpp
View file

@ -71,7 +71,7 @@ static int local_entry_s(lua_State * L) {
static int local_entry_n(lua_State * L) {
local_entry & e = to_local_entry(L, 1);
if (!e.is_lift())
luaL_error(L, "Lean lift local entry expected");
throw exception("Lean lift local entry expected");
lua_pushinteger(L, to_local_entry(L, 1).n());
return 1;
}
@ -79,7 +79,7 @@ static int local_entry_n(lua_State * L) {
static int local_entry_v(lua_State * L) {
local_entry & e = to_local_entry(L, 1);
if (!e.is_inst())
luaL_error(L, "Lean inst local entry expected");
throw exception("Lean inst local entry expected");
return push_expr(L, to_local_entry(L, 1).v());
return 1;
}

8
src/bindings/lua/numerics.cpp
View file

@ -83,7 +83,7 @@ static int mpz_mul(lua_State * L) {
static int mpz_div(lua_State * L) {
mpz const & arg2 = to_mpz<2>(L);
if (arg2 == 0) luaL_error(L, "division by zero");
if (arg2 == 0) throw exception("division by zero");
return push_mpz(L, to_mpz<1>(L) / arg2);
}
@ -93,7 +93,7 @@ static int mpz_umn(lua_State * L) {
static int mpz_power(lua_State * L) {
int k = luaL_checkinteger(L, 2);
if (k < 0) luaL_error(L, "argument #2 must be positive");
if (k < 0) throw exception("argument #2 must be positive");
return push_mpz(L, pow(to_mpz<1>(L), k));
}
@ -200,7 +200,7 @@ static int mpq_mul(lua_State * L) {
static int mpq_div(lua_State * L) {
mpq const & arg2 = to_mpq<2>(L);
if (arg2 == 0) luaL_error(L, "division by zero");
if (arg2 == 0) throw exception("division by zero");
return push_mpq(L, to_mpq<1>(L) / arg2);
}
@ -210,7 +210,7 @@ static int mpq_umn(lua_State * L) {
static int mpq_power(lua_State * L) {
int k = luaL_checkinteger(L, 2);
if (k < 0) luaL_error(L, "argument #2 must be positive");
if (k < 0) throw exception("argument #2 must be positive");
return push_mpq(L, pow(to_mpq<1>(L), k));
}

9
src/bindings/lua/options.cpp
View file

@ -8,6 +8,7 @@ Author: Leonardo de Moura
#include <lua.hpp>
#include "util/debug.h"
#include "util/name.h"
#include "util/sstream.h"
#include "util/sexpr/options.h"
#include "util/sexpr/option_declarations.h"
#include "bindings/lua/util.h"
@ -133,7 +134,7 @@ static int options_get(lua_State * L) {
name k = to_key(L, 2);
auto it = get_option_declarations().find(k);
if (it == get_option_declarations().end()) {
return luaL_error(L, "unknown option '%s'", k.to_string().c_str());
throw exception(sstream() << "unknown option '" << k.to_string().c_str() << "'");
} else {
option_declaration const & d = it->second;
switch (d.kind()) {
@ -142,7 +143,7 @@ static int options_get(lua_State * L) {
case UnsignedOption: return options_get_unsigned(L);
case DoubleOption: return options_get_double(L);
case StringOption: return options_get_string(L);
default: return luaL_error(L, "unsupported option kind for '%s'", k.to_string().c_str());
default: throw exception(sstream() << "unsupported option kind for '" << k.to_string().c_str() << "'");
}
}
}
@ -151,7 +152,7 @@ static int options_update(lua_State * L) {
name k = to_key(L, 2);
auto it = get_option_declarations().find(k);
if (it == get_option_declarations().end()) {
return luaL_error(L, "unknown option '%s'", k.to_string().c_str());
throw exception(sstream() << "unknown option '" << k.to_string().c_str() << "'");
} else {
option_declaration const & d = it->second;
switch (d.kind()) {
@ -160,7 +161,7 @@ static int options_update(lua_State * L) {
case UnsignedOption: return options_update_unsigned(L);
case DoubleOption: return options_update_double(L);
case StringOption: return options_update_string(L);
default: return luaL_error(L, "unsupported option kind for '%s'", k.to_string().c_str());
default: throw exception(sstream() << "unsupported option kind for '" << k.to_string().c_str() << "'");
}
}
}

20
src/bindings/lua/sexpr.cpp
View file

@ -97,7 +97,7 @@ static int sexpr_is_mpq(lua_State * L) { lua_pushboolean(L, is_mpq(to_sexpr(L
static int sexpr_length(lua_State * L) {
sexpr const & e = to_sexpr(L, 1);
if (!is_list(e))
return luaL_error(L, "s-expression is not a list");
throw exception("s-expression is not a list");
lua_pushinteger(L, length(e));
return 1;
}
@ -105,21 +105,21 @@ static int sexpr_length(lua_State * L) {
static int sexpr_head(lua_State * L) {
sexpr const & e = to_sexpr(L, 1);
if (!is_cons(e))
return luaL_error(L, "s-expression is not a cons cell");
throw exception("s-expression is not a cons cell");
return push_sexpr(L, head(e));
}
static int sexpr_tail(lua_State * L) {
sexpr const & e = to_sexpr(L, 1);
if (!is_cons(e))
return luaL_error(L, "s-expression is not a cons cell");
throw exception("s-expression is not a cons cell");
return push_sexpr(L, tail(e));
}
static int sexpr_to_bool(lua_State * L) {
sexpr const & e = to_sexpr(L, 1);
if (!is_bool(e))
return luaL_error(L, "s-expression is not a Boolean");
throw exception("s-expression is not a Boolean");
lua_pushboolean(L, to_bool(e));
return 1;
}
@ -127,7 +127,7 @@ static int sexpr_to_bool(lua_State * L) {
static int sexpr_to_string(lua_State * L) {
sexpr const & e = to_sexpr(L, 1);
if (!is_string(e))
return luaL_error(L, "s-expression is not a string");
throw exception("s-expression is not a string");
lua_pushfstring(L, to_string(e).c_str());
return 1;
}
@ -135,7 +135,7 @@ static int sexpr_to_string(lua_State * L) {
static int sexpr_to_int(lua_State * L) {
sexpr const & e = to_sexpr(L, 1);
if (!is_int(e))
return luaL_error(L, "s-expression is not an integer");
throw exception("s-expression is not an integer");
lua_pushinteger(L, to_int(e));
return 1;
}
@ -143,7 +143,7 @@ static int sexpr_to_int(lua_State * L) {
static int sexpr_to_double(lua_State * L) {
sexpr const & e = to_sexpr(L, 1);
if (!is_double(e))
return luaL_error(L, "s-expression is not a double");
throw exception("s-expression is not a double");
lua_pushnumber(L, to_double(e));
return 1;
}
@ -151,21 +151,21 @@ static int sexpr_to_double(lua_State * L) {
static int sexpr_to_name(lua_State * L) {
sexpr const & e = to_sexpr(L, 1);
if (!is_name(e))
return luaL_error(L, "s-expression is not a name");
throw exception("s-expression is not a name");
return push_name(L, to_name(e));
}
static int sexpr_to_mpz(lua_State * L) {
sexpr const & e = to_sexpr(L, 1);
if (!is_mpz(e))
return luaL_error(L, "s-expression is not a multi-precision integer");
throw exception("s-expression is not a multi-precision integer");
return push_mpz(L, to_mpz(e));
}
static int sexpr_to_mpq(lua_State * L) {
sexpr const & e = to_sexpr(L, 1);
if (!is_mpq(e))
return luaL_error(L, "s-expression is not a multi-precision rational");
throw exception("s-expression is not a multi-precision rational");
return push_mpq(L, to_mpq(e));
}

5
tests/lua/expr5.lua
View file

@ -15,8 +15,3 @@ check_error(function() Pi({{"x"}}, Const("x")) end)
check_error(function() Pi(Const("x")) end)
check_error(function() Pi(Const("x"), Const("N"), Const("x"), Const("a")) end)
check_error(function() Pi({}, Const("x")) end)