Add support for __fp16 where appropriate

src/ansi-c/ansi_c_language.cpp

@@ -78,6 +78,7 @@ bool ansi_c_languaget::parse(
   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.fp16_type = config.ansi_c.fp16_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;
@@ -202,6 +203,7 @@ bool ansi_c_languaget::to_expr(
   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.fp16_type = config.ansi_c.fp16_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

@@ -37,7 +37,8 @@ class ansi_c_parsert:public parsert
       for_has_scope(false),
       ts_18661_3_Floatn_types(false),
       float16_type(false),
-      bf16_type(false)
+      bf16_type(false),
+      fp16_type(false)
   {
     // set up global scope
     scopes.clear();
@@ -69,6 +70,7 @@ class ansi_c_parsert:public parsert
   bool ts_18661_3_Floatn_types;
   bool float16_type;
   bool bf16_type;
+  bool fp16_type;
 
   typedef ansi_c_identifiert identifiert;
   typedef ansi_c_scopet scopet;

src/ansi-c/builtin_factory.cpp

@@ -54,6 +54,7 @@ static bool convert(
   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.fp16_type = config.ansi_c.fp16_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/gcc_version.cpp

@@ -174,4 +174,11 @@ void configure_gcc(const gcc_versiont &gcc_version)
      gcc_version.is_at_least(13u)) ||
     (gcc_version.flavor == gcc_versiont::flavort::CLANG &&
      gcc_version.is_at_least(15u));
+
+  config.ansi_c.fp16_type =
+    (gcc_version.flavor == gcc_versiont::flavort::GCC &&
+     gcc_version.is_at_least(4u, 5u) &&
+     (config.ansi_c.arch == "arm" || config.ansi_c.arch == "arm64")) ||
+    (gcc_version.flavor == gcc_versiont::flavort::CLANG &&
+     gcc_version.is_at_least(6u));
 }

src/ansi-c/scanner.l

@@ -546,6 +546,12 @@ enable_or_disable ("enable"|"disable")
                     return make_identifier();
                 }
 
+"__fp16"        { if(PARSER.fp16_type)
+                  { loc(); return TOK_GCC_FLOAT16; }
+                  else
+                    return make_identifier();
+                }
+
 "_Float32"      { if(PARSER.ts_18661_3_Floatn_types)
                   { loc(); return TOK_GCC_FLOAT32; }
                   else

src/cpp/cpp_parser.cpp

@@ -42,6 +42,7 @@ bool cpp_parsert::parse()
     false; // these are still typedefs
   token_buffer.ansi_c_parser.float16_type = *support_float16;
   token_buffer.ansi_c_parser.bf16_type = *support_float16;
+  token_buffer.ansi_c_parser.fp16_type = *support_float16;
   token_buffer.ansi_c_parser.in = in;
   token_buffer.ansi_c_parser.mode = mode;
   token_buffer.ansi_c_parser.set_file(get_file());

src/goto-instrument/contracts/contracts_wrangler.cpp

@@ -147,6 +147,7 @@ void contracts_wranglert::mangle(
   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.fp16_type = config.ansi_c.fp16_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/util/config.cpp

@@ -837,6 +837,7 @@ bool configt::set(const cmdlinet &cmdline)
   ansi_c.ts_18661_3_Floatn_types=false;
   ansi_c.float16_type = false;
   ansi_c.bf16_type = false;
+  ansi_c.fp16_type = false;
   ansi_c.c_standard=ansi_ct::default_c_standard();
   ansi_c.endianness=ansi_ct::endiannesst::NO_ENDIANNESS;
   ansi_c.os=ansi_ct::ost::NO_OS;
@@ -1328,8 +1329,8 @@ void configt::set_from_symbol_table(const symbol_table_baset &symbol_table)
   ansi_c.char_is_unsigned=unsigned_from_ns(ns, "char_is_unsigned")!=0;
   ansi_c.wchar_t_is_unsigned=unsigned_from_ns(ns, "wchar_t_is_unsigned")!=0;
   // for_has_scope, single_precision_constant, rounding_mode,
-  // ts_18661_3_Floatn_types, float16_type, bf16_type are not architectural
-  // features, and thus not stored in namespace
+  // ts_18661_3_Floatn_types, float16_type, bf16_type, fp16_type are not
+  // architectural features, and thus not stored in namespace
 
   ansi_c.alignment=unsigned_from_ns(ns, "alignment");
 

src/util/config.h

@@ -153,6 +153,7 @@ class configt
     bool gcc__float128_type;      // __float128, a gcc extension since 4.3/4.5
     bool float16_type;            // _Float16 (Clang >= 15, GCC >= 12)
     bool bf16_type;               // __bf16 (Clang >= 15, GCC >= 13)
+    bool fp16_type;               // __fp16 (GCC >= 4.5 on ARM, Clang >= 6)
     bool single_precision_constant;
     enum class c_standardt
     {

unit/cpp_scanner.cpp

@@ -43,6 +43,7 @@ int main(int argc, const char *argv[])
   ansi_c_parser.ts_18661_3_Floatn_types = false;
   ansi_c_parser.float16_type = false;
   ansi_c_parser.bf16_type = false;
+  ansi_c_parser.fp16_type = false;
   ansi_c_parser.in=∈
   cpp_parser.in=∈