Inherit cproverNondetInitialize like a virtual method

We should look for it on the super class, and on that's super class,
and so on till we reach the top of the class hierarchy.

Author: owen-mc-diffblue

jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp

@@ -11,6 +11,8 @@ Author: Chris Smowton, [email protected]
 
 #include "ci_lazy_methods_needed.h"
 
+#include <goto-programs/resolve_inherited_component.h>
+
 #include <util/namespace.h>
 #include <util/std_types.h>
 
@@ -43,6 +45,24 @@ void ci_lazy_methods_neededt::add_clinit_call(const irep_idt &class_id)
     add_needed_method(clinit_wrapper);
 }
 
+/// For a given class id, if cproverNondetInitialize exists on it or any of its
+/// ancestors then note that it is needed.
+/// \param class_id: The given class id
+void ci_lazy_methods_neededt::add_cprover_nondet_initialize_if_it_exists(
+  const irep_idt &class_id)
+{
+  resolve_inherited_componentt resolve_inherited_component{symbol_table};
+  optionalt<resolve_inherited_componentt::inherited_componentt>
+    cprover_nondet_initialize = resolve_inherited_component(
+      class_id, "cproverNondetInitialize:()V", true);
+
+  if(cprover_nondet_initialize)
+  {
+    add_needed_method(
+      cprover_nondet_initialize->get_full_component_identifier());
+  }
+}
+
 /// Notes class `class_symbol_name` will be instantiated, or a static field
 /// belonging to it will be accessed. Also notes that its static initializer is
 /// therefore reachable.
@@ -54,11 +74,7 @@ bool ci_lazy_methods_neededt::add_needed_class(
   if(!instantiated_classes.insert(class_symbol_name).second)
     return false;
 
-  const std::string &class_name_string = id2string(class_symbol_name);
-  const irep_idt cprover_validate(
-    class_name_string + ".cproverNondetInitialize:()V");
-  if(symbol_table.symbols.count(cprover_validate))
-    add_needed_method(cprover_validate);
+  add_cprover_nondet_initialize_if_it_exists(class_symbol_name);
 
   // Special case for enums. We may want to generalise this, the comment in
   // \ref java_object_factoryt::gen_nondet_pointer_init (TG-4689).

jbmc/src/java_bytecode/ci_lazy_methods_needed.h

@@ -57,6 +57,7 @@ class ci_lazy_methods_neededt
   const select_pointer_typet &pointer_type_selector;
 
   void add_clinit_call(const irep_idt &class_id);
+  void add_cprover_nondet_initialize_if_it_exists(const irep_idt &class_id);
 
   void initialize_instantiated_classes_from_pointer(
     const pointer_typet &pointer_type,

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -897,17 +897,25 @@ void java_object_factoryt::gen_nondet_struct_init(
     }
   }
 
-  // If <class_identifier>.cproverNondetInitialize() can be found in the
-  // symbol table, we add a call:
+  // If cproverNondetInitialize() can be found in the symbol table as a method
+  // on this class or any parent, we add a call:
   // ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
   // expr.cproverNondetInitialize();
   // ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-  const irep_idt init_method_name =
-    "java::" + id2string(struct_tag) + ".cproverNondetInitialize:()V";
-  if(const auto init_func = symbol_table.lookup(init_method_name))
+  resolve_inherited_componentt resolve_inherited_component{symbol_table};
+  optionalt<resolve_inherited_componentt::inherited_componentt>
+    cprover_nondet_initialize = resolve_inherited_component(
+      "java::" + id2string(struct_tag), "cproverNondetInitialize:()V", true);
+
+  if(cprover_nondet_initialize)
+  {
+    const symbolt &cprover_nondet_initialize_symbol =
+      ns.lookup(cprover_nondet_initialize->get_full_component_identifier());
     assignments.add(
-      code_function_callt{init_func->symbol_expr(), {address_of_exprt{expr}}});
+      code_function_callt{cprover_nondet_initialize_symbol.symbol_expr(),
+                          {address_of_exprt{expr}}});
+  }
 }
 
 /// Generate code block that verifies that an expression of type float or