diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp index f00a0bfb17c..36ad3bff30d 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp @@ -279,6 +279,7 @@ void java_bytecode_convert_classt::convert( class_type.set_is_inner_class(c.is_inner_class); class_type.set_is_static_class(c.is_static_class); class_type.set_is_anonymous_class(c.is_anonymous_class); + class_type.set_outer_class(c.outer_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 431dd4804f5..29b3bb056a5 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parse_tree.h +++ b/jbmc/src/java_bytecode/java_bytecode_parse_tree.h @@ -221,6 +221,7 @@ class java_bytecode_parse_treet bool is_static_class = false; bool is_anonymous_class = false; bool attribute_bootstrapmethods_read = false; + irep_idt outer_class; // when no outer class is set, there is no outer class size_t enum_elements=0; enum class method_handle_typet diff --git a/jbmc/src/java_bytecode/java_bytecode_parser.cpp b/jbmc/src/java_bytecode/java_bytecode_parser.cpp index 8bcb491939e..0ac957a849b 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parser.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_parser.cpp @@ -1643,6 +1643,11 @@ void java_bytecode_parsert::rinner_classes_attribute( } else { + std::string outer_class_info_name = + class_infot(pool_entry(outer_class_info_index)) + .get_name(pool_entry_lambda); + parsed_class.outer_class = + constant(outer_class_info_index).type().get(ID_C_base_name); parsed_class.is_private = is_private; parsed_class.is_protected = is_protected; parsed_class.is_public = is_public; diff --git a/jbmc/src/java_bytecode/java_types.h b/jbmc/src/java_bytecode/java_types.h index 8e9f092eee6..a82f30a260e 100644 --- a/jbmc/src/java_bytecode/java_types.h +++ b/jbmc/src/java_bytecode/java_types.h @@ -121,6 +121,16 @@ class java_class_typet:public class_typet return set(ID_is_inner_class, is_inner_class); } + const irep_idt get_outer_class() const + { + return get(ID_outer_class); + } + + void set_outer_class(irep_idt outer_class) + { + return set(ID_outer_class, outer_class); + } + const bool get_is_static_class() const { return get_bool(ID_is_static); diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass$1.class b/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass$1.class index dc41102018b..77a27888382 100644 Binary files a/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass$1.class 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 index 502987e5162..fc1723fb3e7 100644 Binary files a/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass$2.class 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 index 80d5d4a52ae..15da3d3d9c3 100644 Binary files a/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass$3.class 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 index d215c74a240..3dea79cbfda 100644 Binary files a/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass$4.class and b/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass$4.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass.class index eafeaf17b03..84f32ec5ee3 100644 Binary files a/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsAnonymousClass.class 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 index 2d58f305b14..c1d636b312e 100644 Binary files a/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsLocalClass$1LocalClass.class 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 index 40be03e68ea..aa5f1a7fcfa 100644 Binary files a/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsLocalClass.class and b/jbmc/unit/java_bytecode/java_bytecode_parser/ContainsLocalClass.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClasses.java b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClasses.java index 7b4792fa26a..3650237d60e 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClasses.java +++ b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerClasses.java @@ -85,6 +85,72 @@ private PrivateDoublyNestedInnerClass(int i) { } } +class InnerPrivateClassesDeeplyNested { + private class SinglyNestedPrivateClass { + int i; + SinglyNestedPrivateClass(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 OuterClassMostRestrictiveDeeplyNested { + public class SinglyNestedPublicClass { + int i; + SinglyNestedPublicClass(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; diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/InnerPrivateClassesDeeplyNested$SinglyNestedPrivateClass$DefaultDoublyNestedInnerClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerPrivateClassesDeeplyNested$SinglyNestedPrivateClass$DefaultDoublyNestedInnerClass.class new file mode 100644 index 00000000000..5756a620a6b Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerPrivateClassesDeeplyNested$SinglyNestedPrivateClass$DefaultDoublyNestedInnerClass.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/InnerPrivateClassesDeeplyNested$SinglyNestedPrivateClass$PrivateDoublyNestedInnerClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerPrivateClassesDeeplyNested$SinglyNestedPrivateClass$PrivateDoublyNestedInnerClass.class new file mode 100644 index 00000000000..992c6e65a73 Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerPrivateClassesDeeplyNested$SinglyNestedPrivateClass$PrivateDoublyNestedInnerClass.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/InnerPrivateClassesDeeplyNested$SinglyNestedPrivateClass$ProtectedDoublyNestedInnerClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerPrivateClassesDeeplyNested$SinglyNestedPrivateClass$ProtectedDoublyNestedInnerClass.class new file mode 100644 index 00000000000..e491e5e5d3a Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerPrivateClassesDeeplyNested$SinglyNestedPrivateClass$ProtectedDoublyNestedInnerClass.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/InnerPrivateClassesDeeplyNested$SinglyNestedPrivateClass$PublicDoublyNestedInnerClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerPrivateClassesDeeplyNested$SinglyNestedPrivateClass$PublicDoublyNestedInnerClass.class new file mode 100644 index 00000000000..f6ebc058502 Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerPrivateClassesDeeplyNested$SinglyNestedPrivateClass$PublicDoublyNestedInnerClass.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/InnerPrivateClassesDeeplyNested$SinglyNestedPrivateClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerPrivateClassesDeeplyNested$SinglyNestedPrivateClass.class new file mode 100644 index 00000000000..2cbdcac9276 Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerPrivateClassesDeeplyNested$SinglyNestedPrivateClass.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/InnerPrivateClassesDeeplyNested.class b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerPrivateClassesDeeplyNested.class new file mode 100644 index 00000000000..62fe78d71cc Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/InnerPrivateClassesDeeplyNested.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/OuterClassMostRestrictiveDeeplyNested$SinglyNestedPublicClass$DefaultDoublyNestedInnerClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/OuterClassMostRestrictiveDeeplyNested$SinglyNestedPublicClass$DefaultDoublyNestedInnerClass.class new file mode 100644 index 00000000000..3d617927ca0 Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/OuterClassMostRestrictiveDeeplyNested$SinglyNestedPublicClass$DefaultDoublyNestedInnerClass.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/OuterClassMostRestrictiveDeeplyNested$SinglyNestedPublicClass$PrivateDoublyNestedInnerClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/OuterClassMostRestrictiveDeeplyNested$SinglyNestedPublicClass$PrivateDoublyNestedInnerClass.class new file mode 100644 index 00000000000..5644211bd98 Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/OuterClassMostRestrictiveDeeplyNested$SinglyNestedPublicClass$PrivateDoublyNestedInnerClass.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/OuterClassMostRestrictiveDeeplyNested$SinglyNestedPublicClass$ProtectedDoublyNestedInnerClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/OuterClassMostRestrictiveDeeplyNested$SinglyNestedPublicClass$ProtectedDoublyNestedInnerClass.class new file mode 100644 index 00000000000..594fcb965c4 Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/OuterClassMostRestrictiveDeeplyNested$SinglyNestedPublicClass$ProtectedDoublyNestedInnerClass.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/OuterClassMostRestrictiveDeeplyNested$SinglyNestedPublicClass$PublicDoublyNestedInnerClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/OuterClassMostRestrictiveDeeplyNested$SinglyNestedPublicClass$PublicDoublyNestedInnerClass.class new file mode 100644 index 00000000000..965e22f81c1 Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/OuterClassMostRestrictiveDeeplyNested$SinglyNestedPublicClass$PublicDoublyNestedInnerClass.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/OuterClassMostRestrictiveDeeplyNested$SinglyNestedPublicClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/OuterClassMostRestrictiveDeeplyNested$SinglyNestedPublicClass.class new file mode 100644 index 00000000000..ee361a25684 Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/OuterClassMostRestrictiveDeeplyNested$SinglyNestedPublicClass.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/OuterClassMostRestrictiveDeeplyNested.class b/jbmc/unit/java_bytecode/java_bytecode_parser/OuterClassMostRestrictiveDeeplyNested.class new file mode 100644 index 00000000000..466827419bf Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/OuterClassMostRestrictiveDeeplyNested.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 index c823c1acae5..367e343acb8 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_attributes.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_attributes.cpp @@ -22,7 +22,7 @@ SCENARIO( 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") + THEN("The inner class should be marked as public") { const symbolt &class_symbol = new_symbol_table.lookup_ref("java::InnerClasses$PublicInnerClass"); @@ -31,11 +31,12 @@ SCENARIO( REQUIRE_FALSE(java_class.get_is_anonymous_class()); REQUIRE(java_class.get_is_inner_class()); REQUIRE(java_class.get_access() == ID_public); + REQUIRE(id2string(java_class.get_outer_class()) == "InnerClasses"); } } WHEN("Parsing the InnerClasses attribute for a package private inner class") { - THEN("The class should be marked as default") + THEN("The inner class should be marked as default") { const symbolt &class_symbol = new_symbol_table.lookup_ref("java::InnerClasses$DefaultInnerClass"); @@ -44,11 +45,12 @@ SCENARIO( REQUIRE_FALSE(java_class.get_is_anonymous_class()); REQUIRE(java_class.get_is_inner_class()); REQUIRE(java_class.get_access() == ID_default); + REQUIRE(id2string(java_class.get_outer_class()) == "InnerClasses"); } } WHEN("Parsing the InnerClasses attribute for a protected inner class") { - THEN("The class should be marked as protected") + THEN("The inner class should be marked as protected") { const symbolt &class_symbol = new_symbol_table.lookup_ref("java::InnerClasses$ProtectedInnerClass"); @@ -57,11 +59,12 @@ SCENARIO( REQUIRE_FALSE(java_class.get_is_anonymous_class()); REQUIRE(java_class.get_is_inner_class()); REQUIRE(java_class.get_access() == ID_protected); + REQUIRE(id2string(java_class.get_outer_class()) == "InnerClasses"); } } WHEN("Parsing the InnerClasses attribute for a private inner class") { - THEN("The class should be marked as private") + THEN("The inner class should be marked as private") { const symbolt &class_symbol = new_symbol_table.lookup_ref("java::InnerClasses$PrivateInnerClass"); @@ -70,10 +73,13 @@ SCENARIO( REQUIRE_FALSE(java_class.get_is_anonymous_class()); REQUIRE(java_class.get_is_inner_class()); REQUIRE(java_class.get_access() == ID_private); + REQUIRE(id2string(java_class.get_outer_class()) == "InnerClasses"); } } } - GIVEN("Some package-private class files in the class path with inner classes") + GIVEN( + "Some package-private (default) class files in the class path with inner " + "classes") { const symbol_tablet &new_symbol_table = load_java_class( "InnerClassesDefault", "./java_bytecode/java_bytecode_parser"); @@ -88,11 +94,15 @@ SCENARIO( REQUIRE_FALSE(java_class.get_is_anonymous_class()); REQUIRE(java_class.get_is_inner_class()); REQUIRE(java_class.get_access() == ID_public); + REQUIRE( + id2string(java_class.get_outer_class()) == "InnerClassesDefault"); } } - WHEN("Parsing the InnerClasses attribute for a package private inner class") + WHEN( + "Parsing the InnerClasses attribute for a package private (default) " + "inner class") { - THEN("The class should be marked as default") + THEN("The inner class should be marked as package-private (default)") { const symbolt &class_symbol = new_symbol_table.lookup_ref( "java::InnerClassesDefault$DefaultInnerClass"); @@ -101,6 +111,8 @@ SCENARIO( REQUIRE_FALSE(java_class.get_is_anonymous_class()); REQUIRE(java_class.get_is_inner_class()); REQUIRE(java_class.get_access() == ID_default); + REQUIRE( + id2string(java_class.get_outer_class()) == "InnerClassesDefault"); } } WHEN("Parsing the InnerClasses attribute for a protected inner class") @@ -114,11 +126,13 @@ SCENARIO( REQUIRE_FALSE(java_class.get_is_anonymous_class()); REQUIRE(java_class.get_is_inner_class()); REQUIRE(java_class.get_access() == ID_protected); + REQUIRE( + id2string(java_class.get_outer_class()) == "InnerClassesDefault"); } } WHEN("Parsing the InnerClasses attribute for a private inner class") { - THEN("The class should be marked as private") + THEN("The inner class should be marked as private") { const symbolt &class_symbol = new_symbol_table.lookup_ref( "java::InnerClassesDefault$PrivateInnerClass"); @@ -127,6 +141,8 @@ SCENARIO( REQUIRE_FALSE(java_class.get_is_anonymous_class()); REQUIRE(java_class.get_is_inner_class()); REQUIRE(java_class.get_access() == ID_private); + REQUIRE( + id2string(java_class.get_outer_class()) == "InnerClassesDefault"); } } } @@ -151,54 +167,246 @@ SCENARIO( REQUIRE_FALSE(java_class.get_is_anonymous_class()); REQUIRE(java_class.get_is_inner_class()); REQUIRE(java_class.get_access() == ID_public); + REQUIRE( + id2string(java_class.get_outer_class()) == + "InnerClassesDeeplyNested$SinglyNestedClass"); + } + } + WHEN( + "Parsing the InnerClasses attribute for a package private (default) " + "doubly-nested inner class") + { + THEN("The inner class should be marked as package-private (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_FALSE(java_class.get_is_anonymous_class()); + REQUIRE(java_class.get_is_inner_class()); + REQUIRE(java_class.get_access() == ID_default); + REQUIRE( + id2string(java_class.get_outer_class()) == + "InnerClassesDeeplyNested$SinglyNestedClass"); + } + } + WHEN( + "Parsing the InnerClasses attribute for a package private (default) " + "doubly-nested inner class ") + { + THEN("The inner 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_FALSE(java_class.get_is_anonymous_class()); + REQUIRE(java_class.get_is_inner_class()); + REQUIRE(java_class.get_access() == ID_protected); + REQUIRE( + id2string(java_class.get_outer_class()) == + "InnerClassesDeeplyNested$SinglyNestedClass"); + } + } + WHEN( + "Parsing the InnerClasses attribute for a private doubly-nested inner " + "class") + { + THEN("The inner 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_FALSE(java_class.get_is_anonymous_class()); + REQUIRE(java_class.get_is_inner_class()); + REQUIRE(java_class.get_access() == ID_private); + REQUIRE( + id2string(java_class.get_outer_class()) == + "InnerClassesDeeplyNested$SinglyNestedClass"); + } + } + } + + GIVEN( + "Some package-private class files in the class path with private deeply" + "nested inner classes") + { + const symbol_tablet &new_symbol_table = load_java_class( + "InnerPrivateClassesDeeplyNested", + "./java_bytecode/java_bytecode_parser"); + WHEN( + "Parsing the InnerClasses attribute for a public doubly-nested inner " + "class") + { + THEN( + "The inner class should be marked as private because its containing " + "class has stricter access ") + { + const symbolt &class_symbol = new_symbol_table.lookup_ref( + "java::InnerPrivateClassesDeeplyNested$SinglyNestedPrivateClass$" + "PublicDoublyNestedInnerClass"); + const java_class_typet java_class = + to_java_class_type(class_symbol.type); + REQUIRE_FALSE(java_class.get_is_anonymous_class()); + REQUIRE(java_class.get_is_inner_class()); + REQUIRE(java_class.get_access() == ID_public); + REQUIRE( + id2string(java_class.get_outer_class()) == + "InnerPrivateClassesDeeplyNested$SinglyNestedPrivateClass"); } } WHEN( "Parsing the InnerClasses attribute for a package private doubly-nested " "inner class") { - THEN("The class should be marked as default") + THEN( + "The inner class should be marked as private because its containing " + "class has stricter access ") { const symbolt &class_symbol = new_symbol_table.lookup_ref( - "java::InnerClassesDeeplyNested$SinglyNestedClass$" + "java::InnerPrivateClassesDeeplyNested$SinglyNestedPrivateClass$" "DefaultDoublyNestedInnerClass"); const java_class_typet java_class = to_java_class_type(class_symbol.type); REQUIRE_FALSE(java_class.get_is_anonymous_class()); REQUIRE(java_class.get_is_inner_class()); REQUIRE(java_class.get_access() == ID_default); + REQUIRE( + id2string(java_class.get_outer_class()) == + "InnerPrivateClassesDeeplyNested$SinglyNestedPrivateClass"); } } WHEN( "Parsing the InnerClasses attribute for a protected doubly-nested inner " "class") { - THEN("The class should be marked as protected") + THEN( + "The inner class should be marked as private because its containing " + "class has stricter access ") { const symbolt &class_symbol = new_symbol_table.lookup_ref( - "java::InnerClassesDeeplyNested$SinglyNestedClass$" + "java::InnerPrivateClassesDeeplyNested$SinglyNestedPrivateClass$" "ProtectedDoublyNestedInnerClass"); const java_class_typet java_class = to_java_class_type(class_symbol.type); REQUIRE_FALSE(java_class.get_is_anonymous_class()); REQUIRE(java_class.get_is_inner_class()); REQUIRE(java_class.get_access() == ID_protected); + REQUIRE( + id2string(java_class.get_outer_class()) == + "InnerPrivateClassesDeeplyNested$SinglyNestedPrivateClass"); } } WHEN( "Parsing the InnerClasses attribute for a private doubly-nested inner " "class") { - THEN("The class should be marked as private") + THEN("The inner class should be marked as private ") { const symbolt &class_symbol = new_symbol_table.lookup_ref( - "java::InnerClassesDeeplyNested$SinglyNestedClass$" + "java::InnerPrivateClassesDeeplyNested$SinglyNestedPrivateClass$" + "PrivateDoublyNestedInnerClass"); + const java_class_typet java_class = + to_java_class_type(class_symbol.type); + REQUIRE_FALSE(java_class.get_is_anonymous_class()); + REQUIRE(java_class.get_is_inner_class()); + REQUIRE(java_class.get_access() == ID_private); + REQUIRE( + id2string(java_class.get_outer_class()) == + "InnerPrivateClassesDeeplyNested$SinglyNestedPrivateClass"); + } + } + } + + GIVEN( + "Some class files where the outer class is more restrictive than the first " + "inner class") + { + const symbol_tablet &new_symbol_table = load_java_class( + "OuterClassMostRestrictiveDeeplyNested", + "./java_bytecode/java_bytecode_parser"); + WHEN( + "Parsing the InnerClasses attribute for a public doubly-nested inner " + "class") + { + THEN( + "The inner class should be marked as default (package-private) because " + "one of its containing classes has stricter access ") + { + const symbolt &class_symbol = new_symbol_table.lookup_ref( + "java::OuterClassMostRestrictiveDeeplyNested$SinglyNestedPublicClass$" + "PublicDoublyNestedInnerClass"); + const java_class_typet java_class = + to_java_class_type(class_symbol.type); + REQUIRE_FALSE(java_class.get_is_anonymous_class()); + REQUIRE(java_class.get_is_inner_class()); + REQUIRE(java_class.get_access() == ID_public); + REQUIRE( + id2string(java_class.get_outer_class()) == + "OuterClassMostRestrictiveDeeplyNested$SinglyNestedPublicClass"); + } + } + WHEN( + "Parsing the InnerClasses attribute for a package private doubly-nested " + "inner class") + { + THEN( + "The inner class should be marked as default (package-private) because " + "one of its containing classes has stricter access ") + { + const symbolt &class_symbol = new_symbol_table.lookup_ref( + "java::OuterClassMostRestrictiveDeeplyNested$SinglyNestedPublicClass$" + "DefaultDoublyNestedInnerClass"); + const java_class_typet java_class = + to_java_class_type(class_symbol.type); + REQUIRE_FALSE(java_class.get_is_anonymous_class()); + REQUIRE(java_class.get_is_inner_class()); + REQUIRE(java_class.get_access() == ID_default); + REQUIRE( + id2string(java_class.get_outer_class()) == + "OuterClassMostRestrictiveDeeplyNested$SinglyNestedPublicClass"); + } + } + WHEN( + "Parsing the InnerClasses attribute for a protected doubly-nested inner " + "class") + { + THEN("The inner class should be marked as default (package-private)") + { + const symbolt &class_symbol = new_symbol_table.lookup_ref( + "java::OuterClassMostRestrictiveDeeplyNested$SinglyNestedPublicClass$" + "ProtectedDoublyNestedInnerClass"); + const java_class_typet java_class = + to_java_class_type(class_symbol.type); + REQUIRE_FALSE(java_class.get_is_anonymous_class()); + REQUIRE(java_class.get_is_inner_class()); + REQUIRE(java_class.get_access() == ID_protected); + REQUIRE( + id2string(java_class.get_outer_class()) == + "OuterClassMostRestrictiveDeeplyNested$SinglyNestedPublicClass"); + } + } + WHEN( + "Parsing the InnerClasses attribute for a private doubly-nested inner " + "class") + { + THEN("The inner class should be marked as private") + { + const symbolt &class_symbol = new_symbol_table.lookup_ref( + "java::OuterClassMostRestrictiveDeeplyNested$SinglyNestedPublicClass$" "PrivateDoublyNestedInnerClass"); const java_class_typet java_class = to_java_class_type(class_symbol.type); REQUIRE_FALSE(java_class.get_is_anonymous_class()); REQUIRE(java_class.get_is_inner_class()); REQUIRE(java_class.get_access() == ID_private); + REQUIRE( + id2string(java_class.get_outer_class()) == + "OuterClassMostRestrictiveDeeplyNested$SinglyNestedPublicClass"); } } } @@ -219,6 +427,7 @@ SCENARIO( REQUIRE(java_class.get_is_inner_class()); REQUIRE(java_class.get_is_anonymous_class()); REQUIRE(java_class.get_access() == ID_private); + REQUIRE(java_class.get_outer_class().empty()); } } WHEN( @@ -234,6 +443,7 @@ SCENARIO( REQUIRE(java_class.get_is_inner_class()); REQUIRE(java_class.get_is_anonymous_class()); REQUIRE(java_class.get_access() == ID_private); + REQUIRE(java_class.get_outer_class().empty()); } } WHEN("Parsing the InnerClasses attribute for a protected anonymous class") @@ -247,6 +457,7 @@ SCENARIO( REQUIRE(java_class.get_is_inner_class()); REQUIRE(java_class.get_is_anonymous_class()); REQUIRE(java_class.get_access() == ID_private); + REQUIRE(java_class.get_outer_class().empty()); } } WHEN("Parsing the InnerClasses attribute for a private anonymous class") @@ -260,6 +471,7 @@ SCENARIO( REQUIRE(java_class.get_is_inner_class()); REQUIRE(java_class.get_is_anonymous_class()); REQUIRE(java_class.get_access() == ID_private); + REQUIRE(java_class.get_outer_class().empty()); } } } @@ -280,6 +492,7 @@ SCENARIO( REQUIRE(java_class.get_is_inner_class()); REQUIRE(java_class.get_access() == ID_private); REQUIRE_FALSE(java_class.get_is_anonymous_class()); + REQUIRE(java_class.get_outer_class().empty()); } } } @@ -299,6 +512,7 @@ SCENARIO( REQUIRE(java_class.get_is_inner_class()); REQUIRE(java_class.get_is_static_class()); REQUIRE_FALSE(java_class.get_is_anonymous_class()); + REQUIRE(id2string(java_class.get_outer_class()) == "StaticInnerClass"); } } WHEN("Parsing the InnerClasses attribute for a non-static inner class ") @@ -312,6 +526,7 @@ SCENARIO( REQUIRE(java_class.get_is_inner_class()); REQUIRE_FALSE(java_class.get_is_static_class()); REQUIRE_FALSE(java_class.get_is_anonymous_class()); + REQUIRE(id2string(java_class.get_outer_class()) == "StaticInnerClass"); } } } @@ -328,6 +543,7 @@ SCENARIO( REQUIRE(java_class.get_is_inner_class()); REQUIRE(java_class.get_is_anonymous_class()); REQUIRE(java_class.get_is_static_class()); + REQUIRE(java_class.get_outer_class().empty()); } } WHEN("Parsing the InnerClasses attribute for a non-static anonymous class ") @@ -341,6 +557,7 @@ SCENARIO( REQUIRE(java_class.get_is_inner_class()); REQUIRE(java_class.get_is_anonymous_class()); REQUIRE_FALSE(java_class.get_is_static_class()); + REQUIRE(java_class.get_outer_class().empty()); } } } @@ -359,6 +576,7 @@ SCENARIO( REQUIRE(java_class.get_is_inner_class()); REQUIRE_FALSE(java_class.get_is_static_class()); REQUIRE_FALSE(java_class.get_is_anonymous_class()); + REQUIRE(java_class.get_outer_class().empty()); } } WHEN( @@ -374,6 +592,7 @@ SCENARIO( REQUIRE(java_class.get_is_inner_class()); REQUIRE_FALSE(java_class.get_is_static_class()); REQUIRE_FALSE(java_class.get_is_anonymous_class()); + REQUIRE(java_class.get_outer_class().empty()); } } } diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index e2d7d160112..bcc6a8f6906 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -675,6 +675,7 @@ IREP_ID_ONE(interface) IREP_ID_TWO(C_must_not_throw, #must_not_throw) IREP_ID_ONE(is_inner_class) IREP_ID_ONE(is_anonymous) +IREP_ID_ONE(outer_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