From 888d62633db53a473bd0b8ec6ad239b976ac06e4 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Tue, 5 Jul 2016 08:59:29 +0000 Subject: [PATCH] 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 | 51 ------------------------------------- prism/include/JDD.h | 16 ++++++++++++ prism/src/jdd/DebugJDD.java | 29 ++++++--------------- prism/src/jdd/JDD.cc | 5 ++-- prism/src/jdd/JDD.java | 4 +++ prism/src/jdd/Makefile | 8 +----- 6 files changed, 31 insertions(+), 82 deletions(-) delete mode 100644 prism/include/DebugJDD.h diff --git a/prism/include/DebugJDD.h b/prism/include/DebugJDD.h deleted file mode 100644 index 47c56198..00000000 --- a/prism/include/DebugJDD.h +++ /dev/null @@ -1,51 +0,0 @@ -/* DO NOT EDIT THIS FILE - it is machine generated */ -#include -/* 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 diff --git a/prism/include/JDD.h b/prism/include/JDD.h index 5c87f2bd..ef18ba45 100644 --- a/prism/include/JDD.h +++ b/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 diff --git a/prism/src/jdd/DebugJDD.java b/prism/src/jdd/DebugJDD.java index cc7d6e92..7f0ca8ce 100644 --- a/prism/src/jdd/DebugJDD.java +++ b/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 result = new TreeMap(); // 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()); } diff --git a/prism/src/jdd/JDD.cc b/prism/src/jdd/JDD.cc index 5b248e04..afb6acba 100644 --- a/prism/src/jdd/JDD.cc +++ b/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 @@ -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 diff --git a/prism/src/jdd/JDD.java b/prism/src/jdd/JDD.java index 5682c5fa..ebfe9e75 100644 --- a/prism/src/jdd/JDD.java +++ b/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. diff --git a/prism/src/jdd/Makefile b/prism/src/jdd/Makefile index 85e523e8..bdbeb417 100644 --- a/prism/src/jdd/Makefile +++ b/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)