Uses the containing_class to determine accessibility.

An inner class is only as accessible as its containing classes. When determining the accessibility of an inner class, take the strictest of all of its containing classes.

Author: jeannielynnmoulton

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -279,6 +279,7 @@ void java_bytecode_convert_classt::convert(
   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);
+  class_type.set_containing_class(c.containing_class);
   if(c.is_enum)
   {
     if(max_array_length != 0 && c.enum_elements > max_array_length)
@@ -1153,3 +1154,60 @@ void mark_java_implicitly_generic_class_type(
     }
   }
 }
+
+/// If access1 is stricter than access2, returns true, otherwise returns false.
+/// Assumed order of strictness:
+/// private, default (package_private), protected, public
+bool compare_access(irep_idt access1, irep_idt access2)
+{
+  if(access1 == access2)
+    return false;
+  if(access1 == ID_private)
+    return true;
+  if(access1 == ID_default && access2 != ID_private)
+    return true;
+  if(access1 == ID_protected && access2 == ID_public)
+    return true;
+  return false;
+}
+
+/// Inner class accessibility depends not only on the inner class' access
+/// modifier, but the access modifiers of its containing classes. This checks
+/// all of the containing classes of an inner class and sets the access of the
+/// inner class to the strictest of its containing classes. For example, for a
+/// deeply nested structure Outer.Middle.Inner with access modifiers public,
+/// private, public, respectively, the access of Inner should be private
+/// (not public) because one of its containing classes has private access.
+/// \param inner_class_name
+/// \param symbol_table
+void determine_inner_class_accessibility(
+  const irep_idt &inner_class_name,
+  symbol_tablet &symbol_table)
+{
+  const std::string qualified_inner_class_name =
+    "java::" + id2string(inner_class_name);
+  PRECONDITION(symbol_table.has_symbol(qualified_inner_class_name));
+  symbolt &inner_class_symbol =
+    symbol_table.get_writeable_ref(qualified_inner_class_name);
+  java_class_typet &inner_class_type =
+    to_java_class_type(inner_class_symbol.type);
+
+  if(!inner_class_type.get_is_inner_class())
+    return;
+  if(inner_class_type.get_containing_class().empty())
+    return;
+  const std::string qualified_containing_class_name =
+    "java::" + id2string(inner_class_type.get_containing_class());
+  PRECONDITION(symbol_table.has_symbol(qualified_containing_class_name));
+  symbolt &containing_class_symbol =
+    symbol_table.get_writeable_ref(qualified_containing_class_name);
+  java_class_typet &containing_class_type =
+    to_java_class_type(containing_class_symbol.type);
+
+  if(
+    compare_access(
+      containing_class_type.get_access(), inner_class_type.get_access()))
+  {
+    inner_class_type.set_access(containing_class_type.get_access());
+  }
+}

jbmc/src/java_bytecode/java_bytecode_convert_class.h

@@ -41,6 +41,10 @@ void mark_java_implicitly_generic_class_type(
   const irep_idt &class_name,
   symbol_tablet &symbol_table);
 
+void determine_inner_class_accessibility(
+  const irep_idt &class_name,
+  symbol_tablet &symbol_table);
+
 /// An exception that is raised checking whether a class is implicitly
 /// generic if a symbol for an outer class is missing
 class missing_outer_class_symbol_exceptiont : public std::logic_error

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -677,6 +677,16 @@ bool java_bytecode_languaget::typecheck(
     }
   }
 
+  // Determine inner class accessibility by taking the most strict of access
+  // modifiers of all of the containing classes
+  for(const auto &c : java_class_loader.get_class_with_overlays_map())
+  {
+    if(c.second.front().parsed_class.containing_class.empty())
+      continue;
+    determine_inner_class_accessibility(
+      c.second.front().parsed_class.name, symbol_table);
+  }
+
   // Infer fields on opaque types based on the method instructions just loaded.
   // For example, if we don't have bytecode for field x of class A, but we can
   // see an int-typed getfield instruction referring to it, add that field now.

jbmc/src/java_bytecode/java_bytecode_parser.cpp

@@ -1643,6 +1643,11 @@ void java_bytecode_parsert::rinner_classes_attribute(
     }
     else
     {
+      std::string outer_class_info_name =
+        class_infot(pool_entry(outer_class_info_index))
+          .get_name(pool_entry_lambda);
+      parsed_class.containing_class =
+        constant(outer_class_info_index).type().get(ID_C_base_name);
       parsed_class.is_private = is_private;
       parsed_class.is_protected = is_protected;
       parsed_class.is_public = is_public;