Lowers high-level exception descriptions into low-level operations suitable for symex and other analyses that don't understand the THROW or CATCH GOTO instructions. More...
Collaboration diagram for remove_exceptionst:Public Types | |
| typedef std::function< bool(const irep_idt &)> | function_may_throwt |
Public Member Functions | |
| 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) | |
| void | operator() (goto_functionst &goto_functions) |
| void | operator() (const irep_idt &function_identifier, goto_programt &goto_program) |
Protected Types | |
| enum class | instrumentation_resultt { DID_NOTHING , ADDED_CODE_WITHOUT_MAY_THROW , ADDED_CODE_WITH_MAY_THROW } |
Protected Member Functions | |
| symbol_exprt | get_inflight_exception_global () |
| Create a global named java::@inflight_exception that holds any exception that has been thrown but not yet caught. More... | |
| 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. More... | |
| 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 nominated expression, then clear the in-flight exception (i.e. More... | |
| 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.e. More... | |
| 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) then goto handlerB else goto universal_handler or (dead locals; function exit) More... | |
| 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 More... | |
| 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 exception handlers More... | |
| void | instrument_exceptions (const irep_idt &function_identifier, goto_programt &goto_program) |
| instruments throws, function calls that may escape exceptions and exception handlers. More... | |
Protected Attributes | |
| symbol_table_baset & | symbol_table |
| const class_hierarchyt * | class_hierarchy |
| function_may_throwt | function_may_throw |
| bool | remove_added_instanceof |
| message_handlert & | message_handler |
Private Types | |
| typedef std::vector< std::pair< irep_idt, goto_programt::targett > > | catch_handlerst |
| typedef std::vector< catch_handlerst > | stack_catcht |
Detailed Description
Lowers high-level exception descriptions into low-level operations suitable for symex and other analyses that don't understand the THROW or CATCH GOTO instructions.
The instructions affected by the lowering are:
THROW, whose operand must be a code_expressiont wrapping a side_effect_expr_throwt. This starts propagating an exception, aborting functions until a suitable catch point is found.
CATCH with a code_push_catcht operand, which commences a region in which exceptions should be caught, commonly a try block. It specifies one or more exception tags to handle (in instruction->code.exception_list()) and a corresponding GOTO program target for each (in instruction->targets). Thrown instructions are currently always matched to tags using java_instanceof, optionally lowered to a check on the @class_identifier field, so a language frontend wanting to use this class must use exceptions with a Java-compatible structure.
CATCH with a code_pop_catcht operand terminates a try-block begun by a code_push_catcht. At present the try block consists of the instructions between the push and the pop in program order, not according to dynamic control flow, so goto_convert_exceptions must ensure that control-flow within the try block does not leave this range.
CATCH with a code_landingpadt operand marks a point where exceptional control flow terminates and normal control flow resumes, typically the top of a catch or finally block, and the target of a code_push_catcht describing the correponding try block. It gives an lvalue expression that should be assigned the caught exception, typically a local variable.
FUNCTION_CALL instructions are also affected: if the callee may abort due to an escaping instruction, a dispatch sequence is inserted to check whether the callee aborted and propagate the exception further if so.
Exception propagation is implemented using a global variable per function (named function_name::exception_value) that carries a reference to an in-flight exception, or is null during normal control flow. THROW assigns it a reference to the thrown instance; CALL instructions copy between the exception_value for the callee and caller, catch_push and catch_pop instructions indicate how they should be checked to dispatch the right exception type to the right catch block, and landingpad instructions copy back to an ordinary local variable (or other expression) and set #exception_value back to null, indicating the exception has been caught and normal control flow resumed.
Definition at line 81 of file remove_exceptions.cpp.
Member Typedef Documentation
◆ catch_handlerst
|
private |
Definition at line 84 of file remove_exceptions.cpp.
◆ function_may_throwt
| typedef std::function<bool(const irep_idt &)> remove_exceptionst::function_may_throwt |
Definition at line 88 of file remove_exceptions.cpp.
◆ stack_catcht
|
private |
Definition at line 85 of file remove_exceptions.cpp.
Member Enumeration Documentation
◆ instrumentation_resultt
|
strongprotected |
| Enumerator | |
|---|---|
| DID_NOTHING | |
| ADDED_CODE_WITHOUT_MAY_THROW | |
| ADDED_CODE_WITH_MAY_THROW | |
Definition at line 122 of file remove_exceptions.cpp.
Constructor & Destructor Documentation
◆ remove_exceptionst()
|
inlineexplicit |
Definition at line 90 of file remove_exceptions.cpp.
Member Function Documentation
◆ add_exception_dispatch_sequence()
|
protected |
Emit the code: if (exception instanceof ExnA) then goto handlerA else if (exception instanceof ExnB) then goto handlerB else goto universal_handler or (dead locals; function exit)
- Parameters
-
function_identifier name of the function containing instr_itgoto_program body of the function to which instr_it belongs instr_it throw or call instruction that may be an exception source stack_catch exception handlers currently registered locals local variables to kill on a function-exit edge
Definition at line 320 of file remove_exceptions.cpp.
◆ find_universal_exception()
|
protected |
Find the innermost universal exception handler for the current program location which may throw (i.e.
the first catch of type any in the innermost try that contains such). We record this one because no handler after it can possibly catch. The context is contained in stack_catch which is a stack of all the tries which contain the current program location in their bodies. Each of these in turn contains a list of all possible catches for that try giving the type of exception they catch and the location of the handler. This function returns the indices of the try and the catch within that try as well as the location of the handler. The first loop is in forward order because the insertion reverses the order we note that try1{ try2 {} catch2c {} catch2d {}} catch1a() {} catch1b{} must catch in the following order: 2c 2d 1a 1b hence the numerical index is reversed whereas the letter ordering remains the same.
- Parameters
-
stack_catch exception table goto_program program being evaluated [out] universal_try returns the try block corresponding to the desired exception handler [out] universal_catch returns the catch block corresponding to the exception desired exception handler
- Returns
- the desired exception handler
Definition at line 282 of file remove_exceptions.cpp.
◆ function_or_callees_may_throw()
|
protected |
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.
- Parameters
-
goto_program program to check for throws and throwing calls
- Returns
- true if any throw or throwing call was found
Definition at line 187 of file remove_exceptions.cpp.
◆ get_inflight_exception_global()
|
protected |
Create a global named java::@inflight_exception that holds any exception that has been thrown but not yet caught.
Definition at line 172 of file remove_exceptions.cpp.
◆ instrument_exception_handler()
|
protected |
Translates an exception landing-pad into instructions that copy the in-flight exception pointer to a nominated expression, then clear the in-flight exception (i.e.
null the pointer), hence marking it caught.
- Parameters
-
[out] goto_program body of the function containing this landingpad instruction instr_it iterator pointing to the landingpad instruction. Will be overwritten. may_catch if true, an exception may be caught here; otherwise the catch site is unreachable. At present this will only be false if this function is known never to throw, and never to call functions that throw.
Definition at line 223 of file remove_exceptions.cpp.
◆ instrument_exceptions()
|
protected |
instruments throws, function calls that may escape exceptions and exception handlers.
Additionally, it re-computes the live-range of local variables in order to add DEAD instructions.
Definition at line 485 of file remove_exceptions.cpp.
◆ instrument_function_call()
|
protected |
instruments each function call that may escape exceptions with conditional GOTOS to the corresponding exception handlers
Definition at line 427 of file remove_exceptions.cpp.
◆ instrument_throw()
|
protected |
instruments each throw with conditional GOTOS to the corresponding exception handlers
Definition at line 396 of file remove_exceptions.cpp.
◆ operator()() [1/2]
| void remove_exceptionst::operator() | ( | const irep_idt & | function_identifier, |
| goto_programt & | goto_program | ||
| ) |
Definition at line 616 of file remove_exceptions.cpp.
◆ operator()() [2/2]
| void remove_exceptionst::operator() | ( | goto_functionst & | goto_functions | ) |
Definition at line 610 of file remove_exceptions.cpp.
Member Data Documentation
◆ class_hierarchy
|
protected |
Definition at line 117 of file remove_exceptions.cpp.
◆ function_may_throw
|
protected |
Definition at line 118 of file remove_exceptions.cpp.
◆ message_handler
|
protected |
Definition at line 120 of file remove_exceptions.cpp.
◆ remove_added_instanceof
|
protected |
Definition at line 119 of file remove_exceptions.cpp.
◆ symbol_table
|
protected |
Definition at line 116 of file remove_exceptions.cpp.
The documentation for this class was generated from the following file:
- /home/runner/work/cbmc/cbmc/jbmc/src/java_bytecode/remove_exceptions.cpp
