From a7bbeb18ae679e2c4efeaa855eba5c6e359577b0 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Thu, 13 Jul 2017 15:11:56 +0000 Subject: [PATCH] DoubleVector: Check that number of states fit into int If the number of states is too large for the index of the vector to fit into a Java int throw a PrismNotSupportedException. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12022 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/dv/DoubleVector.java | 9 +++++++-- prism/src/prism/ProbModelChecker.java | 2 +- prism/src/prism/StateValues.java | 2 +- prism/src/prism/StateValuesDV.java | 2 +- prism/src/prism/StateValuesMTBDD.java | 2 +- 5 files changed, 11 insertions(+), 6 deletions(-) diff --git a/prism/src/dv/DoubleVector.java b/prism/src/dv/DoubleVector.java index abec1a8a..1b66e4a2 100644 --- a/prism/src/dv/DoubleVector.java +++ b/prism/src/dv/DoubleVector.java @@ -105,11 +105,16 @@ public class DoubleVector /** * Create a new DoubleVector from an existing MTBDD representation of an array. *
[ DEREFS: none ] + * @throws PrismException if number of states is too large (uses Java int based indices) */ - public DoubleVector(JDDNode dd, JDDVars vars, ODDNode odd) + public DoubleVector(JDDNode dd, JDDVars vars, ODDNode odd) throws PrismException { + long numStates = odd.getEOff() + odd.getTOff(); + if (numStates > Integer.MAX_VALUE) { + throw new PrismNotSupportedException("Can not create DoubleVector with more than " + Integer.MAX_VALUE + " states, have " + numStates + " states"); + } v = DV_ConvertMTBDD(dd.ptr(), vars.array(), vars.n(), odd.ptr()); - n = (int)(odd.getEOff() + odd.getTOff()); + n = (int)numStates; } private native long DV_ConvertMTBDD(long dd, long vars, int num_vars, long odd); diff --git a/prism/src/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java index 3cebbe1c..82289243 100644 --- a/prism/src/prism/ProbModelChecker.java +++ b/prism/src/prism/ProbModelChecker.java @@ -1252,7 +1252,7 @@ public class ProbModelChecker extends NonProbModelChecker * the (single) initial state or equiprobable over multiple initial states. * The type of storage (MTBDD or double vector) matches the current engine. */ - private StateValues buildInitialDistribution() + private StateValues buildInitialDistribution() throws PrismException { StateValues dist = null; JDDNode init; diff --git a/prism/src/prism/StateValues.java b/prism/src/prism/StateValues.java index ac4b876f..d7501945 100644 --- a/prism/src/prism/StateValues.java +++ b/prism/src/prism/StateValues.java @@ -38,7 +38,7 @@ import parser.ast.RelOp; public interface StateValues extends StateVector { /** Converts to StateValuesDV, destroys (clear) this vector */ - StateValuesDV convertToStateValuesDV(); + StateValuesDV convertToStateValuesDV() throws PrismException; /** Converts to StateValuesMTBDD, destroys (clear) this vector */ StateValuesMTBDD convertToStateValuesMTBDD(); diff --git a/prism/src/prism/StateValuesDV.java b/prism/src/prism/StateValuesDV.java index d318a2f4..8fc1aa37 100644 --- a/prism/src/prism/StateValuesDV.java +++ b/prism/src/prism/StateValuesDV.java @@ -113,7 +113,7 @@ public class StateValuesDV implements StateValues * @param dd the double vector * @param model the underlying model */ - public StateValuesDV(JDDNode dd, Model model) + public StateValuesDV(JDDNode dd, Model model) throws PrismException { // TODO: Enforce/check that dd is zero for all non-reachable states this(new DoubleVector(dd, model.getAllDDRowVars(), model.getODD()), model); diff --git a/prism/src/prism/StateValuesMTBDD.java b/prism/src/prism/StateValuesMTBDD.java index 0a49ac16..b46ef20e 100644 --- a/prism/src/prism/StateValuesMTBDD.java +++ b/prism/src/prism/StateValuesMTBDD.java @@ -104,7 +104,7 @@ public class StateValuesMTBDD implements StateValues // CONVERSION METHODS @Override - public StateValuesDV convertToStateValuesDV() + public StateValuesDV convertToStateValuesDV() throws PrismException { // convert to StateValuesDV, destroy (clear) old vector StateValuesDV res = new StateValuesDV(values, model);