java_bytecode_concurrency_instrumentation.cpp

Go to the documentation of this file.

/*******************************************************************\
 
Module: Java Convert Thread blocks
 
Author: Kurt Degiogrio, kurt.degiorgio@diffblue.com
 
\*******************************************************************/
 
#include "java_bytecode_concurrency_instrumentation.h"
 
#include <util/arith_tools.h>
#include <util/cprover_prefix.h>
#include <util/expr_iterator.h>
#include <util/message.h>
#include <util/namespace.h>
#include <util/std_types.h>
#include <util/symbol_table_base.h>
 
#include "expr2java.h"
#include "java_types.h"
#include "java_utils.h"
 
// Disable linter to allow an std::string constant.
const std::string next_thread_id = CPROVER_PREFIX "_next_thread_id";// NOLINT(*)
const std::string thread_id = CPROVER_PREFIX "_thread_id";// NOLINT(*)
 
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)
{
  const symbolt *psymbol = nullptr;
  namespacet ns(symbol_table);
  ns.lookup(name, psymbol);
  if(psymbol != nullptr)
    return *psymbol;
  symbolt new_symbol{name, type, ID_java};
  new_symbol.pretty_name = name;
  new_symbol.base_name = base_name;
  new_symbol.value = value;
  new_symbol.is_lvalue = true;
  new_symbol.is_state_var = true;
  new_symbol.is_static_lifetime = is_static_lifetime;
  new_symbol.is_thread_local = is_thread_local;
  symbol_table.add(new_symbol);
  return new_symbol;
}
 
static const std::string get_first_label_id(const std::string &id)
{
  return CPROVER_PREFIX "_THREAD_ENTRY_" + id;
}
 
static const std::string get_second_label_id(const std::string &id)
{
  return CPROVER_PREFIX "_THREAD_EXIT_" + id;
}
 
static const std::string get_thread_block_identifier(
  const code_function_callt &f_code)
{
  PRECONDITION(f_code.arguments().size() == 1);
  const exprt &expr = f_code.arguments()[0];
  const mp_integer lbl_id =
    numeric_cast_v<mp_integer>(to_constant_expr(to_multi_ary_expr(expr).op0()));
  return integer2string(lbl_id);
}
 
static codet get_monitor_call(
  const symbol_table_baset &symbol_table,
  bool is_enter,
  const exprt &object)
{
  const irep_idt symbol =
    is_enter ? "java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V"
             : "java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V";
 
  auto it = symbol_table.symbols.find(symbol);
 
  // If the 'java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V' or
  // 'java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V' method is not
  // found symex will rightfully complain as it cannot find the symbol
  // associated with the method in question. To avoid this and thereby ensuring
  // JBMC works both with and without the models, we replace the aforementioned
  // methods with skips when we cannot find them.
  //
  // Note: this can only happen if the java-core-models library is not loaded.
  //
  // Note': we explicitly prevent JBMC from stubbing these methods.
  if(it == symbol_table.symbols.end())
    return code_skipt();
 
  // Otherwise we create a function call
  return code_function_callt(symbol_exprt(symbol, it->second.type), {object});
}
 
static void monitor_exits(codet &code, const codet &monitorexit)
{
  const irep_idt &statement = code.get_statement();
  if(statement == ID_return)
  {
    // Replace the return with a monitor exit plus return block
    code = code_blockt({monitorexit, code});
  }
  else if(
    statement == ID_label || statement == ID_block ||
    statement == ID_decl_block)
  {
    // If label or block found, explore the code inside the block
    Forall_operands(it, code)
    {
      codet &sub_code = to_code(*it);
      monitor_exits(sub_code, monitorexit);
    }
  }
}
 
static void instrument_synchronized_code(
  symbol_table_baset &symbol_table,
  symbolt &symbol,
  const exprt &sync_object)
{
  PRECONDITION(!symbol.type.get_bool(ID_is_static));
 
  codet &code = to_code(symbol.value);
 
  // Get the calls to the functions that implement the critical section
  codet monitorenter = get_monitor_call(symbol_table, true, sync_object);
  codet monitorexit = get_monitor_call(symbol_table, false, sync_object);
 
  // Create a unique catch label and empty throw type (i.e. any)
  // and catch-push them at the beginning of the code (i.e. begin try)
  code_push_catcht catch_push;
  irep_idt handler("pc-synchronized-catch");
  irep_idt exception_id;
  code_push_catcht::exception_listt &exception_list =
    catch_push.exception_list();
  exception_list.push_back(
    code_push_catcht::exception_list_entryt(exception_id, handler));
 
  // Create a catch-pop to indicate the end of the try block
  code_pop_catcht catch_pop;
 
  // Create the finally block with the same label targeted in the catch-push
  const symbolt &tmp_symbol = fresh_java_symbol(
    java_reference_type(struct_tag_typet("java::java.lang.Throwable")),
    "caught-synchronized-exception",
    code.source_location(),
    id2string(symbol.name),
    symbol_table);
  symbol_exprt catch_var(tmp_symbol.name, tmp_symbol.type);
  catch_var.set(ID_C_base_name, tmp_symbol.base_name);
  code_landingpadt catch_statement(catch_var);
  codet catch_instruction = catch_statement;
  code_labelt catch_label(handler, code_blockt());
  code_blockt &catch_block = to_code_block(catch_label.code());
  catch_block.add(catch_instruction);
  catch_block.add(monitorexit);
 
  // Re-throw exception
  side_effect_expr_throwt throw_expr(irept(), typet(), code.source_location());
  throw_expr.copy_to_operands(catch_var);
  catch_block.add(code_expressiont(throw_expr));
 
  // Write a monitorexit before every return
  monitor_exits(code, monitorexit);
 
  // Wrap the code into a try finally
  code = code_blockt({monitorenter, catch_push, code, catch_pop, catch_label});
}
 
