cprover
remove_exceptions.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Remove exception handling
4 
5 Author: Cristina David
6 
7 Date: December 2016
8 
9 \*******************************************************************/
10 
13 
14 #include "remove_exceptions.h"
15 
16 #ifdef DEBUG
17 #include <iostream>
18 #endif
19 
20 #include <stack>
21 #include <algorithm>
22 
23 #include <util/c_types.h>
24 #include <util/std_expr.h>
25 #include <util/symbol_table.h>
26 
28 {
29  typedef std::vector<std::pair<
31  typedef std::vector<catch_handlerst> stack_catcht;
32 
33 public:
34  explicit remove_exceptionst(symbol_tablet &_symbol_table):
35  symbol_table(_symbol_table)
36  {
37  }
38 
39  void operator()(
40  goto_functionst &goto_functions);
41 
42 protected:
44 
46  const goto_functionst::function_mapt::iterator &);
47 
49  const goto_functionst::function_mapt::iterator &,
50  const goto_programt::instructionst::iterator &);
51 
52  void instrument_throw(
53  const goto_functionst::function_mapt::iterator &,
54  const goto_programt::instructionst::iterator &,
55  const stack_catcht &,
56  std::vector<exprt> &);
57 
59  const goto_functionst::function_mapt::iterator &,
60  const goto_programt::instructionst::iterator &,
61  const stack_catcht &,
62  std::vector<exprt> &);
63 
65  const goto_functionst::function_mapt::iterator &);
66 };
67 
71  const goto_functionst::function_mapt::iterator &func_it)
72 {
73  const irep_idt &function_id=func_it->first;
74  goto_programt &goto_program=func_it->second.body;
75 
76  assert(symbol_table.has_symbol(function_id));
77  const symbolt &function_symbol=symbol_table.lookup(function_id);
78 
79  // for now only add exceptional returns for Java
80  if(function_symbol.mode!=ID_java)
81  return;
82 
83  if(goto_program.empty())
84  return;
85 
86  // We generate an exceptional return value for any function that has
87  // a throw or a function call. This can be improved by only considering
88  // function calls that may escape exceptions. However, this will
89  // require multiple passes.
90  bool add_exceptional_var=false;
91  forall_goto_program_instructions(instr_it, goto_program)
92  if(instr_it->is_throw() || instr_it->is_function_call())
93  {
94  add_exceptional_var=true;
95  break;
96  }
97 
98  if(add_exceptional_var)
99  {
100  // look up the function symbol
101  symbol_tablet::symbolst::iterator s_it=
102  symbol_table.symbols.find(function_id);
103 
104  assert(s_it!=symbol_table.symbols.end());
105 
106  auxiliary_symbolt new_symbol;
107  new_symbol.is_static_lifetime=true;
108  new_symbol.module=function_symbol.module;
109  new_symbol.base_name=id2string(function_symbol.base_name)+EXC_SUFFIX;
110  new_symbol.name=id2string(function_symbol.name)+EXC_SUFFIX;
111  new_symbol.mode=function_symbol.mode;
112  new_symbol.type=pointer_type(empty_typet());
113  symbol_table.add(new_symbol);
114 
115  // initialize the exceptional return with NULL
116  symbol_exprt lhs_expr_null=new_symbol.symbol_expr();
117  null_pointer_exprt rhs_expr_null(pointer_type(empty_typet()));
118  goto_programt::targett t_null=
119  goto_program.insert_before(goto_program.instructions.begin());
120  t_null->make_assignment();
121  t_null->source_location=
122  goto_program.instructions.begin()->source_location;
123  t_null->code=code_assignt(
124  lhs_expr_null,
125  rhs_expr_null);
126  t_null->function=function_id;
127  }
128 }
129 
133  const goto_functionst::function_mapt::iterator &func_it,
134  const goto_programt::instructionst::iterator &instr_it)
135 {
136  const irep_idt &function_id=func_it->first;
137  goto_programt &goto_program=func_it->second.body;
138 
139  assert(instr_it->type==CATCH && instr_it->code.has_operands());
140 
141  // retrieve the exception variable
142  const exprt &exception=instr_it->code.op0();
143 
144  if(symbol_table.has_symbol(id2string(function_id)+EXC_SUFFIX))
145  {
146  const symbolt &function_symbol=
147  symbol_table.lookup(id2string(function_id)+EXC_SUFFIX);
148  // next we reset the exceptional return to NULL
149  symbol_exprt lhs_expr_null=function_symbol.symbol_expr();
150  null_pointer_exprt rhs_expr_null(pointer_type(empty_typet()));
151 
152  // add the assignment
153  goto_programt::targett t_null=goto_program.insert_after(instr_it);
154  t_null->make_assignment();
155  t_null->source_location=instr_it->source_location;
156  t_null->code=code_assignt(
157  lhs_expr_null,
158  rhs_expr_null);
159  t_null->function=instr_it->function;
160 
161  // add the assignment exc=f#exception_value
162  symbol_exprt rhs_expr_exc=function_symbol.symbol_expr();
163 
164  goto_programt::targett t_exc=goto_program.insert_after(instr_it);
165  t_exc->make_assignment();
166  t_exc->source_location=instr_it->source_location;
167  t_exc->code=code_assignt(
168  typecast_exprt(exception, rhs_expr_exc.type()),
169  rhs_expr_exc);
170  t_exc->function=instr_it->function;
171  }
172  instr_it->make_skip();
173 }
174 
178  const goto_functionst::function_mapt::iterator &func_it,
179  const goto_programt::instructionst::iterator &instr_it,
180  const remove_exceptionst::stack_catcht &stack_catch,
181  std::vector<exprt> &locals)
182 {
183  assert(instr_it->type==THROW);
184 
185  goto_programt &goto_program=func_it->second.body;
186  const irep_idt &function_id=func_it->first;
187 
188  assert(instr_it->code.operands().size()==1);
189 
190  // find the end of the function
191  goto_programt::targett end_function=goto_program.get_end_function();
192  if(end_function!=instr_it)
193  {
194  // jump to the end of the function
195  // this will appear after the GOTO-based dynamic dispatch below
196  goto_programt::targett t_end=goto_program.insert_after(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;
200  }
201 
202 
203  // find the symbol corresponding to the caught exceptions
204  const symbolt &exc_symbol=
205  symbol_table.lookup(id2string(function_id)+EXC_SUFFIX);
206  symbol_exprt exc_thrown=exc_symbol.symbol_expr();
207 
208  // add GOTOs implementing the dynamic dispatch of the
209  // exception handlers
210  for(std::size_t i=stack_catch.size(); i-->0;)
211  {
212  for(std::size_t j=stack_catch[i].size(); j-->0;)
213  {
214  goto_programt::targett new_state_pc=
215  stack_catch[i][j].second;
216 
217  // find handler
218  goto_programt::targett t_exc=goto_program.insert_after(instr_it);
219  t_exc->make_goto(new_state_pc);
220  t_exc->source_location=instr_it->source_location;
221  t_exc->function=instr_it->function;
222 
223  // use instanceof to check that this is the correct handler
224  symbol_typet type(stack_catch[i][j].first);
225  type_exprt expr(type);
226 
227  binary_predicate_exprt check(exc_thrown, ID_java_instanceof, expr);
228  t_exc->guard=check;
229  }
230  }
231 
232  // add dead instructions
233  for(const auto &local : locals)
234  {
235  goto_programt::targett t_dead=goto_program.insert_after(instr_it);
236  t_dead->make_dead();
237  t_dead->code=code_deadt(local);
238  t_dead->source_location=instr_it->source_location;
239  t_dead->function=instr_it->function;
240  }
241 
242  // replace "throw x;" by "f#exception_value=x;"
243  exprt exc_expr=instr_it->code;
244  while(exc_expr.id()!=ID_symbol && exc_expr.has_operands())
245  exc_expr=exc_expr.op0();
246 
247  // add the assignment with the appropriate cast
248  code_assignt assignment(typecast_exprt(exc_thrown, exc_expr.type()),
249  exc_expr);
250  // now turn the `throw' into `assignment'
251  instr_it->type=ASSIGN;
252  instr_it->code=assignment;
253 }
254 
258  const goto_functionst::function_mapt::iterator &func_it,
259  const goto_programt::instructionst::iterator &instr_it,
260  const stack_catcht &stack_catch,
261  std::vector<exprt> &locals)
262 {
263  assert(instr_it->type==FUNCTION_CALL);
264 
265  goto_programt &goto_program=func_it->second.body;
266  const irep_idt &function_id=func_it->first;
267 
268  // save the address of the next instruction
269  goto_programt::instructionst::iterator next_it=instr_it;
270  next_it++;
271 
272  code_function_callt &function_call=to_code_function_call(instr_it->code);
273  assert(function_call.function().id()==ID_symbol);
274  const irep_idt &callee_id=
275  to_symbol_expr(function_call.function()).get_identifier();
276 
278  {
279  // we may have an escaping exception
280  const symbolt &callee_exc_symbol=
282  symbol_exprt callee_exc=callee_exc_symbol.symbol_expr();
283 
284  // find the end of the function
285  goto_programt::targett end_function=goto_program.get_end_function();
286  if(end_function!=instr_it)
287  {
288  // jump to the end of the function
289  // this will appear after the GOTO-based dynamic dispatch below
290  goto_programt::targett t_end=goto_program.insert_after(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;
294  }
295 
296  for(std::size_t i=stack_catch.size(); i-->0;)
297  {
298  for(std::size_t j=stack_catch[i].size(); j-->0;)
299  {
300  goto_programt::targett new_state_pc;
301  new_state_pc=stack_catch[i][j].second;
302  goto_programt::targett t_exc=goto_program.insert_after(instr_it);
303  t_exc->make_goto(new_state_pc);
304  t_exc->source_location=instr_it->source_location;
305  t_exc->function=instr_it->function;
306  // use instanceof to check that this is the correct handler
307  symbol_typet type(stack_catch[i][j].first);
308  type_exprt expr(type);
309  binary_predicate_exprt check_instanceof(
310  callee_exc,
311  ID_java_instanceof,
312  expr);
313  t_exc->guard=check_instanceof;
314  }
315  }
316 
317  // add dead instructions
318  for(const auto &local : locals)
319  {
320  goto_programt::targett t_dead=goto_program.insert_after(instr_it);
321  t_dead->make_dead();
322  t_dead->code=code_deadt(local);
323  t_dead->source_location=instr_it->source_location;
324  t_dead->function=instr_it->function;
325  }
326 
327  // add a null check (so that instanceof can be applied)
328  equal_exprt eq_null(
329  callee_exc,
331  goto_programt::targett t_null=goto_program.insert_after(instr_it);
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;
336 
337  // after each function call g() in function f
338  // adds f#exception_value=g#exception_value;
339  const symbolt &caller=
340  symbol_table.lookup(id2string(function_id)+EXC_SUFFIX);
341  const symbol_exprt &lhs_expr=caller.symbol_expr();
342 
343  goto_programt::targett t=goto_program.insert_after(instr_it);
344  t->make_assignment();
345  t->source_location=instr_it->source_location;
346  t->code=code_assignt(lhs_expr, callee_exc);
347  t->function=instr_it->function;
348  }
349 }
350 
355  const goto_functionst::function_mapt::iterator &func_it)
356 {
357  stack_catcht stack_catch; // stack of try-catch blocks
358  std::vector<std::vector<exprt>> stack_locals; // stack of local vars
359  std::vector<exprt> locals;
360  goto_programt &goto_program=func_it->second.body;
361 
362  if(goto_program.empty())
363  return;
364  Forall_goto_program_instructions(instr_it, goto_program)
365  {
366  if(instr_it->is_decl())
367  {
368  code_declt decl=to_code_decl(instr_it->code);
369  locals.push_back(decl.symbol());
370  }
371  // it's a CATCH but not a handler (as it has no operands)
372  else if(instr_it->type==CATCH && !instr_it->code.has_operands())
373  {
374  if(instr_it->targets.empty()) // pop
375  {
376  // pop the local vars stack
377  if(!stack_locals.empty())
378  {
379  locals=stack_locals.back();
380  stack_locals.pop_back();
381  }
382  // pop from the stack if possible
383  if(!stack_catch.empty())
384  {
385  stack_catch.pop_back();
386  }
387  else
388  {
389 #ifdef DEBUG
390  std::cout << "Remove exceptions: empty stack\n";
391 #endif
392  }
393  }
394  else // push
395  {
396  stack_locals.push_back(locals);
397  locals.clear();
398 
400  stack_catch.push_back(exception);
401  remove_exceptionst::catch_handlerst &last_exception=
402  stack_catch.back();
403 
404  // copy targets
405  const irept::subt &exception_list=
406  instr_it->code.find(ID_exception_list).get_sub();
407  assert(exception_list.size()==instr_it->targets.size());
408 
409  // Fill the map with the catch type and the target
410  unsigned i=0;
411  for(auto target : instr_it->targets)
412  {
413  last_exception.push_back(
414  std::make_pair(exception_list[i].id(), target));
415  i++;
416  }
417  }
418  instr_it->make_skip();
419  }
420  // CATCH handler
421  else if(instr_it->type==CATCH && instr_it->code.has_operands())
422  {
423  instrument_exception_handler(func_it, instr_it);
424  }
425  else if(instr_it->type==THROW)
426  {
427  instrument_throw(func_it, instr_it, stack_catch, locals);
428  }
429  else if(instr_it->type==FUNCTION_CALL)
430  {
431  instrument_function_call(func_it, instr_it, stack_catch, locals);
432  }
433  }
434 }
435 
437 {
438  Forall_goto_functions(it, goto_functions)
440  Forall_goto_functions(it, goto_functions)
442 }
443 
446  symbol_tablet &symbol_table,
447  goto_functionst &goto_functions)
448 {
450  remove_exceptions(goto_functions);
451 }
452 
455 {
457  remove_exceptions(goto_model.goto_functions);
458 }
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:218
semantic type conversion
Definition: std_expr.h:1725
symbolt & lookup(const irep_idt &identifier)
Find a symbol in the symbol table.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:296
Remove function exceptional returns.
symbol_tablet & symbol_table
exprt & op0()
Definition: expr.h:84
std::vector< irept > subt
Definition: irep.h:91
exprt & symbol()
Definition: std_code.h:205
instructionst instructions
The list of instructions in the goto program.
The null pointer constant.
Definition: std_expr.h:3774
An expression denoting a type.
Definition: std_expr.h:3671
bool empty() const
Is the program empty?
typet & type()
Definition: expr.h:60
symbol_tablet symbol_table
Definition: goto_model.h:25
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
void remove_exceptions(symbol_tablet &symbol_table, goto_functionst &goto_functions)
removes throws/CATCH-POP/CATCH-PUSH
bool is_static_lifetime
Definition: symbol.h:70
equality
Definition: std_expr.h:1082
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
Definition: irep.h:189
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:191
symbolst symbols
Definition: symbol_table.h:57
A reference into the symbol table.
Definition: std_types.h:109
A declaration of a local variable.
Definition: std_code.h:192
void instrument_exceptions(const goto_functionst::function_mapt::iterator &)
instruments throws, function calls that may escape exceptions and exception handlers.
The empty type.
Definition: std_types.h:53
API to expression classes.
The symbol table.
Definition: symbol_table.h:52
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition: symbol.h:137
A function call.
Definition: std_code.h:657
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.
Symbol table.
bool has_operands() const
Definition: expr.h:67
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...
Definition: goto_program.h:24
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 ...
#define EXC_SUFFIX
exprt & function()
Definition: std_code.h:677
Base class for all expressions.
Definition: expr.h:46
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
#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.
Definition: std_code.h:234
bool has_symbol(const irep_idt &name) const
Definition: symbol_table.h:87
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:73
Expression to hold a symbol (variable)
Definition: std_expr.h:82
dstringt irep_idt
Definition: irep.h:32
A generic base class for expressions that are predicates, i.e., boolean-typed, and that take exactly ...
Definition: std_expr.h:546
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:68
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
Definition: goto_model.h:26
std::vector< catch_handlerst > stack_catcht
Assignment.
Definition: std_code.h:144
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:700