diff --git a/regression/cbmc-java/exceptions22/test.class b/regression/cbmc-java/exceptions22/test.class new file mode 100644 index 00000000000..38081aaa0f2 Binary files /dev/null and b/regression/cbmc-java/exceptions22/test.class differ diff --git a/regression/cbmc-java/exceptions22/test.desc b/regression/cbmc-java/exceptions22/test.desc new file mode 100644 index 00000000000..a3eaa698597 --- /dev/null +++ b/regression/cbmc-java/exceptions22/test.desc @@ -0,0 +1,11 @@ +CORE +test.class + +^EXIT=0$ +^SIGNAL=0$ +VERIFICATION SUCCESSFUL +-- +^warning: ignoring +-- +This test checks that a thrown exception is caught, and is not erroneously rethrown +on function exit such that another surrounding try block can catch it again. diff --git a/regression/cbmc-java/exceptions22/test.java b/regression/cbmc-java/exceptions22/test.java new file mode 100644 index 00000000000..7ca29cddab9 --- /dev/null +++ b/regression/cbmc-java/exceptions22/test.java @@ -0,0 +1,20 @@ +public class test { + public static void main () { + try { + f(); + } + catch(Exception e) { + assert(false); // Should be unreachable + } + } + + public static void f() { + try { + throw new Exception(); + } + catch(Exception e) { + // Should prevent main's catch handler from being invoked + } + } +} + diff --git a/regression/cbmc-java/finally1/test.class b/regression/cbmc-java/finally1/test.class new file mode 100644 index 00000000000..73e239d42e5 Binary files /dev/null and b/regression/cbmc-java/finally1/test.class differ diff --git a/regression/cbmc-java/finally1/test.desc b/regression/cbmc-java/finally1/test.desc new file mode 100644 index 00000000000..a5fb4996899 --- /dev/null +++ b/regression/cbmc-java/finally1/test.desc @@ -0,0 +1,9 @@ +CORE +test.class + +^EXIT=10$ +^SIGNAL=0$ +assertion at file test\.java line 7 function java::test\.main:\(\)V bytecode-index 9: FAILURE +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/finally1/test.java b/regression/cbmc-java/finally1/test.java new file mode 100644 index 00000000000..f1a964d83d3 --- /dev/null +++ b/regression/cbmc-java/finally1/test.java @@ -0,0 +1,11 @@ +public class test { + public static void main() throws Exception { + try { + throw new Exception(); + } + finally { + assert(false); + } + } +} + diff --git a/regression/cbmc-java/finally2/test.class b/regression/cbmc-java/finally2/test.class new file mode 100644 index 00000000000..a7e4c2e4c22 Binary files /dev/null and b/regression/cbmc-java/finally2/test.class differ diff --git a/regression/cbmc-java/finally2/test.desc b/regression/cbmc-java/finally2/test.desc new file mode 100644 index 00000000000..ae317e016fe --- /dev/null +++ b/regression/cbmc-java/finally2/test.desc @@ -0,0 +1,9 @@ +CORE +test.class + +^EXIT=10$ +^SIGNAL=0$ +assertion at file test\.java line 8 function java::test\.main:\(\)V bytecode-index 9: FAILURE +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/finally2/test.java b/regression/cbmc-java/finally2/test.java new file mode 100644 index 00000000000..548936094dc --- /dev/null +++ b/regression/cbmc-java/finally2/test.java @@ -0,0 +1,12 @@ +public class test { + public static void main() throws Exception { + try { + throw new Exception(); + } + catch(Exception e) { } + finally { + assert(false); + } + } +} + diff --git a/regression/cbmc-java/finally3/test.class b/regression/cbmc-java/finally3/test.class new file mode 100644 index 00000000000..e73e96ce4ad Binary files /dev/null and b/regression/cbmc-java/finally3/test.class differ diff --git a/regression/cbmc-java/finally3/test.desc b/regression/cbmc-java/finally3/test.desc new file mode 100644 index 00000000000..40c2fe0ab68 --- /dev/null +++ b/regression/cbmc-java/finally3/test.desc @@ -0,0 +1,10 @@ +CORE +test.class + +^EXIT=10$ +^SIGNAL=0$ +assertion at file test\.java line 7 function java::test\.main:\(\)V bytecode-index 9: SUCCESS +assertion at file test\.java line 10 function java::test\.main:\(\)V bytecode-index 22: FAILURE +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/finally3/test.java b/regression/cbmc-java/finally3/test.java new file mode 100644 index 00000000000..51d347c3327 --- /dev/null +++ b/regression/cbmc-java/finally3/test.java @@ -0,0 +1,14 @@ +public class test { + public static void main() throws Exception { + try { + throw new NullPointerException(); + } + catch(ArithmeticException e) { + assert(false); + } + finally { + assert(false); + } + } +} + diff --git a/regression/cbmc-java/finally4/test.class b/regression/cbmc-java/finally4/test.class new file mode 100644 index 00000000000..f7989f80e54 Binary files /dev/null and b/regression/cbmc-java/finally4/test.class differ diff --git a/regression/cbmc-java/finally4/test.desc b/regression/cbmc-java/finally4/test.desc new file mode 100644 index 00000000000..eeba95d006c --- /dev/null +++ b/regression/cbmc-java/finally4/test.desc @@ -0,0 +1,9 @@ +CORE +test.class + +^EXIT=10$ +^SIGNAL=0$ +assertion at file test\.java line 11 function java::test\.main:\(\)V bytecode-index 7: FAILURE +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/finally4/test.java b/regression/cbmc-java/finally4/test.java new file mode 100644 index 00000000000..4943a8d251d --- /dev/null +++ b/regression/cbmc-java/finally4/test.java @@ -0,0 +1,15 @@ +public class test { + public static void main() throws Exception { + try { + int x = 1; + x++; + } + catch(ArithmeticException e) { + assert(false); + } + finally { + assert(false); + } + } +} + diff --git a/regression/cbmc-java/finally5/test.class b/regression/cbmc-java/finally5/test.class new file mode 100644 index 00000000000..0bde735c6af Binary files /dev/null and b/regression/cbmc-java/finally5/test.class differ diff --git a/regression/cbmc-java/finally5/test.desc b/regression/cbmc-java/finally5/test.desc new file mode 100644 index 00000000000..cc3b6780920 --- /dev/null +++ b/regression/cbmc-java/finally5/test.desc @@ -0,0 +1,9 @@ +CORE +test.class + +^EXIT=10$ +^SIGNAL=0$ +assertion at file test\.java line 7 function java::test\.main:\(\)V bytecode-index 12: FAILURE +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/finally5/test.java b/regression/cbmc-java/finally5/test.java new file mode 100644 index 00000000000..3411b175943 --- /dev/null +++ b/regression/cbmc-java/finally5/test.java @@ -0,0 +1,15 @@ +public class test { + public static void main() throws Exception { + try { + f(); + } + finally { + assert(false); + } + } + + public static void f() throws Exception { + throw new Exception(); + } +} + diff --git a/regression/cbmc-java/finally6/test.class b/regression/cbmc-java/finally6/test.class new file mode 100644 index 00000000000..5f4d1321761 Binary files /dev/null and b/regression/cbmc-java/finally6/test.class differ diff --git a/regression/cbmc-java/finally6/test.desc b/regression/cbmc-java/finally6/test.desc new file mode 100644 index 00000000000..91aca5d1b77 --- /dev/null +++ b/regression/cbmc-java/finally6/test.desc @@ -0,0 +1,9 @@ +CORE +test.class + +^EXIT=10$ +^SIGNAL=0$ +assertion at file test\.java line 8 function java::test\.main:\(\)V bytecode-index 12: FAILURE +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/finally6/test.java b/regression/cbmc-java/finally6/test.java new file mode 100644 index 00000000000..e7c328bdf56 --- /dev/null +++ b/regression/cbmc-java/finally6/test.java @@ -0,0 +1,16 @@ +public class test { + public static void main() throws Exception { + try { + f(); + } + catch(Exception e) { } + finally { + assert(false); + } + } + + public static void f() throws Exception { + throw new Exception(); + } +} + diff --git a/regression/cbmc-java/finally7/test.class b/regression/cbmc-java/finally7/test.class new file mode 100644 index 00000000000..94bdd643637 Binary files /dev/null and b/regression/cbmc-java/finally7/test.class differ diff --git a/regression/cbmc-java/finally7/test.desc b/regression/cbmc-java/finally7/test.desc new file mode 100644 index 00000000000..5772f2dea33 --- /dev/null +++ b/regression/cbmc-java/finally7/test.desc @@ -0,0 +1,10 @@ +CORE +test.class + +^EXIT=10$ +^SIGNAL=0$ +assertion at file test\.java line 7 function java::test\.main:\(\)V bytecode-index 12: SUCCESS +assertion at file test\.java line 10 function java::test\.main:\(\)V bytecode-index 25: FAILURE +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/finally7/test.java b/regression/cbmc-java/finally7/test.java new file mode 100644 index 00000000000..b9e8e16380e --- /dev/null +++ b/regression/cbmc-java/finally7/test.java @@ -0,0 +1,18 @@ +public class test { + public static void main() throws Exception { + try { + f(); + } + catch(ArithmeticException e) { + assert(false); + } + finally { + assert(false); + } + } + + public static void f() throws NullPointerException { + throw new NullPointerException(); + } +} + diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 34f330e3f9f..7f272956083 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -815,7 +815,7 @@ bool cbmc_parse_optionst::process_goto_program( cmdline.isset("pointer-check")); // Java virtual functions -> explicit dispatch tables: remove_virtual_functions(symbol_table, goto_functions); - // remove catch and throw + // remove catch and throw (introduces instanceof) remove_exceptions(symbol_table, goto_functions); // Similar removal of RTTI inspection: remove_instanceof(symbol_table, goto_functions); diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 91e7694aba4..ffa471086a0 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -356,6 +356,7 @@ bool goto_analyzer_parse_optionst::process_goto_program( // 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); // remove rtti remove_instanceof(goto_model); diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index d657a500f9b..8991ab985d3 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -806,6 +806,7 @@ void goto_instrument_parse_optionst::do_indirect_call_and_rtti_removal( status() << "Virtual function removal" << eom; remove_virtual_functions(symbol_table, goto_functions); status() << "Catch and throw removal" << eom; + // This introduces instanceof, so order is important: remove_exceptions(symbol_table, goto_functions); status() << "Java instanceof removal" << eom; remove_instanceof(symbol_table, goto_functions); diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index 5f308b3f9ff..022526863e4 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -58,31 +58,24 @@ static void finish_catch_push_targets(goto_programt &dest) // in the second pass set the targets Forall_goto_program_instructions(it, dest) { - if(it->is_catch()) + if(it->is_catch() && it->code.get_statement()==ID_push_catch) { - bool handler_added=true; - irept exceptions=it->code.find(ID_exception_list); + // Populate `targets` with a GOTO instruction target per + // exception handler if it isn't already populated. + // (Java handlers, for example, need this finish step; C++ + // handlers will already be populated by now) - if(exceptions.is_nil() && - it->code.has_operands()) - exceptions=it->code.op0().find(ID_exception_list); - - const irept::subt &exception_list=exceptions.get_sub(); - - if(!exception_list.empty()) + if(it->targets.empty()) { - // in this case we have a CATCH_PUSH - irept handlers=it->code.find(ID_label); - if(handlers.is_nil() && - it->code.has_operands()) - handlers=it->code.op0().find(ID_label); - const irept::subt &handler_list=handlers.get_sub(); - - // some handlers may not have been converted (if there was no - // exception to be caught); in such a situation we abort + bool handler_added=true; + const code_push_catcht::exception_listt &handler_list= + to_code_push_catch(it->code).exception_list(); + for(const auto &handler : handler_list) { - if(label_targets.find(handler.id())==label_targets.end()) + // some handlers may not have been converted (if there was no + // exception to be caught); in such a situation we abort + if(label_targets.find(handler.get_label())==label_targets.end()) { handler_added=false; break; @@ -93,14 +86,7 @@ static void finish_catch_push_targets(goto_programt &dest) continue; for(const auto &handler : handler_list) - { - std::map::const_iterator handler_it= - label_targets.find(handler.id()); - assert(handler_it!=label_targets.end()); - // set the target - it->targets.push_back(handler_it->second); - } + it->targets.push_back(label_targets.at(handler.get_label())); } } } @@ -566,6 +552,10 @@ void goto_convertt::convert( forall_operands(it, code) convert(to_code(*it), dest); } + else if(statement==ID_push_catch || + statement==ID_pop_catch || + statement==ID_exception_landingpad) + copy(code, CATCH, dest); else copy(code, OTHER, dest); diff --git a/src/goto-programs/goto_convert_class.h b/src/goto-programs/goto_convert_class.h index 8e6fe4da973..ceefa622c9d 100644 --- a/src/goto-programs/goto_convert_class.h +++ b/src/goto-programs/goto_convert_class.h @@ -97,9 +97,6 @@ class goto_convertt:public messaget side_effect_exprt &expr, goto_programt &dest, bool result_is_used); - void remove_push_catch( - side_effect_exprt &expr, - goto_programt &dest); void remove_assignment( side_effect_exprt &expr, goto_programt &dest, @@ -243,7 +240,6 @@ class goto_convertt:public messaget void convert_msc_try_except(const codet &code, goto_programt &dest); void convert_msc_leave(const codet &code, goto_programt &dest); void convert_try_catch(const codet &code, goto_programt &dest); - void convert_java_try_catch(const codet &code, goto_programt &dest); void convert_CPROVER_try_catch(const codet &code, goto_programt &dest); void convert_CPROVER_try_finally(const codet &code, goto_programt &dest); void convert_CPROVER_throw(const codet &code, goto_programt &dest); diff --git a/src/goto-programs/goto_convert_exceptions.cpp b/src/goto-programs/goto_convert_exceptions.cpp index 581ae2bcecd..f34d4d2f3fa 100644 --- a/src/goto-programs/goto_convert_exceptions.cpp +++ b/src/goto-programs/goto_convert_exceptions.cpp @@ -93,61 +93,6 @@ void goto_convertt::convert_msc_leave( t->source_location=code.source_location(); } -void goto_convertt::convert_java_try_catch( - const codet &code, - goto_programt &dest) -{ - assert(!code.operands().empty()); - - // add the CATCH instruction to 'dest' - goto_programt::targett catch_instruction=dest.add_instruction(); - catch_instruction->make_catch(); - catch_instruction->code.set_statement(ID_catch); - catch_instruction->source_location=code.source_location(); - catch_instruction->function=code.source_location().get_function(); - - // the CATCH instruction is annotated with a list of exception IDs - const irept exceptions=code.op0().find(ID_exception_list); - if(exceptions.is_not_nil()) - { - irept::subt exceptions_sub=exceptions.get_sub(); - irept::subt &exception_list= - catch_instruction->code.add(ID_exception_list).get_sub(); - exception_list.resize(exceptions_sub.size()); - for(size_t i=0; icode.add(ID_label).get_sub(); - handlers_list.resize(handlers_sub.size()); - for(size_t i=0; icode.get_sub().resize(1); - catch_instruction->code.get_sub()[0]=code.op0().op0(); - } - - // add a SKIP target for the end of everything - goto_programt end; - goto_programt::targett end_target=end.add_instruction(); - end_target->make_skip(); - end_target->source_location=code.source_location(); - end_target->function=code.source_location().get_function(); - - // add the end-target - dest.destructive_append(end); -} - void goto_convertt::convert_try_catch( const codet &code, goto_programt &dest) @@ -157,13 +102,14 @@ void goto_convertt::convert_try_catch( // add the CATCH-push instruction to 'dest' goto_programt::targett catch_push_instruction=dest.add_instruction(); catch_push_instruction->make_catch(); - catch_push_instruction->code.set_statement(ID_catch); catch_push_instruction->source_location=code.source_location(); + code_push_catcht push_catch_code; + // the CATCH-push instruction is annotated with a list of IDs, // one per target - irept::subt &exception_list= - catch_push_instruction->code.add(ID_exception_list).get_sub(); + code_push_catcht::exception_listt &exception_list= + push_catch_code.exception_list(); // add a SKIP target for the end of everything goto_programt end; @@ -176,7 +122,7 @@ void goto_convertt::convert_try_catch( // add the CATCH-pop to the end of the 'try' block goto_programt::targett catch_pop_instruction=dest.add_instruction(); catch_pop_instruction->make_catch(); - catch_pop_instruction->code.set_statement(ID_catch); + catch_pop_instruction->code=code_pop_catcht(); // add a goto to the end of the 'try' block dest.add_instruction()->make_goto(end_target); @@ -186,7 +132,8 @@ void goto_convertt::convert_try_catch( const codet &block=to_code(code.operands()[i]); // grab the ID and add to CATCH instruction - exception_list.push_back(irept(block.get(ID_exception_id))); + exception_list.push_back( + code_push_catcht::exception_list_entryt(block.get(ID_exception_id))); goto_programt tmp; convert(block, tmp); @@ -197,6 +144,8 @@ void goto_convertt::convert_try_catch( dest.add_instruction()->make_goto(end_target); } + catch_push_instruction->code=push_catch_code; + // add the end-target dest.destructive_append(end); } diff --git a/src/goto-programs/goto_convert_side_effect.cpp b/src/goto-programs/goto_convert_side_effect.cpp index 1d12ba8e9d7..2fc795254d2 100644 --- a/src/goto-programs/goto_convert_side_effect.cpp +++ b/src/goto-programs/goto_convert_side_effect.cpp @@ -636,17 +636,6 @@ void goto_convertt::remove_statement_expression( static_cast(expr)=tmp_symbol_expr; } -void goto_convertt::remove_push_catch( - side_effect_exprt &expr, - goto_programt &dest) -{ - // we only get here for ID_push_catch, which is only used for Java - convert_java_try_catch(code_expressiont(expr), dest); - - // the result can't be used, these are void - expr.make_nil(); -} - void goto_convertt::remove_side_effect( side_effect_exprt &expr, goto_programt &dest, @@ -707,8 +696,6 @@ void goto_convertt::remove_side_effect( // the result can't be used, these are void expr.make_nil(); } - else if(statement==ID_push_catch) - remove_push_catch(expr, dest); else { error().source_location=expr.find_source_location(); diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp index 347e156e589..8b376d25022 100644 --- a/src/goto-programs/goto_program.cpp +++ b/src/goto-programs/goto_program.cpp @@ -157,7 +157,17 @@ std::ostream &goto_programt::output_instruction( break; case CATCH: - if(!instruction.targets.empty()) + { + if(instruction.code.get_statement()==ID_exception_landingpad) + { + const auto &landingpad=to_code_landingpad(instruction.code); + out << "EXCEPTION LANDING PAD (" + << from_type(ns, identifier, landingpad.catch_expr().type()) + << ' ' + << from_expr(ns, identifier, landingpad.catch_expr()) + << ")"; + } + else if(instruction.code.get_statement()==ID_push_catch) { out << "CATCH-PUSH "; @@ -166,10 +176,9 @@ std::ostream &goto_programt::output_instruction( instruction.code.find(ID_exception_list).get_sub(); assert(instruction.targets.size()==exception_list.size()); for(instructiont::targetst::const_iterator - gt_it=instruction.targets.begin(); + gt_it=instruction.targets.begin(); gt_it!=instruction.targets.end(); - gt_it++, - i++) + gt_it++, i++) { if(gt_it!=instruction.targets.begin()) out << ", "; @@ -177,11 +186,18 @@ std::ostream &goto_programt::output_instruction( << (*gt_it)->target_number; } } - else + else if(instruction.code.get_statement()==ID_pop_catch) + { out << "CATCH-POP"; + } + else + { + UNREACHABLE; + } out << '\n'; break; + } case ATOMIC_BEGIN: out << "ATOMIC_BEGIN" << '\n'; diff --git a/src/goto-programs/goto_program_template.h b/src/goto-programs/goto_program_template.h index 9b46dd2ba62..cbdaef8dcfd 100644 --- a/src/goto-programs/goto_program_template.h +++ b/src/goto-programs/goto_program_template.h @@ -44,7 +44,7 @@ enum goto_program_instruction_typet DEAD=15, // marks the end-of-live of a local variable FUNCTION_CALL=16, // call a function THROW=17, // throw an exception - CATCH=18 // catch an exception + CATCH=18 // push, pop or enter an exception handler }; std::ostream &operator<<(std::ostream &, goto_program_instruction_typet); diff --git a/src/goto-programs/remove_exceptions.cpp b/src/goto-programs/remove_exceptions.cpp index 0c99e44b81a..45f57dfc82d 100644 --- a/src/goto-programs/remove_exceptions.cpp +++ b/src/goto-programs/remove_exceptions.cpp @@ -22,10 +22,59 @@ Date: December 2016 #include #include +#include #include #include +/// Lowers high-level exception descriptions into low-level operations suitable +/// for symex and other analyses that don't understand the THROW or CATCH GOTO +/// instructions. +/// +/// The instructions affected by the lowering are: +/// +/// THROW, whose operand must be a code_expressiont wrapping a +/// side_effect_expr_throwt. This starts propagating an exception, aborting +/// functions until a suitable catch point is found. +/// +/// CATCH with a code_push_catcht operand, which commences a region in which +/// exceptions should be caught, commonly a try block. +/// It specifies one or more exception tags to handle +/// (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. +/// +/// 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 +/// between the push and the pop *in program order*, not according to dynamic +/// control flow, so goto_convert_exceptions must ensure that control-flow +/// within the try block does not leave this range. +/// +/// CATCH with a code_landingpadt operand marks a point where exceptional +/// control flow terminates and normal control flow resumes, typically the top +/// of a catch or finally block, and the target of a code_push_catcht +/// describing the correponding try block. It gives an lvalue expression that +/// should be assigned the caught exception, typically a local variable. +/// +/// FUNCTION_CALL instructions are also affected: if the callee may abort +/// due to an escaping instruction, a dispatch sequence is inserted to check +/// whether the callee aborted and propagate the exception further if so. +/// +/// Exception propagation is implemented using a global variable per function +/// (named function_name#exception_value) that carries a reference to an +/// in-flight exception, or is null during normal control flow. +/// THROW assigns it a reference to the thrown instance; CALL instructions +/// copy between the exception_value for the callee and caller, catch_push +/// and catch_pop instructions indicate how they should be checked to dispatch +/// the right exception type to the right catch block, and landingpad +/// 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 &locals); void instrument_throw( const goto_functionst::function_mapt::iterator &, - const goto_programt::instructionst::iterator &, + const goto_programt::targett &, const stack_catcht &, - std::vector &); + const std::vector &); void instrument_function_call( const goto_functionst::function_mapt::iterator &, - const goto_programt::instructionst::iterator &, + const goto_programt::targett &, const stack_catcht &, - std::vector &); + const std::vector &); void instrument_exceptions( const goto_functionst::function_mapt::iterator &); @@ -179,119 +234,87 @@ void remove_exceptionst::add_exceptional_returns( } } -/// at the beginning of each handler in function f adds exc=f#exception_value; -/// f#exception_value=NULL; +/// 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. +/// Will be overwritten. void remove_exceptionst::instrument_exception_handler( const goto_functionst::function_mapt::iterator &func_it, - const goto_programt::instructionst::iterator &instr_it) + 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 && instr_it->code.has_operands()); + PRECONDITION(instr_it->type==CATCH); // retrieve the exception variable - const exprt &exception=instr_it->code.op0(); + const exprt &thrown_exception_local= + to_code_landingpad(instr_it->code).catch_expr(); + irep_idt thrown_exception_global=id2string(function_id)+EXC_SUFFIX; - if(symbol_table.has_symbol(id2string(function_id)+EXC_SUFFIX)) + if(symbol_table.has_symbol(thrown_exception_global)) { - const symbolt &function_symbol= - symbol_table.lookup(id2string(function_id)+EXC_SUFFIX); + const symbol_exprt thrown_global_symbol= + symbol_table.lookup(thrown_exception_global).symbol_expr(); // next we reset the exceptional return to NULL - symbol_exprt lhs_expr_null=function_symbol.symbol_expr(); - null_pointer_exprt rhs_expr_null(pointer_type(empty_typet())); + null_pointer_exprt null_voidptr((pointer_type(empty_typet()))); // add the assignment goto_programt::targett t_null=goto_program.insert_after(instr_it); t_null->make_assignment(); t_null->source_location=instr_it->source_location; t_null->code=code_assignt( - lhs_expr_null, - rhs_expr_null); + thrown_global_symbol, + null_voidptr); t_null->function=instr_it->function; - // add the assignment exc=f#exception_value - symbol_exprt rhs_expr_exc=function_symbol.symbol_expr(); - + // add the assignment exc=f#exception_value (before the null assignment) goto_programt::targett t_exc=goto_program.insert_after(instr_it); t_exc->make_assignment(); t_exc->source_location=instr_it->source_location; t_exc->code=code_assignt( - typecast_exprt(exception, rhs_expr_exc.type()), - rhs_expr_exc); + thrown_exception_local, + typecast_exprt(thrown_global_symbol, thrown_exception_local.type())); t_exc->function=instr_it->function; } instr_it->make_skip(); } -/// finds the instruction where the exceptional output is set or the end of the -/// function if no such output exists -static goto_programt::targett get_exceptional_output( - goto_programt &goto_program) -{ - Forall_goto_program_instructions(it, goto_program) - { - const irep_idt &statement=it->code.get_statement(); - if(statement==ID_output) - { - DATA_INVARIANT( - it->code.operands().size()>=2, - "output expected to have at least 2 operands"); - const exprt &expr=it->code.op1(); - DATA_INVARIANT( - expr.id()==ID_symbol, - "identifier expected to be a symbol"); - const symbol_exprt &symbol=to_symbol_expr(expr); - if(id2string(symbol.get_identifier()).find(EXC_SUFFIX) - !=std::string::npos) - return it; - } - } - return goto_program.get_end_function(); -} - -/// instruments each throw with conditional GOTOS to the corresponding -/// exception handlers -void remove_exceptionst::instrument_throw( +/// Emit the code: +/// 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 function_id: function instr_it belongs to +/// \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 goto_programt::instructionst::iterator &instr_it, + const goto_programt::targett &instr_it, const remove_exceptionst::stack_catcht &stack_catch, - std::vector &locals) + const std::vector &locals) { - PRECONDITION(instr_it->type==THROW); - - const exprt &exc_expr= - uncaught_exceptions_domaint::get_exception_symbol(instr_it->code); - bool assertion_error=id2string( - uncaught_exceptions_domaint::get_exception_type(exc_expr.type())). - find("java.lang.AssertionError")!=std::string::npos; - - // we don't count AssertionError (we couldn't catch it anyway - // and this may reduce the instrumentation considerably if the programmer - // used assertions) - if(assertion_error) - return; - - goto_programt &goto_program=func_it->second.body; const irep_idt &function_id=func_it->first; + goto_programt &goto_program=func_it->second.body; - // find the end of the function - goto_programt::targett exceptional_output= - get_exceptional_output(goto_program); - if(exceptional_output!=instr_it) - { - // jump to the end of the function - // this will appear after the GOTO-based dynamic dispatch below - goto_programt::targett t_end=goto_program.insert_after(instr_it); - t_end->make_goto(exceptional_output); - t_end->source_location=instr_it->source_location; - t_end->function=instr_it->function; - } + // 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(); + // Jump to the universal handler or function end, as appropriate. + // This will appear after the GOTO-based dynamic dispatch below + goto_programt::targett default_dispatch=goto_program.insert_after(instr_it); + default_dispatch->make_goto(); + default_dispatch->source_location=instr_it->source_location; + default_dispatch->function=instr_it->function; // find the symbol corresponding to the caught exceptions const symbolt &exc_symbol= - symbol_table.lookup(id2string(function_id)+EXC_SUFFIX); + symbol_table.lookup(id2string(function_id)+EXC_SUFFIX); symbol_exprt exc_thrown=exc_symbol.symbol_expr(); // add GOTOs implementing the dynamic dispatch of the @@ -302,22 +325,32 @@ void remove_exceptionst::instrument_throw( { goto_programt::targett new_state_pc= stack_catch[i][j].second; + if(stack_catch[i][j].first.empty()) + { + // Universal handler. Highest on the stack takes + // precedence, so overwrite any we've already seen: + default_target=new_state_pc; + } + else + { + // Normal exception handler, make an instanceof check. + goto_programt::targett t_exc=goto_program.insert_after(instr_it); + t_exc->make_goto(new_state_pc); + t_exc->source_location=instr_it->source_location; + t_exc->function=instr_it->function; - // find handler - goto_programt::targett t_exc=goto_program.insert_after(instr_it); - t_exc->make_goto(new_state_pc); - t_exc->source_location=instr_it->source_location; - t_exc->function=instr_it->function; - - // use instanceof to check that this is the correct handler - symbol_typet type(stack_catch[i][j].first); - type_exprt expr(type); + // use instanceof to check that this is the correct handler + symbol_typet type(stack_catch[i][j].first); + type_exprt expr(type); - binary_predicate_exprt check(exc_thrown, ID_java_instanceof, expr); - t_exc->guard=check; + binary_predicate_exprt check(exc_thrown, ID_java_instanceof, expr); + t_exc->guard=check; + } } } + default_dispatch->set_target(default_target); + // add dead instructions for(const auto &local : locals) { @@ -327,6 +360,37 @@ void remove_exceptionst::instrument_throw( t_dead->source_location=instr_it->source_location; t_dead->function=instr_it->function; } +} + +/// 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 goto_programt::targett &instr_it, + const remove_exceptionst::stack_catcht &stack_catch, + const std::vector &locals) +{ + PRECONDITION(instr_it->type==THROW); + + const exprt &exc_expr= + uncaught_exceptions_domaint::get_exception_symbol(instr_it->code); + bool assertion_error=id2string( + uncaught_exceptions_domaint::get_exception_type(exc_expr.type())). + find("java.lang.AssertionError")!=std::string::npos; + + // we don't count AssertionError (we couldn't catch it anyway + // and this may reduce the instrumentation considerably if the programmer + // used assertions) + if(assertion_error) + return; + + add_exception_dispatch_sequence( + func_it, instr_it, stack_catch, locals); + + // find the symbol where the thrown exception should be stored: + const symbolt &exc_symbol= + symbol_table.lookup(id2string(func_it->first)+EXC_SUFFIX); + symbol_exprt exc_thrown=exc_symbol.symbol_expr(); // add the assignment with the appropriate cast code_assignt assignment(typecast_exprt(exc_thrown, exc_expr.type()), @@ -340,9 +404,9 @@ void remove_exceptionst::instrument_throw( /// GOTOS to the corresponding exception handlers void remove_exceptionst::instrument_function_call( const goto_functionst::function_mapt::iterator &func_it, - const goto_programt::instructionst::iterator &instr_it, + const goto_programt::targett &instr_it, const stack_catcht &stack_catch, - std::vector &locals) + const std::vector &locals) { PRECONDITION(instr_it->type==FUNCTION_CALL); @@ -350,7 +414,7 @@ void remove_exceptionst::instrument_function_call( const irep_idt &function_id=func_it->first; // save the address of the next instruction - goto_programt::instructionst::iterator next_it=instr_it; + goto_programt::targett next_it=instr_it; next_it++; code_function_callt &function_call=to_code_function_call(instr_it->code); @@ -360,61 +424,23 @@ void remove_exceptionst::instrument_function_call( const irep_idt &callee_id= to_symbol_expr(function_call.function()).get_identifier(); - if(symbol_table.has_symbol(id2string(callee_id)+EXC_SUFFIX) && - symbol_table.has_symbol(id2string(function_id)+EXC_SUFFIX)) - { - // we may have an escaping exception - const symbolt &callee_exc_symbol= - symbol_table.lookup(id2string(callee_id)+EXC_SUFFIX); - symbol_exprt callee_exc=callee_exc_symbol.symbol_expr(); - - // find the end of the function - goto_programt::targett exceptional_output= - get_exceptional_output(goto_program); - if(exceptional_output!=instr_it) - { - // jump to the end of the function - // this will appear after the GOTO-based dynamic dispatch below - goto_programt::targett t_end=goto_program.insert_after(instr_it); - t_end->make_goto(exceptional_output); - t_end->source_location=instr_it->source_location; - t_end->function=instr_it->function; - } + const irep_idt &callee_inflight_exception=id2string(callee_id)+EXC_SUFFIX; + const irep_idt &local_inflight_exception=id2string(function_id)+EXC_SUFFIX; - for(std::size_t i=stack_catch.size(); i-->0;) - { - for(std::size_t j=stack_catch[i].size(); j-->0;) - { - goto_programt::targett new_state_pc; - new_state_pc=stack_catch[i][j].second; - goto_programt::targett t_exc=goto_program.insert_after(instr_it); - t_exc->make_goto(new_state_pc); - t_exc->source_location=instr_it->source_location; - t_exc->function=instr_it->function; - // use instanceof to check that this is the correct handler - symbol_typet type(stack_catch[i][j].first); - type_exprt expr(type); - binary_predicate_exprt check_instanceof( - callee_exc, - ID_java_instanceof, - expr); - t_exc->guard=check_instanceof; - } - } + if(symbol_table.has_symbol(callee_inflight_exception) && + symbol_table.has_symbol(local_inflight_exception)) + { + add_exception_dispatch_sequence( + func_it, instr_it, stack_catch, locals); - // add dead instructions - for(const auto &local : locals) - { - goto_programt::targett t_dead=goto_program.insert_after(instr_it); - t_dead->make_dead(); - t_dead->code=code_deadt(local); - t_dead->source_location=instr_it->source_location; - t_dead->function=instr_it->function; - } + const symbol_exprt callee_inflight_exception_expr= + symbol_table.lookup(callee_inflight_exception).symbol_expr(); + const symbol_exprt local_inflight_exception_expr= + symbol_table.lookup(local_inflight_exception).symbol_expr(); // add a null check (so that instanceof can be applied) equal_exprt eq_null( - callee_exc, + local_inflight_exception_expr, null_pointer_exprt(pointer_type(empty_typet()))); goto_programt::targett t_null=goto_program.insert_after(instr_it); t_null->make_goto(next_it); @@ -424,14 +450,12 @@ void remove_exceptionst::instrument_function_call( // after each function call g() in function f // adds f#exception_value=g#exception_value; - const symbolt &caller= - symbol_table.lookup(id2string(function_id)+EXC_SUFFIX); - const symbol_exprt &lhs_expr=caller.symbol_expr(); - goto_programt::targett t=goto_program.insert_after(instr_it); t->make_assignment(); t->source_location=instr_it->source_location; - t->code=code_assignt(lhs_expr, callee_exc); + t->code=code_assignt( + local_inflight_exception_expr, + callee_inflight_exception_expr); t->function=instr_it->function; } } @@ -456,10 +480,17 @@ void remove_exceptionst::instrument_exceptions( code_declt decl=to_code_decl(instr_it->code); locals.push_back(decl.symbol()); } - // it's a CATCH but not a handler (as it has no operands) - else if(instr_it->type==CATCH && !instr_it->code.has_operands()) + // Is it a handler push/pop or catch landing-pad? + else if(instr_it->type==CATCH) { - if(instr_it->targets.empty()) // pop + const irep_idt &statement=instr_it->code.get_statement(); + // Is it an exception landing pad (start of a catch block)? + if(statement==ID_exception_landingpad) + { + instrument_exception_handler(func_it, instr_it); + } + // Is it a catch handler pop? + else if(statement==ID_pop_catch) { // pop the local vars stack if(!stack_locals.empty()) @@ -479,7 +510,8 @@ void remove_exceptionst::instrument_exceptions( #endif } } - else // push + // Is it a catch handler push? + else if(statement==ID_push_catch) { stack_locals.push_back(locals); locals.clear(); @@ -490,9 +522,14 @@ void remove_exceptionst::instrument_exceptions( stack_catch.back(); // copy targets - const irept::subt &exception_list= - instr_it->code.find(ID_exception_list).get_sub(); + const code_push_catcht::exception_listt &exception_list= + to_code_push_catch(instr_it->code).exception_list(); + + // The target list can be empty if `finish_catch_push_targets` found that + // the targets were unreachable (in which case no exception can truly + // be thrown at runtime) INVARIANT( + instr_it->targets.empty() || exception_list.size()==instr_it->targets.size(), "`exception_list` should contain current instruction's targets"); @@ -501,17 +538,18 @@ void remove_exceptionst::instrument_exceptions( for(auto target : instr_it->targets) { last_exception.push_back( - std::make_pair(exception_list[i].id(), target)); + std::make_pair(exception_list[i].get_tag(), target)); i++; } } + else + { + INVARIANT( + false, + "CATCH opcode should be one of push-catch, pop-catch, landingpad"); + } instr_it->make_skip(); } - // CATCH handler - else if(instr_it->type==CATCH && instr_it->code.has_operands()) - { - instrument_exception_handler(func_it, instr_it); - } else if(instr_it->type==THROW) { instrument_throw(func_it, instr_it, stack_catch, locals); diff --git a/src/java_bytecode/expr2java.cpp b/src/java_bytecode/expr2java.cpp index 69829c676d8..e58b78fa690 100644 --- a/src/java_bytecode/expr2java.cpp +++ b/src/java_bytecode/expr2java.cpp @@ -392,6 +392,17 @@ std::string expr2javat::convert_with_precedence( else if(src.id()==ID_side_effect && src.get(ID_statement)==ID_throw) return convert_function(src, "throw", precedence=16); + else if(src.id()==ID_code && + to_code(src).get_statement()==ID_exception_landingpad) + { + const exprt &catch_expr= + to_code_landingpad(to_code(src)).catch_expr(); + return "catch_landingpad("+ + convert(catch_expr.type())+ + ' '+ + convert(catch_expr)+ + ')'; + } else if(src.id()==ID_unassigned) return "?"; else if(src.id()=="pod_constructor") diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index 53643d43016..cfc07f97c9b 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -1206,29 +1206,47 @@ codet java_bytecode_convert_methodt::convert_instructions( statement=std::string(id2string(statement), 0, statement.size()-2); } + typet catch_type; + + // Find catch blocks that begin here. For now we assume if more than + // one catch targets the same bytecode then we must be indifferent to + // its type and just call it a Throwable. auto it=method.exception_table.begin(); for(; it!=method.exception_table.end(); ++it) { if(cur_pc==it->handler_pc) { - // at the beginning of a handler, clear the stack and - // push the corresponding exceptional return variable - stack.clear(); - auxiliary_symbolt new_symbol; - new_symbol.is_static_lifetime=true; - // generate the name of the exceptional return variable - const std::string &exceptional_var_name= - id2string(method_name)+ - EXC_SUFFIX; - new_symbol.base_name=exceptional_var_name; - new_symbol.name=exceptional_var_name; - new_symbol.type=typet(ID_pointer, empty_typet()); - new_symbol.mode=ID_java; - symbol_table.add(new_symbol); - stack.push_back(new_symbol.symbol_expr()); + if(catch_type!=typet() || it->catch_type==symbol_typet()) + { + catch_type=symbol_typet("java::java.lang.Throwable"); + break; + } + else + catch_type=it->catch_type; } } + codet catch_instruction; + + if(catch_type!=typet()) + { + // at the beginning of a handler, clear the stack and + // push the corresponding exceptional return variable + // We also create a catch exception instruction that + // precedes the catch block, and which remove_exceptionst + // will transform into something like: + // catch_var = GLOBAL_THROWN_EXCEPTION; + // GLOBAL_THROWN_EXCEPTION = null; + stack.clear(); + symbol_exprt catch_var= + tmp_variable( + "caught_exception", + pointer_typet(catch_type)); + stack.push_back(catch_var); + code_landingpadt catch_statement(catch_var); + catch_instruction=catch_statement; + } + exprt::operandst op=pop(bytecode_info.pop); exprt::operandst results; results.resize(bytecode_info.push, nil_exprt()); @@ -2371,23 +2389,21 @@ codet java_bytecode_convert_methodt::convert_instructions( // add the actual PUSH-CATCH instruction if(!exception_ids.empty()) { - // add the exception ids - side_effect_expr_catcht catch_push_expr; - irept result(ID_exception_list); - result.get_sub().resize(exception_ids.size()); + code_push_catcht catch_push; + INVARIANT( + exception_ids.size()==handler_labels.size(), + "Exception tags and handler labels should be 1-to-1"); + code_push_catcht::exception_listt &exception_list= + catch_push.exception_list(); for(size_t i=0; isource_location.get_line().empty()) merge_source_location_rec(c, i_it->source_location); diff --git a/src/java_bytecode/java_class_loader.cpp b/src/java_bytecode/java_class_loader.cpp index 6b720f05fb6..0d643602906 100644 --- a/src/java_bytecode/java_class_loader.cpp +++ b/src/java_bytecode/java_class_loader.cpp @@ -31,6 +31,9 @@ java_bytecode_parse_treet &java_class_loadert::operator()( queue.push("java.lang.String"); // add java.lang.Class queue.push("java.lang.Class"); + // Require java.lang.Throwable as the catch-type used for + // universal exception handlers: + queue.push("java.lang.Throwable"); queue.push(class_name); java_class_loader_limitt class_loader_limit( diff --git a/src/java_bytecode/java_entry_point.cpp b/src/java_bytecode/java_entry_point.cpp index 9cf1989c418..4d2ebd95f23 100644 --- a/src/java_bytecode/java_entry_point.cpp +++ b/src/java_bytecode/java_entry_point.cpp @@ -307,11 +307,9 @@ void java_record_outputs( codet output(ID_output); output.operands().resize(2); - assert(symbol_table.has_symbol(id2string(function.name)+EXC_SUFFIX)); - // retrieve the exception variable const symbolt exc_symbol=symbol_table.lookup( - id2string(function.name)+EXC_SUFFIX); + JAVA_ENTRY_POINT_EXCEPTION_SYMBOL); output.op0()=address_of_exprt( index_exprt(string_constantt(exc_symbol.base_name), @@ -613,17 +611,19 @@ bool java_entry_point( call_main.lhs()=return_symbol.symbol_expr(); } - if(!symbol_table.has_symbol(id2string(symbol.name)+EXC_SUFFIX)) - { - // add the exceptional return value - auxiliary_symbolt exc_symbol; - exc_symbol.mode=ID_java; - exc_symbol.is_static_lifetime=true; - exc_symbol.name=id2string(symbol.name)+EXC_SUFFIX; - exc_symbol.base_name=id2string(symbol.name)+EXC_SUFFIX; - exc_symbol.type=java_reference_type(empty_typet()); - symbol_table.add(exc_symbol); - } + // add the exceptional return value + auxiliary_symbolt exc_symbol; + exc_symbol.mode=ID_java; + exc_symbol.name=JAVA_ENTRY_POINT_EXCEPTION_SYMBOL; + exc_symbol.base_name=exc_symbol.name; + exc_symbol.type=java_reference_type(empty_typet()); + symbol_table.add(exc_symbol); + + // Zero-initialise the top-level exception catch variable: + init_code.copy_to_operands( + code_assignt( + exc_symbol.symbol_expr(), + null_pointer_exprt(to_pointer_type(exc_symbol.type)))); // create code that allocates the objects used as test arguments and // non-deterministically initializes them @@ -638,8 +638,42 @@ bool java_entry_point( pointer_type_selector); call_main.arguments()=main_arguments; + // Create target labels for the toplevel exception handler: + code_labelt toplevel_catch("toplevel_catch", code_skipt()); + code_labelt after_catch("after_catch", code_skipt()); + + code_blockt call_block; + + // Push a universal exception handler: + // Catch all exceptions: + // This is equivalent to catching Throwable, but also works if some of + // the class hierarchy is missing so that we can't determine that + // the thrown instance is an indirect child of Throwable + code_push_catcht push_universal_handler( + irep_idt(), toplevel_catch.get_label()); + irept catch_type_list(ID_exception_list); + irept catch_target_list(ID_label); + + call_block.move_to_operands(push_universal_handler); + // we insert the call to the method AFTER the argument initialization code - init_code.move_to_operands(call_main); + call_block.move_to_operands(call_main); + + // Pop the handler: + code_pop_catcht pop_handler; + call_block.move_to_operands(pop_handler); + init_code.move_to_operands(call_block); + + // Normal return: skip the exception handler: + init_code.copy_to_operands(code_gotot(after_catch.get_label())); + + // Exceptional return: catch and assign to exc_symbol. + code_landingpadt landingpad(exc_symbol.symbol_expr()); + init_code.copy_to_operands(toplevel_catch); + init_code.move_to_operands(landingpad); + + // Converge normal and exceptional return: + init_code.move_to_operands(after_catch); // declare certain (which?) variables as test outputs java_record_outputs(symbol, main_arguments, init_code, symbol_table); diff --git a/src/java_bytecode/java_entry_point.h b/src/java_bytecode/java_entry_point.h index 97828ed2bdb..18e42aafc65 100644 --- a/src/java_bytecode/java_entry_point.h +++ b/src/java_bytecode/java_entry_point.h @@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #define JAVA_ENTRY_POINT_RETURN_SYMBOL "return'" +#define JAVA_ENTRY_POINT_EXCEPTION_SYMBOL "uncaught_exception'" bool java_entry_point( class symbol_tablet &symbol_table, diff --git a/src/symex/symex_parse_options.cpp b/src/symex/symex_parse_options.cpp index 739b733c03d..57c13b7d075 100644 --- a/src/symex/symex_parse_options.cpp +++ b/src/symex/symex_parse_options.cpp @@ -304,6 +304,7 @@ bool symex_parse_optionst::process_goto_program(const optionst &options) // Java virtual functions -> explicit dispatch tables: remove_virtual_functions(goto_model); // Java throw and catch -> explicit exceptional return variables: + // This introduces instanceof, so order is important: remove_exceptions(goto_model); // Java instanceof -> clsid comparison: remove_instanceof(goto_model); diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index e24d7cd981f..04eaa8a83d6 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -745,6 +745,8 @@ IREP_ID_ONE(java_instanceof) IREP_ID_ONE(java_super_method_call) IREP_ID_ONE(java_enum_static_unwind) IREP_ID_ONE(push_catch) +IREP_ID_ONE(pop_catch) +IREP_ID_ONE(exception_landingpad) IREP_ID_ONE(length_upper_bound) IREP_ID_ONE(string_constraint) IREP_ID_ONE(string_not_contains_constraint) diff --git a/src/util/std_code.h b/src/util/std_code.h index 1591348ed32..f48c48cb71a 100644 --- a/src/util/std_code.h +++ b/src/util/std_code.h @@ -1152,34 +1152,153 @@ inline const side_effect_expr_throwt &to_side_effect_expr_throw( assert(expr.get(ID_statement)==ID_throw); return static_cast(expr); } -/*! \brief A side effect that pushes/pops a catch handler -*/ -class side_effect_expr_catcht:public side_effect_exprt + +/// Pushes an exception handler, of the form: +/// exception_tag1 -> label1 +/// exception_tag2 -> label2 +/// ... +/// When used in a GOTO program instruction, the corresponding +/// opcode must be CATCH, and the instruction's `targets` must +/// be in one-to-one correspondence with the exception tags. +/// The labels may be unspecified for the case where +/// there is no corresponding source-language label, in whic +/// case the GOTO instruction targets must be set at the same +/// time. +class code_push_catcht:public codet { public: - side_effect_expr_catcht():side_effect_exprt(ID_push_catch) + code_push_catcht():codet(ID_push_catch) { + set(ID_exception_list, irept(ID_exception_list)); } - explicit side_effect_expr_catcht(const irept &exception_list): - side_effect_exprt(ID_push_catch) + + class exception_list_entryt:public irept { - set(ID_exception_list, exception_list); + public: + exception_list_entryt() + { + } + + explicit exception_list_entryt(const irep_idt &tag) + { + set(ID_tag, tag); + } + + exception_list_entryt(const irep_idt &tag, const irep_idt &label) + { + set(ID_tag, tag); + set(ID_label, label); + } + + void set_tag(const irep_idt &tag) + { + set(ID_tag, tag); + } + + const irep_idt &get_tag() const { + return get(ID_tag); + } + + void set_label(const irep_idt &label) + { + set(ID_label, label); + } + + const irep_idt &get_label() const { + return get(ID_label); + } + }; + + typedef std::vector exception_listt; + + code_push_catcht( + const irep_idt &tag, + const irep_idt &label): + codet(ID_push_catch) + { + set(ID_exception_list, irept(ID_exception_list)); + exception_list().push_back(exception_list_entryt(tag, label)); + } + + exception_listt &exception_list() { + return (exception_listt &)find(ID_exception_list).get_sub(); + } + + const exception_listt &exception_list() const { + return (const exception_listt &)find(ID_exception_list).get_sub(); } }; -static inline side_effect_expr_catcht &to_side_effect_expr_catch(exprt &expr) +static inline code_push_catcht &to_code_push_catch(codet &code) { - assert(expr.id()==ID_side_effect); - assert(expr.get(ID_statement)==ID_push_catch); - return static_cast(expr); + assert(code.get_statement()==ID_push_catch); + return static_cast(code); } -static inline const side_effect_expr_catcht &to_side_effect_expr_catch( - const exprt &expr) +static inline const code_push_catcht &to_code_push_catch(const codet &code) { - assert(expr.id()==ID_side_effect); - assert(expr.get(ID_statement)==ID_push_catch); - return static_cast(expr); + assert(code.get_statement()==ID_push_catch); + return static_cast(code); +} + +/// Pops an exception handler from the stack of active handlers +/// (i.e. whichever handler was most recently pushed by a +/// `code_push_catcht`). +class code_pop_catcht:public codet +{ +public: + code_pop_catcht():codet(ID_pop_catch) + { + } +}; + +static inline code_pop_catcht &to_code_pop_catch(codet &code) +{ + assert(code.get_statement()==ID_pop_catch); + return static_cast(code); +} + +static inline const code_pop_catcht &to_code_pop_catch(const codet &code) +{ + assert(code.get_statement()==ID_pop_catch); + return static_cast(code); +} + +/// A statement that catches an exception, assigning the exception +/// in flight to an expression (e.g. Java catch(Exception e) might be expressed +/// landingpadt(symbol_expr("e", ...))) +class code_landingpadt:public codet +{ + public: + code_landingpadt():codet(ID_exception_landingpad) + { + operands().resize(1); + } + explicit code_landingpadt(const exprt &catch_expr): + codet(ID_exception_landingpad) + { + copy_to_operands(catch_expr); + } + const exprt &catch_expr() const + { + return op0(); + } + exprt &catch_expr() + { + return op0(); + } +}; + +static inline code_landingpadt &to_code_landingpad(codet &code) +{ + assert(code.get_statement()==ID_exception_landingpad); + return static_cast(code); +} + +static inline const code_landingpadt &to_code_landingpad(const codet &code) +{ + assert(code.get_statement()==ID_exception_landingpad); + return static_cast(code); } /*! \brief A try/catch block