From 23d245bb2e5b85d93eea0a08e66aa42fd02e813d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 14 Aug 2013 15:19:05 -0700 Subject: [PATCH] Sanitize context names before generating error messages. Add [[ noreturn ]] attribute to functions that always throw exceptions. Signed-off-by: Leonardo de Moura --- src/kernel/context.h | 2 +- src/kernel/expr_locator.h | 4 +-- src/kernel/type_check.cpp | 59 +++++++++++++++++++-------------- src/tests/kernel/type_check.cpp | 17 ++++++++++ 4 files changed, 54 insertions(+), 28 deletions(-) diff --git a/src/kernel/context.h b/src/kernel/context.h index 7cad176c8..1b784ce23 100644 --- a/src/kernel/context.h +++ b/src/kernel/context.h @@ -42,7 +42,7 @@ inline context extend(context const & c, name const & n, expr const & d, expr co inline context extend(context const & c, name const & n, expr const & d) { return context(context_entry(n, d), c); } -inline bool empty(context const & c) { +inline bool is_empty(context const & c) { return is_nil(c); } diff --git a/src/kernel/expr_locator.h b/src/kernel/expr_locator.h index c0fc0b778..94312aeca 100644 --- a/src/kernel/expr_locator.h +++ b/src/kernel/expr_locator.h @@ -30,6 +30,6 @@ std::shared_ptr mk_dummy_expr_locator(); \brief Throw an exception with the given msg, and include location of the given expression (if available). */ -void throw_exception(expr_locator const & loc, expr const & src, char const * msg); -void throw_exception(expr_locator const & loc, expr const & src, format const & msg); +void throw_exception [[noreturn]] (expr_locator const & loc, expr const & src, char const * msg); +void throw_exception [[noreturn]] (expr_locator const & loc, expr const & src, format const & msg); } diff --git a/src/kernel/type_check.cpp b/src/kernel/type_check.cpp index 0c8249f07..8e2f48c32 100644 --- a/src/kernel/type_check.cpp +++ b/src/kernel/type_check.cpp @@ -61,14 +61,41 @@ struct infer_type_fn { format nl_indent(format const & f) { return fmt().nest(format{line(), f}); } - void throw_exception(expr const & src, format const & msg) { - ::lean::throw_exception(m_env.get_locator(), src, msg); + void throw_error [[ noreturn ]] (expr const & src, format const & msg) { + throw_exception(m_env.get_locator(), src, msg); } /** \brief Include context (if not empty) in the formatted message */ void push_context(format & msg, context const & ctx) { - if (!empty(ctx)) + if (!is_empty(ctx)) { msg += format{format("in context: "), nl_indent(pp(fmt(), ctx)), line()}; + } + } + + void throw_type_expected_error [[ noreturn ]] (expr const & t, context const & ctx) { + context ctx2 = sanitize_names(ctx, t); + format msg = format("type expected, "); + push_context(msg, ctx2); + msg += format{format("got:"), nl_indent(fmt()(t, ctx2))}; + throw_error(t, msg); + } + + void throw_function_expected_error [[ noreturn ]] (expr const & s, context const & ctx) { + context ctx2 = sanitize_names(ctx, s); + format msg = format("function expected, "); + push_context(msg, ctx2); + msg += format{format("got:"), nl_indent(fmt()(s, ctx2))}; + throw_error(s, msg); + } + + void throw_type_mismatch_error [[ noreturn ]] (expr const & app, unsigned arg_pos, + expr const & expected, expr const & given, context const & ctx) { + context ctx2 = sanitize_names(ctx, {app, expected, given}); + format msg = format{format("type mismatch at argument "), format(arg_pos), space(), format("of"), + nl_indent(fmt()(app, ctx2)), line()}; + push_context(msg, ctx2); + msg += format{format("expected type:"), nl_indent(fmt()(expected, ctx2)), line(), format("given type:"), nl_indent(fmt()(given, ctx2))}; + throw_error(arg(app, arg_pos), msg); } level infer_universe(expr const & t, context const & ctx) { @@ -78,12 +105,7 @@ struct infer_type_fn { return ty_level(u); if (u == Bool) return level(); - format msg = format("type expected, "); - push_context(msg, ctx); - msg += format{format("got:"), nl_indent(fmt()(t, ctx))}; - throw_exception(t, msg); - lean_unreachable(); - return level(); + throw_type_expected_error(t, ctx); } expr check_pi(expr const & e, expr const & s, context const & ctx) { @@ -92,12 +114,7 @@ struct infer_type_fn { expr r = normalize(e, m_env, ctx); if (is_pi(r)) return r; - format msg = format("function expected, "); - push_context(msg, ctx); - msg += format{format("got:"), nl_indent(fmt()(s, ctx))}; - throw_exception(s, msg); - lean_unreachable(); - return expr(); + throw_function_expected_error(s, ctx); } expr infer_pi(expr const & e, context const & ctx) { @@ -134,16 +151,8 @@ struct infer_type_fn { while (true) { expr const & c = arg(e, i); expr c_t = infer_type(c, ctx); - if (!is_convertible(abst_domain(f_t), c_t, m_env, ctx)) { - format msg = format{format("type mismatch at argument "), format(i), space(), format("of"), - nl_indent(fmt()(e, ctx)), line(), - format("expected type:"), - nl_indent(fmt()(abst_domain(f_t), ctx)), line(), - format("given type:"), - nl_indent(fmt()(c_t, ctx)), line()}; - push_context(msg, ctx); - throw_exception(arg(e,i), msg); - } + if (!is_convertible(abst_domain(f_t), c_t, m_env, ctx)) + throw_type_mismatch_error(e, i, abst_domain(f_t), c_t, ctx); if (closed(abst_body(f_t))) f_t = abst_body(f_t); else if (closed(c)) diff --git a/src/tests/kernel/type_check.cpp b/src/tests/kernel/type_check.cpp index 169fd04e6..c8daac0b5 100644 --- a/src/tests/kernel/type_check.cpp +++ b/src/tests/kernel/type_check.cpp @@ -129,6 +129,22 @@ static void tst7() { } } +static void tst8() { + environment env = mk_toplevel(); + env.add_var("P", arrow(Int, arrow(Int, Bool))); + env.add_var("x", Int); + expr P = Const("P"); + context c; + c = extend(c, "x", Bool); + expr t = P(Const("x"), Var(0)); + try { + infer_type(t, env, c); + lean_unreachable(); + } catch (exception & ex) { + std::cout << "Error: " << ex.what() << "\n"; + } +} + int main() { tst1(); tst2(); @@ -137,5 +153,6 @@ int main() { tst5(); tst6(); tst7(); + tst8(); return has_violations() ? 1 : 0; }