Skip to content

Fixup GCC 12 errors #7665

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 5 commits into from
Apr 18, 2023
Merged

Fixup GCC 12 errors #7665

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
1c222cb
Fixed UNREACHABLE missing return warning on GCC 12
Apr 12, 2023
7c15f2b
Fixed UNIMPLEMENTED_FEATURE missing return warning
Apr 12, 2023
440093b
Add UNREACHABLE_BECAUSE to fail with a reason
Apr 13, 2023
1a0f60d
Replaced INVARIANT(false) with UNREACHABLE_BECAUSE
Apr 12, 2023
b829f63
Add regression tests for UNREACHABLE_BECAUSE
Apr 13, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions regression/invariants/driver.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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")
Expand Down
12 changes: 12 additions & 0 deletions regression/invariants/invariant-failure21/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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$
5 changes: 2 additions & 3 deletions src/solvers/smt2/smt2_conv.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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(
Expand Down
3 changes: 2 additions & 1 deletion src/solvers/strings/string_format_builtin_function.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
43 changes: 38 additions & 5 deletions src/util/invariant.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 \
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

{ \
INVARIANT(false, "Unreachable"); \
__builtin_unreachable(); \
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

} 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.
Expand All @@ -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

Expand Down