diff --git a/jbmc/src/java_bytecode/lazy_goto_model.cpp b/jbmc/src/java_bytecode/lazy_goto_model.cpp index a0e9585c431..dd379d9cbbd 100644 --- a/jbmc/src/java_bytecode/lazy_goto_model.cpp +++ b/jbmc/src/java_bytecode/lazy_goto_model.cpp @@ -5,17 +5,17 @@ #include "lazy_goto_model.h" -#include "java_bytecode_language.h" +#include +#include +#include +#include +#include #include -#include #include -#include -#include -#include -#include +#include "java_bytecode_language.h" #ifdef _MSC_VER # include @@ -164,93 +164,20 @@ void lazy_goto_modelt::initialize( } else { - for(const auto &filename : sources) - { -#ifdef _MSC_VER - std::ifstream infile(widen(filename)); -#else - std::ifstream infile(filename); -#endif - - if(!infile) - { - throw system_exceptiont( - "failed to open input file '" + filename + '\''); - } - - language_filet &lf = add_language_file(filename); - lf.language = get_language_from_filename(filename); - - if(lf.language == nullptr) - { - throw invalid_source_file_exceptiont( - "failed to figure out type of file '" + filename + '\''); - } - - languaget &language = *lf.language; - language.set_message_handler(message_handler); - language.set_language_options(options); - - msg.status() << "Parsing " << filename << messaget::eom; - - if(language.parse(infile, filename)) - { - throw invalid_source_file_exceptiont("PARSING ERROR"); - } - - lf.get_modules(); - } - - msg.status() << "Converting" << messaget::eom; - - if(language_files.typecheck(symbol_table)) - { - throw invalid_source_file_exceptiont("CONVERSION ERROR"); - } + initialize_from_source_files( + sources, options, language_files, symbol_table, message_handler); } if(read_objects_and_link(binaries, *goto_model, message_handler)) throw incorrect_goto_program_exceptiont{"failed to read/link goto model"}; - bool binaries_provided_start = - symbol_table.has_symbol(goto_functionst::entry_point()); - - bool entry_point_generation_failed = false; - - if(binaries_provided_start && options.is_set("function")) - { - // The goto binaries provided already contain a __CPROVER_start - // function that may be tied to a different entry point `function`. - // Hence, we will rebuild the __CPROVER_start function. - - // Get the language annotation of the existing __CPROVER_start function. - std::unique_ptr language = - get_entry_point_language(symbol_table, options, message_handler); - - // To create a new entry point we must first remove the old one - remove_existing_entry_point(symbol_table); - - // Create the new entry-point - entry_point_generation_failed = - language->generate_support_functions(symbol_table); - - // Remove the function from the goto functions so it is copied back in - // from the symbol table during goto_convert - if(!entry_point_generation_failed) - unload(goto_functionst::entry_point()); - } - else if(!binaries_provided_start) - { - // Allow all language front-ends to try to provide the user-specified - // (--function) entry-point, or some language-specific default: - entry_point_generation_failed = - language_files.generate_support_functions(symbol_table); - } - - if(entry_point_generation_failed) - { - throw invalid_source_file_exceptiont("SUPPORT FUNCTION GENERATION ERROR"); - } + set_up_custom_entry_point( + language_files, + symbol_table, + [this](const irep_idt &id) { goto_functions.unload(id); }, + options, + false, + message_handler); // stupid hack config.set_object_bits_from_symbol_table(symbol_table); diff --git a/jbmc/src/java_bytecode/lazy_goto_model.h b/jbmc/src/java_bytecode/lazy_goto_model.h index ab29564314f..dc36f9c8fb1 100644 --- a/jbmc/src/java_bytecode/lazy_goto_model.h +++ b/jbmc/src/java_bytecode/lazy_goto_model.h @@ -183,11 +183,6 @@ class lazy_goto_modelt : public abstract_goto_modelt /// Eagerly loads all functions from the symbol table. void load_all_functions() const; - void unload(const irep_idt &name) const - { - goto_functions.unload(name); - } - language_filet &add_language_file(const std::string &filename) { return language_files.add_file(filename); diff --git a/src/goto-programs/initialize_goto_model.cpp b/src/goto-programs/initialize_goto_model.cpp index 89b9b2f725f..caf1307dd69 100644 --- a/src/goto-programs/initialize_goto_model.cpp +++ b/src/goto-programs/initialize_goto_model.cpp @@ -34,13 +34,13 @@ Author: Daniel Kroening, kroening@kroening.com /// Generate an entry point that calls a function with the given name, based on /// the functions language mode in the symbol table static bool generate_entry_point_for_function( - const irep_idt &entry_function_name, const optionst &options, - goto_modelt &goto_model, + symbol_tablet &symbol_table, message_handlert &message_handler) { - auto const entry_function_sym = - goto_model.symbol_table.lookup(entry_function_name); + const irep_idt &entry_function_name = options.get_option("function"); + CHECK_RETURN(!entry_function_name.empty()); + auto const entry_function_sym = symbol_table.lookup(entry_function_name); if(entry_function_sym == nullptr) { throw invalid_command_line_argument_exceptiont{ @@ -54,42 +54,23 @@ static bool generate_entry_point_for_function( CHECK_RETURN(entry_language != nullptr); entry_language->set_message_handler(message_handler); entry_language->set_language_options(options); - return entry_language->generate_support_functions(goto_model.symbol_table); + return entry_language->generate_support_functions(symbol_table); } -goto_modelt initialize_goto_model( - const std::vector &files, - message_handlert &message_handler, - const optionst &options) +void initialize_from_source_files( + const std::list &sources, + const optionst &options, + language_filest &language_files, + symbol_tablet &symbol_table, + message_handlert &message_handler) { - messaget msg(message_handler); - if(files.empty()) - { - throw invalid_command_line_argument_exceptiont( - "missing program argument", - "filename", - "one or more paths to program files"); - } - - std::list binaries, sources; - - for(const auto &file : files) - { - if(is_goto_binary(file, message_handler)) - binaries.push_back(file); - else - sources.push_back(file); - } + if(sources.empty()) + return; - language_filest language_files; - language_files.set_message_handler(message_handler); - - goto_modelt goto_model; + messaget msg(message_handler); - if(!sources.empty()) + for(const auto &filename : sources) { - for(const auto &filename : sources) - { #ifdef _MSC_VER std::ifstream infile(widen(filename)); #else @@ -107,8 +88,8 @@ goto_modelt initialize_goto_model( if(lf.language==nullptr) { - throw invalid_source_file_exceptiont( - "Failed to figure out type of file '" + filename + '\''); + throw invalid_command_line_argument_exceptiont{ + "Failed to figure out type of file", filename}; } languaget &language=*lf.language; @@ -119,7 +100,7 @@ goto_modelt initialize_goto_model( if(language.parse(infile, filename)) { - throw invalid_source_file_exceptiont("PARSING ERROR"); + throw invalid_input_exceptiont("PARSING ERROR"); } lf.get_modules(); @@ -127,67 +108,119 @@ goto_modelt initialize_goto_model( msg.status() << "Converting" << messaget::eom; - if(language_files.typecheck(goto_model.symbol_table)) + if(language_files.typecheck(symbol_table)) { - throw invalid_source_file_exceptiont("CONVERSION ERROR"); + throw invalid_input_exceptiont("CONVERSION ERROR"); } - } - - if(read_objects_and_link(binaries, goto_model, message_handler)) - { - throw invalid_source_file_exceptiont{ - "failed to read object or link in files"}; - } +} - bool binaries_provided_start= - goto_model.symbol_table.has_symbol(goto_functionst::entry_point()); +void set_up_custom_entry_point( + language_filest &language_files, + symbol_tablet &symbol_table, + const std::function &unload, + const optionst &options, + bool try_mode_lookup, + message_handlert &message_handler) +{ + bool binaries_provided_start = + symbol_table.has_symbol(goto_functionst::entry_point()); bool entry_point_generation_failed=false; if(binaries_provided_start && options.is_set("function")) { + // The goto binaries provided already contain a __CPROVER_start + // function that may be tied to a different entry point `function`. + // Hence, we will rebuild the __CPROVER_start function. + // Get the language annotation of the existing __CPROVER_start function. - std::unique_ptr language = get_entry_point_language( - goto_model.symbol_table, options, message_handler); + std::unique_ptr language = + get_entry_point_language(symbol_table, options, message_handler); // To create a new entry point we must first remove the old one - remove_existing_entry_point(goto_model.symbol_table); + remove_existing_entry_point(symbol_table); // Create the new entry-point entry_point_generation_failed = - language->generate_support_functions(goto_model.symbol_table); + language->generate_support_functions(symbol_table); // Remove the function from the goto functions so it is copied back in // from the symbol table during goto_convert if(!entry_point_generation_failed) - goto_model.unload(goto_functionst::entry_point()); + unload(goto_functionst::entry_point()); } else if(!binaries_provided_start) { - if(options.is_set("function")) + if(try_mode_lookup && options.is_set("function")) { // no entry point is present; Use the mode of the specified entry function // to generate one entry_point_generation_failed = generate_entry_point_for_function( - options.get_option("function"), options, goto_model, message_handler); + options, symbol_table, message_handler); } - if(entry_point_generation_failed || !options.is_set("function")) + if( + !try_mode_lookup || entry_point_generation_failed || + !options.is_set("function")) { // Allow all language front-ends to try to provide the user-specified // (--function) entry-point, or some language-specific default: entry_point_generation_failed = - language_files.generate_support_functions(goto_model.symbol_table); + language_files.generate_support_functions(symbol_table); } } if(entry_point_generation_failed) { - throw invalid_source_file_exceptiont("SUPPORT FUNCTION GENERATION ERROR"); + throw invalid_input_exceptiont("SUPPORT FUNCTION GENERATION ERROR"); + } +} + +goto_modelt initialize_goto_model( + const std::vector &files, + message_handlert &message_handler, + const optionst &options) +{ + messaget msg(message_handler); + if(files.empty()) + { + throw invalid_command_line_argument_exceptiont( + "missing program argument", + "filename", + "one or more paths to program files"); + } + + std::list binaries, sources; + + for(const auto &file : files) + { + if(is_goto_binary(file, message_handler)) + binaries.push_back(file); + else + sources.push_back(file); } + language_filest language_files; + language_files.set_message_handler(message_handler); + + goto_modelt goto_model; + + initialize_from_source_files( + sources, options, language_files, goto_model.symbol_table, message_handler); + + if(read_objects_and_link(binaries, goto_model, message_handler)) + throw incorrect_goto_program_exceptiont{"failed to read/link goto model"}; + + set_up_custom_entry_point( + language_files, + goto_model.symbol_table, + [&goto_model](const irep_idt &id) { goto_model.goto_functions.unload(id); }, + options, + true, + message_handler); + if(language_files.final(goto_model.symbol_table)) { - throw invalid_source_file_exceptiont("FINAL STAGE CONVERSION ERROR"); + throw invalid_input_exceptiont("FINAL STAGE CONVERSION ERROR"); } msg.status() << "Generating GOTO Program" << messaget::eom; diff --git a/src/goto-programs/initialize_goto_model.h b/src/goto-programs/initialize_goto_model.h index 139263e09d5..e0cb1f23112 100644 --- a/src/goto-programs/initialize_goto_model.h +++ b/src/goto-programs/initialize_goto_model.h @@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "goto_model.h" +class language_filest; class message_handlert; class optionst; @@ -22,4 +23,37 @@ goto_modelt initialize_goto_model( message_handlert &message_handler, const optionst &options); +/// Populate \p symbol_table from \p sources by parsing and type checking via +/// \p language_files. Throws exceptions if processing fails. +/// \param sources: Collection of input source files. No operation is performed +/// if the collection is empty. +/// \param options: Configuration options. +/// \param language_files: Language parsing and type checking facilities. +/// \param [out] symbol_table: Symbol table to be populated. +/// \param message_handler: Message handler. +void initialize_from_source_files( + const std::list &sources, + const optionst &options, + language_filest &language_files, + symbol_tablet &symbol_table, + message_handlert &message_handler); + +/// Process the "function" option in \p options to prepare a custom entry point +/// to replace \c __CPROVER_start. +/// \param language_files: Language parsing and type checking facilities. +/// \param symbol_table: Symbol table for mode lookup and removal of an existing +/// entry point. +/// \param unload: Functor to remove an existing entry point. +/// \param options: Configuration options. +/// \param try_mode_lookup: Try to infer the entry point's mode from the symbol +/// table. +/// \param message_handler: Message handler. +void set_up_custom_entry_point( + language_filest &language_files, + symbol_tablet &symbol_table, + const std::function &unload, + const optionst &options, + bool try_mode_lookup, + message_handlert &message_handler); + #endif // CPROVER_GOTO_PROGRAMS_INITIALIZE_GOTO_MODEL_H diff --git a/src/goto-programs/read_goto_binary.h b/src/goto-programs/read_goto_binary.h index f704855dad4..462657df8b6 100644 --- a/src/goto-programs/read_goto_binary.h +++ b/src/goto-programs/read_goto_binary.h @@ -27,7 +27,7 @@ bool is_goto_binary(const std::string &filename, message_handlert &); /// Reads object files and updates the config if any files were read. /// \param file_names: file names of goto binaries; if empty, just returns false -/// \param dest: goto model to update +/// \param [out] dest: GOTO model to update. /// \param message_handler: for diagnostics /// \return True on error, false otherwise bool read_objects_and_link(