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

@@ -1014,6 +1014,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" ||
@@ -1304,6 +1306,20 @@ codet java_bytecode_convert_methodt::convert_instructions(
       loc.set_function(method_id);
       c.add_source_location()=loc;
     }
+    // replace calls to CProver.atomicBegin
+    else if(statement == "invokestatic" &&
+            id2string(arg0.get(ID_identifier)) ==
+            "java::org.cprover.CProver.atomicBegin:()V")
+    {
+      c = codet(ID_atomic_begin);
+    }
+    // replace calls to CProver.atomicEnd
+    else if(statement == "invokestatic" &&
+            id2string(arg0.get(ID_identifier)) ==
+            "java::org.cprover.CProver.atomicEnd:()V")
+    {
+      c = codet(ID_atomic_end);
+    }
     else if(statement=="invokeinterface" ||
             statement=="invokespecial" ||
             statement=="invokevirtual" ||
@@ -2340,33 +2356,30 @@ codet java_bytecode_convert_methodt::convert_instructions(
       results[0]=
         binary_predicate_exprt(op[0], ID_java_instanceof, arg0);
     }
-    else if(statement=="monitorenter")
-    {
-      // becomes a function call
-      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()=i_it->source_location;
-      c=call;
-    }
-    else if(statement=="monitorexit")
+    else if(statement == "monitorenter" || statement == "monitorexit")
     {
+      std::string descriptor;
+      if(statement == "monitorenter")
+        descriptor =
+          "java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V";
+      else
+        descriptor =
+          "java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V";
+
       // becomes a function call
       code_typet type;
-      type.return_type()=void_typet();
+      type.return_type() = void_typet();
       type.parameters().resize(1);
-      type.parameters()[0].type()=java_reference_type(void_typet());
+      type.parameters()[0].type() = java_reference_type(void_typet());
+
       code_function_callt call;
-      call.function()=symbol_exprt("java::monitorexit", type);
+      call.function() = symbol_exprt(descriptor, type);
       call.lhs().make_nil();
       call.arguments().push_back(op[0]);
-      call.add_source_location()=i_it->source_location;
-      c=call;
+      call.add_source_location() = i_it->source_location;
+      if(needed_lazy_methods && symbol_table.has_symbol(descriptor))
+        needed_lazy_methods->add_needed_method(descriptor);
+      c = call;
     }
     else if(statement=="swap")
     {

jbmc/src/java_bytecode/simple_method_stubbing.cpp

@@ -222,10 +222,13 @@ 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
+    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

@@ -883,12 +883,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);