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 <algorithm>
22 
23 #include <util/c_types.h>
24 #include <util/pointer_expr.h>
25 #include <util/std_code.h>
26 #include <util/symbol_table.h>
27 
30 
32 
34 
35 #include "java_expr.h"
36 #include "java_types.h"
37 
85 {
86  typedef std::vector<std::pair<
88  typedef std::vector<catch_handlerst> stack_catcht;
89 
90 public:
91  typedef std::function<bool(const irep_idt &)> function_may_throwt;
92 
94  symbol_table_baset &_symbol_table,
95  const class_hierarchyt *_class_hierarchy,
96  function_may_throwt _function_may_throw,
97  bool _remove_added_instanceof,
98  message_handlert &_message_handler)
99  : symbol_table(_symbol_table),
100  class_hierarchy(_class_hierarchy),
101  function_may_throw(_function_may_throw),
102  remove_added_instanceof(_remove_added_instanceof),
103  message_handler(_message_handler)
104  {
106  {
107  INVARIANT(
108  class_hierarchy != nullptr,
109  "remove_exceptions needs a class hierarchy to remove instanceof "
110  "statements (either supply one, or don't use REMOVE_ADDED_INSTANCEOF)");
111  }
112  }
113 
114  void operator()(goto_functionst &goto_functions);
115  void
116  operator()(const irep_idt &function_identifier, goto_programt &goto_program);
117 
118 protected:
124 
126  {
127  DID_NOTHING,
130  };
131 
133 
134  bool function_or_callees_may_throw(const goto_programt &) const;
135 
137  goto_programt &goto_program,
138  const goto_programt::targett &,
139  bool may_catch);
140 
142  const remove_exceptionst::stack_catcht &stack_catch,
143  goto_programt &goto_program,
144  std::size_t &universal_try,
145  std::size_t &universal_catch);
146 
148  const irep_idt &function_identifier,
149  goto_programt &goto_program,
150  const goto_programt::targett &instr_it,
151  const stack_catcht &stack_catch,
152  const std::vector<symbol_exprt> &locals);
153 
154  bool instrument_throw(
155  const irep_idt &function_identifier,
156  goto_programt &goto_program,
157  const goto_programt::targett &,
158  const stack_catcht &,
159  const std::vector<symbol_exprt> &);
160 
162  const irep_idt &function_identifier,
163  goto_programt &goto_program,
164  const goto_programt::targett &,
165  const stack_catcht &,
166  const std::vector<symbol_exprt> &);
167 
169  const irep_idt &function_identifier,
170  goto_programt &goto_program);
171 };
172 
176 {
177  const symbolt *existing_symbol =
179  INVARIANT(
180  existing_symbol != nullptr,
181  "Java frontend should have created @inflight_exception variable");
182  return existing_symbol->symbol_expr();
183 }
184 
191  const goto_programt &goto_program) const
192 {
193  for(const auto &instruction : goto_program.instructions)
194  {
195  if(instruction.is_throw())
196  {
197  return true;
198  }
199 
200  if(instruction.is_function_call())
201  {
202  const exprt &function_expr = instruction.call_function();
204  function_expr.id()==ID_symbol,
205  "identifier expected to be a symbol");
206  const irep_idt &function_name=
207  to_symbol_expr(function_expr).get_identifier();
208  if(function_may_throw(function_name))
209  return true;
210  }
211  }
212 
213  return false;
214 }
215 
227  goto_programt &goto_program,
228  const goto_programt::targett &instr_it,
229  bool may_catch)
230 {
231  PRECONDITION(instr_it->type==CATCH);
232 
233  if(may_catch)
234  {
235  // retrieve the exception variable
236  const exprt &thrown_exception_local =
237  to_code_landingpad(instr_it->get_code()).catch_expr();
238 
239  const symbol_exprt thrown_global_symbol=
241  // next we reset the exceptional return to NULL
243 
244  // add the assignment @inflight_exception = NULL
245  goto_program.insert_after(
246  instr_it,
248  code_assignt(thrown_global_symbol, null_voidptr),
249  instr_it->source_location));
250 
251  // add the assignment exc = @inflight_exception (before the null assignment)
252  goto_program.insert_after(
253  instr_it,
255  code_assignt(
256  thrown_exception_local,
257  typecast_exprt(thrown_global_symbol, thrown_exception_local.type())),
258  instr_it->source_location));
259  }
260 
261  instr_it->turn_into_skip();
262 }
263 
286  const remove_exceptionst::stack_catcht &stack_catch,
287  goto_programt &goto_program,
288  std::size_t &universal_try,
289  std::size_t &universal_catch)
290 {
291  for(std::size_t i=stack_catch.size(); i>0;)
292  {
293  i--;
294  for(std::size_t j=0; j<stack_catch[i].size(); ++j)
295  {
296  if(stack_catch[i][j].first.empty())
297  {
298  // Record the position of the default behaviour as any further catches
299  // will not capture the throw
300  universal_try=i;
301  universal_catch=j;
302 
303  // Universal handler. Highest on the stack takes
304  // precedence, so overwrite any we've already seen:
305  return stack_catch[i][j].second;
306  }
307  }
308  }
309  // Unless we have a universal exception handler, jump to end of function
310  return goto_program.get_end_function();
311 }
312 
324  const irep_idt &function_identifier,
325  goto_programt &goto_program,
326  const goto_programt::targett &instr_it,
327  const remove_exceptionst::stack_catcht &stack_catch,
328  const std::vector<symbol_exprt> &locals)
329 {
330  // Jump to the universal handler or function end, as appropriate.
331  // This will appear after the GOTO-based dynamic dispatch below
332  goto_programt::targett default_dispatch=goto_program.insert_after(instr_it);
333 
334  // find the symbol corresponding to the caught exceptions
335  symbol_exprt exc_thrown =
337 
338  std::size_t default_try=0;
339  std::size_t default_catch=(!stack_catch.empty()) ? stack_catch[0].size() : 0;
340 
341  goto_programt::targett default_target=
342  find_universal_exception(stack_catch, goto_program,
343  default_try, default_catch);
344 
345  // add GOTOs implementing the dynamic dispatch of the
346  // exception handlers.
347  // The first loop is in forward order because the insertion reverses the order
348  // we note that try1{ try2 {} catch2c {} catch2d {}} catch1a() {} catch1b{}
349  // must catch in the following order: 2c 2d 1a 1b hence the numerical index
350  // is reversed whereas the letter ordering remains the same.
351  for(std::size_t i=default_try; i<stack_catch.size(); i++)
352  {
353  for(std::size_t j=(i==default_try) ? default_catch : stack_catch[i].size();
354  j>0;)
355  {
356  j--;
357  goto_programt::targett new_state_pc=
358  stack_catch[i][j].second;
359  if(!stack_catch[i][j].first.empty())
360  {
361  // Normal exception handler, make an instanceof check.
362  goto_programt::targett t_exc = goto_program.insert_after(
363  instr_it,
365  new_state_pc, true_exprt(), instr_it->source_location));
366 
367  // use instanceof to check that this is the correct handler
368  struct_tag_typet type(stack_catch[i][j].first);
369 
370  java_instanceof_exprt check(exc_thrown, type);
371  t_exc->guard=check;
372 
374  {
376  function_identifier,
377  t_exc,
378  goto_program,
379  symbol_table,
382  }
383  }
384  }
385  }
386 
387  *default_dispatch = goto_programt::make_goto(
388  default_target, true_exprt(), instr_it->source_location);
389 
390  // add dead instructions
391  for(const auto &local : locals)
392  {
393  goto_program.insert_after(
394  instr_it, goto_programt::make_dead(local, instr_it->source_location));
395  }
396 }
397 
401  const irep_idt &function_identifier,
402  goto_programt &goto_program,
403  const goto_programt::targett &instr_it,
404  const remove_exceptionst::stack_catcht &stack_catch,
405  const std::vector<symbol_exprt> &locals)
406 {
407  PRECONDITION(instr_it->type==THROW);
408 
409  const exprt &exc_expr =
411 
413  function_identifier, goto_program, instr_it, stack_catch, locals);
414 
415  // find the symbol where the thrown exception should be stored:
416  symbol_exprt exc_thrown =
418 
419  // add the assignment with the appropriate cast
420  code_assignt assignment(
421  exc_thrown,
422  typecast_exprt(exc_expr, exc_thrown.type()));
423  // now turn the `throw' into `assignment'
424  instr_it->type=ASSIGN;
425  instr_it->code_nonconst() = assignment;
426 
427  return true;
428 }
429 
434  const irep_idt &function_identifier,
435  goto_programt &goto_program,
436  const goto_programt::targett &instr_it,
437  const stack_catcht &stack_catch,
438  const std::vector<symbol_exprt> &locals)
439 {
440  PRECONDITION(instr_it->type==FUNCTION_CALL);
441 
442  // save the address of the next instruction
443  goto_programt::targett next_it=instr_it;
444  next_it++;
445 
446  const auto &function = instr_it->call_function();
447 
449  function.id() == ID_symbol, "function call expected to be a symbol");
450  const irep_idt &callee_id = to_symbol_expr(function).get_identifier();
451 
452  if(function_may_throw(callee_id))
453  {
454  equal_exprt no_exception_currently_in_flight(
457 
458  if(symbol_table.lookup_ref(callee_id).type.get_bool(ID_C_must_not_throw))
459  {
460  // Function is annotated must-not-throw, but we can't prove that here.
461  // Insert an ASSUME(@inflight_exception == null):
462  goto_program.insert_after(
463  instr_it,
464  goto_programt::make_assumption(no_exception_currently_in_flight));
465 
467  }
468  else
469  {
471  function_identifier, goto_program, instr_it, stack_catch, locals);
472 
473  // add a null check (so that instanceof can be applied)
474  goto_program.insert_after(
475  instr_it,
477  next_it,
478  no_exception_currently_in_flight,
479  instr_it->source_location));
480 
482  }
483  }
484 
486 }
487 
492  const irep_idt &function_identifier,
493  goto_programt &goto_program)
494 {
495  stack_catcht stack_catch; // stack of try-catch blocks
496  std::vector<std::vector<symbol_exprt>> stack_locals; // stack of local vars
497  std::vector<symbol_exprt> locals;
498 
499  if(goto_program.empty())
500  return;
501 
502  bool program_or_callees_may_throw =
503  function_or_callees_may_throw(goto_program);
504 
505  bool did_something = false;
506  bool added_goto_instruction = false;
507 
508  Forall_goto_program_instructions(instr_it, goto_program)
509  {
510  if(instr_it->is_decl())
511  {
512  locals.push_back(instr_it->decl_symbol());
513  }
514  // Is it a handler push/pop or catch landing-pad?
515  else if(instr_it->type==CATCH)
516  {
517  const irep_idt &statement = instr_it->get_code().get_statement();
518  // Is it an exception landing pad (start of a catch block)?
519  if(statement==ID_exception_landingpad)
520  {
522  goto_program, instr_it, program_or_callees_may_throw);
523  }
524  // Is it a catch handler pop?
525  else if(statement==ID_pop_catch)
526  {
527  // pop the local vars stack
528  if(!stack_locals.empty())
529  {
530  locals=stack_locals.back();
531  stack_locals.pop_back();
532  }
533  // pop from the stack if possible
534  if(!stack_catch.empty())
535  {
536  stack_catch.pop_back();
537  }
538  else
539  {
540 #ifdef DEBUG
541  std::cout << "Remove exceptions: empty stack\n";
542 #endif
543  }
544  }
545  // Is it a catch handler push?
546  else if(statement==ID_push_catch)
547  {
548  stack_locals.push_back(locals);
549  locals.clear();
550 
552  stack_catch.push_back(exception);
553  remove_exceptionst::catch_handlerst &last_exception=
554  stack_catch.back();
555 
556  // copy targets
557  const code_push_catcht::exception_listt &exception_list =
558  to_code_push_catch(instr_it->get_code()).exception_list();
559 
560  // The target list can be empty if `finish_catch_push_targets` found that
561  // the targets were unreachable (in which case no exception can truly
562  // be thrown at runtime)
563  INVARIANT(
564  instr_it->targets.empty() ||
565  exception_list.size()==instr_it->targets.size(),
566  "`exception_list` should contain current instruction's targets");
567 
568  // Fill the map with the catch type and the target
569  unsigned i=0;
570  for(auto target : instr_it->targets)
571  {
572  last_exception.push_back(
573  std::make_pair(exception_list[i].get_tag(), target));
574  i++;
575  }
576  }
577  else
578  {
579  INVARIANT(
580  false,
581  "CATCH opcode should be one of push-catch, pop-catch, landingpad");
582  }
583 
584  instr_it->turn_into_skip();
585  did_something = true;
586  }
587  else if(instr_it->type==THROW)
588  {
589  did_something = instrument_throw(
590  function_identifier, goto_program, instr_it, stack_catch, locals);
591  }
592  else if(instr_it->type==FUNCTION_CALL)
593  {
594  instrumentation_resultt result =
596  function_identifier, goto_program, instr_it, stack_catch, locals);
597  did_something = result != instrumentation_resultt::DID_NOTHING;
598  added_goto_instruction =
600  }
601  }
602 
603  // INITIALIZE_FUNCTION should not contain any exception handling branches for
604  // two reasons: (1) with symex-driven lazy loading it means that code that
605  // references @inflight_exception might be generated before
606  // @inflight_exception is initialized; (2) symex can analyze
607  // INITIALIZE_FUNCTION much faster if it doesn't contain any branching.
608  INVARIANT(
609  function_identifier != INITIALIZE_FUNCTION || !added_goto_instruction,
610  INITIALIZE_FUNCTION " should not contain any exception handling branches");
611 
612  if(did_something)
613  remove_skip(goto_program);
614 }
615 
617 {
618  for(auto &gf_entry : goto_functions.function_map)
619  instrument_exceptions(gf_entry.first, gf_entry.second.body);
620 }
621 
623 operator()(const irep_idt &function_identifier, goto_programt &goto_program)
624 {
625  instrument_exceptions(function_identifier, goto_program);
626 }
627 
630  symbol_table_baset &symbol_table,
631  goto_functionst &goto_functions,
632  message_handlert &message_handler)
633 {
634  const namespacet ns(symbol_table);
635  std::map<irep_idt, std::set<irep_idt>> exceptions_map;
636 
637  uncaught_exceptions(goto_functions, ns, exceptions_map);
638 
639  remove_exceptionst::function_may_throwt function_may_throw =
640  [&exceptions_map](const irep_idt &id) {
641  return !exceptions_map[id].empty();
642  };
643 
645  symbol_table, nullptr, function_may_throw, false, message_handler);
646 
647  remove_exceptions(goto_functions);
648 }
649 
663  const irep_idt &function_identifier,
664  goto_programt &goto_program,
665  symbol_table_baset &symbol_table,
666  message_handlert &message_handler)
667 {
668  remove_exceptionst::function_may_throwt any_function_may_throw =
669  [](const irep_idt &) { return true; };
670 
672  symbol_table, nullptr, any_function_may_throw, false, message_handler);
673 
674  remove_exceptions(function_identifier, goto_program);
675 }
676 
685  goto_modelt &goto_model,
686  message_handlert &message_handler)
687 {
689  goto_model.symbol_table, goto_model.goto_functions, message_handler);
690 }
691 
694  symbol_table_baset &symbol_table,
695  goto_functionst &goto_functions,
696  const class_hierarchyt &class_hierarchy,
697  message_handlert &message_handler)
698 {
699  const namespacet ns(symbol_table);
700  std::map<irep_idt, std::set<irep_idt>> exceptions_map;
701 
702  uncaught_exceptions(goto_functions, ns, exceptions_map);
703 
704  remove_exceptionst::function_may_throwt function_may_throw =
705  [&exceptions_map](const irep_idt &id) {
706  return !exceptions_map[id].empty();
707  };
708 
710  symbol_table, &class_hierarchy, function_may_throw, true, message_handler);
711 
712  remove_exceptions(goto_functions);
713 }
714 
730  const irep_idt &function_identifier,
731  goto_programt &goto_program,
732  symbol_table_baset &symbol_table,
733  const class_hierarchyt &class_hierarchy,
734  message_handlert &message_handler)
735 {
736  remove_exceptionst::function_may_throwt any_function_may_throw =
737  [](const irep_idt &) { return true; };
738 
740  symbol_table,
741  &class_hierarchy,
742  any_function_may_throw,
743  true,
744  message_handler);
745 
746  remove_exceptions(function_identifier, goto_program);
747 }
748 
759  goto_modelt &goto_model,
760  const class_hierarchyt &class_hierarchy,
761  message_handlert &message_handler)
762 {
764  goto_model.symbol_table,
765  goto_model.goto_functions,
766  class_hierarchy,
767  message_handler);
768 }
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
Non-graph-based representation of the class hierarchy.
A codet representing an assignment in the program.
Definition: std_code.h:293
const exprt & catch_expr() const
Definition: std_code.h:2394
std::vector< exception_list_entryt > exception_listt
Definition: std_code.h:2295
exception_listt & exception_list()
Definition: std_code.h:2306
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Equality.
Definition: std_expr.h:1225
Base class for all expressions.
Definition: expr.h:54
const source_locationt & source_location() const
Definition: expr.h:230
typet & type()
Return the type of the expression.
Definition: expr.h:82
A collection of goto functions.
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:71
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:963
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:652
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:985
instructionst::iterator targett
Definition: goto_program.h:646
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
targett get_end_function()
Get an instruction iterator pointing to the END_FUNCTION instruction of the goto program.
Definition: goto_program.h:854
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:722
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
bool empty() const
Is the program empty?
Definition: goto_program.h:826
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:58
const irep_idt & id() const
Definition: irep.h:407
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
The null pointer constant.
Definition: pointer_expr.h:703
Lowers high-level exception descriptions into low-level operations suitable for symex and other analy...
const class_hierarchyt * class_hierarchy
std::vector< catch_handlerst > stack_catcht
function_may_throwt function_may_throw
symbol_exprt get_inflight_exception_global()
Create a global named java::@inflight_exception that holds any exception that has been thrown but not...
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) ...
message_handlert & message_handler
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< std::pair< irep_idt, goto_programt::targett > > catch_handlerst
bool function_or_callees_may_throw(const goto_programt &) const
Checks whether a function may ever experience an exception (whether or not it catches),...
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....
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
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...
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
void instrument_exceptions(const irep_idt &function_identifier, goto_programt &goto_program)
instruments throws, function calls that may escape exceptions and exception handlers.
symbol_table_baset & symbol_table
void operator()(goto_functionst &goto_functions)
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:449
Expression to hold a symbol (variable)
Definition: std_expr.h:80
const irep_idt & get_identifier() const
Definition: std_expr.h:109
The symbol table base class interface.
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Symbol table entry.
Definition: symbol.h:28
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
typet type
Type of symbol.
Definition: symbol.h:31
The Boolean constant true.
Definition: std_expr.h:2802
Semantic type conversion.
Definition: std_expr.h:1866
static exprt get_exception_symbol(const exprt &exor)
Returns the symbol corresponding to an exception.
Symbol Table + CFG.
#define Forall_goto_program_instructions(it, program)
@ FUNCTION_CALL
Definition: goto_program.h:47
@ ASSIGN
Definition: goto_program.h:44
@ CATCH
Definition: goto_program.h:49
@ THROW
Definition: goto_program.h:48
dstringt irep_idt
Definition: irep.h:37
Java-specific exprt subclasses.
static irep_idt get_tag(const typet &type)
empty_typet java_void_type()
Definition: java_types.cpp:37
API to expression classes for Pointers.
void remove_exceptions_using_instanceof(symbol_table_baset &symbol_table, goto_functionst &goto_functions, message_handlert &message_handler)
removes throws/CATCH-POP/CATCH-PUSH
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 function exceptional returns.
#define INFLIGHT_EXCEPTION_VARIABLE_NAME
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...
Remove Instance-of Operators.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:86
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:510
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
#define INITIALIZE_FUNCTION
static code_landingpadt & to_code_landingpad(codet &code)
Definition: std_code.h:2418
static code_push_catcht & to_code_push_catch(codet &code)
Definition: std_code.h:2329
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
Author: Diffblue Ltd.
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.
Over-approximative uncaught exceptions analysis.