Enable propagation of AssertionError

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

Author: peterschrammel

jbmc/src/janalyzer/janalyzer_parse_options.cpp

@@ -670,7 +670,7 @@ bool janalyzer_parse_optionst::process_goto_program(const optionst &options)
     remove_virtual_functions(goto_model);
     // remove Java throw and catch
     // This introduces instanceof, so order is important:
-    remove_exceptions(goto_model);
+    remove_exceptions(goto_model, cmdline.isset("propagate-assertion-error"));
     // remove rtti
     remove_instanceof(goto_model);
 

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*/ \
   "(no-uncaught-exception-check)" \
+  "(propagate-assertion-error)" \
   "(java-assume-inputs-non-null)" \
   "(java-throw-runtime-exceptions)" \
   "(java-max-input-array-length):" \
@@ -42,6 +43,7 @@ Author: Daniel Kroening, [email protected]
 
 #define JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP /*NOLINT*/                                          \
   " --no-uncaught-exception-check    ignore uncaught exceptions and errors\n" \
+  " --propagate-assertion-error      propagate java.lang.AssertionError as exception\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(*) */ \

jbmc/src/java_bytecode/remove_exceptions.cpp

@@ -88,9 +88,11 @@ class remove_exceptionst
   explicit remove_exceptionst(
     symbol_table_baset &_symbol_table,
     function_may_throwt _function_may_throw,
+    bool propagate_assertion_error,
     bool remove_added_instanceof)
     : symbol_table(_symbol_table),
       function_may_throw(_function_may_throw),
+      propagate_assertion_error(propagate_assertion_error),
       remove_added_instanceof(remove_added_instanceof)
   {
   }
@@ -101,6 +103,7 @@ class remove_exceptionst
 protected:
   symbol_table_baset &symbol_table;
   function_may_throwt function_may_throw;
+  bool propagate_assertion_error;
   bool remove_added_instanceof;
 
   symbol_exprt get_inflight_exception_global();
