Enable throwing of AssertionError

Introduces --throw-assertion-error which allows
to propgate AssertionError as performed in the JVM
rather than using a goto ASSERT statement.

Author: peterschrammel

jbmc/regression/jbmc/assert3/test_propagate_no_uncaught.desc renamed to jbmc/regression/jbmc/assert3/test_throw_no_uncaught.desc

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

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -1241,6 +1241,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
     {
       PRECONDITION(op.size() == 1 && results.size() == 1);
       if(
+        !throw_assertion_error &&
         uncaught_exceptions_domaint::get_exception_type(op[0].type()) ==
           "java::java.lang.AssertionError")
       {
@@ -2867,6 +2868,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)
@@ -2885,6 +2887,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_language.cpp

@@ -47,6 +47,7 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd)
   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");
+  throw_assertion_error = cmd.isset("throw-assertion-error");
   threading_support = cmd.isset("java-threading");
 
   if(cmd.isset("java-max-input-array-length"))
@@ -1038,6 +1039,7 @@ bool java_bytecode_languaget::convert_single_method(
       symbol_table,
       get_message_handler(),
       max_user_array_length,
+      throw_assertion_error,
       std::move(needed_lazy_methods),
       string_preprocess,
       class_hierarchy);

jbmc/src/java_bytecode/java_bytecode_language.h

@@ -29,6 +29,7 @@ Author: Daniel Kroening, [email protected]
 // clang-format off
 #define JAVA_BYTECODE_LANGUAGE_OPTIONS /*NOLINT*/ \
   "(disable-uncaught-exception-check)" \
+  "(throw-assertion-error)" \
   "(java-assume-inputs-non-null)" \
   "(java-throw-runtime-exceptions)" \
   "(java-max-input-array-length):" \
@@ -43,6 +44,9 @@ Author: Daniel Kroening, [email protected]
 #define JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP /*NOLINT*/                                          \
   " --disable-uncaught-exception-check" \
   "                                  ignore uncaught exceptions and errors\n" \
+  " --throw-assertion-error          throw java.lang.AssertionError on violated\n"               /* NOLINT(*) */ \
+  "                                  assert statements instead of failing\n" \
+  "                                  at the location of the assert statement\n"                  /* NOLINT(*) */ \
   " --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(*) */ \
@@ -173,6 +177,7 @@ class java_bytecode_languaget:public languaget
   bool string_refinement_enabled;
   bool throw_runtime_exceptions;
   bool assert_uncaught_exceptions;
+  bool throw_assertion_error;
   java_string_library_preprocesst string_preprocess;
   std::string java_cp_include_files;