41 const bool is_thread_local,
42 const bool is_static_lifetime)
44 const symbolt *psymbol =
nullptr;
47 if(psymbol !=
nullptr)
50 new_symbol.
name = name;
53 new_symbol.
type = type;
54 new_symbol.
value = value;
59 new_symbol.
mode = ID_java;
60 symbol_table.
add(new_symbol);
109 is_enter ?
"java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V"
110 :
"java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V";
112 auto it = symbol_table.
symbols.find(symbol);
124 if(it == symbol_table.
symbols.end())
138 if(statement == ID_return)
144 statement == ID_label || statement == ID_block ||
145 statement == ID_decl_block)
211 const exprt &sync_object)
224 irep_idt handler(
"pc-synchronized-catch");
228 exception_list.push_back(
237 "caught-synchronized-exception",
244 codet catch_instruction = catch_statement;
247 catch_block.
add(catch_instruction);
248 catch_block.
add(monitorexit);
259 code =
code_blockt({monitorenter, catch_push, code, catch_pop, catch_label});
292 const symbolt ¤t_symbol =
313 codet tmp_a(ID_start_thread);
314 tmp_a.
set(ID_destination, lbl1);
325 codet(ID_atomic_begin),
328 codet(ID_atomic_end)});
358 codet tmp_a(ID_end_thread);
382 const symbolt& current_symbol =
414 const auto &followed_type =
421 object_type.get_component(
"cproverMonitorCount")));
489 using instrument_callbackt =
491 using expr_replacement_mapt =
492 std::unordered_map<const exprt, instrument_callbackt, irep_hash>;
496 for(
const auto &entry : symbol_table)
498 expr_replacement_mapt expr_replacement_map;
499 const symbolt &symbol = entry.second;
507 instrument_callbackt cb;
509 const exprt &expr = *it;
510 if(expr.
id() != ID_code)
519 if(f_name ==
"org.cprover.CProver.startThread:(I)V")
522 std::placeholders::_1,
523 std::placeholders::_2,
524 std::placeholders::_3);
525 else if(f_name ==
"org.cprover.CProver.endThread:(I)V")
528 std::placeholders::_1,
529 std::placeholders::_2,
530 std::placeholders::_3);
531 else if(f_name ==
"org.cprover.CProver.getCurrentThreadId:()I")
534 std::placeholders::_1,
535 std::placeholders::_2,
536 std::placeholders::_3);
538 f_name ==
"org.cprover.CProver.getMonitorCount:(Ljava/lang/Object;)I")
541 std::placeholders::_1,
542 std::placeholders::_2,
543 std::placeholders::_3);
546 expr_replacement_map.insert({expr, cb});
549 if(!expr_replacement_map.empty())
558 expr_replacement_mapt::iterator m_it = expr_replacement_map.find(*it);
559 if(m_it != expr_replacement_map.end())
563 m_it->second(f_code, code, symbol_table);
564 it.next_sibling_or_parent();
566 expr_replacement_map.erase(m_it);
567 if(expr_replacement_map.empty())
610 for(
const auto &entry : symbol_table)
612 const symbolt &symbol = entry.second;
614 if(symbol.
type.
id() != ID_code)
624 message.
warning() <<
"Java method '" << entry.first
625 <<
"' is static and synchronized."
626 <<
" This is unsupported, the synchronized keyword"
627 <<
" will be ignored."
634 exprt this_expr(this_id);
636 auto it = symbol_table.
symbols.find(this_id);
638 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.
bool get_bool(const irep_idt &name) const
void set(const irep_idt &name, const irep_idt &value)
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 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.
const typet & base_type() const
The type of the data what we point to.
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.
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 codet &code)
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)
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 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.