DebugJDD: Move JNI methods to JDD class

The order of the content of the prism/include/DebugJDD.h header (auto-generated
by javah) sometimes changes nondeterministically. This seems to be due to the
combination of JNI methods and internal classes in DebugJDD.

We move the two DebugJDD JNI methods to JDD instead and remove the
prism/include/DebugJDD.h header, as well as the generation in the Makefile.


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

prism/include/DebugJDD.h

@@ -1,51 +0,0 @@
-/* DO NOT EDIT THIS FILE - it is machine generated */
-#include <jni.h>
-/* Header for class jdd_DebugJDD */
-
-#ifndef _Included_jdd_DebugJDD
-#define _Included_jdd_DebugJDD
-#ifdef __cplusplus
-extern "C" {
-#endif
-/*
- * Class:     jdd_DebugJDD
- * Method:    DebugJDD_GetRefCount
- * Signature: (J)I
- */
-JNIEXPORT jint JNICALL Java_jdd_DebugJDD_DebugJDD_1GetRefCount
-  (JNIEnv *, jclass, jlong);
-
-/*
- * Class:     jdd_DebugJDD
- * Method:    DebugJDD_GetExternalRefCounts
- * Signature: ()[J
- */
-JNIEXPORT jlongArray JNICALL Java_jdd_DebugJDD_DebugJDD_1GetExternalRefCounts
-  (JNIEnv *, jclass);
-
-#ifdef __cplusplus
-}
-#endif
-#endif
-/* Header for class jdd_DebugJDD_DebugJDDNodeLight */
-
-#ifndef _Included_jdd_DebugJDD_DebugJDDNodeLight
-#define _Included_jdd_DebugJDD_DebugJDDNodeLight
-#ifdef __cplusplus
-extern "C" {
-#endif
-#ifdef __cplusplus
-}
-#endif
-#endif
-/* Header for class jdd_DebugJDD_DebugJDDNode */
-
-#ifndef _Included_jdd_DebugJDD_DebugJDDNode
-#define _Included_jdd_DebugJDD_DebugJDDNode
-#ifdef __cplusplus
-extern "C" {
-#endif
-#ifdef __cplusplus
-}
-#endif
-#endif

prism/include/JDD.h

@@ -679,6 +679,22 @@ JNIEXPORT void JNICALL Java_jdd_JDD_DD_1ExportMatrixToMatlabFile
 JNIEXPORT void JNICALL Java_jdd_JDD_DD_1ExportMatrixToSpyFile
   (JNIEnv *, jclass, jlong, jlong, jint, jlong, jint, jint, jstring);
 
+/*
+ * Class:     jdd_JDD
+ * Method:    DebugJDD_GetRefCount
+ * Signature: (J)I
+ */
+JNIEXPORT jint JNICALL Java_jdd_JDD_DebugJDD_1GetRefCount
+  (JNIEnv *, jclass, jlong);
+
+/*
+ * Class:     jdd_JDD
+ * Method:    DebugJDD_GetExternalRefCounts
+ * Signature: ()[J
+ */
+JNIEXPORT jlongArray JNICALL Java_jdd_JDD_DebugJDD_1GetExternalRefCounts
+  (JNIEnv *, jclass);
+
 #ifdef __cplusplus
 }
 #endif

prism/src/jdd/DebugJDD.java