static void instrument_start_thread(
  const code_function_callt &f_code,
  codet &code,
  symbol_table_baset &symbol_table)
{
  PRECONDITION(f_code.arguments().size() == 1);
 
  // Create global variable __CPROVER__next_thread_id. Used as a counter
  // in-order to to assign ids to new threads.
  const symbol_exprt next_symbol_expr = add_or_get_symbol(
                                          symbol_table,
                                          next_thread_id,
                                          next_thread_id,
                                          java_int_type(),
                                          from_integer(0, java_int_type()),
                                          false,
                                          true)
                                          .symbol_expr();
 
  // Create thread-local variable __CPROVER__thread_id. Holds the id of
  // the thread.
  const symbolt &current_symbol =
    add_or_get_symbol(
        symbol_table, thread_id, thread_id, java_int_type(),
        from_integer(0, java_int_type()), true, true);
 
  // Construct appropriate labels.
  // Note: java does not have labels so this should be safe.
  const std::string &thread_block_id = get_thread_block_identifier(f_code);
  const std::string &lbl1 = get_first_label_id(thread_block_id);
  const std::string &lbl2 = get_second_label_id(thread_block_id);
 
  // Instrument the following codet's:
  //
  // A: codet(id=ID_start_thread, destination=__CPROVER_THREAD_ENTRY_<ID>)
  // B: codet(id=ID_goto, destination=__CPROVER_THREAD_EXIT_<ID>)
  // C: codet(id=ID_label, label=__CPROVER_THREAD_ENTRY_<ID>)
  // C.1: codet(id=ID_atomic_begin)
  // D: CPROVER__next_thread_id += 1;
  // E: __CPROVER__thread_id = __CPROVER__next_thread_id;
  // F: codet(id=ID_atomic_end)
 
  codet tmp_a(ID_start_thread);
  tmp_a.set(ID_destination, lbl1);
  code_gotot tmp_b(lbl2);
  const code_labelt tmp_c(lbl1, code_skipt());
 
  const plus_exprt plus(next_symbol_expr, from_integer(1, java_int_type()));
  const code_assignt tmp_d(next_symbol_expr, plus);
  const code_assignt tmp_e(current_symbol.symbol_expr(), next_symbol_expr);
 
  code = code_blockt({tmp_a,
                      tmp_b,
                      tmp_c,
                      codet(ID_atomic_begin),
                      tmp_d,
                      tmp_e,
                      codet(ID_atomic_end)});
  code.add_source_location() = f_code.source_location();
}
 
static void instrument_end_thread(
  const code_function_callt &f_code,
  codet &code,
  const symbol_table_baset &symbol_table)
{
  PRECONDITION(f_code.arguments().size() == 1);
  (void)symbol_table; // unused parameter
 
  // Build id, used to construct appropriate labels.
  // Note: java does not have labels so this should be safe
  const std::string &thread_block_id = get_thread_block_identifier(f_code);
  const std::string &lbl2 = get_second_label_id(thread_block_id);
 
  // Instrument the following code:
  //
  // A: codet(id=ID_end_thread)
  // B: codet(id=ID_label,label= __CPROVER_THREAD_EXIT_<ID>)
  codet tmp_a(ID_end_thread);
  const code_labelt tmp_b(lbl2, code_skipt());
 
  const auto location = code.source_location();
  code = code_blockt({tmp_a, tmp_b});
  code.add_source_location() = location;
}
 
static void instrument_get_current_thread_id(
  const code_function_callt &f_code,
  codet &code,
  symbol_table_baset &symbol_table)
{
  PRECONDITION(f_code.arguments().size() == 0);
 
  const symbolt& current_symbol =
    add_or_get_symbol(symbol_table,
      thread_id,
      thread_id,
      java_int_type(),
      from_integer(0, java_int_type()),
      true, true);
 
  code_assignt code_assign(f_code.lhs(), current_symbol.symbol_expr());
  code_assign.add_source_location() = f_code.source_location();
 
  code = code_assign;
}
 
