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`).

13 files changed, 51 insertions, 44 deletions

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 <algorithm>
+
+#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 <algorithm>
-
 // 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<bool, Node> 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<unsigned int>(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<unsigned int>(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<unsigned int>(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);
   }
 };