From 75a631173f5a51712f06ee2539fddf7d32966e94 Mon Sep 17 00:00:00 2001 From: Cristina Date: Tue, 14 Mar 2017 10:54:08 +0000 Subject: [PATCH 1/3] Modified the expected goto-program for cbmc-java/virtual7 The uncaught exceptions analysis is used to reduce the exception handling instrumentation and consequently the number of new labels and GOTOs --- regression/cbmc-java/virtual7/test.desc | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) 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 From 8feff9555f35b7749d0480234034d669d63fb26e Mon Sep 17 00:00:00 2001 From: Cristina Date: Tue, 14 Mar 2017 11:07:07 +0000 Subject: [PATCH 2/3] Added an uncaught exceptions analysis This analysis computes an overapproximation of the set of exceptions thrown by each method and it is used to prune some of the exception handling instrumentation introduced by remove_exceptions.cpp --- src/analyses/Makefile | 1 + src/analyses/uncaught_exceptions_analysis.cpp | 352 ++++++++++++++++++ src/analyses/uncaught_exceptions_analysis.h | 89 +++++ src/goto-programs/remove_exceptions.cpp | 34 +- 4 files changed, 471 insertions(+), 5 deletions(-) create mode 100644 src/analyses/uncaught_exceptions_analysis.cpp create mode 100644 src/analyses/uncaught_exceptions_analysis.h diff --git a/src/analyses/Makefile b/src/analyses/Makefile index 89f14e4f768..dcc7bad30d7 100644 --- a/src/analyses/Makefile +++ b/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 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..a834de18595 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) { @@ -520,7 +538,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 +559,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); } From 727f37b4791f1449b8cd4a76fe6d25740d0f4b34 Mon Sep 17 00:00:00 2001 From: Cristina Date: Thu, 16 Mar 2017 14:17:08 +0000 Subject: [PATCH 3/3] Make sure that both the caller and callee have exceptional return vars before instrumenting function calls --- src/goto-programs/remove_exceptions.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/goto-programs/remove_exceptions.cpp b/src/goto-programs/remove_exceptions.cpp index a834de18595..dcd4fc9bd1b 100644 --- a/src/goto-programs/remove_exceptions.cpp +++ b/src/goto-programs/remove_exceptions.cpp @@ -332,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=