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/src/java_bytecode/java_bytecode_instrument.cpp

@@ -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/unit/Makefile

@@ -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/unit/java_bytecode/java_bytecode_instrument/A.class

@@ -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/unit/java_bytecode/java_bytecode_instrument/B.class

@@ -0,0 +1,94 @@
+/*******************************************************************\
+
+ 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>
+
+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");
+    namespacet ns(symbol_table);
+    goto_functionst goto_functions;
+    goto_convert(symbol_table, goto_functions, null_message_handler);
+
+    WHEN("The virtual call is converted")
+    {
+      const auto &main_function =
+        goto_functions.function_map.at("java::VirtualCallNullChecks.main:()V");
+
+      THEN("The callee should be of the form some_ptr->field")
+      {
+        bool found_virtual_call = false;
+
+        for(const auto &instruction : main_function.body.instructions)
+        {
+          if(instruction.type == FUNCTION_CALL)
+          {
+            const auto &virtual_call = to_code_function_call(instruction.code);
+            if(virtual_call.function().id() == ID_virtual_function)
+            {
+              REQUIRE(virtual_call.arguments().size() == 1);
+              const auto &this_argument = virtual_call.arguments()[0];
+              REQUIRE(this_argument.id() == ID_member);
+              REQUIRE(this_argument.op0().id() == ID_dereference);
+              found_virtual_call = true;
+            }
+          }
+        }
+
+        REQUIRE(found_virtual_call);
+      }
+      THEN("All pointer usages should be safe")
+      {
+        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));
+            }
+          }
+        }
+      }
+    }
+  }
+}