Skip to content

Commit

Permalink
Captures anonymous inner class information.
Browse files Browse the repository at this point in the history
  • Loading branch information
@jeannielynnmoulton
jeannielynnmoulton committed Jul 6, 2018
1 parent d20a12e commit af0ce5a
Show file tree
Hide file tree
Showing 6 changed files with 45 additions and 7 deletions.
1 change: 1 addition & 0 deletions jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
View file
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
View file
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
View file
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)
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
View file
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
35 changes: 29 additions & 6 deletions jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_attributes.cpp
View file
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
View file
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

0 comments on commit af0ce5a

Please sign in to comment.