From e11163cb7c8722b105fd809b8cc636845c7c5e10 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Fri, 9 Mar 2018 17:35:47 +0100 Subject: [PATCH 01/19] Continue parsing after unsupported BootstrapMethods entry Before it was possible to keep some `BootstrapMethods` entries unparsed, after a currently unsupported was found. This lead to the situation that JBMC ended up with a wrong file offset which caused problems in the case of class file attributes being present after the `BootstrapMethods` attribute. This was not observed using the Oracle or OpenJDK compilers, but currently only on the Eclipse compiler for Java. --- src/java_bytecode/java_bytecode_parser.cpp | 121 +++++++++++---------- 1 file changed, 65 insertions(+), 56 deletions(-) diff --git a/src/java_bytecode/java_bytecode_parser.cpp b/src/java_bytecode/java_bytecode_parser.cpp index d4eb82002c0..60509302592 100644 --- a/src/java_bytecode/java_bytecode_parser.cpp +++ b/src/java_bytecode/java_bytecode_parser.cpp @@ -1803,7 +1803,7 @@ java_bytecode_parsert::parse_method_handle(const method_handle_infot &entry) void java_bytecode_parsert::read_bootstrapmethods_entry(classt &parsed_class) { u2 num_bootstrap_methods = read_u2(); - for(size_t i = 0; i < num_bootstrap_methods; i++) + for(size_t j = 0; j < num_bootstrap_methods; j++) { u2 bootstrap_methodhandle_ref = read_u2(); const pool_entryt &entry = pool_entry(bootstrap_methodhandle_ref); @@ -1868,72 +1868,81 @@ void java_bytecode_parsert::read_bootstrapmethods_entry(classt &parsed_class) lambda_method_handlet lambda_method_handle; lambda_method_handle.handle_type = method_handle_typet::UNKNOWN_HANDLE; lambda_method_handle.u2_values = std::move(u2_values); - parsed_class.lambda_method_handle_map[{parsed_class.name, i}] = + parsed_class.lambda_method_handle_map[{parsed_class.name, j}] = lambda_method_handle; - return; - } - const pool_entryt &interface_type_argument = pool_entry(argument_index1); - const pool_entryt &method_handle_argument = pool_entry(argument_index2); - const pool_entryt &method_type_argument = pool_entry(argument_index3); - - if( - !(interface_type_argument.tag == CONSTANT_MethodType && - method_handle_argument.tag == CONSTANT_MethodHandle && - method_type_argument.tag == CONSTANT_MethodType)) - { - lambda_method_handlet lambda_method_handle; - lambda_method_handle.handle_type = method_handle_typet::UNKNOWN_HANDLE; - lambda_method_handle.u2_values = std::move(u2_values); - parsed_class.lambda_method_handle_map[{parsed_class.name, i}] = - lambda_method_handle; - return; - } - - debug() << "INFO: parse lambda handle" << eom; - optionalt lambda_method_handle = - parse_method_handle(method_handle_infot{method_handle_argument}); - - if(!lambda_method_handle.has_value()) - { - lambda_method_handlet lambda_method_handle; - lambda_method_handle.handle_type = method_handle_typet::UNKNOWN_HANDLE; - lambda_method_handle.u2_values = std::move(u2_values); - parsed_class.lambda_method_handle_map[{parsed_class.name, i}] = - lambda_method_handle; - return; - } - else if( - lambda_method_handle->handle_type != - method_handle_typet::LAMBDA_METHOD_HANDLE) - { - lambda_method_handle->u2_values = std::move(u2_values); - error() << "ERROR: could not parse lambda function method handle" - << eom; } else { - lambda_method_handle->interface_type = - pool_entry(interface_type_argument.ref1).s; - lambda_method_handle->method_type = - pool_entry(method_type_argument.ref1).s; - lambda_method_handle->u2_values = std::move(u2_values); - debug() << "lambda function reference " - << id2string(lambda_method_handle->lambda_method_name) - << " in class \"" << parsed_class.name << "\"" - << "\n interface type is " - << id2string(pool_entry(interface_type_argument.ref1).s) - << "\n method type is " - << id2string(pool_entry(method_type_argument.ref1).s) << eom; + const pool_entryt &interface_type_argument = + pool_entry(argument_index1); + const pool_entryt &method_handle_argument = pool_entry(argument_index2); + const pool_entryt &method_type_argument = pool_entry(argument_index3); + + if( + !(interface_type_argument.tag == CONSTANT_MethodType && + method_handle_argument.tag == CONSTANT_MethodHandle && + method_type_argument.tag == CONSTANT_MethodType)) + { + lambda_method_handlet lambda_method_handle; + lambda_method_handle.handle_type = + method_handle_typet::UNKNOWN_HANDLE; + lambda_method_handle.u2_values = std::move(u2_values); + parsed_class.lambda_method_handle_map[{parsed_class.name, j}] = + lambda_method_handle; + } + else + { + debug() << "INFO: parse lambda handle" << eom; + optionalt lambda_method_handle = + parse_method_handle(method_handle_infot{method_handle_argument}); + + if(!lambda_method_handle.has_value()) + { + lambda_method_handlet lambda_method_handle; + lambda_method_handle.handle_type = + method_handle_typet::UNKNOWN_HANDLE; + lambda_method_handle.u2_values = std::move(u2_values); + parsed_class.lambda_method_handle_map[{parsed_class.name, j}] = + lambda_method_handle; + } + else + { + if( + lambda_method_handle->handle_type != + method_handle_typet::LAMBDA_METHOD_HANDLE) + { + lambda_method_handle->u2_values = std::move(u2_values); + error() << "ERROR: could not parse lambda function method handle" + << eom; + } + else + { + lambda_method_handle->interface_type = + pool_entry(interface_type_argument.ref1).s; + lambda_method_handle->method_type = + pool_entry(method_type_argument.ref1).s; + lambda_method_handle->u2_values = std::move(u2_values); + debug() << "lambda function reference " + << id2string(lambda_method_handle->lambda_method_name) + << " in class \"" << parsed_class.name << "\"" + << "\n interface type is " + << id2string(pool_entry(interface_type_argument.ref1).s) + << "\n method type is " + << id2string(pool_entry(method_type_argument.ref1).s) + << eom; + } + parsed_class.lambda_method_handle_map[{parsed_class.name, j}] = + *lambda_method_handle; + } + } } - parsed_class.lambda_method_handle_map[{parsed_class.name, i}] = - *lambda_method_handle; } else { lambda_method_handlet lambda_method_handle; lambda_method_handle.handle_type = method_handle_typet::UNKNOWN_HANDLE; lambda_method_handle.u2_values = std::move(u2_values); - parsed_class.lambda_method_handle_map[{parsed_class.name, i}] = + parsed_class.lambda_method_handle_map[{parsed_class.name, j}] = lambda_method_handle; error() << "ERROR: num_bootstrap_arguments must be at least 3" << eom; } From d7a4e50f0f5cd3bf414ff86a19408fb0deff2147 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Fri, 9 Mar 2018 18:05:52 +0100 Subject: [PATCH 02/19] Add regression test compiled with ecj --- .../cbmc-java/lambda2/StaticMethodRef.class | Bin 0 -> 1624 bytes .../cbmc-java/lambda2/StaticMethodRef.java | 25 ++++++++++++++++++ .../cbmc-java/lambda2/test_no_crash_ecj.desc | 9 +++++++ 3 files changed, 34 insertions(+) create mode 100644 regression/cbmc-java/lambda2/StaticMethodRef.class create mode 100644 regression/cbmc-java/lambda2/StaticMethodRef.java create mode 100644 regression/cbmc-java/lambda2/test_no_crash_ecj.desc diff --git a/regression/cbmc-java/lambda2/StaticMethodRef.class b/regression/cbmc-java/lambda2/StaticMethodRef.class new file mode 100644 index 0000000000000000000000000000000000000000..ae9332a81412ee265ed5196c3493dde605679ee9 GIT binary patch literal 1624 zcmbVLZBr6a6n-u*t^&$RsHypa`GTS%W@Tb!QYHo3gwuzG;vTb=SB61=T*Vr zHAKx=XBdhuX1e~;njwxwHR;0uWC=lr!5fbO3?jrJHMm+Ahb4yLXxhmKk;#>-4AH1V z04G2I!x$lEyi!rm7^XVR>V~4mOLeVaD7qHkYhRKfs?$&il!6HyXNWihb`=}Mg)u)S zF)d+=Vcg2i*}dsA!Z2?q->P=f&b_TN>vcbXSGf(s>?!6zgs+X- zs!4{1ZCBTgno;GI))3ZwG@OqlJY<;Zj)tN&^ivVf@N&M$$&i&_=eL?{lrFirQ>O*H7z}q%DV>QB|~KyXFe;=&U0C@39r~cC5YO?XW4XsyW3F z$zTs2$cWI&DV9&Ijg56nX-3a|m#*U0t6aC6W?_FD*HrjF12>y~` z%ORMpf}L1S@n!5Y1k#!&swtJ%YN93~!!UQF!A@>0SDc-mi3F@R2m10S`$(0wk}PdViq*{F;P z7zGZRxCd-`V#{(LIk>=t3*RvF1tFW_7Y5E_E1~)BYq0ZWJ&k%oQ8WAnmfS6L_=?Ih zGP${|G?pwWQ93?KBR~uXFoz(m(jZa@;gA>?Fa!f5h!aYN`w|-xCaqs=Y?i9EW_e3s loz7|cenS5(B(ZJXp5g^|ty>DOk;WUc@=+DuB1_&!{{f3Yns)#I literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/lambda2/StaticMethodRef.java b/regression/cbmc-java/lambda2/StaticMethodRef.java new file mode 100644 index 00000000000..e03173e3b72 --- /dev/null +++ b/regression/cbmc-java/lambda2/StaticMethodRef.java @@ -0,0 +1,25 @@ +import java.util.function.Function; +import java.util.function.BiFunction; + +public class StaticMethodRef{ + public Integer test2(){return 2;} + public Integer Smr(Integer ctr) { + Function func1 = Integer::valueOf; + + // Uses Integer.valueOf(String) + Function func2 = Integer::valueOf; + + BiFunction func3 = Integer::valueOf; + + if (ctr.equals(func1.apply(9))) + return func1.apply(9); + + if(ctr.equals(func2.apply("8"))) + return func2.apply("8"); + + if(ctr.equals(func3.apply("0111", 2))) + return func3.apply("0111", 2); + + return ctr; + } +} diff --git a/regression/cbmc-java/lambda2/test_no_crash_ecj.desc b/regression/cbmc-java/lambda2/test_no_crash_ecj.desc new file mode 100644 index 00000000000..4033a1aff4d --- /dev/null +++ b/regression/cbmc-java/lambda2/test_no_crash_ecj.desc @@ -0,0 +1,9 @@ +CORE +StaticMethodRef.class +--function StaticMethodRef.test2 +^EXIT=0 +^SIGNAL=0 +-- +-- +Tests that it doesn't crash when failing to read a `BootstrapMethods` entry and +there is another attribute after this. From 067ccbf3f374a1bd6173757c62b97c5a09164a12 Mon Sep 17 00:00:00 2001 From: thk123 Date: Mon, 12 Mar 2018 11:38:18 +0000 Subject: [PATCH 03/19] Rename j to boostrap_method_index --- src/java_bytecode/java_bytecode_parser.cpp | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/src/java_bytecode/java_bytecode_parser.cpp b/src/java_bytecode/java_bytecode_parser.cpp index 60509302592..f53e13d689b 100644 --- a/src/java_bytecode/java_bytecode_parser.cpp +++ b/src/java_bytecode/java_bytecode_parser.cpp @@ -1803,7 +1803,9 @@ java_bytecode_parsert::parse_method_handle(const method_handle_infot &entry) void java_bytecode_parsert::read_bootstrapmethods_entry(classt &parsed_class) { u2 num_bootstrap_methods = read_u2(); - for(size_t j = 0; j < num_bootstrap_methods; j++) + for(size_t bootstrap_method_index = 0; + bootstrap_method_index < num_bootstrap_methods; + ++bootstrap_method_index) { u2 bootstrap_methodhandle_ref = read_u2(); const pool_entryt &entry = pool_entry(bootstrap_methodhandle_ref); @@ -1868,7 +1870,7 @@ void java_bytecode_parsert::read_bootstrapmethods_entry(classt &parsed_class) lambda_method_handlet lambda_method_handle; lambda_method_handle.handle_type = method_handle_typet::UNKNOWN_HANDLE; lambda_method_handle.u2_values = std::move(u2_values); - parsed_class.lambda_method_handle_map[{parsed_class.name, j}] = + parsed_class.lambda_method_handle_map[{parsed_class.name, bootstrap_method_index}] = lambda_method_handle; } else @@ -1887,7 +1889,7 @@ void java_bytecode_parsert::read_bootstrapmethods_entry(classt &parsed_class) lambda_method_handle.handle_type = method_handle_typet::UNKNOWN_HANDLE; lambda_method_handle.u2_values = std::move(u2_values); - parsed_class.lambda_method_handle_map[{parsed_class.name, j}] = + parsed_class.lambda_method_handle_map[{parsed_class.name, bootstrap_method_index}] = lambda_method_handle; } else @@ -1902,7 +1904,7 @@ void java_bytecode_parsert::read_bootstrapmethods_entry(classt &parsed_class) lambda_method_handle.handle_type = method_handle_typet::UNKNOWN_HANDLE; lambda_method_handle.u2_values = std::move(u2_values); - parsed_class.lambda_method_handle_map[{parsed_class.name, j}] = + parsed_class.lambda_method_handle_map[{parsed_class.name, bootstrap_method_index}] = lambda_method_handle; } else @@ -1931,7 +1933,7 @@ void java_bytecode_parsert::read_bootstrapmethods_entry(classt &parsed_class) << id2string(pool_entry(method_type_argument.ref1).s) << eom; } - parsed_class.lambda_method_handle_map[{parsed_class.name, j}] = + parsed_class.lambda_method_handle_map[{parsed_class.name, bootstrap_method_index}] = *lambda_method_handle; } } @@ -1942,7 +1944,7 @@ void java_bytecode_parsert::read_bootstrapmethods_entry(classt &parsed_class) lambda_method_handlet lambda_method_handle; lambda_method_handle.handle_type = method_handle_typet::UNKNOWN_HANDLE; lambda_method_handle.u2_values = std::move(u2_values); - parsed_class.lambda_method_handle_map[{parsed_class.name, j}] = + parsed_class.lambda_method_handle_map[{parsed_class.name, bootstrap_method_index}] = lambda_method_handle; error() << "ERROR: num_bootstrap_arguments must be at least 3" << eom; } From 64002947865d59aebb703bf6fac6dbff254fad1a Mon Sep 17 00:00:00 2001 From: thk123 Date: Mon, 12 Mar 2018 11:39:11 +0000 Subject: [PATCH 04/19] Replace nested else ifs with a continue on error conditions --- src/java_bytecode/java_bytecode_parser.cpp | 230 ++++++++++----------- 1 file changed, 113 insertions(+), 117 deletions(-) diff --git a/src/java_bytecode/java_bytecode_parser.cpp b/src/java_bytecode/java_bytecode_parser.cpp index f53e13d689b..8cd1b71834b 100644 --- a/src/java_bytecode/java_bytecode_parser.cpp +++ b/src/java_bytecode/java_bytecode_parser.cpp @@ -1822,131 +1822,127 @@ void java_bytecode_parsert::read_bootstrapmethods_entry(classt &parsed_class) u2_values[i] = read_u2(); // try parsing bootstrap method handle - if(num_bootstrap_arguments >= 3) + if(num_bootstrap_arguments < 3) { - // each entry contains a MethodHandle structure - // u2 tag - // u2 reference kind which must be in the range from 1 to 9 - // u2 reference index into the constant pool - // - // reference kinds use the following - // 1 to 4 must point to a CONSTANT_Fieldref structure - // 5 or 8 must point to a CONSTANT_Methodref structure - // 6 or 7 must point to a CONSTANT_Methodref or - // CONSTANT_InterfaceMethodref structure, if the class file version - // number is 52.0 or above, to a CONSTANT_Methodref only in the case - // of less than 52.0 - // 9 must point to a CONSTANT_InterfaceMethodref structure - - // the index must point to a CONSTANT_String - // CONSTANT_Class - // CONSTANT_Integer - // CONSTANT_Long - // CONSTANT_Float - // CONSTANT_Double - // CONSTANT_MethodHandle - // CONSTANT_MethodType - - // We read the three arguments here to see whether they correspond to - // our hypotheses for this being a lambda function entry. - - u2 argument_index1 = u2_values[0]; - u2 argument_index2 = u2_values[1]; - u2 argument_index3 = u2_values[2]; - - // The additional arguments for the altmetafactory call are skipped, - // as they are currently not used. We verify though that they are of - // CONSTANT_Integer type, cases where this does not hold will be - // analyzed further. - bool recognized = true; - for(size_t i = 3; i < num_bootstrap_arguments; i++) - { - u2 skipped_argument = u2_values[i]; - recognized &= pool_entry(skipped_argument).tag == CONSTANT_Integer; - } - if(!recognized) - { - debug() << "format of BootstrapMethods entry not recognized" << eom; - lambda_method_handlet lambda_method_handle; - lambda_method_handle.handle_type = method_handle_typet::UNKNOWN_HANDLE; - lambda_method_handle.u2_values = std::move(u2_values); - parsed_class.lambda_method_handle_map[{parsed_class.name, bootstrap_method_index}] = - lambda_method_handle; - } - else - { - const pool_entryt &interface_type_argument = - pool_entry(argument_index1); - const pool_entryt &method_handle_argument = pool_entry(argument_index2); - const pool_entryt &method_type_argument = pool_entry(argument_index3); - - if( - !(interface_type_argument.tag == CONSTANT_MethodType && - method_handle_argument.tag == CONSTANT_MethodHandle && - method_type_argument.tag == CONSTANT_MethodType)) - { - lambda_method_handlet lambda_method_handle; - lambda_method_handle.handle_type = - method_handle_typet::UNKNOWN_HANDLE; - lambda_method_handle.u2_values = std::move(u2_values); - parsed_class.lambda_method_handle_map[{parsed_class.name, bootstrap_method_index}] = - lambda_method_handle; - } - else - { - debug() << "INFO: parse lambda handle" << eom; - optionalt lambda_method_handle = - parse_method_handle(method_handle_infot{method_handle_argument}); - - if(!lambda_method_handle.has_value()) - { - lambda_method_handlet lambda_method_handle; - lambda_method_handle.handle_type = - method_handle_typet::UNKNOWN_HANDLE; - lambda_method_handle.u2_values = std::move(u2_values); - parsed_class.lambda_method_handle_map[{parsed_class.name, bootstrap_method_index}] = - lambda_method_handle; - } - else - { - if( - lambda_method_handle->handle_type != - method_handle_typet::LAMBDA_METHOD_HANDLE) - { - lambda_method_handle->u2_values = std::move(u2_values); - error() << "ERROR: could not parse lambda function method handle" - << eom; - } - else - { - lambda_method_handle->interface_type = - pool_entry(interface_type_argument.ref1).s; - lambda_method_handle->method_type = - pool_entry(method_type_argument.ref1).s; - lambda_method_handle->u2_values = std::move(u2_values); - debug() << "lambda function reference " - << id2string(lambda_method_handle->lambda_method_name) - << " in class \"" << parsed_class.name << "\"" - << "\n interface type is " - << id2string(pool_entry(interface_type_argument.ref1).s) - << "\n method type is " - << id2string(pool_entry(method_type_argument.ref1).s) - << eom; - } - parsed_class.lambda_method_handle_map[{parsed_class.name, bootstrap_method_index}] = - *lambda_method_handle; - } - } - } + lambda_method_handlet lambda_method_handle; + lambda_method_handle.handle_type = method_handle_typet::UNKNOWN_HANDLE; + lambda_method_handle.u2_values = std::move(u2_values); + parsed_class.lambda_method_handle_map[{parsed_class.name, + bootstrap_method_index}] = + lambda_method_handle; + error() << "ERROR: num_bootstrap_arguments must be at least 3" << eom; + continue; } - else + // each entry contains a MethodHandle structure + // u2 tag + // u2 reference kind which must be in the range from 1 to 9 + // u2 reference index into the constant pool + // + // reference kinds use the following + // 1 to 4 must point to a CONSTANT_Fieldref structure + // 5 or 8 must point to a CONSTANT_Methodref structure + // 6 or 7 must point to a CONSTANT_Methodref or + // CONSTANT_InterfaceMethodref structure, if the class file version + // number is 52.0 or above, to a CONSTANT_Methodref only in the case + // of less than 52.0 + // 9 must point to a CONSTANT_InterfaceMethodref structure + + // the index must point to a CONSTANT_String + // CONSTANT_Class + // CONSTANT_Integer + // CONSTANT_Long + // CONSTANT_Float + // CONSTANT_Double + // CONSTANT_MethodHandle + // CONSTANT_MethodType + + // We read the three arguments here to see whether they correspond to + // our hypotheses for this being a lambda function entry. + + u2 argument_index1 = u2_values[0]; + u2 argument_index2 = u2_values[1]; + u2 argument_index3 = u2_values[2]; + + // The additional arguments for the altmetafactory call are skipped, + // as they are currently not used. We verify though that they are of + // CONSTANT_Integer type, cases where this does not hold will be + // analyzed further. + bool recognized = true; + for(size_t i = 3; i < num_bootstrap_arguments; i++) + { + u2 skipped_argument = u2_values[i]; + recognized &= pool_entry(skipped_argument).tag == CONSTANT_Integer; + } + if(!recognized) { + debug() << "format of BootstrapMethods entry not recognized" << eom; lambda_method_handlet lambda_method_handle; lambda_method_handle.handle_type = method_handle_typet::UNKNOWN_HANDLE; lambda_method_handle.u2_values = std::move(u2_values); parsed_class.lambda_method_handle_map[{parsed_class.name, bootstrap_method_index}] = lambda_method_handle; - error() << "ERROR: num_bootstrap_arguments must be at least 3" << eom; + continue; + } + + const pool_entryt &interface_type_argument = + pool_entry(argument_index1); + const pool_entryt &method_handle_argument = pool_entry(argument_index2); + const pool_entryt &method_type_argument = pool_entry(argument_index3); + + if( + !(interface_type_argument.tag == CONSTANT_MethodType && + method_handle_argument.tag == CONSTANT_MethodHandle && + method_type_argument.tag == CONSTANT_MethodType)) + { + lambda_method_handlet lambda_method_handle; + lambda_method_handle.handle_type = + method_handle_typet::UNKNOWN_HANDLE; + lambda_method_handle.u2_values = std::move(u2_values); + parsed_class.lambda_method_handle_map[{parsed_class.name, bootstrap_method_index}] = + lambda_method_handle; + continue; + } + + debug() << "INFO: parse lambda handle" << eom; + optionalt lambda_method_handle = + parse_method_handle(method_handle_infot{method_handle_argument}); + + if(!lambda_method_handle.has_value()) + { + lambda_method_handlet lambda_method_handle; + lambda_method_handle.handle_type = + method_handle_typet::UNKNOWN_HANDLE; + lambda_method_handle.u2_values = std::move(u2_values); + parsed_class.lambda_method_handle_map[{parsed_class.name, bootstrap_method_index}] = + lambda_method_handle; + continue; + } + + if( + lambda_method_handle->handle_type != + method_handle_typet::LAMBDA_METHOD_HANDLE) + { + lambda_method_handle->u2_values = std::move(u2_values); + error() << "ERROR: could not parse lambda function method handle" + << eom; + continue; } + + lambda_method_handle->interface_type = + pool_entry(interface_type_argument.ref1).s; + lambda_method_handle->method_type = + pool_entry(method_type_argument.ref1).s; + lambda_method_handle->u2_values = std::move(u2_values); + debug() << "lambda function reference " + << id2string(lambda_method_handle->lambda_method_name) + << " in class \"" << parsed_class.name << "\"" + << "\n interface type is " + << id2string(pool_entry(interface_type_argument.ref1).s) + << "\n method type is " + << id2string(pool_entry(method_type_argument.ref1).s) + << eom; + parsed_class.lambda_method_handle_map[{parsed_class.name, bootstrap_method_index}] = + *lambda_method_handle; + } } From 9749d5ac33eccf07cbb9aff1df855f88ec202b54 Mon Sep 17 00:00:00 2001 From: thk123 Date: Mon, 12 Mar 2018 11:50:37 +0000 Subject: [PATCH 05/19] Refactored error reporting method into a seperate function --- src/java_bytecode/java_bytecode_parse_tree.h | 9 ++++ src/java_bytecode/java_bytecode_parser.cpp | 54 +++++++++++--------- 2 files changed, 40 insertions(+), 23 deletions(-) diff --git a/src/java_bytecode/java_bytecode_parse_tree.h b/src/java_bytecode/java_bytecode_parse_tree.h index b4593f58d2e..c055b615284 100644 --- a/src/java_bytecode/java_bytecode_parse_tree.h +++ b/src/java_bytecode/java_bytecode_parse_tree.h @@ -194,6 +194,15 @@ class java_bytecode_parse_treet lambda_method_handlet() : handle_type(method_handle_typet::UNKNOWN_HANDLE) { } + + static lambda_method_handlet + create_unknown_handle(const u2_valuest params) + { + lambda_method_handlet lambda_method_handle; + lambda_method_handle.handle_type = method_handle_typet::UNKNOWN_HANDLE; + lambda_method_handle.u2_values = std::move(params); + return lambda_method_handle; + } }; typedef std::map, lambda_method_handlet> diff --git a/src/java_bytecode/java_bytecode_parser.cpp b/src/java_bytecode/java_bytecode_parser.cpp index 8cd1b71834b..3f87318154b 100644 --- a/src/java_bytecode/java_bytecode_parser.cpp +++ b/src/java_bytecode/java_bytecode_parser.cpp @@ -186,6 +186,11 @@ class java_bytecode_parsert:public parsert { return read_bytes(8); } + + void store_unknown_method_handle( + classt &parsed_class, + size_t bootstrap_method_index, + u2_valuest u2_values) const; }; #define CONSTANT_Class 7 @@ -1824,12 +1829,8 @@ void java_bytecode_parsert::read_bootstrapmethods_entry(classt &parsed_class) // try parsing bootstrap method handle if(num_bootstrap_arguments < 3) { - lambda_method_handlet lambda_method_handle; - lambda_method_handle.handle_type = method_handle_typet::UNKNOWN_HANDLE; - lambda_method_handle.u2_values = std::move(u2_values); - parsed_class.lambda_method_handle_map[{parsed_class.name, - bootstrap_method_index}] = - lambda_method_handle; + store_unknown_method_handle( + parsed_class, bootstrap_method_index, std::move(u2_values)); error() << "ERROR: num_bootstrap_arguments must be at least 3" << eom; continue; } @@ -1876,11 +1877,8 @@ void java_bytecode_parsert::read_bootstrapmethods_entry(classt &parsed_class) if(!recognized) { debug() << "format of BootstrapMethods entry not recognized" << eom; - lambda_method_handlet lambda_method_handle; - lambda_method_handle.handle_type = method_handle_typet::UNKNOWN_HANDLE; - lambda_method_handle.u2_values = std::move(u2_values); - parsed_class.lambda_method_handle_map[{parsed_class.name, bootstrap_method_index}] = - lambda_method_handle; + store_unknown_method_handle( + parsed_class, bootstrap_method_index, std::move(u2_values)); continue; } @@ -1894,12 +1892,9 @@ void java_bytecode_parsert::read_bootstrapmethods_entry(classt &parsed_class) method_handle_argument.tag == CONSTANT_MethodHandle && method_type_argument.tag == CONSTANT_MethodType)) { - lambda_method_handlet lambda_method_handle; - lambda_method_handle.handle_type = - method_handle_typet::UNKNOWN_HANDLE; - lambda_method_handle.u2_values = std::move(u2_values); - parsed_class.lambda_method_handle_map[{parsed_class.name, bootstrap_method_index}] = - lambda_method_handle; + debug() << "format of BootstrapMethods entry not recognized" << eom; + store_unknown_method_handle( + parsed_class, bootstrap_method_index, std::move(u2_values)); continue; } @@ -1909,12 +1904,9 @@ void java_bytecode_parsert::read_bootstrapmethods_entry(classt &parsed_class) if(!lambda_method_handle.has_value()) { - lambda_method_handlet lambda_method_handle; - lambda_method_handle.handle_type = - method_handle_typet::UNKNOWN_HANDLE; - lambda_method_handle.u2_values = std::move(u2_values); - parsed_class.lambda_method_handle_map[{parsed_class.name, bootstrap_method_index}] = - lambda_method_handle; + debug() << "format of BootstrapMethods entry not recognized" << eom; + store_unknown_method_handle( + parsed_class, bootstrap_method_index, std::move(u2_values)); continue; } @@ -1946,3 +1938,19 @@ void java_bytecode_parsert::read_bootstrapmethods_entry(classt &parsed_class) } } + +/// Creates an unknown method handle and puts it into the parsed_class +/// \param parsed_class: The class whose bootstrap method handles we are using +/// \param bootstrap_method_index: The current index in the boostrap entry table +/// \param u2_values: The indices of the arguments for the call +void java_bytecode_parsert::store_unknown_method_handle( + java_bytecode_parsert::classt &parsed_class, + size_t bootstrap_method_index, + java_bytecode_parsert::u2_valuest u2_values) const +{ + const lambda_method_handlet lambda_method_handle = + lambda_method_handlet::create_unknown_handle(move(u2_values)); + parsed_class + .lambda_method_handle_map[{parsed_class.name, bootstrap_method_index}] = + lambda_method_handle; +} From 4bb98f06fd08cf3d81a2e11dea3e9975172f09a5 Mon Sep 17 00:00:00 2001 From: thk123 Date: Mon, 12 Mar 2018 12:12:48 +0000 Subject: [PATCH 06/19] Removed impossible condition Either an optional was returned or a correct lamdba so no need to handle the third case. Added an invariant to catch the case this changes. --- src/java_bytecode/java_bytecode_parser.cpp | 11 +++-------- 1 file changed, 3 insertions(+), 8 deletions(-) diff --git a/src/java_bytecode/java_bytecode_parser.cpp b/src/java_bytecode/java_bytecode_parser.cpp index 3f87318154b..633da4f3edf 100644 --- a/src/java_bytecode/java_bytecode_parser.cpp +++ b/src/java_bytecode/java_bytecode_parser.cpp @@ -1910,15 +1910,10 @@ void java_bytecode_parsert::read_bootstrapmethods_entry(classt &parsed_class) continue; } - if( + // If parse_method_handle can't parse the lambda method, it should return {} + POSTCONDITION( lambda_method_handle->handle_type != - method_handle_typet::LAMBDA_METHOD_HANDLE) - { - lambda_method_handle->u2_values = std::move(u2_values); - error() << "ERROR: could not parse lambda function method handle" - << eom; - continue; - } + method_handle_typet::LAMBDA_METHOD_HANDLE); lambda_method_handle->interface_type = pool_entry(interface_type_argument.ref1).s; From c1aa16cd33f511d9e59a932cdaed922480be54dc Mon Sep 17 00:00:00 2001 From: thk123 Date: Mon, 12 Mar 2018 12:13:36 +0000 Subject: [PATCH 07/19] Renamed parameter variables --- src/java_bytecode/java_bytecode_parser.cpp | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/java_bytecode/java_bytecode_parser.cpp b/src/java_bytecode/java_bytecode_parser.cpp index 633da4f3edf..c1c742a61ac 100644 --- a/src/java_bytecode/java_bytecode_parser.cpp +++ b/src/java_bytecode/java_bytecode_parser.cpp @@ -1860,9 +1860,9 @@ void java_bytecode_parsert::read_bootstrapmethods_entry(classt &parsed_class) // We read the three arguments here to see whether they correspond to // our hypotheses for this being a lambda function entry. - u2 argument_index1 = u2_values[0]; - u2 argument_index2 = u2_values[1]; - u2 argument_index3 = u2_values[2]; + u2 interface_type_index = u2_values[0]; + u2 method_handle_index = u2_values[1]; + u2 method_type_index = u2_values[2]; // The additional arguments for the altmetafactory call are skipped, // as they are currently not used. We verify though that they are of @@ -1883,9 +1883,9 @@ void java_bytecode_parsert::read_bootstrapmethods_entry(classt &parsed_class) } const pool_entryt &interface_type_argument = - pool_entry(argument_index1); - const pool_entryt &method_handle_argument = pool_entry(argument_index2); - const pool_entryt &method_type_argument = pool_entry(argument_index3); + pool_entry(interface_type_index); + const pool_entryt &method_handle_argument = pool_entry(method_handle_index); + const pool_entryt &method_type_argument = pool_entry(method_type_index); if( !(interface_type_argument.tag == CONSTANT_MethodType && From 1db68a505f72de746b9a387a354197550d1c1db5 Mon Sep 17 00:00:00 2001 From: thk123 Date: Mon, 12 Mar 2018 12:14:15 +0000 Subject: [PATCH 08/19] Moved the first condition to after the explanation of our assumptions Here it is clearer why we need at least 3 arguments. Also documented this explictly above the condition. Also changed to a debug as there is nothing in the java spec requiring entries to have at least 3 parameters, it is simpyl our assumption about what entries can appear in the bootstrap methods table --- src/java_bytecode/java_bytecode_parser.cpp | 20 +++++++++++++------- 1 file changed, 13 insertions(+), 7 deletions(-) diff --git a/src/java_bytecode/java_bytecode_parser.cpp b/src/java_bytecode/java_bytecode_parser.cpp index c1c742a61ac..ceb52c38716 100644 --- a/src/java_bytecode/java_bytecode_parser.cpp +++ b/src/java_bytecode/java_bytecode_parser.cpp @@ -1827,13 +1827,6 @@ void java_bytecode_parsert::read_bootstrapmethods_entry(classt &parsed_class) u2_values[i] = read_u2(); // try parsing bootstrap method handle - if(num_bootstrap_arguments < 3) - { - store_unknown_method_handle( - parsed_class, bootstrap_method_index, std::move(u2_values)); - error() << "ERROR: num_bootstrap_arguments must be at least 3" << eom; - continue; - } // each entry contains a MethodHandle structure // u2 tag // u2 reference kind which must be in the range from 1 to 9 @@ -1860,6 +1853,19 @@ void java_bytecode_parsert::read_bootstrapmethods_entry(classt &parsed_class) // We read the three arguments here to see whether they correspond to // our hypotheses for this being a lambda function entry. + // Need at least 3 arguments, the interface type, the method hanlde + // and the method_type, otherwise it doesn't look like a call that we + // understand + if(num_bootstrap_arguments < 3) + { + store_unknown_method_handle( + parsed_class, bootstrap_method_index, std::move(u2_values)); + debug() + << "format of BootstrapMethods entry not recognized: too few arguments" + << eom; + continue; + } + u2 interface_type_index = u2_values[0]; u2 method_handle_index = u2_values[1]; u2 method_type_index = u2_values[2]; From 12f049e1f605094e8c6639b6453428fb3ad2eb62 Mon Sep 17 00:00:00 2001 From: thk123 Date: Mon, 12 Mar 2018 12:15:51 +0000 Subject: [PATCH 09/19] Added extra information to the warnings to differentaite the different cases --- src/java_bytecode/java_bytecode_parser.cpp | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/src/java_bytecode/java_bytecode_parser.cpp b/src/java_bytecode/java_bytecode_parser.cpp index ceb52c38716..b153893b144 100644 --- a/src/java_bytecode/java_bytecode_parser.cpp +++ b/src/java_bytecode/java_bytecode_parser.cpp @@ -1880,9 +1880,12 @@ void java_bytecode_parsert::read_bootstrapmethods_entry(classt &parsed_class) u2 skipped_argument = u2_values[i]; recognized &= pool_entry(skipped_argument).tag == CONSTANT_Integer; } + if(!recognized) { - debug() << "format of BootstrapMethods entry not recognized" << eom; + debug() << "format of BootstrapMethods entry not recognized: extra " + "arguments of wrong type" + << eom; store_unknown_method_handle( parsed_class, bootstrap_method_index, std::move(u2_values)); continue; @@ -1898,7 +1901,9 @@ void java_bytecode_parsert::read_bootstrapmethods_entry(classt &parsed_class) method_handle_argument.tag == CONSTANT_MethodHandle && method_type_argument.tag == CONSTANT_MethodType)) { - debug() << "format of BootstrapMethods entry not recognized" << eom; + debug() << "format of BootstrapMethods entry not recognized: arguments " + "wrong type" + << eom; store_unknown_method_handle( parsed_class, bootstrap_method_index, std::move(u2_values)); continue; @@ -1910,7 +1915,9 @@ void java_bytecode_parsert::read_bootstrapmethods_entry(classt &parsed_class) if(!lambda_method_handle.has_value()) { - debug() << "format of BootstrapMethods entry not recognized" << eom; + debug() << "format of BootstrapMethods entry not recognized: method " + "handle not recognised" + << eom; store_unknown_method_handle( parsed_class, bootstrap_method_index, std::move(u2_values)); continue; @@ -1936,7 +1943,6 @@ void java_bytecode_parsert::read_bootstrapmethods_entry(classt &parsed_class) << eom; parsed_class.lambda_method_handle_map[{parsed_class.name, bootstrap_method_index}] = *lambda_method_handle; - } } From a604b26e29efae4977412ee19f48ec49321b0c98 Mon Sep 17 00:00:00 2001 From: thk123 Date: Mon, 12 Mar 2018 12:44:16 +0000 Subject: [PATCH 10/19] !fixup Removed impossible condition (9fc5bfdc) --- src/java_bytecode/java_bytecode_parser.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/java_bytecode/java_bytecode_parser.cpp b/src/java_bytecode/java_bytecode_parser.cpp index b153893b144..111d772013c 100644 --- a/src/java_bytecode/java_bytecode_parser.cpp +++ b/src/java_bytecode/java_bytecode_parser.cpp @@ -1926,7 +1926,7 @@ void java_bytecode_parsert::read_bootstrapmethods_entry(classt &parsed_class) // If parse_method_handle can't parse the lambda method, it should return {} POSTCONDITION( lambda_method_handle->handle_type != - method_handle_typet::LAMBDA_METHOD_HANDLE); + method_handle_typet::UNKNOWN_HANDLE); lambda_method_handle->interface_type = pool_entry(interface_type_argument.ref1).s; From 861550002e1e595369f543f86549dc573c54ac73 Mon Sep 17 00:00:00 2001 From: thk123 Date: Mon, 12 Mar 2018 13:39:47 +0000 Subject: [PATCH 11/19] Added to readme that the file is compiled using the eclipse compiler --- regression/cbmc-java/lambda2/readme.txt | 2 ++ 1 file changed, 2 insertions(+) diff --git a/regression/cbmc-java/lambda2/readme.txt b/regression/cbmc-java/lambda2/readme.txt index 38647bdebb1..c9a632a07b1 100644 --- a/regression/cbmc-java/lambda2/readme.txt +++ b/regression/cbmc-java/lambda2/readme.txt @@ -1 +1,3 @@ from https://github.com/symphonyoss/symphony-java-client/ + +The StaticMethodRef.class is compiled using the Eclipse Compiler From f494674aa6b2dec9b6748609dc355152fb15a24f Mon Sep 17 00:00:00 2001 From: thk123 Date: Mon, 12 Mar 2018 13:40:00 +0000 Subject: [PATCH 12/19] Use function that actually contains the lambdas --- regression/cbmc-java/lambda2/test_no_crash_ecj.desc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/regression/cbmc-java/lambda2/test_no_crash_ecj.desc b/regression/cbmc-java/lambda2/test_no_crash_ecj.desc index 4033a1aff4d..266c19bea58 100644 --- a/regression/cbmc-java/lambda2/test_no_crash_ecj.desc +++ b/regression/cbmc-java/lambda2/test_no_crash_ecj.desc @@ -1,6 +1,6 @@ CORE StaticMethodRef.class ---function StaticMethodRef.test2 +--function StaticMethodRef.Smr ^EXIT=0 ^SIGNAL=0 -- From c0f054a82ac3b3b1b3e81f5f75d15ff17a59f3df Mon Sep 17 00:00:00 2001 From: thk123 Date: Mon, 12 Mar 2018 14:06:39 +0000 Subject: [PATCH 13/19] Removing redundant method from test --- .../cbmc-java/lambda2/StaticMethodRef.class | Bin 1624 -> 1549 bytes .../cbmc-java/lambda2/StaticMethodRef.java | 1 - 2 files changed, 1 deletion(-) diff --git a/regression/cbmc-java/lambda2/StaticMethodRef.class b/regression/cbmc-java/lambda2/StaticMethodRef.class index ae9332a81412ee265ed5196c3493dde605679ee9..9e65a471da3963700e2f27007a3cb52799b22554 100644 GIT binary patch delta 543 zcmY+ByKWOf6o$Xq9ed;5b-dXmo7j#MgX7$MAqxf^1G$+50wj3^gitz^0wdZqw1BLs zcmsqeQXz1GphE~G3JOXdfM`i8vdH!zK9ni$dpZMbsrWb^=Y z^5DU{haQZP9*jq0`~W5<#mQG=CXcn%$iqN)9;L*V=ErnSRX?k2|905T=X4zUQkI_&?muJR?4>9Eqr#v-oDqtf53MaC9b6g1(u^E2 z`SLhbd>)GACydZ0NlCIi%yTL>>2MatXE0d`tCd$-7LXC*s;qT3xE7-8+~ih>s@!9n O2NLB-A9mQ2@~Pjp$zVMI diff --git a/regression/cbmc-java/lambda2/StaticMethodRef.java b/regression/cbmc-java/lambda2/StaticMethodRef.java index e03173e3b72..c6eb4110676 100644 --- a/regression/cbmc-java/lambda2/StaticMethodRef.java +++ b/regression/cbmc-java/lambda2/StaticMethodRef.java @@ -2,7 +2,6 @@ import java.util.function.BiFunction; public class StaticMethodRef{ - public Integer test2(){return 2;} public Integer Smr(Integer ctr) { Function func1 = Integer::valueOf; From d8edf4f9466cd1a105401b60618b84844bc7ea7f Mon Sep 17 00:00:00 2001 From: thk123 Date: Mon, 12 Mar 2018 14:56:38 +0000 Subject: [PATCH 14/19] Adjusted test to pass We expect verification failure as currently we don't support lambdas so there are lots of NPEs in the test code --- regression/cbmc-java/lambda2/test_no_crash_ecj.desc | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/regression/cbmc-java/lambda2/test_no_crash_ecj.desc b/regression/cbmc-java/lambda2/test_no_crash_ecj.desc index 266c19bea58..a33445a8b6b 100644 --- a/regression/cbmc-java/lambda2/test_no_crash_ecj.desc +++ b/regression/cbmc-java/lambda2/test_no_crash_ecj.desc @@ -1,7 +1,9 @@ CORE StaticMethodRef.class --function StaticMethodRef.Smr -^EXIT=0 +VERIFICATION FAILED +EXIT=10 +SIGNAL=0 ^SIGNAL=0 -- -- From dcd680f61b97ac3e805076b040ca663c54515434 Mon Sep 17 00:00:00 2001 From: thk123 Date: Mon, 12 Mar 2018 16:31:41 +0000 Subject: [PATCH 15/19] Correcting formating on java file --- .../cbmc-java/lambda2/StaticMethodRef.java | 24 +++++++++---------- 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/regression/cbmc-java/lambda2/StaticMethodRef.java b/regression/cbmc-java/lambda2/StaticMethodRef.java index c6eb4110676..1254c60ffb7 100644 --- a/regression/cbmc-java/lambda2/StaticMethodRef.java +++ b/regression/cbmc-java/lambda2/StaticMethodRef.java @@ -3,22 +3,22 @@ public class StaticMethodRef{ public Integer Smr(Integer ctr) { - Function func1 = Integer::valueOf; + Function func1 = Integer::valueOf; - // Uses Integer.valueOf(String) - Function func2 = Integer::valueOf; + // Uses Integer.valueOf(String) + Function func2 = Integer::valueOf; - BiFunction func3 = Integer::valueOf; + BiFunction func3 = Integer::valueOf; - if (ctr.equals(func1.apply(9))) - return func1.apply(9); + if (ctr.equals(func1.apply(9))) + return func1.apply(9); - if(ctr.equals(func2.apply("8"))) - return func2.apply("8"); + if (ctr.equals(func2.apply("8"))) + return func2.apply("8"); - if(ctr.equals(func3.apply("0111", 2))) - return func3.apply("0111", 2); + if (ctr.equals(func3.apply("0111", 2))) + return func3.apply("0111", 2); - return ctr; - } + return ctr; +} } From 42065ecc67ba25cc83fa417e50d3ecb865278722 Mon Sep 17 00:00:00 2001 From: thk123 Date: Mon, 12 Mar 2018 16:31:51 +0000 Subject: [PATCH 16/19] Adjust the interface of the bootstrap methods map Added a todo to make private (needs adjustments to the test) --- src/java_bytecode/java_bytecode_parse_tree.h | 14 ++++++++++++++ src/java_bytecode/java_bytecode_parser.cpp | 13 +++++-------- 2 files changed, 19 insertions(+), 8 deletions(-) diff --git a/src/java_bytecode/java_bytecode_parse_tree.h b/src/java_bytecode/java_bytecode_parse_tree.h index c055b615284..6f47f9e0dea 100644 --- a/src/java_bytecode/java_bytecode_parse_tree.h +++ b/src/java_bytecode/java_bytecode_parse_tree.h @@ -205,6 +205,10 @@ class java_bytecode_parse_treet } }; + + // TODO(tkiley): This map shouldn't be interacted with directly (instead + // TODO(tkiley): using add_method_handle and get_method_handle and instead + // TODO(tkiley): should be made private. TG-2785 typedef std::map, lambda_method_handlet> lambda_method_handle_mapt; lambda_method_handle_mapt lambda_method_handle_map; @@ -230,6 +234,16 @@ class java_bytecode_parse_treet return methods.back(); } + void add_method_handle(size_t bootstrap_index, lambda_method_handlet handle) + { + lambda_method_handle_map[{name, bootstrap_index}] = handle; + } + + const lambda_method_handlet &get_method_handle(size_t bootstrap_index) const + { + return lambda_method_handle_map.at({name, bootstrap_index}); + } + void output(std::ostream &out) const; void swap(classt &other); diff --git a/src/java_bytecode/java_bytecode_parser.cpp b/src/java_bytecode/java_bytecode_parser.cpp index 111d772013c..5e8278e5a3a 100644 --- a/src/java_bytecode/java_bytecode_parser.cpp +++ b/src/java_bytecode/java_bytecode_parser.cpp @@ -52,8 +52,6 @@ class java_bytecode_parsert:public parsert method_handle_typet; typedef java_bytecode_parse_treet::classt::lambda_method_handlet lambda_method_handlet; - typedef java_bytecode_parse_treet::classt::lambda_method_handle_mapt - lambda_method_handle_mapt; typedef java_bytecode_parse_treet::classt::u2_valuest u2_valuest; java_bytecode_parse_treet parse_tree; @@ -1941,14 +1939,14 @@ void java_bytecode_parsert::read_bootstrapmethods_entry(classt &parsed_class) << "\n method type is " << id2string(pool_entry(method_type_argument.ref1).s) << eom; - parsed_class.lambda_method_handle_map[{parsed_class.name, bootstrap_method_index}] = - *lambda_method_handle; + parsed_class.add_method_handle( + bootstrap_method_index, *lambda_method_handle); } } /// Creates an unknown method handle and puts it into the parsed_class /// \param parsed_class: The class whose bootstrap method handles we are using -/// \param bootstrap_method_index: The current index in the boostrap entry table +/// \param bootstrap_method_index: The current index in the bootstrap entry table /// \param u2_values: The indices of the arguments for the call void java_bytecode_parsert::store_unknown_method_handle( java_bytecode_parsert::classt &parsed_class, @@ -1957,7 +1955,6 @@ void java_bytecode_parsert::store_unknown_method_handle( { const lambda_method_handlet lambda_method_handle = lambda_method_handlet::create_unknown_handle(move(u2_values)); - parsed_class - .lambda_method_handle_map[{parsed_class.name, bootstrap_method_index}] = - lambda_method_handle; + parsed_class.add_method_handle( + bootstrap_method_index, lambda_method_handle); } From 197401089f729dd20a8317a43c6705cf6486bb3b Mon Sep 17 00:00:00 2001 From: thk123 Date: Mon, 12 Mar 2018 17:04:36 +0000 Subject: [PATCH 17/19] Adjusted the if check to aid readability --- src/java_bytecode/java_bytecode_parser.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/java_bytecode/java_bytecode_parser.cpp b/src/java_bytecode/java_bytecode_parser.cpp index 5e8278e5a3a..90949a33ab8 100644 --- a/src/java_bytecode/java_bytecode_parser.cpp +++ b/src/java_bytecode/java_bytecode_parser.cpp @@ -1895,9 +1895,9 @@ void java_bytecode_parsert::read_bootstrapmethods_entry(classt &parsed_class) const pool_entryt &method_type_argument = pool_entry(method_type_index); if( - !(interface_type_argument.tag == CONSTANT_MethodType && - method_handle_argument.tag == CONSTANT_MethodHandle && - method_type_argument.tag == CONSTANT_MethodType)) + interface_type_argument.tag != CONSTANT_MethodType || + method_handle_argument.tag != CONSTANT_MethodHandle || + method_type_argument.tag != CONSTANT_MethodType) { debug() << "format of BootstrapMethods entry not recognized: arguments " "wrong type" From 0b20a818cdae16d4a7e56f28f4d79fff881625fb Mon Sep 17 00:00:00 2001 From: thk123 Date: Mon, 12 Mar 2018 17:06:22 +0000 Subject: [PATCH 18/19] Added explanation to the test --- regression/cbmc-java/lambda2/test_no_crash_ecj.desc | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/regression/cbmc-java/lambda2/test_no_crash_ecj.desc b/regression/cbmc-java/lambda2/test_no_crash_ecj.desc index a33445a8b6b..2532ac7cf69 100644 --- a/regression/cbmc-java/lambda2/test_no_crash_ecj.desc +++ b/regression/cbmc-java/lambda2/test_no_crash_ecj.desc @@ -8,4 +8,7 @@ SIGNAL=0 -- -- Tests that it doesn't crash when failing to read a `BootstrapMethods` entry and -there is another attribute after this. +there is another attribute after this. The EXIT=10/VERIFCATION FAILED comes from +the fact that the invokedynamic currently returns a null object, causing our +model of this to predict a null pointer exception. This test will need to be +adjusted when lambdas work. From ea6f00f8fa36e85902dcaf8e94159855cfb33f40 Mon Sep 17 00:00:00 2001 From: thk123 Date: Mon, 12 Mar 2018 17:07:40 +0000 Subject: [PATCH 19/19] Fixing linter error --- src/java_bytecode/java_bytecode_parse_tree.h | 1 - src/java_bytecode/java_bytecode_parser.cpp | 15 ++++++--------- 2 files changed, 6 insertions(+), 10 deletions(-) diff --git a/src/java_bytecode/java_bytecode_parse_tree.h b/src/java_bytecode/java_bytecode_parse_tree.h index 6f47f9e0dea..42a04f5200b 100644 --- a/src/java_bytecode/java_bytecode_parse_tree.h +++ b/src/java_bytecode/java_bytecode_parse_tree.h @@ -205,7 +205,6 @@ class java_bytecode_parse_treet } }; - // TODO(tkiley): This map shouldn't be interacted with directly (instead // TODO(tkiley): using add_method_handle and get_method_handle and instead // TODO(tkiley): should be made private. TG-2785 diff --git a/src/java_bytecode/java_bytecode_parser.cpp b/src/java_bytecode/java_bytecode_parser.cpp index 90949a33ab8..e721962cde6 100644 --- a/src/java_bytecode/java_bytecode_parser.cpp +++ b/src/java_bytecode/java_bytecode_parser.cpp @@ -1923,13 +1923,11 @@ void java_bytecode_parsert::read_bootstrapmethods_entry(classt &parsed_class) // If parse_method_handle can't parse the lambda method, it should return {} POSTCONDITION( - lambda_method_handle->handle_type != - method_handle_typet::UNKNOWN_HANDLE); + lambda_method_handle->handle_type != method_handle_typet::UNKNOWN_HANDLE); lambda_method_handle->interface_type = pool_entry(interface_type_argument.ref1).s; - lambda_method_handle->method_type = - pool_entry(method_type_argument.ref1).s; + lambda_method_handle->method_type = pool_entry(method_type_argument.ref1).s; lambda_method_handle->u2_values = std::move(u2_values); debug() << "lambda function reference " << id2string(lambda_method_handle->lambda_method_name) @@ -1937,8 +1935,7 @@ void java_bytecode_parsert::read_bootstrapmethods_entry(classt &parsed_class) << "\n interface type is " << id2string(pool_entry(interface_type_argument.ref1).s) << "\n method type is " - << id2string(pool_entry(method_type_argument.ref1).s) - << eom; + << id2string(pool_entry(method_type_argument.ref1).s) << eom; parsed_class.add_method_handle( bootstrap_method_index, *lambda_method_handle); } @@ -1946,7 +1943,8 @@ void java_bytecode_parsert::read_bootstrapmethods_entry(classt &parsed_class) /// Creates an unknown method handle and puts it into the parsed_class /// \param parsed_class: The class whose bootstrap method handles we are using -/// \param bootstrap_method_index: The current index in the bootstrap entry table +/// \param bootstrap_method_index: The current index in the bootstrap entry +/// table /// \param u2_values: The indices of the arguments for the call void java_bytecode_parsert::store_unknown_method_handle( java_bytecode_parsert::classt &parsed_class, @@ -1955,6 +1953,5 @@ void java_bytecode_parsert::store_unknown_method_handle( { const lambda_method_handlet lambda_method_handle = lambda_method_handlet::create_unknown_handle(move(u2_values)); - parsed_class.add_method_handle( - bootstrap_method_index, lambda_method_handle); + parsed_class.add_method_handle(bootstrap_method_index, lambda_method_handle); }