static void instrument_get_monitor_count(
  const code_function_callt &f_code,
  codet &code,
  symbol_table_baset &symbol_table)
{
  PRECONDITION(f_code.arguments().size() == 1);
 
  const namespacet ns(symbol_table);
  const auto &object_type = ns.follow_tag(to_struct_tag_type(
    to_pointer_type(f_code.arguments()[0].type()).base_type()));
  code_assignt code_assign(
    f_code.lhs(),
    member_exprt(
      dereference_exprt(f_code.arguments()[0]),
      object_type.get_component("cproverMonitorCount")));
  code_assign.add_source_location() = f_code.source_location();
 
  code = code_assign;
}
 
void convert_threadblock(symbol_table_baset &symbol_table)
{
  using instrument_callbackt = std::function<void(
    const code_function_callt &, codet &, symbol_table_baset &)>;
  using expr_replacement_mapt =
    std::unordered_map<const exprt, instrument_callbackt, irep_hash>;
 
  namespacet ns(symbol_table);
 
  for(const auto &entry : symbol_table)
  {
    expr_replacement_mapt expr_replacement_map;
    const symbolt &symbol = entry.second;
 
    // Look for code_function_callt's (without breaking sharing)
    // and insert each one into a replacement map along with an associated
    // callback that will handle their instrumentation.
    for(auto it = symbol.value.depth_begin(), itend = symbol.value.depth_end();
       it != itend; ++it)
    {
      instrument_callbackt cb;
 
      const exprt &expr = *it;
      if(expr.id() != ID_code)
        continue;
 
      const codet &code = to_code(expr);
      if(code.get_statement() != ID_function_call)
        continue;
 
      const code_function_callt &f_code = to_code_function_call(code);
      const std::string &f_name = expr2java(f_code.function(), ns);
      if(f_name == "org.cprover.CProver.startThread:(I)V")
        cb = std::bind(
          instrument_start_thread,
          std::placeholders::_1,
          std::placeholders::_2,
          std::placeholders::_3);
      else if(f_name == "org.cprover.CProver.endThread:(I)V")
        cb = std::bind(
          &instrument_end_thread,
          std::placeholders::_1,
          std::placeholders::_2,
          std::placeholders::_3);
      else if(f_name == "org.cprover.CProver.getCurrentThreadId:()I")
        cb = std::bind(
          &instrument_get_current_thread_id,
          std::placeholders::_1,
          std::placeholders::_2,
          std::placeholders::_3);
      else if(
        f_name == "org.cprover.CProver.getMonitorCount:(Ljava/lang/Object;)I")
        cb = std::bind(
          &instrument_get_monitor_count,
          std::placeholders::_1,
          std::placeholders::_2,
          std::placeholders::_3);
 
      if(cb)
        expr_replacement_map.insert({expr, cb});
    }
 
    if(!expr_replacement_map.empty())
    {
      symbolt &w_symbol = symbol_table.get_writeable_ref(entry.first);
      // Use expr_replacment_map to look for exprt's that need to be replaced.
      // Once found, get a non-const exprt (breaking sharing in the process) and
      // call it's associated instrumentation function.
      for(auto it = w_symbol.value.depth_begin(),
         itend = w_symbol.value.depth_end(); it != itend;)
      {
        expr_replacement_mapt::iterator m_it = expr_replacement_map.find(*it);
        if(m_it != expr_replacement_map.end())
        {
          codet &code = to_code(it.mutate());
          const code_function_callt &f_code = to_code_function_call(code);
          m_it->second(f_code, code, symbol_table);
          it.next_sibling_or_parent();
 
          expr_replacement_map.erase(m_it);
          if(expr_replacement_map.empty())
            break;
        }
        else
          ++it;
      }
    }
  }
}
 
void convert_synchronized_methods(
  symbol_table_baset &symbol_table,
  message_handlert &message_handler)
{
  namespacet ns(symbol_table);
  for(auto s_it = symbol_table.begin(); s_it != symbol_table.end(); ++s_it)
  {
    const symbolt &symbol = s_it->second;
 
    if(symbol.type.id() != ID_code)
      continue;
    if(symbol.value.is_nil())
      continue;
    if(!symbol.type.get_bool(ID_is_synchronized))
      continue;
 
    if(symbol.type.get_bool(ID_is_static))
    {
      messaget message(message_handler);
      message.warning() << "Java method '" << s_it->first
                        << "' is static and synchronized."
                        << " This is unsupported, the synchronized keyword"
                        << " will be ignored." << messaget::eom;
      continue;
    }
 
    // find the object to synchronize on
    const irep_idt this_id(id2string(symbol.name) + "::this");
    exprt this_expr(this_id);
 
    auto it = symbol_table.symbols.find(this_id);
 
    if(it == symbol_table.symbols.end())
      // failed to find object to synchronize on
      continue;
 
    // get writeable reference and instrument the method
    symbolt &w_symbol = s_it.get_writeable_symbol();
    instrument_synchronized_code(
      symbol_table, w_symbol, it->second.symbol_expr());
  }
}