From af0ce5a1925ebe445f39f336baccd190fa39edb1 Mon Sep 17 00:00:00 2001 From: Jeannie Moulton Date: Tue, 3 Jul 2018 15:43:04 +0100 Subject: [PATCH] Captures anonymous inner class information. --- .../java_bytecode_convert_class.cpp | 1 + .../java_bytecode/java_bytecode_parse_tree.h | 1 + .../java_bytecode/java_bytecode_parser.cpp | 5 ++- jbmc/src/java_bytecode/java_types.h | 9 +++++ .../parse_java_attributes.cpp | 35 +++++++++++++++---- src/util/irep_ids.def | 1 + 6 files changed, 45 insertions(+), 7 deletions(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp index 650dbb6d93e..f00a0bfb17c 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp @@ -278,6 +278,7 @@ void java_bytecode_convert_classt::convert( class_type.set_final(c.is_final); 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); 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 6a8c4a46fbc..431dd4804f5 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parse_tree.h +++ b/jbmc/src/java_bytecode/java_bytecode_parse_tree.h @@ -219,6 +219,7 @@ class java_bytecode_parse_treet bool is_annotation = false; bool is_inner_class = false; bool is_static_class = false; + bool is_anonymous_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 74b5e977616..82c66bf5c5e 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parser.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_parser.cpp @@ -1613,7 +1613,7 @@ void java_bytecode_parsert::rinner_classes_attribute( { u2 inner_class_info_index = read_u2(); u2 outer_class_info_index = read_u2(); - UNUSED u2 inner_name_index = read_u2(); + u2 inner_name_index = read_u2(); u2 inner_class_access_flags = read_u2(); std::string inner_class_info_name = @@ -1634,6 +1634,9 @@ void java_bytecode_parsert::rinner_classes_attribute( if(!is_inner_class) continue; parsed_class.is_static_class = is_static; + // This is a marker that a class is anonymous. + if(inner_name_index == 0) + parsed_class.is_anonymous_class = true; // 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 92afbde3ccd..8e9f092eee6 100644 --- a/jbmc/src/java_bytecode/java_types.h +++ b/jbmc/src/java_bytecode/java_types.h @@ -131,6 +131,15 @@ class java_class_typet:public class_typet return set(ID_is_static, is_static_class); } + const bool get_is_anonymous_class() const + { + return get_bool(ID_is_anonymous); + } + + void set_is_anonymous_class(const bool &is_anonymous_class) + { + return set(ID_is_anonymous, is_anonymous_class); + } bool get_final() { 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 b431593857f..c823c1acae5 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 @@ -28,6 +28,7 @@ SCENARIO( new_symbol_table.lookup_ref("java::InnerClasses$PublicInnerClass"); 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); } @@ -40,6 +41,7 @@ SCENARIO( new_symbol_table.lookup_ref("java::InnerClasses$DefaultInnerClass"); 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); } @@ -52,6 +54,7 @@ SCENARIO( new_symbol_table.lookup_ref("java::InnerClasses$ProtectedInnerClass"); 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); } @@ -64,6 +67,7 @@ SCENARIO( new_symbol_table.lookup_ref("java::InnerClasses$PrivateInnerClass"); 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); } @@ -81,6 +85,7 @@ SCENARIO( "java::InnerClassesDefault$PublicInnerClass"); 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); } @@ -93,6 +98,7 @@ SCENARIO( "java::InnerClassesDefault$DefaultInnerClass"); 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); } @@ -105,6 +111,7 @@ SCENARIO( "java::InnerClassesDefault$ProtectedInnerClass"); 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); } @@ -117,6 +124,7 @@ SCENARIO( "java::InnerClassesDefault$PrivateInnerClass"); 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); } @@ -140,6 +148,7 @@ SCENARIO( "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); } @@ -155,6 +164,7 @@ SCENARIO( "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); } @@ -170,6 +180,7 @@ SCENARIO( "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); } @@ -185,6 +196,7 @@ SCENARIO( "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); } @@ -198,13 +210,14 @@ SCENARIO( "ContainsAnonymousClass", "./java_bytecode/java_bytecode_parser"); WHEN("Parsing the InnerClasses attribute for a public anonymous class") { - THEN("The class should be marked as public") + THEN("The class should be marked as private and anonymous") { 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_is_anonymous_class()); REQUIRE(java_class.get_access() == ID_private); } } @@ -212,37 +225,40 @@ SCENARIO( "Parsing the InnerClasses attribute for a package-private anonymous " "class") { - THEN("The class should be marked as default") + THEN("The class should be marked as private and anonymous") { 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_is_anonymous_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") + THEN("The class should be marked as private and anonymous") { 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_is_anonymous_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") + THEN("The class should be marked as private and anonymous") { 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_is_anonymous_class()); REQUIRE(java_class.get_access() == ID_private); } } @@ -263,6 +279,7 @@ SCENARIO( to_java_class_type(class_symbol.type); REQUIRE(java_class.get_is_inner_class()); REQUIRE(java_class.get_access() == ID_private); + REQUIRE_FALSE(java_class.get_is_anonymous_class()); } } } @@ -281,6 +298,7 @@ SCENARIO( to_java_class_type(class_symbol.type); REQUIRE(java_class.get_is_inner_class()); REQUIRE(java_class.get_is_static_class()); + REQUIRE_FALSE(java_class.get_is_anonymous_class()); } } WHEN("Parsing the InnerClasses attribute for a non-static inner class ") @@ -293,6 +311,7 @@ SCENARIO( to_java_class_type(class_symbol.type); REQUIRE(java_class.get_is_inner_class()); REQUIRE_FALSE(java_class.get_is_static_class()); + REQUIRE_FALSE(java_class.get_is_anonymous_class()); } } } @@ -300,25 +319,27 @@ SCENARIO( { WHEN("Parsing the InnerClasses attribute for a static anonymous class ") { - THEN("The class should be marked as static") + THEN("The class should be marked as static and anonymous") { const symbolt &class_symbol = new_symbol_table.lookup_ref("java::StaticInnerClass$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_is_anonymous_class()); REQUIRE(java_class.get_is_static_class()); } } WHEN("Parsing the InnerClasses attribute for a non-static anonymous class ") { - THEN("The class should not be marked as static") + THEN("The class should be marked as anonymous and not static") { const symbolt &class_symbol = new_symbol_table.lookup_ref("java::StaticInnerClass$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_is_anonymous_class()); REQUIRE_FALSE(java_class.get_is_static_class()); } } @@ -337,6 +358,7 @@ SCENARIO( to_java_class_type(class_symbol.type); REQUIRE(java_class.get_is_inner_class()); REQUIRE_FALSE(java_class.get_is_static_class()); + REQUIRE_FALSE(java_class.get_is_anonymous_class()); } } WHEN( @@ -351,6 +373,7 @@ SCENARIO( to_java_class_type(class_symbol.type); REQUIRE(java_class.get_is_inner_class()); REQUIRE_FALSE(java_class.get_is_static_class()); + REQUIRE_FALSE(java_class.get_is_anonymous_class()); } } } diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index a0899029370..8372cba0caf 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -676,6 +676,7 @@ 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) +IREP_ID_ONE(is_anonymous) // 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