JBMC: Modified the instrumentation of monitorexit/enter instructions

The monitorenter and monitorexit instructions are used by the JVM to
coordinate access to an object in the context of multiple threads.

We have previously added two methods to the object model that use a
counter to implement a reentrant lock. Calls to
'org.cprover.CProver.atomicBegin:()V"' and
'org.cprover.CProver.atomicEnd:()V' ensure that multiple threads do
not race in the access/modification of this counter.

In-order to support synchronization blocks, when the
monitorexit/moniitorenter bytecode instruction is executed JBMC must
call the aforementioned object model. To this end,  this commit makes
the following changes:

1. Transforms the monitorenter and monitorexit bytecode instructions
   into function-calls to the object model. Specifically,
   'java.lang.Object.monitorenter:(Ljava/lang/Object;)V' and
   'java.lang.Object.monitorexit:(Ljava/lang/Object;)V'.

2.  Transforms 'org.cprover.CProver.atomicBegin:()V"' and
    'org.cprover.CProver.atomicEnd:()V' into the appropriate
    codet instructions.

Added the appropriate target-handlers if monitorenter or monitorexit
are in the context of a try-catch block.

Author: dcattaruzza

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -1021,6 +1021,8 @@ codet java_bytecode_convert_methodt::convert_instructions(
     }
 
     if(i_it->statement=="athrow" ||
+       i_it->statement=="monitorenter" ||
+       i_it->statement=="monitorexit" ||
        i_it->statement=="putfield" ||
        i_it->statement=="getfield" ||
        i_it->statement=="checkcast" ||
@@ -1246,6 +1248,20 @@ codet java_bytecode_convert_methodt::convert_instructions(
                 "function expected to have exactly one parameter");
       c = replace_call_to_cprover_assume(i_it->source_location, c);
     }
