[PSym] Throw error if number of choices are greater than 10000

p-org · May 2, 2024 · 4fa1b5d · 4fa1b5d
1 parent 895d1f1
commit 4fa1b5d
Show file tree

Hide file tree

Showing 3 changed files with 37 additions and 1 deletion.
diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/Scheduler.java b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/Scheduler.java
@@ -16,6 +16,7 @@
 import psym.runtime.scheduler.search.symmetry.SymmetryTracker;
 import psym.runtime.statistics.SearchStats;
 import psym.utils.Assert;
+import psym.utils.exception.BugFoundException;
 import psym.utils.random.NondetUtil;
 import psym.valuesummary.*;
 
@@ -148,7 +149,14 @@ public List<PrimitiveVS> getNextIntegerChoices(PrimitiveVS<Integer> bound, Guard
     if (!zeroGuard.isFalse()) {
       bound = bound.updateUnderGuard(zeroGuard, new PrimitiveVS<Integer>(1));
     }
-    for (int i = 0; i < IntegerVS.maxValue(bound); i++) {
+    int maxBound = IntegerVS.maxValue(bound);
+    if (maxBound > 10000) {
+      Guard maxBoundGuard = bound.getGuardFor(maxBound);
+      throw new BugFoundException(
+              String.format("choose expects a parameter with at most 10,000 choices, got %d choices instead.", maxBound),
+              maxBoundGuard);
+    }
+    for (int i = 0; i < maxBound; i++) {
       Guard cond = IntegerVS.lessThan(i, bound).getGuardFor(true);
       choices.add(new PrimitiveVS<>(i).restrict(cond).restrict(pc));
     }
@@ -190,6 +198,13 @@ public PrimitiveVS<Boolean> getNextBoolean(Guard pc) {
 
   public List<ValueSummary> getNextElementChoices(ListVS candidates, Guard pc) {
     PrimitiveVS<Integer> size = candidates.size();
+    int maxSize = IntegerVS.maxValue(size);
+    if (maxSize > 10000) {
+      Guard maxSizeGuard = size.getGuardFor(maxSize);
+      throw new BugFoundException(
+              String.format("choose expects a parameter with at most 10,000 choices, got %d choices instead.", maxSize),
+              maxSizeGuard);
+    }
     PrimitiveVS<Integer> index = new PrimitiveVS<>(0).restrict(size.getUniverse());
     List<ValueSummary> list = new ArrayList<>();
     while (BooleanVS.isEverTrue(IntegerVS.lessThan(index, size))) {

diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/replay/ReplayScheduler.java b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/replay/ReplayScheduler.java
@@ -15,6 +15,7 @@
 import psym.runtime.scheduler.Scheduler;
 import psym.runtime.scheduler.search.symmetry.SymmetryMode;
 import psym.utils.Assert;
+import psym.utils.exception.BugFoundException;
 import psym.utils.exception.LivenessException;
 import psym.valuesummary.*;
 
@@ -197,6 +198,13 @@ public PrimitiveVS<Boolean> getNextBoolean(Guard pc) {
 
   @Override
   public PrimitiveVS<Integer> getNextInteger(PrimitiveVS<Integer> bound, Guard pc) {
+    int maxBound = IntegerVS.maxValue(bound);
+    if (maxBound > 10000) {
+      Guard maxBoundGuard = bound.getGuardFor(maxBound);
+      throw new BugFoundException(
+              String.format("choose expects a parameter with at most 10,000 choices, got %d choices instead.", maxBound),
+              maxBoundGuard);
+    }
     PrimitiveVS<Integer> res = schedule.getRepeatInt(choiceDepth);
     ScheduleWriter.logInteger(res);
     choiceDepth++;
@@ -205,6 +213,14 @@ public PrimitiveVS<Integer> getNextInteger(PrimitiveVS<Integer> bound, Guard pc)
 
   @Override
   public ValueSummary getNextPrimitiveList(ListVS<? extends ValueSummary> candidates, Guard pc) {
+    PrimitiveVS<Integer> size = candidates.size();
+    int maxSize = IntegerVS.maxValue(size);
+    if (maxSize > 10000) {
+      Guard maxSizeGuard = size.getGuardFor(maxSize);
+      throw new BugFoundException(
+              String.format("choose expects a parameter with at most 10,000 choices, got %d choices instead.", maxSize),
+              maxSizeGuard);
+    }
     ValueSummary res = getNextElementFlattener(schedule.getRepeatElement(choiceDepth));
     List<GuardedValue<?>> gv = ValueSummary.getGuardedValues(res);
     assert (gv.size() == 1);

diff --git a/Src/PRuntimes/PSymRuntime/src/test/java/psym/TestSymbolicRegression.java b/Src/PRuntimes/PSymRuntime/src/test/java/psym/TestSymbolicRegression.java
@@ -68,6 +68,11 @@ private static void setRunArgs() {
   }
 
   private static void createExcludeList() {
+    // TODO Unsupported: too many choices to throw error if choices more than 10000
+    excluded.add("../../../Tst/RegressionTests/Feature3Exprs/DynamicError/tooManyChoicesSeq");
+    excluded.add("../../../Tst/RegressionTests/Feature3Exprs/DynamicError/tooManyChoicesSet");
+    excluded.add("../../../Tst/RegressionTests/Feature3Exprs/DynamicError/tooManyChoicesMap");
+
     // TODO Unsupported: liveness with temperatures
     excluded.add("../../../Tst/RegressionTests/Liveness/Correct/Liveness_1");
     excluded.add("../../../Tst/RegressionTests/Liveness/Correct/Liveness_1_falsePass");