From ee6fab594c6d5eb04351af1a73b1d16718b65554 Mon Sep 17 00:00:00 2001
From: Daniel Raffler <daniel-raffler@gmx.de>
Date: Thu, 28 Dec 2023 22:16:23 +0100
Subject: [PATCH] Quickfix for https://github.com/sosy-lab/java-smt/issues/347

---
 src/api/java/jni/api_utilities.h | 8 ++++++++
 src/api/java/jni/solver.cpp      | 9 +++++++++
 2 files changed, 17 insertions(+)

diff --git a/src/api/java/jni/api_utilities.h b/src/api/java/jni/api_utilities.h
index e6eaffd5920..f87dd921e1b 100644
--- a/src/api/java/jni/api_utilities.h
+++ b/src/api/java/jni/api_utilities.h
@@ -19,6 +19,7 @@
 #include <cvc5/cvc5_parser.h>
 #include <jni.h>
 
+#include <mutex>
 #include <string>
 #include <vector>
 
@@ -149,8 +150,15 @@ jobject getBooleanObject(JNIEnv* env, bool value);
  * a map from solver pointers to global references that need to be freed when
  * the java Solver.deletePointer method is called
  */
+
 inline std::map<jlong, std::vector<jobject> > globalReferences;
 
+/**
+ * a lock to protect globalReferences
+ */
+
+inline std::mutex globalLock;
+
 /**
  * @param env jni environment
  * @param solverRef a global reference to java Solver object
diff --git a/src/api/java/jni/solver.cpp b/src/api/java/jni/solver.cpp
index daf2da5379f..eaaed870f20 100644
--- a/src/api/java/jni/solver.cpp
+++ b/src/api/java/jni/solver.cpp
@@ -41,6 +41,7 @@ JNIEXPORT void JNICALL Java_io_github_cvc5_Solver_deletePointer(JNIEnv* env,
                                                                 jobject,
                                                                 jlong pointer)
 {
+  std::lock_guard<std::mutex> guard(globalLock);
   const std::vector<jobject>& refs = globalReferences[pointer];
   for (jobject ref : refs)
   {
@@ -2437,6 +2438,7 @@ Java_io_github_cvc5_Solver_declareOracleFun(JNIEnv* env,
                                             jobject oracle)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  std::lock_guard<std::mutex> guard(globalLock);
   jobject oracleReference = env->NewGlobalRef(oracle);
   globalReferences[pointer].push_back(oracleReference);
   Solver* solver = reinterpret_cast<Solver*>(pointer);
@@ -2446,6 +2448,13 @@ Java_io_github_cvc5_Solver_declareOracleFun(JNIEnv* env,
   std::vector<Sort> sorts = getObjectsFromPointers<Sort>(env, sortPointers);
   std::function<Term(std::vector<Term>)> fn =
       [env, oracleReference](std::vector<Term> input) {
+        // FIXME:
+        // This is likely still broken if multiple threads are
+        // used as the captured JEnv ("env") is only valid on the
+        // current thread. However, the callback might come from
+        // any thread that encouters a term for the oracle.
+        //
+        // See https://github.com/sosy-lab/java-smt/pull/345
         Term term = applyOracle(env, oracleReference, input);
         return term;
       };