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 
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  forall_goto_program_instructions(instr_it, goto_program)
194  {
195  if(instr_it->is_throw())
196  {
197  return true;
198  }
199 
200  if(instr_it->is_function_call())
201  {
202  const exprt &function_expr=
203  to_code_function_call(instr_it->code).function();
205  function_expr.id()==ID_symbol,
206  "identifier expected to be a symbol");
207  const irep_idt &function_name=
208  to_symbol_expr(function_expr).get_identifier();
209  if(function_may_throw(function_name))
210  return true;
211  }
212  }
213 
214  return false;
215 }
216 
228  goto_programt &goto_program,
229  const goto_programt::targett &instr_it,
230  bool may_catch)
231 {
232  PRECONDITION(instr_it->type==CATCH);
233 
234  if(may_catch)
235  {
236  // retrieve the exception variable
237  const exprt &thrown_exception_local=
238  to_code_landingpad(instr_it->code).catch_expr();
239 
240  const symbol_exprt thrown_global_symbol=
242  // next we reset the exceptional return to NULL
244 
245  // add the assignment @inflight_exception = NULL
246  goto_program.insert_after(
247  instr_it,
249  code_assignt(thrown_global_symbol, null_voidptr),
250  instr_it->source_location));
251 
252  // add the assignment exc = @inflight_exception (before the null assignment)
253  goto_program.insert_after(
254  instr_it,
256  code_assignt(
257  thrown_exception_local,
258  typecast_exprt(thrown_global_symbol, thrown_exception_local.type())),
259  instr_it->source_location));
260  }
261 
262  instr_it->turn_into_skip();
263 }
264 
287  const remove_exceptionst::stack_catcht &stack_catch,
288  goto_programt &goto_program,
289  std::size_t &universal_try,
290  std::size_t &universal_catch)
291 {
292  for(std::size_t i=stack_catch.size(); i>0;)
293  {
294  i--;
295  for(std::size_t j=0; j<stack_catch[i].size(); ++j)
296  {
297  if(stack_catch[i][j].first.empty())
298  {
299  // Record the position of the default behaviour as any further catches
300  // will not capture the throw
301  universal_try=i;
302  universal_catch=j;
303 
304  // Universal handler. Highest on the stack takes
305  // precedence, so overwrite any we've already seen:
306  return stack_catch[i][j].second;
307  }
308  }
309  }
310  // Unless we have a universal exception handler, jump to end of function
311  return goto_program.get_end_function();
312 }
313 
325  const irep_idt &function_identifier,
326  goto_programt &goto_program,
327  const goto_programt::targett &instr_it,
328  const remove_exceptionst::stack_catcht &stack_catch,
329  const std::vector<symbol_exprt> &locals)
330 {
331  // Jump to the universal handler or function end, as appropriate.
332  // This will appear after the GOTO-based dynamic dispatch below
333  goto_programt::targett default_dispatch=goto_program.insert_after(instr_it);
334 
335  // find the symbol corresponding to the caught exceptions
336  symbol_exprt exc_thrown =
338 
339  std::size_t default_try=0;
340  std::size_t default_catch=(!stack_catch.empty()) ? stack_catch[0].size() : 0;
341 
342  goto_programt::targett default_target=
343  find_universal_exception(stack_catch, goto_program,
344  default_try, default_catch);
345 
346  // add GOTOs implementing the dynamic dispatch of the
347  // exception handlers.
348  // The first loop is in forward order because the insertion reverses the order
349  // we note that try1{ try2 {} catch2c {} catch2d {}} catch1a() {} catch1b{}
350  // must catch in the following order: 2c 2d 1a 1b hence the numerical index
351  // is reversed whereas the letter ordering remains the same.
352  for(std::size_t i=default_try; i<stack_catch.size(); i++)
353  {
354  for(std::size_t j=(i==default_try) ? default_catch : stack_catch[i].size();
355  j>0;)
356  {
357  j--;
358  goto_programt::targett new_state_pc=
359  stack_catch[i][j].second;
360  if(!stack_catch[i][j].first.empty())
361  {
362  // Normal exception handler, make an instanceof check.
363  goto_programt::targett t_exc = goto_program.insert_after(
364  instr_it,
366  new_state_pc, true_exprt(), instr_it->source_location));
367 
368  // use instanceof to check that this is the correct handler
369  struct_tag_typet type(stack_catch[i][j].first);
370 
371  java_instanceof_exprt check(exc_thrown, type);
372  t_exc->guard=check;
373 
375  {
377  function_identifier,
378  t_exc,
379  goto_program,
380  symbol_table,
383  }
384  }
385  }
386  }
387 
388  *default_dispatch = goto_programt::make_goto(
389  default_target, true_exprt(), instr_it->source_location);
390 
391  // add dead instructions
392  for(const auto &local : locals)
393  {
394  goto_program.insert_after(
395  instr_it, goto_programt::make_dead(local, instr_it->source_location));
396  }
397 }
398 
402  const irep_idt &function_identifier,
403  goto_programt &goto_program,
404  const goto_programt::targett &instr_it,
405  const remove_exceptionst::stack_catcht &stack_catch,
406  const std::vector<symbol_exprt> &locals)
407 {
408  PRECONDITION(instr_it->type==THROW);
409 
410  const exprt &exc_expr=
412 
414  function_identifier, goto_program, instr_it, stack_catch, locals);
415 
416  // find the symbol where the thrown exception should be stored:
417  symbol_exprt exc_thrown =
419 
420  // add the assignment with the appropriate cast
421  code_assignt assignment(
422  exc_thrown,
423  typecast_exprt(exc_expr, exc_thrown.type()));
424  // now turn the `throw' into `assignment'
425  instr_it->type=ASSIGN;
426  instr_it->code=assignment;
427 
428  return true;
429 }
430 
435  const irep_idt &function_identifier,
436  goto_programt &goto_program,
437  const goto_programt::targett &instr_it,
438  const stack_catcht &stack_catch,
439  const std::vector<symbol_exprt> &locals)
440 {
441  PRECONDITION(instr_it->type==FUNCTION_CALL);
442 
443  // save the address of the next instruction
444  goto_programt::targett next_it=instr_it;
445  next_it++;
446 
447  const code_function_callt &function_call = instr_it->get_function_call();
448 
450  function_call.function().id()==ID_symbol,
451  "identified expected to be a symbol");
452  const irep_idt &callee_id=
453  to_symbol_expr(function_call.function()).get_identifier();
454 
455  if(function_may_throw(callee_id))
456  {
457  equal_exprt no_exception_currently_in_flight(
460 
461  if(symbol_table.lookup_ref(callee_id).type.get_bool(ID_C_must_not_throw))
462  {
463  // Function is annotated must-not-throw, but we can't prove that here.
464  // Insert an ASSUME(@inflight_exception == null):
465  goto_program.insert_after(
466  instr_it,
467  goto_programt::make_assumption(no_exception_currently_in_flight));
468 
470  }
471  else
472  {
474  function_identifier, goto_program, instr_it, stack_catch, locals);
475 
476  // add a null check (so that instanceof can be applied)
477  goto_program.insert_after(
478  instr_it,
480  next_it,
481  no_exception_currently_in_flight,
482  instr_it->source_location));
483 
485  }
486  }
487 
489 }
490 
495  const irep_idt &function_identifier,
496  goto_programt &goto_program)
497 {
498  stack_catcht stack_catch; // stack of try-catch blocks
499  std::vector<std::vector<symbol_exprt>> stack_locals; // stack of local vars
500  std::vector<symbol_exprt> locals;
501 
502  if(goto_program.empty())
503  return;
504 
505  bool program_or_callees_may_throw =
506  function_or_callees_may_throw(goto_program);
507 
508  bool did_something = false;
509  bool added_goto_instruction = false;
510 
511  Forall_goto_program_instructions(instr_it, goto_program)
512  {
513  if(instr_it->is_decl())
514  {
515  code_declt decl = instr_it->get_decl();
516  locals.push_back(decl.symbol());
517  }
518  // Is it a handler push/pop or catch landing-pad?
519  else if(instr_it->type==CATCH)
520  {
521  const irep_idt &statement=instr_it->code.get_statement();
522  // Is it an exception landing pad (start of a catch block)?
523  if(statement==ID_exception_landingpad)
524  {
526  goto_program, instr_it, program_or_callees_may_throw);
527  }
528  // Is it a catch handler pop?
529  else if(statement==ID_pop_catch)
530  {
531  // pop the local vars stack
532  if(!stack_locals.empty())
533  {
534  locals=stack_locals.back();
535  stack_locals.pop_back();
536  }
537  // pop from the stack if possible
538  if(!stack_catch.empty())
539  {
540  stack_catch.pop_back();
541  }
542  else
543  {
544 #ifdef DEBUG
545  std::cout << "Remove exceptions: empty stack\n";
546 #endif
547  }
548  }
549  // Is it a catch handler push?
550  else if(statement==ID_push_catch)
551  {
552  stack_locals.push_back(locals);
553  locals.clear();
554 
556  stack_catch.push_back(exception);
557  remove_exceptionst::catch_handlerst &last_exception=
558  stack_catch.back();
559 
560  // copy targets
561  const code_push_catcht::exception_listt &exception_list=
562  to_code_push_catch(instr_it->code).exception_list();
563 
564  // The target list can be empty if `finish_catch_push_targets` found that
565  // the targets were unreachable (in which case no exception can truly
566  // be thrown at runtime)
567  INVARIANT(
568  instr_it->targets.empty() ||
569  exception_list.size()==instr_it->targets.size(),
570  "`exception_list` should contain current instruction's targets");
571 
572  // Fill the map with the catch type and the target
573  unsigned i=0;
574  for(auto target : instr_it->targets)
575  {
576  last_exception.push_back(
577  std::make_pair(exception_list[i].get_tag(), target));
578  i++;
579  }
580  }
581  else
582  {
583  INVARIANT(
584  false,
585  "CATCH opcode should be one of push-catch, pop-catch, landingpad");
586  }
587 
588  instr_it->turn_into_skip();
589  did_something = true;
590  }
591  else if(instr_it->type==THROW)
592  {
593  did_something = instrument_throw(
594  function_identifier, goto_program, instr_it, stack_catch, locals);
595  }
596  else if(instr_it->type==FUNCTION_CALL)
597  {
598  instrumentation_resultt result =
600  function_identifier, goto_program, instr_it, stack_catch, locals);
601  did_something = result != instrumentation_resultt::DID_NOTHING;
602  added_goto_instruction =
604  }
605  }
606 
607  // INITIALIZE_FUNCTION should not contain any exception handling branches for
608  // two reasons: (1) with symex-driven lazy loading it means that code that
609  // references @inflight_exception might be generated before
610  // @inflight_exception is initialized; (2) symex can analyze
611  // INITIALIZE_FUNCTION much faster if it doesn't contain any branching.
612  INVARIANT(
613  function_identifier != INITIALIZE_FUNCTION || !added_goto_instruction,
614  INITIALIZE_FUNCTION " should not contain any exception handling branches");
615 
616  if(did_something)
617  remove_skip(goto_program);
618 }
619 
621 {
622  Forall_goto_functions(it, goto_functions)
623  instrument_exceptions(it->first, it->second.body);
624 }
625 
627 operator()(const irep_idt &function_identifier, goto_programt &goto_program)
628 {
629  instrument_exceptions(function_identifier, goto_program);
630 }
631 
634  symbol_table_baset &symbol_table,
635  goto_functionst &goto_functions,
636  message_handlert &message_handler)
637 {
638  const namespacet ns(symbol_table);
639  std::map<irep_idt, std::set<irep_idt>> exceptions_map;
640 
641  uncaught_exceptions(goto_functions, ns, exceptions_map);
642 
643  remove_exceptionst::function_may_throwt function_may_throw =
644  [&exceptions_map](const irep_idt &id) {
645  return !exceptions_map[id].empty();
646  };
647 
649  symbol_table, nullptr, function_may_throw, false, message_handler);
650 
651  remove_exceptions(goto_functions);
652 }
653 
667  const irep_idt &function_identifier,
668  goto_programt &goto_program,
669  symbol_table_baset &symbol_table,
670  message_handlert &message_handler)
671 {
672  remove_exceptionst::function_may_throwt any_function_may_throw =
673  [](const irep_idt &) { return true; };
674 
676  symbol_table, nullptr, any_function_may_throw, false, message_handler);
677 
678  remove_exceptions(function_identifier, goto_program);
679 }
680 
689  goto_modelt &goto_model,
690  message_handlert &message_handler)
691 {
693  goto_model.symbol_table, goto_model.goto_functions, message_handler);
694 }
695 
698  symbol_table_baset &symbol_table,
699  goto_functionst &goto_functions,
700  const class_hierarchyt &class_hierarchy,
701  message_handlert &message_handler)
702 {
703  const namespacet ns(symbol_table);
704  std::map<irep_idt, std::set<irep_idt>> exceptions_map;
705 
706  uncaught_exceptions(goto_functions, ns, exceptions_map);
707 
708  remove_exceptionst::function_may_throwt function_may_throw =
709  [&exceptions_map](const irep_idt &id) {
710  return !exceptions_map[id].empty();
711  };
712 
714  symbol_table, &class_hierarchy, function_may_throw, true, message_handler);
715 
716  remove_exceptions(goto_functions);
717 }
718 
734  const irep_idt &function_identifier,
735  goto_programt &goto_program,
736  symbol_table_baset &symbol_table,
737  const class_hierarchyt &class_hierarchy,
738  message_handlert &message_handler)
739 {
740  remove_exceptionst::function_may_throwt any_function_may_throw =
741  [](const irep_idt &) { return true; };
742 
744  symbol_table,
745  &class_hierarchy,
746  any_function_may_throw,
747  true,
748  message_handler);
749 
750  remove_exceptions(function_identifier, goto_program);
751 }
752 
763  goto_modelt &goto_model,
764  const class_hierarchyt &class_hierarchy,
765  message_handlert &message_handler)
766 {
768  goto_model.symbol_table,
769  goto_model.goto_functions,
770  class_hierarchy,
771  message_handler);
772 }
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:1201
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
symbol_table_baset::lookup_ref
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:104
class_hierarchyt
Non-graph-based representation of the class hierarchy.
Definition: class_hierarchy.h:43
remove_exceptionst::remove_exceptionst
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)
Definition: remove_exceptions.cpp:93
goto_programt::make_dead
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:927
remove_exceptions_using_instanceof
void remove_exceptions_using_instanceof(symbol_table_baset &symbol_table, goto_functionst &goto_functions, message_handlert &message_handler)
removes throws/CATCH-POP/CATCH-PUSH
Definition: remove_exceptions.cpp:633
remove_exceptionst::stack_catcht
std::vector< catch_handlerst > stack_catcht
Definition: remove_exceptions.cpp:88
remove_exceptionst::function_or_callees_may_throw
bool function_or_callees_may_throw(const goto_programt &) const
Checks whether a function may ever experience an exception (whether or not it catches),...
Definition: remove_exceptions.cpp:190
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
remove_exceptionst::remove_added_instanceof
bool remove_added_instanceof
Definition: remove_exceptions.cpp:122
remove_skip
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:85
remove_exceptionst::instrumentation_resultt::ADDED_CODE_WITH_MAY_THROW
@ ADDED_CODE_WITH_MAY_THROW
code_declt
A codet representing the declaration of a local variable.
Definition: std_code.h:402
remove_exceptionst::operator()
void operator()(goto_functionst &goto_functions)
Definition: remove_exceptions.cpp:620
goto_programt::empty
bool empty() const
Is the program empty?
Definition: goto_program.h:762
exprt
Base class for all expressions.
Definition: expr.h:53
goto_modelt
Definition: goto_model.h:26
struct_tag_typet
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:490
remove_exceptionst::instrument_throw
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
Definition: remove_exceptions.cpp:401
java_expr.h
Java-specific exprt subclasses.
irep_idt
dstringt irep_idt
Definition: irep.h:32
remove_exceptionst::class_hierarchy
const class_hierarchyt * class_hierarchy
Definition: remove_exceptions.cpp:120
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
equal_exprt
Equality.
Definition: std_expr.h:1190
remove_exceptionst::instrumentation_resultt::ADDED_CODE_WITHOUT_MAY_THROW
@ ADDED_CODE_WITHOUT_MAY_THROW
goto_programt::make_assignment
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
Definition: goto_program.h:1024
goto_programt::make_goto
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:998
remove_instanceof
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...
Definition: remove_instanceof.cpp:299
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
THROW
@ THROW
Definition: goto_program.h:50
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
remove_exceptionst::instrumentation_resultt
instrumentation_resultt
Definition: remove_exceptions.cpp:126
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1183
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
remove_exceptionst::add_exception_dispatch_sequence
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) ...
Definition: remove_exceptions.cpp:324
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
null_pointer_exprt
The null pointer constant.
Definition: std_expr.h:3989
remove_exceptions
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
Definition: remove_exceptions.cpp:697
remove_exceptionst::find_universal_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....
Definition: remove_exceptions.cpp:286
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:22
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
INFLIGHT_EXCEPTION_VARIABLE_NAME
#define INFLIGHT_EXCEPTION_VARIABLE_NAME
Definition: remove_exceptions.h:23
INITIALIZE_FUNCTION
#define INITIALIZE_FUNCTION
Definition: static_lifetime_init.h:23
code_push_catcht::exception_list
exception_listt & exception_list()
Definition: std_code.h:2303
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
remove_exceptionst::function_may_throw
function_may_throwt function_may_throw
Definition: remove_exceptions.cpp:121
irept::id
const irep_idt & id() const
Definition: irep.h:418
message_handlert
Definition: message.h:28
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1294
std_code.h
code_declt::symbol
symbol_exprt & symbol()
Definition: std_code.h:408
code_landingpadt::catch_expr
const exprt & catch_expr() const
Definition: std_code.h:2391
Forall_goto_functions
#define Forall_goto_functions(it, functions)
Definition: goto_functions.h:117
remove_exceptions.h
Remove function exceptional returns.
uncaught_exceptions_domaint::get_exception_symbol
static exprt get_exception_symbol(const exprt &exor)
Returns the symbol corresponding to an exception.
Definition: uncaught_exceptions_analysis.cpp:29
remove_instanceof.h
Remove Instance-of Operators.
goto_programt::get_end_function
targett get_end_function()
Get an instruction iterator pointing to the END_FUNCTION instruction of the goto program.
Definition: goto_program.h:790
ASSIGN
@ ASSIGN
Definition: goto_program.h:46
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
remove_exceptionst::catch_handlerst
std::vector< std::pair< irep_idt, goto_programt::targett > > catch_handlerst
Definition: remove_exceptions.cpp:87
uncaught_exceptions
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.
Definition: uncaught_exceptions_analysis.cpp:249
to_code_landingpad
static code_landingpadt & to_code_landingpad(codet &code)
Definition: std_code.h:2415
CATCH
@ CATCH
Definition: goto_program.h:51
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
remove_exceptionst::instrument_exception_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 ...
Definition: remove_exceptions.cpp:227
code_push_catcht::exception_listt
std::vector< exception_list_entryt > exception_listt
Definition: std_code.h:2292
symbolt
Symbol table entry.
Definition: symbol.h:28
uncaught_exceptions_analysis.h
Over-approximative uncaught exceptions analysis.
remove_exceptionst::instrument_function_call
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...
Definition: remove_exceptions.cpp:434
FUNCTION_CALL
@ FUNCTION_CALL
Definition: goto_program.h:49
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
goto_programt::insert_after
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:655
symbol_table_baset::lookup
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:95
remove_exceptionst::symbol_table
symbol_table_baset & symbol_table
Definition: remove_exceptions.cpp:119
goto_programt::make_assumption
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:905
remove_exceptionst::function_may_throwt
std::function< bool(const irep_idt &)> function_may_throwt
Definition: remove_exceptions.cpp:91
static_lifetime_init.h
java_types.h
symbol_table.h
Author: Diffblue Ltd.
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2013
remove_skip.h
Program Transformation.
java_void_type
empty_typet java_void_type()
Definition: java_types.cpp:38
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
true_exprt
The Boolean constant true.
Definition: std_expr.h:3955
remove_exceptionst::instrumentation_resultt::DID_NOTHING
@ DID_NOTHING
remove_exceptionst::get_inflight_exception_global
symbol_exprt get_inflight_exception_global()
Create a global named java::@inflight_exception that holds any exception that has been thrown but not...
Definition: remove_exceptions.cpp:175
std_expr.h
API to expression classes.
remove_exceptionst::message_handler
message_handlert & message_handler
Definition: remove_exceptions.cpp:123
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:254
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
c_types.h
remove_exceptionst::instrument_exceptions
void instrument_exceptions(const irep_idt &function_identifier, goto_programt &goto_program)
instruments throws, function calls that may escape exceptions and exception handlers.
Definition: remove_exceptions.cpp:494
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:579
code_function_callt::function
exprt & function()
Definition: std_code.h:1218
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:1196
remove_exceptionst
Lowers high-level exception descriptions into low-level operations suitable for symex and other analy...
Definition: remove_exceptions.cpp:85
java_instanceof_exprt
Definition: java_expr.h:18
validation_modet::INVARIANT
@ INVARIANT
to_code_push_catch
static code_push_catcht & to_code_push_catch(codet &code)
Definition: std_code.h:2326
get_tag
static irep_idt get_tag(const typet &type)
Definition: java_string_library_preprocess.cpp:38