Adding concurrency related methods to CProver.java

Specifically: startThread, endThread, atomicBegin, atomicEnd and getCurrentThreadID.
NathanJPhillips · May 10, 2018 · 46849e9 · 46849e9
1 parent 784b6dd
commit 46849e9
Show file tree

Hide file tree

Showing 2 changed files with 52 additions and 0 deletions.
diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -2834,6 +2834,11 @@ void java_bytecode_convert_method(
     "nondetWithNull",
     "nondetWithoutNull",
     "notModelled",
+    "atomicBegin",
+    "atomicEnd",
+    "startThread",
+    "endThread",
+    "getCurrentThreadID"
   };
 
   if(std::regex_match(

diff --git a/src/java_bytecode/library/src/org/cprover/CProver.java b/src/java_bytecode/library/src/org/cprover/CProver.java
@@ -4,6 +4,7 @@ public final class CProver
 {
   public static boolean enableAssume=true;
   public static boolean enableNondet=true;
+  public static boolean enableConcurrency=true;
 
   public static boolean nondetBoolean()
   {
@@ -115,6 +116,52 @@ public static <T> T nondetWithoutNull()
     return null;
   }
 
+  public static void startThread(int id)
+  {
+    if(enableConcurrency)
+    {
+      throw new RuntimeException(
+          "Cannot execute program with CProver.startThread()");
+    }
+  }
+
+  public static void endThread(int id)
+  {
+    if(enableConcurrency)
+    {
+      throw new RuntimeException(
+          "Cannot execute program with CProver.endThread()");
+    }
+  }
+
+  public static void atomicBegin()
+  {
+    if(enableConcurrency)
+    {
+      throw new RuntimeException(
+          "Cannot execute program with CProver.atomicBegin()");
+    }
+  }
+
+  public static void atomicEnd()
+  {
+    if(enableConcurrency)
+    {
+      throw new RuntimeException(
+          "Cannot execute program with CProver.atomicEnd()");
+    }
+  }
+
+  public static int getCurrentThreadID()
+  {
+    if(enableConcurrency)
+    {
+      throw new RuntimeException(
+          "Cannot execute program with CProver.getCurrentThreadID()");
+    }
+    return 0;
+  }
+
   public static void assume(boolean condition)
   {
     if(enableAssume && !condition)