This graph shows which files directly or indirectly include this file:

Functions
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...

Function Documentation

◆ 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_table	a symbol table
message_handler	status 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)

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_table a symbol table

Definition at line 484 of file java_bytecode_concurrency_instrumentation.cpp.

Functions

Function Documentation

◆ convert_synchronized_methods()

◆ convert_threadblock()