Merge pull request #4629 from diffblue/__float128

fix up __float128 and _Float128 support

Author: tautschnig

regression/ansi-c/gcc_version1/gcc-5.c

@@ -3,7 +3,8 @@ typedef float _Float32;
 typedef double _Float32x;
 typedef double _Float64;
 typedef long double _Float64x;
+typedef long double _Float128;
 typedef long double _Float128x;
 
 // But this type should:
-_Float128 f128;
+__float128 f128;

regression/ansi-c/gcc_version1/gcc-7.c

@@ -5,3 +5,5 @@ _Float64 f64;
 _Float64x f64x;
 _Float128 f128;
 _Float128x f128x;
+
+__float128 gcc_f128;

regression/cbmc/ts18661_typedefs/main.c

@@ -1,31 +1,51 @@
-#if defined(__GNUC__) && !defined(__clang__)
+#if defined(__GNUC__)
 
-#include <features.h> // For __GNUC_PREREQ
+#  ifdef __clang__
 
-#ifdef __x86_64__
-#define FLOAT128_MINOR_VERSION 3
-#else
-#define FLOAT128_MINOR_VERSION 5
-#endif
+#    define HAS_FLOAT128
 
-#if __GNUC__ >= 7
-#define HAS_FLOATN
-#elif __GNUC_PREREQ(4, FLOAT128_MINOR_VERSION)
-#define HAS_FLOAT128
-#endif
+#  else
+
+#    include <features.h> // For __GNUC_PREREQ
+
+#    ifdef __x86_64__
+#      define FLOAT128_MINOR_VERSION 3
+#    else
+#      define FLOAT128_MINOR_VERSION 5
+#    endif
+
+#    if __GNUC__ >= 7
+#      define HAS_FLOATN
+#    endif
+
+#    if __GNUC_PREREQ(4, FLOAT128_MINOR_VERSION)
+#      define HAS_FLOAT128
+#    endif
+
+#  endif
 
 #endif
 
-#ifndef HAS_FLOATN
+#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,8 +208,12 @@ 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,8 +226,12 @@ 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";
+      }
     }
 
     if(

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

@@ -28,16 +28,15 @@ class ansi_c_parsert:public parsert
 public:
   ansi_c_parse_treet parse_tree;
 
-  ansi_c_parsert():
-    tag_following(false),
-    asm_block_following(false),
-    parenthesis_counter(0),
-    mode(modet::NONE),
-    cpp98(false),
-    cpp11(false),
-    for_has_scope(false),
-    ts_18661_3_Floatn_types(false),
-    Float128_type(false)
+  ansi_c_parsert()
+    : tag_following(false),
+      asm_block_following(false),
+      parenthesis_counter(0),
+      mode(modet::NONE),
+      cpp98(false),
+      cpp11(false),
+      for_has_scope(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/gcc_version.cpp

@@ -142,3 +142,23 @@ std::ostream &operator<<(std::ostream &out, const gcc_versiont &v)
 {
   return out << v.v_major << '.' << v.v_minor << '.' << v.v_patchlevel;
 }
+
+void configure_gcc(const gcc_versiont &gcc_version)
+{
+  // ISO/IEC TS 18661-3:2015 support was introduced with gcc 7.0
+  if(
+    gcc_version.flavor == gcc_versiont::flavort::GCC &&
+    gcc_version.is_at_least(7u))
+  {
+    config.ansi_c.ts_18661_3_Floatn_types = true;
+  }
+
+  const auto gcc_float128_minor_version =
+    config.ansi_c.arch == "x86_64" ? 3u : 5u;
+
+  // __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/ansi-c/gcc_version.h

@@ -50,6 +50,8 @@ class gcc_versiont
   }
 };
 
+void configure_gcc(const gcc_versiont &);
+
 std::ostream &operator<<(std::ostream &, const gcc_versiont &);
 
 #endif

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/cbmc/cbmc_parse_options.cpp

@@ -28,6 +28,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <ansi-c/c_preprocess.h>
 #include <ansi-c/cprover_library.h>
+#include <ansi-c/gcc_version.h>
 
 #include <assembler/remove_asm.h>
 
@@ -490,6 +491,14 @@ int cbmc_parse_optionst::doit()
 
   register_languages();
 
+  // configure gcc, if required
+  if(config.ansi_c.preprocessor == configt::ansi_ct::preprocessort::GCC)
+  {
+    gcc_versiont gcc_version;
+    gcc_version.get("gcc");
+    configure_gcc(gcc_version);
+  }
+
   if(cmdline.isset("test-preprocessor"))
     return test_c_preprocessor(ui_message_handler)
              ? CPROVER_EXIT_PREPROCESSOR_TEST_FAILED

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

@@ -531,22 +531,13 @@ int gcc_modet::doit()
   if(cmdline.isset("-fsingle-precision-constant"))
     config.ansi_c.single_precision_constant=true;
 
-  // ISO/IEC TS 18661-3:2015 support was introduced with gcc 7.0
-  if(gcc_version.flavor==gcc_versiont::flavort::GCC &&
-     gcc_version.is_at_least(7))
-    config.ansi_c.ts_18661_3_Floatn_types=true;
-
-  const auto gcc_float128_minor_version =
-    config.ansi_c.arch == "x86_64" ? 3u : 5u;
-
-  config.ansi_c.Float128_type =
-    gcc_version.flavor == gcc_versiont::flavort::GCC &&
-    gcc_version.is_at_least(4u, 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;
 
+  // configure version-specific gcc settings
+  configure_gcc(gcc_version);
+
   switch(compiler.mode)
   {
   case compilet::LINK_LIBRARY:

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();