From 6477708d78888dc39acab41fd1346dbc7e5ee095 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 25 Sep 2013 21:27:20 -0700 Subject: [PATCH] refactor(debug): improve lean_unreachable(), now we can avoid 'fake' return statements Signed-off-by: Leonardo de Moura --- src/frontends/lean/elaborator.cpp | 1 - src/frontends/lean/operator_info.cpp | 4 +--- src/frontends/lean/parser.cpp | 6 +++--- src/frontends/lean/pp.cpp | 4 ---- src/kernel/environment.cpp | 1 - src/kernel/expr.cpp | 1 - src/kernel/expr_eq.h | 5 ++--- src/kernel/free_vars.cpp | 5 ++--- src/kernel/level.cpp | 4 ---- src/kernel/normalizer.cpp | 1 - src/kernel/object.h | 10 +++++----- src/library/expr_lt.cpp | 5 ++--- src/library/ho_unifier.cpp | 1 - src/library/light_checker.cpp | 1 - src/library/max_sharing.cpp | 1 - src/library/rewriter/fo_match.cpp | 1 - src/util/debug.h | 14 +++++++++----- src/util/interval/interval_def.h | 1 - src/util/numerics/xnumeral.h | 2 -- src/util/pdeque.h | 2 +- src/util/pvector.h | 4 +--- src/util/sexpr/format.cpp | 15 +++++---------- src/util/sexpr/sexpr.cpp | 8 +++----- 23 files changed, 34 insertions(+), 63 deletions(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index f2312eb11..ccc22b4e7 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -476,7 +476,6 @@ class elaborator::imp { return expr_pair(new_e, t); }} lean_unreachable(); - return expr_pair(expr(), expr()); } expr infer(expr const & e, context const & ctx) { diff --git a/src/frontends/lean/operator_info.cpp b/src/frontends/lean/operator_info.cpp index 28f28dd5d..6e183af6e 100644 --- a/src/frontends/lean/operator_info.cpp +++ b/src/frontends/lean/operator_info.cpp @@ -120,7 +120,6 @@ char const * to_string(fixity f) { case fixity::Mixfixo: return "Mixfixo"; } lean_unreachable(); - return 0; } format pp(operator_info const & o) { @@ -170,11 +169,10 @@ format pp(operator_info const & o) { r += format{space(), format("_"), space(), format(p)}; r += format{space(), format("_")}; return r; - default: lean_unreachable(); break; + default: lean_unreachable(); } } lean_unreachable(); - return format(); } char const * notation_declaration::keyword() const { diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index b96a69acb..554d3fec0 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -601,7 +601,7 @@ class parser::imp { case fixity::Prefix: return parse_prefix(op); case fixity::Mixfixl: return parse_mixfixl(op); case fixity::Mixfixc: return parse_mixfixc(op); - default: lean_unreachable(); return expr(); + default: lean_unreachable(); } } else { return save(get_name_ref(id, p), p); @@ -636,7 +636,7 @@ class parser::imp { case fixity::Mixfixr: return parse_mixfixr(left, op); case fixity::Mixfixo: return parse_mixfixo(left, op); case fixity::Postfix: return parse_postfix(left, op); - default: lean_unreachable(); return expr(); + default: lean_unreachable(); } } else { return save(mk_app(left, save(get_name_ref(id, p), p)), p2); @@ -1244,7 +1244,7 @@ class parser::imp { case fixity::Infix: m_frontend.add_infix(op_id, prec, d); break; case fixity::Infixl: m_frontend.add_infixl(op_id, prec, d); break; case fixity::Infixr: m_frontend.add_infixr(op_id, prec, d); break; - default: lean_unreachable(); break; + default: lean_unreachable(); } } diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index b034051d5..e2177eb17 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -572,7 +572,6 @@ class pp_fn { } } lean_unreachable(); - return arg(m_app, n - 1); } else { return arg(m_app, i + 1); } @@ -602,7 +601,6 @@ class pp_fn { return app.get_num_args() == length(op.get_op_name_parts()) + 1; } lean_unreachable(); - return false; } /** @@ -676,7 +674,6 @@ class pp_fn { return mk_result(group(r_format), r_weight); }} lean_unreachable(); - return mk_result(format(), 0); } else if (m_notation && is_forall_expr(e)) { return pp_forall(e, depth); } else if (m_notation && is_exists_expr(e)) { @@ -1361,7 +1358,6 @@ public: } } lean_unreachable(); - return format(); } virtual format operator()(environment const & env, options const & opts) { diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index 2383c7be9..7cce8e1cf 100644 --- a/src/kernel/environment.cpp +++ b/src/kernel/environment.cpp @@ -118,7 +118,6 @@ struct environment::imp { case level_kind::Max: return std::all_of(max_begin_levels(l2), max_end_levels(l2), [&](level const & l) { return is_ge(l1, l, k); }); } lean_unreachable(); - return false; } /** \brief Return true iff l1 >= l2 is implied by asserted universe constraints. */ diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index 22956472c..04b997f0c 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -175,6 +175,5 @@ expr copy(expr const & a) { case expr_kind::MetaVar: return mk_metavar(metavar_idx(a), metavar_ctx(a)); } lean_unreachable(); - return expr(); } } diff --git a/src/kernel/expr_eq.h b/src/kernel/expr_eq.h index 689d176d6..1829e4c57 100644 --- a/src/kernel/expr_eq.h +++ b/src/kernel/expr_eq.h @@ -42,7 +42,7 @@ class expr_eq_fn { m_eq_visited.insert(p); } switch (a.kind()) { - case expr_kind::Var: lean_unreachable(); return true; // LCOV_EXCL_LINE + case expr_kind::Var: lean_unreachable(); case expr_kind::Constant: return const_name(a) == const_name(b); case expr_kind::App: if (num_args(a) != num_args(b)) @@ -75,8 +75,7 @@ class expr_eq_fn { return e1.n() == e2.n(); }); } - lean_unreachable(); // LCOV_EXCL_LINE - return false; // LCOV_EXCL_LINE + lean_unreachable(); } public: expr_eq_fn(N const & norm = N()):m_norm(norm) {} diff --git a/src/kernel/free_vars.cpp b/src/kernel/free_vars.cpp index bd71fddcd..200821a4b 100644 --- a/src/kernel/free_vars.cpp +++ b/src/kernel/free_vars.cpp @@ -60,7 +60,7 @@ protected: switch (e.kind()) { case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value: case expr_kind::Var: case expr_kind::MetaVar: // easy cases were already handled - lean_unreachable(); return false; + lean_unreachable(); case expr_kind::App: result = std::any_of(begin_args(e), end_args(e), [=](expr const & arg){ return apply(arg, offset); }); break; @@ -135,7 +135,7 @@ protected: switch (e.kind()) { case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value: case expr_kind::Var: case expr_kind::MetaVar: // easy cases were already handled - lean_unreachable(); return false; + lean_unreachable(); case expr_kind::App: result = std::any_of(begin_args(e), end_args(e), [=](expr const & arg){ return apply(arg, offset); }); break; @@ -183,7 +183,6 @@ expr lower_free_vars(expr const & e, unsigned s, unsigned d) { return mk_var(var_idx(e) - d); } else if (is_metavar(e)) { lean_unreachable(); - return e; } else { return e; } diff --git a/src/kernel/level.cpp b/src/kernel/level.cpp index df01d32ae..dc53571d9 100644 --- a/src/kernel/level.cpp +++ b/src/kernel/level.cpp @@ -149,7 +149,6 @@ level operator+(level const & l, unsigned k) { return max_core(new_lvls.size(), new_lvls.data()); }} lean_unreachable(); - return level(); } level_kind kind (level const & l) { lean_assert(l.m_ptr); return l.m_ptr->m_kind; } @@ -178,7 +177,6 @@ bool operator==(level const & l1, level const & l2) { } } lean_unreachable(); - return false; } bool operator<(level const & l1, level const & l2) { @@ -199,7 +197,6 @@ bool operator<(level const & l1, level const & l2) { return false; } lean_unreachable(); - return false; } std::ostream & operator<<(std::ostream & out, level const & l) { @@ -244,7 +241,6 @@ format pp(level const & l, bool unicode) { } }} lean_unreachable(); - return format(); } format pp(level const & l, options const & opts) { diff --git a/src/kernel/normalizer.cpp b/src/kernel/normalizer.cpp index c4da9f21f..1d88d8e73 100644 --- a/src/kernel/normalizer.cpp +++ b/src/kernel/normalizer.cpp @@ -139,7 +139,6 @@ class normalizer::imp { case svalue_kind::Closure: return reify_closure(to_expr(v), stack_of(v), k); } lean_unreachable(); - return expr(); } /** \brief Return true iff the value_stack does affect the context of a metavariable */ diff --git a/src/kernel/object.h b/src/kernel/object.h index 2f1bf205c..d03ef1183 100644 --- a/src/kernel/object.h +++ b/src/kernel/object.h @@ -36,24 +36,24 @@ public: /** \brief Return true iff object has a name. */ virtual bool has_name() const { return false; } /** \brief Return object name. \pre has_name() */ - virtual name get_name() const { lean_unreachable(); return name(); } + virtual name get_name() const { lean_unreachable(); } /** \brief Has constraint level associated with it (for universal variables). */ virtual bool has_cnstr_level() const { return false; } /** \brief Return the constraint level associated with the object. */ - virtual level get_cnstr_level() const { lean_unreachable(); return level(); } + virtual level get_cnstr_level() const { lean_unreachable(); } /** \brief Return true iff object has a type. */ virtual bool has_type() const { return false; } /** \brief Return object type. \pre has_type() */ - virtual expr get_type() const { lean_unreachable(); return expr(); } + virtual expr get_type() const { lean_unreachable(); } /** \brief Return true iff object is a definition */ virtual bool is_definition() const { return false; } /** \brief Return true iff the definition is opaque. \pre is_definition() */ - virtual bool is_opaque() const { lean_unreachable(); return false; } + virtual bool is_opaque() const { lean_unreachable(); } /** \brief Return object value. \pre is_definition() */ - virtual expr get_value() const { lean_unreachable(); return expr(); } + virtual expr get_value() const { lean_unreachable(); } virtual bool is_axiom() const { return false; } virtual bool is_builtin() const { return false; } diff --git a/src/library/expr_lt.cpp b/src/library/expr_lt.cpp index a9489ab34..8fc8a3eed 100644 --- a/src/library/expr_lt.cpp +++ b/src/library/expr_lt.cpp @@ -16,7 +16,7 @@ bool is_lt(expr const & a, expr const & b) { if (is_var(a)) return var_idx(a) < var_idx(b); switch (a.kind()) { case expr_kind::Var: - lean_unreachable(); return true; // LCOV_EXCL_LINE + lean_unreachable(); case expr_kind::Constant: return const_name(a) < const_name(b); case expr_kind::App: @@ -74,7 +74,6 @@ bool is_lt(expr const & a, expr const & b) { return false; } } - lean_unreachable(); // LCOV_EXCL_LINE - return false; // LCOV_EXCL_LINE + lean_unreachable(); } } diff --git a/src/library/ho_unifier.cpp b/src/library/ho_unifier.cpp index d612fa88e..40977eae5 100644 --- a/src/library/ho_unifier.cpp +++ b/src/library/ho_unifier.cpp @@ -596,7 +596,6 @@ class ho_unifier::imp { return true; case expr_kind::Let: case expr_kind::MetaVar: case expr_kind::App: lean_unreachable(); - return false; } } diff --git a/src/library/light_checker.cpp b/src/library/light_checker.cpp index ec13b074a..95de6cdf7 100644 --- a/src/library/light_checker.cpp +++ b/src/library/light_checker.cpp @@ -123,7 +123,6 @@ class light_checker::imp { case expr_kind::Value: case expr_kind::Type: case expr_kind::MetaVar: lean_unreachable(); - break; case expr_kind::Var: { auto p = lookup_ext(ctx, var_idx(e)); context_entry const & ce = p.first; diff --git a/src/library/max_sharing.cpp b/src/library/max_sharing.cpp index be723d81a..e39c5cb83 100644 --- a/src/library/max_sharing.cpp +++ b/src/library/max_sharing.cpp @@ -73,7 +73,6 @@ struct max_sharing_fn::imp { return r; }} lean_unreachable(); - return a; } expr operator()(expr const & a) { return apply(a); } }; diff --git a/src/library/rewriter/fo_match.cpp b/src/library/rewriter/fo_match.cpp index ccdc556dd..490f067f6 100644 --- a/src/library/rewriter/fo_match.cpp +++ b/src/library/rewriter/fo_match.cpp @@ -184,6 +184,5 @@ bool fo_match::match(expr const & p, expr const & t, unsigned o, subst_map & s) return match_metavar(p, t, o, s); } lean_unreachable(); - return false; } } diff --git a/src/util/debug.h b/src/util/debug.h index c6cc8d9ae..8929df5dc 100644 --- a/src/util/debug.h +++ b/src/util/debug.h @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #pragma once #include +#include "util/exception.h" #ifndef __has_builtin #define __has_builtin(x) 0 @@ -17,11 +18,7 @@ Author: Leonardo de Moura #define DEBUG_CODE(CODE) #endif -#if __has_builtin(__builtin_unreachable) -#define lean_unreachable() __builtin_unreachable() -#else -#define lean_unreachable() DEBUG_CODE({lean::notify_assertion_violation(__FILE__, __LINE__, "UNREACHABLE CODE WAS REACHED."); lean::invoke_debugger();}) -#endif +#define lean_unreachable() DEBUG_CODE({lean::notify_assertion_violation(__FILE__, __LINE__, "UNREACHABLE CODE WAS REACHED."); lean::invoke_debugger();}) throw unreachable_reached(); #ifdef LEAN_DEBUG #define lean_verify(COND) if (!(COND)) { lean::notify_assertion_violation(__FILE__, __LINE__, #COND); lean::invoke_debugger(); } @@ -100,6 +97,13 @@ void disable_debug(char const * tag); bool is_debug_enabled(char const * tag); void invoke_debugger(); bool has_violations(); +/** \brief Exception used to sign that unreachable code was reached */ +class unreachable_reached : public exception { +public: + unreachable_reached() {} + virtual ~unreachable_reached() noexcept {} + virtual char const * what() const noexcept { return "'unreachable' code was reached"; } +}; namespace debug { template void display_var(char const * name, T const & value) { std::cerr << name << " := " << value << "\n"; } } diff --git a/src/util/interval/interval_def.h b/src/util/interval/interval_def.h index 4aec8aa1c..7854b3ebf 100644 --- a/src/util/interval/interval_def.h +++ b/src/util/interval/interval_def.h @@ -1880,7 +1880,6 @@ void interval::csc (interval_deps & deps) { return; } lean_unreachable(); - return; } if (m_lower <= pi && m_upper <= pi) { diff --git a/src/util/numerics/xnumeral.h b/src/util/numerics/xnumeral.h index a03f20503..3c9b67415 100644 --- a/src/util/numerics/xnumeral.h +++ b/src/util/numerics/xnumeral.h @@ -217,13 +217,11 @@ bool lt(T const & a, xnumeral_kind ak, T const & b, xnumeral_kind bk) { return true; default: lean_unreachable(); - return false; } case XN_PLUS_INFINITY: return false; default: lean_unreachable(); - return false; } } diff --git a/src/util/pdeque.h b/src/util/pdeque.h index c2aace081..0d85cfbf6 100644 --- a/src/util/pdeque.h +++ b/src/util/pdeque.h @@ -226,7 +226,7 @@ class pdeque { case cell_kind::PopBack: update_cell(new pop_back_cell(to_pop_back(m_ptr))); break; case cell_kind::PopFront: update_cell(new pop_front_cell(to_pop_front(m_ptr))); break; case cell_kind::Set: update_cell(new set_cell(to_set(m_ptr))); break; - case cell_kind::Root: lean_unreachable(); break; + case cell_kind::Root: lean_unreachable(); } } lean_assert(!is_shared()); diff --git a/src/util/pvector.h b/src/util/pvector.h index 4bc8b1539..8bdf8e231 100644 --- a/src/util/pvector.h +++ b/src/util/pvector.h @@ -191,7 +191,7 @@ class pvector { case cell_kind::PushBack: update_cell(new push_cell(to_push(m_ptr))); break; case cell_kind::PopBack: update_cell(new pop_cell(to_pop(m_ptr))); break; case cell_kind::Set: update_cell(new set_cell(to_set(m_ptr))); break; - case cell_kind::Root: lean_unreachable(); break; + case cell_kind::Root: lean_unreachable(); } } lean_assert(!is_shared()); @@ -397,7 +397,6 @@ unsigned pvector::cell::size() const { return static_cast(this)->m_vector.size(); } lean_unreachable(); - return 0; } template @@ -414,7 +413,6 @@ unsigned pvector::cell::quota() const { } } lean_unreachable(); - return 0; } /** \brief Non-destructive push_back. It is simulated using O(1) copy. */ diff --git a/src/util/sexpr/format.cpp b/src/util/sexpr/format.cpp index 776467867..49a7b200a 100644 --- a/src/util/sexpr/format.cpp +++ b/src/util/sexpr/format.cpp @@ -75,8 +75,7 @@ std::ostream & layout(std::ostream & out, bool colors, sexpr const & s) { case format::format_kind::CHOICE: case format::format_kind::COMPOSE: case format::format_kind::FLAT_COMPOSE: - lean_unreachable(); // LCOV_EXCL_LINE - break; // LCOV_EXCL_LINE + lean_unreachable(); case format::format_kind::NIL: out << ""; @@ -195,8 +194,7 @@ sexpr format::flatten(sexpr const & s) { case format_kind::COLOR_END: return s; } - lean_unreachable(); // LCOV_EXCL_LINE - return s; // LCOV_EXCL_LINE + lean_unreachable(); } format format::flatten(format const & f){ return format(flatten(f.m_value)); @@ -304,8 +302,7 @@ int format::space_upto_line_break(sexpr const & s, int available, bool & found_n return space_upto_line_break(x, available, found_newline); } } - lean_unreachable(); // LCOV_EXCL_LINE - return 0; // LCOV_EXCL_LINE + lean_unreachable(); } sexpr format::be(unsigned w, unsigned k, sexpr const & s) { @@ -360,8 +357,7 @@ sexpr format::be(unsigned w, unsigned k, sexpr const & s) { } } } - lean_unreachable(); // LCOV_EXCL_LINE - return sexpr(); // LCOV_EXCL_LINE + lean_unreachable(); } sexpr format::best(unsigned w, unsigned k, sexpr const & s) { @@ -431,8 +427,7 @@ struct sexpr_pp_fn { } } }} - lean_unreachable(); // LCOV_EXCL_LINE - return format(); // LCOV_EXCL_LINE + lean_unreachable(); } format operator()(sexpr const & s) { diff --git a/src/util/sexpr/sexpr.cpp b/src/util/sexpr/sexpr.cpp index d2a322046..71b324101 100644 --- a/src/util/sexpr/sexpr.cpp +++ b/src/util/sexpr/sexpr.cpp @@ -96,7 +96,7 @@ struct sexpr_cons : public sexpr_cell { void sexpr_cell::dealloc() { switch (m_kind) { - case sexpr_kind::NIL: lean_unreachable(); break; // LCOV_EXCL_LINE + case sexpr_kind::NIL: lean_unreachable(); case sexpr_kind::STRING: delete static_cast(this); break; case sexpr_kind::BOOL: delete static_cast(this); break; case sexpr_kind::INT: delete static_cast(this); break; @@ -193,8 +193,7 @@ bool operator==(sexpr const & a, sexpr const & b) { case sexpr_kind::MPQ: return to_mpq(a) == to_mpq(b); case sexpr_kind::CONS: return head(a) == head(b) && tail(a) == tail(b); } - lean_unreachable(); // LCOV_EXCL_LINE - return false; // LCOV_EXCL_LINE + lean_unreachable(); } int cmp(sexpr const & a, sexpr const & b) { @@ -223,8 +222,7 @@ int cmp(sexpr const & a, sexpr const & b) { return r; return cmp(tail(a), tail(b)); }} - lean_unreachable(); // LCOV_EXCL_LINE - return 0; // LCOV_EXCL_LINE + lean_unreachable(); } std::ostream & operator<<(std::ostream & out, sexpr const & s) {