+    // replace calls to CProver.atomicBegin
+    else if(statement == "invokestatic" &&
+            arg0.get(ID_identifier) ==
+            "java::org.cprover.CProver.atomicBegin:()V")
+    {
+      c = codet(ID_atomic_begin);
+    }
+    // replace calls to CProver.atomicEnd
+    else if(statement == "invokestatic" &&
+            arg0.get(ID_identifier) ==
+            "java::org.cprover.CProver.atomicEnd:()V")
+    {
+      c = codet(ID_atomic_end);
+    }
     else if(statement=="invokeinterface" ||
             statement=="invokespecial" ||
             statement=="invokevirtual" ||
@@ -1634,13 +1650,9 @@ codet java_bytecode_convert_methodt::convert_instructions(
       results[0]=
         binary_predicate_exprt(op[0], ID_java_instanceof, arg0);
     }
-    else if(statement=="monitorenter")
+    else if(statement == "monitorenter" || statement == "monitorexit")
     {
-      c = convert_monitorenter(i_it->source_location, op);
-    }
-    else if(statement=="monitorexit")
-    {
-      c = convert_monitorexit(i_it->source_location, op);
+      c = convert_monitorenterexit(statement, op, i_it->source_location);
     }
     else if(statement=="swap")
     {
@@ -1960,6 +1972,29 @@ codet java_bytecode_convert_methodt::convert_switch(
   return code_switch;
 }
 
+codet java_bytecode_convert_methodt::convert_monitorenterexit(
+  const irep_idt &statement,
+  const exprt::operandst &op,
+  const source_locationt &source_location)
+{
+  const irep_idt descriptor = (statement == "monitorenter") ?
+    "java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V" :
+    "java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V";
+
+  // becomes a function call
+  code_typet type(
+    {code_typet::parametert(java_reference_type(void_typet()))},
+    void_typet());
+  code_function_callt call;
+  call.function() = symbol_exprt(descriptor, type);
+  call.lhs().make_nil();
+  call.arguments().push_back(op[0]);
+  call.add_source_location() = source_location;
+  if(needed_lazy_methods && symbol_table.has_symbol(descriptor))
+    needed_lazy_methods->add_needed_method(descriptor);
+  return call;
+}
+
 void java_bytecode_convert_methodt::convert_dup2(
   exprt::operandst &op,
   exprt::operandst &results)
@@ -2399,38 +2434,6 @@ codet &java_bytecode_convert_methodt::do_exception_handling(
   return c;
 }
 
-codet java_bytecode_convert_methodt::convert_monitorexit(
-  const source_locationt &location,
-  const exprt::operandst &op) const
-{
-  code_typet type;
-  type.return_type() = void_typet();
-  type.parameters().resize(1);
-  type.parameters()[0].type() = java_reference_type(void_typet());
-  code_function_callt call;
-  call.function() = symbol_exprt("java::monitorexit", type);
-  call.lhs().make_nil();
-  call.arguments().push_back(op[0]);
-  call.add_source_location() = location;
-  return call;
-}
-
-codet java_bytecode_convert_methodt::convert_monitorenter(
-  const source_locationt &location,
-  const exprt::operandst &op) const
-{
-  code_typet type;
-  type.return_type() = void_typet();
-  type.parameters().resize(1);
-  type.parameters()[0].type() = java_reference_type(void_typet());
-  code_function_callt call;
-  call.function() = symbol_exprt("java::monitorenter", type);
-  call.lhs().make_nil();
-  call.arguments().push_back(op[0]);
-  call.add_source_location() = location;
-  return call;
-}
-
 void java_bytecode_convert_methodt::convert_multianewarray(
   const source_locationt &location,
   const exprt &arg0,

jbmc/src/java_bytecode/java_bytecode_convert_method_class.h

@@ -420,14 +420,6 @@ class java_bytecode_convert_methodt:public messaget
     codet &c,
     exprt::operandst &results);
 
-  codet convert_monitorenter(
-    const source_locationt &location,
-    const exprt::operandst &op) const;
-
-  codet convert_monitorexit(
-    const source_locationt &location,
-    const exprt::operandst &op) const;
-
   codet &do_exception_handling(
     const methodt &method,
     const std::set<unsigned int> &working_set,
@@ -446,6 +438,11 @@ class java_bytecode_convert_methodt:public messaget
     codet &c,
     exprt::operandst &results) const;
 
+  codet convert_monitorenterexit(
+    const irep_idt &statement,
+    const exprt::operandst &op,
+    const source_locationt &source_location);
+
   codet &replace_call_to_cprover_assume(source_locationt location, codet &c);
 
   void convert_invoke(

jbmc/src/java_bytecode/simple_method_stubbing.cpp

@@ -233,10 +233,17 @@ void java_simple_method_stubst::create_method_stub(symbolt &symbol)
 void java_simple_method_stubst::check_method_stub(const irep_idt &symname)
 {
   const symbolt &sym = *symbol_table.lookup(symname);
-  if(
-    !sym.is_type && sym.value.id() == ID_nil && sym.type.id() == ID_code &&
-    // Don't stub internal locking primitives:
-    sym.name != "java::monitorenter" && sym.name != "java::monitorexit")
+  if(!sym.is_type && sym.value.id() == ID_nil &&
+    sym.type.id() == ID_code &&
+    // do not stub internal locking calls as 'create_method_stub' does not
+    // automatically create the appropriate symbols for the formal parameters.
+    // This means that symex will (rightfully) crash  when it encounters the
+    // function call as it will not be able to find symbols for the fromal
+    // parameters.
+    sym.name !=
+      "java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V" &&
+    sym.name !=
+      "java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V")
   {
     create_method_stub(*symbol_table.get_writeable(symname));
   }

src/goto-programs/builtin_functions.cpp

@@ -855,12 +855,14 @@ void goto_convertt::do_function_call_symbol(
   }
   else if(identifier==CPROVER_PREFIX "atomic_begin" ||
           identifier=="__CPROVER::atomic_begin" ||
+          identifier=="java::org.cprover.CProver.atomicBegin:()V" ||
           identifier=="__VERIFIER_atomic_begin")
   {
     do_atomic_begin(lhs, function, arguments, dest);
   }
   else if(identifier==CPROVER_PREFIX "atomic_end" ||
           identifier=="__CPROVER::atomic_end" ||
+          identifier=="java::org.cprover.CProver.atomicEnd:()V" ||
           identifier=="__VERIFIER_atomic_end")
   {
     do_atomic_end(lhs, function, arguments, dest);