diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp index 6200190276f..d370672d76f 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp @@ -303,6 +303,7 @@ void java_bytecode_convert_classt::convert( } class_type.set_tag(c.name); + class_type.set_inner_name(c.inner_name); class_type.set(ID_abstract, c.is_abstract); class_type.set(ID_is_annotation, c.is_annotation); class_type.set(ID_interface, c.is_interface); diff --git a/jbmc/src/java_bytecode/java_bytecode_parse_tree.h b/jbmc/src/java_bytecode/java_bytecode_parse_tree.h index 9a9fe8c0c20..5efbfcc22f5 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parse_tree.h +++ b/jbmc/src/java_bytecode/java_bytecode_parse_tree.h @@ -213,7 +213,7 @@ struct java_bytecode_parse_treet classt &operator=(classt &&) = default; #endif - irep_idt name, super_class; + irep_idt name, super_class, inner_name; bool is_abstract=false; bool is_enum=false; bool is_public=false, is_protected=false, is_private=false; diff --git a/jbmc/src/java_bytecode/java_bytecode_parser.cpp b/jbmc/src/java_bytecode/java_bytecode_parser.cpp index 2c7f8f4eb2b..c6ed74717d8 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parser.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_parser.cpp @@ -1696,6 +1696,8 @@ void java_bytecode_parsert::rinner_classes_attribute( // This is a marker that a class is anonymous. if(inner_name_index == 0) parsed_class.is_anonymous_class = true; + else + parsed_class.inner_name = pool_entry_lambda(inner_name_index).s; // Note that if outer_class_info_index == 0, the inner class is an anonymous // or local class, and is treated as private. if(outer_class_info_index == 0) diff --git a/jbmc/src/java_bytecode/java_types.h b/jbmc/src/java_bytecode/java_types.h index 0fa28f8cdf1..9319c918255 100644 --- a/jbmc/src/java_bytecode/java_types.h +++ b/jbmc/src/java_bytecode/java_types.h @@ -241,6 +241,18 @@ class java_class_typet:public class_typet { set(ID_name, name); } + + /// Get the name of a java inner class. + const irep_idt &get_inner_name() const + { + return get(ID_inner_name); + } + + /// Set the name of a java inner class. + void set_inner_name(const irep_idt &name) + { + set(ID_inner_name, name); + } }; inline const java_class_typet &to_java_class_type(const typet &type) diff --git a/jbmc/unit/Makefile b/jbmc/unit/Makefile index f569358baae..d1e009b831c 100644 --- a/jbmc/unit/Makefile +++ b/jbmc/unit/Makefile @@ -38,6 +38,7 @@ SRC += java_bytecode/ci_lazy_methods/lazy_load_lambdas.cpp \ java_bytecode/java_bytecode_parse_lambdas/java_bytecode_convert_class_lambda_method_handles.cpp \ java_bytecode/java_bytecode_parse_lambdas/java_bytecode_parse_lambda_method_table.cpp \ java_bytecode/java_bytecode_parser/parse_class_without_instructions.cpp \ + java_bytecode/java_bytecode_parser/parse_inner_class.cpp \ java_bytecode/java_bytecode_parser/parse_java_annotations.cpp \ java_bytecode/java_bytecode_parser/parse_java_attributes.cpp \ java_bytecode/java_bytecode_parser/parse_java_class.cpp \ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/Outer$1.class b/jbmc/unit/java_bytecode/java_bytecode_parser/Outer$1.class new file mode 100644 index 00000000000..2e2d935ee62 Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/Outer$1.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/Outer$Inner.class b/jbmc/unit/java_bytecode/java_bytecode_parser/Outer$Inner.class new file mode 100644 index 00000000000..182f2dcd1e6 Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/Outer$Inner.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/Outer$RedHerring.class b/jbmc/unit/java_bytecode/java_bytecode_parser/Outer$RedHerring.class new file mode 100644 index 00000000000..185cd39a7a6 Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/Outer$RedHerring.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/Outer$RedHerring.java b/jbmc/unit/java_bytecode/java_bytecode_parser/Outer$RedHerring.java new file mode 100644 index 00000000000..a12d8e0f858 --- /dev/null +++ b/jbmc/unit/java_bytecode/java_bytecode_parser/Outer$RedHerring.java @@ -0,0 +1,2 @@ +class Outer$RedHerring { +} diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/Outer.class b/jbmc/unit/java_bytecode/java_bytecode_parser/Outer.class new file mode 100644 index 00000000000..7e7b1ab9a4b Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/Outer.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/Outer.java b/jbmc/unit/java_bytecode/java_bytecode_parser/Outer.java new file mode 100644 index 00000000000..4842cf0e2c8 --- /dev/null +++ b/jbmc/unit/java_bytecode/java_bytecode_parser/Outer.java @@ -0,0 +1,7 @@ +class Outer { + class Inner { + } + + Outer anonymous = new Outer() { + }; +} diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/parse_inner_class.cpp b/jbmc/unit/java_bytecode/java_bytecode_parser/parse_inner_class.cpp new file mode 100644 index 00000000000..e6a4d11a525 --- /dev/null +++ b/jbmc/unit/java_bytecode/java_bytecode_parser/parse_inner_class.cpp @@ -0,0 +1,143 @@ +/*******************************************************************\ + + Module: Unit tests for converting inner classes + + Author: Diffblue Ltd. + +\*******************************************************************/ + +#include +#include +#include + +#include +#include + +SCENARIO( + "Parsing inner java classes", + "[core][java_bytecode][java_bytecode_parser]") +{ + for(const auto &load_first : std::vector{"Outer$Inner", "Outer"}) + { + const symbol_tablet &symbol_table = + load_java_class(load_first, "./java_bytecode/java_bytecode_parser"); + + GIVEN("A class file of an inner class and " + load_first + " loaded first.") + { + WHEN("Parsing an inner class called \"Inner\".") + { + const symbolt *class_symbol = symbol_table.lookup("java::Outer$Inner"); + REQUIRE(class_symbol); + const java_class_typet *class_type = + type_try_dynamic_cast(class_symbol->type); + REQUIRE(class_type); + + THEN("The inner class should have the name \"java::Outer$Inner\".") + { + REQUIRE(id2string(class_type->get_name()) == "java::Outer$Inner"); + } + THEN("The inner class should have the inner name \"Inner\".") + { + REQUIRE(id2string(class_type->get_inner_name()) == "Inner"); + } + THEN("The inner class is not considered to be an anonymous class.") + { + REQUIRE_FALSE(class_type->get_is_anonymous_class()); + } + THEN("The inner class has the outer class \"Outer\".") + { + REQUIRE(id2string(class_type->get_outer_class()) == "Outer"); + } + } + } + GIVEN( + "A class file of a class which is not an inner class and " + load_first + + " loaded first.") + { + WHEN("Parsing an outer class.") + { + const symbolt *class_symbol = symbol_table.lookup("java::Outer"); + REQUIRE(class_symbol); + const java_class_typet *class_type = + type_try_dynamic_cast(class_symbol->type); + REQUIRE(class_type); + + THEN("The outer class should have the name \"java::Outer\".") + { + REQUIRE(id2string(class_type->get_name()) == "java::Outer"); + } + THEN("The outer class should not have an inner name.") + { + REQUIRE(id2string(class_type->get_inner_name()).empty()); + } + THEN("The outer class is not considered to be an anonymous class.") + { + REQUIRE_FALSE(class_type->get_is_anonymous_class()); + } + THEN("The outer class does not have an outer class.") + { + REQUIRE(id2string(class_type->get_outer_class()).empty()); + } + } + } + GIVEN( + "A class file of an anonymous class and " + load_first + " loaded first.") + { + WHEN("Parsing an anonymous class.") + { + const symbolt *class_symbol = symbol_table.lookup("java::Outer$1"); + REQUIRE(class_symbol); + const java_class_typet *class_type = + type_try_dynamic_cast(class_symbol->type); + REQUIRE(class_type); + + THEN("The anonymous class should have the name \"java::Outer$1\".") + { + REQUIRE(id2string(class_type->get_name()) == "java::Outer$1"); + } + THEN("The anonymous class should not have an inner name.") + { + REQUIRE(id2string(class_type->get_inner_name()).empty()); + } + THEN("The anonymous class is considered to be an anonymous class.") + { + REQUIRE(class_type->get_is_anonymous_class()); + } + THEN("The anonymous class does not have an outer class.") + { + REQUIRE(id2string(class_type->get_outer_class()).empty()); + } + } + } + } + GIVEN("A class file of an outer class which is named with a '$'.") + { + WHEN("Parsing an outer class named with a '$'.") + { + const symbol_tablet &symbol_table = load_java_class( + "Outer$RedHerring", "./java_bytecode/java_bytecode_parser"); + const auto *class_symbol = symbol_table.lookup("java::Outer$RedHerring"); + REQUIRE(class_symbol); + const java_class_typet *class_type = + type_try_dynamic_cast(class_symbol->type); + REQUIRE(class_type); + + THEN("The outer class should have the name \"java::Outer$RedHerring\".") + { + REQUIRE(id2string(class_type->get_name()) == "java::Outer$RedHerring"); + } + THEN("The outer class should not have an inner name.") + { + REQUIRE(id2string(class_type->get_inner_name()).empty()); + } + THEN("The inner class is not considered to be an anonymous class.") + { + REQUIRE_FALSE(class_type->get_is_anonymous_class()); + } + THEN("The outer class does not have an outer class.") + { + REQUIRE(id2string(class_type->get_outer_class()).empty()); + } + } + } +} diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index 190f892d725..2fdfad6e5a8 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -131,6 +131,7 @@ IREP_ID_ONE(incomplete_c_enum) IREP_ID_TWO(C_incomplete, #incomplete) IREP_ID_ONE(identifier) IREP_ID_ONE(name) +IREP_ID_ONE(inner_name) IREP_ID_ONE(cpp_name) IREP_ID_ONE(component_cpp_name) IREP_ID_TWO(C_id_class, #id_class)