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  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 =
203  to_code_function_call(instruction.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  locals.push_back(instr_it->decl_symbol());
516  }
517  // Is it a handler push/pop or catch landing-pad?
518  else if(instr_it->type==CATCH)
519  {
520  const irep_idt &statement=instr_it->code.get_statement();
521  // Is it an exception landing pad (start of a catch block)?
522  if(statement==ID_exception_landingpad)
523  {
525  goto_program, instr_it, program_or_callees_may_throw);
526  }
527  // Is it a catch handler pop?
528  else if(statement==ID_pop_catch)
529  {
530  // pop the local vars stack
531  if(!stack_locals.empty())
532  {
533  locals=stack_locals.back();
534  stack_locals.pop_back();
535  }
536  // pop from the stack if possible
537  if(!stack_catch.empty())
538  {
539  stack_catch.pop_back();
540  }
541  else
542  {
543 #ifdef DEBUG
544  std::cout << "Remove exceptions: empty stack\n";
545 #endif
546  }
547  }
548  // Is it a catch handler push?
549  else if(statement==ID_push_catch)
550  {
551  stack_locals.push_back(locals);
552  locals.clear();
553 
555  stack_catch.push_back(exception);
556  remove_exceptionst::catch_handlerst &last_exception=
557  stack_catch.back();
558 
559  // copy targets
560  const code_push_catcht::exception_listt &exception_list=
561  to_code_push_catch(instr_it->code).exception_list();
562 
563  // The target list can be empty if `finish_catch_push_targets` found that
564  // the targets were unreachable (in which case no exception can truly
565  // be thrown at runtime)
566  INVARIANT(
567  instr_it->targets.empty() ||
568  exception_list.size()==instr_it->targets.size(),
569  "`exception_list` should contain current instruction's targets");
570 
571  // Fill the map with the catch type and the target
572  unsigned i=0;
573  for(auto target : instr_it->targets)
574  {
575  last_exception.push_back(
576  std::make_pair(exception_list[i].get_tag(), target));
577  i++;
578  }
579  }
580  else
581  {
582  INVARIANT(
583  false,
584  "CATCH opcode should be one of push-catch, pop-catch, landingpad");
585  }
586 
587  instr_it->turn_into_skip();
588  did_something = true;
589  }
590  else if(instr_it->type==THROW)
591  {
592  did_something = instrument_throw(
593  function_identifier, goto_program, instr_it, stack_catch, locals);
594  }
595  else if(instr_it->type==FUNCTION_CALL)
596  {
597  instrumentation_resultt result =
599  function_identifier, goto_program, instr_it, stack_catch, locals);
600  did_something = result != instrumentation_resultt::DID_NOTHING;
601  added_goto_instruction =
603  }
604  }
605 
606  // INITIALIZE_FUNCTION should not contain any exception handling branches for
607  // two reasons: (1) with symex-driven lazy loading it means that code that
608  // references @inflight_exception might be generated before
609  // @inflight_exception is initialized; (2) symex can analyze
610  // INITIALIZE_FUNCTION much faster if it doesn't contain any branching.
611  INVARIANT(
612  function_identifier != INITIALIZE_FUNCTION || !added_goto_instruction,
613  INITIALIZE_FUNCTION " should not contain any exception handling branches");
614 
615  if(did_something)
616  remove_skip(goto_program);
617 }
618 
620 {
621  for(auto &gf_entry : goto_functions.function_map)
622  instrument_exceptions(gf_entry.first, gf_entry.second.body);
623 }
624 
626 operator()(const irep_idt &function_identifier, goto_programt &goto_program)
627 {
628  instrument_exceptions(function_identifier, goto_program);
629 }
630 
633  symbol_table_baset &symbol_table,
634  goto_functionst &goto_functions,
635  message_handlert &message_handler)
636 {
637  const namespacet ns(symbol_table);
638  std::map<irep_idt, std::set<irep_idt>> exceptions_map;
639 
640  uncaught_exceptions(goto_functions, ns, exceptions_map);
641 
642  remove_exceptionst::function_may_throwt function_may_throw =
643  [&exceptions_map](const irep_idt &id) {
644  return !exceptions_map[id].empty();
645  };
646 
648  symbol_table, nullptr, function_may_throw, false, message_handler);
649 
650  remove_exceptions(goto_functions);
651 }
652 
666  const irep_idt &function_identifier,
667  goto_programt &goto_program,
668  symbol_table_baset &symbol_table,
669  message_handlert &message_handler)
670 {
671  remove_exceptionst::function_may_throwt any_function_may_throw =
672  [](const irep_idt &) { return true; };
673 
675  symbol_table, nullptr, any_function_may_throw, false, message_handler);
676 
677  remove_exceptions(function_identifier, goto_program);
678 }
679 
688  goto_modelt &goto_model,
689  message_handlert &message_handler)
690 {
692  goto_model.symbol_table, goto_model.goto_functions, message_handler);
693 }
694 
697  symbol_table_baset &symbol_table,
698  goto_functionst &goto_functions,
699  const class_hierarchyt &class_hierarchy,
700  message_handlert &message_handler)
701 {
702  const namespacet ns(symbol_table);
703  std::map<irep_idt, std::set<irep_idt>> exceptions_map;
704 
705  uncaught_exceptions(goto_functions, ns, exceptions_map);
706 
707  remove_exceptionst::function_may_throwt function_may_throw =
708  [&exceptions_map](const irep_idt &id) {
709  return !exceptions_map[id].empty();
710  };
711 
713  symbol_table, &class_hierarchy, function_may_throw, true, message_handler);
714 
715  remove_exceptions(goto_functions);
716 }
717 
733  const irep_idt &function_identifier,
734  goto_programt &goto_program,
735  symbol_table_baset &symbol_table,
736  const class_hierarchyt &class_hierarchy,
737  message_handlert &message_handler)
738 {
739  remove_exceptionst::function_may_throwt any_function_may_throw =
740  [](const irep_idt &) { return true; };
741 
743  symbol_table,
744  &class_hierarchy,
745  any_function_may_throw,
746  true,
747  message_handler);
748 
749  remove_exceptions(function_identifier, goto_program);
750 }
751 
762  goto_modelt &goto_model,
763  const class_hierarchyt &class_hierarchy,
764  message_handlert &message_handler)
765 {
767  goto_model.symbol_table,
768  goto_model.goto_functions,
769  class_hierarchy,
770  message_handler);
771 }
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:1172
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:898
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:632
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
remove_exceptionst::operator()
void operator()(goto_functionst &goto_functions)
Definition: remove_exceptions.cpp:619
goto_programt::empty
bool empty() const
Is the program empty?
Definition: goto_program.h:733
exprt
Base class for all expressions.
Definition: expr.h:54
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:498
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:37
remove_exceptionst::class_hierarchy
const class_hierarchyt * class_hierarchy
Definition: remove_exceptions.cpp:120
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:81
equal_exprt
Equality.
Definition: std_expr.h:1140
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:995
goto_programt::make_goto
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:969
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:51
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
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:1215
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:2751
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:696
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:110
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:2308
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:190
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:407
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:1326
std_code.h
code_landingpadt::catch_expr
const exprt & catch_expr() const
Definition: std_code.h:2396
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:761
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:556
ASSIGN
@ ASSIGN
Definition: goto_program.h:47
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:2420
CATCH
@ CATCH
Definition: goto_program.h:52
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:2297
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:50
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:74
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:626
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:876
remove_exceptionst::function_may_throwt
std::function< bool(const irep_idt &)> function_may_throwt
Definition: remove_exceptions.cpp:91
static_lifetime_init.h
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
java_types.h
symbol_table.h
Author: Diffblue Ltd.
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:1781
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:2717
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:234
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:550
code_function_callt::function
exprt & function()
Definition: std_code.h:1250
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
to_code_push_catch
static code_push_catcht & to_code_push_catch(codet &code)
Definition: std_code.h:2331
get_tag
static irep_idt get_tag(const typet &type)
Definition: java_string_library_preprocess.cpp:41