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 #include "remove_instanceof.h"
16 
17 #ifdef DEBUG
18 #include <iostream>
19 #endif
20 
21 #include <stack>
22 #include <algorithm>
23 
24 #include <util/c_types.h>
25 #include <util/std_expr.h>
26 #include <util/std_code.h>
27 #include <util/symbol_table.h>
28 
30 
32 
80 {
81  typedef std::vector<std::pair<
83  typedef std::vector<catch_handlerst> stack_catcht;
84 
85 public:
86  typedef std::function<bool(const irep_idt &)> function_may_throwt;
87 
89  symbol_table_baset &_symbol_table,
90  function_may_throwt _function_may_throw,
92  : symbol_table(_symbol_table),
93  function_may_throw(_function_may_throw),
95  {
96  }
97 
98  void operator()(goto_functionst &goto_functions);
100 
101 protected:
105 
107 
108  bool function_or_callees_may_throw(const goto_programt &) const;
109 
112  const goto_programt::targett &,
113  bool may_catch);
114 
116  const remove_exceptionst::stack_catcht &stack_catch,
118  std::size_t &universal_try,
119  std::size_t &universal_catch);
120 
123  const goto_programt::targett &instr_it,
124  const stack_catcht &stack_catch,
125  const std::vector<exprt> &locals);
126 
127  bool instrument_throw(
129  const goto_programt::targett &,
130  const stack_catcht &,
131  const std::vector<exprt> &);
132 
135  const goto_programt::targett &,
136  const stack_catcht &,
137  const std::vector<exprt> &);
138 
141 };
142 
146 {
147  const symbolt *existing_symbol =
149  INVARIANT(
150  existing_symbol != nullptr,
151  "Java frontend should have created @inflight_exception variable");
152  return existing_symbol->symbol_expr();
153 }
154 
161  const goto_programt &goto_program) const
162 {
164  {
165  if(instr_it->is_throw())
166  {
167  return true;
168  }
169 
170  if(instr_it->is_function_call())
171  {
172  const exprt &function_expr=
173  to_code_function_call(instr_it->code).function();
175  function_expr.id()==ID_symbol,
176  "identifier expected to be a symbol");
177  const irep_idt &function_name=
178  to_symbol_expr(function_expr).get_identifier();
179  if(function_may_throw(function_name))
180  return true;
181  }
182  }
183 
184  return false;
185 }
186 
199  const goto_programt::targett &instr_it,
200  bool may_catch)
201 {
202  PRECONDITION(instr_it->type==CATCH);
203 
204  if(may_catch)
205  {
206  // retrieve the exception variable
207  const exprt &thrown_exception_local=
208  to_code_landingpad(instr_it->code).catch_expr();
209 
210  const symbol_exprt thrown_global_symbol=
212  // next we reset the exceptional return to NULL
213  null_pointer_exprt null_voidptr((pointer_type(empty_typet())));
214 
215  // add the assignment @inflight_exception = NULL
217  t_null->make_assignment();
218  t_null->source_location=instr_it->source_location;
219  t_null->code=code_assignt(
220  thrown_global_symbol,
221  null_voidptr);
222  t_null->function=instr_it->function;
223 
224  // add the assignment exc = @inflight_exception (before the null assignment)
226  t_exc->make_assignment();
227  t_exc->source_location=instr_it->source_location;
228  t_exc->code=code_assignt(
229  thrown_exception_local,
230  typecast_exprt(thrown_global_symbol, thrown_exception_local.type()));
231  t_exc->function=instr_it->function;
232  }
233  instr_it->make_skip();
234 }
235 
258  const remove_exceptionst::stack_catcht &stack_catch,
260  std::size_t &universal_try,
261  std::size_t &universal_catch)
262 {
263  for(std::size_t i=stack_catch.size(); i>0;)
264  {
265  i--;
266  for(std::size_t j=0; j<stack_catch[i].size(); ++j)
267  {
268  if(stack_catch[i][j].first.empty())
269  {
270  // Record the position of the default behaviour as any further catches
271  // will not capture the throw
272  universal_try=i;
273  universal_catch=j;
274 
275  // Universal handler. Highest on the stack takes
276  // precedence, so overwrite any we've already seen:
277  return stack_catch[i][j].second;
278  }
279  }
280  }
281  // Unless we have a universal exception handler, jump to end of function
283 }
284 
296  const goto_programt::targett &instr_it,
297  const remove_exceptionst::stack_catcht &stack_catch,
298  const std::vector<exprt> &locals)
299 {
300  // Jump to the universal handler or function end, as appropriate.
301  // This will appear after the GOTO-based dynamic dispatch below
302  goto_programt::targett default_dispatch=goto_program.insert_after(instr_it);
303 
304  // find the symbol corresponding to the caught exceptions
305  symbol_exprt exc_thrown =
307 
308  std::size_t default_try=0;
309  std::size_t default_catch=(!stack_catch.empty()) ? stack_catch[0].size() : 0;
310 
311  goto_programt::targett default_target=
313  default_try, default_catch);
314 
315  // add GOTOs implementing the dynamic dispatch of the
316  // exception handlers.
317  // The first loop is in forward order because the insertion reverses the order
318  // we note that try1{ try2 {} catch2c {} catch2d {}} catch1a() {} catch1b{}
319  // must catch in the following order: 2c 2d 1a 1b hence the numerical index
320  // is reversed whereas the letter ordering remains the same.
321  for(std::size_t i=default_try; i<stack_catch.size(); i++)
322  {
323  for(std::size_t j=(i==default_try) ? default_catch : stack_catch[i].size();
324  j>0;)
325  {
326  j--;
327  goto_programt::targett new_state_pc=
328  stack_catch[i][j].second;
329  if(!stack_catch[i][j].first.empty())
330  {
331  // Normal exception handler, make an instanceof check.
333  t_exc->make_goto(new_state_pc);
334  t_exc->source_location=instr_it->source_location;
335  t_exc->function=instr_it->function;
336 
337  // use instanceof to check that this is the correct handler
338  symbol_typet type(stack_catch[i][j].first);
339  type_exprt expr(type);
340 
341  binary_predicate_exprt check(exc_thrown, ID_java_instanceof, expr);
342  t_exc->guard=check;
343 
346  }
347  }
348  }
349 
350  default_dispatch->make_goto(default_target);
351  default_dispatch->source_location=instr_it->source_location;
352  default_dispatch->function=instr_it->function;
353 
354  // add dead instructions
355  for(const auto &local : locals)
356  {
358  t_dead->make_dead();
359  t_dead->code=code_deadt(local);
360  t_dead->source_location=instr_it->source_location;
361  t_dead->function=instr_it->function;
362  }
363 }
364 
369  const goto_programt::targett &instr_it,
370  const remove_exceptionst::stack_catcht &stack_catch,
371  const std::vector<exprt> &locals)
372 {
373  PRECONDITION(instr_it->type==THROW);
374 
375  const exprt &exc_expr=
377 
379  goto_program, instr_it, stack_catch, locals);
380 
381  // find the symbol where the thrown exception should be stored:
382  symbol_exprt exc_thrown =
384 
385  // add the assignment with the appropriate cast
386  code_assignt assignment(
387  exc_thrown,
388  typecast_exprt(exc_expr, exc_thrown.type()));
389  // now turn the `throw' into `assignment'
390  instr_it->type=ASSIGN;
391  instr_it->code=assignment;
392 
393  return true;
394 }
395 
400  const goto_programt::targett &instr_it,
401  const stack_catcht &stack_catch,
402  const std::vector<exprt> &locals)
403 {
404  PRECONDITION(instr_it->type==FUNCTION_CALL);
405 
406  // save the address of the next instruction
407  goto_programt::targett next_it=instr_it;
408  next_it++;
409 
410  code_function_callt &function_call=to_code_function_call(instr_it->code);
412  function_call.function().id()==ID_symbol,
413  "identified expected to be a symbol");
414  const irep_idt &callee_id=
415  to_symbol_expr(function_call.function()).get_identifier();
416 
417  if(function_may_throw(callee_id))
418  {
419  equal_exprt no_exception_currently_in_flight(
422 
423  if(symbol_table.lookup_ref(callee_id).type.get_bool(ID_C_must_not_throw))
424  {
425  // Function is annotated must-not-throw, but we can't prove that here.
426  // Insert an ASSUME(@inflight_exception == null):
427  goto_programt::targett assume_null = goto_program.insert_after(instr_it);
428  assume_null->make_assumption(no_exception_currently_in_flight);
429  }
430  else
431  {
433  goto_program, instr_it, stack_catch, locals);
434 
435  // add a null check (so that instanceof can be applied)
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;
441  }
442 
443  return true;
444  }
445 
446  return false;
447 }
448 
454 {
455  stack_catcht stack_catch; // stack of try-catch blocks
456  std::vector<std::vector<exprt>> stack_locals; // stack of local vars
457  std::vector<exprt> locals;
458 
459  if(goto_program.empty())
460  return;
461 
462  bool program_or_callees_may_throw =
464 
465  bool did_something = false;
466 
468  {
469  if(instr_it->is_decl())
470  {
471  code_declt decl=to_code_decl(instr_it->code);
472  locals.push_back(decl.symbol());
473  }
474  // Is it a handler push/pop or catch landing-pad?
475  else if(instr_it->type==CATCH)
476  {
477  const irep_idt &statement=instr_it->code.get_statement();
478  // Is it an exception landing pad (start of a catch block)?
479  if(statement==ID_exception_landingpad)
480  {
482  goto_program, instr_it, program_or_callees_may_throw);
483  }
484  // Is it a catch handler pop?
485  else if(statement==ID_pop_catch)
486  {
487  // pop the local vars stack
488  if(!stack_locals.empty())
489  {
490  locals=stack_locals.back();
491  stack_locals.pop_back();
492  }
493  // pop from the stack if possible
494  if(!stack_catch.empty())
495  {
496  stack_catch.pop_back();
497  }
498  else
499  {
500 #ifdef DEBUG
501  std::cout << "Remove exceptions: empty stack\n";
502 #endif
503  }
504  }
505  // Is it a catch handler push?
506  else if(statement==ID_push_catch)
507  {
508  stack_locals.push_back(locals);
509  locals.clear();
510 
512  stack_catch.push_back(exception);
513  remove_exceptionst::catch_handlerst &last_exception=
514  stack_catch.back();
515 
516  // copy targets
517  const code_push_catcht::exception_listt &exception_list=
518  to_code_push_catch(instr_it->code).exception_list();
519 
520  // The target list can be empty if `finish_catch_push_targets` found that
521  // the targets were unreachable (in which case no exception can truly
522  // be thrown at runtime)
523  INVARIANT(
524  instr_it->targets.empty() ||
525  exception_list.size()==instr_it->targets.size(),
526  "`exception_list` should contain current instruction's targets");
527 
528  // Fill the map with the catch type and the target
529  unsigned i=0;
530  for(auto target : instr_it->targets)
531  {
532  last_exception.push_back(
533  std::make_pair(exception_list[i].get_tag(), target));
534  i++;
535  }
536  }
537  else
538  {
539  INVARIANT(
540  false,
541  "CATCH opcode should be one of push-catch, pop-catch, landingpad");
542  }
543  instr_it->make_skip();
544  did_something = true;
545  }
546  else if(instr_it->type==THROW)
547  {
548  did_something |=
549  instrument_throw(goto_program, instr_it, stack_catch, locals);
550  }
551  else if(instr_it->type==FUNCTION_CALL)
552  {
553  did_something |=
554  instrument_function_call(goto_program, instr_it, stack_catch, locals);
555  }
556  }
557 
558  if(did_something)
560 }
561 
563 {
564  Forall_goto_functions(it, goto_functions)
565  instrument_exceptions(it->second.body);
566 }
567 
569 {
571 }
572 
575  symbol_table_baset &symbol_table,
576  goto_functionst &goto_functions,
578 {
579  const namespacet ns(symbol_table);
580  std::map<irep_idt, std::set<irep_idt>> exceptions_map;
581  uncaught_exceptions(goto_functions, ns, exceptions_map);
582  remove_exceptionst::function_may_throwt function_may_throw =
583  [&exceptions_map](const irep_idt &id) {
584  return !exceptions_map[id].empty();
585  };
587  symbol_table,
588  function_may_throw,
590  remove_exceptions(goto_functions);
591 }
592 
608  symbol_table_baset &symbol_table,
610 {
611  remove_exceptionst::function_may_throwt any_function_may_throw =
612  [](const irep_idt &id) { return true; };
613 
615  symbol_table,
616  any_function_may_throw,
619 }
620 
623 {
624  remove_exceptions(goto_model.symbol_table, goto_model.goto_functions, type);
625 }
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:289
std::vector< exception_list_entryt > exception_listt
Definition: std_code.h:1503
semantic type conversion
Definition: std_expr.h:2111
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)
Definition: c_types.cpp:243
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.
exprt & symbol()
Definition: std_code.h:266
irep_idt get_tag(const typet &type)
remove_exceptionst(symbol_table_baset &_symbol_table, function_may_throwt _function_may_throw, bool remove_added_instanceof)
remove_exceptions_typest
const irep_idt & get_identifier() const
Definition: std_expr.h:128
The null pointer constant.
Definition: std_expr.h:4520
An expression denoting a type.
Definition: std_expr.h:4410
function_may_throwt function_may_throw
typet & type()
Definition: expr.h:56
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
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
Definition: irep.cpp:240
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:205
equality
Definition: std_expr.h:1354
const irep_idt & id() const
Definition: irep.h:189
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
Definition: symbol.cpp:111
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.
Definition: std_types.h:110
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
Definition: goto_program.h:397
A declaration of a local variable.
Definition: std_code.h:253
static code_push_catcht & to_code_push_catch(codet &code)
Definition: std_code.h:1531
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.
The empty type.
Definition: std_types.h:54
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.
TO_BE_DOCUMENTED.
Definition: namespace.h:74
#define PRECONDITION(CONDITION)
Definition: invariant.h:230
targett insert_after(const_targett target)
Insertion after the given target.
Definition: goto_program.h:480
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 ...
A function call.
Definition: std_code.h:828
void operator()(goto_functionst &goto_functions)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
Author: Diffblue Ltd.
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.
Definition: goto_program.h:70
typet type
Type of symbol.
Definition: symbol.h:34
static code_landingpadt & to_code_landingpad(codet &code)
Definition: std_code.h:1607
symbol_table_baset & symbol_table
std::function< bool(const irep_idt &)> function_may_throwt
exprt & function()
Definition: std_code.h:848
Base class for all expressions.
Definition: expr.h:42
targett get_end_function()
Definition: goto_program.h:616
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
Definition: remove_skip.cpp:86
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?
Definition: goto_program.h:590
A removal of a local variable.
Definition: std_code.h:305
goto_programt & goto_program
Definition: cover.cpp:63
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:740
Expression to hold a symbol (variable)
Definition: std_expr.h:90
const exprt & catch_expr() const
Definition: std_code.h:1589
dstringt irep_idt
Definition: irep.h:31
A generic base class for expressions that are predicates, i.e., boolean-typed, and that take exactly ...
Definition: std_expr.h:730
Program Transformation.
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:257
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)
Definition: goto_program.h:735
exception_listt & exception_list()
Definition: std_code.h:1514
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
std::vector< catch_handlerst > stack_catcht
Assignment.
Definition: std_code.h:195
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:879