#include "java_bytecode_concurrency_instrumentation.h"
#include <util/arith_tools.h>
#include <util/cprover_prefix.h>
#include <util/expr_iterator.h>
#include <util/message.h>
#include <util/namespace.h>
#include <util/std_types.h>
#include <util/symbol_table_base.h>
#include "expr2java.h"
#include "java_types.h"
#include "java_utils.h"

Include dependency graph for java_bytecode_concurrency_instrumentation.cpp:

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

Definition at line 603 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 485 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_table	a symbol table
is_enter	indicates whether we are creating a monitorenter or monitorexit.
object	expression 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_code	function call to CProver.endThread:(I)V
[out]	code	resulting transformation
	symbol_table	a 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_code	function call to CProver.getCurrentThreadId:()I
[out]	code	resulting transformation
	symbol_table	a 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_code	call to CProver.getMonitorCount:(Ljava/lang/Object;)I
[out]	code	resulting transformation
	symbol_table	a 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_code	function call to CProver.startThread:(I)V
[out]	code	resulting transformation
	symbol_table	a 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_table	a symbol_table
symbol	writeable symbol hosting code to synchronize
sync_object	object 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]	code	current element to modify
	monitorexit	codet 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"

Definition at line 24 of file java_bytecode_concurrency_instrumentation.cpp.

◆ thread_id

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

Definition at line 25 of file java_bytecode_concurrency_instrumentation.cpp.

Functions

Variables

Function Documentation

◆ add_or_get_symbol()

◆ convert_synchronized_methods()

◆ convert_threadblock()

◆ get_first_label_id()

◆ get_monitor_call()

◆ get_second_label_id()

◆ get_thread_block_identifier()

◆ instrument_end_thread()

◆ instrument_get_current_thread_id()

◆ instrument_get_monitor_count()

◆ instrument_start_thread()

◆ instrument_synchronized_code()

◆ monitor_exits()

Variable Documentation

◆ next_thread_id

◆ thread_id