Be precise as to whether __float128 is a keyword or a typedef

Add a new parser configuration setting to correctly configure the
scanner.

Author: tautschnig

src/ansi-c/ansi_c_internal_additions.cpp

@@ -268,18 +268,6 @@ void ansi_c_internal_additions(std::string &code, bool support_float16_type)
         code+="typedef long double __float128;\n";
       }
     }
-    else if(
-      config.ansi_c.arch == "arm64" &&
-      config.ansi_c.os == configt::ansi_ct::ost::OS_MACOS &&
-      config.ansi_c.mode != configt::ansi_ct::flavourt::CLANG &&
-      config.ansi_c.gcc__float128_type)
-    {
-      // https://gcc.gnu.org/onlinedocs/gcc/Floating-Types.html doesn't say so,
-      // but GCC on macOS supports __float128 also for Apple Silicon. It really
-      // appears to be a keyword, but we don't handle GCC version+platform
-      // specifics in the scanner.
-      code += "typedef " CPROVER_PREFIX "Float128 __float128;\n";
-    }
 
     if(
       config.ansi_c.arch == "i386" || config.ansi_c.arch == "x86_64" ||

src/ansi-c/ansi_c_language.cpp

@@ -76,6 +76,7 @@ bool ansi_c_languaget::parse(
   ansi_c_parser.in=&codestr;
   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_is_keyword = config.ansi_c.__float128_is_keyword;
   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;
@@ -201,6 +202,7 @@ bool ansi_c_languaget::to_expr(
   ansi_c_parser.in=&i_preprocessed;
   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_is_keyword = config.ansi_c.__float128_is_keyword;
   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;

src/ansi-c/ansi_c_parser.h

@@ -36,6 +36,7 @@ class ansi_c_parsert:public parsert
       cpp11(false),
       for_has_scope(false),
       ts_18661_3_Floatn_types(false),
+      __float128_is_keyword(false),
       float16_type(false),
       bf16_type(false),
       fp16_type(false)
@@ -68,6 +69,7 @@ class ansi_c_parsert:public parsert
 
   // ISO/IEC TS 18661-3:2015
   bool ts_18661_3_Floatn_types;
+  bool __float128_is_keyword;
   bool float16_type;
   bool bf16_type;
   bool fp16_type;

src/ansi-c/builtin_factory.cpp

@@ -52,6 +52,7 @@ static bool convert(
   ansi_c_parser.in=∈
   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_is_keyword = config.ansi_c.__float128_is_keyword;
   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;

src/ansi-c/gcc_version.cpp

@@ -162,6 +162,12 @@ 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.__float128_is_keyword =
+    gcc_version.flavor == gcc_versiont::flavort::CLANG ||
+    (gcc_version.flavor == gcc_versiont::flavort::GCC &&
+     config.ansi_c.arch == "arm64" &&
+     config.ansi_c.os == configt::ansi_ct::ost::OS_MACOS &&
+     config.ansi_c.gcc__float128_type);
 
   config.ansi_c.float16_type =
     (gcc_version.flavor == gcc_versiont::flavort::GCC &&

src/ansi-c/scanner.l

@@ -584,9 +584,7 @@ enable_or_disable ("enable"|"disable")
                   loc(); return TOK_GCC_FLOAT80;
                 }
 
-"__float128"    { // This is a keyword for CLANG,
-                  // but a typedef for GCC
-                  if(PARSER.mode==configt::ansi_ct::flavourt::CLANG)
+"__float128"    { if(PARSER.__float128_is_keyword)
                   { loc(); return TOK_GCC_FLOAT128; }
                   else
                     return make_identifier();

src/cbmc/cbmc_parse_options.cpp

@@ -548,6 +548,12 @@ int cbmc_parse_optionst::doit()
     gcc_version.get("gcc");
     configure_gcc(gcc_version);
   }
+  else if(config.ansi_c.preprocessor == configt::ansi_ct::preprocessort::CLANG)
+  {
+    gcc_versiont gcc_version;
+    gcc_version.get("clang");
+    configure_gcc(gcc_version);
+  }
 
   if(cmdline.isset("test-preprocessor"))
     return test_c_preprocessor(ui_message_handler)

src/cpp/cpp_parser.cpp

@@ -40,6 +40,7 @@ bool cpp_parsert::parse()
     config.cpp.cpp_standard == configt::cppt::cpp_standardt::CPP17;
   token_buffer.ansi_c_parser.ts_18661_3_Floatn_types =
     false; // these are still typedefs
+  token_buffer.ansi_c_parser.__float128_is_keyword = false;
   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;

src/cprover/cprover_parse_options.cpp

@@ -131,6 +131,13 @@ int cprover_parse_optionst::main()
       gcc_version.get("gcc");
       configure_gcc(gcc_version);
     }
+    else if(
+      config.ansi_c.preprocessor == configt::ansi_ct::preprocessort::CLANG)
+    {
+      gcc_versiont gcc_version;
+      gcc_version.get("clang");
+      configure_gcc(gcc_version);
+    }
 
     console_message_handlert message_handler;
     null_message_handlert null_message_handler;

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -421,6 +421,12 @@ int goto_analyzer_parse_optionst::doit()
     gcc_version.get("gcc");
     configure_gcc(gcc_version);
   }
+  else if(config.ansi_c.preprocessor == configt::ansi_ct::preprocessort::CLANG)
+  {
+    gcc_versiont gcc_version;
+    gcc_version.get("clang");
+    configure_gcc(gcc_version);
+  }
 
   goto_model = initialize_goto_model(cmdline.args, ui_message_handler, options);
 

src/goto-diff/goto_diff_parse_options.cpp

@@ -107,6 +107,12 @@ int goto_diff_parse_optionst::doit()
     gcc_version.get("gcc");
     configure_gcc(gcc_version);
   }
+  else if(config.ansi_c.preprocessor == configt::ansi_ct::preprocessort::CLANG)
+  {
+    gcc_versiont gcc_version;
+    gcc_version.get("clang");
+    configure_gcc(gcc_version);
+  }
 
   if(process_goto_program(options, goto_model1))
     return CPROVER_EXIT_INTERNAL_ERROR;

src/goto-instrument/contracts/contracts_wrangler.cpp

@@ -145,6 +145,7 @@ void contracts_wranglert::mangle(
   ansi_c_parser.in = &is;
   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_is_keyword = config.ansi_c.__float128_is_keyword;
   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;

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -139,6 +139,13 @@ int goto_instrument_parse_optionst::doit()
       gcc_version.get("gcc");
       configure_gcc(gcc_version);
     }
+    else if(
+      config.ansi_c.preprocessor == configt::ansi_ct::preprocessort::CLANG)
+    {
+      gcc_versiont gcc_version;
+      gcc_version.get("clang");
+      configure_gcc(gcc_version);
+    }
 
     {
       const bool validate_only = cmdline.isset("validate-goto-binary");

src/goto-synthesizer/goto_synthesizer_parse_options.cpp

@@ -73,6 +73,12 @@ int goto_synthesizer_parse_optionst::doit()
     gcc_version.get("gcc");
     configure_gcc(gcc_version);
   }
+  else if(config.ansi_c.preprocessor == configt::ansi_ct::preprocessort::CLANG)
+  {
+    gcc_versiont gcc_version;
+    gcc_version.get("clang");
+    configure_gcc(gcc_version);
+  }
 
   update_max_malloc_size(goto_model, ui_message_handler);
 

src/libcprover-cpp/api.cpp

@@ -69,6 +69,12 @@ api_sessiont::api_sessiont(const api_optionst &options)
     gcc_version.get("gcc");
     configure_gcc(gcc_version);
   }
+  else if(config.ansi_c.preprocessor == configt::ansi_ct::preprocessort::CLANG)
+  {
+    gcc_versiont gcc_version;
+    gcc_version.get("clang");
+    configure_gcc(gcc_version);
+  }
 }
 
 api_sessiont::~api_sessiont() = default;

