Add call to cproverValidate in nondet initialization TG-1313

regression/cbmc-java/NondetInitValidate/Test.java

@@ -0,0 +1,31 @@
+import org.cprover.CProver;
+
+class Test {
+    int size;
+    int[] data1;
+    int[] data2;
+
+    void cproverNondetInitialize() {
+        // This specifies invariants about object of this class.
+        // This avoids finding spurious bugs.
+        CProver.assume(data1 != null && data2 != null && size == data1.length + data2.length);
+    }
+
+    int check(int x) {
+        int i;
+        if(x >= size || x < 0)
+            return -1;
+
+        assert(data1 != null || data2 == null);
+
+        if (x >= data1.length) {
+            i = x - data1.length;
+            assert(i < data2.length);
+            return data2[i];
+        } else {
+            assert(x < data1.length);
+            return data1[x];
+        }
+
+    }
+}

regression/cbmc-java/NondetInitValidate/test.desc

@@ -0,0 +1,5 @@
+CORE
+Test.class
+--function Test.check
+^VERIFICATION SUCCESSFUL$
+--

regression/cbmc-java/NondetInitValidate/test_lazy.desc

@@ -0,0 +1,5 @@
+CORE
+Test.class
+--function Test.check --lazy-methods
+^VERIFICATION SUCCESSFUL$
+--

src/java_bytecode/ci_lazy_methods_needed.cpp

@@ -34,8 +34,14 @@ bool ci_lazy_methods_neededt::add_needed_class(
 {
   if(!needed_classes.insert(class_symbol_name).second)
     return false;
-  const irep_idt clinit_name(id2string(class_symbol_name)+".<clinit>:()V");
+  const std::string &class_name_string = id2string(class_symbol_name);
+  const irep_idt clinit_name(class_name_string + ".<clinit>:()V");
   if(symbol_table.symbols.count(clinit_name))
     add_needed_method(clinit_name);
+
+  const irep_idt cprover_validate(
+    class_name_string + ".cproverNondetInitialize:()V");
+  if(symbol_table.symbols.count(cprover_validate))
+    add_needed_method(cprover_validate);
   return true;
 }

src/java_bytecode/java_object_factory.cpp

@@ -926,6 +926,8 @@ symbol_exprt java_object_factoryt::gen_nondet_subtype_pointer_init(
 /// Initializes an object tree rooted at `expr`, allocating child objects as
 /// necessary and nondet-initializes their members, or if MUST_UPDATE_IN_PLACE
 /// is set, re-initializes already-allocated objects.
+/// After initialization calls validation method
+/// `expr.cproverNondetInitialize()` if it was provided by the user.
 ///
 /// \param assignments:
 ///   The code block to append the new instructions to.
@@ -1028,6 +1030,26 @@ void java_object_factoryt::gen_nondet_struct_init(
         substruct_in_place);
     }
   }
+
+  // If <class_identifier>.cproverValidate() can be found in the
+  // symbol table, we add a call:
+  // ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+  // expr.cproverValidate();
+  // ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+  const irep_idt validate_method_name =
+    "java::" + id2string(class_identifier) + ".cproverNondetInitialize:()V";
+
+  if(const auto func = symbol_table.lookup(validate_method_name))
+  {
+    const code_typet &type = to_code_type(func->type);
+    code_function_callt fun_call;
+    fun_call.function() = func->symbol_expr();
+    if(type.has_this())
+      fun_call.arguments().push_back(address_of_exprt(expr));
+
+    assignments.add(fun_call);
+  }
 }
 
 /// Initializes a primitive-typed or referece-typed object tree rooted at