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,
93  : symbol_table(_symbol_table),
94  function_may_throw(_function_may_throw),
97  {
98  }
99 
100  void operator()(goto_functionst &goto_functions);
102 
103 protected:
108 
110 
111  bool function_or_callees_may_throw(const goto_programt &) const;
112 
115  const goto_programt::targett &,
116  bool may_catch);
117 
119  const remove_exceptionst::stack_catcht &stack_catch,
121  std::size_t &universal_try,
122  std::size_t &universal_catch);
123 
126  const goto_programt::targett &instr_it,
127  const stack_catcht &stack_catch,
128  const std::vector<exprt> &locals);
129 
130  bool instrument_throw(
132  const goto_programt::targett &,
133  const stack_catcht &,
134  const std::vector<exprt> &);
135 
138  const goto_programt::targett &,
139  const stack_catcht &,
140  const std::vector<exprt> &);
141 
144 };
145 
149 {
150  const symbolt *existing_symbol =
152  INVARIANT(
153  existing_symbol != nullptr,
154  "Java frontend should have created @inflight_exception variable");
155  return existing_symbol->symbol_expr();
156 }
157 
164  const goto_programt &goto_program) const
165 {
167  {
168  if(instr_it->is_throw())
169  {
170  return true;
171  }
172 
173  if(instr_it->is_function_call())
174  {
175  const exprt &function_expr=
176  to_code_function_call(instr_it->code).function();
178  function_expr.id()==ID_symbol,
179  "identifier expected to be a symbol");
180  const irep_idt &function_name=
181  to_symbol_expr(function_expr).get_identifier();
182  if(function_may_throw(function_name))
183  return true;
184  }
185  }
186 
187  return false;
188 }
189 
202  const goto_programt::targett &instr_it,
203  bool may_catch)
204 {
205  PRECONDITION(instr_it->type==CATCH);
206 
207  if(may_catch)
208  {
209  // retrieve the exception variable
210  const exprt &thrown_exception_local=
211  to_code_landingpad(instr_it->code).catch_expr();
212 
213  const symbol_exprt thrown_global_symbol=
215  // next we reset the exceptional return to NULL
216  null_pointer_exprt null_voidptr((pointer_type(empty_typet())));
217 
218  // add the assignment @inflight_exception = NULL
220  t_null->make_assignment();
221  t_null->source_location=instr_it->source_location;
222  t_null->code=code_assignt(
223  thrown_global_symbol,
224  null_voidptr);
225  t_null->function=instr_it->function;
226 
227  // add the assignment exc = @inflight_exception (before the null assignment)
229  t_exc->make_assignment();
230  t_exc->source_location=instr_it->source_location;
231  t_exc->code=code_assignt(
232  thrown_exception_local,
233  typecast_exprt(thrown_global_symbol, thrown_exception_local.type()));
234  t_exc->function=instr_it->function;
235  }
236  instr_it->make_skip();
237 }
238 
261  const remove_exceptionst::stack_catcht &stack_catch,
263  std::size_t &universal_try,
264  std::size_t &universal_catch)
265 {
266  for(std::size_t i=stack_catch.size(); i>0;)
267  {
268  i--;
269  for(std::size_t j=0; j<stack_catch[i].size(); ++j)
270  {
271  if(stack_catch[i][j].first.empty())
272  {
273  // Record the position of the default behaviour as any further catches
274  // will not capture the throw
275  universal_try=i;
276  universal_catch=j;
277 
278  // Universal handler. Highest on the stack takes
279  // precedence, so overwrite any we've already seen:
280  return stack_catch[i][j].second;
281  }
282  }
283  }
284  // Unless we have a universal exception handler, jump to end of function
286 }
287 
299  const goto_programt::targett &instr_it,
300  const remove_exceptionst::stack_catcht &stack_catch,
301  const std::vector<exprt> &locals)
302 {
303  // Jump to the universal handler or function end, as appropriate.
304  // This will appear after the GOTO-based dynamic dispatch below
305  goto_programt::targett default_dispatch=goto_program.insert_after(instr_it);
306 
307  // find the symbol corresponding to the caught exceptions
308  symbol_exprt exc_thrown =
310 
311  std::size_t default_try=0;
312  std::size_t default_catch=(!stack_catch.empty()) ? stack_catch[0].size() : 0;
313 
314  goto_programt::targett default_target=
316  default_try, default_catch);
317 
318  // add GOTOs implementing the dynamic dispatch of the
319  // exception handlers.
320  // The first loop is in forward order because the insertion reverses the order
321  // we note that try1{ try2 {} catch2c {} catch2d {}} catch1a() {} catch1b{}
322  // must catch in the following order: 2c 2d 1a 1b hence the numerical index
323  // is reversed whereas the letter ordering remains the same.
324  for(std::size_t i=default_try; i<stack_catch.size(); i++)
325  {
326  for(std::size_t j=(i==default_try) ? default_catch : stack_catch[i].size();
327  j>0;)
328  {
329  j--;
330  goto_programt::targett new_state_pc=
331  stack_catch[i][j].second;
332  if(!stack_catch[i][j].first.empty())
333  {
334  // Normal exception handler, make an instanceof check.
336  t_exc->make_goto(new_state_pc);
337  t_exc->source_location=instr_it->source_location;
338  t_exc->function=instr_it->function;
339 
340  // use instanceof to check that this is the correct handler
341  symbol_typet type(stack_catch[i][j].first);
342  type_exprt expr(type);
343 
344  binary_predicate_exprt check(exc_thrown, ID_java_instanceof, expr);
345  t_exc->guard=check;
346 
349  }
350  }
351  }
352 
353  default_dispatch->make_goto(default_target);
354  default_dispatch->source_location=instr_it->source_location;
355  default_dispatch->function=instr_it->function;
356 
357  // add dead instructions
358  for(const auto &local : locals)
359  {
361  t_dead->make_dead();
362  t_dead->code=code_deadt(local);
363  t_dead->source_location=instr_it->source_location;
364  t_dead->function=instr_it->function;
365  }
366 }
367 
372  const goto_programt::targett &instr_it,
373  const remove_exceptionst::stack_catcht &stack_catch,
374  const std::vector<exprt> &locals)
375 {
376  PRECONDITION(instr_it->type==THROW);
377 
378  const exprt &exc_expr=
380 
382  goto_program, instr_it, stack_catch, locals);
383 
384  // find the symbol where the thrown exception should be stored:
385  symbol_exprt exc_thrown =
387 
388  // add the assignment with the appropriate cast
389  code_assignt assignment(
390  exc_thrown,
391  typecast_exprt(exc_expr, exc_thrown.type()));
392  // now turn the `throw' into `assignment'
393  instr_it->type=ASSIGN;
394  instr_it->code=assignment;
395 
396  return true;
397 }
398 
403  const goto_programt::targett &instr_it,
404  const stack_catcht &stack_catch,
405  const std::vector<exprt> &locals)
406 {
407  PRECONDITION(instr_it->type==FUNCTION_CALL);
408 
409  // save the address of the next instruction
410  goto_programt::targett next_it=instr_it;
411  next_it++;
412 
413  code_function_callt &function_call=to_code_function_call(instr_it->code);
415  function_call.function().id()==ID_symbol,
416  "identified expected to be a symbol");
417  const irep_idt &callee_id=
418  to_symbol_expr(function_call.function()).get_identifier();
419 
420  if(function_may_throw(callee_id))
421  {
422  equal_exprt no_exception_currently_in_flight(
425 
426  if(symbol_table.lookup_ref(callee_id).type.get_bool(ID_C_must_not_throw))
427  {
428  // Function is annotated must-not-throw, but we can't prove that here.
429  // Insert an ASSUME(@inflight_exception == null):
430  goto_programt::targett assume_null = goto_program.insert_after(instr_it);
431  assume_null->make_assumption(no_exception_currently_in_flight);
432  }
433  else
434  {
436  goto_program, instr_it, stack_catch, locals);
437 
438  // add a null check (so that instanceof can be applied)
440  t_null->make_goto(next_it);
441  t_null->source_location=instr_it->source_location;
442  t_null->function=instr_it->function;
443  t_null->guard=no_exception_currently_in_flight;
444  }
445 
446  return true;
447  }
448 
449  return false;
450 }
451 
457 {
458  stack_catcht stack_catch; // stack of try-catch blocks
459  std::vector<std::vector<exprt>> stack_locals; // stack of local vars
460  std::vector<exprt> locals;
461 
462  if(goto_program.empty())
463  return;
464 
465  bool program_or_callees_may_throw =
467 
468  bool did_something = false;
469 
471  {
472  if(instr_it->is_decl())
473  {
474  code_declt decl=to_code_decl(instr_it->code);
475  locals.push_back(decl.symbol());
476  }
477  // Is it a handler push/pop or catch landing-pad?
478  else if(instr_it->type==CATCH)
479  {
480  const irep_idt &statement=instr_it->code.get_statement();
481  // Is it an exception landing pad (start of a catch block)?
482  if(statement==ID_exception_landingpad)
483  {
485  goto_program, instr_it, program_or_callees_may_throw);
486  }
487  // Is it a catch handler pop?
488  else if(statement==ID_pop_catch)
489  {
490  // pop the local vars stack
491  if(!stack_locals.empty())
492  {
493  locals=stack_locals.back();
494  stack_locals.pop_back();
495  }
496  // pop from the stack if possible
497  if(!stack_catch.empty())
498  {
499  stack_catch.pop_back();
500  }
501  else
502  {
503 #ifdef DEBUG
504  std::cout << "Remove exceptions: empty stack\n";
505 #endif
506  }
507  }
508  // Is it a catch handler push?
509  else if(statement==ID_push_catch)
510  {
511  stack_locals.push_back(locals);
512  locals.clear();
513 
515  stack_catch.push_back(exception);
516  remove_exceptionst::catch_handlerst &last_exception=
517  stack_catch.back();
518 
519  // copy targets
520  const code_push_catcht::exception_listt &exception_list=
521  to_code_push_catch(instr_it->code).exception_list();
522 
523  // The target list can be empty if `finish_catch_push_targets` found that
524  // the targets were unreachable (in which case no exception can truly
525  // be thrown at runtime)
526  INVARIANT(
527  instr_it->targets.empty() ||
528  exception_list.size()==instr_it->targets.size(),
529  "`exception_list` should contain current instruction's targets");
530 
531  // Fill the map with the catch type and the target
532  unsigned i=0;
533  for(auto target : instr_it->targets)
534  {
535  last_exception.push_back(
536  std::make_pair(exception_list[i].get_tag(), target));
537  i++;
538  }
539  }
540  else
541  {
542  INVARIANT(
543  false,
544  "CATCH opcode should be one of push-catch, pop-catch, landingpad");
545  }
546  instr_it->make_skip();
547  did_something = true;
548  }
549  else if(instr_it->type==THROW)
550  {
551  did_something |=
552  instrument_throw(goto_program, instr_it, stack_catch, locals);
553  }
554  else if(instr_it->type==FUNCTION_CALL)
555  {
556  did_something |=
557  instrument_function_call(goto_program, instr_it, stack_catch, locals);
558  }
559  }
560 
561  if(did_something)
563 }
564 
566 {
567  Forall_goto_functions(it, goto_functions)
568  instrument_exceptions(it->second.body);
569 }
570 
572 {
574 }
575 
578  symbol_table_baset &symbol_table,
579  goto_functionst &goto_functions,
582 {
583  const namespacet ns(symbol_table);
584  std::map<irep_idt, std::set<irep_idt>> exceptions_map;
585  uncaught_exceptions(goto_functions, ns, exceptions_map);
586  remove_exceptionst::function_may_throwt function_may_throw =
587  [&exceptions_map](const irep_idt &id) {
588  return !exceptions_map[id].empty();
589  };
591  symbol_table,
592  function_may_throw,
595  remove_exceptions(goto_functions);
596 }
597 
614  symbol_table_baset &symbol_table,
617 {
618  remove_exceptionst::function_may_throwt any_function_may_throw =
619  [](const irep_idt &) { return true; };
620 
622  symbol_table,
623  any_function_may_throw,
627 }
628 
631  goto_modelt &goto_model,
634 {
636  goto_model.symbol_table, goto_model.goto_functions, message_handler, type);
637 }
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:291
std::vector< exception_list_entryt > exception_listt
Definition: std_code.h:1589
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:268
irep_idt get_tag(const typet &type)
remove_exceptions_typest
const irep_idt & get_identifier() const
Definition: std_expr.h:128
The null pointer constant.
Definition: std_expr.h:4518
An expression denoting a type.
Definition: std_expr.h:4408
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
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), 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:204
equality
Definition: std_expr.h:1354
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: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:254
static code_push_catcht & to_code_push_catch(codet &code)
Definition: std_code.h:1617
void remove_exceptions(symbol_table_baset &symbol_table, goto_functionst &goto_functions, message_handlert &message_handler, remove_exceptions_typest type)
removes throws/CATCH-POP/CATCH-PUSH
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
API to expression classes.
TO_BE_DOCUMENTED.
Definition: namespace.h:74
#define PRECONDITION(CONDITION)
Definition: invariant.h:242
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:858
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
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
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
void remove_instanceof(goto_programt::targett target, goto_programt &goto_program, symbol_table_baset &symbol_table, message_handlert &message_handler)
Replace an instanceof in the expression or guard of the passed instruction of the given function body...
typet type
Type of symbol.
Definition: symbol.h:34
static code_landingpadt & to_code_landingpad(codet &code)
Definition: std_code.h:1693
symbol_table_baset & symbol_table
std::function< bool(const irep_idt &)> function_may_throwt
exprt & function()
Definition: std_code.h:878
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:307
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:1675
goto_programt coverage_criteriont message_handlert & message_handler
Definition: cover.cpp:66
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:730
remove_exceptionst(symbol_table_baset &_symbol_table, function_may_throwt _function_may_throw, bool remove_added_instanceof, message_handlert &message_handler)
Program Transformation.
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:278
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:1600
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
std::vector< catch_handlerst > stack_catcht
Assignment.
Definition: std_code.h:196
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:909