refactor(debug): improve lean_unreachable(), now we can avoid 'fake' return statements

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

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) {

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 {

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();
         }
     }
 

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) {

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. */

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();
 }
 }

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) {}

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;
         }

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) {

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 */

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; }

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();
 }
 }

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;
             }
         }
 

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;

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); }
 };

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;
 }
 }

src/util/debug.h

@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include <iostream>
+#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<typename T> void display_var(char const * name, T const & value) { std::cerr << name << " := " << value << "\n"; }
 }

src/util/interval/interval_def.h

@@ -1880,7 +1880,6 @@ void interval<T>::csc  (interval_deps & deps) {
             return;
         }
         lean_unreachable();
-        return;
     }
 
     if (m_lower <= pi && m_upper <= pi) {

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;
     }
 }
 

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());

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<T>::cell::size() const {
         return static_cast<root_cell const *>(this)->m_vector.size();
     }
     lean_unreachable();
-    return 0;
 }
 
 template<typename T>
@@ -414,7 +413,6 @@ unsigned pvector<T>::cell::quota() const {
     }
     }
     lean_unreachable();
-    return 0;
 }
 
 /** \brief Non-destructive push_back. It is simulated using O(1) copy. */

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) {

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<sexpr_string*>(this); break;
     case sexpr_kind::BOOL:        delete static_cast<sexpr_bool*>(this);   break;
     case sexpr_kind::INT:         delete static_cast<sexpr_int*>(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) {