Go to the documentation of this file.
39 const bool is_thread_local,
40 const bool is_static_lifetime)
42 const symbolt *psymbol =
nullptr;
45 if(psymbol !=
nullptr)
48 new_symbol.
name = name;
51 new_symbol.
type = type;
52 new_symbol.
value = value;
57 new_symbol.
mode = ID_java;
58 symbol_table.
add(new_symbol);
107 is_enter ?
"java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V"
108 :
"java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V";
110 auto it = symbol_table.
symbols.find(symbol);
122 if(it == symbol_table.
symbols.end())
136 if(statement == ID_return)
142 statement == ID_label || statement == ID_block ||
143 statement == ID_decl_block)
209 const exprt &sync_object)
222 irep_idt handler(
"pc-synchronized-catch");
226 exception_list.push_back(
235 "caught-synchronized-exception",
242 codet catch_instruction = catch_statement;
245 catch_block.
add(catch_instruction);
246 catch_block.
add(monitorexit);
257 code =
code_blockt({monitorenter, catch_push, code, catch_pop, catch_label});
290 const symbolt ¤t_symbol =
311 codet tmp_a(ID_start_thread);
312 tmp_a.
set(ID_destination, lbl1);
323 codet(ID_atomic_begin),
326 codet(ID_atomic_end)});
356 codet tmp_a(ID_end_thread);
380 const symbolt& current_symbol =
456 using instrument_callbackt =
458 using expr_replacement_mapt =
459 std::unordered_map<const exprt, instrument_callbackt, irep_hash>;
463 for(
const auto &entry : symbol_table)
465 expr_replacement_mapt expr_replacement_map;
466 const symbolt &symbol = entry.second;
474 instrument_callbackt cb;
476 const exprt &expr = *it;
477 if(expr.
id() != ID_code)
486 if(f_name ==
"org.cprover.CProver.startThread:(I)V")
489 std::placeholders::_1,
490 std::placeholders::_2,
491 std::placeholders::_3);
492 else if(f_name ==
"org.cprover.CProver.endThread:(I)V")
495 std::placeholders::_1,
496 std::placeholders::_2,
497 std::placeholders::_3);
498 else if(f_name ==
"org.cprover.CProver.getCurrentThreadID:()I")
501 std::placeholders::_1,
502 std::placeholders::_2,
503 std::placeholders::_3);
506 expr_replacement_map.insert({expr, cb});
509 if(!expr_replacement_map.empty())
511 symbolt &w_symbol = symbol_table.get_writeable_ref(entry.first);
518 expr_replacement_mapt::iterator m_it = expr_replacement_map.find(*it);
519 if(m_it != expr_replacement_map.end())
523 m_it->second(f_code, code, symbol_table);
524 it.next_sibling_or_parent();
526 expr_replacement_map.erase(m_it);
527 if(expr_replacement_map.empty())
570 for(
const auto &entry : symbol_table)
572 const symbolt &symbol = entry.second;
574 if(symbol.
type.
id() != ID_code)
584 message.warning() <<
"Java method '" << entry.first
585 <<
"' is static and synchronized."
586 <<
" This is unsupported, the synchronized keyword"
587 <<
" will be ignored."
594 exprt this_expr(this_id);
596 auto it = symbol_table.symbols.find(this_id);
598 if(it == symbol_table.symbols.end())
603 symbolt &w_symbol = symbol_table.get_writeable_ref(entry.first);
Class that provides messages with a built-in verbosity 'level'.
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
A codet representing sequential composition of program statements.
void convert_synchronized_methods(symbol_tablet &symbol_table, message_handlert &message_handler)
Iterate through the symbol table to find and instrument synchronized methods.
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....
#define Forall_operands(it, expr)
reference_typet java_reference_type(const typet &subtype)
depth_iteratort depth_begin()
const std::string thread_id
The type of an expression, extends irept.
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.
typet type
Type of symbol.
static void monitor_exits(codet &code, const codet &monitorexit)
Introduces a monitorexit before every return recursively.
The plus expression Associativity is not specified.
Base class for all expressions.
irep_idt base_name
Base (non-scoped) name.
Pushes an exception handler, of the form: exception_tag1 -> label1 exception_tag2 -> label2 ....
A struct tag type, i.e., struct_typet with an identifier.
void convert_threadblock(symbol_tablet &symbol_table)
Iterate through the symbol table to find and appropriately instrument thread-blocks.
static const std::string get_first_label_id(const std::string &id)
Retrieve the first label identifier.
Expression to hold a symbol (variable)
Pops an exception handler from the stack of active handlers (i.e.
irep_idt pretty_name
Language-specific display name.
const codet & to_code(const exprt &expr)
static void instrument_end_thread(const code_function_callt &f_code, codet &code, const symbol_tablet &symbol_table)
Transforms the codet stored in in f_code, which is a call to function CProver.endThread:(I)V into a b...
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
static const char * message(const static_verifier_resultt::statust &status)
Makes a status message string from a status.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
codet representation of a function call statement.
bool get_bool(const irep_namet &name) const
irep_idt mode
Language mode.
const std::string & id2string(const irep_idt &d)
const std::string next_thread_id
codet representation of a goto statement.
codet representation of a label for branch targets.
#define PRECONDITION(CONDITION)
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
exception_listt & exception_list()
static const std::string get_second_label_id(const std::string &id)
Retrieve the second label identifier.
const irep_idt & id() const
static codet get_monitor_call(const symbol_tablet &symbol_table, bool is_enter, const exprt &object)
Creates a monitorenter/monitorexit code_function_callt for the given synchronization object.
const code_function_callt & to_code_function_call(const codet &code)
void add(const codet &code)
signedbv_typet java_int_type()
symbolt & fresh_java_symbol(const typet &type, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &function_name, symbol_table_baset &symbol_table)
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
exprt value
Initial value of symbol.
A codet representing a skip statement.
Forward depth-first search iterators These iterators' copy operations are expensive,...
A statement that catches an exception, assigning the exception in flight to an expression (e....
std::vector< exception_list_entryt > exception_listt
void set(const irep_namet &name, const irep_idt &value)
const symbolst & symbols
Read-only field, used to look up symbols given their names.
std::string expr2java(const exprt &expr, const namespacet &ns)
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...
A side_effect_exprt representation of a side effect that throws an exception.
const code_blockt & to_code_block(const codet &code)
There are a large number of kinds of tree structured or tree-like data in CPROVER.
source_locationt & add_source_location()
A codet representing an assignment in the program.
const irep_idt & get_statement() const
depth_iteratort depth_end()
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
static void instrument_synchronized_code(symbol_tablet &symbol_table, symbolt &symbol, const exprt &sync_object)
Transforms the codet stored in symbol.value.
const source_locationt & source_location() const
static void instrument_get_current_thread_id(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 ...
irep_idt name
The unique identifier.
codet representation of an expression statement.
Data structure for representing an arbitrary statement in a program.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const std::string integer2string(const mp_integer &n, unsigned base)