ODD: Use int64_t for offsets everywhere, check for arithmetic overflow

Before, the ODD offsets (for indexing into the reachable states) were
stored as longs, resulting in inconsistent numbers of (symbolic)
states that can be treated. In particular, on Win64, long is 32bit.

We switch to int64_t for the ODD offsets everywhere, allowing
MTBDD computations for models with >2^31 states.

Additionally, we check for arithmetic overflow in the offset
computations.  Due to the symbolic storage for the models and the
state space explosion, it's possible to construct simple model files
that reach the 2^63 states limit.

If this limit is reached, we now throw an error message. In the future
it might be worthwile to ensure that PRISM can deal with the absence
of an ODD for all the computations that don't absolutely require it
and carry on (most MTBDD engine algorithms should be fine).



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

prism/include/odd.h

@@ -29,6 +29,8 @@
 
 //------------------------------------------------------------------------------
 
+#include <cstdint>
+
 #include <util.h>
 #include <cudd.h>
 #include <dd.h>
@@ -51,8 +53,8 @@ struct ODDNode
 	ODDNode *next;
 	ODDNode *e;
 	ODDNode *t;
-	long eoff;
-	long toff;
+	int64_t eoff;
+	int64_t toff;
 };
 
 // function prototypes

prism/src/odd/ODDUtils.java

@@ -27,6 +27,7 @@
 package odd;
 
 import jdd.*;
+import prism.PrismException;
 
 public class ODDUtils
 {
@@ -65,17 +66,20 @@ public class ODDUtils
 	private static native long ODD_BuildODD(long dd, long vars, int num_vars);
 	/**
 	 *  Build an ODD.
+	 * @throws PrismException if the ODD could not be constructed
 	 */
-	public static ODDNode BuildODD(JDDNode dd, JDDVars vars)
+	public static ODDNode BuildODD(JDDNode dd, JDDVars vars) throws PrismException
 	{
 		if (jdd.SanityJDD.enabled) {
 			// ODD construction requires the JDDVars to be in ascending order
 			jdd.SanityJDD.checkVarsAreSorted(vars);
 		}
 
-		return new ODDNode(
-			ODD_BuildODD(dd.ptr(), vars.array(), vars.n())
-		);
+		long res = ODD_BuildODD(dd.ptr(), vars.array(), vars.n());
+		if (res == 0) {
+			throw new PrismException("Can not construct ODD for this model, number of states too large: " + JDD.GetNumMintermsString(dd, vars.n()) + " states");
+		}
+		return new ODDNode(res);
 	}
 
 	private static native void ODD_ClearODD(long ptr);

prism/src/odd/odd.cc

@@ -32,7 +32,7 @@ static int num_odd_nodes = 0;
 
 // local prototypes
 static ODDNode *build_odd_rec(DdManager *ddman, DdNode *dd, int level, DdNode **vars, int num_vars, ODDNode **tables);
-static long add_offsets(DdManager *ddman, ODDNode *dd, int level, int num_vars);
+static int64_t add_offsets(DdManager *ddman, ODDNode *dd, int level, int num_vars);
 static DdNode *single_index_to_bdd_rec(DdManager *ddman, int i, DdNode **vars, int num_vars, int level, ODDNode *odd, long o);
 
 //------------------------------------------------------------------------------
@@ -82,7 +82,12 @@ ODDNode *build_odd(DdManager *ddman, DdNode *dd, DdNode **vars, int num_vars)
 	}
 
 	// add offsets to odd
-	add_offsets(ddman, res, 0, num_vars);
+	if (add_offsets(ddman, res, 0, num_vars) < 0) {
+		// negative value indicates that there was an arithmetic overflow
+		// cleanup and return 0
+		clear_odd(res);
+		res = 0;
+	}
 
 	// free memory
 	delete tables;