@@ -82,19 +82,6 @@ import prism.PrismLog;
  */
 public class DebugJDD
 {
-	private static native int DebugJDD_GetRefCount(long dd);
-
-	private static native long[] DebugJDD_GetExternalRefCounts();
-
-	static {
-		try {
-			System.loadLibrary("jdd");
-		} catch (UnsatisfiedLinkError e) {
-			System.out.println(e);
-			System.exit(1);
-		}
-	}
-
 	/**
 	 * A DebugJDDNode extends a JDDNode with additional information
 	 * useful for tracking refs/derefs and tracing.
@@ -172,7 +159,7 @@ public class DebugJDD
 				throw new RuntimeException("DebugJDD: The number of Java references is negative for\n " + toStringVerbose());
 			}
 			// (2) There are more Java references than CUDD references
-			if (jrefs > DebugJDD_GetRefCount(ptr())) {
+			if (jrefs > JDD.DebugJDD_GetRefCount(ptr())) {
 				throw new RuntimeException("DebugJDD: More Java refs than CUDD refs for\n " + toStringVerbose());
 			}
 			// (3) This node has more refs than there are Java refs in total
@@ -194,7 +181,7 @@ public class DebugJDD
 			       + ", refs for this JDDNode = " + getNodeRefs()
 			       + ", refs from Java = " + getJavaRefCount(ptr())
 			       + ", refs from CUDD (including internal MTBDD refs) = "
-			       + DebugJDD_GetRefCount(ptr());
+			       + JDD.DebugJDD_GetRefCount(ptr());
 		}
 
 		public String ptrAsHex()
@@ -370,7 +357,7 @@ public class DebugJDD
 	/** Get the CUDD reference count for the pointer of the JDDNode */
 	public static int getRefCount(JDDNode n)
 	{
-		return DebugJDD_GetRefCount(n.ptr());
+		return JDD.DebugJDD_GetRefCount(n.ptr());
 	}
 
 	/** Get the number of DebugJDDNodes that reference the pointer */
@@ -387,7 +374,7 @@ public class DebugJDD
 	{
 		Map<Long, Integer> result = new TreeMap<Long, Integer>();
 		// Array consists of (pointer, count) pairs
-		long[] externalRefCounts = DebugJDD_GetExternalRefCounts();
+		long[] externalRefCounts = JDD.DebugJDD_GetExternalRefCounts();
 		int i = 0;
 		while (i < externalRefCounts.length) {
 			long node = externalRefCounts[i++];
@@ -403,9 +390,9 @@ public class DebugJDD
 	private static String nodeInfo(long ptr)
 	{
 		if (JDDNode.DDN_IsConstant(ptr)) {
-			return "constant(" + JDDNode.DDN_GetValue(ptr) + "), CUDD refs=" + DebugJDD_GetRefCount(ptr);
+			return "constant(" + JDDNode.DDN_GetValue(ptr) + "), CUDD refs=" + JDD.DebugJDD_GetRefCount(ptr);
 		} else {
-			return "var(" + JDDNode.DDN_GetIndex(ptr) + "), CUDD refs=" + DebugJDD_GetRefCount(ptr);
+			return "var(" + JDDNode.DDN_GetIndex(ptr) + "), CUDD refs=" + JDD.DebugJDD_GetRefCount(ptr);
 		}
 	}
 
@@ -515,7 +502,7 @@ public class DebugJDD
 			throw new RuntimeException("DebugJDD: Trying to Deref a JDDNode with non-positive Java ref count:\n " + dNode.toStringVerbose());
 		}
 
-		int cuddRefCount = DebugJDD_GetRefCount(node.ptr());
+		int cuddRefCount = JDD.DebugJDD_GetRefCount(node.ptr());
 		if (cuddRefCount <= 0) {
 			throw new RuntimeException("DebugJDD: Trying to Deref a JDDNode with a non-positive CUDD ref count\n " + dNode.toStringVerbose());
 		}
@@ -626,7 +613,7 @@ public class DebugJDD
 			throw new RuntimeException("DebugJDD: Trying to use a JDDNode with non-positive Java ref count in a method call:\n " + dNode.toStringVerbose());
 		}
 
-		int cuddRefCount = DebugJDD_GetRefCount(node.ptr());
+		int cuddRefCount = JDD.DebugJDD_GetRefCount(node.ptr());
 		if (cuddRefCount <= 0) {
 			throw new RuntimeException("DebugJDD: Trying to use a JDDNode with a non-positive CUDD ref count in a method call:\n " + dNode.toStringVerbose());
 		}

prism/src/jdd/JDD.cc

@@ -28,7 +28,6 @@
 #include "JDD.h"
 #include "JDDNode.h"
 #include "JDDVars.h"
-#include "DebugJDD.h"
 #include "jnipointer.h"
 
 #include <stdio.h>
@@ -881,14 +880,14 @@ JNIEXPORT jint JNICALL Java_jdd_JDDVars_DDV_1GetIndex(JNIEnv *env, jobject obj,
 
 //------------------------------------------------------------------------------
 
-JNIEXPORT jint JNICALL Java_jdd_DebugJDD_DebugJDD_1GetRefCount(JNIEnv *env, jclass cls, jlong __jlongpointer dd)
+JNIEXPORT jint JNICALL Java_jdd_JDD_DebugJDD_1GetRefCount(JNIEnv *env, jclass cls, jlong __jlongpointer dd)
 {
 	return (jlong_to_DdNode(dd))->ref;
 }
 
 //------------------------------------------------------------------------------
 
-JNIEXPORT jlongArray JNICALL Java_jdd_DebugJDD_DebugJDD_1GetExternalRefCounts(JNIEnv *env, jclass cls)
+JNIEXPORT jlongArray JNICALL Java_jdd_JDD_DebugJDD_1GetExternalRefCounts(JNIEnv *env, jclass cls)
 {
 	// get external reference counts and return as a long[] Java array
 	// the entries of the array will be alternating ptr / count values

prism/src/jdd/JDD.java

@@ -123,6 +123,10 @@ public class JDD
 	private static native void DD_ExportMatrixToMatlabFile(long dd, long rvars, int num_rvars, long cvars, int num_cvars, String name, String filename);
 	private static native void DD_ExportMatrixToSpyFile(long dd, long rvars, int num_rvars, long cvars, int num_cvars, int depth, String filename);
 
+	// helpers for DebugJDD, package visibility
+	static native int DebugJDD_GetRefCount(long dd);
+	static native long[] DebugJDD_GetExternalRefCounts();
+
 	/**
 	 * An exception indicating that CUDD ran out of memory or that another internal error
 	 * occurred.

prism/src/jdd/Makefile

@@ -33,7 +33,7 @@ O_FILES = $(CC_FILES:%.cc=$(PRISM_DIR_REL)/$(OBJ_DIR)/$(THIS_DIR)/%.o)
 
 default: all
 
-all: checks $(CLASS_FILES) $(PRISM_DIR_REL)/$(INCLUDE_DIR)/JDD.h $(PRISM_DIR_REL)/$(INCLUDE_DIR)/JDDNode.h $(PRISM_DIR_REL)/$(INCLUDE_DIR)/JDDVars.h $(PRISM_DIR_REL)/$(INCLUDE_DIR)/DebugJDD.h $(PRISM_DIR_REL)/$(LIB_DIR)/$(LIBPREFIX)jdd$(LIBSUFFIX)
+all: checks $(CLASS_FILES) $(PRISM_DIR_REL)/$(INCLUDE_DIR)/JDD.h $(PRISM_DIR_REL)/$(INCLUDE_DIR)/JDDNode.h $(PRISM_DIR_REL)/$(INCLUDE_DIR)/JDDVars.h $(PRISM_DIR_REL)/$(LIB_DIR)/$(LIBPREFIX)jdd$(LIBSUFFIX)
 
 # Try and prevent accidental makes (i.e. called manually, not from top-level Makefile)
 checks:
@@ -62,12 +62,6 @@ $(PRISM_DIR_REL)/$(INCLUDE_DIR)/JDDVars.h: $(PRISM_DIR_REL)/$(CLASSES_DIR)/$(THI
 	  (dos2unix $@) \
 	fi; 
 
-$(PRISM_DIR_REL)/$(INCLUDE_DIR)/DebugJDD.h: $(PRISM_DIR_REL)/$(CLASSES_DIR)/$(THIS_DIR)/DebugJDD.class
-	($(JAVAH) -classpath $(PRISM_DIR_REL)/$(CLASSES_DIR) -jni -o $@ $(THIS_DIR).DebugJDD; touch $@)
-	@if [ "$(LIBSUFFIX)" = ".dll" ]; then \
-	  (dos2unix $@) \
-	fi; 
-
 $(PRISM_DIR_REL)/$(LIB_DIR)/$(LIBPREFIX)jdd$(LIBSUFFIX): $(O_FILES)
 	$(LD) $(SHARED) $(LDFLAGS) -o $@ $(O_FILES) $(LIBRARIES)