Go to the documentation of this file.
81 typedef std::vector<std::pair<
92 bool _remove_added_instanceof,
104 "remove_exceptions needs a class hierarchy to remove instanceof "
105 "statements (either supply one, or don't use REMOVE_ADDED_INSTANCEOF)");
131 std::size_t &universal_try,
132 std::size_t &universal_catch);
138 const std::vector<symbol_exprt> &locals);
144 const std::vector<symbol_exprt> &);
150 const std::vector<symbol_exprt> &);
160 const symbolt *existing_symbol =
163 existing_symbol !=
nullptr,
164 "Java frontend should have created @inflight_exception variable");
178 if(instr_it->is_throw())
183 if(instr_it->is_function_call())
185 const exprt &function_expr=
188 function_expr.
id()==ID_symbol,
189 "identifier expected to be a symbol");
220 const exprt &thrown_exception_local=
230 t_null->make_assignment();
231 t_null->source_location=instr_it->source_location;
233 thrown_global_symbol,
235 t_null->function=instr_it->function;
239 t_exc->make_assignment();
240 t_exc->source_location=instr_it->source_location;
242 thrown_exception_local,
244 t_exc->function=instr_it->function;
246 instr_it->make_skip();
273 std::size_t &universal_try,
274 std::size_t &universal_catch)
276 for(std::size_t i=stack_catch.size(); i>0;)
279 for(std::size_t j=0; j<stack_catch[i].size(); ++j)
281 if(stack_catch[i][j].first.empty())
290 return stack_catch[i][j].second;
311 const std::vector<symbol_exprt> &locals)
321 std::size_t default_try=0;
322 std::size_t default_catch=(!stack_catch.empty()) ? stack_catch[0].size() : 0;
326 default_try, default_catch);
334 for(std::size_t i=default_try; i<stack_catch.size(); i++)
336 for(std::size_t j=(i==default_try) ? default_catch : stack_catch[i].size();
341 stack_catch[i][j].second;
342 if(!stack_catch[i][j].first.empty())
346 t_exc->make_goto(new_state_pc);
347 t_exc->source_location=instr_it->source_location;
348 t_exc->function=instr_it->function;
370 default_dispatch->make_goto(default_target);
371 default_dispatch->source_location=instr_it->source_location;
372 default_dispatch->function=instr_it->function;
375 for(
const auto &local : locals)
380 t_dead->source_location=instr_it->source_location;
381 t_dead->function=instr_it->function;
391 const std::vector<symbol_exprt> &locals)
395 const exprt &exc_expr=
399 goto_program, instr_it, stack_catch, locals);
411 instr_it->code=assignment;
422 const std::vector<symbol_exprt> &locals)
433 "identified expected to be a symbol");
448 assume_null->make_assumption(no_exception_currently_in_flight);
453 goto_program, instr_it, stack_catch, locals);
457 t_null->make_goto(next_it);
458 t_null->source_location=instr_it->source_location;
459 t_null->function=instr_it->function;
460 t_null->guard=no_exception_currently_in_flight;
476 std::vector<std::vector<symbol_exprt>> stack_locals;
477 std::vector<symbol_exprt> locals;
479 if(goto_program.
empty())
482 bool program_or_callees_may_throw =
485 bool did_something =
false;
489 if(instr_it->is_decl())
492 locals.push_back(decl.
symbol());
495 else if(instr_it->type==
CATCH)
497 const irep_idt &statement=instr_it->code.get_statement();
499 if(statement==ID_exception_landingpad)
502 goto_program, instr_it, program_or_callees_may_throw);
505 else if(statement==ID_pop_catch)
508 if(!stack_locals.empty())
510 locals=stack_locals.back();
511 stack_locals.pop_back();
514 if(!stack_catch.empty())
516 stack_catch.pop_back();
521 std::cout <<
"Remove exceptions: empty stack\n";
526 else if(statement==ID_push_catch)
528 stack_locals.push_back(locals);
532 stack_catch.push_back(exception);
544 instr_it->targets.empty() ||
545 exception_list.size()==instr_it->targets.size(),
546 "`exception_list` should contain current instruction's targets");
550 for(
auto target : instr_it->targets)
552 last_exception.push_back(
553 std::make_pair(exception_list[i].
get_tag(), target));
561 "CATCH opcode should be one of push-catch, pop-catch, landingpad");
563 instr_it->make_skip();
564 did_something =
true;
566 else if(instr_it->type==
THROW)
600 std::map<irep_idt, std::set<irep_idt>> exceptions_map;
605 [&exceptions_map](
const irep_idt &id) {
606 return !exceptions_map[id].empty();
610 symbol_table,
nullptr, function_may_throw,
false, message_handler);
632 [](
const irep_idt &) {
return true; };
635 symbol_table,
nullptr, any_function_may_throw,
false, message_handler);
663 std::map<irep_idt, std::set<irep_idt>> exceptions_map;
668 [&exceptions_map](
const irep_idt &id) {
669 return !exceptions_map[id].empty();
673 symbol_table, &class_hierarchy, function_may_throw,
true, message_handler);
698 [](
const irep_idt &) {
return true; };
703 any_function_may_throw,
#define Forall_goto_program_instructions(it, program)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
#define PRECONDITION(CONDITION)
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Non-graph-based representation of the class hierarchy.
remove_exceptionst(symbol_table_baset &_symbol_table, const class_hierarchyt *_class_hierarchy, function_may_throwt _function_may_throw, bool _remove_added_instanceof, message_handlert &_message_handler)
void remove_exceptions_using_instanceof(symbol_table_baset &symbol_table, goto_functionst &goto_functions, message_handlert &message_handler)
removes throws/CATCH-POP/CATCH-PUSH
const code_declt & to_code_decl(const codet &code)
std::vector< catch_handlerst > stack_catcht
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
bool instrument_throw(goto_programt &goto_program, const goto_programt::targett &, const stack_catcht &, const std::vector< symbol_exprt > &)
instruments each throw with conditional GOTOS to the corresponding exception handlers
void add_exception_dispatch_sequence(goto_programt &goto_program, const goto_programt::targett &instr_it, const stack_catcht &stack_catch, const std::vector< symbol_exprt > &locals)
Emit the code: if (exception instanceof ExnA) then goto handlerA else if (exception instanceof ExnB) ...
bool function_or_callees_may_throw(const goto_programt &) const
Checks whether a function may ever experience an exception (whether or not it catches),...
typet type
Type of symbol.
bool remove_added_instanceof
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
A codet representing the declaration of a local variable.
void operator()(goto_functionst &goto_functions)
bool empty() const
Is the program empty?
Base class for all expressions.
A struct tag type, i.e., struct_typet with an identifier.
const class_hierarchyt * class_hierarchy
Expression to hold a symbol (variable)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
typet & type()
Return the type of the expression.
codet representation of a function call statement.
bool get_bool(const irep_namet &name) const
The null pointer constant.
void remove_exceptions(symbol_table_baset &symbol_table, goto_functionst &goto_functions, const class_hierarchyt &class_hierarchy, message_handlert &message_handler)
removes throws/CATCH-POP/CATCH-PUSH
goto_programt::targett find_universal_exception(const remove_exceptionst::stack_catcht &stack_catch, goto_programt &goto_program, std::size_t &universal_try, std::size_t &universal_catch)
Find the innermost universal exception handler for the current program location which may throw (i....
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
const irep_idt & get_identifier() const
The symbol table base class interface.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
#define INFLIGHT_EXCEPTION_VARIABLE_NAME
exception_listt & exception_list()
pointer_typet pointer_type(const typet &subtype)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
function_may_throwt function_may_throw
const irep_idt & id() const
const code_function_callt & to_code_function_call(const codet &code)
A codet representing the removal of a local variable going out of scope.
const exprt & catch_expr() const
#define Forall_goto_functions(it, functions)
static exprt get_exception_symbol(const exprt &exor)
Returns the symbol corresponding to an exception.
targett get_end_function()
Get an instruction iterator pointing to the END_FUNCTION instruction of the goto program.
A collection of goto functions.
std::vector< std::pair< irep_idt, goto_programt::targett > > catch_handlerst
void remove_instanceof(goto_programt::targett target, goto_programt &goto_program, symbol_table_baset &symbol_table, const class_hierarchyt &class_hierarchy, message_handlert &message_handler)
Replace an instanceof in the expression or guard of the passed instruction of the given function body...
void uncaught_exceptions(const goto_functionst &goto_functions, const namespacet &ns, std::map< irep_idt, std::set< irep_idt >> &exceptions_map)
Applies the uncaught exceptions analysis and outputs the result.
An expression denoting a type.
static code_landingpadt & to_code_landingpad(codet &code)
goto_functionst goto_functions
GOTO functions.
void instrument_exception_handler(goto_programt &goto_program, const goto_programt::targett &, bool may_catch)
Translates an exception landing-pad into instructions that copy the in-flight exception pointer to a ...
std::vector< exception_list_entryt > exception_listt
bool instrument_function_call(goto_programt &goto_program, const goto_programt::targett &, const stack_catcht &, const std::vector< symbol_exprt > &)
instruments each function call that may escape exceptions with conditional GOTOS to the corresponding...
A generic container class for the GOTO intermediate representation of one function.
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
symbol_table_baset & symbol_table
std::function< bool(const irep_idt &)> function_may_throwt
Semantic type conversion.
A codet representing an assignment in the program.
symbol_exprt get_inflight_exception_global()
Create a global named java::@inflight_exception that holds any exception that has been thrown but not...
message_handlert & message_handler
symbol_tablet symbol_table
Symbol table.
void instrument_exceptions(goto_programt &goto_program)
instruments throws, function calls that may escape exceptions and exception handlers.
instructionst::iterator targett
#define forall_goto_program_instructions(it, program)
Lowers high-level exception descriptions into low-level operations suitable for symex and other analy...
static code_push_catcht & to_code_push_catch(codet &code)
static irep_idt get_tag(const typet &type)