JBMC report FAILURE on uncaught exception

jbmc/regression/jbmc-strings/max-length/test1.desc

@@ -3,4 +3,4 @@ Test.class
 --refine-strings --verbosity 10 --string-max-input-length 499999 --function Test.checkMaxInputLength
 ^EXIT=0$
 ^SIGNAL=0$
-assertion.* line 9 function java::Test.checkMaxInputLength.* bytecode-index 16: SUCCESS
+assertion.* line 9 function java::Test.checkMaxInputLength.* bytecode-index 17: SUCCESS

jbmc/regression/jbmc-strings/max-length/test2.desc

@@ -3,4 +3,4 @@ Test.class
 --refine-strings --verbosity 10 --string-max-input-length 500000 --function Test.checkMaxInputLength
 ^EXIT=10$
 ^SIGNAL=0$
-assertion.* line 9 function java::Test.checkMaxInputLength.* bytecode-index 16: FAILURE
+assertion.* line 9 function java::Test.checkMaxInputLength.* bytecode-index 17: FAILURE

jbmc/regression/jbmc-strings/max-length/test3.desc

@@ -3,4 +3,4 @@ Test.class
 --refine-strings --verbosity 10 --string-max-length 4001 --function Test.checkMaxLength
 ^EXIT=10$
 ^SIGNAL=0$
-assertion.* line 25 function java::Test.checkMaxLength.* bytecode-index 26: FAILURE
+assertion.* line 25 function java::Test.checkMaxLength.* bytecode-index 27: FAILURE

jbmc/regression/jbmc/assert3/test_throw_no_uncaught.desc

@@ -0,0 +1,8 @@
+CORE
+assert3.class
+--throw-assertion-error --disable-uncaught-exception-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

jbmc/regression/jbmc/assert7/Test.java

@@ -0,0 +1,9 @@
+class Test
+{
+  public static void main(String[] args)
+  {
+    AssertionError a = new AssertionError();
+    if(false)
+      throw a;
+  }
+}

jbmc/regression/jbmc/assert7/test.desc

@@ -0,0 +1,8 @@
+CORE
+Test.class
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

jbmc/regression/jbmc/catch1/test.desc

@@ -1,8 +1,9 @@
 CORE
 catch1.class
 
-^EXIT=0$
+^EXIT=10$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
+^VERIFICATION FAILED$
+^\[.*\] no uncaught exception: FAILURE$
 --
 ^warning: ignoring

jbmc/regression/jbmc/catch1/test_no_uncaught_exceptions.desc

@@ -0,0 +1,8 @@
+CORE
+catch1.class
+--disable-uncaught-exception-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

jbmc/regression/jbmc/exceptions18/test.desc

@@ -1,8 +1,9 @@
 CORE
 Test.class
 --function Test.goo
-^EXIT=0$
+^EXIT=10$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
+^VERIFICATION FAILED$
+no uncaught exception: FAILURE
 --
 ^warning: ignoring

jbmc/regression/jbmc/exceptions23/test.desc

@@ -4,7 +4,7 @@ test.class
 ^EXIT=10$
 ^SIGNAL=0$
 VERIFICATION FAILED
-assertion at file test\.java line 9 function java::test\.main:\(\)V bytecode-index 12: FAILURE
+assertion at file test\.java line 9 function java::test\.main:\(\)V bytecode-index 13: FAILURE
 --
 ^warning: ignoring
 --

jbmc/regression/jbmc/exceptions24/test.desc

@@ -4,7 +4,7 @@ test.class
 ^EXIT=10$
 ^SIGNAL=0$
 VERIFICATION FAILED
-assertion at file test\.java line 9 function java::test\.main:\(\)V bytecode-index 10: FAILURE
+assertion at file test\.java line 9 function java::test\.main:\(\)V bytecode-index 11: FAILURE
 --
 ^warning: ignoring
 --

jbmc/regression/jbmc/finally1/test.desc

@@ -3,7 +3,7 @@ test.class
 --function test.main
 ^EXIT=10$
 ^SIGNAL=0$
-assertion at file test\.java line 7 function java::test\.main:\(\)V bytecode-index 9: FAILURE
+assertion at file test\.java line 7 function java::test\.main:\(\)V bytecode-index 10: FAILURE
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