src/util/config.cpp

@@ -835,6 +835,7 @@ bool configt::set(const cmdlinet &cmdline)
   ansi_c.single_precision_constant=false;
   ansi_c.for_has_scope=true; // C99 or later
   ansi_c.ts_18661_3_Floatn_types=false;
+  ansi_c.__float128_is_keyword = false;
   ansi_c.float16_type = false;
   ansi_c.bf16_type = false;
   ansi_c.fp16_type = false;
@@ -1329,8 +1330,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, fp16_type are not
-  // architectural features, and thus not stored in namespace
+  // ts_18661_3_Floatn_types, __float128_is_keyword, 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

@@ -151,6 +151,7 @@ class configt
     bool for_has_scope;
     bool ts_18661_3_Floatn_types; // ISO/IEC TS 18661-3:2015
     bool gcc__float128_type;      // __float128, a gcc extension since 4.3/4.5
+    bool __float128_is_keyword;   // __float128 as a keyword (and not typedef)
     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)

unit/cpp_scanner.cpp

@@ -41,6 +41,7 @@ int main(int argc, const char *argv[])
   ansi_c_parser.cpp98=true;
   ansi_c_parser.cpp11=false;
   ansi_c_parser.ts_18661_3_Floatn_types = false;
+  ansi_c_parser.__float128_is_keyword = false;
   ansi_c_parser.float16_type = false;
   ansi_c_parser.bf16_type = false;
   ansi_c_parser.fp16_type = false;