diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp index 9f3ff3d7744..3a74e264b55 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp @@ -268,6 +268,7 @@ void java_bytecode_convert_classt::convert( class_type.set(ID_interface, c.is_interface); class_type.set(ID_synthetic, c.is_synthetic); class_type.set_final(c.is_final); + class_type.set_is_inner_class(c.is_inner_class); if(c.is_enum) { if(max_array_length != 0 && c.enum_elements > max_array_length) diff --git a/jbmc/src/java_bytecode/java_bytecode_parse_tree.h b/jbmc/src/java_bytecode/java_bytecode_parse_tree.h index c5762137152..d663a669c63 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parse_tree.h +++ b/jbmc/src/java_bytecode/java_bytecode_parse_tree.h @@ -212,6 +212,7 @@ class java_bytecode_parse_treet bool is_interface = false; bool is_synthetic = false; bool is_annotation = false; + bool is_inner_class = false; bool attribute_bootstrapmethods_read = false; size_t enum_elements=0; diff --git a/jbmc/src/java_bytecode/java_bytecode_parser.cpp b/jbmc/src/java_bytecode/java_bytecode_parser.cpp index 9553e3a4544..53b69181fe2 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parser.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_parser.cpp @@ -119,6 +119,8 @@ class java_bytecode_parsert:public parsert void rfields(classt &parsed_class); void rmethods(classt &parsed_class); void rmethod(classt &parsed_class); + void + rinner_classes_attribute(classt &parsed_class, const u4 &attribute_length); void rclass_attribute(classt &parsed_class); void rRuntimeAnnotation_attribute(annotationst &); void rRuntimeAnnotation(annotationt &); @@ -1576,6 +1578,77 @@ void java_bytecode_parsert::relement_value_pair( } } +/// Corresponds to the element_value structure +/// Described in Java 8 specification 4.7.6 +/// https://docs.oracle.com/javase/specs/jvms/se8/html/jvms-4.html#jvms-4.7.6 +/// Parses the InnerClasses attribute for the current parsed class, +/// which contains an array of information about its inner classes. We are +/// interested in getting information only for inner classes, which is +/// determined by checking if the parsed class matches any of the inner classes +/// in its inner class array. If the parsed class is not an inner class, then it +/// is ignored. When a parsed class is an inner class, the accessibility +/// information for the parsed class is overwritten, and the parsed class is +/// marked as an inner class. +void java_bytecode_parsert::rinner_classes_attribute( + classt &parsed_class, + const u4 &attribute_length) +{ + std::string name = parsed_class.name.c_str(); + u2 number_of_classes = read_u2(); + u4 number_of_bytes_to_be_read = number_of_classes * 8 + 2; + INVARIANT( + number_of_bytes_to_be_read == attribute_length, + "The number of bytes to be read for the InnerClasses attribute does not " + "match the attribute length."); + + const auto pool_entry_lambda = [this](u2 index) -> pool_entryt & { + return pool_entry(index); + }; + const auto remove_separator_char = [](std::string str, char ch) { + str.erase(std::remove(str.begin(), str.end(), ch), str.end()); + return str; + }; + + for(int i = 0; i < number_of_classes; i++) + { + u2 inner_class_info_index = read_u2(); + u2 outer_class_info_index = read_u2(); + UNUSED u2 inner_name_index = read_u2(); + u2 inner_class_access_flags = read_u2(); + + std::string inner_class_info_name = + class_infot(pool_entry(inner_class_info_index)) + .get_name(pool_entry_lambda); + bool is_private = (inner_class_access_flags & ACC_PRIVATE) != 0; + bool is_public = (inner_class_access_flags & ACC_PUBLIC) != 0; + bool is_protected = (inner_class_access_flags & ACC_PROTECTED) != 0; + + // If the original parsed class name matches the inner class name, + // the parsed class is an inner class, so overwrite the parsed class' + // access information and mark it as an inner class. + bool is_inner_class = remove_separator_char(id2string(parsed_class.name), '.') == + remove_separator_char(inner_class_info_name, '/'); + if(is_inner_class) + parsed_class.is_inner_class = is_inner_class; + if(!is_inner_class) + continue; + // 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) + { + parsed_class.is_private = true; + parsed_class.is_protected = false; + parsed_class.is_public = false; + } + else + { + parsed_class.is_private = is_private; + parsed_class.is_protected = is_protected; + parsed_class.is_public = is_public; + } + } +} + void java_bytecode_parsert::rclass_attribute(classt &parsed_class) { u2 attribute_name_index=read_u2(); @@ -1640,6 +1713,11 @@ void java_bytecode_parsert::rclass_attribute(classt &parsed_class) parsed_class.attribute_bootstrapmethods_read = true; read_bootstrapmethods_entry(parsed_class); } + else if(attribute_name == "InnerClasses") + { + java_bytecode_parsert::rinner_classes_attribute( + parsed_class, attribute_length); + } else skip_bytes(attribute_length); } diff --git a/jbmc/src/java_bytecode/java_types.h b/jbmc/src/java_bytecode/java_types.h index ed2750317f9..1a8579f3b69 100644 --- a/jbmc/src/java_bytecode/java_types.h +++ b/jbmc/src/java_bytecode/java_types.h @@ -111,6 +111,16 @@ class java_class_typet:public class_typet return set(ID_access, access); } + const bool get_is_inner_class() const + { + return get_bool(ID_is_inner_class); + } + + void set_is_inner_class(const bool &is_inner_class) + { + return set(ID_is_inner_class, is_inner_class); + } + bool get_final() { return get_bool(ID_final); diff --git a/jbmc/unit/Makefile b/jbmc/unit/Makefile index 741ff87c8ff..4c04bf031ee 100644 --- a/jbmc/unit/Makefile +++ b/jbmc/unit/Makefile @@ -12,6 +12,7 @@ SRC += java_bytecode/goto-programs/class_hierarchy_output.cpp \ java_bytecode/java_bytecode_convert_class/convert_java_annotations.cpp \ java_bytecode/java_bytecode_convert_method/convert_invoke_dynamic.cpp \ java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp \ + java_bytecode/java_bytecode_parser/parse_java_attributes.cpp \ java_bytecode/java_object_factory/gen_nondet_string_init.cpp \ java_bytecode/java_bytecode_parse_lambdas/java_bytecode_parse_lambda_method_table.cpp \ java_bytecode/java_bytecode_parse_lambdas/java_bytecode_convert_class_lambda_method_handles.cpp \ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass$1.class b/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass$1.class new file mode 100644 index 00000000000..dc41102018b Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass$1.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass$2.class b/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass$2.class new file mode 100644 index 00000000000..502987e5162 Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass$2.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass$3.class b/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass$3.class new file mode 100644 index 00000000000..80d5d4a52ae Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass$3.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass$4.class b/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass$4.class new file mode 100644 index 00000000000..d215c74a240 Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass$4.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass$InnerInterface.class b/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass$InnerInterface.class new file mode 100644 index 00000000000..6914c2338db Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass$InnerInterface.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass.class new file mode 100644 index 00000000000..eafeaf17b03 Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsLocalClass$1LocalClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsLocalClass$1LocalClass.class new file mode 100644 index 00000000000..2d58f305b14 Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsLocalClass$1LocalClass.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsLocalClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsLocalClass.class new file mode 100644 index 00000000000..40be03e68ea Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsLocalClass.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClasses$DefaultInnerClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClasses$DefaultInnerClass.class new file mode 100644 index 00000000000..4170d0b67a9 Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClasses$DefaultInnerClass.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClasses$PrivateInnerClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClasses$PrivateInnerClass.class new file mode 100644 index 00000000000..b17f91da63c Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClasses$PrivateInnerClass.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClasses$ProtectedInnerClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClasses$ProtectedInnerClass.class new file mode 100644 index 00000000000..7a8ae4aefa3 Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClasses$ProtectedInnerClass.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClasses$PublicInnerClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClasses$PublicInnerClass.class new file mode 100644 index 00000000000..a5f5c2b47c3 Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClasses$PublicInnerClass.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClasses.class b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClasses.class new file mode 100644 index 00000000000..0d9ad31914f Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClasses.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClasses.java b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClasses.java new file mode 100644 index 00000000000..7b4792fa26a --- /dev/null +++ b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClasses.java @@ -0,0 +1,115 @@ +public class InnerClasses { + public class PublicInnerClass { + public int i; + public PublicInnerClass(int i) { + this.i = i; + } + } + class DefaultInnerClass { + int i; + DefaultInnerClass(int i) { + this.i = i; + } + } + protected class ProtectedInnerClass { + protected int i; + protected ProtectedInnerClass(int i) { + this.i = i; + } + } + private class PrivateInnerClass { + private int i; + private PrivateInnerClass(int i) { + this.i = i; + } + } +} + +class InnerClassesDefault { + public class PublicInnerClass { + public int i; + public PublicInnerClass(int i) { + this.i = i; + } + } + class DefaultInnerClass { + int i; + DefaultInnerClass(int i) { + this.i = i; + } + } + protected class ProtectedInnerClass { + protected int i; + protected ProtectedInnerClass(int i) { + this.i = i; + } + } + private class PrivateInnerClass { + private int i; + private PrivateInnerClass(int i) { + this.i = i; + } + } +} + +class InnerClassesDeeplyNested { + class SinglyNestedClass { + int i; + SinglyNestedClass(int i) { + this.i = i; + } + public class PublicDoublyNestedInnerClass { + public int i; + public PublicDoublyNestedInnerClass(int i) { + this.i = i; + } + } + class DefaultDoublyNestedInnerClass { + int i; + DefaultDoublyNestedInnerClass(int i) { + this.i = i; + } + } + protected class ProtectedDoublyNestedInnerClass { + protected int i; + protected ProtectedDoublyNestedInnerClass(int i) { + this.i = i; + } + } + private class PrivateDoublyNestedInnerClass { + private int i; + private PrivateDoublyNestedInnerClass(int i) { + this.i = i; + } + } + } +} + +class ContainsAnonymousClass { + interface InnerInterface { + int i = 0; + } + public InnerInterface anonymousPublic = new InnerInterface() { + int i = 1; + }; + InnerInterface anonymousDefault = new InnerInterface() { + int i = 2; + }; + protected InnerInterface anonymousProtected = new InnerInterface() { + int i = 3; + }; + private InnerInterface anonymousPrivate = new InnerInterface() { + int i = 4; + }; +} + +class ContainsLocalClass { + public void test() { + class LocalClass { + int i = 55; + LocalClass(int i) { + this.i = i; + } + } + } +} diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDeeplyNested$SinglyNestedClass$DefaultDoublyNestedInnerClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDeeplyNested$SinglyNestedClass$DefaultDoublyNestedInnerClass.class new file mode 100644 index 00000000000..55ee343fcc8 Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDeeplyNested$SinglyNestedClass$DefaultDoublyNestedInnerClass.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDeeplyNested$SinglyNestedClass$PrivateDoublyNestedInnerClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDeeplyNested$SinglyNestedClass$PrivateDoublyNestedInnerClass.class new file mode 100644 index 00000000000..07f49f71e44 Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDeeplyNested$SinglyNestedClass$PrivateDoublyNestedInnerClass.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDeeplyNested$SinglyNestedClass$ProtectedDoublyNestedInnerClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDeeplyNested$SinglyNestedClass$ProtectedDoublyNestedInnerClass.class new file mode 100644 index 00000000000..3e316106695 Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDeeplyNested$SinglyNestedClass$ProtectedDoublyNestedInnerClass.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDeeplyNested$SinglyNestedClass$PublicDoublyNestedInnerClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDeeplyNested$SinglyNestedClass$PublicDoublyNestedInnerClass.class new file mode 100644 index 00000000000..26929198050 Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDeeplyNested$SinglyNestedClass$PublicDoublyNestedInnerClass.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDeeplyNested$SinglyNestedClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDeeplyNested$SinglyNestedClass.class new file mode 100644 index 00000000000..0baab876049 Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDeeplyNested$SinglyNestedClass.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDeeplyNested.class b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDeeplyNested.class new file mode 100644 index 00000000000..38ae4c2b9cb Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDeeplyNested.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDefault$DefaultInnerClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDefault$DefaultInnerClass.class new file mode 100644 index 00000000000..963ceb186cf Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDefault$DefaultInnerClass.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDefault$PrivateInnerClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDefault$PrivateInnerClass.class new file mode 100644 index 00000000000..6961af273b8 Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDefault$PrivateInnerClass.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDefault$ProtectedInnerClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDefault$ProtectedInnerClass.class new file mode 100644 index 00000000000..80306a39a33 Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDefault$ProtectedInnerClass.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDefault$PublicInnerClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDefault$PublicInnerClass.class new file mode 100644 index 00000000000..77340e82c70 Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDefault$PublicInnerClass.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDefault.class b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDefault.class new file mode 100644 index 00000000000..fd18bd4c3c5 Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClassesDefault.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_attributes.cpp b/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_attributes.cpp new file mode 100644 index 00000000000..737ad516577 --- /dev/null +++ b/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_attributes.cpp @@ -0,0 +1,269 @@ +/*******************************************************************\ + + Module: Unit tests for converting annotations + + Author: Diffblue Ltd. + +\*******************************************************************/ + +#include +#include +#include +#include +#include + +SCENARIO( + "java_bytecode_parse_attributes", + "[core][java_bytecode][java_bytecode_parser]") +{ + GIVEN("Some public class files in the class path with inner classes") + { + const symbol_tablet &new_symbol_table = + load_java_class("InnerClasses", "./java_bytecode/java_bytecode_parser"); + WHEN("Parsing the InnerClasses attribute for a public inner class") + { + THEN("The class should be marked as public") + { + const symbolt &class_symbol = + new_symbol_table.lookup_ref("java::InnerClasses$PublicInnerClass"); + const java_class_typet java_class = + to_java_class_type(class_symbol.type); + REQUIRE(java_class.get_is_inner_class()); + REQUIRE(java_class.get_access() == ID_public); + } + } + WHEN("Parsing the InnerClasses attribute for a package private inner class") + { + THEN("The class should be marked as default") + { + const symbolt &class_symbol = + new_symbol_table.lookup_ref("java::InnerClasses$DefaultInnerClass"); + const java_class_typet java_class = + to_java_class_type(class_symbol.type); + REQUIRE(java_class.get_is_inner_class()); + REQUIRE(java_class.get_access() == ID_default); + } + } + WHEN("Parsing the InnerClasses attribute for a protected inner class") + { + THEN("The class should be marked as protected") + { + const symbolt &class_symbol = + new_symbol_table.lookup_ref("java::InnerClasses$ProtectedInnerClass"); + const java_class_typet java_class = + to_java_class_type(class_symbol.type); + REQUIRE(java_class.get_is_inner_class()); + REQUIRE(java_class.get_access() == ID_protected); + } + } + WHEN("Parsing the InnerClasses attribute for a private inner class") + { + THEN("The class should be marked as private") + { + const symbolt &class_symbol = + new_symbol_table.lookup_ref("java::InnerClasses$PrivateInnerClass"); + const java_class_typet java_class = + to_java_class_type(class_symbol.type); + REQUIRE(java_class.get_is_inner_class()); + REQUIRE(java_class.get_access() == ID_private); + } + } + } + GIVEN("Some package-private class files in the class path with inner classes") + { + const symbol_tablet &new_symbol_table = load_java_class( + "InnerClassesDefault", "./java_bytecode/java_bytecode_parser"); + WHEN("Parsing the InnerClasses attribute for a public inner class") + { + THEN("The class should be marked as public") + { + const symbolt &class_symbol = new_symbol_table.lookup_ref( + "java::InnerClassesDefault$PublicInnerClass"); + const java_class_typet java_class = + to_java_class_type(class_symbol.type); + REQUIRE(java_class.get_is_inner_class()); + REQUIRE(java_class.get_access() == ID_public); + } + } + WHEN("Parsing the InnerClasses attribute for a package private inner class") + { + THEN("The class should be marked as default") + { + const symbolt &class_symbol = new_symbol_table.lookup_ref( + "java::InnerClassesDefault$DefaultInnerClass"); + const java_class_typet java_class = + to_java_class_type(class_symbol.type); + REQUIRE(java_class.get_is_inner_class()); + REQUIRE(java_class.get_access() == ID_default); + } + } + WHEN("Parsing the InnerClasses attribute for a protected inner class") + { + THEN("The class should be marked as protected") + { + const symbolt &class_symbol = new_symbol_table.lookup_ref( + "java::InnerClassesDefault$ProtectedInnerClass"); + const java_class_typet java_class = + to_java_class_type(class_symbol.type); + REQUIRE(java_class.get_is_inner_class()); + REQUIRE(java_class.get_access() == ID_protected); + } + } + WHEN("Parsing the InnerClasses attribute for a private inner class") + { + THEN("The class should be marked as private") + { + const symbolt &class_symbol = new_symbol_table.lookup_ref( + "java::InnerClassesDefault$PrivateInnerClass"); + const java_class_typet java_class = + to_java_class_type(class_symbol.type); + REQUIRE(java_class.get_is_inner_class()); + REQUIRE(java_class.get_access() == ID_private); + } + } + } + + GIVEN( + "Some package-private class files in the class path with deeply nested " + "inner classes") + { + const symbol_tablet &new_symbol_table = load_java_class( + "InnerClassesDeeplyNested", "./java_bytecode/java_bytecode_parser"); + WHEN( + "Parsing the InnerClasses attribute for a public doubly-nested inner " + "class") + { + THEN("The class should be marked as public") + { + const symbolt &class_symbol = new_symbol_table.lookup_ref( + "java::InnerClassesDeeplyNested$SinglyNestedClass$" + "PublicDoublyNestedInnerClass"); + const java_class_typet java_class = + to_java_class_type(class_symbol.type); + REQUIRE(java_class.get_is_inner_class()); + REQUIRE(java_class.get_access() == ID_public); + } + } + WHEN( + "Parsing the InnerClasses attribute for a package private doubly-nested " + "inner class") + { + THEN("The class should be marked as default") + { + const symbolt &class_symbol = new_symbol_table.lookup_ref( + "java::InnerClassesDeeplyNested$SinglyNestedClass$" + "DefaultDoublyNestedInnerClass"); + const java_class_typet java_class = + to_java_class_type(class_symbol.type); + REQUIRE(java_class.get_is_inner_class()); + REQUIRE(java_class.get_access() == ID_default); + } + } + WHEN( + "Parsing the InnerClasses attribute for a protected doubly-nested inner " + "class") + { + THEN("The class should be marked as protected") + { + const symbolt &class_symbol = new_symbol_table.lookup_ref( + "java::InnerClassesDeeplyNested$SinglyNestedClass$" + "ProtectedDoublyNestedInnerClass"); + const java_class_typet java_class = + to_java_class_type(class_symbol.type); + REQUIRE(java_class.get_is_inner_class()); + REQUIRE(java_class.get_access() == ID_protected); + } + } + WHEN( + "Parsing the InnerClasses attribute for a private doubly-nested inner " + "class") + { + THEN("The class should be marked as private") + { + const symbolt &class_symbol = new_symbol_table.lookup_ref( + "java::InnerClassesDeeplyNested$SinglyNestedClass$" + "PrivateDoublyNestedInnerClass"); + const java_class_typet java_class = + to_java_class_type(class_symbol.type); + REQUIRE(java_class.get_is_inner_class()); + REQUIRE(java_class.get_access() == ID_private); + } + } + } + + GIVEN( + "Some package-private class files in the class path with anonymous classes") + { + const symbol_tablet &new_symbol_table = load_java_class( + "ContainsAnonymousClass", "./java_bytecode/java_bytecode_parser"); + WHEN("Parsing the InnerClasses attribute for a public anonymous class") + { + THEN("The class should be marked as public") + { + const symbolt &class_symbol = + new_symbol_table.lookup_ref("java::ContainsAnonymousClass$1"); + const java_class_typet java_class = + to_java_class_type(class_symbol.type); + REQUIRE(java_class.get_is_inner_class()); + REQUIRE(java_class.get_access() == ID_private); + } + } + WHEN( + "Parsing the InnerClasses attribute for a package-private anonymous " + "class") + { + THEN("The class should be marked as default") + { + const symbolt &class_symbol = + new_symbol_table.lookup_ref("java::ContainsAnonymousClass$2"); + const java_class_typet java_class = + to_java_class_type(class_symbol.type); + REQUIRE(java_class.get_is_inner_class()); + REQUIRE(java_class.get_access() == ID_private); + } + } + WHEN("Parsing the InnerClasses attribute for a protected anonymous class") + { + THEN("The class should be marked as protected") + { + const symbolt &class_symbol = + new_symbol_table.lookup_ref("java::ContainsAnonymousClass$3"); + const java_class_typet java_class = + to_java_class_type(class_symbol.type); + REQUIRE(java_class.get_is_inner_class()); + REQUIRE(java_class.get_access() == ID_private); + } + } + WHEN("Parsing the InnerClasses attribute for a private anonymous class") + { + THEN("The class should be marked as private") + { + const symbolt &class_symbol = + new_symbol_table.lookup_ref("java::ContainsAnonymousClass$4"); + const java_class_typet java_class = + to_java_class_type(class_symbol.type); + REQUIRE(java_class.get_is_inner_class()); + REQUIRE(java_class.get_access() == ID_private); + } + } + } + + GIVEN( + "Some package-private class files in the class path with local classes ") + { + const symbol_tablet &new_symbol_table = load_java_class( + "ContainsLocalClass", "./java_bytecode/java_bytecode_parser"); + WHEN("Parsing the InnerClasses attribute for a package-private class ") + { + THEN("The class should be marked as package-private") + { + const symbolt &class_symbol = + new_symbol_table.lookup_ref("java::ContainsLocalClass$1LocalClass"); + const java_class_typet java_class = + to_java_class_type(class_symbol.type); + REQUIRE(java_class.get_is_inner_class()); + REQUIRE(java_class.get_access() == ID_private); + } + } + } +} diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index 05e84f1d9f2..a374a101b86 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -674,6 +674,7 @@ IREP_ID_ONE(interface) IREP_ID_TWO(C_must_not_throw, #must_not_throw) IREP_ID_ONE(always_inline) IREP_ID_ONE(is_always_inline) +IREP_ID_ONE(is_inner_class) // Projects depending on this code base that wish to extend the list of // available ids should provide a file local_irep_ids.h in their source tree and