From 6af4d4ea319d142389dd4608e384b70b52263929 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Fri, 23 Nov 2018 14:54:14 +0000 Subject: [PATCH] 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. --- .../jbmc/dereference-virtual-call/A.class | Bin 0 -> 242 bytes .../jbmc/dereference-virtual-call/B.class | Bin 0 -> 234 bytes .../jbmc/dereference-virtual-call/Test.class | Bin 0 -> 368 bytes .../jbmc/dereference-virtual-call/Test.java | 26 ++++ .../jbmc/dereference-virtual-call/test.desc | 17 +++ .../java_bytecode_instrument.cpp | 6 +- jbmc/unit/Makefile | 1 + .../java_bytecode_instrument/A.class | Bin 0 -> 259 bytes .../java_bytecode_instrument/B.class | Bin 0 -> 251 bytes .../VirtualCallNullChecks.class | Bin 0 -> 354 bytes .../VirtualCallNullChecks.java | 26 ++++ .../module_dependencies.txt | 6 + .../virtual_call_null_checks.cpp | 111 ++++++++++++++++++ 13 files changed, 190 insertions(+), 3 deletions(-) create mode 100644 jbmc/regression/jbmc/dereference-virtual-call/A.class create mode 100644 jbmc/regression/jbmc/dereference-virtual-call/B.class create mode 100644 jbmc/regression/jbmc/dereference-virtual-call/Test.class create mode 100644 jbmc/regression/jbmc/dereference-virtual-call/Test.java create mode 100644 jbmc/regression/jbmc/dereference-virtual-call/test.desc create mode 100644 jbmc/unit/java_bytecode/java_bytecode_instrument/A.class create mode 100644 jbmc/unit/java_bytecode/java_bytecode_instrument/B.class create mode 100644 jbmc/unit/java_bytecode/java_bytecode_instrument/VirtualCallNullChecks.class create mode 100644 jbmc/unit/java_bytecode/java_bytecode_instrument/VirtualCallNullChecks.java create mode 100644 jbmc/unit/java_bytecode/java_bytecode_instrument/module_dependencies.txt create mode 100644 jbmc/unit/java_bytecode/java_bytecode_instrument/virtual_call_null_checks.cpp 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 0000000000000000000000000000000000000000..41d500574defd069664ceb9ef0fa255d7057bde7 GIT binary patch literal 242 zcmXYr!A`TF zWrSpAOEceZaO(oN-arCVH0kaiD9_Z#Q=fcuH}@o&aDTWV;JN1KF>+D&DL)*r6o BB=!IR literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..7bd5e52298f106cb481eaa6bbc4a668cd1012a9a GIT binary patch literal 234 zcmZ9FF%Q8|6ot=iRjC$}Fi4CTbTNv7#3T$F`ztRzsWz$C{x6fn;0O3o;W<#qCETKKa}5A`cn^82q{@gPTF{f8P2$ giKjJwfbP5yY}RUNc35jav{$A~{9|3l>KqzyzD)Tfs{jB1 literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..3972dd2cd6882b0f546c2f3199a6df67df2a231a GIT binary patch literal 368 zcmW+x%Sr=55Uk!u#$7j0Ur96vZ&ATqyeXm)0>Y|?1i|BMcGQWRjl|u2k2lYP7*Oy7 z{3x+!=g`$%Q&m0l`}g$&;0PTb0u6yR9~K%OmvtW-*c8|jXc9^%I@Q@J!S3$e5}b=! ztO(Umr|LSNMruBiQNoNfl{#hUUK&|>n91?em3%I4Ii27SXZd`r2HL2-k$TAvCvqVJ ztiU7Cd4Lw$0^0$04B;3Bp=LC_M5YhDn`olOOu6@3B{4rJ>>snS&)XJyp5-!`s_bzV zV;3dM#69SaEH_`!HEyh;cc}4jf*4+~J8ypG` iKHz-9HFm48S73ARqRv50-d5pBz^a}JR5`6y2field . 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 0000000000000000000000000000000000000000..44a74d0497d89473f7aafa7e758b0e87e73646cd GIT binary patch literal 259 zcmXYru}Z^G6o$W>q=}8ONvo5SqjsaEulV&Z!_NI}5|@S(&L zaXI|o`M(3_`{&~eIAt#;B#p>oJkmZrh7qHPT}AKS8n;yVv+0>4Jhzo?E(8yc7K$KW zFO4Fd*~-k@=fc#tx^S|IZ`N&Hnk(DE{=(Kxt6i?0o43y8kEVQjIbP{kozN#%sA)pP zmV`@1))f<{tB1*Tu`*@Dfjkt-qtbWUf09e#ZJ`r-3I@i;O);$WDdlT Oo`4}KBe8dcJqEw~Ei1MF literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..608fd6f4ca0924e72eef8361a0e265c44c8b53c3 GIT binary patch literal 251 zcmZ9G%?`m(5QWdwPpRLPAdy&N!NyW7G_evE#QwIu(aY5))%LxtBo-dPLy0Mgg-Pbj z%sJm;p0E1@z!Y^0IaEwkP1Fd*nF>@qC*%ghJt1$0o+LC@Dv;~s?8s;*9L-KGRZ*M> zeU`BwdIW15CXp+bDhs>&Z)gjx*NN7)FWu8+d=#muB98)r7KCPYPqYXQlZ|tfZj3$* s{v|7en?dkHy!Chz&%)>iy7EFWS&JXD#ajBIolnZdKh|cf%%K764b>?tYXATM literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..7f1d5a85e796443e492738e9038833bdb010bb6f GIT binary patch literal 354 zcmZus%Syvg5IvKpjj@T3`Y5e<7(MRxITL5Qw*WnJL0DyUmL&0*|2ulTlmg*9jJpNQtKJK&SJ;25Hq6F~?HvS+ Jd&oY literal 0 HcmV?d00001 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)); + } + } + } + } + } + } +}