From 770728742fa094fef3bbe8e84b94d9d4150436e6 Mon Sep 17 00:00:00 2001 From: Cristina Date: Thu, 8 Jun 2017 15:05:21 +0100 Subject: [PATCH 1/3] Always push the current exceptional return variable on the stack before converting an exception handler --- src/goto-programs/remove_exceptions.cpp | 4 +- .../java_bytecode_convert_method.cpp | 67 ++++++++----------- src/java_bytecode/java_entry_point.cpp | 19 +++--- 3 files changed, 42 insertions(+), 48 deletions(-) diff --git a/src/goto-programs/remove_exceptions.cpp b/src/goto-programs/remove_exceptions.cpp index 5726831804f..3cac66456d0 100644 --- a/src/goto-programs/remove_exceptions.cpp +++ b/src/goto-programs/remove_exceptions.cpp @@ -90,8 +90,8 @@ void remove_exceptionst::add_exceptional_returns( if(goto_program.empty()) return; - // the entry function has already been added to the symbol table - // if you find it, initialise it + // some methods (e.g. the entry method) have already been added to + // the symbol table; if you find it, initialise it if(symbol_table.has_symbol(id2string(function_id)+EXC_SUFFIX)) { const symbolt &symbol= diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index 9e295f2dcc6..1c469b01ffb 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -20,6 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include "java_bytecode_convert_method.h" @@ -1305,48 +1306,37 @@ 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 auto it=method.exception_table.begin(); for(; it!=method.exception_table.end(); ++it) { if(cur_pc==it->handler_pc) { - exprt exc_var=variable( - arg0, statement[0], - i_it->address, - NO_CAST); - - // 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.get_sub().resize(1); - catch_handler_expr.get_sub()[0]=exc_var; - - code_expressiont catch_handler(catch_handler_expr); - code_labelt newlabel(label(std::to_string(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; + // at the beginning of a handler, clear the stack and + // push the corresponding exceptional return variable + stack.clear(); + auxiliary_symbolt new_symbol; + new_symbol.is_static_lifetime=true; + int file_name_length= + id2string(method.source_location.get_file()).size(); + // remove the file extension + const std::string &file_name= + id2string(method.source_location.get_file()). + substr(0, file_name_length-5); + // generate the name of the exceptional return variable + const std::string &exceptional_var_name= + "java::"+file_name+"."+ + id2string(method.name)+":"+ + id2string(method.signature)+ + EXC_SUFFIX; + new_symbol.base_name=exceptional_var_name; + new_symbol.name=exceptional_var_name; + new_symbol.type=typet(ID_pointer, empty_typet()); + new_symbol.mode=ID_java; + symbol_table.add(new_symbol); + stack.push_back(new_symbol.symbol_expr()); } } - if(it!=method.exception_table.end()) - { - // go straight to the next statement - continue; - } - exprt::operandst op=pop(bytecode_info.pop); exprt::operandst results; results.resize(bytecode_info.push, nil_exprt()); @@ -2407,6 +2397,10 @@ codet java_bytecode_convert_methodt::convert_instructions( results[1]=op[0]; results[0]=op[1]; } + else if(statement=="nop") + { + c=code_skipt(); + } else { c=codet(statement); @@ -2533,9 +2527,7 @@ 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 + // clear the stack if this is an exception handler for(const auto &exception_row : method.exception_table) { if(address==exception_row.handler_pc) @@ -2604,7 +2596,6 @@ codet java_bytecode_convert_methodt::convert_instructions( c.copy_to_operands(*o_it); } } - a_it2->second.stack=stack; } } diff --git a/src/java_bytecode/java_entry_point.cpp b/src/java_bytecode/java_entry_point.cpp index a16959b96da..0e7c0c14b51 100644 --- a/src/java_bytecode/java_entry_point.cpp +++ b/src/java_bytecode/java_entry_point.cpp @@ -589,14 +589,17 @@ bool java_entry_point( call_main.lhs()=return_symbol.symbol_expr(); } - // add the exceptional return value - auxiliary_symbolt exc_symbol; - exc_symbol.mode=ID_C; - exc_symbol.is_static_lifetime=false; - exc_symbol.name=id2string(symbol.name)+EXC_SUFFIX; - exc_symbol.base_name=id2string(symbol.name)+EXC_SUFFIX; - exc_symbol.type=typet(ID_pointer, empty_typet()); - symbol_table.add(exc_symbol); + if(!symbol_table.has_symbol(id2string(symbol.name)+EXC_SUFFIX)) + { + // add the exceptional return value + auxiliary_symbolt exc_symbol; + exc_symbol.mode=ID_C; + exc_symbol.is_static_lifetime=false; + exc_symbol.name=id2string(symbol.name)+EXC_SUFFIX; + exc_symbol.base_name=id2string(symbol.name)+EXC_SUFFIX; + exc_symbol.type=typet(ID_pointer, empty_typet()); + symbol_table.add(exc_symbol); + } exprt::operandst main_arguments= java_build_arguments( From bb9c28ac6768c2d3bcb37a158139489c5df9b80a Mon Sep 17 00:00:00 2001 From: Cristina Date: Thu, 8 Jun 2017 17:32:35 +0100 Subject: [PATCH 2/3] Added regression test capturing an exception handler that does not start with astore --- .../exceptions19/exception_handler.class | Bin 0 -> 254 bytes .../exceptions19/exception_handler.j | 25 ++++++++++++++++++ regression/cbmc-java/exceptions19/test.desc | 8 ++++++ 3 files changed, 33 insertions(+) create mode 100644 regression/cbmc-java/exceptions19/exception_handler.class create mode 100644 regression/cbmc-java/exceptions19/exception_handler.j create mode 100644 regression/cbmc-java/exceptions19/test.desc diff --git a/regression/cbmc-java/exceptions19/exception_handler.class b/regression/cbmc-java/exceptions19/exception_handler.class new file mode 100644 index 0000000000000000000000000000000000000000..a274bf56dfb91f308560f74850f522fe47989d8e GIT binary patch literal 254 zcmZWj%?`m}5S*>*AEk{4;D|%LfVc=JiGxJqBvl{UG_5oxUaJ=p67C*KYzYqbu#?%D z+06ZMz5;My8K^=bSb@8DJE0q`JL5$lyp&)};$7m2p&tr@()A-h?HSOZlp(`Zp{pnp zY;o|!Hud9ZzHy^vC=!C)kC&XG6`}U~JNOt0g=TBY+F#TOR7hw*()V + aload_0 + invokevirtual java/lang/Object/()V + return +.end method + +.method public f()V + .limit stack 4 + .limit locals 4 + + begin: + new java/lang/Exception + dup + invokespecial java/lang/Exception.()V + athrow + start: + nop + end: + astore_1 + return +.catch all from begin to end using start +.end method diff --git a/regression/cbmc-java/exceptions19/test.desc b/regression/cbmc-java/exceptions19/test.desc new file mode 100644 index 00000000000..ed4bf5a2715 --- /dev/null +++ b/regression/cbmc-java/exceptions19/test.desc @@ -0,0 +1,8 @@ +CORE +exception_handler.class +--function exception_handler.f +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring From 8f629b6a0ea49f064cd883945fae9efbee8706c7 Mon Sep 17 00:00:00 2001 From: Cristina Date: Mon, 12 Jun 2017 08:53:32 +0100 Subject: [PATCH 3/3] Addressed reviewers comments --- .../exceptions19/exception_handler.class | Bin 254 -> 254 bytes .../exceptions19/exception_handler.j | 2 +- .../java_bytecode_convert_method.cpp | 20 +++++------------- .../java_bytecode_convert_method_class.h | 3 ++- src/java_bytecode/java_entry_point.cpp | 2 +- 5 files changed, 9 insertions(+), 18 deletions(-) diff --git a/regression/cbmc-java/exceptions19/exception_handler.class b/regression/cbmc-java/exceptions19/exception_handler.class index a274bf56dfb91f308560f74850f522fe47989d8e..39457a939710f4a25765957805c6fb57bb965544 100644 GIT binary patch delta 32 jcmeyz_>XbIQ^`o5jSP$o3=EtM96*u*$YutTObmPgiD3l^ delta 32 jcmeyz_>XbIQ%MG&jSP$o3=EtM96*u*$YutTObmPgfUpFx diff --git a/regression/cbmc-java/exceptions19/exception_handler.j b/regression/cbmc-java/exceptions19/exception_handler.j index 60ecf0461b8..04b3c177689 100644 --- a/regression/cbmc-java/exceptions19/exception_handler.j +++ b/regression/cbmc-java/exceptions19/exception_handler.j @@ -17,7 +17,7 @@ invokespecial java/lang/Exception.()V athrow start: - nop + dup end: astore_1 return diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index 1c469b01ffb..5b7f71d9554 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -473,7 +473,8 @@ void java_bytecode_convert_methodt::convert( tmp_vars.clear(); if((!m.is_abstract) && (!m.is_native)) - method_symbol.value=convert_instructions(m, code_type); + method_symbol.value=convert_instructions( + m, code_type, method_symbol.name); // Replace the existing stub symbol with the real deal: const auto s_it=symbol_table.symbols.find(method.get_name()); @@ -1120,7 +1121,8 @@ Function: java_bytecode_convert_methodt::convert_instructions codet java_bytecode_convert_methodt::convert_instructions( const methodt &method, - const code_typet &method_type) + const code_typet &method_type, + const irep_idt &method_name) { const instructionst &instructions=method.instructions; @@ -1316,17 +1318,9 @@ codet java_bytecode_convert_methodt::convert_instructions( stack.clear(); auxiliary_symbolt new_symbol; new_symbol.is_static_lifetime=true; - int file_name_length= - id2string(method.source_location.get_file()).size(); - // remove the file extension - const std::string &file_name= - id2string(method.source_location.get_file()). - substr(0, file_name_length-5); // generate the name of the exceptional return variable const std::string &exceptional_var_name= - "java::"+file_name+"."+ - id2string(method.name)+":"+ - id2string(method.signature)+ + id2string(method_name)+ EXC_SUFFIX; new_symbol.base_name=exceptional_var_name; new_symbol.name=exceptional_var_name; @@ -2397,10 +2391,6 @@ codet java_bytecode_convert_methodt::convert_instructions( results[1]=op[0]; results[0]=op[1]; } - else if(statement=="nop") - { - c=code_skipt(); - } else { c=codet(statement); diff --git a/src/java_bytecode/java_bytecode_convert_method_class.h b/src/java_bytecode/java_bytecode_convert_method_class.h index da9196e6a67..c4c1e1a8788 100644 --- a/src/java_bytecode/java_bytecode_convert_method_class.h +++ b/src/java_bytecode/java_bytecode_convert_method_class.h @@ -214,7 +214,8 @@ class java_bytecode_convert_methodt:public messaget codet convert_instructions( const methodt &, - const code_typet &); + const code_typet &, + const irep_idt &); const bytecode_infot &get_bytecode_info(const irep_idt &statement); diff --git a/src/java_bytecode/java_entry_point.cpp b/src/java_bytecode/java_entry_point.cpp index 0e7c0c14b51..8d7b479ff60 100644 --- a/src/java_bytecode/java_entry_point.cpp +++ b/src/java_bytecode/java_entry_point.cpp @@ -594,7 +594,7 @@ bool java_entry_point( // add the exceptional return value auxiliary_symbolt exc_symbol; exc_symbol.mode=ID_C; - exc_symbol.is_static_lifetime=false; + exc_symbol.is_static_lifetime=true; exc_symbol.name=id2string(symbol.name)+EXC_SUFFIX; exc_symbol.base_name=id2string(symbol.name)+EXC_SUFFIX; exc_symbol.type=typet(ID_pointer, empty_typet());