[TG-3694] Parse and store inner class information

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -268,6 +268,7 @@ void java_bytecode_convert_classt::convert(
   class_type.set(ID_interface, c.is_interface);
   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);
   if(c.is_enum)
   {
     if(max_array_length != 0 && c.enum_elements > max_array_length)

jbmc/src/java_bytecode/java_bytecode_parse_tree.h

@@ -212,6 +212,7 @@ class java_bytecode_parse_treet
     bool is_interface = false;
     bool is_synthetic = false;
     bool is_annotation = false;
+    bool is_inner_class = false;
     bool attribute_bootstrapmethods_read = false;
     size_t enum_elements=0;
 

jbmc/src/java_bytecode/java_bytecode_parser.cpp

@@ -119,6 +119,8 @@ class java_bytecode_parsert:public parsert
   void rfields(classt &parsed_class);
   void rmethods(classt &parsed_class);
   void rmethod(classt &parsed_class);
+  void
+  rinner_classes_attribute(classt &parsed_class, const u4 &attribute_length);
   void rclass_attribute(classt &parsed_class);
   void rRuntimeAnnotation_attribute(annotationst &);
   void rRuntimeAnnotation(annotationt &);
@@ -1576,6 +1578,81 @@ void java_bytecode_parsert::relement_value_pair(
   }
 }
 
+/// Corresponds to the element_value structure
+/// Described in Java 8 specification 4.7.6
+/// https://docs.oracle.com/javase/specs/jvms/se8/html/jvms-4.html#jvms-4.7.6
+/// Parses the InnerClasses attribute for the current parsed class,
+/// which contains an array of information about its inner classes. We are
+/// interested in getting information only for inner classes, which is
+/// determined by checking if the parsed class matches any of the inner classes
+/// in its inner class array. If the parsed class is not an inner class, then it
+/// is ignored. When a parsed class is an inner class, the accessibility
+/// information for the parsed class is overwritten, and the parsed class is
+/// marked as an inner class.
+void java_bytecode_parsert::rinner_classes_attribute(
+  classt &parsed_class,
+  const u4 &attribute_length)
+{
+  std::string name = parsed_class.name.c_str();
+  u2 number_of_classes = read_u2();
+  u4 number_of_bytes_to_be_read = number_of_classes * 8 + 2;
+  INVARIANT(
+    number_of_bytes_to_be_read == attribute_length,
+    "The number of bytes to be read for the InnerClasses attribute does not "
+    "match the attribute length.");
+
+  const auto pool_entry_lambda = [this](u2 index) -> pool_entryt & {
+    return pool_entry(index);
+  };
+  const auto remove_separator_char = [](std::string str, char ch) {
+    str.erase(std::remove(str.begin(), str.end(), ch), str.end());
+    return str;
+  };
+
+  for(int i = 0; i < number_of_classes; i++)
+  {
+    u2 inner_class_info_index = read_u2();
+    UNUSED u2 outer_class_info_index = read_u2();
+    UNUSED u2 inner_name_index = read_u2();
+    u2 inner_class_access_flags = read_u2();
+
+    if(inner_class_info_index == 0)
+      continue;
+
+    std::string inner_class_info_name =
+      class_infot(pool_entry(inner_class_info_index))
+        .get_name(pool_entry_lambda);
+    bool is_private = inner_class_access_flags & ACC_PRIVATE;
+    bool is_public = inner_class_access_flags & ACC_PUBLIC;
+    bool is_protected = inner_class_access_flags & ACC_PROTECTED;
+
+    // If the original parsed class name matches the inner class name,
+    // the parsed class is an inner class, so overwrite the parsed class'
+    // access information and mark it as an inner class
+    parsed_class.is_inner_class =
+      remove_separator_char(id2string(parsed_class.name), '.') ==
+      remove_separator_char(inner_class_info_name, '/');
+    if(!parsed_class.is_inner_class)
+      continue;
+    // 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)
+    {
+      // This is a marker for an anonymous or local class
+      // which are treated as private
+      parsed_class.is_private = true;
+      parsed_class.is_protected = false;
+      parsed_class.is_public = false;
+    }
+    else
+    {
+      parsed_class.is_private = is_private;
+      parsed_class.is_protected = is_protected;
+      parsed_class.is_public = is_public;
+    }
+  }
+}
+
 void java_bytecode_parsert::rclass_attribute(classt &parsed_class)
 {
   u2 attribute_name_index=read_u2();
@@ -1640,6 +1717,11 @@ void java_bytecode_parsert::rclass_attribute(classt &parsed_class)
     parsed_class.attribute_bootstrapmethods_read = true;
     read_bootstrapmethods_entry(parsed_class);
   }
