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,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;
+      }
     }
   }
 

regression/cbmc-java/repeated_guards/test_divbyzero.desc

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

regression/cbmc-java/repeated_guards/test_nullderef.desc

@@ -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;
+}

src/goto-instrument/cover.cpp

@@ -350,8 +350,7 @@ inline code_deadt &to_code_dead(codet &code)
   return static_cast<code_deadt &>(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_assumet &>(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_assertt &>(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