Merge pull request diffblue#5104 from owen-mc-diffblue/owen/change-how-cprover-nondetinitialize-is-called

Make cproverNondetInitialize be inherited [TG-8677]

Author: owen-mc-diffblue

jbmc/regression/jbmc-inheritance/cprover_nondet_initialize/A.class

@@ -0,0 +1,68 @@
+import org.cprover.CProver;
+
+class A {
+  int x;
+
+  public void cproverNondetInitialize() { CProver.assume(x == 42); }
+}
+
+class B extends A {}
+
+class C extends B {}
+
+class F extends A {
+  public void cproverNondetInitialize() {}
+}
+
+interface I {
+}
+
+class J extends A implements I {
+}
+
+class K extends A {
+  int y;
+
+  public void cproverNondetInitialize() {
+    super.cproverNondetInitialize();
+    CProver.assume(y == 6);
+  }
+}
+
+abstract class M {
+  int x;
+
+  public void cproverNondetInitialize() { CProver.assume(x == 42); }
+}
+
+class N extends M {}
+
+public class Test {
+
+  void inheritanceTwoLevels(C c) {
+    if (c != null)
+      assert (c.x == 42);
+  }
+
+  void override(F f) {
+    if (f != null)
+      assert (f.x == 42);
+  }
+
+  void callingSuperCproverNondetInitialize(K k) {
+    if (k != null) {
+      assert (k.x == 42);
+      assert (k.y == 6);
+    }
+  }
+
+  void inheritanceFromAbstractClass(N n) {
+    if (n != null)
+      assert (n.x == 42);
+  }
+
+  void alsoImplementsInterface(J j) {
+    if (j != null)
+        assert (j.x == 42);
+    }
+}

jbmc/regression/jbmc-inheritance/cprover_nondet_initialize/B.class

@@ -0,0 +1,12 @@
+CORE
+Test.class
+--function Test.alsoImplementsInterface --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Check that if J extends A and implements the interface I,
+J.cproverNondetInitialize doesn't exist and A.cproverNondetInitialize does then
+a nondet J gets the constraints specified in A.cproverNondetInitialize.

jbmc/regression/jbmc-inheritance/cprover_nondet_initialize/C.class

@@ -0,0 +1,11 @@
+CORE
+Test.class
+--function Test.callingSuperCproverNondetInitialize --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Check that calls to super.cproverNondetInitialize call cproverNondetInitialize
+in the base class.

jbmc/regression/jbmc-inheritance/cprover_nondet_initialize/F.class

@@ -0,0 +1,12 @@
+CORE
+Test.class
+--function Test.inheritanceFromAbstractClass --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Check that if N extends the abstract class M, N.cproverNondetInitialize doesn't
+exist and M.cproverNondetInitialize does and is defined then a
+nondet N gets the constraints specified in M.cproverNondetInitialize.

jbmc/regression/jbmc-inheritance/cprover_nondet_initialize/I.class

@@ -0,0 +1,12 @@
+CORE
+Test.class
+--function Test.inheritanceTwoLevels --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Check that if C extends B, B extends A, B.cproverNondetInitialize and
+C.cproverNondetInitialize don't exist and A.cproverNondetInitialize does then a
+nondet C gets the constraints specified in A.cproverNondetInitialize.

jbmc/regression/jbmc-inheritance/cprover_nondet_initialize/J.class

@@ -0,0 +1,14 @@
+CORE
+Test.class
+--function Test.override --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+--
+Check that if F extends A, and A.cproverNondetInitialize and
+F.cproverNondetInitialize both exist then a nondet F doesn't get the constraint
+specified in A.cproverNondetInitialize. Specifically, it doesn't get the
+constraint that x must be 42, so when we assert that x is 42 jbmc is able to
+falsify it.

jbmc/regression/jbmc-inheritance/cprover_nondet_initialize/K.class

@@ -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/regression/jbmc-inheritance/cprover_nondet_initialize/M.class

@@ -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/regression/jbmc-inheritance/cprover_nondet_initialize/N.class

@@ -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

jbmc/regression/jbmc-inheritance/cprover_nondet_initialize/Test.class

@@ -30,9 +30,12 @@ SCENARIO(
     register_language(new_java_bytecode_language);
 
     // Add java.lang.Object to symbol table
+    java_class_typet jlo_class_type;
+    jlo_class_type.set_tag("java.lang.Object");
+    jlo_class_type.set_name("java::java.lang.Object");
     symbolt jlo_sym;
     jlo_sym.name = "java::java.lang.Object";
-    jlo_sym.type = struct_typet();
+    jlo_sym.type = jlo_class_type;
     jlo_sym.is_type = true;
     java_root_class(jlo_sym);
     bool failed = symbol_table.add(jlo_sym);