Fixup GCC 12 errors

[esteffin]

GCC 12 when using -O0 fails because of a missing-return-statement warning caused by the implementation of INVARIANT(false).

This is because the condition if (true) is not considered exahustive.

The solution involves marking the unreachable path as __builtin_unreachable().

This PR also replaces some INVARIANT(false, REASON) statement used to have UNREACHABLE, but with a reason.

• Each commit message has a non-empty body, explaining why the change was made.
• Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[codecov]

Codecov Report

Patch coverage has no change and project coverage change: +0.09 🎉

Comparison is base (68af7a4) 78.42% compared to head (b829f63) 78.51%.

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #7665      +/-   ##
===========================================
+ Coverage    78.42%   78.51%   +0.09%     
===========================================
  Files         1674     1674              
  Lines       191935   191933       -2     
===========================================
+ Hits        150521   150704     +183     
+ Misses       41414    41229     -185     

Impacted Files	Coverage Δ
src/solvers/smt2/smt2_conv.cpp	67.39% <ø> (+0.02%)	⬆️
...solvers/strings/string_format_builtin_function.cpp	73.10% <ø> (+0.16%)	⬆️
src/util/invariant.h	95.55% <ø> (ø)

... and 10 files with indirect coverage changes

Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here.

☔ View full report in Codecov by Sentry.
📢 Do you have feedback about the report comment? Let us know in this issue.

[NlightNFotis]

Why do we need a new do ... while(false) block here? The INVARIANT definition has one of its own.

Would it make more sense to just have a block { INVARIANT(false, "Unreachable"); __builtin_unreachable(); } or am I mistaken?

[esteffin]

The do { ... } while (false) in the macros is because it allows a ; (semicolon) after the macro, but does not require it (it works with both).

It is a common C methodology.

[tautschnig]

Shouldn't we instead be adding this to the expansion of the INVARIANT macro?

[esteffin]

No as the invariant can actually be satisfied (INVARIANT(condition, "some reason") succeed when condition is true).

The problem is just related to GCC 12 with -O0 refusing to statically resolve cases of the form if (true) { <terminate> }.

The only cases I found of this are UNREACHABLE, UNIMPLEMENTED_FEATURE and some INVARIANT(false, "unreachable because") and they have all been fixed.

[tautschnig]

What I meant was putting the __builtin_unreachable() inside the if(!(CONDITION)) branch, which wouldn't have the problem of the invariant being satisfied. Wouldn't that have worked? (It's possible that GCC's reachability analysis will remain confused in that case.)