diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.cpp b/jbmc/src/janalyzer/janalyzer_parse_options.cpp index 9dd74b66638..1480391ef3a 100644 --- a/jbmc/src/janalyzer/janalyzer_parse_options.cpp +++ b/jbmc/src/janalyzer/janalyzer_parse_options.cpp @@ -673,7 +673,7 @@ 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, nullptr, get_message_handler()); + remove_exceptions_using_instanceof(goto_model, get_message_handler()); // Java instanceof -> clsid comparison: class_hierarchyt class_hierarchy(goto_model.symbol_table); diff --git a/jbmc/src/java_bytecode/remove_exceptions.cpp b/jbmc/src/java_bytecode/remove_exceptions.cpp index 8e404b7b955..6a51d810657 100644 --- a/jbmc/src/java_bytecode/remove_exceptions.cpp +++ b/jbmc/src/java_bytecode/remove_exceptions.cpp @@ -87,15 +87,15 @@ class remove_exceptionst explicit remove_exceptionst( symbol_table_baset &_symbol_table, - const class_hierarchyt *class_hierarchy, + const class_hierarchyt *_class_hierarchy, function_may_throwt _function_may_throw, - bool remove_added_instanceof, - message_handlert &message_handler) + bool _remove_added_instanceof, + message_handlert &_message_handler) : symbol_table(_symbol_table), - class_hierarchy(class_hierarchy), + class_hierarchy(_class_hierarchy), function_may_throw(_function_may_throw), - remove_added_instanceof(remove_added_instanceof), - message_handler(message_handler) + remove_added_instanceof(_remove_added_instanceof), + message_handler(_message_handler) { if(remove_added_instanceof) { @@ -590,27 +590,88 @@ void remove_exceptionst::operator()(goto_programt &goto_program) instrument_exceptions(goto_program); } +/// removes throws/CATCH-POP/CATCH-PUSH +void remove_exceptions_using_instanceof( + symbol_table_baset &symbol_table, + goto_functionst &goto_functions, + message_handlert &message_handler) +{ + const namespacet ns(symbol_table); + std::map> exceptions_map; + + uncaught_exceptions(goto_functions, ns, exceptions_map); + + remove_exceptionst::function_may_throwt function_may_throw = + [&exceptions_map](const irep_idt &id) { + return !exceptions_map[id].empty(); + }; + + remove_exceptionst remove_exceptions( + symbol_table, nullptr, function_may_throw, false, message_handler); + + remove_exceptions(goto_functions); +} + +/// removes throws/CATCH-POP/CATCH-PUSH from a single GOTO program, replacing +/// them with explicit exception propagation. +/// Note this is somewhat less accurate than the whole-goto-model version, +/// because we can't inspect other functions to determine whether they throw +/// or not, and therefore must assume they do and always introduce post-call +/// exception dispatch. +/// \param goto_program: program to remove exceptions from +/// \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 message_handler: logging output +void remove_exceptions_using_instanceof( + goto_programt &goto_program, + symbol_table_baset &symbol_table, + message_handlert &message_handler) +{ + remove_exceptionst::function_may_throwt any_function_may_throw = + [](const irep_idt &) { return true; }; + + remove_exceptionst remove_exceptions( + symbol_table, nullptr, any_function_may_throw, false, message_handler); + + remove_exceptions(goto_program); +} + +/// 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 message_handler: logging output +void remove_exceptions_using_instanceof( + goto_modelt &goto_model, + message_handlert &message_handler) +{ + remove_exceptions_using_instanceof( + goto_model.symbol_table, goto_model.goto_functions, message_handler); +} + /// 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) + const class_hierarchyt &class_hierarchy, + message_handlert &message_handler) { const namespacet ns(symbol_table); std::map> exceptions_map; + uncaught_exceptions(goto_functions, ns, exceptions_map); + remove_exceptionst::function_may_throwt function_may_throw = [&exceptions_map](const irep_idt &id) { return !exceptions_map[id].empty(); }; + remove_exceptionst remove_exceptions( - symbol_table, - class_hierarchy, - function_may_throw, - type == remove_exceptions_typest::REMOVE_ADDED_INSTANCEOF, - message_handler); + symbol_table, &class_hierarchy, function_may_throw, true, message_handler); + remove_exceptions(goto_functions); } @@ -627,25 +688,22 @@ void remove_exceptions( /// \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_programt &goto_program, symbol_table_baset &symbol_table, - const class_hierarchyt *class_hierarchy, - message_handlert &message_handler, - remove_exceptions_typest type) + const class_hierarchyt &class_hierarchy, + message_handlert &message_handler) { remove_exceptionst::function_may_throwt any_function_may_throw = [](const irep_idt &) { return true; }; remove_exceptionst remove_exceptions( symbol_table, - class_hierarchy, + &class_hierarchy, any_function_may_throw, - type == remove_exceptions_typest::REMOVE_ADDED_INSTANCEOF, + true, message_handler); + remove_exceptions(goto_program); } @@ -658,19 +716,14 @@ void remove_exceptions( /// \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) + const class_hierarchyt &class_hierarchy, + message_handlert &message_handler) { remove_exceptions( goto_model.symbol_table, - class_hierarchy, goto_model.goto_functions, - message_handler, - type); + class_hierarchy, + message_handler); } diff --git a/jbmc/src/java_bytecode/remove_exceptions.h b/jbmc/src/java_bytecode/remove_exceptions.h index db80df72756..a55026c1e31 100644 --- a/jbmc/src/java_bytecode/remove_exceptions.h +++ b/jbmc/src/java_bytecode/remove_exceptions.h @@ -23,28 +23,34 @@ Date: December 2016 #define INFLIGHT_EXCEPTION_VARIABLE_NAME \ "java::" INFLIGHT_EXCEPTION_VARIABLE_BASENAME -// Removes 'throw x' and CATCH-PUSH/CATCH-POP -// and adds the required instrumentation (GOTOs and assignments) - -enum class remove_exceptions_typest -{ - REMOVE_ADDED_INSTANCEOF, - DONT_REMOVE_INSTANCEOF, -}; - +/// Removes 'throw x' and CATCH-PUSH/CATCH-POP +/// and adds the required instrumentation (GOTOs and assignments) +/// This introduces instanceof expressions. +void remove_exceptions_using_instanceof( + goto_programt &, + symbol_table_baset &, + message_handlert &); + +/// Removes 'throw x' and CATCH-PUSH/CATCH-POP +/// and adds the required instrumentation (GOTOs and assignments) +/// This introduces instanceof expressions. +void remove_exceptions_using_instanceof(goto_modelt &, message_handlert &); + +/// Removes 'throw x' and CATCH-PUSH/CATCH-POP +/// and adds the required instrumentation (GOTOs and assignments) +/// This does not introduce instanceof expressions. 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); - + goto_programt &, + symbol_table_baset &, + const class_hierarchyt &, + message_handlert &); + +/// Removes 'throw x' and CATCH-PUSH/CATCH-POP +/// and adds the required instrumentation (GOTOs and assignments) +/// This does not introduce instanceof expressions. 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); + goto_modelt &, + const class_hierarchyt &, + message_handlert &); #endif diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index 35b59d0ec1d..afffb2382cb 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -748,9 +748,8 @@ 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); + *class_hierarchy.get(), + get_message_handler()); } auto function_is_stub = [&symbol_table, &model](const irep_idt &id) { @@ -891,12 +890,8 @@ bool jbmc_parse_optionst::process_goto_functions( return false; // remove catch and throw - // (introduces instanceof but request it is removed) remove_exceptions( - goto_model, - class_hierarchy.get(), - get_message_handler(), - remove_exceptions_typest::REMOVE_ADDED_INSTANCEOF); + goto_model, *class_hierarchy.get(), get_message_handler()); // instrument library preconditions instrument_preconditions(goto_model); diff --git a/jbmc/src/jdiff/jdiff_parse_options.cpp b/jbmc/src/jdiff/jdiff_parse_options.cpp index b80719694c4..356baf1b0d5 100644 --- a/jbmc/src/jdiff/jdiff_parse_options.cpp +++ b/jbmc/src/jdiff/jdiff_parse_options.cpp @@ -354,7 +354,7 @@ bool jdiff_parse_optionst::process_goto_program( // remove Java throw and catch // This introduces instanceof, so order is important: - remove_exceptions(goto_model, nullptr, get_message_handler()); + remove_exceptions_using_instanceof(goto_model, get_message_handler()); // Java instanceof -> clsid comparison: class_hierarchyt class_hierarchy(goto_model.symbol_table);