diff --git a/regression/cbmc-java/lambda2/StaticMethodRef.class b/regression/cbmc-java/lambda2/StaticMethodRef.class new file mode 100644 index 00000000000..9e65a471da3 Binary files /dev/null and b/regression/cbmc-java/lambda2/StaticMethodRef.class differ diff --git a/regression/cbmc-java/lambda2/StaticMethodRef.java b/regression/cbmc-java/lambda2/StaticMethodRef.java new file mode 100644 index 00000000000..1254c60ffb7 --- /dev/null +++ b/regression/cbmc-java/lambda2/StaticMethodRef.java @@ -0,0 +1,24 @@ +import java.util.function.Function; +import java.util.function.BiFunction; + +public class StaticMethodRef{ + 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/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 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..2532ac7cf69 --- /dev/null +++ b/regression/cbmc-java/lambda2/test_no_crash_ecj.desc @@ -0,0 +1,14 @@ +CORE +StaticMethodRef.class +--function StaticMethodRef.Smr +VERIFICATION FAILED +EXIT=10 +SIGNAL=0 +^SIGNAL=0 +-- +-- +Tests that it doesn't crash when failing to read a `BootstrapMethods` entry and +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. diff --git a/src/java_bytecode/java_bytecode_parse_tree.h b/src/java_bytecode/java_bytecode_parse_tree.h index b4593f58d2e..42a04f5200b 100644 --- a/src/java_bytecode/java_bytecode_parse_tree.h +++ b/src/java_bytecode/java_bytecode_parse_tree.h @@ -194,8 +194,20 @@ 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; + } }; + // 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; @@ -221,6 +233,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 d4eb82002c0..e721962cde6 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; @@ -186,6 +184,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 @@ -1803,7 +1806,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 i = 0; i < num_bootstrap_methods; i++) + 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); @@ -1820,122 +1825,133 @@ 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) + // 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. + + // 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) { - // 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, i}] = - 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; - } + 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; + } - debug() << "INFO: parse lambda handle" << eom; - optionalt lambda_method_handle = - parse_method_handle(method_handle_infot{method_handle_argument}); + u2 interface_type_index = u2_values[0]; + u2 method_handle_index = u2_values[1]; + u2 method_type_index = u2_values[2]; - 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; - } - parsed_class.lambda_method_handle_map[{parsed_class.name, i}] = - *lambda_method_handle; + // 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; } - else + + if(!recognized) { - 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; - error() << "ERROR: num_bootstrap_arguments must be at least 3" << 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; + } + + const pool_entryt &interface_type_argument = + 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 || + method_handle_argument.tag != CONSTANT_MethodHandle || + method_type_argument.tag != CONSTANT_MethodType) + { + 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; + } + + 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()) + { + 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; } + + // 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->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.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 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, + 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.add_method_handle(bootstrap_method_index, lambda_method_handle); +}