fix up __float128 and _Float128 support

_Float128 is a keyword, defined in ISO/IEC TS 18661-3:2015, and exists since
gcc 7.0. clang does not offer it.

__float128 is a typedef in gcc since 4.3/4.5, depending on architecture.

__float128 is a keyword in clang.

This PR attempts to clean this up.

Author: Daniel Kroening

regression/cbmc/ts18661_typedefs/main.c

@@ -1,4 +1,10 @@
-#if defined(__GNUC__) && !defined(__clang__)
+#if defined(__GNUC__)
+
+#ifdef __clang__
+
+#define HAS_FLOAT128
+
+#else
 
 #include <features.h> // For __GNUC_PREREQ
 
@@ -10,22 +16,36 @@
 
 #if __GNUC__ >= 7
 #define HAS_FLOATN
-#elif __GNUC_PREREQ(4, FLOAT128_MINOR_VERSION)
+#endif
+
+#if __GNUC_PREREQ(4, FLOAT128_MINOR_VERSION)
 #define HAS_FLOAT128
 #endif
 
 #endif
 
-#ifndef HAS_FLOATN
+#endif
+
+#ifdef HAS_FLOATN
+typedef _Float32 f1;
+typedef _Float32x f2;
+typedef _Float64 f3;
+typedef _Float64x f4;
+typedef _Float128 f5;
+typedef _Float128x f6;
+#else
 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;
+#if defined(HAS_FLOAT128)
+typedef __float128 f7;
+#else
+typedef long double __float128;
 #endif
 
 int main(int argc, char** argv) {

src/ansi-c/ansi_c_internal_additions.cpp

@@ -208,7 +208,8 @@ void ansi_c_internal_additions(std::string &code)
       // https://gcc.gnu.org/onlinedocs/gcc/Floating-Types.html
       // For clang, __float128 is a keyword.
       // For gcc, this is a typedef and not a keyword.
-      if(config.ansi_c.mode != configt::ansi_ct::flavourt::CLANG)
+      if(config.ansi_c.mode != configt::ansi_ct::flavourt::CLANG &&
+         config.ansi_c.gcc__float128_type)
         code += "typedef " CPROVER_PREFIX "Float128 __float128;\n";
     }
     else if(config.ansi_c.arch == "ppc64le")
@@ -222,7 +223,8 @@ void ansi_c_internal_additions(std::string &code)
       // https://gcc.gnu.org/onlinedocs/gcc/Floating-Types.html
       // For clang, __float128 is a keyword.
       // For gcc, this is a typedef and not a keyword.
-      if(config.ansi_c.mode != configt::ansi_ct::flavourt::CLANG)
+      if(config.ansi_c.mode != configt::ansi_ct::flavourt::CLANG &&
+         config.ansi_c.gcc__float128_type)
         code+="typedef long double __float128;\n";
     }
 

src/ansi-c/ansi_c_language.cpp

@@ -76,7 +76,6 @@ 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;

src/ansi-c/ansi_c_parser.h

@@ -36,8 +36,7 @@ class ansi_c_parsert:public parsert
     cpp98(false),
     cpp11(false),
     for_has_scope(false),
-    ts_18661_3_Floatn_types(false),
-    Float128_type(false)
+    ts_18661_3_Floatn_types(false)
   {
   }
 
@@ -84,9 +83,6 @@ 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;
 

src/ansi-c/scanner.l

@@ -565,7 +565,7 @@ void ansi_c_scanner_init()
                     return make_identifier();
                 }
 
-"_Float128"     { if(PARSER.Float128_type)
+"_Float128"     { if(PARSER.ts_18661_3_Floatn_types)
                   { loc(); return TOK_GCC_FLOAT128; }
                   else
                     return make_identifier();

src/cpp/cpp_parser.cpp

@@ -25,7 +25,6 @@ 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());

src/goto-cc/gcc_mode.cpp

@@ -539,7 +539,9 @@ int gcc_modet::doit()
   const auto gcc_float128_minor_version =
     config.ansi_c.arch == "x86_64" ? 3u : 5u;
 
-  config.ansi_c.Float128_type =
+  // __float128 exists (as a typedef) since gcc 4.5 everywhere,
+  // and since 4.3 on x86_64
+  config.ansi_c.gcc__float128_type =
     gcc_version.flavor == gcc_versiont::flavort::GCC &&
     gcc_version.is_at_least(4u, gcc_float128_minor_version);
 

src/util/config.cpp

@@ -948,7 +948,7 @@ bool configt::set(const cmdlinet &cmdline)
   }
 
   if(ansi_c.preprocessor == ansi_ct::preprocessort::GCC)
-    ansi_c.Float128_type = true;
+    ansi_c.gcc__float128_type = true;
 
   set_arch(arch);
 

src/util/config.h

@@ -44,7 +44,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 gcc__float128_type; // __float128, a gcc extension since 4.3/4.5
     bool single_precision_constant;
     enum class c_standardt { C89, C99, C11 } c_standard;
     static c_standardt default_c_standard();