Assert that there is uncaught exception

That's the default behaviour because an escaping exception
makes the JVM abort. The user can override this behaviour
using the --no-uncaught-exception-check option.

Author: peterschrammel

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
+--no-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/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,30 @@ 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 symbol_table: global symbol table
+void java_bytecode_instrument_uncaught_exceptions(symbol_tablet &symbol_table)
+{
+  // retrieve the exception variable
+  const symbolt &exc_symbol =
+    symbol_table.lookup_ref(JAVA_ENTRY_POINT_EXCEPTION_SYMBOL);
+
+  symbolt &function =
+    symbol_table.get_writeable_ref(goto_functionst::entry_point());
+  codet &init_code = to_code(function.value);
+
+  // 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 = function.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

@@ -26,6 +26,8 @@ void java_bytecode_instrument(
   const bool throw_runtime_exceptions,
   message_handlert &_message_handler);
 
+void java_bytecode_instrument_uncaught_exceptions(symbol_tablet &symbol_table);
+
 extern const std::vector<std::string> exception_needed_classes;
 
 #endif

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -46,6 +46,9 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd)
   assume_inputs_non_null=cmd.isset("java-assume-inputs-non-null");
   string_refinement_enabled=cmd.isset("refine-strings");
   throw_runtime_exceptions=cmd.isset("java-throw-runtime-exceptions");
+  assert_uncaught_exceptions = !cmd.isset("no-uncaught-exception-check");
+  threading_support = cmd.isset("java-threading");
+
   if(cmd.isset("java-max-input-array-length"))
     object_factory_parameters.max_nondet_array_length=
       std::stoi(cmd.get_value("java-max-input-array-length"));
@@ -69,14 +72,8 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd)
   else
     lazy_methods_mode=LAZY_METHODS_MODE_EAGER;
 
-  if(cmd.isset("java-threading"))
-    threading_support = true;
-  else
-    threading_support = false;
-
-  if(cmd.isset("java-throw-runtime-exceptions"))
+  if(throw_runtime_exceptions)
   {
-    throw_runtime_exceptions = true;
     java_load_classes.insert(
         java_load_classes.end(),
         exception_needed_classes.begin(),
@@ -777,15 +774,23 @@ bool java_bytecode_languaget::generate_support_functions(
   convert_lazy_method(res.main_function.name, symbol_table);
 
   // generate the test harness in __CPROVER__start and a call the entry point
-  return
+  if(
     java_entry_point(
       symbol_table,
       main_class,
       get_message_handler(),
       assume_inputs_non_null,
       object_factory_parameters,
       get_pointer_type_selector(),
-      string_refinement_enabled);
+      string_refinement_enabled))
+  {
+    return true;
+  }
+
+  if(assert_uncaught_exceptions)
+    java_bytecode_instrument_uncaught_exceptions(symbol_table);
+
+  return false;
 }
 
 /// Uses a simple context-insensitive ('ci') analysis to determine which methods

jbmc/src/java_bytecode/java_bytecode_language.h

@@ -26,19 +26,22 @@ Author: Daniel Kroening, [email protected]
 
 #include <langapi/language.h>
 
-#define JAVA_BYTECODE_LANGUAGE_OPTIONS /*NOLINT*/                              \
-  "(java-assume-inputs-non-null)"                                              \
-  "(java-throw-runtime-exceptions)"                                            \
-  "(java-max-input-array-length):"                                             \
-  "(java-max-input-tree-depth):"                                               \
-  "(java-max-vla-length):"                                                     \
-  "(java-cp-include-files):"                                                   \
-  "(lazy-methods)"                                                             \
-  "(lazy-methods-extra-entry-point):"                                          \
-  "(java-load-class):"                                                         \
+// clang-format off
+#define JAVA_BYTECODE_LANGUAGE_OPTIONS /*NOLINT*/ \
+  "(no-uncaught-exception-check)" \
+  "(java-assume-inputs-non-null)" \
+  "(java-throw-runtime-exceptions)" \
+  "(java-max-input-array-length):" \
+  "(java-max-input-tree-depth):" \
+  "(java-max-vla-length):" \
+  "(java-cp-include-files):" \
+  "(lazy-methods)" \
+  "(lazy-methods-extra-entry-point):" \
+  "(java-load-class):" \
   "(java-no-load-class):"
 
 #define JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP /*NOLINT*/                                          \
+  " --no-uncaught-exception-check    ignore uncaught exceptions and errors\n" \
   " --java-assume-inputs-non-null    never initialize reference-typed parameter to the\n"        /* NOLINT(*) */ \
   "                                  entry point with null\n"                                    /* NOLINT(*) */ \
   " --java-throw-runtime-exceptions  make implicit runtime exceptions explicit\n"                /* NOLINT(*) */ \
@@ -55,6 +58,7 @@ Author: Daniel Kroening, [email protected]
   "                                  treat METHODNAME as a possible program entry point for\n"   /* NOLINT(*) */ \
   "                                  the purpose of lazy method loading\n"                       /* NOLINT(*) */ \
   "                                  A '.*' wildcard is allowed to specify all class members\n"
+// clang-format on
 
 class symbolt;
 
@@ -167,6 +171,7 @@ class java_bytecode_languaget:public languaget
   std::vector<irep_idt> lazy_methods_extra_entry_points;
   bool string_refinement_enabled;
   bool throw_runtime_exceptions;
+  bool assert_uncaught_exceptions;
   java_string_library_preprocesst string_preprocess;
   std::string java_cp_include_files;