cprover
java_bytecode_convert_threadblock.cpp File Reference
Include dependency graph for java_bytecode_convert_threadblock.cpp:

Go to the source code of this file.

Functions

static symbolt add_or_get_symbol (symbol_tablet &symbol_table, const irep_idt &name, const irep_idt &base_name, const typet &type, const exprt &value, const bool is_thread_local, const bool is_static_lifetime)
 Adds a new symbol to the symbol table if it doesn't exist. More...
 
static const std::string get_first_label_id (const std::string &id)
 Retrieve the first label identifier. More...
 
static const std::string get_second_label_id (const std::string &id)
 Retrieve the second label identifier. More...
 
static const std::string get_thread_block_identifier (const code_function_callt &f_code)
 Retrieves a thread block identifier from a function call to CProver.startThread:(I)V or CProver.endThread:(I)V /param code: function call to CProver.startThread or CProver.endThread /return: unique thread block identifier. More...
 
static void instrument_start_thread (const code_function_callt &f_code, codet &code, symbol_tablet &symbol_table)
 Transforms the codet stored in in f_code, which is a call to function CProver.startThread:(I)V into a block of code as described by the documentation of function convert_thread_block. More...
 
static void instrument_endThread (const code_function_callt &f_code, codet &code, symbol_tablet symbol_table)
 Transforms the codet stored in in f_code, which is a call to function CProver.endThread:(I)V into a block of code as described by the documentation of the function convert_thread_block. More...
 
static void instrument_getCurrentThreadID (const code_function_callt &f_code, codet &code, symbol_tablet symbol_table)
 Transforms the codet stored in in f_code, which is a call to function CProver.getCurrentThreadID:()I into a code_assignt as described by the documentation of the function convert_thread_block. More...
 
void convert_threadblock (symbol_tablet &symbol_table)
 Iterate through the symbol table to find and appropriately instrument thread-blocks. More...
 

Variables

const std::string next_thread_id = CPROVER_PREFIX "_next_thread_id"
 
const std::string thread_id = CPROVER_PREFIX "_thread_id"
 

Function Documentation

◆ add_or_get_symbol()

static symbolt add_or_get_symbol ( symbol_tablet symbol_table,
const irep_idt name,
const irep_idt base_name,
const typet type,
const exprt value,
const bool  is_thread_local,
const bool  is_static_lifetime 
)
static

Adds a new symbol to the symbol table if it doesn't exist.

Otherwise, returns the existing one. /param name: name of the symbol to be generated /param base_name: base name of the symbol to be generated /param type: type of the symbol to be generated /param value: initial value of the symbol to be generated /param is_thread_local: if true this symbol will be set as thread local /param is_static_lifetime: if true this symbol will be set as static /return returns new or existing symbol.

Definition at line 32 of file java_bytecode_convert_threadblock.cpp.

References symbol_table_baset::add(), symbolt::base_name, symbolt::is_lvalue, symbolt::is_state_var, symbolt::is_static_lifetime, symbolt::is_thread_local, namespacet::lookup(), symbolt::mode, symbolt::name, symbolt::pretty_name, symbolt::type, and symbolt::value.

Referenced by instrument_getCurrentThreadID(), and instrument_start_thread().

◆ convert_threadblock()

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:

CProver.startThread(333)
... // thread body
CProver.endThread(333)

Is transformed into:

codet(id=ID_start_thread, destination=__CPROVER_THREAD_ENTRY_333)
codet(id=ID_goto, destination=__CPROVER_THREAD_EXIT_333)
codet(id=ID_label, label=__CPROVER_THREAD_ENTRY_333)
codet(id=ID_atomic_begin)
__CPROVER__next_thread_id += 1;
__CPROVER__thread_id = __CPROVER__next_thread_id;
... // thread body
codet(id=ID_end_thread)
codet(id=ID_label, label=__CPROVER_THREAD_EXIT_333)

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.

Parameters
symbol_tablea 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().

◆ get_first_label_id()

static const std::string get_first_label_id ( const std::string &  id)
static

