Merge pull request #8169 from tautschnig/bugfixes/float-extensions

tautschnig · web-flow · commit 689c552a095a · 2024-03-12T11:22:27.000+01:00
C/C++ front-end: accept all floating-point extensions that GCC and Clang support
diff --git a/.gitignore b/.gitignore
@@ -52,7 +52,6 @@ src/ansi-c/compiler_headers/gcc_builtin_headers_omp.inc
 src/ansi-c/compiler_headers/gcc_builtin_headers_power.inc
 src/ansi-c/compiler_headers/gcc_builtin_headers_tm.inc
 src/ansi-c/compiler_headers/gcc_builtin_headers_types.inc
-src/ansi-c/compiler_headers/gcc_builtin_headers_types_gcc7plus.inc
 src/ansi-c/compiler_headers/gcc_builtin_headers_ubsan.inc
 src/ansi-c/compiler_headers/windows_builtin_headers.inc
 src/cpp/cprover_library.inc
diff --git a/regression/ansi-c/float_constant1/main.c b/regression/ansi-c/float_constant1/main.c
@@ -21,9 +21,21 @@ STATIC_ASSERT(__builtin_types_compatible_p(_Float64, __typeof(1.0f64)));
 STATIC_ASSERT(__builtin_types_compatible_p(_Float128, __typeof(1.0f128)));
 STATIC_ASSERT(__builtin_types_compatible_p(_Float32x, __typeof(1.0f32x)));
 STATIC_ASSERT(__builtin_types_compatible_p(_Float64x, __typeof(1.0f64x)));
+// f128x should be supported by GCC >= 7 (and for C++ in GCC >=13), but there
+// are no current GCC target architectures that actually support such types
 STATIC_ASSERT(__builtin_types_compatible_p(_Float128x, __typeof(1.0f128x)));
 #endif
 
+#if defined(__GNUC__) && !defined(__clang__) && __GNUC__ >= 13
+STATIC_ASSERT(__builtin_types_compatible_p(_Float16, __typeof(1.0f16)));
+STATIC_ASSERT(__builtin_types_compatible_p(__bf16, __typeof(1.0bf16)));
+STATIC_ASSERT(__builtin_types_compatible_p(__bf16, __typeof(1.BF16)));
+#endif
+
+#if defined(__clang__) && __clang_major__ >= 15
+STATIC_ASSERT(__builtin_types_compatible_p(_Float16, __typeof(1.0f16)));
+#endif
+
 #ifdef __GNUC__
 _Complex c;
 #endif
diff --git a/src/ansi-c/CMakeLists.txt b/src/ansi-c/CMakeLists.txt
@@ -79,7 +79,6 @@ make_inc(compiler_headers/gcc_builtin_headers_omp)
 make_inc(compiler_headers/gcc_builtin_headers_power)
 make_inc(compiler_headers/gcc_builtin_headers_tm)
 make_inc(compiler_headers/gcc_builtin_headers_types)
-make_inc(compiler_headers/gcc_builtin_headers_types_gcc7plus)
 make_inc(compiler_headers/gcc_builtin_headers_ubsan)
 make_inc(compiler_headers/windows_builtin_headers)
 make_inc(cprover_builtin_headers)
