JBMC: Fixed asymmetry between synchronized blocks and methods.

Previously, the conversation of synchronized methods only took place if
the 'java-threading' flag is specified, while in the case of
synchronized blocks the conversation is undertaken with and without the
aforementioned flag. This commit fixes this asymmetry by replacing
the instructions 'monitorenter' and 'moinitorexit' with 'code_skipt' if
the 'java-threading' option is not specified (instead of instrumenting
calls to 'java::java.lang.Object.monitorexit/enter').

The 'monitorenter' and monitiorexit instructions are also replaced with
a 'code_skipt' if the Java-core-models library is not loaded. This
prevents JBMC from outputting missing function-body warnings.

Commit also modifies relevant regression tests.

Author: Degiorgio

jbmc/regression/jbmc-concurrency/synchronized-blocks-illegal-state/test.desc

@@ -1,6 +1,6 @@
 KNOWNBUG
 Sync.class
---lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$

jbmc/regression/jbmc-concurrency/synchronized-blocks-null-throw/test.desc

@@ -1,6 +1,6 @@
 KNOWNBUG
 Sync.class
---cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring

jbmc/regression/jbmc-concurrency/synchronized-blocks-throw/test.desc

@@ -1,6 +1,6 @@
 KNOWNBUG
 Sync.class
---cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --lazy-methods
+--cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --lazy-methods --java-threading
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring

jbmc/regression/jbmc-concurrency/synchronized-blocks/A.class

@@ -14,6 +14,25 @@ public void me0()
     }
   }
 
+  // expected verification success
+  public static void aStatic() throws java.io.IOException
+  {
+    Object _lock = new Object();
+    try
+    {
+      synchronized (_lock)
+      {
+        if(true)
+          throw new java.io.IOException();
+      }
+    }
+    catch (java.io.IOException e)
+    {
+      return;
+    }
+    assert false; // unreachable
+  }
+
   // expected verification success
   // --
   // base-case, no synchronization

jbmc/regression/jbmc-concurrency/synchronized-blocks/A.java

@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me0:()V' --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --show-goto-functions
+--function 'A.me0:()V' --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --show-goto-functions --java-threading
 ATOMIC_BEGIN
 ATOMIC_END
 --

jbmc/regression/jbmc-concurrency/synchronized-blocks/B.class

@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+--function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

jbmc/regression/jbmc-concurrency/synchronized-blocks/test1.desc

@@ -1,6 +1,6 @@
 CORE
 A.class
---function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --lazy-methods
+--function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --lazy-methods --java-threading
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

jbmc/regression/jbmc-concurrency/synchronized-blocks/test2.desc

@@ -0,0 +1,10 @@
+CORE
+A.class
+--function 'A.aStatic' --lazy-methods
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Tests that throwing an exception from a synchronization blocks does not cause reachability issues when the java-threading flag is not specified.
+

jbmc/regression/jbmc-concurrency/synchronized-blocks/test3.desc

@@ -1026,8 +1026,6 @@ 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" ||
@@ -1042,7 +1040,9 @@ codet java_bytecode_convert_methodt::convert_instructions(
        i_it->statement=="invokestatic" ||
        i_it->statement=="invokevirtual" ||
        i_it->statement=="invokespecial" ||
-       i_it->statement=="invokeinterface")
+       i_it->statement=="invokeinterface" ||
+       (threading_support && (i_it->statement=="monitorenter" ||
+       i_it->statement=="monitorexit")))
     {
       const std::vector<unsigned int> handler =
         try_catch_handler(i_it->address, method.exception_table);
@@ -1986,6 +1986,9 @@ codet java_bytecode_convert_methodt::convert_monitorenterexit(
     "java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V" :
     "java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V";
 
+  if(!threading_support || !symbol_table.has_symbol(descriptor))
+    return code_skipt();
+
   // becomes a function call
   code_typet type(
     {code_typet::parametert(java_reference_type(void_typet()))},
@@ -3099,7 +3102,9 @@ void java_bytecode_convert_method(
   bool throw_assertion_error,
   optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
   java_string_library_preprocesst &string_preprocess,
-  const class_hierarchyt &class_hierarchy)
+  const class_hierarchyt &class_hierarchy,
+  bool threading_support)
+
 {
   if(std::regex_match(
        id2string(class_symbol.name),
@@ -3118,7 +3123,8 @@ void java_bytecode_convert_method(
     throw_assertion_error,
     needed_lazy_methods,
     string_preprocess,
-    class_hierarchy);
+    class_hierarchy,
+    threading_support);
 
   java_bytecode_convert_method(class_symbol, method);
 }

jbmc/regression/jbmc-concurrency/synchronized-blocks/test4.desc

@@ -36,7 +36,8 @@ void java_bytecode_convert_method(
   bool throw_assertion_error,
   optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
   java_string_library_preprocesst &string_preprocess,
-  const class_hierarchyt &class_hierarchy);
+  const class_hierarchyt &class_hierarchy,
+  bool threading_support);
 
 void java_bytecode_convert_method_lazy(
   const symbolt &class_symbol,

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -39,11 +39,13 @@ class java_bytecode_convert_methodt:public messaget
     bool throw_assertion_error,
     optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
     java_string_library_preprocesst &_string_preprocess,
-    const class_hierarchyt &class_hierarchy)
+    const class_hierarchyt &class_hierarchy,
+    bool threading_support)
     : messaget(_message_handler),
       symbol_table(symbol_table),
       max_array_length(_max_array_length),
       throw_assertion_error(throw_assertion_error),
+      threading_support(threading_support),
       needed_lazy_methods(std::move(needed_lazy_methods)),
       string_preprocess(_string_preprocess),
       slots_for_parameters(0),
@@ -67,6 +69,7 @@ class java_bytecode_convert_methodt:public messaget
   symbol_table_baset &symbol_table;
   const size_t max_array_length;
   const bool throw_assertion_error;
+  const bool threading_support;
   optionalt<ci_lazy_methods_neededt> needed_lazy_methods;
 
   /// Fully qualified name of the method under translation.

jbmc/src/java_bytecode/java_bytecode_convert_method.h

@@ -1040,7 +1040,8 @@ bool java_bytecode_languaget::convert_single_method(
       throw_assertion_error,
       std::move(needed_lazy_methods),
       string_preprocess,
-      class_hierarchy);
+      class_hierarchy,
+      threading_support);
     return false;
   }