From d4378331ef051c99df42afc7622e36ab659f97d7 Mon Sep 17 00:00:00 2001 From: Cristina Date: Tue, 14 Mar 2017 11:07:07 +0000 Subject: [PATCH 1/7] 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/uncaught_exceptions_analysis.cpp | 352 ++++++++++++++++++ src/analyses/uncaught_exceptions_analysis.h | 89 +++++ src/goto-programs/remove_exceptions.cpp | 34 +- 3 files changed, 470 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/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 5726831804f..9ed00e661c1 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 &); @@ -115,12 +120,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) { @@ -575,7 +593,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); } @@ -593,6 +614,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 047671b09dce9079fc73af1930772587a57a0bbe Mon Sep 17 00:00:00 2001 From: Cristina Date: Fri, 19 May 2017 09:57:54 +0100 Subject: [PATCH 2/7] add the uncaught exceptions analysis to the Makefile --- src/analyses/Makefile | 1 + 1 file changed, 1 insertion(+) 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 From ca693b4de41ede4cf6019431cf3dcfd38fb71996 Mon Sep 17 00:00:00 2001 From: Cristina Date: Thu, 16 Mar 2017 14:17:08 +0000 Subject: [PATCH 3/7] Make sure that both the caller and callee have exceptional return vars before instrumenting function calls --- src/analyses/uncaught_exceptions_analysis.cpp | 5 +++-- src/goto-programs/remove_exceptions.cpp | 3 ++- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/src/analyses/uncaught_exceptions_analysis.cpp b/src/analyses/uncaught_exceptions_analysis.cpp index 75b18923c6a..6b89cfa3499 100644 --- a/src/analyses/uncaught_exceptions_analysis.cpp +++ b/src/analyses/uncaught_exceptions_analysis.cpp @@ -52,10 +52,11 @@ static void get_subtypes( candidate)!=subtypes.end()) continue; // get its base class - const irept::subt &bases=to_class_type((it->second).type).bases(); + const class_typet::basest &bases= + to_class_type((it->second).type).bases(); if(bases.size()>0) { - const irept &base = bases[0]; + const class_typet::baset &base = bases[0]; const irept &base_type=base.find(ID_type); assert(base_type.id()==ID_symbol); diff --git a/src/goto-programs/remove_exceptions.cpp b/src/goto-programs/remove_exceptions.cpp index 9ed00e661c1..22ace26d82d 100644 --- a/src/goto-programs/remove_exceptions.cpp +++ b/src/goto-programs/remove_exceptions.cpp @@ -386,7 +386,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= From f59ec9a7414969ae969ac4eb55c9290fb30f7f62 Mon Sep 17 00:00:00 2001 From: Cristina Date: Tue, 14 Mar 2017 10:54:08 +0000 Subject: [PATCH 4/7] 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 47cd9273e799563cbf66a7ede15a7ae2c71adfca Mon Sep 17 00:00:00 2001 From: Cristina Date: Wed, 24 May 2017 14:32:04 +0100 Subject: [PATCH 5/7] Ignore AssertionError This is ignored when we comoute the set of escaped exceptions as well as when replacing throws. --- src/analyses/uncaught_exceptions_analysis.cpp | 44 ++++++++++++++----- src/analyses/uncaught_exceptions_analysis.h | 4 ++ src/goto-programs/remove_exceptions.cpp | 36 +++++++++++---- 3 files changed, 66 insertions(+), 18 deletions(-) diff --git a/src/analyses/uncaught_exceptions_analysis.cpp b/src/analyses/uncaught_exceptions_analysis.cpp index 6b89cfa3499..01824f10d27 100644 --- a/src/analyses/uncaught_exceptions_analysis.cpp +++ b/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 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 subtypes; + get_subtypes(type_id, subtypes, ns); + join(subtypes); + } break; } case CATCH: diff --git a/src/analyses/uncaught_exceptions_analysis.h b/src/analyses/uncaught_exceptions_analysis.h index ff9df50fdaf..78deaaa8f3f 100644 --- a/src/analyses/uncaught_exceptions_analysis.h +++ b/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 &elements); private: diff --git a/src/goto-programs/remove_exceptions.cpp b/src/goto-programs/remove_exceptions.cpp index 22ace26d82d..14fae24a906 100644 --- a/src/goto-programs/remove_exceptions.cpp +++ b/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()), From 229817d23ce340a17046ac311d27e2387cf7625b Mon Sep 17 00:00:00 2001 From: Cristina Date: Thu, 25 May 2017 14:22:22 +0100 Subject: [PATCH 6/7] Remove duplicate version of class_hierarchyt::get_children_trans_rec --- src/analyses/uncaught_exceptions_analysis.cpp | 98 ++++++------------- src/analyses/uncaught_exceptions_analysis.h | 5 + 2 files changed, 34 insertions(+), 69 deletions(-) diff --git a/src/analyses/uncaught_exceptions_analysis.cpp b/src/analyses/uncaught_exceptions_analysis.cpp index 01824f10d27..a541d6632d1 100644 --- a/src/analyses/uncaught_exceptions_analysis.cpp +++ b/src/analyses/uncaught_exceptions_analysis.cpp @@ -5,7 +5,6 @@ Module: Over-approximating uncaught exceptions analysis Author: Cristina David \*******************************************************************/ - #ifdef DEBUG #include #endif @@ -13,70 +12,6 @@ Author: Cristina David /*******************************************************************\ -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 class_typet::basest &bases= - to_class_type((it->second).type).bases(); - if(bases.size()>0) - { - const class_typet::baset &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: @@ -144,6 +79,12 @@ void uncaught_exceptions_domaint::join( thrown.insert(elements.begin(), elements.end()); } +void uncaught_exceptions_domaint::join( + const std::vector &elements) +{ + thrown.insert(elements.begin(), elements.end()); +} + /*******************************************************************\ @@ -178,8 +119,8 @@ void uncaught_exceptions_domaint::transform( 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); + std::vector subtypes= + class_hierarchy.get_children_trans(type_id); join(subtypes); } break; @@ -199,8 +140,8 @@ void uncaught_exceptions_domaint::transform( for(const auto &exc : exception_list) { last_caught.insert(exc.id()); - std::set subtypes; - get_subtypes(exc.id(), subtypes, ns); + std::vector subtypes= + class_hierarchy.get_children_trans(exc.id()); last_caught.insert(subtypes.begin(), subtypes.end()); } } @@ -260,6 +201,24 @@ void uncaught_exceptions_domaint::get_elements( /*******************************************************************\ +Function: uncaught_exceptions_domaint::operator() + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void uncaught_exceptions_domaint::operator()( + const namespacet &ns) +{ + class_hierarchy(ns.get_symbol_table()); +} + +/*******************************************************************\ + Function: uncaught_exceptions_analysist::collect_uncaught_exceptions Inputs: @@ -350,6 +309,7 @@ void uncaught_exceptions_analysist::operator()( const namespacet &ns, exceptions_mapt &exceptions) { + domain(ns); collect_uncaught_exceptions(goto_functions, ns); exceptions=exceptions_map; output(goto_functions); diff --git a/src/analyses/uncaught_exceptions_analysis.h b/src/analyses/uncaught_exceptions_analysis.h index 78deaaa8f3f..b7691fc8150 100644 --- a/src/analyses/uncaught_exceptions_analysis.h +++ b/src/analyses/uncaught_exceptions_analysis.h @@ -13,6 +13,7 @@ Author: Cristina David #include #include #include +#include /*******************************************************************\ @@ -34,6 +35,7 @@ class uncaught_exceptions_domaint void join(const irep_idt &); void join(const std::set &); + void join(const std::vector &); void make_top() { @@ -47,10 +49,13 @@ class uncaught_exceptions_domaint void get_elements(std::set &elements); + void operator()(const namespacet &ns); + private: typedef std::vector> stack_caughtt; stack_caughtt stack_caught; std::set thrown; + class_hierarchyt class_hierarchy; }; /*******************************************************************\ From f42cc33e42b472c7825a5edf95d92c5b140985de Mon Sep 17 00:00:00 2001 From: Cristina Date: Thu, 25 May 2017 14:36:21 +0100 Subject: [PATCH 7/7] Addressed reviewers comments --- src/analyses/uncaught_exceptions_analysis.cpp | 60 +++++++------ src/analyses/uncaught_exceptions_analysis.h | 4 +- src/goto-programs/remove_exceptions.cpp | 86 +++++++++---------- 3 files changed, 71 insertions(+), 79 deletions(-) diff --git a/src/analyses/uncaught_exceptions_analysis.cpp b/src/analyses/uncaught_exceptions_analysis.cpp index a541d6632d1..814fcaf3730 100644 --- a/src/analyses/uncaught_exceptions_analysis.cpp +++ b/src/analyses/uncaught_exceptions_analysis.cpp @@ -5,6 +5,7 @@ Module: Over-approximating uncaught exceptions analysis Author: Cristina David \*******************************************************************/ + #ifdef DEBUG #include #endif @@ -12,7 +13,7 @@ Author: Cristina David /*******************************************************************\ -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::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 &elements) +const std::set &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 elements; - domain.get_elements(elements); - change=change|| - exceptions_map[current_function->first].size()!=elements.size(); - exceptions_map[current_function->first]=elements; + const std::set &elements=domain.get_elements(); + if(exceptions_map[current_function->first].size()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 \*******************************************************************/ diff --git a/src/analyses/uncaught_exceptions_analysis.h b/src/analyses/uncaught_exceptions_analysis.h index b7691fc8150..50ed75b202c 100644 --- a/src/analyses/uncaught_exceptions_analysis.h +++ b/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 &elements); + const std::set &get_elements() const; void operator()(const namespacet &ns); diff --git a/src/goto-programs/remove_exceptions.cpp b/src/goto-programs/remove_exceptions.cpp index 14fae24a906..de2ab742c07 100644 --- a/src/goto-programs/remove_exceptions.cpp +++ b/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);