cprover
|
#include <util/symbol_table.h>
Go to the source code of this file.
Functions | |
void | convert_threadblock (symbol_tablet &symbol_table) |
Iterate through the symbol table to find and appropriately instrument thread-blocks. More... | |
void convert_threadblock | ( | symbol_tablet & | symbol_table | ) |
Iterate through the symbol table to find and appropriately instrument thread-blocks.
A thread block is a sequence of codet's surrounded with calls to CProver.startThread:(I)V and CProver.endThread:(I)V. A thread block corresponds to the body of the thread to be created. The only parameter accepted by these functions is an integer used to differentiate between different thread blocks. Function startThread() is transformed into a codet ID_start_thread, which carries a target label in the field 'destination'. Similarly endThread() is transformed into a codet ID_end_thread, which marks the end of the thread body. Both codet's will later be transformed (in goto_convertt) into the goto instructions START_THREAD and END_THREAD.
Additionally the variable __CPROVER__thread_id (thread local) will store the ID of the new thread. The new id is obtained by incrementing a global variable __CPROVER__next_thread_id.
The ID of the thread is made accessible to the Java program by having calls to the function 'CProver.getCurrentThreadID()I' replaced by the variable __CPROVER__thread_id. We also perform this substitution in here. The substitution that we perform here assumes that calls to getCurrentThreadID() are ONLY made in the RHS of an expression.
Example:
Is transformed into:
Observe that the semantics of ID_start_thread roughly corresponds to: fork the current thread, continue the execution of the current thread in the next line, and continue the execution of the new thread at the destination field of the codet (__CPROVER_THREAD_ENTRY_333).
Note: the current version assumes that a call to startThread(n), where n is an immediate integer, is in the same scope (nesting block) as a call to endThread(n). Some assertion will fail during symex if this is not the case.
Note': the ID of the thread is assigned after the thread is created, this creates bogus interleavings. Currently, it's not possible to assign the thread ID before the creation of the thead, due to a bug in symex. See https://github.com/diffblue/cbmc/issues/1630/for more details.
symbol_table | a symbol table |
Definition at line 291 of file java_bytecode_convert_threadblock.cpp.
References exprt::depth_begin(), exprt::depth_end(), expr2java(), code_function_callt::function(), codet::get_statement(), irept::id(), instrument_endThread(), instrument_getCurrentThreadID(), instrument_start_thread(), to_code(), to_code_function_call(), and symbolt::value.
Referenced by java_bytecode_languaget::typecheck().