From c0788586aca62092980d29835c91e4a507c926e0 Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Wed, 20 Sep 2017 17:06:04 +0100 Subject: [PATCH 01/21] Introduce lazy_goto_modelt Introduces a class that holds a goto_modelt and language_filest to allow for lazy loading of functions. Don't eagerly convert functions during initialisation of lazy_goto_modelt. Instead adds a function to allow eager loading at a later stage if required (it always is at the moment). --- src/goto-programs/Makefile | 1 + src/goto-programs/goto_functions_template.h | 2 + src/goto-programs/initialize_goto_model.cpp | 5 +- src/goto-programs/lazy_goto_model.cpp | 179 ++++++++++++++++++ src/goto-programs/lazy_goto_model.h | 62 ++++++ .../rebuild_goto_start_function.cpp | 59 +++--- .../rebuild_goto_start_function.h | 24 ++- src/jbmc/jbmc_parse_options.cpp | 41 ++-- src/jbmc/jbmc_parse_options.h | 10 +- 9 files changed, 326 insertions(+), 57 deletions(-) create mode 100644 src/goto-programs/lazy_goto_model.cpp create mode 100644 src/goto-programs/lazy_goto_model.h diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile index 2474a7d7e8b..38a75637776 100644 --- a/src/goto-programs/Makefile +++ b/src/goto-programs/Makefile @@ -27,6 +27,7 @@ SRC = basic_blocks.cpp \ interpreter.cpp \ interpreter_evaluate.cpp \ json_goto_trace.cpp \ + lazy_goto_model.cpp \ link_goto_model.cpp \ link_to_library.cpp \ loop_ids.cpp \ diff --git a/src/goto-programs/goto_functions_template.h b/src/goto-programs/goto_functions_template.h index 1a95d670f60..f2551c72483 100644 --- a/src/goto-programs/goto_functions_template.h +++ b/src/goto-programs/goto_functions_template.h @@ -121,6 +121,8 @@ class goto_functions_templatet return *this; } + void unload(const irep_idt &name) { function_map.erase(name); } + void clear() { function_map.clear(); diff --git a/src/goto-programs/initialize_goto_model.cpp b/src/goto-programs/initialize_goto_model.cpp index fd3fa158207..d5ec80461e1 100644 --- a/src/goto-programs/initialize_goto_model.cpp +++ b/src/goto-programs/initialize_goto_model.cpp @@ -132,10 +132,9 @@ goto_modelt initialize_goto_model( // Rebuild the entry-point, using the language annotation of the // existing __CPROVER_start function: rebuild_goto_start_functiont rebuild_existing_start( - msg.get_message_handler(), cmdline, - goto_model.symbol_table, - goto_model.goto_functions); + goto_model, + msg.get_message_handler()); entry_point_generation_failed=rebuild_existing_start(); } else if(!binaries_provided_start) diff --git a/src/goto-programs/lazy_goto_model.cpp b/src/goto-programs/lazy_goto_model.cpp new file mode 100644 index 00000000000..811436eeb3a --- /dev/null +++ b/src/goto-programs/lazy_goto_model.cpp @@ -0,0 +1,179 @@ +// Copyright 2017 Diffblue Limited. All Rights Reserved. + +/// \file +/// Model for lazy loading of functions + +#include "lazy_goto_model.h" +#include "read_goto_binary.h" +#include "rebuild_goto_start_function.h" + +#include + +#include +#include +#include +#include + +#include + +lazy_goto_modelt::lazy_goto_modelt(message_handlert &message_handler) + : goto_model(new goto_modelt()), + symbol_table(goto_model->symbol_table), + goto_functions(goto_model->goto_functions), + message_handler(message_handler) +{ + language_files.set_message_handler(message_handler); +} + +lazy_goto_modelt::lazy_goto_modelt(lazy_goto_modelt &&other) + : goto_model(std::move(other.goto_model)), + symbol_table(goto_model->symbol_table), + goto_functions(goto_model->goto_functions), + language_files(std::move(other.language_files)), + message_handler(other.message_handler) +{ +} + +void lazy_goto_modelt::initialize(const cmdlinet &cmdline) +{ + messaget msg(message_handler); + + const std::vector &files=cmdline.args; + if(files.empty()) + { + msg.error() << "Please provide a program" << messaget::eom; + throw 0; + } + + std::vector binaries, sources; + binaries.reserve(files.size()); + sources.reserve(files.size()); + + for(const auto &file : files) + { + if(is_goto_binary(file)) + binaries.push_back(file); + else + sources.push_back(file); + } + + if(!sources.empty()) + { + for(const auto &filename : sources) + { +#ifdef _MSC_VER + std::ifstream infile(widen(filename)); +#else + std::ifstream infile(filename); +#endif + + if(!infile) + { + msg.error() << "failed to open input file `" << filename + << '\'' << messaget::eom; + throw 0; + } + + std::pair result = + language_files.file_map.emplace(filename, language_filet()); + + language_filet &lf=result.first->second; + + lf.filename=filename; + lf.language=get_language_from_filename(filename); + + if(lf.language==nullptr) + { + source_locationt location; + location.set_file(filename); + msg.error().source_location=location; + msg.error() << "failed to figure out type of file" << messaget::eom; + throw 0; + } + + languaget &language=*lf.language; + language.set_message_handler(message_handler); + language.get_language_options(cmdline); + + msg.status() << "Parsing " << filename << messaget::eom; + + if(language.parse(infile, filename)) + { + msg.error() << "PARSING ERROR" << messaget::eom; + throw 0; + } + + lf.get_modules(); + } + + msg.status() << "Converting" << messaget::eom; + + if(language_files.typecheck(symbol_table)) + { + msg.error() << "CONVERSION ERROR" << messaget::eom; + throw 0; + } + } + + for(const auto &file : binaries) + { + msg.status() << "Reading GOTO program from file" << messaget::eom; + + if(read_object_and_link( + file, symbol_table, goto_functions, message_handler)) + { + throw 0; + } + } + + bool binaries_provided_start = + symbol_table.has_symbol(goto_functionst::entry_point()); + + bool entry_point_generation_failed=false; + + if(binaries_provided_start && cmdline.isset("function")) + { + // Rebuild the entry-point, using the language annotation of the + // existing __CPROVER_start function: + rebuild_lazy_goto_start_functiont rebuild_existing_start( + cmdline, *this, message_handler); + entry_point_generation_failed=rebuild_existing_start(); + } + else if(!binaries_provided_start) + { + // Unsure of the rationale for only generating stubs when there are no + // GOTO binaries in play; simply mirroring old code in language_uit here. + if(binaries.empty()) + { + // Enable/disable stub generation for opaque methods + bool stubs_enabled=cmdline.isset("generate-opaque-stubs"); + language_files.set_should_generate_opaque_method_stubs(stubs_enabled); + } + + // 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) + { + msg.error() << "SUPPORT FUNCTION GENERATION ERROR" << messaget::eom; + throw 0; + } + + if(language_files.final(symbol_table)) + { + msg.error() << "FINAL STAGE CONVERSION ERROR" << messaget::eom; + throw 0; + } + + // stupid hack + config.set_object_bits_from_symbol_table(symbol_table); +} + +/// Eagerly loads all functions from the symbol table. +void lazy_goto_modelt::load_all_functions() const +{ + goto_convert(*goto_model, message_handler); +} diff --git a/src/goto-programs/lazy_goto_model.h b/src/goto-programs/lazy_goto_model.h new file mode 100644 index 00000000000..cf4404fd994 --- /dev/null +++ b/src/goto-programs/lazy_goto_model.h @@ -0,0 +1,62 @@ +// Copyright 2016-2017 Diffblue Limited. All Rights Reserved. + +/// \file +/// Model for lazy loading of functions + +#ifndef CPROVER_GOTO_PROGRAMS_LAZY_GOTO_MODEL_H +#define CPROVER_GOTO_PROGRAMS_LAZY_GOTO_MODEL_H + +#include + +#include "goto_model.h" +#include "goto_convert_functions.h" + +class cmdlinet; + + +/// Model that holds partially loaded map of functions +class lazy_goto_modelt +{ +public: + explicit lazy_goto_modelt(message_handlert &message_handler); + + lazy_goto_modelt(lazy_goto_modelt &&other); + + lazy_goto_modelt &operator=(lazy_goto_modelt &&other) + { + goto_model = std::move(other.goto_model); + language_files = std::move(other.language_files); + return *this; + } + + void initialize(const cmdlinet &cmdline); + + /// Eagerly loads all functions from the symbol table. + void load_all_functions() const; + + /// The model returned here has access to the functions we've already + /// loaded but is frozen in the sense that, with regard to the facility to + /// load new functions, it has let it go. + /// \param model: The lazy_goto_modelt to freeze + /// \returns The frozen goto_modelt or an empty optional if freezing fails + static std::unique_ptr freeze(lazy_goto_modelt &&model) + { + return std::move(model.goto_model); + } + +private: + std::unique_ptr goto_model; + +public: + /// Reference to symbol_table in the internal goto_model + symbol_tablet &symbol_table; + goto_functionst &goto_functions; + +private: + language_filest language_files; + + /// Logging helper field + message_handlert &message_handler; +}; + +#endif // CPROVER_GOTO_PROGRAMS_LAZY_GOTO_MODEL_H diff --git a/src/goto-programs/rebuild_goto_start_function.cpp b/src/goto-programs/rebuild_goto_start_function.cpp index 230490318dc..1b9e1ea4028 100644 --- a/src/goto-programs/rebuild_goto_start_function.cpp +++ b/src/goto-programs/rebuild_goto_start_function.cpp @@ -8,7 +8,6 @@ #include "rebuild_goto_start_function.h" -#include #include #include #include @@ -17,22 +16,21 @@ #include #include -/// To rebuild the _start funciton in the event the program was compiled into +/// To rebuild the _start function in the event the program was compiled into /// GOTO with a different entry function selected. +/// \param goto_model: The goto functions (to replace the body of the _start +/// function) and symbol table (to replace the _start function symbol) of the +/// program. /// \param _message_handler: The message handler to report any messages with -/// \param symbol_table: The symbol table of the program (to replace the _start -/// functions symbo) -/// \param goto_functions: The goto functions of the program (to replace the -/// body of the _start function). -rebuild_goto_start_functiont::rebuild_goto_start_functiont( - message_handlert &_message_handler, +template +rebuild_goto_start_function_baset:: +rebuild_goto_start_function_baset( const cmdlinet &cmdline, - symbol_tablet &symbol_table, - goto_functionst &goto_functions): - messaget(_message_handler), + goto_modelt &goto_model, + message_handlert &message_handler): + messaget(message_handler), cmdline(cmdline), - symbol_table(symbol_table), - goto_functions(goto_functions) + goto_model(goto_model) { } @@ -44,7 +42,8 @@ rebuild_goto_start_functiont::rebuild_goto_start_functiont( /// called from _start /// \return Returns true if either the symbol is not found, or something went /// wrong with generating the start_function. False otherwise. -bool rebuild_goto_start_functiont::operator()() +template +bool rebuild_goto_start_function_baset::operator()() { const irep_idt &mode=get_entry_point_mode(); @@ -58,19 +57,12 @@ bool rebuild_goto_start_functiont::operator()() remove_existing_entry_point(); bool return_code= - language->generate_support_functions(symbol_table); + language->generate_support_functions(goto_model.symbol_table); - // Remove the function from the goto_functions so it is copied back in + // Remove the function from the goto functions so it is copied back in // from the symbol table during goto_convert if(!return_code) - { - const auto &start_function= - goto_functions.function_map.find(goto_functionst::entry_point()); - if(start_function!=goto_functions.function_map.end()) - { - goto_functions.function_map.erase(start_function); - } - } + goto_model.goto_functions.unload(goto_functionst::entry_point()); return return_code; } @@ -78,23 +70,27 @@ bool rebuild_goto_start_functiont::operator()() /// Find out the mode of the current entry point to determine the mode of the /// replacement entry point /// \return A mode string saying which language to use -irep_idt rebuild_goto_start_functiont::get_entry_point_mode() const +template +irep_idt +rebuild_goto_start_function_baset::get_entry_point_mode() const { const symbolt ¤t_entry_point= - *symbol_table.lookup(goto_functionst::entry_point()); + *goto_model.symbol_table.lookup(goto_functionst::entry_point()); return current_entry_point.mode; } /// Eliminate the existing entry point function symbol and any symbols created /// in that scope from the symbol table. -void rebuild_goto_start_functiont::remove_existing_entry_point() +template +void +rebuild_goto_start_function_baset::remove_existing_entry_point() { // Remove the function itself - symbol_table.remove(goto_functionst::entry_point()); + goto_model.symbol_table.remove(goto_functionst::entry_point()); // And any symbols created in the scope of the entry point std::vector entry_point_symbols; - for(const auto &symbol_entry : symbol_table.symbols) + for(const auto &symbol_entry : goto_model.symbol_table.symbols) { const bool is_entry_point_symbol= has_prefix( @@ -107,6 +103,9 @@ void rebuild_goto_start_functiont::remove_existing_entry_point() for(const irep_idt &entry_point_symbol : entry_point_symbols) { - symbol_table.remove(entry_point_symbol); + goto_model.symbol_table.remove(entry_point_symbol); } } + +template class rebuild_goto_start_function_baset; +template class rebuild_goto_start_function_baset; diff --git a/src/goto-programs/rebuild_goto_start_function.h b/src/goto-programs/rebuild_goto_start_function.h index 15516389fc4..08129bf3981 100644 --- a/src/goto-programs/rebuild_goto_start_function.h +++ b/src/goto-programs/rebuild_goto_start_function.h @@ -12,6 +12,9 @@ #include class cmdlinet; +#include "lazy_goto_model.h" + + class symbol_tablet; class goto_functionst; @@ -21,14 +24,14 @@ class goto_functionst; #define HELP_FUNCTIONS \ " --function name set main function name\n" -class rebuild_goto_start_functiont: public messaget +template +class rebuild_goto_start_function_baset: public messaget { public: - rebuild_goto_start_functiont( - message_handlert &_message_handler, + rebuild_goto_start_function_baset( const cmdlinet &cmdline, - symbol_tablet &symbol_table, - goto_functionst &goto_functions); + goto_modelt &goto_model, + message_handlert &message_handler); bool operator()(); @@ -38,8 +41,15 @@ class rebuild_goto_start_functiont: public messaget void remove_existing_entry_point(); const cmdlinet &cmdline; - symbol_tablet &symbol_table; - goto_functionst &goto_functions; + goto_modelt &goto_model; }; +// NOLINTNEXTLINE(readability/namespace) using required for templates +using rebuild_goto_start_functiont = + rebuild_goto_start_function_baset; + +// NOLINTNEXTLINE(readability/namespace) using required for templates +using rebuild_lazy_goto_start_functiont = + rebuild_goto_start_function_baset; + #endif // CPROVER_GOTO_PROGRAMS_REBUILD_GOTO_START_FUNCTION_H diff --git a/src/jbmc/jbmc_parse_options.cpp b/src/jbmc/jbmc_parse_options.cpp index 7d3da461fd5..07225a401de 100644 --- a/src/jbmc/jbmc_parse_options.cpp +++ b/src/jbmc/jbmc_parse_options.cpp @@ -26,7 +26,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include #include #include @@ -480,18 +480,20 @@ int jbmc_parse_optionst::doit() return 0; } - int get_goto_program_ret=get_goto_program(options); - + std::unique_ptr goto_model_ptr; + int get_goto_program_ret=get_goto_program(goto_model_ptr, options); if(get_goto_program_ret!=-1) return get_goto_program_ret; + goto_modelt &goto_model = *goto_model_ptr; + if(cmdline.isset("show-properties")) { show_properties(goto_model, ui_message_handler.get_ui()); return 0; // should contemplate EX_OK from sysexits.h } - if(set_properties()) + if(set_properties(goto_model)) return 7; // should contemplate EX_USAGE from sysexits.h // unwinds loops to number of enum elements @@ -529,10 +531,10 @@ int jbmc_parse_optionst::doit() prop_conv); // do actual BMC - return do_bmc(bmc); + return do_bmc(bmc, goto_model); } -bool jbmc_parse_optionst::set_properties() +bool jbmc_parse_optionst::set_properties(goto_modelt &goto_model) { try { @@ -561,6 +563,7 @@ bool jbmc_parse_optionst::set_properties() } int jbmc_parse_optionst::get_goto_program( + std::unique_ptr &goto_model, const optionst &options) { if(cmdline.args.empty()) @@ -571,28 +574,41 @@ int jbmc_parse_optionst::get_goto_program( try { - goto_model=initialize_goto_model(cmdline, get_message_handler()); + lazy_goto_modelt lazy_goto_model(get_message_handler()); + lazy_goto_model.initialize(cmdline); + + status() << "Generating GOTO Program" << messaget::eom; + lazy_goto_model.load_all_functions(); + // Show the symbol table before process_goto_functions mangles return + // values, etc if(cmdline.isset("show-symbol-table")) { - show_symbol_table(goto_model, ui_message_handler.get_ui()); + show_symbol_table( + lazy_goto_model.symbol_table, ui_message_handler.get_ui()); return 0; } - if(process_goto_program(options)) + // Move the model out of the local lazy_goto_model + // and into the caller's goto_model + goto_model=lazy_goto_modelt::freeze(std::move(lazy_goto_model)); + if(goto_model == nullptr) + return 6; + + if(process_goto_program(*goto_model, options)) return 6; // show it? if(cmdline.isset("show-loops")) { - show_loop_ids(ui_message_handler.get_ui(), goto_model); + show_loop_ids(ui_message_handler.get_ui(), *goto_model); return 0; } // show it? if(cmdline.isset("show-goto-functions")) { - show_goto_functions(goto_model, ui_message_handler.get_ui()); + show_goto_functions(*goto_model, ui_message_handler.get_ui()); return 0; } @@ -626,6 +642,7 @@ int jbmc_parse_optionst::get_goto_program( } bool jbmc_parse_optionst::process_goto_program( + goto_modelt &goto_model, const optionst &options) { try @@ -790,7 +807,7 @@ bool jbmc_parse_optionst::process_goto_program( } /// invoke main modules -int jbmc_parse_optionst::do_bmc(bmct &bmc) +int jbmc_parse_optionst::do_bmc(bmct &bmc, goto_modelt &goto_model) { bmc.set_ui(ui_message_handler.get_ui()); diff --git a/src/jbmc/jbmc_parse_options.h b/src/jbmc/jbmc_parse_options.h index 06916c296a9..442053b5760 100644 --- a/src/jbmc/jbmc_parse_options.h +++ b/src/jbmc/jbmc_parse_options.h @@ -79,15 +79,15 @@ class jbmc_parse_optionst: const std::string &extra_options); protected: - goto_modelt goto_model; ui_message_handlert ui_message_handler; void eval_verbosity(); void get_command_line_options(optionst &); - int get_goto_program(const optionst &); - bool process_goto_program(const optionst &); - bool set_properties(); - int do_bmc(bmct &); + int get_goto_program( + std::unique_ptr &goto_model, const optionst &); + bool process_goto_program(goto_modelt &goto_model, const optionst &); + bool set_properties(goto_modelt &goto_model); + int do_bmc(bmct &, goto_modelt &goto_model); }; #endif // CPROVER_JBMC_JBMC_PARSE_OPTIONS_H From 05a8da26aa479027d3b6f37d198c5405304bf46a Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Wed, 20 Sep 2017 14:33:12 +0100 Subject: [PATCH 02/21] Make goto_convert_functions not add directly to function map This won't be supported with lazy function loading as it won't use goto_functionst --- src/goto-cc/compile.cpp | 4 ++-- src/goto-programs/goto_convert_functions.cpp | 24 +++++++++----------- src/goto-programs/goto_convert_functions.h | 10 ++++---- 3 files changed, 18 insertions(+), 20 deletions(-) diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp index 9ace2924747..f81983a8793 100644 --- a/src/goto-cc/compile.cpp +++ b/src/goto-cc/compile.cpp @@ -691,7 +691,7 @@ void compilet::add_compiler_specific_defines(configt &config) const void compilet::convert_symbols(goto_functionst &dest) { - goto_convert_functionst converter(symbol_table, dest, get_message_handler()); + goto_convert_functionst converter(symbol_table, get_message_handler()); // the compilation may add symbols! @@ -724,7 +724,7 @@ 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); + converter.convert_function(s_it->first, dest.function_map[s_it->first]); symbol_table.get_writeable_ref(*it).value=exprt("compiled"); } } diff --git a/src/goto-programs/goto_convert_functions.cpp b/src/goto-programs/goto_convert_functions.cpp index 3efae701a9c..8a4f28c4dd7 100644 --- a/src/goto-programs/goto_convert_functions.cpp +++ b/src/goto-programs/goto_convert_functions.cpp @@ -21,10 +21,8 @@ Date: June 2003 goto_convert_functionst::goto_convert_functionst( symbol_tablet &_symbol_table, - goto_functionst &_functions, message_handlert &_message_handler): - goto_convertt(_symbol_table, _message_handler), - functions(_functions) + goto_convertt(_symbol_table, _message_handler) { } @@ -32,7 +30,7 @@ goto_convert_functionst::~goto_convert_functionst() { } -void goto_convert_functionst::goto_convert() +void goto_convert_functionst::goto_convert(goto_functionst &functions) { // warning! hash-table iterators are not stable @@ -53,7 +51,7 @@ void goto_convert_functionst::goto_convert() for(const auto &id : symbol_list) { - convert_function(id); + convert_function(id, functions.function_map[id]); } functions.compute_location_numbers(); @@ -135,10 +133,11 @@ void goto_convert_functionst::add_return( t->source_location=source_location; } -void goto_convert_functionst::convert_function(const irep_idt &identifier) +void goto_convert_functionst::convert_function( + const irep_idt &identifier, + goto_functionst::goto_functiont &f) { const symbolt &symbol=ns.lookup(identifier); - goto_functionst::goto_functiont &f=functions.function_map[identifier]; if(f.body_available()) return; // already converted @@ -240,12 +239,11 @@ void goto_convert( const unsigned errors_before= message_handler.get_message_count(messaget::M_ERROR); - goto_convert_functionst goto_convert_functions( - symbol_table, functions, message_handler); + goto_convert_functionst goto_convert_functions(symbol_table, message_handler); try { - goto_convert_functions.goto_convert(); + goto_convert_functions.goto_convert(functions); } catch(int) @@ -276,12 +274,12 @@ void goto_convert( const unsigned errors_before= message_handler.get_message_count(messaget::M_ERROR); - goto_convert_functionst goto_convert_functions( - symbol_table, functions, message_handler); + goto_convert_functionst goto_convert_functions(symbol_table, message_handler); try { - goto_convert_functions.convert_function(identifier); + goto_convert_functions.convert_function( + identifier, functions.function_map[identifier]); } catch(int) diff --git a/src/goto-programs/goto_convert_functions.h b/src/goto-programs/goto_convert_functions.h index 3162b453d0f..310d5e3c62c 100644 --- a/src/goto-programs/goto_convert_functions.h +++ b/src/goto-programs/goto_convert_functions.h @@ -16,6 +16,7 @@ Date: June 2003 #include "goto_model.h" #include "goto_convert_class.h" +#include "goto_functions.h" // convert it all! void goto_convert( @@ -38,19 +39,18 @@ void goto_convert( class goto_convert_functionst:public goto_convertt { public: - void goto_convert(); - void convert_function(const irep_idt &identifier); + void goto_convert(goto_functionst &functions); + void convert_function( + const irep_idt &identifier, + goto_functionst::goto_functiont &result); goto_convert_functionst( symbol_tablet &_symbol_table, - goto_functionst &_functions, message_handlert &_message_handler); virtual ~goto_convert_functionst(); protected: - goto_functionst &functions; - static bool hide(const goto_programt &); // From 0c05be676f813804844e425ea37d9593252ecd6e Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Thu, 14 Sep 2017 14:26:57 +0100 Subject: [PATCH 03/21] Allow convert_lazy_method on functions that don't have a lazy body The call will do nothing if a lazy body doesn't exist to be converted This allows calling for example on functions that will be stubbed --- src/util/language_file.h | 13 +++++-------- 1 file changed, 5 insertions(+), 8 deletions(-) diff --git a/src/util/language_file.h b/src/util/language_file.h index 19f644b8d44..dd24e071533 100644 --- a/src/util/language_file.h +++ b/src/util/language_file.h @@ -17,9 +17,8 @@ Author: Daniel Kroening, kroening@kroening.com #include // unique_ptr #include "message.h" +#include "symbol_table.h" -class symbol_tablet; -class symbol_table_baset; class language_filet; class languaget; @@ -92,11 +91,6 @@ class language_filest:public messaget bool interfaces(symbol_tablet &symbol_table); - bool has_lazy_method(const irep_idt &id) - { - return lazy_method_map.count(id)!=0; - } - // The method must have been added to the symbol table and registered // in lazy_method_map (currently always in language_filest::typecheck) // for this to be legal. @@ -104,7 +98,10 @@ class language_filest:public messaget const irep_idt &id, symbol_tablet &symbol_table) { - return lazy_method_map.at(id)->convert_lazy_method(id, symbol_table); + PRECONDITION(symbol_table.has_symbol(id)); + lazy_method_mapt::iterator it=lazy_method_map.find(id); + if(it!=lazy_method_map.end()) + it->second->convert_lazy_method(id, symbol_table); } void clear() From 7e1ecc9e82a4a70ba50292ddcdd314a85ddc1d1e Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Tue, 12 Dec 2017 11:31:30 +0000 Subject: [PATCH 04/21] Allow post-processing functions to run on a function-by-function basis --- src/goto-diff/goto_diff_parse_options.cpp | 2 +- src/goto-programs/remove_asm.cpp | 33 +++++------ src/goto-programs/remove_asm.h | 8 ++- src/goto-programs/remove_instanceof.cpp | 62 ++++++++++----------- src/goto-programs/remove_instanceof.h | 8 ++- src/goto-symex/adjust_float_expressions.cpp | 2 +- src/goto-symex/adjust_float_expressions.h | 7 ++- src/goto-symex/rewrite_union.cpp | 2 +- src/goto-symex/rewrite_union.h | 4 ++ 9 files changed, 68 insertions(+), 60 deletions(-) diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp index d439f1b9aa0..5b64f186749 100644 --- a/src/goto-diff/goto_diff_parse_options.cpp +++ b/src/goto-diff/goto_diff_parse_options.cpp @@ -396,7 +396,7 @@ bool goto_diff_parse_optionst::process_goto_program( // Remove inline assembler; this needs to happen before // adding the library. - remove_asm(symbol_table, goto_functions); + remove_asm(goto_model); // add the library link_to_library(symbol_table, goto_functions, ui_message_handler); diff --git a/src/goto-programs/remove_asm.cpp b/src/goto-programs/remove_asm.cpp index 29958434d48..98af6d6867c 100644 --- a/src/goto-programs/remove_asm.cpp +++ b/src/goto-programs/remove_asm.cpp @@ -25,27 +25,20 @@ Date: December 2014 class remove_asmt { public: - inline remove_asmt( - symbol_tablet &_symbol_table, - goto_functionst &_goto_functions): - symbol_table(_symbol_table), - goto_functions(_goto_functions) + explicit remove_asmt(symbol_tablet &_symbol_table) + : symbol_table(_symbol_table) { } - void operator()(); + void process_function(goto_functionst::goto_functiont &); protected: symbol_tablet &symbol_table; - goto_functionst &goto_functions; void process_instruction( goto_programt::instructiont &instruction, goto_programt &dest); - void process_function( - goto_functionst::goto_functiont &); - void gcc_asm_function_call( const irep_idt &function_base_name, const codet &code, @@ -305,24 +298,24 @@ void remove_asmt::process_function( } /// removes assembler -void remove_asmt::operator()() +void remove_asm( + goto_functionst::goto_functiont &goto_function, + symbol_tablet &symbol_table) { - Forall_goto_functions(it, goto_functions) - { - process_function(it->second); - } + remove_asmt rem(symbol_table); + rem.process_function(goto_function); } /// removes assembler -void remove_asm( - symbol_tablet &symbol_table, - goto_functionst &goto_functions) +void remove_asm(goto_functionst &goto_functions, symbol_tablet &symbol_table) { - remove_asmt(symbol_table, goto_functions)(); + remove_asmt rem(symbol_table); + for(auto &f : goto_functions.function_map) + rem.process_function(f.second); } /// removes assembler void remove_asm(goto_modelt &goto_model) { - remove_asmt(goto_model.symbol_table, goto_model.goto_functions)(); + remove_asm(goto_model.goto_functions, goto_model.symbol_table); } diff --git a/src/goto-programs/remove_asm.h b/src/goto-programs/remove_asm.h index 7717ba59ca0..913fe85c336 100644 --- a/src/goto-programs/remove_asm.h +++ b/src/goto-programs/remove_asm.h @@ -17,8 +17,12 @@ Date: December 2014 #include -void remove_asm(symbol_tablet &, goto_functionst &); +void remove_asm( + goto_functionst::goto_functiont &goto_function, + symbol_tablet &symbol_table); -void remove_asm(goto_modelt &); +void remove_asm(goto_functionst &goto_functions, symbol_tablet &symbol_table); + +void remove_asm(goto_modelt &goto_model); #endif // CPROVER_GOTO_PROGRAMS_REMOVE_ASM_H diff --git a/src/goto-programs/remove_instanceof.cpp b/src/goto-programs/remove_instanceof.cpp index 69db2a8859e..6d8a8de329b 100644 --- a/src/goto-programs/remove_instanceof.cpp +++ b/src/goto-programs/remove_instanceof.cpp @@ -22,26 +22,19 @@ Author: Chris Smowton, chris.smowton@diffblue.com class remove_instanceoft { public: - remove_instanceoft( - symbol_tablet &_symbol_table, - goto_functionst &_goto_functions): - symbol_table(_symbol_table), - ns(_symbol_table), - goto_functions(_goto_functions) + explicit remove_instanceoft(symbol_tablet &symbol_table) + : symbol_table(symbol_table), ns(symbol_table) { - class_hierarchy(_symbol_table); + class_hierarchy(symbol_table); } - // Lower instanceof for all functions: - void lower_instanceof(); + // Lower instanceof for a single functions + bool lower_instanceof(goto_programt &); protected: symbol_tablet &symbol_table; namespacet ns; class_hierarchyt class_hierarchy; - goto_functionst &goto_functions; - - bool lower_instanceof(goto_programt &); bool lower_instanceof(goto_programt &, goto_programt::targett); @@ -174,33 +167,38 @@ bool remove_instanceoft::lower_instanceof(goto_programt &goto_program) return true; } -/// See function above -/// \return Side-effects on this->goto_functions, replacing every instanceof in -/// every function with an explicit test. -void remove_instanceoft::lower_instanceof() + +/// Replace every instanceof in the passed function with an explicit +/// class-identifier test. +/// Extra auxiliary variables may be introduced into symbol_table. +/// \param function: The function to work on. +/// \param symbol_table: The symbol table to add symbols to. +void remove_instanceof( + goto_functionst::goto_functiont &function, + symbol_tablet &symbol_table) { - bool changed=false; - for(auto &f : goto_functions.function_map) - changed=(lower_instanceof(f.second.body) || changed); - if(changed) - goto_functions.compute_location_numbers(); + remove_instanceoft rem(symbol_table); + rem.lower_instanceof(function.body); } -/// See function above -/// \par parameters: `goto_functions`, a function map, and the corresponding -/// `symbol_table`. -/// \return Side-effects on goto_functions, replacing every instanceof in every -/// function with an explicit test. Extra auxiliary variables may be -/// introduced into `symbol_table`. +/// Replace every instanceof in every function with an explicit +/// class-identifier test. +/// Extra auxiliary variables may be introduced into symbol_table. +/// \param goto_functions: The functions to work on. +/// \param symbol_table: The symbol table to add symbols to. void remove_instanceof( - symbol_tablet &symbol_table, - goto_functionst &goto_functions) + goto_functionst &goto_functions, + symbol_tablet &symbol_table) { - remove_instanceoft rem(symbol_table, goto_functions); - rem.lower_instanceof(); + remove_instanceoft rem(symbol_table); + bool changed=false; + for(auto &f : goto_functions.function_map) + changed=rem.lower_instanceof(f.second.body) || changed; + if(changed) + goto_functions.compute_location_numbers(); } void remove_instanceof(goto_modelt &goto_model) { - remove_instanceof(goto_model.symbol_table, goto_model.goto_functions); + remove_instanceof(goto_model.goto_functions, goto_model.symbol_table); } diff --git a/src/goto-programs/remove_instanceof.h b/src/goto-programs/remove_instanceof.h index 15a02bf35b2..509b0157282 100644 --- a/src/goto-programs/remove_instanceof.h +++ b/src/goto-programs/remove_instanceof.h @@ -17,8 +17,12 @@ Author: Chris Smowton, chris.smowton@diffblue.com #include "goto_model.h" void remove_instanceof( - symbol_tablet &symbol_table, - goto_functionst &goto_functions); + goto_functionst::goto_functiont &function, + symbol_tablet &symbol_table); + +void remove_instanceof( + goto_functionst &goto_functions, + symbol_tablet &symbol_table); void remove_instanceof(goto_modelt &model); diff --git a/src/goto-symex/adjust_float_expressions.cpp b/src/goto-symex/adjust_float_expressions.cpp index f2b09db09ec..89abaf65757 100644 --- a/src/goto-symex/adjust_float_expressions.cpp +++ b/src/goto-symex/adjust_float_expressions.cpp @@ -179,7 +179,7 @@ void adjust_float_expressions( } } -static void adjust_float_expressions( +void adjust_float_expressions( goto_functionst::goto_functiont &goto_function, const namespacet &ns) { diff --git a/src/goto-symex/adjust_float_expressions.h b/src/goto-symex/adjust_float_expressions.h index 5cfd01d740f..bd011641d54 100644 --- a/src/goto-symex/adjust_float_expressions.h +++ b/src/goto-symex/adjust_float_expressions.h @@ -12,15 +12,20 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_GOTO_SYMEX_ADJUST_FLOAT_EXPRESSIONS_H #define CPROVER_GOTO_SYMEX_ADJUST_FLOAT_EXPRESSIONS_H +#include + class exprt; class namespacet; -class goto_functionst; class goto_modelt; void adjust_float_expressions( exprt &expr, const namespacet &ns); +void adjust_float_expressions( + goto_functionst::goto_functiont &goto_function, + const namespacet &ns); + void adjust_float_expressions( goto_functionst &goto_functions, const namespacet &ns); diff --git a/src/goto-symex/rewrite_union.cpp b/src/goto-symex/rewrite_union.cpp index e033188da4b..61cd69ee49b 100644 --- a/src/goto-symex/rewrite_union.cpp +++ b/src/goto-symex/rewrite_union.cpp @@ -107,7 +107,7 @@ void rewrite_union( } } -static void rewrite_union( +void rewrite_union( goto_functionst::goto_functiont &goto_function, const namespacet &ns) { diff --git a/src/goto-symex/rewrite_union.h b/src/goto-symex/rewrite_union.h index d2c9b1772b4..379e47c6b4d 100644 --- a/src/goto-symex/rewrite_union.h +++ b/src/goto-symex/rewrite_union.h @@ -23,6 +23,10 @@ void rewrite_union( exprt &expr, const namespacet &ns); +void rewrite_union( + goto_functionst::goto_functiont &goto_function, + const namespacet &ns); + void rewrite_union( goto_functionst &goto_functions, const namespacet &ns); From a659bc0c804840b3940ad2b83158fdb9ee61e8aa Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Thu, 14 Sep 2017 14:27:11 +0100 Subject: [PATCH 05/21] Add lazy_goto_functions_mapt Add lazy_goto_functions_mapt, a lazily populated function map, and use it in lazy_goto_modelt Allow post-processing functions run on a function-by-function basis Update lazy_goto_modelt to run module passes --- src/goto-programs/lazy_goto_functions_map.h | 161 ++++++++++++++++++++ src/goto-programs/lazy_goto_model.cpp | 46 +++++- src/goto-programs/lazy_goto_model.h | 53 ++++++- src/jbmc/jbmc_parse_options.cpp | 45 ++++-- src/jbmc/jbmc_parse_options.h | 6 +- 5 files changed, 287 insertions(+), 24 deletions(-) create mode 100644 src/goto-programs/lazy_goto_functions_map.h diff --git a/src/goto-programs/lazy_goto_functions_map.h b/src/goto-programs/lazy_goto_functions_map.h new file mode 100644 index 00000000000..5c749c2941a --- /dev/null +++ b/src/goto-programs/lazy_goto_functions_map.h @@ -0,0 +1,161 @@ +// Copyright 2016-2017 Diffblue Limited. All Rights Reserved. + +/// \file +/// A lazy wrapper for goto_functionst. + +#ifndef CPROVER_GOTO_PROGRAMS_LAZY_GOTO_FUNCTIONS_MAP_H +#define CPROVER_GOTO_PROGRAMS_LAZY_GOTO_FUNCTIONS_MAP_H + +#include +#include "goto_functions.h" +#include "goto_convert_functions.h" +#include +#include + + +/// Provides a wrapper for a map of lazily loaded goto_functiont. +/// This incrementally builds a goto-functions object, while permitting +/// access to goto programs while they are still under construction. +/// The intended workflow: +/// 1. The front-end registers the functions that are potentially +/// available, probably by use of util/language_files.h +/// 2. The main function registers functions that should be run on +/// each program, in sequence, after it is converted. +/// 3. Analyses will then access functions using the `at` function +/// \tparam bodyt: The type of the function bodies, usually goto_programt +template +class lazy_goto_functions_mapt final +{ +public: + // NOLINTNEXTLINE(readability/identifiers) - name matches those used in STL + typedef irep_idt key_type; + // NOLINTNEXTLINE(readability/identifiers) - name matches those used in STL + typedef goto_function_templatet &mapped_type; + /// The type of elements returned by const members + // NOLINTNEXTLINE(readability/identifiers) - name matches mapped_type + typedef const goto_function_templatet &const_mapped_type; + // NOLINTNEXTLINE(readability/identifiers) - name matches those used in STL + typedef std::pair> value_type; + // NOLINTNEXTLINE(readability/identifiers) - name matches those used in STL + typedef value_type &reference; + // NOLINTNEXTLINE(readability/identifiers) - name matches those used in STL + typedef const value_type &const_reference; + // NOLINTNEXTLINE(readability/identifiers) - name matches those used in STL + typedef value_type *pointer; + // NOLINTNEXTLINE(readability/identifiers) - name matches those used in STL + typedef const value_type *const_pointer; + // NOLINTNEXTLINE(readability/identifiers) - name matches those used in STL + typedef std::size_t size_type; + + typedef + std::function + post_process_functiont; + +private: + typedef std::map> underlying_mapt; + underlying_mapt &goto_functions; + /// Names of functions that are already fully available in the programt state. + /// \remarks These functions do not need processing before being returned + /// whenever they are requested + mutable std::unordered_set processed_functions; + + language_filest &language_files; + symbol_tablet &symbol_table; + // This is mutable because it has internal state that it changes during the + // course of conversion. Strictly it should make that state mutable or + // recreate it for each conversion, but it's easier just to store it mutable. + mutable goto_convert_functionst convert_functions; + const post_process_functiont post_process_function; + +public: + /// Creates a lazy_goto_functions_mapt. + lazy_goto_functions_mapt( + underlying_mapt &goto_functions, + language_filest &language_files, + symbol_tablet &symbol_table, + post_process_functiont post_process_function, + message_handlert &message_handler) + : goto_functions(goto_functions), + language_files(language_files), + symbol_table(symbol_table), + convert_functions(symbol_table, message_handler), + post_process_function(std::move(post_process_function)) + { + } + + /// Gets the number of functions in the map. + /// \return The number of functions in the map. + size_type size() const + { + return language_files.lazy_method_map.size(); + } + + /// Returns whether the map contains any mappings. + /// \return Whether the map contains any mappings. + bool empty() const { return language_files.lazy_method_map.empty(); } + + /// Checks whether a given function exists in the map. + /// \param name: The name of the function to search for. + /// \return True if the map contains the given function. + bool contains(const key_type &name) const + { + return language_files.lazy_method_map.count(name)!=0; + } + + /// Gets the body for a given function. + /// \param name: The name of the function to search for. + /// \return The function body corresponding to the given function. + const_mapped_type at(const key_type &name) const + { + return ensure_function_loaded_internal(name).second; + } + + /// Gets the body for a given function. + /// \param name: The name of the function to search for. + /// \return The function body corresponding to the given function. + mapped_type at(const key_type &name) + { + return ensure_function_loaded_internal(name).second; + } + + void unload(const key_type &name) const { goto_functions.erase(name); } + +private: + // This returns a non-const reference, but if you use this method from a + // const method then you should not return such a reference without making it + // const first + reference ensure_function_loaded_internal(const key_type &name) const + { + reference named_function=ensure_entry_converted(name); + mapped_type function=named_function.second; + if(processed_functions.count(name)==0) + { + // Run function-pass conversions + post_process_function(function); + // Assign procedure-local location numbers for now + function.body.compute_location_numbers(); + processed_functions.insert(name); + } + return named_function; + } + + reference ensure_entry_converted(const key_type &name) const + { + typename underlying_mapt::iterator it=goto_functions.find(name); + if(it!=goto_functions.end()) + return *it; + if(symbol_table.lookup_ref(name).value.is_nil()) + { + // Fill in symbol table entry body + // If this returns false then it's a stub + language_files.convert_lazy_method(name, symbol_table); + } + // Create goto_functiont + goto_functionst::goto_functiont function; + convert_functions.convert_function(name, function); + // Add to map + return *goto_functions.emplace(name, std::move(function)).first; + } +}; + +#endif // CPROVER_GOTO_PROGRAMS_LAZY_GOTO_FUNCTIONS_MAP_H diff --git a/src/goto-programs/lazy_goto_model.cpp b/src/goto-programs/lazy_goto_model.cpp index 811436eeb3a..da1ccd639cc 100644 --- a/src/goto-programs/lazy_goto_model.cpp +++ b/src/goto-programs/lazy_goto_model.cpp @@ -16,10 +16,24 @@ #include -lazy_goto_modelt::lazy_goto_modelt(message_handlert &message_handler) +//! @cond Doxygen_suppress_Lambda_in_initializer_list +lazy_goto_modelt::lazy_goto_modelt( + post_process_functiont post_process_function, + post_process_functionst post_process_functions, + message_handlert &message_handler) : goto_model(new goto_modelt()), symbol_table(goto_model->symbol_table), - goto_functions(goto_model->goto_functions), + goto_functions( + goto_model->goto_functions.function_map, + language_files, + symbol_table, + [this] (goto_functionst::goto_functiont &function) -> void + { + this->post_process_function(function, symbol_table); + }, + message_handler), + post_process_function(std::move(post_process_function)), + post_process_functions(std::move(post_process_functions)), message_handler(message_handler) { language_files.set_message_handler(message_handler); @@ -28,11 +42,22 @@ lazy_goto_modelt::lazy_goto_modelt(message_handlert &message_handler) lazy_goto_modelt::lazy_goto_modelt(lazy_goto_modelt &&other) : goto_model(std::move(other.goto_model)), symbol_table(goto_model->symbol_table), - goto_functions(goto_model->goto_functions), + goto_functions( + goto_model->goto_functions.function_map, + language_files, + symbol_table, + [this] (goto_functionst::goto_functiont &function) -> void + { + this->post_process_function(function, symbol_table); + }, + other.message_handler), language_files(std::move(other.language_files)), + post_process_function(std::move(other.post_process_function)), + post_process_functions(std::move(other.post_process_functions)), message_handler(other.message_handler) { } +//! @endcond void lazy_goto_modelt::initialize(const cmdlinet &cmdline) { @@ -115,15 +140,12 @@ void lazy_goto_modelt::initialize(const cmdlinet &cmdline) } } - for(const auto &file : binaries) + for(const std::string &file : binaries) { msg.status() << "Reading GOTO program from file" << messaget::eom; - if(read_object_and_link( - file, symbol_table, goto_functions, message_handler)) - { + if(read_object_and_link(file, *goto_model, message_handler)) throw 0; - } } bool binaries_provided_start = @@ -177,3 +199,11 @@ void lazy_goto_modelt::load_all_functions() const { goto_convert(*goto_model, message_handler); } + + +bool lazy_goto_modelt::finalize() +{ + language_files.clear(); + + return post_process_functions(*goto_model); +} diff --git a/src/goto-programs/lazy_goto_model.h b/src/goto-programs/lazy_goto_model.h index cf4404fd994..ddcbbe64718 100644 --- a/src/goto-programs/lazy_goto_model.h +++ b/src/goto-programs/lazy_goto_model.h @@ -9,16 +9,26 @@ #include #include "goto_model.h" +#include "lazy_goto_functions_map.h" #include "goto_convert_functions.h" class cmdlinet; +class optionst; /// Model that holds partially loaded map of functions class lazy_goto_modelt { public: - explicit lazy_goto_modelt(message_handlert &message_handler); + typedef std::function post_process_functiont; + typedef std::function post_process_functionst; + + explicit lazy_goto_modelt( + post_process_functiont post_process_function, + post_process_functionst post_process_functions, + message_handlert &message_handler); lazy_goto_modelt(lazy_goto_modelt &&other); @@ -29,6 +39,33 @@ class lazy_goto_modelt return *this; } + /// Create a lazy_goto_modelt from a object that defines function/module pass + /// handlers + /// \param handler: An object that defines the handlers + /// \param options: The options passed to process_goto_functions + /// \param message_handler: The message_handler to use for logging + /// \tparam THandler a type that defines methods process_goto_function and + /// process_goto_functions + template + static lazy_goto_modelt from_handler_object( + THandler &handler, + const optionst &options, + message_handlert &message_handler) + { + return lazy_goto_modelt( + [&handler] ( + goto_functionst::goto_functiont &function, + symbol_tablet &symbol_table) -> void + { + handler.process_goto_function(function, symbol_table); + }, + [&handler, &options] (goto_modelt &goto_model) -> bool + { + return handler.process_goto_functions(goto_model, options); + }, + message_handler); + } + void initialize(const cmdlinet &cmdline); /// Eagerly loads all functions from the symbol table. @@ -37,10 +74,14 @@ class lazy_goto_modelt /// The model returned here has access to the functions we've already /// loaded but is frozen in the sense that, with regard to the facility to /// load new functions, it has let it go. + /// Before freezing the functions all module-level passes are run /// \param model: The lazy_goto_modelt to freeze /// \returns The frozen goto_modelt or an empty optional if freezing fails - static std::unique_ptr freeze(lazy_goto_modelt &&model) + static std::unique_ptr process_whole_model_and_freeze( + lazy_goto_modelt &&model) { + if(model.finalize()) + return nullptr; return std::move(model.goto_model); } @@ -50,13 +91,19 @@ class lazy_goto_modelt public: /// Reference to symbol_table in the internal goto_model symbol_tablet &symbol_table; - goto_functionst &goto_functions; + const lazy_goto_functions_mapt goto_functions; private: language_filest language_files; + // Function/module processing functions + const post_process_functiont post_process_function; + const post_process_functionst post_process_functions; + /// Logging helper field message_handlert &message_handler; + + bool finalize(); }; #endif // CPROVER_GOTO_PROGRAMS_LAZY_GOTO_MODEL_H diff --git a/src/jbmc/jbmc_parse_options.cpp b/src/jbmc/jbmc_parse_options.cpp index 07225a401de..bf423b85af4 100644 --- a/src/jbmc/jbmc_parse_options.cpp +++ b/src/jbmc/jbmc_parse_options.cpp @@ -574,7 +574,8 @@ int jbmc_parse_optionst::get_goto_program( try { - lazy_goto_modelt lazy_goto_model(get_message_handler()); + lazy_goto_modelt lazy_goto_model=lazy_goto_modelt::from_handler_object( + *this, options, get_message_handler()); lazy_goto_model.initialize(cmdline); status() << "Generating GOTO Program" << messaget::eom; @@ -591,13 +592,11 @@ int jbmc_parse_optionst::get_goto_program( // Move the model out of the local lazy_goto_model // and into the caller's goto_model - goto_model=lazy_goto_modelt::freeze(std::move(lazy_goto_model)); + goto_model=lazy_goto_modelt::process_whole_model_and_freeze( + std::move(lazy_goto_model)); if(goto_model == nullptr) return 6; - if(process_goto_program(*goto_model, options)) - return 6; - // show it? if(cmdline.isset("show-loops")) { @@ -641,16 +640,41 @@ int jbmc_parse_optionst::get_goto_program( return -1; // no error, continue } -bool jbmc_parse_optionst::process_goto_program( - goto_modelt &goto_model, - const optionst &options) +void jbmc_parse_optionst::process_goto_function( + goto_functionst::goto_functiont &function, symbol_tablet &symbol_table) { try { // Remove inline assembler; this needs to happen before // adding the library. - remove_asm(goto_model); + remove_asm(function, symbol_table); + } + + catch(const char *e) + { + error() << e << eom; + throw; + } + catch(const std::string &e) + { + error() << e << eom; + throw; + } + + catch(const std::bad_alloc &) + { + error() << "Out of memory" << eom; + throw; + } +} + +bool jbmc_parse_optionst::process_goto_functions( + goto_modelt &goto_model, + const optionst &options) +{ + try + { // add the library link_to_library(goto_model, get_message_handler()); @@ -734,9 +758,6 @@ bool jbmc_parse_optionst::process_goto_program( // recalculate numbers, etc. goto_model.goto_functions.update(); - // add loop ids - goto_model.goto_functions.compute_loop_numbers(); - if(cmdline.isset("drop-unused-functions")) { // Entry point will have been set before and function pointers removed diff --git a/src/jbmc/jbmc_parse_options.h b/src/jbmc/jbmc_parse_options.h index 442053b5760..5c722e0821a 100644 --- a/src/jbmc/jbmc_parse_options.h +++ b/src/jbmc/jbmc_parse_options.h @@ -78,6 +78,10 @@ class jbmc_parse_optionst: const char **argv, const std::string &extra_options); + void process_goto_function( + goto_functionst::goto_functiont &function, symbol_tablet &symbol_table); + bool process_goto_functions(goto_modelt &goto_model, const optionst &options); + protected: ui_message_handlert ui_message_handler; @@ -85,7 +89,7 @@ class jbmc_parse_optionst: void get_command_line_options(optionst &); int get_goto_program( std::unique_ptr &goto_model, const optionst &); - bool process_goto_program(goto_modelt &goto_model, const optionst &); + bool set_properties(goto_modelt &goto_model); int do_bmc(bmct &, goto_modelt &goto_model); }; From aa5440b7ca1bf34213c9cbc2e3faf1fd4697dda3 Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Mon, 25 Sep 2017 16:28:55 +0100 Subject: [PATCH 06/21] Moved call to final to lazy_goto_modelt::finalize Explicitly load any functions added by call to final --- src/goto-programs/lazy_goto_functions_map.h | 5 +++++ src/goto-programs/lazy_goto_model.cpp | 25 ++++++++++++++++----- src/util/symbol.h | 5 +++++ 3 files changed, 29 insertions(+), 6 deletions(-) diff --git a/src/goto-programs/lazy_goto_functions_map.h b/src/goto-programs/lazy_goto_functions_map.h index 5c749c2941a..8f1bce86f84 100644 --- a/src/goto-programs/lazy_goto_functions_map.h +++ b/src/goto-programs/lazy_goto_functions_map.h @@ -120,6 +120,11 @@ class lazy_goto_functions_mapt final void unload(const key_type &name) const { goto_functions.erase(name); } + void ensure_function_loaded(const key_type &name) const + { + ensure_function_loaded_internal(name); + } + private: // This returns a non-const reference, but if you use this method from a // const method then you should not return such a reference without making it diff --git a/src/goto-programs/lazy_goto_model.cpp b/src/goto-programs/lazy_goto_model.cpp index da1ccd639cc..685cdc85da8 100644 --- a/src/goto-programs/lazy_goto_model.cpp +++ b/src/goto-programs/lazy_goto_model.cpp @@ -11,6 +11,7 @@ #include #include +#include #include #include @@ -184,12 +185,6 @@ void lazy_goto_modelt::initialize(const cmdlinet &cmdline) throw 0; } - if(language_files.final(symbol_table)) - { - msg.error() << "FINAL STAGE CONVERSION ERROR" << messaget::eom; - throw 0; - } - // stupid hack config.set_object_bits_from_symbol_table(symbol_table); } @@ -203,6 +198,24 @@ void lazy_goto_modelt::load_all_functions() const bool lazy_goto_modelt::finalize() { + messaget msg(message_handler); + journalling_symbol_tablet symbol_table= + journalling_symbol_tablet::wrap(this->symbol_table); + if(language_files.final(symbol_table)) + { + msg.error() << "CONVERSION ERROR" << messaget::eom; + return true; + } + for(const irep_idt &updated_symbol_id : symbol_table.get_updated()) + { + if(symbol_table.lookup_ref(updated_symbol_id).is_function()) + { + // Re-convert any that already exist + goto_functions.unload(updated_symbol_id); + goto_functions.ensure_function_loaded(updated_symbol_id); + } + } + language_files.clear(); return post_process_functions(*goto_model); diff --git a/src/util/symbol.h b/src/util/symbol.h index 7edae3146c0..06945fc6c1f 100644 --- a/src/util/symbol.h +++ b/src/util/symbol.h @@ -109,6 +109,11 @@ class symbolt { return !is_static_lifetime; } + + bool is_function() const + { + return !is_type && !is_macro && type.id()==ID_code; + } }; std::ostream &operator<<(std::ostream &out, const symbolt &symbol); From 5f06e366e09fd8757c0d5373e6b8b04fad7bb557 Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Thu, 28 Sep 2017 18:56:40 +0100 Subject: [PATCH 07/21] Recreate initialize in final Creates the initialize methods again taking account of symbols added to the symbol table during instantiation of lazy methods since they were first created. --- src/java_bytecode/java_bytecode_language.cpp | 8 +++- src/java_bytecode/java_entry_point.cpp | 42 ++++++++++++++++++++ src/java_bytecode/java_entry_point.h | 8 ++++ 3 files changed, 57 insertions(+), 1 deletion(-) diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index 630bfaae078..f69a48d42c6 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/src/java_bytecode/java_bytecode_language.cpp @@ -466,7 +466,13 @@ bool java_bytecode_languaget::final(symbol_table_baset &symbol_table) { PRECONDITION(language_options_initialized); - return false; + return recreate_initialize( + symbol_table, + main_class, + get_message_handler(), + assume_inputs_non_null, + object_factory_parameters, + get_pointer_type_selector()); } void java_bytecode_languaget::show_parse(std::ostream &out) diff --git a/src/java_bytecode/java_entry_point.cpp b/src/java_bytecode/java_entry_point.cpp index 1a2b83911f1..5343358a53c 100644 --- a/src/java_bytecode/java_entry_point.cpp +++ b/src/java_bytecode/java_entry_point.cpp @@ -485,6 +485,48 @@ bool java_entry_point( pointer_type_selector); } +/// Creates the initialize methods again taking account of symbols added to the +/// symbol table during instantiation of lazy methods since they were first +/// created, +/// \param symbol_table: global symbol table containing symbols to initialize +/// \param main_class: the class containing the "main" entry point +/// \param message_handler: message_handlert for logging +/// \param assume_init_pointers_not_null: specifies behaviour for +/// java_static_lifetime_init +/// \param object_factory_parameters: specifies behaviour for +/// java_static_lifetime_init +/// \param pointer_type_selector: specifies behaviour for +/// java_static_lifetime_init +bool recreate_initialize( + symbol_table_baset &symbol_table, + const irep_idt &main_class, + message_handlert &message_handler, + bool assume_init_pointers_not_null, + const object_factory_parameterst &object_factory_parameters, + const select_pointer_typet &pointer_type_selector) +{ + messaget message(message_handler); + main_function_resultt res= + get_main_symbol(symbol_table, main_class, message_handler); + if(res.status!=main_function_resultt::Success) + { + // No initialization was originally created (yikes!) so we can't recreate + // it now + return res.status==main_function_resultt::Error; + } + + create_initialize(symbol_table); + + java_static_lifetime_init( + symbol_table, + res.main_function.location, + assume_init_pointers_not_null, + object_factory_parameters, + pointer_type_selector); + + return false; +} + /// Generate a _start function for a specific function. See /// java_entry_point for more details. /// \param symbol: The symbol representing the function to call diff --git a/src/java_bytecode/java_entry_point.h b/src/java_bytecode/java_entry_point.h index 8a21df6d389..9e776ebce69 100644 --- a/src/java_bytecode/java_entry_point.h +++ b/src/java_bytecode/java_entry_point.h @@ -74,4 +74,12 @@ bool generate_java_start_function( const object_factory_parameterst& object_factory_parameters, const select_pointer_typet &pointer_type_selector); +bool recreate_initialize( + symbol_table_baset &symbol_table, + const irep_idt &main_class, + message_handlert &message_handler, + bool assume_init_pointers_not_null, + const object_factory_parameterst &object_factory_parameters, + const select_pointer_typet &pointer_type_selector); + #endif // CPROVER_JAVA_BYTECODE_JAVA_ENTRY_POINT_H From 2ba1364faa2a82762944e954274ad430fa240906 Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Mon, 25 Sep 2017 16:49:09 +0100 Subject: [PATCH 08/21] Update load_all_functions Made load_all_functions compatible with some functions having already been loaded by using the lazy load procedure --- src/goto-programs/lazy_goto_model.cpp | 26 ++++++++++++++++++++++++-- 1 file changed, 24 insertions(+), 2 deletions(-) diff --git a/src/goto-programs/lazy_goto_model.cpp b/src/goto-programs/lazy_goto_model.cpp index 685cdc85da8..d2162e57de6 100644 --- a/src/goto-programs/lazy_goto_model.cpp +++ b/src/goto-programs/lazy_goto_model.cpp @@ -192,9 +192,31 @@ void lazy_goto_modelt::initialize(const cmdlinet &cmdline) /// Eagerly loads all functions from the symbol table. void lazy_goto_modelt::load_all_functions() const { - goto_convert(*goto_model, message_handler); -} + symbol_tablet::symbolst::size_type table_size; + symbol_tablet::symbolst::size_type new_table_size=symbol_table.symbols.size(); + do + { + table_size=new_table_size; + + // Find symbols that correspond to functions + std::vector fn_ids_to_convert; + for(const auto &named_symbol : symbol_table.symbols) + { + if(named_symbol.second.is_function()) + fn_ids_to_convert.push_back(named_symbol.first); + } + + for(const irep_idt &symbol_name : fn_ids_to_convert) + goto_functions.ensure_function_loaded(symbol_name); + // Repeat while new symbols are being added in case any of those are + // stubbed functions. Even stubs can create new stubs while being + // converted if they are special stubs (e.g. string functions) + new_table_size=symbol_table.symbols.size(); + } while(new_table_size!=table_size); + + goto_model->goto_functions.compute_location_numbers(); +} bool lazy_goto_modelt::finalize() { From e3e44c8f504c86efd8e80f670d3c86c7016125f4 Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Wed, 20 Sep 2017 10:50:02 +0100 Subject: [PATCH 09/21] Do type-checking as a function pass After convert each function in convert_lazy_method call instrument and typecheck --- .../java_bytecode_instrument.cpp | 4 ++- src/java_bytecode/java_bytecode_language.cpp | 25 ++++++++++++-- src/java_bytecode/java_bytecode_typecheck.cpp | 33 ++++++++++++------- src/java_bytecode/java_bytecode_typecheck.h | 14 +++++--- 4 files changed, 58 insertions(+), 18 deletions(-) diff --git a/src/java_bytecode/java_bytecode_instrument.cpp b/src/java_bytecode/java_bytecode_instrument.cpp index a5981a913c5..b0bb08ef14b 100644 --- a/src/java_bytecode/java_bytecode_instrument.cpp +++ b/src/java_bytecode/java_bytecode_instrument.cpp @@ -598,7 +598,9 @@ void java_bytecode_instrument_symbol( message_handler); INVARIANT( symbol.value.id()==ID_code, - "java_bytecode_instrument expects a code-typed symbol"); + "java_bytecode_instrument expects a code-typed symbol but was called with" + " " + id2string(symbol.name) + " which has a value with an id of " + + id2string(symbol.value.id())); instrument(symbol.value); } diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index f69a48d42c6..9aea518c80c 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/src/java_bytecode/java_bytecode_language.cpp @@ -372,12 +372,33 @@ void java_bytecode_languaget::methods_provided(id_sett &methods) const /// to have a value representing the method body identical to that produced /// using eager method conversion. /// \param function_id: method ID to convert -/// \param symbol_table: global symbol table +/// \param symtab: global symbol table void java_bytecode_languaget::convert_lazy_method( const irep_idt &function_id, - symbol_tablet &symbol_table) + symbol_tablet &symtab) { + const symbolt &symbol = symtab.lookup_ref(function_id); + if(symbol.value.is_not_nil()) + return; + + journalling_symbol_tablet symbol_table= + journalling_symbol_tablet::wrap(symtab); + convert_single_method(function_id, symbol_table); + + // Instrument runtime exceptions (unless symbol is a stub) + if(symbol.value.is_not_nil()) + { + java_bytecode_instrument_symbol( + symbol_table, + symbol_table.get_writeable_ref(function_id), + throw_runtime_exceptions, + get_message_handler()); + } + + // now typecheck this function + java_bytecode_typecheck_updated_symbols( + symbol_table, get_message_handler(), string_refinement_enabled); } /// \brief Convert a method (one whose type is known but whose body hasn't diff --git a/src/java_bytecode/java_bytecode_typecheck.cpp b/src/java_bytecode/java_bytecode_typecheck.cpp index e7f096c8333..36d9e170068 100644 --- a/src/java_bytecode/java_bytecode_typecheck.cpp +++ b/src/java_bytecode/java_bytecode_typecheck.cpp @@ -38,34 +38,35 @@ void java_bytecode_typecheckt::typecheck() { // The hash table iterators are not stable, // and we might add new symbols. - - std::vector identifiers; + journalling_symbol_tablet::changesett identifiers; identifiers.reserve(symbol_table.symbols.size()); forall_symbols(s_it, symbol_table.symbols) - identifiers.push_back(s_it->first); + identifiers.insert(s_it->first); + typecheck(identifiers); +} +void java_bytecode_typecheckt::typecheck( + const journalling_symbol_tablet::changesett &identifiers) +{ // We first check all type symbols, // recursively doing base classes first. for(const irep_idt &id : identifiers) { symbolt &symbol=*symbol_table.get_writeable(id); - if(!symbol.is_type) - continue; - typecheck_type_symbol(symbol); + if(symbol.is_type) + typecheck_type_symbol(symbol); } - // We now check all non-type symbols for(const irep_idt &id : identifiers) { symbolt &symbol=*symbol_table.get_writeable(id); - if(symbol.is_type) - continue; - typecheck_non_type_symbol(symbol); + if(!symbol.is_type) + typecheck_non_type_symbol(symbol); } } bool java_bytecode_typecheck( - symbol_tablet &symbol_table, + symbol_table_baset &symbol_table, message_handlert &message_handler, bool string_refinement_enabled) { @@ -74,6 +75,16 @@ bool java_bytecode_typecheck( return java_bytecode_typecheck.typecheck_main(); } +void java_bytecode_typecheck_updated_symbols( + journalling_symbol_tablet &symbol_table, + message_handlert &message_handler, + bool string_refinement_enabled) +{ + java_bytecode_typecheckt java_bytecode_typecheck( + symbol_table, message_handler, string_refinement_enabled); + return java_bytecode_typecheck.typecheck(symbol_table.get_updated()); +} + bool java_bytecode_typecheck( exprt &expr, message_handlert &message_handler, diff --git a/src/java_bytecode/java_bytecode_typecheck.h b/src/java_bytecode/java_bytecode_typecheck.h index fa35ba5eda9..29175fe875c 100644 --- a/src/java_bytecode/java_bytecode_typecheck.h +++ b/src/java_bytecode/java_bytecode_typecheck.h @@ -15,7 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include #include #include @@ -23,7 +23,12 @@ Author: Daniel Kroening, kroening@kroening.com #include bool java_bytecode_typecheck( - symbol_tablet &symbol_table, + symbol_table_baset &symbol_table, + message_handlert &message_handler, + bool string_refinement_enabled); + +void java_bytecode_typecheck_updated_symbols( + journalling_symbol_tablet &symbol_table, message_handlert &message_handler, bool string_refinement_enabled); @@ -36,7 +41,7 @@ class java_bytecode_typecheckt:public typecheckt { public: java_bytecode_typecheckt( - symbol_tablet &_symbol_table, + symbol_table_baset &_symbol_table, message_handlert &_message_handler, bool _string_refinement_enabled): typecheckt(_message_handler), @@ -49,10 +54,11 @@ class java_bytecode_typecheckt:public typecheckt virtual ~java_bytecode_typecheckt() { } virtual void typecheck(); + void typecheck(const journalling_symbol_tablet::changesett &identifiers); virtual void typecheck_expr(exprt &expr); protected: - symbol_tablet &symbol_table; + symbol_table_baset &symbol_table; const namespacet ns; bool string_refinement_enabled; From 87c6b28bc86e3455cddad9eb2ee05b6a79825baf Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Fri, 29 Sep 2017 12:33:44 +0100 Subject: [PATCH 10/21] Don't erase symbol in java_bytecode_convert_methodt::convert The symbolt was erased and recreated rather than being modified. This was bad as it invalidated the reference to the symbol that we now use later. --- .../java_bytecode_convert_method.cpp | 29 +++++++++---------- 1 file changed, 13 insertions(+), 16 deletions(-) diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index ac6bceab861..fb9b18bd871 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -382,11 +382,11 @@ void java_bytecode_convert_methodt::convert( id2string(class_symbol.name)+"."+id2string(m.name)+":"+m.descriptor; method_id=method_identifier; - const symbolt &old_sym=*symbol_table.lookup(method_identifier); + symbolt &method_symbol=*symbol_table.get_writeable(method_identifier); // Obtain a std::vector of code_typet::parametert objects from the // (function) type of the symbol - typet member_type=old_sym.type; + typet member_type=method_symbol.type; code_typet &code_type=to_code_type(member_type); method_return_type=code_type.return_type(); code_typet::parameterst ¶meters=code_type.parameters(); @@ -527,10 +527,17 @@ void java_bytecode_convert_methodt::convert( if(is_constructor(method)) method.set(ID_constructor, true); - // we add the symbol for the method - symbolt method_symbol; - method_symbol.name=method.get_name(); - method_symbol.base_name=method.get_base_name(); + // Check the fields that can't change are valid + INVARIANT( + method_symbol.name==method.get_name(), + "Name of method symbol shouldn't change"); + INVARIANT( + method_symbol.base_name==method.get_base_name(), + "Base name of method symbol shouldn't change"); + INVARIANT( + method_symbol.module.empty(), + "Method symbol shouldn't have module"); + // Update the symbol for the method method_symbol.mode=ID_java; method_symbol.location=m.source_location; method_symbol.location.set_function(method_identifier); @@ -554,16 +561,6 @@ void java_bytecode_convert_methodt::convert( method_has_this=code_type.has_this(); if((!m.is_abstract) && (!m.is_native)) method_symbol.value=convert_instructions(m, code_type, method_symbol.name); - - // Replace the existing stub symbol with the real deal: - const auto s_it=symbol_table.symbols.find(method.get_name()); - INVARIANT( - s_it!=symbol_table.symbols.end(), - "the symbol was there earlier on this function; it must be there now"); - symbol_table.erase(s_it); - - // Insert the method symbol in the symbol table - symbol_table.add(method_symbol); } const bytecode_infot &java_bytecode_convert_methodt::get_bytecode_info( From c938b08adf8ec3558e4104f4e803756ae6ebffd3 Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Thu, 28 Sep 2017 11:41:56 +0100 Subject: [PATCH 11/21] Encapsulate maps in language_filest --- src/goto-cc/compile.cpp | 11 ++----- src/goto-programs/initialize_goto_model.cpp | 8 +---- src/goto-programs/lazy_goto_functions_map.h | 19 ------------ src/goto-programs/lazy_goto_model.cpp | 7 +---- src/langapi/language_ui.cpp | 8 +---- src/util/language_file.cpp | 5 +++- src/util/language_file.h | 33 +++++++++++++++++---- 7 files changed, 37 insertions(+), 54 deletions(-) diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp index f81983a8793..63ef74ee201 100644 --- a/src/goto-cc/compile.cpp +++ b/src/goto-cc/compile.cpp @@ -483,14 +483,7 @@ bool compilet::parse(const std::string &file_name) languagep->set_message_handler(get_message_handler()); - language_filet language_file; - - std::pair - res=language_files.file_map.insert( - std::pair(file_name, language_file)); - - language_filet &lf=res.first->second; - lf.filename=file_name; + language_filet &lf=language_files.add_file(file_name); lf.language=std::move(languagep); if(mode==PREPROCESS_ONLY) @@ -640,7 +633,7 @@ bool compilet::parse_source(const std::string &file_name) return true; // so we remove it from the list afterwards - language_files.file_map.erase(file_name); + language_files.remove_file(file_name); return false; } diff --git a/src/goto-programs/initialize_goto_model.cpp b/src/goto-programs/initialize_goto_model.cpp index d5ec80461e1..13953d721b4 100644 --- a/src/goto-programs/initialize_goto_model.cpp +++ b/src/goto-programs/initialize_goto_model.cpp @@ -72,13 +72,7 @@ goto_modelt initialize_goto_model( throw 0; } - std::pair - result=language_files.file_map.insert( - std::pair(filename, language_filet())); - - language_filet &lf=result.first->second; - - lf.filename=filename; + language_filet &lf=language_files.add_file(filename); lf.language=get_language_from_filename(filename); if(lf.language==nullptr) diff --git a/src/goto-programs/lazy_goto_functions_map.h b/src/goto-programs/lazy_goto_functions_map.h index 8f1bce86f84..629af8a0630 100644 --- a/src/goto-programs/lazy_goto_functions_map.h +++ b/src/goto-programs/lazy_goto_functions_map.h @@ -83,25 +83,6 @@ class lazy_goto_functions_mapt final { } - /// Gets the number of functions in the map. - /// \return The number of functions in the map. - size_type size() const - { - return language_files.lazy_method_map.size(); - } - - /// Returns whether the map contains any mappings. - /// \return Whether the map contains any mappings. - bool empty() const { return language_files.lazy_method_map.empty(); } - - /// Checks whether a given function exists in the map. - /// \param name: The name of the function to search for. - /// \return True if the map contains the given function. - bool contains(const key_type &name) const - { - return language_files.lazy_method_map.count(name)!=0; - } - /// Gets the body for a given function. /// \param name: The name of the function to search for. /// \return The function body corresponding to the given function. diff --git a/src/goto-programs/lazy_goto_model.cpp b/src/goto-programs/lazy_goto_model.cpp index d2162e57de6..5aea7a9e944 100644 --- a/src/goto-programs/lazy_goto_model.cpp +++ b/src/goto-programs/lazy_goto_model.cpp @@ -100,12 +100,7 @@ void lazy_goto_modelt::initialize(const cmdlinet &cmdline) throw 0; } - std::pair result = - language_files.file_map.emplace(filename, language_filet()); - - language_filet &lf=result.first->second; - - lf.filename=filename; + language_filet &lf=language_files.add_file(filename); lf.language=get_language_from_filename(filename); if(lf.language==nullptr) diff --git a/src/langapi/language_ui.cpp b/src/langapi/language_ui.cpp index 0d515d81afb..560fd43bb89 100644 --- a/src/langapi/language_ui.cpp +++ b/src/langapi/language_ui.cpp @@ -58,13 +58,7 @@ bool language_uit::parse(const std::string &filename) return true; } - std::pair - result=language_files.file_map.insert( - std::pair(filename, language_filet())); - - language_filet &lf=result.first->second; - - lf.filename=filename; + language_filet &lf=language_files.add_file(filename); lf.language=get_language_from_filename(filename); if(lf.language==nullptr) diff --git a/src/util/language_file.cpp b/src/util/language_file.cpp index f42e7f88159..559648182aa 100644 --- a/src/util/language_file.cpp +++ b/src/util/language_file.cpp @@ -25,7 +25,10 @@ language_filet::language_filet(const language_filet &rhs): /// destructor in the source file, where the full definition is availible. language_filet::~language_filet()=default; -language_filet::language_filet()=default; +language_filet::language_filet(const std::string &filename) + : filename(filename) +{ +} void language_filet::get_modules() { diff --git a/src/util/language_file.h b/src/util/language_file.h index dd24e071533..6c32c68496a 100644 --- a/src/util/language_file.h +++ b/src/util/language_file.h @@ -18,9 +18,9 @@ Author: Daniel Kroening, kroening@kroening.com #include "message.h" #include "symbol_table.h" +#include "language.h" class language_filet; -class languaget; class language_modulet final { @@ -51,7 +51,7 @@ class language_filet final const irep_idt &id, symbol_tablet &symbol_table); - language_filet(); + explicit language_filet(const std::string &filename); language_filet(const language_filet &rhs); ~language_filet(); @@ -59,21 +59,44 @@ class language_filet final class language_filest:public messaget { -public: +private: typedef std::map file_mapt; file_mapt file_map; - // Contains pointers into file_mapt! typedef std::map module_mapt; module_mapt module_map; - // Contains pointers into filemapt! + // Contains pointers into file_map! // This is safe-ish as long as this is std::map. typedef std::map lazy_method_mapt; lazy_method_mapt lazy_method_map; +public: + language_filet &add_file(const std::string &filename) + { + language_filet language_file(filename); + return file_map.emplace(filename, std::move(language_file)).first->second; + } + + void remove_file(const std::string &filename) + { + // Clear relevant entries from lazy_method_map + language_filet *language_file = &file_map.at(filename); + id_sett files_methods; + for(const std::pair &method : lazy_method_map) + { + if(method.second == language_file) + files_methods.insert(method.first); + } + for(const irep_idt &method_name : files_methods) + lazy_method_map.erase(method_name); + + file_map.erase(filename); + } + void clear_files() { + lazy_method_map.clear(); file_map.clear(); } From 7e52e22dac5029726f2e4036d69ba203507748dc Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Thu, 28 Sep 2017 18:47:16 +0100 Subject: [PATCH 12/21] Always allow the main function not to have a body --- src/java_bytecode/ci_lazy_methods.cpp | 2 +- src/java_bytecode/java_entry_point.cpp | 25 ++----------------------- src/java_bytecode/java_entry_point.h | 3 +-- 3 files changed, 4 insertions(+), 26 deletions(-) diff --git a/src/java_bytecode/ci_lazy_methods.cpp b/src/java_bytecode/ci_lazy_methods.cpp index 4c108ba51b0..dd434acb372 100644 --- a/src/java_bytecode/ci_lazy_methods.cpp +++ b/src/java_bytecode/ci_lazy_methods.cpp @@ -73,7 +73,7 @@ bool ci_lazy_methodst::operator()( std::vector method_worklist2; main_function_resultt main_function = - get_main_symbol(symbol_table, main_class, get_message_handler(), true); + get_main_symbol(symbol_table, main_class, get_message_handler()); if(!main_function.is_success()) { // Failed, mark all functions in the given main class(es) diff --git a/src/java_bytecode/java_entry_point.cpp b/src/java_bytecode/java_entry_point.cpp index 5343358a53c..eab1a397286 100644 --- a/src/java_bytecode/java_entry_point.cpp +++ b/src/java_bytecode/java_entry_point.cpp @@ -321,8 +321,7 @@ void java_record_outputs( main_function_resultt get_main_symbol( const symbol_table_baset &symbol_table, const irep_idt &main_class, - message_handlert &message_handler, - bool allow_no_body) + message_handlert &message_handler) { messaget message(message_handler); @@ -348,14 +347,6 @@ main_function_resultt get_main_symbol( symbol != nullptr, "resolve_friendly_method_name should return a symbol-table identifier"); - // check if it has a body - if(symbol->value.is_nil() && !allow_no_body) - { - message.error() - << "main method `" << main_class << "' has no body" << messaget::eom; - return main_function_resultt::Error; - } - return *symbol; // Return found function } else @@ -395,18 +386,7 @@ main_function_resultt get_main_symbol( return main_function_resultt::Error; // give up with error, no main } - // function symbol - const symbolt &symbol = **matches.begin(); - - // check if it has a body - if(symbol.value.is_nil() && !allow_no_body) - { - message.error() - << "main method `" << main_class << "' has no body" << messaget::eom; - return main_function_resultt::Error; // give up with error - } - - return symbol; // Return found function + return **matches.begin(); // Return found function } } @@ -464,7 +444,6 @@ bool java_entry_point( return true; symbolt symbol=res.main_function; - assert(!symbol.value.is_nil()); assert(symbol.type.id()==ID_code); create_initialize(symbol_table); diff --git a/src/java_bytecode/java_entry_point.h b/src/java_bytecode/java_entry_point.h index 9e776ebce69..98495c72a5a 100644 --- a/src/java_bytecode/java_entry_point.h +++ b/src/java_bytecode/java_entry_point.h @@ -63,8 +63,7 @@ struct main_function_resultt main_function_resultt get_main_symbol( const symbol_table_baset &symbol_table, const irep_idt &main_class, - message_handlert &, - bool allow_no_body = false); + message_handlert &); bool generate_java_start_function( const symbolt &symbol, From 377978257bae703bb3cbfddf66d81b146aa6d0ae Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Fri, 17 Nov 2017 17:23:43 +0000 Subject: [PATCH 13/21] Always convert the main function from bytecode into the symbol_table Load the main function into the symbol table before generating the entry point so that we have access to its parameter names Allow attempts to load a function already loaded for non-lazy cases --- src/goto-programs/lazy_goto_functions_map.h | 9 +++------ src/java_bytecode/java_bytecode_language.cpp | 4 ++++ 2 files changed, 7 insertions(+), 6 deletions(-) diff --git a/src/goto-programs/lazy_goto_functions_map.h b/src/goto-programs/lazy_goto_functions_map.h index 629af8a0630..5df717b5088 100644 --- a/src/goto-programs/lazy_goto_functions_map.h +++ b/src/goto-programs/lazy_goto_functions_map.h @@ -130,12 +130,9 @@ class lazy_goto_functions_mapt final typename underlying_mapt::iterator it=goto_functions.find(name); if(it!=goto_functions.end()) return *it; - if(symbol_table.lookup_ref(name).value.is_nil()) - { - // Fill in symbol table entry body - // If this returns false then it's a stub - language_files.convert_lazy_method(name, symbol_table); - } + // Fill in symbol table entry body if not already done + // If this returns false then it's a stub + language_files.convert_lazy_method(name, symbol_table); // Create goto_functiont goto_functionst::goto_functiont function; convert_functions.convert_function(name, function); diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index 9aea518c80c..73c23711f03 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/src/java_bytecode/java_bytecode_language.cpp @@ -295,6 +295,10 @@ bool java_bytecode_languaget::generate_support_functions( if(!res.is_success()) return res.is_error(); + // Load the main function into the symbol table to get access to its + // parameter names + convert_lazy_method(res.main_function.name, symbol_table); + // generate the test harness in __CPROVER__start and a call the entry point return java_entry_point( From 166563fe74426954f9bc860f62e1e3babc3450de Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Mon, 2 Oct 2017 09:59:33 +0100 Subject: [PATCH 14/21] Do lowering of java_new as a function-level pass --- src/clobber/clobber_parse_options.cpp | 3 + .../goto_analyzer_parse_options.cpp | 3 + src/goto-diff/goto_diff_parse_options.cpp | 3 + src/goto-programs/Makefile | 1 + src/goto-programs/builtin_functions.cpp | 63 +---------- src/goto-programs/class_identifier.cpp | 36 ++++++ src/goto-programs/class_identifier.h | 6 + src/goto-programs/goto_convert.cpp | 5 +- src/goto-programs/goto_convert_class.h | 5 - src/goto-programs/remove_java_new.cpp | 105 ++++++++++++++++++ src/goto-programs/remove_java_new.h | 29 +++++ src/jbmc/jbmc_parse_options.cpp | 3 + 12 files changed, 191 insertions(+), 71 deletions(-) create mode 100644 src/goto-programs/remove_java_new.cpp create mode 100644 src/goto-programs/remove_java_new.h diff --git a/src/clobber/clobber_parse_options.cpp b/src/clobber/clobber_parse_options.cpp index bfad81dd7da..fe5886721a0 100644 --- a/src/clobber/clobber_parse_options.cpp +++ b/src/clobber/clobber_parse_options.cpp @@ -32,6 +32,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include @@ -207,6 +208,8 @@ bool clobber_parse_optionst::process_goto_program( goto_modelt &goto_model) { { + remove_java_new(goto_model, get_message_handler()); + // do partial inlining status() << "Partial Inlining" << eom; goto_partial_inline(goto_model, get_message_handler()); diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index f8d1fc1d331..c9f3548e7df 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -37,6 +37,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include @@ -735,6 +736,8 @@ bool goto_analyzer_parse_optionst::process_goto_program( link_to_library(goto_model, ui_message_handler); #endif + remove_java_new(goto_model, get_message_handler()); + // remove function pointers status() << "Removing function pointers and virtual functions" << eom; remove_function_pointers( diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp index 5b64f186749..ea8b8cd1622 100644 --- a/src/goto-diff/goto_diff_parse_options.cpp +++ b/src/goto-diff/goto_diff_parse_options.cpp @@ -37,6 +37,7 @@ Author: Peter Schrammel #include #include #include +#include #include @@ -394,6 +395,8 @@ bool goto_diff_parse_optionst::process_goto_program( { namespacet ns(symbol_table); + remove_java_new(goto_model, get_message_handler()); + // Remove inline assembler; this needs to happen before // adding the library. remove_asm(goto_model); diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile index 38a75637776..bf4e5bb2491 100644 --- a/src/goto-programs/Makefile +++ b/src/goto-programs/Makefile @@ -45,6 +45,7 @@ SRC = basic_blocks.cpp \ remove_exceptions.cpp \ remove_function_pointers.cpp \ remove_instanceof.cpp \ + remove_java_new.cpp \ remove_returns.cpp \ remove_skip.cpp \ remove_static_init_loops.cpp \ diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp index 5f28a25e150..6a5826da46d 100644 --- a/src/goto-programs/builtin_functions.cpp +++ b/src/goto-programs/builtin_functions.cpp @@ -33,6 +33,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include "format_strings.h" +#include "class_identifier.h" void goto_convertt::do_prob_uniform( const exprt &lhs, @@ -539,68 +540,6 @@ void goto_convertt::do_cpp_new( dest.destructive_append(tmp_initializer); } -void set_class_identifier( - struct_exprt &expr, - const namespacet &ns, - const symbol_typet &class_type) -{ - const struct_typet &struct_type= - to_struct_type(ns.follow(expr.type())); - const struct_typet::componentst &components=struct_type.components(); - - if(components.empty()) - return; - assert(!expr.operands().empty()); - - if(components.front().get_name()=="@class_identifier") - { - assert(expr.op0().id()==ID_constant); - expr.op0()=constant_exprt(class_type.get_identifier(), string_typet()); - } - else - { - assert(expr.op0().id()==ID_struct); - set_class_identifier(to_struct_expr(expr.op0()), ns, class_type); - } -} - -void goto_convertt::do_java_new( - const exprt &lhs, - const side_effect_exprt &rhs, - goto_programt &dest) -{ - PRECONDITION(!lhs.is_nil()); - PRECONDITION(rhs.operands().empty()); - PRECONDITION(rhs.type().id() == ID_pointer); - source_locationt location=rhs.source_location(); - typet object_type=rhs.type().subtype(); - - // build size expression - exprt object_size=size_of_expr(object_type, ns); - CHECK_RETURN(object_size.is_not_nil()); - - // we produce a malloc side-effect, which stays - side_effect_exprt malloc_expr(ID_allocate); - malloc_expr.copy_to_operands(object_size); - // could use true and get rid of the code below - malloc_expr.copy_to_operands(false_exprt()); - malloc_expr.type()=rhs.type(); - - goto_programt::targett t_n=dest.add_instruction(ASSIGN); - t_n->code=code_assignt(lhs, malloc_expr); - t_n->source_location=location; - - // zero-initialize the object - dereference_exprt deref(lhs, object_type); - exprt zero_object= - zero_initializer(object_type, location, ns, get_message_handler()); - set_class_identifier( - to_struct_expr(zero_object), ns, to_symbol_type(object_type)); - goto_programt::targett t_i=dest.add_instruction(ASSIGN); - t_i->code=code_assignt(deref, zero_object); - t_i->source_location=location; -} - void goto_convertt::do_java_new_array( const exprt &lhs, const side_effect_exprt &rhs, diff --git a/src/goto-programs/class_identifier.cpp b/src/goto-programs/class_identifier.cpp index 3e92586e759..44683e847ce 100644 --- a/src/goto-programs/class_identifier.cpp +++ b/src/goto-programs/class_identifier.cpp @@ -71,3 +71,39 @@ exprt get_class_identifier_field( exprt deref=dereference_exprt(this_expr, this_expr.type().subtype()); return build_class_identifier(deref, ns); } + +/// If expr has its components filled in then sets the `@class_identifier` +/// member of the struct +/// \remarks Follows through base class members until it gets to the object +/// type that contains the `@class_identifier` member +/// \param expr: An expression that represents a struct +/// \param ns: The namespace used to resolve symbol referencess in the type of +/// the struct +/// \param class_type: A symbol whose identifier is the name of the class +void set_class_identifier( + struct_exprt &expr, + const namespacet &ns, + const symbol_typet &class_type) +{ + const struct_typet &struct_type=to_struct_type(ns.follow(expr.type())); + const struct_typet::componentst &components=struct_type.components(); + + if(components.empty()) + // Presumably this means the type has not yet been determined + return; + PRECONDITION(!expr.operands().empty()); + + if(components.front().get_name()=="@class_identifier") + { + INVARIANT( + expr.op0().id()==ID_constant, "@class_identifier must be a constant"); + expr.op0()=constant_exprt(class_type.get_identifier(), string_typet()); + } + else + { + // The first member must be the base class + INVARIANT( + expr.op0().id()==ID_struct, "Non @class_identifier must be a structure"); + set_class_identifier(to_struct_expr(expr.op0()), ns, class_type); + } +} diff --git a/src/goto-programs/class_identifier.h b/src/goto-programs/class_identifier.h index ccc679b8e1f..277c99895d2 100644 --- a/src/goto-programs/class_identifier.h +++ b/src/goto-programs/class_identifier.h @@ -15,10 +15,16 @@ Author: Chris Smowton, chris.smowton@diffblue.com class exprt; class namespacet; class symbol_typet; +class struct_exprt; exprt get_class_identifier_field( const exprt &this_expr, const symbol_typet &suggested_type, const namespacet &ns); +void set_class_identifier( + struct_exprt &expr, + const namespacet &ns, + const symbol_typet &class_type); + #endif diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index 85ffe47a4a4..4234e855cd1 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -756,10 +756,7 @@ void goto_convertt::convert_assign( else if(rhs.id()==ID_side_effect && rhs.get(ID_statement)==ID_java_new) { - Forall_operands(it, rhs) - clean_expr(*it, dest); - - do_java_new(lhs, to_side_effect_expr(rhs), dest); + copy(code, ASSIGN, dest); } else if(rhs.id()==ID_side_effect && rhs.get(ID_statement)==ID_java_new_array) diff --git a/src/goto-programs/goto_convert_class.h b/src/goto-programs/goto_convert_class.h index fe227986a71..21fcd1d0140 100644 --- a/src/goto-programs/goto_convert_class.h +++ b/src/goto-programs/goto_convert_class.h @@ -142,11 +142,6 @@ class goto_convertt:public messaget const side_effect_exprt &rhs, goto_programt &dest); - void do_java_new( - const exprt &lhs, - const side_effect_exprt &rhs, - goto_programt &dest); - void do_java_new_array( const exprt &lhs, const side_effect_exprt &rhs, diff --git a/src/goto-programs/remove_java_new.cpp b/src/goto-programs/remove_java_new.cpp new file mode 100644 index 00000000000..b7059bbadff --- /dev/null +++ b/src/goto-programs/remove_java_new.cpp @@ -0,0 +1,105 @@ +// Copyright 2017 Diffblue Limited. All Rights Reserved. + +/// \file +/// Function-level/module-level pass to remove java_new and replace with +/// malloc & zero-initialize + +#include "remove_java_new.h" + +#include +#include +#include + +#include "class_identifier.h" + +static bool remove_java_new( + goto_programt &goto_program, + const namespacet &ns, + message_handlert &message_handler) +{ + messaget msg(message_handler); + + bool changed=false; + for(goto_programt::targett target=goto_program.instructions.begin(); + target!=goto_program.instructions.end(); + ++target) + { + code_assignt *assign=expr_try_dynamic_cast(target->code); + if(assign==nullptr) + continue; + side_effect_exprt *rhs= + expr_try_dynamic_cast(assign->rhs()); + if(rhs==nullptr) + continue; + if(rhs->get_statement()!=ID_java_new) + continue; + INVARIANT(rhs->operands().empty(), "java_new does not have operands"); + INVARIANT(rhs->type().id()==ID_pointer, "java_new returns pointer"); + + const exprt &lhs=assign->lhs(); + INVARIANT( + !lhs.is_nil(), "remove_java_new without lhs is yet to be implemented"); + + typet object_type=rhs->type().subtype(); + + // build size expression + exprt object_size=size_of_expr(object_type, ns); + CHECK_RETURN(object_size.is_not_nil()); + + changed=true; + + source_locationt location=rhs->source_location(); + + // We produce a malloc side-effect + side_effect_exprt malloc_expr(ID_allocate); + malloc_expr.copy_to_operands(object_size); + // could use true and get rid of the code below + malloc_expr.copy_to_operands(false_exprt()); + malloc_expr.type()=rhs->type(); + *rhs=std::move(malloc_expr); + + // zero-initialize the object + dereference_exprt deref(lhs, object_type); + exprt zero_object= + zero_initializer(object_type, location, ns, message_handler); + set_class_identifier( + expr_dynamic_cast(zero_object), + ns, + to_symbol_type(object_type)); + goto_programt::targett zi_assign=goto_program.insert_after(target); + zi_assign->make_assignment(); + zi_assign->code=code_assignt(deref, zero_object); + zi_assign->source_location=location; + } + if(!changed) + return false; + goto_program.update(); + return true; +} + +bool remove_java_new( + goto_functionst::goto_functiont &goto_function, + const namespacet &ns, + message_handlert &message_handler) +{ + return remove_java_new(goto_function.body, ns, message_handler); +} + +void remove_java_new( + goto_functionst &goto_functions, + const namespacet &ns, + message_handlert &message_handler) +{ + for(auto &named_fn : goto_functions.function_map) + remove_java_new(named_fn.second, ns, message_handler); +} + +void remove_java_new( + goto_modelt &goto_model, + message_handlert &message_handler) +{ + remove_java_new( + goto_model.goto_functions, + namespacet(goto_model.symbol_table), + message_handler); +} diff --git a/src/goto-programs/remove_java_new.h b/src/goto-programs/remove_java_new.h new file mode 100644 index 00000000000..99263203a0f --- /dev/null +++ b/src/goto-programs/remove_java_new.h @@ -0,0 +1,29 @@ +// Copyright 2017 Diffblue Limited. All Rights Reserved. + +/// \file +/// Function-level/module-level pass to remove java_new and replace with +/// malloc & zero-initialize + +#ifndef CPROVER_GOTO_PROGRAMS_REMOVE_JAVA_NEW_H +#define CPROVER_GOTO_PROGRAMS_REMOVE_JAVA_NEW_H + +#include "goto_model.h" + +class message_handlert; + + +bool remove_java_new( + goto_functionst::goto_functiont &goto_function, + const namespacet &ns, + message_handlert &message_handler); + +void remove_java_new( + goto_functionst &goto_functions, + const namespacet &ns, + message_handlert &message_handler); + +void remove_java_new( + goto_modelt &goto_model, + message_handlert &message_handler); + +#endif // CPROVER_GOTO_PROGRAMS_REMOVE_JAVA_NEW_H diff --git a/src/jbmc/jbmc_parse_options.cpp b/src/jbmc/jbmc_parse_options.cpp index bf423b85af4..387064b40e8 100644 --- a/src/jbmc/jbmc_parse_options.cpp +++ b/src/jbmc/jbmc_parse_options.cpp @@ -50,6 +50,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include @@ -675,6 +676,8 @@ bool jbmc_parse_optionst::process_goto_functions( { try { + remove_java_new(goto_model, get_message_handler()); + // add the library link_to_library(goto_model, get_message_handler()); From cb09d8ead942269e23f727170e293b6bae098ac3 Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Tue, 24 Oct 2017 15:44:26 +0100 Subject: [PATCH 15/21] Fix new tests to use lazy loading --- src/goto-programs/lazy_goto_model.h | 5 +++ unit/testing-utils/load_java_class.cpp | 50 +++++++++++++++++++------- unit/testing-utils/load_java_class.h | 2 +- 3 files changed, 43 insertions(+), 14 deletions(-) diff --git a/src/goto-programs/lazy_goto_model.h b/src/goto-programs/lazy_goto_model.h index ddcbbe64718..9729fe11bf6 100644 --- a/src/goto-programs/lazy_goto_model.h +++ b/src/goto-programs/lazy_goto_model.h @@ -71,6 +71,11 @@ class lazy_goto_modelt /// Eagerly loads all functions from the symbol table. void load_all_functions() const; + language_filet &add_language_file(const std::string &filename) + { + return language_files.add_file(filename); + } + /// The model returned here has access to the functions we've already /// loaded but is frozen in the sense that, with regard to the facility to /// load new functions, it has let it go. diff --git a/unit/testing-utils/load_java_class.cpp b/unit/testing-utils/load_java_class.cpp index f79e14f7c9b..737dae1a162 100644 --- a/unit/testing-utils/load_java_class.cpp +++ b/unit/testing-utils/load_java_class.cpp @@ -12,8 +12,11 @@ #include #include +#include #include +#include + #include /// Go through the process of loading, typechecking and finalising loading a @@ -34,11 +37,21 @@ symbol_tablet load_java_class( symbol_tablet load_java_class( const std::string &java_class_name, const std::string &class_path, - std::unique_ptr java_lang) + std::unique_ptr &&java_lang) { - // We don't expect the .class suffix to allow us to check the name of the - // class + // We expect the name of the class without the .class suffix to allow us to + // check it PRECONDITION(!has_suffix(java_class_name, ".class")); + std::string filename=java_class_name + ".class"; + + // Construct a lazy_goto_modelt + null_message_handlert message_handler; + lazy_goto_modelt lazy_goto_model( + [] (goto_functionst::goto_functiont &function, symbol_tablet &symbol_table) + { }, + [] (goto_modelt &goto_model) + { return false; }, + message_handler); // Configure the path loading cmdlinet command_line; @@ -46,22 +59,33 @@ symbol_tablet load_java_class( config.java.classpath.clear(); config.java.classpath.push_back(class_path); - symbol_tablet new_symbol_table; + // Add the language to the model + language_filet &lf=lazy_goto_model.add_language_file(filename); + lf.language=std::move(java_lang); + languaget &language=*lf.language; std::istringstream java_code_stream("ignored"); - null_message_handlert message_handler; // Configure the language, load the class files - java_lang->get_language_options(command_line); - java_lang->set_message_handler(message_handler); - java_lang->parse(java_code_stream, java_class_name + ".class"); - java_lang->typecheck(new_symbol_table, ""); - java_lang->final(new_symbol_table); + language.set_message_handler(message_handler); + language.get_language_options(command_line); + language.parse(java_code_stream, filename); + language.typecheck(lazy_goto_model.symbol_table, ""); + language.generate_support_functions(lazy_goto_model.symbol_table); + language.final(lazy_goto_model.symbol_table); + + lazy_goto_model.load_all_functions(); + + std::unique_ptr maybe_goto_model= + lazy_goto_modelt::process_whole_model_and_freeze( + std::move(lazy_goto_model)); + INVARIANT(maybe_goto_model, "Freezing lazy_goto_model failed"); // Verify that the class was loaded const std::string class_symbol_name="java::"+java_class_name; - REQUIRE(new_symbol_table.has_symbol(class_symbol_name)); - const symbolt &class_symbol=*new_symbol_table.lookup(class_symbol_name); + REQUIRE(maybe_goto_model->symbol_table.has_symbol(class_symbol_name)); + const symbolt &class_symbol= + *maybe_goto_model->symbol_table.lookup(class_symbol_name); REQUIRE(class_symbol.is_type); const typet &class_type=class_symbol.type; REQUIRE(class_type.id()==ID_struct); @@ -70,5 +94,5 @@ symbol_tablet load_java_class( // Check your working directory and the class path is correctly configured // as this often indicates that one of these is wrong. REQUIRE_FALSE(class_type.get_bool(ID_incomplete_class)); - return new_symbol_table; + return std::move(maybe_goto_model->symbol_table); } diff --git a/unit/testing-utils/load_java_class.h b/unit/testing-utils/load_java_class.h index c1c8ecd65cf..7460ca6d693 100644 --- a/unit/testing-utils/load_java_class.h +++ b/unit/testing-utils/load_java_class.h @@ -24,6 +24,6 @@ symbol_tablet load_java_class( symbol_tablet load_java_class( const std::string &java_class_name, const std::string &class_path, - std::unique_ptr java_lang); + std::unique_ptr &&java_lang); #endif // CPROVER_TESTING_UTILS_LOAD_JAVA_CLASS_H From f759f252ae3e91fa4c68a16b04bb3d9758fc248a Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Mon, 27 Nov 2017 13:48:59 +0000 Subject: [PATCH 16/21] Fix new test to run remove_java_new pass --- unit/pointer-analysis/custom_value_set_analysis.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/unit/pointer-analysis/custom_value_set_analysis.cpp b/unit/pointer-analysis/custom_value_set_analysis.cpp index b3f64a14476..db657133a51 100644 --- a/unit/pointer-analysis/custom_value_set_analysis.cpp +++ b/unit/pointer-analysis/custom_value_set_analysis.cpp @@ -12,6 +12,7 @@ Author: Chris Smowton, chris@smowton.net #include #include #include +#include #include #include #include @@ -183,6 +184,9 @@ SCENARIO("test_value_set_analysis", namespacet ns(goto_model.symbol_table); + // VSA doesn't currently support java_new as an allocator + remove_java_new(goto_model, null_output); + // Fully inline the test program, to avoid VSA conflating // constructor callsites confusing the results we're trying to check: goto_function_inline(goto_model, TEST_FUNCTION_NAME, null_output); From 441d2691537ce6e3c682fd02bbf88b6d6053bb51 Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Wed, 25 Oct 2017 10:40:54 +0100 Subject: [PATCH 17/21] Reset counter used by get_fresh_aux_symbol in unit tests Otherwise symbols won't have reproducible names --- .../convert_exprt_to_string_exprt.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp b/unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp index 78c85045929..7970c2af11f 100644 --- a/unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp +++ b/unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp @@ -9,7 +9,7 @@ #include #include -#include +#include #include #include #include @@ -32,6 +32,8 @@ TEST_CASE("Convert exprt to string exprt") { GIVEN("A location, a string expression, and a symbol table") { + reset_temporary_counter(); + source_locationt loc; symbol_tablet symbol_table; namespacet ns(symbol_table); From ef02f4ded0041fcf667740ce127ab9bfb280f49f Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Mon, 4 Dec 2017 13:27:17 +0000 Subject: [PATCH 18/21] Update test to handle changed symbol creation order Remove line that depends on generated symbol name - Lucas confirms it wasn't the purpose of the test anyway. --- regression/jbmc-strings/StaticCharMethods05/test.desc | 1 - 1 file changed, 1 deletion(-) diff --git a/regression/jbmc-strings/StaticCharMethods05/test.desc b/regression/jbmc-strings/StaticCharMethods05/test.desc index e6f2a0e6ee8..41218e79141 100644 --- a/regression/jbmc-strings/StaticCharMethods05/test.desc +++ b/regression/jbmc-strings/StaticCharMethods05/test.desc @@ -3,7 +3,6 @@ StaticCharMethods05.class --refine-strings --string-max-length 1000 ^EXIT=10$ ^SIGNAL=0$ -null-pointer-exception\.14\] Throw null: FAILURE ^\[.*assertion\.1\] .* line 12 .* FAILURE$ ^\[.*assertion\.2\] .* line 22 .* FAILURE$ ^VERIFICATION FAILED$ From b0cd57b34eafc9332645cd6b1d70688bd71835e6 Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Wed, 22 Nov 2017 15:02:09 +0000 Subject: [PATCH 19/21] Encapsulate lazy_goto_modelt::goto_functions --- src/goto-programs/goto_model.h | 2 ++ src/goto-programs/lazy_goto_model.cpp | 2 +- src/goto-programs/lazy_goto_model.h | 4 +++- src/goto-programs/rebuild_goto_start_function.cpp | 2 +- 4 files changed, 7 insertions(+), 3 deletions(-) diff --git a/src/goto-programs/goto_model.h b/src/goto-programs/goto_model.h index 2f9c5939bc2..1d819c233ad 100644 --- a/src/goto-programs/goto_model.h +++ b/src/goto-programs/goto_model.h @@ -63,6 +63,8 @@ class goto_modelt goto_functions=std::move(other.goto_functions); return *this; } + + void unload(const irep_idt &name) { goto_functions.unload(name); } }; #endif // CPROVER_GOTO_PROGRAMS_GOTO_MODEL_H diff --git a/src/goto-programs/lazy_goto_model.cpp b/src/goto-programs/lazy_goto_model.cpp index 5aea7a9e944..bc6c52a6f55 100644 --- a/src/goto-programs/lazy_goto_model.cpp +++ b/src/goto-programs/lazy_goto_model.cpp @@ -100,7 +100,7 @@ void lazy_goto_modelt::initialize(const cmdlinet &cmdline) throw 0; } - language_filet &lf=language_files.add_file(filename); + language_filet &lf=add_language_file(filename); lf.language=get_language_from_filename(filename); if(lf.language==nullptr) diff --git a/src/goto-programs/lazy_goto_model.h b/src/goto-programs/lazy_goto_model.h index 9729fe11bf6..1d91891638d 100644 --- a/src/goto-programs/lazy_goto_model.h +++ b/src/goto-programs/lazy_goto_model.h @@ -71,6 +71,8 @@ class lazy_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); @@ -96,9 +98,9 @@ class lazy_goto_modelt public: /// Reference to symbol_table in the internal goto_model symbol_tablet &symbol_table; - const lazy_goto_functions_mapt goto_functions; private: + const lazy_goto_functions_mapt goto_functions; language_filest language_files; // Function/module processing functions diff --git a/src/goto-programs/rebuild_goto_start_function.cpp b/src/goto-programs/rebuild_goto_start_function.cpp index 1b9e1ea4028..ea0d48ce947 100644 --- a/src/goto-programs/rebuild_goto_start_function.cpp +++ b/src/goto-programs/rebuild_goto_start_function.cpp @@ -62,7 +62,7 @@ bool rebuild_goto_start_function_baset::operator()() // Remove the function from the goto functions so it is copied back in // from the symbol table during goto_convert if(!return_code) - goto_model.goto_functions.unload(goto_functionst::entry_point()); + goto_model.unload(goto_functionst::entry_point()); return return_code; } From f96efb42208487f1df92289ff387a8eaf756bfb8 Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Fri, 24 Nov 2017 19:07:46 +0000 Subject: [PATCH 20/21] Change template parameter name to not clash with existing type --- .../rebuild_goto_start_function.cpp | 22 +++++++++---------- .../rebuild_goto_start_function.h | 6 ++--- 2 files changed, 14 insertions(+), 14 deletions(-) diff --git a/src/goto-programs/rebuild_goto_start_function.cpp b/src/goto-programs/rebuild_goto_start_function.cpp index ea0d48ce947..8621ff4a44c 100644 --- a/src/goto-programs/rebuild_goto_start_function.cpp +++ b/src/goto-programs/rebuild_goto_start_function.cpp @@ -22,11 +22,11 @@ /// function) and symbol table (to replace the _start function symbol) of the /// program. /// \param _message_handler: The message handler to report any messages with -template -rebuild_goto_start_function_baset:: +template +rebuild_goto_start_function_baset:: rebuild_goto_start_function_baset( const cmdlinet &cmdline, - goto_modelt &goto_model, + maybe_lazy_goto_modelt &goto_model, message_handlert &message_handler): messaget(message_handler), cmdline(cmdline), @@ -42,8 +42,8 @@ rebuild_goto_start_function_baset( /// called from _start /// \return Returns true if either the symbol is not found, or something went /// wrong with generating the start_function. False otherwise. -template -bool rebuild_goto_start_function_baset::operator()() +template +bool rebuild_goto_start_function_baset::operator()() { const irep_idt &mode=get_entry_point_mode(); @@ -70,9 +70,9 @@ bool rebuild_goto_start_function_baset::operator()() /// Find out the mode of the current entry point to determine the mode of the /// replacement entry point /// \return A mode string saying which language to use -template -irep_idt -rebuild_goto_start_function_baset::get_entry_point_mode() const +template +irep_idt rebuild_goto_start_function_baset:: +get_entry_point_mode() const { const symbolt ¤t_entry_point= *goto_model.symbol_table.lookup(goto_functionst::entry_point()); @@ -81,9 +81,9 @@ rebuild_goto_start_function_baset::get_entry_point_mode() const /// Eliminate the existing entry point function symbol and any symbols created /// in that scope from the symbol table. -template -void -rebuild_goto_start_function_baset::remove_existing_entry_point() +template +void rebuild_goto_start_function_baset:: +remove_existing_entry_point() { // Remove the function itself goto_model.symbol_table.remove(goto_functionst::entry_point()); diff --git a/src/goto-programs/rebuild_goto_start_function.h b/src/goto-programs/rebuild_goto_start_function.h index 08129bf3981..8d5ad9f8fbe 100644 --- a/src/goto-programs/rebuild_goto_start_function.h +++ b/src/goto-programs/rebuild_goto_start_function.h @@ -24,13 +24,13 @@ class goto_functionst; #define HELP_FUNCTIONS \ " --function name set main function name\n" -template +template class rebuild_goto_start_function_baset: public messaget { public: rebuild_goto_start_function_baset( const cmdlinet &cmdline, - goto_modelt &goto_model, + maybe_lazy_goto_modelt &goto_model, message_handlert &message_handler); bool operator()(); @@ -41,7 +41,7 @@ class rebuild_goto_start_function_baset: public messaget void remove_existing_entry_point(); const cmdlinet &cmdline; - goto_modelt &goto_model; + maybe_lazy_goto_modelt &goto_model; }; // NOLINTNEXTLINE(readability/namespace) using required for templates From a2cf16d80c98828a527bfa92398e14ccaca7d667 Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Mon, 4 Dec 2017 14:52:20 +0000 Subject: [PATCH 21/21] Store symbol type instead of followed type when clean casting Don't store followed type as type of superclass when doing clean cast as it may later change since we can now convert more methods after typechecking and doing this may change the type --- src/java_bytecode/java_pointer_casts.cpp | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/src/java_bytecode/java_pointer_casts.cpp b/src/java_bytecode/java_pointer_casts.cpp index 26b42e0bd31..702211faeb1 100644 --- a/src/java_bytecode/java_pointer_casts.cpp +++ b/src/java_bytecode/java_pointer_casts.cpp @@ -45,16 +45,20 @@ bool find_superclass_with_type( if(base_struct.components().empty()) return false; - const typet &first_field_type= - ns.follow(base_struct.components()[0].type()); + const typet &first_field_type=base_struct.components()[0].type(); ptr=clean_deref(ptr); + // Careful not to use the followed type here, as stub types may be + // extended by later method conversion adding fields (e.g. an access + // against x->y might add a new field `y` to the type of `*x`) ptr=member_exprt( ptr, base_struct.components()[0].get_name(), first_field_type); ptr=address_of_exprt(ptr); - if(first_field_type==target_type) + // Compare the real (underlying) type, as target_type is already a non- + // symbolic type. + if(ns.follow(first_field_type)==target_type) return true; } }