@@ -138,9 +143,14 @@ static ODDNode *build_odd_rec(DdManager *ddman, DdNode *dd, int level, DdNode **
 
 //------------------------------------------------------------------------------
 
-long add_offsets(DdManager *ddman, ODDNode *odd, int level, int num_vars)
+//
+// Compute the actual eoff and toff values.
+// Returns eoff + toff for this odd node or -1 if there is an arithmetic overflow
+// (can not store eoff+toff in an int64_t)
+int64_t add_offsets(DdManager *ddman, ODDNode *odd, int level, int num_vars)
 {
 	if ((odd->eoff == -1) || (odd->toff == -1)) {
+		// this node has not yet been seen
 		if (level == num_vars) {
 			if (odd->dd == Cudd_ReadZero(ddman)) {
 				odd->eoff = 0;
@@ -153,10 +163,22 @@ long add_offsets(DdManager *ddman, ODDNode *odd, int level, int num_vars)
 		}
 		else {
 			odd->eoff = add_offsets(ddman, odd->e, level+1, num_vars);
+			if (odd->eoff < 0) return -1;
 			odd->toff = add_offsets(ddman, odd->t, level+1, num_vars);
+			if (odd->toff < 0) return -1;
+		}
+
+		// overflow check for sum
+		// do unsigned addition, guaranteed to not overflow
+		// as eoff and toff are signed and positive, cast sum to signed and
+		// check that it is larger than one of the summands
+		int64_t tmp = (int64_t)((uint64_t)odd->eoff + (uint64_t)odd->toff);
+		if (tmp < odd->eoff) {
+			// we have an overflow
+			return -1;
 		}
 	}
-	
+
 	return odd->eoff + odd->toff;
 }
 

prism/src/prism/Model.java

@@ -164,9 +164,9 @@ public interface Model
 
 	void resetTrans(JDDNode trans);
 	void resetTransRewards(int i, JDDNode transRewards);
-	void doReachability();
-	void skipReachability();
-	void setReach(JDDNode reach);
+	void doReachability() throws PrismException;
+	void skipReachability() throws PrismException;
+	void setReach(JDDNode reach) throws PrismException;
 	void setTransActions(JDDNode transActions); // MDPs only
 	void setTransPerAction(JDDNode[] transPerAction); // D/CTMCs only
 	void filterReachableStates();

prism/src/prism/NondetModel.java

@@ -202,7 +202,7 @@ public class NondetModel extends ProbModel
 
 	// do reachability
 
-	public void doReachability()
+	public void doReachability() throws PrismException
 	{
 		JDDNode tmp;
 
@@ -227,7 +227,7 @@ public class NondetModel extends ProbModel
 	 * <br/>[ REFS: <i>result</i>, DEREFS: seed ]
 	 * @param seed set of states (over ddRowVars) that is known to be reachable
 	 */
-	public void doReachability(JDDNode seed)
+	public void doReachability(JDDNode seed) throws PrismException
 	{
 		JDDNode tmp;
 

prism/src/prism/ProbModel.java

@@ -567,7 +567,7 @@ public class ProbModel implements Model
 
 	// do reachability
 
-	public void doReachability()
+	public void doReachability() throws PrismException
 	{
 		// compute reachable states
 		setReach(PrismMTBDD.Reachability(trans01, allDDRowVars, allDDColVars, start));
@@ -581,7 +581,7 @@ public class ProbModel implements Model
 	 * <br/>[ REFS: <i>result</i>, DEREFS: seed ]
 	 * @param seed set of states (over ddRowVars) that is known to be reachable
 	 */
-	public void doReachability(JDDNode seed)
+	public void doReachability(JDDNode seed) throws PrismException
 	{
 		// do sanity check on seed if checking is enabled
 		if (SanityJDD.enabled)
@@ -597,7 +597,7 @@ public class ProbModel implements Model
 	// this method allows you to skip the reachability phase
 	// it is only here for experimental purposes - not general use.
 
-	public void skipReachability()
+	public void skipReachability() throws PrismException
 	{
 		// don't compute reachable states - assume all reachable
 		reach = JDD.Constant(1);
@@ -608,6 +608,7 @@ public class ProbModel implements Model
 		// build odd, clear old one
 		if (odd != null) {
 			ODDUtils.ClearODD(odd);
+			odd = null;
 		}
 		odd = ODDUtils.BuildODD(reach, allDDRowVars);
 	}
@@ -616,7 +617,7 @@ public class ProbModel implements Model
 	 * Set reachable states BDD (and compute number of states and ODD)
 	 */
 
-	public void setReach(JDDNode reach)
+	public void setReach(JDDNode reach) throws PrismException
 	{
 		if (this.reach != null)
 			JDD.Deref(this.reach);
@@ -628,6 +629,7 @@ public class ProbModel implements Model
 		// build odd, clear old one
 		if (odd != null) {
 			ODDUtils.ClearODD(odd);
+			odd = null;
 		}
 		odd = ODDUtils.BuildODD(reach, allDDRowVars);
 	}