Standardise interface for accessing the owner of a symbol

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -689,10 +689,9 @@ void java_bytecode_convert_classt::convert(
     new_symbol.name=id2string(class_symbol.name)+"."+id2string(f.name);
     new_symbol.base_name=f.name;
     new_symbol.type=field_type;
-    // Annotating the type with ID_C_class to provide a static field -> class
-    // link matches the method used by java_bytecode_convert_method::convert
-    // for methods.
-    new_symbol.type.set(ID_C_class, class_symbol.name);
+    // Provide a static field -> class link, like
+    // java_bytecode_convert_method::convert does for method -> class.
+    set_owning_class(new_symbol, class_symbol.name);
     new_symbol.type.set(ID_C_field, f.name);
     new_symbol.type.set(ID_C_constant, f.is_final);
     new_symbol.pretty_name=id2string(class_symbol.pretty_name)+

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -419,6 +419,8 @@ void java_bytecode_convert_methodt::convert(
     get_method_identifier(class_symbol.name, m);
 
   method_id=method_identifier;
+  set_owning_class(
+    symbol_table.get_writeable_ref(method_identifier), class_symbol.name);
 
   // Obtain a std::vector of java_method_typet::parametert objects from the
   // (function) type of the symbol
@@ -428,7 +430,6 @@ void java_bytecode_convert_methodt::convert(
   // to the symbol later.
   java_method_typet method_type =
     to_java_method_type(symbol_table.lookup_ref(method_identifier).type);
-  method_type.set(ID_C_class, class_symbol.name);
   method_type.set_is_final(m.is_final);
   method_return_type = method_type.return_type();
   java_method_typet::parameterst &parameters = method_type.parameters();

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -496,7 +496,7 @@ static void create_stub_global_symbol(
   new_symbol.name = symbol_id;
   new_symbol.base_name = symbol_basename;
   new_symbol.type = symbol_type;
-  new_symbol.type.set(ID_C_class, class_id);
+  set_owning_class(new_symbol, class_id);
   // Public access is a guess; it encourages merging like-typed static fields,
   // whereas a more restricted visbility would encourage separating them.
   // Neither is correct, as without the class file we can't know the truth.

jbmc/src/java_bytecode/java_enum_static_init_unwind_handler.cpp

@@ -10,6 +10,7 @@ Author: Chris Smowton, [email protected]
 /// Unwind loops in static initializers
 
 #include "java_enum_static_init_unwind_handler.h"
+#include "java_utils.h"
 
 #include <util/invariant.h>
 #include <util/suffix.h>
@@ -76,11 +77,10 @@ tvt java_enum_static_init_unwind_handler(
     return tvt::unknown();
 
   const symbolt &function_symbol = symbol_table.lookup_ref(enum_function_id);
-  irep_idt class_id = function_symbol.type.get(ID_C_class);
-  INVARIANT(
-    !class_id.empty(), "functions should have their defining class annotated");
+  const auto class_id = owning_class(function_symbol);
+  INVARIANT(class_id, "Java methods should have a defining class.");
 
-  const typet &class_type = symbol_table.lookup_ref(class_id).type;
+  const typet &class_type = symbol_table.lookup_ref(*class_id).type;
   size_t unwinds = class_type.get_size_t(ID_java_enum_static_unwind);
   if(unwinds != 0 && unwind_count < unwinds)
   {

jbmc/src/java_bytecode/java_static_initializers.cpp

@@ -232,7 +232,7 @@ static void clinit_wrapper_do_recursive_calls(
       symbol_table.symbols.end(),
       [&](const std::pair<irep_idt, symbolt> &symbol) {
         if(
-          symbol.second.type.get(ID_C_class) == class_name &&
+          owning_class(symbol.second) == class_name &&
           symbol.second.is_static_lifetime &&
           !symbol.second.type.get_bool(ID_C_constant))
         {
@@ -352,10 +352,9 @@ static void create_clinit_wrapper_symbols(
   wrapper_method_symbol.pretty_name = wrapper_method_symbol.name;
   wrapper_method_symbol.base_name = "clinit_wrapper";
   wrapper_method_symbol.type = wrapper_method_type;
-  // Note this use of a type-comment to provide a back-link from a method
-  // to its associated class is the same one used in
-  // java_bytecode_convert_methodt::convert
-  wrapper_method_symbol.type.set(ID_C_class, class_name);
+  // This provides a back-link from a method to its associated class, as is done
+  // for java_bytecode_convert_methodt::convert.
+  set_owning_class(wrapper_method_symbol, class_name);
   wrapper_method_symbol.mode = ID_java;
   bool failed = symbol_table.add(wrapper_method_symbol);
   INVARIANT(!failed, "clinit-wrapper symbol should be fresh");
@@ -453,21 +452,20 @@ code_blockt get_thread_safe_clinit_wrapper_body(
   message_handlert &message_handler)
 {
   const symbolt &wrapper_method_symbol = symbol_table.lookup_ref(function_id);
-  irep_idt class_name = wrapper_method_symbol.type.get(ID_C_class);
-  INVARIANT(
-    !class_name.empty(), "wrapper function should be annotated with its class");
+  const auto class_name = owning_class(wrapper_method_symbol);
+  INVARIANT(class_name, "Wrapper function should have an owning class.");
 
   const symbolt &clinit_state_sym =
-    symbol_table.lookup_ref(clinit_state_var_name(class_name));
+    symbol_table.lookup_ref(clinit_state_var_name(*class_name));
   const symbolt &clinit_thread_local_state_sym =
-    symbol_table.lookup_ref(clinit_thread_local_state_var_name(class_name));
+    symbol_table.lookup_ref(clinit_thread_local_state_var_name(*class_name));
 
   // Create a function-local variable "init_complete". This variable is used to
   // avoid inspecting the global state (clinit_state_sym) outside of
   // the critical-section.
   const symbolt &init_complete = add_new_variable_symbol(
     symbol_table,
-    clinit_local_init_complete_var_name(class_name),
+    clinit_local_init_complete_var_name(*class_name),
     bool_typet(),
     nil_exprt(),
     true,
@@ -598,7 +596,7 @@ code_blockt get_thread_safe_clinit_wrapper_body(
     code_blockt init_body;
     clinit_wrapper_do_recursive_calls(
       symbol_table,
-      class_name,
+      *class_name,
       init_body,
       nondet_static,
       object_factory_parameters,
@@ -666,12 +664,11 @@ code_ifthenelset get_clinit_wrapper_body(
   //   }
   // }
   const symbolt &wrapper_method_symbol = symbol_table.lookup_ref(function_id);
-  irep_idt class_name = wrapper_method_symbol.type.get(ID_C_class);
-  INVARIANT(
-    !class_name.empty(), "wrapper function should be annotated with its class");
+  const auto class_name = owning_class(wrapper_method_symbol);
+  INVARIANT(class_name, "Wrapper function should have an owning class.");
 
   const symbolt &already_run_symbol =
-    symbol_table.lookup_ref(clinit_already_run_variable_name(class_name));
+    symbol_table.lookup_ref(clinit_already_run_variable_name(*class_name));
 
   equal_exprt check_already_run(
     already_run_symbol.symbol_expr(),
@@ -683,7 +680,7 @@ code_ifthenelset get_clinit_wrapper_body(
 
   clinit_wrapper_do_recursive_calls(
     symbol_table,
-    class_name,
+    *class_name,
     init_body,
     nondet_static,
     object_factory_parameters,
@@ -766,12 +763,9 @@ void stub_global_initializer_factoryt::create_stub_global_initializer_symbols(
       continue;
     }
 
-    const irep_idt class_id =
-      global_symbol.type.get(ID_C_class);
-    INVARIANT(
-      !class_id.empty(),
-      "static field should be annotated with its defining class");
-    stub_globals_by_class.insert({class_id, stub_global});
+    const auto class_id = owning_class(global_symbol);
+    INVARIANT(class_id, "Static field should have a defining class.");
+    stub_globals_by_class.insert({*class_id, stub_global});
   }
 
   // For each distinct class that has stub globals, create a clinit symbol:
@@ -799,10 +793,9 @@ void stub_global_initializer_factoryt::create_stub_global_initializer_symbols(
     static_init_symbol.base_name = "clinit():V";
     static_init_symbol.mode = ID_java;
     static_init_symbol.type = thunk_type;
-    // Note this use of a type-comment to provide a back-link from a method
-    // to its associated class is the same one used in
-    // java_bytecode_convert_methodt::convert
-    static_init_symbol.type.set(ID_C_class, it->first);
+    // This provides a back-link from a method to its associated class, as is
+    // done for java_bytecode_convert_methodt::convert.
+    set_owning_class(static_init_symbol, it->first);
 
     bool failed = symbol_table.add(static_init_symbol);
     INVARIANT(!failed, "symbol should not already exist");
@@ -839,17 +832,16 @@ code_blockt stub_global_initializer_factoryt::get_stub_initializer_body(
   message_handlert &message_handler)
 {
   const symbolt &stub_initializer_symbol = symbol_table.lookup_ref(function_id);
-  irep_idt class_id = stub_initializer_symbol.type.get(ID_C_class);
+  const auto class_id = owning_class(stub_initializer_symbol);
   INVARIANT(
-    !class_id.empty(),
-    "synthetic static initializer should be annotated with its class");
+    class_id, "Synthetic static initializer should have an owning class.");
   code_blockt static_init_body;
 
   // Add a standard nondet initialisation for each global declared on this
   // class. Note this is the same invocation used in
   // java_static_lifetime_init.
 
-  auto class_globals = stub_globals_by_class.equal_range(class_id);
+  auto class_globals = stub_globals_by_class.equal_range(*class_id);
   INVARIANT(
     class_globals.first != class_globals.second,
     "class with synthetic clinit should have at least one global to init");

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/src/jdiff/java_syntactic_diff.cpp

@@ -12,6 +12,7 @@ Author: Peter Schrammel
 #include "java_syntactic_diff.h"
 
 #include <goto-programs/goto_model.h>
+#include <java_bytecode/java_utils.h>
 
 bool java_syntactic_difft::operator()()
 {
@@ -35,16 +36,16 @@ bool java_syntactic_difft::operator()()
     CHECK_RETURN(fun1 != nullptr);
     const symbolt *fun2 = goto_model2.symbol_table.lookup(it->first);
     CHECK_RETURN(fun2 != nullptr);
-    const irep_idt &class_name = fun1->type.get(ID_C_class);
+    const optionalt<irep_idt> class_name = owning_class(*fun1);
     bool function_access_changed =
       fun1->type.get(ID_access) != fun2->type.get(ID_access);
     bool class_access_changed = false;
     bool field_access_changed = false;
-    if(!class_name.empty())
+    if(class_name)
     {
-      const symbolt *class1 = goto_model1.symbol_table.lookup(class_name);
+      const symbolt *class1 = goto_model1.symbol_table.lookup(*class_name);
       CHECK_RETURN(class1 != nullptr);
-      const symbolt *class2 = goto_model2.symbol_table.lookup(class_name);
+      const symbolt *class2 = goto_model2.symbol_table.lookup(*class_name);
       CHECK_RETURN(class2 != nullptr);
       class_access_changed =
         class1->type.get(ID_access) != class2->type.get(ID_access);

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);
+    }
+  }
+}