Merge pull request #7665 from esteffin/esteffin/gcc-12-unreachable-fix

Fixup GCC 12 errors

Author: NlightNFotis

regression/invariants/driver.cpp

@@ -112,6 +112,8 @@ int main(int argc, char** argv)
     UNREACHABLE_STRUCTURED(structured_error_testt, 1, "Structured error"); // NOLINT
   else if(arg=="unreachable-string")
     UNREACHABLE;
+  else if(arg == "unreachable-because")
+    UNREACHABLE_BECAUSE("Unreachable with explanation text");
   else if(arg=="data-invariant-structured")
     DATA_INVARIANT_STRUCTURED(false, structured_error_testt, 1, "Structured error"); // NOLINT
   else if(arg=="data-invariant-string")

regression/invariants/invariant-failure21/test.desc

@@ -0,0 +1,12 @@
+CORE
+dummy_parameter.c
+unreachable-because
+^EXIT=(0|127|134|137)$
+^SIGNAL=0$
+--- begin invariant violation report ---
+Unreachable with explanation text
+Invariant check failed
+^(Backtrace)|(Backtraces not supported)$
+--
+^warning: ignoring
+^VERIFICATION SUCCESSFUL$

src/solvers/smt2/smt2_conv.cpp

@@ -516,10 +516,9 @@ constant_exprt smt2_convt::parse_literal(
     return from_integer(value, type);
   }
   else
-    INVARIANT(
-      false,
+    UNREACHABLE_BECAUSE(
       "smt2_convt::parse_literal should not be of unsupported type " +
-        type.id_string());
+      type.id_string());
 }
 
 exprt smt2_convt::parse_array(

src/solvers/strings/string_format_builtin_function.cpp

@@ -232,7 +232,8 @@ add_axioms_for_format_specifier(
   }
   }
 
-  INVARIANT(false, "format specifier must belong to [bBhHsScCdoxXeEfgGaAtT%n]");
+  UNREACHABLE_BECAUSE(
+    "format specifier must belong to [bBhHsScCdoxXeEfgGaAtT%n]");
 }
 
 /// Deserialize an argument for format from \p string.

src/util/invariant.h

@@ -500,9 +500,33 @@ CBMC_NORETURN void report_invariant_failure(
   EXPAND_MACRO(INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__))
 
 /// This should be used to mark dead code
-#define UNREACHABLE INVARIANT(false, "Unreachable")
-#define UNREACHABLE_STRUCTURED(TYPENAME, ...)                                  \
-  EXPAND_MACRO(INVARIANT_STRUCTURED(false, TYPENAME, __VA_ARGS__))
+#ifdef __GNUC__
+// GCC 12 with -O0 fails reporting missing return when using UNREACHABLE.
+// Using __builtin_unreachable fixes this without breaking the invariant.
+#  define UNREACHABLE                                                          \
+    do                                                                         \
+    {                                                                          \
+      INVARIANT(false, "Unreachable");                                         \
+      __builtin_unreachable();                                                 \
+    } while(false)
+#  define UNREACHABLE_BECAUSE(REASON)                                          \
+    do                                                                         \
+    {                                                                          \
+      INVARIANT(false, REASON);                                                \
+      __builtin_unreachable();                                                 \
+    } while(false)
+#  define UNREACHABLE_STRUCTURED(TYPENAME, ...)                                \
+    do                                                                         \
+    {                                                                          \
+      EXPAND_MACRO(INVARIANT_STRUCTURED(false, TYPENAME, __VA_ARGS__));        \
+      __builtin_unreachable();                                                 \
+    } while(false)
+#else
+#  define UNREACHABLE INVARIANT(false, "Unreachable")
+#  define UNREACHABLE_BECAUSE(REASON) INVARIANT(false, REASON)
+#  define UNREACHABLE_STRUCTURED(TYPENAME, ...)                                \
+    EXPAND_MACRO(INVARIANT_STRUCTURED(false, TYPENAME, __VA_ARGS__))
+#endif
 
 /// This condition should be used to document that assumptions that are
 /// made on goto_functions, goto_programs, exprts, etc. being well formed.
@@ -514,8 +538,17 @@ CBMC_NORETURN void report_invariant_failure(
 #define DATA_INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...)                    \
   EXPAND_MACRO(INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__))
 
-#define UNIMPLEMENTED_FEATURE(FEATURE)                                         \
-  INVARIANT(false, std::string{"Reached unimplemented "} + (FEATURE))
+#if __GNUC__
+#  define UNIMPLEMENTED_FEATURE(FEATURE)                                       \
+    do                                                                         \
+    {                                                                          \
+      INVARIANT(false, std::string{"Reached unimplemented "} + (FEATURE));     \
+      __builtin_unreachable();                                                 \
+    } while(false)
+#else
+#  define UNIMPLEMENTED_FEATURE(FEATURE)                                       \
+    INVARIANT(false, std::string{"Reached unimplemented "} + (FEATURE))
+#endif
 
 // Legacy annotations