From 7eb318ef2bc6927f2194a1a596011305881afce9 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Tue, 24 Jan 2017 13:32:11 +0000 Subject: [PATCH 1/2] Discover lexical scopes for anonymous variables This enables tight variable scoping even when Java debug information is not available, which helps with analyses that benefit from DEAD instructions keeping their domains as small as possible. --- .../java_bytecode_convert_method.cpp | 130 ++++++++++++------ .../java_bytecode_convert_method_class.h | 2 +- 2 files changed, 90 insertions(+), 42 deletions(-) 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; From b3b268313a0344fe0c78a55d5e836c83b74327d4 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Tue, 24 Jan 2017 13:50:54 +0000 Subject: [PATCH 2/2] Add test for anonymous local scoping This creates three source-level variables that are notionally live for the whole function, but then uses the function's dominator tree information to show that they actually have disjoint scopes. Similarly the temporary used to hold a new instance between creation and assignment to a local variable should be given a bounded scope. --- .../cbmc-java/LocalVarTable5/test.class | Bin 0 -> 329 bytes regression/cbmc-java/LocalVarTable5/test.desc | 10 ++++++ regression/cbmc-java/LocalVarTable5/test.java | 29 ++++++++++++++++++ 3 files changed, 39 insertions(+) create mode 100644 regression/cbmc-java/LocalVarTable5/test.class create mode 100644 regression/cbmc-java/LocalVarTable5/test.desc create mode 100644 regression/cbmc-java/LocalVarTable5/test.java diff --git a/regression/cbmc-java/LocalVarTable5/test.class b/regression/cbmc-java/LocalVarTable5/test.class new file mode 100644 index 0000000000000000000000000000000000000000..b3a59b41f299dcc1935e2f7bdfc0e6c0619287d0 GIT binary patch literal 329 zcmXX=yGjF56r8hr#xmLnf}pX82$px(i`SaBRMzh7d)R)Fe!&<-ACu8-d68LCw$u|h%?ql-PnRQqt#B;ci_Sxx@|*gG)! literal 0 HcmV?d00001 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(); + } + } +}