From 6c9f05ea478901862fff5f464cebf991f6535094 Mon Sep 17 00:00:00 2001 From: Dario Cattaruzza Date: Thu, 16 Nov 2017 08:17:49 +0000 Subject: [PATCH] Fixes to exception handling behaviour Corrected the ordering of exception catching and added tests to verify the correct behaviour. Previously, the universal catch would be the one on the outermost try (should be the innermost try). Also, a throw can never throw directly past this catch, so there is no need to include these alternatives (they will appear in the rethrow of the finally). --- regression/cbmc-java/exceptions26/A.class | Bin 0 -> 189 bytes regression/cbmc-java/exceptions26/B.class | Bin 0 -> 164 bytes regression/cbmc-java/exceptions26/test.class | Bin 0 -> 780 bytes regression/cbmc-java/exceptions26/test.desc | 8 ++ regression/cbmc-java/exceptions26/test.java | 31 +++++++ regression/cbmc-java/exceptions27/A.class | Bin 0 -> 189 bytes regression/cbmc-java/exceptions27/B.class | Bin 0 -> 164 bytes regression/cbmc-java/exceptions27/test.class | Bin 0 -> 1068 bytes regression/cbmc-java/exceptions27/test.desc | 7 ++ regression/cbmc-java/exceptions27/test.java | 54 ++++++++++++ src/goto-programs/remove_exceptions.cpp | 86 ++++++++++++++++--- 11 files changed, 172 insertions(+), 14 deletions(-) create mode 100644 regression/cbmc-java/exceptions26/A.class create mode 100644 regression/cbmc-java/exceptions26/B.class create mode 100644 regression/cbmc-java/exceptions26/test.class create mode 100644 regression/cbmc-java/exceptions26/test.desc create mode 100644 regression/cbmc-java/exceptions26/test.java create mode 100644 regression/cbmc-java/exceptions27/A.class create mode 100644 regression/cbmc-java/exceptions27/B.class create mode 100644 regression/cbmc-java/exceptions27/test.class create mode 100644 regression/cbmc-java/exceptions27/test.desc create mode 100644 regression/cbmc-java/exceptions27/test.java diff --git a/regression/cbmc-java/exceptions26/A.class b/regression/cbmc-java/exceptions26/A.class new file mode 100644 index 0000000000000000000000000000000000000000..503ff3deda02d64dff00301332953b41a3c00f06 GIT binary patch literal 189 zcmX^0Z`VEs1_l!bUM>b^1}=66ZgvJ9Mg}&U%)HDJJ4Oa(4b3n{1{UZ1lvG9rexJ;| zRKL>Pq|~C2#H1Xc2v=}^X;E^jTPBFZS&~{@qL-CemdL}v!obSN!05=xAO+&<=OpH( z>j#zQm1O3ox>h8o7L;V>=P@WSFaa$E0Y)GOY5~%0K$a|!28pn0ZD(NI2$p6Cl5Ai> MkQ4`y$Hc%10C|lfRsaA1 literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/exceptions26/B.class b/regression/cbmc-java/exceptions26/B.class new file mode 100644 index 0000000000000000000000000000000000000000..90286c673da7b0ab3f04916c9712e58d582eaf11 GIT binary patch literal 164 zcmX^0Z`VEs1_l!bUM>b^1}=66ZgvJ9Mg}&U%)HDJJ4Oa(4b3n{1{UZ1lvG9rexJ;| zRKL>Pq|~C2#H1Xc2v=}^X;E^jTPBFZS&~{@qL-CemdL}v!obSNz~}_TjtmM6OhB_i ofDwp+GC-OQ$dU!pAQ4ur?F@_?!P4wNk_{}#1SC0tJSGNC06vKrO8@`> literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/exceptions26/test.class b/regression/cbmc-java/exceptions26/test.class new file mode 100644 index 0000000000000000000000000000000000000000..94f6293f49e20a855b6a7120dfb71508772ab68d GIT binary patch literal 780 zcmZuv%Wl&^6g^`*p2TsRw4rI}11J>LA;JAK)vx zVad86QHe-o&&Tiq2qvr2U)C0tU55Xz2v~cN(LER zmbl_TYUi4RtGFhyE>KwaqDY0Y-w&cke&n@#sw*H`0(Q+0{P@0rS>AXiVAcCwC6L?k z1GPIiYO8Qh2NO8*{6L^se!g?)z4od-FF2?+-?snp|m^_aH&pPxQpUSil|L>dfB8MeJh<7m_^tOqZ2dpk9gM6N$y2lty!=t51N^ y4-_Oy-&rTk{K=R$lX(Dh^O;X@jv=l0u*{FJ^~lbtO-82MrC_)Z^kA0~c=b^1}=66ZgvJ9Mg}&U%)HDJJ4Oa(4b3n{1{UZ1lvG9rexJ;| zRKL>Pq|~C2#H1Xc2v=}^X;E^jTPBFZS&~{@qL-CemdL}v!obSN!05=xAO+&<=OpH( z>j#zQm1O3ox>h8o7L;V>=P@WSFaa$E0Y)GOY5~%0K$a|!28pn0ZD(NI2$p6Cl5Ai> NCLqZHb^1}=66ZgvJ9Mg}&U%)HDJJ4Oa(4b3n{1{UZ1lvG9rexJ;| zRKL>Pq|~C2#H1Xc2v=}^X;E^jTPBFZS&~{@qL-CemdL}v!obSNz~}_TjtmM6OhB_i ofDwp+GC-OQ$dU!pAQ4ur?F@_?!P4wNk_{}#3?w;#JSGNC06vr$OaK4? literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/exceptions27/test.class b/regression/cbmc-java/exceptions27/test.class new file mode 100644 index 0000000000000000000000000000000000000000..3cbd24c6d6d5c215336e7f55a34100ea709b697b GIT binary patch literal 1068 zcmZuwT~8BH5IwiM?Y2vyrPaz;MFbTPsU#STpb-jc0-_1T&&0U28(b{AxLxoM@Phw9 z5`%9L-_S&iBsMWIQKP@WKcb1C=WZ$Gfi&H@duHa$nYpvycRzjt(2tCcDAGEPqgBHR z9SYJK+H?ewjzGsr4edI@670}%3a2%k5lD6z#iHqYmSY!3t)ekgF!KW9fk0@;vMuk5 zfYRA@M?lRwc~c-ZVcF*7;{1&1PRn3A<_*ghNOeA(m@}4)Ou?{cGgF>x*|UQ(v3ANc za!+p>3w}HmQJjWO4P64^pPIf zwWt$lsMZ^PoW|D_A!C1$g&Eytb zXUTLk+1tKlW42@GO>e|;3Z}sca84Xstje1$aJHOG-Yino9#(w6hYjK@ zc;j0YU+|T9z#o~7X8OW>i;$s~SRGm8MC-}dgg&17(L&ZFE^?@YI7;>=+#~*o_wWp@ ztkXsIHoQPPUZDf8`3Y?h`-~pe>SMKDe8YMCzy)RlHxS!FLWt`cQmHWw$Hp}@?2w%1 z4}yui#Q!46=RfX&qM=dny6N0S3Nq+70!&LO)Gf7^ccS0Fe4sv|zemj~G<6-S@(!BZ Wk8-n>{g5I!faq1ZMY8_@TK)sA0?k(d literal 0 HcmV?d00001 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);