JBMC: Support for synchronized methods

This commit adds support for synchronized methods by instrumenting all
methods marked with the synchronization flag with calls to
'monitorenter' and 'monitorexit'. These two methods are located in the
java models library and implement a critical section.

To this end the following changes are made:

1. New irep_id, 'is_synchronized', to represent the synchronized keyword
   and appropriate changes to 'java_byecode_convert_method.cpp' to set
   this flag when a synchronized method is encountered.
2. Setting of the 'is_static' flag when the method in question is static.
3. Functions to find and instrument synchronized methods. Specifically,
   calls to "java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V"
   and "java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V" are
   respectively instrumented at the start and end of a synchronized
   method . Note, the former is instrumented at every point where
   the execution of the synchronized methods terminates. Specifically
   out of order return statements and exceptions.

Note: instrumentation of synchronized methods is only triggered if the
      '--java-threading' command line option is specified.

Note': instrumentation of synchronized methods requires the use of the
       java core models library as the locking mechanism is implemented
       in the model 'java.long.Object'.

Note'': static synchronized methods are not supported yet.

Author: Degiorgio

jbmc/src/java_bytecode/Makefile

@@ -8,7 +8,7 @@ SRC = bytecode_info.cpp \
       jar_file.cpp \
       java_bytecode_convert_class.cpp \
       java_bytecode_convert_method.cpp \
-      java_bytecode_convert_threadblock.cpp \
+      java_bytecode_concurrency_instrumentation.cpp \
       java_bytecode_instrument.cpp \
       java_bytecode_internal_additions.cpp \
       java_bytecode_language.cpp \

jbmc/src/java_bytecode/java_bytecode_convert_threadblock.cpp renamed to jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp

@@ -6,14 +6,15 @@ Author: Kurt Degiogrio, kurt.degiorgio@diffblue.com
 
 \*******************************************************************/
 
-#include "java_bytecode_convert_threadblock.h"
+#include "java_bytecode_concurrency_instrumentation.h"
 #include "expr2java.h"
 #include "java_types.h"
 
 #include <util/expr_iterator.h>
 #include <util/namespace.h>
 #include <util/cprover_prefix.h>
 #include <util/std_types.h>
+#include <util/fresh_symbol.h>
 #include <util/arith_tools.h>
 
 // Disable linter to allow an std::string constant.
