cprover
java_bytecode_concurrency_instrumentation.h File Reference
#include <util/symbol_table.h>
#include <util/message.h>
Include dependency graph for java_bytecode_concurrency_instrumentation.h:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

## Functions

Iterate through the symbol table to find and appropriately instrument thread-blocks. More...

void convert_synchronized_methods (symbol_tablet &symbol_table, message_handlert &message_handler)
Iterate through the symbol table to find and instrument synchronized methods. More...

## ◆ convert_synchronized_methods()

 void convert_synchronized_methods ( symbol_tablet & 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 565 of file java_bytecode_concurrency_instrumentation.cpp.

 void convert_threadblock ( symbol_tablet & symbol_table )

Iterate through the symbol table to find and appropriately instrument thread-blocks.

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:

codet(id=ID_atomic_begin)