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.

Author: smowton

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

regression/cbmc-java/repeated_guards/A.class

@@ -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 {}

regression/cbmc-java/repeated_guards/B.class

@@ -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

regression/cbmc-java/repeated_guards/Test.class

@@ -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

regression/cbmc-java/repeated_guards/Test.java

@@ -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

regression/cbmc-java/repeated_guards/test_arraybounds.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

regression/cbmc-java/repeated_guards/test_arraycreation.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

regression/cbmc-java/repeated_guards/test_assertion.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

regression/cbmc-java/repeated_guards/test_classcast.desc

@@ -261,8 +261,21 @@ 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)
+        {
+          i_it->make_skip();
+        }
+        else
+        {
+          i_it->type = goto_program_instruction_typet::ASSUME;
+        }
+      }
     }
   }
 

regression/cbmc-java/repeated_guards/test_divbyzero.desc

@@ -11,6 +11,7 @@ Date:   June 2017
 #include "java_bytecode_instrument.h"
 
 #include <util/arith_tools.h>
+#include <util/assert_or_die.h>
 #include <util/fresh_symbol.h>
 #include <util/std_code.h>
 #include <util/std_expr.h>
@@ -82,6 +83,21 @@ const std::vector<std::string> exception_needed_classes = {
   "java.lang.NegativeArraySizeException",
   "java.lang.NullPointerException"};
 
+/// Get a copy of a source location with additional assertion information
+/// \param loc: original source location
+/// \param comment: human-readable assertion description
+/// \param property_class: assertion property class
+static source_locationt with_assertion_description(
+  const source_locationt &loc,
+  const irep_idt &comment,
+  const irep_idt &property_class)
+{
+  source_locationt ret = loc;
+  ret.set_comment(comment);
+  ret.set_property_class(property_class);
+  return ret;
+}
+
 /// Creates a class stub for exc_name and generates a
 ///  conditional GOTO such that exc_name is thrown when
 ///  cond is met.
@@ -160,11 +176,14 @@ 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 =
+    with_assertion_description(
+      original_loc,
+      "Denominator should be nonzero",
+      "integer-divide-by-zero");
+
+  return create_assert_or_die(
+    binary_relation_exprt(denominator, ID_notequal, zero), assertion_loc);
 }
 
 /// Checks whether the array access array_struct[idx] is out-of-bounds,
@@ -195,19 +214,21 @@ 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");
+
+  bounds_checks.add(
+    create_assert_or_die(
+      ge_zero,
+      with_assertion_description(
+        original_loc,
+        "Array index should be >= 0",
+        "array-index-out-of-bounds-low")));
+  bounds_checks.add(
+    create_assert_or_die(
+      lt_length,
+      with_assertion_description(
+        original_loc,
+        "Array index should be < length",
+        "array-index-out-of-bounds-high")));
 
   return bounds_checks;
 }
@@ -246,11 +267,14 @@ 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");
+    codet assert_class =
+      create_assert_or_die(
+        class_cast_check,
+        with_assertion_description(
+          original_loc,
+          "Dynamic cast check",
+          "bad-dynamic-cast"));
+
     check_code=std::move(assert_class);
   }
 
@@ -283,12 +307,12 @@ 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;
+  return create_assert_or_die(
+    not_exprt(equal_expr),
+    with_assertion_description(
+      original_loc,
+      "Null pointer check",
+      "null-pointer-exception"));
 }
 
 /// Checks whether `length`>=0 and throws NegativeArraySizeException/
@@ -313,11 +337,12 @@ 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;
+  return create_assert_or_die(
+    ge_zero,
+    with_assertion_description(
+      original_loc,
+      "Array size should be >= 0",
+      "array-create-negative-size"));
 }
 
 /// Checks whether `expr` requires instrumentation, and if so adds it

regression/cbmc-java/repeated_guards/test_nullderef.desc

@@ -1,5 +1,6 @@
 SRC = arith_tools.cpp \
       array_name.cpp \
+      assert_or_die.cpp \
       base_type.cpp \
       bv_arithmetic.cpp \
       byte_operators.cpp \

src/goto-instrument/cover.cpp

@@ -0,0 +1,23 @@
+
+#include "assert_or_die.h"
+
+/// Cprover's code_assertt is non-fatal -- we check the condition and continue
+/// to execute the target program. By contrast code_assumet requires that the
+/// condition hold for execution to continue. This method therefore creates an
+/// "assert or die" construct, as C's `assert` function for example, that
+/// checks the condition and then halts if it does not hold.
+/// 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
+/// \return code of the form `assert(condition); assume(condition);`
+codet create_assert_or_die(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;
+}

src/java_bytecode/java_bytecode_instrument.cpp

@@ -0,0 +1,16 @@
+/*******************************************************************\
+
+Module: Assert or die
+
+Author: Diffblue Ltd
+
+\*******************************************************************/
+
+#ifndef CPROVER_UTIL_ASSERT_OR_DIE_H
+#define CPROVER_UTIL_ASSERT_OR_DIE_H
+
+#include "std_code.h"
+
+codet create_assert_or_die(const exprt &condition, const source_locationt &loc);
+
+#endif // CPROVER_UTIL_ASSERT_OR_DIE_H