From 3531be628ace5ed2efc36dc49bd8b0acaed030e1 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 22 May 2019 12:50:48 +0000 Subject: [PATCH 1/2] Do not pass the compiler object to linker-script merging There is no need to access the goto model stored in compilet as we read the goto binary that compilet wrote anyway. This avoids tight coupling and enables removing public class members from compilet. --- scripts/expected_doxygen_warnings.txt | 4 ++-- src/goto-cc/compile.cpp | 33 +++++++++++++------------- src/goto-cc/compile.h | 32 +++++++++++++++++++++---- src/goto-cc/gcc_mode.cpp | 6 +++-- src/goto-cc/ld_mode.cpp | 8 +++---- src/goto-cc/ld_mode.h | 2 +- src/goto-cc/linker_script_merge.cpp | 34 +++++++++++++++------------ src/goto-cc/linker_script_merge.h | 9 ++++--- 8 files changed, 80 insertions(+), 48 deletions(-) diff --git a/scripts/expected_doxygen_warnings.txt b/scripts/expected_doxygen_warnings.txt index d53b0be7381..656ec83e465 100644 --- a/scripts/expected_doxygen_warnings.txt +++ b/scripts/expected_doxygen_warnings.txt @@ -91,11 +91,11 @@ warning: Included by graph for 'expr.h' not generated, too many nodes (88), thre warning: Included by graph for 'expr_util.h' not generated, too many nodes (60), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'invariant.h' not generated, too many nodes (187), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'irep.h' not generated, too many nodes (62), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. -warning: Included by graph for 'message.h' not generated, too many nodes (115), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. +warning: Included by graph for 'message.h' not generated, too many nodes (116), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'namespace.h' not generated, too many nodes (111), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'prefix.h' not generated, too many nodes (86), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'simplify_expr.h' not generated, too many nodes (76), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'std_code.h' not generated, too many nodes (78), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. -warning: Included by graph for 'std_expr.h' not generated, too many nodes (245), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. +warning: Included by graph for 'std_expr.h' not generated, too many nodes (246), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'std_types.h' not generated, too many nodes (124), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'symbol_table.h' not generated, too many nodes (95), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp index 91e860fa02b..1eb5b143e39 100644 --- a/src/goto-cc/compile.cpp +++ b/src/goto-cc/compile.cpp @@ -556,32 +556,33 @@ bool compilet::parse_stdin(languaget &language) return false; } -/// Writes the goto functions of \p src_goto_model to a binary format object -/// file. -/// \param file_name: Target file to serialize \p src_goto_model to -/// \param src_goto_model: goto model to serialize -/// \return true on error, false otherwise bool compilet::write_bin_object_file( const std::string &file_name, - const goto_modelt &src_goto_model) + const goto_modelt &src_goto_model, + bool validate_goto_model, + message_handlert &message_handler) { + messaget log(message_handler); + if(validate_goto_model) { - status() << "Validating goto model" << eom; + log.status() << "Validating goto model" << messaget::eom; src_goto_model.validate(); } - statistics() << "Writing binary format object '" << file_name << "'" << eom; + log.statistics() << "Writing binary format object '" << file_name << "'" + << messaget::eom; // symbols - statistics() << "Symbols in table: " - << src_goto_model.symbol_table.symbols.size() << eom; + log.statistics() << "Symbols in table: " + << src_goto_model.symbol_table.symbols.size() + << messaget::eom; std::ofstream outfile(file_name, std::ios::binary); if(!outfile.is_open()) { - error() << "Error opening file '" << file_name << "'" << eom; + log.error() << "Error opening file '" << file_name << "'" << messaget::eom; return true; } @@ -590,12 +591,11 @@ bool compilet::write_bin_object_file( const auto cnt = function_body_count(src_goto_model.goto_functions); - statistics() << "Functions: " - << src_goto_model.goto_functions.function_map.size() << "; " - << cnt << " have a body." << eom; + log.statistics() << "Functions: " + << src_goto_model.goto_functions.function_map.size() << "; " + << cnt << " have a body." << messaget::eom; outfile.close(); - wrote_object=true; return false; } @@ -661,8 +661,7 @@ compilet::~compilet() delete_directory(dir); } -std::size_t -compilet::function_body_count(const goto_functionst &functions) const +std::size_t compilet::function_body_count(const goto_functionst &functions) { std::size_t count = 0; diff --git a/src/goto-cc/compile.h b/src/goto-cc/compile.h index d81cdba809d..d83098f3570 100644 --- a/src/goto-cc/compile.h +++ b/src/goto-cc/compile.h @@ -68,7 +68,18 @@ class compilet : public messaget bool parse_source(const std::string &); - bool write_bin_object_file(const std::string &, const goto_modelt &); + /// Writes the goto functions of \p src_goto_model to a binary format object + /// file. + /// \param file_name: Target file to serialize \p src_goto_model to + /// \param src_goto_model: goto model to serialize + /// \param validate_goto_model: enable goto-model validation + /// \param message_handler: message handler + /// \return true on error, false otherwise + static bool write_bin_object_file( + const std::string &file_name, + const goto_modelt &src_goto_model, + bool validate_goto_model, + message_handlert &message_handler); /// \brief Has this compiler written any object files? bool wrote_object_files() const { return wrote_object; } @@ -88,8 +99,6 @@ class compilet : public messaget } protected: - namespacet ns; - std::string working_directory; std::string override_language; @@ -105,7 +114,22 @@ class compilet : public messaget /// \brief String to include in all mangled names const std::string file_local_mangle_suffix; - std::size_t function_body_count(const goto_functionst &) const; + static std::size_t function_body_count(const goto_functionst &); + + bool write_bin_object_file( + const std::string &file_name, + const goto_modelt &src_goto_model) + { + if(write_bin_object_file( + file_name, src_goto_model, validate_goto_model, get_message_handler())) + { + return true; + } + + wrote_object = true; + + return false; + } void add_compiler_specific_defines() const; diff --git a/src/goto-cc/gcc_mode.cpp b/src/goto-cc/gcc_mode.cpp index 3ac2fdf560d..32753f4d875 100644 --- a/src/goto-cc/gcc_mode.cpp +++ b/src/goto-cc/gcc_mode.cpp @@ -972,8 +972,10 @@ int gcc_modet::gcc_hybrid_binary(compilet &compiler) output_files.size()==1) { linker_script_merget ls_merge( - compiler, output_files.front(), goto_binaries.front(), - cmdline, gcc_message_handler); + output_files.front(), + goto_binaries.front(), + cmdline, + gcc_message_handler); result=ls_merge.add_linker_script_definitions(); } diff --git a/src/goto-cc/ld_mode.cpp b/src/goto-cc/ld_mode.cpp index 80f62b1d1b6..830fdd7ba9c 100644 --- a/src/goto-cc/ld_mode.cpp +++ b/src/goto-cc/ld_mode.cpp @@ -145,7 +145,7 @@ int ld_modet::doit() // We can generate hybrid ELF and Mach-O binaries // containing both executable machine code and the goto-binary. - return ld_hybrid_binary(compiler); + return ld_hybrid_binary(compiler.mode == compilet::COMPILE_LINK_EXECUTABLE); } int ld_modet::run_ld() @@ -170,7 +170,7 @@ int ld_modet::run_ld() return run(new_argv[0], new_argv, cmdline.stdin_file, "", ""); } -int ld_modet::ld_hybrid_binary(compilet &compiler) +int ld_modet::ld_hybrid_binary(bool building_executable) { std::string output_file; @@ -206,7 +206,7 @@ int ld_modet::ld_hybrid_binary(compilet &compiler) if(result == 0 && cmdline.isset('T')) { linker_script_merget ls_merge( - compiler, output_file, goto_binary, cmdline, message_handler); + output_file, goto_binary, cmdline, message_handler); result = ls_merge.add_linker_script_definitions(); } @@ -218,7 +218,7 @@ int ld_modet::ld_hybrid_binary(compilet &compiler) native_linker, goto_binary, output_file, - compiler.mode == compilet::COMPILE_LINK_EXECUTABLE, + building_executable, message_handler); } diff --git a/src/goto-cc/ld_mode.h b/src/goto-cc/ld_mode.h index 6c0ce556714..3d24547c536 100644 --- a/src/goto-cc/ld_mode.h +++ b/src/goto-cc/ld_mode.h @@ -40,7 +40,7 @@ class ld_modet : public goto_cc_modet /// \brief call ld with original command line int run_ld(); - int ld_hybrid_binary(compilet &compiler); + int ld_hybrid_binary(bool); }; #endif // CPROVER_GOTO_CC_LD_MODE_H diff --git a/src/goto-cc/linker_script_merge.cpp b/src/goto-cc/linker_script_merge.cpp index e21dbf33a1d..881e192ff5b 100644 --- a/src/goto-cc/linker_script_merge.cpp +++ b/src/goto-cc/linker_script_merge.cpp @@ -25,16 +25,28 @@ Author: Kareem Khazem , 2017 #include +#include "compile.h" + int linker_script_merget::add_linker_script_definitions() { if(!cmdline.isset('T')) return 0; + auto original_goto_model = + read_goto_binary(goto_binary, log.get_message_handler()); + + if(!original_goto_model.has_value()) + { + log.error() << "Unable to read goto binary for linker script merging" + << messaget::eom; + return 1; + } + temporary_filet linker_def_outfile("goto-cc-linker-info", ".json"); std::list linker_defined_symbols; int fail = get_linker_script_data( linker_defined_symbols, - compiler.goto_model.symbol_table, + original_goto_model->symbol_table, elf_binary, linker_def_outfile()); // ignore linker script parsing failures until the code is tested more widely @@ -57,16 +69,6 @@ int linker_script_merget::add_linker_script_definitions() return fail; } - auto original_goto_model = - read_goto_binary(goto_binary, log.get_message_handler()); - - if(!original_goto_model.has_value()) - { - log.error() << "Unable to read goto binary for linker script merging" - << messaget::eom; - return 1; - } - fail=1; linker_valuest linker_values; const auto &pair = @@ -106,7 +108,11 @@ int linker_script_merget::add_linker_script_definitions() return fail; } - fail = compiler.write_bin_object_file(goto_binary, *original_goto_model); + fail = compilet::write_bin_object_file( + goto_binary, + *original_goto_model, + cmdline.isset("validate-goto-model"), + log.get_message_handler()); if(fail!=0) { @@ -118,13 +124,11 @@ int linker_script_merget::add_linker_script_definitions() } linker_script_merget::linker_script_merget( - compilet &compiler, const std::string &elf_binary, const std::string &goto_binary, const cmdlinet &cmdline, message_handlert &message_handler) - : compiler(compiler), - elf_binary(elf_binary), + : elf_binary(elf_binary), goto_binary(goto_binary), cmdline(cmdline), log(message_handler), diff --git a/src/goto-cc/linker_script_merge.h b/src/goto-cc/linker_script_merge.h index 98dc86bc45a..e53ace4ea34 100644 --- a/src/goto-cc/linker_script_merge.h +++ b/src/goto-cc/linker_script_merge.h @@ -8,10 +8,15 @@ #include #include +#include +#include -#include "compile.h" #include "gcc_cmdline.h" +class goto_modelt; +class goto_programt; +class symbol_tablet; + /// \brief Patterns of expressions that should be replaced /// /// Each instance of this class describes an expression 'shape' that should be @@ -79,14 +84,12 @@ class linker_script_merget typedef std::map> linker_valuest; linker_script_merget( - compilet &, const std::string &elf_binary, const std::string &goto_binary, const cmdlinet &, message_handlert &); protected: - compilet &compiler; const std::string &elf_binary; const std::string &goto_binary; const cmdlinet &cmdline; From adaefcfca13eadde23bd61b7f5a4a9ce4c02e175 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 28 Feb 2019 10:42:41 +0000 Subject: [PATCH 2/2] goto-cc: also use the linker when processing multiple source files The linker is able to do some type sanitisation across translation units, and there is no reason behaviour should be different whether we link previously compiled object files or a set of source files. --- .../ansi-c/linking_conflicts1/test.desc | 1 - .../ansi-c/linking_conflicts2/test.desc | 3 +- src/goto-cc/compile.cpp | 86 +++++++++++-------- src/goto-cc/compile.h | 11 +-- 4 files changed, 54 insertions(+), 47 deletions(-) diff --git a/regression/ansi-c/linking_conflicts1/test.desc b/regression/ansi-c/linking_conflicts1/test.desc index 73decc3320d..fb6ea7a2909 100644 --- a/regression/ansi-c/linking_conflicts1/test.desc +++ b/regression/ansi-c/linking_conflicts1/test.desc @@ -3,7 +3,6 @@ main.c other.c ^EXIT=(64|1)$ ^SIGNAL=0$ -^CONVERSION ERROR$ error: conflicting function declarations 'bar' error: conflicting function declarations 'bar2' -- diff --git a/regression/ansi-c/linking_conflicts2/test.desc b/regression/ansi-c/linking_conflicts2/test.desc index 824f75300d6..f579050c99b 100644 --- a/regression/ansi-c/linking_conflicts2/test.desc +++ b/regression/ansi-c/linking_conflicts2/test.desc @@ -1,9 +1,8 @@ -CORE broken-test-c++-front-end +CORE main.c other.c ^EXIT=(64|1)$ ^SIGNAL=0$ -^CONVERSION ERROR$ error: conflicting function declarations 'foo' -- ^warning: ignoring diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp index 1eb5b143e39..ba00db47150 100644 --- a/src/goto-cc/compile.cpp +++ b/src/goto-cc/compile.cpp @@ -42,6 +42,7 @@ Date: June 2006 #include #include +#include #include #define DOTGRAPHSETTINGS "color=black;" \ @@ -56,8 +57,6 @@ Date: June 2006 /// \return true on error, false otherwise bool compilet::doit() { - goto_model.goto_functions.clear(); - add_compiler_specific_defines(); // Parse command line for source and object file names @@ -98,15 +97,15 @@ bool compilet::doit() const unsigned warnings_before= get_message_handler().get_message_count(messaget::M_WARNING); - if(!source_files.empty()) - if(compile()) - return true; + auto symbol_table_opt = compile(); + if(!symbol_table_opt.has_value()) + return true; if(mode==LINK_LIBRARY || mode==COMPILE_LINK || mode==COMPILE_LINK_EXECUTABLE) { - if(link()) + if(link(*symbol_table_opt)) return true; } @@ -308,11 +307,14 @@ bool compilet::find_library(const std::string &name) /// parses object files and links them /// \return true on error, false otherwise -bool compilet::link() +bool compilet::link(optionalt &&symbol_table) { // "compile" hitherto uncompiled functions statistics() << "Compiling functions" << eom; - convert_symbols(goto_model.goto_functions); + goto_modelt goto_model; + if(symbol_table.has_value()) + goto_model.symbol_table = std::move(*symbol_table); + convert_symbols(goto_model); // parse object files for(const auto &file_name : object_files) @@ -343,7 +345,7 @@ bool compilet::link() return true; // entry_point may (should) add some more functions. - convert_symbols(goto_model.goto_functions); + convert_symbols(goto_model); } if(keep_file_local) @@ -359,11 +361,13 @@ bool compilet::link() return add_written_cprover_symbols(goto_model.symbol_table); } -/// parses source files and writes object files, or keeps the symbols in the -/// symbol_table depending on the doLink flag. -/// \return true on error, false otherwise -bool compilet::compile() +/// Parses source files and writes object files, or keeps the symbols in the +/// symbol_table if not compiling/assembling only. +/// \return Symbol table, if parsing and type checking succeeded, else empty +optionalt compilet::compile() { + symbol_tablet symbol_table; + while(!source_files.empty()) { std::string file_name=source_files.front(); @@ -374,9 +378,9 @@ bool compilet::compile() if(echo_file_name) std::cout << get_base_name(file_name, false) << '\n' << std::flush; - bool r=parse_source(file_name); // don't break the program! + auto file_symbol_table = parse_source(file_name); - if(r) + if(!file_symbol_table.has_value()) { const std::string &debug_outfile= cmdline.get_value("print-rejected-preprocessed-source"); @@ -388,7 +392,7 @@ bool compilet::compile() warning() << "Failed sources in " << debug_outfile << eom; } - return true; // parser/typecheck error + return {}; // parser/typecheck error } if(mode==COMPILE_ONLY || mode==ASSEMBLE_ONLY) @@ -396,7 +400,9 @@ bool compilet::compile() // output an object file for every source file // "compile" functions - convert_symbols(goto_model.goto_functions); + goto_modelt file_goto_model; + file_goto_model.symbol_table = std::move(*file_symbol_table); + convert_symbols(file_goto_model); std::string cfn; @@ -416,21 +422,26 @@ bool compilet::compile() if(keep_file_local) { function_name_manglert mangler( - get_message_handler(), goto_model, file_local_mangle_suffix); + get_message_handler(), file_goto_model, file_local_mangle_suffix); mangler.mangle(); } - if(write_bin_object_file(cfn, goto_model)) - return true; - - if(add_written_cprover_symbols(goto_model.symbol_table)) - return true; + if(write_bin_object_file(cfn, file_goto_model)) + return {}; - goto_model.clear(); // clean symbol table for next source file. + if(add_written_cprover_symbols(file_goto_model.symbol_table)) + return {}; + } + else + { + if(linking(symbol_table, *file_symbol_table, get_message_handler())) + { + return {}; + } } } - return false; + return std::move(symbol_table); } /// parses a source file (low-level parsing) @@ -600,37 +611,37 @@ bool compilet::write_bin_object_file( return false; } -/// parses a source file -/// \return true on error, false otherwise -bool compilet::parse_source(const std::string &file_name) +/// Parses and type checks a source file located at \p file_name. +/// \return A symbol table if, and only if, parsing and type checking succeeded. +optionalt compilet::parse_source(const std::string &file_name) { language_filest language_files; language_files.set_message_handler(get_message_handler()); if(parse(file_name, language_files)) - return true; + return {}; // we just typecheck one file here - if(language_files.typecheck(goto_model.symbol_table, keep_file_local)) + symbol_tablet file_symbol_table; + if(language_files.typecheck(file_symbol_table, keep_file_local)) { error() << "CONVERSION ERROR" << eom; - return true; + return {}; } - if(language_files.final(goto_model.symbol_table)) + if(language_files.final(file_symbol_table)) { error() << "CONVERSION ERROR" << eom; - return true; + return {}; } - return false; + return std::move(file_symbol_table); } /// constructor /// \return nothing compilet::compilet(cmdlinet &_cmdline, message_handlert &mh, bool Werror) : messaget(mh), - ns(goto_model.symbol_table), cmdline(_cmdline), warning_is_fatal(Werror), keep_file_local( @@ -678,7 +689,7 @@ void compilet::add_compiler_specific_defines() const std::string("__GOTO_CC_VERSION__=") + CBMC_VERSION); } -void compilet::convert_symbols(goto_functionst &dest) +void compilet::convert_symbols(goto_modelt &goto_model) { symbol_table_buildert symbol_table_builder = symbol_table_buildert::wrap(goto_model.symbol_table); @@ -712,7 +723,8 @@ void compilet::convert_symbols(goto_functionst &dest) s_it->second.value.is_not_nil()) { debug() << "Compiling " << s_it->first << eom; - converter.convert_function(s_it->first, dest.function_map[s_it->first]); + converter.convert_function( + s_it->first, goto_model.goto_functions.function_map[s_it->first]); symbol_table_builder.get_writeable_ref(symbol).set_compiled(); } } diff --git a/src/goto-cc/compile.h b/src/goto-cc/compile.h index d83098f3570..da64ead844d 100644 --- a/src/goto-cc/compile.h +++ b/src/goto-cc/compile.h @@ -26,9 +26,6 @@ class languaget; class compilet : public messaget { public: - // compilation results - goto_modelt goto_model; - // configuration bool echo_file_name; bool validate_goto_model = false; @@ -63,10 +60,10 @@ class compilet : public messaget bool parse(const std::string &filename, language_filest &); bool parse_stdin(languaget &); bool doit(); - bool compile(); - bool link(); + optionalt compile(); + bool link(optionalt &&symbol_table); - bool parse_source(const std::string &); + optionalt parse_source(const std::string &); /// Writes the goto functions of \p src_goto_model to a binary format object /// file. @@ -133,7 +130,7 @@ class compilet : public messaget void add_compiler_specific_defines() const; - void convert_symbols(goto_functionst &dest); + void convert_symbols(goto_modelt &); bool add_written_cprover_symbols(const symbol_tablet &symbol_table); std::map written_macros;