jbmc/regression/jbmc/finally2/test.desc

@@ -3,7 +3,7 @@ test.class
 --function test.main
 ^EXIT=10$
 ^SIGNAL=0$
-assertion at file test\.java line 8 function java::test\.main:\(\)V bytecode-index 9: FAILURE
+assertion at file test\.java line 8 function java::test\.main:\(\)V bytecode-index 10: FAILURE
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

jbmc/regression/jbmc/finally3/test.desc

@@ -3,8 +3,8 @@ test.class
 --function test.main
 ^EXIT=10$
 ^SIGNAL=0$
-assertion at file test\.java line 7 function java::test\.main:\(\)V bytecode-index 9: SUCCESS
-assertion at file test\.java line 10 function java::test\.main:\(\)V bytecode-index 22: FAILURE
+assertion at file test\.java line 7 function java::test\.main:\(\)V bytecode-index 10: SUCCESS
+assertion at file test\.java line 10 function java::test\.main:\(\)V bytecode-index 23: FAILURE
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

jbmc/regression/jbmc/finally4/test.desc

@@ -3,7 +3,7 @@ test.class
 --function test.main
 ^EXIT=10$
 ^SIGNAL=0$
-assertion at file test\.java line 11 function java::test\.main:\(\)V bytecode-index 7: FAILURE
+assertion at file test\.java line 11 function java::test\.main:\(\)V bytecode-index 8: FAILURE
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

jbmc/regression/jbmc/finally5/test.desc

@@ -3,7 +3,7 @@ test.class
 --function test.main
 ^EXIT=10$
 ^SIGNAL=0$
-assertion at file test\.java line 7 function java::test\.main:\(\)V bytecode-index 12: FAILURE
+assertion at file test\.java line 7 function java::test\.main:\(\)V bytecode-index 13: FAILURE
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

jbmc/regression/jbmc/finally6/test.desc

@@ -3,7 +3,7 @@ test.class
 --function test.main
 ^EXIT=10$
 ^SIGNAL=0$
-assertion at file test\.java line 8 function java::test\.main:\(\)V bytecode-index 12: FAILURE
+assertion at file test\.java line 8 function java::test\.main:\(\)V bytecode-index 13: FAILURE
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

jbmc/regression/jbmc/finally7/test.desc

@@ -3,8 +3,8 @@ test.class
 --function test.main
 ^EXIT=10$
 ^SIGNAL=0$
-assertion at file test\.java line 7 function java::test\.main:\(\)V bytecode-index 12: SUCCESS
-assertion at file test\.java line 10 function java::test\.main:\(\)V bytecode-index 25: FAILURE
+assertion at file test\.java line 7 function java::test\.main:\(\)V bytecode-index 13: SUCCESS
+assertion at file test\.java line 10 function java::test\.main:\(\)V bytecode-index 26: FAILURE
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

jbmc/regression/jbmc/no-main-int-array-maybe-null1/test.desc

@@ -4,9 +4,9 @@ Main.class
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-assertion at file Main\.java line 5 function .* bytecode-index 6: FAILURE
-assertion at file Main\.java line 6 function .* bytecode-index 14: FAILURE
-assertion at file Main\.java line 12 function .* bytecode-index 31: SUCCESS
+assertion at file Main\.java line 5 function .* bytecode-index 7: FAILURE
+assertion at file Main\.java line 6 function .* bytecode-index 15: FAILURE
+assertion at file Main\.java line 12 function .* bytecode-index 32: SUCCESS
 \*\* 2 of .* failed
 --
 ^warning: ignoring

jbmc/regression/jbmc/no-main-multi-array-maybe-null1/test.desc

@@ -4,7 +4,7 @@ Main.class
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-assertion at file Main\.java line 5 function .* bytecode-index 24: FAILURE
+assertion at file Main\.java line 5 function .* bytecode-index 25: FAILURE
 \*\* 1 of .* failed
 --
 ^warning: ignoring

jbmc/regression/jbmc/no-main-multi-array-maybe-null2/test.desc

@@ -4,7 +4,7 @@ Main.class
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-assertion at file Main\.java line 5 function .* bytecode-index 24: FAILURE
+assertion at file Main\.java line 5 function .* bytecode-index 25: FAILURE
 \*\* 1 of .* failed
 --
 ^warning: ignoring

