cprover
|
#include "java_bytecode_convert_threadblock.h"
#include "expr2java.h"
#include "java_types.h"
#include <util/expr_iterator.h>
#include <util/namespace.h>
#include <util/cprover_prefix.h>
#include <util/std_types.h>
#include <util/arith_tools.h>
Go to the source code of this file.
Functions | |
static symbolt | add_or_get_symbol (symbol_tablet &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 void | instrument_start_thread (const code_function_callt &f_code, codet &code, symbol_tablet &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_endThread (const code_function_callt &f_code, codet &code, symbol_tablet 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_getCurrentThreadID (const code_function_callt &f_code, codet &code, symbol_tablet 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... | |
void | convert_threadblock (symbol_tablet &symbol_table) |
Iterate through the symbol table to find and appropriately instrument thread-blocks. More... | |
Variables | |
const std::string | next_thread_id = CPROVER_PREFIX "_next_thread_id" |
const std::string | thread_id = CPROVER_PREFIX "_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 32 of file java_bytecode_convert_threadblock.cpp.
References symbol_table_baset::add(), symbolt::base_name, symbolt::is_lvalue, symbolt::is_state_var, symbolt::is_static_lifetime, symbolt::is_thread_local, namespacet::lookup(), symbolt::mode, symbolt::name, symbolt::pretty_name, symbolt::type, and symbolt::value.
Referenced by instrument_getCurrentThreadID(), and instrument_start_thread().
void convert_threadblock | ( | symbol_tablet & | 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 thead, 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 291 of file java_bytecode_convert_threadblock.cpp.
References exprt::depth_begin(), exprt::depth_end(), expr2java(), code_function_callt::function(), codet::get_statement(), irept::id(), instrument_endThread(), instrument_getCurrentThreadID(), instrument_start_thread(), to_code(), to_code_function_call(), and symbolt::value.
Referenced by java_bytecode_languaget::typecheck().
|
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 65 of file java_bytecode_convert_threadblock.cpp.
References CPROVER_PREFIX.
Referenced by instrument_start_thread().
|
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 74 of file java_bytecode_convert_threadblock.cpp.
References CPROVER_PREFIX.
Referenced by instrument_endThread(), and instrument_start_thread().
|
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 83 of file java_bytecode_convert_threadblock.cpp.
References code_function_callt::arguments(), binary2integer(), integer2string(), and PRECONDITION.
Referenced by instrument_endThread(), and instrument_start_thread().
|
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 173 of file java_bytecode_convert_threadblock.cpp.
References code_blockt::add(), exprt::add_source_location(), code_function_callt::arguments(), get_second_label_id(), get_thread_block_identifier(), exprt::op0(), PRECONDITION, and exprt::source_location().
Referenced by convert_threadblock().
|
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 210 of file java_bytecode_convert_threadblock.cpp.
References add_or_get_symbol(), exprt::add_source_location(), code_function_callt::arguments(), from_integer(), java_int_type(), code_function_callt::lhs(), PRECONDITION, exprt::source_location(), and thread_id.
Referenced by convert_threadblock().
|
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 101 of file java_bytecode_convert_threadblock.cpp.
References code_blockt::add(), add_or_get_symbol(), code_function_callt::arguments(), exprt::copy_to_operands(), from_integer(), get_first_label_id(), get_second_label_id(), get_thread_block_identifier(), java_int_type(), next_thread_id, exprt::op0(), PRECONDITION, irept::set(), exprt::source_location(), symbolt::symbol_expr(), and thread_id.
Referenced by convert_threadblock().
const std::string next_thread_id = CPROVER_PREFIX "_next_thread_id" |
Definition at line 20 of file java_bytecode_convert_threadblock.cpp.
Referenced by instrument_start_thread(), and memory_model_sct::thread_spawn().
const std::string thread_id = CPROVER_PREFIX "_thread_id" |
Definition at line 21 of file java_bytecode_convert_threadblock.cpp.
Referenced by instrument_getCurrentThreadID(), and instrument_start_thread().