From 11f337ad4193d371a2e5f951f81ba0db7c467a97 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Wed, 24 Aug 2016 10:11:52 +0100 Subject: [PATCH 1/4] Don't try to use named local variables out of scope, even if only one named local uses a particular slot. (Anonymous locals of different types might use the slot before or afterwards) --- .../java_bytecode_convert_method.cpp | 44 +++++++------------ 1 file changed, 16 insertions(+), 28 deletions(-) diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index 20a97d0f031..07858e57bab 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -100,34 +100,22 @@ class java_bytecode_convert_methodt:public messaget variablest &var_list, instruction_sizet inst_size) { size_t var_list_length = var_list.size(); - if(var_list_length > 1) - { - for(variablet &var : var_list) - { - size_t start_pc = var.start_pc; - size_t length = var.length; - if (address + (size_t) inst_size >= start_pc && address < start_pc + length) - return var; - } - // add unnamed local variable to end of list at this index - // with scope from 0 to INT_MAX - // as it is at the end of the vector, it will only be taken into account - // if no other variable is valid - size_t list_length = var_list.size(); - var_list.resize(list_length + 1); - var_list[list_length].start_pc = 0; - var_list[list_length].length = std::numeric_limits::max(); - return var_list[list_length]; - } - else if(var_list_length == 1) - return var_list[0]; - else - { - // return reference to unnamed local variable - // if no local variable is defined for this index - var_list.resize(1); - return var_list[0]; - } + for(variablet &var : var_list) + { + size_t start_pc = var.start_pc; + size_t length = var.length; + if (address + (size_t) inst_size >= start_pc && address < start_pc + length) + return var; + } + // add unnamed local variable to end of list at this index + // with scope from 0 to INT_MAX + // as it is at the end of the vector, it will only be taken into account + // if no other variable is valid + size_t list_length = var_list.size(); + var_list.resize(list_length + 1); + var_list[list_length].start_pc = 0; + var_list[list_length].length = std::numeric_limits::max(); + return var_list[list_length]; } // JVM local variables From 92a068f36a2fc65457816cc70b4d4f7ab8b7aad6 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Wed, 24 Aug 2016 15:49:18 +0100 Subject: [PATCH 2/4] Fix parameter live ranges --- src/java_bytecode/java_bytecode_convert_method.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index 07858e57bab..578ad3a7540 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -363,6 +363,8 @@ void java_bytecode_convert_methodt::convert( // add as a JVM variable std::size_t slots=get_variable_slots(parameters[i]); variables[param_index][0].symbol_expr=parameter_symbol.symbol_expr(); + variables[param_index][0].start_pc=0; + variables[param_index][0].length = std::numeric_limits::max(); param_index+=slots; } From addb642ad05c66dbf7c5b535810b622430ba3a19 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Wed, 24 Aug 2016 16:25:29 +0100 Subject: [PATCH 3/4] Add testcase for local variable table fixes --- .../LocalVarTable2/LocalVarTable2.class | Bin 0 -> 952 bytes .../LocalVarTable2/LocalVarTable2.java | 19 ++++++++++++++++++ regression/cbmc-java/LocalVarTable2/test.desc | 7 +++++++ 3 files changed, 26 insertions(+) create mode 100644 regression/cbmc-java/LocalVarTable2/LocalVarTable2.class create mode 100644 regression/cbmc-java/LocalVarTable2/LocalVarTable2.java create mode 100644 regression/cbmc-java/LocalVarTable2/test.desc diff --git a/regression/cbmc-java/LocalVarTable2/LocalVarTable2.class b/regression/cbmc-java/LocalVarTable2/LocalVarTable2.class new file mode 100644 index 0000000000000000000000000000000000000000..3191b63267e45e9d65d0ddb98d51bf476a1f2efc GIT binary patch literal 952 zcmZuwO>@#v6g`im1kynHD5z*HMXP~o(YES>jxIXW8Ah}^bm%y)9`K~8A?c){+PzDE zg&Vi(qIPuDy??`h;W+Ajffmp%^6q>0_q7!*n8T95T`X9I2BCMUZzq45=fGbN_EL2i(gY-i0nP3l1u1sF!KSS zl%jrt`b5bcVWNJB@YXA^w|{Q(1Xn1&b{6Lb%$CUptd9`g8jht0bQ7dR@&r?kmcx0% LW4J(T2s3{Hf>F&D literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/LocalVarTable2/LocalVarTable2.java b/regression/cbmc-java/LocalVarTable2/LocalVarTable2.java new file mode 100644 index 00000000000..9d32afe52a8 --- /dev/null +++ b/regression/cbmc-java/LocalVarTable2/LocalVarTable2.java @@ -0,0 +1,19 @@ +// Must compile this with -g (produces LocalVarTable) to exhibit bug. + +public class LocalVarTable2 { + + public static Object f() { + for(int i = 0; i < 10; ++i) { System.out.printf("Count %d\n", i); } + try { + return new Object(); + } + finally { + System.out.println("Finally executed\n"); + } + } + + public static void main(String[] args) { + f(); + } + +} diff --git a/regression/cbmc-java/LocalVarTable2/test.desc b/regression/cbmc-java/LocalVarTable2/test.desc new file mode 100644 index 00000000000..1e982eeac10 --- /dev/null +++ b/regression/cbmc-java/LocalVarTable2/test.desc @@ -0,0 +1,7 @@ +CORE +LocalVarTable2.class +--show-goto-functions +^EXIT=0$ +^SIGNAL=0$ +-- +return_value.*(void \*)i From bef5f77b78ad4d2563bd7d800d0704d03596edd4 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Wed, 24 Aug 2016 17:51:11 +0100 Subject: [PATCH 4/4] Cleanup unused var --- src/java_bytecode/java_bytecode_convert_method.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index 578ad3a7540..699c6556b80 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -99,7 +99,6 @@ class java_bytecode_convert_methodt:public messaget variablet &find_variable_for_slot(unsigned number_int, size_t address, variablest &var_list, instruction_sizet inst_size) { - size_t var_list_length = var_list.size(); for(variablet &var : var_list) { size_t start_pc = var.start_pc;