@@ -38,7 +39,7 @@ static symbolt add_or_get_symbol(
   const bool is_thread_local,
   const bool is_static_lifetime)
 {
-  const symbolt* psymbol = nullptr;
+  const symbolt *psymbol = nullptr;
   namespacet ns(symbol_table);
   ns.lookup(name, psymbol);
   if(psymbol != nullptr)
@@ -89,6 +90,141 @@ static const std::string get_thread_block_identifier(
   return integer2string(lbl_id);
 }
 
+/// Creates a monitorenter/monitorexit code_function_callt for
+/// the given synchronization object.
+/// \param symbol_table: a symbol table
+/// \param is_enter: indicates whether we are creating a monitorenter or
+///   monitorexit.
+/// \param object: expression representing a 'java.Lang.Object'. This object is
+///   used to achieve object-level locking by calling monitoroenter/monitorexit.
+static codet get_monitor_call(
+  const symbol_tablet &symbol_table,
+  bool is_enter,
+  const exprt &object)
+{
+  const std::string 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
+  code_function_callt call;
+  call.function() = symbol_exprt(symbol, it->second.type);
+  call.lhs().make_nil();
+  call.arguments().push_back(object);
+  return call;
+}
+
+/// Introduces a monitorexit before every return recursively
+/// \param [out] code: current element to modify
+/// \param monitorexit: codet to insert before the return
+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_blockt return_block;
+    return_block.add(monitorexit);
+    return_block.move_to_operands(code);
+    code = return_block;
+  }
+  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);
+    }
+  }
+}
+
+/// Transforms the codet stored in in the value field of \p symbol. This
+/// expected to be a codet that needs to be synchronized, the transformation
+/// makes it thread-safe as described in the documentation of function
+/// convert_synchronized_methods
+///
+/// The resulting thread-safe codet is stored in the value field of \p symbol.
+///
+/// \param symbol_table: a symbol_table
+/// \param symbol: writeable symbol hosting code to synchronized
+/// \param sync_object: object to use as a lock
+static void instrument_synchronized_code(
+  symbol_tablet &symbol_table,
+  symbolt &symbol,
+  const exprt &sync_object)
+{
+  codet &code = to_code(symbol.value);
+
+  // Get interposition code for the monitor lock/unlock
+  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 = get_fresh_aux_symbol(
+    java_reference_type(symbol_typet("java::java.lang.Throwable")),
+    id2string(symbol.name),
+    "caught-synchronized-exception",
+    code.source_location(),
+    ID_java,
+    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;
+  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_blockt try_block;
+  try_block.move_to_operands(monitorenter);
+  try_block.move_to_operands(catch_push);
+  try_block.move_to_operands(code);
+  try_block.move_to_operands(catch_pop);
+  try_block.move_to_operands(catch_label);
+  code = try_block;
+}
+
 /// Transforms the codet stored in in \p f_code, which is a call to function
 /// CProver.startThread:(I)V into a block of code as described by the
 /// documentation of function convert_thread_block
@@ -284,20 +420,20 @@ static void instrument_getCurrentThreadID(
 ///
 /// Note': the ID of the thread is assigned after the thread is created, this
 /// creates bogus interleavings. Currently, it's not possible to
-/// assign the thread ID before the creation of the thead, due to a bug in
+/// assign the thread ID before the creation of the thread, due to a bug in
 /// symex. See https://github.com/diffblue/cbmc/issues/1630/for more details.
 ///
 /// \param symbol_table: a symbol table
 void convert_threadblock(symbol_tablet &symbol_table)
 {
   using instrument_callbackt =
-      std::function<void(const code_function_callt&, codet&, symbol_tablet&)>;
+    std::function<void(const code_function_callt&, codet&, symbol_tablet&)>;
   using expr_replacement_mapt =
-      std::unordered_map<const exprt, instrument_callbackt, irep_hash>;
+    std::unordered_map<const exprt, instrument_callbackt, irep_hash>;
 
   namespacet ns(symbol_table);
 
-  for(auto entry : symbol_table)
+  for(const auto &entry : symbol_table)
   {
     expr_replacement_mapt expr_replacement_map;
     const symbolt &symbol = entry.second;
@@ -361,3 +497,58 @@ void convert_threadblock(symbol_tablet &symbol_table)
     }
   }
 }
+
+/// Iterate through the symbol table to find and appropriately instrument
+/// synchronized methods.
+///
+/// A synchronized method is a method with the synchronization keyword. Any
+/// code inside of such methods has to be thread-safe. To this end, a call to
+/// "java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V" and
+/// "java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V" is instrumented
+/// at the start and end of the method. Note, that the former is instrumented
+/// at every statement where the execution can exit the method in question.
+/// Specifically, out of order return statements and exceptions. The latter
+/// is dealt with by instrumenting a try catch block.
+///
+/// Note: current version cannot handle static methods.
+///
+/// Note': This method requires the availability of
+///   "java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V" and
+///   "java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V".
+///   (java-library-models)
+///
+/// \param symbol_table: a symbol table
+void convert_synchronized_methods(symbol_tablet &symbol_table)
+{
+  for(const auto &entry : symbol_table)
+  {
+    const symbolt &symbol = entry.second;
+
+    if(symbol.type.id() != ID_code)
+      continue;
+    if(symbol.value.is_nil())
+      continue;
+    if(symbol.type.get(ID_is_synchronized) != "1")
+      continue;
+
+    bool is_static = (symbol.type.get(ID_is_static) == "1");
+    if(is_static)
+      // FIXME: handle static synchronized methods
+      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 = symbol_table.get_writeable_ref(entry.first);
+    instrument_synchronized_code(
+      symbol_table, w_symbol, it->second.symbol_expr());
+  }
+}

jbmc/src/java_bytecode/java_bytecode_convert_threadblock.h renamed to jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.h

@@ -5,11 +5,13 @@ Module: Java Convert Thread blocks
 Author: Kurt Degiogrio, kurt.degiorgio@diffblue.com
 
 \*******************************************************************/
-#ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_THREADBLOCK_H
-#define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_THREADBLOCK_H
+#ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONCURRENCY_INSTRUMENTATION_H
+#define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONCURRENCY_INSTRUMENTATION_H
 
 #include <util/symbol_table.h>
 
 void convert_threadblock(symbol_tablet &symbol_table);
 
+void convert_synchronized_methods(symbol_tablet &symbol_table);
+
 #endif

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -363,6 +363,11 @@ void java_bytecode_convert_method_lazy(
   else
     member_type.set_access(ID_default);
 
+  if(m.is_synchronized)
+    member_type.set(ID_is_synchronized, true);
+  if(m.is_static)
+    member_type.set(ID_is_static, true);
+
   // do we need to add 'this' as a parameter?
   if(!m.is_static)
   {

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -22,9 +22,9 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <goto-programs/class_hierarchy.h>
 
+#include "java_bytecode_concurrency_instrumentation.h"
 #include "java_bytecode_convert_class.h"
 #include "java_bytecode_convert_method.h"
-#include "java_bytecode_convert_threadblock.h"
 #include "java_bytecode_internal_additions.h"
 #include "java_bytecode_instrument.h"
 #include "java_bytecode_typecheck.h"
@@ -755,9 +755,12 @@ bool java_bytecode_languaget::typecheck(
   bool res = java_bytecode_typecheck(
     symbol_table, get_message_handler(), string_refinement_enabled);
 
-  // now instrument thread-blocks
+  // now instrument thread-blocks and synchronized methods.
   if(threading_support)
+  {
     convert_threadblock(symbol_table);
+    convert_synchronized_methods(symbol_table);
+  }
 
   return res;
 }

src/util/irep_ids.def

@@ -384,6 +384,7 @@ IREP_ID_TWO(C_is_anonymous, #is_anonymous)
 IREP_ID_ONE(is_enum_constant)
 IREP_ID_ONE(is_inline)
 IREP_ID_ONE(is_extern)
+IREP_ID_ONE(is_synchronized)
 IREP_ID_ONE(is_global)
 IREP_ID_ONE(is_thread_local)
 IREP_ID_ONE(is_parameter)