diff --git a/appveyor.yml b/appveyor.yml index 3a7c2d5c363..2efea4e75c2 100644 --- a/appveyor.yml +++ b/appveyor.yml @@ -109,6 +109,7 @@ test_script: rmdir /s /q cbmc-java\classpath1 rmdir /s /q cbmc-java\jar-file3 rmdir /s /q cbmc-java\tableswitch2 + rmdir /s /q goto-gcc rmdir /s /q goto-instrument\slice08 make test diff --git a/regression/Makefile b/regression/Makefile index 3315fb90a6d..ff713b428e4 100644 --- a/regression/Makefile +++ b/regression/Makefile @@ -6,6 +6,7 @@ DIRS = ansi-c \ cbmc-cover \ goto-analyzer \ goto-diff \ + goto-gcc \ goto-instrument \ goto-instrument-typedef \ invariants \ @@ -14,9 +15,14 @@ DIRS = ansi-c \ test-script \ # Empty last line - +# Check for the existence of $dir. Tests under goto-gcc cannot be run on +# Windows, so appveyor.yml unlinks the entire directory under Windows. test: - $(foreach var,$(DIRS), $(MAKE) -C $(var) test || exit 1;) + @for dir in $(DIRS); do \ + if [ -d "$$dir" ]; then \ + $(MAKE) -C "$$dir" test || exit 1; \ + fi; \ + done; clean: @for dir in *; do \ diff --git a/regression/goto-gcc/Makefile b/regression/goto-gcc/Makefile new file mode 100644 index 00000000000..c845d7e2e2a --- /dev/null +++ b/regression/goto-gcc/Makefile @@ -0,0 +1,27 @@ +default: tests.log + +test: + -@ln -s goto-cc ../../src/goto-cc/goto-gcc + @if ! ../test.pl -c ../../../src/goto-cc/goto-gcc ; then \ + ../failed-tests-printer.pl ; \ + exit 1 ; \ + fi + +tests.log: ../test.pl + -@ln -s goto-cc ../../src/goto-cc/goto-gcc + @if ! ../test.pl -c ../../../src/goto-cc/goto-gcc ; then \ + ../failed-tests-printer.pl ; \ + exit 1 ; \ + fi + +show: + @for dir in *; do \ + if [ -d "$$dir" ]; then \ + vim -o "$$dir/*.c" "$$dir/*.out"; \ + fi; \ + done; + +clean: + find -name '*.out' -execdir $(RM) '{}' \; + find -name '*.gb' -execdir $(RM) '{}' \; + $(RM) tests.log diff --git a/regression/goto-gcc/ignore_cprover_macros/main.c b/regression/goto-gcc/ignore_cprover_macros/main.c new file mode 100644 index 00000000000..864f7dac484 --- /dev/null +++ b/regression/goto-gcc/ignore_cprover_macros/main.c @@ -0,0 +1,6 @@ +int main() +{ + unsigned x; + __CPROVER_assume(x); + __CPROVER_assert(x, ""); +} diff --git a/regression/goto-gcc/ignore_cprover_macros/test.desc b/regression/goto-gcc/ignore_cprover_macros/test.desc new file mode 100644 index 00000000000..c542c24273d --- /dev/null +++ b/regression/goto-gcc/ignore_cprover_macros/test.desc @@ -0,0 +1,13 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +^CONVERSION ERROR$ +-- +-- +goto-gcc must define out all CPROVER macros that are used in the +codebase. This test succeeds iff GCC doesn't see the CPROVER macros in +the test file. diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp index c54b6b60f6b..71f0d81160e 100644 --- a/src/goto-cc/compile.cpp +++ b/src/goto-cc/compile.cpp @@ -379,7 +379,7 @@ bool compilet::link() output_file_executable, symbol_table, compiled_functions)) return true; - return false; + return add_written_cprover_symbols(symbol_table); } /// parses source files and writes object files, or keeps the symbols in the @@ -430,6 +430,9 @@ bool compilet::compile() if(write_object_file(cfn, symbol_table, compiled_functions)) return true; + if(add_written_cprover_symbols(symbol_table)) + return true; + symbol_table.clear(); // clean symbol table for next source file. compiled_functions.clear(); } @@ -616,6 +619,7 @@ bool compilet::write_bin_object_file( << "; " << cnt << " have a body." << eom; outfile.close(); + wrote_object=true; return false; } @@ -650,6 +654,7 @@ compilet::compilet(cmdlinet &_cmdline, ui_message_handlert &mh, bool Werror): { mode=COMPILE_LINK_EXECUTABLE; echo_file_name=false; + wrote_object=false; working_directory=get_current_working_directory(); } @@ -724,3 +729,28 @@ void compilet::convert_symbols(goto_functionst &dest) } } } + +bool compilet::add_written_cprover_symbols(const symbol_tablet &symbol_table) +{ + for(const auto &pair : symbol_table.symbols) + { + const irep_idt &name=pair.second.name; + const typet &new_type=pair.second.type; + if(!(has_prefix(id2string(name), CPROVER_PREFIX) && new_type.id()==ID_code)) + continue; + + bool inserted; + std::map::iterator old; + std::tie(old, inserted)=written_macros.insert({name, pair.second}); + + if(!inserted && old->second.type!=new_type) + { + error() << "Incompatible CPROVER macro symbol types:" << eom + << old->second.type.pretty() << "(at " << old->second.location + << ")" << eom << "and" << eom << new_type.pretty() + << "(at " << pair.second.location << ")" << eom; + return true; + } + } + return false; +} diff --git a/src/goto-cc/compile.h b/src/goto-cc/compile.h index d0a521769c1..b0c61d137a3 100644 --- a/src/goto-cc/compile.h +++ b/src/goto-cc/compile.h @@ -72,6 +72,23 @@ class compilet:public language_uit const symbol_tablet &, goto_functionst &); + /// \brief Has this compiler written any object files? + bool wrote_object_files() const { return wrote_object; } + + /// \brief `__CPROVER_...` macros written to object files and their arities + /// + /// \return A mapping from every `__CPROVER` macro that this compiler + /// wrote to one or more object files, to how many parameters that + /// `__CPROVER` macro has. + void cprover_macro_arities(std::map &cprover_macros) const + { + PRECONDITION(wrote_object); + for(const auto &pair : written_macros) + cprover_macros.insert({pair.first, + to_code_type(pair.second.type).parameters().size()}); + } + protected: cmdlinet &cmdline; bool warning_is_fatal; @@ -81,6 +98,16 @@ class compilet:public language_uit void add_compiler_specific_defines(class configt &config) const; void convert_symbols(goto_functionst &dest); + + bool add_written_cprover_symbols(const symbol_tablet &symbol_table); + std::map written_macros; + + // clients must only call add_written_cprover_symbols() if an object + // file has been written. The case where an object file was written + // but there were no __CPROVER symbols in the goto-program is distinct + // from the case where the user forgot to write an object file before + // calling add_written_cprover_symbols(). + bool wrote_object; }; #endif // CPROVER_GOTO_CC_COMPILE_H diff --git a/src/goto-cc/gcc_mode.cpp b/src/goto-cc/gcc_mode.cpp index db33ac5b194..231baff6eb5 100644 --- a/src/goto-cc/gcc_mode.cpp +++ b/src/goto-cc/gcc_mode.cpp @@ -19,10 +19,13 @@ Author: CM Wintersteiger, 2006 #include #endif +#include #include #include #include #include +#include +#include #include #include @@ -337,10 +340,16 @@ int gcc_modet::doit() std::cout << "gcc version 3.4.4 (goto-cc " CBMC_VERSION ")\n"; } + compilet compiler(cmdline, + gcc_message_handler, + cmdline.isset("Werror") && + cmdline.isset("Wextra") && + !cmdline.isset("Wno-error")); + if(cmdline.isset("version")) { if(produce_hybrid_binary) - return run_gcc(); + return run_gcc(compiler); std::cout << '\n' << "Copyright (C) 2006-2014 Daniel Kroening, Christoph Wintersteiger\n" << @@ -354,7 +363,7 @@ int gcc_modet::doit() if(cmdline.isset("dumpversion")) { if(produce_hybrid_binary) - return run_gcc(); + return run_gcc(compiler); std::cout << "3.4.4\n"; return EX_OK; @@ -390,6 +399,24 @@ int gcc_modet::doit() debug() << "GCC mode" << eom; } + // determine actions to be undertaken + if(act_as_ld) + compiler.mode=compilet::LINK_LIBRARY; + else if(cmdline.isset('S')) + compiler.mode=compilet::ASSEMBLE_ONLY; + else if(cmdline.isset('c')) + compiler.mode=compilet::COMPILE_ONLY; + else if(cmdline.isset('E')) + { + compiler.mode=compilet::PREPROCESS_ONLY; + UNREACHABLE; + } + else if(cmdline.isset("shared") || + cmdline.isset('r')) // really not well documented + compiler.mode=compilet::COMPILE_LINK; + else + compiler.mode=compilet::COMPILE_LINK_EXECUTABLE; + // In gcc mode, we have just pass on to gcc to handle the following: // * if -M or -MM is given, we do dependencies only // * preprocessing (-E) @@ -402,7 +429,7 @@ int gcc_modet::doit() cmdline.isset("MM") || cmdline.isset('E') || !cmdline.have_infile_arg()) - return run_gcc(); // exit! + return run_gcc(compiler); // exit! // get configuration config.set(cmdline); @@ -489,30 +516,6 @@ int gcc_modet::doit() if(cmdline.isset("fshort-double")) config.ansi_c.double_width=config.ansi_c.single_width; - // determine actions to be undertaken - compilet compiler(cmdline, - gcc_message_handler, - cmdline.isset("Werror") && - cmdline.isset("Wextra") && - !cmdline.isset("Wno-error")); - - if(act_as_ld) - compiler.mode=compilet::LINK_LIBRARY; - else if(cmdline.isset('S')) - compiler.mode=compilet::ASSEMBLE_ONLY; - else if(cmdline.isset('c')) - compiler.mode=compilet::COMPILE_ONLY; - else if(cmdline.isset('E')) - { - compiler.mode=compilet::PREPROCESS_ONLY; - UNREACHABLE; - } - else if(cmdline.isset("shared") || - cmdline.isset('r')) // really not well documented - compiler.mode=compilet::COMPILE_LINK; - else - compiler.mode=compilet::COMPILE_LINK_EXECUTABLE; - switch(compiler.mode) { case compilet::LINK_LIBRARY: @@ -695,10 +698,10 @@ int gcc_modet::doit() if(compiler.source_files.empty() && compiler.object_files.empty()) - return run_gcc(); // exit! + return run_gcc(compiler); // exit! if(compiler.mode==compilet::ASSEMBLE_ONLY) - return asm_output(act_as_bcc, compiler.source_files); + return asm_output(act_as_bcc, compiler.source_files, compiler); // do all the rest if(compiler.doit()) @@ -707,7 +710,7 @@ int gcc_modet::doit() // We can generate hybrid ELF and Mach-O binaries // containing both executable machine code and the goto-binary. if(produce_hybrid_binary && !act_as_bcc) - return gcc_hybrid_binary(); + return gcc_hybrid_binary(compiler); return EX_OK; } @@ -791,8 +794,7 @@ int gcc_modet::preprocess( return run(new_argv[0], new_argv, cmdline.stdin_file, stdout_file); } -/// run gcc or clang with original command line -int gcc_modet::run_gcc() +int gcc_modet::run_gcc(const compilet &compiler) { PRECONDITION(!cmdline.parsed_argv.empty()); @@ -802,6 +804,28 @@ int gcc_modet::run_gcc() for(const auto &a : cmdline.parsed_argv) new_argv.push_back(a.arg); + if(compiler.wrote_object_files()) + { + // Undefine all __CPROVER macros for the system compiler + std::map arities; + compiler.cprover_macro_arities(arities); + for(const auto &pair : arities) + { + std::ostringstream addition; + addition << "-D" << id2string(pair.first) << "("; + std::vector params(pair.second); + std::iota(params.begin(), params.end(), 'a'); + for(std::vector::iterator it=params.begin(); it!=params.end(); ++it) + { + addition << *it; + if(it+1!=params.end()) + addition << ","; + } + addition << ")= "; + new_argv.push_back(addition.str()); + } + } + // overwrite argv[0] new_argv[0]=native_tool_name; @@ -813,7 +837,7 @@ int gcc_modet::run_gcc() return run(new_argv[0], new_argv, cmdline.stdin_file, ""); } -int gcc_modet::gcc_hybrid_binary() +int gcc_modet::gcc_hybrid_binary(const compilet &compiler) { { bool have_files=false; @@ -861,7 +885,7 @@ int gcc_modet::gcc_hybrid_binary() if(output_files.empty() || (output_files.size()==1 && output_files.front()=="/dev/null")) - return run_gcc(); + return EX_OK; debug() << "Running " << native_tool_name << " to generate hybrid binary" << eom; @@ -893,7 +917,7 @@ int gcc_modet::gcc_hybrid_binary() } objcopy_cmd+="objcopy"; - int result=run_gcc(); + int result=run_gcc(compiler); // merge output from gcc with goto-binaries // using objcopy, or do cleanup if an earlier call failed @@ -975,7 +999,8 @@ int gcc_modet::gcc_hybrid_binary() int gcc_modet::asm_output( bool act_as_bcc, - const std::list &preprocessed_source_files) + const std::list &preprocessed_source_files, + const compilet &compiler) { { bool have_files=false; @@ -996,7 +1021,7 @@ int gcc_modet::asm_output( debug() << "Running " << native_tool_name << " to generate native asm output" << eom; - int result=run_gcc(); + int result=run_gcc(compiler); if(result!=0) // native tool failed return result; diff --git a/src/goto-cc/gcc_mode.h b/src/goto-cc/gcc_mode.h index cd4f1cb1a56..497546ff2a0 100644 --- a/src/goto-cc/gcc_mode.h +++ b/src/goto-cc/gcc_mode.h @@ -18,6 +18,8 @@ Date: June 2006 #include "goto_cc_mode.h" +class compilet; + class gcc_modet:public goto_cc_modet { public: @@ -45,13 +47,15 @@ class gcc_modet:public goto_cc_modet const std::string &dest, bool act_as_bcc); - int run_gcc(); // call gcc with original command line + /// \brief call gcc with original command line + int run_gcc(const compilet &compiler); - int gcc_hybrid_binary(); + int gcc_hybrid_binary(const compilet &compiler); int asm_output( bool act_as_bcc, - const std::list &preprocessed_source_files); + const std::list &preprocessed_source_files, + const compilet &compiler); static bool needs_preprocessing(const std::string &); };