Uncaught exceptions analysis

regression/cbmc-java/virtual7/test.desc

@@ -3,9 +3,9 @@ test.class
 --show-goto-functions
 ^EXIT=0$
 ^SIGNAL=0$
-IF "java::E".*THEN GOTO [67]
-IF "java::B".*THEN GOTO [67]
-IF "java::D".*THEN GOTO [67]
-IF "java::C".*THEN GOTO [67]
+IF "java::E".*THEN GOTO [12]
+IF "java::B".*THEN GOTO [12]
+IF "java::D".*THEN GOTO [12]
+IF "java::C".*THEN GOTO [12]
 --
 IF "java::A".*THEN GOTO

src/analyses/Makefile

@@ -5,6 +5,7 @@ SRC = natural_loops.cpp is_threaded.cpp dirty.cpp interval_analysis.cpp \
       goto_rw.cpp reaching_definitions.cpp ai.cpp local_cfg.cpp \
       local_bitvector_analysis.cpp dependence_graph.cpp \
       constant_propagator.cpp replace_symbol_ext.cpp \
+      uncaught_exceptions_analysis.cpp \
       flow_insensitive_analysis.cpp \
       custom_bitvector_analysis.cpp escape_analysis.cpp global_may_alias.cpp
 

src/analyses/uncaught_exceptions_analysis.cpp

