38 const bool is_thread_local,
39 const bool is_static_lifetime)
41 const symbolt* psymbol =
nullptr;
44 if(psymbol !=
nullptr)
47 new_symbol.
name = name;
50 new_symbol.
type = type;
51 new_symbol.
value = value;
56 new_symbol.
mode = ID_java;
57 symbol_table.
add(new_symbol);
118 const symbolt ¤t_symbol =
139 codet tmp_a(ID_start_thread);
140 tmp_a.
set(ID_destination, lbl1);
155 block.add(
codet(ID_atomic_begin));
158 block.add(
codet(ID_atomic_end));
189 codet tmp_a(ID_end_thread);
217 const symbolt& current_symbol =
293 using instrument_callbackt =
294 std::function<void(const code_function_callt&, codet&, symbol_tablet&)>;
295 using expr_replacement_mapt =
296 std::unordered_map<const exprt, instrument_callbackt, irep_hash>;
300 for(
auto entry : symbol_table)
302 expr_replacement_mapt expr_replacement_map;
303 const symbolt &symbol = entry.second;
311 instrument_callbackt cb;
313 const exprt &expr = *it;
314 if(expr.
id() != ID_code)
323 if(f_name ==
"org.cprover.CProver.startThread:(I)V")
325 std::placeholders::_2, std::placeholders::_3);
326 else if(f_name ==
"org.cprover.CProver.endThread:(I)V")
328 std::placeholders::_2, std::placeholders::_3);
329 else if(f_name ==
"org.cprover.CProver.getCurrentThreadID:()I")
331 std::placeholders::_2, std::placeholders::_3);
334 expr_replacement_map.insert({expr, cb});
337 if(!expr_replacement_map.empty())
339 symbolt &w_symbol = symbol_table.get_writeable_ref(entry.first);
346 expr_replacement_mapt::iterator m_it = expr_replacement_map.find(*it);
347 if(m_it != expr_replacement_map.end())
351 m_it->second(f_code, code, symbol_table);
352 it.next_sibling_or_parent();
354 expr_replacement_map.erase(m_it);
355 if(expr_replacement_map.empty())
const irep_idt & get_statement() const
The type of an expression.
irep_idt name
The unique identifier.
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 ...
const std::string integer2string(const mp_integer &n, unsigned base)
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 b...
irep_idt mode
Language mode.
void convert_threadblock(symbol_tablet &symbol_table)
Iterate through the symbol table to find and appropriately instrument thread-blocks.
void copy_to_operands(const exprt &expr)
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
exprt value
Initial value of symbol.
irep_idt pretty_name
Language-specific display name.
depth_iteratort depth_begin()
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
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...
const irep_idt & id() const
void add(const codet &code)
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
static const std::string get_first_label_id(const std::string &id)
Retrieve the first label identifier.
const std::string next_thread_id
const std::string thread_id
A label for branch targets.
#define PRECONDITION(CONDITION)
typet type
Type of symbol.
static const std::string get_second_label_id(const std::string &id)
Retrieve the second label identifier.
Base class for all expressions.
irep_idt base_name
Base (non-scoped) name.
const source_locationt & source_location() const
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.
source_locationt & add_source_location()
const codet & to_code(const exprt &expr)
depth_iteratort depth_end()
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
A statement in a programming language.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
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...
void set(const irep_namet &name, const irep_idt &value)
std::string expr2java(const exprt &expr, const namespacet &ns)
const code_function_callt & to_code_function_call(const codet &code)