jbmc/regression/jbmc/no-main-object-array-elements-maybe-null1/test.desc

@@ -4,7 +4,7 @@ Main.class
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-assertion at file Main\.java line 6 function .* bytecode-index 13: FAILURE
+assertion at file Main\.java line 6 function .* bytecode-index 14: FAILURE
 \*\* 1 of .* failed
 --
 ^warning: ignoring

jbmc/regression/jbmc/no-main-object-array-elements-maybe-null2/test.desc

@@ -4,7 +4,7 @@ Main.class
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-assertion at file Main\.java line 6 function .* bytecode-index 13: FAILURE
+assertion at file Main\.java line 6 function .* bytecode-index 14: FAILURE
 \*\* 1 of .* failed
 --
 ^warning: ignoring

jbmc/regression/jbmc/no-main-object-array-maybe-null1/test.desc

@@ -4,8 +4,8 @@ Main.class
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-assertion at file Main\.java line 10 function .* bytecode-index 6: FAILURE
-assertion at file Main\.java line 14 function .* bytecode-index 26: FAILURE
+assertion at file Main\.java line 10 function .* bytecode-index 7: FAILURE
+assertion at file Main\.java line 14 function .* bytecode-index 27: FAILURE
 \*\* 2 of .* failed
 --
 ^warning: ignoring

jbmc/regression/jbmc/no-main-object-array-maybe-null2/test.desc

@@ -4,8 +4,8 @@ Main.class
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-assertion at file Main\.java line 10 function .* bytecode-index 6: FAILURE
-assertion at file Main\.java line 14 function .* bytecode-index 26: FAILURE
+assertion at file Main\.java line 10 function .* bytecode-index 7: FAILURE
+assertion at file Main\.java line 14 function .* bytecode-index 27: FAILURE
 \*\* 2 of .* failed
 --
 ^warning: ignoring

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -32,11 +32,14 @@ Author: Daniel Kroening, [email protected]
 #include <util/simplify_expr.h>
 #include <util/std_expr.h>
 #include <util/string2int.h>
+#include <util/string_constant.h>
 
 #include <goto-programs/cfg.h>
 #include <goto-programs/class_hierarchy.h>
 #include <goto-programs/resolve_inherited_component.h>
+
 #include <analyses/cfg_dominators.h>
+#include <analyses/uncaught_exceptions_analysis.h>
 
 #include <limits>
 #include <algorithm>
@@ -2248,10 +2251,40 @@ void java_bytecode_convert_methodt::convert_athrow(
   codet &c,
   exprt::operandst &results) const
 {
-  side_effect_expr_throwt throw_expr;
-  throw_expr.add_source_location() = location;
-  throw_expr.copy_to_operands(op[0]);
-  c = code_expressiont(throw_expr);
+  if(
+    !throw_assertion_error &&
+    uncaught_exceptions_domaint::get_exception_type(op[0].type()) ==
+      "java::java.lang.AssertionError")
+  {
+    // we translate athrow into
+    // ASSERT false;
+    // ASSUME false:
+    code_assertt assert_code;
+    assert_code.assertion() = false_exprt();
+    source_locationt assert_location = location; // copy
+    assert_location.set_comment("assertion at " + location.as_string());
+    assert_location.set("user-provided", true);
+    assert_location.set_property_class(ID_assertion);
+    assert_code.add_source_location() = assert_location;
+
+    code_assumet assume_code;
+    assume_code.assumption() = false_exprt();
+    source_locationt assume_location = location; // copy
+    assume_location.set("user-provided", true);
+    assume_code.add_source_location() = assume_location;
+
+    code_blockt ret_block;
+    ret_block.move_to_operands(assert_code);
+    ret_block.move_to_operands(assume_code);
+    c = ret_block;
+  }
+  else
+  {
+    side_effect_expr_throwt throw_expr;
+    throw_expr.add_source_location() = location;
+    throw_expr.copy_to_operands(op[0]);
+    c = code_expressiont(throw_expr);
+  }
   results[0] = op[0];
 }
 
