JBMC: Regression tests for synchronized methods

Author: Degiorgio

jbmc/regression/jbmc-concurrency/synchronized-method-illegal-state/Sync.class

@@ -0,0 +1,45 @@
+import java.lang.RuntimeException;
+import org.cprover.CProver;
+
+public class Sync
+{
+  public int field;
+
+  public static void main(String[] args)
+  {
+    final Sync o = new Sync();
+    o.field = 0;
+    // test regular synchronized method (monitorexit on return)
+    o.f();
+    // test synchronized method with throw (monitorexit on catch)
+    try
+    {
+      o.g();
+    }
+    catch (RuntimeException e)
+    {
+      o.field++;
+    }
+    // Make sure both functions were executed and the second threw
+    // The object should remain unlocked
+    if ((o.field !=3) || (CProver.getMonitorCount(o) !=0))
+      assert(false);
+  }
+
+  public synchronized void f()
+  {
+    // Check that we acquired  the lock
+    if (CProver.getMonitorCount(this) !=1)
+      assert(false);
+    field++;
+  }
+
+  public synchronized void g()
+  {
+    field++;
+    // Check that we acquired  the lock
+    if (CProver.getMonitorCount(this) !=1)
+      assert(false);
+    throw new RuntimeException();
+  }
+}

jbmc/regression/jbmc-concurrency/synchronized-method-illegal-state/Sync.java

@@ -0,0 +1,13 @@
+KNOWNBUG
+Sync.class
+--cp ../../../src/java_bytecode/library/core-models.jar:. --lazy-methods --java-threading
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Checks all possible paths to ensure a synchronized method does not end in an illegal monitor state.
+
+This is currently not working as explicit throws have been removed from the underlying model due to performance considerations.

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

@@ -0,0 +1,49 @@
+public class A
+{
+  static int g;
+
+  public synchronized void me1()
+  {
+    g = 0;
+  }
+
+  // expected verification success
+  // --
+  // base-case, no synchronization
+  public void me2()
+  {
+    B t = new B();
+    t.shared = 5;
+    t.start();
+    assert(t.shared == 5 || t.shared == 6);
+  }
+
+  // expected verification success
+  // --
+  // locking mechanism
+  public void me3()
+  {
+    B t = new B();
+    synchronized(t)
+    {
+      t.shared = 5;
+      t.start();
+      assert(t.shared == 5);
+    }
+  }
+}
+
+class B extends Thread
+{
+  public int shared = 0;
+
+  @Override
+  public void run()
+  {
+    set();
+  }
+  public synchronized void set()
+  {
+    shared++;
+  }
+}

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

@@ -0,0 +1,7 @@
+CORE
+A.class
+--function "A.me1:()V" --java-threading --cp ../../../src/java_bytecode/library/core-models.jar:. --show-goto-functions
+ATOMIC_BEGIN
+ATOMIC_END
+--
+--

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

@@ -0,0 +1,8 @@
+CORE
+A.class
+--function "A.me1:()V" --java-threading --lazy-methods --cp ../../../src/java_bytecode/library/core-models.jar:. --show-goto-functions
+ATOMIC_BEGIN
+ATOMIC_END
+--
+--
+Making sure that monitorEnter and monitorExit are not removed by lazy-methods

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

@@ -0,0 +1,8 @@
+CORE
+A.class
+--function "A.me1:()V" --java-threading --lazy-methods --cp ../../../src/java_bytecode/library/core-models.jar:.
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL
+--
+--

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

@@ -0,0 +1,8 @@
+CORE
+A.class
+--function "A.me3:()V" --java-threading --lazy-methods --cp ../../../src/java_bytecode/library/core-models.jar:.
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--

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

@@ -0,0 +1,8 @@
+CORE
+A.class
+--function "A.me2:()V" --java-threading --lazy-methods --cp ../../../src/java_bytecode/library/core-models.jar:.
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--