From 81bf49b003cd80dd7233132b4b931301dae98049 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 30 Nov 2018 16:06:51 +0100 Subject: [PATCH] PrismSparse.java: Protect interval iteration JNI calls against large state spaces The corresponding `checkNumStates(odd)` were missing. --- prism/src/sparse/PrismSparse.java | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/prism/src/sparse/PrismSparse.java b/prism/src/sparse/PrismSparse.java index 41429007..95008a8a 100644 --- a/prism/src/sparse/PrismSparse.java +++ b/prism/src/sparse/PrismSparse.java @@ -204,6 +204,8 @@ public class PrismSparse private static native long PS_ProbUntilInterval(long trans, long odd, long rv, int nrv, long cv, int ncv, long yes, long maybe, int flags); public static DoubleVector ProbUntilInterval(JDDNode trans, ODDNode odd, JDDVars rows, JDDVars cols, JDDNode yes, JDDNode maybe, int flags) throws PrismException { + checkNumStates(odd); + long ptr = PS_ProbUntilInterval(trans.ptr(), odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), yes.ptr(), maybe.ptr(), flags); if (ptr == 0) throw generateExceptionForError(); return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff())); @@ -246,6 +248,8 @@ public class PrismSparse private static native long PS_ProbReachRewardInterval(long trans, long sr, long trr, long odd, long rv, int nrv, long cv, int ncv, long goal, long inf, long maybe, long lower, long upper, int flags); public static DoubleVector ProbReachRewardInterval(JDDNode trans, JDDNode sr, JDDNode trr, ODDNode odd, JDDVars rows, JDDVars cols, JDDNode goal, JDDNode inf, JDDNode maybe, JDDNode lower, JDDNode upper, int flags) throws PrismException { + checkNumStates(odd); + long ptr = PS_ProbReachRewardInterval(trans.ptr(), sr.ptr(), trr.ptr(), odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), goal.ptr(), inf.ptr(), maybe.ptr(), lower.ptr(), upper.ptr(), flags); if (ptr == 0) throw generateExceptionForError(); return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff())); @@ -292,6 +296,8 @@ public class PrismSparse private static native long PS_NondetUntilInterval(long trans, long trans_actions, List synchs, long odd, long rv, int nrv, long cv, int ncv, long ndv, int nndv, long yes, long maybe, boolean minmax, long strat, int flags); public static DoubleVector NondetUntilInterval(JDDNode trans, JDDNode transActions, List synchs, ODDNode odd, JDDVars rows, JDDVars cols, JDDVars nondet, JDDNode yes, JDDNode maybe, boolean minmax, IntegerVector strat, int flags) throws PrismException { + checkNumStates(odd); + long ptr = PS_NondetUntilInterval(trans.ptr(), (transActions == null) ? 0 : transActions.ptr(), synchs, odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), nondet.array(), nondet.n(), yes.ptr(), maybe.ptr(), minmax, (strat == null) ? 0 : strat.getPtr(), flags); if (ptr == 0) throw generateExceptionForError(); return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff())); @@ -334,6 +340,8 @@ public class PrismSparse private static native long PS_NondetReachRewardInterval(long trans, long trans_actions, List synchs, long sr, long trr, long odd, long rv, int nrv, long cv, int ncv, long ndv, int nndv, long goal, long inf, long maybe, long lower, long upper, boolean minmax, int flags); public static DoubleVector NondetReachRewardInterval(JDDNode trans, JDDNode transActions, List synchs, JDDNode sr, JDDNode trr, ODDNode odd, JDDVars rows, JDDVars cols, JDDVars nondet, JDDNode goal, JDDNode inf, JDDNode maybe, JDDNode lower, JDDNode upper, boolean minmax, int flags) throws PrismException { + checkNumStates(odd); + long ptr = PS_NondetReachRewardInterval(trans.ptr(), (transActions == null) ? 0 : transActions.ptr(), synchs, sr.ptr(), trr.ptr(), odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), nondet.array(), nondet.n(), goal.ptr(), inf.ptr(), maybe.ptr(), lower.ptr(), upper.ptr(), minmax, flags); if (ptr == 0) throw generateExceptionForError(); return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff()));