cprover
java_bytecode_concurrency_instrumentation.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Java Convert Thread blocks
4 
5 Author: Kurt Degiogrio, kurt.degiorgio@diffblue.com
6 
7 \*******************************************************************/
8 
10 #include "expr2java.h"
11 #include "java_types.h"
12 
13 #include <util/expr_iterator.h>
14 #include <util/namespace.h>
15 #include <util/cprover_prefix.h>
16 #include <util/std_types.h>
17 #include <util/fresh_symbol.h>
18 #include <util/arith_tools.h>
19 
20 // Disable linter to allow an std::string constant.
21 const std::string next_thread_id = CPROVER_PREFIX "_next_thread_id";// NOLINT(*)
22 const std::string thread_id = CPROVER_PREFIX "_thread_id";// NOLINT(*)
23 
34  symbol_tablet &symbol_table,
35  const irep_idt &name,
36  const irep_idt &base_name,
37  const typet &type,
38  const exprt &value,
39  const bool is_thread_local,
40  const bool is_static_lifetime)
41 {
42  const symbolt *psymbol = nullptr;
43  namespacet ns(symbol_table);
44  ns.lookup(name, psymbol);
45  if(psymbol != nullptr)
46  return *psymbol;
47  symbolt new_symbol;
48  new_symbol.name = name;
49  new_symbol.pretty_name = name;
50  new_symbol.base_name = base_name;
51  new_symbol.type = type;
52  new_symbol.value = value;
53  new_symbol.is_lvalue = true;
54  new_symbol.is_state_var = true;
55  new_symbol.is_static_lifetime = is_static_lifetime;
56  new_symbol.is_thread_local = is_thread_local;
57  new_symbol.mode = ID_java;
58  symbol_table.add(new_symbol);
59  return new_symbol;
60 }
61 
66 static const std::string get_first_label_id(const std::string &id)
67 {
68  return CPROVER_PREFIX "_THREAD_ENTRY_" + id;
69 }
70 
75 static const std::string get_second_label_id(const std::string &id)
76 {
77  return CPROVER_PREFIX "_THREAD_EXIT_" + id;
78 }
79 
84 static const std::string get_thread_block_identifier(
85  const code_function_callt &f_code)
86 {
87  PRECONDITION(f_code.arguments().size() == 1);
88  const exprt &expr = f_code.arguments()[0];
89  mp_integer lbl_id = binary2integer(expr.op0().get_string(ID_value), false);
90  return integer2string(lbl_id);
91 }
92 
101  const symbol_tablet &symbol_table,
102  bool is_enter,
103  const exprt &object)
104 {
105  const irep_idt symbol =
106  is_enter ? "java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V"
107  : "java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V";
108 
109  auto it = symbol_table.symbols.find(symbol);
110 
111  // If the 'java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V' or
112  // 'java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V' method is not
113  // found symex will rightfully complain as it cannot find the symbol
114  // associated with the method in question. To avoid this and thereby ensuring
115  // JBMC works both with and without the models, we replace the aforementioned
116  // methods with skips when we cannot find them.
117  //
118  // Note: this can only happen if the java-core-models library is not loaded.
119  //
120  // Note': we explicitly prevent JBMC from stubbing these methods.
121  if(it == symbol_table.symbols.end())
122  return code_skipt();
123 
124  // Otherwise we create a function call
125  code_function_callt call;
126  call.function() = symbol_exprt(symbol, it->second.type);
127  call.lhs().make_nil();
128  call.arguments().push_back(object);
129  return call;
130 }
131 
136 static void monitor_exits(codet &code, const codet &monitorexit)
137 {
138  const irep_idt &statement = code.get_statement();
139  if(statement == ID_return)
140  {
141  // Replace the return with a monitor exit plus return block
142  code_blockt return_block;
143  return_block.add(monitorexit);
144  return_block.move_to_operands(code);
145  code = return_block;
146  }
147  else if(
148  statement == ID_label || statement == ID_block ||
149  statement == ID_decl_block)
150  {
151  // If label or block found, explore the code inside the block
152  Forall_operands(it, code)
153  {
154  codet &sub_code = to_code(*it);
155  monitor_exits(sub_code, monitorexit);
156  }
157  }
158 }
159 
213  symbol_tablet &symbol_table,
214  symbolt &symbol,
215  const exprt &sync_object)
216 {
217  PRECONDITION(!symbol.type.get_bool(ID_is_static));
218 
219  codet &code = to_code(symbol.value);
220 
221  // Get the calls to the functions that implement the critical section
222  codet monitorenter = get_monitor_call(symbol_table, true, sync_object);
223  codet monitorexit = get_monitor_call(symbol_table, false, sync_object);
224 
225  // Create a unique catch label and empty throw type (i.e. any)
226  // and catch-push them at the beginning of the code (i.e. begin try)
227  code_push_catcht catch_push;
228  irep_idt handler("pc-synchronized-catch");
229  irep_idt exception_id;
230  code_push_catcht::exception_listt &exception_list =
231  catch_push.exception_list();
232  exception_list.push_back(
233  code_push_catcht::exception_list_entryt(exception_id, handler));
234 
235  // Create a catch-pop to indicate the end of the try block
236  code_pop_catcht catch_pop;
237 
238  // Create the finally block with the same label targeted in the catch-push
239  const symbolt &tmp_symbol = get_fresh_aux_symbol(
240  java_reference_type(symbol_typet("java::java.lang.Throwable")),
241  id2string(symbol.name),
242  "caught-synchronized-exception",
243  code.source_location(),
244  ID_java,
245  symbol_table);
246  symbol_exprt catch_var(tmp_symbol.name, tmp_symbol.type);
247  catch_var.set(ID_C_base_name, tmp_symbol.base_name);
248  code_landingpadt catch_statement(catch_var);
249  codet catch_instruction = catch_statement;
250  code_labelt catch_label(handler, code_blockt());
251  code_blockt &catch_block = to_code_block(catch_label.code());
252  catch_block.add(catch_instruction);
253  catch_block.add(monitorexit);
254 
255  // Re-throw exception
256  side_effect_expr_throwt throw_expr(irept(), typet(), code.source_location());
257  throw_expr.copy_to_operands(catch_var);
258  catch_block.add(code_expressiont(throw_expr));
259 
260  // Write a monitorexit before every return
261  monitor_exits(code, monitorexit);
262 
263  // Wrap the code into a try finally
264  code_blockt try_block;
265  try_block.move_to_operands(monitorenter);
266  try_block.move_to_operands(catch_push);
267  try_block.move_to_operands(code);
268  try_block.move_to_operands(catch_pop);
269  try_block.move_to_operands(catch_label);
270  code = try_block;
271 }
272 
283  const code_function_callt &f_code,
284  codet &code,
285  symbol_tablet &symbol_table)
286 {
287  PRECONDITION(f_code.arguments().size() == 1);
288 
289  // Create global variable __CPROVER__next_thread_id. Used as a counter
290  // in-order to to assign ids to new threads.
291  const symbolt &next_symbol =
293  symbol_table, next_thread_id, next_thread_id,
294  java_int_type(),
295  from_integer(0, java_int_type()), false, true);
296 
297  // Create thread-local variable __CPROVER__thread_id. Holds the id of
298  // the thread.
299  const symbolt &current_symbol =
301  symbol_table, thread_id, thread_id, java_int_type(),
302  from_integer(0, java_int_type()), true, true);
303 
304  // Construct appropriate labels.
305  // Note: java does not have labels so this should be safe.
306  const std::string &thread_block_id = get_thread_block_identifier(f_code);
307  const std::string &lbl1 = get_first_label_id(thread_block_id);
308  const std::string &lbl2 = get_second_label_id(thread_block_id);
309 
310  // Instrument the following codet's:
311  //
312  // A: codet(id=ID_start_thread, destination=__CPROVER_THREAD_ENTRY_<ID>)
313  // B: codet(id=ID_goto, destination=__CPROVER_THREAD_EXIT_<ID>)
314  // C: codet(id=ID_label, label=__CPROVER_THREAD_ENTRY_<ID>)
315  // C.1: codet(id=ID_atomic_begin)
316  // D: CPROVER__next_thread_id += 1;
317  // E: __CPROVER__thread_id = __CPROVER__next_thread_id;
318  // F: codet(id=ID_atomic_end)
319 
320  codet tmp_a(ID_start_thread);
321  tmp_a.set(ID_destination, lbl1);
322  code_gotot tmp_b(lbl2);
323  code_labelt tmp_c(lbl1);
324  tmp_c.op0() = codet(ID_skip);
325 
326  exprt plus(ID_plus, java_int_type());
327  plus.copy_to_operands(next_symbol.symbol_expr());
329  code_assignt tmp_d(next_symbol.symbol_expr(), plus);
330  code_assignt tmp_e(current_symbol.symbol_expr(), next_symbol.symbol_expr());
331 
332  code_blockt block;
333  block.add(tmp_a);
334  block.add(tmp_b);
335  block.add(tmp_c);
336  block.add(codet(ID_atomic_begin));
337  block.add(tmp_d);
338  block.add(tmp_e);
339  block.add(codet(ID_atomic_end));
340  block.add_source_location() = f_code.source_location();
341 
342  code = block;
343 }
344 
355  const code_function_callt &f_code,
356  codet &code,
357  const symbol_tablet &symbol_table)
358 {
359  PRECONDITION(f_code.arguments().size() == 1);
360 
361  // Build id, used to construct appropriate labels.
362  // Note: java does not have labels so this should be safe
363  const std::string &thread_block_id = get_thread_block_identifier(f_code);
364  const std::string &lbl2 = get_second_label_id(thread_block_id);
365 
366  // Instrument the following code:
367  //
368  // A: codet(id=ID_end_thread)
369  // B: codet(id=ID_label,label= __CPROVER_THREAD_EXIT_<ID>)
370  codet tmp_a(ID_end_thread);
371  code_labelt tmp_b(lbl2);
372  tmp_b.op0() = codet(ID_skip);
373 
374  code_blockt block;
375  block.add(tmp_a);
376  block.add(tmp_b);
377  block.add_source_location() = code.source_location();
378 
379  code = block;
380 }
381 
392  const code_function_callt &f_code,
393  codet &code,
394  symbol_tablet &symbol_table)
395 {
396  PRECONDITION(f_code.arguments().size() == 0);
397 
398  const symbolt& current_symbol =
399  add_or_get_symbol(symbol_table,
400  thread_id,
401  thread_id,
402  java_int_type(),
404  true, true);
405 
406  code_assignt code_assign(f_code.lhs(), current_symbol.symbol_expr());
407  code_assign.add_source_location() = f_code.source_location();
408 
409  code = code_assign;
410 }
411 
473 {
474  using instrument_callbackt =
475  std::function<void(const code_function_callt&, codet&, symbol_tablet&)>;
476  using expr_replacement_mapt =
477  std::unordered_map<const exprt, instrument_callbackt, irep_hash>;
478 
479  namespacet ns(symbol_table);
480 
481  for(const auto &entry : symbol_table)
482  {
483  expr_replacement_mapt expr_replacement_map;
484  const symbolt &symbol = entry.second;
485 
486  // Look for code_function_callt's (without breaking sharing)
487  // and insert each one into a replacement map along with an associated
488  // callback that will handle their instrumentation.
489  for(auto it = symbol.value.depth_begin(), itend = symbol.value.depth_end();
490  it != itend; ++it)
491  {
492  instrument_callbackt cb;
493 
494  const exprt &expr = *it;
495  if(expr.id() != ID_code)
496  continue;
497 
498  const codet &code = to_code(expr);
499  if(code.get_statement() != ID_function_call)
500  continue;
501 
502  const code_function_callt &f_code = to_code_function_call(code);
503  const std::string &f_name = expr2java(f_code.function(), ns);
504  if(f_name == "org.cprover.CProver.startThread:(I)V")
505  cb = std::bind(
507  std::placeholders::_1,
508  std::placeholders::_2,
509  std::placeholders::_3);
510  else if(f_name == "org.cprover.CProver.endThread:(I)V")
511  cb = std::bind(
513  std::placeholders::_1,
514  std::placeholders::_2,
515  std::placeholders::_3);
516  else if(f_name == "org.cprover.CProver.getCurrentThreadID:()I")
517  cb = std::bind(
519  std::placeholders::_1,
520  std::placeholders::_2,
521  std::placeholders::_3);
522 
523  if(cb)
524  expr_replacement_map.insert({expr, cb});
525  }
526 
527  if(!expr_replacement_map.empty())
528  {
529  symbolt &w_symbol = symbol_table.get_writeable_ref(entry.first);
530  // Use expr_replacment_map to look for exprt's that need to be replaced.
531  // Once found, get a non-const exprt (breaking sharing in the process) and
532  // call it's associated instrumentation function.
533  for(auto it = w_symbol.value.depth_begin(),
534  itend = w_symbol.value.depth_end(); it != itend;)
535  {
536  expr_replacement_mapt::iterator m_it = expr_replacement_map.find(*it);
537  if(m_it != expr_replacement_map.end())
538  {
539  codet &code = to_code(it.mutate());
540  const code_function_callt &f_code = to_code_function_call(code);
541  m_it->second(f_code, code, symbol_table);
542  it.next_sibling_or_parent();
543 
544  expr_replacement_map.erase(m_it);
545  if(expr_replacement_map.empty())
546  break;
547  }
548  else
549  ++it;
550  }
551  }
552  }
553 }
554 
584  symbol_tablet &symbol_table,
586 {
587  namespacet ns(symbol_table);
588  for(const auto &entry : symbol_table)
589  {
590  const symbolt &symbol = entry.second;
591 
592  if(symbol.type.id() != ID_code)
593  continue;
594  if(symbol.value.is_nil())
595  continue;
596  if(!symbol.type.get_bool(ID_is_synchronized))
597  continue;
598 
599  if(symbol.type.get_bool(ID_is_static))
600  {
601  messaget message(message_handler);
602  message.warning() << "Java method '" << entry.first
603  << "' is static and synchronized."
604  << " This is unsupported, the synchronized keyword"
605  << " will be ignored."
606  << messaget::eom;
607  continue;
608  }
609 
610  // find the object to synchronize on
611  const irep_idt this_id(id2string(symbol.name) + "::this");
612  exprt this_expr(this_id);
613 
614  auto it = symbol_table.symbols.find(this_id);
615 
616  if(it == symbol_table.symbols.end())
617  // failed to find object to synchronize on
618  continue;
619 
620  // get writeable reference and instrument the method
621  symbolt &w_symbol = symbol_table.get_writeable_ref(entry.first);
623  symbol_table, w_symbol, it->second.symbol_expr());
624  }
625 }
const irep_idt & get_statement() const
Definition: std_code.h:40
The type of an expression.
Definition: type.h:22
irep_idt name
The unique identifier.
Definition: symbol.h:43
std::vector< exception_list_entryt > exception_listt
Definition: std_code.h:1589
BigInt mp_integer
Definition: mp_arith.h:22
bool is_nil() const
Definition: irep.h:172
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_thread_local
Definition: symbol.h:67
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:106
exprt & op0()
Definition: expr.h:72
#define CPROVER_PREFIX
irep_idt mode
Language mode.
Definition: symbol.h:52
reference_typet java_reference_type(const typet &subtype)
Definition: java_types.cpp:80
typet java_int_type()
Definition: java_types.cpp:32
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:55
Pushes an exception handler, of the form: exception_tag1 -> label1 exception_tag2 -> label2 ...
Definition: std_code.h:1544
void move_to_operands(exprt &expr)
Definition: expr.cpp:22
Fresh auxiliary symbol creation.
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
Definition: mp_arith.cpp:120
exprt value
Initial value of symbol.
Definition: symbol.h:37
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...
const std::string thread_id
A ‘goto’ instruction.
Definition: std_code.h:803
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:55
Pops an exception handler from the stack of active handlers (i.e.
Definition: std_code.h:1632
depth_iteratort depth_begin()
Definition: expr.cpp:299
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
An expression statement.
Definition: std_code.h:1220
A side effect that throws an exception.
Definition: std_code.h:1491
bool is_static_lifetime
Definition: symbol.h:67
mstreamt & warning() const
Definition: message.h:307
const irep_idt & id() const
Definition: irep.h:259
void add(const codet &code)
Definition: std_code.h:112
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:111
argumentst & arguments()
Definition: std_code.h:890
void convert_synchronized_methods(symbol_tablet &symbol_table, message_handlert &message_handler)
Iterate through the symbol table to find and instrument synchronized methods.
A reference into the symbol table.
Definition: std_types.h:110
codet & code()
Definition: std_code.h:1010
The symbol table.
Definition: symbol_table.h:19
TO_BE_DOCUMENTED.
Definition: namespace.h:74
A label for branch targets.
Definition: std_code.h:977
#define PRECONDITION(CONDITION)
Definition: invariant.h:242
Base class for tree-like data structures with sharing.
Definition: irep.h:156
A function call.
Definition: std_code.h:858
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 ...
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
static void monitor_exits(codet &code, const codet &monitorexit)
Introduces a monitorexit before every return recursively.
const symbolst & symbols
const source_locationt & source_location() const
Definition: type.h:97
typet type
Type of symbol.
Definition: symbol.h:34
API to type classes.
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...
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with the requested name pattern.
exprt & function()
Definition: std_code.h:878
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&#39;t exist.
Base class for all expressions.
Definition: expr.h:42
bool is_state_var
Definition: symbol.h:63
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:49
const std::string next_thread_id
const source_locationt & source_location() const
Definition: expr.h:125
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...
void make_nil()
Definition: irep.h:315
#define Forall_operands(it, expr)
Definition: expr.h:23
source_locationt & add_source_location()
Definition: expr.h:130
Sequential composition.
Definition: std_code.h:89
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...
const codet & to_code(const exprt &expr)
Definition: std_code.h:75
void convert_threadblock(symbol_tablet &symbol_table)
Iterate through the symbol table to find and appropriately instrument thread-blocks.
static const std::string get_second_label_id(const std::string &id)
Retrieve the second label identifier.
static void instrument_synchronized_code(symbol_tablet &symbol_table, symbolt &symbol, const exprt &sync_object)
Transforms the codet stored in symbol.value.
Skip.
Definition: std_code.h:179
Expression to hold a symbol (variable)
Definition: std_expr.h:90
depth_iteratort depth_end()
Definition: expr.cpp:301
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:165
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
goto_programt coverage_criteriont message_handlert & message_handler
Definition: cover.cpp:66
A statement in a programming language.
Definition: std_code.h:21
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
exception_listt & exception_list()
Definition: std_code.h:1600
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:136
Assignment.
Definition: std_code.h:196
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
std::string expr2java(const exprt &expr, const namespacet &ns)
Definition: expr2java.cpp:453
static const std::string get_first_label_id(const std::string &id)
Retrieve the first label identifier.
A statement that catches an exception, assigning the exception in flight to an expression (e...
Definition: std_code.h:1663
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:909
bool is_lvalue
Definition: symbol.h:68