Ignore AssertionError

This is ignored when we comoute the set of escaped exceptions as well as when replacing throws.

Author: cristina-david

src/analyses/uncaught_exceptions_analysis.cpp

@@ -83,11 +83,11 @@ Function: get_static_type
 
  Outputs:
 
- Purpose: 
+ Purpose: Returns the compile type of an exception
 
 \*******************************************************************/
 
-static irep_idt get_static_type(const typet &type)
+irep_idt uncaught_exceptions_domaint::get_static_type(const typet &type)
 {
   if(type.id()==ID_pointer)
   {
@@ -102,6 +102,26 @@ static irep_idt get_static_type(const typet &type)
 
 /*******************************************************************\
 
+Function: get_exception_symbol
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: Returns the symbol corresponding to an exception
+
+\*******************************************************************/
+
+exprt uncaught_exceptions_domaint::get_exception_symbol(const exprt &expr)
+{
+  if(expr.id()!=ID_symbol && expr.has_operands())
+    return get_exception_symbol(expr.op0());
+
+  return expr;
+}
+
+/*******************************************************************\
+
 Function: uncaught_exceptions_domaint::join
 
   Inputs:
@@ -148,16 +168,20 @@ void uncaught_exceptions_domaint::transform(
   {
   case THROW:
   {
-    const exprt &exc_symbol=instruction.code;
-
+    const exprt &exc_symbol=get_exception_symbol(instruction.code);
     // retrieve the static type of the thrown exception
     const irep_idt &type_id=get_static_type(exc_symbol.type());
-    join(type_id);
-    // we must consider all the subtypes given that
-    // the runtime type is a subtype of the static type
-    std::set<irep_idt> subtypes;
-    get_subtypes(type_id, subtypes, ns);
-    join(subtypes);
+    bool assertion_error=
+      id2string(type_id).find("java.lang.AssertionError")!=std::string::npos;
+    if(!assertion_error)
+    {
+      join(type_id);
+      // we must consider all the subtypes given that
+      // the runtime type is a subtype of the static type
+      std::set<irep_idt> subtypes;
+      get_subtypes(type_id, subtypes, ns);
+      join(subtypes);
+    }
     break;
   }
   case CATCH:

src/analyses/uncaught_exceptions_analysis.h

@@ -41,6 +41,10 @@ class uncaught_exceptions_domaint
     stack_caught.clear();
   }
 
+  static irep_idt get_static_type(const typet &type);
+
+  static exprt get_exception_symbol(const exprt &exor);
+
   void get_elements(std::set<irep_idt> &elements);
 
  private:

src/goto-programs/remove_exceptions.cpp

@@ -115,10 +115,8 @@ void remove_exceptionst::add_exceptional_returns(
     return;
   }
 
-  // We generate an exceptional return value for any function that has
-  // a throw or a function call. This can be improved by only considering
-  // function calls that may escape exceptions. However, this will
-  // require multiple passes.
+  // We generate an exceptional return value for any function that
+  // contains a throw or a function call that may escape exceptions.
   bool add_exceptional_var=false;
   bool has_uncaught_exceptions=false;
   forall_goto_program_instructions(instr_it, goto_program)
@@ -133,7 +131,17 @@ void remove_exceptionst::add_exceptional_returns(
       has_uncaught_exceptions=!exceptions_map[function_name].empty();
     }
 
-    if(instr_it->is_throw() || has_uncaught_exceptions)
+    const exprt &exc =
+      uncaught_exceptions_domaint::get_exception_symbol(instr_it->code);
+    bool assertion_error =
+      id2string(uncaught_exceptions_domaint::get_static_type(exc.type())).
+      find("java.lang.AssertionError")!=std::string::npos;
+
+    // if we find a throw that is not AssertionError of a function call
+    // that may escape exceptions, then we add an exceptional return
+    // variable
+    if((instr_it->is_throw() && !assertion_error)
+       || has_uncaught_exceptions)
     {
       add_exceptional_var=true;
       break;
@@ -282,6 +290,18 @@ void remove_exceptionst::instrument_throw(
 {
   assert(instr_it->type==THROW);
 
+  const exprt &exc_expr=
+    uncaught_exceptions_domaint::get_exception_symbol(instr_it->code);
+  bool assertion_error=id2string(
+    uncaught_exceptions_domaint::get_static_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)
+    return;
+
   goto_programt &goto_program=func_it->second.body;
   const irep_idt &function_id=func_it->first;
 
@@ -341,9 +361,9 @@ void remove_exceptionst::instrument_throw(
   }
 
   // replace "throw x;" by "f#exception_value=x;"
-  exprt exc_expr=instr_it->code;
-  while(exc_expr.id()!=ID_symbol && exc_expr.has_operands())
-    exc_expr=exc_expr.op0();
+  // exprt exc_expr=instr_it->code;
+  // while(exc_expr.id()!=ID_symbol && exc_expr.has_operands())
+  //   exc_expr=exc_expr.op0();
 
   // add the assignment with the appropriate cast
   code_assignt assignment(typecast_exprt(exc_thrown, exc_expr.type()),