Add owning class functions as interface to the owner of a symbol

Without the functions added by this commit, the only way to access the
owner of a symbol for static fields and java methods is through
`symbol.type.get(ID_C_class)`. When this technique is used by downstream
repositories, they are vulnerable to being broken by upstream changes to
how this information is stored in JBMC. The intension of this commit is
that the two new functions added will be the standard interface to this
symbol -> owner link. This means that future changes to how this
information is stored can be made without breaking downstream
repositories by changing these two functions.

Author: thomasspriggs

jbmc/src/java_bytecode/java_utils.cpp

@@ -464,3 +464,14 @@ symbolt &fresh_java_symbol(
   return get_fresh_aux_symbol(
     type, name_prefix, basename_prefix, source_location, ID_java, symbol_table);
 }
+
+optionalt<irep_idt> owning_class(const symbolt &symbol)
+{
+  const irep_idt &class_id = symbol.type.get(ID_C_class);
+  return class_id.empty() ? optionalt<irep_idt>{} : class_id;
+}
+
+void set_owning_class(symbolt &symbol, const irep_idt &owning_class)
+{
+  symbol.type.set(ID_C_class, owning_class);
+}

jbmc/src/java_bytecode/java_utils.h

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 #include <unordered_set>
 
 #include <util/message.h>
+#include <util/optional.h>
 #include <util/std_expr.h>
 #include <util/symbol_table.h>
 
@@ -115,4 +116,14 @@ symbolt &fresh_java_symbol(
   const irep_idt &function_name,
   symbol_table_baset &symbol_table);
 
+/// Gets the identifier of the class which owns a given \p symbol. If the symbol
+/// is not owned by a class the an empty optional is returned. This is used for
+/// method symbols and static field symbols to link them back to the class which
+/// owns them.
+optionalt<irep_idt> owning_class(const symbolt &symbol);
+
+/// Sets the identifier of the class which owns a given \p symbol to \p
+/// owning_class.
+void set_owning_class(symbolt &symbol, const irep_idt &owning_class);
+
 #endif // CPROVER_JAVA_BYTECODE_JAVA_UTILS_H

jbmc/unit/java_bytecode/java_utils_test.cpp

@@ -368,3 +368,28 @@ SCENARIO("Test pretty printing auxiliary function", "[core][java_util_test]")
     }
   }
 }
+
+SCENARIO("Test symbol ownership.", "[core][java_util_test]")
+{
+  WHEN("We have a new symbol.")
+  {
+    symbolt symbol;
+
+    THEN("The symbol has no owner.")
+    {
+      REQUIRE(!owning_class(symbol).has_value());
+    }
+  }
+
+  WHEN("The owning class of a symbol is set.")
+  {
+    const auto owning_class = "java::java.lang.object";
+    symbolt symbol;
+    set_owning_class(symbol, owning_class);
+
+    THEN("Getting the owning class of a symbol returns the class set.")
+    {
+      REQUIRE(id2string(*::owning_class(symbol)) == owning_class);
+    }
+  }
+}