max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: interpreter: print stacktrace on stack overflow

Browse source
This commit is contained in:
Sebastian Ullrich 2020-03-13 17:06:35 +01:00 • committed by Leonardo de Moura
parent 87f8ae99eb
commit d7170df527
1 changed files with 17 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
src/library/compiler/ir_interpreter.cpp
View file

@ -470,8 +470,23 @@ class interpreter {
}
}
void check_system() {
try {
lean::check_system("interpreter");
} catch (stack_space_exception & ex) {
sstream ss;
ss << ex.what() << "\n";
ss << "interpreter stacktrace:\n";
for (unsigned i = 0; i < m_call_stack.size(); i++) {
ss << "#" << (i + 1) << " " << m_call_stack[m_call_stack.size() - i - 1].m_fn << "\n";
}
throw throwable(ss);
}
}
value eval_body(fn_body const & b0) {
check_system("interpreter");
check_system();
// make reference reassignable...
std::reference_wrapper<fn_body const> b(b0);
while (true) {
@ -498,7 +513,7 @@ class interpreter {
}
m_arg_stack.resize(get_frame().m_arg_bp + args.size());
b = b0;
check_system("interpreter");
check_system();
break;
}
value v = eval_expr(fn_body_vdecl_expr(b), fn_body_vdecl_type(b));