diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp index 8eb9cae4d81..650dbb6d93e 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp @@ -277,6 +277,7 @@ void java_bytecode_convert_classt::convert( 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); + class_type.set_is_static_class(c.is_static_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 5d48175fd96..6a8c4a46fbc 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parse_tree.h +++ b/jbmc/src/java_bytecode/java_bytecode_parse_tree.h @@ -218,6 +218,7 @@ class java_bytecode_parse_treet bool is_synthetic = false; bool is_annotation = false; bool is_inner_class = false; + bool is_static_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 aa86988ebc4..74b5e977616 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parser.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_parser.cpp @@ -1622,6 +1622,7 @@ void java_bytecode_parsert::rinner_classes_attribute( 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; + bool is_static = (inner_class_access_flags & ACC_STATIC) != 0; // If the original parsed class name matches the inner class name, // the parsed class is an inner class, so overwrite the parsed class' @@ -1632,6 +1633,7 @@ void java_bytecode_parsert::rinner_classes_attribute( parsed_class.is_inner_class = is_inner_class; if(!is_inner_class) continue; + parsed_class.is_static_class = is_static; // 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 1a8579f3b69..92afbde3ccd 100644 --- a/jbmc/src/java_bytecode/java_types.h +++ b/jbmc/src/java_bytecode/java_types.h @@ -121,6 +121,17 @@ class java_class_typet:public class_typet return set(ID_is_inner_class, is_inner_class); } + const bool get_is_static_class() const + { + return get_bool(ID_is_static); + } + + void set_is_static_class(const bool &is_static_class) + { + return set(ID_is_static, is_static_class); + } + + bool get_final() { return get_bool(ID_final); diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/StaticInnerClass$1.class b/jbmc/unit/java_bytecode/java_bytecode_parser/StaticInnerClass$1.class new file mode 100644 index 00000000000..6495bd34e75 Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/StaticInnerClass$1.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/StaticInnerClass$1LocalClassInNonStatic.class b/jbmc/unit/java_bytecode/java_bytecode_parser/StaticInnerClass$1LocalClassInNonStatic.class new file mode 100644 index 00000000000..57bfd5c4710 Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/StaticInnerClass$1LocalClassInNonStatic.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/StaticInnerClass$1LocalClassInStatic.class b/jbmc/unit/java_bytecode/java_bytecode_parser/StaticInnerClass$1LocalClassInStatic.class new file mode 100644 index 00000000000..6fa9b79bf13 Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/StaticInnerClass$1LocalClassInStatic.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/StaticInnerClass$2.class b/jbmc/unit/java_bytecode/java_bytecode_parser/StaticInnerClass$2.class new file mode 100644 index 00000000000..e4abe97b8da Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/StaticInnerClass$2.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/StaticInnerClass$PublicNonStaticInnerClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/StaticInnerClass$PublicNonStaticInnerClass.class new file mode 100644 index 00000000000..57219cf2e2e Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/StaticInnerClass$PublicNonStaticInnerClass.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/StaticInnerClass$PublicStaticInnerClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/StaticInnerClass$PublicStaticInnerClass.class new file mode 100644 index 00000000000..6c06bd7ecff Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/StaticInnerClass$PublicStaticInnerClass.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/StaticInnerClass$SomeInterface.class b/jbmc/unit/java_bytecode/java_bytecode_parser/StaticInnerClass$SomeInterface.class new file mode 100644 index 00000000000..8588826f47b Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/StaticInnerClass$SomeInterface.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/StaticInnerClass.class b/jbmc/unit/java_bytecode/java_bytecode_parser/StaticInnerClass.class new file mode 100644 index 00000000000..da02b08a8a3 Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parser/StaticInnerClass.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/StaticInnerClass.java b/jbmc/unit/java_bytecode/java_bytecode_parser/StaticInnerClass.java new file mode 100644 index 00000000000..118f36e0777 --- /dev/null +++ b/jbmc/unit/java_bytecode/java_bytecode_parser/StaticInnerClass.java @@ -0,0 +1,33 @@ +public class StaticInnerClass { + public static interface SomeInterface { + public int i = 0; + } + public static class PublicStaticInnerClass { + public int i; + public PublicStaticInnerClass(int i) { + this.i = i; + } + } + public class PublicNonStaticInnerClass { + public int i; + public PublicNonStaticInnerClass(int i) { + this.i = i; + } + } + public static SomeInterface staticAnonymousClass = new SomeInterface() { + public int i = 50; + }; + public SomeInterface anonymousClass = new SomeInterface() { + public int i = 25; + }; + public void testNonStatic() { + class LocalClassInNonStatic { + public int i = 1; + } + } + public static void testStatic() { + class LocalClassInStatic { + public int i = 2; + } + } +} 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 737ad516577..b431593857f 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 @@ -266,4 +266,92 @@ SCENARIO( } } } + + const symbol_tablet &new_symbol_table = + load_java_class("StaticInnerClass", "./java_bytecode/java_bytecode_parser"); + GIVEN("Some class with a static inner class") + { + WHEN("Parsing the InnerClasses attribute for a static inner class ") + { + THEN("The class should be marked as static") + { + const symbolt &class_symbol = new_symbol_table.lookup_ref( + "java::StaticInnerClass$PublicStaticInnerClass"); + 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_static_class()); + } + } + WHEN("Parsing the InnerClasses attribute for a non-static inner class ") + { + THEN("The class should not be marked as static") + { + const symbolt &class_symbol = new_symbol_table.lookup_ref( + "java::StaticInnerClass$PublicNonStaticInnerClass"); + const java_class_typet java_class = + to_java_class_type(class_symbol.type); + REQUIRE(java_class.get_is_inner_class()); + REQUIRE_FALSE(java_class.get_is_static_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") + { + 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_static_class()); + } + } + WHEN("Parsing the InnerClasses attribute for a non-static anonymous class ") + { + THEN("The class should not be marked as 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_FALSE(java_class.get_is_static_class()); + } + } + } + GIVEN("Some method containing a local class") + { + WHEN( + "Parsing the InnerClasses attribute for a local class in a static " + "method ") + { + THEN("The local class should be marked as static") + { + const symbolt &class_symbol = new_symbol_table.lookup_ref( + "java::StaticInnerClass$1LocalClassInStatic"); + const java_class_typet java_class = + to_java_class_type(class_symbol.type); + REQUIRE(java_class.get_is_inner_class()); + REQUIRE_FALSE(java_class.get_is_static_class()); + } + } + WHEN( + "Parsing the InnerClasses attribute for a local class in a non-static " + "method ") + { + THEN("The local class should not be marked as static") + { + const symbolt &class_symbol = new_symbol_table.lookup_ref( + "java::StaticInnerClass$1LocalClassInNonStatic"); + const java_class_typet java_class = + to_java_class_type(class_symbol.type); + REQUIRE(java_class.get_is_inner_class()); + REQUIRE_FALSE(java_class.get_is_static_class()); + } + } + } }