42 const bool is_thread_local,
43 const bool is_static_lifetime)
51 new_symbol.pretty_name = name;
52 new_symbol.base_name = base_name;
53 new_symbol.value = value;
54 new_symbol.is_lvalue =
true;
55 new_symbol.is_state_var =
true;
56 new_symbol.is_static_lifetime = is_static_lifetime;
57 new_symbol.is_thread_local = is_thread_local;
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())
226 exception_list.push_back(
235 "caught-synchronized-exception",
290 const symbolt ¤t_symbol =
380 const symbolt& current_symbol =
418 object_type.get_component(
"cproverMonitorCount")));
489 std::unordered_map<const exprt, instrument_callbackt, irep_hash>;
493 for(
const auto &entry : symbol_table)
496 const symbolt &symbol = entry.second;
506 const exprt &expr = *it;
516 if(
f_name ==
"org.cprover.CProver.startThread:(I)V")
519 std::placeholders::_1,
520 std::placeholders::_2,
521 std::placeholders::_3);
522 else if(
f_name ==
"org.cprover.CProver.endThread:(I)V")
525 std::placeholders::_1,
526 std::placeholders::_2,
527 std::placeholders::_3);
528 else if(
f_name ==
"org.cprover.CProver.getCurrentThreadId:()I")
531 std::placeholders::_1,
532 std::placeholders::_2,
533 std::placeholders::_3);
535 f_name ==
"org.cprover.CProver.getMonitorCount:(Ljava/lang/Object;)I")
538 std::placeholders::_1,
539 std::placeholders::_2,
540 std::placeholders::_3);
552 for(
auto it =
w_symbol.value.depth_begin(),
561 it.next_sibling_or_parent();
621 message.
warning() <<
"Java method '" <<
s_it->first
622 <<
"' is static and synchronized."
623 <<
" This is unsupported, the synchronized keyword"
634 if(it == symbol_table.
symbols.end())
641 symbol_table,
w_symbol, it->second.symbol_expr());
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
A goto_instruction_codet representing an assignment in the program.
A codet representing sequential composition of program statements.
codet representation of an expression statement.
goto_instruction_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
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.
depth_iteratort depth_end()
depth_iteratort depth_begin()
const source_locationt & source_location() const
source_locationt & add_source_location()
There are a large number of kinds of tree structured or tree-like data in CPROVER.
bool get_bool(const irep_idt &name) const
const irep_idt & id() const
Extract member of struct or union.
Class that provides messages with a built-in verbosity 'level'.
mstreamt & warning() const
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
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)
The symbol table base class interface.
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
virtual iteratort begin()=0
const symbolst & symbols
Read-only field, used to look up symbols given their names.
virtual iteratort end()=0
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
typet type
Type of symbol.
irep_idt name
The unique identifier.
exprt value
Initial value of symbol.
The type of an expression, extends irept.
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 code_function_callt & to_code_function_call(const goto_instruction_codet &code)
const std::string & id2string(const irep_idt &d)
const std::string next_thread_id
const std::string thread_id
static void instrument_get_monitor_count(const code_function_callt &f_code, codet &code, symbol_table_baset &symbol_table)
Transforms the codet stored in in f_code, which is a call to function CProver.getMonitorCount:(Ljava/...
static void instrument_start_thread(const code_function_callt &f_code, codet &code, symbol_table_baset &symbol_table)
Transforms the codet stored in in f_code, which is a call to function CProver.startThread:(I)V into a...
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 symbolt add_or_get_symbol(symbol_table_baset &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.
static void instrument_end_thread(const code_function_callt &f_code, codet &code, const symbol_table_baset &symbol_table)
Transforms the codet stored in in f_code, which is a call to function CProver.endThread:(I)V into a b...
static void monitor_exits(codet &code, const codet &monitorexit)
Introduces a monitorexit before every return recursively.
void convert_synchronized_methods(symbol_table_baset &symbol_table, message_handlert &message_handler)
Iterate through the symbol table to find and instrument synchronized methods.
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 codet get_monitor_call(const symbol_table_baset &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_table_baset &symbol_table, symbolt &symbol, const exprt &sync_object)
Transforms the codet stored in symbol.value.
static void instrument_get_current_thread_id(const code_function_callt &f_code, codet &code, symbol_table_baset &symbol_table)
Transforms the codet stored in in f_code, which is a call to function CProver.getCurrentThreadId:()I ...
void convert_threadblock(symbol_table_baset &symbol_table)
Iterate through the symbol table to find and appropriately instrument thread-blocks.
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)
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
#define PRECONDITION(CONDITION)
const code_blockt & to_code_block(const codet &code)
const codet & to_code(const exprt &expr)
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.