From 7a205f05643119b875a363c0190a5ff7a820e965 Mon Sep 17 00:00:00 2001 From: thk123 Date: Mon, 5 Feb 2018 17:20:34 +0000 Subject: [PATCH 1/3] Correct handling of two byte offsets TODO: test the 4 last offset fixes --- src/java_bytecode/java_bytecode_parser.cpp | 20 +++++++++++++++----- 1 file changed, 15 insertions(+), 5 deletions(-) diff --git a/src/java_bytecode/java_bytecode_parser.cpp b/src/java_bytecode/java_bytecode_parser.cpp index 0db26a5ec06..8b53f1bc781 100644 --- a/src/java_bytecode/java_bytecode_parser.cpp +++ b/src/java_bytecode/java_bytecode_parser.cpp @@ -756,8 +756,10 @@ void java_bytecode_parsert::rbytecode( case 'o': // two byte branch offset, signed { s2 offset=read_u2(); + // By converting the signed offset into an absolute address (by adding + // the current address) the number represented becomes unsigned. instruction.args.push_back( - from_integer(address+offset, signedbv_typet(16))); + from_integer(address+offset, unsignedbv_typet(16))); } address+=2; break; @@ -765,8 +767,10 @@ void java_bytecode_parsert::rbytecode( case 'O': // four byte branch offset, signed { s4 offset=read_u4(); + // By converting the signed offset into an absolute address (by adding + // the current address) the number represented becomes unsigned. instruction.args.push_back( - from_integer(address+offset, signedbv_typet(32))); + from_integer(address+offset, unsignedbv_typet(32))); } address+=4; break; @@ -820,8 +824,10 @@ void java_bytecode_parsert::rbytecode( // now default value s4 default_value=read_u4(); + // By converting the signed offset into an absolute address (by adding + // the current address) the number represented becomes unsigned. instruction.args.push_back( - from_integer(base_offset+default_value, signedbv_typet(32))); + from_integer(base_offset+default_value, unsignedbv_typet(32))); address+=4; // number of pairs @@ -834,8 +840,10 @@ void java_bytecode_parsert::rbytecode( s4 offset=read_u4(); instruction.args.push_back( from_integer(match, signedbv_typet(32))); + // By converting the signed offset into an absolute address (by adding + // the current address) the number represented becomes unsigned. instruction.args.push_back( - from_integer(base_offset+offset, signedbv_typet(32))); + from_integer(base_offset+offset, unsignedbv_typet(32))); address+=8; } } @@ -867,8 +875,10 @@ void java_bytecode_parsert::rbytecode( { s4 offset=read_u4(); instruction.args.push_back(from_integer(i, signedbv_typet(32))); + // By converting the signed offset into an absolute address (by adding + // the current address) the number represented becomes unsigned. instruction.args.push_back( - from_integer(base_offset+offset, signedbv_typet(32))); + from_integer(base_offset+offset, unsignedbv_typet(32))); address+=4; } } From 3f202fad69263a0963cc312bb408469f73a09ef7 Mon Sep 17 00:00:00 2001 From: thk123 Date: Thu, 8 Feb 2018 17:01:51 +0000 Subject: [PATCH 2/3] Add support for reading nop operations Previously this fell through to a naked codet("nop"). This would crash in the symex phase. This correctly converts it into an appropriate skip --- src/java_bytecode/java_bytecode_convert_method.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index ec771081f2f..c3bbd217a0b 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -2324,6 +2324,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); From dda54c7f35ed58104b02e10885bc6fc842e0e6c4 Mon Sep 17 00:00:00 2001 From: thk123 Date: Thu, 8 Feb 2018 17:08:53 +0000 Subject: [PATCH 3/3] Adding test includes a jump to address 2^16 --- .../cbmc-java/very-long-jumps/NopJumps.class | Bin 0 -> 32912 bytes .../cbmc-java/very-long-jumps/NopJumps.j | 32787 ++++++++++++++++ .../cbmc-java/very-long-jumps/test.desc | 4 + 3 files changed, 32791 insertions(+) create mode 100644 regression/cbmc-java/very-long-jumps/NopJumps.class create mode 100644 regression/cbmc-java/very-long-jumps/NopJumps.j create mode 100644 regression/cbmc-java/very-long-jumps/test.desc diff --git a/regression/cbmc-java/very-long-jumps/NopJumps.class b/regression/cbmc-java/very-long-jumps/NopJumps.class new file mode 100644 index 0000000000000000000000000000000000000000..2f35f515d44d58f742c14988dc75d4f845d10de6 GIT binary patch literal 32912 zcmeIuu}#BZ5C!1(CkBU9S%D4;$Ph>r6i^`1n_wZVfFqL7!Zz$c!2k>eI7n>qU2*TE zch&dx{qdP`PBJZ-b