Fix bug assigning nondetWithNull to Object

In the case where we really want to create a nondet java.lang.Object,
the java compiler does not emit a checkcast instruction, which means
that our attempt to divine the nondet type using checkcast fails.

This commit changes the behaviour of nondetWithNull so that it will
create an Object if the following instruction is not a checkcast.
The test nondetCastToObject tests this behaviour.

Author: reuk

regression/cbmc-java/Makefile

@@ -18,3 +18,16 @@ show:
 			vim -o "$$dir/*.java" "$$dir/*.out"; \
 		fi; \
 	done;
+
+%.class: %.java ../../src/org.cprover.jar
+	javac -g -cp ../../src/org.cprover.jar:. $<
+
+nondet_java_files := $(shell find . -name "Nondet*.java")
+nondet_class_files := $(patsubst %.java, %.class, $(nondet_java_files))
+
+.PHONY: nondet-class-files
+nondet-class-files: $(nondet_class_files)
+
+.PHONY: clean-nondet-class-files
+clean-nondet-class-files:
+	-rm $(nondet_class_files)

regression/cbmc-java/nondetCastToObject/NondetCastToObject.class

@@ -0,0 +1,11 @@
+import org.cprover.CProver;
+
+class NondetCastToObject
+{
+  void foo()
+  {
+    Object o = CProver.nondetWithNull();
+    CProver.assume(o != null);
+    assert o != null;
+  }
+}

regression/cbmc-java/nondetCastToObject/NondetCastToObject.java

@@ -0,0 +1,6 @@
+CORE
+NondetCastToObject.class
+--function NondetCastToObject.foo
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-java/nondetCastToObject/test.desc

@@ -74,8 +74,8 @@ static void remove_assert_after_generic_nondet(exprt &expr)
           if(&(*it)==before_1)
           {
             const auto next_it=std::next(it);
-            assert(next_it!=end);
-            if(next_it->id()==ID_code &&
+            if(next_it!=end &&
+               next_it->id()==ID_code &&
                to_code(*next_it).get_statement()=="assert")
             {
               *next_it=code_skipt();
@@ -1288,16 +1288,23 @@ codet java_bytecode_convert_methodt::convert_instructions(
           ".*org.cprover.CProver.(nondetWithNull|nondetWithoutNull).*")) &&
       !working_set.empty())
     {
+      // Get the nondet function code type.
+      auto func_type=to_code_type(arg0.type());
+
+      // Find the next instruction.
       const auto working_set_begin=working_set.begin();
       const auto next_address=address_map.find(*working_set_begin);
       assert(next_address!=address_map.end());
 
       // Find the correct return type.
       const auto next_source=next_address->second.source;
       const auto next_statement=next_source->statement;
-      assert(next_statement=="checkcast");
-      assert(next_source->args.size()>=1);
-      const auto return_type=pointer_typet(next_source->args[0].type());
+      // The next return type is the casted-to type *if* the next statement is
+      // a checkcast. Otherwise, we leave it as-is.
+      const auto return_type=
+        (next_statement=="checkcast" && next_source->args.size()>=1) ?
+        pointer_typet(next_source->args[0].type()) :
+        func_type.return_type();
 
       // Reconstruct a function call with the correct return type.
       code_function_callt call;
@@ -1306,11 +1313,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
       loc.set_function(method_id);
       call.add_source_location()=loc;
       call.function().add_source_location()=loc;
-
-      // Update the pointed-to type.
-      auto func_type=arg0.type();
-      to_code_type(func_type).return_type()=return_type;
-
+      func_type.return_type()=return_type;
       call.function()=symbol_exprt(arg0.get(ID_identifier), func_type);
       call.lhs()=tmp_variable("return", return_type);