@@ -3055,6 +3088,7 @@ void java_bytecode_convert_method(
   symbol_table_baset &symbol_table,
   message_handlert &message_handler,
   size_t max_array_length,
+  bool throw_assertion_error,
   optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
   java_string_library_preprocesst &string_preprocess,
   const class_hierarchyt &class_hierarchy)
@@ -3073,6 +3107,7 @@ void java_bytecode_convert_method(
     symbol_table,
     message_handler,
     max_array_length,
+    throw_assertion_error,
     needed_lazy_methods,
     string_preprocess,
     class_hierarchy);

jbmc/src/java_bytecode/java_bytecode_convert_method.h

@@ -33,6 +33,7 @@ void java_bytecode_convert_method(
   symbol_table_baset &symbol_table,
   message_handlert &message_handler,
   size_t max_array_length,
+  bool throw_assertion_error,
   optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
   java_string_library_preprocesst &string_preprocess,
   const class_hierarchyt &class_hierarchy);

jbmc/src/java_bytecode/java_bytecode_convert_method_class.h

@@ -36,12 +36,14 @@ class java_bytecode_convert_methodt:public messaget
     symbol_table_baset &symbol_table,
     message_handlert &_message_handler,
     size_t _max_array_length,
+    bool throw_assertion_error,
     optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
     java_string_library_preprocesst &_string_preprocess,
     const class_hierarchyt &class_hierarchy)
     : messaget(_message_handler),
       symbol_table(symbol_table),
       max_array_length(_max_array_length),
+      throw_assertion_error(throw_assertion_error),
       needed_lazy_methods(std::move(needed_lazy_methods)),
       string_preprocess(_string_preprocess),
       slots_for_parameters(0),
@@ -64,6 +66,7 @@ class java_bytecode_convert_methodt:public messaget
 protected:
   symbol_table_baset &symbol_table;
   const size_t max_array_length;
+  const bool throw_assertion_error;
   optionalt<ci_lazy_methods_neededt> needed_lazy_methods;
 
   /// Fully qualified name of the method under translation.

jbmc/src/java_bytecode/java_bytecode_instrument.cpp

@@ -19,6 +19,7 @@ Date:   June 2017
 #include <goto-programs/goto_functions.h>
 
 #include "java_bytecode_convert_class.h"
+#include "java_entry_point.h"
 #include "java_utils.h"
 
 class java_bytecode_instrumentt:public messaget
@@ -592,6 +593,27 @@ void java_bytecode_instrument_symbol(
   instrument(to_code(symbol.value));
 }
 
+/// Instruments the start function with an assertion that checks whether
+/// an exception has escaped the entry point
+/// \param init_code: the code block to which the assertion is appended
+/// \param exc_symbol: the top-level exception symbol
+/// \param source_location: the source location to attach to the assertion
+void java_bytecode_instrument_uncaught_exceptions(
+  codet &init_code,
+  const symbolt &exc_symbol,
+  const source_locationt &source_location)
+{
+  // check that there is no uncaught exception
+  code_assertt assert_no_exception;
+  assert_no_exception.assertion() = equal_exprt(
+    exc_symbol.symbol_expr(),
+    null_pointer_exprt(to_pointer_type(exc_symbol.type)));
+  source_locationt assert_location = source_location;
+  assert_location.set_comment("no uncaught exception");
+  assert_no_exception.add_source_location() = assert_location;
+  init_code.move_to_operands(assert_no_exception);
+}
+
 /// Instruments all the code in the symbol_table with
 /// runtime exceptions or corresponding assertions.
 /// Exceptions are thrown when the `throw_runtime_exceptions` flag is set.

jbmc/src/java_bytecode/java_bytecode_instrument.h

@@ -15,6 +15,8 @@ Date:   June 2017
 #include <util/message.h>
 #include <util/irep.h>
 
+class codet;
+
 void java_bytecode_instrument_symbol(
   symbol_table_baset &symbol_table,
   symbolt &symbol,
@@ -26,6 +28,11 @@ void java_bytecode_instrument(
   const bool throw_runtime_exceptions,
   message_handlert &_message_handler);
 
+void java_bytecode_instrument_uncaught_exceptions(
+  codet &init_code,
+  const symbolt &exc_symbol,
+  const source_locationt &source_location);
+
 extern const std::vector<std::string> exception_needed_classes;
 
 #endif