From be446745fef8a92754fa6e84a9f7cc0413510074 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Mon, 22 Oct 2018 12:28:21 +0100 Subject: [PATCH 1/7] Add missing doc-string for a remove_exceptions overload --- jbmc/src/java_bytecode/remove_exceptions.cpp | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/jbmc/src/java_bytecode/remove_exceptions.cpp b/jbmc/src/java_bytecode/remove_exceptions.cpp index 4ac6aa5ae95..cda0c9854fe 100644 --- a/jbmc/src/java_bytecode/remove_exceptions.cpp +++ b/jbmc/src/java_bytecode/remove_exceptions.cpp @@ -626,7 +626,18 @@ void remove_exceptions( 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, message_handlert &message_handler, From 253e33115d38f68c0d7dc191193fdc44d1fd832b Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Mon, 22 Oct 2018 12:28:42 +0100 Subject: [PATCH 2/7] Fix missing newline at end of file --- jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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..a5ec52970e7 100644 --- a/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp +++ b/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp @@ -292,4 +292,4 @@ SCENARIO( // load_and_test_method("replaceNondetReturnUnboxed:()I", functions, symbol_table); // } } -} \ No newline at end of file +} From 22638e2624c40b7fe6f0810ee35dcca16e99ad3d Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Mon, 22 Oct 2018 12:28:58 +0100 Subject: [PATCH 3/7] Make jdiff log message match janalyzer --- jbmc/src/jdiff/jdiff_parse_options.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/jbmc/src/jdiff/jdiff_parse_options.cpp b/jbmc/src/jdiff/jdiff_parse_options.cpp index 4ebfdaf919f..9b6f01f1656 100644 --- a/jbmc/src/jdiff/jdiff_parse_options.cpp +++ b/jbmc/src/jdiff/jdiff_parse_options.cpp @@ -345,7 +345,7 @@ 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")); From e39721f7301f7683fbe0ffa47d43ebe44d0df6c1 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Mon, 22 Oct 2018 12:29:20 +0100 Subject: [PATCH 4/7] Add whitespace between unrelated pass invocations --- jbmc/src/janalyzer/janalyzer_parse_options.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.cpp b/jbmc/src/janalyzer/janalyzer_parse_options.cpp index 0385ea439ba..7988ce012df 100644 --- a/jbmc/src/janalyzer/janalyzer_parse_options.cpp +++ b/jbmc/src/janalyzer/janalyzer_parse_options.cpp @@ -667,8 +667,10 @@ 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()); From eb5df0a4cd1a43fe25d2d36081b3e50e7b68cf91 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Tue, 23 Oct 2018 10:16:18 +0100 Subject: [PATCH 5/7] Add one-shot constructor to class_hierarchyt Allows alloc-and-init in one go. --- src/goto-programs/class_hierarchy.h | 4 ++++ 1 file changed, 4 insertions(+) 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; From df455b895051481c273420c973ac9514a9ce450d Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Mon, 22 Oct 2018 12:26:05 +0100 Subject: [PATCH 6/7] Avoid recomputing class hierarchy The class hierarchy never changes once the symbol table is computed. By sharing one instance owned by the driver program, particularly across function passes, we can avoid many potentially expensive recomputations. --- .../src/janalyzer/janalyzer_parse_options.cpp | 8 +++-- jbmc/src/java_bytecode/remove_exceptions.cpp | 32 +++++++++++++++-- jbmc/src/java_bytecode/remove_exceptions.h | 3 ++ jbmc/src/java_bytecode/remove_instanceof.cpp | 34 +++++++++++++------ jbmc/src/java_bytecode/remove_instanceof.h | 9 ++++- jbmc/src/jbmc/jbmc_parse_options.cpp | 15 +++++--- jbmc/src/jbmc/jbmc_parse_options.h | 2 ++ jbmc/src/jdiff/jdiff_parse_options.cpp | 10 ++++-- .../java_replace_nondet/replace_nondet.cpp | 4 ++- 9 files changed, 93 insertions(+), 24 deletions(-) diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.cpp b/jbmc/src/janalyzer/janalyzer_parse_options.cpp index 7988ce012df..9dd74b66638 100644 --- a/jbmc/src/janalyzer/janalyzer_parse_options.cpp +++ b/jbmc/src/janalyzer/janalyzer_parse_options.cpp @@ -673,9 +673,11 @@ bool janalyzer_parse_optionst::process_goto_program(const optionst &options) // 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 cda0c9854fe..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,6 +642,7 @@ void remove_exceptions( remove_exceptionst remove_exceptions( symbol_table, + class_hierarchy, any_function_may_throw, type == remove_exceptions_typest::REMOVE_ADDED_INSTANCEOF, message_handler); @@ -640,9 +663,14 @@ void remove_exceptions( /// 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..b399ae56b61 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( @@ -240,14 +242,16 @@ bool remove_instanceoft::lower_instanceof(goto_programt &goto_program) /// \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 +260,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 +277,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 +297,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 9b6f01f1656..b80719694c4 100644 --- a/jbmc/src/jdiff/jdiff_parse_options.cpp +++ b/jbmc/src/jdiff/jdiff_parse_options.cpp @@ -351,10 +351,14 @@ bool jdiff_parse_optionst::process_goto_program( // 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 a5ec52970e7..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); From 5e9aba835839ca40ca50d5dc16ac9e0477279178 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Tue, 23 Oct 2018 08:12:49 +0100 Subject: [PATCH 7/7] Remove unnecessary newline To pacify clang-format. All hail clang-format. --- jbmc/src/java_bytecode/remove_instanceof.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/jbmc/src/java_bytecode/remove_instanceof.cpp b/jbmc/src/java_bytecode/remove_instanceof.cpp index b399ae56b61..094886ce279 100644 --- a/jbmc/src/java_bytecode/remove_instanceof.cpp +++ b/jbmc/src/java_bytecode/remove_instanceof.cpp @@ -235,7 +235,6 @@ 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.