Java concurrency, support for synchronization

appveyor.yml

@@ -18,6 +18,7 @@ install:
     Move-Item win_flex.exe bin\flex.exe -force
     Move-Item FlexLexer.h include\FlexLexer.h -force
     Remove-Item bin\data -Force -Recurse -ErrorAction SilentlyContinue
+    Remove-Item java-models-library-master -Force -Recurse -ErrorAction SilentlyContinue
     Move-Item data bin\data -force
     bison -V
     flex -V
@@ -90,7 +91,6 @@ test_script:
     rmdir /s /q jbmc\classpath1
     rmdir /s /q jbmc\jar-file3
     rmdir /s /q jbmc\tableswitch2
-    rmdir /s /q jbmc-concurrency\explicit_thread_blocks
     cd ../..
 
     make -C jbmc/regression test

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

@@ -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/test.desc

@@ -0,0 +1,6 @@
+CORE
+A.class
+--function 'A.me:()V' --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/anonymous-java.lang.thread/test2.desc

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

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

@@ -1,7 +1,6 @@
 CORE
 A.class
---function "A.me:()V" --lazy-methods --java-threading
-
+--function 'A.me:()V' --lazy-methods --java-threading
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL

jbmc/regression/jbmc-concurrency/explicit-thread-blocks/test2.desc

@@ -0,0 +1,5 @@
+CORE
+A.class
+--function 'A.me2:()V' --lazy-methods --java-threading
+^SIGNAL=0$
+^VERIFICATION FAILED

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

@@ -0,0 +1,112 @@
+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
+  // ---
+  // For some reason symex assigns 'g' to zero, even though
+  // 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 'me4')
+  //
+  // Seems related to: https://github.com/diffblue/cbmc/issues/1630/
+  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/get-current-thread/test.desc

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

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

@@ -0,0 +1,9 @@
+KNOWNBUG
+A.class
+--function 'A.me2:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../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/get-current-thread/test3.desc

@@ -0,0 +1,9 @@
+KNOWNBUG
+A.class
+--function 'A.me3:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../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/get-current-thread/test4.desc

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

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

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

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

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

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

@@ -0,0 +1,18 @@
+KNOWNBUG
+A.class
+--function 'A.me_bug:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL
+--
+--
+For some reason symex assigns 'g' to zero, even though
+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/java-lang-runnable/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/java-lang-runnable/test.desc

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

jbmc/regression/jbmc-concurrency/java-lang-runnable/test2.desc

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

jbmc/regression/jbmc-concurrency/java-lang-runnable/test3.desc

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

jbmc/regression/jbmc-concurrency/java-lang-runnable/test4.desc

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