@@ -104,7 +103,6 @@ set(extra_dependencies
     ${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_power.inc
     ${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_tm.inc
     ${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_types.inc
-    ${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_types_gcc7plus.inc
     ${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/gcc_builtin_headers_ubsan.inc
     ${CMAKE_CURRENT_BINARY_DIR}/compiler_headers/windows_builtin_headers.inc
     ${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc
diff --git a/src/ansi-c/Makefile b/src/ansi-c/Makefile
@@ -70,7 +70,6 @@ BUILTIN_FILES = \
   compiler_headers/gcc_builtin_headers_power.inc \
   compiler_headers/gcc_builtin_headers_tm.inc \
   compiler_headers/gcc_builtin_headers_types.inc \
-  compiler_headers/gcc_builtin_headers_types_gcc7plus.inc \
   compiler_headers/gcc_builtin_headers_ubsan.inc \
   compiler_headers/windows_builtin_headers.inc
 
diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp
@@ -22,12 +22,6 @@ const char gcc_builtin_headers_types[] =
 #include "compiler_headers/gcc_builtin_headers_types.inc" // IWYU pragma: keep
   ; // NOLINT(whitespace/semicolon)
 
-const char gcc_builtin_headers_types_gcc7plus[] =
-  "#line 1 \"gcc_builtin_headers_types_gcc7plus.h\"\n"
-// NOLINTNEXTLINE(whitespace/line_length)
-#include "compiler_headers/gcc_builtin_headers_types_gcc7plus.inc" // IWYU pragma: keep
-  ; // NOLINT(whitespace/semicolon)
-
 const char gcc_builtin_headers_generic[] =
   "#line 1 \"gcc_builtin_headers_generic.h\"\n"
 #include "compiler_headers/gcc_builtin_headers_generic.inc" // IWYU pragma: keep
@@ -158,9 +152,7 @@ max_malloc_size(std::size_t pointer_width, std::size_t object_bits)
   return ((mp_integer)1) << (mp_integer)bits_for_positive_offset;
 }
 
-void ansi_c_internal_additions(
-  std::string &code,
-  bool support_ts_18661_3_Floatn_types)
+void ansi_c_internal_additions(std::string &code, bool support_float16_type)
 {
   // clang-format off
   // do the built-in types and variables
@@ -249,8 +241,15 @@ void ansi_c_internal_additions(
     config.ansi_c.mode == configt::ansi_ct::flavourt::ARM)
   {
     code+=gcc_builtin_headers_types;
-    if(support_ts_18661_3_Floatn_types)
-      code += gcc_builtin_headers_types_gcc7plus;
+    if(support_float16_type)
+    {
+      code +=
+        "typedef _Float16 __gcc_v8hf __attribute__((__vector_size__(16)));\n";
+      code +=
+        "typedef _Float16 __gcc_v16hf __attribute__((__vector_size__(32)));\n";
+      code +=
+        "typedef _Float16 __gcc_v32hf __attribute__((__vector_size__(64)));\n";
+    }
 
     // there are many more, e.g., look at
     // https://developer.apple.com/library/mac/#documentation/developertools/gcc-4.0.1/gcc/Target-Builtins.html
diff --git a/src/ansi-c/ansi_c_internal_additions.h b/src/ansi-c/ansi_c_internal_additions.h
@@ -12,15 +12,12 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <string>
 
-void ansi_c_internal_additions(
-  std::string &code,
-  bool support_ts_18661_3_Floatn_types);
+void ansi_c_internal_additions(std::string &code, bool support_float16_type);
 void ansi_c_architecture_strings(std::string &code);
 
 extern const char clang_builtin_headers[];
 extern const char cprover_builtin_headers[];
 extern const char gcc_builtin_headers_types[];
-extern const char gcc_builtin_headers_types_gcc7plus[];
 extern const char gcc_builtin_headers_generic[];
 extern const char gcc_builtin_headers_math[];
 extern const char gcc_builtin_headers_mem_string[];
diff --git a/src/ansi-c/ansi_c_language.cpp b/src/ansi-c/ansi_c_language.cpp
@@ -68,7 +68,7 @@ bool ansi_c_languaget::parse(
   // parsing
 
   std::string code;
-  ansi_c_internal_additions(code, config.ansi_c.ts_18661_3_Floatn_types);
+  ansi_c_internal_additions(code, config.ansi_c.float16_type);
   std::istringstream codestr(code);
 
   ansi_c_parser.clear();
@@ -77,6 +77,8 @@ bool ansi_c_languaget::parse(
   ansi_c_parser.log.set_message_handler(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.float16_type = config.ansi_c.float16_type;
+  ansi_c_parser.bf16_type = config.ansi_c.bf16_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;
@@ -203,6 +205,8 @@ bool ansi_c_languaget::to_expr(
   ansi_c_parser.log.set_message_handler(message_handler);
   ansi_c_parser.mode=config.ansi_c.mode;
   ansi_c_parser.ts_18661_3_Floatn_types=config.ansi_c.ts_18661_3_Floatn_types;
+  ansi_c_parser.float16_type = config.ansi_c.float16_type;
+  ansi_c_parser.bf16_type = config.ansi_c.bf16_type;
   ansi_c_scanner_init();
 
   bool result=ansi_c_parser.parse();
diff --git a/src/ansi-c/ansi_c_parser.h b/src/ansi-c/ansi_c_parser.h
@@ -33,7 +33,9 @@ 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),
+      float16_type(false),
+      bf16_type(false)
   {
   }
 
@@ -78,6 +80,8 @@ class ansi_c_parsert:public parsert
 
   // ISO/IEC TS 18661-3:2015
   bool ts_18661_3_Floatn_types;
+  bool float16_type;
+  bool bf16_type;
 
   typedef ansi_c_identifiert identifiert;
   typedef ansi_c_scopet scopet;
diff --git a/src/ansi-c/builtin_factory.cpp b/src/ansi-c/builtin_factory.cpp
@@ -97,7 +97,7 @@ static bool convert(
 //! \return 'true' on error
 bool builtin_factory(
   const irep_idt &identifier,
-  bool support_ts_18661_3_Floatn_types,
+  bool support_float16_type,
   symbol_table_baset &symbol_table,
   message_handlert &mh)
 {
@@ -107,7 +107,7 @@ bool builtin_factory(
   std::ostringstream s;
 
   std::string code;
-  ansi_c_internal_additions(code, support_ts_18661_3_Floatn_types);
+  ansi_c_internal_additions(code, support_float16_type);
   s << code;
 
   // our own extensions
diff --git a/src/ansi-c/builtin_factory.h b/src/ansi-c/builtin_factory.h
@@ -17,7 +17,7 @@ class symbol_table_baset;
 //! \return 'true' in case of error
 bool builtin_factory(
   const irep_idt &identifier,
-  bool support_ts_18661_3_Floatn_types,
+  bool support_float16_type,
   symbol_table_baset &,
   message_handlert &);
 
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
@@ -2077,7 +2077,7 @@ bool c_typecheck_baset::builtin_factory(const irep_idt &identifier)
 {
   return ::builtin_factory(
     identifier,
-    config.ansi_c.ts_18661_3_Floatn_types,
+    config.ansi_c.float16_type,
     symbol_table,
     get_message_handler());
 }
diff --git a/src/ansi-c/compiler_headers/gcc_builtin_headers_types_gcc7plus.h b/src/ansi-c/compiler_headers/gcc_builtin_headers_types_gcc7plus.h
diff --git a/src/ansi-c/gcc_version.cpp b/src/ansi-c/gcc_version.cpp
@@ -162,4 +162,16 @@ void configure_gcc(const gcc_versiont &gcc_version)
   config.ansi_c.gcc__float128_type =
     gcc_version.flavor == gcc_versiont::flavort::GCC &&
     gcc_version.is_at_least(4u, gcc_float128_minor_version);
+
+  config.ansi_c.float16_type =
+    (gcc_version.flavor == gcc_versiont::flavort::GCC &&
+     gcc_version.is_at_least(12u)) ||
+    (gcc_version.flavor == gcc_versiont::flavort::CLANG &&
+     gcc_version.is_at_least(15u));
+
+  config.ansi_c.bf16_type =
+    (gcc_version.flavor == gcc_versiont::flavort::GCC &&
+     gcc_version.is_at_least(13u)) ||
+    (gcc_version.flavor == gcc_versiont::flavort::CLANG &&
+     gcc_version.is_at_least(15u));
 }
diff --git a/src/ansi-c/literals/parse_float.cpp b/src/ansi-c/literals/parse_float.cpp
@@ -77,8 +77,8 @@ parse_floatt::parse_floatt(const std::string &src)
       p++;
 
     // get exponent
-    while(*p!=0 && *p!='f' && *p!='l' &&
-          *p!='w' && *p!='q' && *p!='d')
+    while(*p != 0 && *p != 'f' && *p != 'l' && *p != 'w' && *p != 'q' &&
+          *p != 'd' && *p != 'b')
     {
       str_exponent+=*p;
       p++;
@@ -121,10 +121,8 @@ parse_floatt::parse_floatt(const std::string &src)
       p++;
 
     // get fraction part
-    while(*p!=0 && *p!='e' &&
-          *p!='f' && *p!='l' &&
-          *p!='w' && *p!='q' && *p!='d' &&
-          *p!='i' && *p!='j')
+    while(*p != 0 && *p != 'e' && *p != 'f' && *p != 'l' && *p != 'w' &&
+          *p != 'q' && *p != 'd' && *p != 'i' && *p != 'j' && *p != 'b')
     {
       str_fraction_part+=*p;
       p++;
@@ -139,9 +137,8 @@ parse_floatt::parse_floatt(const std::string &src)
       p++;
 
     // get exponent
-    while(*p!=0 && *p!='f' && *p!='l' &&
-          *p!='w' && *p!='q' && *p!='d' &&
-          *p!='i' && *p!='j')
+    while(*p != 0 && *p != 'f' && *p != 'l' && *p != 'w' && *p != 'q' &&
+          *p != 'd' && *p != 'i' && *p != 'j' && *p != 'b')
     {
       str_exponent+=*p;
       p++;
@@ -173,7 +170,7 @@ parse_floatt::parse_floatt(const std::string &src)
   is_float80=false;
   is_float128=is_float128x=false;
 
-  if(strcmp(p, "f16")==0)
+  if(strcmp(p, "f16") == 0 || strcmp(p, "bf16") == 0)
     is_float16=true;
   else if(strcmp(p, "f32")==0)
     is_float32=true;
diff --git a/src/ansi-c/scanner.l b/src/ansi-c/scanner.l
@@ -217,10 +217,13 @@ hexfloat1       "0"[xX]{hexdigit}*"."{hexdigit}+[pP][+-]?{integer}
 hexfloat2       "0"[xX]{hexdigit}*"."[pP][+-]?{integer}
 hexfloat3       "0"[xX]{hexdigit}*[pP][+-]?{integer}
 float_suffix    [fFlLiIjJ]*
-gcc_ext_float_suffix    [wWqQ]|[dD][fFdDlL]?|"f16"|"f32"|"f64"|"f128"|"f32x"|"f64x"|"f128x"
+clang_ext_float_suffix [qQ]|"f16"|"F16"
+gcc_ext_float_width (("bf"|"BF")"16")|([fF]("32"|"64"|"128"|"32x"|"64x"|"128x"))
+gcc_ext_float_suffix {clang_ext_float_suffix}|[wW]|[dD][fFdDlL]?|{gcc_ext_float_width}
 float           {float1}|{float2}|{float3}|{hexfloat1}|{hexfloat2}|{hexfloat3}
 float_s         {float}{float_suffix}|{integer}[fF]
 gcc_ext_float_s {float}{gcc_ext_float_suffix}
+clang_ext_float_s {float}{clang_ext_float_suffix}
 cppstart        {ws}"#"{ws}
 cpplineno       {cppstart}"line"*{ws}{integer}{ws}.*{newline}
 cppdirective    {cppstart}({newline}|[^p].*|"p"[^r].*|"pr"[^a].*|"pra"[^g].*|"prag"[^m].*|"pragm"[^a].*)
@@ -524,13 +527,13 @@ void ansi_c_scanner_init()
                     return make_identifier();
                 }
 
-"_Float16"      { if(PARSER.ts_18661_3_Floatn_types)
+"_Float16"      { if(PARSER.float16_type)
                   { loc(); return TOK_GCC_FLOAT16; }
                   else
                     return make_identifier();
                 }
 
-"__bf16"        { if(PARSER.ts_18661_3_Floatn_types)
+"__bf16"        { if(PARSER.bf16_type)
                   { loc(); return TOK_GCC_FLOAT16; }
                   else
                     return make_identifier();
@@ -1561,9 +1564,21 @@ __decltype          { if(PARSER.cpp98 &&
                   return TOK_INTEGER;
                 }
 
+{clang_ext_float_s} { if(PARSER.mode!=configt::ansi_ct::flavourt::GCC &&
+                         PARSER.mode != configt::ansi_ct::flavourt::CLANG)
+                      {
+                        yyansi_cerror("Floating-point constant with unsupported extension");
+                        return TOK_SCANNER_ERROR;
+                      }
+                      newstack(yyansi_clval);
+                      parser_stack(yyansi_clval)=convert_float_literal(yytext);
+                      PARSER.set_source_location(parser_stack(yyansi_clval));
+                      return TOK_FLOATING;
+                    }
+
 {gcc_ext_float_s} { if(PARSER.mode!=configt::ansi_ct::flavourt::GCC)
                     {
-                      yyansi_cerror("Preprocessor directive found");
+                      yyansi_cerror("Floating-point constant with unsupported extension");
                       return TOK_SCANNER_ERROR;
                     }
                     newstack(yyansi_clval);
diff --git a/src/cpp/cpp_parser.cpp b/src/cpp/cpp_parser.cpp
@@ -13,19 +13,36 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 
 #include <util/config.h>
 
+#include <ansi-c/gcc_version.h>
+
 cpp_parsert cpp_parser;
 
 bool cpp_parse();
 
 bool cpp_parsert::parse()
 {
+  if(!support_float16.has_value())
+  {
+    if(config.ansi_c.preprocessor == configt::ansi_ct::preprocessort::GCC)
+    {
+      gcc_versiont gcc_version;
+      gcc_version.get("gcc");
+      support_float16 = gcc_version.flavor == gcc_versiont::flavort::GCC &&
+                        gcc_version.is_at_least(13u);
+    }
+    else
+      support_float16 = false;
+  }
+
   // We use the ANSI-C scanner
   ansi_c_parser.cpp98=true;
   ansi_c_parser.cpp11 =
     config.cpp.cpp_standard == configt::cppt::cpp_standardt::CPP11 ||
     config.cpp.cpp_standard == configt::cppt::cpp_standardt::CPP14 ||
     config.cpp.cpp_standard == configt::cppt::cpp_standardt::CPP17;
-  ansi_c_parser.ts_18661_3_Floatn_types=false;
+  ansi_c_parser.ts_18661_3_Floatn_types = false; // these are still typedefs
+  ansi_c_parser.float16_type = *support_float16;
+  ansi_c_parser.bf16_type = *support_float16;
   ansi_c_parser.in=in;
   ansi_c_parser.mode=mode;
   ansi_c_parser.set_file(get_file());
diff --git a/src/cpp/cpp_parser.h b/src/cpp/cpp_parser.h
@@ -19,6 +19,8 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #include "cpp_parse_tree.h"
 #include "cpp_token_buffer.h"
 
+#include <optional>
+
 class cpp_parsert:public parsert
 {
 public:
@@ -34,10 +36,11 @@ class cpp_parsert:public parsert
     asm_block_following=false;
   }
 
-  cpp_parsert():
-    mode(configt::ansi_ct::flavourt::ANSI),
-    recognize_wchar_t(true),
-    asm_block_following(false)
+  cpp_parsert()
+    : mode(configt::ansi_ct::flavourt::ANSI),
+      recognize_wchar_t(true),
+      asm_block_following(false),
+      support_float16(std::nullopt)
   {
   }
 
@@ -65,6 +68,9 @@ class cpp_parsert:public parsert
   // scanner
   unsigned parenthesis_counter;
   bool asm_block_following;
+
+protected:
+  std::optional<bool> support_float16;
 };
 
 extern cpp_parsert cpp_parser;
diff --git a/src/cpp/cpp_typecheck.cpp b/src/cpp/cpp_typecheck.cpp
diff --git a/src/cpp/cpp_typecheck.h b/src/cpp/cpp_typecheck.h
diff --git a/src/util/config.cpp b/src/util/config.cpp
diff --git a/src/util/config.h b/src/util/config.h
