From d46fbad3b602a471a05333fbe70d75d64beb1bd7 Mon Sep 17 00:00:00 2001 From: davedets Date: Wed, 29 Jul 2026 09:05:42 -0700 Subject: [PATCH] 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 | 1 + src/ast/normal_forms/nnf.cpp | 10 ++++++++++ src/ast/rewriter/seq_rewriter.cpp | 1 + src/math/lp/lar_solver.cpp | 1 + src/muz/spacer/spacer_farkas_learner.cpp | 1 + src/opt/opt_context.cpp | 1 + src/parsers/util/scanner.cpp | 1 + src/sat/smt/pb_card.cpp | 4 +++- src/sat/smt/pb_pb.cpp | 4 +++- src/sat/tactic/goal2sat.cpp | 2 +- src/smt/theory_arith_core.h | 2 ++ src/smt/theory_pb.cpp | 2 ++ src/tactic/aig/aig.cpp | 3 +++ src/tactic/arith/probe_arith.cpp | 2 +- src/tactic/core/elim_uncnstr_tactic.cpp | 1 + src/tactic/core/tseitin_cnf_tactic.cpp | 2 +- src/util/debug.h | 12 +++++++++--- 17 files changed, 42 insertions(+), 8 deletions(-) diff --git a/cmake/compiler_warnings.cmake b/cmake/compiler_warnings.cmake index 9e11d9082b..b9424e1b25 100644 --- a/cmake/compiler_warnings.cmake +++ b/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") diff --git a/src/ast/normal_forms/nnf.cpp b/src/ast/normal_forms/nnf.cpp index 219cea3f86..84079bf7c8 100644 --- a/src/ast/normal_forms/nnf.cpp +++ b/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; } diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index af45569b40..8aed5bf43a 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/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; } diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index 0eb204f19d..a47eb6ede6 100644 --- a/src/math/lp/lar_solver.cpp +++ b/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(right_side.x, y_of_bound); if (low < get_lower_bound(j)) { diff --git a/src/muz/spacer/spacer_farkas_learner.cpp b/src/muz/spacer/spacer_farkas_learner.cpp index 3016b69fe9..263cffadda 100644 --- a/src/muz/spacer/spacer_farkas_learner.cpp +++ b/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; diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index b3a1661d67..06b2a60a56 100644 --- a/src/opt/opt_context.cpp +++ b/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)) { diff --git a/src/parsers/util/scanner.cpp b/src/parsers/util/scanner.cpp index a10c50150e..c30543ba1b 100644 --- a/src/parsers/util/scanner.cpp +++ b/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 '.': diff --git a/src/sat/smt/pb_card.cpp b/src/sat/smt/pb_card.cpp index eaa994b677..f88ae499fd 100644 --- a/src/sat/smt/pb_card.cpp +++ b/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; diff --git a/src/sat/smt/pb_pb.cpp b/src/sat/smt/pb_pb.cpp index a2cb20a895..a718e9ebde 100644 --- a/src/sat/smt/pb_pb.cpp +++ b/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; diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 0e6d88b1a1..f85f747ffa 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/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)); } diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 2c352a6a25..123f40978c 100644 --- a/src/smt/theory_arith_core.h +++ b/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);); diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index 40c2cec2ae..e0e2b1ea51 100644 --- a/src/smt/theory_pb.cpp +++ b/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; diff --git a/src/tactic/aig/aig.cpp b/src/tactic/aig/aig.cpp index fc165b009a..a0b7d05382 100644 --- a/src/tactic/aig/aig.cpp +++ b/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); diff --git a/src/tactic/arith/probe_arith.cpp b/src/tactic/arith/probe_arith.cpp index 85d9acd9a0..3e2596e9f6 100644 --- a/src/tactic/arith/probe_arith.cpp +++ b/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(); } diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp index 7aecd4d505..0d836bf4d5 100644 --- a/src/tactic/core/elim_uncnstr_tactic.cpp +++ b/src/tactic/core/elim_uncnstr_tactic.cpp @@ -763,6 +763,7 @@ class elim_uncnstr_tactic : public tactic { } return r; } + return nullptr; default: return nullptr; } diff --git a/src/tactic/core/tseitin_cnf_tactic.cpp b/src/tactic/core/tseitin_cnf_tactic.cpp index ba396a7565..886a603cd7 100644 --- a/src/tactic/core/tseitin_cnf_tactic.cpp +++ b/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"); } diff --git a/src/util/debug.h b/src/util/debug.h index 4be061e562..481d46e1a8 100644 --- a/src/util/debug.h +++ b/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