Merge pull request diffblue#2486 from Degiorgio/jbmc-synchronoization-asymmetry-fix

JBMC: Fixed asymmetry between synchronized blocks and methods.

Author: Thomas Kiley

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;
   }