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.

Static synchronized methods are not supported yet as the synchronization
semantics for static methods is different (locking on the class instead
the of the object). Upon encountering a static synchronized method the
current implementation will ignore the synchronized flag.  (showing a
warning in the process). This may obviously result in superfluous
interleavings.

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'.

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, [email protected]
 
 \*******************************************************************/
 
-#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,186 @@ 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 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
+  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.
+/// Note: this breaks sharing on \p code
+/// \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 \c symbol.value. The \p symbol is expected to
+/// be a Java synchronized method. Java synchronized methods do not have
+/// explicit calls to the instructions monitorenter and monitorexit, the JVM
+/// interprets the synchronized flag in a method and uses monitor of the object
+/// to implement locking and unlocking. Therefore JBMC has to emulate this same
+/// behavior. We insert a call to our model of monitorenter at the beginning of
+/// the method and calls to our model of monitorexit at each return instruction.
+/// We wrap the entire body of the method with an exception handler that will
+/// call our model of monitorexit if the method returns exceptionally.
+///
+/// Example:
+///
+/// \code
+/// synchronized int amethod(int p)
+/// {
+///   int x = 0;
+///   if(p == 0)
+///     return -1;
+///   x = p / 10
+///   return x
+/// }
+/// \endcode
+///
+/// Is transformed into the codet equivalent of:
+///
+/// \code
+/// synchronized int amethod(int p)
+/// {
+///   try
+///   {
+///     java::java.lang.Object.monitorenter(this);
+///     int x = 0;
+///     if(p == 0)
+///     {
+///       java::java.lang.Object.monitorexit(this);
+///       return -1;
+///     }
+///     java::java.lang.Object.monitorexit(this);
+///     return x
+///   }
+///   catch(java::java.lang.Throwable e)
+///   {
+///     // catch every exception, including errors!
+///     java::java.lang.Object.monitorexit(this);
+///     throw e;
+///   }
+/// }
+/// \endcode
+///
+/// \param symbol_table: a symbol_table
+/// \param symbol: writeable symbol hosting code to synchronize
+/// \param sync_object: object to use as a lock
+static void instrument_synchronized_code(
+  symbol_tablet &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 = 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 +465,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 +542,75 @@ void convert_threadblock(symbol_tablet &symbol_table)
     }
   }
 }
+
+/// Iterate through the symbol table to find and instrument synchronized
+/// methods.
+///
+/// Synchronized methods make it impossible for two invocations of the same
+/// method on the same object to interleave. In-order to replicate
+/// these semantics 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: Static synchronized methods are not supported yet as the
+///   synchronization semantics for static methods is different (locking on the
+///   class instead the of the object). Upon encountering a static synchronized
+///   method the current implementation will ignore the synchronized flag.
+///   (showing a warning in the process). This may result in superfluous
+///   interleavings.
+///
+/// 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). If they are not available code_skipt will inserted
+///   instead of calls to the aforementioned methods.
+///
+/// \param symbol_table: a symbol table
+/// \param message_handler: status output
+void convert_synchronized_methods(
+  symbol_tablet &symbol_table,
+  message_handlert &message_handler)
+{
+  namespacet ns(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_bool(ID_is_synchronized))
+      continue;
+
+    if(symbol.type.get_bool(ID_is_static))
+    {
+      messaget message(message_handler);
+      message.warning() << "Java method '" << entry.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 = 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,15 @@ Module: Java Convert Thread blocks
 Author: Kurt Degiogrio, [email protected]
 
 \*******************************************************************/
-#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>
+#include <util/message.h>
 
 void convert_threadblock(symbol_tablet &symbol_table);
+void convert_synchronized_methods(
+  symbol_tablet &symbol_table,
+  message_handlert &message_handler);
 
 #endif

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -366,6 +366,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, [email protected]
 
 #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, get_message_handler());
+  }
 
   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)