Merge pull request #3469 from smowton/smowton/fix/java-null-check-ordering

Add null check on virtual function calls after its subexpressions

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 \