From b0d1f9e0016a414dccca004e4dc4d23cc3596e5d Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Wed, 6 Jun 2018 17:14:20 +0100 Subject: [PATCH 1/4] Restore _Float128 support by default _Float128 was exposed by GCC as of version 4.3 (x86-64) to 4.5 (i386 and I think others). cbmc still makes no effort to imitate a particular GCC version, so I simply enable recognising the token by default, which used to happen universally; goto-cc on the other hand uses the new `gcc_versiont` to choose an appropriate behaviour. This fixes a regression on tests using math.h due to some versions of glibc defining _Float128 conditional on the compiler version, which cbmc and goto-cc now both allow to appear like the gcc found on the path. --- src/ansi-c/ansi_c_language.cpp | 1 + src/ansi-c/ansi_c_parser.h | 6 +++++- src/ansi-c/scanner.l | 2 +- src/cpp/cpp_parser.cpp | 1 + src/goto-cc/gcc_mode.cpp | 6 ++++++ src/util/config.cpp | 3 +++ src/util/config.h | 1 + 7 files changed, 18 insertions(+), 2 deletions(-) diff --git a/src/ansi-c/ansi_c_language.cpp b/src/ansi-c/ansi_c_language.cpp index 16d63d06157..fc412f0387e 100644 --- a/src/ansi-c/ansi_c_language.cpp +++ b/src/ansi-c/ansi_c_language.cpp @@ -76,6 +76,7 @@ bool ansi_c_languaget::parse( ansi_c_parser.set_message_handler(get_message_handler()); ansi_c_parser.for_has_scope=config.ansi_c.for_has_scope; ansi_c_parser.ts_18661_3_Floatn_types=config.ansi_c.ts_18661_3_Floatn_types; + ansi_c_parser.Float128_type = config.ansi_c.Float128_type; ansi_c_parser.cpp98=false; // it's not C++ ansi_c_parser.cpp11=false; // it's not C++ ansi_c_parser.mode=config.ansi_c.mode; diff --git a/src/ansi-c/ansi_c_parser.h b/src/ansi-c/ansi_c_parser.h index a7c03191fce..0dee96c5a18 100644 --- a/src/ansi-c/ansi_c_parser.h +++ b/src/ansi-c/ansi_c_parser.h @@ -36,7 +36,8 @@ class ansi_c_parsert:public parsert cpp98(false), cpp11(false), for_has_scope(false), - ts_18661_3_Floatn_types(false) + ts_18661_3_Floatn_types(false), + Float128_type(false) { } @@ -81,6 +82,9 @@ class ansi_c_parsert:public parsert // ISO/IEC TS 18661-3:2015 bool ts_18661_3_Floatn_types; + // Does the compiler version emulated provide _Float128? + bool Float128_type; + typedef ansi_c_identifiert identifiert; typedef ansi_c_scopet scopet; diff --git a/src/ansi-c/scanner.l b/src/ansi-c/scanner.l index c45228e9ca5..29e5da340e7 100644 --- a/src/ansi-c/scanner.l +++ b/src/ansi-c/scanner.l @@ -503,7 +503,7 @@ void ansi_c_scanner_init() return make_identifier(); } -"_Float128" { if(PARSER.ts_18661_3_Floatn_types) +"_Float128" { if(PARSER.Float128_type) { loc(); return TOK_GCC_FLOAT128; } else return make_identifier(); diff --git a/src/cpp/cpp_parser.cpp b/src/cpp/cpp_parser.cpp index e73fba627f9..59b9be5e4e0 100644 --- a/src/cpp/cpp_parser.cpp +++ b/src/cpp/cpp_parser.cpp @@ -25,6 +25,7 @@ bool cpp_parsert::parse() config.cpp.cpp_standard==configt::cppt::cpp_standardt::CPP11 || config.cpp.cpp_standard==configt::cppt::cpp_standardt::CPP14; ansi_c_parser.ts_18661_3_Floatn_types=false; + ansi_c_parser.Float128_type = false; ansi_c_parser.in=in; ansi_c_parser.mode=mode; ansi_c_parser.set_file(get_file()); diff --git a/src/goto-cc/gcc_mode.cpp b/src/goto-cc/gcc_mode.cpp index f4dee67c0dc..94ca81ccbac 100644 --- a/src/goto-cc/gcc_mode.cpp +++ b/src/goto-cc/gcc_mode.cpp @@ -530,6 +530,12 @@ int gcc_modet::doit() gcc_version.is_at_least(7)) config.ansi_c.ts_18661_3_Floatn_types=true; + int gcc_float128_minor_version = config.ansi_c.arch == "x86_64" ? 3 : 5; + + config.ansi_c.Float128_type = + gcc_version.flavor == gcc_versiont::flavort::GCC && + gcc_version.is_at_least(4, gcc_float128_minor_version); + // -fshort-double makes double the same as float if(cmdline.isset("fshort-double")) config.ansi_c.double_width=config.ansi_c.single_width; diff --git a/src/util/config.cpp b/src/util/config.cpp index f9ce580485d..521c1b7dbad 100644 --- a/src/util/config.cpp +++ b/src/util/config.cpp @@ -912,6 +912,9 @@ bool configt::set(const cmdlinet &cmdline) ansi_c.preprocessor=ansi_ct::preprocessort::GCC; } + if(ansi_c.preprocessor == ansi_ct::preprocessort::GCC) + ansi_c.Float128_type = true; + set_arch(arch); if(os=="windows") diff --git a/src/util/config.h b/src/util/config.h index 9f3bf9ee61a..2209d92b4ab 100644 --- a/src/util/config.h +++ b/src/util/config.h @@ -43,6 +43,7 @@ class configt bool char_is_unsigned, wchar_t_is_unsigned; bool for_has_scope; bool ts_18661_3_Floatn_types; // ISO/IEC TS 18661-3:2015 + bool Float128_type; bool single_precision_constant; enum class c_standardt { C89, C99, C11 } c_standard; static c_standardt default_c_standard(); From b46e4bf562d7fb1bf1ace204569d876dc19a0e6b Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Thu, 7 Jun 2018 10:31:13 +0100 Subject: [PATCH 2/4] Improve gcc-4 and -7 tests These now check all ts18661 types, and the wrapper scripts avoid argument re-parsing --- regression/ansi-c/gcc_version1/fake-gcc-4 | 2 +- regression/ansi-c/gcc_version1/fake-gcc-7 | 2 +- regression/ansi-c/gcc_version1/gcc-4.c | 8 +++++++- regression/ansi-c/gcc_version1/gcc-7.c | 9 +++++++-- 4 files changed, 16 insertions(+), 5 deletions(-) diff --git a/regression/ansi-c/gcc_version1/fake-gcc-4 b/regression/ansi-c/gcc_version1/fake-gcc-4 index 7519ebbb295..b28d4c34836 100755 --- a/regression/ansi-c/gcc_version1/fake-gcc-4 +++ b/regression/ansi-c/gcc_version1/fake-gcc-4 @@ -1,4 +1,4 @@ #!/bin/sh -gcc -Wno-macro-redefined -U __clang_major__ -D __GNUC__=4 -D __GNUC_MINOR__=9 -D __GNUC_PATCHLEVEL__=1 $* +gcc -Wno-macro-redefined -U __clang_major__ -D __GNUC__=4 -D __GNUC_MINOR__=2 -D __GNUC_PATCHLEVEL__=1 "$@" diff --git a/regression/ansi-c/gcc_version1/fake-gcc-7 b/regression/ansi-c/gcc_version1/fake-gcc-7 index 2677c324fc4..081e44240fd 100755 --- a/regression/ansi-c/gcc_version1/fake-gcc-7 +++ b/regression/ansi-c/gcc_version1/fake-gcc-7 @@ -1,4 +1,4 @@ #!/bin/sh -gcc -Wno-macro-redefined -U __clang_major__ -D __GNUC__=7 -D __GNUC_MINOR__=0 -D __GNUC_PATCHLEVEL__=0 $* +gcc -Wno-macro-redefined -U __clang_major__ -D __GNUC__=7 -D __GNUC_MINOR__=0 -D __GNUC_PATCHLEVEL__=0 "$@" diff --git a/regression/ansi-c/gcc_version1/gcc-4.c b/regression/ansi-c/gcc_version1/gcc-4.c index 146830401fb..4d625cef096 100644 --- a/regression/ansi-c/gcc_version1/gcc-4.c +++ b/regression/ansi-c/gcc_version1/gcc-4.c @@ -1,2 +1,8 @@ -typedef double _Float64; +// None of these types should be defined when emulating gcc-4: +typedef float _Float32; +typedef double _Float32x; +typedef double _Float64; +typedef long double _Float64x; +typedef long double _Float128; +typedef long double _Float128x; diff --git a/regression/ansi-c/gcc_version1/gcc-7.c b/regression/ansi-c/gcc_version1/gcc-7.c index f2b0379790b..94aad952ebf 100644 --- a/regression/ansi-c/gcc_version1/gcc-7.c +++ b/regression/ansi-c/gcc_version1/gcc-7.c @@ -1,2 +1,7 @@ -_Float64 some_var; - +// All these types should be provided when emulating gcc-7: +_Float32 f32; +_Float32x f32x; +_Float64 f64; +_Float64x f64x; +_Float128 f128; +_Float128x f128x; From 4180e654f2671aea3489253b7e36a212c7afd1a5 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Thu, 7 Jun 2018 10:32:16 +0100 Subject: [PATCH 3/4] Add test for gcc-5 This version should expose _Float128, but not other ts18661 types --- regression/ansi-c/gcc_version1/fake-gcc-5 | 3 +++ regression/ansi-c/gcc_version1/gcc-5.c | 9 +++++++++ regression/ansi-c/gcc_version1/test-gcc-5.desc | 7 +++++++ 3 files changed, 19 insertions(+) create mode 100755 regression/ansi-c/gcc_version1/fake-gcc-5 create mode 100644 regression/ansi-c/gcc_version1/gcc-5.c create mode 100644 regression/ansi-c/gcc_version1/test-gcc-5.desc diff --git a/regression/ansi-c/gcc_version1/fake-gcc-5 b/regression/ansi-c/gcc_version1/fake-gcc-5 new file mode 100755 index 00000000000..567dae0a7b2 --- /dev/null +++ b/regression/ansi-c/gcc_version1/fake-gcc-5 @@ -0,0 +1,3 @@ +#!/bin/sh + +gcc -Wno-macro-redefined -U __clang_major__ -D __GNUC__=5 -D __GNUC_MINOR__=0 -D __GNUC_PATCHLEVEL__=0 "$@" diff --git a/regression/ansi-c/gcc_version1/gcc-5.c b/regression/ansi-c/gcc_version1/gcc-5.c new file mode 100644 index 00000000000..83e2d409263 --- /dev/null +++ b/regression/ansi-c/gcc_version1/gcc-5.c @@ -0,0 +1,9 @@ +// These types should *not* be provided when emulating gcc-5: +typedef float _Float32; +typedef double _Float32x; +typedef double _Float64; +typedef long double _Float64x; +typedef long double _Float128x; + +// But this type should: +_Float128 f128; diff --git a/regression/ansi-c/gcc_version1/test-gcc-5.desc b/regression/ansi-c/gcc_version1/test-gcc-5.desc new file mode 100644 index 00000000000..aaa4eb3ac65 --- /dev/null +++ b/regression/ansi-c/gcc_version1/test-gcc-5.desc @@ -0,0 +1,7 @@ +CORE +gcc-5.c +--native-compiler ./fake-gcc-5 +^EXIT=0$ +^SIGNAL=0$ +-- +^CONVERSION ERROR$ From 7b6148279371942a95a93884fbbdeba81c2e8218 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Thu, 7 Jun 2018 10:32:47 +0100 Subject: [PATCH 4/4] Extend cbmc ts18661 test This now expects to find _Float128 when gcc-4.3+ (x86-64) for -4.5+ (other targets) is in use. --- regression/cbmc/ts18661_typedefs/main.c | 20 +++++++++++++++++--- 1 file changed, 17 insertions(+), 3 deletions(-) diff --git a/regression/cbmc/ts18661_typedefs/main.c b/regression/cbmc/ts18661_typedefs/main.c index 1c3972d9656..8fc3d9c62d9 100644 --- a/regression/cbmc/ts18661_typedefs/main.c +++ b/regression/cbmc/ts18661_typedefs/main.c @@ -1,8 +1,19 @@ -#if defined(__clang__) -#elif defined(__GNUC__) +#if defined(__GNUC__) && !defined(__clang__) + +#include // For __GNUC_PREREQ + +#ifdef __x86_64__ +#define FLOAT128_MINOR_VERSION 3 +#else +#define FLOAT128_MINOR_VERSION 5 +#endif + #if __GNUC__ >= 7 #define HAS_FLOATN +#elif __GNUC_PREREQ(4, FLOAT128_MINOR_VERSION) +#define HAS_FLOAT128 #endif + #endif #ifndef HAS_FLOATN @@ -10,9 +21,12 @@ typedef float _Float32; typedef double _Float32x; typedef double _Float64; typedef long double _Float64x; -typedef long double _Float128; typedef long double _Float128x; #endif +#if !defined(HAS_FLOATN) && !defined(HAS_FLOAT128) +typedef long double _Float128; +#endif + int main(int argc, char** argv) { }