81 typedef std::vector<std::pair<
118 std::size_t &universal_try,
119 std::size_t &universal_catch);
125 const std::vector<exprt> &locals);
131 const std::vector<exprt> &);
137 const std::vector<exprt> &);
147 const symbolt *existing_symbol =
150 existing_symbol !=
nullptr,
151 "Java frontend should have created @inflight_exception variable");
165 if(instr_it->is_throw())
170 if(instr_it->is_function_call())
172 const exprt &function_expr=
175 function_expr.
id()==ID_symbol,
176 "identifier expected to be a symbol");
207 const exprt &thrown_exception_local=
217 t_null->make_assignment();
218 t_null->source_location=instr_it->source_location;
220 thrown_global_symbol,
222 t_null->function=instr_it->function;
226 t_exc->make_assignment();
227 t_exc->source_location=instr_it->source_location;
229 thrown_exception_local,
231 t_exc->function=instr_it->function;
233 instr_it->make_skip();
260 std::size_t &universal_try,
261 std::size_t &universal_catch)
263 for(std::size_t i=stack_catch.size(); i>0;)
266 for(std::size_t j=0; j<stack_catch[i].size(); ++j)
268 if(stack_catch[i][j].first.empty())
277 return stack_catch[i][j].second;
298 const std::vector<exprt> &locals)
308 std::size_t default_try=0;
309 std::size_t default_catch=(!stack_catch.empty()) ? stack_catch[0].size() : 0;
313 default_try, default_catch);
321 for(std::size_t i=default_try; i<stack_catch.size(); i++)
323 for(std::size_t j=(i==default_try) ? default_catch : stack_catch[i].size();
328 stack_catch[i][j].second;
329 if(!stack_catch[i][j].first.empty())
333 t_exc->make_goto(new_state_pc);
334 t_exc->source_location=instr_it->source_location;
335 t_exc->function=instr_it->function;
350 default_dispatch->make_goto(default_target);
351 default_dispatch->source_location=instr_it->source_location;
352 default_dispatch->function=instr_it->function;
355 for(
const auto &local : locals)
360 t_dead->source_location=instr_it->source_location;
361 t_dead->function=instr_it->function;
371 const std::vector<exprt> &locals)
375 const exprt &exc_expr=
391 instr_it->code=assignment;
402 const std::vector<exprt> &locals)
413 "identified expected to be a symbol");
428 assume_null->make_assumption(no_exception_currently_in_flight);
437 t_null->make_goto(next_it);
438 t_null->source_location=instr_it->source_location;
439 t_null->function=instr_it->function;
440 t_null->guard=no_exception_currently_in_flight;
456 std::vector<std::vector<exprt>> stack_locals;
457 std::vector<exprt> locals;
462 bool program_or_callees_may_throw =
465 bool did_something =
false;
469 if(instr_it->is_decl())
472 locals.push_back(decl.
symbol());
475 else if(instr_it->type==
CATCH)
477 const irep_idt &statement=instr_it->code.get_statement();
479 if(statement==ID_exception_landingpad)
485 else if(statement==ID_pop_catch)
488 if(!stack_locals.empty())
490 locals=stack_locals.back();
491 stack_locals.pop_back();
494 if(!stack_catch.empty())
496 stack_catch.pop_back();
501 std::cout <<
"Remove exceptions: empty stack\n";
506 else if(statement==ID_push_catch)
508 stack_locals.push_back(locals);
512 stack_catch.push_back(exception);
524 instr_it->targets.empty() ||
525 exception_list.size()==instr_it->targets.size(),
526 "`exception_list` should contain current instruction's targets");
530 for(
auto target : instr_it->targets)
532 last_exception.push_back(
533 std::make_pair(exception_list[i].
get_tag(), target));
541 "CATCH opcode should be one of push-catch, pop-catch, landingpad");
543 instr_it->make_skip();
544 did_something =
true;
546 else if(instr_it->type==
THROW)
580 std::map<irep_idt, std::set<irep_idt>> exceptions_map;
583 [&exceptions_map](
const irep_idt &id) {
584 return !exceptions_map[id].empty();
612 [](
const irep_idt &id) {
return true; };
616 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)
remove_exceptionst(symbol_table_baset &_symbol_table, function_may_throwt _function_may_throw, bool remove_added_instanceof)
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...
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
void remove_instanceof(goto_programt::targett target, goto_programt &goto_program, symbol_table_baset &symbol_table)
Replace an instanceof in the expression or guard of the passed instruction of the given function body...
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 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.
void remove_exceptions(symbol_table_baset &symbol_table, goto_functionst &goto_functions, remove_exceptions_typest type)
removes throws/CATCH-POP/CATCH-PUSH
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.
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.
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
A generic base class for expressions that are predicates, i.e., boolean-typed, and that take exactly ...
#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)