Merge pull request diffblue#2179 from cesaro/java-concurrency-support3

Java concurrency support

Author: cesaro

regression/cbmc-java-concurrency/CMakeLists.txt

@@ -0,0 +1,3 @@
+add_test_pl_tests(
+    "$<TARGET_FILE:jbmc>"
+)

regression/cbmc-java-concurrency/Makefile

@@ -0,0 +1,32 @@
+default: tests.log
+
+test:
+	@../test.pl -p -c ../../../src/jbmc/jbmc
+
+tests.log: ../test.pl
+	@../test.pl -p -c ../../../src/jbmc/jbmc
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.java" "$$dir/*.out"; \
+		fi; \
+	done;
+
+clean:
+	find -name '*.out' -execdir $(RM) '{}' \;
+	find -name '*.gb' -execdir $(RM) '{}' \;
+	$(RM) tests.log
+
+%.class: %.java ../../src/org.cprover.jar
+	javac -g -cp ../../src/org.cprover.jar:. $<
+
+nondet_java_files := $(shell find . -name "Nondet*.java")
+nondet_class_files := $(patsubst %.java, %.class, $(nondet_java_files))
+
+.PHONY: nondet-class-files
+nondet-class-files: $(nondet_class_files)
+
+.PHONY: clean-nondet-class-files
+clean-nondet-class-files:
+	-rm $(nondet_class_files)

regression/cbmc-java-concurrency/explicit_thread_blocks/A.class

@@ -0,0 +1,61 @@
+import java.lang.Thread;
+import org.cprover.CProver;
+
+public class A
+{
+  static int x = 0;
+
+  // verification success
+  public void me()
+  {
+    x = 5;
+    CProver.startThread(333);
+    x = 10;
+    CProver.endThread(333);
+    assert(x == 5 || x == 10);
+  }
+
+  // verification failed
+  public void me2()
+  {
+    x = 5;
+    CProver.startThread(333);
+    x = 10;
+    CProver.endThread(333);
+    assert(x == 10);
+  }
+
+  // Known-bug, thread id mismatch, this should be detected by the conversation
+  // process. It is currently not and thus will result in an assertion violation
+  // during symbolic execution.
+  public void me3()
+  {
+    x = 5;
+    CProver.startThread(22333);
+    x = 10;
+    CProver.endThread(333);
+    assert(x == 10);
+  }
+
+  // Known-bug, see: https://github.com/diffblue/cbmc/issues/1630
+  public void me4()
+  {
+    int x2 = 10;
+    CProver.startThread(22333);
+    x = x2;
+    assert(x == 10);
+    CProver.endThread(333);
+  }
+
+  // Known-bug, symex cannot handle nested thread-blocks
+  public void me5()
+  {
+    CProver.startThread(333);
+    x = 5;
+    CProver.startThread(222);
+    x = 8;
+    CProver.endThread(222);
+    CProver.endThread(333);
+    assert(x == 5 || x == 0 || x == 8);
+  }
+}

regression/cbmc-java-concurrency/explicit_thread_blocks/A.java

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

regression/cbmc-java-concurrency/explicit_thread_blocks/test.desc

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

regression/cbmc-java-concurrency/explicit_thread_blocks/test2.desc

@@ -7,6 +7,7 @@ SRC = bytecode_info.cpp \
       jar_file.cpp \
       java_bytecode_convert_class.cpp \
       java_bytecode_convert_method.cpp \
+      java_bytecode_convert_threadblock.cpp \
       java_bytecode_instrument.cpp \
       java_bytecode_internal_additions.cpp \
       java_bytecode_language.cpp \

src/java_bytecode/Makefile

@@ -2834,6 +2834,11 @@ void java_bytecode_convert_method(
     "nondetWithNull",
     "nondetWithoutNull",
     "notModelled",
+    "atomicBegin",
+    "atomicEnd",
+    "startThread",
+    "endThread",
+    "getCurrentThreadID"
   };
 
   if(std::regex_match(