Add an assume-no-exceptions-thrown option

This is to specify that we want to replace all throw instructions by
assume 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

@@ -2344,9 +2344,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")
+    assume_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;
@@ -3184,7 +3185,8 @@ void java_bytecode_convert_method(
   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 assume_no_exceptions_thrown)
 
 {
   java_bytecode_convert_methodt java_bytecode_convert_method(
@@ -3195,7 +3197,8 @@ void java_bytecode_convert_method(
     needed_lazy_methods,
     string_preprocess,
     class_hierarchy,
-    threading_support);
+    threading_support,
+    assume_no_exceptions_thrown);
 
   java_bytecode_convert_method(class_symbol, method);
 }

jbmc/src/java_bytecode/java_bytecode_convert_method.h

@@ -37,7 +37,8 @@ void java_bytecode_convert_method(
   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 assume_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 assume_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),
+      assume_no_exceptions_thrown(assume_no_exceptions_thrown),
       threading_support(threading_support),
       needed_lazy_methods(std::move(needed_lazy_methods)),
       string_preprocess(_string_preprocess),
@@ -73,6 +75,7 @@ class java_bytecode_convert_methodt:public messaget
   namespacet ns;
   const size_t max_array_length;
   const bool throw_assertion_error;
+  const bool assume_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(
+    "assume-no-exceptions-thrown", cmd.isset("assume-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");
+  assume_no_exceptions_thrown =
+    options.get_bool_option("assume-no-exceptions-thrown");
   threading_support = options.get_bool_option("java-threading");
   max_user_array_length =
     options.get_unsigned_int_option("java-max-vla-length");
@@ -1328,7 +1332,8 @@ bool java_bytecode_languaget::convert_single_method(
       std::move(needed_lazy_methods),
       string_preprocess,
       class_hierarchy,
-      language_options->threading_support);
+      language_options->threading_support,
+      language_options->assume_no_exceptions_thrown);
     INVARIANT(declaring_class(symbol), "Method must have a declaring class.");
     return false;
   }
@@ -1359,7 +1364,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

@@ -32,6 +32,7 @@ Author: Daniel Kroening, [email protected]
 #define JAVA_BYTECODE_LANGUAGE_OPTIONS /*NOLINT*/ \
   "(disable-uncaught-exception-check)" \
   "(throw-assertion-error)" \
+  "(assume-no-exceptions-thrown)" \
   "(java-assume-inputs-non-null)" \
   "(java-assume-inputs-interval):" \
   "(java-assume-inputs-integral)" \
@@ -56,6 +57,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" \
+  " --assume-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(*) */ \
@@ -110,9 +114,9 @@ Author: Daniel Kroening, [email protected]
   "                              (clinit) method.\n" \
   "                              The argument can be a relative or absolute path to\n"/* NOLINT(*) */ \
   "                              the file.\n"
-// clang-format on
+  // clang-format on
 
-class symbolt;
+  class symbolt;
 
 enum lazy_methods_modet
 {
@@ -164,6 +168,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 assume_no_exceptions_thrown = false;
+
   /// max size for user code created arrays
   size_t max_user_array_length = 0;
   lazy_methods_modet lazy_methods_mode =