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);
106 is_enter ?
"java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V" 107 :
"java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V";
109 auto it = symbol_table.
symbols.find(symbol);
121 if(it == symbol_table.
symbols.end())
139 if(statement == ID_return)
143 return_block.
add(monitorexit);
148 statement == ID_label || statement == ID_block ||
149 statement == ID_decl_block)
215 const exprt &sync_object)
228 irep_idt handler(
"pc-synchronized-catch");
232 exception_list.push_back(
242 "caught-synchronized-exception",
243 code.source_location(),
247 catch_var.set(ID_C_base_name, tmp_symbol.
base_name);
249 codet catch_instruction = catch_statement;
252 catch_block.
add(catch_instruction);
253 catch_block.
add(monitorexit);
299 const symbolt ¤t_symbol =
320 codet tmp_a(ID_start_thread);
321 tmp_a.
set(ID_destination, lbl1);
336 block.add(
codet(ID_atomic_begin));
339 block.add(
codet(ID_atomic_end));
370 codet tmp_a(ID_end_thread);
398 const symbolt& current_symbol =
474 using instrument_callbackt =
475 std::function<void(const code_function_callt&, codet&, symbol_tablet&)>;
476 using expr_replacement_mapt =
477 std::unordered_map<const exprt, instrument_callbackt, irep_hash>;
481 for(
const auto &entry : symbol_table)
483 expr_replacement_mapt expr_replacement_map;
484 const symbolt &symbol = entry.second;
492 instrument_callbackt cb;
494 const exprt &expr = *it;
495 if(expr.
id() != ID_code)
504 if(f_name ==
"org.cprover.CProver.startThread:(I)V")
507 std::placeholders::_1,
508 std::placeholders::_2,
509 std::placeholders::_3);
510 else if(f_name ==
"org.cprover.CProver.endThread:(I)V")
513 std::placeholders::_1,
514 std::placeholders::_2,
515 std::placeholders::_3);
516 else if(f_name ==
"org.cprover.CProver.getCurrentThreadID:()I")
519 std::placeholders::_1,
520 std::placeholders::_2,
521 std::placeholders::_3);
524 expr_replacement_map.insert({expr, cb});
527 if(!expr_replacement_map.empty())
529 symbolt &w_symbol = symbol_table.get_writeable_ref(entry.first);
536 expr_replacement_mapt::iterator m_it = expr_replacement_map.find(*it);
537 if(m_it != expr_replacement_map.end())
541 m_it->second(f_code, code, symbol_table);
542 it.next_sibling_or_parent();
544 expr_replacement_map.erase(m_it);
545 if(expr_replacement_map.empty())
588 for(
const auto &entry : symbol_table)
590 const symbolt &symbol = entry.second;
592 if(symbol.
type.
id() != ID_code)
602 message.
warning() <<
"Java method '" << entry.first
603 <<
"' is static and synchronized." 604 <<
" This is unsupported, the synchronized keyword" 605 <<
" will be ignored." 612 exprt this_expr(this_id);
614 auto it = symbol_table.symbols.find(this_id);
616 if(it == symbol_table.symbols.end())
621 symbolt &w_symbol = symbol_table.get_writeable_ref(entry.first);
const irep_idt & get_statement() const
The type of an expression.
irep_idt name
The unique identifier.
std::vector< exception_list_entryt > exception_listt
const std::string & id2string(const irep_idt &d)
const std::string integer2string(const mp_integer &n, unsigned base)
irep_idt mode
Language mode.
reference_typet java_reference_type(const typet &subtype)
void copy_to_operands(const exprt &expr)
Pushes an exception handler, of the form: exception_tag1 -> label1 exception_tag2 -> label2 ...
void move_to_operands(exprt &expr)
Fresh auxiliary symbol creation.
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
exprt value
Initial value of symbol.
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 std::string thread_id
irep_idt pretty_name
Language-specific display name.
Pops an exception handler from the stack of active handlers (i.e.
depth_iteratort depth_begin()
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
static mstreamt & eom(mstreamt &m)
bool get_bool(const irep_namet &name) const
A side effect that throws an exception.
mstreamt & warning() const
const irep_idt & id() const
void add(const codet &code)
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
void convert_synchronized_methods(symbol_tablet &symbol_table, message_handlert &message_handler)
Iterate through the symbol table to find and instrument synchronized methods.
A reference into the symbol table.
A label for branch targets.
#define PRECONDITION(CONDITION)
Base class for tree-like data structures with sharing.
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 ...
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
static void monitor_exits(codet &code, const codet &monitorexit)
Introduces a monitorexit before every return recursively.
const source_locationt & source_location() const
typet type
Type of symbol.
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...
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with the requested name pattern.
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.
Base class for all expressions.
irep_idt base_name
Base (non-scoped) name.
const std::string next_thread_id
const source_locationt & source_location() const
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...
#define Forall_operands(it, expr)
source_locationt & add_source_location()
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...
const codet & to_code(const exprt &expr)
void convert_threadblock(symbol_tablet &symbol_table)
Iterate through the symbol table to find and appropriately instrument thread-blocks.
static const std::string get_second_label_id(const std::string &id)
Retrieve the second label identifier.
static void instrument_synchronized_code(symbol_tablet &symbol_table, symbolt &symbol, const exprt &sync_object)
Transforms the codet stored in symbol.value.
Expression to hold a symbol (variable)
depth_iteratort depth_end()
const code_blockt & to_code_block(const codet &code)
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
goto_programt coverage_criteriont message_handlert & message_handler
A statement in a programming language.
exception_listt & exception_list()
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
void set(const irep_namet &name, const irep_idt &value)
std::string expr2java(const exprt &expr, const namespacet &ns)
static const std::string get_first_label_id(const std::string &id)
Retrieve the first label identifier.
A statement that catches an exception, assigning the exception in flight to an expression (e...
const code_function_callt & to_code_function_call(const codet &code)