From ca3dbab050c9440f4131fd466bbea2c976f2d323 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Thu, 6 Jul 2017 11:42:24 +0100 Subject: [PATCH 1/2] check_class_cast: don't duplicate existing assertion java_bytecode_convert_method.cpp already creates an assertion; we should replace it with an appropriately elaborated one rather than leaving the existing one in place. --- regression/cbmc-java/cast_null1/test.class | Bin 0 -> 237 bytes regression/cbmc-java/cast_null1/test.desc | 9 +++++++++ regression/cbmc-java/cast_null1/test.java | 8 ++++++++ src/java_bytecode/java_bytecode_instrument.cpp | 8 +++----- 4 files changed, 20 insertions(+), 5 deletions(-) create mode 100644 regression/cbmc-java/cast_null1/test.class create mode 100644 regression/cbmc-java/cast_null1/test.desc create mode 100644 regression/cbmc-java/cast_null1/test.java diff --git a/regression/cbmc-java/cast_null1/test.class b/regression/cbmc-java/cast_null1/test.class new file mode 100644 index 0000000000000000000000000000000000000000..efced7cc257cac8cfdecc4f16a14a90d133f346e GIT binary patch literal 237 zcmYL?Jr4mv5Qg8``*P>=4=AWmxJD@&iH1-R{T>@xxjPAa{+CLk5VapAW<}UZW@eu} zGxL1i?f?d;MQ~6KPzg{a_(Pp*Ga@*h?wa6^4_ig3&vdTlMV6@JN+u~2Hw!f-R4~XgCjd&$5;ILC6_X5!ytcoLW literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/cast_null1/test.desc b/regression/cbmc-java/cast_null1/test.desc new file mode 100644 index 00000000000..86a52fc73e7 --- /dev/null +++ b/regression/cbmc-java/cast_null1/test.desc @@ -0,0 +1,9 @@ +CORE +test.class + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +Dynamic cast check: FAILURE +^warning: ignoring diff --git a/regression/cbmc-java/cast_null1/test.java b/regression/cbmc-java/cast_null1/test.java new file mode 100644 index 00000000000..b6eb1d11817 --- /dev/null +++ b/regression/cbmc-java/cast_null1/test.java @@ -0,0 +1,8 @@ + +public class test { + + public static void main() { + test t = (test)null; + } + +} diff --git a/src/java_bytecode/java_bytecode_instrument.cpp b/src/java_bytecode/java_bytecode_instrument.cpp index 9ec9f3293b2..1a858fc11ea 100644 --- a/src/java_bytecode/java_bytecode_instrument.cpp +++ b/src/java_bytecode/java_bytecode_instrument.cpp @@ -327,7 +327,7 @@ void java_bytecode_instrumentt::instrument_code(exprt &expr) } else if(statement==ID_assert) { - code_assertt code_assert=to_code_assert(code); + const code_assertt &code_assert=to_code_assert(code); // does this correspond to checkcast? if(code_assert.assertion().id()==ID_java_instanceof) @@ -338,13 +338,11 @@ void java_bytecode_instrumentt::instrument_code(exprt &expr) code_assert.assertion().operands().size()==2, "Instanceof should have 2 operands"); - block.copy_to_operands( + code= check_class_cast( code_assert.assertion().op0(), code_assert.assertion().op1(), - code_assert.source_location())); - block.copy_to_operands(code_assert); - code=block; + code_assert.source_location()); } } else if(statement==ID_block) From 73bd18d6a2494f729e62a595238bdc0e150b0fb1 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Thu, 6 Jul 2017 11:50:51 +0100 Subject: [PATCH 2/2] Don't throw ClassCastException when casting null pointer Much like the assert-correct-class case, this is now guarded by a conditional that only applies the check when the source pointer is non-null. --- regression/cbmc-java/cast_null2/test.class | Bin 0 -> 237 bytes regression/cbmc-java/cast_null2/test.desc | 8 +++++ regression/cbmc-java/cast_null2/test.java | 8 +++++ .../java_bytecode_instrument.cpp | 34 ++++++++++-------- 4 files changed, 35 insertions(+), 15 deletions(-) create mode 100644 regression/cbmc-java/cast_null2/test.class create mode 100644 regression/cbmc-java/cast_null2/test.desc create mode 100644 regression/cbmc-java/cast_null2/test.java diff --git a/regression/cbmc-java/cast_null2/test.class b/regression/cbmc-java/cast_null2/test.class new file mode 100644 index 0000000000000000000000000000000000000000..efced7cc257cac8cfdecc4f16a14a90d133f346e GIT binary patch literal 237 zcmYL?Jr4mv5Qg8``*P>=4=AWmxJD@&iH1-R{T>@xxjPAa{+CLk5VapAW<}UZW@eu} zGxL1i?f?d;MQ~6KPzg{a_(Pp*Ga@*h?wa6^4_ig3&vdTlMV6@JN+u~2Hw!f-R4~XgCjd&$5;ILC6_X5!ytcoLW literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/cast_null2/test.desc b/regression/cbmc-java/cast_null2/test.desc new file mode 100644 index 00000000000..c621e5854e5 --- /dev/null +++ b/regression/cbmc-java/cast_null2/test.desc @@ -0,0 +1,8 @@ +CORE +test.class +--java-throw-runtime-exceptions +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/cast_null2/test.java b/regression/cbmc-java/cast_null2/test.java new file mode 100644 index 00000000000..b6eb1d11817 --- /dev/null +++ b/regression/cbmc-java/cast_null2/test.java @@ -0,0 +1,8 @@ + +public class test { + + public static void main() { + test t = (test)null; + } + +} diff --git a/src/java_bytecode/java_bytecode_instrument.cpp b/src/java_bytecode/java_bytecode_instrument.cpp index 1a858fc11ea..f522269554f 100644 --- a/src/java_bytecode/java_bytecode_instrument.cpp +++ b/src/java_bytecode/java_bytecode_instrument.cpp @@ -199,26 +199,30 @@ codet java_bytecode_instrumentt::check_class_cast( exprt null_check_op=class1; if(null_check_op.type()!=voidptr) null_check_op.make_typecast(voidptr); - notequal_exprt op_not_null(null_check_op, null_pointer_exprt(voidptr)); - - // checkcast passes when the operand is null - and_exprt and_expr(op_not_null, not_exprt(class_cast_check)); + codet check_code; if(throw_runtime_exceptions) - return throw_exception( - and_expr, - original_loc, - "ClassCastException"); - - code_assertt assert_class(class_cast_check); - assert_class.add_source_location(). - set_comment("Dynamic cast check"); - assert_class.add_source_location(). - set_property_class("bad-dynamic-cast"); + { + check_code= + throw_exception( + not_exprt(class_cast_check), + original_loc, + "ClassCastException"); + } + else + { + code_assertt assert_class(class_cast_check); + assert_class.add_source_location(). + set_comment("Dynamic cast check"); + assert_class.add_source_location(). + set_property_class("bad-dynamic-cast"); + check_code=std::move(assert_class); + } code_ifthenelset conditional_check; + notequal_exprt op_not_null(null_check_op, null_pointer_exprt(voidptr)); conditional_check.cond()=std::move(op_not_null); - conditional_check.then_case()=std::move(assert_class); + conditional_check.then_case()=std::move(check_code); return conditional_check; }