Retrieve the first label identifier.

This is used to mark the start of a thread block. /param id: unique thread block identifier /return: fully qualified label identifier

Definition at line 65 of file java_bytecode_convert_threadblock.cpp.

References CPROVER_PREFIX.

Referenced by instrument_start_thread().

◆ get_second_label_id()

static const std::string get_second_label_id ( const std::string &  id)
static

Retrieve the second label identifier.

This is used to mark the end of a thread block. /param id: unique thread block identifier /return: fully qualified label identifier

Definition at line 74 of file java_bytecode_convert_threadblock.cpp.

References CPROVER_PREFIX.

Referenced by instrument_endThread(), and instrument_start_thread().

◆ get_thread_block_identifier()

static const std::string get_thread_block_identifier ( const code_function_callt f_code)
static

Retrieves a thread block identifier from a function call to CProver.startThread:(I)V or CProver.endThread:(I)V /param code: function call to CProver.startThread or CProver.endThread /return: unique thread block identifier.

Definition at line 83 of file java_bytecode_convert_threadblock.cpp.

References code_function_callt::arguments(), binary2integer(), integer2string(), and PRECONDITION.

Referenced by instrument_endThread(), and instrument_start_thread().

◆ instrument_endThread()

static void instrument_endThread ( const code_function_callt f_code,
codet code,
symbol_tablet  symbol_table 
)
static

Transforms the codet stored in in f_code, which is a call to function CProver.endThread:(I)V into a block of code as described by the documentation of the function convert_thread_block.

The resulting code_blockt is stored in the output parameter code.

Parameters
f_codefunction call to CProver.endThread:(I)V
[out]coderesulting transformation
symbol_tablea symbol table

Definition at line 173 of file java_bytecode_convert_threadblock.cpp.

References code_blockt::add(), exprt::add_source_location(), code_function_callt::arguments(), get_second_label_id(), get_thread_block_identifier(), exprt::op0(), PRECONDITION, and exprt::source_location().

Referenced by convert_threadblock().

◆ instrument_getCurrentThreadID()

static void instrument_getCurrentThreadID ( const code_function_callt f_code,
codet code,
symbol_tablet  symbol_table 
)
static

Transforms the codet stored in in f_code, which is a call to function CProver.getCurrentThreadID:()I into a code_assignt as described by the documentation of the function convert_thread_block.

The resulting code_blockt is stored in the output parameter code.

Parameters
f_codefunction call to CProver.getCurrentThreadID:()I
[out]coderesulting transformation
symbol_tablea symbol table

Definition at line 210 of file java_bytecode_convert_threadblock.cpp.

References add_or_get_symbol(), exprt::add_source_location(), code_function_callt::arguments(), from_integer(), java_int_type(), code_function_callt::lhs(), PRECONDITION, exprt::source_location(), and thread_id.

Referenced by convert_threadblock().

◆ instrument_start_thread()

static void instrument_start_thread ( const code_function_callt f_code,
codet code,
symbol_tablet symbol_table 
)
static

Transforms the codet stored in in f_code, which is a call to function CProver.startThread:(I)V into a block of code as described by the documentation of function convert_thread_block.

The resulting code_blockt is stored in the output parameter code.

Parameters
f_codefunction call to CProver.startThread:(I)V
[out]coderesulting transformation
symbol_tablea symbol table

Definition at line 101 of file java_bytecode_convert_threadblock.cpp.

References code_blockt::add(), add_or_get_symbol(), code_function_callt::arguments(), exprt::copy_to_operands(), from_integer(), get_first_label_id(), get_second_label_id(), get_thread_block_identifier(), java_int_type(), next_thread_id, exprt::op0(), PRECONDITION, irept::set(), exprt::source_location(), symbolt::symbol_expr(), and thread_id.

Referenced by convert_threadblock().

Variable Documentation

◆ next_thread_id

const std::string next_thread_id = CPROVER_PREFIX "_next_thread_id"

◆ thread_id

const std::string thread_id = CPROVER_PREFIX "_thread_id"