From: Andres Noetzli Date: Mon, 18 Nov 2019 20:28:54 +0000 (-0800) Subject: Use -Wimplicit-fallthrough (#3464) X-Git-Tag: cvc5-1.0.0~3831 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=17f0468c1656aa91d7cc5e3174a797312a9364c3;p=cvc5.git Use -Wimplicit-fallthrough (#3464) This commit enables compiler warnings for implicit fallthroughs in switch statements that are not explicitly marked as such. The commit introduces a new macro `CVC4_FALLTHROUGH` that can be used to indicate that a fallthrough is intentional. The commit fixes existing warnings and a bug in the arithmetic rewriter for `abs` (the bug likely couldn't be triggered easily because we rewrite `abs` to an `ite` while expanding definitions). To have the new macro also available in the parser, the commit changes `src/base/check.h` to be visible to the parser (it includes `cvc4_private_library.h` now instead of `cvc4_private.h`). --- diff --git a/CMakeLists.txt b/CMakeLists.txt index fbdd05c95..c2ce3e6ac 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -189,6 +189,7 @@ add_check_c_flag("-fexceptions") add_check_c_cxx_flag("-Wno-deprecated") add_check_cxx_flag("-Wsuggest-override") add_check_cxx_flag("-Wnon-virtual-dtor") +add_check_c_cxx_flag("-Wimplicit-fallthrough") # Temporarily disable -Wclass-memaccess to suppress 'no trivial copy-assignment' # cdlist.h warnings. Remove when fixed. diff --git a/src/base/check.h b/src/base/check.h index 915f6e4cb..93ad71100 100644 --- a/src/base/check.h +++ b/src/base/check.h @@ -29,7 +29,7 @@ ** AlwaysAssert may be added. **/ -#include "cvc4_private.h" +#include "cvc4_private_library.h" #ifndef CVC4__CHECK_H #define CVC4__CHECK_H @@ -65,6 +65,15 @@ #define CVC4_PREDICT_TRUE(x) x #endif +#ifdef __has_cpp_attribute +#if __has_cpp_attribute(fallthrough) +#define CVC4_FALLTHROUGH [[fallthrough]] +#endif // __has_cpp_attribute(fallthrough) +#endif // __has_cpp_attribute +#ifndef CVC4_FALLTHROUGH +#define CVC4_FALLTHROUGH +#endif + namespace CVC4 { // Implementation notes: diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index ae0607b53..b693eae5b 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -15,6 +15,9 @@ **/ #include "parser/smt2/smt2.h" +#include + +#include "base/check.h" #include "expr/type.h" #include "options/options.h" #include "parser/antlr_input.h" @@ -23,8 +26,6 @@ #include "printer/sygus_print_callback.h" #include "util/bitvector.h" -#include - // ANTLR defines these, which is really bad! #undef true #undef false @@ -303,6 +304,7 @@ void Smt2::addTheory(Theory theory) { addOperator(kind::IS_INTEGER, "is_int"); addOperator(kind::TO_REAL, "to_real"); // falling through on purpose, to add Ints part of Reals_Ints + CVC4_FALLTHROUGH; case THEORY_INTS: defineType("Int", getExprManager()->integerType()); addArithmeticOperators(); diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp index c41f1fca9..1695ae2ff 100644 --- a/src/preprocessing/passes/unconstrained_simplifier.cpp +++ b/src/preprocessing/passes/unconstrained_simplifier.cpp @@ -251,6 +251,7 @@ void UnconstrainedSimplifier::processUnconstrained() checkParent = true; break; } + CVC4_FALLTHROUGH; case kind::BITVECTOR_COMP: case kind::LT: case kind::LEQ: @@ -424,6 +425,7 @@ void UnconstrainedSimplifier::processUnconstrained() { break; } + CVC4_FALLTHROUGH; case kind::XOR: case kind::BITVECTOR_XOR: case kind::BITVECTOR_XNOR: diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 0d3bab3d0..1f45d8536 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -615,7 +615,7 @@ void Smt2Printer::toStream(std::ostream& out, // arrays theory case kind::SELECT: - case kind::STORE: typeChildren = true; + case kind::STORE: typeChildren = true; CVC4_FALLTHROUGH; case kind::PARTIAL_SELECT_0: case kind::PARTIAL_SELECT_1: case kind::ARRAY_TYPE: @@ -751,7 +751,7 @@ void Smt2Printer::toStream(std::ostream& out, parametricTypeChildren = true; out << smtKindString(k, d_variant) << " "; break; - case kind::MEMBER: typeChildren = true; + case kind::MEMBER: typeChildren = true; CVC4_FALLTHROUGH; case kind::INSERT: case kind::SET_TYPE: case kind::SINGLETON: diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp index 1f3e6abf1..8b9204a20 100644 --- a/src/proof/theory_proof.cpp +++ b/src/proof/theory_proof.cpp @@ -1186,7 +1186,7 @@ void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLe } // If letification is off or there were 2 children, same treatment as the other cases. - // (No break is intentional). + CVC4_FALLTHROUGH; case kind::XOR: case kind::IMPLIES: case kind::NOT: diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 7df5fb492..6d60bfafc 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -740,6 +740,7 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool negated) { convertAndAssertIff(node, negated); break; } + CVC4_FALLTHROUGH; default: { Node nnode = node; diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index c95d6f53d..13ab03b45 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -197,6 +197,7 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){ NodeManager::currentNM()->mkConst(-rat)); } } + return RewriteResponse(REWRITE_DONE, t); case kind::TO_REAL: return RewriteResponse(REWRITE_DONE, t[0]); case kind::TO_INTEGER: diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp index e17605ead..810eded82 100644 --- a/src/theory/arith/arith_static_learner.cpp +++ b/src/theory/arith/arith_static_learner.cpp @@ -252,25 +252,23 @@ void ArithStaticLearner::addBound(TNode n) { DeltaRational bound = constant; switch(Kind k = n.getKind()) { - case kind::LT: - bound = DeltaRational(constant, -1); - /* fall through */ - case kind::LEQ: - if (maxFind == d_maxMap.end() || (*maxFind).second > bound) { - d_maxMap.insert(n[0], bound); - Debug("arith::static") << "adding bound " << n << endl; - } - break; - case kind::GT: - bound = DeltaRational(constant, 1); - /* fall through */ - case kind::GEQ: - if (minFind == d_minMap.end() || (*minFind).second < bound) { - d_minMap.insert(n[0], bound); - Debug("arith::static") << "adding bound " << n << endl; - } - break; - default: Unhandled() << k; break; + case kind::LT: bound = DeltaRational(constant, -1); CVC4_FALLTHROUGH; + case kind::LEQ: + if (maxFind == d_maxMap.end() || (*maxFind).second > bound) + { + d_maxMap.insert(n[0], bound); + Debug("arith::static") << "adding bound " << n << endl; + } + break; + case kind::GT: bound = DeltaRational(constant, 1); CVC4_FALLTHROUGH; + case kind::GEQ: + if (minFind == d_minMap.end() || (*minFind).second < bound) + { + d_minMap.insert(n[0], bound); + Debug("arith::static") << "adding bound " << n << endl; + } + break; + default: Unhandled() << k; break; } } diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 62be1fcc1..a6a47c73c 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -5392,6 +5392,7 @@ std::pair TheoryArithPrivate::entailmentCheck(TNode lit, const Arith } // intentionally fall through to DISTINCT case! // entailments of negations are eager exit cases for EQUAL + CVC4_FALLTHROUGH; case DISTINCT: if(!bestPrimDiff.first.isNull()){ // primDir [dm * dp] <= primDir * dm * U < primDir * sep diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp index 56d0c59cc..49ceebfd6 100644 --- a/src/theory/uf/symmetry_breaker.cpp +++ b/src/theory/uf/symmetry_breaker.cpp @@ -370,7 +370,7 @@ Node SymmetryBreaker::normInternal(TNode n, size_t level) { Debug("ufsymm:eq") << "UFSYMM " << n[0] << " <==> " << n[1] << endl; } } - /* intentional fall-through! */ + CVC4_FALLTHROUGH; case kind::XOR: // commutative binary operator handling return n[1] < n[0] ? NodeManager::currentNM()->mkNode(k, n[1], n[0]) : Node(n); diff --git a/src/util/sampler.cpp b/src/util/sampler.cpp index eeb38f988..60d38bb34 100644 --- a/src/util/sampler.cpp +++ b/src/util/sampler.cpp @@ -73,37 +73,27 @@ FloatingPoint Sampler::pickFpBiased(unsigned e, unsigned s) // +/- inf // sign = x, exp = 11...11, sig = 00...00 - case 1: - sign = one; - // Intentional fall-through + case 1: sign = one; CVC4_FALLTHROUGH; case 2: exp = BitVector::mkOnes(e); break; // +/- zero // sign = x, exp = 00...00, sig = 00...00 - case 3: - sign = one; - // Intentional fall-through + case 3: sign = one; CVC4_FALLTHROUGH; case 4: break; // +/- max subnormal // sign = x, exp = 00...00, sig = 11...11 - case 5: - sign = one; - // Intentional fall-through + case 5: sign = one; CVC4_FALLTHROUGH; case 6: sig = BitVector::mkOnes(s - 1); break; // +/- min subnormal // sign = x, exp = 00...00, sig = 00...01 - case 7: - sign = one; - // Intentional fall-through + case 7: sign = one; CVC4_FALLTHROUGH; case 8: sig = BitVector(s - 1, static_cast(1)); break; // +/- max normal // sign = x, exp = 11...10, sig = 11...11 - case 9: - sign = one; - // Intentional fall-through + case 9: sign = one; CVC4_FALLTHROUGH; case 10: exp = BitVector::mkOnes(e) - BitVector(e, static_cast(1)); sig = BitVector::mkOnes(s - 1); @@ -111,9 +101,7 @@ FloatingPoint Sampler::pickFpBiased(unsigned e, unsigned s) // +/- min normal // sign = x, exp = 00...01, sig = 00...00 - case 11: - sign = one; - // Intentional fall-through + case 11: sign = one; CVC4_FALLTHROUGH; case 12: exp = BitVector(e, static_cast(1)); break; default: Unreachable(); diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h index 235931efd..0e71fe911 100644 --- a/test/unit/theory/theory_arith_white.h +++ b/test/unit/theory/theory_arith_white.h @@ -323,5 +323,9 @@ public: TS_ASSERT_EQUALS(Rewriter::rewrite(leq0), Rewriter::rewrite(geq1.notNode())); TS_ASSERT_EQUALS(Rewriter::rewrite(leq1), Rewriter::rewrite(geq2.notNode())); + + // (abs x) --> (abs x) + Node absX = d_nm->mkNode(ABS, x); + TS_ASSERT_EQUALS(Rewriter::rewrite(absX), absX); } };