Add null check on virtual function calls after its subexpressions

For example, for "x->y . f()" we should `assert(x != null); assert(x->y != null);`,
not the other way around.

Author: smowton

jbmc/regression/jbmc/dereference-virtual-call/A.class

@@ -0,0 +1,26 @@
+public class Test {
+
+  public static void main(int argc) {
+
+    A a = argc == 1 ? new A() : null;
+    a.field.virtualmethod();
+
+  }
+
+}
+
+class A {
+
+  public B field;
+
+  public A() {
+    field = new B();
+  }
+
+}
+
+class B {
+
+  public void virtualmethod() { }
+
+}

jbmc/regression/jbmc/dereference-virtual-call/B.class

@@ -0,0 +1,17 @@
+CORE
+Test.class
+--function Test.main
+^EXIT=10$
+^SIGNAL=0$
+\[java::Test\.main:\(I\)V\.null-pointer-exception\.3\] line 6.*SUCCESS
+\[java::Test\.main:\(I\)V\.null-pointer-exception\.2\] line 6.*FAILURE
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+--
+This is testing the construct "something->field . some_method()"
+That requires a null check against "something" (for the deref to read 'field')
+and another one against "something->field" (for the instance method call).
+If they're made in the correct order (check "something" first) then one of the
+null checks cannot fail in this particular scenario; if they're made in the
+wrong order ("something->field" first) then they can both fail.

jbmc/regression/jbmc/dereference-virtual-call/Test.class

@@ -445,6 +445,9 @@ void java_bytecode_instrumentt::instrument_code(codet &code)
     const java_method_typet &function_type =
       to_java_method_type(code_function_call.function().type());
 
+    for(const auto &arg : code_function_call.arguments())
+      add_expr_instrumentation(block, arg);
+
     // Check for a null this-argument of a virtual call:
     if(function_type.has_this())
     {
@@ -453,9 +456,6 @@ void java_bytecode_instrumentt::instrument_code(codet &code)
         code_function_call.source_location()));
     }
 
-    for(const auto &arg : code_function_call.arguments())
-      add_expr_instrumentation(block, arg);
-
     prepend_instrumentation(code, block);
   }
 

jbmc/regression/jbmc/dereference-virtual-call/Test.java

@@ -19,6 +19,7 @@ SRC += java_bytecode/ci_lazy_methods/lazy_load_lambdas.cpp \
        java_bytecode/java_bytecode_convert_method/convert_initalizers.cpp \
        java_bytecode/java_bytecode_convert_method/convert_invoke_dynamic.cpp \
        java_bytecode/java_bytecode_convert_method/convert_method.cpp \
+       java_bytecode/java_bytecode_instrument/virtual_call_null_checks.cpp \
        java_bytecode/java_bytecode_parse_generics/parse_bounded_generic_inner_classes.cpp \
        java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp \
        java_bytecode/java_bytecode_parse_generics/parse_functions_with_generics.cpp \

jbmc/regression/jbmc/dereference-virtual-call/test.desc

@@ -0,0 +1,26 @@
+public class VirtualCallNullChecks {
+
+  public static void main() {
+
+    A a = new A();
+    a.field.virtualmethod();
+
+  }
+
+}
+
+class A {
+
+  public B field;
+
+  public A() {
+    field = new B();
+  }
+
+}
+
+class B {
+
+  public void virtualmethod() { }
+
+}

jbmc/src/java_bytecode/java_bytecode_instrument.cpp

@@ -0,0 +1,6 @@
+testing-utils
+java-testing-utils
+analyses
+goto-programs
+java_bytecode
+util

jbmc/unit/Makefile

@@ -0,0 +1,111 @@
+/*******************************************************************\
+
+ Module: Unit test to check Java virtual calls via a pointer
+         yield a correct sequence of not-null assumptions.
+
+ Author: Diffblue Limited.
+
+\*******************************************************************/
+
+#include <testing-utils/catch.hpp>
+#include <testing-utils/message.h>
+#include <java-testing-utils/load_java_class.h>
+
+#include <analyses/local_safe_pointers.h>
+#include <goto-programs/goto_convert_functions.h>
+#include <java_bytecode/java_bytecode_language.h>
+#include <util/expr_iterator.h>
+
+// We're expecting a call "something->field . B.virtualmethod()":
+static bool is_expected_virtualmethod_call(
+  const goto_programt::instructiont &instruction)
+{
+  if(instruction.type != FUNCTION_CALL)
+    return false;
+  const auto &virtual_call = to_code_function_call(instruction.code);
+  const auto &called_function = virtual_call.function();
+  if(called_function.id() != ID_virtual_function)
+    return false;
+  if(called_function.get(ID_identifier) != "java::B.virtualmethod:()V")
+    return false;
+  if(virtual_call.arguments().size() != 1)
+    return false;
+  const auto &this_argument = virtual_call.arguments()[0];
+  if(this_argument.id() != ID_member)
+    return false;
+  if(this_argument.op0().id() != ID_dereference)
+    return false;
+
+  return true;
+}
+
+SCENARIO(
+  "java_bytecode_virtual_call_null_checks",
+  "[core][java_bytecode][java_bytecode_instrument]")
+{
+  GIVEN("A class that makes a virtual call via a pointer")
+  {
+    symbol_tablet symbol_table = load_java_class(
+      "VirtualCallNullChecks", "./java_bytecode/java_bytecode_instrument");
+
+    WHEN("The virtual call is converted")
+    {
+      namespacet ns(symbol_table);
+      goto_functionst goto_functions;
+      goto_convert(symbol_table, goto_functions, null_message_handler);
+
+      const auto &main_function =
+        goto_functions.function_map.at("java::VirtualCallNullChecks.main:()V");
+
+      THEN("The loaded function should call B.virtualmethod via a pointer")
+      {
+        // This just checks that the class actually makes the expected call,
+        // i.e. that it hasn't been optimised away or similar.
+        std::size_t found_virtualmethod_calls =
+          std::count_if(
+            main_function.body.instructions.begin(),
+            main_function.body.instructions.end(),
+            is_expected_virtualmethod_call);
+
+        REQUIRE(found_virtualmethod_calls == 1);
+      }
+      THEN("All pointer usages should be safe")
+      {
+        // This analysis checks that any usage of a pointer is preceded by an
+        // assumption that it is non-null
+        // (e.g. assume(x != nullptr); y = x->...)
+        local_safe_pointerst safe_pointers(ns);
+        safe_pointers(main_function.body);
+
+        for(auto instrit = main_function.body.instructions.begin(),
+              instrend = main_function.body.instructions.end();
+            instrit != instrend; ++instrit)
+        {
+          for(auto it = instrit->code.depth_begin(),
+                itend = instrit->code.depth_end();
+              it != itend; ++it)
+          {
+            if(it->id() == ID_dereference)
+            {
+              const auto &deref = to_dereference_expr(*it);
+              REQUIRE(
+                safe_pointers.is_safe_dereference(deref, instrit));
+            }
+          }
+
+          for(auto it = instrit->guard.depth_begin(),
+                itend = instrit->guard.depth_end();
+              it != itend; ++it)
+          {
+            if(it->id() == ID_dereference)
+            {
+              const auto &deref = to_dereference_expr(*it);
+              REQUIRE(
+                safe_pointers.is_safe_dereference(deref, instrit));
+            }
+          }
+        }
+      }
+    }
+  }
+}