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  const class_hierarchyt *_class_hierarchy,
91  function_may_throwt _function_may_throw,
92  bool _remove_added_instanceof,
93  message_handlert &_message_handler)
94  : symbol_table(_symbol_table),
95  class_hierarchy(_class_hierarchy),
96  function_may_throw(_function_may_throw),
97  remove_added_instanceof(_remove_added_instanceof),
98  message_handler(_message_handler)
99  {
101  {
102  INVARIANT(
103  class_hierarchy != nullptr,
104  "remove_exceptions needs a class hierarchy to remove instanceof "
105  "statements (either supply one, or don't use REMOVE_ADDED_INSTANCEOF)");
106  }
107  }
108 
109  void operator()(goto_functionst &goto_functions);
110  void operator()(goto_programt &goto_program);
111 
112 protected:
118 
120 
121  bool function_or_callees_may_throw(const goto_programt &) const;
122 
124  goto_programt &goto_program,
125  const goto_programt::targett &,
126  bool may_catch);
127 
129  const remove_exceptionst::stack_catcht &stack_catch,
130  goto_programt &goto_program,
131  std::size_t &universal_try,
132  std::size_t &universal_catch);
133 
135  goto_programt &goto_program,
136  const goto_programt::targett &instr_it,
137  const stack_catcht &stack_catch,
138  const std::vector<symbol_exprt> &locals);
139 
140  bool instrument_throw(
141  goto_programt &goto_program,
142  const goto_programt::targett &,
143  const stack_catcht &,
144  const std::vector<symbol_exprt> &);
145 
147  goto_programt &goto_program,
148  const goto_programt::targett &,
149  const stack_catcht &,
150  const std::vector<symbol_exprt> &);
151 
153  goto_programt &goto_program);
154 };
155 
159 {
160  const symbolt *existing_symbol =
162  INVARIANT(
163  existing_symbol != nullptr,
164  "Java frontend should have created @inflight_exception variable");
165  return existing_symbol->symbol_expr();
166 }
167 
174  const goto_programt &goto_program) const
175 {
176  forall_goto_program_instructions(instr_it, goto_program)
177  {
178  if(instr_it->is_throw())
179  {
180  return true;
181  }
182 
183  if(instr_it->is_function_call())
184  {
185  const exprt &function_expr=
186  to_code_function_call(instr_it->code).function();
188  function_expr.id()==ID_symbol,
189  "identifier expected to be a symbol");
190  const irep_idt &function_name=
191  to_symbol_expr(function_expr).get_identifier();
192  if(function_may_throw(function_name))
193  return true;
194  }
195  }
196 
197  return false;
198 }
199 
211  goto_programt &goto_program,
212  const goto_programt::targett &instr_it,
213  bool may_catch)
214 {
215  PRECONDITION(instr_it->type==CATCH);
216 
217  if(may_catch)
218  {
219  // retrieve the exception variable
220  const exprt &thrown_exception_local=
221  to_code_landingpad(instr_it->code).catch_expr();
222 
223  const symbol_exprt thrown_global_symbol=
225  // next we reset the exceptional return to NULL
226  null_pointer_exprt null_voidptr((pointer_type(empty_typet())));
227 
228  // add the assignment @inflight_exception = NULL
229  goto_programt::targett t_null=goto_program.insert_after(instr_it);
230  t_null->make_assignment();
231  t_null->source_location=instr_it->source_location;
232  t_null->code=code_assignt(
233  thrown_global_symbol,
234  null_voidptr);
235  t_null->function=instr_it->function;
236 
237  // add the assignment exc = @inflight_exception (before the null assignment)
238  goto_programt::targett t_exc=goto_program.insert_after(instr_it);
239  t_exc->make_assignment();
240  t_exc->source_location=instr_it->source_location;
241  t_exc->code=code_assignt(
242  thrown_exception_local,
243  typecast_exprt(thrown_global_symbol, thrown_exception_local.type()));
244  t_exc->function=instr_it->function;
245  }
246  instr_it->make_skip();
247 }
248 
271  const remove_exceptionst::stack_catcht &stack_catch,
272  goto_programt &goto_program,
273  std::size_t &universal_try,
274  std::size_t &universal_catch)
275 {
276  for(std::size_t i=stack_catch.size(); i>0;)
277  {
278  i--;
279  for(std::size_t j=0; j<stack_catch[i].size(); ++j)
280  {
281  if(stack_catch[i][j].first.empty())
282  {
283  // Record the position of the default behaviour as any further catches
284  // will not capture the throw
285  universal_try=i;
286  universal_catch=j;
287 
288  // Universal handler. Highest on the stack takes
289  // precedence, so overwrite any we've already seen:
290  return stack_catch[i][j].second;
291  }
292  }
293  }
294  // Unless we have a universal exception handler, jump to end of function
295  return goto_program.get_end_function();
296 }
297 
308  goto_programt &goto_program,
309  const goto_programt::targett &instr_it,
310  const remove_exceptionst::stack_catcht &stack_catch,
311  const std::vector<symbol_exprt> &locals)
312 {
313  // Jump to the universal handler or function end, as appropriate.
314  // This will appear after the GOTO-based dynamic dispatch below
315  goto_programt::targett default_dispatch=goto_program.insert_after(instr_it);
316 
317  // find the symbol corresponding to the caught exceptions
318  symbol_exprt exc_thrown =
320 
321  std::size_t default_try=0;
322  std::size_t default_catch=(!stack_catch.empty()) ? stack_catch[0].size() : 0;
323 
324  goto_programt::targett default_target=
325  find_universal_exception(stack_catch, goto_program,
326  default_try, default_catch);
327 
328  // add GOTOs implementing the dynamic dispatch of the
329  // exception handlers.
330  // The first loop is in forward order because the insertion reverses the order
331  // we note that try1{ try2 {} catch2c {} catch2d {}} catch1a() {} catch1b{}
332  // must catch in the following order: 2c 2d 1a 1b hence the numerical index
333  // is reversed whereas the letter ordering remains the same.
334  for(std::size_t i=default_try; i<stack_catch.size(); i++)
335  {
336  for(std::size_t j=(i==default_try) ? default_catch : stack_catch[i].size();
337  j>0;)
338  {
339  j--;
340  goto_programt::targett new_state_pc=
341  stack_catch[i][j].second;
342  if(!stack_catch[i][j].first.empty())
343  {
344  // Normal exception handler, make an instanceof check.
345  goto_programt::targett t_exc=goto_program.insert_after(instr_it);
346  t_exc->make_goto(new_state_pc);
347  t_exc->source_location=instr_it->source_location;
348  t_exc->function=instr_it->function;
349 
350  // use instanceof to check that this is the correct handler
351  struct_tag_typet type(stack_catch[i][j].first);
352  type_exprt expr(type);
353 
354  binary_predicate_exprt check(exc_thrown, ID_java_instanceof, expr);
355  t_exc->guard=check;
356 
358  {
360  t_exc,
361  goto_program,
362  symbol_table,
365  }
366  }
367  }
368  }
369 
370  default_dispatch->make_goto(default_target);
371  default_dispatch->source_location=instr_it->source_location;
372  default_dispatch->function=instr_it->function;
373 
374  // add dead instructions
375  for(const auto &local : locals)
376  {
377  goto_programt::targett t_dead=goto_program.insert_after(instr_it);
378  t_dead->make_dead();
379  t_dead->code=code_deadt(local);
380  t_dead->source_location=instr_it->source_location;
381  t_dead->function=instr_it->function;
382  }
383 }
384 
388  goto_programt &goto_program,
389  const goto_programt::targett &instr_it,
390  const remove_exceptionst::stack_catcht &stack_catch,
391  const std::vector<symbol_exprt> &locals)
392 {
393  PRECONDITION(instr_it->type==THROW);
394 
395  const exprt &exc_expr=
397 
399  goto_program, instr_it, stack_catch, locals);
400 
401  // find the symbol where the thrown exception should be stored:
402  symbol_exprt exc_thrown =
404 
405  // add the assignment with the appropriate cast
406  code_assignt assignment(
407  exc_thrown,
408  typecast_exprt(exc_expr, exc_thrown.type()));
409  // now turn the `throw' into `assignment'
410  instr_it->type=ASSIGN;
411  instr_it->code=assignment;
412 
413  return true;
414 }
415 
419  goto_programt &goto_program,
420  const goto_programt::targett &instr_it,
421  const stack_catcht &stack_catch,
422  const std::vector<symbol_exprt> &locals)
423 {
424  PRECONDITION(instr_it->type==FUNCTION_CALL);
425 
426  // save the address of the next instruction
427  goto_programt::targett next_it=instr_it;
428  next_it++;
429 
430  code_function_callt &function_call=to_code_function_call(instr_it->code);
432  function_call.function().id()==ID_symbol,
433  "identified expected to be a symbol");
434  const irep_idt &callee_id=
435  to_symbol_expr(function_call.function()).get_identifier();
436 
437  if(function_may_throw(callee_id))
438  {
439  equal_exprt no_exception_currently_in_flight(
442 
443  if(symbol_table.lookup_ref(callee_id).type.get_bool(ID_C_must_not_throw))
444  {
445  // Function is annotated must-not-throw, but we can't prove that here.
446  // Insert an ASSUME(@inflight_exception == null):
447  goto_programt::targett assume_null = goto_program.insert_after(instr_it);
448  assume_null->make_assumption(no_exception_currently_in_flight);
449  }
450  else
451  {
453  goto_program, instr_it, stack_catch, locals);
454 
455  // add a null check (so that instanceof can be applied)
456  goto_programt::targett t_null=goto_program.insert_after(instr_it);
457  t_null->make_goto(next_it);
458  t_null->source_location=instr_it->source_location;
459  t_null->function=instr_it->function;
460  t_null->guard=no_exception_currently_in_flight;
461  }
462 
463  return true;
464  }
465 
466  return false;
467 }
468 
473  goto_programt &goto_program)
474 {
475  stack_catcht stack_catch; // stack of try-catch blocks
476  std::vector<std::vector<symbol_exprt>> stack_locals; // stack of local vars
477  std::vector<symbol_exprt> locals;
478 
479  if(goto_program.empty())
480  return;
481 
482  bool program_or_callees_may_throw =
483  function_or_callees_may_throw(goto_program);
484 
485  bool did_something = false;
486 
487  Forall_goto_program_instructions(instr_it, goto_program)
488  {
489  if(instr_it->is_decl())
490  {
491  code_declt decl=to_code_decl(instr_it->code);
492  locals.push_back(decl.symbol());
493  }
494  // Is it a handler push/pop or catch landing-pad?
495  else if(instr_it->type==CATCH)
496  {
497  const irep_idt &statement=instr_it->code.get_statement();
498  // Is it an exception landing pad (start of a catch block)?
499  if(statement==ID_exception_landingpad)
500  {
502  goto_program, instr_it, program_or_callees_may_throw);
503  }
504  // Is it a catch handler pop?
505  else if(statement==ID_pop_catch)
506  {
507  // pop the local vars stack
508  if(!stack_locals.empty())
509  {
510  locals=stack_locals.back();
511  stack_locals.pop_back();
512  }
513  // pop from the stack if possible
514  if(!stack_catch.empty())
515  {
516  stack_catch.pop_back();
517  }
518  else
519  {
520 #ifdef DEBUG
521  std::cout << "Remove exceptions: empty stack\n";
522 #endif
523  }
524  }
525  // Is it a catch handler push?
526  else if(statement==ID_push_catch)
527  {
528  stack_locals.push_back(locals);
529  locals.clear();
530 
532  stack_catch.push_back(exception);
533  remove_exceptionst::catch_handlerst &last_exception=
534  stack_catch.back();
535 
536  // copy targets
537  const code_push_catcht::exception_listt &exception_list=
538  to_code_push_catch(instr_it->code).exception_list();
539 
540  // The target list can be empty if `finish_catch_push_targets` found that
541  // the targets were unreachable (in which case no exception can truly
542  // be thrown at runtime)
543  INVARIANT(
544  instr_it->targets.empty() ||
545  exception_list.size()==instr_it->targets.size(),
546  "`exception_list` should contain current instruction's targets");
547 
548  // Fill the map with the catch type and the target
549  unsigned i=0;
550  for(auto target : instr_it->targets)
551  {
552  last_exception.push_back(
553  std::make_pair(exception_list[i].get_tag(), target));
554  i++;
555  }
556  }
557  else
558  {
559  INVARIANT(
560  false,
561  "CATCH opcode should be one of push-catch, pop-catch, landingpad");
562  }
563  instr_it->make_skip();
564  did_something = true;
565  }
566  else if(instr_it->type==THROW)
567  {
568  did_something |=
569  instrument_throw(goto_program, instr_it, stack_catch, locals);
570  }
571  else if(instr_it->type==FUNCTION_CALL)
572  {
573  did_something |=
574  instrument_function_call(goto_program, instr_it, stack_catch, locals);
575  }
576  }
577 
578  if(did_something)
579  remove_skip(goto_program);
580 }
581 
583 {
584  Forall_goto_functions(it, goto_functions)
585  instrument_exceptions(it->second.body);
586 }
587 
589 {
590  instrument_exceptions(goto_program);
591 }
592 
595  symbol_table_baset &symbol_table,
596  goto_functionst &goto_functions,
597  message_handlert &message_handler)
598 {
599  const namespacet ns(symbol_table);
600  std::map<irep_idt, std::set<irep_idt>> exceptions_map;
601 
602  uncaught_exceptions(goto_functions, ns, exceptions_map);
603 
604  remove_exceptionst::function_may_throwt function_may_throw =
605  [&exceptions_map](const irep_idt &id) {
606  return !exceptions_map[id].empty();
607  };
608 
610  symbol_table, nullptr, function_may_throw, false, message_handler);
611 
612  remove_exceptions(goto_functions);
613 }
614 
627  goto_programt &goto_program,
628  symbol_table_baset &symbol_table,
629  message_handlert &message_handler)
630 {
631  remove_exceptionst::function_may_throwt any_function_may_throw =
632  [](const irep_idt &) { return true; };
633 
635  symbol_table, nullptr, any_function_may_throw, false, message_handler);
636 
637  remove_exceptions(goto_program);
638 }
639 
648  goto_modelt &goto_model,
649  message_handlert &message_handler)
650 {
652  goto_model.symbol_table, goto_model.goto_functions, message_handler);
653 }
654 
657  symbol_table_baset &symbol_table,
658  goto_functionst &goto_functions,
659  const class_hierarchyt &class_hierarchy,
660  message_handlert &message_handler)
661 {
662  const namespacet ns(symbol_table);
663  std::map<irep_idt, std::set<irep_idt>> exceptions_map;
664 
665  uncaught_exceptions(goto_functions, ns, exceptions_map);
666 
667  remove_exceptionst::function_may_throwt function_may_throw =
668  [&exceptions_map](const irep_idt &id) {
669  return !exceptions_map[id].empty();
670  };
671 
673  symbol_table, &class_hierarchy, function_may_throw, true, message_handler);
674 
675  remove_exceptions(goto_functions);
676 }
677 
692  goto_programt &goto_program,
693  symbol_table_baset &symbol_table,
694  const class_hierarchyt &class_hierarchy,
695  message_handlert &message_handler)
696 {
697  remove_exceptionst::function_may_throwt any_function_may_throw =
698  [](const irep_idt &) { return true; };
699 
701  symbol_table,
702  &class_hierarchy,
703  any_function_may_throw,
704  true,
705  message_handler);
706 
707  remove_exceptions(goto_program);
708 }
709 
720  goto_modelt &goto_model,
721  const class_hierarchyt &class_hierarchy,
722  message_handlert &message_handler)
723 {
725  goto_model.symbol_table,
726  goto_model.goto_functions,
727  class_hierarchy,
728  message_handler);
729 }
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:399
std::vector< exception_list_entryt > exception_listt
Definition: std_code.h:1890
Semantic type conversion.
Definition: std_expr.h:2277
symbol_exprt get_inflight_exception_global()
Create a global named java::@inflight_exception that holds any exception that has been thrown but not...
bool instrument_throw(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
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.
Non-graph-based representation of the class hierarchy.
const irep_idt & get_identifier() const
Definition: std_expr.h:176
The null pointer constant.
Definition: std_expr.h:4471
An expression denoting a type.
Definition: std_expr.h:4370
function_may_throwt function_may_throw
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:517
typet & type()
Return the type of the expression.
Definition: expr.h:68
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
Symbol table entry.
Definition: symbol.h:27
message_handlert & message_handler
bool function_or_callees_may_throw(const goto_programt &) const
Checks whether a function may ever experience an exception (whether or not it catches),...
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:239
void remove_instanceof(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...
Equality.
Definition: std_expr.h:1484
void remove_exceptions_using_instanceof(symbol_table_baset &symbol_table, goto_functionst &goto_functions, message_handlert &message_handler)
removes throws/CATCH-POP/CATCH-PUSH
const irep_idt & id() const
Definition: irep.h:259
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
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:414
A codet representing the declaration of a local variable.
Definition: std_code.h:352
static code_push_catcht & to_code_push_catch(codet &code)
Definition: std_code.h:1918
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.
const class_hierarchyt * class_hierarchy
The empty type.
Definition: std_types.h:48
API to expression classes.
void add_exception_dispatch_sequence(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) ...
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:518
codet representation of a function call statement.
Definition: std_code.h:1036
void operator()(goto_functionst &goto_functions)
A collection of goto functions.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
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
static irep_idt get_tag(const typet &type)
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
typet type
Type of symbol.
Definition: symbol.h:31
static code_landingpadt & to_code_landingpad(codet &code)
Definition: std_code.h:1994
symbol_exprt & symbol()
Definition: std_code.h:360
symbol_table_baset & symbol_table
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
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)
std::function< bool(const irep_idt &)> function_may_throwt
exprt & function()
Definition: std_code.h:1099
Base class for all expressions.
Definition: expr.h:54
targett get_end_function()
Get an instruction iterator pointing to the END_FUNCTION instruction of the goto program.
Definition: goto_program.h:654
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
#define Forall_goto_functions(it, functions)
bool empty() const
Is the program empty?
Definition: goto_program.h:626
A codet representing the removal of a local variable going out of scope.
Definition: std_code.h:424
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:809
bool instrument_function_call(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...
Expression to hold a symbol (variable)
Definition: std_expr.h:143
const exprt & catch_expr() const
Definition: std_code.h:1976
dstringt irep_idt
Definition: irep.h:32
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:835
Program Transformation.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:485
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:804
exception_listt & exception_list()
Definition: std_code.h:1901
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
std::vector< catch_handlerst > stack_catcht
A codet representing an assignment in the program.
Definition: std_code.h:256
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1173