Go to the documentation of this file.
86 typedef std::vector<std::pair<
97 bool _remove_added_instanceof,
109 "remove_exceptions needs a class hierarchy to remove instanceof "
110 "statements (either supply one, or don't use REMOVE_ADDED_INSTANCEOF)");
144 std::size_t &universal_try,
145 std::size_t &universal_catch);
148 const irep_idt &function_identifier,
152 const std::vector<symbol_exprt> &locals);
155 const irep_idt &function_identifier,
159 const std::vector<symbol_exprt> &);
162 const irep_idt &function_identifier,
166 const std::vector<symbol_exprt> &);
169 const irep_idt &function_identifier,
177 const symbolt *existing_symbol =
180 existing_symbol !=
nullptr,
181 "Java frontend should have created @inflight_exception variable");
195 if(instr_it->is_throw())
200 if(instr_it->is_function_call())
202 const exprt &function_expr=
205 function_expr.
id()==ID_symbol,
206 "identifier expected to be a symbol");
237 const exprt &thrown_exception_local=
257 thrown_exception_local,
262 instr_it->turn_into_skip();
289 std::size_t &universal_try,
290 std::size_t &universal_catch)
292 for(std::size_t i=stack_catch.size(); i>0;)
295 for(std::size_t j=0; j<stack_catch[i].size(); ++j)
297 if(stack_catch[i][j].first.empty())
306 return stack_catch[i][j].second;
325 const irep_idt &function_identifier,
329 const std::vector<symbol_exprt> &locals)
339 std::size_t default_try=0;
340 std::size_t default_catch=(!stack_catch.empty()) ? stack_catch[0].size() : 0;
344 default_try, default_catch);
352 for(std::size_t i=default_try; i<stack_catch.size(); i++)
354 for(std::size_t j=(i==default_try) ? default_catch : stack_catch[i].size();
359 stack_catch[i][j].second;
360 if(!stack_catch[i][j].first.empty())
392 for(
const auto &local : locals)
402 const irep_idt &function_identifier,
406 const std::vector<symbol_exprt> &locals)
410 const exprt &exc_expr=
414 function_identifier, goto_program, instr_it, stack_catch, locals);
426 instr_it->code=assignment;
435 const irep_idt &function_identifier,
439 const std::vector<symbol_exprt> &locals)
451 "identified expected to be a symbol");
474 function_identifier, goto_program, instr_it, stack_catch, locals);
481 no_exception_currently_in_flight,
495 const irep_idt &function_identifier,
499 std::vector<std::vector<symbol_exprt>> stack_locals;
500 std::vector<symbol_exprt> locals;
502 if(goto_program.
empty())
505 bool program_or_callees_may_throw =
508 bool did_something =
false;
509 bool added_goto_instruction =
false;
513 if(instr_it->is_decl())
516 locals.push_back(decl.
symbol());
519 else if(instr_it->type==
CATCH)
521 const irep_idt &statement=instr_it->code.get_statement();
523 if(statement==ID_exception_landingpad)
526 goto_program, instr_it, program_or_callees_may_throw);
529 else if(statement==ID_pop_catch)
532 if(!stack_locals.empty())
534 locals=stack_locals.back();
535 stack_locals.pop_back();
538 if(!stack_catch.empty())
540 stack_catch.pop_back();
545 std::cout <<
"Remove exceptions: empty stack\n";
550 else if(statement==ID_push_catch)
552 stack_locals.push_back(locals);
556 stack_catch.push_back(exception);
568 instr_it->targets.empty() ||
569 exception_list.size()==instr_it->targets.size(),
570 "`exception_list` should contain current instruction's targets");
574 for(
auto target : instr_it->targets)
576 last_exception.push_back(
577 std::make_pair(exception_list[i].
get_tag(), target));
585 "CATCH opcode should be one of push-catch, pop-catch, landingpad");
588 instr_it->turn_into_skip();
589 did_something =
true;
591 else if(instr_it->type==
THROW)
594 function_identifier, goto_program, instr_it, stack_catch, locals);
600 function_identifier, goto_program, instr_it, stack_catch, locals);
602 added_goto_instruction =
639 std::map<irep_idt, std::set<irep_idt>> exceptions_map;
644 [&exceptions_map](
const irep_idt &id) {
645 return !exceptions_map[id].empty();
649 symbol_table,
nullptr, function_may_throw,
false, message_handler);
667 const irep_idt &function_identifier,
673 [](
const irep_idt &) {
return true; };
676 symbol_table,
nullptr, any_function_may_throw,
false, message_handler);
704 std::map<irep_idt, std::set<irep_idt>> exceptions_map;
709 [&exceptions_map](
const irep_idt &id) {
710 return !exceptions_map[id].empty();
714 symbol_table, &class_hierarchy, function_may_throw,
true, message_handler);
734 const irep_idt &function_identifier,
741 [](
const irep_idt &) {
return true; };
746 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.
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)
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
void remove_exceptions_using_instanceof(symbol_table_baset &symbol_table, goto_functionst &goto_functions, message_handlert &message_handler)
removes throws/CATCH-POP/CATCH-PUSH
std::vector< catch_handlerst > stack_catcht
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
@ ADDED_CODE_WITH_MAY_THROW
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.
bool instrument_throw(const irep_idt &function_identifier, 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
Java-specific exprt subclasses.
const class_hierarchyt * class_hierarchy
Expression to hold a symbol (variable)
@ ADDED_CODE_WITHOUT_MAY_THROW
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
void remove_instanceof(const irep_idt &function_identifier, 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...
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
void add_exception_dispatch_sequence(const irep_idt &function_identifier, 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) ...
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
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....
#define PRECONDITION(CONDITION)
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
#define INITIALIZE_FUNCTION
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)
const exprt & catch_expr() const
#define Forall_goto_functions(it, functions)
Remove function exceptional returns.
static exprt get_exception_symbol(const exprt &exor)
Returns the symbol corresponding to an exception.
Remove Instance-of Operators.
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 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.
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
Over-approximative uncaught exceptions analysis.
instrumentation_resultt instrument_function_call(const irep_idt &function_identifier, 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
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
std::function< bool(const irep_idt &)> function_may_throwt
Semantic type conversion.
empty_typet java_void_type()
A codet representing an assignment in the program.
The Boolean constant true.
symbol_exprt get_inflight_exception_global()
Create a global named java::@inflight_exception that holds any exception that has been thrown but not...
API to expression classes.
message_handlert & message_handler
const source_locationt & source_location() const
symbol_tablet symbol_table
Symbol table.
void instrument_exceptions(const irep_idt &function_identifier, 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)