From d73591178be303cae13fcc7f04744a4129399469 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 30 Nov 2018 16:09:15 +0100 Subject: [PATCH] PrismHybrid.java: Protect interval iteration JNI calls against large state spaces The corresponding `checkNumStates(odd)` were missing. --- prism/src/hybrid/PrismHybrid.java | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/prism/src/hybrid/PrismHybrid.java b/prism/src/hybrid/PrismHybrid.java index bad55505..bf52be94 100644 --- a/prism/src/hybrid/PrismHybrid.java +++ b/prism/src/hybrid/PrismHybrid.java @@ -204,6 +204,8 @@ public class PrismHybrid private static native long PH_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 = PH_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 PrismHybrid private static native long PH_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 = PH_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()));