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/regression/jbmc/assert3/test_propagate_assertion_error.desc

@@ -0,0 +1,9 @@
+CORE
+assert3.class
+--propagate-assertion-error
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+^\[.*\] no uncaught exception: FAILURE$
+--
+^warning: ignoring

jbmc/regression/jbmc/assert3/test_propagate_no_uncaught.desc

@@ -0,0 +1,8 @@
+CORE
+assert3.class
+--propagate-assertion-error --no-uncaught-exception-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

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,18 +600,21 @@ 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);
   std::map<irep_idt, std::set<irep_idt>> exceptions_map;
-  uncaught_exceptions(goto_functions, ns, exceptions_map);
+  uncaught_exceptions(
+    goto_functions, ns, propagate_assertion_error, exceptions_map);
   remove_exceptionst::function_may_throwt function_may_throw =
     [&exceptions_map](const irep_idt &id) {
       return !exceptions_map[id].empty();
     };
   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 +635,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 +644,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);
 

src/analyses/uncaught_exceptions_analysis.cpp

@@ -72,7 +72,7 @@ void uncaught_exceptions_domaint::transform(
     const irep_idt &type_id=get_exception_type(exc_symbol.type());
     bool assertion_error=
       id2string(type_id).find("java.lang.AssertionError")!=std::string::npos;
-    if(!assertion_error)
+    if(!assertion_error || propagate_assertion_error)
     {
       join(type_id);
       // we must consider all the subtypes given that
@@ -227,8 +227,9 @@ void uncaught_exceptions_analysist::operator()(
 void uncaught_exceptions(
   const goto_functionst &goto_functions,
   const namespacet &ns,
+  bool propagate_assertion_error,
   std::map<irep_idt, std::set<irep_idt>> &exceptions_map)
 {
-  uncaught_exceptions_analysist exceptions;
+  uncaught_exceptions_analysist exceptions(propagate_assertion_error);
   exceptions(goto_functions, ns, exceptions_map);
 }

src/analyses/uncaught_exceptions_analysis.h

@@ -23,7 +23,12 @@ class uncaught_exceptions_analysist;
 
 class uncaught_exceptions_domaint
 {
- public:
+public:
+  explicit uncaught_exceptions_domaint(bool propagate_assertion_error)
+    : propagate_assertion_error(propagate_assertion_error)
+  {
+  }
+
   void transform(const goto_programt::const_targett,
                  uncaught_exceptions_analysist &,
                  const namespacet &);
@@ -46,18 +51,24 @@ class uncaught_exceptions_domaint
 
   void operator()(const namespacet &ns);
 
- private:
+private:
+  const bool propagate_assertion_error;
   typedef std::vector<std::set<irep_idt>> stack_caughtt;
   stack_caughtt stack_caught;
   std::set<irep_idt> thrown;
   class_hierarchyt class_hierarchy;
 };
 
-/// computes in exceptions_map an overapproximation of the  exceptions thrown by
+/// computes in exceptions_map an overapproximation of the exceptions thrown by
 /// each method
 class uncaught_exceptions_analysist
 {
 public:
+  explicit uncaught_exceptions_analysist(bool propagate_assertion_error)
+    : domain(propagate_assertion_error)
+  {
+  }
+
   typedef std::map<irep_idt, std::set<irep_idt>> exceptions_mapt;
 
   void collect_uncaught_exceptions(
@@ -73,14 +84,15 @@ class uncaught_exceptions_analysist
 
   friend class uncaught_exceptions_domaint;
 
- private:
+private:
   uncaught_exceptions_domaint domain;
   exceptions_mapt exceptions_map;
 };
 
 void uncaught_exceptions(
   const goto_functionst &,
   const namespacet &,
+  bool propagate_assertion_error,
   std::map<irep_idt, std::set<irep_idt>> &);
 
 #endif