Add an assert-no-exceptions-thrown option

This is to specify that we want to replace all throw instructions by
assert false.
This is useful mainly for performance reasons as it simplifies
conditions for symex, while retaining the non-exceptional behaviour of
the program.

Author: romainbrenguier

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -2349,9 +2349,10 @@ void java_bytecode_convert_methodt::convert_athrow(
   exprt::operandst &results) const
 {
   if(
-    !throw_assertion_error &&
-    uncaught_exceptions_domaint::get_exception_type(op[0].type()) ==
-      "java::java.lang.AssertionError")
+    assert_no_exceptions_thrown ||
+    ((uncaught_exceptions_domaint::get_exception_type(op[0].type()) ==
+      "java::java.lang.AssertionError") &&
+     !throw_assertion_error))
   {
     // we translate athrow into
     // ASSERT false;
@@ -3190,7 +3191,8 @@ void java_bytecode_convert_method(
   java_string_library_preprocesst &string_preprocess,
   const class_hierarchyt &class_hierarchy,
   bool threading_support,
-  const optionalt<prefix_filtert> &method_context)
+  const optionalt<prefix_filtert> &method_context,
+  bool assert_no_exceptions_thrown)
 
 {
   java_bytecode_convert_methodt java_bytecode_convert_method(
@@ -3201,7 +3203,8 @@ void java_bytecode_convert_method(
     needed_lazy_methods,
     string_preprocess,
     class_hierarchy,
-    threading_support);
+    threading_support,
+    assert_no_exceptions_thrown);
 
   java_bytecode_convert_method(class_symbol, method, method_context);
 }

jbmc/src/java_bytecode/java_bytecode_convert_method.h

@@ -39,7 +39,8 @@ void java_bytecode_convert_method(
   java_string_library_preprocesst &string_preprocess,
   const class_hierarchyt &class_hierarchy,
   bool threading_support,
-  const optionalt<prefix_filtert> &method_context);
+  const optionalt<prefix_filtert> &method_context,
+  bool assert_no_exceptions_thrown);
 
 void create_method_stub_symbol(
   const irep_idt &identifier,

jbmc/src/java_bytecode/java_bytecode_convert_method_class.h

@@ -40,12 +40,14 @@ class java_bytecode_convert_methodt:public messaget
     optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
     java_string_library_preprocesst &_string_preprocess,
     const class_hierarchyt &class_hierarchy,
-    bool threading_support)
+    bool threading_support,
+    bool assert_no_exceptions_thrown)
     : messaget(_message_handler),
       symbol_table(symbol_table),
       ns(symbol_table),
       max_array_length(_max_array_length),
       throw_assertion_error(throw_assertion_error),
+      assert_no_exceptions_thrown(assert_no_exceptions_thrown),
       threading_support(threading_support),
       needed_lazy_methods(std::move(needed_lazy_methods)),
       string_preprocess(_string_preprocess),
@@ -76,6 +78,7 @@ class java_bytecode_convert_methodt:public messaget
   namespacet ns;
   const size_t max_array_length;
   const bool throw_assertion_error;
+  const bool assert_no_exceptions_thrown;
   const bool threading_support;
   optionalt<ci_lazy_methods_neededt> needed_lazy_methods;
 

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -59,6 +59,8 @@ void parse_java_language_options(const cmdlinet &cmd, optionst &options)
     "uncaught-exception-check", !cmd.isset("disable-uncaught-exception-check"));
   options.set_option(
     "throw-assertion-error", cmd.isset("throw-assertion-error"));
+  options.set_option(
+    "assert-no-exceptions-thrown", cmd.isset("assert-no-exceptions-thrown"));
   options.set_option("java-threading", cmd.isset("java-threading"));
 
   if(cmd.isset("java-max-vla-length"))
@@ -144,6 +146,8 @@ java_bytecode_language_optionst::java_bytecode_language_optionst(
   assert_uncaught_exceptions =
     options.get_bool_option("uncaught-exception-check");
   throw_assertion_error = options.get_bool_option("throw-assertion-error");
+  assert_no_exceptions_thrown =
+    options.get_bool_option("assert-no-exceptions-thrown");
   threading_support = options.get_bool_option("java-threading");
   max_user_array_length =
     options.get_unsigned_int_option("java-max-vla-length");
@@ -1321,7 +1325,8 @@ bool java_bytecode_languaget::convert_single_method(
       string_preprocess,
       class_hierarchy,
       language_options->threading_support,
-      language_options->method_context);
+      language_options->method_context,
+      language_options->assert_no_exceptions_thrown);
     INVARIANT(declaring_class(symbol), "Method must have a declaring class.");
     return false;
   }
