diff --git a/jbmc/regression/jbmc/dereference-virtual-call/A.class b/jbmc/regression/jbmc/dereference-virtual-call/A.class new file mode 100644 index 00000000000..41d500574de Binary files /dev/null and b/jbmc/regression/jbmc/dereference-virtual-call/A.class differ diff --git a/jbmc/regression/jbmc/dereference-virtual-call/B.class b/jbmc/regression/jbmc/dereference-virtual-call/B.class new file mode 100644 index 00000000000..7bd5e52298f Binary files /dev/null and b/jbmc/regression/jbmc/dereference-virtual-call/B.class differ diff --git a/jbmc/regression/jbmc/dereference-virtual-call/Test.class b/jbmc/regression/jbmc/dereference-virtual-call/Test.class new file mode 100644 index 00000000000..3972dd2cd68 Binary files /dev/null and b/jbmc/regression/jbmc/dereference-virtual-call/Test.class differ diff --git a/jbmc/regression/jbmc/dereference-virtual-call/Test.java b/jbmc/regression/jbmc/dereference-virtual-call/Test.java new file mode 100644 index 00000000000..d5af07e3498 --- /dev/null +++ b/jbmc/regression/jbmc/dereference-virtual-call/Test.java @@ -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() { } + +} diff --git a/jbmc/regression/jbmc/dereference-virtual-call/test.desc b/jbmc/regression/jbmc/dereference-virtual-call/test.desc new file mode 100644 index 00000000000..1df60514e8c --- /dev/null +++ b/jbmc/regression/jbmc/dereference-virtual-call/test.desc @@ -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. diff --git a/jbmc/src/java_bytecode/java_bytecode_instrument.cpp b/jbmc/src/java_bytecode/java_bytecode_instrument.cpp index 858ee62b92c..5af959797e9 100644 --- a/jbmc/src/java_bytecode/java_bytecode_instrument.cpp +++ b/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); } diff --git a/jbmc/unit/Makefile b/jbmc/unit/Makefile index 4022f95675d..229fd7fd906 100644 --- a/jbmc/unit/Makefile +++ b/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 \ diff --git a/jbmc/unit/java_bytecode/java_bytecode_instrument/A.class b/jbmc/unit/java_bytecode/java_bytecode_instrument/A.class new file mode 100644 index 00000000000..44a74d0497d Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_instrument/A.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_instrument/B.class b/jbmc/unit/java_bytecode/java_bytecode_instrument/B.class new file mode 100644 index 00000000000..608fd6f4ca0 Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_instrument/B.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_instrument/VirtualCallNullChecks.class b/jbmc/unit/java_bytecode/java_bytecode_instrument/VirtualCallNullChecks.class new file mode 100644 index 00000000000..7f1d5a85e79 Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_instrument/VirtualCallNullChecks.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_instrument/VirtualCallNullChecks.java b/jbmc/unit/java_bytecode/java_bytecode_instrument/VirtualCallNullChecks.java new file mode 100644 index 00000000000..639c926ab92 --- /dev/null +++ b/jbmc/unit/java_bytecode/java_bytecode_instrument/VirtualCallNullChecks.java @@ -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() { } + +} diff --git a/jbmc/unit/java_bytecode/java_bytecode_instrument/module_dependencies.txt b/jbmc/unit/java_bytecode/java_bytecode_instrument/module_dependencies.txt new file mode 100644 index 00000000000..4eee39351ab --- /dev/null +++ b/jbmc/unit/java_bytecode/java_bytecode_instrument/module_dependencies.txt @@ -0,0 +1,6 @@ +testing-utils +java-testing-utils +analyses +goto-programs +java_bytecode +util diff --git a/jbmc/unit/java_bytecode/java_bytecode_instrument/virtual_call_null_checks.cpp b/jbmc/unit/java_bytecode/java_bytecode_instrument/virtual_call_null_checks.cpp new file mode 100644 index 00000000000..d5f46b093e0 --- /dev/null +++ b/jbmc/unit/java_bytecode/java_bytecode_instrument/virtual_call_null_checks.cpp @@ -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 +#include +#include + +#include +#include +#include +#include + +// 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)); + } + } + } + } + } + } +}