Addressed reviewers comments

Author: cristina-david

src/analyses/uncaught_exceptions_analysis.cpp

@@ -5,14 +5,15 @@ Module: Over-approximating uncaught exceptions analysis
 Author: Cristina David
 
 \*******************************************************************/
+
 #ifdef DEBUG
 #include <iostream>
 #endif
 #include "uncaught_exceptions_analysis.h"
 
 /*******************************************************************\
 
-Function: get_static_type
+Function: get_exception_type
 
   Inputs:
 
@@ -22,15 +23,13 @@ Function: get_static_type
 
 \*******************************************************************/
 
-irep_idt uncaught_exceptions_domaint::get_static_type(const typet &type)
+irep_idt uncaught_exceptions_domaint::get_exception_type(const typet &type)
 {
-  if(type.id()==ID_pointer)
-  {
-    return get_static_type(type.subtype());
-  }
-  else if(type.id()==ID_symbol)
+  assert(type.id()==ID_pointer);
+
+  if(type.subtype().id()==ID_symbol)
   {
-     return to_symbol_type(type).get_identifier();
+    return to_symbol_type(type.subtype()).get_identifier();
   }
   return ID_empty;
 }
@@ -63,7 +62,7 @@ Function: uncaught_exceptions_domaint::join
 
  Outputs:
 
- Purpose: 
+ Purpose: The join operator for the uncaught exceptions domain
 
 \*******************************************************************/
 
@@ -94,7 +93,7 @@ Function: uncaught_exceptions_domaint::transform
 
  Outputs:
 
- Purpose: 
+ Purpose: The transformer for the uncaught exceptions domain
 
 \*******************************************************************/
 
@@ -111,7 +110,7 @@ void uncaught_exceptions_domaint::transform(
   {
     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());
+    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)
@@ -153,12 +152,7 @@ void uncaught_exceptions_domaint::transform(
           join(caught);
           // remove the caught exceptions
           for(const auto &exc_id : caught)
-          {
-            const std::set<irep_idt>::iterator it=
-              std::find(thrown.begin(), thrown.end(), exc_id);
-            if(it!=thrown.end())
-              thrown.erase(it);
-          }
+            thrown.erase(exc_id);
           stack_caught.pop_back();
         }
       }
@@ -189,14 +183,13 @@ Function: uncaught_exceptions_domaint::get_elements
 
  Outputs:
 
- Purpose: 
+ Purpose: Returns the value of the private member thrown
 
 \*******************************************************************/
 
-void uncaught_exceptions_domaint::get_elements(
-  std::set<irep_idt> &elements)
+const std::set<irep_idt> &uncaught_exceptions_domaint::get_elements() const
 {
-  elements=thrown;
+  return thrown;
 }
 
 /*******************************************************************\
@@ -207,7 +200,7 @@ Function: uncaught_exceptions_domaint::operator()
 
  Outputs:
 
- Purpose: 
+ Purpose: Constructs the class hierarchy
 
 \*******************************************************************/
 
@@ -225,7 +218,8 @@ Function: uncaught_exceptions_analysist::collect_uncaught_exceptions
 
  Outputs:
 
- Purpose: 
+ Purpose: Runs the uncaught exceptions analysis, which 
+          populates the exceptions map
 
 \*******************************************************************/
 
@@ -252,11 +246,12 @@ void uncaught_exceptions_analysist::collect_uncaught_exceptions(
         domain.transform(instr_it, *this, ns);
       }
       // did our estimation for the current function improve?
-      std::set<irep_idt> elements;
-      domain.get_elements(elements);
-      change=change||
-        exceptions_map[current_function->first].size()!=elements.size();
-      exceptions_map[current_function->first]=elements;
+      const std::set<irep_idt> &elements=domain.get_elements();
+      if(exceptions_map[current_function->first].size()<elements.size())
+      {
+        change=true;
+        exceptions_map[current_function->first]=elements;
+      }
     }
   }
 }
@@ -269,7 +264,8 @@ Function: uncaught_exceptions_analysist::output
 
  Outputs:
 
- Purpose: 
+ Purpose: Prints the exceptions map that maps each method to the 
+          set of exceptions that may escape it
 
 \*******************************************************************/
 
@@ -300,7 +296,8 @@ Function: uncaught_exceptions_analysist::operator()
 
  Outputs:
 
- Purpose: 
+ Purpose: Applies the uncaught exceptions analysis and 
+          outputs the result
 
 \*******************************************************************/
 
@@ -323,7 +320,8 @@ Function: uncaught_exceptions
 
  Outputs:
 
