From ac41f93895200d2532a5889dfd3deea81cddb1ed Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Wed, 14 Dec 2016 11:22:40 +0000 Subject: [PATCH 01/14] Use remove_instanceof in driver programs This adds a remove_instanceof call wherever there was an existing remove_virtual_functions call. --- src/cbmc/cbmc_parse_options.cpp | 2 +- src/goto-analyzer/goto_analyzer_parse_options.cpp | 2 +- src/symex/symex_parse_options.cpp | 1 - 3 files changed, 2 insertions(+), 3 deletions(-) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 7364752d093..842b0b26f70 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -894,7 +894,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); - // Java instanceof -> clsid comparison: + // Similar removal of RTTI inspection: remove_instanceof(symbol_table, goto_functions); // full slice? diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 68e28755041..89d3d56731c 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -387,7 +387,7 @@ bool goto_analyzer_parse_optionst::process_goto_program( remove_function_pointers(goto_model, cmdline.isset("pointer-check")); // Java virtual functions -> explicit dispatch tables: remove_virtual_functions(goto_model); - // Java instanceof -> clsid comparison: + // remove rtti remove_instanceof(goto_model); // do partial inlining diff --git a/src/symex/symex_parse_options.cpp b/src/symex/symex_parse_options.cpp index 518e64a2ecd..2ed3fedc518 100644 --- a/src/symex/symex_parse_options.cpp +++ b/src/symex/symex_parse_options.cpp @@ -369,7 +369,6 @@ bool symex_parse_optionst::process_goto_program(const optionst &options) remove_vector(goto_model); // Java virtual functions -> explicit dispatch tables: remove_virtual_functions(goto_model); - // Java instanceof -> clsid comparison: remove_instanceof(goto_model); rewrite_union(goto_model); adjust_float_expressions(goto_model); From ddb4f420d8e1c45b1b4c6829fc318dca2eea4d22 Mon Sep 17 00:00:00 2001 From: Cristina Date: Wed, 8 Feb 2017 17:16:06 +0000 Subject: [PATCH 02/14] Added a side effect expr that pushes/pops Java try-catch handlers + irep ids for Java exception handling These are used to recreate Java try-catch contructs from bytecode. --- src/util/irep_ids.txt | 4 +++- src/util/std_code.h | 30 ++++++++++++++++++++++++++++++ 2 files changed, 33 insertions(+), 1 deletion(-) diff --git a/src/util/irep_ids.txt b/src/util/irep_ids.txt index 9bcb7807671..666556d4b78 100644 --- a/src/util/irep_ids.txt +++ b/src/util/irep_ids.txt @@ -738,6 +738,8 @@ java_bytecode_index java_instanceof java_super_method_call java_enum_static_unwind +push_catch +handler string_constraint string_not_contains_constraint cprover_char_literal_func @@ -800,4 +802,4 @@ cprover_string_to_char_array_func cprover_string_to_lower_case_func cprover_string_to_upper_case_func cprover_string_trim_func -cprover_string_value_of_func \ No newline at end of file +cprover_string_value_of_func diff --git a/src/util/std_code.h b/src/util/std_code.h index 08aec694e9e..ed1f8f28b74 100644 --- a/src/util/std_code.h +++ b/src/util/std_code.h @@ -1122,6 +1122,36 @@ 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 +{ +public: + inline side_effect_expr_catcht():side_effect_exprt(ID_push_catch) + { + } + // TODO: change to ID_catch + inline explicit side_effect_expr_catcht(const irept &exception_list): + side_effect_exprt(ID_push_catch) + { + set(ID_exception_list, exception_list); + } +}; + +static inline side_effect_expr_catcht &to_side_effect_expr_catch(exprt &expr) +{ + assert(expr.id()==ID_side_effect); + assert(expr.get(ID_statement)==ID_push_catch); + return static_cast(expr); +} + +static inline const side_effect_expr_catcht &to_side_effect_expr_catch( + const exprt &expr) +{ + assert(expr.id()==ID_side_effect); + assert(expr.get(ID_statement)==ID_push_catch); + return static_cast(expr); +} /*! \brief A try/catch block */ From a805db9832a575078ce05088e419a6bbf0cb1442 Mon Sep 17 00:00:00 2001 From: Cristina Date: Thu, 15 Dec 2016 09:42:25 +0000 Subject: [PATCH 03/14] Regression tests for exception handling --- regression/exceptions/Makefile | 14 +++++++ regression/exceptions/exceptions1/A.class | Bin 0 -> 234 bytes regression/exceptions/exceptions1/B.class | Bin 0 -> 216 bytes regression/exceptions/exceptions1/C.class | Bin 0 -> 216 bytes regression/exceptions/exceptions1/D.class | Bin 0 -> 216 bytes regression/exceptions/exceptions1/test.class | Bin 0 -> 1025 bytes regression/exceptions/exceptions1/test.desc | 10 +++++ regression/exceptions/exceptions1/test.java | 30 ++++++++++++++ regression/exceptions/exceptions10/A.class | Bin 0 -> 241 bytes regression/exceptions/exceptions10/B.class | Bin 0 -> 216 bytes regression/exceptions/exceptions10/C.class | Bin 0 -> 216 bytes regression/exceptions/exceptions10/test.class | Bin 0 -> 875 bytes regression/exceptions/exceptions10/test.desc | 9 ++++ regression/exceptions/exceptions10/test.java | 25 +++++++++++ regression/exceptions/exceptions11/A.class | Bin 0 -> 276 bytes regression/exceptions/exceptions11/B.class | Bin 0 -> 216 bytes regression/exceptions/exceptions11/test.class | Bin 0 -> 976 bytes regression/exceptions/exceptions11/test.desc | 9 ++++ regression/exceptions/exceptions11/test.java | 39 ++++++++++++++++++ regression/exceptions/exceptions12/A.class | Bin 0 -> 241 bytes regression/exceptions/exceptions12/B.class | Bin 0 -> 216 bytes regression/exceptions/exceptions12/C.class | Bin 0 -> 216 bytes regression/exceptions/exceptions12/F.class | Bin 0 -> 641 bytes regression/exceptions/exceptions12/test.class | Bin 0 -> 740 bytes regression/exceptions/exceptions12/test.desc | 9 ++++ regression/exceptions/exceptions12/test.java | 27 ++++++++++++ regression/exceptions/exceptions13/A.class | Bin 0 -> 241 bytes regression/exceptions/exceptions13/B.class | Bin 0 -> 216 bytes regression/exceptions/exceptions13/C.class | Bin 0 -> 216 bytes regression/exceptions/exceptions13/F.class | Bin 0 -> 405 bytes regression/exceptions/exceptions13/test.class | Bin 0 -> 740 bytes regression/exceptions/exceptions13/test.desc | 9 ++++ regression/exceptions/exceptions13/test.java | 28 +++++++++++++ regression/exceptions/exceptions14/A.class | Bin 0 -> 241 bytes regression/exceptions/exceptions14/B.class | Bin 0 -> 216 bytes regression/exceptions/exceptions14/C.class | Bin 0 -> 216 bytes regression/exceptions/exceptions14/test.class | Bin 0 -> 858 bytes regression/exceptions/exceptions14/test.desc | 8 ++++ regression/exceptions/exceptions14/test.java | 24 +++++++++++ regression/exceptions/exceptions2/A.class | Bin 0 -> 234 bytes regression/exceptions/exceptions2/B.class | Bin 0 -> 216 bytes regression/exceptions/exceptions2/C.class | Bin 0 -> 216 bytes regression/exceptions/exceptions2/test.class | Bin 0 -> 771 bytes regression/exceptions/exceptions2/test.desc | 10 +++++ regression/exceptions/exceptions2/test.java | 18 ++++++++ regression/exceptions/exceptions3/A.class | Bin 0 -> 234 bytes regression/exceptions/exceptions3/B.class | Bin 0 -> 216 bytes regression/exceptions/exceptions3/C.class | Bin 0 -> 216 bytes regression/exceptions/exceptions3/test.class | Bin 0 -> 751 bytes regression/exceptions/exceptions3/test.desc | 9 ++++ regression/exceptions/exceptions3/test.java | 17 ++++++++ regression/exceptions/exceptions4/A.class | Bin 0 -> 234 bytes regression/exceptions/exceptions4/B.class | Bin 0 -> 216 bytes regression/exceptions/exceptions4/C.class | Bin 0 -> 216 bytes regression/exceptions/exceptions4/test.class | Bin 0 -> 743 bytes regression/exceptions/exceptions4/test.desc | 8 ++++ regression/exceptions/exceptions4/test.java | 19 +++++++++ regression/exceptions/exceptions5/A.class | Bin 0 -> 234 bytes regression/exceptions/exceptions5/B.class | Bin 0 -> 216 bytes regression/exceptions/exceptions5/C.class | Bin 0 -> 216 bytes regression/exceptions/exceptions5/D.class | Bin 0 -> 216 bytes regression/exceptions/exceptions5/test.class | Bin 0 -> 997 bytes regression/exceptions/exceptions5/test.desc | 8 ++++ regression/exceptions/exceptions5/test.java | 27 ++++++++++++ regression/exceptions/exceptions6/A.class | Bin 0 -> 280 bytes regression/exceptions/exceptions6/B.class | Bin 0 -> 216 bytes regression/exceptions/exceptions6/C.class | Bin 0 -> 216 bytes regression/exceptions/exceptions6/D.class | Bin 0 -> 216 bytes regression/exceptions/exceptions6/test.class | Bin 0 -> 806 bytes regression/exceptions/exceptions6/test.desc | 9 ++++ regression/exceptions/exceptions6/test.java | 26 ++++++++++++ regression/exceptions/exceptions7/A.class | Bin 0 -> 241 bytes regression/exceptions/exceptions7/B.class | Bin 0 -> 216 bytes regression/exceptions/exceptions7/C.class | Bin 0 -> 216 bytes regression/exceptions/exceptions7/test.class | Bin 0 -> 871 bytes regression/exceptions/exceptions7/test.desc | 9 ++++ regression/exceptions/exceptions7/test.java | 25 +++++++++++ regression/exceptions/exceptions8/A.class | Bin 0 -> 241 bytes regression/exceptions/exceptions8/B.class | Bin 0 -> 216 bytes regression/exceptions/exceptions8/C.class | Bin 0 -> 216 bytes regression/exceptions/exceptions8/test.class | Bin 0 -> 935 bytes regression/exceptions/exceptions8/test.desc | 9 ++++ regression/exceptions/exceptions8/test.java | 29 +++++++++++++ regression/exceptions/exceptions9/A.class | Bin 0 -> 276 bytes regression/exceptions/exceptions9/B.class | Bin 0 -> 216 bytes regression/exceptions/exceptions9/C.class | Bin 0 -> 216 bytes regression/exceptions/exceptions9/test.class | Bin 0 -> 976 bytes regression/exceptions/exceptions9/test.desc | 8 ++++ regression/exceptions/exceptions9/test.java | 39 ++++++++++++++++++ 89 files changed, 511 insertions(+) create mode 100644 regression/exceptions/Makefile create mode 100644 regression/exceptions/exceptions1/A.class create mode 100644 regression/exceptions/exceptions1/B.class create mode 100644 regression/exceptions/exceptions1/C.class create mode 100644 regression/exceptions/exceptions1/D.class create mode 100644 regression/exceptions/exceptions1/test.class create mode 100644 regression/exceptions/exceptions1/test.desc create mode 100644 regression/exceptions/exceptions1/test.java create mode 100644 regression/exceptions/exceptions10/A.class create mode 100644 regression/exceptions/exceptions10/B.class create mode 100644 regression/exceptions/exceptions10/C.class create mode 100644 regression/exceptions/exceptions10/test.class create mode 100644 regression/exceptions/exceptions10/test.desc create mode 100644 regression/exceptions/exceptions10/test.java create mode 100644 regression/exceptions/exceptions11/A.class create mode 100644 regression/exceptions/exceptions11/B.class create mode 100644 regression/exceptions/exceptions11/test.class create mode 100644 regression/exceptions/exceptions11/test.desc create mode 100644 regression/exceptions/exceptions11/test.java create mode 100644 regression/exceptions/exceptions12/A.class create mode 100644 regression/exceptions/exceptions12/B.class create mode 100644 regression/exceptions/exceptions12/C.class create mode 100644 regression/exceptions/exceptions12/F.class create mode 100644 regression/exceptions/exceptions12/test.class create mode 100644 regression/exceptions/exceptions12/test.desc create mode 100644 regression/exceptions/exceptions12/test.java create mode 100644 regression/exceptions/exceptions13/A.class create mode 100644 regression/exceptions/exceptions13/B.class create mode 100644 regression/exceptions/exceptions13/C.class create mode 100644 regression/exceptions/exceptions13/F.class create mode 100644 regression/exceptions/exceptions13/test.class create mode 100644 regression/exceptions/exceptions13/test.desc create mode 100644 regression/exceptions/exceptions13/test.java create mode 100644 regression/exceptions/exceptions14/A.class create mode 100644 regression/exceptions/exceptions14/B.class create mode 100644 regression/exceptions/exceptions14/C.class create mode 100644 regression/exceptions/exceptions14/test.class create mode 100644 regression/exceptions/exceptions14/test.desc create mode 100644 regression/exceptions/exceptions14/test.java create mode 100644 regression/exceptions/exceptions2/A.class create mode 100644 regression/exceptions/exceptions2/B.class create mode 100644 regression/exceptions/exceptions2/C.class create mode 100644 regression/exceptions/exceptions2/test.class create mode 100644 regression/exceptions/exceptions2/test.desc create mode 100644 regression/exceptions/exceptions2/test.java create mode 100644 regression/exceptions/exceptions3/A.class create mode 100644 regression/exceptions/exceptions3/B.class create mode 100644 regression/exceptions/exceptions3/C.class create mode 100644 regression/exceptions/exceptions3/test.class create mode 100644 regression/exceptions/exceptions3/test.desc create mode 100644 regression/exceptions/exceptions3/test.java create mode 100644 regression/exceptions/exceptions4/A.class create mode 100644 regression/exceptions/exceptions4/B.class create mode 100644 regression/exceptions/exceptions4/C.class create mode 100644 regression/exceptions/exceptions4/test.class create mode 100644 regression/exceptions/exceptions4/test.desc create mode 100644 regression/exceptions/exceptions4/test.java create mode 100644 regression/exceptions/exceptions5/A.class create mode 100644 regression/exceptions/exceptions5/B.class create mode 100644 regression/exceptions/exceptions5/C.class create mode 100644 regression/exceptions/exceptions5/D.class create mode 100644 regression/exceptions/exceptions5/test.class create mode 100644 regression/exceptions/exceptions5/test.desc create mode 100644 regression/exceptions/exceptions5/test.java create mode 100644 regression/exceptions/exceptions6/A.class create mode 100644 regression/exceptions/exceptions6/B.class create mode 100644 regression/exceptions/exceptions6/C.class create mode 100644 regression/exceptions/exceptions6/D.class create mode 100644 regression/exceptions/exceptions6/test.class create mode 100644 regression/exceptions/exceptions6/test.desc create mode 100644 regression/exceptions/exceptions6/test.java create mode 100644 regression/exceptions/exceptions7/A.class create mode 100644 regression/exceptions/exceptions7/B.class create mode 100644 regression/exceptions/exceptions7/C.class create mode 100644 regression/exceptions/exceptions7/test.class create mode 100644 regression/exceptions/exceptions7/test.desc create mode 100644 regression/exceptions/exceptions7/test.java create mode 100644 regression/exceptions/exceptions8/A.class create mode 100644 regression/exceptions/exceptions8/B.class create mode 100644 regression/exceptions/exceptions8/C.class create mode 100644 regression/exceptions/exceptions8/test.class create mode 100644 regression/exceptions/exceptions8/test.desc create mode 100644 regression/exceptions/exceptions8/test.java create mode 100644 regression/exceptions/exceptions9/A.class create mode 100644 regression/exceptions/exceptions9/B.class create mode 100644 regression/exceptions/exceptions9/C.class create mode 100644 regression/exceptions/exceptions9/test.class create mode 100644 regression/exceptions/exceptions9/test.desc create mode 100644 regression/exceptions/exceptions9/test.java diff --git a/regression/exceptions/Makefile b/regression/exceptions/Makefile new file mode 100644 index 00000000000..5ac5a21995e --- /dev/null +++ b/regression/exceptions/Makefile @@ -0,0 +1,14 @@ +default: tests.log + +test: + @../test.pl -c ../../../src/cbmc/cbmc + +tests.log: ../test.pl + @../test.pl -c ../../../src/cbmc/cbmc + +show: + @for dir in *; do \ + if [ -d "$$dir" ]; then \ + vim -o "$$dir/*.java" "$$dir/*.out"; \ + fi; \ + done; diff --git a/regression/exceptions/exceptions1/A.class b/regression/exceptions/exceptions1/A.class new file mode 100644 index 0000000000000000000000000000000000000000..eb19ef6be2b4b0dc315cdfd2ae091ecc67882efd GIT binary patch literal 234 zcmXX=%MQU%5IsX5TBX7dSYn|YJ0fW$R*em@zv_l7)h5;QT~-ncAK;_J+%n0`dF0Gw z-k;|Szyuu^b+l}>ZTJLhrczbR3H8BnOE4DMUK0FBrE*oCcQW6IUBXT`%3_ghMXt2| zn?`X|7ha9RDZyQ5Wgg3=(s8GdmtuSpSK+~cNuZF>(>h2*dI&bhJiF;j=%dE}=pt^; iGFr?6M(voR2k6eE2Aii7D1o9M#q%+AiT z@6YoEV1a=P9X%U;8$Q8WsZ3RCf!TDLcb3PedAtLN)W> zG^(>I`7{ic1ox2FMIv{qi93}ntJy`|ga-pAfda+`BWV1+DPr)3*K{pl# WT<*@-G|^!l`~vXc^F-)=Q^5xrb|N0ia<-WNlvOJ0;V`m%{smNkcs&?*7 zqdu#OPor>6a1TXOrgEp+xKqojUR=aYcraiRC}aefK;!Ri5ra3(7ON$5>zMNg=*~ie V&E4u^J=Weo00%Blg#It(eE}M}B0B&8 literal 0 HcmV?d00001 diff --git a/regression/exceptions/exceptions1/test.class b/regression/exceptions/exceptions1/test.class new file mode 100644 index 0000000000000000000000000000000000000000..c76687b1bc7a0547086d763afd30f531210e3b7a GIT binary patch literal 1025 zcmZuvZBNr+6g|({ty|ZPF%&@&5kWUp<_m&uXoR7Oro#^y5+Q+fTZQ82Ok0eORw}P5==E;f zRp_%l-(B9@ZMwl*NmeM@-Imi?bplWPlb{}Ldm($+ksC%eR_{8VuP|6zw|AURPNn1c zTa}e4@cgZsbXOdz*-Ok+EkSibO+kx-96<|$I8bvxOO6w4asB`FQ^>7EPU}O%`513Q zai|L=p&AP5`BvwIn7Pv33tH|=PiSOh(`i}GLJ#!;P(Z)J(AoA2e|38i z1l@oXrGbH}g&O7+3TK&bnmcYQqIPGYdWW)8kG30nf!jXq#l@pN{z1*xaGkH#$5&Q` zA(>93fqG+r_XT(nJgW;RQ;<1aL6vgU$mkWZP0kH+T_@fk z*G;nB#Yn8gd-h3VjQ@;Kfdczo#VEHBX|FM^vAe-D&W$GN-5^SGN*)t&MJ-07tZl?- zjA%1P<3!YvRX1sG@eCrpZJ?B2G*FgnO0L^^&cAc|cr$So&|l1bLw+BIegIwj3iJF! RO3Ne?)^mC8yL1wm{teh!r=|b^ literal 0 HcmV?d00001 diff --git a/regression/exceptions/exceptions1/test.desc b/regression/exceptions/exceptions1/test.desc new file mode 100644 index 00000000000..baf72e7da81 --- /dev/null +++ b/regression/exceptions/exceptions1/test.desc @@ -0,0 +1,10 @@ +CORE +test.class + +^EXIT=10$ +^SIGNAL=0$ +^.*assertion at file test.java line 26 function.*: FAILURE$ +\*\* 1 of 35 failed (2 iterations)$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/exceptions/exceptions1/test.java b/regression/exceptions/exceptions1/test.java new file mode 100644 index 00000000000..bc925b32d65 --- /dev/null +++ b/regression/exceptions/exceptions1/test.java @@ -0,0 +1,30 @@ +class A extends Throwable {} +class B extends A {} +class C extends B {} +class D extends C {} + +public class test { + public static void main (String arg[]) { + try { + D d = new D(); + C c = new C(); + B b = new B(); + A a = new A(); + A e = a; + throw e; + } + catch(D exc) { + assert false; + } + catch(C exc) { + assert false; + } + catch(B exc) { + assert false; + } + catch(A exc) { + assert false; + } + } +} + diff --git a/regression/exceptions/exceptions10/A.class b/regression/exceptions/exceptions10/A.class new file mode 100644 index 0000000000000000000000000000000000000000..963ae156be051ca07ea2d602053e012a3d27a7a4 GIT binary patch literal 241 zcmXX=O;5r=5PbuswY3W2=*gpUuorF+lg8kw;Q*%hZQaP2c5B)#@o#xD@!${OM-gX{ zNoL+h-b?0i{P_hi$0WiKR{^dAj0ygd4ckY;@a{e*cu&o%CX6#SdfnHBZeLVUi8IZb zQdPNX+3BSuQG(CW@UysN#6;bBCelyKv8QYrJ6YoqP1btzNpmRpEZ_t;J0Rp-H$s}9|kN*P*5s4yPo>K82_(?21 literal 0 HcmV?d00001 diff --git a/regression/exceptions/exceptions10/B.class b/regression/exceptions/exceptions10/B.class new file mode 100644 index 0000000000000000000000000000000000000000..47ae8f218e49b4ac942425d72a88b21c2772b518 GIT binary patch literal 216 zcmXX7D1o9M#q%+AiT z@6YoEV1a=P9X%U;8$Q8WsZ3RCf!TDLcb3PedAtLN)W> zG^(>I`7{ic1ox2FMIv{qi93}ntJy`|ga-pAfda+`BWV1+DPr)3*K{pl# WT<*@-G|^!l`~vXc^F-)=Q^5xrb|NGzlS}mmtic&3AsXFXn91H3~A};DMBd*dk)?i7TBz61){t5m7 zYjj2&nUTFe%JJM-=|UEHxgY1Ad+vSj*Y6)c0j%Mni6R;XZkf=~D4>Ab2AU?aXqa?X z473c~F>x3746G_tmYq2EqQnn__=z7oy`k4vPp=^h)Gu(9|U;J@UPu}@4IqbxXlXY^u4MWoQXxSa{y-%*fR5x+l_b;3e zX%$7Y&4J?w3f1Ntd*Au!w1-YGXm^vy4+iTZLpegRNebPG25eEe0LUQ~@*D1OJb~E_ zN0IA2^F?n#B&`a$g=x%?vSY!*ltOLNvGZ>!PopS|EL={3o9rsp2HFh9BU|a6SQy`qZi{yAdYb>Xb+ut;YQFpJD&;ExO}pLPUgJ5 zs~2-yJ(_tz(#y)+6f;w~rr$ypUfhz_Y;-Nq4`p5DcIuk-B-mxRcs1`PMU34PJ81LZ zNO01?L1Fy!;J)_3E$rkYw{O9f9;f_J@nd1ou&wAPN!VQ>+RSwS8`4)_h(1XpXl6}q ToQk@~D*fN2?r-=3bA-+x##1h8 literal 0 HcmV?d00001 diff --git a/regression/exceptions/exceptions11/B.class b/regression/exceptions/exceptions11/B.class new file mode 100644 index 0000000000000000000000000000000000000000..3af09687e1afeb9c7dd88272ec5fde0e48c3b12d GIT binary patch literal 216 zcmXX7D18_mM(%+AiT z@6YoEV1a=P9X%U;8$Q8WsZ3RCf!TDLcb3PedAtLN#-1 z8r4~qd>RHzf_up8B9S}Q#GOi()$Af}!h->mKmlWe5j6hZ6fth>=A0{wU*lk3vm!G4I`v^Ugi@-psGxKYjvOz#R)IR1C~o(ByqNi2+3dBm~bpd_V zZ@B`4b+6+-?(Q_);F$yqWb1y@X|FqhC;eVfk6wErIqH!cMvLTl<@@9))yg%pI}Fs9 z85Rv%?z^V+SERqqkBHP-OE2qN&ReJ2b~>BYwJ7j9n~O@H z6Kt|#?mubHMZjEYwtEd(YkoIqx(_`mKPeT?NlF_T46*()zZDy44BEJXQGr6g;PT0^ z9t43O*f@s*rAZ0{H*MU)ZGlW5{-m+xHY4(RoLoP=+UC&NOUn(tz-^t9vg@eJ1Sh_M zaV{*y?TSo6YN4frRa{Ci0>jd`xOcO0|pLZ5MmzbpA=<*L^@)s-~@?5tvc1psij#U z&rE^khIv*|RAMSb*ep6spS{yMudHF(Be^7l6ndy%qXE_#F@k#3zf}` zD4{@^sA=^U{H3&~24?bvUOL^$f+_|KWe2{&-i4v>L63bw{NMeIktYt#z9+X>qNAbw E2bxcsM*si- literal 0 HcmV?d00001 diff --git a/regression/exceptions/exceptions11/test.desc b/regression/exceptions/exceptions11/test.desc new file mode 100644 index 00000000000..cb92a091217 --- /dev/null +++ b/regression/exceptions/exceptions11/test.desc @@ -0,0 +1,9 @@ +CORE +test.class + +^EXIT=10$ +^SIGNAL=0$ +^.*assertion at file test.java line 36 function.*: FAILURE$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/exceptions/exceptions11/test.java b/regression/exceptions/exceptions11/test.java new file mode 100644 index 00000000000..032af621fc3 --- /dev/null +++ b/regression/exceptions/exceptions11/test.java @@ -0,0 +1,39 @@ +class A extends RuntimeException { + int i=1; +}; + +class B extends A { +}; + +public class test { + static int foo(int k) { + try { + if(k==0) + { + A a = new A(); + throw a; + } + else + { + A b = new A(); + throw b; + } + + } + catch(B exc) { + assert exc.i==1; + } + return 1; + } + + + public static void main (String args[]) { + try { + A a = new A(); + foo(6); + } + catch(A exc) { + assert exc.i==2; + } + } +} diff --git a/regression/exceptions/exceptions12/A.class b/regression/exceptions/exceptions12/A.class new file mode 100644 index 0000000000000000000000000000000000000000..963ae156be051ca07ea2d602053e012a3d27a7a4 GIT binary patch literal 241 zcmXX=O;5r=5PbuswY3W2=*gpUuorF+lg8kw;Q*%hZQaP2c5B)#@o#xD@!${OM-gX{ zNoL+h-b?0i{P_hi$0WiKR{^dAj0ygd4ckY;@a{e*cu&o%CX6#SdfnHBZeLVUi8IZb zQdPNX+3BSuQG(CW@UysN#6;bBCelyKv8QYrJ6YoqP1btzNpmRpEZ_t;J0Rp-H$s}9|kN*P*5s4yPo>K82_(?21 literal 0 HcmV?d00001 diff --git a/regression/exceptions/exceptions12/B.class b/regression/exceptions/exceptions12/B.class new file mode 100644 index 0000000000000000000000000000000000000000..47ae8f218e49b4ac942425d72a88b21c2772b518 GIT binary patch literal 216 zcmXX7D1o9M#q%+AiT z@6YoEV1a=P9X%U;8$Q8WsZ3RCf!TDLcb3PedAtLN)W> zG^(>I`7{ic1ox2FMIv{qi93}ntJy`|ga-pAfda+`BWV1+DPr)3*K{pl# WT<*@-G|^!l`~vXc^F-)=Q^5xrb|Nukq z=Ym8fD$zS1g?Q_R^nk40ee?8Y-pu&-pP#<~Y~oIc0ILdDLU>pWpm0^;T8OG6yCJUQ zhQdw3(wfe5lNB}{=TB^|hlv>pWM5F*vSV936jatX_5}V;Ix>QVfgPI{lMh3ay>enf zYmmk|+0&VI@s#w7cQ$A0p#OmPn>1z3p^LX&Y(B?=x!pp?@1N_BWePhL)VJbfY8vjQ zlPorU>nwu8{?EwbJZ3YoZDdyMbVysK;0MR_`7| zjtD#~@UESaXc9+LyoeSfU}={8g=&w?$_c#J$6V9B)4@0RhiIIjN}_gpROW`X_Gs)X zxA`xDI=`T7sKNTnY{fZssi{+W0T-FqAlohx9dPD;i7Ex}nL=lt(&bqzo23!3*it`G bKZNqX!moUX|Nl&`MipN4$W6Y&z{BOgR*PqV literal 0 HcmV?d00001 diff --git a/regression/exceptions/exceptions12/test.class b/regression/exceptions/exceptions12/test.class new file mode 100644 index 0000000000000000000000000000000000000000..a4350fcd81d62534433b034e2f9d88328d74c8b8 GIT binary patch literal 740 zcmZuu%Tg0T6g@q8OfnhrRE($u5H)}j7wn)c1qnOJ^-AHff} zMysGos&wy1S)Lw|EOgP`_ufADoYS{|{`&SEzy=;Ws9?#)T?ZDH%(iUfUKwTFxADM% zZ7#bGR6=*PUJ99BLQ(BP~6g?PM-+mx-0tv`JHH_1ZtiR)vL+z zP{n%&EYS2KUk3X!)+WC!=F_)2A%~Z$B;929vDBf!Z1;_KBtOVrAj5HQkj6S3ZyI)S zNFA?FWKMnbO}uToWIQHI>px8bGlNw6?_SFHnIs=6P}=f?OViFEn#8{9Yh$r&T&x>m z7gf|K*LU$S3$|Ujm=S1CZ9V%tkQZ?r#dKl1Z9HuSq<}#KJ5x3cUhs%bwYh%7jXy@ud8yO5} fG|OjjPGHkeKKB*He;;Q!3b5R#W&{gNEG+&8z8Qep literal 0 HcmV?d00001 diff --git a/regression/exceptions/exceptions12/test.desc b/regression/exceptions/exceptions12/test.desc new file mode 100644 index 00000000000..4654e88cbb6 --- /dev/null +++ b/regression/exceptions/exceptions12/test.desc @@ -0,0 +1,9 @@ +CORE +test.class + +^EXIT=10$ +^SIGNAL=0$ +^.*assertion at file test.java line 12 function.*: FAILURE$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/exceptions/exceptions12/test.java b/regression/exceptions/exceptions12/test.java new file mode 100644 index 00000000000..5828419fac6 --- /dev/null +++ b/regression/exceptions/exceptions12/test.java @@ -0,0 +1,27 @@ +class A extends RuntimeException {} +class B extends A {} +class C extends B {} + +class F { + void foo() { + try { + B b = new B(); + throw b; + } + catch(B exc) { + assert false; + } + } +} + +public class test { + public static void main (String args[]) { + try { + F f = new F(); + f.foo(); + } + catch(B exc) { + assert false; + } + } +} diff --git a/regression/exceptions/exceptions13/A.class b/regression/exceptions/exceptions13/A.class new file mode 100644 index 0000000000000000000000000000000000000000..963ae156be051ca07ea2d602053e012a3d27a7a4 GIT binary patch literal 241 zcmXX=O;5r=5PbuswY3W2=*gpUuorF+lg8kw;Q*%hZQaP2c5B)#@o#xD@!${OM-gX{ zNoL+h-b?0i{P_hi$0WiKR{^dAj0ygd4ckY;@a{e*cu&o%CX6#SdfnHBZeLVUi8IZb zQdPNX+3BSuQG(CW@UysN#6;bBCelyKv8QYrJ6YoqP1btzNpmRpEZ_t;J0Rp-H$s}9|kN*P*5s4yPo>K82_(?21 literal 0 HcmV?d00001 diff --git a/regression/exceptions/exceptions13/B.class b/regression/exceptions/exceptions13/B.class new file mode 100644 index 0000000000000000000000000000000000000000..47ae8f218e49b4ac942425d72a88b21c2772b518 GIT binary patch literal 216 zcmXX7D1o9M#q%+AiT z@6YoEV1a=P9X%U;8$Q8WsZ3RCf!TDLcb3PedAtLN)W> zG^(>I`7{ic1ox2FMIv{qi93}ntJy`|ga-pAfda+`BWV1+DPr)3*K{pl# WT<*@-G|^!l`~vXc^F-)=Q^5xrb|N~W_5d{6*B%>=cEi9Za@cY?f zme?@W+*)qu`SH-amqnOJ^-AHff} zMysGos&wy1S)Lw|EOgP`_ufADoYS{|{`&SEzy=;Ws9?#)T?ZDH%(iUfUKwTFxADM% zZ7#bGR6=*PUJ99BLQ(BP~6g?PM-+mx-0tv`JHH_1ZtiR)vL+z zP{n%&EYS2KUk3X!)+WC!=F_)2A%~Z$B;929vDBf!Z1;_KBtOVrAj5HQkj6S3ZyI)S zNFA?FWKMnbO}uToWIQHI>px8bGlNw6?_SFHnIs=6P}=f?OViFEn#8{9Yh$r&T&x>m z7gf|K*LU$S3$|Ujm=S1CZ9V%tkQZ?r#dKl1Z9HuSq<}#KJ5x3cUhs%bwYh%7jXy@ud8yO5} fG|OjjPGHkeKKB*He;;Q!3b5R#W&{gNEG+&8z8Qep literal 0 HcmV?d00001 diff --git a/regression/exceptions/exceptions13/test.desc b/regression/exceptions/exceptions13/test.desc new file mode 100644 index 00000000000..cb7c1b81341 --- /dev/null +++ b/regression/exceptions/exceptions13/test.desc @@ -0,0 +1,9 @@ +CORE +test.class + +^EXIT=10$ +^SIGNAL=0$ +^.*assertion at file test.java line 25 function.*: FAILURE$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/exceptions/exceptions13/test.java b/regression/exceptions/exceptions13/test.java new file mode 100644 index 00000000000..56d763f68d3 --- /dev/null +++ b/regression/exceptions/exceptions13/test.java @@ -0,0 +1,28 @@ +class A extends RuntimeException {} +class B extends A {} +class C extends B {} + +class F { + void foo() { + try { + B b = new B(); + throw b; + } + catch(B exc) { + throw exc; + } + } +} + +public class test { + + public static void main (String args[]) { + try { + F f = new F(); + f.foo(); + } + catch(B exc) { + assert false; + } + } +} diff --git a/regression/exceptions/exceptions14/A.class b/regression/exceptions/exceptions14/A.class new file mode 100644 index 0000000000000000000000000000000000000000..963ae156be051ca07ea2d602053e012a3d27a7a4 GIT binary patch literal 241 zcmXX=O;5r=5PbuswY3W2=*gpUuorF+lg8kw;Q*%hZQaP2c5B)#@o#xD@!${OM-gX{ zNoL+h-b?0i{P_hi$0WiKR{^dAj0ygd4ckY;@a{e*cu&o%CX6#SdfnHBZeLVUi8IZb zQdPNX+3BSuQG(CW@UysN#6;bBCelyKv8QYrJ6YoqP1btzNpmRpEZ_t;J0Rp-H$s}9|kN*P*5s4yPo>K82_(?21 literal 0 HcmV?d00001 diff --git a/regression/exceptions/exceptions14/B.class b/regression/exceptions/exceptions14/B.class new file mode 100644 index 0000000000000000000000000000000000000000..47ae8f218e49b4ac942425d72a88b21c2772b518 GIT binary patch literal 216 zcmXX7D1o9M#q%+AiT z@6YoEV1a=P9X%U;8$Q8WsZ3RCf!TDLcb3PedAtLN)W> zG^(>I`7{ic1ox2FMIv{qi93}ntJy`|ga-pAfda+`BWV1+DPr)3*K{pl# WT<*@-G|^!l`~vXc^F-)=Q^5xrb|NKQjnAn#E;R9?=Y8JyydTf=o__!NT6@^@1Qu*R z@ScxOx?cEFCJW^4q3a9|ozR#5G^oXI{D?j5*o)$AR-ZV2Ah1+>Z67=Do%+BD`t?p6 z`ayqNb{8(^*llL2-iHLYB(|Hf)(QLURrp7#zCjx5%nH_g96<~CR zqtNyCd`UMe8LdkaCKh0Ebemt(#5{5Wr5U^CpS|pc;V@)Qi&SK>j)x{5VMD;0Wxwbi zdv47A%tGw}S4+)3FY-gLchQfG;}I{o*CQ| zcl=-EENNzOsKTZeDjX(%yG{OOYC>xx(UL`msw`3{&@WQg3UP(1s*E;BbCWk)yxAjF zDWQQBYceR|3aJ;lhpP#yCg>VtTM4?JNZrQ`++@`)ev3$VbllFhbS%qbCC4^*F4osb h3YeBRK4b0_x;BQUenR^1RmyHDDCSeS@G>0*m0$24k%|BS literal 0 HcmV?d00001 diff --git a/regression/exceptions/exceptions14/test.desc b/regression/exceptions/exceptions14/test.desc new file mode 100644 index 00000000000..dc5ca4fa5cb --- /dev/null +++ b/regression/exceptions/exceptions14/test.desc @@ -0,0 +1,8 @@ +CORE +test.class + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/exceptions/exceptions14/test.java b/regression/exceptions/exceptions14/test.java new file mode 100644 index 00000000000..24f44a5d3d9 --- /dev/null +++ b/regression/exceptions/exceptions14/test.java @@ -0,0 +1,24 @@ +class A extends RuntimeException {} +class B extends A {} +class C extends B {} + +public class test { + public static void main (String args[]) { + try { + try { + C c = new C(); + A a = new A(); + } + catch(C exc) { + assert false; + } + catch(B exc) { + assert false; + } + } + catch(A exc) { + assert false; + } + + } +} diff --git a/regression/exceptions/exceptions2/A.class b/regression/exceptions/exceptions2/A.class new file mode 100644 index 0000000000000000000000000000000000000000..eb19ef6be2b4b0dc315cdfd2ae091ecc67882efd GIT binary patch literal 234 zcmXX=%MQU%5IsX5TBX7dSYn|YJ0fW$R*em@zv_l7)h5;QT~-ncAK;_J+%n0`dF0Gw z-k;|Szyuu^b+l}>ZTJLhrczbR3H8BnOE4DMUK0FBrE*oCcQW6IUBXT`%3_ghMXt2| zn?`X|7ha9RDZyQ5Wgg3=(s8GdmtuSpSK+~cNuZF>(>h2*dI&bhJiF;j=%dE}=pt^; iGFr?6M(voR2k6eE2Aii7D1o9M#q%+AiT z@6YoEV1a=P9X%U;8$Q8WsZ3RCf!TDLcb3PedAtLN)W> zG^(>I`7{ic1ox2FMIv{qi93}ntJy`|ga-pAfda+`BWV1+DPr)3*K{pl# WT<*@-G|^!l`~vXc^F-)=Q^5xrb|Nfgc6r6RO*m2x6O`rrwftCVkQkqL|tq>%@0U0<1Rid0W&MIti9b`L*-_k$O zbBjbJD$zSX3Naf(BLs)_``9;c=DqcgpWnU%*v6Iz4{HwYda#ULFT%w=2lqV`O#Hw@ z6B`a%0=0FSrYgzwI8LAHR1P9F6cGCYg=9%t&31@BlsXnzZoUf+3-?PC)U1uFB(*MkEUW?acU)r+`IjyY7RPSo(S z7o}zsUT~HBSmk4Qd?!(<8+Lj*a2%BRU1Zdu6}0)*8N>-43l)9~zmr&^@6Y@yYK)4w zf~(9J@F}Y;+RbxVZ_l{L_C;`t{1Hm$C@|q%9P`Eg&YVmU=AW^N^w40On{uvEDtKIS zcob{oUgu4NVpqu5rW&KCMWjpAGOkfaiMMsu3Dy|Tn|0k`U}5za)c=H& literal 0 HcmV?d00001 diff --git a/regression/exceptions/exceptions2/test.desc b/regression/exceptions/exceptions2/test.desc new file mode 100644 index 00000000000..eb7fa309bea --- /dev/null +++ b/regression/exceptions/exceptions2/test.desc @@ -0,0 +1,10 @@ +CORE +test.class + +^EXIT=10$ +^SIGNAL=0$ +^.*assertion at file test.java line 15 function.*: FAILURE$ +^\*\* 1 of 20 failed (2 iterations)$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/exceptions/exceptions2/test.java b/regression/exceptions/exceptions2/test.java new file mode 100644 index 00000000000..420b50219c1 --- /dev/null +++ b/regression/exceptions/exceptions2/test.java @@ -0,0 +1,18 @@ +class A extends Throwable {} +class B extends A {} +class C extends B {} + +public class test { + public static void main (String args[]) { + try { + B b = new B(); + throw b; + } + catch(C exc) { + assert false; + } + catch(B exc) { + assert false; + } + } +} diff --git a/regression/exceptions/exceptions3/A.class b/regression/exceptions/exceptions3/A.class new file mode 100644 index 0000000000000000000000000000000000000000..eb19ef6be2b4b0dc315cdfd2ae091ecc67882efd GIT binary patch literal 234 zcmXX=%MQU%5IsX5TBX7dSYn|YJ0fW$R*em@zv_l7)h5;QT~-ncAK;_J+%n0`dF0Gw z-k;|Szyuu^b+l}>ZTJLhrczbR3H8BnOE4DMUK0FBrE*oCcQW6IUBXT`%3_ghMXt2| zn?`X|7ha9RDZyQ5Wgg3=(s8GdmtuSpSK+~cNuZF>(>h2*dI&bhJiF;j=%dE}=pt^; iGFr?6M(voR2k6eE2Aii7D1o9M#q%+AiT z@6YoEV1a=P9X%U;8$Q8WsZ3RCf!TDLcb3PedAtLN)W> zG^(>I`7{ic1ox2FMIv{qi93}ntJy`|ga-pAfda+`BWV1+DPr)3*K{pl# WT<*@-G|^!l`~vXc^F-)=Q^5xrb|Nfgc5PfSqaqPNjnm`BzN(%*&@R3Vztq>%DI2d{eszf<$oK@J8I>>eqzokbm zJr^V@QHkF9QHZxDG(vFLoq4lwX5P&H`1$QSfKA-@;bYy!4Ih@VH$9ZF;o_E$qQSR) z+(FYtOQ5zP(^Msyp2X=Boyx&j4F$xWKyh2gI(sN!H(R>`PH!?)0!yKe)ywI@KqapX zS)dwDB01ibi8go^bh5WPWsNXXX|~1e1F2(ydh<=VFF(l6SjMAHKTC8x+A`H`^)ccd z_QO!6dq92e^xS0+l&)XRxoLjO&<(dSh;qBMw!n6E!@q zMXA}84_xCO*7*@W|439CraL_w90z6IOGF)7L0f2_KpfMtP~lzt9mF#IVCGj*Bl2(o z7a1|hpUAdo+o!NzpTIr~KcjGng;Nv>-LoV9)!&ihoL{0Shj}He5ZigjRk(S?$n_}o z5<9F==oLzBkztgqk?RrH`6}|4IvTmUHZGG5#*AL)xr?jiu8V7B_EZTJLhrczbR3H8BnOE4DMUK0FBrE*oCcQW6IUBXT`%3_ghMXt2| zn?`X|7ha9RDZyQ5Wgg3=(s8GdmtuSpSK+~cNuZF>(>h2*dI&bhJiF;j=%dE}=pt^; iGFr?6M(voR2k6eE2Aii7D1o9M#q%+AiT z@6YoEV1a=P9X%U;8$Q8WsZ3RCf!TDLcb3PedAtLN)W> zG^(>I`7{ic1ox2FMIv{qi93}ntJy`|ga-pAfda+`BWV1+DPr)3*K{pl# WT<*@-G|^!l`~vXc^F-)=Q^5xrb|Nfgc5Pj=7apJgXnm|b*4gCVr7Me?Mtq>%@0U3G-szf<$oK@J8+Q@bgzl1~o z0Ox{4B`VQ7KML{IgysOUc6Vm>&Ad0W{`u?s4*Y0ysJ>V!4?R3+&ivrnWB1s2!u>G?PWBwAGSQkzDxs0U+hmj(` z6657e;1Vl0DQ}qw!@fdnkr|7)LDn*F8d%B{wQv)+h-h+ou%A0vu5=x=OvT$*4en-G gV4+t0hSDhZTJLhrczbR3H8BnOE4DMUK0FBrE*oCcQW6IUBXT`%3_ghMXt2| zn?`X|7ha9RDZyQ5Wgg3=(s8GdmtuSpSK+~cNuZF>(>h2*dI&bhJiF;j=%dE}=pt^; iGFr?6M(voR2k6eE2Aii7D1o9M#q%+AiT z@6YoEV1a=P9X%U;8$Q8WsZ3RCf!TDLcb3PedAtLN)W> zG^(>I`7{ic1ox2FMIv{qi93}ntJy`|ga-pAfda+`BWV1+DPr)3*K{pl# WT<*@-G|^!l`~vXc^F-)=Q^5xrb|N0ia<-WNlvOJ0;V`m%{smNkcs&?*7 zqdu#OPor>6a1TXOrgEp+xKqojUR=aYcraiRC}aefK;!Ri5ra3(7ON$5>zMNg=*~ie V&E4u^J=Weo00%Blg#It(eE}M}B0B&8 literal 0 HcmV?d00001 diff --git a/regression/exceptions/exceptions5/test.class b/regression/exceptions/exceptions5/test.class new file mode 100644 index 0000000000000000000000000000000000000000..1b251e32471f5d7fe325eac698256834648f5e0a GIT binary patch literal 997 zcmZuv+fEZv6kVq??X=U<7SKw)AS&p9O1)Ik77etO#AJ#O7!tuC({=)br8P5y@mu%- zp3y`So5;H#Wn6nic)&F0?6r6IZLKrEe*gFhpo|wLawr*iU?L{=p$T2=BNGX+k4+>| zN?{0P15Zq(CHU0D9G)3?t}r_31cB>^UcVPKyufL7-Hw73oW| zp*Ylql28qWqNx%U}ef9M#~d^VE12Gst6DVeD-C#ecfJ z^8LO~iqgP9C4(yF74m19Z(2KUJEV4Jp?a6HQ;&`tc)r^??Zw5zJ^n$>*KmWcmg6g{ z{FqE9(m=g2%KHMn60M?*&m2J=62x$kcOnYvC=h4tZhbUBGPe_ zxwqN<4o?BeZ39-eW?)*b8M*F)Q}3NVP&ujshDV0JBfAenKY*@%gL(e3q-7kj%z`}W JeL6AB{sHnbp}znC literal 0 HcmV?d00001 diff --git a/regression/exceptions/exceptions5/test.desc b/regression/exceptions/exceptions5/test.desc new file mode 100644 index 00000000000..dc5ca4fa5cb --- /dev/null +++ b/regression/exceptions/exceptions5/test.desc @@ -0,0 +1,8 @@ +CORE +test.class + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/exceptions/exceptions5/test.java b/regression/exceptions/exceptions5/test.java new file mode 100644 index 00000000000..e539f06df1e --- /dev/null +++ b/regression/exceptions/exceptions5/test.java @@ -0,0 +1,27 @@ +class A extends Throwable {} +class B extends A {} +class C extends B {} +class D extends C {}public class test { + public static void main (String arg[]) { + try { + D d = new D(); + C c = new C(); + B b = new B(); + A a = new A(); + A e = a; + throw e; + } + catch(D exc) { + assert false; + } + catch(C exc) { + assert false; + } + catch(B exc) { + assert false; + } + catch(A exc) { + } + } +} + diff --git a/regression/exceptions/exceptions6/A.class b/regression/exceptions/exceptions6/A.class new file mode 100644 index 0000000000000000000000000000000000000000..fbaaf105dbaddd4eb32dc843a524880a3ff50fe4 GIT binary patch literal 280 zcmXYru};H45JYF4ON@<4AW%_JLJHE*5g|ngBqWOhQ2L8G!6N63oHNRAQ6MA=K7fxx zj6;gO-FZ8s+n?XBZvbaFNMW#>po6^_!x;MlQPz#1H&L(QLeM!rnF-8g_2>kHT)n$( z7IRlW*m+4Z%&WqdGh1t`H_(J7D1o9M#q%+AiT z@6YoEV1a=P9X%U;8$Q8WsZ3RCf!TDLcb3PedAtLN)W> zG^(>I`7{ic1ox2FMIv{qi93}ntJy`|ga-pAfda+`BWV1+DPr)3*?v$M18 z`}2GOSYqfwN8iT4MnJIEDp&P}piibT!3c|!Bm|Ml<-WNlvOJ0;V`mf*X@L|9tP{`O~42{3HMGW3BTdWq$tz*s}pgRi< WHg~Ht9XPE0UjQyVo(R1z<$nPh2O>NG literal 0 HcmV?d00001 diff --git a/regression/exceptions/exceptions6/D.class b/regression/exceptions/exceptions6/D.class new file mode 100644 index 0000000000000000000000000000000000000000..12179e84294d669f8f9f06e51f5400f5cc8f5db6 GIT binary patch literal 216 zcmXX0ia<-WNlvOJ0;V`m%{smNkcs&?*7 zqdu#OPor>6a1TXOrgEp+xKqojUR=aYcraiRC}aefK;!Ri5ra3(7ON$5>zMNg=*~ie V&E4u^J=Weo00%Blg#It(eE}M}B0B&8 literal 0 HcmV?d00001 diff --git a/regression/exceptions/exceptions6/test.class b/regression/exceptions/exceptions6/test.class new file mode 100644 index 0000000000000000000000000000000000000000..e0c57f3e31882cdf481a96c6f9f53834e3440c85 GIT binary patch literal 806 zcmZuv&2JJx9DTF9u95vnGdRS%dZ*3+_Va4KEQ?qd8~dhytE z)!4))Hu2~mWqh;NVxotc`F+0Mn>X|0=htrlHgMO5gNBLgHZ(LW*tlWQYMNNJkyV+N zg`D!&Y}~{x6YBz{x);Yml*nlqKajCEoCG5Qu`Q78%1|cv1oYvhMR)3ZlPxcj%0CGj$!i%C!%c!X>9Bj(lc7Ml`O4k#-g)hb7mnM5B$DB{ zqtJ!qddykDd!M`8V~_6kRi_t?iB$Seqrk!-@%%SWy|?LDUY&Oo$aVe633q!iokf1| zNGhh5BD1dMJ6J@46MGI8aK=Fe%L0`-v)&&~9!AkLVqu>|RJVz?gWI?xP?%RgAMONx zLT%=u%?V}YeMdnoqhNH3N509732M5H8lTAF(}_Yw(V(S+C@64WqSxjrcxGCM5C=3g z6uD>9pp6o3=XU|l;v78-Wt?Y3HGgNd#^gZg$fASglwS)5YjR3p^2#$) z#RXcbrizOx`z|iwGSRMZIWV4>xLWR;sFm5baw^6~S_>={?Jvmh!8G<^=$~NxD~tll OKy&UZ`L5B?Q2zx(l8Oxg literal 0 HcmV?d00001 diff --git a/regression/exceptions/exceptions6/test.desc b/regression/exceptions/exceptions6/test.desc new file mode 100644 index 00000000000..79549d80731 --- /dev/null +++ b/regression/exceptions/exceptions6/test.desc @@ -0,0 +1,9 @@ +CORE +test.class + +^EXIT=10$ +^SIGNAL=0$ +^.*assertion at file test.java line 18 function.*: FAILURE$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/exceptions/exceptions6/test.java b/regression/exceptions/exceptions6/test.java new file mode 100644 index 00000000000..fd9a7fd5326 --- /dev/null +++ b/regression/exceptions/exceptions6/test.java @@ -0,0 +1,26 @@ +class A extends RuntimeException { + int i; + A() { + i = 1; + } +} +class B extends A {} +class C extends B {} + +public class test { + public static void main (String args[]) { + try { + try { + int i = 0; + throw new A(); + } + catch(A exc) { + assert exc.i==2; + } + } + catch(B exc) { + assert exc.i==2; + } + + } +} diff --git a/regression/exceptions/exceptions7/A.class b/regression/exceptions/exceptions7/A.class new file mode 100644 index 0000000000000000000000000000000000000000..963ae156be051ca07ea2d602053e012a3d27a7a4 GIT binary patch literal 241 zcmXX=O;5r=5PbuswY3W2=*gpUuorF+lg8kw;Q*%hZQaP2c5B)#@o#xD@!${OM-gX{ zNoL+h-b?0i{P_hi$0WiKR{^dAj0ygd4ckY;@a{e*cu&o%CX6#SdfnHBZeLVUi8IZb zQdPNX+3BSuQG(CW@UysN#6;bBCelyKv8QYrJ6YoqP1btzNpmRpEZ_t;J0Rp-H$s}9|kN*P*5s4yPo>K82_(?21 literal 0 HcmV?d00001 diff --git a/regression/exceptions/exceptions7/B.class b/regression/exceptions/exceptions7/B.class new file mode 100644 index 0000000000000000000000000000000000000000..47ae8f218e49b4ac942425d72a88b21c2772b518 GIT binary patch literal 216 zcmXX7D1o9M#q%+AiT z@6YoEV1a=P9X%U;8$Q8WsZ3RCf!TDLcb3PedAtLN)W> zG^(>I`7{ic1ox2FMIv{qi93}ntJy`|ga-pAfda+`BWV1+DPr)3*K{pl# WT<*@-G|^!l`~vXc^F-)=Q^5xrb|NB-u+J+&n?qEXyU`Y_q(UxcfNDJ+wVWWegjZL&47s&9jgWud6o@mSV_acnvRDC zbP2BOcw}G$6&;TS3d>Fyx|^JHQyDmZztWBZ z&+qR@cF|=YyU9%9$f(Xpbw9>vL)JS%pL~UXlnZ3rk<)#5;JlBU(|&BSERfpm4kjjy z_HYz*-IgaMr=_Y5Da6DKEH-U&)lFoP6DUp<)_>1tKL~~aa~hN)i*-CPv5BgHHO+p} zId;1dXEcSH1CE!zdv53jZto8t6-Og};B1eu#0N6@fWj(D1&maX1s3;N-YPr=&&1jV z#5n^6dG5(85Cz8OB%Z@H-qM)Ibt1C(2eVb4tud6>7aZ*v8qdVR`lbB|$x~#;&3ni+mQr{NluuZl5 zD8>%<=ttHRaf8Y&^54V)cUgNY#!7K?n_su%Xd(98!W}G9!(FafBwy-S$~AP{liU3q oDP_~EQPkoBrsa(<$ecpg&Y-EEk^Fn6k}Uznd@3hj;zhxOUndZfg#Z8m literal 0 HcmV?d00001 diff --git a/regression/exceptions/exceptions7/test.desc b/regression/exceptions/exceptions7/test.desc new file mode 100644 index 00000000000..e138e4349ec --- /dev/null +++ b/regression/exceptions/exceptions7/test.desc @@ -0,0 +1,9 @@ +CORE +test.class + +^EXIT=10$ +^SIGNAL=0$ +^.*assertion at file test.java line 21 function.*: FAILURE$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/exceptions/exceptions7/test.java b/regression/exceptions/exceptions7/test.java new file mode 100644 index 00000000000..e03be8a56fb --- /dev/null +++ b/regression/exceptions/exceptions7/test.java @@ -0,0 +1,25 @@ +class A extends RuntimeException {} +class B extends A {} +class C extends B {} + +public class test { + public static void main (String args[]) { + try { + try { + C c = new C(); + A a = new A(); + throw a; + } + catch(C exc) { + assert false; + } + catch(B exc) { + assert false; + } + } + catch(A exc) { + assert false; + } + + } +} diff --git a/regression/exceptions/exceptions8/A.class b/regression/exceptions/exceptions8/A.class new file mode 100644 index 0000000000000000000000000000000000000000..963ae156be051ca07ea2d602053e012a3d27a7a4 GIT binary patch literal 241 zcmXX=O;5r=5PbuswY3W2=*gpUuorF+lg8kw;Q*%hZQaP2c5B)#@o#xD@!${OM-gX{ zNoL+h-b?0i{P_hi$0WiKR{^dAj0ygd4ckY;@a{e*cu&o%CX6#SdfnHBZeLVUi8IZb zQdPNX+3BSuQG(CW@UysN#6;bBCelyKv8QYrJ6YoqP1btzNpmRpEZ_t;J0Rp-H$s}9|kN*P*5s4yPo>K82_(?21 literal 0 HcmV?d00001 diff --git a/regression/exceptions/exceptions8/B.class b/regression/exceptions/exceptions8/B.class new file mode 100644 index 0000000000000000000000000000000000000000..47ae8f218e49b4ac942425d72a88b21c2772b518 GIT binary patch literal 216 zcmXX7D1o9M#q%+AiT z@6YoEV1a=P9X%U;8$Q8WsZ3RCf!TDLcb3PedAtLN)W> zG^(>I`7{ic1ox2FMIv{qi93}ntJy`|ga-pAfda+`BWV1+DPr)3*K{pl# WT<*@-G|^!l`~vXc^F-)=Q^5xrb|Nfgc5Ph3Cwd2@nJ|MJEXn<0Z6dFDX92y~#00-*AA*d4NQYh~Lsb z&~rheKqPwSMRbKYo7u4qycjOxUREsF_H}xuoNUi4>|PGPs%M zwydLWA}yDKU-GSFvP@4)<4S(pz4;7M?>V|^W4*H(L zwBrxG=X<+dFMKJ%3I!+Vxq}Ti^u?YywfK!6k;93-C|)JURuGW3OXRe~_CE9kw~6ge z?DpQSyYI%il+I$iu0K>LRbD$g?t8aBaEIIVP8|Bf?Nt$@TuE*+S#!f}7ApQHki*~* z6pTi1Floi?1bbo6d+Lkuv}juvehWF|$=c#-b2TlTL*7Cb(+V@E3YvdL^&|{~ki~^T z$BKn}xUY~qjeODF@p>`Gb?RylIBE9O_aZ;^`X^lMKHlR6$GnNld?=d_s&X?@ok#_5ZRp+UArfNq}hXe@}xljFe;ta7h!DmsTWk@IVNb(k=6FjpcBwigMxmG(~OEwP2 z@g_``N{-n|{5O(m@VChK$&k~g9APh!!Qh&~EUgUDd0ZfxlWdliWSexUiMU15gY6iUnxQ0{lCo@a zjxy#cs!T!4v_x!;Eg8%#bFPX}S>DYOmB&bYGSMrz%2OJ!psnjz$hLG`%QAEEWOOUz iSRh}>e1^3TT|0o5`~>6QHxQx}64oPmsp~WnsQdzqm68qs literal 0 HcmV?d00001 diff --git a/regression/exceptions/exceptions8/test.desc b/regression/exceptions/exceptions8/test.desc new file mode 100644 index 00000000000..a400cbb8d02 --- /dev/null +++ b/regression/exceptions/exceptions8/test.desc @@ -0,0 +1,9 @@ +CORE +test.class + +^EXIT=10$ +^SIGNAL=0$ +^.*assertion at file test.java line 23 function.*: FAILURE$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/exceptions/exceptions8/test.java b/regression/exceptions/exceptions8/test.java new file mode 100644 index 00000000000..7d6af5324b7 --- /dev/null +++ b/regression/exceptions/exceptions8/test.java @@ -0,0 +1,29 @@ +class A extends RuntimeException {} +class B extends A {} +class C extends B {} + +public class test { + static void foo() { + try { + B b = new B(); + throw b; + } + catch(C exc) { + int i=0; + } + } + + public static void main (String args[]) { + try { + A a = new A(); + foo(); + throw a; + } + catch(B exc) { + assert false; + } + catch(A exc) { + assert false; + } + } +} diff --git a/regression/exceptions/exceptions9/A.class b/regression/exceptions/exceptions9/A.class new file mode 100644 index 0000000000000000000000000000000000000000..ad46eafd1d9234e74590cd579aff0f7eb17f9bfd GIT binary patch literal 276 zcmXYrK}*9x5QX2QYh%`EYxU&GqxN7g9t4X}N((~ppwjy`F1nI#B;AOA%Yz6W`UCt? z#h2Q{%$xaU9y7n|pA~>h9BU|a6SQy`qZi{yAdYb>Xb+ut;YQFpJD&;ExO}pLPUgJ5 zs~2-yJ(_tz(#y)+6f;w~rr$ypUfhz_Y;-Nq4`p5DcIuk-B-mxRcs1`PMU34PJ81LZ zNO01?L1Fy!;J)_3E$rkYw{O9f9;f_J@nd1ou&wAPN!VQ>+RSwS8`4)_h(1XpXl6}q ToQk@~D*fN2?r-=3bA-+x##1h8 literal 0 HcmV?d00001 diff --git a/regression/exceptions/exceptions9/B.class b/regression/exceptions/exceptions9/B.class new file mode 100644 index 0000000000000000000000000000000000000000..3af09687e1afeb9c7dd88272ec5fde0e48c3b12d GIT binary patch literal 216 zcmXX7D18_mM(%+AiT z@6YoEV1a=P9X%U;8$Q8WsZ3RCf!TDLcb3PedAtLN#-1 z8r4~qd>RHzf_up8B9S}Q#GOi()$Af}!h->mKmlWe5j6hZ6ftK{pl# WT<*@-G|^!l`~vXc^F-)=Q^5xrb|Nl=Sil_%DO3#1TF~TuIf(&WNkYe* zfvN=q6^oIpNv0W@w{Q*D4J-)cCY>;JgUIu{;e9W38XdPKAT|UNOJ3KD?h3?8<#hpl z)o-~1gLSX#KHk}GxWO|C7Rc89rqfw>0#EwApdP*ULUPn2H;fj^@yhqfQL2?|WOo>- zFEcC}wA^=1>90tCiyslGwa961J#yYCI`+f2+m6>2$d_K$H=Vamwc~W#)wL+_y6r`! z&k5SBnEOwfa}h9?nw?%l)|$T)G~I`ul%JFe=Om?#42D>Lncs?yGzM+lz^Fi>UvT+k zSPz204{V%6fzl*}ftxmN;kH1g4}a3wbej?RJWj43UhQz`?4{*~Uf{M)N!fL@!vrV3 zfpIP@#qEkrL299;gX9?EnWb0dEqKQ(2N3%-G~{?DRM5m3+V(L3XOX98O0|s0#~+E- zc+VGikvfF-;(!~NJ?dNa&xr3LH~SR{{R0LLVGv>->7Nv3fkZlDs^A2PL9IH~%BiJU zAkR#J<%W4yQB-0oMA$4kOrO2eI|^7$T$eZ|(_iuV<9nq$*?f{UDyEMaoQX-qRSN$M$-Fr$Qy5oZ!}EL1i# zqJ#ovBB#__@R!n_8ko)#I&->{1yu|f$_{*ky$eI%gC6^W_`mxZBTpQfeNS$&L`OsU E51X%=N&o-= literal 0 HcmV?d00001 diff --git a/regression/exceptions/exceptions9/test.desc b/regression/exceptions/exceptions9/test.desc new file mode 100644 index 00000000000..dc5ca4fa5cb --- /dev/null +++ b/regression/exceptions/exceptions9/test.desc @@ -0,0 +1,8 @@ +CORE +test.class + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/exceptions/exceptions9/test.java b/regression/exceptions/exceptions9/test.java new file mode 100644 index 00000000000..53f7838fd03 --- /dev/null +++ b/regression/exceptions/exceptions9/test.java @@ -0,0 +1,39 @@ +class A extends RuntimeException { + int i=1; +}; + +class B extends A { +}; + +public class test { + static int foo(int k) { + try { + if(k==0) + { + A a = new A(); + throw a; + } + else + { + A b = new A(); + throw b; + } + + } + catch(B exc) { + assert exc.i==1; + } + return 1; + } + + + public static void main (String args[]) { + try { + A a = new A(); + foo(6); + } + catch(A exc) { + assert exc.i==1; + } + } +} From 1aafb6103b2b0b14fd7f7e2a4b2216143a74c96b Mon Sep 17 00:00:00 2001 From: Cristina Date: Wed, 8 Feb 2017 17:26:27 +0000 Subject: [PATCH 04/14] Recreate the try-catch structure from the exception table - Adjust the working set conversion algorithm from bytecode to codet to also handler exception handlers. - Use CATCH-PUSH and CATCH-POP expressions to recreate the try-catch blocks. --- .../java_bytecode_convert_method.cpp | 225 ++++++++++++++++-- .../java_bytecode_convert_method_class.h | 1 + 2 files changed, 201 insertions(+), 25 deletions(-) diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index f101d19c824..69d4dffd04f 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -108,6 +108,13 @@ exprt::operandst java_bytecode_convert_methodt::pop(std::size_t n) return operands; } +void java_bytecode_convert_methodt::pop_residue(std::size_t n) +{ + std::size_t residue_size=n<=stack.size()?n:stack.size(); + + stack.resize(stack.size()-residue_size); +} + void java_bytecode_convert_methodt::push(const exprt::operandst &o) { stack.resize(stack.size()+o.size()); @@ -169,7 +176,6 @@ const exprt java_bytecode_convert_methodt::variable( symbol_exprt result(identifier, t); result.set(ID_C_base_name, base_name); used_local_names.insert(result); - return result; } else @@ -866,6 +872,24 @@ codet java_bytecode_convert_methodt::convert_instructions( a_entry.first->second.successors.push_back(next->address); } + if(i_it->statement=="athrow" || + i_it->statement=="invokestatic" || + i_it->statement=="invokevirtual") + { + // find the corresponding try-catch blocks and add the handlers + // to the targets + for(std::size_t e=0; eaddress>=method.exception_table[e].start_pc && + i_it->addresssecond.successors.push_back( + method.exception_table[e].handler_pc); + targets.insert(method.exception_table[e].handler_pc); + } + } + } + if(i_it->statement=="goto" || i_it->statement==patternt("if_?cmp??") || i_it->statement==patternt("if??") || @@ -943,7 +967,6 @@ codet java_bytecode_convert_methodt::convert_instructions( setup_local_variables(method, address_map); std::set working_set; - bool assertion_failure=false; if(!instructions.empty()) working_set.insert(instructions.front().address); @@ -953,6 +976,7 @@ codet java_bytecode_convert_methodt::convert_instructions( std::set::iterator cur=working_set.begin(); address_mapt::iterator a_it=address_map.find(*cur); assert(a_it!=address_map.end()); + unsigned cur_pc=*cur; working_set.erase(cur); if(a_it->second.done) @@ -989,6 +1013,46 @@ codet java_bytecode_convert_methodt::convert_instructions( statement=std::string(id2string(statement), 0, statement.size()-2); } + // we throw away the first statement in an exception handler + // as we don't know if a function call had a normal or exceptional return + size_t e; + for(e=0; eaddress, + false); + + // throw away the operands + pop_residue(bytecode_info.pop); + + // add a CATCH-PUSH signaling a handler + side_effect_expr_catcht catch_handler_expr; + // pack the exception variable so that it can be used + // later for instrumentation + catch_handler_expr.set(ID_handler, exc_var); + codet catch_handler=code_expressiont(catch_handler_expr); + + code_labelt newlabel(label(i2string(cur_pc)), code_blockt()); + code_blockt label_block=to_code_block(newlabel.code()); + code_blockt handler_block; + handler_block.move_to_operands(c); + handler_block.move_to_operands(catch_handler); + handler_block.move_to_operands(label_block); + c=handler_block; + + break; + } + } + + if(esource_location; - throw_expr.copy_to_operands(op[0]); - c=code_expressiont(throw_expr); - results[0]=op[0]; - } - else - { - // TODO: this can be removed once we properly handle throw - // if this athrow is generated by an assertion, then skip it - c=code_skipt(); - assertion_failure=false; - } + side_effect_expr_throwt throw_expr; + throw_expr.add_source_location()=i_it->source_location; + throw_expr.copy_to_operands(op[0]); + c=code_expressiont(throw_expr); + results[0]=op[0]; } else if(statement=="checkcast") { @@ -1061,14 +1115,7 @@ codet java_bytecode_convert_methodt::convert_instructions( statement=="invokevirtual" || statement=="invokestatic") { - // Remember that this is triggered by an assertion - if(statement=="invokespecial" && - id2string(arg0.get(ID_identifier)) - .find("AssertionError")!=std::string::npos) - { - assertion_failure=true; - } - const bool use_this(statement!="invokestatic"); + const bool use_this(statement != "invokestatic"); const bool is_virtual( statement=="invokevirtual" || statement=="invokeinterface"); @@ -1992,6 +2039,134 @@ codet java_bytecode_convert_methodt::convert_instructions( c.operands()=op; } + // next we do the exception handling + std::vector exception_ids; + std::vector handler_labels; + + // add the CATCH-PUSH instruction(s) + // be aware of different try-catch blocks with the same starting pc + std::size_t pos=0; + int end_pc=-1; + while(possource_location.get_line().empty()) c.add_source_location()=i_it->source_location; diff --git a/src/java_bytecode/java_bytecode_convert_method_class.h b/src/java_bytecode/java_bytecode_convert_method_class.h index ae4ba711640..4fb24c47b84 100644 --- a/src/java_bytecode/java_bytecode_convert_method_class.h +++ b/src/java_bytecode/java_bytecode_convert_method_class.h @@ -141,6 +141,7 @@ class java_bytecode_convert_methodt:public messaget exprt::operandst pop(std::size_t n); + void pop_residue(std::size_t n); void push(const exprt::operandst &o); bool is_constructor(const class_typet::methodt &method); From b9283bbd14e445d161aae284e4161574d0ad4636 Mon Sep 17 00:00:00 2001 From: Cristina Date: Wed, 14 Dec 2016 15:24:53 +0000 Subject: [PATCH 05/14] Remove throw/try-catch and add the required instrumentation For each function f we record its exceptional return value as variable f#exception_value and each throw/function call is instrumented with assignments involving these variables. Then, the dynamic dispatch of exception handlers is done by using instanceof over such variables. --- regression/exceptions/exceptions1/test.desc | 2 +- .../exceptions/exceptions15/InetAddress.class | Bin 0 -> 251 bytes .../exceptions15/InetSocketAddress.class | Bin 0 -> 263 bytes regression/exceptions/exceptions15/test.class | Bin 0 -> 1006 bytes regression/exceptions/exceptions15/test.desc | 8 + regression/exceptions/exceptions15/test.java | 20 + regression/exceptions/exceptions2/test.desc | 2 +- regression/exceptions/exceptions4/test.class | Bin 743 -> 914 bytes regression/exceptions/exceptions4/test.java | 2 + regression/exceptions/exceptions5/test.class | Bin 997 -> 1198 bytes regression/exceptions/exceptions5/test.java | 45 +- src/cbmc/cbmc_parse_options.cpp | 3 + .../goto_analyzer_parse_options.cpp | 3 + .../goto_instrument_parse_options.cpp | 3 + src/goto-programs/Makefile | 4 +- src/goto-programs/goto_convert.cpp | 80 +++ src/goto-programs/goto_convert_class.h | 4 + src/goto-programs/goto_convert_exceptions.cpp | 67 ++ .../goto_convert_side_effect.cpp | 25 + src/goto-programs/remove_exceptions.cpp | 586 ++++++++++++++++++ src/goto-programs/remove_exceptions.h | 24 + .../java_bytecode_convert_method.cpp | 132 ++-- src/symex/symex_parse_options.cpp | 4 + src/util/irep_ids.txt | 1 - src/util/std_code.h | 1 - 25 files changed, 936 insertions(+), 80 deletions(-) create mode 100644 regression/exceptions/exceptions15/InetAddress.class create mode 100644 regression/exceptions/exceptions15/InetSocketAddress.class create mode 100644 regression/exceptions/exceptions15/test.class create mode 100644 regression/exceptions/exceptions15/test.desc create mode 100644 regression/exceptions/exceptions15/test.java create mode 100644 src/goto-programs/remove_exceptions.cpp create mode 100644 src/goto-programs/remove_exceptions.h diff --git a/regression/exceptions/exceptions1/test.desc b/regression/exceptions/exceptions1/test.desc index baf72e7da81..7c6146907d0 100644 --- a/regression/exceptions/exceptions1/test.desc +++ b/regression/exceptions/exceptions1/test.desc @@ -4,7 +4,7 @@ test.class ^EXIT=10$ ^SIGNAL=0$ ^.*assertion at file test.java line 26 function.*: FAILURE$ -\*\* 1 of 35 failed (2 iterations)$ +\*\* 1 of 4 failed (2 iterations)$ ^VERIFICATION FAILED$ -- ^warning: ignoring diff --git a/regression/exceptions/exceptions15/InetAddress.class b/regression/exceptions/exceptions15/InetAddress.class new file mode 100644 index 0000000000000000000000000000000000000000..3229324e624dde300b6b541750ba938c64539274 GIT binary patch literal 251 zcmYjL%L>9k44i0fwbloIfk*XVFWwYE1VJczP`q#3MOSJI?dpGd5RBA;vM9y`caxp-NG_CFtZ7;3;Za4qX5S)!MscHOZ`v-bd56#7!QV>B9f*vg1Uy?gsTsgIcyWh>;*9Bn6Ea5_wy;6I@t#$?TN)8~h3U z0bWHDNHo!Rf0Xe|S=)kXI(O#YbI+N3W`F$_|cZHLUYcNw*C;NIJq%NwVKMc%#)@86=7l6Vr{gSn8!_ zQ^_=4m}%_!hkiZs-_(AvzwRHjhohYWg~cGs>~S}fmI~x*Xv`>@dFRY1 z9!eObd8> zu`tXv-%i>nbMKu4FoG*Q(MD9bn&#(>7Gth#ePQTr&9_@C=jE)GKwQNbn}l&HBYBpQ zShJTo+#U|A!(nweZlIcRd?vHa8;sX#v!}?N!rnMWdE+bcN9g|n=lvN9zfK4ST$<2F zxS6uT9cYCS8sJ1FW~&r3Q`bmX;%^)`i6(XD0^`{QOzswLbHoYO9a!rQ?vzl#-HyBS jZAoCbTs(z)1jjyxo%@FT|4ti@K3LvMLsZm5udj0q%O9*WOr-yukZ(W z1`{xn$h$wvc%~qP$WC_VyMO09Gr#}*`~_ecbrVx4X_z+=QD@n}0xCMnCKhqafQ2Ou zRTBnEI_5RhOx(sD4R-~y1v?0&A3B~JJa+=SGmt$2u`Up=JFXKx6^ND>)&ycruO|hP zEytB_M#GNu->YDOOv~%qgEiZClzwcCg`b>&HCmwz!WCu@ZO0YJmp`^P>@Rk0V7vWV zJMKnK@ufXvjqJF_S+jt)se%S%EmuCD zwB%{;=785oetR--eAznzO^(759lXPJ%<&;i@xh4Hv>KCA6hg7VJxi^|Q}CRq>_hBO zh~NVE_>mDg%GR-*$3TvUff@Nl@FP*XWFu4USwvAZyJM{nQ Rm}S@mBGxlST7gOg#lQE)sVM*e delta 439 zcmZWlOG*Pl6s(?K&(AoCzeFcv)G=zJ1|$av<4yu@bvcR%L0pO3oIwX%?DK4x$40NOZo;bK!_%Y~+V?7+shMBRm@@Q#aJ>`62p zl20S1E-Q(8Fo%MGNO+HZc<{3`5m%Z%_HiH(^wRsZb(7v+w@xp5SC@C$Otkwp>i{As zD?K9}0!%|YPt>9p^k!oWF=C)0ptXKT6dC)!aS01V4i>RQMty#wTBDC9(9XxuyUl6$ z8Rh`q1QrQ79ine^N4ZGNYf$VWB-ZmX5hNL#$06_K9afk+WPepERQVdUHh(N*g=Iay zlu^lBim-|`Dnec##)(9=kVr%-}2OhKRI6MW_e zcm@+lY$ES|lyRK_Aw)8nv)4ZRa`s;PoZo+b{sPdCIUTJSQ1L=XK*~WKij+e-!cq?F z&@d3e2u3yOG=`TEG-F)FgpO+%&@iZBNW-v-NgWwvRpbPkJ51NL9M7&++$q~N3ngn! zKr9P{$LxyjjSB=*-HQTBuDWIkMDupVny-}$mh(Y63&iu)qFGur9b4*Wn~Jw#yUdaI zEY}-lblJ2k0*Tbe{HD2Wrb}jJJ-y&Lc4d83W*0m(n4hAjC`y!*s31{RB2%J_L_9EP zeUUzY+jUKx0eHwF^8E|9$FCi9QSX~(HLY*{8$@z%gB@&d67&v%7Q ztLR?wkD_m$wDfE$LJuy{)OM*^OSDohxzP z9K@RC+K#n$UNjl=YBX@z%V_7lY2~F8v7~I1C6=9hmZ-0gz*SOcG0LUBO%8UL z^&6RyJbhv=joh^3KKY5!>j64gQIfb5U96xTDjxD2g?f-@r4ZtpK#w1h^HB$5SAEn) zw8M-&^phjn#UnhXe8N8gZ9_$Gf-gTUm#1>+lU+SKA8o%M1vJH*kI=FQRoRCU{DH>* S$1GEZ5HKd?Wq3{{fd0S!tketu delta 581 zcmZXRO-~b16o#LfX*=!hv=q=DdonxX zo}CGjK!S%KzIDn z8}6$|G??=!>~!`!)pwoUt?G+6JDYF!;-+8g&xs0ng_6a~3-C}o=_~PpU!12YsWwQ$@U@HFJxEGh`t?BX?@0A$`t?0BwEKB0Tq3| zv-Q7m%eAerp{oQ~LW^4MLooP$MkMN@-4Nwv`7IGy5n@gLhA6%kJxh9BMAMY%=Z44@ z^m>y4O|eVgQa)giP%@;6BZ_XzOEONLVOP;`-hgUXoL6>7XzvOE~ zZq*&DCeYZ)Ki3qd=E|VECwEHzkT7vXA~?Yu>(O_c{X4a7nZ%Et>R)o#J>R #include #include +#include #include #include #include @@ -894,6 +895,8 @@ 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_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 89d3d56731c..e462740c1cc 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -19,6 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include @@ -387,6 +388,8 @@ bool goto_analyzer_parse_optionst::process_goto_program( remove_function_pointers(goto_model, cmdline.isset("pointer-check")); // Java virtual functions -> explicit dispatch tables: remove_virtual_functions(goto_model); + // remove Java throw and catch + 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 3cbbac3a55b..209a5daeed1 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include @@ -810,6 +811,8 @@ void goto_instrument_parse_optionst::do_indirect_call_and_rtti_removal( cmdline.isset("pointer-check")); status() << "Virtual function removal" << eom; remove_virtual_functions(symbol_table, goto_functions); + status() << "Catch and throw removal" << eom; + remove_exceptions(symbol_table, goto_functions); status() << "Java instanceof removal" << eom; remove_instanceof(symbol_table, goto_functions); } diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile index d8cb835e4a8..d5cc5ea25eb 100644 --- a/src/goto-programs/Makefile +++ b/src/goto-programs/Makefile @@ -13,8 +13,8 @@ SRC = goto_convert.cpp goto_convert_function_call.cpp \ remove_unused_functions.cpp remove_vector.cpp \ wp.cpp goto_clean_expr.cpp safety_checker.cpp parameter_assignments.cpp \ compute_called_functions.cpp link_to_library.cpp \ - remove_returns.cpp osx_fat_reader.cpp remove_complex.cpp \ - goto_trace.cpp xml_goto_trace.cpp vcd_goto_trace.cpp \ + remove_returns.cpp remove_exceptions.cpp osx_fat_reader.cpp \ + remove_complex.cpp goto_trace.cpp xml_goto_trace.cpp vcd_goto_trace.cpp \ graphml_witness.cpp remove_virtual_functions.cpp \ class_hierarchy.cpp show_goto_functions.cpp get_goto_model.cpp \ slice_global_inits.cpp goto_inline_class.cpp class_identifier.cpp \ diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index a3124f3b898..58cf6666897 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -47,6 +47,85 @@ static bool is_empty(const goto_programt &goto_program) /*******************************************************************\ +Function: finish_catch_push_targets + + Inputs: + + Outputs: + + Purpose: Populate the CATCH instructions with the targets + corresponding to their associated labels + +\*******************************************************************/ + +static void finish_catch_push_targets(goto_programt &dest) +{ + std::map label_targets; + + // in the first pass collect the labels and the corresponding targets + Forall_goto_program_instructions(it, dest) + { + if(!it->labels.empty()) + { + for(auto label : it->labels) + // record the label and the corresponding target + label_targets.insert(std::make_pair(label, it)); + } + } + + // in the second pass set the targets + Forall_goto_program_instructions(it, dest) + { + if(it->is_catch()) + { + bool handler_added=true; + irept exceptions=it->code.find(ID_exception_list); + + 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()) + { + // 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 + for(const auto &handler : handler_list) + { + if(label_targets.find(handler.id())==label_targets.end()) + { + handler_added=false; + break; + } + } + + if(!handler_added) + 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); + } + } + } + } +} + +/******************************************************************* \ + Function: goto_convertt::finish_gotos Inputs: @@ -302,6 +381,7 @@ void goto_convertt::goto_convert_rec( finish_gotos(dest); finish_computed_gotos(dest); finish_guarded_gotos(dest); + finish_catch_push_targets(dest); } /*******************************************************************\ diff --git a/src/goto-programs/goto_convert_class.h b/src/goto-programs/goto_convert_class.h index feab8197046..05c35efa3c0 100644 --- a/src/goto-programs/goto_convert_class.h +++ b/src/goto-programs/goto_convert_class.h @@ -94,6 +94,9 @@ 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, @@ -237,6 +240,7 @@ 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 8d04f3cca16..63f503e8a0b 100644 --- a/src/goto-programs/goto_convert_exceptions.cpp +++ b/src/goto-programs/goto_convert_exceptions.cpp @@ -128,6 +128,73 @@ void goto_convertt::convert_msc_leave( /*******************************************************************\ +Function: goto_convertt::convert_java_try_catch + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +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); +} + +/*******************************************************************\ + Function: goto_convertt::convert_try_catch Inputs: diff --git a/src/goto-programs/goto_convert_side_effect.cpp b/src/goto-programs/goto_convert_side_effect.cpp index f34ee9d03a0..dbebb856ec1 100644 --- a/src/goto-programs/goto_convert_side_effect.cpp +++ b/src/goto-programs/goto_convert_side_effect.cpp @@ -767,6 +767,29 @@ void goto_convertt::remove_statement_expression( /*******************************************************************\ +Function: goto_convertt::remove_push_catch + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +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(); +} + +/*******************************************************************\ + Function: goto_convertt::remove_side_effect Inputs: @@ -837,6 +860,8 @@ 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/remove_exceptions.cpp b/src/goto-programs/remove_exceptions.cpp new file mode 100644 index 00000000000..14700921e24 --- /dev/null +++ b/src/goto-programs/remove_exceptions.cpp @@ -0,0 +1,586 @@ +/*******************************************************************\ + +Module: Remove exception handling + +Author: Cristina David + +Date: December 2016 + +\*******************************************************************/ +#define DEBUG +#ifdef DEBUG +#include +#endif +#include + +#include +#include + +#include "remove_exceptions.h" + +class remove_exceptionst +{ + typedef std::vector> catch_handlerst; + typedef std::vector stack_catcht; + +public: + explicit remove_exceptionst(symbol_tablet &_symbol_table): + symbol_table(_symbol_table) + { + } + + void operator()( + goto_functionst &goto_functions); + +protected: + symbol_tablet &symbol_table; + + void add_exceptional_returns( + const goto_functionst::function_mapt::iterator &); + + void replace_throws( + const goto_functionst::function_mapt::iterator &); + + void instrument_function_calls( + const goto_functionst::function_mapt::iterator &); + + void instrument_exception_handlers( + const goto_functionst::function_mapt::iterator &); + + void add_gotos( + const goto_functionst::function_mapt::iterator &); + + void add_throw_gotos( + const goto_functionst::function_mapt::iterator &, + const goto_programt::instructionst::iterator &, + const stack_catcht &); + + void add_function_call_gotos( + const goto_functionst::function_mapt::iterator &, + const goto_programt::instructionst::iterator &, + const stack_catcht &); +}; + +/*******************************************************************\ + +Function: remove_exceptionst::add_exceptional_returns + +Inputs: + +Outputs: + +Purpose: 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=func_it->first; + goto_programt &goto_program=func_it->second.body; + + assert(symbol_table.has_symbol(function_id)); + const symbolt &function_symbol=symbol_table.lookup(function_id); + + // for now only add exceptional returns for Java + if(function_symbol.mode!=ID_java) + return; + + if(goto_program.empty()) + return; + + // We generate an exceptional return value for any function that has + // a throw or a function call. This can be improved by only considering + // function calls that may escape exceptions. However, this will + // require multiple passes. + bool add_exceptional_var=false; + Forall_goto_program_instructions(instr_it, goto_program) + if(instr_it->is_throw() || instr_it->is_function_call()) + { + add_exceptional_var=true; + break; + } + + if(add_exceptional_var) + { + // look up the function symbol + symbol_tablet::symbolst::iterator s_it= + symbol_table.symbols.find(function_id); + + assert(s_it!=symbol_table.symbols.end()); + + auxiliary_symbolt new_symbol; + new_symbol.is_static_lifetime=true; + new_symbol.module=function_symbol.module; + new_symbol.base_name=id2string(function_symbol.base_name)+EXC_SUFFIX; + new_symbol.name=id2string(function_symbol.name)+EXC_SUFFIX; + new_symbol.mode=function_symbol.mode; + new_symbol.type=typet(ID_pointer, empty_typet()); + symbol_table.add(new_symbol); + + // initialize the exceptional return with NULL + symbol_exprt lhs_expr_null=new_symbol.symbol_expr(); + exprt rhs_expr_null; + rhs_expr_null=null_pointer_exprt(pointer_typet(empty_typet())); + goto_programt::targett t_null= + goto_program.insert_before(goto_program.instructions.begin()); + t_null->make_assignment(); + t_null->source_location= + goto_program.instructions.begin()->source_location; + t_null->code=code_assignt( + lhs_expr_null, + rhs_expr_null); + t_null->function=function_id; + } + return; +} + +/*******************************************************************\ + +Function: remove_exceptionst::replace_throws + +Inputs: + +Outputs: + +Purpose: turns 'throw x' in function f into an assignment to f#exc_value + +\*******************************************************************/ + +void remove_exceptionst::replace_throws( + const goto_functionst::function_mapt::iterator &func_it) +{ + const irep_idt &function_id=func_it->first; + goto_programt &goto_program=func_it->second.body; + + if(goto_program.empty()) + return; + + Forall_goto_program_instructions(instr_it, goto_program) + { + if(instr_it->is_throw() && + symbol_table.has_symbol(id2string(function_id)+EXC_SUFFIX)) + { + assert(instr_it->code.operands().size()==1); + const symbolt &exc_symbol= + symbol_table.lookup(id2string(function_id)+EXC_SUFFIX); + + // replace "throw x;" by "f#exception_value=x;" + symbol_exprt lhs_expr=exc_symbol.symbol_expr(); + // find the symbol corresponding to the thrown exceptions + exprt exc_expr=instr_it->code; + while(exc_expr.id()!=ID_symbol && exc_expr.has_operands()) + exc_expr=exc_expr.op0(); + + // add the assignment with the appropriate cast + code_assignt assignment(typecast_exprt(lhs_expr, exc_expr.type()), + exc_expr); + // now turn the `throw' into `assignment' + instr_it->type=ASSIGN; + instr_it->code=assignment; + } + } +} + +/*******************************************************************\ + +Function: remove_exceptionst::instrument_function_calls + +Inputs: + +Outputs: + +Purpose: after each function call g() in function f + adds f#exception_value=g#exception_value; + +\*******************************************************************/ + +void remove_exceptionst::instrument_function_calls( + const goto_functionst::function_mapt::iterator &func_it) +{ + const irep_idt &caller_id=func_it->first; + goto_programt &goto_program=func_it->second.body; + + if(goto_program.empty()) + return; + + Forall_goto_program_instructions(instr_it, goto_program) + { + if(instr_it->is_function_call()) + { + code_function_callt &function_call=to_code_function_call(instr_it->code); + const irep_idt &callee_id= + to_symbol_expr(function_call.function()).get_identifier(); + + // can exceptions escape? + if(symbol_table.has_symbol(id2string(callee_id)+EXC_SUFFIX) && + symbol_table.has_symbol(id2string(caller_id)+EXC_SUFFIX)) + { + const symbolt &callee= + symbol_table.lookup(id2string(callee_id)+EXC_SUFFIX); + const symbolt &caller= + symbol_table.lookup(id2string(caller_id)+EXC_SUFFIX); + + symbol_exprt rhs_expr=callee.symbol_expr(); + 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, rhs_expr); + t->function=instr_it->function; + } + } + } +} + +/*******************************************************************\ + +Function: remove_exceptionst::instrument_exception_handlers + +Inputs: + +Outputs: + +Purpose: at the beginning of each handler in function f + adds exc=f#exception_value; f#exception_value=NULL; + +\*******************************************************************/ + +void remove_exceptionst::instrument_exception_handlers( + const goto_functionst::function_mapt::iterator &func_it) +{ + const irep_idt &function_id=func_it->first; + goto_programt &goto_program=func_it->second.body; + + if(goto_program.empty()) + return; + + Forall_goto_program_instructions(instr_it, goto_program) + { + // is this a handler + if(instr_it->type==CATCH && instr_it->code.has_operands()) + { + // retrieve the exception variable + const irept &exception=instr_it->code.op0(); + + if(symbol_table.has_symbol(id2string(function_id)+EXC_SUFFIX)) + { + const symbolt &function_symbol= + symbol_table.lookup(id2string(function_id)+EXC_SUFFIX); + // next we reset the exceptional return to NULL + symbol_exprt lhs_expr_null=function_symbol.symbol_expr(); + exprt rhs_expr_null; + rhs_expr_null=null_pointer_exprt(pointer_typet(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); + t_null->function=instr_it->function; + + // add the assignment exc=f#exception_value + symbol_exprt rhs_expr_exc=function_symbol.symbol_expr(); + + const exprt &lhs_expr_exc=static_cast(exception); + 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(lhs_expr_exc, rhs_expr_exc.type()), + rhs_expr_exc); + t_exc->function=instr_it->function; + } + + instr_it->make_skip(); + } + } +} + +/*******************************************************************\ + +Function: remove_exceptionst::add_gotos_throw + +Inputs: + +Outputs: + +Purpose: instruments each throw with conditional GOTOS to the + corresponding exception handlers + +\*******************************************************************/ + +void remove_exceptionst::add_throw_gotos( + const goto_functionst::function_mapt::iterator &func_it, + const goto_programt::instructionst::iterator &instr_it, + const remove_exceptionst::stack_catcht &stack_catch) +{ + assert(instr_it->type==THROW); + + goto_programt &goto_program=func_it->second.body; + + assert(instr_it->code.operands().size()==1); + + // find the end of the function + goto_programt::targett end_function; + for(end_function=instr_it; + !end_function->is_end_function(); + end_function++) {} + if(end_function!=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(end_function); + t_end->source_location=instr_it->source_location; + t_end->function=instr_it->function; + } + + // add GOTOs implementing the dynamic dispatch of the + // exception handlers + 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= + stack_catch[i][j].second; + + // 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); + // find the symbol corresponding to the caught exceptions + exprt exc_symbol=instr_it->code; + while(exc_symbol.id()!=ID_symbol) + exc_symbol=exc_symbol.op0(); + + binary_predicate_exprt check(exc_symbol, ID_java_instanceof, expr); + t_exc->guard=check; + } + } +} + +/*******************************************************************\ + +Function: remove_exceptionst::add_function_call_gotos + +Inputs: + +Outputs: + +Purpose: instruments each function call that may escape exceptions + with conditional GOTOS to the corresponding exception handlers + +\*******************************************************************/ + +void remove_exceptionst::add_function_call_gotos( + const goto_functionst::function_mapt::iterator &func_it, + const goto_programt::instructionst::iterator &instr_it, + const stack_catcht &stack_catch) +{ + assert(instr_it->type==FUNCTION_CALL); + + goto_programt &goto_program=func_it->second.body; + + // save the address of the next instruction + goto_programt::instructionst::iterator next_it=instr_it; + next_it++; + + code_function_callt &function_call=to_code_function_call(instr_it->code); + assert(function_call.function().id()==ID_symbol); + const irep_idt &callee_id= + to_symbol_expr(function_call.function()).get_identifier(); + + if(symbol_table.has_symbol(id2string(callee_id)+EXC_SUFFIX)) + { + // dynamic dispatch of the escaped exception + const symbolt &callee_exc_symbol= + symbol_table.lookup(id2string(callee_id)+EXC_SUFFIX); + symbol_exprt callee_exc=callee_exc_symbol.symbol_expr(); + + 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; + } + } + + // add a null check (so that instanceof can be applied) + equal_exprt eq_null( + callee_exc, + null_pointer_exprt(pointer_typet(empty_typet()))); + // jump to the next instruction + goto_programt::targett t_null=goto_program.insert_after(instr_it); + t_null->make_goto(next_it); + t_null->source_location=instr_it->source_location; + t_null->function=instr_it->function; + t_null->guard=eq_null; + } +} + +/*******************************************************************\ + +Function: remove_exceptionst::add_gotos + +Inputs: + +Outputs: + +Purpose: instruments each throw and function calls that may escape exceptions + with conditional GOTOS to the corresponding exception handlers + +\*******************************************************************/ + +void remove_exceptionst::add_gotos( + const goto_functionst::function_mapt::iterator &func_it) +{ + // Stack of try-catch blocks + stack_catcht stack_catch; + + goto_programt &goto_program=func_it->second.body; + + if(goto_program.empty()) + return; + Forall_goto_program_instructions(instr_it, goto_program) + { + // it's a CATCH but not a handler + if(instr_it->type==CATCH && !instr_it->code.has_operands()) + { + if(instr_it->targets.empty()) // pop + { + // pop from the stack if possible + if(!stack_catch.empty()) + { + stack_catch.pop_back(); + } + else + { +#ifdef DEBUG + std::cout << "Remove exceptions: empty stack" << std::endl; +#endif + } + } + else // push + { + remove_exceptionst::catch_handlerst exception; + stack_catch.push_back(exception); + remove_exceptionst::catch_handlerst &last_exception= + stack_catch.back(); + + // copy targets + const irept::subt &exception_list= + instr_it->code.find(ID_exception_list).get_sub(); + assert(exception_list.size()==instr_it->targets.size()); + + // Fill the map with the catch type and the target + unsigned i=0; + for(auto target : instr_it->targets) + { + last_exception.push_back( + std::make_pair(exception_list[i].id(), target)); + i++; + } + } + + instr_it->make_skip(); + } + else if(instr_it->type==THROW) + { + add_throw_gotos(func_it, instr_it, stack_catch); + } + else if(instr_it->type==FUNCTION_CALL) + { + add_function_call_gotos(func_it, instr_it, stack_catch); + } + } +} + + +/*******************************************************************\ + +Function: remove_exceptionst::operator() + +Inputs: + +Outputs: + +Purpose: + +\*******************************************************************/ + +void remove_exceptionst::operator()(goto_functionst &goto_functions) +{ + Forall_goto_functions(it, goto_functions) + { + add_exceptional_returns(it); + } + Forall_goto_functions(it, goto_functions) + { + instrument_exception_handlers(it); + add_gotos(it); + instrument_function_calls(it); + replace_throws(it); + } +} + +/*******************************************************************\ + +Function: remove_exceptions + +Inputs: + +Outputs: + +Purpose: removes throws/CATCH-POP/CATCH-PUSH + +\*******************************************************************/ + +void remove_exceptions( + symbol_tablet &symbol_table, + goto_functionst &goto_functions) +{ + remove_exceptionst remove_exceptions(symbol_table); + remove_exceptions(goto_functions); +} + +/*******************************************************************\ + +Function: remove_exceptions + +Inputs: + +Outputs: + +Purpose: removes throws/CATCH-POP/CATCH-PUSH + +\*******************************************************************/ + +void remove_exceptions(goto_modelt &goto_model) +{ + remove_exceptionst remove_exceptions(goto_model.symbol_table); + remove_exceptions(goto_model.goto_functions); +} diff --git a/src/goto-programs/remove_exceptions.h b/src/goto-programs/remove_exceptions.h new file mode 100644 index 00000000000..89162b5833d --- /dev/null +++ b/src/goto-programs/remove_exceptions.h @@ -0,0 +1,24 @@ +/*******************************************************************\ + +Module: Remove function exceptional returns + +Author: Cristina David + +Date: December 2016 + +\*******************************************************************/ + +#ifndef CPROVER_GOTO_PROGRAMS_REMOVE_EXCEPTIONS_H +#define CPROVER_GOTO_PROGRAMS_REMOVE_EXCEPTIONS_H + +#include + +#define EXC_SUFFIX "#exception_value" + +// 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 &); + +#endif diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index 69d4dffd04f..19174326c6c 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -108,9 +108,21 @@ exprt::operandst java_bytecode_convert_methodt::pop(std::size_t n) return operands; } +/*******************************************************************\ + +Function: java_bytecode_convert_methodt::pop_residue + +Inputs: + +Outputs: + +Purpose: removes minimum(n, stack.size()) elements from the stack + +\*******************************************************************/ + void java_bytecode_convert_methodt::pop_residue(std::size_t n) { - std::size_t residue_size=n<=stack.size()?n:stack.size(); + std::size_t residue_size=std::min(n, stack.size()); stack.resize(stack.size()-residue_size); } @@ -804,8 +816,10 @@ static void gather_symbol_live_ranges( } } else + { forall_operands(it, e) gather_symbol_live_ranges(pc, *it, result); + } } /*******************************************************************\ @@ -874,18 +888,20 @@ codet java_bytecode_convert_methodt::convert_instructions( if(i_it->statement=="athrow" || i_it->statement=="invokestatic" || - i_it->statement=="invokevirtual") + i_it->statement=="invokevirtual" || + i_it->statement=="invokespecial" || + i_it->statement=="invokeinterface") { // find the corresponding try-catch blocks and add the handlers // to the targets - for(std::size_t e=0; eaddress>=method.exception_table[e].start_pc && - i_it->addressaddress>=exception_row.start_pc && + i_it->addresssecond.successors.push_back( - method.exception_table[e].handler_pc); - targets.insert(method.exception_table[e].handler_pc); + exception_row.handler_pc); + targets.insert(exception_row.handler_pc); } } } @@ -1023,7 +1039,7 @@ codet java_bytecode_convert_methodt::convert_instructions( exprt exc_var=variable( arg0, statement[0], i_it->address, - false); + NO_CAST); // throw away the operands pop_residue(bytecode_info.pop); @@ -1032,17 +1048,19 @@ codet java_bytecode_convert_methodt::convert_instructions( side_effect_expr_catcht catch_handler_expr; // pack the exception variable so that it can be used // later for instrumentation - catch_handler_expr.set(ID_handler, exc_var); + catch_handler_expr.get_sub().resize(1); + catch_handler_expr.get_sub()[0]=exc_var; + codet catch_handler=code_expressiont(catch_handler_expr); + code_labelt newlabel(label(std::to_string(cur_pc)), + code_blockt()); - code_labelt newlabel(label(i2string(cur_pc)), code_blockt()); code_blockt label_block=to_code_block(newlabel.code()); code_blockt handler_block; handler_block.move_to_operands(c); handler_block.move_to_operands(catch_handler); handler_block.move_to_operands(label_block); c=handler_block; - break; } } @@ -1065,11 +1083,30 @@ codet java_bytecode_convert_methodt::convert_instructions( else if(statement=="athrow") { assert(op.size()==1 && results.size()==1); + code_blockt block; + if(!disable_runtime_checks) + { + // TODO throw NullPointerException instead + const typecast_exprt lhs(op[0], pointer_typet(empty_typet())); + const exprt rhs(null_pointer_exprt(to_pointer_type(lhs.type()))); + const exprt not_equal_null( + binary_relation_exprt(lhs, ID_notequal, rhs)); + code_assertt check(not_equal_null); + check.add_source_location() + .set_comment("Throw null"); + check.add_source_location() + .set_property_class("null-pointer-exception"); + block.move_to_operands(check); + } + side_effect_expr_throwt throw_expr; throw_expr.add_source_location()=i_it->source_location; throw_expr.copy_to_operands(op[0]); c=code_expressiont(throw_expr); results[0]=op[0]; + + block.move_to_operands(c); + c=block; } else if(statement=="checkcast") { @@ -1115,7 +1152,7 @@ codet java_bytecode_convert_methodt::convert_instructions( statement=="invokevirtual" || statement=="invokestatic") { - const bool use_this(statement != "invokestatic"); + const bool use_this(statement!="invokestatic"); const bool is_virtual( statement=="invokevirtual" || statement=="invokeinterface"); @@ -2046,17 +2083,19 @@ codet java_bytecode_convert_methodt::convert_instructions( // add the CATCH-PUSH instruction(s) // be aware of different try-catch blocks with the same starting pc std::size_t pos=0; - int end_pc=-1; + size_t end_pc=0; while(possource_location.get_line().empty()) c.add_source_location()=i_it->source_location; @@ -2178,6 +2194,18 @@ codet java_bytecode_convert_methodt::convert_instructions( address_mapt::iterator a_it2=address_map.find(address); assert(a_it2!=address_map.end()); + // we don't worry about exception handlers as we don't load the + // operands from the stack anyway -- we keep explicit global + // exception variables + for(const auto &exception_row : method.exception_table) + { + if(address==exception_row.handler_pc) + { + stack.clear(); + break; + } + } + if(!stack.empty() && a_it2->second.predecessors.size()>1) { // copy into temporaries @@ -2242,8 +2270,6 @@ codet java_bytecode_convert_methodt::convert_instructions( } } - // TODO: add exception handlers from exception table - // review successor computation of athrow! code_blockt code; // Add anonymous locals to the symtab: diff --git a/src/symex/symex_parse_options.cpp b/src/symex/symex_parse_options.cpp index 2ed3fedc518..54aa9382759 100644 --- a/src/symex/symex_parse_options.cpp +++ b/src/symex/symex_parse_options.cpp @@ -32,6 +32,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include @@ -369,6 +370,9 @@ bool symex_parse_optionst::process_goto_program(const optionst &options) remove_vector(goto_model); // Java virtual functions -> explicit dispatch tables: remove_virtual_functions(goto_model); + // Java throw and catch -> explicit exceptional return variables: + remove_exceptions(goto_model); + // Java instanceof -> clsid comparison: remove_instanceof(goto_model); rewrite_union(goto_model); adjust_float_expressions(goto_model); diff --git a/src/util/irep_ids.txt b/src/util/irep_ids.txt index 666556d4b78..066a5f831cc 100644 --- a/src/util/irep_ids.txt +++ b/src/util/irep_ids.txt @@ -739,7 +739,6 @@ java_instanceof java_super_method_call java_enum_static_unwind push_catch -handler string_constraint string_not_contains_constraint cprover_char_literal_func diff --git a/src/util/std_code.h b/src/util/std_code.h index ed1f8f28b74..eb7982f3bbd 100644 --- a/src/util/std_code.h +++ b/src/util/std_code.h @@ -1130,7 +1130,6 @@ class side_effect_expr_catcht:public side_effect_exprt inline side_effect_expr_catcht():side_effect_exprt(ID_push_catch) { } - // TODO: change to ID_catch inline explicit side_effect_expr_catcht(const irept &exception_list): side_effect_exprt(ID_push_catch) { From eb89cc51eb189a539f6b1e6d1e481d48c32341cf Mon Sep 17 00:00:00 2001 From: Cristina Date: Wed, 15 Feb 2017 14:20:28 +0000 Subject: [PATCH 06/14] Moved Java exceptions regression tests These tests are now under cbmc-java. --- .../cbmc-java/NullPointer3/NullPointer3.class | Bin 270 -> 380 bytes .../cbmc-java/NullPointer3/NullPointer3.java | 1 - regression/cbmc-java/NullPointer3/test.desc | 4 ++-- .../exceptions1/A.class | Bin .../exceptions1/B.class | Bin .../exceptions1/C.class | Bin .../exceptions1/D.class | Bin .../exceptions1/test.class | Bin .../exceptions1/test.desc | 2 +- .../exceptions1/test.java | 0 .../exceptions10/A.class | Bin .../exceptions10/B.class | Bin .../exceptions10/C.class | Bin .../exceptions10/test.class | Bin .../exceptions10/test.desc | 0 .../exceptions10/test.java | 0 .../exceptions11/A.class | Bin .../exceptions11/B.class | Bin .../exceptions11/test.class | Bin .../exceptions11/test.desc | 0 .../exceptions11/test.java | 0 .../exceptions12/A.class | Bin .../exceptions12/B.class | Bin .../exceptions12/C.class | Bin .../exceptions12/F.class | Bin .../exceptions12/test.class | Bin .../exceptions12/test.desc | 0 .../exceptions12/test.java | 0 .../exceptions13/A.class | Bin .../exceptions13/B.class | Bin .../exceptions13/C.class | Bin .../exceptions13/F.class | Bin .../exceptions13/test.class | Bin .../exceptions13/test.desc | 0 .../exceptions13/test.java | 0 .../exceptions14/A.class | Bin .../exceptions14/B.class | Bin .../exceptions14/C.class | Bin .../exceptions14/test.class | Bin .../exceptions14/test.desc | 0 .../exceptions14/test.java | 0 .../exceptions15/InetAddress.class | Bin .../exceptions15/InetSocketAddress.class | Bin .../exceptions15/test.class | Bin .../exceptions15/test.desc | 0 .../exceptions15/test.java | 0 .../exceptions16}/A.class | Bin .../exceptions16}/B.class | Bin .../exceptions16}/C.class | Bin regression/cbmc-java/exceptions16/test.class | Bin 0 -> 718 bytes regression/cbmc-java/exceptions16/test.desc | 9 ++++++++ regression/cbmc-java/exceptions16/test.java | 21 ++++++++++++++++++ .../exceptions2/A.class | Bin .../exceptions2}/B.class | Bin .../exceptions2}/C.class | Bin .../exceptions2/test.class | Bin .../exceptions2/test.desc | 2 +- .../exceptions2/test.java | 0 .../exceptions3/A.class | Bin .../exceptions3}/B.class | Bin .../exceptions3}/C.class | Bin .../exceptions3/test.class | Bin .../exceptions3/test.desc | 0 .../exceptions3/test.java | 0 .../exceptions4/A.class | Bin .../exceptions4}/B.class | Bin .../exceptions4}/C.class | Bin .../exceptions4/test.class | Bin .../exceptions4/test.desc | 0 .../exceptions4/test.java | 0 .../exceptions5/A.class | Bin .../exceptions5}/B.class | Bin .../exceptions5}/C.class | Bin .../exceptions5/D.class | Bin .../exceptions5/test.class | Bin .../exceptions5/test.desc | 0 .../exceptions5/test.java | 0 .../exceptions6/A.class | Bin .../exceptions6/B.class | Bin .../exceptions6/C.class | Bin .../exceptions6/D.class | Bin .../exceptions6/test.class | Bin .../exceptions6/test.desc | 0 .../exceptions6/test.java | 0 .../exceptions7}/A.class | Bin .../exceptions7}/B.class | Bin .../exceptions7}/C.class | Bin .../exceptions7/test.class | Bin .../exceptions7/test.desc | 0 .../exceptions7/test.java | 0 regression/cbmc-java/exceptions8/A.class | Bin 0 -> 241 bytes regression/cbmc-java/exceptions8/B.class | Bin 0 -> 216 bytes .../exceptions8}/C.class | Bin .../exceptions8/test.class | Bin .../exceptions8/test.desc | 0 .../exceptions8/test.java | 0 .../exceptions9/A.class | Bin .../exceptions9/B.class | Bin regression/cbmc-java/exceptions9/C.class | Bin 0 -> 216 bytes .../exceptions9/test.class | Bin .../exceptions9/test.desc | 0 .../exceptions9/test.java | 0 regression/exceptions/Makefile | 14 ------------ 103 files changed, 34 insertions(+), 19 deletions(-) rename regression/{exceptions => cbmc-java}/exceptions1/A.class (100%) rename regression/{exceptions => cbmc-java}/exceptions1/B.class (100%) rename regression/{exceptions => cbmc-java}/exceptions1/C.class (100%) rename regression/{exceptions => cbmc-java}/exceptions1/D.class (100%) rename regression/{exceptions => cbmc-java}/exceptions1/test.class (100%) rename regression/{exceptions => cbmc-java}/exceptions1/test.desc (80%) rename regression/{exceptions => cbmc-java}/exceptions1/test.java (100%) rename regression/{exceptions => cbmc-java}/exceptions10/A.class (100%) rename regression/{exceptions => cbmc-java}/exceptions10/B.class (100%) rename regression/{exceptions => cbmc-java}/exceptions10/C.class (100%) rename regression/{exceptions => cbmc-java}/exceptions10/test.class (100%) rename regression/{exceptions => cbmc-java}/exceptions10/test.desc (100%) rename regression/{exceptions => cbmc-java}/exceptions10/test.java (100%) rename regression/{exceptions => cbmc-java}/exceptions11/A.class (100%) rename regression/{exceptions => cbmc-java}/exceptions11/B.class (100%) rename regression/{exceptions => cbmc-java}/exceptions11/test.class (100%) rename regression/{exceptions => cbmc-java}/exceptions11/test.desc (100%) rename regression/{exceptions => cbmc-java}/exceptions11/test.java (100%) rename regression/{exceptions => cbmc-java}/exceptions12/A.class (100%) rename regression/{exceptions => cbmc-java}/exceptions12/B.class (100%) rename regression/{exceptions => cbmc-java}/exceptions12/C.class (100%) rename regression/{exceptions => cbmc-java}/exceptions12/F.class (100%) rename regression/{exceptions => cbmc-java}/exceptions12/test.class (100%) rename regression/{exceptions => cbmc-java}/exceptions12/test.desc (100%) rename regression/{exceptions => cbmc-java}/exceptions12/test.java (100%) rename regression/{exceptions => cbmc-java}/exceptions13/A.class (100%) rename regression/{exceptions => cbmc-java}/exceptions13/B.class (100%) rename regression/{exceptions => cbmc-java}/exceptions13/C.class (100%) rename regression/{exceptions => cbmc-java}/exceptions13/F.class (100%) rename regression/{exceptions => cbmc-java}/exceptions13/test.class (100%) rename regression/{exceptions => cbmc-java}/exceptions13/test.desc (100%) rename regression/{exceptions => cbmc-java}/exceptions13/test.java (100%) rename regression/{exceptions => cbmc-java}/exceptions14/A.class (100%) rename regression/{exceptions => cbmc-java}/exceptions14/B.class (100%) rename regression/{exceptions => cbmc-java}/exceptions14/C.class (100%) rename regression/{exceptions => cbmc-java}/exceptions14/test.class (100%) rename regression/{exceptions => cbmc-java}/exceptions14/test.desc (100%) rename regression/{exceptions => cbmc-java}/exceptions14/test.java (100%) rename regression/{exceptions => cbmc-java}/exceptions15/InetAddress.class (100%) rename regression/{exceptions => cbmc-java}/exceptions15/InetSocketAddress.class (100%) rename regression/{exceptions => cbmc-java}/exceptions15/test.class (100%) rename regression/{exceptions => cbmc-java}/exceptions15/test.desc (100%) rename regression/{exceptions => cbmc-java}/exceptions15/test.java (100%) rename regression/{exceptions/exceptions7 => cbmc-java/exceptions16}/A.class (100%) rename regression/{exceptions/exceptions2 => cbmc-java/exceptions16}/B.class (100%) rename regression/{exceptions/exceptions2 => cbmc-java/exceptions16}/C.class (100%) create mode 100644 regression/cbmc-java/exceptions16/test.class create mode 100644 regression/cbmc-java/exceptions16/test.desc create mode 100644 regression/cbmc-java/exceptions16/test.java rename regression/{exceptions => cbmc-java}/exceptions2/A.class (100%) rename regression/{exceptions/exceptions3 => cbmc-java/exceptions2}/B.class (100%) rename regression/{exceptions/exceptions3 => cbmc-java/exceptions2}/C.class (100%) rename regression/{exceptions => cbmc-java}/exceptions2/test.class (100%) rename regression/{exceptions => cbmc-java}/exceptions2/test.desc (79%) rename regression/{exceptions => cbmc-java}/exceptions2/test.java (100%) rename regression/{exceptions => cbmc-java}/exceptions3/A.class (100%) rename regression/{exceptions/exceptions4 => cbmc-java/exceptions3}/B.class (100%) rename regression/{exceptions/exceptions4 => cbmc-java/exceptions3}/C.class (100%) rename regression/{exceptions => cbmc-java}/exceptions3/test.class (100%) rename regression/{exceptions => cbmc-java}/exceptions3/test.desc (100%) rename regression/{exceptions => cbmc-java}/exceptions3/test.java (100%) rename regression/{exceptions => cbmc-java}/exceptions4/A.class (100%) rename regression/{exceptions/exceptions5 => cbmc-java/exceptions4}/B.class (100%) rename regression/{exceptions/exceptions5 => cbmc-java/exceptions4}/C.class (100%) rename regression/{exceptions => cbmc-java}/exceptions4/test.class (100%) rename regression/{exceptions => cbmc-java}/exceptions4/test.desc (100%) rename regression/{exceptions => cbmc-java}/exceptions4/test.java (100%) rename regression/{exceptions => cbmc-java}/exceptions5/A.class (100%) rename regression/{exceptions/exceptions7 => cbmc-java/exceptions5}/B.class (100%) rename regression/{exceptions/exceptions7 => cbmc-java/exceptions5}/C.class (100%) rename regression/{exceptions => cbmc-java}/exceptions5/D.class (100%) rename regression/{exceptions => cbmc-java}/exceptions5/test.class (100%) rename regression/{exceptions => cbmc-java}/exceptions5/test.desc (100%) rename regression/{exceptions => cbmc-java}/exceptions5/test.java (100%) rename regression/{exceptions => cbmc-java}/exceptions6/A.class (100%) rename regression/{exceptions => cbmc-java}/exceptions6/B.class (100%) rename regression/{exceptions => cbmc-java}/exceptions6/C.class (100%) rename regression/{exceptions => cbmc-java}/exceptions6/D.class (100%) rename regression/{exceptions => cbmc-java}/exceptions6/test.class (100%) rename regression/{exceptions => cbmc-java}/exceptions6/test.desc (100%) rename regression/{exceptions => cbmc-java}/exceptions6/test.java (100%) rename regression/{exceptions/exceptions8 => cbmc-java/exceptions7}/A.class (100%) rename regression/{exceptions/exceptions8 => cbmc-java/exceptions7}/B.class (100%) rename regression/{exceptions/exceptions8 => cbmc-java/exceptions7}/C.class (100%) rename regression/{exceptions => cbmc-java}/exceptions7/test.class (100%) rename regression/{exceptions => cbmc-java}/exceptions7/test.desc (100%) rename regression/{exceptions => cbmc-java}/exceptions7/test.java (100%) create mode 100644 regression/cbmc-java/exceptions8/A.class create mode 100644 regression/cbmc-java/exceptions8/B.class rename regression/{exceptions/exceptions9 => cbmc-java/exceptions8}/C.class (100%) rename regression/{exceptions => cbmc-java}/exceptions8/test.class (100%) rename regression/{exceptions => cbmc-java}/exceptions8/test.desc (100%) rename regression/{exceptions => cbmc-java}/exceptions8/test.java (100%) rename regression/{exceptions => cbmc-java}/exceptions9/A.class (100%) rename regression/{exceptions => cbmc-java}/exceptions9/B.class (100%) create mode 100644 regression/cbmc-java/exceptions9/C.class rename regression/{exceptions => cbmc-java}/exceptions9/test.class (100%) rename regression/{exceptions => cbmc-java}/exceptions9/test.desc (100%) rename regression/{exceptions => cbmc-java}/exceptions9/test.java (100%) delete mode 100644 regression/exceptions/Makefile diff --git a/regression/cbmc-java/NullPointer3/NullPointer3.class b/regression/cbmc-java/NullPointer3/NullPointer3.class index 8ad089310c3a7896b660934861b104537c1edd65..b79f5adef44f30757862ddef9c91c22f2700cf2a 100644 GIT binary patch delta 224 zcmeBU`oko8>ff$?3=9k=3?f_%%nX9;3_|P-!V^Wcw1s@~lM{2o5{ohulX6l+Km;QL zOG!p%F(U(?k6&p{PC$NUUP)?^vGqh-C25w#qI95)aI{ZWVp*boPGVlVesD=qW?s7W z#Ms0VeFjD#WME*`+RnhZ5y)U-Uff$?3=9k=4E$US%nUs247}_Nd=o{rCgvziTp1rA%fJYP3=FJV+Zh-) r0vU`9>_CzYEXc^f$-n``j6gmEgA|YkDP>~ZkEV_lD9#0vVc-S;HuwxN diff --git a/regression/cbmc-java/NullPointer3/NullPointer3.java b/regression/cbmc-java/NullPointer3/NullPointer3.java index 00004f14467..fa8b227dd94 100644 --- a/regression/cbmc-java/NullPointer3/NullPointer3.java +++ b/regression/cbmc-java/NullPointer3/NullPointer3.java @@ -4,5 +4,4 @@ public static void main(String[] args) { throw null; // NULL pointer dereference } - } diff --git a/regression/cbmc-java/NullPointer3/test.desc b/regression/cbmc-java/NullPointer3/test.desc index cc33c21738b..5dd14d8dfb9 100644 --- a/regression/cbmc-java/NullPointer3/test.desc +++ b/regression/cbmc-java/NullPointer3/test.desc @@ -1,9 +1,9 @@ CORE NullPointer3.class ---pointer-check --stop-on-fail +--pointer-check ^EXIT=10$ ^SIGNAL=0$ -^ file NullPointer3.java line 5 function java::NullPointer3.main:\(\[Ljava/lang/String;\)V bytecode_index 1$ +^.*Throw null: FAILURE$ ^VERIFICATION FAILED$ -- ^warning: ignoring diff --git a/regression/exceptions/exceptions1/A.class b/regression/cbmc-java/exceptions1/A.class similarity index 100% rename from regression/exceptions/exceptions1/A.class rename to regression/cbmc-java/exceptions1/A.class diff --git a/regression/exceptions/exceptions1/B.class b/regression/cbmc-java/exceptions1/B.class similarity index 100% rename from regression/exceptions/exceptions1/B.class rename to regression/cbmc-java/exceptions1/B.class diff --git a/regression/exceptions/exceptions1/C.class b/regression/cbmc-java/exceptions1/C.class similarity index 100% rename from regression/exceptions/exceptions1/C.class rename to regression/cbmc-java/exceptions1/C.class diff --git a/regression/exceptions/exceptions1/D.class b/regression/cbmc-java/exceptions1/D.class similarity index 100% rename from regression/exceptions/exceptions1/D.class rename to regression/cbmc-java/exceptions1/D.class diff --git a/regression/exceptions/exceptions1/test.class b/regression/cbmc-java/exceptions1/test.class similarity index 100% rename from regression/exceptions/exceptions1/test.class rename to regression/cbmc-java/exceptions1/test.class diff --git a/regression/exceptions/exceptions1/test.desc b/regression/cbmc-java/exceptions1/test.desc similarity index 80% rename from regression/exceptions/exceptions1/test.desc rename to regression/cbmc-java/exceptions1/test.desc index 7c6146907d0..ca52107829c 100644 --- a/regression/exceptions/exceptions1/test.desc +++ b/regression/cbmc-java/exceptions1/test.desc @@ -4,7 +4,7 @@ test.class ^EXIT=10$ ^SIGNAL=0$ ^.*assertion at file test.java line 26 function.*: FAILURE$ -\*\* 1 of 4 failed (2 iterations)$ +\*\* 1 of 9 failed (2 iterations)$ ^VERIFICATION FAILED$ -- ^warning: ignoring diff --git a/regression/exceptions/exceptions1/test.java b/regression/cbmc-java/exceptions1/test.java similarity index 100% rename from regression/exceptions/exceptions1/test.java rename to regression/cbmc-java/exceptions1/test.java diff --git a/regression/exceptions/exceptions10/A.class b/regression/cbmc-java/exceptions10/A.class similarity index 100% rename from regression/exceptions/exceptions10/A.class rename to regression/cbmc-java/exceptions10/A.class diff --git a/regression/exceptions/exceptions10/B.class b/regression/cbmc-java/exceptions10/B.class similarity index 100% rename from regression/exceptions/exceptions10/B.class rename to regression/cbmc-java/exceptions10/B.class diff --git a/regression/exceptions/exceptions10/C.class b/regression/cbmc-java/exceptions10/C.class similarity index 100% rename from regression/exceptions/exceptions10/C.class rename to regression/cbmc-java/exceptions10/C.class diff --git a/regression/exceptions/exceptions10/test.class b/regression/cbmc-java/exceptions10/test.class similarity index 100% rename from regression/exceptions/exceptions10/test.class rename to regression/cbmc-java/exceptions10/test.class diff --git a/regression/exceptions/exceptions10/test.desc b/regression/cbmc-java/exceptions10/test.desc similarity index 100% rename from regression/exceptions/exceptions10/test.desc rename to regression/cbmc-java/exceptions10/test.desc diff --git a/regression/exceptions/exceptions10/test.java b/regression/cbmc-java/exceptions10/test.java similarity index 100% rename from regression/exceptions/exceptions10/test.java rename to regression/cbmc-java/exceptions10/test.java diff --git a/regression/exceptions/exceptions11/A.class b/regression/cbmc-java/exceptions11/A.class similarity index 100% rename from regression/exceptions/exceptions11/A.class rename to regression/cbmc-java/exceptions11/A.class diff --git a/regression/exceptions/exceptions11/B.class b/regression/cbmc-java/exceptions11/B.class similarity index 100% rename from regression/exceptions/exceptions11/B.class rename to regression/cbmc-java/exceptions11/B.class diff --git a/regression/exceptions/exceptions11/test.class b/regression/cbmc-java/exceptions11/test.class similarity index 100% rename from regression/exceptions/exceptions11/test.class rename to regression/cbmc-java/exceptions11/test.class diff --git a/regression/exceptions/exceptions11/test.desc b/regression/cbmc-java/exceptions11/test.desc similarity index 100% rename from regression/exceptions/exceptions11/test.desc rename to regression/cbmc-java/exceptions11/test.desc diff --git a/regression/exceptions/exceptions11/test.java b/regression/cbmc-java/exceptions11/test.java similarity index 100% rename from regression/exceptions/exceptions11/test.java rename to regression/cbmc-java/exceptions11/test.java diff --git a/regression/exceptions/exceptions12/A.class b/regression/cbmc-java/exceptions12/A.class similarity index 100% rename from regression/exceptions/exceptions12/A.class rename to regression/cbmc-java/exceptions12/A.class diff --git a/regression/exceptions/exceptions12/B.class b/regression/cbmc-java/exceptions12/B.class similarity index 100% rename from regression/exceptions/exceptions12/B.class rename to regression/cbmc-java/exceptions12/B.class diff --git a/regression/exceptions/exceptions12/C.class b/regression/cbmc-java/exceptions12/C.class similarity index 100% rename from regression/exceptions/exceptions12/C.class rename to regression/cbmc-java/exceptions12/C.class diff --git a/regression/exceptions/exceptions12/F.class b/regression/cbmc-java/exceptions12/F.class similarity index 100% rename from regression/exceptions/exceptions12/F.class rename to regression/cbmc-java/exceptions12/F.class diff --git a/regression/exceptions/exceptions12/test.class b/regression/cbmc-java/exceptions12/test.class similarity index 100% rename from regression/exceptions/exceptions12/test.class rename to regression/cbmc-java/exceptions12/test.class diff --git a/regression/exceptions/exceptions12/test.desc b/regression/cbmc-java/exceptions12/test.desc similarity index 100% rename from regression/exceptions/exceptions12/test.desc rename to regression/cbmc-java/exceptions12/test.desc diff --git a/regression/exceptions/exceptions12/test.java b/regression/cbmc-java/exceptions12/test.java similarity index 100% rename from regression/exceptions/exceptions12/test.java rename to regression/cbmc-java/exceptions12/test.java diff --git a/regression/exceptions/exceptions13/A.class b/regression/cbmc-java/exceptions13/A.class similarity index 100% rename from regression/exceptions/exceptions13/A.class rename to regression/cbmc-java/exceptions13/A.class diff --git a/regression/exceptions/exceptions13/B.class b/regression/cbmc-java/exceptions13/B.class similarity index 100% rename from regression/exceptions/exceptions13/B.class rename to regression/cbmc-java/exceptions13/B.class diff --git a/regression/exceptions/exceptions13/C.class b/regression/cbmc-java/exceptions13/C.class similarity index 100% rename from regression/exceptions/exceptions13/C.class rename to regression/cbmc-java/exceptions13/C.class diff --git a/regression/exceptions/exceptions13/F.class b/regression/cbmc-java/exceptions13/F.class similarity index 100% rename from regression/exceptions/exceptions13/F.class rename to regression/cbmc-java/exceptions13/F.class diff --git a/regression/exceptions/exceptions13/test.class b/regression/cbmc-java/exceptions13/test.class similarity index 100% rename from regression/exceptions/exceptions13/test.class rename to regression/cbmc-java/exceptions13/test.class diff --git a/regression/exceptions/exceptions13/test.desc b/regression/cbmc-java/exceptions13/test.desc similarity index 100% rename from regression/exceptions/exceptions13/test.desc rename to regression/cbmc-java/exceptions13/test.desc diff --git a/regression/exceptions/exceptions13/test.java b/regression/cbmc-java/exceptions13/test.java similarity index 100% rename from regression/exceptions/exceptions13/test.java rename to regression/cbmc-java/exceptions13/test.java diff --git a/regression/exceptions/exceptions14/A.class b/regression/cbmc-java/exceptions14/A.class similarity index 100% rename from regression/exceptions/exceptions14/A.class rename to regression/cbmc-java/exceptions14/A.class diff --git a/regression/exceptions/exceptions14/B.class b/regression/cbmc-java/exceptions14/B.class similarity index 100% rename from regression/exceptions/exceptions14/B.class rename to regression/cbmc-java/exceptions14/B.class diff --git a/regression/exceptions/exceptions14/C.class b/regression/cbmc-java/exceptions14/C.class similarity index 100% rename from regression/exceptions/exceptions14/C.class rename to regression/cbmc-java/exceptions14/C.class diff --git a/regression/exceptions/exceptions14/test.class b/regression/cbmc-java/exceptions14/test.class similarity index 100% rename from regression/exceptions/exceptions14/test.class rename to regression/cbmc-java/exceptions14/test.class diff --git a/regression/exceptions/exceptions14/test.desc b/regression/cbmc-java/exceptions14/test.desc similarity index 100% rename from regression/exceptions/exceptions14/test.desc rename to regression/cbmc-java/exceptions14/test.desc diff --git a/regression/exceptions/exceptions14/test.java b/regression/cbmc-java/exceptions14/test.java similarity index 100% rename from regression/exceptions/exceptions14/test.java rename to regression/cbmc-java/exceptions14/test.java diff --git a/regression/exceptions/exceptions15/InetAddress.class b/regression/cbmc-java/exceptions15/InetAddress.class similarity index 100% rename from regression/exceptions/exceptions15/InetAddress.class rename to regression/cbmc-java/exceptions15/InetAddress.class diff --git a/regression/exceptions/exceptions15/InetSocketAddress.class b/regression/cbmc-java/exceptions15/InetSocketAddress.class similarity index 100% rename from regression/exceptions/exceptions15/InetSocketAddress.class rename to regression/cbmc-java/exceptions15/InetSocketAddress.class diff --git a/regression/exceptions/exceptions15/test.class b/regression/cbmc-java/exceptions15/test.class similarity index 100% rename from regression/exceptions/exceptions15/test.class rename to regression/cbmc-java/exceptions15/test.class diff --git a/regression/exceptions/exceptions15/test.desc b/regression/cbmc-java/exceptions15/test.desc similarity index 100% rename from regression/exceptions/exceptions15/test.desc rename to regression/cbmc-java/exceptions15/test.desc diff --git a/regression/exceptions/exceptions15/test.java b/regression/cbmc-java/exceptions15/test.java similarity index 100% rename from regression/exceptions/exceptions15/test.java rename to regression/cbmc-java/exceptions15/test.java diff --git a/regression/exceptions/exceptions7/A.class b/regression/cbmc-java/exceptions16/A.class similarity index 100% rename from regression/exceptions/exceptions7/A.class rename to regression/cbmc-java/exceptions16/A.class diff --git a/regression/exceptions/exceptions2/B.class b/regression/cbmc-java/exceptions16/B.class similarity index 100% rename from regression/exceptions/exceptions2/B.class rename to regression/cbmc-java/exceptions16/B.class diff --git a/regression/exceptions/exceptions2/C.class b/regression/cbmc-java/exceptions16/C.class similarity index 100% rename from regression/exceptions/exceptions2/C.class rename to regression/cbmc-java/exceptions16/C.class diff --git a/regression/cbmc-java/exceptions16/test.class b/regression/cbmc-java/exceptions16/test.class new file mode 100644 index 0000000000000000000000000000000000000000..189317658cea5cab3e52e378ccf0809e28a7198b GIT binary patch literal 718 zcmZWl-A)rh7(KJQ-D#JllpL{WOy5=F+pcO~F+XCaec^JKW z5q>CWH~=*Zl-Hwpq{Z7!hH0d>wCP+is}Ty$=DyobxbiU;~J(}F`qvZZPB+sL7Z^k zUtk|&>>SSPGn6jQ;nK^Cf6AxD7n?0C5;b{TYBEh1NNyU~Z0S<9q~d8dYEs55>R4rK zBWR8Y$q8m~okC`ds8NV);|6XLaf{c7vn6r6`dp$}C9A<*%3dq5z+}Dr4V7a^=LC-Z V754x08=?{{|B2bs9VQm$egkzSbi@Dv literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/exceptions16/test.desc b/regression/cbmc-java/exceptions16/test.desc new file mode 100644 index 00000000000..960b995f7d3 --- /dev/null +++ b/regression/cbmc-java/exceptions16/test.desc @@ -0,0 +1,9 @@ +CORE +test.class +--function test.foo +^EXIT=10$ +^SIGNAL=0$ +^.*assertion at file test.java line 18 function.*: FAILURE$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/exceptions16/test.java b/regression/cbmc-java/exceptions16/test.java new file mode 100644 index 00000000000..9d1c2729516 --- /dev/null +++ b/regression/cbmc-java/exceptions16/test.java @@ -0,0 +1,21 @@ +class A extends RuntimeException {} +class B extends A {} +class C extends B {} + +public class test { + static void foo (int x) { + try { + x++; + } + catch(A exc) { + assert false; + } + + try { + throw new B(); + } + catch(B exc) { + assert false; + } + } +} diff --git a/regression/exceptions/exceptions2/A.class b/regression/cbmc-java/exceptions2/A.class similarity index 100% rename from regression/exceptions/exceptions2/A.class rename to regression/cbmc-java/exceptions2/A.class diff --git a/regression/exceptions/exceptions3/B.class b/regression/cbmc-java/exceptions2/B.class similarity index 100% rename from regression/exceptions/exceptions3/B.class rename to regression/cbmc-java/exceptions2/B.class diff --git a/regression/exceptions/exceptions3/C.class b/regression/cbmc-java/exceptions2/C.class similarity index 100% rename from regression/exceptions/exceptions3/C.class rename to regression/cbmc-java/exceptions2/C.class diff --git a/regression/exceptions/exceptions2/test.class b/regression/cbmc-java/exceptions2/test.class similarity index 100% rename from regression/exceptions/exceptions2/test.class rename to regression/cbmc-java/exceptions2/test.class diff --git a/regression/exceptions/exceptions2/test.desc b/regression/cbmc-java/exceptions2/test.desc similarity index 79% rename from regression/exceptions/exceptions2/test.desc rename to regression/cbmc-java/exceptions2/test.desc index 179b234c875..45f5bac3bc2 100644 --- a/regression/exceptions/exceptions2/test.desc +++ b/regression/cbmc-java/exceptions2/test.desc @@ -4,7 +4,7 @@ test.class ^EXIT=10$ ^SIGNAL=0$ ^.*assertion at file test.java line 15 function.*: FAILURE$ -^\*\* 1 of 2 failed (2 iterations)$ +^\*\* 1 of 5 failed (2 iterations)$ ^VERIFICATION FAILED$ -- ^warning: ignoring diff --git a/regression/exceptions/exceptions2/test.java b/regression/cbmc-java/exceptions2/test.java similarity index 100% rename from regression/exceptions/exceptions2/test.java rename to regression/cbmc-java/exceptions2/test.java diff --git a/regression/exceptions/exceptions3/A.class b/regression/cbmc-java/exceptions3/A.class similarity index 100% rename from regression/exceptions/exceptions3/A.class rename to regression/cbmc-java/exceptions3/A.class diff --git a/regression/exceptions/exceptions4/B.class b/regression/cbmc-java/exceptions3/B.class similarity index 100% rename from regression/exceptions/exceptions4/B.class rename to regression/cbmc-java/exceptions3/B.class diff --git a/regression/exceptions/exceptions4/C.class b/regression/cbmc-java/exceptions3/C.class similarity index 100% rename from regression/exceptions/exceptions4/C.class rename to regression/cbmc-java/exceptions3/C.class diff --git a/regression/exceptions/exceptions3/test.class b/regression/cbmc-java/exceptions3/test.class similarity index 100% rename from regression/exceptions/exceptions3/test.class rename to regression/cbmc-java/exceptions3/test.class diff --git a/regression/exceptions/exceptions3/test.desc b/regression/cbmc-java/exceptions3/test.desc similarity index 100% rename from regression/exceptions/exceptions3/test.desc rename to regression/cbmc-java/exceptions3/test.desc diff --git a/regression/exceptions/exceptions3/test.java b/regression/cbmc-java/exceptions3/test.java similarity index 100% rename from regression/exceptions/exceptions3/test.java rename to regression/cbmc-java/exceptions3/test.java diff --git a/regression/exceptions/exceptions4/A.class b/regression/cbmc-java/exceptions4/A.class similarity index 100% rename from regression/exceptions/exceptions4/A.class rename to regression/cbmc-java/exceptions4/A.class diff --git a/regression/exceptions/exceptions5/B.class b/regression/cbmc-java/exceptions4/B.class similarity index 100% rename from regression/exceptions/exceptions5/B.class rename to regression/cbmc-java/exceptions4/B.class diff --git a/regression/exceptions/exceptions5/C.class b/regression/cbmc-java/exceptions4/C.class similarity index 100% rename from regression/exceptions/exceptions5/C.class rename to regression/cbmc-java/exceptions4/C.class diff --git a/regression/exceptions/exceptions4/test.class b/regression/cbmc-java/exceptions4/test.class similarity index 100% rename from regression/exceptions/exceptions4/test.class rename to regression/cbmc-java/exceptions4/test.class diff --git a/regression/exceptions/exceptions4/test.desc b/regression/cbmc-java/exceptions4/test.desc similarity index 100% rename from regression/exceptions/exceptions4/test.desc rename to regression/cbmc-java/exceptions4/test.desc diff --git a/regression/exceptions/exceptions4/test.java b/regression/cbmc-java/exceptions4/test.java similarity index 100% rename from regression/exceptions/exceptions4/test.java rename to regression/cbmc-java/exceptions4/test.java diff --git a/regression/exceptions/exceptions5/A.class b/regression/cbmc-java/exceptions5/A.class similarity index 100% rename from regression/exceptions/exceptions5/A.class rename to regression/cbmc-java/exceptions5/A.class diff --git a/regression/exceptions/exceptions7/B.class b/regression/cbmc-java/exceptions5/B.class similarity index 100% rename from regression/exceptions/exceptions7/B.class rename to regression/cbmc-java/exceptions5/B.class diff --git a/regression/exceptions/exceptions7/C.class b/regression/cbmc-java/exceptions5/C.class similarity index 100% rename from regression/exceptions/exceptions7/C.class rename to regression/cbmc-java/exceptions5/C.class diff --git a/regression/exceptions/exceptions5/D.class b/regression/cbmc-java/exceptions5/D.class similarity index 100% rename from regression/exceptions/exceptions5/D.class rename to regression/cbmc-java/exceptions5/D.class diff --git a/regression/exceptions/exceptions5/test.class b/regression/cbmc-java/exceptions5/test.class similarity index 100% rename from regression/exceptions/exceptions5/test.class rename to regression/cbmc-java/exceptions5/test.class diff --git a/regression/exceptions/exceptions5/test.desc b/regression/cbmc-java/exceptions5/test.desc similarity index 100% rename from regression/exceptions/exceptions5/test.desc rename to regression/cbmc-java/exceptions5/test.desc diff --git a/regression/exceptions/exceptions5/test.java b/regression/cbmc-java/exceptions5/test.java similarity index 100% rename from regression/exceptions/exceptions5/test.java rename to regression/cbmc-java/exceptions5/test.java diff --git a/regression/exceptions/exceptions6/A.class b/regression/cbmc-java/exceptions6/A.class similarity index 100% rename from regression/exceptions/exceptions6/A.class rename to regression/cbmc-java/exceptions6/A.class diff --git a/regression/exceptions/exceptions6/B.class b/regression/cbmc-java/exceptions6/B.class similarity index 100% rename from regression/exceptions/exceptions6/B.class rename to regression/cbmc-java/exceptions6/B.class diff --git a/regression/exceptions/exceptions6/C.class b/regression/cbmc-java/exceptions6/C.class similarity index 100% rename from regression/exceptions/exceptions6/C.class rename to regression/cbmc-java/exceptions6/C.class diff --git a/regression/exceptions/exceptions6/D.class b/regression/cbmc-java/exceptions6/D.class similarity index 100% rename from regression/exceptions/exceptions6/D.class rename to regression/cbmc-java/exceptions6/D.class diff --git a/regression/exceptions/exceptions6/test.class b/regression/cbmc-java/exceptions6/test.class similarity index 100% rename from regression/exceptions/exceptions6/test.class rename to regression/cbmc-java/exceptions6/test.class diff --git a/regression/exceptions/exceptions6/test.desc b/regression/cbmc-java/exceptions6/test.desc similarity index 100% rename from regression/exceptions/exceptions6/test.desc rename to regression/cbmc-java/exceptions6/test.desc diff --git a/regression/exceptions/exceptions6/test.java b/regression/cbmc-java/exceptions6/test.java similarity index 100% rename from regression/exceptions/exceptions6/test.java rename to regression/cbmc-java/exceptions6/test.java diff --git a/regression/exceptions/exceptions8/A.class b/regression/cbmc-java/exceptions7/A.class similarity index 100% rename from regression/exceptions/exceptions8/A.class rename to regression/cbmc-java/exceptions7/A.class diff --git a/regression/exceptions/exceptions8/B.class b/regression/cbmc-java/exceptions7/B.class similarity index 100% rename from regression/exceptions/exceptions8/B.class rename to regression/cbmc-java/exceptions7/B.class diff --git a/regression/exceptions/exceptions8/C.class b/regression/cbmc-java/exceptions7/C.class similarity index 100% rename from regression/exceptions/exceptions8/C.class rename to regression/cbmc-java/exceptions7/C.class diff --git a/regression/exceptions/exceptions7/test.class b/regression/cbmc-java/exceptions7/test.class similarity index 100% rename from regression/exceptions/exceptions7/test.class rename to regression/cbmc-java/exceptions7/test.class diff --git a/regression/exceptions/exceptions7/test.desc b/regression/cbmc-java/exceptions7/test.desc similarity index 100% rename from regression/exceptions/exceptions7/test.desc rename to regression/cbmc-java/exceptions7/test.desc diff --git a/regression/exceptions/exceptions7/test.java b/regression/cbmc-java/exceptions7/test.java similarity index 100% rename from regression/exceptions/exceptions7/test.java rename to regression/cbmc-java/exceptions7/test.java diff --git a/regression/cbmc-java/exceptions8/A.class b/regression/cbmc-java/exceptions8/A.class new file mode 100644 index 0000000000000000000000000000000000000000..963ae156be051ca07ea2d602053e012a3d27a7a4 GIT binary patch literal 241 zcmXX=O;5r=5PbuswY3W2=*gpUuorF+lg8kw;Q*%hZQaP2c5B)#@o#xD@!${OM-gX{ zNoL+h-b?0i{P_hi$0WiKR{^dAj0ygd4ckY;@a{e*cu&o%CX6#SdfnHBZeLVUi8IZb zQdPNX+3BSuQG(CW@UysN#6;bBCelyKv8QYrJ6YoqP1btzNpmRpEZ_t;J0Rp-H$s}9|kN*P*5s4yPo>K82_(?21 literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/exceptions8/B.class b/regression/cbmc-java/exceptions8/B.class new file mode 100644 index 0000000000000000000000000000000000000000..47ae8f218e49b4ac942425d72a88b21c2772b518 GIT binary patch literal 216 zcmXX7D1o9M#q%+AiT z@6YoEV1a=P9X%U;8$Q8WsZ3RCf!TDLcb3PedAtLN)W> zG^(>I`7{ic1ox2FMIv{qi93}ntJy`|ga-pAfda+`BWV1+DPr)3*K{pl# WT<*@-G|^!l`~vXc^F-)=Q^5xrb|N Date: Fri, 17 Feb 2017 08:42:35 +0000 Subject: [PATCH 07/14] Escaping brackets in test descriptions --- regression/cbmc-java/exceptions1/test.desc | 2 +- regression/cbmc-java/exceptions2/test.desc | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/regression/cbmc-java/exceptions1/test.desc b/regression/cbmc-java/exceptions1/test.desc index ca52107829c..638351f4397 100644 --- a/regression/cbmc-java/exceptions1/test.desc +++ b/regression/cbmc-java/exceptions1/test.desc @@ -4,7 +4,7 @@ test.class ^EXIT=10$ ^SIGNAL=0$ ^.*assertion at file test.java line 26 function.*: FAILURE$ -\*\* 1 of 9 failed (2 iterations)$ +\*\* 1 of 9 failed \(2 iterations\)$ ^VERIFICATION FAILED$ -- ^warning: ignoring diff --git a/regression/cbmc-java/exceptions2/test.desc b/regression/cbmc-java/exceptions2/test.desc index 45f5bac3bc2..8645e5ea074 100644 --- a/regression/cbmc-java/exceptions2/test.desc +++ b/regression/cbmc-java/exceptions2/test.desc @@ -4,7 +4,7 @@ test.class ^EXIT=10$ ^SIGNAL=0$ ^.*assertion at file test.java line 15 function.*: FAILURE$ -^\*\* 1 of 5 failed (2 iterations)$ +^\*\* 1 of 5 failed \(2 iterations\)$ ^VERIFICATION FAILED$ -- ^warning: ignoring From b96e03ac99867fdc3d3d72d7a32f85e6ad0c6dbe Mon Sep 17 00:00:00 2001 From: Cristina Date: Fri, 17 Feb 2017 09:38:26 +0000 Subject: [PATCH 08/14] Fixed test description for cbmc-java/virtual7 The exception handling instrumentation introduces new labels and thus the target of the gotos in the goto-program needs to be incremented. --- regression/cbmc-java/virtual7/test.desc | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/regression/cbmc-java/virtual7/test.desc b/regression/cbmc-java/virtual7/test.desc index b2b26ecb9ce..3846f5c4a69 100644 --- a/regression/cbmc-java/virtual7/test.desc +++ b/regression/cbmc-java/virtual7/test.desc @@ -3,10 +3,10 @@ test.class --show-goto-functions ^EXIT=0$ ^SIGNAL=0$ -IF "java::E".*THEN GOTO [12] -IF "java::B".*THEN GOTO [12] -IF "java::D".*THEN GOTO [12] -IF "java::C".*THEN GOTO [12] +IF "java::E".*THEN GOTO [67] +IF "java::B".*THEN GOTO [67] +IF "java::D".*THEN GOTO [67] +IF "java::C".*THEN GOTO [67] -- IF "java::A".*THEN GOTO -GOTO 4 +GOTO 9 From 3b31d232ce5405b06857a8d34e620f1b6b614841 Mon Sep 17 00:00:00 2001 From: Cristina Date: Tue, 28 Feb 2017 19:34:06 +0000 Subject: [PATCH 09/14] Recompute live ranges for local variables and add corresponding DEAD instructions This needs to be done because the exception handling instrumentation introduces GOTOs which modify the existent live ranges. --- src/goto-programs/remove_exceptions.cpp | 104 +++++++++++++++++++----- 1 file changed, 83 insertions(+), 21 deletions(-) diff --git a/src/goto-programs/remove_exceptions.cpp b/src/goto-programs/remove_exceptions.cpp index 14700921e24..4b4e5debe35 100644 --- a/src/goto-programs/remove_exceptions.cpp +++ b/src/goto-programs/remove_exceptions.cpp @@ -7,11 +7,13 @@ Author: Cristina David Date: December 2016 \*******************************************************************/ -#define DEBUG + #ifdef DEBUG #include #endif + #include +#include #include #include @@ -47,19 +49,20 @@ class remove_exceptionst void instrument_exception_handlers( const goto_functionst::function_mapt::iterator &); - void add_gotos( const goto_functionst::function_mapt::iterator &); void add_throw_gotos( const goto_functionst::function_mapt::iterator &, const goto_programt::instructionst::iterator &, - const stack_catcht &); + const stack_catcht &, + std::vector &); void add_function_call_gotos( const goto_functionst::function_mapt::iterator &, const goto_programt::instructionst::iterator &, - const stack_catcht &); + const stack_catcht &, + std::vector &); }; /*******************************************************************\ @@ -134,7 +137,6 @@ void remove_exceptionst::add_exceptional_returns( rhs_expr_null); t_null->function=function_id; } - return; } /*******************************************************************\ @@ -318,11 +320,13 @@ Purpose: instruments each throw with conditional GOTOS to the void remove_exceptionst::add_throw_gotos( const goto_functionst::function_mapt::iterator &func_it, const goto_programt::instructionst::iterator &instr_it, - const remove_exceptionst::stack_catcht &stack_catch) + const remove_exceptionst::stack_catcht &stack_catch, + std::vector &locals) { assert(instr_it->type==THROW); goto_programt &goto_program=func_it->second.body; + const irep_idt &function_id=func_it->first; assert(instr_it->code.operands().size()==1); @@ -341,6 +345,11 @@ void remove_exceptionst::add_throw_gotos( t_end->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_exprt exc_thrown=exc_symbol.symbol_expr(); + // add GOTOs implementing the dynamic dispatch of the // exception handlers for(std::size_t i=stack_catch.size(); i-->0;) @@ -359,15 +368,21 @@ void remove_exceptionst::add_throw_gotos( // use instanceof to check that this is the correct handler symbol_typet type(stack_catch[i][j].first); type_exprt expr(type); - // find the symbol corresponding to the caught exceptions - exprt exc_symbol=instr_it->code; - while(exc_symbol.id()!=ID_symbol) - exc_symbol=exc_symbol.op0(); - binary_predicate_exprt check(exc_symbol, ID_java_instanceof, expr); + binary_predicate_exprt check(exc_thrown, ID_java_instanceof, expr); t_exc->guard=check; } } + + // 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; + } } /*******************************************************************\ @@ -386,7 +401,8 @@ Purpose: instruments each function call that may escape exceptions void remove_exceptionst::add_function_call_gotos( const goto_functionst::function_mapt::iterator &func_it, const goto_programt::instructionst::iterator &instr_it, - const stack_catcht &stack_catch) + const stack_catcht &stack_catch, + std::vector &locals) { assert(instr_it->type==FUNCTION_CALL); @@ -403,7 +419,7 @@ void remove_exceptionst::add_function_call_gotos( if(symbol_table.has_symbol(id2string(callee_id)+EXC_SUFFIX)) { - // dynamic dispatch of the escaped exception + // 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(); @@ -429,11 +445,20 @@ void remove_exceptionst::add_function_call_gotos( } } + // 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; + } + // add a null check (so that instanceof can be applied) equal_exprt eq_null( callee_exc, null_pointer_exprt(pointer_typet(empty_typet()))); - // jump to the next instruction goto_programt::targett t_null=goto_program.insert_after(instr_it); t_null->make_goto(next_it); t_null->source_location=instr_it->source_location; @@ -458,20 +483,54 @@ Purpose: instruments each throw and function calls that may escape exceptions void remove_exceptionst::add_gotos( const goto_functionst::function_mapt::iterator &func_it) { - // Stack of try-catch blocks - stack_catcht stack_catch; - + stack_catcht stack_catch; // stack of try-catch blocks + std::vector> stack_locals; // stack of local vars + std::vector locals; + bool skip_dead=false; goto_programt &goto_program=func_it->second.body; if(goto_program.empty()) return; Forall_goto_program_instructions(instr_it, goto_program) { + if(!instr_it->labels.empty()) + skip_dead=false; + if(instr_it->is_decl()) + { + code_declt decl=to_code_decl(instr_it->code); + locals.push_back(decl.symbol()); + } + if(instr_it->is_dead()) + { + code_deadt dead=to_code_dead(instr_it->code); + auto it=std::find(locals.begin(), + locals.end(), + dead.symbol()); + // avoid DEAD re-declarations + if(it==locals.end()) + { + if(skip_dead) + { + // this DEAD has been already added by a throw + instr_it->make_skip(); + } + } + else + { + locals.erase(it); + } + } // it's a CATCH but not a handler - if(instr_it->type==CATCH && !instr_it->code.has_operands()) + else if(instr_it->type==CATCH && !instr_it->code.has_operands()) { if(instr_it->targets.empty()) // pop { + // pop the local vars stack + if(!stack_locals.empty()) + { + locals=stack_locals.back(); + stack_locals.pop_back(); + } // pop from the stack if possible if(!stack_catch.empty()) { @@ -486,6 +545,9 @@ void remove_exceptionst::add_gotos( } else // push { + stack_locals.push_back(locals); + locals.clear(); + remove_exceptionst::catch_handlerst exception; stack_catch.push_back(exception); remove_exceptionst::catch_handlerst &last_exception= @@ -505,16 +567,16 @@ void remove_exceptionst::add_gotos( i++; } } - instr_it->make_skip(); } else if(instr_it->type==THROW) { - add_throw_gotos(func_it, instr_it, stack_catch); + skip_dead=true; + add_throw_gotos(func_it, instr_it, stack_catch, locals); } else if(instr_it->type==FUNCTION_CALL) { - add_function_call_gotos(func_it, instr_it, stack_catch); + add_function_call_gotos(func_it, instr_it, stack_catch, locals); } } } From 96764a2db85552749cbc876d806f84126134a08f Mon Sep 17 00:00:00 2001 From: Cristina Date: Tue, 28 Feb 2017 19:35:54 +0000 Subject: [PATCH 10/14] Forced try-catch to start a new basic block This was required in order for variables local to the try-catch to be declared at the right location. This way, after adding the exception instrumentation in remove_exceptions, we will be able to correctly re-compute live ranges for these variables. --- .../java_bytecode_convert_method.cpp | 27 ++++++++++++++----- 1 file changed, 21 insertions(+), 6 deletions(-) diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index 19174326c6c..bc13e61c1cf 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -5,7 +5,7 @@ Module: JAVA Bytecode Language Conversion Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ - +#define DEBUG #ifdef DEBUG #include #endif @@ -2080,7 +2080,10 @@ codet java_bytecode_convert_methodt::convert_instructions( std::vector exception_ids; std::vector handler_labels; - // add the CATCH-PUSH instruction(s) + // for each try-catch add a CATCH-PUSH instruction + // each CATCH-PUSH records a list of all the handler labels + // together with a list of all the exception ids + // be aware of different try-catch blocks with the same starting pc std::size_t pos=0; size_t end_pc=0; @@ -2100,8 +2103,7 @@ codet java_bytecode_convert_methodt::convert_instructions( method.exception_table[pos].end_pc==end_pc) { exception_ids.push_back( - method.exception_table[pos]. - catch_type.get_identifier()); + method.exception_table[pos].catch_type.get_identifier()); // record the exception handler in the CATCH-PUSH // instruction by generating a label corresponding to // the handler's pc @@ -2122,7 +2124,7 @@ codet java_bytecode_convert_methodt::convert_instructions( for(size_t i=0; i1; - + // Start a new lexical block if we've just entered a try block + if(!start_new_block && previous_address!=-1) + { + for(const auto &exception_row : method.exception_table) + if(exception_row.start_pc==previous_address) + { + start_new_block=true; + break; + } + } + if(start_new_block) { code_labelt newlabel(label(std::to_string(address)), code_blockt()); @@ -2330,6 +2343,8 @@ codet java_bytecode_convert_methodt::convert_instructions( add_to_block.add(c); } start_new_block=address_pair.second.successors.size()>1; + + previous_address=address; } // Find out where temporaries are used: From 13c8f8366f3cbf83360dad302110863c45738438 Mon Sep 17 00:00:00 2001 From: Cristina Date: Thu, 2 Mar 2017 15:46:03 +0000 Subject: [PATCH 11/14] Restructuring such that the exceptions instrumentation is added in one pass over the goto-program --- src/goto-programs/goto_program_template.h | 8 + src/goto-programs/remove_exceptions.cpp | 286 +++++++----------- .../java_bytecode_convert_method.cpp | 22 +- src/util/std_code.h | 4 +- 4 files changed, 124 insertions(+), 196 deletions(-) diff --git a/src/goto-programs/goto_program_template.h b/src/goto-programs/goto_program_template.h index 77161fcb4d8..bd9cb39c73e 100644 --- a/src/goto-programs/goto_program_template.h +++ b/src/goto-programs/goto_program_template.h @@ -474,6 +474,14 @@ class goto_program_templatet instructions.clear(); } + targett get_end_function() + { + assert(!instructions.empty()); + targett end_function=--instructions.end(); + assert(end_function->is_end_function()); + return end_function; + } + //! Copy a full goto program, preserving targets void copy_from(const goto_program_templatet &src); diff --git a/src/goto-programs/remove_exceptions.cpp b/src/goto-programs/remove_exceptions.cpp index 4b4e5debe35..8bbbd79e165 100644 --- a/src/goto-programs/remove_exceptions.cpp +++ b/src/goto-programs/remove_exceptions.cpp @@ -41,28 +41,24 @@ class remove_exceptionst void add_exceptional_returns( const goto_functionst::function_mapt::iterator &); - void replace_throws( - const goto_functionst::function_mapt::iterator &); - - void instrument_function_calls( - const goto_functionst::function_mapt::iterator &); - - void instrument_exception_handlers( - const goto_functionst::function_mapt::iterator &); - void add_gotos( - const goto_functionst::function_mapt::iterator &); + void instrument_exception_handler( + const goto_functionst::function_mapt::iterator &, + const goto_programt::instructionst::iterator &); - void add_throw_gotos( + void instrument_throw( const goto_functionst::function_mapt::iterator &, const goto_programt::instructionst::iterator &, const stack_catcht &, std::vector &); - void add_function_call_gotos( + void instrument_function_call( const goto_functionst::function_mapt::iterator &, const goto_programt::instructionst::iterator &, const stack_catcht &, std::vector &); + + void instrument_exceptions( + const goto_functionst::function_mapt::iterator &); }; /*******************************************************************\ @@ -99,7 +95,7 @@ void remove_exceptionst::add_exceptional_returns( // function calls that may escape exceptions. However, this will // require multiple passes. bool add_exceptional_var=false; - Forall_goto_program_instructions(instr_it, goto_program) + forall_goto_program_instructions(instr_it, goto_program) if(instr_it->is_throw() || instr_it->is_function_call()) { add_exceptional_var=true; @@ -125,8 +121,7 @@ void remove_exceptionst::add_exceptional_returns( // initialize the exceptional return with NULL symbol_exprt lhs_expr_null=new_symbol.symbol_expr(); - exprt rhs_expr_null; - rhs_expr_null=null_pointer_exprt(pointer_typet(empty_typet())); + null_pointer_exprt rhs_expr_null((pointer_typet(empty_typet()))); goto_programt::targett t_null= goto_program.insert_before(goto_program.instructions.begin()); t_null->make_assignment(); @@ -141,106 +136,7 @@ void remove_exceptionst::add_exceptional_returns( /*******************************************************************\ -Function: remove_exceptionst::replace_throws - -Inputs: - -Outputs: - -Purpose: turns 'throw x' in function f into an assignment to f#exc_value - -\*******************************************************************/ - -void remove_exceptionst::replace_throws( - const goto_functionst::function_mapt::iterator &func_it) -{ - const irep_idt &function_id=func_it->first; - goto_programt &goto_program=func_it->second.body; - - if(goto_program.empty()) - return; - - Forall_goto_program_instructions(instr_it, goto_program) - { - if(instr_it->is_throw() && - symbol_table.has_symbol(id2string(function_id)+EXC_SUFFIX)) - { - assert(instr_it->code.operands().size()==1); - const symbolt &exc_symbol= - symbol_table.lookup(id2string(function_id)+EXC_SUFFIX); - - // replace "throw x;" by "f#exception_value=x;" - symbol_exprt lhs_expr=exc_symbol.symbol_expr(); - // find the symbol corresponding to the thrown exceptions - exprt exc_expr=instr_it->code; - while(exc_expr.id()!=ID_symbol && exc_expr.has_operands()) - exc_expr=exc_expr.op0(); - - // add the assignment with the appropriate cast - code_assignt assignment(typecast_exprt(lhs_expr, exc_expr.type()), - exc_expr); - // now turn the `throw' into `assignment' - instr_it->type=ASSIGN; - instr_it->code=assignment; - } - } -} - -/*******************************************************************\ - -Function: remove_exceptionst::instrument_function_calls - -Inputs: - -Outputs: - -Purpose: after each function call g() in function f - adds f#exception_value=g#exception_value; - -\*******************************************************************/ - -void remove_exceptionst::instrument_function_calls( - const goto_functionst::function_mapt::iterator &func_it) -{ - const irep_idt &caller_id=func_it->first; - goto_programt &goto_program=func_it->second.body; - - if(goto_program.empty()) - return; - - Forall_goto_program_instructions(instr_it, goto_program) - { - if(instr_it->is_function_call()) - { - code_function_callt &function_call=to_code_function_call(instr_it->code); - const irep_idt &callee_id= - to_symbol_expr(function_call.function()).get_identifier(); - - // can exceptions escape? - if(symbol_table.has_symbol(id2string(callee_id)+EXC_SUFFIX) && - symbol_table.has_symbol(id2string(caller_id)+EXC_SUFFIX)) - { - const symbolt &callee= - symbol_table.lookup(id2string(callee_id)+EXC_SUFFIX); - const symbolt &caller= - symbol_table.lookup(id2string(caller_id)+EXC_SUFFIX); - - symbol_exprt rhs_expr=callee.symbol_expr(); - 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, rhs_expr); - t->function=instr_it->function; - } - } - } -} - -/*******************************************************************\ - -Function: remove_exceptionst::instrument_exception_handlers +Function: remove_exceptionst::instrument_exception_handler Inputs: @@ -251,62 +147,52 @@ Purpose: at the beginning of each handler in function f \*******************************************************************/ -void remove_exceptionst::instrument_exception_handlers( - const goto_functionst::function_mapt::iterator &func_it) +void remove_exceptionst::instrument_exception_handler( + const goto_functionst::function_mapt::iterator &func_it, + const goto_programt::instructionst::iterator &instr_it) { const irep_idt &function_id=func_it->first; goto_programt &goto_program=func_it->second.body; - if(goto_program.empty()) - return; + assert(instr_it->type==CATCH && instr_it->code.has_operands()); - Forall_goto_program_instructions(instr_it, goto_program) + // retrieve the exception variable + const exprt &exception=instr_it->code.op0(); + + if(symbol_table.has_symbol(id2string(function_id)+EXC_SUFFIX)) { - // is this a handler - if(instr_it->type==CATCH && instr_it->code.has_operands()) - { - // retrieve the exception variable - const irept &exception=instr_it->code.op0(); + const symbolt &function_symbol= + symbol_table.lookup(id2string(function_id)+EXC_SUFFIX); + // next we reset the exceptional return to NULL + symbol_exprt lhs_expr_null=function_symbol.symbol_expr(); + null_pointer_exprt rhs_expr_null((pointer_typet(empty_typet()))); - if(symbol_table.has_symbol(id2string(function_id)+EXC_SUFFIX)) - { - const symbolt &function_symbol= - symbol_table.lookup(id2string(function_id)+EXC_SUFFIX); - // next we reset the exceptional return to NULL - symbol_exprt lhs_expr_null=function_symbol.symbol_expr(); - exprt rhs_expr_null; - rhs_expr_null=null_pointer_exprt(pointer_typet(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); - t_null->function=instr_it->function; - - // add the assignment exc=f#exception_value - symbol_exprt rhs_expr_exc=function_symbol.symbol_expr(); - - const exprt &lhs_expr_exc=static_cast(exception); - 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(lhs_expr_exc, rhs_expr_exc.type()), - rhs_expr_exc); - t_exc->function=instr_it->function; - } + // 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); + t_null->function=instr_it->function; - instr_it->make_skip(); - } + // add the assignment exc=f#exception_value + symbol_exprt rhs_expr_exc=function_symbol.symbol_expr(); + + 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); + t_exc->function=instr_it->function; } + instr_it->make_skip(); } /*******************************************************************\ -Function: remove_exceptionst::add_gotos_throw +Function: remove_exceptionst::instrument_throw Inputs: @@ -317,7 +203,7 @@ Purpose: instruments each throw with conditional GOTOS to the \*******************************************************************/ -void remove_exceptionst::add_throw_gotos( +void remove_exceptionst::instrument_throw( const goto_functionst::function_mapt::iterator &func_it, const goto_programt::instructionst::iterator &instr_it, const remove_exceptionst::stack_catcht &stack_catch, @@ -331,10 +217,7 @@ void remove_exceptionst::add_throw_gotos( assert(instr_it->code.operands().size()==1); // find the end of the function - goto_programt::targett end_function; - for(end_function=instr_it; - !end_function->is_end_function(); - end_function++) {} + goto_programt::targett end_function=goto_program.get_end_function(); if(end_function!=instr_it) { // jump to the end of the function @@ -345,6 +228,7 @@ void remove_exceptionst::add_throw_gotos( t_end->function=instr_it->function; } + // find the symbol corresponding to the caught exceptions const symbolt &exc_symbol= symbol_table.lookup(id2string(function_id)+EXC_SUFFIX); @@ -383,22 +267,34 @@ void remove_exceptionst::add_throw_gotos( t_dead->source_location=instr_it->source_location; t_dead->function=instr_it->function; } + + // replace "throw x;" by "f#exception_value=x;" + exprt exc_expr=instr_it->code; + while(exc_expr.id()!=ID_symbol && exc_expr.has_operands()) + exc_expr=exc_expr.op0(); + + // add the assignment with the appropriate cast + code_assignt assignment(typecast_exprt(exc_thrown, exc_expr.type()), + exc_expr); + // now turn the `throw' into `assignment' + instr_it->type=ASSIGN; + instr_it->code=assignment; } /*******************************************************************\ -Function: remove_exceptionst::add_function_call_gotos +Function: remove_exceptionst::instrument_function_call Inputs: Outputs: Purpose: instruments each function call that may escape exceptions - with conditional GOTOS to the corresponding exception handlers + with conditional GOTOS to the corresponding exception handlers \*******************************************************************/ -void remove_exceptionst::add_function_call_gotos( +void remove_exceptionst::instrument_function_call( const goto_functionst::function_mapt::iterator &func_it, const goto_programt::instructionst::iterator &instr_it, const stack_catcht &stack_catch, @@ -407,6 +303,7 @@ void remove_exceptionst::add_function_call_gotos( assert(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::instructionst::iterator next_it=instr_it; @@ -424,6 +321,18 @@ void remove_exceptionst::add_function_call_gotos( 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 end_function=goto_program.get_end_function(); + if(end_function!=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(end_function); + t_end->source_location=instr_it->source_location; + t_end->function=instr_it->function; + } + for(std::size_t i=stack_catch.size(); i-->0;) { for(std::size_t j=stack_catch[i].size(); j-->0;) @@ -464,43 +373,57 @@ void remove_exceptionst::add_function_call_gotos( t_null->source_location=instr_it->source_location; t_null->function=instr_it->function; t_null->guard=eq_null; + + // 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->function=instr_it->function; } } /*******************************************************************\ -Function: remove_exceptionst::add_gotos +Function: remove_exceptionst::instrument_exceptions Inputs: Outputs: -Purpose: instruments each throw and function calls that may escape exceptions - with conditional GOTOS to the corresponding exception handlers +Purpose: instruments throws, function calls that may escape exceptions + and exception handlers. Additionally, it re-computes + the live-range of local variables in order to add DEAD instructions. \*******************************************************************/ -void remove_exceptionst::add_gotos( +void remove_exceptionst::instrument_exceptions( const goto_functionst::function_mapt::iterator &func_it) { stack_catcht stack_catch; // stack of try-catch blocks std::vector> stack_locals; // stack of local vars std::vector locals; - bool skip_dead=false; goto_programt &goto_program=func_it->second.body; if(goto_program.empty()) return; Forall_goto_program_instructions(instr_it, goto_program) { + // this flag is used to skip DEAD redeclaration if(!instr_it->labels.empty()) skip_dead=false; + if(instr_it->is_decl()) { code_declt decl=to_code_decl(instr_it->code); locals.push_back(decl.symbol()); } - if(instr_it->is_dead()) + else if(instr_it->is_dead()) { code_deadt dead=to_code_dead(instr_it->code); auto it=std::find(locals.begin(), @@ -569,19 +492,23 @@ void remove_exceptionst::add_gotos( } instr_it->make_skip(); } + // 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) { skip_dead=true; - add_throw_gotos(func_it, instr_it, stack_catch, locals); + instrument_throw(func_it, instr_it, stack_catch, locals); } else if(instr_it->type==FUNCTION_CALL) { - add_function_call_gotos(func_it, instr_it, stack_catch, locals); + instrument_function_call(func_it, instr_it, stack_catch, locals); } } } - /*******************************************************************\ Function: remove_exceptionst::operator() @@ -597,16 +524,9 @@ Function: remove_exceptionst::operator() void remove_exceptionst::operator()(goto_functionst &goto_functions) { Forall_goto_functions(it, goto_functions) - { add_exceptional_returns(it); - } Forall_goto_functions(it, goto_functions) - { - instrument_exception_handlers(it); - add_gotos(it); - instrument_function_calls(it); - replace_throws(it); - } + instrument_exceptions(it); } /*******************************************************************\ diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index bc13e61c1cf..678dfe13576 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -5,7 +5,7 @@ Module: JAVA Bytecode Language Conversion Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ -#define DEBUG + #ifdef DEBUG #include #endif @@ -1031,10 +1031,10 @@ codet java_bytecode_convert_methodt::convert_instructions( // we throw away the first statement in an exception handler // as we don't know if a function call had a normal or exceptional return - size_t e; - for(e=0; ehandler_pc) { exprt exc_var=variable( arg0, statement[0], @@ -1051,7 +1051,7 @@ codet java_bytecode_convert_methodt::convert_instructions( catch_handler_expr.get_sub().resize(1); catch_handler_expr.get_sub()[0]=exc_var; - codet catch_handler=code_expressiont(catch_handler_expr); + code_expressiont catch_handler(catch_handler_expr); code_labelt newlabel(label(std::to_string(cur_pc)), code_blockt()); @@ -1065,7 +1065,7 @@ codet java_bytecode_convert_methodt::convert_instructions( } } - if(e Date: Thu, 2 Mar 2017 16:53:29 +0000 Subject: [PATCH 12/14] Add jump to the end of the current function if a function call throws an exception for which there is no handler --- regression/cbmc-java/exceptions9/test.class | Bin 976 -> 976 bytes src/goto-programs/remove_exceptions.cpp | 29 ++---------------- .../java_bytecode_convert_method.cpp | 6 ++-- 3 files changed, 5 insertions(+), 30 deletions(-) diff --git a/regression/cbmc-java/exceptions9/test.class b/regression/cbmc-java/exceptions9/test.class index 42f38bdf8b411bc40f4fb15444a6d085cda2a375..ee137ed9bf6ccb8312157e118fe6f87aedaec1a9 100644 GIT binary patch delta 25 gcmcb>et~_13p1}OgCK)4gAjuXg9d}zet~_13p1}8gCK(ngAju%g9d~8labels.empty()) - skip_dead=false; - if(instr_it->is_decl()) { code_declt decl=to_code_decl(instr_it->code); locals.push_back(decl.symbol()); } - else if(instr_it->is_dead()) - { - code_deadt dead=to_code_dead(instr_it->code); - auto it=std::find(locals.begin(), - locals.end(), - dead.symbol()); - // avoid DEAD re-declarations - if(it==locals.end()) - { - if(skip_dead) - { - // this DEAD has been already added by a throw - instr_it->make_skip(); - } - } - else - { - locals.erase(it); - } - } - // it's a CATCH but not a handler + // it's a CATCH but not a handler (as it has no operands) else if(instr_it->type==CATCH && !instr_it->code.has_operands()) { if(instr_it->targets.empty()) // pop @@ -492,14 +468,13 @@ void remove_exceptionst::instrument_exceptions( } instr_it->make_skip(); } - // handler + // 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) { - skip_dead=true; instrument_throw(func_it, instr_it, stack_catch, locals); } else if(instr_it->type==FUNCTION_CALL) diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index 678dfe13576..3e9cebc116a 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -2083,7 +2083,7 @@ codet java_bytecode_convert_methodt::convert_instructions( // for each try-catch add a CATCH-PUSH instruction // each CATCH-PUSH records a list of all the handler labels // together with a list of all the exception ids - + // be aware of different try-catch blocks with the same starting pc std::size_t pos=0; std::size_t end_pc=0; @@ -2124,7 +2124,7 @@ codet java_bytecode_convert_methodt::convert_instructions( for(size_t i=0; i Date: Thu, 2 Mar 2017 16:59:39 +0000 Subject: [PATCH 13/14] Modified the expected goto-program for cbmc-java/virtual7 as exception handling instrumentation introduces new labels and GOTOs --- regression/cbmc-java/virtual7/test.desc | 1 - 1 file changed, 1 deletion(-) diff --git a/regression/cbmc-java/virtual7/test.desc b/regression/cbmc-java/virtual7/test.desc index 3846f5c4a69..2e196d82e8c 100644 --- a/regression/cbmc-java/virtual7/test.desc +++ b/regression/cbmc-java/virtual7/test.desc @@ -9,4 +9,3 @@ IF "java::D".*THEN GOTO [67] IF "java::C".*THEN GOTO [67] -- IF "java::A".*THEN GOTO -GOTO 9 From 4a446687be65bec3260dc26fe7f2cc4a292db4ee Mon Sep 17 00:00:00 2001 From: Cristina Date: Thu, 2 Mar 2017 17:13:47 +0000 Subject: [PATCH 14/14] + regression test for Java exception handling --- regression/cbmc-java/exceptions18/A.class | Bin 0 -> 241 bytes regression/cbmc-java/exceptions18/Test.class | Bin 0 -> 756 bytes regression/cbmc-java/exceptions18/Test.java | 23 +++++++++++++++++++ regression/cbmc-java/exceptions18/test.desc | 8 +++++++ 4 files changed, 31 insertions(+) create mode 100644 regression/cbmc-java/exceptions18/A.class create mode 100644 regression/cbmc-java/exceptions18/Test.class create mode 100644 regression/cbmc-java/exceptions18/Test.java create mode 100644 regression/cbmc-java/exceptions18/test.desc diff --git a/regression/cbmc-java/exceptions18/A.class b/regression/cbmc-java/exceptions18/A.class new file mode 100644 index 0000000000000000000000000000000000000000..eb37079f4ed73d57cc2b6947f9e46c6bcc1e8e5b GIT binary patch literal 241 zcmXX=Jxjzu5Pg$RlZ!?ytt{2z(%30N5Uqm6T}Z!)i|&!^9?3@hTULUFKfoU)&PE4j z-Usi&eE)oY0l30(3Ll3tj$-75=tgN}ZwdbSMMDVg%#$SKmD2KY9$GopqV3r^sZ1yO zMvThoe>1QzYT{~DUK7%-na55(C>Kv^Iob72yow9~LIRb9Q>Tkw=;vZHYpVu%|JKR9 tRYv0s9>3*=c)7wDF)J9I6JCCR-kEra`9_OLIAEUr1&|=)<>EFAy< literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/exceptions18/Test.class b/regression/cbmc-java/exceptions18/Test.class new file mode 100644 index 0000000000000000000000000000000000000000..1c2f3dba0083acf483f5b48a1fc3425e77f16268 GIT binary patch literal 756 zcmX|7O-~b16g_w5&Ac)cD71peSBs#fel!v60+j?zNH7%_5E2s;GOZ&H){ZGtqptfq z+_GjPi6(aMPjZ2t_gY=N`*H5Q=e&D=U48!vU<0cGd=xcG0UQ(qcv#lBsj(vPAII%D z-4eLvwIhLgn!Jt#6ZNR6n0{h4?&f_jnBwYKa9@ON8~t3 z5`jm195SnK8|;n2RC&+P%NM>qfew%3c01}Y`@~0nB1t#3$Y*Aaf7#eU8aCfO4?kE* z`|FY*I7qskX0#iduZ`={Z@Fbjnm=*?_?u z9#$x0S*8b_LzWD)3FIvEB&G&@QX#52Rdb*898p_6SKOMK`-;3<^M)Fme&rifPsuq( zHx)Z(RsS6R{=NPMrvt3uHoe2e9?-gWn`cx2e{VEBs%lIU&l4#ynx>t>0