Uses containing class to determine accessibility

Author: jeannielynnmoulton

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -1154,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.