CBMC
|
#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"
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" |
|
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.
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.
symbol_table | a symbol table |
message_handler | status output |
Definition at line 602 of file java_bytecode_concurrency_instrumentation.cpp.
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:
Is transformed into:
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.
symbol_table | a symbol table |
Definition at line 484 of file java_bytecode_concurrency_instrumentation.cpp.
|
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.
|
static |
Creates a monitorenter/monitorexit code_function_callt for the given synchronization object.
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.
|
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.
|
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.
|
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
.
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.
|
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
.
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.
|
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
.
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.
|
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
.
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.
|
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:
Is transformed into the codet equivalent of:
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.
Introduces a monitorexit before every return recursively.
Note: this breaks sharing on code
[out] | code | current element to modify |
monitorexit | codet to insert before the return |
Definition at line 133 of file java_bytecode_concurrency_instrumentation.cpp.
const std::string next_thread_id = "__CPROVER_" "_next_thread_id" |
Definition at line 24 of file java_bytecode_concurrency_instrumentation.cpp.
const std::string thread_id = "__CPROVER_" "_thread_id" |
Definition at line 25 of file java_bytecode_concurrency_instrumentation.cpp.