diff --git a/regression/cbmc-java/lambda1/B.class b/regression/cbmc-java/lambda1/B.class new file mode 100644 index 00000000000..ee0d07a678c Binary files /dev/null and b/regression/cbmc-java/lambda1/B.class differ diff --git a/regression/cbmc-java/lambda1/B.java b/regression/cbmc-java/lambda1/B.java new file mode 100644 index 00000000000..21a3432c08b --- /dev/null +++ b/regression/cbmc-java/lambda1/B.java @@ -0,0 +1,9 @@ +public class B { + public int y; + + public static java.util.function.Function dmul = x -> x * 3.1415; + + public void set(int x) { + y = x; + } +} diff --git a/regression/cbmc-java/lambda1/C.class b/regression/cbmc-java/lambda1/C.class new file mode 100644 index 00000000000..710b045719f Binary files /dev/null and b/regression/cbmc-java/lambda1/C.class differ diff --git a/regression/cbmc-java/lambda1/CustomLambda.class b/regression/cbmc-java/lambda1/CustomLambda.class new file mode 100644 index 00000000000..9834c858288 Binary files /dev/null and b/regression/cbmc-java/lambda1/CustomLambda.class differ diff --git a/regression/cbmc-java/lambda1/CustomLambda.java b/regression/cbmc-java/lambda1/CustomLambda.java new file mode 100644 index 00000000000..1091fe62c46 --- /dev/null +++ b/regression/cbmc-java/lambda1/CustomLambda.java @@ -0,0 +1,4 @@ +@FunctionalInterface +interface CustomLambda { + boolean is_ok(T t); +} diff --git a/regression/cbmc-java/lambda1/Lambdatest$A.class b/regression/cbmc-java/lambda1/Lambdatest$A.class new file mode 100644 index 00000000000..71fae8c53b3 Binary files /dev/null and b/regression/cbmc-java/lambda1/Lambdatest$A.class differ diff --git a/regression/cbmc-java/lambda1/Lambdatest.class b/regression/cbmc-java/lambda1/Lambdatest.class new file mode 100644 index 00000000000..4dbc3b78291 Binary files /dev/null and b/regression/cbmc-java/lambda1/Lambdatest.class differ diff --git a/regression/cbmc-java/lambda1/Lambdatest.java b/regression/cbmc-java/lambda1/Lambdatest.java new file mode 100644 index 00000000000..0e021165b59 --- /dev/null +++ b/regression/cbmc-java/lambda1/Lambdatest.java @@ -0,0 +1,84 @@ +import java.util.function.*; + +public class Lambdatest { + + class A { + int x; + } + + CustomLambda custom = x -> true; + BiFunction add = (x0, y0) -> x0.intValue() + y0; + int z = 10; + + A a; + B b = new B(); + + public Integer g(Float x, Integer y, BiFunction fun) { + return fun.apply(x, y); + } + + public int f(Float x, Integer y, Integer z) { + Integer tmp = add.apply(x, y); + Function mul = (a) -> a * tmp; + return mul.apply(z); + } + + public int i(int x) { + int z = 5; + Function foo = (a) -> a * z; + return foo.apply(x); + } + + public int j(int x) { + Function foo = (a) -> a * z; + return foo.apply(x); + } + + public int k(int x) { + a.x = 10; + + Function foo = (y) -> y * a.x; + return foo.apply(x); + } + + public int l(int x) { + b.y = 10; + Function foo = (y) -> { + int r = y * b.y; + b.set(r); + return r; + }; + b = new B(); + b.y = 14; + return foo.apply(x); + } + + public int m(int x) { + b.y = 10; + Function foo = (y) -> { + int r = y * b.y; + b.y = r; + return r; + }; + return foo.apply(x); + } + + // test static field of different class + public double d(Double x) { + return B.dmul.apply(x); + } + + public int capture2(Float a) { + return add.apply(a, 1); + } + + public boolean custom(Integer i) { + return custom.is_ok(i); + } +} + +class C implements CustomLambda { + public boolean is_ok(Integer i) { + return true; + } +} diff --git a/regression/cbmc-java/lambda1/test.desc b/regression/cbmc-java/lambda1/test.desc new file mode 100644 index 00000000000..9ec5bd91cbd --- /dev/null +++ b/regression/cbmc-java/lambda1/test.desc @@ -0,0 +1,12 @@ +CORE +Lambdatest.class +--verbosity 10 --show-goto-functions +lambda function reference lambda\$new\$0 in class \"Lambdatest\" +lambda function reference lambda\$new\$1 in class \"Lambdatest\" +lambda function reference lambda\$f\$2 in class \"Lambdatest\" +lambda function reference lambda\$i\$3 in class \"Lambdatest\" +lambda function reference lambda\$j\$4 in class \"Lambdatest\" +lambda function reference lambda\$k\$5 in class \"Lambdatest\" +lambda function reference lambda\$l\$6 in class \"Lambdatest\" +lambda function reference lambda\$m\$7 in class \"Lambdatest\" +lambda function reference lambda\$static\$0 in class \"B\" diff --git a/src/java_bytecode/java_bytecode_parse_tree.cpp b/src/java_bytecode/java_bytecode_parse_tree.cpp index b8a60d8ddca..6f6f0b92d41 100644 --- a/src/java_bytecode/java_bytecode_parse_tree.cpp +++ b/src/java_bytecode/java_bytecode_parse_tree.cpp @@ -33,6 +33,9 @@ void java_bytecode_parse_treet::classt::swap( other.fields.swap(fields); other.methods.swap(methods); other.annotations.swap(annotations); + std::swap( + other.attribute_bootstrapmethods_read, attribute_bootstrapmethods_read); + std::swap(other.lambda_method_handle_map, lambda_method_handle_map); } void java_bytecode_parse_treet::output(std::ostream &out) const diff --git a/src/java_bytecode/java_bytecode_parse_tree.h b/src/java_bytecode/java_bytecode_parse_tree.h index bf5b36c5a2b..b4593f58d2e 100644 --- a/src/java_bytecode/java_bytecode_parse_tree.h +++ b/src/java_bytecode/java_bytecode_parse_tree.h @@ -173,8 +173,33 @@ class java_bytecode_parse_treet bool is_abstract=false; bool is_enum=false; bool is_public=false, is_protected=false, is_private=false; + bool attribute_bootstrapmethods_read = false; size_t enum_elements=0; + enum class method_handle_typet + { + LAMBDA_METHOD_HANDLE, + UNKNOWN_HANDLE + }; + + typedef std::vector u2_valuest; + class lambda_method_handlet + { + public: + method_handle_typet handle_type; + irep_idt lambda_method_name; + irep_idt interface_type; + irep_idt method_type; + u2_valuest u2_values; + lambda_method_handlet() : handle_type(method_handle_typet::UNKNOWN_HANDLE) + { + } + }; + + typedef std::map, lambda_method_handlet> + lambda_method_handle_mapt; + lambda_method_handle_mapt lambda_method_handle_map; + typedef std::list implementst; implementst implements; optionalt signature; diff --git a/src/java_bytecode/java_bytecode_parser.cpp b/src/java_bytecode/java_bytecode_parser.cpp index 3c45f87c399..cce0f95a89c 100644 --- a/src/java_bytecode/java_bytecode_parser.cpp +++ b/src/java_bytecode/java_bytecode_parser.cpp @@ -19,6 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include "java_bytecode_parse_tree.h" #include "java_types.h" @@ -47,6 +48,13 @@ class java_bytecode_parsert:public parsert typedef java_bytecode_parse_treet::instructiont instructiont; typedef java_bytecode_parse_treet::annotationt annotationt; typedef java_bytecode_parse_treet::annotationst annotationst; + typedef java_bytecode_parse_treet::classt::method_handle_typet + 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; @@ -126,6 +134,9 @@ class java_bytecode_parsert:public parsert void get_class_refs(); void get_class_refs_rec(const typet &); void parse_local_variable_type_table(methodt &method); + optionalt + parse_method_handle(const class method_handle_infot &entry); + void read_bootstrapmethods_entry(classt &); void skip_bytes(std::size_t bytes) { @@ -202,6 +213,204 @@ class java_bytecode_parsert:public parsert #define VTYPE_INFO_OBJECT 7 #define VTYPE_INFO_UNINIT 8 +class structured_pool_entryt +{ +public: + explicit structured_pool_entryt(java_bytecode_parsert::pool_entryt entry) + : tag(entry.tag) + { + } + + u1 get_tag() const + { + return tag; + } + + typedef std::function + pool_entry_lookupt; + typedef java_bytecode_parsert::pool_entryt pool_entryt; + +protected: + static std::string read_utf8_constant(const pool_entryt &entry) + { + INVARIANT( + entry.tag == CONSTANT_Utf8, "Name entry must be a constant UTF-8"); + return id2string(entry.s); + } + +private: + u1 tag; +}; + +/// Corresponds to the CONSTANT_Class_info Structure +/// Described in Java 8 specification 4.4.1 +class class_infot : public structured_pool_entryt +{ +public: + explicit class_infot(const pool_entryt &entry) : structured_pool_entryt(entry) + { + PRECONDITION(entry.tag == CONSTANT_Class); + name_index = entry.ref1; + } + + std::string get_name(pool_entry_lookupt pool_entry) const + { + const pool_entryt &name_entry = pool_entry(name_index); + return read_utf8_constant(name_entry); + } + +private: + u2 name_index; +}; + +/// Corresponds to the CONSTANT_NameAndType_info Structure +/// Described in Java 8 specification 4.4.6 +class name_and_type_infot : public structured_pool_entryt +{ +public: + explicit name_and_type_infot(java_bytecode_parsert::pool_entryt entry) + : structured_pool_entryt(entry) + { + PRECONDITION(entry.tag == CONSTANT_NameAndType); + name_index = entry.ref1; + descriptor_index = entry.ref2; + } + + std::string get_name(pool_entry_lookupt pool_entry) const + { + const pool_entryt &name_entry = pool_entry(name_index); + return read_utf8_constant(name_entry); + } + + std::string get_descriptor(pool_entry_lookupt pool_entry) const + { + const pool_entryt &descriptor_entry = pool_entry(descriptor_index); + return read_utf8_constant(descriptor_entry); + } + +private: + u2 name_index; + u2 descriptor_index; +}; + +class base_ref_infot : public structured_pool_entryt +{ +public: + explicit base_ref_infot(pool_entryt entry) : structured_pool_entryt(entry) + { + static std::set info_tags = { + CONSTANT_Fieldref, CONSTANT_Methodref, CONSTANT_InterfaceMethodref}; + PRECONDITION(info_tags.find(entry.tag) != info_tags.end()); + class_index = entry.ref1; + name_and_type_index = entry.ref2; + } + + u1 get_class_index() const + { + return class_index; + } + u1 get_name_and_type_index() const + { + return name_and_type_index; + } + + name_and_type_infot get_name_and_type(pool_entry_lookupt pool_entry) const + { + const pool_entryt &name_and_type_entry = pool_entry(name_and_type_index); + + INVARIANT( + name_and_type_entry.tag == CONSTANT_NameAndType, + "name_and_typeindex did not correspond to a name_and_type in the " + "constant pool"); + + return name_and_type_infot{name_and_type_entry}; + } + + class_infot get_class(pool_entry_lookupt pool_entry) const + { + const pool_entryt &class_entry = pool_entry(class_index); + + return class_infot{class_entry}; + } + +private: + u2 class_index; + u2 name_and_type_index; +}; + +class method_handle_infot : public structured_pool_entryt +{ +public: + /// Correspond to the different valid values for field reference_kind From + /// Java 8 spec 4.4.8 + /// (https://docs.oracle.com/javase/specs/jvms/se8/html/jvms-4.html) + enum class method_handle_kindt + { + REF_getField = 1, + REF_getStatic = 2, + REF_putField = 3, + REF_putStatic = 4, + REF_invokeVirtual = 5, + REF_invokeStatic = 6, + REF_invokeSpecial = 7, + REF_newInvokeSpecial = 8, + REF_invokeInterface = 9 + }; + + explicit method_handle_infot(java_bytecode_parsert::pool_entryt entry) + : structured_pool_entryt(entry) + { + PRECONDITION(entry.tag == CONSTANT_MethodHandle); + PRECONDITION(entry.ref1 > 0 && entry.ref1 < 10); // Java 8 spec 4.4.8 + reference_kind = static_cast(entry.ref1); + reference_index = entry.ref2; + } + + base_ref_infot get_reference(pool_entry_lookupt pool_entry) const + { + const base_ref_infot ref_entry{pool_entry(reference_index)}; + + // validate the correctness of the constant pool entry + switch(reference_kind) + { + case method_handle_kindt::REF_getField: + case method_handle_kindt::REF_getStatic: + case method_handle_kindt::REF_putField: + case method_handle_kindt::REF_putStatic: + { + INVARIANT(ref_entry.get_tag() == CONSTANT_Fieldref, "4.4.2"); + break; + } + case method_handle_kindt::REF_invokeVirtual: + case method_handle_kindt::REF_newInvokeSpecial: + { + INVARIANT(ref_entry.get_tag() == CONSTANT_Methodref, "4.4.2"); + break; + } + case method_handle_kindt::REF_invokeStatic: + case method_handle_kindt::REF_invokeSpecial: + { + INVARIANT( + ref_entry.get_tag() == CONSTANT_Methodref || + ref_entry.get_tag() == CONSTANT_InterfaceMethodref, + "4.4.2"); + break; + } + case method_handle_kindt::REF_invokeInterface: + { + INVARIANT(ref_entry.get_tag() == CONSTANT_InterfaceMethodref, ""); + break; + } + } + + return ref_entry; + } + +private: + method_handle_kindt reference_kind; + u2 reference_index; +}; + bool java_bytecode_parsert::parse() { try @@ -1406,6 +1615,18 @@ void java_bytecode_parsert::rclass_attribute(classt &parsed_class) { rRuntimeAnnotation_attribute(parsed_class.annotations); } + else if(attribute_name == "BootstrapMethods") + { + // for this attribute + // cf. https://docs.oracle.com/javase/specs/jvms/se8/html/jvms-4.html#jvms-4.7.23 + INVARIANT( + !parsed_class.attribute_bootstrapmethods_read, + "only one BootstrapMethods argument is allowed in a class file"); + + // mark as read in parsed class + parsed_class.attribute_bootstrapmethods_read = true; + read_bootstrapmethods_entry(parsed_class); + } else skip_bytes(attribute_length); } @@ -1534,3 +1755,179 @@ void java_bytecode_parsert::parse_local_variable_type_table(methodt &method) "Entry in LocalVariableTypeTable must be present in LVT"); } } + +/// Read method handle pointed to from constant pool entry at index, return type +/// of method handle and name if lambda function is found. +/// \param entry: the constant pool entry of the methodhandle_info structure +/// \returns: the method_handle type of the methodhandle_structure, +/// either for a recognized bootstrap method or for a lambda function +optionalt +java_bytecode_parsert::parse_method_handle(const method_handle_infot &entry) +{ + const std::function pool_entry_lambda = + [this](u2 index) -> pool_entryt & { return pool_entry(index); }; + + const base_ref_infot &ref_entry = entry.get_reference(pool_entry_lambda); + + const class_infot &class_entry = ref_entry.get_class(pool_entry_lambda); + const name_and_type_infot &name_and_type = + ref_entry.get_name_and_type(pool_entry_lambda); + + const std::string method_name = + class_entry.get_name(pool_entry_lambda) + "." + + name_and_type.get_name(pool_entry_lambda) + + name_and_type.get_descriptor(pool_entry_lambda); + + lambda_method_handlet lambda_method_handle; + + if(has_prefix(name_and_type.get_name(pool_entry_lambda), "lambda$")) + { + // names seem to be lambda$POSTFIX$NUM + // where POSTFIX is FUN for a function name in which the lambda is define + // "static" when it is a static member of the class + // "new" when it is a class variable, instantiated in + lambda_method_handle.lambda_method_name = + name_and_type.get_name(pool_entry_lambda); + lambda_method_handle.handle_type = + method_handle_typet::LAMBDA_METHOD_HANDLE; + + return lambda_method_handle; + } + + return {}; +} + +/// Read all entries of the `BootstrapMethods` attribute of a class file. +/// \param parsed_class: the class representation of the class file that is +/// currently parsed +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++) + { + u2 bootstrap_methodhandle_ref = read_u2(); + const pool_entryt &entry = pool_entry(bootstrap_methodhandle_ref); + + method_handle_infot method_handle{entry}; + + u2 num_bootstrap_arguments = read_u2(); + debug() << "INFO: parse BootstrapMethod handle " << num_bootstrap_arguments + << " #args" << eom; + + // read u2 values of entry into vector + u2_valuest u2_values(num_bootstrap_arguments); + for(size_t i = 0; i < num_bootstrap_arguments; i++) + 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. + + 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; + } + + 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_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; + } + 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}] = + lambda_method_handle; + error() << "ERROR: num_bootstrap_arguments must be at least 3" << eom; + } + } +} diff --git a/unit/java_bytecode/java_bytecode_parser/java_bytecode_parse_lambda_method_table.cpp b/unit/java_bytecode/java_bytecode_parser/java_bytecode_parse_lambda_method_table.cpp new file mode 100644 index 00000000000..d1484f098a3 --- /dev/null +++ b/unit/java_bytecode/java_bytecode_parser/java_bytecode_parse_lambda_method_table.cpp @@ -0,0 +1,935 @@ +/*******************************************************************\ + + Module: Unit tests for parsing generic classes + + Author: DiffBlue Limited. All rights reserved. + +\*******************************************************************/ + +#include +#include +#include + +#include + +#include +#include + +#include +#include + +typedef java_bytecode_parse_treet::classt::lambda_method_handlet + lambda_method_handlet; + +SCENARIO( + "lambda_method_handle_map with static lambdas", + "[core][java_bytecode][java_bytecode_parse_lambda_method_handle]") +{ + null_message_handlert message_handler; + GIVEN("A class with a static lambda variables") + { + java_bytecode_parse_treet parse_tree; + java_bytecode_parse( + "./java_bytecode/java_bytecode_parser/lambda_examples/" + "StaticLambdas.class", + parse_tree, + message_handler); + WHEN("Parsing that class") + { + REQUIRE(parse_tree.loading_successful); + const java_bytecode_parse_treet::classt parsed_class = + parse_tree.parsed_class; + REQUIRE(parsed_class.attribute_bootstrapmethods_read); + REQUIRE(parsed_class.lambda_method_handle_map.size() == 12); + + // Simple lambdas + THEN( + "There should be an entry for the lambda that has no parameters or " + "returns and the method it references should have an appropriate " + "descriptor") + { + const lambda_method_handlet &lambda_entry = + require_parse_tree::require_lambda_entry_for_descriptor( + parsed_class, "()V"); + + const irep_idt &lambda_impl_name = lambda_entry.lambda_method_name; + + const auto lambda_method = + require_parse_tree::require_method(parsed_class, lambda_impl_name); + REQUIRE(id2string(lambda_method.descriptor) == "()V"); + } + + // Parameter lambdas + THEN( + "There should be an entry for the lambda that takes parameters and the " + "method it references should have an appropriate descriptor") + { + std::string descriptor = "(ILjava/lang/Object;LDummyGeneric;)V"; + const lambda_method_handlet &lambda_entry = + require_parse_tree::require_lambda_entry_for_descriptor( + parsed_class, descriptor); + + const irep_idt &lambda_impl_name = lambda_entry.lambda_method_name; + + const auto lambda_method = + require_parse_tree::require_method(parsed_class, lambda_impl_name); + REQUIRE(id2string(lambda_method.descriptor) == descriptor); + } + THEN( + "There should be an entry for the lambda that takes array parameters " + "and the method it references should have an appropriate descriptor") + { + std::string descriptor = "([I[Ljava/lang/Object;[LDummyGeneric;)V"; + const lambda_method_handlet &lambda_entry = + require_parse_tree::require_lambda_entry_for_descriptor( + parsed_class, descriptor); + + const irep_idt &lambda_impl_name = lambda_entry.lambda_method_name; + + const auto lambda_method = + require_parse_tree::require_method(parsed_class, lambda_impl_name); + REQUIRE(id2string(lambda_method.descriptor) == descriptor); + } + + // Return lambdas + THEN( + "There should be an entry for the lambda that returns a primitive and " + "the method it references should have an appropriate descriptor") + { + std::string descriptor = "()I"; + const lambda_method_handlet &lambda_entry = + require_parse_tree::require_lambda_entry_for_descriptor( + parsed_class, descriptor); + + const irep_idt &lambda_impl_name = lambda_entry.lambda_method_name; + + const auto lambda_method = + require_parse_tree::require_method(parsed_class, lambda_impl_name); + REQUIRE(id2string(lambda_method.descriptor) == descriptor); + } + THEN( + "There should be an entry for the lambda that returns a reference type " + "and the method it references should have an appropriate descriptor") + { + std::string descriptor = "()Ljava/lang/Object;"; + const lambda_method_handlet &lambda_entry = + require_parse_tree::require_lambda_entry_for_descriptor( + parsed_class, descriptor); + + const irep_idt &lambda_impl_name = lambda_entry.lambda_method_name; + + const auto lambda_method = + require_parse_tree::require_method(parsed_class, lambda_impl_name); + REQUIRE(id2string(lambda_method.descriptor) == descriptor); + } + THEN( + "There should be an entry for the lambda that returns a specialised " + "generic type and the method it references should have an appropriate " + "descriptor") + { + std::string descriptor = "()LDummyGeneric;"; + const lambda_method_handlet &lambda_entry = + require_parse_tree::require_lambda_entry_for_descriptor( + parsed_class, descriptor); + + const irep_idt &lambda_impl_name = lambda_entry.lambda_method_name; + + const auto lambda_method = + require_parse_tree::require_method(parsed_class, lambda_impl_name); + REQUIRE(id2string(lambda_method.descriptor) == descriptor); + } + + // Array returning lambdas + THEN( + "There should be an entry for the lambda that returns an array of " + "primitives and the method it references should have an appropriate " + "descriptor") + { + std::string descriptor = "()[I"; + const lambda_method_handlet &lambda_entry = + require_parse_tree::require_lambda_entry_for_descriptor( + parsed_class, descriptor); + + const irep_idt &lambda_impl_name = lambda_entry.lambda_method_name; + + const auto lambda_method = + require_parse_tree::require_method(parsed_class, lambda_impl_name); + REQUIRE(id2string(lambda_method.descriptor) == descriptor); + } + THEN( + "There should be an entry for the lambda that returns an array of " + "reference types and the method it references should have an " + "appropriate descriptor") + { + std::string descriptor = "()[Ljava/lang/Object;"; + const lambda_method_handlet &lambda_entry = + require_parse_tree::require_lambda_entry_for_descriptor( + parsed_class, descriptor); + + const irep_idt &lambda_impl_name = lambda_entry.lambda_method_name; + + const auto lambda_method = + require_parse_tree::require_method(parsed_class, lambda_impl_name); + REQUIRE(id2string(lambda_method.descriptor) == descriptor); + } + THEN( + "There should be an entry for the lambda that returns an array of " + "specialised generic types and the method it references should have an " + "appropriate descriptor") + { + std::string descriptor = "()[LDummyGeneric;"; + const lambda_method_handlet &lambda_entry = + require_parse_tree::require_lambda_entry_for_descriptor( + parsed_class, descriptor); + + const irep_idt &lambda_impl_name = lambda_entry.lambda_method_name; + + const auto lambda_method = + require_parse_tree::require_method(parsed_class, lambda_impl_name); + REQUIRE(id2string(lambda_method.descriptor) == descriptor); + } + + // Capturing lamdbas + THEN( + "There should be an entry for the lambda that returns a primitive and " + "the method it references should have an appropriate descriptor") + { + std::string descriptor = "()I"; + const lambda_method_handlet &lambda_entry = + require_parse_tree::require_lambda_entry_for_descriptor( + parsed_class, descriptor, 1); + + const irep_idt &lambda_impl_name = lambda_entry.lambda_method_name; + + const auto lambda_method = + require_parse_tree::require_method(parsed_class, lambda_impl_name); + REQUIRE(id2string(lambda_method.descriptor) == descriptor); + + const typet primitive_type = java_int_type(); + + fieldref_exprt fieldref{ + primitive_type, "staticPrimitive", "java::StaticLambdas"}; + + std::vector + expected_instructions{{"getstatic", {fieldref}}, {"ireturn", {}}}; + + require_parse_tree::require_instructions_match_expectation( + expected_instructions, lambda_method.instructions); + } + THEN( + "There should be an entry for the lambda that returns a reference type " + "and the method it references should have an appropriate descriptor") + { + std::string descriptor = "()Ljava/lang/Object;"; + const lambda_method_handlet &lambda_entry = + require_parse_tree::require_lambda_entry_for_descriptor( + parsed_class, descriptor, 1); + + const irep_idt &lambda_impl_name = lambda_entry.lambda_method_name; + + const auto lambda_method = + require_parse_tree::require_method(parsed_class, lambda_impl_name); + REQUIRE(id2string(lambda_method.descriptor) == descriptor); + + const reference_typet dummy_generic_reference_type = + java_reference_type(symbol_typet{"java::java.lang.Object"}); + + fieldref_exprt fieldref{dummy_generic_reference_type, + "staticReference", + "java::StaticLambdas"}; + + std::vector + expected_instructions{{"getstatic", {fieldref}}, {"areturn", {}}}; + + require_parse_tree::require_instructions_match_expectation( + expected_instructions, lambda_method.instructions); + } + THEN( + "There should be an entry for the lambda that returns a specialised " + "generic type and the method it references should have an appropriate " + "descriptor") + { + std::string descriptor = "()LDummyGeneric;"; + const lambda_method_handlet &lambda_entry = + require_parse_tree::require_lambda_entry_for_descriptor( + parsed_class, descriptor, 1); + + const irep_idt &lambda_impl_name = lambda_entry.lambda_method_name; + + const java_bytecode_parse_treet::methodt &lambda_method = + require_parse_tree::require_method(parsed_class, lambda_impl_name); + REQUIRE(id2string(lambda_method.descriptor) == descriptor); + + const reference_typet dummy_generic_reference_type = + java_reference_type(symbol_typet{"java::DummyGeneric"}); + + fieldref_exprt fieldref{dummy_generic_reference_type, + "staticSpecalisedGeneric", + "java::StaticLambdas"}; + + std::vector + expected_instructions{{"getstatic", {fieldref}}, {"areturn", {}}}; + + require_parse_tree::require_instructions_match_expectation( + expected_instructions, lambda_method.instructions); + } + } + } +} +SCENARIO( + "lambda_method_handle_map with local lambdas", + "[core][java_bytecode][java_bytecode_parse_lambda_method_handle]") +{ + null_message_handlert message_handler; + GIVEN("A method with local lambdas") + { + java_bytecode_parse_treet parse_tree; + java_bytecode_parse( + "./java_bytecode/java_bytecode_parser/lambda_examples/" + "LocalLambdas.class", + parse_tree, + message_handler); + WHEN("Parsing that class") + { + REQUIRE(parse_tree.loading_successful); + const java_bytecode_parse_treet::classt parsed_class = + parse_tree.parsed_class; + REQUIRE(parsed_class.attribute_bootstrapmethods_read); + REQUIRE(parsed_class.lambda_method_handle_map.size() == 12); + + // Simple lambdas + THEN( + "There should be an entry for the lambda that has no parameters or " + "returns and the method it references should have an appropriate " + "descriptor") + { + const lambda_method_handlet &lambda_entry = + require_parse_tree::require_lambda_entry_for_descriptor( + parsed_class, "()V"); + + const irep_idt &lambda_impl_name = lambda_entry.lambda_method_name; + + const auto lambda_method = + require_parse_tree::require_method(parsed_class, lambda_impl_name); + REQUIRE(id2string(lambda_method.descriptor) == "()V"); + } + + // Parameter lambdas + THEN( + "There should be an entry for the lambda that takes parameters and the " + "method it references should have an appropriate descriptor") + { + std::string descriptor = "(ILjava/lang/Object;LDummyGeneric;)V"; + const lambda_method_handlet &lambda_entry = + require_parse_tree::require_lambda_entry_for_descriptor( + parsed_class, descriptor); + + const irep_idt &lambda_impl_name = lambda_entry.lambda_method_name; + + const auto lambda_method = + require_parse_tree::require_method(parsed_class, lambda_impl_name); + REQUIRE(id2string(lambda_method.descriptor) == descriptor); + } + THEN( + "There should be an entry for the lambda that takes array parameters " + "and the method it references should have an appropriate descriptor") + { + std::string descriptor = "([I[Ljava/lang/Object;[LDummyGeneric;)V"; + const lambda_method_handlet &lambda_entry = + require_parse_tree::require_lambda_entry_for_descriptor( + parsed_class, descriptor); + + const irep_idt &lambda_impl_name = lambda_entry.lambda_method_name; + + const auto lambda_method = + require_parse_tree::require_method(parsed_class, lambda_impl_name); + REQUIRE(id2string(lambda_method.descriptor) == descriptor); + } + + // Return lambdas + THEN( + "There should be an entry for the lambda that returns a primitive and " + "the method it references should have an appropriate descriptor") + { + std::string descriptor = "()I"; + const lambda_method_handlet &lambda_entry = + require_parse_tree::require_lambda_entry_for_descriptor( + parsed_class, descriptor); + + const irep_idt &lambda_impl_name = lambda_entry.lambda_method_name; + + const auto lambda_method = + require_parse_tree::require_method(parsed_class, lambda_impl_name); + REQUIRE(id2string(lambda_method.descriptor) == descriptor); + } + THEN( + "There should be an entry for the lambda that returns a reference type " + "and the method it references should have an appropriate descriptor") + { + std::string descriptor = "()Ljava/lang/Object;"; + const lambda_method_handlet &lambda_entry = + require_parse_tree::require_lambda_entry_for_descriptor( + parsed_class, descriptor); + + const irep_idt &lambda_impl_name = lambda_entry.lambda_method_name; + + const auto lambda_method = + require_parse_tree::require_method(parsed_class, lambda_impl_name); + REQUIRE(id2string(lambda_method.descriptor) == descriptor); + } + THEN( + "There should be an entry for the lambda that returns a specialised " + "generic type and the method it references should have an appropriate " + "descriptor") + { + std::string descriptor = "()LDummyGeneric;"; + const lambda_method_handlet &lambda_entry = + require_parse_tree::require_lambda_entry_for_descriptor( + parsed_class, descriptor); + + const irep_idt &lambda_impl_name = lambda_entry.lambda_method_name; + + const auto lambda_method = + require_parse_tree::require_method(parsed_class, lambda_impl_name); + REQUIRE(id2string(lambda_method.descriptor) == descriptor); + } + + // Array returning lambdas + THEN( + "There should be an entry for the lambda that returns an array of " + "primitives and the method it references should have an appropriate " + "descriptor") + { + std::string descriptor = "()[I"; + const lambda_method_handlet &lambda_entry = + require_parse_tree::require_lambda_entry_for_descriptor( + parsed_class, descriptor); + + const irep_idt &lambda_impl_name = lambda_entry.lambda_method_name; + + const auto lambda_method = + require_parse_tree::require_method(parsed_class, lambda_impl_name); + REQUIRE(id2string(lambda_method.descriptor) == descriptor); + } + THEN( + "There should be an entry for the lambda that returns an array of " + "reference types and the method it references should have an " + "appropriate descriptor") + { + std::string descriptor = "()[Ljava/lang/Object;"; + const lambda_method_handlet &lambda_entry = + require_parse_tree::require_lambda_entry_for_descriptor( + parsed_class, descriptor); + + const irep_idt &lambda_impl_name = lambda_entry.lambda_method_name; + + const auto lambda_method = + require_parse_tree::require_method(parsed_class, lambda_impl_name); + REQUIRE(id2string(lambda_method.descriptor) == descriptor); + } + THEN( + "There should be an entry for the lambda that returns an array of " + "specialised generic types and the method it references should have an " + "appropriate descriptor") + { + std::string descriptor = "()[LDummyGeneric;"; + const lambda_method_handlet &lambda_entry = + require_parse_tree::require_lambda_entry_for_descriptor( + parsed_class, descriptor); + + const irep_idt &lambda_impl_name = lambda_entry.lambda_method_name; + + const auto lambda_method = + require_parse_tree::require_method(parsed_class, lambda_impl_name); + REQUIRE(id2string(lambda_method.descriptor) == descriptor); + } + + // Capturing lamdbas + THEN( + "There should be an entry for the lambda that returns a primitive " + "local variable and the method it references should have an " + "appropriate descriptor") + { + std::string descriptor = "()I"; + const lambda_method_handlet &lambda_entry = + require_parse_tree::require_lambda_entry_for_descriptor( + parsed_class, descriptor, 1); + + const irep_idt &lambda_impl_name = lambda_entry.lambda_method_name; + + const auto lambda_method = + require_parse_tree::require_method(parsed_class, lambda_impl_name); + // Note here the descriptor of the implementation is different - the + // implementation requries the input to be passed in + REQUIRE(id2string(lambda_method.descriptor) == "(I)I"); + + std::vector + expected_instructions{{"iload_0", {}}, {"ireturn", {}}}; + + require_parse_tree::require_instructions_match_expectation( + expected_instructions, lambda_method.instructions); + } + THEN( + "There should be an entry for the lambda that returns a reference type " + "local variable and the method it references should have an " + "appropriate descriptor") + { + // Since it is a local variable, the corresponding method takes the + // captured variable as an input + std::string descriptor = "()Ljava/lang/Object;"; + const lambda_method_handlet &lambda_entry = + require_parse_tree::require_lambda_entry_for_descriptor( + parsed_class, descriptor, 1); + + const irep_idt &lambda_impl_name = lambda_entry.lambda_method_name; + + const auto lambda_method = + require_parse_tree::require_method(parsed_class, lambda_impl_name); + REQUIRE( + id2string(lambda_method.descriptor) == + "(Ljava/lang/Object;)Ljava/lang/Object;"); + + std::vector + expected_instructions{{"aload_0", {}}, {"areturn", {}}}; + + require_parse_tree::require_instructions_match_expectation( + expected_instructions, lambda_method.instructions); + } + THEN( + "There should be an entry for the lambda that returns a specialised " + "generic type local variable and the method it references should have " + "an appropriate descriptor") + { + // Since it is a local variable, the corresponding method takes the + // captured variable as an input + std::string descriptor = "()LDummyGeneric;"; + const lambda_method_handlet &lambda_entry = + require_parse_tree::require_lambda_entry_for_descriptor( + parsed_class, descriptor, 1); + + const irep_idt &lambda_impl_name = lambda_entry.lambda_method_name; + + const java_bytecode_parse_treet::methodt &lambda_method = + require_parse_tree::require_method(parsed_class, lambda_impl_name); + REQUIRE( + id2string(lambda_method.descriptor) == + "(LDummyGeneric;)LDummyGeneric;"); + + // since just returning the parameter, nothing to put on the stack + std::vector + expected_instructions{{"aload_0", {}}, {"areturn", {}}}; + + require_parse_tree::require_instructions_match_expectation( + expected_instructions, lambda_method.instructions); + } + } + } +} +SCENARIO( + "lambda_method_handle_map with member lambdas", + "[core][java_bytecode][java_bytecode_parse_lambda_method_handle]") +{ + null_message_handlert message_handler; + GIVEN("A class that has lambdas as member variables") + { + java_bytecode_parse_treet parse_tree; + java_bytecode_parse( + "./java_bytecode/java_bytecode_parser/lambda_examples/" + "MemberLambdas.class", + parse_tree, + message_handler); + WHEN("Parsing that class") + { + REQUIRE(parse_tree.loading_successful); + const java_bytecode_parse_treet::classt parsed_class = + parse_tree.parsed_class; + REQUIRE(parsed_class.attribute_bootstrapmethods_read); + REQUIRE(parsed_class.lambda_method_handle_map.size() == 12); + + // Simple lambdas + THEN( + "There should be an entry for the lambda that has no parameters or " + "returns and the method it references should have an appropriate " + "descriptor") + { + const lambda_method_handlet &lambda_entry = + require_parse_tree::require_lambda_entry_for_descriptor( + parsed_class, "()V"); + + const irep_idt &lambda_impl_name = lambda_entry.lambda_method_name; + + const auto lambda_method = + require_parse_tree::require_method(parsed_class, lambda_impl_name); + REQUIRE(id2string(lambda_method.descriptor) == "()V"); + } + + // Parameter lambdas + THEN( + "There should be an entry for the lambda that takes parameters and the " + "method it references should have an appropriate descriptor") + { + std::string descriptor = "(ILjava/lang/Object;LDummyGeneric;)V"; + const lambda_method_handlet &lambda_entry = + require_parse_tree::require_lambda_entry_for_descriptor( + parsed_class, descriptor); + + const irep_idt &lambda_impl_name = lambda_entry.lambda_method_name; + + const auto lambda_method = + require_parse_tree::require_method(parsed_class, lambda_impl_name); + REQUIRE(id2string(lambda_method.descriptor) == descriptor); + } + THEN( + "There should be an entry for the lambda that takes array parameters " + "and the method it references should have an appropriate descriptor") + { + std::string descriptor = "([I[Ljava/lang/Object;[LDummyGeneric;)V"; + const lambda_method_handlet &lambda_entry = + require_parse_tree::require_lambda_entry_for_descriptor( + parsed_class, descriptor); + + const irep_idt &lambda_impl_name = lambda_entry.lambda_method_name; + + const auto lambda_method = + require_parse_tree::require_method(parsed_class, lambda_impl_name); + REQUIRE(id2string(lambda_method.descriptor) == descriptor); + } + + // Return lambdas + THEN( + "There should be an entry for the lambda that returns a primitive and " + "the method it references should have an appropriate descriptor") + { + std::string descriptor = "()I"; + const lambda_method_handlet &lambda_entry = + require_parse_tree::require_lambda_entry_for_descriptor( + parsed_class, descriptor); + + const irep_idt &lambda_impl_name = lambda_entry.lambda_method_name; + + const auto lambda_method = + require_parse_tree::require_method(parsed_class, lambda_impl_name); + REQUIRE(id2string(lambda_method.descriptor) == descriptor); + } + THEN( + "There should be an entry for the lambda that returns a reference type " + "and the method it references should have an appropriate descriptor") + { + std::string descriptor = "()Ljava/lang/Object;"; + const lambda_method_handlet &lambda_entry = + require_parse_tree::require_lambda_entry_for_descriptor( + parsed_class, descriptor); + + const irep_idt &lambda_impl_name = lambda_entry.lambda_method_name; + + const auto lambda_method = + require_parse_tree::require_method(parsed_class, lambda_impl_name); + REQUIRE(id2string(lambda_method.descriptor) == descriptor); + } + THEN( + "There should be an entry for the lambda that returns a specialised " + "generic type and the method it references should have an appropriate " + "descriptor") + { + std::string descriptor = "()LDummyGeneric;"; + const lambda_method_handlet &lambda_entry = + require_parse_tree::require_lambda_entry_for_descriptor( + parsed_class, descriptor); + + const irep_idt &lambda_impl_name = lambda_entry.lambda_method_name; + + const auto lambda_method = + require_parse_tree::require_method(parsed_class, lambda_impl_name); + REQUIRE(id2string(lambda_method.descriptor) == descriptor); + } + + // Array returning lambdas + THEN( + "There should be an entry for the lambda that returns an array of " + "primitives and the method it references should have an appropriate " + "descriptor") + { + std::string descriptor = "()[I"; + const lambda_method_handlet &lambda_entry = + require_parse_tree::require_lambda_entry_for_descriptor( + parsed_class, descriptor); + + const irep_idt &lambda_impl_name = lambda_entry.lambda_method_name; + + const auto lambda_method = + require_parse_tree::require_method(parsed_class, lambda_impl_name); + REQUIRE(id2string(lambda_method.descriptor) == descriptor); + } + THEN( + "There should be an entry for the lambda that returns an array of " + "reference types and the method it references should have an " + "appropriate descriptor") + { + std::string descriptor = "()[Ljava/lang/Object;"; + const lambda_method_handlet &lambda_entry = + require_parse_tree::require_lambda_entry_for_descriptor( + parsed_class, descriptor); + + const irep_idt &lambda_impl_name = lambda_entry.lambda_method_name; + + const auto lambda_method = + require_parse_tree::require_method(parsed_class, lambda_impl_name); + REQUIRE(id2string(lambda_method.descriptor) == descriptor); + } + THEN( + "There should be an entry for the lambda that returns an array of " + "specialised generic types and the method it references should have an " + "appropriate descriptor") + { + std::string descriptor = "()[LDummyGeneric;"; + const lambda_method_handlet &lambda_entry = + require_parse_tree::require_lambda_entry_for_descriptor( + parsed_class, descriptor); + + const irep_idt &lambda_impl_name = lambda_entry.lambda_method_name; + + const auto lambda_method = + require_parse_tree::require_method(parsed_class, lambda_impl_name); + REQUIRE(id2string(lambda_method.descriptor) == descriptor); + } + + // Capturing lamdbas + THEN( + "There should be an entry for the lambda that returns a primitive " + "local variable and the method it references should have an " + "appropriate descriptor") + { + std::string descriptor = "()I"; + const lambda_method_handlet &lambda_entry = + require_parse_tree::require_lambda_entry_for_descriptor( + parsed_class, descriptor, 1); + + const irep_idt &lambda_impl_name = lambda_entry.lambda_method_name; + + const auto lambda_method = + require_parse_tree::require_method(parsed_class, lambda_impl_name); + // Note here the descriptor of the implementation is different - the + // implementation requries the input to be passed in + REQUIRE(id2string(lambda_method.descriptor) == "()I"); + REQUIRE_FALSE(lambda_method.is_static); + + const fieldref_exprt primitive_fieldref{ + java_int_type(), "memberPrimitive", "java::MemberLambdas"}; + + std::vector + expected_instructions{{"aload_0", {}}, // load this of stack + {"getfield", {primitive_fieldref}}, + {"ireturn", {}}}; + + require_parse_tree::require_instructions_match_expectation( + expected_instructions, lambda_method.instructions); + } + THEN( + "There should be an entry for the lambda that returns a reference type " + "local variable and the method it references should have an " + "appropriate descriptor") + { + // Since it is a local variable, the corresponding method takes the + // captured variable as an input + std::string descriptor = "()Ljava/lang/Object;"; + const lambda_method_handlet &lambda_entry = + require_parse_tree::require_lambda_entry_for_descriptor( + parsed_class, descriptor, 1); + + const irep_idt &lambda_impl_name = lambda_entry.lambda_method_name; + + const auto lambda_method = + require_parse_tree::require_method(parsed_class, lambda_impl_name); + REQUIRE(id2string(lambda_method.descriptor) == "()Ljava/lang/Object;"); + REQUIRE_FALSE(lambda_method.is_static); + + const reference_typet dummy_generic_reference_type = + java_reference_type(symbol_typet{"java::java.lang.Object"}); + + const fieldref_exprt reference_fieldref{dummy_generic_reference_type, + "memberReference", + "java::MemberLambdas"}; + + std::vector + expected_instructions{{"aload_0", {}}, // load this of stack + {"getfield", {reference_fieldref}}, + {"areturn", {}}}; + + require_parse_tree::require_instructions_match_expectation( + expected_instructions, lambda_method.instructions); + } + THEN( + "There should be an entry for the lambda that returns a specialised " + "generic type local variable and the method it references should have " + "an appropriate descriptor") + { + // Since it is a local variable, the corresponding method takes the + // captured variable as an input + std::string descriptor = "()LDummyGeneric;"; + const lambda_method_handlet &lambda_entry = + require_parse_tree::require_lambda_entry_for_descriptor( + parsed_class, descriptor, 1); + + const irep_idt &lambda_impl_name = lambda_entry.lambda_method_name; + + const java_bytecode_parse_treet::methodt &lambda_method = + require_parse_tree::require_method(parsed_class, lambda_impl_name); + REQUIRE(id2string(lambda_method.descriptor) == "()LDummyGeneric;"); + REQUIRE_FALSE(lambda_method.is_static); + + const reference_typet dummy_generic_reference_type = + java_reference_type(symbol_typet{"java::DummyGeneric"}); + + const fieldref_exprt generic_reference_fieldref{ + dummy_generic_reference_type, + "memberSpecalisedGeneric", + "java::MemberLambdas"}; + + // since just returning the parameter, nothing to put on the stack + std::vector + expected_instructions{{"aload_0", {}}, // load this of stack + {"getfield", {generic_reference_fieldref}}, + {"areturn", {}}}; + + require_parse_tree::require_instructions_match_expectation( + expected_instructions, lambda_method.instructions); + } + } + } +} +SCENARIO( + "lambda_method_handle_map with member lambdas capturing outer class " + "variables", + "[core][java_bytecode][java_bytecode_parse_lambda_method_handle]") +{ + null_message_handlert message_handler; + GIVEN( + "An inner class with member variables as lambdas that capture outer " + "variables") + { + java_bytecode_parse_treet parse_tree; + java_bytecode_parse( + "./java_bytecode/java_bytecode_parser/lambda_examples/" + "OuterMemberLambdas$Inner.class", + parse_tree, + message_handler); + WHEN("Parsing that class") + { + REQUIRE(parse_tree.loading_successful); + const java_bytecode_parse_treet::classt parsed_class = + parse_tree.parsed_class; + REQUIRE(parsed_class.attribute_bootstrapmethods_read); + REQUIRE(parsed_class.lambda_method_handle_map.size() == 3); + + // Field ref for getting the outer class + const reference_typet outer_class_reference_type = + java_reference_type(symbol_typet{"java::OuterMemberLambdas"}); + const fieldref_exprt outer_fieldref{ + outer_class_reference_type, "this$0", "java::OuterMemberLambdas$Inner"}; + + THEN( + "There should be an entry for the lambda that returns a primitive " + "local variable and the method it references should have an " + "appropriate descriptor") + { + std::string descriptor = "()I"; + const lambda_method_handlet &lambda_entry = + require_parse_tree::require_lambda_entry_for_descriptor( + parsed_class, descriptor); + + const irep_idt &lambda_impl_name = lambda_entry.lambda_method_name; + + const auto lambda_method = + require_parse_tree::require_method(parsed_class, lambda_impl_name); + // Note here the descriptor of the implementation is different - the + // implementation requries the input to be passed in + REQUIRE(id2string(lambda_method.descriptor) == "()I"); + REQUIRE_FALSE(lambda_method.is_static); + + const fieldref_exprt primitive_fieldref{ + java_int_type(), "memberPrimitive", "java::OuterMemberLambdas"}; + + std::vector + expected_instructions{{"aload_0", {}}, // load this of stack + {"getfield", {outer_fieldref}}, + {"getfield", {primitive_fieldref}}, + {"ireturn", {}}}; + + require_parse_tree::require_instructions_match_expectation( + expected_instructions, lambda_method.instructions); + } + THEN( + "There should be an entry for the lambda that returns a reference type " + "local variable and the method it references should have an " + "appropriate descriptor") + { + // Since it is a local variable, the corresponding method takes the + // captured variable as an input + std::string descriptor = "()Ljava/lang/Object;"; + const lambda_method_handlet &lambda_entry = + require_parse_tree::require_lambda_entry_for_descriptor( + parsed_class, descriptor); + + const irep_idt &lambda_impl_name = lambda_entry.lambda_method_name; + + const auto lambda_method = + require_parse_tree::require_method(parsed_class, lambda_impl_name); + REQUIRE(id2string(lambda_method.descriptor) == "()Ljava/lang/Object;"); + REQUIRE_FALSE(lambda_method.is_static); + + const reference_typet dummy_generic_reference_type = + java_reference_type(symbol_typet{"java::java.lang.Object"}); + + const fieldref_exprt reference_fieldref{dummy_generic_reference_type, + "memberReference", + "java::OuterMemberLambdas"}; + + std::vector + expected_instructions{{"aload_0", {}}, // load this of stack + {"getfield", {outer_fieldref}}, + {"getfield", {reference_fieldref}}, + {"areturn", {}}}; + + require_parse_tree::require_instructions_match_expectation( + expected_instructions, lambda_method.instructions); + } + THEN( + "There should be an entry for the lambda that returns a specialised " + "generic type local variable and the method it references should have " + "an appropriate descriptor") + { + // Since it is a local variable, the corresponding method takes the + // captured variable as an input + std::string descriptor = "()LDummyGeneric;"; + const lambda_method_handlet &lambda_entry = + require_parse_tree::require_lambda_entry_for_descriptor( + parsed_class, descriptor); + + const irep_idt &lambda_impl_name = lambda_entry.lambda_method_name; + + const java_bytecode_parse_treet::methodt &lambda_method = + require_parse_tree::require_method(parsed_class, lambda_impl_name); + REQUIRE(id2string(lambda_method.descriptor) == "()LDummyGeneric;"); + REQUIRE_FALSE(lambda_method.is_static); + + const reference_typet dummy_generic_reference_type = + java_reference_type(symbol_typet{"java::DummyGeneric"}); + + const fieldref_exprt generic_reference_fieldref{ + dummy_generic_reference_type, + "memberSpecalisedGeneric", + "java::OuterMemberLambdas"}; + + // since just returning the parameter, nothing to put on the stack + std::vector + expected_instructions{{"aload_0", {}}, // load this of stack + {"getfield", {outer_fieldref}}, + {"getfield", {generic_reference_fieldref}}, + {"areturn", {}}}; + + require_parse_tree::require_instructions_match_expectation( + expected_instructions, lambda_method.instructions); + } + } + } +} diff --git a/unit/java_bytecode/java_bytecode_parser/lambda_examples/ArrayParameterLambda.class b/unit/java_bytecode/java_bytecode_parser/lambda_examples/ArrayParameterLambda.class new file mode 100644 index 00000000000..56886405324 Binary files /dev/null and b/unit/java_bytecode/java_bytecode_parser/lambda_examples/ArrayParameterLambda.class differ diff --git a/unit/java_bytecode/java_bytecode_parser/lambda_examples/DummyGeneric.class b/unit/java_bytecode/java_bytecode_parser/lambda_examples/DummyGeneric.class new file mode 100644 index 00000000000..afbff9f82d1 Binary files /dev/null and b/unit/java_bytecode/java_bytecode_parser/lambda_examples/DummyGeneric.class differ diff --git a/unit/java_bytecode/java_bytecode_parser/lambda_examples/LambdaInterfaces.java b/unit/java_bytecode/java_bytecode_parser/lambda_examples/LambdaInterfaces.java new file mode 100644 index 00000000000..388d8230df6 --- /dev/null +++ b/unit/java_bytecode/java_bytecode_parser/lambda_examples/LambdaInterfaces.java @@ -0,0 +1,39 @@ +interface SimpleLambda { + public void Execute(); +} + +interface ParameterLambda { + public void Execute(int primitive, Object reference, DummyGeneric specalisedGeneric); +} + +interface ArrayParameterLambda { + public void Execute(int[] primitive, Object[] reference, DummyGeneric[] specalisedGeneric); +} + +interface ReturningLambdaPrimitive { + public int Execute(); +} + +interface ReturningLambdaReference { + public Object Execute(); +} + +interface ReturningLambdaSpecalisedGeneric { + public DummyGeneric Execute(); +} + +interface ReturningLambdaPrimitiveArray { + public int[] Execute(); +} + +interface ReturningLambdaReferenceArray { + public Object[] Execute(); +} + +interface ReturningLambdaSpecalisedGenericArray { + public DummyGeneric[] Execute(); +} + +class DummyGeneric { + T field; +} diff --git a/unit/java_bytecode/java_bytecode_parser/lambda_examples/LocalLambdas.class b/unit/java_bytecode/java_bytecode_parser/lambda_examples/LocalLambdas.class new file mode 100644 index 00000000000..28f9f1d7990 Binary files /dev/null and b/unit/java_bytecode/java_bytecode_parser/lambda_examples/LocalLambdas.class differ diff --git a/unit/java_bytecode/java_bytecode_parser/lambda_examples/LocalLambdas.java b/unit/java_bytecode/java_bytecode_parser/lambda_examples/LocalLambdas.java new file mode 100644 index 00000000000..181662018ee --- /dev/null +++ b/unit/java_bytecode/java_bytecode_parser/lambda_examples/LocalLambdas.java @@ -0,0 +1,59 @@ +public class LocalLambdas { + public static void test() { + int localPrimitive = 5; + Object localReference = null; + DummyGeneric localSpecalisedGeneric = null; + + // Declare some local lambdas + SimpleLambda simpleLambda = () -> { /*NOP*/ }; + + ParameterLambda paramLambda = + (int primitive, Object reference, DummyGeneric specalisedGeneric) -> {}; + ArrayParameterLambda arrayParamLambda = + (int[] primitive, Object[] reference, DummyGeneric[] specalisedGeneric) -> {}; + + ReturningLambdaPrimitive returnPrimitiveLambda = () -> { + return 1; + }; + ReturningLambdaReference returnReferenceLambda = () -> { + return null; + }; + ReturningLambdaSpecalisedGeneric returningSpecalisedGenericLambda = () -> { + return null; + }; + + ReturningLambdaPrimitiveArray returnPrimitiveArrayLambda = () -> { + return null; + }; + ReturningLambdaReferenceArray returnReferenceArrayLambda = () -> { + return null; + }; + ReturningLambdaSpecalisedGenericArray returningSpecalisedGenericArrayLambda = () -> { + return null; + }; + + ReturningLambdaPrimitive returnPrimitiveLambdaCapture = () -> { + return localPrimitive; + }; + ReturningLambdaReference returnReferenceLambdaCapture = () -> { + return localReference; + }; + ReturningLambdaSpecalisedGeneric returningSpecalisedGenericLambdaCapture = () -> { + return localSpecalisedGeneric; + }; + + simpleLambda.Execute(); + paramLambda.Execute(4, null, null); + arrayParamLambda.Execute(null, null, null); + returnPrimitiveLambda.Execute(); + returnReferenceLambda.Execute(); + returningSpecalisedGenericLambda.Execute(); + returnPrimitiveArrayLambda.Execute(); + returnReferenceArrayLambda.Execute(); + returningSpecalisedGenericArrayLambda.Execute(); + + returnPrimitiveLambdaCapture.Execute(); + returnReferenceLambdaCapture.Execute(); + returningSpecalisedGenericLambdaCapture.Execute(); + } +} diff --git a/unit/java_bytecode/java_bytecode_parser/lambda_examples/MemberLambdas.class b/unit/java_bytecode/java_bytecode_parser/lambda_examples/MemberLambdas.class new file mode 100644 index 00000000000..04984e52720 Binary files /dev/null and b/unit/java_bytecode/java_bytecode_parser/lambda_examples/MemberLambdas.class differ diff --git a/unit/java_bytecode/java_bytecode_parser/lambda_examples/MemberLambdas.java b/unit/java_bytecode/java_bytecode_parser/lambda_examples/MemberLambdas.java new file mode 100644 index 00000000000..fa7a99e358c --- /dev/null +++ b/unit/java_bytecode/java_bytecode_parser/lambda_examples/MemberLambdas.java @@ -0,0 +1,38 @@ +public class MemberLambdas { + + int memberPrimitive; + Object memberReference; + DummyGeneric memberSpecalisedGeneric; + + SimpleLambda simpleLambda = () -> { /*NOP*/ }; + ParameterLambda paramLambda = (int primitive, Object reference, DummyGeneric specalisedGeneric) -> {}; + ArrayParameterLambda arrayParamLambda = (int[] primitive, Object[] reference, DummyGeneric[] specalisedGeneric) -> {}; + ReturningLambdaPrimitive returnPrimitiveLambda = () -> { return 1; }; + ReturningLambdaReference returnReferenceLambda = () -> { return null; }; + ReturningLambdaSpecalisedGeneric returningSpecalisedGenericLambda = () -> { return null; }; + ReturningLambdaPrimitiveArray returnPrimitiveArrayLambda = () -> { return null; }; + ReturningLambdaReferenceArray returnReferenceArrayLambda = () -> { return null; }; + ReturningLambdaSpecalisedGenericArray returningSpecalisedGenericArrayLambda = () -> { return null; }; + + ReturningLambdaPrimitive returnPrimitiveLambdaCapture = () -> { return memberPrimitive; }; + ReturningLambdaReference returnReferenceLambdaCapture = () -> { return memberReference; }; + ReturningLambdaSpecalisedGeneric returningSpecalisedGenericLambdaCapture = () -> { return memberSpecalisedGeneric; }; + + + public void testMethod() { + simpleLambda.Execute(); + paramLambda.Execute(4, null, null); + arrayParamLambda.Execute(null, null, null); + returnPrimitiveLambda.Execute(); + returnReferenceLambda.Execute(); + returningSpecalisedGenericLambda.Execute(); + returnPrimitiveArrayLambda.Execute(); + returnReferenceArrayLambda.Execute(); + returningSpecalisedGenericArrayLambda.Execute(); + + returnPrimitiveLambdaCapture.Execute(); + returnReferenceLambdaCapture.Execute(); + returningSpecalisedGenericLambdaCapture.Execute(); + } +} + diff --git a/unit/java_bytecode/java_bytecode_parser/lambda_examples/OuterMemberLambdas$Inner.class b/unit/java_bytecode/java_bytecode_parser/lambda_examples/OuterMemberLambdas$Inner.class new file mode 100644 index 00000000000..19b99a98190 Binary files /dev/null and b/unit/java_bytecode/java_bytecode_parser/lambda_examples/OuterMemberLambdas$Inner.class differ diff --git a/unit/java_bytecode/java_bytecode_parser/lambda_examples/OuterMemberLambdas.class b/unit/java_bytecode/java_bytecode_parser/lambda_examples/OuterMemberLambdas.class new file mode 100644 index 00000000000..da380075695 Binary files /dev/null and b/unit/java_bytecode/java_bytecode_parser/lambda_examples/OuterMemberLambdas.class differ diff --git a/unit/java_bytecode/java_bytecode_parser/lambda_examples/OuterMemberLambdas.java b/unit/java_bytecode/java_bytecode_parser/lambda_examples/OuterMemberLambdas.java new file mode 100644 index 00000000000..e1255c0ae20 --- /dev/null +++ b/unit/java_bytecode/java_bytecode_parser/lambda_examples/OuterMemberLambdas.java @@ -0,0 +1,22 @@ +public class OuterMemberLambdas { + + int memberPrimitive; + Object memberReference; + DummyGeneric memberSpecalisedGeneric; + + public class Inner { + + ReturningLambdaPrimitive returnPrimitiveLambdaCapture = () -> { return memberPrimitive; }; + ReturningLambdaReference returnReferenceLambdaCapture = () -> { return memberReference; }; + ReturningLambdaSpecalisedGeneric returningSpecalisedGenericLambdaCapture = () -> { return memberSpecalisedGeneric; }; + + + public void testMethod() { + + returnPrimitiveLambdaCapture.Execute(); + returnReferenceLambdaCapture.Execute(); + returningSpecalisedGenericLambdaCapture.Execute(); + } + } +} + diff --git a/unit/java_bytecode/java_bytecode_parser/lambda_examples/ParameterLambda.class b/unit/java_bytecode/java_bytecode_parser/lambda_examples/ParameterLambda.class new file mode 100644 index 00000000000..9d52eef3aa7 Binary files /dev/null and b/unit/java_bytecode/java_bytecode_parser/lambda_examples/ParameterLambda.class differ diff --git a/unit/java_bytecode/java_bytecode_parser/lambda_examples/ReturningLambdaPrimitive.class b/unit/java_bytecode/java_bytecode_parser/lambda_examples/ReturningLambdaPrimitive.class new file mode 100644 index 00000000000..81073aa0155 Binary files /dev/null and b/unit/java_bytecode/java_bytecode_parser/lambda_examples/ReturningLambdaPrimitive.class differ diff --git a/unit/java_bytecode/java_bytecode_parser/lambda_examples/ReturningLambdaPrimitiveArray.class b/unit/java_bytecode/java_bytecode_parser/lambda_examples/ReturningLambdaPrimitiveArray.class new file mode 100644 index 00000000000..f9f231bc326 Binary files /dev/null and b/unit/java_bytecode/java_bytecode_parser/lambda_examples/ReturningLambdaPrimitiveArray.class differ diff --git a/unit/java_bytecode/java_bytecode_parser/lambda_examples/ReturningLambdaReference.class b/unit/java_bytecode/java_bytecode_parser/lambda_examples/ReturningLambdaReference.class new file mode 100644 index 00000000000..549084ee1a6 Binary files /dev/null and b/unit/java_bytecode/java_bytecode_parser/lambda_examples/ReturningLambdaReference.class differ diff --git a/unit/java_bytecode/java_bytecode_parser/lambda_examples/ReturningLambdaReferenceArray.class b/unit/java_bytecode/java_bytecode_parser/lambda_examples/ReturningLambdaReferenceArray.class new file mode 100644 index 00000000000..423190ffd3f Binary files /dev/null and b/unit/java_bytecode/java_bytecode_parser/lambda_examples/ReturningLambdaReferenceArray.class differ diff --git a/unit/java_bytecode/java_bytecode_parser/lambda_examples/ReturningLambdaSpecalisedGeneric.class b/unit/java_bytecode/java_bytecode_parser/lambda_examples/ReturningLambdaSpecalisedGeneric.class new file mode 100644 index 00000000000..3a82b5ddbda Binary files /dev/null and b/unit/java_bytecode/java_bytecode_parser/lambda_examples/ReturningLambdaSpecalisedGeneric.class differ diff --git a/unit/java_bytecode/java_bytecode_parser/lambda_examples/ReturningLambdaSpecalisedGenericArray.class b/unit/java_bytecode/java_bytecode_parser/lambda_examples/ReturningLambdaSpecalisedGenericArray.class new file mode 100644 index 00000000000..8e9183ed10b Binary files /dev/null and b/unit/java_bytecode/java_bytecode_parser/lambda_examples/ReturningLambdaSpecalisedGenericArray.class differ diff --git a/unit/java_bytecode/java_bytecode_parser/lambda_examples/SimpleLambda.class b/unit/java_bytecode/java_bytecode_parser/lambda_examples/SimpleLambda.class new file mode 100644 index 00000000000..ff1dae8ba4b Binary files /dev/null and b/unit/java_bytecode/java_bytecode_parser/lambda_examples/SimpleLambda.class differ diff --git a/unit/java_bytecode/java_bytecode_parser/lambda_examples/StaticLambdas.class b/unit/java_bytecode/java_bytecode_parser/lambda_examples/StaticLambdas.class new file mode 100644 index 00000000000..a5d959f5781 Binary files /dev/null and b/unit/java_bytecode/java_bytecode_parser/lambda_examples/StaticLambdas.class differ diff --git a/unit/java_bytecode/java_bytecode_parser/lambda_examples/StaticLambdas.java b/unit/java_bytecode/java_bytecode_parser/lambda_examples/StaticLambdas.java new file mode 100644 index 00000000000..697b2209f47 --- /dev/null +++ b/unit/java_bytecode/java_bytecode_parser/lambda_examples/StaticLambdas.java @@ -0,0 +1,37 @@ +public class StaticLambdas { + + static int staticPrimitive; + static Object staticReference; + static DummyGeneric staticSpecalisedGeneric; + + static SimpleLambda simpleLambda = () -> { /*NOP*/ }; + static ParameterLambda paramLambda = (int primitive, Object reference, DummyGeneric specalisedGeneric) -> {}; + static ArrayParameterLambda arrayParamLambda = (int[] primitive, Object[] reference, DummyGeneric[] specalisedGeneric) -> {}; + static ReturningLambdaPrimitive returnPrimitiveLambda = () -> { return 1; }; + static ReturningLambdaReference returnReferenceLambda = () -> { return null; }; + static ReturningLambdaSpecalisedGeneric returningSpecalisedGenericLambda = () -> { return null; }; + static ReturningLambdaPrimitiveArray returnPrimitiveArrayLambda = () -> { return null; }; + static ReturningLambdaReferenceArray returnReferenceArrayLambda = () -> { return null; }; + static ReturningLambdaSpecalisedGenericArray returningSpecalisedGenericArrayLambda = () -> { return null; }; + + static ReturningLambdaPrimitive returnPrimitiveLambdaCapture = () -> { return staticPrimitive; }; + static ReturningLambdaReference returnReferenceLambdaCapture = () -> { return staticReference; }; + static ReturningLambdaSpecalisedGeneric returningSpecalisedGenericLambdaCapture = () -> { return staticSpecalisedGeneric; }; + + + public static void testMethod() { + simpleLambda.Execute(); + paramLambda.Execute(4, null, null); + arrayParamLambda.Execute(null, null, null); + returnPrimitiveLambda.Execute(); + returnReferenceLambda.Execute(); + returningSpecalisedGenericLambda.Execute(); + returnPrimitiveArrayLambda.Execute(); + returnReferenceArrayLambda.Execute(); + returningSpecalisedGenericArrayLambda.Execute(); + + returnPrimitiveLambdaCapture.Execute(); + returnReferenceLambdaCapture.Execute(); + returningSpecalisedGenericLambdaCapture.Execute(); + } +} diff --git a/unit/testing-utils/require_parse_tree.cpp b/unit/testing-utils/require_parse_tree.cpp new file mode 100644 index 00000000000..70922d4b55a --- /dev/null +++ b/unit/testing-utils/require_parse_tree.cpp @@ -0,0 +1,117 @@ +/*******************************************************************\ + + Module: Unit test utilities + + Author: DiffBlue Limited. All rights reserved. + +\*******************************************************************/ + +#include "require_parse_tree.h" + +/// Find in the parsed class a specific entry within the +/// lambda_method_handle_map with a matching descriptor. Will fail if no +/// matching lambda entry found. +/// \param parsed_class: the class to inspect +/// \param descriptor: the descriptor the lambda method should have +/// \param entry_index: the number to skip (i.e. if multiple entries with the +/// same descriptor +/// \return +require_parse_tree::lambda_method_handlet +require_parse_tree::require_lambda_entry_for_descriptor( + const java_bytecode_parse_treet::classt &parsed_class, + const std::string &descriptor, + const size_t entry_index) +{ + REQUIRE(entry_index < parsed_class.lambda_method_handle_map.size()); + typedef java_bytecode_parse_treet::classt::lambda_method_handle_mapt:: + value_type lambda_method_entryt; + + size_t matches_found = 0; + + const auto matching_lambda_entry = std::find_if( + parsed_class.lambda_method_handle_map.begin(), + parsed_class.lambda_method_handle_map.end(), + [&descriptor, &matches_found, &entry_index]( + const lambda_method_entryt &entry) { + if(entry.second.method_type == descriptor) + { + ++matches_found; + return matches_found == entry_index + 1; + } + return false; + }); + + INFO("Looking for descriptor: " << descriptor); + std::ostringstream found_entries; + for(const auto entry : parsed_class.lambda_method_handle_map) + { + found_entries << id2string(entry.first.first) << ": " + << id2string(entry.second.method_type) << std::endl; + } + INFO("Found descriptors:\n" << found_entries.str()); + + REQUIRE(matching_lambda_entry != parsed_class.lambda_method_handle_map.end()); + + return matching_lambda_entry->second; +} + +/// Finds a specific method in the parsed class with a matching name. +/// \param parsed_class: The class +/// \param method_name: The name of the method to look for +/// \return The methodt structure with the corresponding name +const require_parse_tree::methodt require_parse_tree::require_method( + const java_bytecode_parse_treet::classt &parsed_class, + const irep_idt &method_name) +{ + const auto method = std::find_if( + parsed_class.methods.begin(), + parsed_class.methods.end(), + [&method_name](const java_bytecode_parse_treet::methodt &method) { + return method.name == method_name; + }); + + INFO("Looking for method: " << method_name); + std::ostringstream found_methods; + for(const auto entry : parsed_class.methods) + { + found_methods << id2string(entry.name) << std::endl; + } + INFO("Found methods:\n" << found_methods.str()); + + REQUIRE(method != parsed_class.methods.end()); + + return *method; +} + +/// Verify whether a given methods instructions match an expectation +/// \param expected_instructions: The expected instructions for a given method +/// \param instructions: The instructions of a method +void require_parse_tree::require_instructions_match_expectation( + const expected_instructionst &expected_instructions, + const java_bytecode_parse_treet::methodt::instructionst instructions) +{ + REQUIRE(instructions.size() == expected_instructions.size()); + auto actual_instruction_it = instructions.begin(); + for(const auto expected_instruction : expected_instructions) + { + expected_instruction.require_instructions_equal(*actual_instruction_it); + ++actual_instruction_it; + } +} + +/// Check whether a given instruction matches an expectation of the instruction +/// \param actual_instruction: The instruction to check +void require_parse_tree::expected_instructiont::require_instructions_equal( + java_bytecode_parse_treet::instructiont actual_instruction) const +{ + REQUIRE(actual_instruction.statement == instruction_mnemoic); + REQUIRE(actual_instruction.args.size() == instruction_arguments.size()); + auto actual_arg_it = actual_instruction.args.begin(); + for(const exprt &expected_arg : actual_instruction.args) + { + INFO("Expected argument" << expected_arg.pretty()); + INFO("Actual argument" << actual_arg_it->pretty()); + REQUIRE(*actual_arg_it == expected_arg); + ++actual_arg_it; + } +} diff --git a/unit/testing-utils/require_parse_tree.h b/unit/testing-utils/require_parse_tree.h new file mode 100644 index 00000000000..35b3ab195d2 --- /dev/null +++ b/unit/testing-utils/require_parse_tree.h @@ -0,0 +1,60 @@ +/*******************************************************************\ + + Module: Unit test utilities + + Author: DiffBlue Limited. All rights reserved. + +\*******************************************************************/ + +/// \file +/// Utilties for inspecting java_parse_treet + +#ifndef CPROVER_TESTING_UTILS_REQUIRE_PARSE_TREE_H +#define CPROVER_TESTING_UTILS_REQUIRE_PARSE_TREE_H + +#include +#include "catch.hpp" + +// NOLINTNEXTLINE(readability/namespace) +namespace require_parse_tree +{ +typedef java_bytecode_parse_treet::classt::lambda_method_handlet + lambda_method_handlet; + +lambda_method_handlet require_lambda_entry_for_descriptor( + const java_bytecode_parse_treet::classt &parsed_class, + const std::string &descriptor, + const size_t entry_index = 0); + +typedef java_bytecode_parse_treet::methodt methodt; + +const methodt require_method( + const java_bytecode_parse_treet::classt &parsed_class, + const irep_idt &method_name); + +struct expected_instructiont +{ + expected_instructiont( + const irep_idt &instruction_mnemoic, + const std::vector &instruction_arguments) + : instruction_mnemoic(instruction_mnemoic), + instruction_arguments(instruction_arguments) + { + } + + void require_instructions_equal( + java_bytecode_parse_treet::instructiont actual_instruction) const; + +private: + const irep_idt instruction_mnemoic; + const std::vector instruction_arguments; +}; + +typedef std::vector expected_instructionst; + +void require_instructions_match_expectation( + const expected_instructionst &expected_instructions, + const java_bytecode_parse_treet::methodt::instructionst instructions); +} + +#endif //CPROVER_TESTING_UTILS_REQUIRE_PARSE_TREE_H