From 1d8f9fc6b9a8ec44ade8f7dbc04b3688f8f95bc5 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Thu, 13 Jul 2017 15:09:47 +0000 Subject: [PATCH] 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 | 6 ++++-- prism/src/odd/ODDUtils.java | 12 ++++++++---- prism/src/odd/odd.cc | 30 ++++++++++++++++++++++++++---- prism/src/prism/Model.java | 6 +++--- prism/src/prism/NondetModel.java | 4 ++-- prism/src/prism/ProbModel.java | 10 ++++++---- 6 files changed, 49 insertions(+), 19 deletions(-) diff --git a/prism/include/odd.h b/prism/include/odd.h index c7c8f2f6..2af55eed 100644 --- a/prism/include/odd.h +++ b/prism/include/odd.h @@ -29,6 +29,8 @@ //------------------------------------------------------------------------------ +#include + #include #include #include @@ -51,8 +53,8 @@ struct ODDNode ODDNode *next; ODDNode *e; ODDNode *t; - long eoff; - long toff; + int64_t eoff; + int64_t toff; }; // function prototypes diff --git a/prism/src/odd/ODDUtils.java b/prism/src/odd/ODDUtils.java index c209c881..5fdbad7d 100644 --- a/prism/src/odd/ODDUtils.java +++ b/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); diff --git a/prism/src/odd/odd.cc b/prism/src/odd/odd.cc index 9efea586..bd530756 100644 --- a/prism/src/odd/odd.cc +++ b/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; } diff --git a/prism/src/prism/Model.java b/prism/src/prism/Model.java index da47dad8..98b0fb00 100644 --- a/prism/src/prism/Model.java +++ b/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(); diff --git a/prism/src/prism/NondetModel.java b/prism/src/prism/NondetModel.java index f3ac6d23..46715248 100644 --- a/prism/src/prism/NondetModel.java +++ b/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 *
[ REFS: result, 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; diff --git a/prism/src/prism/ProbModel.java b/prism/src/prism/ProbModel.java index 2f608030..7843fb1e 100644 --- a/prism/src/prism/ProbModel.java +++ b/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 *
[ REFS: result, 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); }