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 --disable-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
+--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/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

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("disable-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,15 @@ 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
-    java_entry_point(
-      symbol_table,
-      main_class,
-      get_message_handler(),
-      assume_inputs_non_null,
-      object_factory_parameters,
-      get_pointer_type_selector(),
-      string_refinement_enabled);
+  return java_entry_point(
+    symbol_table,
+    main_class,
+    get_message_handler(),
+    assume_inputs_non_null,
+    assert_uncaught_exceptions,
+    object_factory_parameters,
+    get_pointer_type_selector(),
+    string_refinement_enabled);
 }
 
 /// Uses a simple context-insensitive ('ci') analysis to determine which methods

jbmc/src/java_bytecode/java_bytecode_language.h

@@ -26,19 +26,23 @@ 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*/ \
+  "(disable-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*/                                          \
+  " --disable-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 +59,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 +172,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;
 

jbmc/src/java_bytecode/java_entry_point.cpp

@@ -18,6 +18,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <linking/static_lifetime_init.h>
 
+#include "java_bytecode_instrument.h"
 #include "java_object_factory.h"
 #include "java_string_literals.h"
 #include "java_utils.h"
@@ -520,6 +521,7 @@ bool java_entry_point(
   const irep_idt &main_class,
   message_handlert &message_handler,
   bool assume_init_pointers_not_null,
+  bool assert_uncaught_exceptions,
   const object_factory_parameterst &object_factory_parameters,
   const select_pointer_typet &pointer_type_selector,
   bool string_refinement_enabled)
@@ -554,6 +556,7 @@ bool java_entry_point(
     symbol_table,
     message_handler,
     assume_init_pointers_not_null,
+    assert_uncaught_exceptions,
     object_factory_parameters,
     pointer_type_selector);
 }
@@ -576,7 +579,8 @@ bool generate_java_start_function(
   symbol_table_baset &symbol_table,
   message_handlert &message_handler,
   bool assume_init_pointers_not_null,
-  const object_factory_parameterst& object_factory_parameters,
+  bool assert_uncaught_exceptions,
+  const object_factory_parameterst &object_factory_parameters,
   const select_pointer_typet &pointer_type_selector)
 {
   messaget message(message_handler);
@@ -699,6 +703,13 @@ bool generate_java_start_function(
   // declare certain (which?) variables as test outputs
   java_record_outputs(symbol, main_arguments, init_code, symbol_table);
 
+  // add uncaught-exception check if requested
+  if(assert_uncaught_exceptions)
+  {
+    java_bytecode_instrument_uncaught_exceptions(
+      init_code, exc_symbol, symbol.location);
+  }
+
   // create a symbol for the __CPROVER__start function, associate the code that
   // we just built and register it in the symbol table
   symbolt new_symbol;

jbmc/src/java_bytecode/java_entry_point.h

@@ -24,6 +24,7 @@ bool java_entry_point(
   const irep_idt &main_class,
   class message_handlert &message_handler,
   bool assume_init_pointers_not_null,
+  bool assert_uncaught_exceptions,
   const object_factory_parameterst &object_factory_parameters,
   const select_pointer_typet &pointer_type_selector,
   bool string_refinement_enabled);
@@ -74,7 +75,8 @@ bool generate_java_start_function(
   class symbol_table_baset &symbol_table,
   class message_handlert &message_handler,
   bool assume_init_pointers_not_null,
-  const object_factory_parameterst& object_factory_parameters,
+  bool assert_uncaught_exceptions,
+  const object_factory_parameterst &object_factory_parameters,
   const select_pointer_typet &pointer_type_selector);
 
 #endif // CPROVER_JAVA_BYTECODE_JAVA_ENTRY_POINT_H