cprover
java_bytecode_concurrency_instrumentation.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Java Convert Thread blocks
4
5Author: Kurt Degiogrio, kurt.degiorgio@diffblue.com
6
7\*******************************************************************/
8
10#include "expr2java.h"
11#include "java_types.h"
12#include "java_utils.h"
13
14#include <util/arith_tools.h>
15#include <util/cprover_prefix.h>
16#include <util/expr_iterator.h>
17#include <util/message.h>
18#include <util/namespace.h>
19#include <util/std_types.h>
20#include <util/symbol_table.h>
21
22// Disable linter to allow an std::string constant.
23const std::string next_thread_id = CPROVER_PREFIX "_next_thread_id";// NOLINT(*)
24const std::string thread_id = CPROVER_PREFIX "_thread_id";// NOLINT(*)
25
36 symbol_tablet &symbol_table,
37 const irep_idt &name,
38 const irep_idt &base_name,
39 const typet &type,
40 const exprt &value,
41 const bool is_thread_local,
42 const bool is_static_lifetime)
43{
44 const symbolt *psymbol = nullptr;
45 namespacet ns(symbol_table);
46 ns.lookup(name, psymbol);
47 if(psymbol != nullptr)
48 return *psymbol;
49 symbolt new_symbol;
50 new_symbol.name = name;
51 new_symbol.pretty_name = name;
52 new_symbol.base_name = base_name;
53 new_symbol.type = type;
54 new_symbol.value = value;
55 new_symbol.is_lvalue = true;
56 new_symbol.is_state_var = true;
57 new_symbol.is_static_lifetime = is_static_lifetime;
58 new_symbol.is_thread_local = is_thread_local;
59 new_symbol.mode = ID_java;
60 symbol_table.add(new_symbol);
61 return new_symbol;
62}
63
68static const std::string get_first_label_id(const std::string &id)
69{
70 return CPROVER_PREFIX "_THREAD_ENTRY_" + id;
71}
72
77static const std::string get_second_label_id(const std::string &id)
78{
79 return CPROVER_PREFIX "_THREAD_EXIT_" + id;
80}
81
86static const std::string get_thread_block_identifier(
87 const code_function_callt &f_code)
88{
89 PRECONDITION(f_code.arguments().size() == 1);
90 const exprt &expr = f_code.arguments()[0];
91 const mp_integer lbl_id =
92 numeric_cast_v<mp_integer>(to_constant_expr(to_multi_ary_expr(expr).op0()));
93 return integer2string(lbl_id);
94}
95
104 const symbol_tablet &symbol_table,
105 bool is_enter,
106 const exprt &object)
107{
108 const irep_idt symbol =
109 is_enter ? "java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V"
110 : "java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V";
111
112 auto it = symbol_table.symbols.find(symbol);
113
114 // If the 'java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V' or
115 // 'java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V' method is not
116 // found symex will rightfully complain as it cannot find the symbol
117 // associated with the method in question. To avoid this and thereby ensuring
118 // JBMC works both with and without the models, we replace the aforementioned
119 // methods with skips when we cannot find them.
120 //
121 // Note: this can only happen if the java-core-models library is not loaded.
122 //
123 // Note': we explicitly prevent JBMC from stubbing these methods.
124 if(it == symbol_table.symbols.end())
125 return code_skipt();
126
127 // Otherwise we create a function call
128 return code_function_callt(symbol_exprt(symbol, it->second.type), {object});
129}
130
135static void monitor_exits(codet &code, const codet &monitorexit)
136{
137 const irep_idt &statement = code.get_statement();
138 if(statement == ID_return)
139 {
140 // Replace the return with a monitor exit plus return block
141 code = code_blockt({monitorexit, code});
142 }
143 else if(
144 statement == ID_label || statement == ID_block ||
145 statement == ID_decl_block)
146 {
147 // If label or block found, explore the code inside the block
148 Forall_operands(it, code)
149 {
150 codet &sub_code = to_code(*it);
151 monitor_exits(sub_code, monitorexit);
152 }
153 }
154}
155
209 symbol_tablet &symbol_table,
210 symbolt &symbol,
211 const exprt &sync_object)
212{
213 PRECONDITION(!symbol.type.get_bool(ID_is_static));
214
215 codet &code = to_code(symbol.value);
216
217 // Get the calls to the functions that implement the critical section
218 codet monitorenter = get_monitor_call(symbol_table, true, sync_object);
219 codet monitorexit = get_monitor_call(symbol_table, false, sync_object);
220
221 // Create a unique catch label and empty throw type (i.e. any)
222 // and catch-push them at the beginning of the code (i.e. begin try)
223 code_push_catcht catch_push;
224 irep_idt handler("pc-synchronized-catch");
225 irep_idt exception_id;
226 code_push_catcht::exception_listt &exception_list =
227 catch_push.exception_list();
228 exception_list.push_back(
229 code_push_catcht::exception_list_entryt(exception_id, handler));
230
231 // Create a catch-pop to indicate the end of the try block
232 code_pop_catcht catch_pop;
233
234 // Create the finally block with the same label targeted in the catch-push
235 const symbolt &tmp_symbol = fresh_java_symbol(
236 java_reference_type(struct_tag_typet("java::java.lang.Throwable")),
237 "caught-synchronized-exception",
238 code.source_location(),
239 id2string(symbol.name),
240 symbol_table);
241 symbol_exprt catch_var(tmp_symbol.name, tmp_symbol.type);
242 catch_var.set(ID_C_base_name, tmp_symbol.base_name);
243 code_landingpadt catch_statement(catch_var);
244 codet catch_instruction = catch_statement;
245 code_labelt catch_label(handler, code_blockt());
246 code_blockt &catch_block = to_code_block(catch_label.code());
247 catch_block.add(catch_instruction);
248 catch_block.add(monitorexit);
249
250 // Re-throw exception
251 side_effect_expr_throwt throw_expr(irept(), typet(), code.source_location());
252 throw_expr.copy_to_operands(catch_var);
253 catch_block.add(code_expressiont(throw_expr));
254
255 // Write a monitorexit before every return
256 monitor_exits(code, monitorexit);
257
258 // Wrap the code into a try finally
259 code = code_blockt({monitorenter, catch_push, code, catch_pop, catch_label});
260}
261
272 const code_function_callt &f_code,
273 codet &code,
274 symbol_tablet &symbol_table)
275{
276 PRECONDITION(f_code.arguments().size() == 1);
277
278 // Create global variable __CPROVER__next_thread_id. Used as a counter
279 // in-order to to assign ids to new threads.
280 const symbol_exprt next_symbol_expr = add_or_get_symbol(
281 symbol_table,
286 false,
287 true)
288 .symbol_expr();
289
290 // Create thread-local variable __CPROVER__thread_id. Holds the id of
291 // the thread.
292 const symbolt &current_symbol =
294 symbol_table, thread_id, thread_id, java_int_type(),
295 from_integer(0, java_int_type()), true, true);
296
297 // Construct appropriate labels.
298 // Note: java does not have labels so this should be safe.
299 const std::string &thread_block_id = get_thread_block_identifier(f_code);
300 const std::string &lbl1 = get_first_label_id(thread_block_id);
301 const std::string &lbl2 = get_second_label_id(thread_block_id);
302
303 // Instrument the following codet's:
304 //
305 // A: codet(id=ID_start_thread, destination=__CPROVER_THREAD_ENTRY_<ID>)
306 // B: codet(id=ID_goto, destination=__CPROVER_THREAD_EXIT_<ID>)
307 // C: codet(id=ID_label, label=__CPROVER_THREAD_ENTRY_<ID>)
308 // C.1: codet(id=ID_atomic_begin)
309 // D: CPROVER__next_thread_id += 1;
310 // E: __CPROVER__thread_id = __CPROVER__next_thread_id;
311 // F: codet(id=ID_atomic_end)
312
313 codet tmp_a(ID_start_thread);
314 tmp_a.set(ID_destination, lbl1);
315 code_gotot tmp_b(lbl2);
316 const code_labelt tmp_c(lbl1, code_skipt());
317
318 const plus_exprt plus(next_symbol_expr, from_integer(1, java_int_type()));
319 const code_assignt tmp_d(next_symbol_expr, plus);
320 const code_assignt tmp_e(current_symbol.symbol_expr(), next_symbol_expr);
321
322 code = code_blockt({tmp_a,
323 tmp_b,
324 tmp_c,
325 codet(ID_atomic_begin),
326 tmp_d,
327 tmp_e,
328 codet(ID_atomic_end)});
329 code.add_source_location() = f_code.source_location();
330}
331
342 const code_function_callt &f_code,
343 codet &code,
344 const symbol_tablet &symbol_table)
345{
346 PRECONDITION(f_code.arguments().size() == 1);
347 (void)symbol_table; // unused parameter
348
349 // Build id, used to construct appropriate labels.
350 // Note: java does not have labels so this should be safe
351 const std::string &thread_block_id = get_thread_block_identifier(f_code);
352 const std::string &lbl2 = get_second_label_id(thread_block_id);
353
354 // Instrument the following code:
355 //
356 // A: codet(id=ID_end_thread)
357 // B: codet(id=ID_label,label= __CPROVER_THREAD_EXIT_<ID>)
358 codet tmp_a(ID_end_thread);
359 const code_labelt tmp_b(lbl2, code_skipt());
360
361 const auto location = code.source_location();
362 code = code_blockt({tmp_a, tmp_b});
363 code.add_source_location() = location;
364}
365
376 const code_function_callt &f_code,
377 codet &code,
378 symbol_tablet &symbol_table)
379{
380 PRECONDITION(f_code.arguments().size() == 0);
381
382 const symbolt& current_symbol =
383 add_or_get_symbol(symbol_table,
384 thread_id,
385 thread_id,
388 true, true);
389
390 code_assignt code_assign(f_code.lhs(), current_symbol.symbol_expr());
391 code_assign.add_source_location() = f_code.source_location();
392
393 code = code_assign;
394}
395
407 const code_function_callt &f_code,
408 codet &code,
409 symbol_tablet &symbol_table)
410{
411 PRECONDITION(f_code.arguments().size() == 1);
412
413 const namespacet ns(symbol_table);
414 const auto &followed_type =
415 ns.follow(to_pointer_type(f_code.arguments()[0].type()).base_type());
416 const auto &object_type = to_struct_type(followed_type);
417 code_assignt code_assign(
418 f_code.lhs(),
420 dereference_exprt(f_code.arguments()[0]),
421 object_type.get_component("cproverMonitorCount")));
422 code_assign.add_source_location() = f_code.source_location();
423
424 code = code_assign;
425}
426
488{
489 using instrument_callbackt =
490 std::function<void(const code_function_callt&, codet&, symbol_tablet&)>;
491 using expr_replacement_mapt =
492 std::unordered_map<const exprt, instrument_callbackt, irep_hash>;
493
494 namespacet ns(symbol_table);
495
496 for(const auto &entry : symbol_table)
497 {
498 expr_replacement_mapt expr_replacement_map;
499 const symbolt &symbol = entry.second;
500
501 // Look for code_function_callt's (without breaking sharing)
502 // and insert each one into a replacement map along with an associated
503 // callback that will handle their instrumentation.
504 for(auto it = symbol.value.depth_begin(), itend = symbol.value.depth_end();
505 it != itend; ++it)
506 {
507 instrument_callbackt cb;
508
509 const exprt &expr = *it;
510 if(expr.id() != ID_code)
511 continue;
512
513 const codet &code = to_code(expr);
514 if(code.get_statement() != ID_function_call)
515 continue;
516
517 const code_function_callt &f_code = to_code_function_call(code);
518 const std::string &f_name = expr2java(f_code.function(), ns);
519 if(f_name == "org.cprover.CProver.startThread:(I)V")
520 cb = std::bind(
522 std::placeholders::_1,
523 std::placeholders::_2,
524 std::placeholders::_3);
525 else if(f_name == "org.cprover.CProver.endThread:(I)V")
526 cb = std::bind(
528 std::placeholders::_1,
529 std::placeholders::_2,
530 std::placeholders::_3);
531 else if(f_name == "org.cprover.CProver.getCurrentThreadId:()I")
532 cb = std::bind(
534 std::placeholders::_1,
535 std::placeholders::_2,
536 std::placeholders::_3);
537 else if(
538 f_name == "org.cprover.CProver.getMonitorCount:(Ljava/lang/Object;)I")
539 cb = std::bind(
541 std::placeholders::_1,
542 std::placeholders::_2,
543 std::placeholders::_3);
544
545 if(cb)
546 expr_replacement_map.insert({expr, cb});
547 }
548
549 if(!expr_replacement_map.empty())
550 {
551 symbolt &w_symbol = symbol_table.get_writeable_ref(entry.first);
552 // Use expr_replacment_map to look for exprt's that need to be replaced.
553 // Once found, get a non-const exprt (breaking sharing in the process) and
554 // call it's associated instrumentation function.
555 for(auto it = w_symbol.value.depth_begin(),
556 itend = w_symbol.value.depth_end(); it != itend;)
557 {
558 expr_replacement_mapt::iterator m_it = expr_replacement_map.find(*it);
559 if(m_it != expr_replacement_map.end())
560 {
561 codet &code = to_code(it.mutate());
562 const code_function_callt &f_code = to_code_function_call(code);
563 m_it->second(f_code, code, symbol_table);
564 it.next_sibling_or_parent();
565
566 expr_replacement_map.erase(m_it);
567 if(expr_replacement_map.empty())
568 break;
569 }
570 else
571 ++it;
572 }
573 }
574 }
575}
576
606 symbol_tablet &symbol_table,
607 message_handlert &message_handler)
608{
609 namespacet ns(symbol_table);
610 for(const auto &entry : symbol_table)
611 {
612 const symbolt &symbol = entry.second;
613
614 if(symbol.type.id() != ID_code)
615 continue;
616 if(symbol.value.is_nil())
617 continue;
618 if(!symbol.type.get_bool(ID_is_synchronized))
619 continue;
620
621 if(symbol.type.get_bool(ID_is_static))
622 {
623 messaget message(message_handler);
624 message.warning() << "Java method '" << entry.first
625 << "' is static and synchronized."
626 << " This is unsupported, the synchronized keyword"
627 << " will be ignored."
628 << messaget::eom;
629 continue;
630 }
631
632 // find the object to synchronize on
633 const irep_idt this_id(id2string(symbol.name) + "::this");
634 exprt this_expr(this_id);
635
636 auto it = symbol_table.symbols.find(this_id);
637
638 if(it == symbol_table.symbols.end())
639 // failed to find object to synchronize on
640 continue;
641
642 // get writeable reference and instrument the method
643 symbolt &w_symbol = symbol_table.get_writeable_ref(entry.first);
645 symbol_table, w_symbol, it->second.symbol_expr());
646 }
647}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
A codet representing an assignment in the program.
A codet representing sequential composition of program statements.
Definition: std_code.h:130
void add(const codet &code)
Definition: std_code.h:168
codet representation of an expression statement.
Definition: std_code.h:1394
codet representation of a function call statement.
codet representation of a goto statement.
Definition: std_code.h:841
codet representation of a label for branch targets.
Definition: std_code.h:959
codet & code()
Definition: std_code.h:977
A statement that catches an exception, assigning the exception in flight to an expression (e....
Definition: std_code.h:1936
Pops an exception handler from the stack of active handlers (i.e.
Definition: std_code.h:1899
Pushes an exception handler, of the form: exception_tag1 -> label1 exception_tag2 -> label2 ....
Definition: std_code.h:1805
exception_listt & exception_list()
Definition: std_code.h:1860
std::vector< exception_list_entryt > exception_listt
Definition: std_code.h:1849
A codet representing a skip statement.
Definition: std_code.h:322
Data structure for representing an arbitrary statement in a program.
Definition: std_code_base.h:29
const irep_idt & get_statement() const
Definition: std_code_base.h:65
Operator to dereference a pointer.
Definition: pointer_expr.h:648
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:129
depth_iteratort depth_end()
Definition: expr.cpp:267
depth_iteratort depth_begin()
Definition: expr.cpp:265
const source_locationt & source_location() const
Definition: expr.h:230
source_locationt & add_source_location()
Definition: expr.h:235
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:372
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:58
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:420
const irep_idt & id() const
Definition: irep.h:396
bool is_nil() const
Definition: irep.h:376
Extract member of struct or union.
Definition: std_expr.h:2667
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
mstreamt & warning() const
Definition: message.h:404
static eomt eom
Definition: message.h:297
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:49
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
The plus expression Associativity is not specified.
Definition: std_expr.h:914
const typet & base_type() const
The type of the data what we point to.
Definition: pointer_expr.h:35
A side_effect_exprt representation of a side effect that throws an exception.
Definition: std_code.h:1757
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:449
Expression to hold a symbol (variable)
Definition: std_expr.h:80
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.
The symbol table.
Definition: symbol_table.h:14
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
bool is_static_lifetime
Definition: symbol.h:65
bool is_thread_local
Definition: symbol.h:65
bool is_state_var
Definition: symbol.h:62
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
typet type
Type of symbol.
Definition: symbol.h:31
irep_idt name
The unique identifier.
Definition: symbol.h:40
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
bool is_lvalue
Definition: symbol.h:66
exprt value
Initial value of symbol.
Definition: symbol.h:34
irep_idt mode
Language mode.
Definition: symbol.h:49
The type of an expression, extends irept.
Definition: type.h:29
#define CPROVER_PREFIX
std::string expr2java(const exprt &expr, const namespacet &ns)
Definition: expr2java.cpp:450
#define Forall_operands(it, expr)
Definition: expr.h:25
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)
Definition: irep.h:47
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()
Definition: java_types.cpp:31
reference_typet java_reference_type(const typet &subtype)
Definition: java_types.cpp:88
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)
Definition: java_utils.cpp:558
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:103
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:79
BigInt mp_integer
Definition: smt_terms.h:12
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:203
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.
Definition: std_expr.h:899
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2840
Pre-defined types.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
Author: Diffblue Ltd.