JDD: Add a flag that can be set/checked in native code to indicate that a CuDD error has occurred.

For DD functions that return a DdNode*, errors can be reported by returning NULL.
Functions that have no return value (printing, etc) or a data value (double, etc)
should set the flag, which can be converted into an CuddOutOfMemoryException on
the PRISM side using JDD.checkForCuddError()


git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10474 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/include/JDD.h

@@ -143,6 +143,14 @@ JNIEXPORT void JNICALL Java_jdd_JDD_DD_1Deref
 JNIEXPORT void JNICALL Java_jdd_JDD_DD_1PrintCacheInfo
   (JNIEnv *, jclass);
 
+/*
+ * Class:     jdd_JDD
+ * Method:    DD_GetErrorFlag
+ * Signature: ()Z
+ */
+JNIEXPORT jboolean JNICALL Java_jdd_JDD_DD_1GetErrorFlag
+  (JNIEnv *, jclass);
+
 /*
  * Class:     jdd_JDD
  * Method:    DD_Create

prism/include/dd_cudd.h

@@ -36,5 +36,7 @@ void DD_SetCUDDEpsilon(DdManager *ddman, double epsilon);
 void DD_PrintCacheInfo(DdManager *ddman);
 void DD_CloseDownCUDD(DdManager *ddman);
 void DD_CloseDownCUDD(DdManager *ddman, bool check);
+bool DD_GetErrorFlag(DdManager *ddman);
+void DD_SetErrorFlag();
 
 //------------------------------------------------------------------------------

prism/src/dd/dd_cudd.cc

@@ -31,6 +31,11 @@
 
 extern FILE *dd_out;
 
+// A flag indicating that a CuDD error has occurred
+// that could not be signaled by returning a NULL DdNode*
+// from a function
+bool dd_cudd_error_flag = false;
+
 static int Cudd_CheckZeroRefVerbose(DdManager *ddman);
 
 //-----------------------------------------------------------------------------------
@@ -226,3 +231,23 @@ int Cudd_CheckZeroRefVerbose(DdManager *manager)
 
 //-----------------------------------------------------------------------------------
 
+// Get the value of the DD error flag
+bool DD_GetErrorFlag(DdManager *ddman)
+{
+	return dd_cudd_error_flag || (ddman->errorCode != CUDD_NO_ERROR);
+}
+
+//-----------------------------------------------------------------------------------
+
+// Set the DD error flag. Should be set if a CuDD error has been
+// detected that could not be signaled by returning a NULL DdNode*
+// from the function
+void DD_SetErrorFlag()
+{
+	dd_cudd_error_flag = true;
+}
+
+
+//-----------------------------------------------------------------------------------
+
+

prism/src/jdd/JDD.cc

@@ -872,3 +872,10 @@ JNIEXPORT jint JNICALL Java_jdd_DebugJDD_DebugJDD_1GetRefCount(JNIEnv *env, jcla
 {
 	return (jlong_to_DdNode(dd))->ref;
 }
+
+//------------------------------------------------------------------------------
+
+JNIEXPORT jboolean JNICALL Java_jdd_JDD_DD_1GetErrorFlag(JNIEnv *env, jclass cls)
+{
+	return DD_GetErrorFlag(ddman);
+}

prism/src/jdd/JDD.java

@@ -48,6 +48,7 @@ public class JDD
 	private static native void DD_Ref(long dd);
 	private static native void DD_Deref(long dd);
 	private static native void DD_PrintCacheInfo();
+	private static native boolean DD_GetErrorFlag();
 	// dd_basics
 	private static native long DD_Create();
 	private static native long DD_Constant(double value);
@@ -1380,6 +1381,17 @@ public class JDD
 		return new JDDNode(ptr);
 	}
 
+	/**
+	 * Check whether the DD error flag is set, indicating an
+	 * out-of-meory situation in CuDD or another internal error.
+	 * If the flag is set, throws a {@code CuddOutOfMemoryException}.
+	 */
+	public static void checkForCuddError()
+	{
+		if (DD_GetErrorFlag())
+			throw new CuddOutOfMemoryException();
+	}
+
 }
 
 //------------------------------------------------------------------------------