cprover
Loading...
Searching...
No Matches
remove_exceptions.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Remove exception handling
4
5Author: Cristina David
6
7Date: 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
90public:
91 typedef std::function<bool(const irep_idt &)> function_may_throwt;
92
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
118protected:
124
131
133
135
137 goto_programt &goto_program,
139 bool may_catch);
140
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,
152 const std::vector<symbol_exprt> &locals);
153
154 bool instrument_throw(
155 const irep_idt &function_identifier,
156 goto_programt &goto_program,
158 const stack_catcht &,
159 const std::vector<symbol_exprt> &);
160
162 const irep_idt &function_identifier,
163 goto_programt &goto_program,
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();
205 "identifier expected to be a symbol");
206 const irep_idt &function_name=
208 if(function_may_throw(function_name))
209 return true;
210 }
211 }
212
213 return false;
214}
215
227 goto_programt &goto_program,
229 bool may_catch)
230{
231 PRECONDITION(instr_it->type() == CATCH);
232
233 if(may_catch)
234 {
235 // retrieve the exception variable
237 to_code_landingpad(instr_it->get_code()).catch_expr();
238
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,
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,
258 instr_it->source_location()));
259 }
260
261 instr_it->turn_into_skip();
262}
263
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
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,
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
333
334 // find the symbol corresponding to the caught exceptions
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=
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--;
358 stack_catch[i][j].second;
359 if(!stack_catch[i][j].first.empty())
360 {
361 // Normal exception handler, make an instanceof check.
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
371 t_exc->guard=check;
372
374 {
376 function_identifier,
377 t_exc,
378 goto_program,
382 }
383 }
384 }
385 }
386
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,
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:
418
419 // now turn the `throw' into an assignment with the appropriate cast
423 instr_it->source_location());
424
425 return true;
426}
427
432 const irep_idt &function_identifier,
433 goto_programt &goto_program,
436 const std::vector<symbol_exprt> &locals)
437{
439
440 // save the address of the next instruction
442 next_it++;
443
444 const auto &function = instr_it->call_function();
445
447 function.id() == ID_symbol, "function call expected to be a symbol");
448 const irep_idt &callee_id = to_symbol_expr(function).get_identifier();
449
451 {
455
457 {
458 // Function is annotated must-not-throw, but we can't prove that here.
459 // Insert an ASSUME(@inflight_exception == null):
460 goto_program.insert_after(
461 instr_it,
463
465 }
466 else
467 {
469 function_identifier, goto_program, instr_it, stack_catch, locals);
470
471 // add a null check (so that instanceof can be applied)
472 goto_program.insert_after(
473 instr_it,
475 next_it,
477 instr_it->source_location()));
478
480 }
481 }
482
484}
485
490 const irep_idt &function_identifier,
491 goto_programt &goto_program)
492{
493 stack_catcht stack_catch; // stack of try-catch blocks
494 std::vector<std::vector<symbol_exprt>> stack_locals; // stack of local vars
495 std::vector<symbol_exprt> locals;
496
497 if(goto_program.empty())
498 return;
499
501 function_or_callees_may_throw(goto_program);
502
503 bool did_something = false;
504 bool added_goto_instruction = false;
505
507 {
508 if(instr_it->is_decl())
509 {
510 locals.push_back(instr_it->decl_symbol());
511 }
512 // Is it a handler push/pop or catch landing-pad?
513 else if(instr_it->type() == CATCH)
514 {
515 const irep_idt &statement = instr_it->get_code().get_statement();
516 // Is it an exception landing pad (start of a catch block)?
517 if(statement==ID_exception_landingpad)
518 {
521 }
522 // Is it a catch handler pop?
523 else if(statement==ID_pop_catch)
524 {
525 // pop the local vars stack
526 if(!stack_locals.empty())
527 {
528 locals=stack_locals.back();
529 stack_locals.pop_back();
530 }
531 // pop from the stack if possible
532 if(!stack_catch.empty())
533 {
534 stack_catch.pop_back();
535 }
536 else
537 {
538#ifdef DEBUG
539 std::cout << "Remove exceptions: empty stack\n";
540#endif
541 }
542 }
543 // Is it a catch handler push?
544 else if(statement==ID_push_catch)
545 {
546 stack_locals.push_back(locals);
547 locals.clear();
548
550 stack_catch.push_back(exception);
552 stack_catch.back();
553
554 // copy targets
555 const code_push_catcht::exception_listt &exception_list =
556 to_code_push_catch(instr_it->get_code()).exception_list();
557
558 // The target list can be empty if `finish_catch_push_targets` found that
559 // the targets were unreachable (in which case no exception can truly
560 // be thrown at runtime)
561 INVARIANT(
562 instr_it->targets.empty() ||
563 exception_list.size()==instr_it->targets.size(),
564 "`exception_list` should contain current instruction's targets");
565
566 // Fill the map with the catch type and the target
567 unsigned i=0;
568 for(auto target : instr_it->targets)
569 {
570 last_exception.push_back(
571 std::make_pair(exception_list[i].get_tag(), target));
572 i++;
573 }
574 }
575 else
576 {
577 INVARIANT(
578 false,
579 "CATCH opcode should be one of push-catch, pop-catch, landingpad");
580 }
581
582 instr_it->turn_into_skip();
583 did_something = true;
584 }
585 else if(instr_it->type() == THROW)
586 {
588 function_identifier, goto_program, instr_it, stack_catch, locals);
589 }
590 else if(instr_it->type() == FUNCTION_CALL)
591 {
594 function_identifier, goto_program, instr_it, stack_catch, locals);
598 }
599 }
600
601 // INITIALIZE_FUNCTION should not contain any exception handling branches for
602 // two reasons: (1) with symex-driven lazy loading it means that code that
603 // references @inflight_exception might be generated before
604 // @inflight_exception is initialized; (2) symex can analyze
605 // INITIALIZE_FUNCTION much faster if it doesn't contain any branching.
606 INVARIANT(
607 function_identifier != INITIALIZE_FUNCTION || !added_goto_instruction,
608 INITIALIZE_FUNCTION " should not contain any exception handling branches");
609
610 if(did_something)
611 remove_skip(goto_program);
612}
613
615{
616 for(auto &gf_entry : goto_functions.function_map)
617 instrument_exceptions(gf_entry.first, gf_entry.second.body);
618}
619
621operator()(const irep_idt &function_identifier, goto_programt &goto_program)
622{
623 instrument_exceptions(function_identifier, goto_program);
624}
625
628 symbol_table_baset &symbol_table,
629 goto_functionst &goto_functions,
630 message_handlert &message_handler)
631{
632 const namespacet ns(symbol_table);
633 std::map<irep_idt, std::set<irep_idt>> exceptions_map;
634
635 uncaught_exceptions(goto_functions, ns, exceptions_map);
636
637 remove_exceptionst::function_may_throwt function_may_throw =
638 [&exceptions_map](const irep_idt &id) {
639 return !exceptions_map[id].empty();
640 };
641
643 symbol_table, nullptr, function_may_throw, false, message_handler);
644
645 remove_exceptions(goto_functions);
646}
647
661 const irep_idt &function_identifier,
662 goto_programt &goto_program,
663 symbol_table_baset &symbol_table,
664 message_handlert &message_handler)
665{
667 [](const irep_idt &) { return true; };
668
670 symbol_table, nullptr, any_function_may_throw, false, message_handler);
671
672 remove_exceptions(function_identifier, goto_program);
673}
674
683 goto_modelt &goto_model,
684 message_handlert &message_handler)
685{
687 goto_model.symbol_table, goto_model.goto_functions, message_handler);
688}
689
692 symbol_table_baset &symbol_table,
693 goto_functionst &goto_functions,
694 const class_hierarchyt &class_hierarchy,
695 message_handlert &message_handler)
696{
697 const namespacet ns(symbol_table);
698 std::map<irep_idt, std::set<irep_idt>> exceptions_map;
699
700 uncaught_exceptions(goto_functions, ns, exceptions_map);
701
702 remove_exceptionst::function_may_throwt function_may_throw =
703 [&exceptions_map](const irep_idt &id) {
704 return !exceptions_map[id].empty();
705 };
706
708 symbol_table, &class_hierarchy, function_may_throw, true, message_handler);
709
710 remove_exceptions(goto_functions);
711}
712
728 const irep_idt &function_identifier,
729 goto_programt &goto_program,
730 symbol_table_baset &symbol_table,
731 const class_hierarchyt &class_hierarchy,
732 message_handlert &message_handler)
733{
735 [](const irep_idt &) { return true; };
736
738 symbol_table,
739 &class_hierarchy,
741 true,
742 message_handler);
743
744 remove_exceptions(function_identifier, goto_program);
745}
746
757 goto_modelt &goto_model,
758 const class_hierarchyt &class_hierarchy,
759 message_handlert &message_handler)
760{
762 goto_model.symbol_table,
763 goto_model.goto_functions,
764 class_hierarchy,
765 message_handler);
766}
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:253
virtual void clear()
Reset the abstract state.
Definition ai.h:267
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
Non-graph-based representation of the class hierarchy.
A codet representing an assignment in the program.
std::vector< exception_list_entryt > exception_listt
Definition std_code.h:1849
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
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.
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
instructionst instructions
The list of instructions in the goto program.
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
instructionst::iterator targett
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.
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
bool empty() const
Is the program empty?
bool get_bool(const irep_idt &name) const
Definition irep.cpp:58
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.
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
typet type
Type of symbol.
Definition symbol.h:31
The Boolean constant true.
Definition std_expr.h:2856
Semantic type conversion.
Definition std_expr.h:1920
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
@ CATCH
@ THROW
dstringt irep_idt
Definition irep.h:37
Java-specific exprt subclasses.
static irep_idt get_tag(const typet &type)
empty_typet java_void_type()
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
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 INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
#define INITIALIZE_FUNCTION
static code_push_catcht & to_code_push_catch(codet &code)
Definition std_code.h:1883
static code_landingpadt & to_code_landingpad(codet &code)
Definition std_code.h:1972
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.