+  else if(attribute_name == "InnerClasses")
+  {
+    java_bytecode_parsert::rinner_classes_attribute(
+      parsed_class, attribute_length);
+  }
   else
     skip_bytes(attribute_length);
 }

jbmc/src/java_bytecode/java_types.h

@@ -111,6 +111,16 @@ class java_class_typet:public class_typet
     return set(ID_access, access);
   }
 
+  const bool get_is_inner_class() const
+  {
+    return get_bool(ID_is_inner_class);
+  }
+
+  void set_is_inner_class(const bool &is_inner_class)
+  {
+    return set(ID_is_inner_class, is_inner_class);
+  }
+
   bool get_final()
   {
     return get_bool(ID_final);

jbmc/unit/Makefile

@@ -12,6 +12,7 @@ SRC += java_bytecode/goto-programs/class_hierarchy_output.cpp \
        java_bytecode/java_bytecode_convert_class/convert_java_annotations.cpp \
        java_bytecode/java_bytecode_convert_method/convert_invoke_dynamic.cpp \
        java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp \
+       java_bytecode/java_bytecode_parser/parse_java_attributes.cpp \
        java_bytecode/java_object_factory/gen_nondet_string_init.cpp \
        java_bytecode/java_bytecode_parse_lambdas/java_bytecode_parse_lambda_method_table.cpp \
        java_bytecode/java_bytecode_parse_lambdas/java_bytecode_convert_class_lambda_method_handles.cpp \

jbmc/unit/java_bytecode/java_bytecode_parser/InnerClasses.java

@@ -0,0 +1,115 @@
+public class InnerClasses {
+    public class PublicInnerClass {
+        public int i;
+        public PublicInnerClass(int i) {
+            this.i = i;
+        }
+    }
+    class DefaultInnerClass {
+        int i;
+        DefaultInnerClass(int i) {
+            this.i = i;
+        }
+    }
+    protected class ProtectedInnerClass {
+        protected int i;
+        protected ProtectedInnerClass(int i) {
+            this.i = i;
+        }
+    }
+    private class PrivateInnerClass {
+        private int i;
+        private PrivateInnerClass(int i) {
+            this.i = i;
+        }
+    }
+}
+
+class InnerClassesDefault {
+    public class PublicInnerClass {
+        public int i;
+        public PublicInnerClass(int i) {
+            this.i = i;
+        }
+    }
+    class DefaultInnerClass {
+        int i;
+        DefaultInnerClass(int i) {
+            this.i = i;
+        }
+    }
+    protected class ProtectedInnerClass {
+        protected int i;
+        protected ProtectedInnerClass(int i) {
+            this.i = i;
+        }
+    }
+    private class PrivateInnerClass {
+        private int i;
+        private PrivateInnerClass(int i) {
+            this.i = i;
+        }
+    }
+}
+
+class InnerClassesDeeplyNested {
+    class SinglyNestedClass {
+        int i;
+        SinglyNestedClass(int i) {
+            this.i = i;
+        }
+        public class PublicDoublyNestedInnerClass {
+            public int i;
+            public PublicDoublyNestedInnerClass(int i) {
+                this.i = i;
+            }
+        }
+        class DefaultDoublyNestedInnerClass {
+            int i;
+            DefaultDoublyNestedInnerClass(int i) {
+                this.i = i;
+            }
+        }
+        protected class ProtectedDoublyNestedInnerClass {
+            protected int i;
+            protected ProtectedDoublyNestedInnerClass(int i) {
+                this.i = i;
+            }
+        }
+        private class PrivateDoublyNestedInnerClass {
+            private int i;
+            private PrivateDoublyNestedInnerClass(int i) {
+                this.i = i;
+            }
+        }
+    }
+}
+
+class ContainsAnonymousClass {
+    interface InnerInterface {
+        int i = 0;
+    }
+    public InnerInterface anonymousPublic = new InnerInterface() {
+        int i = 1;
+    };
+    InnerInterface anonymousDefault = new InnerInterface() {
+        int i = 2;
+    };
+    protected InnerInterface anonymousProtected = new InnerInterface() {
+        int i = 3;
+    };
+    private InnerInterface anonymousPrivate = new InnerInterface() {
+        int i = 4;
+    };
+}
+
+class ContainsLocalClass {
+    public void test() {
+        class LocalClass {
+            int i = 55;
+            LocalClass(int i) {
+                this.i = i;
+            }
+        }
+    }
+}