Add parsing of the names of inner java classes.

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -303,6 +303,7 @@ void java_bytecode_convert_classt::convert(
   }
 
   class_type.set_tag(c.name);
+  class_type.set_inner_name(c.inner_name);
   class_type.set(ID_abstract, c.is_abstract);
   class_type.set(ID_is_annotation, c.is_annotation);
   class_type.set(ID_interface, c.is_interface);

jbmc/src/java_bytecode/java_bytecode_parse_tree.h

@@ -213,7 +213,7 @@ struct java_bytecode_parse_treet
     classt &operator=(classt &&) = default;
     #endif
 
-    irep_idt name, super_class;
+    irep_idt name, super_class, inner_name;
     bool is_abstract=false;
     bool is_enum=false;
     bool is_public=false, is_protected=false, is_private=false;

jbmc/src/java_bytecode/java_bytecode_parser.cpp

@@ -1696,6 +1696,8 @@ void java_bytecode_parsert::rinner_classes_attribute(
     // This is a marker that a class is anonymous.
     if(inner_name_index == 0)
       parsed_class.is_anonymous_class = true;
+    else
+      parsed_class.inner_name = pool_entry_lambda(inner_name_index).s;
     // 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)

jbmc/src/java_bytecode/java_types.h

@@ -241,6 +241,18 @@ class java_class_typet:public class_typet
   {
     set(ID_name, name);
   }
+
+  /// Get the name of a java inner class.
+  const irep_idt &get_inner_name() const
+  {
+    return get(ID_inner_name);
+  }
+
+  /// Set the name of a java inner class.
+  void set_inner_name(const irep_idt &name)
+  {
+    set(ID_inner_name, name);
+  }
 };
 
 inline const java_class_typet &to_java_class_type(const typet &type)

jbmc/unit/Makefile

@@ -38,6 +38,7 @@ SRC += java_bytecode/ci_lazy_methods/lazy_load_lambdas.cpp \
        java_bytecode/java_bytecode_parse_lambdas/java_bytecode_convert_class_lambda_method_handles.cpp \
        java_bytecode/java_bytecode_parse_lambdas/java_bytecode_parse_lambda_method_table.cpp \
        java_bytecode/java_bytecode_parser/parse_class_without_instructions.cpp \
+       java_bytecode/java_bytecode_parser/parse_inner_class.cpp \
        java_bytecode/java_bytecode_parser/parse_java_annotations.cpp \
        java_bytecode/java_bytecode_parser/parse_java_attributes.cpp \
        java_bytecode/java_bytecode_parser/parse_java_class.cpp \

jbmc/unit/java_bytecode/java_bytecode_parser/Outer$RedHerring.java

@@ -0,0 +1,2 @@
+class Outer$RedHerring {
+}

jbmc/unit/java_bytecode/java_bytecode_parser/Outer.java

@@ -0,0 +1,7 @@
+class Outer {
+  class Inner {
+  }
+
+  Outer anonymous = new Outer() {
+  };
+}

jbmc/unit/java_bytecode/java_bytecode_parser/parse_inner_class.cpp

