JBMC: Regression tests for multi-threaded java programs

Author: Degiorgio

jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/A$1.class

@@ -0,0 +1,39 @@
+import java.lang.Thread;
+import org.cprover.CProver;
+
+public class A
+{
+  int x = 0;
+
+  // expected verfication success
+  public void me()
+  {
+    Thread t = new Thread()
+    {
+      public void run()
+      {
+        x = 44;
+        int local_x = x;
+        assert(local_x == 44 || x == 10);
+      }
+    };
+    t.start();
+    x = 10;
+  }
+
+  // expected verfication failure
+  public void me2()
+  {
+    Thread t = new Thread()
+    {
+      public void run()
+      {
+        x = 44;
+        int local_x = x;
+        assert(local_x == 44);
+      }
+    };
+    t.start();
+    x = 10;
+  }
+}

jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/A$2.class

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

jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/A.class

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

jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/A.java

@@ -0,0 +1,101 @@
+import java.lang.Thread;
+import org.cprover.CProver;
+
+public class A
+{
+  public static int g;
+
+  // expected verification success
+  public void me()
+  {
+    int g = CProver.getCurrentThreadID();
+    assert(g == 0);
+  }
+
+  // expected verification success
+  // --
+  // KNOWNBUG
+  public void me_bug()
+  {
+    CProver.startThread(333);
+    int g = 1;
+    assert(g == 1);
+    CProver.endThread(333);
+  }
+
+  // expected verification success
+  // --
+  // KNOWNBUG: see me_bug()
+  public void me2()
+  {
+    CProver.startThread(333);
+    g = CProver.getCurrentThreadID();
+    assert(g == 1);
+    CProver.endThread(333);
+  }
+
+  // expected verification success
+  // --
+  // KNOWNBUG: see me_bug()
+  public void me3()
+  {
+    CProver.startThread(333);
+    int i = CProver.getCurrentThreadID();
+    assert(g == 1);
+    CProver.endThread(333);
+  }
+
+  // expected verification success.
+  public void me4()
+  {
+    CProver.startThread(333);
+    check();
+    CProver.endThread(333);
+  }
+
+  // expected verification success.
+  public void me5()
+  {
+    me();
+    B b = new B();
+    Thread tmp = new Thread(b);
+    tmp.start();
+  }
+
+  // expected verification success.
+  public void me6()
+  {
+    me();
+    C c = new C();
+    c.start();
+  }
+
+  public void check()
+  {
+    g = CProver.getCurrentThreadID();
+    assert(g == 1);
+  }
+}
+
+class B implements Runnable
+{
+  public static int g;
+  @Override
+  public void run()
+  {
+    g = CProver.getCurrentThreadID();
+    assert(g == 1);
+  }
+}
+
+
+class C extends Thread
+{
+  public static int g;
+  @Override
+  public void run()
+  {
+    g = CProver.getCurrentThreadID();
+    assert(g == 1);
+  }
+}

jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/test.desc

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

jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/test2.desc

@@ -0,0 +1,10 @@
+KNOWNBUG
+A.class
+--function "A.me2:()V" --java-threading --cp ../../../src/java_bytecode/library/core-models.jar:.
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL
+--
+--
+Same bug as the one highlighted in 'test_bug.desc'

jbmc/regression/jbmc-concurrency/explicit_thread_blocks/A.class renamed to jbmc/regression/jbmc-concurrency/explicit-thread-blocks/A.class

@@ -0,0 +1,10 @@
+KNOWNBUG
+A.class
+--function "A.me3:()V" --java-threading --cp ../../../src/java_bytecode/library/core-models.jar:.
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL
+--
+--
+Same bug as the one highlighted in 'test_bug.desc'

jbmc/regression/jbmc-concurrency/explicit_thread_blocks/A.java renamed to jbmc/regression/jbmc-concurrency/explicit-thread-blocks/A.java

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

jbmc/regression/jbmc-concurrency/explicit_thread_blocks/test.desc renamed to jbmc/regression/jbmc-concurrency/explicit-thread-blocks/test.desc

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

jbmc/regression/jbmc-concurrency/explicit_thread_blocks/test2.desc renamed to jbmc/regression/jbmc-concurrency/explicit-thread-blocks/test2.desc

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

jbmc/regression/jbmc-concurrency/get-current-thread/A.class

@@ -0,0 +1,19 @@
+KNOWNBUG
+A.class
+--function "A.me_bug:()V" --java-threading --cp ../../../src/java_bytecode/library/core-models.jar:.
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL
+--
+--
+For some reason symex assigns 'g' to zero, even though it
+the only viable assignment should be one.
+This issue seems to only occur when a variable is
+assigned inside the local scope of a thread-block.
+
+If instead, we call a function from inside the thread-block and
+then assign  'g' to 1 then as expected the only viable
+assignment to 'g' is 1 (see test4.desc)
+
+Seems related to: https://github.com/diffblue/cbmc/issues/1630/

jbmc/regression/jbmc-concurrency/get-current-thread/A.java

@@ -0,0 +1,87 @@
+// JBMC, concurrency tests that make use of
+// the java.lang.Runnable model
+
+import java.lang.Thread;
+import org.cprover.CProver;
+
+public class A
+{
+  // calling start from outside.
+  // expected verfication success.
+  public void me3()
+  {
+    C c = new C();
+    Thread tmp = new Thread(c);
+    tmp.start();
+    c.setX();
+  }
+
+  // calling start from outside, no race-condition on B.x
+  // expected verfication success.
+  public void me4()
+  {
+    B b = new B();
+    Thread tmp = new Thread(b);
+    tmp.start();
+  }
+
+  // expected verfication failed
+  public void me2()
+  {
+    B b = new B();
+    b.me();
+  }
+
+  // expected verfication success.
+  public void me()
+  {
+    C c = new C();
+    c.me();
+  }
+}
+
+class B implements Runnable
+{
+  int x = 0;
+
+  @Override
+  public void run()
+  {
+    x = 44;
+    int local_x = x;
+    assert(local_x == 44);
+  }
+
+  public void me()
+  {
+    Thread tmp = new Thread(this);
+    tmp.start();
+    x = 10;
+  }
+}
+
+
+class C implements Runnable
+{
+  int x = 0;
+
+  @Override
+  public void run()
+  {
+    x = 44;
+    int local_x = x;
+    assert(local_x == 44 || x == 10);
+  }
+
+  public void me()
+  {
+    Thread tmp = new Thread(this);
+    tmp.start();
+    setX();
+  }
+
+  public void setX()
+  {
+    x = 10;
+  }
+}

jbmc/regression/jbmc-concurrency/get-current-thread/B.class

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

jbmc/regression/jbmc-concurrency/get-current-thread/C.class

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

jbmc/regression/jbmc-concurrency/get-current-thread/test.desc

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

jbmc/regression/jbmc-concurrency/get-current-thread/test2.desc

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