Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Captures anonymous inner class information #2526

Merged
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
1 change: 1 addition & 0 deletions jbmc/src/java_bytecode/java_bytecode_parse_tree.h
Original file line number Diff line number Diff line change
Expand Up @@ -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;

Expand Down
5 changes: 4 additions & 1 deletion jbmc/src/java_bytecode/java_bytecode_parser.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand All @@ -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)
Copy link
Contributor

@thk123 thk123 Jul 5, 2018

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nit: Might be simpler to say parsed_class.is_anonymous_class = 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)
Expand Down
9 changes: 9 additions & 0 deletions jbmc/src/java_bytecode/java_types.h
Original file line number Diff line number Diff line change
Expand Up @@ -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()
{
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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);
}
Expand All @@ -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);
}
Expand All @@ -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);
}
Expand All @@ -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);
}
Expand All @@ -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);
}
Expand All @@ -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);
}
Expand All @@ -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);
}
Expand All @@ -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);
}
Expand All @@ -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);
}
Expand All @@ -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);
}
Expand All @@ -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);
}
Expand All @@ -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);
}
Expand All @@ -198,51 +210,55 @@ 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);
}
}
WHEN(
"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);
}
}
Expand All @@ -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());
}
}
}
Expand All @@ -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 ")
Expand All @@ -293,32 +311,35 @@ 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());
}
}
}
GIVEN("Some class with a static anonymous class")
{
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());
}
}
Expand All @@ -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(
Expand All @@ -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());
}
}
}
Expand Down
1 change: 1 addition & 0 deletions src/util/irep_ids.def
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down