diff --git a/regression/cbmc-java/LocalVarTable5/test.class b/regression/cbmc-java/LocalVarTable5/test.class new file mode 100644 index 00000000000..b3a59b41f29 Binary files /dev/null and b/regression/cbmc-java/LocalVarTable5/test.class differ diff --git a/regression/cbmc-java/LocalVarTable5/test.desc b/regression/cbmc-java/LocalVarTable5/test.desc new file mode 100644 index 00000000000..bfe77ab09ad --- /dev/null +++ b/regression/cbmc-java/LocalVarTable5/test.desc @@ -0,0 +1,10 @@ +CORE +test.class +--show-goto-functions +dead anonlocal::1i +dead anonlocal::2i +dead anonlocal::3a +dead new_tmp0 +^EXIT=0$ +^SIGNAL=0$ +-- diff --git a/regression/cbmc-java/LocalVarTable5/test.java b/regression/cbmc-java/LocalVarTable5/test.java new file mode 100644 index 00000000000..32f52af80e6 --- /dev/null +++ b/regression/cbmc-java/LocalVarTable5/test.java @@ -0,0 +1,29 @@ + + +public class test +{ + public static void main(int unknown) + { + int i; + int j; + if(unknown==1) + { + // Check that anonymous locals + // get assigned scopes: + i = 0; + i++; + } + else if(unknown==2) + { + j = 0; + j++; + } + else + { + // Check that temporaries (here + // a new_tmp variable) are treated + // likewise + test t = new test(); + } + } +} diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index 854d50ac9ba..8bf424d74c4 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -692,6 +692,43 @@ code_blockt &java_bytecode_convert_methodt::get_or_create_block_for_pcrange( to_code(this_block_children[child_offset])).code()); } +static void gather_symbol_live_ranges( + unsigned pc, + const exprt &e, + std::map &result) +{ + if(e.id()==ID_symbol) + { + const auto &symexpr=to_symbol_expr(e); + auto findit= + result.insert({ + symexpr.get_identifier(), + java_bytecode_convert_methodt::variablet()}); + auto &var=findit.first->second; + if(findit.second) + { + var.symbol_expr=symexpr; + var.start_pc=pc; + var.length=1; + } + else + { + if(pc1; } + // Find out where temporaries are used: + std::map temporary_variable_live_ranges; + for(const auto &aentry : address_map) + gather_symbol_live_ranges( + aentry.first, + aentry.second.code, + temporary_variable_live_ranges); + + std::vector vars_to_process; for(const auto &vlist : variables) - { for(const auto &v : vlist) - { - if(v.is_parameter) - continue; - // Merge lexical scopes as far as possible to allow us to - // declare these variable scopes faithfully. - // Don't insert yet, as for the time being the blocks' only - // operands must be other blocks. - // The declarations will be inserted in the next pass instead. - get_or_create_block_for_pcrange( - root, - root_block, - v.start_pc, - v.start_pc+v.length, - std::numeric_limits::max(), - address_map); - } + vars_to_process.push_back(&v); + + for(const auto &v : tmp_vars) + vars_to_process.push_back( + &temporary_variable_live_ranges.at(v.get_identifier())); + + for(const auto &v : used_local_names) + vars_to_process.push_back( + &temporary_variable_live_ranges.at(v.get_identifier())); + + for(const auto vp : vars_to_process) + { + const auto &v=*vp; + if(v.is_parameter) + continue; + // Merge lexical scopes as far as possible to allow us to + // declare these variable scopes faithfully. + // Don't insert yet, as for the time being the blocks' only + // operands must be other blocks. + // The declarations will be inserted in the next pass instead. + get_or_create_block_for_pcrange( + root, + root_block, + v.start_pc, + v.start_pc+v.length, + std::numeric_limits::max(), + address_map); } - for(const auto &vlist : variables) + for(const auto vp : vars_to_process) { - for(const auto &v : vlist) - { - if(v.is_parameter) - continue; - // Skip anonymous variables: - if(v.symbol_expr.get_identifier()==irep_idt()) - continue; - auto &block=get_block_for_pcrange( - root, - root_block, - v.start_pc, - v.start_pc+v.length, - std::numeric_limits::max()); - code_declt d(v.symbol_expr); - block.operands().insert(block.operands().begin(), d); - } + const auto &v=*vp; + if(v.is_parameter) + continue; + // Skip anonymous variables: + if(v.symbol_expr.get_identifier()==irep_idt()) + continue; + auto &block=get_block_for_pcrange( + root, + root_block, + v.start_pc, + v.start_pc+v.length, + std::numeric_limits::max()); + code_declt d(v.symbol_expr); + block.operands().insert(block.operands().begin(), d); } for(auto &block : root_block.operands()) diff --git a/src/java_bytecode/java_bytecode_convert_method_class.h b/src/java_bytecode/java_bytecode_convert_method_class.h index 003492355d1..b1358065f2c 100644 --- a/src/java_bytecode/java_bytecode_convert_method_class.h +++ b/src/java_bytecode/java_bytecode_convert_method_class.h @@ -63,7 +63,6 @@ class java_bytecode_convert_methodt:public messaget typedef std::vector local_variable_table_with_holest; -protected: class variablet { public: @@ -75,6 +74,7 @@ class java_bytecode_convert_methodt:public messaget variablet() : symbol_expr(), is_parameter(false) {} }; + protected: typedef std::vector variablest; expanding_vector variables; std::set used_local_names;