From ddd1b7a8dd614ff8d381a2084d58e47a72dc850b Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Mon, 8 Jan 2018 14:24:26 +0000 Subject: [PATCH 1/3] Add remove_instanceof overload to remove from a particular instruction --- src/goto-programs/remove_instanceof.cpp | 31 +++++++++++++++++++++---- src/goto-programs/remove_instanceof.h | 5 ++++ 2 files changed, 31 insertions(+), 5 deletions(-) diff --git a/src/goto-programs/remove_instanceof.cpp b/src/goto-programs/remove_instanceof.cpp index 6d8a8de329b..b893c38b0ff 100644 --- a/src/goto-programs/remove_instanceof.cpp +++ b/src/goto-programs/remove_instanceof.cpp @@ -28,16 +28,17 @@ class remove_instanceoft class_hierarchy(symbol_table); } - // Lower instanceof for a single functions + // Lower instanceof for a single function bool lower_instanceof(goto_programt &); + // Lower instanceof for a single instruction + bool lower_instanceof(goto_programt &, goto_programt::targett); + protected: symbol_tablet &symbol_table; namespacet ns; class_hierarchyt class_hierarchy; - bool lower_instanceof(goto_programt &, goto_programt::targett); - std::size_t lower_instanceof( exprt &, goto_programt &, goto_programt::targett); }; @@ -168,9 +169,24 @@ bool remove_instanceoft::lower_instanceof(goto_programt &goto_program) } +/// 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. +void remove_instanceof( + goto_programt::targett target, + goto_programt &goto_program, + symbol_tablet &symbol_table) +{ + remove_instanceoft rem(symbol_table); + rem.lower_instanceof(goto_program, target); +} + /// Replace every instanceof in the passed function with an explicit /// class-identifier test. -/// Extra auxiliary variables may be introduced into symbol_table. +/// \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. void remove_instanceof( @@ -183,7 +199,7 @@ void remove_instanceof( /// Replace every instanceof in every function with an explicit /// class-identifier test. -/// Extra auxiliary variables may be introduced into symbol_table. +/// \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. void remove_instanceof( @@ -198,6 +214,11 @@ void remove_instanceof( goto_functions.compute_location_numbers(); } +/// Replace every instanceof in every function with an explicit +/// 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 +/// symbols to. void remove_instanceof(goto_modelt &goto_model) { 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 509b0157282..0cc6957734a 100644 --- a/src/goto-programs/remove_instanceof.h +++ b/src/goto-programs/remove_instanceof.h @@ -16,6 +16,11 @@ Author: Chris Smowton, chris.smowton@diffblue.com #include "goto_functions.h" #include "goto_model.h" +void remove_instanceof( + goto_programt::targett target, + goto_programt &goto_program, + symbol_tablet &symbol_table); + void remove_instanceof( goto_functionst::goto_functiont &function, symbol_tablet &symbol_table); From 94b7658b7c1e94df33b84bb0ebe7801be152377d Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Mon, 8 Jan 2018 14:28:28 +0000 Subject: [PATCH 2/3] Don't pass iterators into function calls --- src/goto-programs/remove_exceptions.cpp | 88 +++++++++++++------------ 1 file changed, 45 insertions(+), 43 deletions(-) diff --git a/src/goto-programs/remove_exceptions.cpp b/src/goto-programs/remove_exceptions.cpp index 035851beb52..009ed3766a1 100644 --- a/src/goto-programs/remove_exceptions.cpp +++ b/src/goto-programs/remove_exceptions.cpp @@ -90,49 +90,53 @@ class remove_exceptionst { } - void operator()( - goto_functionst &goto_functions); + void operator()(goto_functionst &goto_functions); protected: symbol_tablet &symbol_table; std::map> &exceptions_map; void add_exceptional_returns( - const goto_functionst::function_mapt::iterator &); + const irep_idt &function_id, + goto_programt &goto_program); void instrument_exception_handler( - const goto_functionst::function_mapt::iterator &, + const irep_idt &function_id, + goto_programt &goto_program, const goto_programt::targett &); void add_exception_dispatch_sequence( - const goto_functionst::function_mapt::iterator &, + const irep_idt &function_id, + goto_programt &goto_program, const goto_programt::targett &instr_it, const stack_catcht &stack_catch, const std::vector &locals); void instrument_throw( - const goto_functionst::function_mapt::iterator &, + const irep_idt &function_id, + goto_programt &goto_program, const goto_programt::targett &, const stack_catcht &, const std::vector &); void instrument_function_call( - const goto_functionst::function_mapt::iterator &, + const irep_idt &function_id, + goto_programt &goto_program, const goto_programt::targett &, const stack_catcht &, const std::vector &); void instrument_exceptions( - const goto_functionst::function_mapt::iterator &); + const irep_idt &function_id, + goto_programt &goto_program); }; /// adds exceptional return variables for every function that may escape /// exceptions void remove_exceptionst::add_exceptional_returns( - const goto_functionst::function_mapt::iterator &func_it) + const irep_idt &function_id, + goto_programt &goto_program) { - const irep_idt &function_id=func_it->first; - goto_programt &goto_program=func_it->second.body; auto maybe_symbol=symbol_table.lookup(function_id); INVARIANT(maybe_symbol, "functions should be recorded in the symbol table"); @@ -236,17 +240,17 @@ void remove_exceptionst::add_exceptional_returns( /// Translates an exception landing-pad into instructions that copy the /// in-flight exception pointer to a nominated expression, then clear the /// in-flight exception (i.e. null the pointer), hence marking it caught. -/// \param func_it: iterator pointing to the function containing this -/// landingpad instruction -/// \param instr_it [in, out]: iterator pointing to the landingpad instruction. +/// \param function_id: name of the function containing this landingpad +/// instruction +/// \param goto_program: body of the function containing this landingpad +/// instruction +/// \param instr_it: iterator pointing to the landingpad instruction. /// Will be overwritten. void remove_exceptionst::instrument_exception_handler( - const goto_functionst::function_mapt::iterator &func_it, + const irep_idt &function_id, + goto_programt &goto_program, const goto_programt::targett &instr_it) { - const irep_idt &function_id=func_it->first; - goto_programt &goto_program=func_it->second.body; - PRECONDITION(instr_it->type==CATCH); // retrieve the exception variable @@ -285,20 +289,19 @@ void remove_exceptionst::instrument_exception_handler( /// if (exception instanceof ExnA) then goto handlerA /// else if (exception instanceof ExnB) then goto handlerB /// else goto universal_handler or (dead locals; function exit) -/// \param func_it: iterator pointing to function instr_it belongs to +/// \param function_id: name of the function to which instr_it belongs +/// \param goto_program: body of the function to which instr_it belongs /// \param instr_it: throw or call instruction that may be an /// exception source /// \param stack_catch: exception handlers currently registered /// \param locals: local variables to kill on a function-exit edge void remove_exceptionst::add_exception_dispatch_sequence( - const goto_functionst::function_mapt::iterator &func_it, + const irep_idt &function_id, + goto_programt &goto_program, const goto_programt::targett &instr_it, const remove_exceptionst::stack_catcht &stack_catch, const std::vector &locals) { - const irep_idt &function_id=func_it->first; - goto_programt &goto_program=func_it->second.body; - // Unless we have a universal exception handler, jump to end of function // if not caught: goto_programt::targett default_target=goto_program.get_end_function(); @@ -360,10 +363,11 @@ void remove_exceptionst::add_exception_dispatch_sequence( } } -/// instruments each throw with conditional GOTOS to the corresponding +/// instruments each throw with conditional GOTOS to the corresponding /// exception handlers void remove_exceptionst::instrument_throw( - const goto_functionst::function_mapt::iterator &func_it, + const irep_idt &function_id, + goto_programt &goto_program, const goto_programt::targett &instr_it, const remove_exceptionst::stack_catcht &stack_catch, const std::vector &locals) @@ -383,11 +387,11 @@ void remove_exceptionst::instrument_throw( return; add_exception_dispatch_sequence( - func_it, instr_it, stack_catch, locals); + function_id, goto_program, instr_it, stack_catch, locals); // find the symbol where the thrown exception should be stored: - const symbolt &exc_symbol= - symbol_table.lookup_ref(id2string(func_it->first)+EXC_SUFFIX); + const symbolt &exc_symbol = + symbol_table.lookup_ref(id2string(function_id) + EXC_SUFFIX); symbol_exprt exc_thrown=exc_symbol.symbol_expr(); // add the assignment with the appropriate cast @@ -401,16 +405,14 @@ void remove_exceptionst::instrument_throw( /// instruments each function call that may escape exceptions with conditional /// GOTOS to the corresponding exception handlers void remove_exceptionst::instrument_function_call( - const goto_functionst::function_mapt::iterator &func_it, + const irep_idt &function_id, + goto_programt &goto_program, const goto_programt::targett &instr_it, const stack_catcht &stack_catch, const std::vector &locals) { PRECONDITION(instr_it->type==FUNCTION_CALL); - goto_programt &goto_program=func_it->second.body; - const irep_idt &function_id=func_it->first; - // save the address of the next instruction goto_programt::targett next_it=instr_it; next_it++; @@ -430,7 +432,7 @@ void remove_exceptionst::instrument_function_call( if(callee_inflight_exception && local_inflight_exception) { add_exception_dispatch_sequence( - func_it, instr_it, stack_catch, locals); + function_id, goto_program, instr_it, stack_catch, locals); const symbol_exprt callee_inflight_exception_expr= callee_inflight_exception->symbol_expr(); @@ -463,12 +465,12 @@ void remove_exceptionst::instrument_function_call( /// handlers. Additionally, it re-computes the live-range of local variables in /// order to add DEAD instructions. void remove_exceptionst::instrument_exceptions( - const goto_functionst::function_mapt::iterator &func_it) + const irep_idt &function_id, + goto_programt &goto_program) { stack_catcht stack_catch; // stack of try-catch blocks std::vector> stack_locals; // stack of local vars std::vector locals; - goto_programt &goto_program=func_it->second.body; if(goto_program.empty()) return; @@ -486,7 +488,7 @@ void remove_exceptionst::instrument_exceptions( // Is it an exception landing pad (start of a catch block)? if(statement==ID_exception_landingpad) { - instrument_exception_handler(func_it, instr_it); + instrument_exception_handler(function_id, goto_program, instr_it); } // Is it a catch handler pop? else if(statement==ID_pop_catch) @@ -551,11 +553,13 @@ void remove_exceptionst::instrument_exceptions( } else if(instr_it->type==THROW) { - instrument_throw(func_it, instr_it, stack_catch, locals); + instrument_throw( + function_id, goto_program, instr_it, stack_catch, locals); } else if(instr_it->type==FUNCTION_CALL) { - instrument_function_call(func_it, instr_it, stack_catch, locals); + instrument_function_call( + function_id, goto_program, instr_it, stack_catch, locals); } } } @@ -563,9 +567,9 @@ void remove_exceptionst::instrument_exceptions( void remove_exceptionst::operator()(goto_functionst &goto_functions) { Forall_goto_functions(it, goto_functions) - add_exceptional_returns(it); + add_exceptional_returns(it->first, it->second.body); Forall_goto_functions(it, goto_functions) - instrument_exceptions(it); + instrument_exceptions(it->first, it->second.body); } /// removes throws/CATCH-POP/CATCH-PUSH @@ -583,7 +587,5 @@ void remove_exceptions( /// removes throws/CATCH-POP/CATCH-PUSH void remove_exceptions(goto_modelt &goto_model) { - remove_exceptions( - goto_model.symbol_table, - goto_model.goto_functions); + remove_exceptions(goto_model.symbol_table, goto_model.goto_functions); } From c8821b2a8b1e3ecae26d6de0b902f0424a09fe68 Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Fri, 15 Sep 2017 18:55:54 +0100 Subject: [PATCH 3/3] Allow to remove instanceof when remove exceptions This removes the need to always run remove instanceof after remove exceptions and allows remove_instanceof to be moved to a function-pass --- src/goto-programs/remove_exceptions.cpp | 33 ++++++++++++++++--------- src/goto-programs/remove_exceptions.h | 12 +++++++-- src/jbmc/jbmc_parse_options.cpp | 9 ++++--- 3 files changed, 36 insertions(+), 18 deletions(-) diff --git a/src/goto-programs/remove_exceptions.cpp b/src/goto-programs/remove_exceptions.cpp index 009ed3766a1..73377dd1338 100644 --- a/src/goto-programs/remove_exceptions.cpp +++ b/src/goto-programs/remove_exceptions.cpp @@ -12,6 +12,7 @@ Date: December 2016 /// Remove exception handling #include "remove_exceptions.h" +#include "remove_instanceof.h" #ifdef DEBUG #include @@ -43,8 +44,9 @@ Date: December 2016 /// (in instruction->code.exception_list()) and a corresponding GOTO program /// target for each (in instruction->targets). /// Thrown instructions are currently always matched to tags using -/// java_instanceof, so a language frontend wanting to use this class -/// must use exceptions with a Java-compatible structure. +/// java_instanceof, optionally lowered to a check on the @class_identifier +/// field, so a language frontend wanting to use this class must use +/// exceptions with a Java-compatible structure. /// /// CATCH with a code_pop_catcht operand terminates a try-block begun by /// a code_push_catcht. At present the try block consists of the instructions @@ -72,9 +74,6 @@ Date: December 2016 /// instructions copy back to an ordinary local variable (or other expression) /// and set \#exception_value back to null, indicating the exception has been /// caught and normal control flow resumed. -/// -/// Note that remove_exceptions introduces java_instanceof comparisons at -/// present, so a remove_instanceof may be necessary after it completes. class remove_exceptionst { typedef std::vector> &_exceptions_map): - symbol_table(_symbol_table), - exceptions_map(_exceptions_map) + std::map> &_exceptions_map, + bool remove_added_instanceof) + : symbol_table(_symbol_table), + exceptions_map(_exceptions_map), + remove_added_instanceof(remove_added_instanceof) { } @@ -95,6 +96,7 @@ class remove_exceptionst protected: symbol_tablet &symbol_table; std::map> &exceptions_map; + bool remove_added_instanceof; void add_exceptional_returns( const irep_idt &function_id, @@ -346,6 +348,9 @@ void remove_exceptionst::add_exception_dispatch_sequence( binary_predicate_exprt check(exc_thrown, ID_java_instanceof, expr); t_exc->guard=check; + + if(remove_added_instanceof) + remove_instanceof(t_exc, goto_program, symbol_table); } } } @@ -575,17 +580,21 @@ void remove_exceptionst::operator()(goto_functionst &goto_functions) /// removes throws/CATCH-POP/CATCH-PUSH void remove_exceptions( symbol_tablet &symbol_table, - goto_functionst &goto_functions) + goto_functionst &goto_functions, + remove_exceptions_typest type) { const namespacet ns(symbol_table); std::map> exceptions_map; uncaught_exceptions(goto_functions, ns, exceptions_map); - remove_exceptionst remove_exceptions(symbol_table, exceptions_map); + remove_exceptionst remove_exceptions( + symbol_table, + exceptions_map, + type == remove_exceptions_typest::REMOVE_ADDED_INSTANCEOF); remove_exceptions(goto_functions); } /// removes throws/CATCH-POP/CATCH-PUSH -void remove_exceptions(goto_modelt &goto_model) +void remove_exceptions(goto_modelt &goto_model, remove_exceptions_typest type) { - remove_exceptions(goto_model.symbol_table, goto_model.goto_functions); + remove_exceptions(goto_model.symbol_table, goto_model.goto_functions, type); } diff --git a/src/goto-programs/remove_exceptions.h b/src/goto-programs/remove_exceptions.h index 47cf349cf13..866e8cb5e9a 100644 --- a/src/goto-programs/remove_exceptions.h +++ b/src/goto-programs/remove_exceptions.h @@ -21,7 +21,15 @@ Date: December 2016 // Removes 'throw x' and CATCH-PUSH/CATCH-POP // and adds the required instrumentation (GOTOs and assignments) -void remove_exceptions(symbol_tablet &, goto_functionst &); -void remove_exceptions(goto_modelt &); +enum class remove_exceptions_typest +{ + REMOVE_ADDED_INSTANCEOF, + DONT_REMOVE_INSTANCEOF, +}; + +void remove_exceptions( + goto_modelt &goto_model, + remove_exceptions_typest type = + remove_exceptions_typest::DONT_REMOVE_INSTANCEOF); #endif diff --git a/src/jbmc/jbmc_parse_options.cpp b/src/jbmc/jbmc_parse_options.cpp index e406a373c46..79d954c7196 100644 --- a/src/jbmc/jbmc_parse_options.cpp +++ b/src/jbmc/jbmc_parse_options.cpp @@ -649,6 +649,8 @@ void jbmc_parse_optionst::process_goto_function( // Remove inline assembler; this needs to happen before // adding the library. remove_asm(function, symbol_table); + // Removal of RTTI inspection: + remove_instanceof(function, symbol_table); } catch(const char *e) @@ -692,10 +694,9 @@ bool jbmc_parse_optionst::process_goto_functions( cmdline.isset("pointer-check")); // Java virtual functions -> explicit dispatch tables: remove_virtual_functions(goto_model); - // remove catch and throw (introduces instanceof) - remove_exceptions(goto_model); - // Similar removal of RTTI inspection: - remove_instanceof(goto_model); + // remove catch and throw (introduces instanceof but request it is removed) + remove_exceptions( + goto_model, remove_exceptions_typest::REMOVE_ADDED_INSTANCEOF); // instrument library preconditions instrument_preconditions(goto_model);