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 =
412 const auto &followed_type =
419 object_type.get_component(
"cproverMonitorCount")));
487 using instrument_callbackt =
489 using expr_replacement_mapt =
490 std::unordered_map<const exprt, instrument_callbackt, irep_hash>;
494 for(
const auto &entry : symbol_table)
496 expr_replacement_mapt expr_replacement_map;
497 const symbolt &symbol = entry.second;
505 instrument_callbackt cb;
507 const exprt &expr = *it;
508 if(expr.
id() != ID_code)
517 if(f_name ==
"org.cprover.CProver.startThread:(I)V")
520 std::placeholders::_1,
521 std::placeholders::_2,
522 std::placeholders::_3);
523 else if(f_name ==
"org.cprover.CProver.endThread:(I)V")
526 std::placeholders::_1,
527 std::placeholders::_2,
528 std::placeholders::_3);
529 else if(f_name ==
"org.cprover.CProver.getCurrentThreadId:()I")
532 std::placeholders::_1,
533 std::placeholders::_2,
534 std::placeholders::_3);
536 f_name ==
"org.cprover.CProver.getMonitorCount:(Ljava/lang/Object;)I")
539 std::placeholders::_1,
540 std::placeholders::_2,
541 std::placeholders::_3);
544 expr_replacement_map.insert({expr, cb});
547 if(!expr_replacement_map.empty())
556 expr_replacement_mapt::iterator m_it = expr_replacement_map.find(*it);
557 if(m_it != expr_replacement_map.end())
561 m_it->second(f_code, code, symbol_table);
562 it.next_sibling_or_parent();
564 expr_replacement_map.erase(m_it);
565 if(expr_replacement_map.empty())
608 for(
const auto &entry : symbol_table)
610 const symbolt &symbol = entry.second;
612 if(symbol.
type.
id() != ID_code)
622 message.warning() <<
"Java method '" << entry.first
623 <<
"' is static and synchronized."
624 <<
" This is unsupported, the synchronized keyword"
625 <<
" will be ignored."
632 exprt this_expr(this_id);
634 auto it = symbol_table.
symbols.find(this_id);
636 if(it == symbol_table.
symbols.end())
A codet representing an assignment in the program.
A codet representing sequential composition of program statements.
void add(const codet &code)
codet representation of an expression statement.
codet representation of a function call statement.
codet representation of a goto statement.
codet representation of a label for branch targets.
A statement that catches an exception, assigning the exception in flight to an expression (e....
Pops an exception handler from the stack of active handlers (i.e.
Pushes an exception handler, of the form: exception_tag1 -> label1 exception_tag2 -> label2 ....
std::vector< exception_list_entryt > exception_listt
exception_listt & exception_list()
A codet representing a skip statement.
Data structure for representing an arbitrary statement in a program.
const irep_idt & get_statement() const
Operator to dereference a pointer.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
depth_iteratort depth_end()
source_locationt & add_source_location()
depth_iteratort depth_begin()
const source_locationt & source_location() const
There are a large number of kinds of tree structured or tree-like data in CPROVER.
void set(const irep_namet &name, const irep_idt &value)
bool get_bool(const irep_namet &name) const
const irep_idt & id() const
Extract member of struct or union.
Class that provides messages with a built-in verbosity 'level'.
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
The plus expression Associativity is not specified.
A side_effect_exprt representation of a side effect that throws an exception.
A struct tag type, i.e., struct_typet with an identifier.
Expression to hold a symbol (variable)
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
irep_idt base_name
Base (non-scoped) name.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
typet type
Type of symbol.
irep_idt name
The unique identifier.
irep_idt pretty_name
Language-specific display name.
exprt value
Initial value of symbol.
irep_idt mode
Language mode.
The type of an expression, extends irept.
const typet & subtype() const
std::string expr2java(const exprt &expr, const namespacet &ns)
#define Forall_operands(it, expr)
Forward depth-first search iterators These iterators' copy operations are expensive,...
const std::string & id2string(const irep_idt &d)
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...
const std::string next_thread_id
void convert_synchronized_methods(symbol_tablet &symbol_table, message_handlert &message_handler)
Iterate through the symbol table to find and instrument synchronized methods.
const std::string thread_id
void convert_threadblock(symbol_tablet &symbol_table)
Iterate through the symbol table to find and appropriately instrument thread-blocks.
static void instrument_get_monitor_count(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.getMonitorCount:(Ljava/...
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....
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...
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.
static void instrument_synchronized_code(symbol_tablet &symbol_table, symbolt &symbol, const exprt &sync_object)
Transforms the codet stored in symbol.value.
static void monitor_exits(codet &code, const codet &monitorexit)
Introduces a monitorexit before every return recursively.
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 ...
static const std::string get_first_label_id(const std::string &id)
Retrieve the first label identifier.
static const std::string get_second_label_id(const std::string &id)
Retrieve the second label identifier.
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.
signedbv_typet java_int_type()
reference_typet java_reference_type(const typet &subtype)
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)
const std::string integer2string(const mp_integer &n, unsigned base)
#define PRECONDITION(CONDITION)
static const char * message(const statust &status)
Makes a status message string from a status.
const codet & to_code(const exprt &expr)
const code_blockt & to_code_block(const codet &code)
const code_function_callt & to_code_function_call(const codet &code)
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.