diff --git a/regression/cbmc-java/virtual7/test.desc b/regression/cbmc-java/virtual7/test.desc index 2e196d82e8c..b35404ac657 100644 --- a/regression/cbmc-java/virtual7/test.desc +++ b/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 diff --git a/src/analyses/Makefile b/src/analyses/Makefile index 690b119e83c..77c7d7f92d0 100644 --- a/src/analyses/Makefile +++ b/src/analyses/Makefile @@ -24,6 +24,7 @@ SRC = ai.cpp \ reaching_definitions.cpp \ replace_symbol_ext.cpp \ static_analysis.cpp \ + uncaught_exceptions_analysis.cpp \ uninitialized_domain.cpp \ # Empty last line diff --git a/src/analyses/uncaught_exceptions_analysis.cpp b/src/analyses/uncaught_exceptions_analysis.cpp new file mode 100644 index 00000000000..75b18923c6a --- /dev/null +++ b/src/analyses/uncaught_exceptions_analysis.cpp @@ -0,0 +1,352 @@ +/*******************************************************************\ + +Module: Over-approximating uncaught exceptions analysis + +Author: Cristina David + +\*******************************************************************/ + +#ifdef DEBUG +#include +#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 &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 &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 subtypes; + get_subtypes(type_id, subtypes, ns); + join(subtypes); + break; + } + case CATCH: + { + if(!instruction.code.has_operands()) + { + if(!instruction.targets.empty()) // push + { + std::set caught; + stack_caught.push_back(caught); + std::set &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 subtypes; + get_subtypes(exc.id(), subtypes, ns); + last_caught.insert(subtypes.begin(), subtypes.end()); + } + } + else // pop + { + if(!stack_caught.empty()) + { + const std::set &caught=stack_caught.back(); + join(caught); + // remove the caught exceptions + for(const auto &exc_id : caught) + { + const std::set::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 &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 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> &exceptions_map) +{ + uncaught_exceptions_analysist exceptions; + exceptions(goto_functions, ns, exceptions_map); +} diff --git a/src/analyses/uncaught_exceptions_analysis.h b/src/analyses/uncaught_exceptions_analysis.h new file mode 100644 index 00000000000..ff9df50fdaf --- /dev/null +++ b/src/analyses/uncaught_exceptions_analysis.h @@ -0,0 +1,89 @@ +/*******************************************************************\ + +Module: Over-approximative uncaught exceptions analysis + +Author: Cristina David + +\*******************************************************************/ + +#ifndef CPROVER_ANALYSES_UNCAUGHT_EXCEPTIONS_ANALYSIS_H +#define CPROVER_ANALYSES_UNCAUGHT_EXCEPTIONS_ANALYSIS_H + +#include +#include +#include +#include + +/*******************************************************************\ + + Class: uncaught_exceptions_domaint + + Purpose: defines the domain used by the uncaught + exceptions analysis + +\*******************************************************************/ + +class uncaught_exceptions_analysist; + +class uncaught_exceptions_domaint +{ + public: + void transform(const goto_programt::const_targett, + uncaught_exceptions_analysist &, + const namespacet &); + + void join(const irep_idt &); + void join(const std::set &); + + void make_top() + { + thrown.clear(); + stack_caught.clear(); + } + + void get_elements(std::set &elements); + + private: + typedef std::vector> stack_caughtt; + stack_caughtt stack_caught; + std::set thrown; +}; + +/*******************************************************************\ + + Class: uncaught_exceptions_analysist + + Purpose: computes in exceptions_map an overapproximation of the + exceptions thrown by each method + +\*******************************************************************/ + +class uncaught_exceptions_analysist +{ +public: + typedef std::map> exceptions_mapt; + + void collect_uncaught_exceptions( + const goto_functionst &, + const namespacet &); + + void output(const goto_functionst &); + + void operator()( + const goto_functionst &, + const namespacet &, + exceptions_mapt &); + + friend class uncaught_exceptions_domaint; + + private: + uncaught_exceptions_domaint domain; + exceptions_mapt exceptions_map; +}; + +void uncaught_exceptions( + const goto_functionst &, + const namespacet &, + std::map> &); + +#endif diff --git a/src/goto-programs/remove_exceptions.cpp b/src/goto-programs/remove_exceptions.cpp index e73eba8d2ec..dcd4fc9bd1b 100644 --- a/src/goto-programs/remove_exceptions.cpp +++ b/src/goto-programs/remove_exceptions.cpp @@ -19,6 +19,7 @@ Date: December 2016 #include #include "remove_exceptions.h" +#include class remove_exceptionst { @@ -27,8 +28,11 @@ class remove_exceptionst typedef std::vector stack_catcht; public: - explicit remove_exceptionst(symbol_tablet &_symbol_table): - symbol_table(_symbol_table) + explicit remove_exceptionst( + symbol_tablet &_symbol_table, + std::map> &_exceptions_map): + symbol_table(_symbol_table), + exceptions_map(_exceptions_map) { } @@ -37,6 +41,7 @@ class remove_exceptionst protected: symbol_tablet &symbol_table; + std::map> &exceptions_map; void add_exceptional_returns( const goto_functionst::function_mapt::iterator &); @@ -95,12 +100,25 @@ void remove_exceptionst::add_exceptional_returns( // function calls that may escape exceptions. However, this will // require multiple passes. bool add_exceptional_var=false; + bool has_uncaught_exceptions=false; forall_goto_program_instructions(instr_it, goto_program) - if(instr_it->is_throw() || instr_it->is_function_call()) + { + if(instr_it->is_function_call()) + { + const exprt &function_expr= + to_code_function_call(instr_it->code).function(); + assert(function_expr.id()==ID_symbol); + const irep_idt &function_name= + to_symbol_expr(function_expr).get_identifier(); + has_uncaught_exceptions=!exceptions_map[function_name].empty(); + } + + if(instr_it->is_throw() || has_uncaught_exceptions) { add_exceptional_var=true; break; } + } if(add_exceptional_var) { @@ -314,7 +332,8 @@ void remove_exceptionst::instrument_function_call( const irep_idt &callee_id= to_symbol_expr(function_call.function()).get_identifier(); - if(symbol_table.has_symbol(id2string(callee_id)+EXC_SUFFIX)) + if(symbol_table.has_symbol(id2string(callee_id)+EXC_SUFFIX) && + symbol_table.has_symbol(id2string(function_id)+EXC_SUFFIX)) { // we may have an escaping exception const symbolt &callee_exc_symbol= @@ -520,7 +539,10 @@ void remove_exceptions( symbol_tablet &symbol_table, goto_functionst &goto_functions) { - remove_exceptionst remove_exceptions(symbol_table); + const namespacet ns(symbol_table); + std::map> exceptions_map; + uncaught_exceptions(goto_functions, ns, exceptions_map); + remove_exceptionst remove_exceptions(symbol_table, exceptions_map); remove_exceptions(goto_functions); } @@ -538,6 +560,9 @@ Purpose: removes throws/CATCH-POP/CATCH-PUSH void remove_exceptions(goto_modelt &goto_model) { - remove_exceptionst remove_exceptions(goto_model.symbol_table); + std::map> exceptions_map; + remove_exceptionst remove_exceptions( + goto_model.symbol_table, + exceptions_map); remove_exceptions(goto_model.goto_functions); }