Make implicit switch case fall-throughs explicit (#10284)

This is another PR towards the goal of getting Z3 to compile cleanly
when included via FetchContents into clang-tidy, which uses a pretty
strict set of warnings.

This PR enable the "-Wimplicit-fallthrough" warning, then fix all the
warnings this gets
in the clang build, by:
* Augmenting UNREACHABLE to add __builtin_unreachable(), which
suppresses
warnings for fallthrough in that cse.
* Adding Z3_fallthrough in many cases, to make it clear that
fallthroughs are intentional.
* Adding [[noreturn]] to functions that throw, so the compiler knows
they don't fall through to the next case.
* In a couple of cases, there's a fall-through to a default case, which
does "break", or "return nullptr". In those cases, I duplicated the
action in the preceding case, to make it more self-contained, and robust
in the face of change.

In some cases, I am concerned about whether the warnings are identifying
real bugs. For example, the fall-throughs in these files seem at least a
little suspect:
nnf.cpp
seq_rewriter.cpp
lar_solver.cpp 

while very probably correct, also seem at least a tiny bit suspect.
However, this PR does *not* attempt to change any behavior, only to
silence the warnings. It would be great if somebody with more knowledge
of the code could vet these cases. If vetted, the explicit presence of
the Z3_fallthrough would reassure future readers of the code that the
fall-through is intentional, not accidental.

cmake/compiler_warnings.cmake

@@ -25,6 +25,7 @@ set(CLANG_ONLY_WARNINGS
   "-Winconsistent-missing-override"
   "-Wno-missing-field-initializers"
   "-Wcast-qual"
+  "-Wimplicit-fallthrough"
 )
 
 set(MSVC_WARNINGS "/W3")

src/ast/normal_forms/nnf.cpp

@@ -512,10 +512,12 @@ struct nnf::imp {
             fr.m_i = 1;
             if (!visit(t->get_arg(0), !fr.m_pol, fr.m_in_q))
                 return false;
+            Z3_fallthrough;
         case 1:
             fr.m_i = 2;
             if (!visit(t->get_arg(1), fr.m_pol, fr.m_in_q))
                 return false;
+            Z3_fallthrough;
         default:
             break;
         }
@@ -544,18 +546,22 @@ struct nnf::imp {
             fr.m_i = 1;
             if (!visit(t->get_arg(0), true, fr.m_in_q))
                 return false;
+            Z3_fallthrough;
         case 1:
             fr.m_i = 2;
             if (!visit(t->get_arg(0), false, fr.m_in_q))
                 return false;
+            Z3_fallthrough;
         case 2:
             fr.m_i = 3;
             if (!visit(t->get_arg(1), fr.m_pol, fr.m_in_q))
                 return false;
+            Z3_fallthrough;
         case 3:
             fr.m_i = 4;
             if (!visit(t->get_arg(2), fr.m_pol, fr.m_in_q))
                 return false;
+            Z3_fallthrough;
         default:
             break;
         }
@@ -589,18 +595,22 @@ struct nnf::imp {
             fr.m_i = 1;
             if (!visit(t->get_arg(0), true, fr.m_in_q))
                 return false;
+            Z3_fallthrough;
         case 1:
             fr.m_i = 2;
             if (!visit(t->get_arg(0), false, fr.m_in_q))
                 return false;
+            Z3_fallthrough;
         case 2:
             fr.m_i = 3;
             if (!visit(t->get_arg(1), true, fr.m_in_q))
                 return false;
+            Z3_fallthrough;
         case 3:
             fr.m_i = 4;
             if (!visit(t->get_arg(1), false, fr.m_in_q))
                 return false;
+            Z3_fallthrough;
         default:
             break;
         }

src/ast/rewriter/seq_rewriter.cpp

@@ -103,6 +103,7 @@ br_status seq_rewriter::mk_bool_app(func_decl* f, unsigned n, expr* const* args,
     case OP_EQ:
         SASSERT(n == 2);
         // return mk_eq_helper(args[0], args[1], result);
+        Z3_fallthrough;
     default:
         return BR_FAILED;
     }

src/math/lp/lar_solver.cpp

@@ -2479,6 +2479,7 @@ namespace lp {
             } 
             case GT:
                 y_of_bound += 1;
+                Z3_fallthrough;
             case GE: {
                 auto low = numeric_pair<mpq>(right_side.x, y_of_bound);
                 if (low < get_lower_bound(j)) {

src/muz/spacer/spacer_farkas_learner.cpp

@@ -378,6 +378,7 @@ void farkas_learner::get_lemmas(proof* root, expr_set const& bs, expr_ref_vector
                 INSERT(res);
                 b_closed.mark(p, true);
             }
+            break;
         }
         default:
             break;

src/opt/opt_context.cpp

@@ -650,6 +650,7 @@ namespace opt {
         switch (obj.m_type) {
         case O_MINIMIZE:
             is_ge = !is_ge;
+            Z3_fallthrough;
         case O_MAXIMIZE:
             val = (*mdl)(obj.m_term);
             if (is_numeral(val, k)) {

src/parsers/util/scanner.cpp

@@ -124,6 +124,7 @@ scanner::token scanner::read_id(char first_char) {
             if (!is_alpha || ch != '-') {
                 goto bail_out;  
             }
+            Z3_fallthrough;
         case 'a':
         case ':':
         case '.':

src/sat/smt/pb_card.cpp

@@ -51,7 +51,9 @@ namespace pb {
         double to_add = do_add ? 0 : 1;
         for (literal l : *this) {
             switch (s.value(l)) {
-            case l_true:  --k; if (k == 0) return 0;
+            case l_true:
+                --k; if (k == 0) return 0;
+                Z3_fallthrough;
             case l_undef:
                 if (do_add) to_add += literal_occs(l);
                 ++slack; break;

src/sat/smt/pb_pb.cpp

@@ -95,7 +95,9 @@ namespace pb {
             literal l = wl.second;
             unsigned w = wl.first;
             switch (s.value(l)) {
-            case l_true:  if (k <= w) return 0;
+            case l_true:
+                if (k <= w) return 0;
+                Z3_fallthrough;
             case l_undef:
                 if (do_add) to_add += occs(l);
                 ++undefs;

src/sat/tactic/goal2sat.cpp

@@ -96,7 +96,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
         m_euf = sp.euf() || sp.smt();
     }
 
-    void throw_op_not_handled(std::string const& s) {
+    [[noreturn]] void throw_op_not_handled(std::string const& s) {
         std::string s0 = "operator " + s + " not supported, apply simplifier before invoking translator";
         throw tactic_exception(std::move(s0));
     }

src/smt/theory_arith_core.h

@@ -2460,6 +2460,7 @@ namespace smt {
         case QUASI_BASE:
             quasi_base_row2base_row(get_var_row(v));
             SASSERT(get_var_kind(v) == BASE);
+            Z3_fallthrough;
         case BASE:
             if (!m_to_patch.contains(v) && get_value(v) < k) {
                 TRACE(to_patch_bug, tout << "need to be patched (assert_lower): "; display_var(tout, v););
@@ -2508,6 +2509,7 @@ namespace smt {
         case QUASI_BASE:
             quasi_base_row2base_row(get_var_row(v));
             SASSERT(get_var_kind(v) == BASE);
+            Z3_fallthrough;
         case BASE:
             if (!m_to_patch.contains(v) && get_value(v) > k) {
                 TRACE(to_patch_bug, tout << "need to be patched (assert upper): "; display_var(tout, v););

src/smt/theory_pb.cpp

@@ -2116,6 +2116,7 @@ namespace smt {
             switch(ctx.get_assignment(c.lit(i))) {
             case l_true:
                 ++sum;
+                Z3_fallthrough;
             case l_undef:
                 ++maxsum;
                 break;
@@ -2147,6 +2148,7 @@ namespace smt {
             switch(ctx.get_assignment(c.lit(i))) {
             case l_true:
                 sum += c.coeff(i);
+                Z3_fallthrough;
             case l_undef:
                 maxsum += c.coeff(i);
                 break;

src/tactic/aig/aig.cpp

@@ -480,6 +480,7 @@ struct aig_manager::imp {
                     case OP_EQ:
                         if (!m.m().is_bool(tapp->get_arg(0)))
                             break;
+                        Z3_fallthrough;
                     case OP_NOT:
                     case OP_OR:      
                     case OP_AND:
@@ -1272,10 +1273,12 @@ struct aig_manager::imp {
                     fr.m_idx++;
                     if (!visit(left(n)))
                         goto start;
+                    Z3_fallthrough;
                 case 1:
                     fr.m_idx++;
                     if (!visit(right(n)))
                         goto start;
+                    Z3_fallthrough;
                 default:
                     if (!is_cached(n))
                         improve_sharing(n);

src/tactic/arith/probe_arith.cpp

@@ -135,7 +135,7 @@ struct has_nlmul {
     arith_util   a;
     has_nlmul(ast_manager& m):m(m), a(m) {}
     
-    void throw_found(expr* e) {
+    [[noreturn]] void throw_found(expr* e) {
         TRACE(probe, tout << expr_ref(e, m) << ": " << sort_ref(e->get_sort(), m) << "\n";);
         throw found();
     }

src/tactic/core/elim_uncnstr_tactic.cpp

@@ -763,6 +763,7 @@ class elim_uncnstr_tactic : public tactic {
                     }
                     return r;
                 }
+                return nullptr;
             default:
                 return nullptr;
             }

src/tactic/core/tseitin_cnf_tactic.cpp

@@ -95,7 +95,7 @@ class tseitin_cnf_tactic : public tactic {
         
         void push_frame(app * n) { m_frame_stack.push_back(frame(n)); }
         
-        void throw_op_not_handled() {
+        [[noreturn]] void throw_op_not_handled() {
             throw tactic_exception("operator not supported, apply simplifier before invoking this strategy");
         }
         

src/util/debug.h

@@ -92,10 +92,16 @@ bool is_debug_enabled(const char * tag);
         INVOKE_DEBUGGER();                                                       \
     })
 
-#ifdef Z3DEBUG
-# define UNREACHABLE() DEBUG_CODE(notify_assertion_violation(__FILE__, __LINE__, "UNEXPECTED CODE WAS REACHED."); INVOKE_DEBUGGER();)
+#ifdef __clang__
+#define __compiler_unreachable __builtin_unreachable()
 #else
-# define UNREACHABLE() { notify_assertion_violation(__FILE__, __LINE__, "UNEXPECTED CODE WAS REACHED."); invoke_exit_action(ERR_UNREACHABLE); } ((void) 0)
+#define __compiler_unreachable
+#endif
+
+#ifdef Z3DEBUG
+# define UNREACHABLE() DEBUG_CODE(notify_assertion_violation(__FILE__, __LINE__, "UNEXPECTED CODE WAS REACHED."); INVOKE_DEBUGGER(); __compiler_unreachable;)
+#else
+# define UNREACHABLE() { notify_assertion_violation(__FILE__, __LINE__, "UNEXPECTED CODE WAS REACHED."); invoke_exit_action(ERR_UNREACHABLE); }; __compiler_unreachable
 #endif
 
 #ifdef Z3DEBUG