@@ -0,0 +1,352 @@
+/*******************************************************************\
+
+Module: Over-approximating uncaught exceptions analysis
+
+Author: Cristina David
+
+\*******************************************************************/
+
+#ifdef DEBUG
+#include <iostream>
+#endif
+#include "uncaught_exceptions_analysis.h"
+
+/*******************************************************************\
+
+Function: get_subtypes
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: computes the set of subtypes of "type" by iterating over
+          the symbol table
+\*******************************************************************/
+
+static void get_subtypes(
+  const irep_idt &type,
+  std::set<irep_idt> &subtypes,
+  const namespacet &ns)
+{
+  irep_idt candidate;
+  bool new_subtype=true;
+  const symbol_tablet &symbol_table=ns.get_symbol_table();
+
+  // as we don't know the order types have been recorded,
+  // we need to iterate over the symbol table until there are no more
+  // new subtypes found
+  while(new_subtype)
+  {
+    new_subtype=false;
+    // iterate over the symbol_table in order to find subtypes of type
+    forall_symbols(it, symbol_table.symbols)
+    {
+      // we only look at type entries
+      if(it->second.is_type)
+      {
+        // every type is a potential candidate
+        candidate=it->second.name;
+        // current candidate is already in subtypes
+        if(find(subtypes.begin(),
+                subtypes.end(),
+                candidate)!=subtypes.end())
+          continue;
+        // get its base class
+        const irept::subt &bases=to_class_type((it->second).type).bases();
+        if(bases.size()>0)
+        {
+          const irept &base = bases[0];
+          const irept &base_type=base.find(ID_type);
+          assert(base_type.id()==ID_symbol);
+
+          // is it derived from type?
+          // i.e. does it have type or one of its subtypes as a base?
+          if(base_type.get(ID_identifier)==type ||
+             find(subtypes.begin(), subtypes.end(),
+                  base_type.get(ID_identifier))!=subtypes.end())
+          {
+            subtypes.insert(candidate);
+            new_subtype=true;
+          }
+        }
+      }
+    }
+  }
+}
+
+/*******************************************************************\
+
+Function: get_static_type
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: 
+
+\*******************************************************************/
+
+static irep_idt get_static_type(const typet &type)
+{
+  if(type.id()==ID_pointer)
+  {
+    return get_static_type(type.subtype());
+  }
+  else if(type.id()==ID_symbol)
+  {
+     return to_symbol_type(type).get_identifier();
+  }
+  return ID_empty;
+}
+
+/*******************************************************************\
+
+Function: uncaught_exceptions_domaint::join
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: 
+
+\*******************************************************************/
+
+void uncaught_exceptions_domaint::join(
+  const irep_idt &element)
+{
+  thrown.insert(element);
+}
+
+void uncaught_exceptions_domaint::join(
+  const std::set<irep_idt> &elements)
+{
+  thrown.insert(elements.begin(), elements.end());
+}
+
+
+/*******************************************************************\
+
+Function: uncaught_exceptions_domaint::transform
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: 
+
+\*******************************************************************/
+
+void uncaught_exceptions_domaint::transform(
+  const goto_programt::const_targett from,
+  uncaught_exceptions_analysist &uea,
+  const namespacet &ns)
+{
+  const goto_programt::instructiont &instruction=*from;
+
+  switch(instruction.type)
+  {
+  case THROW:
+  {
+    const exprt &exc_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);
+    break;
+  }
+  case CATCH:
+  {
+    if(!instruction.code.has_operands())
+    {
+      if(!instruction.targets.empty()) // push
+      {
+        std::set<irep_idt> caught;
+        stack_caught.push_back(caught);
+        std::set<irep_idt> &last_caught=stack_caught.back();
+        const irept::subt &exception_list=
+          instruction.code.find(ID_exception_list).get_sub();
+
+        for(const auto &exc : exception_list)
+        {
+          last_caught.insert(exc.id());
+          std::set<irep_idt> subtypes;
+          get_subtypes(exc.id(), subtypes, ns);
+          last_caught.insert(subtypes.begin(), subtypes.end());
+        }
+      }
+      else // pop
+      {
+        if(!stack_caught.empty())
+        {
+          const std::set<irep_idt> &caught=stack_caught.back();
+          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);
+          }
+          stack_caught.pop_back();
+        }
+      }
+    }
+    break;
+  }
+  case FUNCTION_CALL:
+  {
+    const exprt &function_expr=
+      to_code_function_call(instruction.code).function();
+    assert(function_expr.id()==ID_symbol);
+    const irep_idt &function_name=
+      to_symbol_expr(function_expr).get_identifier();
+    // use the current information about the callee
+    join(uea.exceptions_map[function_name]);
+    break;
+  }
+  default:
+  {}
+  }
+}
+
+/*******************************************************************\
+
+Function: uncaught_exceptions_domaint::get_elements
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: 
+
+\*******************************************************************/
+
+void uncaught_exceptions_domaint::get_elements(
+  std::set<irep_idt> &elements)
+{
+  elements=thrown;
+}
+
+/*******************************************************************\
+
+Function: uncaught_exceptions_analysist::collect_uncaught_exceptions
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: 
+
+\*******************************************************************/
+
+void uncaught_exceptions_analysist::collect_uncaught_exceptions(
+  const goto_functionst &goto_functions,
+  const namespacet &ns)
+{
+  bool change=true;
+
+  while(change)
+  {
+    change=false;
+    // add all the functions to the worklist
+    forall_goto_functions(current_function, goto_functions)
+    {
+      domain.make_top();
+      const goto_programt &goto_program=current_function->second.body;
+
+      if(goto_program.empty())
+        continue;
+
+      forall_goto_program_instructions(instr_it, goto_program)
+      {
+        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;
+    }
+  }
+}
+
+/*******************************************************************\
+
+Function: uncaught_exceptions_analysist::output
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: 
+
+\*******************************************************************/
+
+void uncaught_exceptions_analysist::output(
+  const goto_functionst &goto_functions)
+{
+#ifdef DEBUG
+  forall_goto_functions(it, goto_functions)
+  {
+    if(exceptions_map[it->first].size()>0)
+    {
+      std::cout << "Uncaught exceptions in function " <<
+        it->first << ": " << std::endl;
+      assert(exceptions_map.find(it->first)!=exceptions_map.end());
+      for(auto exc_id : exceptions_map[it->first])
+        std::cout << id2string(exc_id) << " ";
+      std::cout << std::endl;
+    }
+  }
+#endif
+}
+
+/*******************************************************************\
+
+Function: uncaught_exceptions_analysist::operator()
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: 
+
+\*******************************************************************/
+
+void uncaught_exceptions_analysist::operator()(
+  const goto_functionst &goto_functions,
+  const namespacet &ns,
+  exceptions_mapt &exceptions)
+{
+  collect_uncaught_exceptions(goto_functions, ns);
+  exceptions=exceptions_map;
+  output(goto_functions);
+}
+
+/*******************************************************************\
+
+Function: uncaught_exceptions
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: 
+
+\*******************************************************************/
+
+void uncaught_exceptions(
+  const goto_functionst &goto_functions,
+  const namespacet &ns,
+  std::map<irep_idt, std::set<irep_idt>> &exceptions_map)
+{
+  uncaught_exceptions_analysist exceptions;
+  exceptions(goto_functions, ns, exceptions_map);
+}