@@ -164,6 +167,9 @@ bool remove_exceptionst::function_or_callees_may_throw(
   {
     if(instr_it->is_throw())
     {
+      if(propagate_assertion_error)
+        return true;
+
       const exprt &exc =
         uncaught_exceptions_domaint::get_exception_symbol(instr_it->code);
       bool is_assertion_error =
@@ -385,10 +391,10 @@ bool remove_exceptionst::instrument_throw(
     uncaught_exceptions_domaint::get_exception_type(exc_expr.type())).
     find("java.lang.AssertionError")!=std::string::npos;
 
-  // we don't count AssertionError (we couldn't catch it anyway
-  // and this may reduce the instrumentation considerably if the programmer
-  // used assertions)
-  if(assertion_error)
+  // we allow AssertionError not to be propagated since
+  // this may reduce the instrumentation considerably if the programmer
+  // used assertions
+  if(assertion_error && !propagate_assertion_error)
     return false;
 
   add_exception_dispatch_sequence(
@@ -472,7 +478,21 @@ void remove_exceptionst::instrument_exceptions(
 
   Forall_goto_program_instructions(instr_it, goto_program)
   {
-    if(instr_it->is_decl())
+    if(instr_it->is_assert())
+    {
+      if(propagate_assertion_error)
+      {
+        // suppress user-provided assertion
+        // because we propgate the AssertionError
+        if(
+          instr_it->guard.is_false() &&
+          instr_it->source_location.get_bool("user-provided"))
+        {
+          instr_it->make_skip();
+        }
+      }
+    }
+    else if(instr_it->is_decl())
     {
       code_declt decl=to_code_decl(instr_it->code);
       locals.push_back(decl.symbol());
@@ -580,6 +600,7 @@ void remove_exceptionst::operator()(goto_programt &goto_program)
 void remove_exceptions(
   symbol_table_baset &symbol_table,
   goto_functionst &goto_functions,
+  bool propagate_assertion_error,
   remove_exceptions_typest type)
 {
   const namespacet ns(symbol_table);
@@ -592,6 +613,7 @@ void remove_exceptions(
   remove_exceptionst remove_exceptions(
     symbol_table,
     function_may_throw,
+    propagate_assertion_error,
     type == remove_exceptions_typest::REMOVE_ADDED_INSTANCEOF);
   remove_exceptions(goto_functions);
 }
@@ -612,6 +634,7 @@ void remove_exceptions(
 void remove_exceptions(
   goto_programt &goto_program,
   symbol_table_baset &symbol_table,
+  bool propagate_assertion_error,
   remove_exceptions_typest type)
 {
   remove_exceptionst::function_may_throwt any_function_may_throw =
@@ -620,12 +643,20 @@ void remove_exceptions(
   remove_exceptionst remove_exceptions(
     symbol_table,
     any_function_may_throw,
+    propagate_assertion_error,
     type == remove_exceptions_typest::REMOVE_ADDED_INSTANCEOF);
   remove_exceptions(goto_program);
 }
 
 /// removes throws/CATCH-POP/CATCH-PUSH
-void remove_exceptions(goto_modelt &goto_model, remove_exceptions_typest type)
+void remove_exceptions(
+  goto_modelt &goto_model,
+  bool propagate_assertion_error,
+  remove_exceptions_typest type)
 {
-  remove_exceptions(goto_model.symbol_table, goto_model.goto_functions, type);
+  remove_exceptions(
+    goto_model.symbol_table,
+    goto_model.goto_functions,
+    propagate_assertion_error,
+    type);
 }

jbmc/src/java_bytecode/remove_exceptions.h

@@ -32,11 +32,13 @@ enum class remove_exceptions_typest
 void remove_exceptions(
   goto_programt &goto_program,
   symbol_table_baset &symbol_table,
+  bool propagate_assertion_error,
   remove_exceptions_typest type =
     remove_exceptions_typest::DONT_REMOVE_INSTANCEOF);
 
 void remove_exceptions(
   goto_modelt &goto_model,
+  bool propagate_assertion_error,
   remove_exceptions_typest type =
     remove_exceptions_typest::DONT_REMOVE_INSTANCEOF);
 

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -382,6 +382,11 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
 
   PARSE_OPTIONS_GOTO_TRACE(cmdline, options);
 
+  if(cmdline.isset("propagate-assertion-error"))
+    options.set_option("propagate-assertion-error", true);
+  else
+    options.set_option("propagate-assertion-error", false);
+
   if(cmdline.isset("symex-driven-lazy-loading"))
   {
     options.set_option("symex-driven-lazy-loading", true);
@@ -743,6 +748,8 @@ void jbmc_parse_optionst::process_goto_function(
 
   bool using_symex_driven_loading =
     options.get_bool_option("symex-driven-lazy-loading");
+  bool propagate_assertion_error =
+    options.get_bool_option("propagate-assertion-error");
 
   try
   {
@@ -761,6 +768,7 @@ void jbmc_parse_optionst::process_goto_function(
       remove_exceptions(
         goto_function.body,
         symbol_table,
+        propagate_assertion_error,
         remove_exceptions_typest::REMOVE_ADDED_INSTANCEOF);
     }
 
@@ -899,6 +907,8 @@ bool jbmc_parse_optionst::process_goto_functions(
 
     bool using_symex_driven_loading =
       options.get_bool_option("symex-driven-lazy-loading");
+    bool propagate_assertion_error =
+      options.get_bool_option("propagate-assertion-error");
 
     // When using symex-driven lazy loading, *all* relevant processing is done
     // during process_goto_function, so we have nothing to do here.
@@ -908,7 +918,9 @@ bool jbmc_parse_optionst::process_goto_functions(
     // remove catch and throw
     // (introduces instanceof but request it is removed)
     remove_exceptions(
-      goto_model, remove_exceptions_typest::REMOVE_ADDED_INSTANCEOF);
+      goto_model,
+      propagate_assertion_error,
+      remove_exceptions_typest::REMOVE_ADDED_INSTANCEOF);
 
     // instrument library preconditions
     instrument_preconditions(goto_model);

jbmc/src/jdiff/jdiff_parse_options.cpp

@@ -346,7 +346,7 @@ bool jdiff_parse_optionst::process_goto_program(
     // Java virtual functions -> explicit dispatch tables:
     remove_virtual_functions(goto_model);
     // remove catch and throw
-    remove_exceptions(goto_model);
+    remove_exceptions(goto_model, cmdline.isset("propagate-assertion-error"));
     // Java instanceof -> clsid comparison:
     remove_instanceof(goto_model);