diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.cpp b/jbmc/src/janalyzer/janalyzer_parse_options.cpp index 0385ea439ba..9dd74b66638 100644 --- a/jbmc/src/janalyzer/janalyzer_parse_options.cpp +++ b/jbmc/src/janalyzer/janalyzer_parse_options.cpp @@ -667,13 +667,17 @@ bool janalyzer_parse_optionst::process_goto_program(const optionst &options) status() << "Removing function pointers and virtual functions" << eom; remove_function_pointers( get_message_handler(), goto_model, cmdline.isset("pointer-check")); + // Java virtual functions -> explicit dispatch tables: remove_virtual_functions(goto_model); + // remove Java throw and catch // This introduces instanceof, so order is important: - remove_exceptions(goto_model, get_message_handler()); - // remove rtti - remove_instanceof(goto_model, get_message_handler()); + remove_exceptions(goto_model, nullptr, get_message_handler()); + + // Java instanceof -> clsid comparison: + class_hierarchyt class_hierarchy(goto_model.symbol_table); + remove_instanceof(goto_model, class_hierarchy, get_message_handler()); // do partial inlining status() << "Partial Inlining" << eom; diff --git a/jbmc/src/java_bytecode/remove_exceptions.cpp b/jbmc/src/java_bytecode/remove_exceptions.cpp index 4ac6aa5ae95..c379709b4a2 100644 --- a/jbmc/src/java_bytecode/remove_exceptions.cpp +++ b/jbmc/src/java_bytecode/remove_exceptions.cpp @@ -87,14 +87,23 @@ class remove_exceptionst explicit remove_exceptionst( symbol_table_baset &_symbol_table, + const class_hierarchyt *class_hierarchy, function_may_throwt _function_may_throw, bool remove_added_instanceof, message_handlert &message_handler) : symbol_table(_symbol_table), + class_hierarchy(class_hierarchy), function_may_throw(_function_may_throw), remove_added_instanceof(remove_added_instanceof), message_handler(message_handler) { + if(remove_added_instanceof) + { + INVARIANT( + class_hierarchy != nullptr, + "remove_exceptions needs a class hierarchy to remove instanceof " + "statements (either supply one, or don't use REMOVE_ADDED_INSTANCEOF)"); + } } void operator()(goto_functionst &goto_functions); @@ -102,6 +111,7 @@ class remove_exceptionst protected: symbol_table_baset &symbol_table; + const class_hierarchyt *class_hierarchy; function_may_throwt function_may_throw; bool remove_added_instanceof; message_handlert &message_handler; @@ -345,7 +355,14 @@ void remove_exceptionst::add_exception_dispatch_sequence( t_exc->guard=check; if(remove_added_instanceof) - remove_instanceof(t_exc, goto_program, symbol_table, message_handler); + { + remove_instanceof( + t_exc, + goto_program, + symbol_table, + *class_hierarchy, + message_handler); + } } } } @@ -576,6 +593,7 @@ void remove_exceptionst::operator()(goto_programt &goto_program) /// removes throws/CATCH-POP/CATCH-PUSH void remove_exceptions( symbol_table_baset &symbol_table, + const class_hierarchyt *class_hierarchy, goto_functionst &goto_functions, message_handlert &message_handler, remove_exceptions_typest type) @@ -589,6 +607,7 @@ void remove_exceptions( }; remove_exceptionst remove_exceptions( symbol_table, + class_hierarchy, function_may_throw, type == remove_exceptions_typest::REMOVE_ADDED_INSTANCEOF, message_handler); @@ -605,6 +624,8 @@ void remove_exceptions( /// \param symbol_table: global symbol table. The `@inflight_exception` global /// may be added if not already present. It will not be initialised; that is /// the caller's responsibility. +/// \param class_hierarchy: class hierarchy analysis of symbol_table. +/// Only needed if type == REMOVE_ADDED_INSTANCEOF; otherwise may be null. /// \param message_handler: logging output /// \param type: specifies whether instanceof operations generated by this pass /// should be lowered to class-identifier comparisons (using @@ -612,6 +633,7 @@ void remove_exceptions( void remove_exceptions( goto_programt &goto_program, symbol_table_baset &symbol_table, + const class_hierarchyt *class_hierarchy, message_handlert &message_handler, remove_exceptions_typest type) { @@ -620,18 +642,35 @@ void remove_exceptions( remove_exceptionst remove_exceptions( symbol_table, + class_hierarchy, any_function_may_throw, type == remove_exceptions_typest::REMOVE_ADDED_INSTANCEOF, message_handler); remove_exceptions(goto_program); } -/// removes throws/CATCH-POP/CATCH-PUSH +/// removes throws/CATCH-POP/CATCH-PUSH, replacing them with explicit exception +/// propagation. +/// \param goto_model: model to remove exceptions from. The +/// `@inflight_exception` global may be added to its symbol table if not +/// already present. It will not be initialised; that is the caller's +/// responsibility. +/// \param class_hierarchy: class hierarchy analysis of symbol_table. +/// Only needed if type == REMOVE_ADDED_INSTANCEOF; otherwise may be null. +/// \param message_handler: logging output +/// \param type: specifies whether instanceof operations generated by this pass +/// should be lowered to class-identifier comparisons (using +/// remove_instanceof). void remove_exceptions( goto_modelt &goto_model, + const class_hierarchyt *class_hierarchy, message_handlert &message_handler, remove_exceptions_typest type) { remove_exceptions( - goto_model.symbol_table, goto_model.goto_functions, message_handler, type); + goto_model.symbol_table, + class_hierarchy, + goto_model.goto_functions, + message_handler, + type); } diff --git a/jbmc/src/java_bytecode/remove_exceptions.h b/jbmc/src/java_bytecode/remove_exceptions.h index 7c0b364b67a..db80df72756 100644 --- a/jbmc/src/java_bytecode/remove_exceptions.h +++ b/jbmc/src/java_bytecode/remove_exceptions.h @@ -14,6 +14,7 @@ Date: December 2016 #ifndef CPROVER_JAVA_BYTECODE_REMOVE_EXCEPTIONS_H #define CPROVER_JAVA_BYTECODE_REMOVE_EXCEPTIONS_H +#include #include #include @@ -34,12 +35,14 @@ enum class remove_exceptions_typest void remove_exceptions( goto_programt &goto_program, symbol_table_baset &symbol_table, + const class_hierarchyt *class_hierarchy, message_handlert &message_handler, remove_exceptions_typest type = remove_exceptions_typest::DONT_REMOVE_INSTANCEOF); void remove_exceptions( goto_modelt &goto_model, + const class_hierarchyt *class_hierarchy, message_handlert &message_handler, remove_exceptions_typest type = remove_exceptions_typest::DONT_REMOVE_INSTANCEOF); diff --git a/jbmc/src/java_bytecode/remove_instanceof.cpp b/jbmc/src/java_bytecode/remove_instanceof.cpp index dbacbac4a04..094886ce279 100644 --- a/jbmc/src/java_bytecode/remove_instanceof.cpp +++ b/jbmc/src/java_bytecode/remove_instanceof.cpp @@ -24,12 +24,14 @@ class remove_instanceoft { public: remove_instanceoft( - symbol_table_baset &symbol_table, message_handlert &message_handler) - : symbol_table(symbol_table) - , ns(symbol_table) - , message_handler(message_handler) + symbol_table_baset &symbol_table, + const class_hierarchyt &class_hierarchy, + message_handlert &message_handler) + : symbol_table(symbol_table), + class_hierarchy(class_hierarchy), + ns(symbol_table), + message_handler(message_handler) { - class_hierarchy(symbol_table); } // Lower instanceof for a single function @@ -40,8 +42,8 @@ class remove_instanceoft protected: symbol_table_baset &symbol_table; + const class_hierarchyt &class_hierarchy; namespacet ns; - class_hierarchyt class_hierarchy; message_handlert &message_handler; bool lower_instanceof( @@ -233,21 +235,22 @@ bool remove_instanceoft::lower_instanceof(goto_programt &goto_program) return true; } - /// Replace an instanceof in the expression or guard of the passed instruction /// of the given function body with an explicit class-identifier test. /// \remarks Extra auxiliary variables may be introduced into symbol_table. /// \param target: The instruction to work on. /// \param goto_program: The function body containing the instruction. /// \param symbol_table: The symbol table to add symbols to. +/// \param class_hierarchy: class hierarchy analysis of symbol_table /// \param message_handler: logging output void remove_instanceof( goto_programt::targett target, goto_programt &goto_program, symbol_table_baset &symbol_table, + const class_hierarchyt &class_hierarchy, message_handlert &message_handler) { - remove_instanceoft rem(symbol_table, message_handler); + remove_instanceoft rem(symbol_table, class_hierarchy, message_handler); rem.lower_instanceof(goto_program, target); } @@ -256,13 +259,15 @@ void remove_instanceof( /// \remarks 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. +/// \param class_hierarchy: class hierarchy analysis of symbol_table /// \param message_handler: logging output void remove_instanceof( goto_functionst::goto_functiont &function, symbol_table_baset &symbol_table, + const class_hierarchyt &class_hierarchy, message_handlert &message_handler) { - remove_instanceoft rem(symbol_table, message_handler); + remove_instanceoft rem(symbol_table, class_hierarchy, message_handler); rem.lower_instanceof(function.body); } @@ -271,13 +276,15 @@ void remove_instanceof( /// \remarks 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. +/// \param class_hierarchy: class hierarchy analysis of symbol_table /// \param message_handler: logging output void remove_instanceof( goto_functionst &goto_functions, symbol_table_baset &symbol_table, + const class_hierarchyt &class_hierarchy, message_handlert &message_handler) { - remove_instanceoft rem(symbol_table, message_handler); + remove_instanceoft rem(symbol_table, class_hierarchy, message_handler); bool changed=false; for(auto &f : goto_functions.function_map) changed=rem.lower_instanceof(f.second.body) || changed; @@ -289,12 +296,18 @@ void remove_instanceof( /// class-identifier test. /// \remarks Extra auxiliary variables may be introduced into symbol_table. /// \param goto_model: The functions to work on and the symbol table to add +/// \param class_hierarchy: class hierarchy analysis of goto_model's symbol +/// table /// \param message_handler: logging output /// symbols to. void remove_instanceof( goto_modelt &goto_model, + const class_hierarchyt &class_hierarchy, message_handlert &message_handler) { remove_instanceof( - goto_model.goto_functions, goto_model.symbol_table, message_handler); + goto_model.goto_functions, + goto_model.symbol_table, + class_hierarchy, + message_handler); } diff --git a/jbmc/src/java_bytecode/remove_instanceof.h b/jbmc/src/java_bytecode/remove_instanceof.h index f3a4c7f907e..46c9b6820de 100644 --- a/jbmc/src/java_bytecode/remove_instanceof.h +++ b/jbmc/src/java_bytecode/remove_instanceof.h @@ -79,6 +79,7 @@ Author: Chris Smowton, chris.smowton@diffblue.com #ifndef CPROVER_JAVA_BYTECODE_REMOVE_INSTANCEOF_H #define CPROVER_JAVA_BYTECODE_REMOVE_INSTANCEOF_H +#include #include #include @@ -89,18 +90,24 @@ void remove_instanceof( goto_programt::targett target, goto_programt &goto_program, symbol_table_baset &symbol_table, + const class_hierarchyt &class_hierarchy, message_handlert &); void remove_instanceof( goto_functionst::goto_functiont &function, symbol_table_baset &symbol_table, + const class_hierarchyt &class_hierarchy, message_handlert &); void remove_instanceof( goto_functionst &goto_functions, symbol_table_baset &symbol_table, + const class_hierarchyt &class_hierarchy, message_handlert &); -void remove_instanceof(goto_modelt &model, message_handlert &); +void remove_instanceof( + goto_modelt &model, + const class_hierarchyt &class_hierarchy, + message_handlert &); #endif diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index e5d3102b045..35b59d0ec1d 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -552,6 +552,9 @@ int jbmc_parse_optionst::doit() *this, options, get_message_handler()); lazy_goto_model.initialize(cmdline, options); + class_hierarchy = + util_make_unique(lazy_goto_model.symbol_table); + // The precise wording of this error matches goto-symex's complaint when no // __CPROVER_start exists (if we just go ahead and run it anyway it will // trip an invariant when it tries to load it) @@ -629,12 +632,13 @@ int jbmc_parse_optionst::get_goto_program( *this, options, get_message_handler()); lazy_goto_model.initialize(cmdline, options); + class_hierarchy = + util_make_unique(lazy_goto_model.symbol_table); + // Show the class hierarchy if(cmdline.isset("show-class-hierarchy")) { - class_hierarchyt hierarchy; - hierarchy(lazy_goto_model.symbol_table); - show_class_hierarchy(hierarchy, ui_message_handler); + show_class_hierarchy(*class_hierarchy, ui_message_handler); return CPROVER_EXIT_SUCCESS; } @@ -729,7 +733,8 @@ void jbmc_parse_optionst::process_goto_function( try { // Removal of RTTI inspection: - remove_instanceof(goto_function, symbol_table, get_message_handler()); + remove_instanceof( + goto_function, symbol_table, *class_hierarchy, get_message_handler()); // Java virtual functions -> explicit dispatch tables: remove_virtual_functions(function); @@ -743,6 +748,7 @@ void jbmc_parse_optionst::process_goto_function( remove_exceptions( goto_function.body, symbol_table, + class_hierarchy.get(), get_message_handler(), remove_exceptions_typest::REMOVE_ADDED_INSTANCEOF); } @@ -888,6 +894,7 @@ bool jbmc_parse_optionst::process_goto_functions( // (introduces instanceof but request it is removed) remove_exceptions( goto_model, + class_hierarchy.get(), get_message_handler(), remove_exceptions_typest::REMOVE_ADDED_INSTANCEOF); diff --git a/jbmc/src/jbmc/jbmc_parse_options.h b/jbmc/src/jbmc/jbmc_parse_options.h index a02628ab244..a605d4b2440 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.h +++ b/jbmc/src/jbmc/jbmc_parse_options.h @@ -123,6 +123,8 @@ class jbmc_parse_optionst: object_factory_parameterst object_factory_params; bool stub_objects_are_not_null; + std::unique_ptr class_hierarchy; + void get_command_line_options(optionst &); int get_goto_program( std::unique_ptr &goto_model, const optionst &); diff --git a/jbmc/src/jdiff/jdiff_parse_options.cpp b/jbmc/src/jdiff/jdiff_parse_options.cpp index 4ebfdaf919f..b80719694c4 100644 --- a/jbmc/src/jdiff/jdiff_parse_options.cpp +++ b/jbmc/src/jdiff/jdiff_parse_options.cpp @@ -345,16 +345,20 @@ bool jdiff_parse_optionst::process_goto_program( try { // remove function pointers - status() << "Removal of function pointers and virtual functions" << eom; + status() << "Removing function pointers and virtual functions" << eom; remove_function_pointers( get_message_handler(), goto_model, cmdline.isset("pointer-check")); // Java virtual functions -> explicit dispatch tables: remove_virtual_functions(goto_model); - // remove catch and throw - remove_exceptions(goto_model, get_message_handler()); + + // remove Java throw and catch + // This introduces instanceof, so order is important: + remove_exceptions(goto_model, nullptr, get_message_handler()); + // Java instanceof -> clsid comparison: - remove_instanceof(goto_model, get_message_handler()); + class_hierarchyt class_hierarchy(goto_model.symbol_table); + remove_instanceof(goto_model, class_hierarchy, get_message_handler()); mm_io(goto_model); diff --git a/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp b/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp index b5490499e3d..46eb0c6749b 100644 --- a/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp +++ b/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp @@ -141,7 +141,9 @@ void load_and_test_method( // Emulate some of the passes that we'd normally do before replace_java_nondet // is called. - remove_instanceof(goto_function, symbol_table, null_message_handler); + class_hierarchyt class_hierarchy(symbol_table); + remove_instanceof( + goto_function, symbol_table, class_hierarchy, null_message_handler); remove_virtual_functions(model_function); @@ -292,4 +294,4 @@ SCENARIO( // load_and_test_method("replaceNondetReturnUnboxed:()I", functions, symbol_table); // } } -} \ No newline at end of file +} diff --git a/src/goto-programs/class_hierarchy.h b/src/goto-programs/class_hierarchy.h index ed4c25f4783..9d962fd21b1 100644 --- a/src/goto-programs/class_hierarchy.h +++ b/src/goto-programs/class_hierarchy.h @@ -57,6 +57,10 @@ class class_hierarchyt void operator()(const symbol_tablet &); class_hierarchyt() = default; + explicit class_hierarchyt(const symbol_tablet &symbol_table) + { + (*this)(symbol_table); + } class_hierarchyt(const class_hierarchyt &) = delete; class_hierarchyt &operator=(const class_hierarchyt &) = delete;