diff --git a/regression/cbmc-java/exceptions26/A.class b/regression/cbmc-java/exceptions26/A.class new file mode 100644 index 00000000000..503ff3deda0 Binary files /dev/null and b/regression/cbmc-java/exceptions26/A.class differ diff --git a/regression/cbmc-java/exceptions26/B.class b/regression/cbmc-java/exceptions26/B.class new file mode 100644 index 00000000000..90286c673da Binary files /dev/null and b/regression/cbmc-java/exceptions26/B.class differ diff --git a/regression/cbmc-java/exceptions26/test.class b/regression/cbmc-java/exceptions26/test.class new file mode 100644 index 00000000000..94f6293f49e Binary files /dev/null and b/regression/cbmc-java/exceptions26/test.class differ diff --git a/regression/cbmc-java/exceptions26/test.desc b/regression/cbmc-java/exceptions26/test.desc new file mode 100644 index 00000000000..0e2ccfc7f46 --- /dev/null +++ b/regression/cbmc-java/exceptions26/test.desc @@ -0,0 +1,8 @@ +CORE +test.class +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +-- +This test verifies that catches are executed in the correct order + diff --git a/regression/cbmc-java/exceptions26/test.java b/regression/cbmc-java/exceptions26/test.java new file mode 100644 index 00000000000..5abcf468b3b --- /dev/null +++ b/regression/cbmc-java/exceptions26/test.java @@ -0,0 +1,31 @@ +class A extends RuntimeException {} +class B extends A {} + +// This test verifies that catches are executed in the correct order +public class test { + public static void main (String args[]) { + int i = 0; + try { + try { + throw new A(); + } + catch(A exc) { + i++; + throw new B(); + } + finally + { + // Make sure A threw into the catch + assert(i==1); + i++; + } + } + catch(B exc) { + // Make sure finally was executed + assert(i==2); + i++; + } + // Make sure B was rethrown by finally + assert(i==3); + } +} diff --git a/regression/cbmc-java/exceptions27/A.class b/regression/cbmc-java/exceptions27/A.class new file mode 100644 index 00000000000..0b1fc6152a0 Binary files /dev/null and b/regression/cbmc-java/exceptions27/A.class differ diff --git a/regression/cbmc-java/exceptions27/B.class b/regression/cbmc-java/exceptions27/B.class new file mode 100644 index 00000000000..bdcdbd8f4e6 Binary files /dev/null and b/regression/cbmc-java/exceptions27/B.class differ diff --git a/regression/cbmc-java/exceptions27/test.class b/regression/cbmc-java/exceptions27/test.class new file mode 100644 index 00000000000..3cbd24c6d6d Binary files /dev/null and b/regression/cbmc-java/exceptions27/test.class differ diff --git a/regression/cbmc-java/exceptions27/test.desc b/regression/cbmc-java/exceptions27/test.desc new file mode 100644 index 00000000000..b4d6b49e539 --- /dev/null +++ b/regression/cbmc-java/exceptions27/test.desc @@ -0,0 +1,7 @@ +CORE +test.class +VERIFICATION SUCCESSFUL +-- +^warning: ignoring +-- +Tests embedded try-catch-finally to ensure the catching order is correct diff --git a/regression/cbmc-java/exceptions27/test.java b/regression/cbmc-java/exceptions27/test.java new file mode 100644 index 00000000000..b760e5736c6 --- /dev/null +++ b/regression/cbmc-java/exceptions27/test.java @@ -0,0 +1,54 @@ +import org.cprover.CProver; +class A extends RuntimeException {} +class B extends A {} + +// This test verifies that catches are executed in the correct order +public class test { + public static void main (String args[]) { + int i = 0; + int j = 0; + try { + try { + try { + if (CProver.nondetBoolean()) throw new A(); + else throw new B(); + } + catch(B exc) { + i++; + } + catch(A exc) { + i++; + throw new B(); + } + finally + { + // Make sure A threw into the catch + assert(i==1); + i++; + } + assert(i==2); + // Account for the rethrow in finally + j++; + } + catch(B exc) { + // Make sure finally was executed + assert(i==2); + i++; + throw new B(); + } + finally + { + assert ((i+j) == 3); + } + // Account for the rethrow in finally + j++; + } + catch(B exc) + { + i++; + } + // Make sure B was rethrown by finally when A was thrown + // or if B was thrown there was no rethrow + assert(i+j == 4); + } +} diff --git a/src/goto-programs/remove_exceptions.cpp b/src/goto-programs/remove_exceptions.cpp index 0fe32e947e3..5d2d758edb6 100644 --- a/src/goto-programs/remove_exceptions.cpp +++ b/src/goto-programs/remove_exceptions.cpp @@ -107,6 +107,12 @@ class remove_exceptionst const goto_programt::targett &, bool may_catch); + goto_programt::targett find_universal_exception( + const remove_exceptionst::stack_catcht &stack_catch, + goto_programt &goto_program, + std::size_t &universal_try, + std::size_t &universal_catch); + void add_exception_dispatch_sequence( goto_programt &goto_program, const goto_programt::targett &instr_it, @@ -229,6 +235,55 @@ void remove_exceptionst::instrument_exception_handler( instr_it->make_skip(); } +/// Find the innermost universal exception handler for the current +/// program location which may throw (i.e. the first catch of type +/// any in the innermost try that contains such). We record this one +/// because no handler after it can possibly catch. +/// The context is contained in stack_catch which is a stack of all the tries +/// which contain the current program location in their bodies. Each of these +/// in turn contains a list of all possible catches for that try giving the +/// type of exception they catch and the location of the handler. +/// This function returns the indices of the try and the catch within that try +/// as well as the location of the handler. +/// The first loop is in forward order because the insertion reverses the order +/// we note that try1{ try2 {} catch2c {} catch2d {}} catch1a() {} catch1b{} +/// must catch in the following order: 2c 2d 1a 1b hence the numerical index +/// is reversed whereas the letter ordering remains the same. +/// @param stack_catch exception table +/// @param goto_program program being evaluated +/// @param[out] universal_try returns the try block +/// corresponding to the desired exception handler +/// @param[out] universal_catch returns the catch block +/// corresponding to the exception desired exception handler +/// @return the desired exception handler +goto_programt::targett remove_exceptionst::find_universal_exception( + const remove_exceptionst::stack_catcht &stack_catch, + goto_programt &goto_program, + std::size_t &universal_try, + std::size_t &universal_catch) +{ + for(std::size_t i=stack_catch.size(); i>0;) + { + i--; + for(std::size_t j=0; j &locals) { - // 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); @@ -259,21 +310,28 @@ void remove_exceptionst::add_exception_dispatch_sequence( symbol_exprt exc_thrown = get_inflight_exception_global(); + std::size_t default_try=0; + std::size_t default_catch=(!stack_catch.empty()) ? stack_catch[0].size() : 0; + + goto_programt::targett default_target= + find_universal_exception(stack_catch, goto_program, + default_try, default_catch); + // add GOTOs implementing the dynamic dispatch of the - // exception handlers - for(std::size_t i=stack_catch.size(); i-->0;) + // exception handlers. + // The first loop is in forward order because the insertion reverses the order + // we note that try1{ try2 {} catch2c {} catch2d {}} catch1a() {} catch1b{} + // must catch in the following order: 2c 2d 1a 1b hence the numerical index + // is reversed whereas the letter ordering remains the same. + for(std::size_t i=default_try; i0;) + for(std::size_t j=(i==default_try) ? default_catch : stack_catch[i].size(); + j>0;) { + j--; 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 + if(!stack_catch[i][j].first.empty()) { // Normal exception handler, make an instanceof check. goto_programt::targett t_exc=goto_program.insert_after(instr_it);