From bf1159faf158e4a17c6b106c44577f667be9118a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 25 Jan 2024 11:15:53 +0000 Subject: [PATCH] C/C++ front-end: accept all floating-point extensions that GCC and Clang support Testing with Compiler Explorer showed that Clang supports a subset of GCC's extensions, and GCC also supports some more extensions than what we previously covered. --- .gitignore | 1 - regression/ansi-c/float_constant1/main.c | 12 +++++ src/ansi-c/CMakeLists.txt | 2 - src/ansi-c/Makefile | 1 - src/ansi-c/ansi_c_internal_additions.cpp | 21 ++++---- src/ansi-c/ansi_c_internal_additions.h | 5 +- src/ansi-c/ansi_c_language.cpp | 6 ++- src/ansi-c/ansi_c_parser.h | 6 ++- src/ansi-c/builtin_factory.cpp | 4 +- src/ansi-c/builtin_factory.h | 2 +- src/ansi-c/c_typecheck_expr.cpp | 2 +- .../gcc_builtin_headers_types_gcc7plus.h | 3 -- src/ansi-c/gcc_version.cpp | 12 +++++ src/ansi-c/literals/parse_float.cpp | 17 +++--- src/ansi-c/scanner.l | 23 ++++++-- src/cpp/cpp_parser.cpp | 19 ++++++- src/cpp/cpp_parser.h | 14 +++-- src/cpp/cpp_typecheck.cpp | 54 ++++++++++++++++++- src/cpp/cpp_typecheck.h | 23 ++------ src/util/config.cpp | 6 ++- src/util/config.h | 2 + 21 files changed, 165 insertions(+), 70 deletions(-) delete mode 100644 src/ansi-c/compiler_headers/gcc_builtin_headers_types_gcc7plus.h diff --git a/.gitignore b/.gitignore index cc8c048280b..95a297d6b30 100644 --- 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 index 93fc5e4b4c4..b7fe6ad4d55 100644 --- 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 index 79588b05139..61173ca5720 100644 --- 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 index 20ca043e900..64ffa497072 100644 --- 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 index e3eaa05834e..9273f40cfc3 100644 --- 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 index c2531b65337..c3d37e4b53e 100644 --- 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 -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 index c4eb9cadc14..0578dccc4d4 100644 --- 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 index 4dde7752afe..dbfcd98949e 100644 --- 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 index bfed926cb03..7440ab3938c 100644 --- 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 index e270d4917f1..6a74b3c6759 100644 --- 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 index 4c8cb1024df..c9c5319b5cb 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -2076,7 +2076,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 deleted file mode 100644 index dd327a67b8e..00000000000 --- a/src/ansi-c/compiler_headers/gcc_builtin_headers_types_gcc7plus.h +++ /dev/null @@ -1,3 +0,0 @@ -typedef _Float16 __gcc_v8hf __attribute__((__vector_size__(16))); -typedef _Float16 __gcc_v16hf __attribute__((__vector_size__(32))); -typedef _Float16 __gcc_v32hf __attribute__((__vector_size__(64))); diff --git a/src/ansi-c/gcc_version.cpp b/src/ansi-c/gcc_version.cpp index 57250dbc62e..f36318f16d9 100644 --- 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 index b56f9e44f93..bd0fc35d144 100644 --- 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 index a55fc3b1fc0..8b920807c37 100644 --- 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 index 0d72414eec9..4efa2b958a4 100644 --- a/src/cpp/cpp_parser.cpp +++ b/src/cpp/cpp_parser.cpp @@ -13,19 +13,36 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include +#include + 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 index 1813872bf76..af49083fc01 100644 --- 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 + 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 support_float16; }; extern cpp_parsert cpp_parser; diff --git a/src/cpp/cpp_typecheck.cpp b/src/cpp/cpp_typecheck.cpp index 6f888c1cb79..19fdd9dc52d 100644 --- a/src/cpp/cpp_typecheck.cpp +++ b/src/cpp/cpp_typecheck.cpp @@ -16,11 +16,63 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include +#include #include "cpp_declarator.h" #include "cpp_util.h" #include "expr2cpp.h" +cpp_typecheckt::cpp_typecheckt( + cpp_parse_treet &_cpp_parse_tree, + symbol_table_baset &_symbol_table, + const std::string &_module, + message_handlert &message_handler) + : c_typecheck_baset(_symbol_table, _module, message_handler), + cpp_parse_tree(_cpp_parse_tree), + template_counter(0), + anon_counter(0), + disable_access_control(false), + support_float16_type(false) +{ + if(config.ansi_c.preprocessor == configt::ansi_ct::preprocessort::GCC) + { + gcc_versiont gcc_version; + gcc_version.get("gcc"); + if( + gcc_version.flavor == gcc_versiont::flavort::GCC && + gcc_version.is_at_least(13u)) + { + support_float16_type = true; + } + } +} + +cpp_typecheckt::cpp_typecheckt( + cpp_parse_treet &_cpp_parse_tree, + symbol_table_baset &_symbol_table1, + const symbol_table_baset &_symbol_table2, + const std::string &_module, + message_handlert &message_handler) + : c_typecheck_baset(_symbol_table1, _symbol_table2, _module, message_handler), + cpp_parse_tree(_cpp_parse_tree), + template_counter(0), + anon_counter(0), + disable_access_control(false), + support_float16_type(false) +{ + if(config.ansi_c.preprocessor == configt::ansi_ct::preprocessort::GCC) + { + gcc_versiont gcc_version; + gcc_version.get("gcc"); + if( + gcc_version.flavor == gcc_versiont::flavort::GCC && + gcc_version.is_at_least(13u)) + { + support_float16_type = true; + } + } +} + void cpp_typecheckt::convert(cpp_itemt &item) { if(item.is_declaration()) @@ -326,7 +378,7 @@ void cpp_typecheckt::clean_up() bool cpp_typecheckt::builtin_factory(const irep_idt &identifier) { return ::builtin_factory( - identifier, false, symbol_table, get_message_handler()); + identifier, support_float16_type, symbol_table, get_message_handler()); } bool cpp_typecheckt::contains_cpp_name(const exprt &expr) diff --git a/src/cpp/cpp_typecheck.h b/src/cpp/cpp_typecheck.h index 0e64a2f38cb..3cec8ae874e 100644 --- a/src/cpp/cpp_typecheck.h +++ b/src/cpp/cpp_typecheck.h @@ -43,32 +43,14 @@ class cpp_typecheckt:public c_typecheck_baset cpp_parse_treet &_cpp_parse_tree, symbol_table_baset &_symbol_table, const std::string &_module, - message_handlert &message_handler) - : c_typecheck_baset(_symbol_table, _module, message_handler), - cpp_parse_tree(_cpp_parse_tree), - template_counter(0), - anon_counter(0), - disable_access_control(false) - { - } + message_handlert &message_handler); cpp_typecheckt( cpp_parse_treet &_cpp_parse_tree, symbol_table_baset &_symbol_table1, const symbol_table_baset &_symbol_table2, const std::string &_module, - message_handlert &message_handler) - : c_typecheck_baset( - _symbol_table1, - _symbol_table2, - _module, - message_handler), - cpp_parse_tree(_cpp_parse_tree), - template_counter(0), - anon_counter(0), - disable_access_control(false) - { - } + message_handlert &message_handler); ~cpp_typecheckt() override { @@ -591,6 +573,7 @@ class cpp_typecheckt:public c_typecheck_baset dynamic_initializationst dynamic_initializations; bool disable_access_control; // Disable protect and private std::unordered_set deferred_typechecking; + bool support_float16_type; }; #endif // CPROVER_CPP_CPP_TYPECHECK_H diff --git a/src/util/config.cpp b/src/util/config.cpp index 50ce2192004..63ac91d8943 100644 --- a/src/util/config.cpp +++ b/src/util/config.cpp @@ -804,6 +804,8 @@ 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.float16_type = false; + ansi_c.bf16_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; @@ -1295,8 +1297,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 are not architectural features, - // and thus not stored in namespace + // ts_18661_3_Floatn_types, float16_type, bf16_type are not architectural + // features, and thus not stored in namespace ansi_c.alignment=unsigned_from_ns(ns, "alignment"); diff --git a/src/util/config.h b/src/util/config.h index 5929c64f6a3..288b244621a 100644 --- a/src/util/config.h +++ b/src/util/config.h @@ -151,6 +151,8 @@ 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 float16_type; // _Float16 (Clang >= 15, GCC >= 12) + bool bf16_type; // __bf16 (Clang >= 15, GCC >= 13) bool single_precision_constant; enum class c_standardt {