Skip to content

Commit 9cf2bfb

Browse files
authored
Merge pull request #3469 from smowton/smowton/fix/java-null-check-ordering
Add null check on virtual function calls after its subexpressions
2 parents 6d85303 + 6af4d4e commit 9cf2bfb

File tree

13 files changed

+190
-3
lines changed

13 files changed

+190
-3
lines changed
Binary file not shown.
Binary file not shown.
Binary file not shown.
Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
public class Test {
2+
3+
public static void main(int argc) {
4+
5+
A a = argc == 1 ? new A() : null;
6+
a.field.virtualmethod();
7+
8+
}
9+
10+
}
11+
12+
class A {
13+
14+
public B field;
15+
16+
public A() {
17+
field = new B();
18+
}
19+
20+
}
21+
22+
class B {
23+
24+
public void virtualmethod() { }
25+
26+
}
Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
CORE
2+
Test.class
3+
--function Test.main
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
\[java::Test\.main:\(I\)V\.null-pointer-exception\.3\] line 6.*SUCCESS
7+
\[java::Test\.main:\(I\)V\.null-pointer-exception\.2\] line 6.*FAILURE
8+
^VERIFICATION FAILED$
9+
--
10+
^warning: ignoring
11+
--
12+
This is testing the construct "something->field . some_method()"
13+
That requires a null check against "something" (for the deref to read 'field')
14+
and another one against "something->field" (for the instance method call).
15+
If they're made in the correct order (check "something" first) then one of the
16+
null checks cannot fail in this particular scenario; if they're made in the
17+
wrong order ("something->field" first) then they can both fail.

jbmc/src/java_bytecode/java_bytecode_instrument.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -445,6 +445,9 @@ void java_bytecode_instrumentt::instrument_code(codet &code)
445445
const java_method_typet &function_type =
446446
to_java_method_type(code_function_call.function().type());
447447

448+
for(const auto &arg : code_function_call.arguments())
449+
add_expr_instrumentation(block, arg);
450+
448451
// Check for a null this-argument of a virtual call:
449452
if(function_type.has_this())
450453
{
@@ -453,9 +456,6 @@ void java_bytecode_instrumentt::instrument_code(codet &code)
453456
code_function_call.source_location()));
454457
}
455458

456-
for(const auto &arg : code_function_call.arguments())
457-
add_expr_instrumentation(block, arg);
458-
459459
prepend_instrumentation(code, block);
460460
}
461461

jbmc/unit/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,7 @@ SRC += java_bytecode/ci_lazy_methods/lazy_load_lambdas.cpp \
1919
java_bytecode/java_bytecode_convert_method/convert_initalizers.cpp \
2020
java_bytecode/java_bytecode_convert_method/convert_invoke_dynamic.cpp \
2121
java_bytecode/java_bytecode_convert_method/convert_method.cpp \
22+
java_bytecode/java_bytecode_instrument/virtual_call_null_checks.cpp \
2223
java_bytecode/java_bytecode_parse_generics/parse_bounded_generic_inner_classes.cpp \
2324
java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp \
2425
java_bytecode/java_bytecode_parse_generics/parse_functions_with_generics.cpp \
Binary file not shown.
Binary file not shown.
Binary file not shown.

0 commit comments

Comments
 (0)