From 3f718ba9ebcd0a85fc48dd037f7bbbeee08b31c1 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Wed, 16 May 2018 18:05:30 +0100 Subject: [PATCH 1/2] Java: make null-pointer and similar checks fatal These previously used code_assertt, which asserts but then continues -- this changes them to use assert(condition); assume(condition), which ensures subsequent code is not executed in conditions which are in practice impossible. With --java-throw-runtime-exceptions this is irrelevant, as a real exception is raised and the conditional GOTO guarding the throw has the same effect as the assume. --- regression/cbmc-java/NullPointer3/test.desc | 2 +- regression/cbmc-java/repeated_guards/A.class | Bin 0 -> 251 bytes regression/cbmc-java/repeated_guards/B.class | Bin 0 -> 216 bytes .../cbmc-java/repeated_guards/Test.class | Bin 0 -> 1391 bytes .../cbmc-java/repeated_guards/Test.java | 45 ++++++++++++ .../repeated_guards/test_arraybounds.desc | 12 ++++ .../repeated_guards/test_arraycreation.desc | 10 +++ .../repeated_guards/test_assertion.desc | 10 +++ .../repeated_guards/test_classcast.desc | 10 +++ .../repeated_guards/test_divbyzero.desc | 10 +++ .../repeated_guards/test_nullderef.desc | 10 +++ src/goto-instrument/cover.cpp | 12 +++- .../java_bytecode_instrument.cpp | 67 +++++++++--------- src/util/std_code.cpp | 12 ++++ src/util/std_code.h | 22 ++++-- 15 files changed, 182 insertions(+), 40 deletions(-) create mode 100644 regression/cbmc-java/repeated_guards/A.class create mode 100644 regression/cbmc-java/repeated_guards/B.class create mode 100644 regression/cbmc-java/repeated_guards/Test.class create mode 100644 regression/cbmc-java/repeated_guards/Test.java create mode 100644 regression/cbmc-java/repeated_guards/test_arraybounds.desc create mode 100644 regression/cbmc-java/repeated_guards/test_arraycreation.desc create mode 100644 regression/cbmc-java/repeated_guards/test_assertion.desc create mode 100644 regression/cbmc-java/repeated_guards/test_classcast.desc create mode 100644 regression/cbmc-java/repeated_guards/test_divbyzero.desc create mode 100644 regression/cbmc-java/repeated_guards/test_nullderef.desc diff --git a/regression/cbmc-java/NullPointer3/test.desc b/regression/cbmc-java/NullPointer3/test.desc index 5dd14d8dfb9..3cf4998f5aa 100644 --- a/regression/cbmc-java/NullPointer3/test.desc +++ b/regression/cbmc-java/NullPointer3/test.desc @@ -3,7 +3,7 @@ NullPointer3.class --pointer-check ^EXIT=10$ ^SIGNAL=0$ -^.*Throw null: FAILURE$ +^.*Null pointer check: FAILURE$ ^VERIFICATION FAILED$ -- ^warning: ignoring diff --git a/regression/cbmc-java/repeated_guards/A.class b/regression/cbmc-java/repeated_guards/A.class new file mode 100644 index 0000000000000000000000000000000000000000..6f4617a522e71e12ef98af492c2e224e7817bc21 GIT binary patch literal 251 zcmXYr%}T>i5QV=<^J8PRwNKzuOEDXFickbW2)eLzf0JI@TVeuf>U+5oT=)P!lsGrI zIh>z4GxPKN^$lDzO&Kswm?WGD(W|r7T98K}zICq`riz@t=nrgU)%`kOLJ&T`{4ZeaB275)y}+|5iyD0S_l)bv&z() z?77(4vg4dU9|O$^iF$@Fs6JAa^$A3?Pvk?5fT3cnHq1#CM?H@?R^}I-C-5{1(9 z-?XZeD)}_nEC}8qzZQwyDIIr1Syt1txCtK?8U)%f))>Ix@4AS=8)lo;j9EL4@dI>c XVZh;T*X9IG*8VR57amW9R-N*{5Ah;C literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/repeated_guards/Test.class b/regression/cbmc-java/repeated_guards/Test.class new file mode 100644 index 0000000000000000000000000000000000000000..057d0b980f2f8f3fe796647dcfb395c321161944 GIT binary patch literal 1391 zcmZWo+inwA6kTU7napGoC#JZm10)6l#z4|bdX2fnxu8e}9zaNhhidFO2?N7SHMUdo zDa{Y?Oj{MHsoK6(>PJ;wdpy{bj&v@2pS{=GYo9ZJ|MTnb0M^j*;A72&htC~+;lae3 zgD*YUvVP^kkwY6_JNU-KI+_k{D4e<&^m;n$M`_aAih4mO)}eyhQ?T5P8Usss!bKQ8$M6~*z zfV$l@2_qqA$b){+eSSCiu7D`zDOnaAwbDTn3R?Zi?yjWSfw&cnC%ZJFB-AfiGxz2} z+Aqj9V+z|0dbFKE@;phuCx`PQIO^zcJB(~^uq;2+`=V0EM?+_8oh>U6?hWF2OJ{mt zm>HfIoCC;75wsN@wvP66mWrmlI5Uh673N0OZ)Q3u6b_U10qsL}&ZG>5$!0e$I_*73 z2U%C|MABDRTDS5nI1GH0FzaI)GYa$KSdD|^V0F~a?JP?Pq&7HOK5k->#Ynb;TRv`s z{@HQb{mwJpWmoL|NXNYE()cLvnL;Jhy(rV+h=4cKAMgVB682Ez1M~Ud)a<;J#N8x_ zf?3XUv{tz)u6E-M)N5`GlsQl2PChv9{b2w;z-d}8D)^8dNe&n-$;&^&I7X>@jHwft zkKe%hTDM1l3|+Yg1U6#CO_CDY10DrED?EJK@I0~g%xVQK=q0-6IjNjq5=oT z%#MT0tfG!9h44FE4T4TJeumr3C*d1j)v%jqsN*bqdM@Xx48zeN1Mij$qEXad#kB%- zn=u0FTGhBI<9)~)g`DSex$q98OV1*cEP`GyAXnaj9M|fpi*sTBn literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/repeated_guards/Test.java b/regression/cbmc-java/repeated_guards/Test.java new file mode 100644 index 00000000000..5f177b7e7e9 --- /dev/null +++ b/regression/cbmc-java/repeated_guards/Test.java @@ -0,0 +1,45 @@ +public class Test { + + // In each of these cases a guard is repeated -- either an explicit assertion, + // or a guard implied by Java's semantics, e.g. that an array index is in bounds. + // It should be possible to violate the condition the first time, but not the second, + // as the program would have aborted (without --java-throw-runtime-exceptions) or a + // runtime exception thrown (with --java-throw-runtime-exceptions). + + public static void testAssertion(boolean condition) { + assert(condition); + assert(condition); + } + + public static void testArrayBounds(int[] array, int index) { + if(array == null) + return; + int got = array[index]; + got = array[index]; + } + + public static void testClassCast(boolean unknown) { + A maybe_b = unknown ? new A() : new B(); + B definitely_b = (B)maybe_b; + definitely_b = (B)maybe_b; + } + + public static void testNullDeref(A maybeNull) { + int got = maybeNull.field; + got = maybeNull.field; + } + + public static void testDivByZero(int unknown) { + int div = 1 / unknown; + div = 1 / unknown; + } + + public static void testArrayCreation(int maybeNegative) { + int[] arr = new int[maybeNegative]; + arr = new int[maybeNegative]; + } + +} + +class A { public int field; } +class B extends A {} diff --git a/regression/cbmc-java/repeated_guards/test_arraybounds.desc b/regression/cbmc-java/repeated_guards/test_arraybounds.desc new file mode 100644 index 00000000000..fd0383545a4 --- /dev/null +++ b/regression/cbmc-java/repeated_guards/test_arraybounds.desc @@ -0,0 +1,12 @@ +CORE +Test.class +--function Test.testArrayBounds +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +array-index-out-of-bounds-low\.1.*: FAILURE$ +array-index-out-of-bounds-low\.2.*: SUCCESS$ +array-index-out-of-bounds-high\.1.*: FAILURE$ +array-index-out-of-bounds-high\.2.*: SUCCESS$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/repeated_guards/test_arraycreation.desc b/regression/cbmc-java/repeated_guards/test_arraycreation.desc new file mode 100644 index 00000000000..f737239e0cd --- /dev/null +++ b/regression/cbmc-java/repeated_guards/test_arraycreation.desc @@ -0,0 +1,10 @@ +CORE +Test.class +--function Test.testArrayCreation +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +array-create-negative-size\.1.*: FAILURE$ +array-create-negative-size\.2.*: SUCCESS$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/repeated_guards/test_assertion.desc b/regression/cbmc-java/repeated_guards/test_assertion.desc new file mode 100644 index 00000000000..182191d772f --- /dev/null +++ b/regression/cbmc-java/repeated_guards/test_assertion.desc @@ -0,0 +1,10 @@ +CORE +Test.class +--function Test.testAssertion +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +assertion at file Test\.java line 10.*: FAILURE$ +assertion at file Test\.java line 11.*: SUCCESS$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/repeated_guards/test_classcast.desc b/regression/cbmc-java/repeated_guards/test_classcast.desc new file mode 100644 index 00000000000..c06857eb924 --- /dev/null +++ b/regression/cbmc-java/repeated_guards/test_classcast.desc @@ -0,0 +1,10 @@ +CORE +Test.class +--function Test.testClassCast +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +bad-dynamic-cast\.1.*: FAILURE$ +bad-dynamic-cast\.2.*: SUCCESS$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/repeated_guards/test_divbyzero.desc b/regression/cbmc-java/repeated_guards/test_divbyzero.desc new file mode 100644 index 00000000000..4d9f15cd63d --- /dev/null +++ b/regression/cbmc-java/repeated_guards/test_divbyzero.desc @@ -0,0 +1,10 @@ +CORE +Test.class +--function Test.testDivByZero +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +integer-divide-by-zero\.1.*: FAILURE$ +integer-divide-by-zero\.2.*: SUCCESS$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/repeated_guards/test_nullderef.desc b/regression/cbmc-java/repeated_guards/test_nullderef.desc new file mode 100644 index 00000000000..082ef0af6a8 --- /dev/null +++ b/regression/cbmc-java/repeated_guards/test_nullderef.desc @@ -0,0 +1,10 @@ +CORE +Test.class +--function Test.testNullDeref +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +testNullDeref:\(LA;\)V\.null-pointer-exception\.1.*: FAILURE$ +testNullDeref:\(LA;\)V\.null-pointer-exception\.2.*: SUCCESS$ +-- +^warning: ignoring diff --git a/src/goto-instrument/cover.cpp b/src/goto-instrument/cover.cpp index 459fccd1ea4..6cebedc173d 100644 --- a/src/goto-instrument/cover.cpp +++ b/src/goto-instrument/cover.cpp @@ -261,8 +261,18 @@ static void instrument_cover_goals( { Forall_goto_program_instructions(i_it, function.body) { + // Simplify the common case where we have ASSERT(x); ASSUME(x): if(i_it->is_assert()) - i_it->type=goto_program_instruction_typet::ASSUME; + { + auto successor = std::next(i_it); + if(successor != function.body.instructions.end() && + successor->is_assume() && + successor->guard == i_it->guard) + { + successor->make_skip(); + } + i_it->type = goto_program_instruction_typet::ASSUME; + } } } diff --git a/src/java_bytecode/java_bytecode_instrument.cpp b/src/java_bytecode/java_bytecode_instrument.cpp index bd2e6a95be4..cbdf8dab7c1 100644 --- a/src/java_bytecode/java_bytecode_instrument.cpp +++ b/src/java_bytecode/java_bytecode_instrument.cpp @@ -160,11 +160,12 @@ codet java_bytecode_instrumentt::check_arithmetic_exception( original_loc, "java.lang.ArithmeticException"); - code_assertt ret(binary_relation_exprt(denominator, ID_notequal, zero)); - ret.add_source_location()=original_loc; - ret.add_source_location().set_comment("Denominator should be nonzero"); - ret.add_source_location().set_property_class("integer-divide-by-zero"); - return ret; + source_locationt assertion_loc = original_loc; + assertion_loc.set_comment("Denominator should be nonzero"); + assertion_loc.set_property_class("integer-divide-by-zero"); + + return create_fatal_assertion( + binary_relation_exprt(denominator, ID_notequal, zero), assertion_loc); } /// Checks whether the array access array_struct[idx] is out-of-bounds, @@ -195,19 +196,17 @@ codet java_bytecode_instrumentt::check_array_access( "java.lang.ArrayIndexOutOfBoundsException"); code_blockt bounds_checks; - bounds_checks.add(code_assertt(ge_zero)); - bounds_checks.operands().back().add_source_location()=original_loc; - bounds_checks.operands().back().add_source_location() - .set_comment("Array index should be >= 0"); - bounds_checks.operands().back().add_source_location() - .set_property_class("array-index-out-of-bounds-low"); - - bounds_checks.add(code_assertt(lt_length)); - bounds_checks.operands().back().add_source_location()=original_loc; - bounds_checks.operands().back().add_source_location() - .set_comment("Array index should be < length"); - bounds_checks.operands().back().add_source_location() - .set_property_class("array-index-out-of-bounds-high"); + + source_locationt low_check_loc = original_loc; + low_check_loc.set_comment("Array index should be >= 0"); + low_check_loc.set_property_class("array-index-out-of-bounds-low"); + + source_locationt high_check_loc = original_loc; + high_check_loc.set_comment("Array index should be < length"); + high_check_loc.set_property_class("array-index-out-of-bounds-high"); + + bounds_checks.add(create_fatal_assertion(ge_zero, low_check_loc)); + bounds_checks.add(create_fatal_assertion(lt_length, high_check_loc)); return bounds_checks; } @@ -246,11 +245,12 @@ codet java_bytecode_instrumentt::check_class_cast( } 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"); + source_locationt check_loc = original_loc; + check_loc.set_comment("Dynamic cast check"); + check_loc.set_property_class("bad-dynamic-cast"); + + codet assert_class = create_fatal_assertion(class_cast_check, check_loc); + check_code=std::move(assert_class); } @@ -283,12 +283,11 @@ codet java_bytecode_instrumentt::check_null_dereference( equal_expr, original_loc, "java.lang.NullPointerException"); - code_assertt check((not_exprt(equal_expr))); - check.add_source_location() - .set_comment("Throw null"); - check.add_source_location() - .set_property_class("null-pointer-exception"); - return check; + source_locationt check_loc = original_loc; + check_loc.set_comment("Null pointer check"); + check_loc.set_property_class("null-pointer-exception"); + + return create_fatal_assertion(not_exprt(equal_expr), check_loc); } /// Checks whether `length`>=0 and throws NegativeArraySizeException/ @@ -313,11 +312,11 @@ codet java_bytecode_instrumentt::check_array_length( original_loc, "java.lang.NegativeArraySizeException"); - code_assertt check(ge_zero); - check.add_source_location().set_comment("Array size should be >= 0"); - check.add_source_location() - .set_property_class("array-create-negative-size"); - return check; + source_locationt check_loc; + check_loc.set_comment("Array size should be >= 0"); + check_loc.set_property_class("array-create-negative-size"); + + return create_fatal_assertion(ge_zero, check_loc); } /// Checks whether `expr` requires instrumentation, and if so adds it diff --git a/src/util/std_code.cpp b/src/util/std_code.cpp index b57f1d1b44d..a280f83d064 100644 --- a/src/util/std_code.cpp +++ b/src/util/std_code.cpp @@ -107,3 +107,15 @@ void code_blockt::append(const code_blockt &extra_block) add(to_code(operand)); } } + +code_blockt create_fatal_assertion( + const exprt &condition, const source_locationt &loc) +{ + code_blockt result; + result.copy_to_operands(code_assertt(condition)); + result.copy_to_operands(code_assumet(condition)); + for(auto &op : result.operands()) + op.add_source_location() = loc; + result.add_source_location() = loc; + return result; +} diff --git a/src/util/std_code.h b/src/util/std_code.h index 82ae531992e..422a492896e 100644 --- a/src/util/std_code.h +++ b/src/util/std_code.h @@ -350,8 +350,7 @@ inline code_deadt &to_code_dead(codet &code) return static_cast(code); } -/*! \brief An assumption -*/ +/// An assumption, which must hold in subsequent code. class code_assumet:public codet { public: @@ -396,8 +395,8 @@ inline code_assumet &to_code_assume(codet &code) return static_cast(code); } -/*! \brief An assertion -*/ +/// A non-fatal assertion, which checks a condition then permits execution to +/// continue. class code_assertt:public codet { public: @@ -442,6 +441,21 @@ inline code_assertt &to_code_assert(codet &code) return static_cast(code); } +/// Create a fatal assertion, which checks a condition and then halts if it does +/// not hold. Equivalent to `ASSERT(condition); ASSUME(condition)`. +/// +/// Source level assertions should probably use this, whilst checks that are +/// normally non-fatal at runtime, such as integer overflows, should use +/// code_assertt by itself. +/// \param condition: condition to assert +/// \param source_location: source location to attach to the generated code; +/// conventionally this should have `comment` and `property_class` fields set +/// to indicate the nature of the assertion. +/// \return A code block that asserts a condition then aborts if it does not +/// hold. +code_blockt create_fatal_assertion( + const exprt &condition, const source_locationt &source_location); + /*! \brief An if-then-else */ class code_ifthenelset:public codet From 48e5b250e07766a685f6cff44aeb2644a962f0eb Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Fri, 18 May 2018 15:55:05 +0100 Subject: [PATCH 2/2] Amend faulty long-string test This test previously checked that the *sum* of the arguments' sizes didn't exceed some critical bound, but this didn't exclude the case where one of them is just within bounds (but still long enough to cause a memout when we try to concretise it) and the other just long enough to push the sum over the boundary. Instead we'll check that one or the other is very long, and the other one acceptably short. --- regression/jbmc-strings/long_string/Test.class | Bin 985 -> 1185 bytes regression/jbmc-strings/long_string/Test.java | 7 ++++++- 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/regression/jbmc-strings/long_string/Test.class b/regression/jbmc-strings/long_string/Test.class index 9442a3c1cf466c5158a588f53da0901a688f5f87..aa76e7deca38c6e0ff8b9a66c641fa186584a088 100644 GIT binary patch delta 556 zcmZXR&rcIk5XV1nU)$H+ZfRJn7DOnt2;JHiv=o0NhJdF62P^Tu5E6+*jnp$9JbG#N zZbIZA=mjDN!wC{SdGs&wVhFQ~>4nS8cjnD}=R5QMm;<~0^Wx+O(Bg^15M_r6rXzDt zQ#(7=n1iCj46~Z?&!22uDhA)drmPdvXQ(>dr)H@4+Rsbg+Pke__f_y=C)nKG-iVAM z(S5zMr%0`BZ0~iS_P#WeNxT^j>Yas0+Bk3Qb`T{KSVpDNab5pQ;RlqH7OJq}EL^3x7e-GbU zt4fC_*1~>NSwxFnVw5}LBQz#Rkz<~_f-J@*n2#Cu+;?+ny;2I^O?t1pQ9yr@qLt@r;NP4VGZJ(G{NOk%l9(QT(B Huqa&uIPFR2 delta 359 zcmX|+PfG$(6vcltqdpyHl1kGwP4iDVYJYTU89}WKSG8#s7OiU0qII-r9mx9x(kGC> zphX0MLEoSc(Yj4UR~Pc&ymRk8=N@i9@}=6Je=o0qk8d+W)+WdD81fd4(VKVg(%4DJ@8D5$ zsMAoaJ8ZD2PmOA5%b`h2KNvstEQUM?de0aGAqH{5(4=WeW`YIb^U~A$-8?i*9kaG~ zlTy2c!u%3bq@qz*q>EGOEhd&od~bxReGnLUwIODwKE#@fKI(6?uy0O+D&m7QVKTyU q#3+)YB)iIj6~QVkxndmX5S#|O;z;Y0fFB=Ef|$hbgCQJW$F)t$k diff --git a/regression/jbmc-strings/long_string/Test.java b/regression/jbmc-strings/long_string/Test.java index 5decee61931..370dea0e183 100644 --- a/regression/jbmc-strings/long_string/Test.java +++ b/regression/jbmc-strings/long_string/Test.java @@ -32,7 +32,12 @@ public static void checkAbort(String s, String t) { // Filter out // 67_108_864 corresponds to the maximum length for which the solver // will concretize the string. - if(u.length() <= 67_108_864) + if(s.length() <= 67_108_864 && t.length() <= 67_108_864) + return; + // Check at least one of them is short-ish, so we don't end up trying + // to concretise a very long but *just* allowable string and memout the + // test infrastructure: + if(s.length() > 1024 && t.length() > 1024) return; if(CProverString.charAt(u, 2_000_000) != 'b') return;