From 4a5b95280a7cef3f9bf999d5bf827bd265230472 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 5 Mar 2018 12:46:52 +0000 Subject: [PATCH 1/6] export all gcc bultin headers --- src/ansi-c/ansi_c_internal_additions.h | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/ansi-c/ansi_c_internal_additions.h b/src/ansi-c/ansi_c_internal_additions.h index a0977a35331..7cdcce2e104 100644 --- a/src/ansi-c/ansi_c_internal_additions.h +++ b/src/ansi-c/ansi_c_internal_additions.h @@ -15,17 +15,22 @@ Author: Daniel Kroening, kroening@kroening.com void ansi_c_internal_additions(std::string &code); void ansi_c_architecture_strings(std::string &code); +extern const char clang_builtin_headers[]; extern const char gcc_builtin_headers_generic[]; extern const char gcc_builtin_headers_math[]; extern const char gcc_builtin_headers_mem_string[]; extern const char gcc_builtin_headers_omp[]; extern const char gcc_builtin_headers_tm[]; extern const char gcc_builtin_headers_ubsan[]; -extern const char clang_builtin_headers[]; extern const char gcc_builtin_headers_ia32[]; extern const char gcc_builtin_headers_ia32_2[]; extern const char gcc_builtin_headers_ia32_3[]; extern const char gcc_builtin_headers_ia32_4[]; +extern const char gcc_builtin_headers_alpha[]; +extern const char gcc_builtin_headers_arm[]; +extern const char gcc_builtin_headers_mips[]; +extern const char gcc_builtin_headers_power[]; extern const char arm_builtin_headers[]; +extern const char cw_builtin_headers[]; #endif // CPROVER_ANSI_C_ANSI_C_INTERNAL_ADDITIONS_H From 1711345ce10fd69d54b2b12f19c955be546d7cbe Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 5 Mar 2018 12:36:50 +0000 Subject: [PATCH 2/6] added a factory for builtin function declarations --- src/ansi-c/Makefile | 1 + src/ansi-c/builtin_factory.cpp | 169 +++++++++++++++++++++++++++++++++ src/ansi-c/builtin_factory.h | 21 ++++ 3 files changed, 191 insertions(+) create mode 100644 src/ansi-c/builtin_factory.cpp create mode 100644 src/ansi-c/builtin_factory.h diff --git a/src/ansi-c/Makefile b/src/ansi-c/Makefile index 559bff9603d..4f1e6c90d10 100644 --- a/src/ansi-c/Makefile +++ b/src/ansi-c/Makefile @@ -10,6 +10,7 @@ SRC = anonymous_member.cpp \ ansi_c_scope.cpp \ ansi_c_typecheck.cpp \ ansi_c_y.tab.cpp \ + builtin_factory.cpp \ c_misc.cpp \ c_nondet_symbol_factory.cpp \ c_preprocess.cpp \ diff --git a/src/ansi-c/builtin_factory.cpp b/src/ansi-c/builtin_factory.cpp new file mode 100644 index 00000000000..534a774b87e --- /dev/null +++ b/src/ansi-c/builtin_factory.cpp @@ -0,0 +1,169 @@ +/*******************************************************************\ + +Module: + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +#include "builtin_factory.h" +#include "ansi_c_internal_additions.h" + +#include "ansi_c_parser.h" +#include "ansi_c_typecheck.h" + +#include +#include +#include + +const char windows_headers[]= + "int __noop();\n" + "int __assume(int);\n"; + +//! Advance to the next line +static const char *next_line(const char *line) +{ + const char *end=strchr(line, '\n'); + + if(end==NULL) + return strchr(line, 0); + else + return end+1; +} + +//! Look for given pattern in given string. +//! Add line with pattern to 'out' if found. +//! \return 'true' if found +static bool find_pattern( + const std::string &pattern, + const char *header_file, + std::ostream &out) +{ + // read line-by-line + const char *line, *line_end; + + for(line=header_file; *line!=0; line=line_end) + { + line_end=next_line(line); + + // skip spaces + while(*line==' ') + line++; + + if(line[0]=='/' && line[1]=='/') // comment + continue; + + for(const char *p=line; psecond); + + return false; +} + +//! Check whether given identifier is a compiler built-in. +//! If so, add declaration to symbol table. +//! \return 'true' on error +bool builtin_factory( + const irep_idt &identifier, + symbol_tablet &symbol_table, + message_handlert &mh) +{ + // we search for "space" "identifier" "(" + const std::string pattern=' '+id2string(identifier)+'('; + + std::ostringstream s; + + std::string code; + ansi_c_internal_additions(code); + s << code; + + if(find_pattern(pattern, gcc_builtin_headers_generic, s)) + return convert(identifier, s, symbol_table, mh); + + if(find_pattern(pattern, gcc_builtin_headers_mem_string, s)) + return convert(identifier, s, symbol_table, mh); + + if(find_pattern(pattern, gcc_builtin_headers_omp, s)) + return convert(identifier, s, symbol_table, mh); + + if(find_pattern(pattern, gcc_builtin_headers_tm, s)) + return convert(identifier, s, symbol_table, mh); + + if(find_pattern(pattern, gcc_builtin_headers_ubsan, s)) + return convert(identifier, s, symbol_table, mh); + + if(find_pattern(pattern, gcc_builtin_headers_ia32, s)) + return convert(identifier, s, symbol_table, mh); + + if(find_pattern(pattern, gcc_builtin_headers_ia32_2, s)) + return convert(identifier, s, symbol_table, mh); + + if(find_pattern(pattern, gcc_builtin_headers_ia32_3, s)) + return convert(identifier, s, symbol_table, mh); + + if(find_pattern(pattern, gcc_builtin_headers_ia32_4, s)) + return convert(identifier, s, symbol_table, mh); + + return true; +} diff --git a/src/ansi-c/builtin_factory.h b/src/ansi-c/builtin_factory.h new file mode 100644 index 00000000000..9fffb891c26 --- /dev/null +++ b/src/ansi-c/builtin_factory.h @@ -0,0 +1,21 @@ +/*******************************************************************\ + +Module: + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +#ifndef CPROVER_ANSI_C_BUILTIN_FACTORY_H +#define CPROVER_ANSI_C_BUILTIN_FACTORY_H + +#include +#include + +//! \return 'true' in case of error +bool builtin_factory( + const irep_idt &identifier, + symbol_tablet &, + message_handlert &); + +#endif // CPROVER_ANSI_C_BUILTIN_FACTORY_H From 15ec42f1165355538fc9aa1670dff99da76d5fd1 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 5 Mar 2018 12:39:01 +0000 Subject: [PATCH 3/6] use the builtins factory in the C frontend --- src/ansi-c/CMakeLists.txt | 2 + src/ansi-c/Makefile | 69 +++++++++----- src/ansi-c/ansi_c_internal_additions.cpp | 48 +++------- src/ansi-c/ansi_c_internal_additions.h | 1 + src/ansi-c/builtin_factory.cpp | 110 ++++++++++++++++++----- src/ansi-c/c_typecheck_expr.cpp | 69 ++++++++------ src/ansi-c/clang_builtin_headers.h | 2 - src/ansi-c/gcc_builtin_headers_generic.h | 35 -------- src/ansi-c/gcc_builtin_headers_types.h | 33 +++++++ 9 files changed, 217 insertions(+), 152 deletions(-) create mode 100644 src/ansi-c/gcc_builtin_headers_types.h diff --git a/src/ansi-c/CMakeLists.txt b/src/ansi-c/CMakeLists.txt index fea313b21b8..be4d003342e 100644 --- a/src/ansi-c/CMakeLists.txt +++ b/src/ansi-c/CMakeLists.txt @@ -72,6 +72,7 @@ make_inc(gcc_builtin_headers_mips) make_inc(gcc_builtin_headers_omp) make_inc(gcc_builtin_headers_power) make_inc(gcc_builtin_headers_tm) +make_inc(gcc_builtin_headers_types) make_inc(gcc_builtin_headers_ubsan) set(extra_dependencies @@ -92,6 +93,7 @@ set(extra_dependencies ${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_omp.inc ${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_power.inc ${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_tm.inc + ${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_types.inc ${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_ubsan.inc ${CMAKE_CURRENT_BINARY_DIR}/library-check.stamp ) diff --git a/src/ansi-c/Makefile b/src/ansi-c/Makefile index 4f1e6c90d10..5b3383a3ab2 100644 --- a/src/ansi-c/Makefile +++ b/src/ansi-c/Makefile @@ -49,15 +49,24 @@ CLEANFILES = ansi-c$(LIBEXT) \ ansi_c_y.output \ library/converter$(EXEEXT) cprover_library.inc \ file_converter$(EXEEXT) library_check \ - gcc_builtin_headers_generic.inc gcc_builtin_headers_ia32.inc \ - arm_builtin_headers.inc cw_builtin_headers.inc \ - gcc_builtin_headers_arm.inc gcc_builtin_headers_alpha.inc \ - gcc_builtin_headers_mips.inc gcc_builtin_headers_power.inc \ - clang_builtin_headers.inc gcc_builtin_headers_ia32-2.inc \ - gcc_builtin_headers_math.inc gcc_builtin_headers_omp.inc \ - gcc_builtin_headers_tm.inc gcc_builtin_headers_ubsan.inc \ + arm_builtin_headers.inc \ + clang_builtin_headers.inc \ + cw_builtin_headers.inc \ + gcc_builtin_headers_alpha.inc \ + gcc_builtin_headers_arm.inc \ + gcc_builtin_headers_generic.inc \ + gcc_builtin_headers_ia32-2.inc \ + gcc_builtin_headers_ia32-3.inc \ + gcc_builtin_headers_ia32-4.inc \ + gcc_builtin_headers_ia32.inc \ + gcc_builtin_headers_math.inc \ gcc_builtin_headers_mem_string.inc \ - gcc_builtin_headers_ia32-3.inc gcc_builtin_headers_ia32-4.inc + gcc_builtin_headers_mips.inc \ + gcc_builtin_headers_omp.inc \ + gcc_builtin_headers_power.inc \ + gcc_builtin_headers_tm.inc \ + gcc_builtin_headers_types.inc \ + gcc_builtin_headers_ubsan.inc all: ansi-c$(LIBEXT) @@ -103,34 +112,46 @@ cprover_library.inc: library/converter$(EXEEXT) library/*.c cprover_library.cpp: cprover_library.inc +ansi_c_internal_additions$(OBJEXT): arm_builtin_headers.inc +ansi_c_internal_additions$(OBJEXT): clang_builtin_headers.inc +ansi_c_internal_additions$(OBJEXT): cw_builtin_headers.inc +ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_alpha.inc +ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_arm.inc ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_generic.inc -ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_ia32.inc ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_ia32-2.inc ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_ia32-3.inc ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_ia32-4.inc -ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_alpha.inc -ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_arm.inc +ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_ia32.inc ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_math.inc ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_mem_string.inc ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_mips.inc ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_omp.inc ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_power.inc ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_tm.inc +ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_types.inc ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_ubsan.inc -ansi_c_internal_additions$(OBJEXT): arm_builtin_headers.inc -ansi_c_internal_additions$(OBJEXT): cw_builtin_headers.inc -ansi_c_internal_additions$(OBJEXT): clang_builtin_headers.inc -generated_files: cprover_library.inc gcc_builtin_headers_generic.inc \ - gcc_builtin_headers_ia32.inc gcc_builtin_headers_alpha.inc \ - gcc_builtin_headers_arm.inc gcc_builtin_headers_mips.inc \ - gcc_builtin_headers_power.inc arm_builtin_headers.inc \ - cw_builtin_headers.inc ansi_c_y.tab.cpp ansi_c_lex.yy.cpp \ - ansi_c_y.tab.h clang_builtin_headers.inc gcc_builtin_headers_ia32-2.inc \ - gcc_builtin_headers_math.inc gcc_builtin_headers_omp.inc \ - gcc_builtin_headers_tm.inc gcc_builtin_headers_ubsan.inc \ - gcc_builtin_headers_mem_string.inc \ - gcc_builtin_headers_ia32-3.inc gcc_builtin_headers_ia32-4.inc +generated_files: \ + ansi_c_y.tab.cpp ansi_c_lex.yy.cpp ansi_c_y.tab.h \ + arm_builtin_headers.inc \ + clang_builtin_headers.inc \ + cprover_library.inc \ + cw_builtin_headers.inc \ + gcc_builtin_headers_alpha.inc \ + gcc_builtin_headers_arm.inc \ + gcc_builtin_headers_generic.inc \ + gcc_builtin_headers_ia32-2.inc \ + gcc_builtin_headers_ia32-3.inc \ + gcc_builtin_headers_ia32-4.inc \ + gcc_builtin_headers_ia32.inc \ + gcc_builtin_headers_math.inc \ + gcc_builtin_headers_mem_string.inc \ + gcc_builtin_headers_mips.inc \ + gcc_builtin_headers_omp.inc \ + gcc_builtin_headers_power.inc \ + gcc_builtin_headers_tm.inc \ + gcc_builtin_headers_types.inc \ + gcc_builtin_headers_ubsan.inc ############################################################################### diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp index 401ff940ce6..abcf362a943 100644 --- a/src/ansi-c/ansi_c_internal_additions.cpp +++ b/src/ansi-c/ansi_c_internal_additions.cpp @@ -10,6 +10,11 @@ Author: Daniel Kroening, kroening@kroening.com #include +const char gcc_builtin_headers_types[]= +"# 1 \"gcc_builtin_headers_types.h\"\n" +#include "gcc_builtin_headers_types.inc" +; // NOLINT(whitespace/semicolon) + const char gcc_builtin_headers_generic[]= "# 1 \"gcc_builtin_headers_generic.h\"\n" #include "gcc_builtin_headers_generic.inc" @@ -89,6 +94,10 @@ const char clang_builtin_headers[]= #include "clang_builtin_headers.inc" ; // NOLINT(whitespace/semicolon) +const char windows_builtin_headers[]= + "int __noop();\n" + "int __assume(int);\n"; + static std::string architecture_string(const std::string &value, const char *s) { return std::string("const char *__CPROVER_architecture_")+ @@ -257,13 +266,7 @@ void ansi_c_internal_additions(std::string &code) config.ansi_c.mode==configt::ansi_ct::flavourt::APPLE || config.ansi_c.mode==configt::ansi_ct::flavourt::ARM) { - code+=gcc_builtin_headers_generic; - code+=gcc_builtin_headers_math; - code+=gcc_builtin_headers_mem_string; - code+=gcc_builtin_headers_omp; - code+=gcc_builtin_headers_tm; - code+=gcc_builtin_headers_ubsan; - code+=clang_builtin_headers; + code+=gcc_builtin_headers_types; // there are many more, e.g., look at // https://developer.apple.com/library/mac/#documentation/developertools/gcc-4.0.1/gcc/Target-Builtins.html @@ -274,37 +277,6 @@ void ansi_c_internal_additions(std::string &code) { if(config.ansi_c.mode==configt::ansi_ct::flavourt::APPLE) code+="typedef double __float128;\n"; // clang doesn't do __float128 - - code+=gcc_builtin_headers_ia32; - code+=gcc_builtin_headers_ia32_2; - code+=gcc_builtin_headers_ia32_3; - code+=gcc_builtin_headers_ia32_4; - } - else if(config.ansi_c.arch=="arm64" || - config.ansi_c.arch=="armel" || - config.ansi_c.arch=="armhf" || - config.ansi_c.arch=="arm") - { - code+=gcc_builtin_headers_arm; - } - else if(config.ansi_c.arch=="alpha") - { - code+=gcc_builtin_headers_alpha; - } - else if(config.ansi_c.arch=="mips64el" || - config.ansi_c.arch=="mipsn32el" || - config.ansi_c.arch=="mipsel" || - config.ansi_c.arch=="mips64" || - config.ansi_c.arch=="mipsn32" || - config.ansi_c.arch=="mips") - { - code+=gcc_builtin_headers_mips; - } - else if(config.ansi_c.arch=="powerpc" || - config.ansi_c.arch=="ppc64" || - config.ansi_c.arch=="ppc64le") - { - code+=gcc_builtin_headers_power; } // On 64-bit systems, gcc has typedefs diff --git a/src/ansi-c/ansi_c_internal_additions.h b/src/ansi-c/ansi_c_internal_additions.h index 7cdcce2e104..c8c5edaa446 100644 --- a/src/ansi-c/ansi_c_internal_additions.h +++ b/src/ansi-c/ansi_c_internal_additions.h @@ -32,5 +32,6 @@ extern const char gcc_builtin_headers_mips[]; extern const char gcc_builtin_headers_power[]; extern const char arm_builtin_headers[]; extern const char cw_builtin_headers[]; +extern const char windows_builtin_headers[]; #endif // CPROVER_ANSI_C_ANSI_C_INTERNAL_ADDITIONS_H diff --git a/src/ansi-c/builtin_factory.cpp b/src/ansi-c/builtin_factory.cpp index 534a774b87e..c52d05879b0 100644 --- a/src/ansi-c/builtin_factory.cpp +++ b/src/ansi-c/builtin_factory.cpp @@ -12,14 +12,12 @@ Author: Daniel Kroening, kroening@kroening.com #include "ansi_c_parser.h" #include "ansi_c_typecheck.h" +#include + #include #include #include -const char windows_headers[]= - "int __noop();\n" - "int __assume(int);\n"; - //! Advance to the next line static const char *next_line(const char *line) { @@ -93,7 +91,8 @@ static bool convert( symbol_tablet new_symbol_table; - // very recursive! + // this is recursive -- builtin_factory is called + // from the typechecker if(ansi_c_typecheck( ansi_c_parser.parse_tree, new_symbol_table, @@ -137,33 +136,96 @@ bool builtin_factory( std::string code; ansi_c_internal_additions(code); s << code; - - if(find_pattern(pattern, gcc_builtin_headers_generic, s)) - return convert(identifier, s, symbol_table, mh); - if(find_pattern(pattern, gcc_builtin_headers_mem_string, s)) - return convert(identifier, s, symbol_table, mh); + // this is Visual C/C++ only + if(config.ansi_c.os==configt::ansi_ct::ost::OS_WIN) + { + if(find_pattern(pattern, windows_builtin_headers, s)) + return convert(identifier, s, symbol_table, mh); + } + + // ARM stuff + if(config.ansi_c.mode==configt::ansi_ct::flavourt::ARM) + { + if(find_pattern(pattern, arm_builtin_headers, s)) + return convert(identifier, s, symbol_table, mh); + } + + // CW stuff + if(config.ansi_c.mode==configt::ansi_ct::flavourt::CODEWARRIOR) + { + if(find_pattern(pattern, cw_builtin_headers, s)) + return convert(identifier, s, symbol_table, mh); + } + + // GCC junk stuff, also for CLANG and ARM + if(config.ansi_c.mode==configt::ansi_ct::flavourt::GCC || + config.ansi_c.mode==configt::ansi_ct::flavourt::APPLE || + config.ansi_c.mode==configt::ansi_ct::flavourt::ARM) + { + if(find_pattern(pattern, gcc_builtin_headers_generic, s)) + return convert(identifier, s, symbol_table, mh); + + if(find_pattern(pattern, gcc_builtin_headers_math, s)) + return convert(identifier, s, symbol_table, mh); + + if(find_pattern(pattern, gcc_builtin_headers_mem_string, s)) + return convert(identifier, s, symbol_table, mh); + + if(find_pattern(pattern, gcc_builtin_headers_omp, s)) + return convert(identifier, s, symbol_table, mh); - if(find_pattern(pattern, gcc_builtin_headers_omp, s)) - return convert(identifier, s, symbol_table, mh); + if(find_pattern(pattern, gcc_builtin_headers_tm, s)) + return convert(identifier, s, symbol_table, mh); - if(find_pattern(pattern, gcc_builtin_headers_tm, s)) - return convert(identifier, s, symbol_table, mh); + if(find_pattern(pattern, gcc_builtin_headers_ubsan, s)) + return convert(identifier, s, symbol_table, mh); - if(find_pattern(pattern, gcc_builtin_headers_ubsan, s)) - return convert(identifier, s, symbol_table, mh); + if(find_pattern(pattern, clang_builtin_headers, s)) + return convert(identifier, s, symbol_table, mh); - if(find_pattern(pattern, gcc_builtin_headers_ia32, s)) - return convert(identifier, s, symbol_table, mh); + if(config.ansi_c.arch=="i386" || + config.ansi_c.arch=="x86_64" || + config.ansi_c.arch=="x32") + { + if(find_pattern(pattern, gcc_builtin_headers_ia32, s)) + return convert(identifier, s, symbol_table, mh); - if(find_pattern(pattern, gcc_builtin_headers_ia32_2, s)) - return convert(identifier, s, symbol_table, mh); + if(find_pattern(pattern, gcc_builtin_headers_ia32_2, s)) + return convert(identifier, s, symbol_table, mh); - if(find_pattern(pattern, gcc_builtin_headers_ia32_3, s)) - return convert(identifier, s, symbol_table, mh); + if(find_pattern(pattern, gcc_builtin_headers_ia32_3, s)) + return convert(identifier, s, symbol_table, mh); - if(find_pattern(pattern, gcc_builtin_headers_ia32_4, s)) - return convert(identifier, s, symbol_table, mh); + if(find_pattern(pattern, gcc_builtin_headers_ia32_4, s)) + return convert(identifier, s, symbol_table, mh); + } + else if(config.ansi_c.arch=="arm64" || + config.ansi_c.arch=="armel" || + config.ansi_c.arch=="armhf" || + config.ansi_c.arch=="arm") + { + if(find_pattern(pattern, gcc_builtin_headers_arm, s)) + return convert(identifier, s, symbol_table, mh); + } + else if(config.ansi_c.arch=="mips64el" || + config.ansi_c.arch=="mipsn32el" || + config.ansi_c.arch=="mipsel" || + config.ansi_c.arch=="mips64" || + config.ansi_c.arch=="mipsn32" || + config.ansi_c.arch=="mips") + { + if(find_pattern(pattern, gcc_builtin_headers_mips, s)) + return convert(identifier, s, symbol_table, mh); + } + else if(config.ansi_c.arch=="powerpc" || + config.ansi_c.arch=="ppc64" || + config.ansi_c.arch=="ppc64le") + { + if(find_pattern(pattern, gcc_builtin_headers_power, s)) + return convert(identifier, s, symbol_table, mh); + } + } return true; } diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 6c7b3ddbcf5..be300c00258 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -26,6 +26,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include "builtin_factory.h" #include "c_typecast.h" #include "c_qualifiers.h" #include "anonymous_member.h" @@ -1913,35 +1914,45 @@ void c_typecheck_baset::typecheck_side_effect_function_call( if(symbol_table.symbols.find(identifier)==symbol_table.symbols.end()) { - // This is an undeclared function. Let's just add it. - // We do a bit of return-type guessing, but just a bit. - typet return_type=signed_int_type(); - - // The following isn't really right and sound, but there - // are too many idiots out there who use malloc and the like - // without the right header file. - if(identifier=="malloc" || - identifier=="realloc" || - identifier=="reallocf" || - identifier=="valloc") - return_type=pointer_type(void_type()); // void * - - symbolt new_symbol; - - new_symbol.name=identifier; - new_symbol.base_name=identifier; - new_symbol.location=expr.source_location(); - new_symbol.type=code_typet(); - new_symbol.type.set(ID_C_incomplete, true); - new_symbol.type.add(ID_return_type)=return_type; - - // TODO: should also guess some argument types - - symbolt *symbol_ptr; - move_symbol(new_symbol, symbol_ptr); - - warning().source_location=f_op.find_source_location(); - warning() << "function `" << identifier << "' is not declared" << eom; + // This is an undeclared function. + // Is this a builtin? + if(!builtin_factory(identifier, symbol_table, get_message_handler())) + { + // yes, it's a builtin + } + else + { + // This is an undeclared function that's not a builtin. + // Let's just add it. + // We do a bit of return-type guessing, but just a bit. + typet return_type=signed_int_type(); + + // The following isn't really right and sound, but there + // are too many idiots out there who use malloc and the like + // without the right header file. + if(identifier=="malloc" || + identifier=="realloc" || + identifier=="reallocf" || + identifier=="valloc") + return_type=pointer_type(void_type()); // void * + + symbolt new_symbol; + + new_symbol.name=identifier; + new_symbol.base_name=identifier; + new_symbol.location=expr.source_location(); + new_symbol.type=code_typet(); + new_symbol.type.set(ID_C_incomplete, true); + new_symbol.type.add(ID_return_type)=return_type; + + // TODO: should also guess some argument types + + symbolt *symbol_ptr; + move_symbol(new_symbol, symbol_ptr); + + warning().source_location=f_op.find_source_location(); + warning() << "function `" << identifier << "' is not declared" << eom; + } } } diff --git a/src/ansi-c/clang_builtin_headers.h b/src/ansi-c/clang_builtin_headers.h index 742cba71dbf..2b4b269ca68 100644 --- a/src/ansi-c/clang_builtin_headers.h +++ b/src/ansi-c/clang_builtin_headers.h @@ -1,5 +1,3 @@ -typedef float __gcc_v4sf __attribute__ ((__vector_size__ (16))); - __gcc_v4sf __builtin_shufflevector(__gcc_v4sf, __gcc_v4sf, ...); int __builtin_flt_rounds(void); diff --git a/src/ansi-c/gcc_builtin_headers_generic.h b/src/ansi-c/gcc_builtin_headers_generic.h index 17d997b8deb..908c8f61e3b 100644 --- a/src/ansi-c/gcc_builtin_headers_generic.h +++ b/src/ansi-c/gcc_builtin_headers_generic.h @@ -1,6 +1,3 @@ -typedef void ** __builtin_va_list; -typedef void ** __builtin_ms_va_list; - // stdarg void* __builtin_apply_args(); void __builtin_ms_va_end(void *ap); @@ -105,35 +102,3 @@ void __builtin_return(void*); void* __builtin_saveregs(); int __builtin_setjmp(void*); void __builtin_update_setjmp_buf(void*); - - -typedef int __gcc_m64 __attribute__ ((__vector_size__ (8), __may_alias__)); - -typedef char __gcc_v8qi __attribute__ ((__vector_size__ (8))); -typedef char __gcc_v16qi __attribute__ ((__vector_size__ (16))); -typedef char __gcc_v32qi __attribute__ ((__vector_size__ (32))); -typedef char __gcc_v64qi __attribute__ ((__vector_size__ (64))); -typedef int __gcc_v2si __attribute__ ((__vector_size__ (8))); -typedef int __gcc_v4si __attribute__ ((__vector_size__ (16))); -typedef int __gcc_v8si __attribute__ ((__vector_size__ (32))); -typedef int __gcc_v16si __attribute__ ((__vector_size__ (64))); -typedef short __gcc_v4hi __attribute__ ((__vector_size__ (8))); -typedef short __gcc_v8hi __attribute__ ((__vector_size__ (16))); -typedef short __gcc_v16hi __attribute__ ((__vector_size__ (32))); -typedef short __gcc_v32hi __attribute__ ((__vector_size__ (64))); -typedef float __gcc_v2sf __attribute__ ((__vector_size__ (8))); -typedef float __gcc_v4sf __attribute__ ((__vector_size__ (16))); -typedef float __gcc_v8sf __attribute__ ((__vector_size__ (32))); -typedef float __gcc_v16sf __attribute__ ((__vector_size__ (64))); -typedef double __gcc_v2df __attribute__ ((__vector_size__ (16))); -typedef double __gcc_v4df __attribute__ ((__vector_size__ (32))); -typedef double __gcc_v8df __attribute__ ((__vector_size__ (64))); -typedef long long __gcc_v1di __attribute__ ((__vector_size__ (8))); -typedef long long __gcc_v2di __attribute__ ((__vector_size__ (16))); -typedef long long __gcc_v4di __attribute__ ((__vector_size__ (32))); -typedef long long __gcc_v8di __attribute__ ((__vector_size__ (64))); -typedef unsigned long long __gcc_di; - -enum __gcc_atomic_memmodels { - __ATOMIC_RELAXED, __ATOMIC_CONSUME, __ATOMIC_ACQUIRE, __ATOMIC_RELEASE, __ATOMIC_ACQ_REL, __ATOMIC_SEQ_CST -}; diff --git a/src/ansi-c/gcc_builtin_headers_types.h b/src/ansi-c/gcc_builtin_headers_types.h new file mode 100644 index 00000000000..6278d277440 --- /dev/null +++ b/src/ansi-c/gcc_builtin_headers_types.h @@ -0,0 +1,33 @@ +typedef void ** __builtin_va_list; +typedef void ** __builtin_ms_va_list; + +typedef int __gcc_m64 __attribute__ ((__vector_size__ (8), __may_alias__)); + +typedef char __gcc_v8qi __attribute__ ((__vector_size__ (8))); +typedef char __gcc_v16qi __attribute__ ((__vector_size__ (16))); +typedef char __gcc_v32qi __attribute__ ((__vector_size__ (32))); +typedef char __gcc_v64qi __attribute__ ((__vector_size__ (64))); +typedef int __gcc_v2si __attribute__ ((__vector_size__ (8))); +typedef int __gcc_v4si __attribute__ ((__vector_size__ (16))); +typedef int __gcc_v8si __attribute__ ((__vector_size__ (32))); +typedef int __gcc_v16si __attribute__ ((__vector_size__ (64))); +typedef short __gcc_v4hi __attribute__ ((__vector_size__ (8))); +typedef short __gcc_v8hi __attribute__ ((__vector_size__ (16))); +typedef short __gcc_v16hi __attribute__ ((__vector_size__ (32))); +typedef short __gcc_v32hi __attribute__ ((__vector_size__ (64))); +typedef float __gcc_v2sf __attribute__ ((__vector_size__ (8))); +typedef float __gcc_v4sf __attribute__ ((__vector_size__ (16))); +typedef float __gcc_v8sf __attribute__ ((__vector_size__ (32))); +typedef float __gcc_v16sf __attribute__ ((__vector_size__ (64))); +typedef double __gcc_v2df __attribute__ ((__vector_size__ (16))); +typedef double __gcc_v4df __attribute__ ((__vector_size__ (32))); +typedef double __gcc_v8df __attribute__ ((__vector_size__ (64))); +typedef long long __gcc_v1di __attribute__ ((__vector_size__ (8))); +typedef long long __gcc_v2di __attribute__ ((__vector_size__ (16))); +typedef long long __gcc_v4di __attribute__ ((__vector_size__ (32))); +typedef long long __gcc_v8di __attribute__ ((__vector_size__ (64))); +typedef unsigned long long __gcc_di; + +enum __gcc_atomic_memmodels { + __ATOMIC_RELAXED, __ATOMIC_CONSUME, __ATOMIC_ACQUIRE, __ATOMIC_RELEASE, __ATOMIC_ACQ_REL, __ATOMIC_SEQ_CST +}; From 80ee0b14d3e1d062be730183368dfb8d5fa85d39 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 5 Mar 2018 21:35:48 +0000 Subject: [PATCH 4/6] pass type definitions to the C++ front-end --- src/ansi-c/ansi_c_internal_additions.h | 1 + src/cpp/cpp_internal_additions.cpp | 1 + 2 files changed, 2 insertions(+) diff --git a/src/ansi-c/ansi_c_internal_additions.h b/src/ansi-c/ansi_c_internal_additions.h index c8c5edaa446..10e7c8e144d 100644 --- a/src/ansi-c/ansi_c_internal_additions.h +++ b/src/ansi-c/ansi_c_internal_additions.h @@ -16,6 +16,7 @@ void ansi_c_internal_additions(std::string &code); void ansi_c_architecture_strings(std::string &code); extern const char clang_builtin_headers[]; +extern const char gcc_builtin_headers_types[]; 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/cpp/cpp_internal_additions.cpp b/src/cpp/cpp_internal_additions.cpp index 0417ed9c3e9..19260f6ac24 100644 --- a/src/cpp/cpp_internal_additions.cpp +++ b/src/cpp/cpp_internal_additions.cpp @@ -112,6 +112,7 @@ void cpp_internal_additions(std::ostream &out) config.ansi_c.mode==configt::ansi_ct::flavourt::ARM) { out << "extern \"C\" {" << '\n'; + out << c2cpp(gcc_builtin_headers_types); out << c2cpp(gcc_builtin_headers_generic); out << c2cpp(gcc_builtin_headers_math); out << c2cpp(gcc_builtin_headers_mem_string); From 17d98979994b8ba7588a172eebb5443cd3b198c4 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 6 Mar 2018 14:44:58 +0000 Subject: [PATCH 5/6] switch to C++ version of find_pattern --- src/ansi-c/builtin_factory.cpp | 45 ++++++---------------------------- 1 file changed, 8 insertions(+), 37 deletions(-) diff --git a/src/ansi-c/builtin_factory.cpp b/src/ansi-c/builtin_factory.cpp index c52d05879b0..cd839a46223 100644 --- a/src/ansi-c/builtin_factory.cpp +++ b/src/ansi-c/builtin_factory.cpp @@ -13,55 +13,26 @@ Author: Daniel Kroening, kroening@kroening.com #include "ansi_c_typecheck.h" #include +#include -#include #include #include -//! Advance to the next line -static const char *next_line(const char *line) -{ - const char *end=strchr(line, '\n'); - - if(end==NULL) - return strchr(line, 0); - else - return end+1; -} - -//! Look for given pattern in given string. -//! Add line with pattern to 'out' if found. -//! \return 'true' if found static bool find_pattern( const std::string &pattern, const char *header_file, std::ostream &out) { - // read line-by-line - const char *line, *line_end; - - for(line=header_file; *line!=0; line=line_end) + std::istringstream hdr(header_file); + std::string line; + while(std::getline(hdr, line)) { - line_end=next_line(line); - - // skip spaces - while(*line==' ') - line++; - - if(line[0]=='/' && line[1]=='/') // comment + line = strip_string(line); + if(has_prefix(line, "//") || line.find(pattern) == std::string::npos) continue; - for(const char *p=line; p Date: Tue, 6 Mar 2018 15:10:39 +0000 Subject: [PATCH 6/6] Makefile: use a variable for all those generated .inc files --- src/ansi-c/Makefile | 51 +++++++++------------------------------------ 1 file changed, 10 insertions(+), 41 deletions(-) diff --git a/src/ansi-c/Makefile b/src/ansi-c/Makefile index 5b3383a3ab2..97519b2a4df 100644 --- a/src/ansi-c/Makefile +++ b/src/ansi-c/Makefile @@ -44,11 +44,7 @@ INCLUDES= -I .. include ../config.inc include ../common -CLEANFILES = ansi-c$(LIBEXT) \ - ansi_c_y.tab.h ansi_c_y.tab.cpp ansi_c_lex.yy.cpp ansi_c_y.tab.cpp.output \ - ansi_c_y.output \ - library/converter$(EXEEXT) cprover_library.inc \ - file_converter$(EXEEXT) library_check \ +BUILTIN_FILES = \ arm_builtin_headers.inc \ clang_builtin_headers.inc \ cw_builtin_headers.inc \ @@ -68,6 +64,13 @@ CLEANFILES = ansi-c$(LIBEXT) \ gcc_builtin_headers_types.inc \ gcc_builtin_headers_ubsan.inc +CLEANFILES = ansi-c$(LIBEXT) \ + ansi_c_y.tab.h ansi_c_y.tab.cpp ansi_c_lex.yy.cpp ansi_c_y.tab.cpp.output \ + ansi_c_y.output \ + library/converter$(EXEEXT) cprover_library.inc \ + file_converter$(EXEEXT) library_check \ + $(BUILTIN_FILES) + all: ansi-c$(LIBEXT) ############################################################################### @@ -112,46 +115,12 @@ cprover_library.inc: library/converter$(EXEEXT) library/*.c cprover_library.cpp: cprover_library.inc -ansi_c_internal_additions$(OBJEXT): arm_builtin_headers.inc -ansi_c_internal_additions$(OBJEXT): clang_builtin_headers.inc -ansi_c_internal_additions$(OBJEXT): cw_builtin_headers.inc -ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_alpha.inc -ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_arm.inc -ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_generic.inc -ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_ia32-2.inc -ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_ia32-3.inc -ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_ia32-4.inc -ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_ia32.inc -ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_math.inc -ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_mem_string.inc -ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_mips.inc -ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_omp.inc -ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_power.inc -ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_tm.inc -ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_types.inc -ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_ubsan.inc +ansi_c_internal_additions$(OBJEXT): $(BUILTIN_FILES) generated_files: \ ansi_c_y.tab.cpp ansi_c_lex.yy.cpp ansi_c_y.tab.h \ - arm_builtin_headers.inc \ - clang_builtin_headers.inc \ cprover_library.inc \ - cw_builtin_headers.inc \ - gcc_builtin_headers_alpha.inc \ - gcc_builtin_headers_arm.inc \ - gcc_builtin_headers_generic.inc \ - gcc_builtin_headers_ia32-2.inc \ - gcc_builtin_headers_ia32-3.inc \ - gcc_builtin_headers_ia32-4.inc \ - gcc_builtin_headers_ia32.inc \ - gcc_builtin_headers_math.inc \ - gcc_builtin_headers_mem_string.inc \ - gcc_builtin_headers_mips.inc \ - gcc_builtin_headers_omp.inc \ - gcc_builtin_headers_power.inc \ - gcc_builtin_headers_tm.inc \ - gcc_builtin_headers_types.inc \ - gcc_builtin_headers_ubsan.inc + $(BUILTIN_FILES) ###############################################################################