From 0debba13327edb40b01c0ea51d304fdce471ea50 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 9 Sep 2011 17:45:49 +0000 Subject: [PATCH] New JDD debugging code from Vojta (disabled by default). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3639 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/include/DebugJDD.h | 23 +++++ prism/src/jdd/DebugJDD.java | 165 ++++++++++++++++++++++++++++++++++++ prism/src/jdd/JDD.cc | 5 ++ prism/src/jdd/JDD.java | 82 ++++++++++++++++++ prism/src/jdd/JDDNode.java | 4 +- prism/src/jdd/Makefile | 5 +- prism/src/prism/Prism.java | 2 + 7 files changed, 284 insertions(+), 2 deletions(-) create mode 100644 prism/include/DebugJDD.h create mode 100644 prism/src/jdd/DebugJDD.java diff --git a/prism/include/DebugJDD.h b/prism/include/DebugJDD.h new file mode 100644 index 00000000..cae8dfad --- /dev/null +++ b/prism/include/DebugJDD.h @@ -0,0 +1,23 @@ +/* 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 +#undef jdd_DebugJDD_debugEnabled +#define jdd_DebugJDD_debugEnabled 1L +/* + * Class: jdd_DebugJDD + * Method: DebugJDD_GetRefCount + * Signature: (J)I + */ +JNIEXPORT jint JNICALL Java_jdd_DebugJDD_DebugJDD_1GetRefCount + (JNIEnv *, jclass, jlong); + +#ifdef __cplusplus +} +#endif +#endif diff --git a/prism/src/jdd/DebugJDD.java b/prism/src/jdd/DebugJDD.java new file mode 100644 index 00000000..b5750f71 --- /dev/null +++ b/prism/src/jdd/DebugJDD.java @@ -0,0 +1,165 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Vojtech Forejt (University of Oxford) +// +//------------------------------------------------------------------------------ +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +package jdd; + +import java.util.HashMap; +import java.util.LinkedList; +import java.util.List; + +public class DebugJDD +{ + private static native int DebugJDD_GetRefCount(long dd); + + static { + try { + System.loadLibrary("jdd"); + } catch (UnsatisfiedLinkError e) { + System.out.println(e); + System.exit(1); + } + } + + /** + * determines if the debugging of JDD nodes is enabled. + */ + public static final boolean debugEnabled = false; + + /** + * Where stack traces are kept. + * Key: hashcode of a JDDNode + * Value: stack trace from the moment the JDDNode was constructed. + */ + protected static HashMap stackTraces; + + /** + * Keeps track of refs and derefs made in Java + * Key: hashcode of a JDDNode + * Value: 1 + (number of times the node was refed) - (number of times the node was derefed) + */ + protected static HashMap localCounters; + + /** + * Keeps track of instances of JDDNode pointing to (native) DdNode + * Key: pointer to a DdNode + * Value: list of hashcodes of JDDNodes pointing to the DdNode + */ + protected static HashMap> instances; + + protected static void addToSet(JDDNode node) + { + //not thread safe + if (instances == null) { + instances = new HashMap>(); + localCounters = new HashMap(); + stackTraces = new HashMap(); + } + + int hc = System.identityHashCode(node); + if (instances.containsKey(node.ptr())) { + long ptr = node.ptr(); + instances.get(ptr).add(hc); + } else { + long ptr = node.ptr(); + List al = new LinkedList(); + al.add(hc); + instances.put(ptr, al); + } + localCounters.put(hc, 1); + + StackTraceElement[] st = Thread.currentThread().getStackTrace(); + //ignore first two elements which are Thread and this constructor + int num = st.length - 2; + StackTraceElement[] creator = new StackTraceElement[num]; + for (int i = 0; i < num; i++) { + creator[i] = st[i + 2]; + } + stackTraces.put(hc, creator); + } + + protected static void decrement(JDDNode node) + { + int hc = System.identityHashCode(node); + int newValue = localCounters.get(hc) - 1; + localCounters.put(hc, newValue); + } + + protected static void increment(JDDNode node) + { + int hc = System.identityHashCode(node); + int newValue = localCounters.get(hc) - 1; + localCounters.put(hc, newValue); + } + + public static void endLifeCycle() + { + for (Long ptr : instances.keySet()) { + //check if cudd has nonzero number of references + int cuddRefCount = DebugJDD_GetRefCount(ptr); + if (cuddRefCount != 0) { + //check if there is a JDD object with nonzero refcount + boolean hasSuspicious = false; + for (Integer hc : instances.get(ptr)) { + int localRefCount = localCounters.get(hc); + if (localRefCount > 0) { + hasSuspicious = true; + break; + } + } + + //if !hasSuspicious, there is no useful output we could give. + //Either it's false alarm, or the problem is in c++ + if (!hasSuspicious) + continue; + System.out.println("WARNING: there are nodes with nonzero references, printing debug info. " + + "Note that the stack traces below are from moments JDDNodes were " + + "created. The actual problem can be elsewhere where the node is used"); + //print warning together with suspicious nodes + System.out.println("Node has " + cuddRefCount + " reference(s), printing out stack traces of suspicious node instances:"); + boolean first = true; + for (Integer hc : instances.get(ptr)) { + int localRefCount = localCounters.get(hc); + if (localRefCount != 0) { + if (!first) { + System.out.println(" &"); + //first=false; + } else { + first = false; + } + //print only top 5 methods from stack + int i = 0; + for (StackTraceElement st : stackTraces.get(hc)) { + if (i++ > 5) { + break; + } + System.out.println(" " + st.toString()); + } + } + } + } + } + } +} diff --git a/prism/src/jdd/JDD.cc b/prism/src/jdd/JDD.cc index 455cea10..af550c42 100644 --- a/prism/src/jdd/JDD.cc +++ b/prism/src/jdd/JDD.cc @@ -28,6 +28,7 @@ #include "JDD.h" #include "JDDNode.h" #include "JDDVars.h" +#include "DebugJDD.h" #include "jnipointer.h" #include @@ -867,3 +868,7 @@ 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) +{ + return (jlong_to_DdNode(dd))->ref; +} diff --git a/prism/src/jdd/JDD.java b/prism/src/jdd/JDD.java index a2bb16f3..1ea2c6e2 100644 --- a/prism/src/jdd/JDD.java +++ b/prism/src/jdd/JDD.java @@ -237,6 +237,8 @@ public class JDD public static void Ref(JDDNode dd) { + if (DebugJDD.debugEnabled) + DebugJDD.increment(dd); DD_Ref(dd.ptr()); } @@ -245,6 +247,8 @@ public class JDD public static void Deref(JDDNode dd) { + if (DebugJDD.debugEnabled) + DebugJDD.decrement(dd); DD_Deref(dd.ptr()); } @@ -306,6 +310,8 @@ public class JDD public static JDDNode Not(JDDNode dd) { + if (DebugJDD.debugEnabled) + DebugJDD.decrement(dd); return new JDDNode(DD_Not(dd.ptr())); } @@ -314,6 +320,10 @@ public class JDD public static JDDNode Or(JDDNode dd1, JDDNode dd2) { + if (DebugJDD.debugEnabled) { + DebugJDD.decrement(dd1); + DebugJDD.decrement(dd2); + } return new JDDNode(DD_Or(dd1.ptr(), dd2.ptr())); } @@ -322,6 +332,11 @@ public class JDD public static JDDNode And(JDDNode dd1, JDDNode dd2) { + if (DebugJDD.debugEnabled) { + DebugJDD.decrement(dd1); + DebugJDD.decrement(dd2); + } + return new JDDNode(DD_And(dd1.ptr(), dd2.ptr())); } @@ -330,6 +345,10 @@ public class JDD public static JDDNode Xor(JDDNode dd1, JDDNode dd2) { + if (DebugJDD.debugEnabled) { + DebugJDD.decrement(dd1); + DebugJDD.decrement(dd2); + } return new JDDNode(DD_Xor(dd1.ptr(), dd2.ptr())); } @@ -354,6 +373,10 @@ public class JDD public static JDDNode Implies(JDDNode dd1, JDDNode dd2) { + if (DebugJDD.debugEnabled) { + DebugJDD.decrement(dd1); + DebugJDD.decrement(dd2); + } return new JDDNode(DD_Implies(dd1.ptr(), dd2.ptr())); } @@ -362,6 +385,10 @@ public class JDD public static JDDNode Apply(int op, JDDNode dd1, JDDNode dd2) { + if (DebugJDD.debugEnabled) { + DebugJDD.decrement(dd1); + DebugJDD.decrement(dd2); + } return new JDDNode(DD_Apply(op, dd1.ptr(), dd2.ptr())); } @@ -370,6 +397,8 @@ public class JDD public static JDDNode MonadicApply(int op, JDDNode dd) { + if (DebugJDD.debugEnabled) + DebugJDD.decrement(dd); return new JDDNode(DD_MonadicApply(op, dd.ptr())); } @@ -378,6 +407,10 @@ public class JDD public static JDDNode Restrict(JDDNode dd, JDDNode cube) { + if (DebugJDD.debugEnabled) { + DebugJDD.decrement(dd); + DebugJDD.decrement(cube); + } return new JDDNode(DD_Restrict(dd.ptr(), cube.ptr())); } @@ -386,6 +419,11 @@ public class JDD public static JDDNode ITE(JDDNode dd1, JDDNode dd2, JDDNode dd3) { + if (DebugJDD.debugEnabled) { + DebugJDD.decrement(dd1); + DebugJDD.decrement(dd2); + DebugJDD.decrement(dd3); + } return new JDDNode(DD_ITE(dd1.ptr(), dd2.ptr(), dd3.ptr())); } @@ -396,6 +434,8 @@ public class JDD public static JDDNode PermuteVariables(JDDNode dd, JDDVars old_vars, JDDVars new_vars) { + if (DebugJDD.debugEnabled) + DebugJDD.decrement(dd); return new JDDNode(DD_PermuteVariables(dd.ptr(), old_vars.array(), new_vars.array(), old_vars.n())); } @@ -404,6 +444,8 @@ public class JDD public static JDDNode SwapVariables(JDDNode dd, JDDVars old_vars, JDDVars new_vars) { + if (DebugJDD.debugEnabled) + DebugJDD.decrement(dd); return new JDDNode(DD_SwapVariables(dd.ptr(), old_vars.array(), new_vars.array(), old_vars.n())); } @@ -454,6 +496,8 @@ public class JDD public static JDDNode ThereExists(JDDNode dd, JDDVars vars) { + if (DebugJDD.debugEnabled) + DebugJDD.decrement(dd); return new JDDNode(DD_ThereExists(dd.ptr(), vars.array(), vars.n())); } @@ -462,6 +506,8 @@ public class JDD public static JDDNode ForAll(JDDNode dd, JDDVars vars) { + if (DebugJDD.debugEnabled) + DebugJDD.decrement(dd); return new JDDNode(DD_ForAll(dd.ptr(), vars.array(), vars.n())); } @@ -470,6 +516,8 @@ public class JDD public static JDDNode SumAbstract(JDDNode dd, JDDVars vars) { + if (DebugJDD.debugEnabled) + DebugJDD.decrement(dd); return new JDDNode(DD_SumAbstract(dd.ptr(), vars.array(), vars.n())); } @@ -478,6 +526,8 @@ public class JDD public static JDDNode ProductAbstract(JDDNode dd, JDDVars vars) { + if (DebugJDD.debugEnabled) + DebugJDD.decrement(dd); return new JDDNode(DD_ProductAbstract(dd.ptr(), vars.array(), vars.n())); } @@ -486,6 +536,8 @@ public class JDD public static JDDNode MinAbstract(JDDNode dd, JDDVars vars) { + if (DebugJDD.debugEnabled) + DebugJDD.decrement(dd); return new JDDNode(DD_MinAbstract(dd.ptr(), vars.array(), vars.n())); } @@ -494,6 +546,8 @@ public class JDD public static JDDNode MaxAbstract(JDDNode dd, JDDVars vars) { + if (DebugJDD.debugEnabled) + DebugJDD.decrement(dd); return new JDDNode(DD_MaxAbstract(dd.ptr(), vars.array(), vars.n())); } @@ -504,6 +558,8 @@ public class JDD public static JDDNode GreaterThan(JDDNode dd, double threshold) { + if (DebugJDD.debugEnabled) + DebugJDD.decrement(dd); return new JDDNode(DD_GreaterThan(dd.ptr(), threshold)); } @@ -512,6 +568,8 @@ public class JDD public static JDDNode GreaterThanEquals(JDDNode dd, double threshold) { + if (DebugJDD.debugEnabled) + DebugJDD.decrement(dd); return new JDDNode(DD_GreaterThanEquals(dd.ptr(), threshold)); } @@ -520,6 +578,8 @@ public class JDD public static JDDNode LessThan(JDDNode dd, double threshold) { + if (DebugJDD.debugEnabled) + DebugJDD.decrement(dd); return new JDDNode(DD_LessThan(dd.ptr(), threshold)); } @@ -528,6 +588,8 @@ public class JDD public static JDDNode LessThanEquals(JDDNode dd, double threshold) { + if (DebugJDD.debugEnabled) + DebugJDD.decrement(dd); return new JDDNode(DD_LessThanEquals(dd.ptr(), threshold)); } @@ -536,6 +598,8 @@ public class JDD public static JDDNode Equals(JDDNode dd, double value) { + if (DebugJDD.debugEnabled) + DebugJDD.decrement(dd); return new JDDNode(DD_Equals(dd.ptr(), value)); } @@ -544,6 +608,8 @@ public class JDD public static JDDNode Interval(JDDNode dd, double lower, double upper) { + if (DebugJDD.debugEnabled) + DebugJDD.decrement(dd); return new JDDNode(DD_Interval(dd.ptr(), lower, upper)); } @@ -552,6 +618,8 @@ public class JDD public static JDDNode RoundOff(JDDNode dd, int places) { + if (DebugJDD.debugEnabled) + DebugJDD.decrement(dd); return new JDDNode(DD_RoundOff(dd.ptr(), places)); } @@ -584,6 +652,8 @@ public class JDD public static JDDNode RestrictToFirst(JDDNode dd, JDDVars vars) { + if (DebugJDD.debugEnabled) + DebugJDD.decrement(dd); return new JDDNode(DD_RestrictToFirst(dd.ptr(), vars.array(), vars.n())); } @@ -792,6 +862,8 @@ public class JDD public static JDDNode SetVectorElement(JDDNode dd, JDDVars vars, long index, double value) { + if (DebugJDD.debugEnabled) + DebugJDD.decrement(dd); return new JDDNode(DD_SetVectorElement(dd.ptr(), vars.array(), vars.n(), index, value)); } @@ -800,6 +872,8 @@ public class JDD public static JDDNode SetMatrixElement(JDDNode dd, JDDVars rvars, JDDVars cvars, long rindex, long cindex, double value) { + if (DebugJDD.debugEnabled) + DebugJDD.decrement(dd); return new JDDNode(DD_SetMatrixElement(dd.ptr(), rvars.array(), rvars.n(), cvars.array(), cvars.n(), rindex, cindex, value)); } @@ -808,6 +882,8 @@ public class JDD public static JDDNode Set3DMatrixElement(JDDNode dd, JDDVars rvars, JDDVars cvars, JDDVars lvars, long rindex, long cindex, long lindex, double value) { + if (DebugJDD.debugEnabled) + DebugJDD.decrement(dd); return new JDDNode(DD_Set3DMatrixElement(dd.ptr(), rvars.array(), rvars.n(), cvars.array(), cvars.n(), lvars.array(), lvars.n(), rindex, cindex, lindex, value)); } @@ -832,6 +908,8 @@ public class JDD public static JDDNode Transpose(JDDNode dd, JDDVars rvars, JDDVars cvars) { + if (DebugJDD.debugEnabled) + DebugJDD.decrement(dd); return new JDDNode(DD_Transpose(dd.ptr(), rvars.array(), cvars.array(), rvars.n())); } @@ -840,6 +918,10 @@ public class JDD public static JDDNode MatrixMultiply(JDDNode dd1, JDDNode dd2, JDDVars vars, int method) { + if (DebugJDD.debugEnabled) { + DebugJDD.decrement(dd1); + DebugJDD.decrement(dd2); + } return new JDDNode(DD_MatrixMultiply(dd1.ptr(), dd2.ptr(), vars.array(), vars.n(), method)); } diff --git a/prism/src/jdd/JDDNode.java b/prism/src/jdd/JDDNode.java index 050e9d7e..81e6684f 100644 --- a/prism/src/jdd/JDDNode.java +++ b/prism/src/jdd/JDDNode.java @@ -51,11 +51,13 @@ public class JDDNode public JDDNode(long p) { ptr = p; + if (DebugJDD.debugEnabled) + DebugJDD.addToSet(this); } public JDDNode(JDDNode dd) { - ptr = dd.ptr; + this(dd.ptr()); } public long ptr() diff --git a/prism/src/jdd/Makefile b/prism/src/jdd/Makefile index ad1d474e..6b5b044b 100644 --- a/prism/src/jdd/Makefile +++ b/prism/src/jdd/Makefile @@ -30,7 +30,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)/$(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)/$(INCLUDE_DIR)/DebugJDD.h $(PRISM_DIR_REL)/$(LIB_DIR)/$(LIBPREFIX)jdd$(LIBSUFFIX) # Try and prevent accidental makes (i.e. called manually, not from top-level Makefile) checks: @@ -50,6 +50,9 @@ $(PRISM_DIR_REL)/$(INCLUDE_DIR)/JDDNode.h: $(PRISM_DIR_REL)/$(CLASSES_DIR)/$(THI $(PRISM_DIR_REL)/$(INCLUDE_DIR)/JDDVars.h: $(PRISM_DIR_REL)/$(CLASSES_DIR)/$(THIS_DIR)/JDDVars.class ($(JAVAH) -classpath $(PRISM_DIR_REL)/$(CLASSES_DIR) -jni -o $@ $(THIS_DIR).JDDVars; touch $@) +$(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 $@) + $(PRISM_DIR_REL)/$(LIB_DIR)/$(LIBPREFIX)jdd$(LIBSUFFIX): $(O_FILES) $(LD) $(SHARED) $(LDFLAGS) -o $@ $(O_FILES) $(LIBRARIES) diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 38bb5845..26432c12 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -1874,6 +1874,8 @@ public class Prism implements PrismSettingsListener if (cuddStarted) { JDD.CloseDownCUDD(check); + if (jdd.DebugJDD.debugEnabled) + DebugJDD.endLifeCycle(); } }