29 typedef std::vector<std::pair<
46 const goto_functionst::function_mapt::iterator &);
49 const goto_functionst::function_mapt::iterator &,
50 const goto_programt::instructionst::iterator &);
53 const goto_functionst::function_mapt::iterator &,
54 const goto_programt::instructionst::iterator &,
56 std::vector<exprt> &);
59 const goto_functionst::function_mapt::iterator &,
60 const goto_programt::instructionst::iterator &,
62 std::vector<exprt> &);
65 const goto_functionst::function_mapt::iterator &);
71 const goto_functionst::function_mapt::iterator &func_it)
73 const irep_idt &function_id=func_it->first;
80 if(function_symbol.mode!=ID_java)
83 if(goto_program.
empty())
90 bool add_exceptional_var=
false;
92 if(instr_it->is_throw() || instr_it->is_function_call())
94 add_exceptional_var=
true;
98 if(add_exceptional_var)
101 symbol_tablet::symbolst::iterator s_it=
108 new_symbol.module=function_symbol.module;
111 new_symbol.mode=function_symbol.mode;
120 t_null->make_assignment();
121 t_null->source_location=
126 t_null->function=function_id;
133 const goto_functionst::function_mapt::iterator &func_it,
134 const goto_programt::instructionst::iterator &instr_it)
136 const irep_idt &function_id=func_it->first;
139 assert(instr_it->type==
CATCH && instr_it->code.has_operands());
142 const exprt &exception=instr_it->code.
op0();
146 const symbolt &function_symbol=
154 t_null->make_assignment();
155 t_null->source_location=instr_it->source_location;
159 t_null->function=instr_it->function;
165 t_exc->make_assignment();
166 t_exc->source_location=instr_it->source_location;
170 t_exc->function=instr_it->function;
172 instr_it->make_skip();
178 const goto_functionst::function_mapt::iterator &func_it,
179 const goto_programt::instructionst::iterator &instr_it,
181 std::vector<exprt> &locals)
183 assert(instr_it->type==
THROW);
186 const irep_idt &function_id=func_it->first;
188 assert(instr_it->code.operands().size()==1);
192 if(end_function!=instr_it)
197 t_end->make_goto(end_function);
198 t_end->source_location=instr_it->source_location;
199 t_end->function=instr_it->function;
210 for(std::size_t i=stack_catch.size(); i-->0;)
212 for(std::size_t j=stack_catch[i].size(); j-->0;)
215 stack_catch[i][j].second;
219 t_exc->make_goto(new_state_pc);
220 t_exc->source_location=instr_it->source_location;
221 t_exc->function=instr_it->function;
233 for(
const auto &local : locals)
238 t_dead->source_location=instr_it->source_location;
239 t_dead->function=instr_it->function;
243 exprt exc_expr=instr_it->code;
245 exc_expr=exc_expr.
op0();
252 instr_it->code=assignment;
258 const goto_functionst::function_mapt::iterator &func_it,
259 const goto_programt::instructionst::iterator &instr_it,
261 std::vector<exprt> &locals)
266 const irep_idt &function_id=func_it->first;
269 goto_programt::instructionst::iterator next_it=instr_it;
273 assert(function_call.
function().
id()==ID_symbol);
280 const symbolt &callee_exc_symbol=
286 if(end_function!=instr_it)
291 t_end->make_goto(end_function);
292 t_end->source_location=instr_it->source_location;
293 t_end->function=instr_it->function;
296 for(std::size_t i=stack_catch.size(); i-->0;)
298 for(std::size_t j=stack_catch[i].size(); j-->0;)
301 new_state_pc=stack_catch[i][j].second;
303 t_exc->make_goto(new_state_pc);
304 t_exc->source_location=instr_it->source_location;
305 t_exc->function=instr_it->function;
313 t_exc->guard=check_instanceof;
318 for(
const auto &local : locals)
323 t_dead->source_location=instr_it->source_location;
324 t_dead->function=instr_it->function;
332 t_null->make_goto(next_it);
333 t_null->source_location=instr_it->source_location;
334 t_null->function=instr_it->function;
335 t_null->guard=eq_null;
344 t->make_assignment();
345 t->source_location=instr_it->source_location;
347 t->function=instr_it->function;
355 const goto_functionst::function_mapt::iterator &func_it)
358 std::vector<std::vector<exprt>> stack_locals;
359 std::vector<exprt> locals;
362 if(goto_program.
empty())
366 if(instr_it->is_decl())
369 locals.push_back(decl.
symbol());
372 else if(instr_it->type==
CATCH && !instr_it->code.has_operands())
374 if(instr_it->targets.empty())
377 if(!stack_locals.empty())
379 locals=stack_locals.back();
380 stack_locals.pop_back();
383 if(!stack_catch.empty())
385 stack_catch.pop_back();
390 std::cout <<
"Remove exceptions: empty stack\n";
396 stack_locals.push_back(locals);
400 stack_catch.push_back(exception);
406 instr_it->code.find(ID_exception_list).get_sub();
407 assert(exception_list.size()==instr_it->targets.size());
411 for(
auto target : instr_it->targets)
413 last_exception.push_back(
414 std::make_pair(exception_list[i].
id(), target));
418 instr_it->make_skip();
421 else if(instr_it->type==
CATCH && instr_it->code.has_operands())
425 else if(instr_it->type==
THROW)
const code_declt & to_code_decl(const codet &code)
symbolt & lookup(const irep_idt &identifier)
Find a symbol in the symbol table.
const std::string & id2string(const irep_idt &d)
pointer_typet pointer_type(const typet &subtype)
Remove function exceptional returns.
symbol_tablet & symbol_table
std::vector< irept > subt
instructionst instructions
The list of instructions in the goto program.
The null pointer constant.
An expression denoting a type.
bool empty() const
Is the program empty?
symbol_tablet symbol_table
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
void remove_exceptions(symbol_tablet &symbol_table, goto_functionst &goto_functions)
removes throws/CATCH-POP/CATCH-PUSH
void instrument_exception_handler(const goto_functionst::function_mapt::iterator &, const goto_programt::instructionst::iterator &)
at the beginning of each handler in function f adds exc=f::exception_value; f::exception_value=NULL; ...
const irep_idt & id() const
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
A reference into the symbol table.
A declaration of a local variable.
void instrument_exceptions(const goto_functionst::function_mapt::iterator &)
instruments throws, function calls that may escape exceptions and exception handlers.
API to expression classes.
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
void operator()(goto_functionst &goto_functions)
remove_exceptionst(symbol_tablet &_symbol_table)
targett insert_after(const_targett target)
Insertion after the given target.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
bool has_operands() const
std::vector< std::pair< irep_idt, goto_programt::targett > > catch_handlerst
targett insert_before(const_targett target)
Insertion before the given target.
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
void instrument_throw(const goto_functionst::function_mapt::iterator &, const goto_programt::instructionst::iterator &, const stack_catcht &, std::vector< exprt > &)
instruments each throw with conditional GOTOS to the corresponding exception handlers ...
Base class for all expressions.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
#define Forall_goto_functions(it, functions)
void add_exceptional_returns(const goto_functionst::function_mapt::iterator &)
adds exceptional return variables for every function that may escape exceptions
A removal of a local variable.
bool has_symbol(const irep_idt &name) const
#define Forall_goto_program_instructions(it, program)
Expression to hold a symbol (variable)
A generic base class for expressions that are predicates, i.e., boolean-typed, and that take exactly ...
#define forall_goto_program_instructions(it, program)
void instrument_function_call(const goto_functionst::function_mapt::iterator &, const goto_programt::instructionst::iterator &, const stack_catcht &, std::vector< exprt > &)
instruments each function call that may escape exceptions with conditional GOTOS to the corresponding...
goto_functionst goto_functions
std::vector< catch_handlerst > stack_catcht
const code_function_callt & to_code_function_call(const codet &code)
instructionst::iterator targett
targett get_end_function()