Limit number of choices in choose expression to at most 10000 (#725)

* Limit number of choices in a choose(.) to atmost 10,000 Adds throwing a compile-time or runtime error if the number of choices in a choose(.) is greater than 10000. Updates GitHub docs to reflect this change. * Adds regression tests for choose exceeding 10000 choices * [PSym] Throw error if number of choices are greater than 10000
p-org · May 2, 2024 · 5f96108 · 5f96108
1 parent 5e7f6c6
commit 5f96108
Show file tree

Hide file tree

Showing 13 changed files with 158 additions and 1 deletion.
diff --git a/Docs/docs/manual/expressions.md b/Docs/docs/manual/expressions.md
@@ -342,3 +342,12 @@ The choose operation can be used to model nondeterministic environment machines
 
 !!! note ""
     Performing a `choose` over an empty collection leads to an error. Also, `choose` from a `map` value returns a random key from the map.
+
+Note that the maximum number of choices allowed in a `choose(expr)` is 10,000. Performing a `choose` with an `int` value greater than 10000 or over a collection with more than 10000 elements leads to an error.
+
+``` java
+choose(10001) // throws a compile-time error
+choose(x)     // throws a runtime error if x is of integer type and has value greater than 10000
+choose(x)     // throws a runtime error if x is of seq/set/map type and has size greater than 10000 elements
+```
+
diff --git a/Src/PCompiler/CompilerCore/DefaultTranslationErrorHandler.cs b/Src/PCompiler/CompilerCore/DefaultTranslationErrorHandler.cs
@@ -159,6 +159,11 @@ public Exception IllegalChooseSubExprType(PParser.ChooseExprContext context, PLa
             return IssueError(context, $"choose expects a parameter of type int (max value) or a collection type (seq, set, or map) got a parameter of type {subExprType}");
         }
 
+        public Exception IllegalChooseSubExprValue(PParser.ChooseExprContext context, int numChoices)
+        {
+            return IssueError(context, $"choose expects a parameter with at most 10000 choices, got {numChoices} choices instead.");
+        }
+
         public Exception IllegalFunctionUsedInSpecMachine(Function function, Machine callerOwner)
         {
             return IssueError(function.SourceLocation,

diff --git a/Src/PCompiler/CompilerCore/ITranslationErrorHandler.cs b/Src/PCompiler/CompilerCore/ITranslationErrorHandler.cs
@@ -116,6 +116,7 @@ Exception DuplicateStartState(
         Exception MoreThanOneParameterForHandlers(ParserRuleContext sourceLocation, int count);
 
         Exception IllegalChooseSubExprType(PParser.ChooseExprContext context, PLanguageType subExprType);
+        Exception IllegalChooseSubExprValue(PParser.ChooseExprContext context, int numChoices);
         Exception IllegalFunctionUsedInSpecMachine(Function function, Machine callerOwner);
 
         String SpecObservesSetIncompleteWarning(ParserRuleContext loc, PEvent ev, Machine machine);

diff --git a/Src/PCompiler/CompilerCore/TypeChecker/ExprVisitor.cs b/Src/PCompiler/CompilerCore/TypeChecker/ExprVisitor.cs
@@ -393,7 +393,11 @@ public override IPExpr VisitChooseExpr(PParser.ChooseExprContext context)
                     return new ChooseExpr(context, subExpr, mapType.KeyType);
 
                 case PrimitiveType primType when primType.IsSameTypeAs(PrimitiveType.Int):
+                {
+                    if (subExpr is IntLiteralExpr subExprAsInt && subExprAsInt.Value > 10000)
+                        throw handler.IllegalChooseSubExprValue(context, subExprAsInt.Value);
                     return new ChooseExpr(context, subExpr, PrimitiveType.Int);
+                }
 
                 default:
                     throw handler.IllegalChooseSubExprType(context, subExprType);

diff --git a/Src/PRuntimes/PCSharpRuntime/PMachine.cs b/Src/PRuntimes/PCSharpRuntime/PMachine.cs
@@ -136,21 +136,27 @@ public IPrtValue TryRandom(IPrtValue param)
             switch (param)
             {
                 case PrtInt maxValue:
+                {
+                    TryAssert(maxValue <= 10000, $"choose expects a parameter with at most 10000 choices, got {maxValue} choices instead.");
                     return (PrtInt)TryRandomInt(maxValue);
+                }
 
                 case PrtSeq seq:
                 {
                     TryAssert(seq.Any(), "Trying to choose from an empty sequence!");
+                    TryAssert(seq.Count <= 10000, $"choose expects a parameter with at most 10000 choices, got {seq.Count} choices instead.");
                     return seq[TryRandomInt(seq.Count)];
                 }
                 case PrtSet set:
                 {
                     TryAssert(set.Any(), "Trying to choose from an empty set!");
+                    TryAssert(set.Count <= 10000, $"choose expects a parameter with at most 10000 choices, got {set.Count} choices instead.");
                     return set.ElementAt(TryRandomInt(set.Count));
                 }
                 case PrtMap map:
                 {
                     TryAssert(map.Any(), "Trying to choose from an empty map!");
+                    TryAssert(map.Keys.Count <= 10000, $"choose expects a parameter with at most 10000 choices, got {map.Keys.Count} choices instead.");
                     return map.Keys.ElementAt(TryRandomInt(map.Keys.Count));
                 }
                 default:

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");

diff --git a/Tst/RegressionTests/Feature3Exprs/DynamicError/tooManyChoicesInt/tooManyChoicesInt.p b/Tst/RegressionTests/Feature3Exprs/DynamicError/tooManyChoicesInt/tooManyChoicesInt.p
@@ -0,0 +1,16 @@
+machine Main {
+	start state S {
+		entry {
+		    var x: int;
+		    var y: int;
+
+		    x = 10000;
+		    y = choose(x); // OK
+		    print format("y is {0}", y);
+
+		    x = 10001;
+		    y = choose(x); // error
+		    print format("y is {0}", y);
+		}
+	}
+}
diff --git a/Tst/RegressionTests/Feature3Exprs/DynamicError/tooManyChoicesMap/tooManyChoicesMap.p b/Tst/RegressionTests/Feature3Exprs/DynamicError/tooManyChoicesMap/tooManyChoicesMap.p
@@ -0,0 +1,22 @@
+machine Main {
+	start state S {
+		entry {
+		    var x: map[int, int];
+		    var y: int;
+		    var i: int;
+
+            i = 0;
+            while (i < 10000) {
+                x[i] = i;
+                i = i + 1;
+            }
+
+		    y = choose(x); // OK
+		    print format("y is {0}", y);
+
+            x[i] = i;
+		    y = choose(x); // error
+		    print format("y is {0}", y);
+		}
+	}
+}
diff --git a/Tst/RegressionTests/Feature3Exprs/DynamicError/tooManyChoicesSeq/tooManyChoicesSeq.p b/Tst/RegressionTests/Feature3Exprs/DynamicError/tooManyChoicesSeq/tooManyChoicesSeq.p
@@ -0,0 +1,22 @@
+machine Main {
+	start state S {
+		entry {
+		    var x: seq[int];
+		    var y: int;
+		    var i: int;
+
+            i = 0;
+            while (i < 10000) {
+                x += (i, i);
+                i = i + 1;
+            }
+
+		    y = choose(x); // OK
+		    print format("y is {0}", y);
+
+            x += (i, i);
+		    y = choose(x); // error
+		    print format("y is {0}", y);
+		}
+	}
+}
diff --git a/Tst/RegressionTests/Feature3Exprs/DynamicError/tooManyChoicesSet/tooManyChoicesSet.p b/Tst/RegressionTests/Feature3Exprs/DynamicError/tooManyChoicesSet/tooManyChoicesSet.p
@@ -0,0 +1,22 @@
+machine Main {
+	start state S {
+		entry {
+		    var x: set[int];
+		    var y: int;
+		    var i: int;
+
+            i = 0;
+            while (i < 10000) {
+                x += (i);
+                i = i + 1;
+            }
+            
+		    y = choose(x); // OK
+		    print format("y is {0}", y);
+		    
+            x += (i);
+		    y = choose(x); // error
+		    print format("y is {0}", y);
+		}
+	}
+}
diff --git a/Tst/RegressionTests/Feature3Exprs/StaticError/tooManyChoices/tooManyChoices.p b/Tst/RegressionTests/Feature3Exprs/StaticError/tooManyChoices/tooManyChoices.p
@@ -0,0 +1,14 @@
+machine Main {
+	start state S {
+		entry {
+		    var x: int;
+		    var y: int;
+
+		    x = choose(10000); // OK
+		    print format("x is {0}", x);
+
+		    y = choose(10001); // error
+		    print format("y is {0}", y);
+		}
+	}
+}