81 typedef std::vector<std::pair<
121 std::size_t &universal_try,
122 std::size_t &universal_catch);
128 const std::vector<exprt> &locals);
134 const std::vector<exprt> &);
140 const std::vector<exprt> &);
150 const symbolt *existing_symbol =
153 existing_symbol !=
nullptr,
154 "Java frontend should have created @inflight_exception variable");
168 if(instr_it->is_throw())
173 if(instr_it->is_function_call())
175 const exprt &function_expr=
178 function_expr.
id()==ID_symbol,
179 "identifier expected to be a symbol");
210 const exprt &thrown_exception_local=
220 t_null->make_assignment();
221 t_null->source_location=instr_it->source_location;
223 thrown_global_symbol,
225 t_null->function=instr_it->function;
229 t_exc->make_assignment();
230 t_exc->source_location=instr_it->source_location;
232 thrown_exception_local,
234 t_exc->function=instr_it->function;
236 instr_it->make_skip();
263 std::size_t &universal_try,
264 std::size_t &universal_catch)
266 for(std::size_t i=stack_catch.size(); i>0;)
269 for(std::size_t j=0; j<stack_catch[i].size(); ++j)
271 if(stack_catch[i][j].first.empty())
280 return stack_catch[i][j].second;
301 const std::vector<exprt> &locals)
311 std::size_t default_try=0;
312 std::size_t default_catch=(!stack_catch.empty()) ? stack_catch[0].size() : 0;
316 default_try, default_catch);
324 for(std::size_t i=default_try; i<stack_catch.size(); i++)
326 for(std::size_t j=(i==default_try) ? default_catch : stack_catch[i].size();
331 stack_catch[i][j].second;
332 if(!stack_catch[i][j].first.empty())
336 t_exc->make_goto(new_state_pc);
337 t_exc->source_location=instr_it->source_location;
338 t_exc->function=instr_it->function;
353 default_dispatch->make_goto(default_target);
354 default_dispatch->source_location=instr_it->source_location;
355 default_dispatch->function=instr_it->function;
358 for(
const auto &local : locals)
363 t_dead->source_location=instr_it->source_location;
364 t_dead->function=instr_it->function;
374 const std::vector<exprt> &locals)
378 const exprt &exc_expr=
394 instr_it->code=assignment;
405 const std::vector<exprt> &locals)
416 "identified expected to be a symbol");
431 assume_null->make_assumption(no_exception_currently_in_flight);
440 t_null->make_goto(next_it);
441 t_null->source_location=instr_it->source_location;
442 t_null->function=instr_it->function;
443 t_null->guard=no_exception_currently_in_flight;
459 std::vector<std::vector<exprt>> stack_locals;
460 std::vector<exprt> locals;
465 bool program_or_callees_may_throw =
468 bool did_something =
false;
472 if(instr_it->is_decl())
475 locals.push_back(decl.
symbol());
478 else if(instr_it->type==
CATCH)
480 const irep_idt &statement=instr_it->code.get_statement();
482 if(statement==ID_exception_landingpad)
488 else if(statement==ID_pop_catch)
491 if(!stack_locals.empty())
493 locals=stack_locals.back();
494 stack_locals.pop_back();
497 if(!stack_catch.empty())
499 stack_catch.pop_back();
504 std::cout <<
"Remove exceptions: empty stack\n";
509 else if(statement==ID_push_catch)
511 stack_locals.push_back(locals);
515 stack_catch.push_back(exception);
527 instr_it->targets.empty() ||
528 exception_list.size()==instr_it->targets.size(),
529 "`exception_list` should contain current instruction's targets");
533 for(
auto target : instr_it->targets)
535 last_exception.push_back(
536 std::make_pair(exception_list[i].
get_tag(), target));
544 "CATCH opcode should be one of push-catch, pop-catch, landingpad");
546 instr_it->make_skip();
547 did_something =
true;
549 else if(instr_it->type==
THROW)
584 std::map<irep_idt, std::set<irep_idt>> exceptions_map;
587 [&exceptions_map](
const irep_idt &id) {
588 return !exceptions_map[id].empty();
619 [](
const irep_idt &) {
return true; };
623 any_function_may_throw,
const code_declt & to_code_decl(const codet &code)
std::vector< exception_list_entryt > exception_listt
symbol_exprt get_inflight_exception_global()
Create a global named java::@inflight_exception that holds any exception that has been thrown but not...
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
pointer_typet pointer_type(const typet &subtype)
void instrument_exceptions(goto_programt &goto_program)
instruments throws, function calls that may escape exceptions and exception handlers.
#define INFLIGHT_EXCEPTION_VARIABLE_NAME
Remove function exceptional returns.
Over-approximative uncaught exceptions analysis.
Remove Instance-of Operators.
irep_idt get_tag(const typet &type)
const irep_idt & get_identifier() const
The null pointer constant.
An expression denoting a type.
function_may_throwt function_may_throw
symbol_tablet symbol_table
Symbol table.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
message_handlert & message_handler
bool function_or_callees_may_throw(const goto_programt &) const
Checks whether a function may ever experience an exception (whether or not it catches), either by throwing one itself, or by calling a function that exceptions escape from.
bool get_bool(const irep_namet &name) const
#define INVARIANT(CONDITION, REASON)
const irep_idt & id() const
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
void add_exception_dispatch_sequence(goto_programt &goto_program, const goto_programt::targett &instr_it, const stack_catcht &stack_catch, const std::vector< exprt > &locals)
Emit the code: if (exception instanceof ExnA) then goto handlerA else if (exception instanceof ExnB) ...
A reference into the symbol table.
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 ...
instructionst::iterator targett
A declaration of a local variable.
static code_push_catcht & to_code_push_catch(codet &code)
void remove_exceptions(symbol_table_baset &symbol_table, goto_functionst &goto_functions, message_handlert &message_handler, remove_exceptions_typest type)
removes throws/CATCH-POP/CATCH-PUSH
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.
API to expression classes.
bool remove_added_instanceof
#define PRECONDITION(CONDITION)
targett insert_after(const_targett target)
Insertion after the given target.
bool instrument_throw(goto_programt &goto_program, const goto_programt::targett &, const stack_catcht &, const std::vector< exprt > &)
instruments each throw with conditional GOTOS to the corresponding exception handlers ...
void operator()(goto_functionst &goto_functions)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
static exprt get_exception_symbol(const exprt &exor)
Returns the symbol corresponding to an exception.
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...
Lowers high-level exception descriptions into low-level operations suitable for symex and other analy...
std::vector< std::pair< irep_idt, goto_programt::targett > > catch_handlerst
A generic container class for the GOTO intermediate representation of one function.
void remove_instanceof(goto_programt::targett target, goto_programt &goto_program, symbol_table_baset &symbol_table, message_handlert &message_handler)
Replace an instanceof in the expression or guard of the passed instruction of the given function body...
typet type
Type of symbol.
static code_landingpadt & to_code_landingpad(codet &code)
symbol_table_baset & symbol_table
std::function< bool(const irep_idt &)> function_may_throwt
Base class for all expressions.
targett get_end_function()
The symbol table base class interface.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
bool instrument_function_call(goto_programt &goto_program, const goto_programt::targett &, const stack_catcht &, const std::vector< exprt > &)
instruments each function call that may escape exceptions with conditional GOTOS to the corresponding...
#define Forall_goto_functions(it, functions)
bool empty() const
Is the program empty?
A removal of a local variable.
goto_programt & goto_program
#define Forall_goto_program_instructions(it, program)
Expression to hold a symbol (variable)
const exprt & catch_expr() const
goto_programt coverage_criteriont message_handlert & message_handler
A generic base class for expressions that are predicates, i.e., boolean-typed, and that take exactly ...
remove_exceptionst(symbol_table_baset &_symbol_table, function_may_throwt _function_may_throw, bool remove_added_instanceof, message_handlert &message_handler)
#define DATA_INVARIANT(CONDITION, REASON)
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
#define forall_goto_program_instructions(it, program)
exception_listt & exception_list()
goto_functionst goto_functions
GOTO functions.
std::vector< catch_handlerst > stack_catcht
const code_function_callt & to_code_function_call(const codet &code)