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

feat(*): distinguish between logical and runtime exceptions.

Browse source 
Now, we use throwable as the new base class for all Lean exceptions, and
exception is the subclass for "logical" exceptions.
This commit is contained in:
Leonardo de Moura 2015-01-15 15:05:47 -08:00
parent 3a865e95fe
commit 8ab775bd6f
24 changed files with 86 additions and 85 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/calc_proof_elaborator.cpp
View file

@ -185,7 +185,7 @@ constraint mk_calc_proof_cnstr(environment const & env, options const & opts,
if (!get_elaborator_calc_assistant(opts)) {
return try_alternative(e, e_type, new_cs);
} else {
std::unique_ptr<exception> saved_ex;
std::unique_ptr<throwable> saved_ex;
try {
return try_alternative(e, e_type, new_cs);
} catch (exception & ex) {

11
src/frontends/lean/parser.cpp
View file

@ -235,7 +235,7 @@ void parser::display_error(char const * msg, unsigned line, unsigned pos) {
void parser::display_error(char const * msg, pos_info p) { display_error(msg, p.first, p.second); }
void parser::display_error(exception const & ex) {
void parser::display_error(throwable const & ex) {
parser_pos_provider pos_provider(m_pos_table, get_stream_name(), m_last_cmd_pos);
::lean::display_error(regular_stream(), &pos_provider, ex);
}
@ -249,8 +249,8 @@ void parser::throw_parser_exception(char const * msg, pos_info p) {
throw parser_exception(msg, get_stream_name().c_str(), p.first, p.second);
}
void parser::throw_nested_exception(exception & ex, pos_info p) {
throw parser_nested_exception(std::shared_ptr<exception>(ex.clone()),
void parser::throw_nested_exception(throwable & ex, pos_info p) {
throw parser_nested_exception(std::shared_ptr<throwable>(ex.clone()),
std::make_shared<parser_pos_provider>(m_pos_table, get_stream_name(), p));
}
@ -264,9 +264,6 @@ if (m_use_exceptions) { ThrowError ; }
void parser::protected_call(std::function<void()> && f, std::function<void()> && sync) {
try {
f();
// } catch (tactic_cmd_error & ex) {
// CATCH(display_error(ex),
// throw parser_exception(ex.what(), m_strm_name.c_str(), ex.m_pos.first, ex.m_pos.second));
} catch (parser_exception & ex) {
CATCH(flycheck_error err(regular_stream()); regular_stream() << ex.what() << endl,
throw);
@ -284,7 +281,7 @@ void parser::protected_call(std::function<void()> && f, std::function<void()> &&
} catch (script_exception & ex) {
reset_interrupt();
CATCH(display_error(ex), throw_nested_exception(ex, m_last_script_pos));
} catch (exception & ex) {
} catch (throwable & ex) {
reset_interrupt();
CATCH(display_error(ex), throw_nested_exception(ex, m_last_cmd_pos));
}

6
src/frontends/lean/parser.h
View file

@ -37,7 +37,7 @@ struct parser_error : public exception {
pos_info m_pos;
parser_error(char const * msg, pos_info const & p):exception(msg), m_pos(p) {}
parser_error(sstream const & msg, pos_info const & p):exception(msg), m_pos(p) {}
virtual exception * clone() const { return new parser_error(m_msg.c_str(), m_pos); }
virtual throwable * clone() const { return new parser_error(m_msg.c_str(), m_pos); }
virtual void rethrow() const { throw *this; }
};
@ -140,10 +140,10 @@ class parser {
void display_error_pos(pos_info p);
void display_error(char const * msg, unsigned line, unsigned pos);
void display_error(char const * msg, pos_info p);
void display_error(exception const & ex);
void display_error(throwable const & ex);
void display_error(script_exception const & ex);
void throw_parser_exception(char const * msg, pos_info p);
void throw_nested_exception(exception & ex, pos_info p);
void throw_nested_exception(throwable & ex, pos_info p);
void sync_command();
void protected_call(std::function<void()> && f, std::function<void()> && sync);

4
src/frontends/lean/server.cpp
View file

@ -217,7 +217,7 @@ server::worker::worker(environment const & env, io_state const & ios, definition
p();
} catch (interrupted &) {
worker_interrupted = true;
} catch (exception & ex) {
} catch (throwable & ex) {
DIAG(std::cerr << "worker exception: " << ex.what() << "\n";)
}
if (!m_terminate && !worker_interrupted) {
@ -888,7 +888,7 @@ bool server::operator()(std::istream & in) {
} else {
throw exception(sstream() << "unexpected command line: " << line);
}
} catch (exception & ex) {
} catch (throwable & ex) {
m_out << "-- ERROR " << ex.what() << std::endl;
}
}

2
src/kernel/kernel_exception.cpp
View file

@ -24,7 +24,7 @@ public:
virtual ~generic_kernel_exception() noexcept {}
virtual optional<expr> get_main_expr() const { return m_main_expr; }
virtual format pp(formatter const & fmt) const { return m_pp_fn(fmt); }
virtual exception * clone() const { return new generic_kernel_exception(m_env, m_msg.c_str(), m_main_expr, m_pp_fn); }
virtual throwable * clone() const { return new generic_kernel_exception(m_env, m_msg.c_str(), m_main_expr, m_pp_fn); }
virtual void rethrow() const { throw *this; }
};

2
src/kernel/kernel_exception.h
View file

@ -29,7 +29,7 @@ public:
*/
virtual optional<expr> get_main_expr() const { return none_expr(); }
virtual format pp(formatter const & fmt) const;
virtual exception * clone() const { return new kernel_exception(m_env, m_msg.c_str()); }
virtual throwable * clone() const { return new kernel_exception(m_env, m_msg.c_str()); }
virtual void rethrow() const { throw *this; }
};

16
src/library/error_handling/error_handling.cpp
View file

@ -68,7 +68,7 @@ void display_error_pos(io_state_stream const & ios, pos_info_provider const * p,
}
}
void display_error(io_state_stream const & ios, pos_info_provider const * p, exception const & ex);
void display_error(io_state_stream const & ios, pos_info_provider const * p, throwable const & ex);
static void display_error(io_state_stream const & ios, pos_info_provider const * p, kernel_exception const & ex) {
display_error_pos(ios, p, ex.get_main_expr());
@ -136,15 +136,7 @@ static void display_error(io_state_stream const & ios, pos_info_provider const *
}
}
// static void display_error(io_state_stream const & ios, pos_info_provider const *, parser_nested_exception const & ex) {
// display_error(ios, &(ex.get_provider()), ex.get_exception());
// }
// static void display_error(io_state_stream const & ios, pos_info_provider const *, parser_exception const & ex) {
// ios << ex.what() << endl;
// }
void display_error(io_state_stream const & ios, pos_info_provider const * p, exception const & ex) {
void display_error(io_state_stream const & ios, pos_info_provider const * p, throwable const & ex) {
flycheck_error err(ios);
if (auto k_ex = dynamic_cast<kernel_exception const *>(&ex)) {
display_error(ios, p, *k_ex);
@ -156,10 +148,6 @@ void display_error(io_state_stream const & ios, pos_info_provider const * p, exc
display_error(ios, p, *ls_ex);
} else if (auto s_ex = dynamic_cast<script_exception const *>(&ex)) {
display_error(ios, p, *s_ex);
// } else if (auto n_ex = dynamic_cast<parser_nested_exception const *>(&ex)) {
// display_error(ios, p, *n_ex);
// } else if (auto n_ex = dynamic_cast<parser_exception const *>(&ex)) {
// display_error(ios, p, *n_ex);
} else if (p) {
display_error_pos(ios, p->get_file_name(), p->get_some_pos().first, p->get_some_pos().second);
ios << " " << ex.what() << endl;

2
src/library/error_handling/error_handling.h
View file

@ -24,5 +24,5 @@ void display_information_pos(io_state_stream const & ios, char const * strm_name
\brief Display exception in the regular stream of \c ios, using the configuration options and formatter from \c ios.
Exceptions that contain expressions use the given \c pos_info_provider (if available) to retrieve line number information.
*/
void display_error(io_state_stream const & ios, pos_info_provider const * p, exception const & ex);
void display_error(io_state_stream const & ios, pos_info_provider const * p, throwable const & ex);
}

2
src/library/generic_exception.h
View file

@ -23,7 +23,7 @@ public:
virtual ~generic_exception() noexcept {}
virtual optional<expr> get_main_expr() const { return m_main_expr; }
virtual format pp(formatter const & fmt) const { return m_pp_fn(fmt); }
virtual exception * clone() const { return new generic_exception(m_msg.c_str(), m_main_expr, m_pp_fn); }
virtual throwable * clone() const { return new generic_exception(m_msg.c_str(), m_main_expr, m_pp_fn); }
virtual void rethrow() const { throw *this; }
};

4
src/library/module.cpp
View file

@ -457,7 +457,7 @@ struct import_modules_fn {
if (m_asynch_tasks.empty())
return;
std::vector<std::unique_ptr<interruptible_thread>> extra_threads;
std::vector<std::unique_ptr<exception>> thread_exceptions(m_num_threads - 1);
std::vector<std::unique_ptr<throwable>> thread_exceptions(m_num_threads - 1);
atomic<int> failed_thread_idx(-1); // >= 0 if error
for (unsigned i = 0; i < m_num_threads - 1; i++) {
extra_threads.push_back(std::unique_ptr<interruptible_thread>(new interruptible_thread([=, &thread_exceptions, &failed_thread_idx]() {
@ -466,7 +466,7 @@ struct import_modules_fn {
(*t)(m_senv);
}
m_asynch_cv.notify_all();
} catch (exception & ex) {
} catch (throwable & ex) {
thread_exceptions[i].reset(ex.clone());
failed_thread_idx = i;
} catch (...) {

2
src/library/num.cpp
View file

@ -45,7 +45,7 @@ bool has_num_decls(environment const & env) {
tc.infer(*g_one).first == *g_pos_num &&
tc.infer(*g_bit0).first == mk_arrow(*g_pos_num, *g_pos_num) &&
tc.infer(*g_bit1).first == mk_arrow(*g_pos_num, *g_pos_num);
} catch (...) {
} catch (exception&) {
return false;
}
}

9
src/library/parser_nested_exception.h
View file

@ -11,15 +11,16 @@ Author: Leonardo de Moura
namespace lean {
/** \brief Lean exception occurred when parsing file. */
class parser_nested_exception : public exception {
std::shared_ptr<exception> m_exception;
std::shared_ptr<throwable> m_exception;
std::shared_ptr<pos_info_provider> m_provider;
public:
parser_nested_exception(std::shared_ptr<exception> const & ex, std::shared_ptr<pos_info_provider> const & pr):exception("parser exception"), m_exception(ex), m_provider(pr) {}
parser_nested_exception(std::shared_ptr<throwable> const & ex, std::shared_ptr<pos_info_provider> const & pr):
exception("parser exception"), m_exception(ex), m_provider(pr) {}
virtual ~parser_nested_exception() {}
virtual exception * clone() const { return new parser_nested_exception(m_exception, m_provider); }
virtual throwable * clone() const { return new parser_nested_exception(m_exception, m_provider); }
virtual void rethrow() const { throw *this; }
virtual char const * what() const noexcept { return m_exception->what(); }
exception const & get_exception() const { return *(m_exception.get()); }
throwable const & get_exception() const { return *(m_exception.get()); }
pos_info_provider const & get_provider() const { return *(m_provider.get()); }
};
}

2
src/library/unifier.h
View file

@ -94,7 +94,7 @@ class unifier_exception : public exception {
substitution m_subst;
public:
unifier_exception(justification const & j, substitution const & s):exception("unifier exception"), m_jst(j), m_subst(s) {}
virtual exception * clone() const { return new unifier_exception(m_jst, m_subst); }
virtual throwable * clone() const { return new unifier_exception(m_jst, m_subst); }
virtual void rethrow() const { throw *this; }
justification const & get_justification() const { return m_jst; }
substitution const & get_substitution() const { return m_subst; }

2
src/library/unsolved_metavar_exception.h
View file

@ -21,7 +21,7 @@ public:
unsolved_metavar_exception(sstream const & strm, expr const & e):exception(strm), m_expr(e) {}
virtual ~unsolved_metavar_exception() {}
expr get_expr() const { return m_expr; }
virtual exception * clone() const { return new unsolved_metavar_exception(m_msg.c_str(), m_expr); }
virtual throwable * clone() const { return new unsolved_metavar_exception(m_msg.c_str(), m_expr); }
virtual void rethrow() const { throw *this; }
};
}

2
src/shell/lean.cpp
View file

@ -559,7 +559,7 @@ int main(int argc, char ** argv) {
export_as_cpp_file(cpp_output, "olean_lib", env);
}
return ok ? 0 : 1;
} catch (lean::exception & ex) {
} catch (lean::throwable & ex) {
lean::display_error(diagnostic(env, ios), nullptr, ex);
}
return 1;

6
src/tests/util/exception.cpp
View file

@ -38,7 +38,7 @@ static void tst3() {
static void tst4() {
try {
throw interrupted();
} catch (exception & ex) {
} catch (throwable & ex) {
lean_assert(std::string("interrupted") == ex.what());
}
}
@ -47,7 +47,7 @@ class ex : public exception {
std::function<char const *()> m_f;
public:
ex(std::function<char const *()> const & f):m_f(f) {}
virtual exception * clone() const { return new ex(m_f); }
virtual throwable * clone() const { return new ex(m_f); }
virtual void rethrow() const { throw *this; }
virtual char const * what() const noexcept { return m_f(); }
};
@ -69,7 +69,7 @@ static void throw_catch_rethrow() {
throw_ex();
} catch (ex & e) {
std::cout << "CATCH 1: {" << e.what() << "}\n";
std::unique_ptr<exception> new_e(e.clone());
std::unique_ptr<throwable> new_e(e.clone());
new_e->rethrow();
}
}

2
src/util/debug.h
View file

@ -108,7 +108,7 @@ public:
unreachable_reached() {}
virtual ~unreachable_reached() noexcept {}
virtual char const * what() const noexcept { return "'unreachable' code was reached"; }
virtual exception * clone() const { return new unreachable_reached(); }
virtual throwable * clone() const { return new unreachable_reached(); }
virtual void rethrow() const { throw *this; }
};
namespace debug {

20
src/util/exception.cpp
View file

@ -11,11 +11,11 @@ Author: Leonardo de Moura
#include "util/thread.h"
namespace lean {
exception::exception(char const * msg):m_msg(msg) {}
exception::exception(std::string const & msg):m_msg(msg) {}
exception::exception(sstream const & strm):m_msg(strm.str()) {}
exception::~exception() noexcept {}
char const * exception::what() const noexcept { return m_msg.c_str(); }
throwable::throwable(char const * msg):m_msg(msg) {}
throwable::throwable(std::string const & msg):m_msg(msg) {}
throwable::throwable(sstream const & strm):m_msg(strm.str()) {}
throwable::~throwable() noexcept {}
char const * throwable::what() const noexcept { return m_msg.c_str(); }
parser_exception::parser_exception(char const * msg, char const * fname, unsigned l, unsigned p):
exception(msg), m_fname(fname), m_line(l), m_pos(p) {}
@ -55,12 +55,12 @@ char const * memory_exception::what() const noexcept {
}
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)));
throwable const & to_exception(lua_State * L, int i) {
return *(*static_cast<throwable**>(luaL_checkudata(L, i, exception_mt)));
}
int push_exception(lua_State * L, exception const & e) {
exception ** mem = static_cast<exception**>(lua_newuserdata(L, sizeof(exception*))); // NOLINT
int push_exception(lua_State * L, throwable const & e) {
throwable ** mem = static_cast<throwable**>(lua_newuserdata(L, sizeof(throwable*))); // NOLINT
*mem = e.clone();
luaL_getmetatable(L, exception_mt);
lua_setmetatable(L, -2);
@ -68,7 +68,7 @@ int push_exception(lua_State * L, exception const & e) {
}
static int exception_gc(lua_State * L) {
exception ** mem = static_cast<exception**>(lua_touserdata(L, 1));
throwable ** mem = static_cast<throwable**>(lua_touserdata(L, 1));
delete (*mem);
return 0;
}

45
src/util/exception.h
View file

@ -13,17 +13,30 @@ Author: Leonardo de Moura
namespace lean {
class sstream;
/** \brief Base class for all Lean exceptions */
class exception : public std::exception {
class throwable : public std::exception {
protected:
std::string m_msg;
throwable() {}
public:
throwable(char const * msg);
throwable(std::string const & msg);
throwable(sstream const & strm);
virtual ~throwable() noexcept;
virtual char const * what() const noexcept;
virtual throwable * clone() const { return new throwable(m_msg); }
virtual void rethrow() const { throw *this; }
};
/** \brief Base class for all Lean "logical" exceptions, that is, exceptions not related
to resource constraints, and runtime errors */
class exception : public throwable {
protected:
exception() {}
public:
exception(char const * msg);
exception(std::string const & msg);
exception(sstream const & strm);
virtual ~exception() noexcept;
virtual char const * what() const noexcept;
virtual exception * clone() const { return new exception(m_msg); }
exception(char const * msg):throwable(msg) {}
exception(std::string const & msg):throwable(msg) {}
exception(sstream const & strm):throwable(strm) {}
virtual throwable * clone() const { return new exception(m_msg); }
virtual void rethrow() const { throw *this; }
};
@ -42,41 +55,41 @@ public:
unsigned get_line() const { return m_line; }
unsigned get_pos() const { return m_pos; }
std::string const & get_file_name() const { return m_fname; }
virtual exception * clone() const { return new parser_exception(m_msg, m_fname.c_str(), m_line, m_pos); }
virtual throwable * clone() const { return new parser_exception(m_msg, m_fname.c_str(), m_line, m_pos); }
virtual void rethrow() const { throw *this; }
parser_exception update_line(unsigned line_delta) const { return parser_exception(m_msg, m_fname.c_str(), m_line + line_delta, m_pos); }
};
/** \brief Exception used to sign that a computation was interrupted */
class interrupted : public exception {
class interrupted : public throwable {
public:
interrupted() {}
virtual ~interrupted() noexcept {}
virtual char const * what() const noexcept { return "interrupted"; }
virtual exception * clone() const { return new interrupted(); }
virtual throwable * clone() const { return new interrupted(); }
virtual void rethrow() const { throw *this; }
};
class stack_space_exception : public exception {
class stack_space_exception : public throwable {
std::string m_component_name;
public:
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 throwable * clone() const { return new stack_space_exception(m_component_name.c_str()); }
virtual void rethrow() const { throw *this; }
};
class memory_exception : public exception {
class memory_exception : public throwable {
std::string m_component_name;
public:
memory_exception(char const * component_name):m_component_name(component_name) {}
virtual char const * what() const noexcept;
virtual exception * clone() const { return new memory_exception(m_component_name.c_str()); }
virtual throwable * clone() const { return new memory_exception(m_component_name.c_str()); }
virtual void rethrow() const { throw *this; }
};
int push_exception(lua_State * L, exception const & e);
exception const & to_exception(lua_State * L, int i);
int push_exception(lua_State * L, throwable const & e);
throwable const & to_exception(lua_State * L, int i);
bool is_exception(lua_State * L, int i);
void open_exception(lua_State * L);
}

8
src/util/lua.cpp
View file

@ -174,14 +174,16 @@ void throw_bad_arg_error(lua_State * L, int i, char const * expected_type) {
int safe_function_wrapper(lua_State * L, lua_CFunction f) {
try {
return f(L);
} catch (exception & e) {
} catch (throwable & e) {
lua_Debug ar;
lua_getstack(L, 1, &ar);
lua_getinfo(L, "Sl", &ar);
if (ar.source && *(ar.source) == '@')
push_exception(L, script_nested_exception(true, ar.source+1, ar.currentline, std::shared_ptr<exception>(e.clone())));
push_exception(L, script_nested_exception(true, ar.source+1, ar.currentline,
std::shared_ptr<throwable>(e.clone())));
else if (ar.source)
push_exception(L, script_nested_exception(false, ar.source, ar.currentline, std::shared_ptr<exception>(e.clone())));
push_exception(L, script_nested_exception(false, ar.source, ar.currentline,
std::shared_ptr<throwable>(e.clone())));
else
push_exception(L, e);
} catch (std::bad_alloc &) {

4
src/util/memory.cpp
View file

@ -119,7 +119,7 @@ public:
// TODO(Leo): use explicit initialization?
static alloc_info g_global_memory;
static size_t g_max_memory = std::numeric_limits<size_t>::max();
static size_t g_max_memory = 0;
void set_max_memory(size_t max) {
g_max_memory = max;
@ -130,7 +130,7 @@ size_t get_allocated_memory() {
}
void check_memory(char const * component_name) {
if (get_allocated_memory() > g_max_memory)
if (g_max_memory != 0 && get_allocated_memory() > g_max_memory)
throw memory_exception(component_name);
}

2
src/util/script_exception.cpp
View file

@ -86,7 +86,7 @@ char const * script_exception::what() const noexcept {
return buffer.c_str();
}
script_nested_exception::script_nested_exception(source s, std::string f, unsigned l, std::shared_ptr<exception> const & ex):
script_nested_exception::script_nested_exception(source s, std::string f, unsigned l, std::shared_ptr<throwable> const & ex):
script_exception(s, f, l, "Lean exception"),
m_exception(ex) {
lean_assert(ex);

12
src/util/script_exception.h
View file

@ -30,7 +30,7 @@ public:
virtual unsigned get_line() const;
/** \brief Return error message without position information */
virtual char const * get_msg() const noexcept;
virtual exception * clone() const { return new script_exception(m_source, m_file, m_line, m_msg); }
virtual throwable * clone() const { return new script_exception(m_source, m_file, m_line, m_msg); }
virtual void rethrow() const { throw *this; }
};
@ -38,14 +38,14 @@ public:
\brief Lean exception occurred inside of a script
*/
class script_nested_exception : public script_exception {
std::shared_ptr<exception> m_exception;
script_nested_exception(source s, std::string f, unsigned l, std::shared_ptr<exception> const & ex);
std::shared_ptr<throwable> m_exception;
script_nested_exception(source s, std::string f, unsigned l, std::shared_ptr<throwable> const & ex);
public:
script_nested_exception(bool file, std::string f, unsigned l, std::shared_ptr<exception> const & ex):script_nested_exception(file ? source::File : source::String, f, l, ex) {}
script_nested_exception(bool file, std::string f, unsigned l, std::shared_ptr<throwable> const & ex):script_nested_exception(file ? source::File : source::String, f, l, ex) {}
virtual ~script_nested_exception();
virtual char const * what() const noexcept;
virtual exception * clone() const { return new script_nested_exception(m_source, m_file, m_line, m_exception); }
virtual throwable * clone() const { return new script_nested_exception(m_source, m_file, m_line, m_exception); }
virtual void rethrow() const { throw *this; }
exception const & get_exception() const { return *(m_exception.get()); }
throwable const & get_exception() const { return *(m_exception.get()); }
};
}

4
src/util/worker_queue.h
View file

@ -19,7 +19,7 @@ template<typename T>
class worker_queue {
typedef std::function<T()> task;
typedef std::unique_ptr<interruptible_thread> thread_ptr;
typedef std::unique_ptr<exception> exception_ptr;
typedef std::unique_ptr<throwable> exception_ptr;
std::vector<thread_ptr> m_threads;
std::vector<exception_ptr> m_thread_exceptions;
std::vector<task> m_todo;
@ -70,7 +70,7 @@ public:
}
m_todo_cv.notify_all();
} catch (interrupted &) {
} catch (exception & ex) {
} catch (throwable & ex) {
m_thread_exceptions[i].reset(ex.clone());
m_failed_thread = i;
} catch (...) {