@@ -0,0 +1,121 @@
+/*******************************************************************\
+
+ Module: Unit tests for converting inner classes
+
+ Author: Diffblue Ltd.
+
+\*******************************************************************/
+
+#include <java-testing-utils/load_java_class.h>
+#include <java_bytecode/java_types.h>
+#include <testing-utils/catch.hpp>
+
+SCENARIO(
+  "Parsing inner java classes",
+  "[core][java_bytecode][java_bytecode_parser]")
+{
+  GIVEN("A class file of an inner class.")
+  {
+    WHEN("Parsing an inner class called \"Inner\".")
+    {
+      const symbol_tablet &symbol_table = load_java_class(
+        "Outer$Inner", "./java_bytecode/java_bytecode_parser");
+      const symbolt *class_symbol = symbol_table.lookup("java::Outer$Inner");
+      REQUIRE(class_symbol);
+      const java_class_typet *class_type =
+        type_try_dynamic_cast<java_class_typet>(class_symbol->type);
+      REQUIRE(class_type);
+
+      THEN("The inner class should have the inner name \"Inner\".")
+      {
+        REQUIRE(id2string(class_type->get_inner_name()) == "Inner");
+      }
+      THEN("The inner class is not considered to be an anonymous class.")
+      {
+        REQUIRE_FALSE(class_type->get_is_anonymous_class());
+      }
+      THEN("The inner class has the outer class \"Outer\".")
+      {
+        REQUIRE(id2string(class_type->get_outer_class()) == "Outer");
+      }
+    }
+  }
+  GIVEN("A class file of a class which is not an inner class.")
+  {
+    WHEN("Parsing an outer class.")
+    {
+      const symbol_tablet &symbol_table =
+        load_java_class("Outer", "./java_bytecode/java_bytecode_parser");
+      const symbolt *class_symbol = symbol_table.lookup("java::Outer");
+      REQUIRE(class_symbol);
+      const java_class_typet *class_type =
+        type_try_dynamic_cast<java_class_typet>(class_symbol->type);
+      REQUIRE(class_type);
+
+      THEN("The outer class should not have an inner name.")
+      {
+        REQUIRE(id2string(class_type->get_inner_name()).empty());
+      }
+      THEN("The outer class is not considered to be an anonymous class.")
+      {
+        REQUIRE_FALSE(class_type->get_is_anonymous_class());
+      }
+      THEN("The outer class does not have an outer class.")
+      {
+        REQUIRE(id2string(class_type->get_outer_class()).empty());
+      }
+    }
+  }
+  GIVEN("A class file of an anonymous class.")
+  {
+    WHEN("Parsing an anonymous class.")
+    {
+      const symbol_tablet &symbol_table = load_java_class(
+        "Outer$1", "./java_bytecode/java_bytecode_parser");
+      const symbolt *class_symbol = symbol_table.lookup("java::Outer$1");
+      REQUIRE(class_symbol);
+      const java_class_typet *class_type =
+        type_try_dynamic_cast<java_class_typet>(class_symbol->type);
+      REQUIRE(class_type);
+
+      THEN("The anonymous class should not have an inner name.")
+      {
+        REQUIRE(id2string(class_type->get_inner_name()).empty());
+      }
+      THEN("The anonymous class is considered to be an anonymous class.")
+      {
+        REQUIRE(class_type->get_is_anonymous_class());
+      }
+      THEN("The anonymous class does not have an outer class.")
+      {
+        REQUIRE(id2string(class_type->get_outer_class()).empty());
+      }
+    }
+  }
+  GIVEN("A class file of an outer class which is named with a '$'.")
+  {
+    WHEN("Parsing an outer class named with a '$'.")
+    {
+      const symbol_tablet &symbol_table = load_java_class(
+        "Outer$RedHerring", "./java_bytecode/java_bytecode_parser");
+      const auto *class_symbol = symbol_table.lookup("java::Outer$RedHerring");
+      REQUIRE(class_symbol);
+      const java_class_typet *class_type =
+        type_try_dynamic_cast<java_class_typet>(class_symbol->type);
+      REQUIRE(class_type);
+
+      THEN("The outer class should not have an inner name.")
+      {
+        REQUIRE(id2string(class_type->get_inner_name()).empty());
+      }
+      THEN("The inner class is not considered to be an anonymous class.")
+      {
+        REQUIRE_FALSE(class_type->get_is_anonymous_class());
+      }
+      THEN("The outer class does not have an outer class.")
+      {
+        REQUIRE(id2string(class_type->get_outer_class()).empty());
+      }
+    }
+  }
+}

src/util/irep_ids.def

@@ -131,6 +131,7 @@ IREP_ID_ONE(incomplete_c_enum)
 IREP_ID_TWO(C_incomplete, #incomplete)
 IREP_ID_ONE(identifier)
 IREP_ID_ONE(name)
+IREP_ID_ONE(inner_name)
 IREP_ID_ONE(cpp_name)
 IREP_ID_ONE(component_cpp_name)
 IREP_ID_TWO(C_id_class, #id_class)