CBMC
java_bytecode_concurrency_instrumentation.cpp File Reference
+ Include dependency graph for java_bytecode_concurrency_instrumentation.cpp:

Go to the source code of this file.

Functions

static symbolt add_or_get_symbol (symbol_table_baset &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 codet get_monitor_call (const symbol_table_baset &symbol_table, bool is_enter, const exprt &object)
 Creates a monitorenter/monitorexit code_function_callt for the given synchronization object. More...
 
static void monitor_exits (codet &code, const codet &monitorexit)
 Introduces a monitorexit before every return recursively. More...
 
static void instrument_synchronized_code (symbol_table_baset &symbol_table, symbolt &symbol, const exprt &sync_object)
 Transforms the codet stored in symbol.value. More...
 
static void instrument_start_thread (const code_function_callt &f_code, codet &code, symbol_table_baset &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_end_thread (const code_function_callt &f_code, codet &code, const symbol_table_baset &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_get_current_thread_id (const code_function_callt &f_code, codet &code, symbol_table_baset &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...
 
static void instrument_get_monitor_count (const code_function_callt &f_code, codet &code, symbol_table_baset &symbol_table)
 Transforms the codet stored in in f_code, which is a call to function CProver.getMonitorCount:(Ljava/lang/Object;)I into a code_assignt that assigns the cproverMonitorCount field of the java.lang.Object argument passed to getMonitorCount. More...
 
void convert_threadblock (symbol_table_baset &symbol_table)
 Iterate through the symbol table to find and appropriately instrument thread-blocks. More...
 
void convert_synchronized_methods (symbol_table_baset &symbol_table, message_handlert &message_handler)
 Iterate through the symbol table to find and instrument synchronized methods. More...
 

Variables

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

Function Documentation

◆ add_or_get_symbol()

static symbolt add_or_get_symbol ( symbol_table_baset 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 36 of file java_bytecode_concurrency_instrumentation.cpp.

◆ convert_synchronized_methods()

void convert_synchronized_methods ( symbol_table_baset symbol_table,
message_handlert message_handler 
)

Iterate through the symbol table to find and instrument synchronized methods.

Synchronized methods make it impossible for two invocations of the same method on the same object to interleave. In-order to replicate these semantics a call to "java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V" and "java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V" is instrumented at the start and end of the method. Note, that the former is instrumented at every statement where the execution can exit the method in question. Specifically, out of order return statements and exceptions. The latter is dealt with by instrumenting a try catch block.

Note: Static synchronized methods are not supported yet as the synchronization semantics for static methods is different (locking on the class instead the of the object). Upon encountering a static synchronized method the current implementation will ignore the synchronized flag. (showing a warning in the process). This may result in superfluous interleavings.

Note': This method requires the availability of "java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V" and "java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V". (java-library-models). If they are not available code_skipt will inserted instead of calls to the aforementioned methods.

Parameters
symbol_tablea symbol table
message_handlerstatus output

Definition at line 602 of file java_bytecode_concurrency_instrumentation.cpp.

◆ convert_threadblock()

void convert_threadblock ( symbol_table_baset 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)
Data structure for representing an arbitrary statement in a program.
Definition: std_code_base.h:29

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 thread, 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 484 of file java_bytecode_concurrency_instrumentation.cpp.

◆ 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 66 of file java_bytecode_concurrency_instrumentation.cpp.

◆ get_monitor_call()

static codet get_monitor_call ( const symbol_table_baset symbol_table,
bool  is_enter,
const exprt object 
)
static

Creates a monitorenter/monitorexit code_function_callt for the given synchronization object.

Parameters
symbol_tablea symbol table
is_enterindicates whether we are creating a monitorenter or monitorexit.
objectexpression representing a 'java.Lang.Object'. This object is used to achieve object-level locking by calling monitoroenter/monitorexit.

Definition at line 101 of file java_bytecode_concurrency_instrumentation.cpp.

◆ 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 75 of file java_bytecode_concurrency_instrumentation.cpp.

◆ 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 84 of file java_bytecode_concurrency_instrumentation.cpp.

◆ instrument_end_thread()

static void instrument_end_thread ( const code_function_callt f_code,
codet code,
const symbol_table_baset 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 339 of file java_bytecode_concurrency_instrumentation.cpp.

◆ instrument_get_current_thread_id()

static void instrument_get_current_thread_id ( const code_function_callt f_code,
codet code,
symbol_table_baset 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 373 of file java_bytecode_concurrency_instrumentation.cpp.

◆ instrument_get_monitor_count()

static void instrument_get_monitor_count ( const code_function_callt f_code,
codet code,
symbol_table_baset symbol_table 
)
static

Transforms the codet stored in in f_code, which is a call to function CProver.getMonitorCount:(Ljava/lang/Object;)I into a code_assignt that assigns the cproverMonitorCount field of the java.lang.Object argument passed to getMonitorCount.

The resulting codet is stored in the output parameter code.

Parameters
f_codecall to CProver.getMonitorCount:(Ljava/lang/Object;)I
[out]coderesulting transformation
symbol_tablea symbol table

Definition at line 404 of file java_bytecode_concurrency_instrumentation.cpp.

◆ instrument_start_thread()

static void instrument_start_thread ( const code_function_callt f_code,
codet code,
symbol_table_baset 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 269 of file java_bytecode_concurrency_instrumentation.cpp.

◆ instrument_synchronized_code()

static void instrument_synchronized_code ( symbol_table_baset symbol_table,
symbolt symbol,
const exprt sync_object 
)
static

Transforms the codet stored in symbol.value.

The symbol is expected to be a Java synchronized method. Java synchronized methods do not have explicit calls to the instructions monitorenter and monitorexit, the JVM interprets the synchronized flag in a method and uses monitor of the object to implement locking and unlocking. Therefore JBMC has to emulate this same behavior. We insert a call to our model of monitorenter at the beginning of the method and calls to our model of monitorexit at each return instruction. We wrap the entire body of the method with an exception handler that will call our model of monitorexit if the method returns exceptionally.

Example:

synchronized int amethod(int p)
{
int x = 0;
if(p == 0)
return -1;
x = p / 10
return x
}

Is transformed into the codet equivalent of:

synchronized int amethod(int p)
{
try
{
java::java.lang.Object.monitorenter(this);
int x = 0;
if(p == 0)
{
java::java.lang.Object.monitorexit(this);
return -1;
}
java::java.lang.Object.monitorexit(this);
return x
}
catch(java::java.lang.Throwable e)
{
// catch every exception, including errors!
java::java.lang.Object.monitorexit(this);
throw e;
}
}
Parameters
symbol_tablea symbol_table
symbolwriteable symbol hosting code to synchronize
sync_objectobject to use as a lock

Definition at line 206 of file java_bytecode_concurrency_instrumentation.cpp.

◆ monitor_exits()

static void monitor_exits ( codet code,
const codet monitorexit 
)
static

Introduces a monitorexit before every return recursively.

Note: this breaks sharing on code

Parameters
[out]codecurrent element to modify
monitorexitcodet to insert before the return

Definition at line 133 of file java_bytecode_concurrency_instrumentation.cpp.

Variable Documentation

◆ next_thread_id

const std::string next_thread_id = "__CPROVER_" "_next_thread_id"

◆ thread_id

const std::string thread_id = "__CPROVER_" "_thread_id"