From 09a4e6c8210423040f6c48f89fba3158b2c981f1 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 26 May 2018 10:03:48 +0100 Subject: [PATCH 1/5] run() can now redirect stderr --- src/goto-cc/as_mode.cpp | 8 ++-- src/goto-cc/gcc_mode.cpp | 2 +- src/util/run.cpp | 88 +++++++++++++++++++++++++++------------- src/util/run.h | 5 ++- 4 files changed, 67 insertions(+), 36 deletions(-) diff --git a/src/goto-cc/as_mode.cpp b/src/goto-cc/as_mode.cpp index 2ad810a4c0f..d130e63cb94 100644 --- a/src/goto-cc/as_mode.cpp +++ b/src/goto-cc/as_mode.cpp @@ -267,7 +267,7 @@ int as_modet::run_as() std::cout << '\n'; #endif - return run(new_argv[0], new_argv, cmdline.stdin_file, ""); + return run(new_argv[0], new_argv, cmdline.stdin_file); } int as_modet::as_hybrid_binary() @@ -314,7 +314,7 @@ int as_modet::as_hybrid_binary() objcopy_argv.push_back("--remove-section=goto-cc"); objcopy_argv.push_back(output_file); - result=run(objcopy_argv[0], objcopy_argv, "", ""); + result = run(objcopy_argv[0], objcopy_argv); } if(result==0) @@ -327,7 +327,7 @@ int as_modet::as_hybrid_binary() objcopy_argv.push_back("goto-cc="+saved); objcopy_argv.push_back(output_file); - result=run(objcopy_argv[0], objcopy_argv, "", ""); + result = run(objcopy_argv[0], objcopy_argv); } int remove_result=remove(saved.c_str()); @@ -354,7 +354,7 @@ int as_modet::as_hybrid_binary() lipo_argv.push_back("-output"); lipo_argv.push_back(output_file); - result=run(lipo_argv[0], lipo_argv, "", ""); + result = run(lipo_argv[0], lipo_argv); } int remove_result=remove(saved.c_str()); diff --git a/src/goto-cc/gcc_mode.cpp b/src/goto-cc/gcc_mode.cpp index 3fa138a05ca..fb58565c6f1 100644 --- a/src/goto-cc/gcc_mode.cpp +++ b/src/goto-cc/gcc_mode.cpp @@ -831,7 +831,7 @@ int gcc_modet::run_gcc(const compilet &compiler) debug() << " " << new_argv[i]; debug() << eom; - return run(new_argv[0], new_argv, cmdline.stdin_file, ""); + return run(new_argv[0], new_argv, cmdline.stdin_file); } int gcc_modet::gcc_hybrid_binary(compilet &compiler) diff --git a/src/util/run.cpp b/src/util/run.cpp index d0fddab27fd..14e1a798f3a 100644 --- a/src/util/run.cpp +++ b/src/util/run.cpp @@ -10,8 +10,6 @@ Date: August 2012 #include "run.h" -#include - #ifdef _WIN32 #include #else @@ -30,6 +28,7 @@ Date: August 2012 #endif +#include #include #include @@ -39,19 +38,59 @@ int run_shell(const std::string &command) std::vector argv; argv.push_back(shell); argv.push_back(command); - return run(shell, argv, "", ""); + return run(shell, argv, "", "", ""); +} + +#ifndef _WIN32 +/// open given file to replace either stdin, stderr, stdout +static int stdio_redirection(int fd, const std::string &file) +{ + int result_fd = fd; + + if(file.empty()) + return result_fd; + + int flags = 0, mode = 0; + std::string name; + + switch(fd) + { + case STDIN_FILENO: + flags = O_RDONLY; + name = "stdin"; + break; + + case STDOUT_FILENO: + case STDERR_FILENO: + flags = O_CREAT | O_WRONLY; + mode = S_IRUSR | S_IWUSR; + name = fd == STDOUT_FILENO ? "stdout" : "stderr"; + break; + + default: + UNREACHABLE; + } + + result_fd = open(file.c_str(), flags, mode); + if(result_fd == -1) + perror(("Failed to open " + name + " file " + file).c_str()); + + return result_fd; } +#endif int run( const std::string &what, const std::vector &argv, const std::string &std_input, - const std::string &std_output) + const std::string &std_output, + const std::string &std_error) { #ifdef _WIN32 - // we don't support stdin/stdout redirection on Windows - assert(std_input.empty()); - assert(std_output.empty()); + // we don't support stdin/stdout/stderr redirection on Windows + PRECONDITION(std_input.empty()); + PRECONDITION(std_output.empty()); + PRECONDITION(std_error.empty()); // unicode version of the arguments std::vector wargv; @@ -77,29 +116,12 @@ int run( return status; #else - int stdin_fd=STDIN_FILENO; + int stdin_fd = stdio_redirection(STDIN_FILENO, std_input); + int stdout_fd = stdio_redirection(STDOUT_FILENO, std_output); + int stderr_fd = stdio_redirection(STDERR_FILENO, std_error); - if(!std_input.empty()) - { - stdin_fd=open(std_input.c_str(), O_RDONLY); - if(stdin_fd==-1) - { - perror("Failed to open stdin copy"); - return 1; - } - } - - int stdout_fd=STDOUT_FILENO; - - if(!std_output.empty()) - { - stdout_fd=open(std_output.c_str(), O_CREAT|O_WRONLY, S_IRUSR|S_IWUSR); - if(stdout_fd==-1) - { - perror("Failed to open stdout copy"); - return 1; - } - } + if(stdin_fd == -1 || stdout_fd == -1 || stderr_fd == -1) + return 1; // temporarily suspend all signals sigset_t new_mask, old_mask; @@ -127,6 +149,8 @@ int run( dup2(stdin_fd, STDIN_FILENO); if(stdout_fd!=STDOUT_FILENO) dup2(stdout_fd, STDOUT_FILENO); + if(stderr_fd != STDERR_FILENO) + dup2(stderr_fd, STDERR_FILENO); errno=0; execvp(what.c_str(), _argv.data()); @@ -153,6 +177,8 @@ int run( close(stdin_fd); if(stdout_fd!=STDOUT_FILENO) close(stdout_fd); + if(stderr_fd != STDERR_FILENO) + close(stderr_fd); return 1; } @@ -160,6 +186,8 @@ int run( close(stdin_fd); if(stdout_fd!=STDOUT_FILENO) close(stdout_fd); + if(stderr_fd != STDERR_FILENO) + close(stderr_fd); return WEXITSTATUS(status); } @@ -173,6 +201,8 @@ int run( close(stdin_fd); if(stdout_fd!=STDOUT_FILENO) close(stdout_fd); + if(stderr_fd != STDERR_FILENO) + close(stderr_fd); return 1; } diff --git a/src/util/run.h b/src/util/run.h index 83f971d5d1a..14e2818edf3 100644 --- a/src/util/run.h +++ b/src/util/run.h @@ -18,8 +18,9 @@ Date: August 2012 int run( const std::string &what, const std::vector &argv, - const std::string &std_input, - const std::string &std_output); + const std::string &std_input = "", + const std::string &std_output = "", + const std::string &std_error = ""); int run_shell(const std::string &command); From fd910a7c99d5d8f4c678fa4932abd33227a6bd47 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 25 May 2018 15:41:07 +0100 Subject: [PATCH 2/5] added gcc_versiont --- src/goto-cc/Makefile | 1 + src/goto-cc/gcc_version.cpp | 89 +++++++++++++++++++++++++++++++++++++ src/goto-cc/gcc_version.h | 45 +++++++++++++++++++ 3 files changed, 135 insertions(+) create mode 100644 src/goto-cc/gcc_version.cpp create mode 100644 src/goto-cc/gcc_version.h diff --git a/src/goto-cc/Makefile b/src/goto-cc/Makefile index f056c1258c1..3e8e6e8bdb1 100644 --- a/src/goto-cc/Makefile +++ b/src/goto-cc/Makefile @@ -8,6 +8,7 @@ SRC = armcc_cmdline.cpp \ cw_mode.cpp \ gcc_cmdline.cpp \ gcc_mode.cpp \ + gcc_version.cpp \ goto_cc_cmdline.cpp \ goto_cc_languages.cpp \ goto_cc_main.cpp \ diff --git a/src/goto-cc/gcc_version.cpp b/src/goto-cc/gcc_version.cpp new file mode 100644 index 00000000000..f96094f91b0 --- /dev/null +++ b/src/goto-cc/gcc_version.cpp @@ -0,0 +1,89 @@ +/*******************************************************************\ + +Module: GCC Mode + +Author: Daniel Kroening, 2018 + +\*******************************************************************/ + +#include "gcc_version.h" + +#include +#include +#include +#include +#include + +#include + +void gcc_versiont::get(const std::string &executable) +{ + temporary_filet tmp_file_in("goto-gcc.", ".in"); + temporary_filet tmp_file_out("goto-gcc.", ".out"); + temporary_filet tmp_file_err("goto-gcc.", ".err"); + + { + std::ofstream out(tmp_file_in()); + + out << "#if defined(__clang_major__)\n" + "clang __clang_major__ __clang_minor__ __clang_patchlevel__\n" + "#elif defined(__BCC__)\n" + "bcc 0 0 0\n" + "#else\n" + "gcc __GNUC__ __GNUC_MINOR__ __GNUC_PATCHLEVEL__\n" + "#endif\n"; + } + + // some variants output stuff on stderr, say Apple LLVM, + // which we silence. + int result = run( + executable, + {executable, "-E", "-", "-o", "-"}, + tmp_file_in(), + tmp_file_out(), + tmp_file_err()); + + v_major = v_minor = v_patchlevel = 0; + flavor = flavort::UNKNOWN; + + if(result >= 0) + { + std::ifstream in(tmp_file_out()); + std::string line; + + while(!in.fail() && std::getline(in, line)) + if(!line.empty() && line[0] != '#') + break; + + auto split = split_string(line, ' '); + + if(split.size() >= 4) + { + if(split[0] == "gcc") + flavor = flavort::GCC; + else if(split[0] == "bcc") + flavor = flavort::BCC; + else if(split[0] == "clang") + flavor = flavort::CLANG; + + v_major = unsafe_string2unsigned(split[1]); + v_minor = unsafe_string2unsigned(split[2]); + v_patchlevel = unsafe_string2unsigned(split[3]); + } + } +} + +bool gcc_versiont::is_at_least( + unsigned _major, + unsigned _minor, + unsigned _patchlevel) const +{ + return v_major > _major || (v_major == _major && v_minor > _minor) || + (v_major == _major && v_minor == _minor && + v_patchlevel >= _patchlevel); +} + +std::ostream &operator<<(std::ostream &out, const gcc_versiont &v) +{ + return out << v.v_major << '.' << v.v_minor << '.' << v.v_patchlevel; +} diff --git a/src/goto-cc/gcc_version.h b/src/goto-cc/gcc_version.h new file mode 100644 index 00000000000..59af0123f0b --- /dev/null +++ b/src/goto-cc/gcc_version.h @@ -0,0 +1,45 @@ +/*******************************************************************\ + +Module: gcc version numbering scheme + +Author: Daniel Kroening + +Date: May 2018 + +\*******************************************************************/ + +#ifndef CPROVER_GOTO_CC_GCC_VERSION_H +#define CPROVER_GOTO_CC_GCC_VERSION_H + +#include +#include + +class gcc_versiont +{ +public: + unsigned v_major, v_minor, v_patchlevel; + + void get(const std::string &executable); + + bool is_at_least( + unsigned v_major, + unsigned v_minor = 0, + unsigned v_patchlevel = 0) const; + + enum class flavort + { + UNKNOWN, + CLANG, + GCC, + BCC + } flavor; + + gcc_versiont() + : v_major(0), v_minor(0), v_patchlevel(0), flavor(flavort::UNKNOWN) + { + } +}; + +std::ostream &operator<<(std::ostream &, const gcc_versiont &); + +#endif From cd6ecec366a6aa865e50374930dfc18850097088 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 25 May 2018 22:00:48 +0100 Subject: [PATCH 3/5] goto-cc now reports version of installed gcc --- src/goto-cc/gcc_mode.cpp | 32 ++++++++++++++++++++++++-------- src/goto-cc/gcc_mode.h | 3 +++ 2 files changed, 27 insertions(+), 8 deletions(-) diff --git a/src/goto-cc/gcc_mode.cpp b/src/goto-cc/gcc_mode.cpp index fb58565c6f1..843bb7f5fe2 100644 --- a/src/goto-cc/gcc_mode.cpp +++ b/src/goto-cc/gcc_mode.cpp @@ -336,6 +336,9 @@ int gcc_modet::doit() base_name=="bcc" || base_name.find("goto-bcc")!=std::string::npos; + // if we are gcc or bcc, then get the version number + gcc_version.get(native_tool_name); + if((cmdline.isset('v') && cmdline.have_infile_arg()) || (cmdline.isset("version") && !produce_hybrid_binary)) { @@ -343,9 +346,16 @@ int gcc_modet::doit() // Compilation continues, don't exit! if(act_as_bcc) - std::cout << "bcc: version 0.16.17 (goto-cc " CBMC_VERSION ")\n"; + std::cout << "bcc: version " << gcc_version + << " (goto-cc " CBMC_VERSION ")\n"; else - std::cout << "gcc version 3.4.4 (goto-cc " CBMC_VERSION ")\n"; + { + if(gcc_version.flavor == gcc_versiont::flavort::CLANG) + std::cout << "clang version " << gcc_version + << " (goto-cc " CBMC_VERSION ")\n"; + else + std::cout << "gcc (goto-cc " CBMC_VERSION ") " << gcc_version << '\n'; + } } compilet compiler(cmdline, @@ -359,11 +369,17 @@ int gcc_modet::doit() if(produce_hybrid_binary) return run_gcc(compiler); - std::cout << '\n' << - "Copyright (C) 2006-2014 Daniel Kroening, Christoph Wintersteiger\n" << - "CBMC version: " CBMC_VERSION << '\n' << - "Architecture: " << config.this_architecture() << '\n' << - "OS: " << config.this_operating_system() << '\n'; + std::cout + << '\n' + << "Copyright (C) 2006-2018 Daniel Kroening, Christoph Wintersteiger\n" + << "CBMC version: " CBMC_VERSION << '\n' + << "Architecture: " << config.this_architecture() << '\n' + << "OS: " << config.this_operating_system() << '\n'; + + if(gcc_version.flavor == gcc_versiont::flavort::CLANG) + std::cout << "clang: " << gcc_version << '\n'; + else + std::cout << "gcc: " << gcc_version << '\n'; return EX_OK; // Exit! } @@ -381,7 +397,7 @@ int gcc_modet::doit() if(cmdline.isset("dumpmachine")) std::cout << config.this_architecture() << '\n'; else if(cmdline.isset("dumpversion")) - std::cout << "3.4.4\n"; + std::cout << gcc_version << '\n'; // we don't have any meaningful output for the other options, and GCC // doesn't necessarily produce non-empty output either diff --git a/src/goto-cc/gcc_mode.h b/src/goto-cc/gcc_mode.h index 10cfb9e7bb1..2bde2c02bb3 100644 --- a/src/goto-cc/gcc_mode.h +++ b/src/goto-cc/gcc_mode.h @@ -15,6 +15,7 @@ Date: June 2006 #define CPROVER_GOTO_CC_GCC_MODE_H #include "compile.h" +#include "gcc_version.h" #include "goto_cc_mode.h" #include @@ -61,6 +62,8 @@ class gcc_modet:public goto_cc_modet const compilet &compiler); static bool needs_preprocessing(const std::string &); + + gcc_versiont gcc_version; }; #endif // CPROVER_GOTO_CC_GCC_MODE_H From e040723285d6e2b170f913e8a2ed1d1af7a0bd7c Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Wed, 30 May 2018 19:39:30 +0100 Subject: [PATCH 4/5] _FloatX support based on gcc version --- appveyor.yml | 1 + regression/ansi-c/float_constant1/main.c | 2 +- .../ansi-c/gcc_types_compatible_p1/main.c | 9 ++++--- regression/ansi-c/gcc_version1/fake-gcc-4 | 4 +++ regression/ansi-c/gcc_version1/fake-gcc-7 | 4 +++ regression/ansi-c/gcc_version1/gcc-4.c | 2 ++ regression/ansi-c/gcc_version1/gcc-7.c | 2 ++ .../ansi-c/gcc_version1/test-gcc-4.desc | 7 +++++ .../ansi-c/gcc_version1/test-gcc-7.desc | 7 +++++ src/ansi-c/ansi_c_language.cpp | 2 ++ src/ansi-c/ansi_c_parser.h | 6 ++++- src/ansi-c/scanner.l | 27 +++++++++---------- src/cpp/cpp_parser.cpp | 1 + src/goto-cc/gcc_mode.cpp | 5 ++++ src/util/config.cpp | 6 +++-- src/util/config.h | 1 + 16 files changed, 65 insertions(+), 21 deletions(-) create mode 100755 regression/ansi-c/gcc_version1/fake-gcc-4 create mode 100755 regression/ansi-c/gcc_version1/fake-gcc-7 create mode 100644 regression/ansi-c/gcc_version1/gcc-4.c create mode 100644 regression/ansi-c/gcc_version1/gcc-7.c create mode 100644 regression/ansi-c/gcc_version1/test-gcc-4.desc create mode 100644 regression/ansi-c/gcc_version1/test-gcc-7.desc diff --git a/appveyor.yml b/appveyor.yml index f887a34225b..ee24f7bcfb8 100644 --- a/appveyor.yml +++ b/appveyor.yml @@ -74,6 +74,7 @@ test_script: rmdir /s /q ansi-c\Universal_characters1 rmdir /s /q ansi-c\function_return1 rmdir /s /q ansi-c\gcc_attributes7 + rmdir /s /q ansi-c\gcc_version1 rmdir /s /q ansi-c\struct6 rmdir /s /q ansi-c\struct7 rmdir /s /q cbmc\Malloc23 diff --git a/regression/ansi-c/float_constant1/main.c b/regression/ansi-c/float_constant1/main.c index 4f109a85d6e..4498df4a605 100644 --- a/regression/ansi-c/float_constant1/main.c +++ b/regression/ansi-c/float_constant1/main.c @@ -12,7 +12,7 @@ STATIC_ASSERT(0X.0p+1f == 0); // 32-bit, 64-bit and 128-bit constants, GCC proper only, // clang doesn't have it -#if defined(__GNUC__) && !defined(__clang__) +#if defined(__GNUC__) && !defined(__clang__) && __GNUC__ >= 7 STATIC_ASSERT(__builtin_types_compatible_p(_Float32, __typeof(1.0f32))); STATIC_ASSERT(__builtin_types_compatible_p(_Float64, __typeof(1.0f64))); STATIC_ASSERT(__builtin_types_compatible_p(_Float128, __typeof(1.0f128))); diff --git a/regression/ansi-c/gcc_types_compatible_p1/main.c b/regression/ansi-c/gcc_types_compatible_p1/main.c index d27ddfdac6b..6a4608bf5bd 100644 --- a/regression/ansi-c/gcc_types_compatible_p1/main.c +++ b/regression/ansi-c/gcc_types_compatible_p1/main.c @@ -67,8 +67,8 @@ STATIC_ASSERT(__builtin_types_compatible_p(typeof (hot) *, int *)); STATIC_ASSERT(__builtin_types_compatible_p(typeof (hot), typeof (janette))); STATIC_ASSERT(__builtin_types_compatible_p(__int128, signed __int128)); -#ifndef __clang__ // clang doesn't have these +#if !defined(__clang__) && __GNUC__ >= 7 #if defined(__x86_64__) || defined(__i386__) STATIC_ASSERT(__builtin_types_compatible_p(__float128, _Float128)); #endif @@ -95,16 +95,19 @@ STATIC_ASSERT(!__builtin_types_compatible_p(long int, int)); STATIC_ASSERT(!__builtin_types_compatible_p(long long int, long int)); STATIC_ASSERT(!__builtin_types_compatible_p(unsigned, signed)); -#ifndef __clang__ +STATIC_ASSERT(!__builtin_types_compatible_p(__int128, unsigned __int128)); + // clang doesn't have these +#if !defined(__clang__) +#if __GNUC__ >= 7 STATIC_ASSERT(!__builtin_types_compatible_p(_Float32, float)); STATIC_ASSERT(!__builtin_types_compatible_p(_Float64, double)); STATIC_ASSERT(!__builtin_types_compatible_p(_Float32x, float)); STATIC_ASSERT(!__builtin_types_compatible_p(_Float64x, double)); +#endif STATIC_ASSERT(!__builtin_types_compatible_p(__float80, double)); STATIC_ASSERT(!__builtin_types_compatible_p(__float128, long double)); STATIC_ASSERT(!__builtin_types_compatible_p(__float128, double)); -STATIC_ASSERT(!__builtin_types_compatible_p(__int128, unsigned __int128)); #endif #endif diff --git a/regression/ansi-c/gcc_version1/fake-gcc-4 b/regression/ansi-c/gcc_version1/fake-gcc-4 new file mode 100755 index 00000000000..7519ebbb295 --- /dev/null +++ b/regression/ansi-c/gcc_version1/fake-gcc-4 @@ -0,0 +1,4 @@ +#!/bin/sh + +gcc -Wno-macro-redefined -U __clang_major__ -D __GNUC__=4 -D __GNUC_MINOR__=9 -D __GNUC_PATCHLEVEL__=1 $* + diff --git a/regression/ansi-c/gcc_version1/fake-gcc-7 b/regression/ansi-c/gcc_version1/fake-gcc-7 new file mode 100755 index 00000000000..2677c324fc4 --- /dev/null +++ b/regression/ansi-c/gcc_version1/fake-gcc-7 @@ -0,0 +1,4 @@ +#!/bin/sh + +gcc -Wno-macro-redefined -U __clang_major__ -D __GNUC__=7 -D __GNUC_MINOR__=0 -D __GNUC_PATCHLEVEL__=0 $* + diff --git a/regression/ansi-c/gcc_version1/gcc-4.c b/regression/ansi-c/gcc_version1/gcc-4.c new file mode 100644 index 00000000000..146830401fb --- /dev/null +++ b/regression/ansi-c/gcc_version1/gcc-4.c @@ -0,0 +1,2 @@ +typedef double _Float64; + diff --git a/regression/ansi-c/gcc_version1/gcc-7.c b/regression/ansi-c/gcc_version1/gcc-7.c new file mode 100644 index 00000000000..f2b0379790b --- /dev/null +++ b/regression/ansi-c/gcc_version1/gcc-7.c @@ -0,0 +1,2 @@ +_Float64 some_var; + diff --git a/regression/ansi-c/gcc_version1/test-gcc-4.desc b/regression/ansi-c/gcc_version1/test-gcc-4.desc new file mode 100644 index 00000000000..880a913fdd6 --- /dev/null +++ b/regression/ansi-c/gcc_version1/test-gcc-4.desc @@ -0,0 +1,7 @@ +CORE +gcc-4.c +--native-compiler ./fake-gcc-4 +^EXIT=0$ +^SIGNAL=0$ +-- +^CONVERSION ERROR$ diff --git a/regression/ansi-c/gcc_version1/test-gcc-7.desc b/regression/ansi-c/gcc_version1/test-gcc-7.desc new file mode 100644 index 00000000000..18c69f9b584 --- /dev/null +++ b/regression/ansi-c/gcc_version1/test-gcc-7.desc @@ -0,0 +1,7 @@ +CORE +gcc-7.c +--native-compiler ./fake-gcc-7 +^EXIT=0$ +^SIGNAL=0$ +-- +^CONVERSION ERROR$ diff --git a/src/ansi-c/ansi_c_language.cpp b/src/ansi-c/ansi_c_language.cpp index bbb1236e9e7..16d63d06157 100644 --- a/src/ansi-c/ansi_c_language.cpp +++ b/src/ansi-c/ansi_c_language.cpp @@ -75,6 +75,7 @@ bool ansi_c_languaget::parse( ansi_c_parser.in=&codestr; 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.cpp98=false; // it's not C++ ansi_c_parser.cpp11=false; // it's not C++ ansi_c_parser.mode=config.ansi_c.mode; @@ -196,6 +197,7 @@ bool ansi_c_languaget::to_expr( ansi_c_parser.in=&i_preprocessed; ansi_c_parser.set_message_handler(get_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_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 b5dad0a515f..a7c03191fce 100644 --- a/src/ansi-c/ansi_c_parser.h +++ b/src/ansi-c/ansi_c_parser.h @@ -35,7 +35,8 @@ class ansi_c_parsert:public parsert mode(modet::NONE), cpp98(false), cpp11(false), - for_has_scope(false) + for_has_scope(false), + ts_18661_3_Floatn_types(false) { } @@ -77,6 +78,9 @@ class ansi_c_parsert:public parsert // in C99 and upwards, for(;;) has a scope bool for_has_scope; + // ISO/IEC TS 18661-3:2015 + bool ts_18661_3_Floatn_types; + typedef ansi_c_identifiert identifiert; typedef ansi_c_scopet scopet; diff --git a/src/ansi-c/scanner.l b/src/ansi-c/scanner.l index 2d0880d8e77..c45228e9ca5 100644 --- a/src/ansi-c/scanner.l +++ b/src/ansi-c/scanner.l @@ -459,36 +459,31 @@ void ansi_c_scanner_init() return make_identifier(); } -"_Float16" { // clang doesn't have it - if(PARSER.mode==configt::ansi_ct::flavourt::GCC) +"_Float16" { if(PARSER.ts_18661_3_Floatn_types) { loc(); return TOK_GCC_FLOAT16; } else return make_identifier(); } -"_Float32" { // clang doesn't have it - if(PARSER.mode==configt::ansi_ct::flavourt::GCC) +"_Float32" { if(PARSER.ts_18661_3_Floatn_types) { loc(); return TOK_GCC_FLOAT32; } else return make_identifier(); } -"_Float32x" { // clang doesn't have it - if(PARSER.mode==configt::ansi_ct::flavourt::GCC) +"_Float32x" { if(PARSER.ts_18661_3_Floatn_types) { loc(); return TOK_GCC_FLOAT32X; } else return make_identifier(); } -"_Float64" { // clang doesn't have it - if(PARSER.mode==configt::ansi_ct::flavourt::GCC) +"_Float64" { if(PARSER.ts_18661_3_Floatn_types) { loc(); return TOK_GCC_FLOAT64; } else return make_identifier(); } -"_Float64x" { // clang doesn't have it - if(PARSER.mode==configt::ansi_ct::flavourt::GCC) +"_Float64x" { if(PARSER.ts_18661_3_Floatn_types) { loc(); return TOK_GCC_FLOAT64X; } else return make_identifier(); @@ -501,16 +496,20 @@ void ansi_c_scanner_init() return make_identifier(); } -"__float128" | -"_Float128" { // clang doesn't have it +"__float128" { // clang doesn't have it if(PARSER.mode==configt::ansi_ct::flavourt::GCC) { loc(); return TOK_GCC_FLOAT128; } else return make_identifier(); } -"_Float128x" { // clang doesn't have it - if(PARSER.mode==configt::ansi_ct::flavourt::GCC) +"_Float128" { if(PARSER.ts_18661_3_Floatn_types) + { loc(); return TOK_GCC_FLOAT128; } + else + return make_identifier(); + } + +"_Float128x" { if(PARSER.ts_18661_3_Floatn_types) { loc(); return TOK_GCC_FLOAT128X; } else return make_identifier(); diff --git a/src/cpp/cpp_parser.cpp b/src/cpp/cpp_parser.cpp index eae4728bbc4..e73fba627f9 100644 --- a/src/cpp/cpp_parser.cpp +++ b/src/cpp/cpp_parser.cpp @@ -24,6 +24,7 @@ bool cpp_parsert::parse() ansi_c_parser.cpp11= 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.in=in; ansi_c_parser.mode=mode; ansi_c_parser.set_file(get_file()); diff --git a/src/goto-cc/gcc_mode.cpp b/src/goto-cc/gcc_mode.cpp index 843bb7f5fe2..f4dee67c0dc 100644 --- a/src/goto-cc/gcc_mode.cpp +++ b/src/goto-cc/gcc_mode.cpp @@ -525,6 +525,11 @@ 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; + // -fshort-double makes double the same as float if(cmdline.isset("fshort-double")) config.ansi_c.double_width=config.ansi_c.single_width; diff --git a/src/util/config.cpp b/src/util/config.cpp index e47d6a77ca2..f9ce580485d 100644 --- a/src/util/config.cpp +++ b/src/util/config.cpp @@ -742,6 +742,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.c_standard=ansi_ct::default_c_standard(); ansi_c.endianness=ansi_ct::endiannesst::NO_ENDIANNESS; ansi_c.os=ansi_ct::ost::NO_OS; @@ -1139,8 +1140,9 @@ void configt::set_from_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 not - // stored in namespace + // for_has_scope, single_precision_constant, rounding_mode, + // ts_18661_3_Floatn_types 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 57cf613956f..9f3bf9ee61a 100644 --- a/src/util/config.h +++ b/src/util/config.h @@ -42,6 +42,7 @@ class configt // various language options 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 single_precision_constant; enum class c_standardt { C89, C99, C11 } c_standard; static c_standardt default_c_standard(); From 78794e21fea0e0d833d0014a51b68572bc5e585e Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 31 May 2018 17:47:19 +0100 Subject: [PATCH 5/5] undo parts of #2185 --- regression/cbmc/ts18661_typedefs/main.c | 9 +++++++++ src/ansi-c/ansi_c_convert_type.cpp | 19 +++---------------- 2 files changed, 12 insertions(+), 16 deletions(-) diff --git a/regression/cbmc/ts18661_typedefs/main.c b/regression/cbmc/ts18661_typedefs/main.c index 06ef87fbc72..1c3972d9656 100644 --- a/regression/cbmc/ts18661_typedefs/main.c +++ b/regression/cbmc/ts18661_typedefs/main.c @@ -1,9 +1,18 @@ +#if defined(__clang__) +#elif defined(__GNUC__) +#if __GNUC__ >= 7 +#define HAS_FLOATN +#endif +#endif + +#ifndef HAS_FLOATN typedef float _Float32; typedef double _Float32x; typedef double _Float64; typedef long double _Float64x; typedef long double _Float128; typedef long double _Float128x; +#endif int main(int argc, char** argv) { } diff --git a/src/ansi-c/ansi_c_convert_type.cpp b/src/ansi-c/ansi_c_convert_type.cpp index c1f8956c64e..e30503ae627 100644 --- a/src/ansi-c/ansi_c_convert_type.cpp +++ b/src/ansi-c/ansi_c_convert_type.cpp @@ -346,22 +346,9 @@ void ansi_c_convert_typet::write(typet &type) gcc_float64_cnt+gcc_float64x_cnt+ gcc_float128_cnt+gcc_float128x_cnt>=2) { - // Temporary workaround for our glibc versions that try to define TS 18661 - // types (for example, typedef float _Float32). This can be removed once - // upgrade cbmc's GCC support to at least 7.0 (when glibc will expect us - // to provide these types natively), or disable parsing them ourselves - // when our preprocessor stage claims support <7.0. - if(c_storage_spec.is_typedef) - { - warning().source_location = source_location; - warning() << "ignoring typedef for TS 18661 (_FloatNNx) type. If you need these, try using goto-cc instead." << eom; - } - else - { - error().source_location=source_location; - error() << "conflicting type modifiers" << eom; - throw 0; - } + error().source_location=source_location; + error() << "conflicting type modifiers" << eom; + throw 0; } // _not_ the same as float, double, long double