Tolerate TS 18661 (_Float32 et al) types

[smowton]

I got fed up with a bunch of cbmc test spuriously failing with Glibc 2.27+, so here's a short-term workaround until #2170 is fixed. I'm aware this isn't quite right, as I think it would also tolerate "typedef float double long double float _Float64x", but it seems to at least restore sanity in the meantime and shouldn't last long.

Commit message follows:

Because we currently claim GCC 4.2.1 support, but also define the TS 18661 floating point types,
we confuse Glibc 2.27+, which checks for GCC >= 7.0 and otherwise defines the types itself.
In the long run we should either upgrade our support to GCC 7.0 standard, or else stop providing
these types and simply ask users interested in these types to use Glibc 2.27 or provide their own
headers; in the meantime this workaround permits us to avoid crashing whenever math.h is included.

[peterschrammel]

I think that's an acceptable workaround for the time being. Please create an issue for documenting the bigger problem.

[smowton]

#2170

[tautschnig]

1. Could you please add a regression test? No need for includes, just a local typedef.
2. I would declare this a fix of New _Float32 type conflicts with libc Ubuntu GLIBC 2.27-3ubuntu1 #2170.
3. My preferred solution is to get rid of the preprocessing code in ansi-c/ and instead always use goto-cc's approach (and code).
4. There should be an issue tracking 3) above, with a note that fixing that would also allow us to drop this bit of code.

[smowton]

Personally I'd say using the system's GCC for preproc is actually worse, as it means the resulting code depends on the version of GCC you happen to have installed. For example, for GCC >= 4.4 glibc expects a __builtin_fpclassify function to be provided (which overloads one of its arguments, so can't be implemented in C; thus this is actually broken with goto-cc right now, we just don't have a test for it). Similar breakages would surely accrue with each GCC release. Compare cbmc is actually doing the same thing as Clang, defining GNUC_MAJOR_VERSION et al to claim to be a particular version of GCC, giving it a stationary target to emulate.

Hence a reasonable solution would be to revert #2146, switch goto-cc to use cbmc's approach, and require people wanting the new types to use glibc >= 2.27, which provides fallback typedefs for them.

[tautschnig]

Personally I'd say using the system's GCC for preproc is actually worse, as it means the resulting code depends on the version of GCC you happen to have installed.

I'd consider this a feature, not a bug. People build their software, run tests, etc. We verify the same code that they build. That breakage may occur with every GCC version is our problem, not the end-user's business.

[smowton]

That's true, but supporting every GCC version between 4.2.1 and present... that's a heck of a regression test suite! I don't envy you the task!

[tautschnig]

That's true, but supporting every GCC version between 4.2.1 and present... that's a heck of a regression test suite! I don't envy you the task!

Yes, setting this up properly is to be done. Speaking of which: how did you notice the __builtin_fpclassify problem, and would you be able to provide a test snippet?

[smowton]

I changed https://github.com/diffblue/cbmc/blob/develop/src/ansi-c/c_preprocess.cpp#L680 to 7 (and the minor and patchlevel defs, to claim GCC 7.0.0) and ran the cbmc tests. Float21, for example, failed.

[smowton]

@tautschnig @peterschrammel I've updated this PR with a test, comment and a slightly better warning message.

One other possibility btw: is it possible to customise the parser to only recognise these tokens when emulating GCC >= 7.0? For now cbmc would statically define its emulated version as 4.2.1, while goto-cc would extract its emulated version using $real_gcc --version. Unfortunately I don't know enough about flex/bison to do this just yet.