@@ -1355,7 +1360,7 @@ bool java_bytecode_languaget::convert_single_method(
 
 bool java_bytecode_languaget::final(symbol_table_baset &)
 {
-  PRECONDITION(language_options_initialized);
+  PRECONDITION(language_options.has_value());
   return false;
 }
 

jbmc/src/java_bytecode/java_bytecode_language.h

@@ -33,6 +33,7 @@ Author: Daniel Kroening, [email protected]
 #define JAVA_BYTECODE_LANGUAGE_OPTIONS /*NOLINT*/ \
   "(disable-uncaught-exception-check)" \
   "(throw-assertion-error)" \
+  "(assert-no-exceptions-thrown)" \
   "(java-assume-inputs-non-null)" \
   "(java-assume-inputs-interval):" \
   "(java-assume-inputs-integral)" \
@@ -57,6 +58,9 @@ Author: Daniel Kroening, [email protected]
   "                              assert statements instead of failing\n" \
   "                              at the location of the assert statement\n" \
   " --throw-runtime-exceptions   make implicit runtime exceptions explicit\n" \
+  " --assert-no-exceptions-thrown\n"\
+  "                              transform `throw` instructions into `assert FALSE`\n"/* NOLINT(*) */ \
+  "                              followed by `assume FALSE`.\n" \
   " --max-nondet-array-length N  limit nondet (e.g. input) array size to <= N\n" /* NOLINT(*) */ \
   " --max-nondet-tree-depth N    limit size of nondet (e.g. input) object tree;\n" /* NOLINT(*) */ \
   "                              at level N references are set to null\n" /* NOLINT(*) */ \
@@ -166,6 +170,10 @@ struct java_bytecode_language_optionst
   bool nondet_static = false;
   bool ignore_manifest_main_class = false;
 
+  /// Transform `athrow` bytecode instructions into `assert FALSE` followed
+  /// by `assume FALSE`.
+  bool assert_no_exceptions_thrown = false;
+
   /// max size for user code created arrays
   size_t max_user_array_length = 0;
   lazy_methods_modet lazy_methods_mode =

jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp

@@ -457,14 +457,16 @@ SCENARIO(
   symbol_tablet symbol_table;
   java_string_library_preprocesst string_preprocess;
   const class_hierarchyt class_hierarchy{};
+  const bool assert_no_exceptions_thrown = false;
   java_bytecode_convert_methodt converter{symbol_table,
                                           null_message_handler,
                                           10,
                                           true,
                                           {},
                                           string_preprocess,
                                           class_hierarchy,
-                                          false};
+                                          false,
+                                          assert_no_exceptions_thrown};
 
   GIVEN("An int array")
   {
@@ -571,14 +573,16 @@ SCENARIO(
   const std::size_t max_array_length = 10;
   const bool throw_assertion_error = true;
   const bool threading_support = false;
+  const bool assert_no_exceptions_thrown = false;
   java_bytecode_convert_methodt converter{symbol_table,
                                           null_message_handler,
                                           max_array_length,
                                           throw_assertion_error,
                                           {},
                                           string_preprocess,
                                           class_hierarchy,
-                                          threading_support};
+                                          threading_support,
+                                          assert_no_exceptions_thrown};
 
   GIVEN("An int_array variable")
   {
@@ -677,14 +681,16 @@ SCENARIO(
   const std::size_t max_array_length = 10;
   const bool throw_assertion_error = true;
   const bool threading_support = false;
+  const bool assert_no_exceptions_thrown = false;
   java_bytecode_convert_methodt converter{symbol_table,
                                           null_message_handler,
                                           max_array_length,
                                           throw_assertion_error,
                                           {},
                                           string_preprocess,
                                           class_hierarchy,
-                                          threading_support};
+                                          threading_support,
+                                          assert_no_exceptions_thrown};
 
   GIVEN("An int_array variable")
   {
@@ -818,14 +824,16 @@ SCENARIO(
   const std::size_t max_array_length = 10;
   const bool throw_assertion_error = true;
   const bool threading_support = false;
+  const bool assert_no_exceptions_thrown = false;
   java_bytecode_convert_methodt converter{symbol_table,
                                           null_message_handler,
                                           max_array_length,
                                           throw_assertion_error,
                                           {},
                                           string_preprocess,
                                           class_hierarchy,
-                                          threading_support};
+                                          threading_support,
+                                          assert_no_exceptions_thrown};
 
   GIVEN("An int_array variable")
   {