- Purpose: 
+ Purpose: Applies the uncaught exceptions analysis and 
+          outputs the result
 
 \*******************************************************************/
 

src/analyses/uncaught_exceptions_analysis.h

@@ -43,11 +43,11 @@ class uncaught_exceptions_domaint
     stack_caught.clear();
   }
 
-  static irep_idt get_static_type(const typet &type);
+  static irep_idt get_exception_type(const typet &type);
 
   static exprt get_exception_symbol(const exprt &exor);
 
-  void get_elements(std::set<irep_idt> &elements);
+  const std::set<irep_idt>  &get_elements() const;
 
   void operator()(const namespacet &ns);
 

src/goto-programs/remove_exceptions.cpp

@@ -117,10 +117,9 @@ void remove_exceptionst::add_exceptional_returns(
 
   // 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)
   {
+    bool has_uncaught_exceptions=false;
     if(instr_it->is_function_call())
     {
       const exprt &function_expr=
@@ -131,53 +130,53 @@ void remove_exceptionst::add_exceptional_returns(
       has_uncaught_exceptions=!exceptions_map[function_name].empty();
     }
 
-    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;
+    bool assertion_error=false;
+    if(instr_it->is_throw())
+    {
+      const exprt &exc =
+        uncaught_exceptions_domaint::get_exception_symbol(instr_it->code);
+      assertion_error =
+        id2string(uncaught_exceptions_domaint::get_exception_type(exc.type())).
+        find("java.lang.AssertionError")!=std::string::npos;
+    }
 
-    // if we find a throw that is not AssertionError of a function call
+    // if we find a throw different from AssertionError or 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;
+      // look up the function symbol
+      symbol_tablet::symbolst::iterator s_it=
+        symbol_table.symbols.find(function_id);
+
+      assert(s_it!=symbol_table.symbols.end());
+
+      auxiliary_symbolt new_symbol;
+      new_symbol.is_static_lifetime=true;
+      new_symbol.module=function_symbol.module;
+      new_symbol.base_name=id2string(function_symbol.base_name)+EXC_SUFFIX;
+      new_symbol.name=id2string(function_symbol.name)+EXC_SUFFIX;
+      new_symbol.mode=function_symbol.mode;
+      new_symbol.type=typet(ID_pointer, empty_typet());
+      symbol_table.add(new_symbol);
+
+      // initialize the exceptional return with NULL
+      symbol_exprt lhs_expr_null=new_symbol.symbol_expr();
+      null_pointer_exprt rhs_expr_null((pointer_typet(empty_typet())));
+      goto_programt::targett t_null=
+        goto_program.insert_before(goto_program.instructions.begin());
+      t_null->make_assignment();
+      t_null->source_location=
+        goto_program.instructions.begin()->source_location;
+      t_null->code=code_assignt(
+        lhs_expr_null,
+        rhs_expr_null);
+      t_null->function=function_id;
+
       break;
     }
   }
-
-  if(add_exceptional_var)
-  {
-    // look up the function symbol
-    symbol_tablet::symbolst::iterator s_it=
-      symbol_table.symbols.find(function_id);
-
-    assert(s_it!=symbol_table.symbols.end());
-
-    auxiliary_symbolt new_symbol;
-    new_symbol.is_static_lifetime=true;
-    new_symbol.module=function_symbol.module;
-    new_symbol.base_name=id2string(function_symbol.base_name)+EXC_SUFFIX;
-    new_symbol.name=id2string(function_symbol.name)+EXC_SUFFIX;
-    new_symbol.mode=function_symbol.mode;
-    new_symbol.type=typet(ID_pointer, empty_typet());
-    symbol_table.add(new_symbol);
-
-    // initialize the exceptional return with NULL
-    symbol_exprt lhs_expr_null=new_symbol.symbol_expr();
-    null_pointer_exprt rhs_expr_null((pointer_typet(empty_typet())));
-    goto_programt::targett t_null=
-      goto_program.insert_before(goto_program.instructions.begin());
-    t_null->make_assignment();
-    t_null->source_location=
-      goto_program.instructions.begin()->source_location;
-    t_null->code=code_assignt(
-      lhs_expr_null,
-      rhs_expr_null);
-    t_null->function=function_id;
-  }
 }
 
 /*******************************************************************\
@@ -293,7 +292,7 @@ void remove_exceptionst::instrument_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())).
+    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
@@ -360,11 +359,6 @@ void remove_exceptionst::instrument_throw(
     t_dead->function=instr_it->function;
   }
 
-  // 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();
-
   // add the assignment with the appropriate cast
   code_assignt assignment(typecast_exprt(exc_thrown, exc_expr.type()),
                           exc_expr);