[PEx] Adds tracking and limiting number of choices per choose(.) stat…

…ement

Adds tracking number of calls and total choices generated in a schedule corresponding to each choose(.) statement in the model.

Adds option --max-choices-per-call and --max-choices-total to limit max number of choices in a schedule corresponding to a choose(.) statement (default is 10,000 for per choose.) call and no limit on total choices, as in C# backend). Else, a TooManyChoicesException is triggered as a bug.

Src/PCompiler/CompilerCore/Backend/PEx/PExCodeGenerator.cs

@@ -1664,37 +1664,45 @@ private void WriteExpr(CompilationContext context, StringWriter output, IPExpr e
                 break;
             case NondetExpr _:
             case FairNondetExpr _:
-                context.Write(output, $"{CompilationContext.SchedulerVar}.getRandomBool()");
+            {
+                var loc = $"\"{context.LocationResolver.GetLocation(expr.SourceLocation).ToString()
+                    .Replace(@"\", @"\\")}\"";
+                context.Write(output, $"{CompilationContext.SchedulerVar}.getRandomBool({loc})");
                 break;
+            }
             case ChooseExpr chooseExpr:
+            {
+                var loc = $"\"{context.LocationResolver.GetLocation(chooseExpr.SourceLocation).ToString()
+                    .Replace(@"\", @"\\")}\"";
+
                 if (chooseExpr.SubExpr == null)
                 {
-                    context.Write(output, $"({CompilationContext.SchedulerVar}.getRandomBool())");
+                    context.Write(output, $"{CompilationContext.SchedulerVar}.getRandomBool({loc})");
                     return;
                 }
 
                 switch (chooseExpr.SubExpr.Type.Canonicalize())
                 {
                     case PrimitiveType primitiveType when primitiveType.IsSameTypeAs(PrimitiveType.Int):
-                        context.Write(output, $"{CompilationContext.SchedulerVar}.getRandomInt(");
+                        context.Write(output, $"{CompilationContext.SchedulerVar}.getRandomInt({loc}, ");
                         WriteExpr(context, output, chooseExpr.SubExpr);
                         context.Write(output, ")");
                         break;
                     case SequenceType sequenceType:
                         context.Write(output,
-                            $"({GetPExType(sequenceType.ElementType)}) {CompilationContext.SchedulerVar}.getRandomEntry(");
+                            $"({GetPExType(sequenceType.ElementType)}) {CompilationContext.SchedulerVar}.getRandomEntry({loc}, ");
                         WriteExpr(context, output, chooseExpr.SubExpr);
                         context.Write(output, ")");
                         break;
                     case SetType setType:
                         context.Write(output,
-                            $"({GetPExType(setType.ElementType)}) {CompilationContext.SchedulerVar}.getRandomEntry(");
+                            $"({GetPExType(setType.ElementType)}) {CompilationContext.SchedulerVar}.getRandomEntry({loc}, ");
                         WriteExpr(context, output, chooseExpr.SubExpr);
                         context.Write(output, ")");
                         break;
                     case MapType mapType:
                         context.Write(output,
-                            $"({GetPExType(mapType.KeyType)}) {CompilationContext.SchedulerVar}.getRandomEntry(");
+                            $"({GetPExType(mapType.KeyType)}) {CompilationContext.SchedulerVar}.getRandomEntry({loc}, ");
                         WriteExpr(context, output, chooseExpr.SubExpr);
                         context.Write(output, ")");
                         break;
@@ -1704,6 +1712,7 @@ private void WriteExpr(CompilationContext context, StringWriter output, IPExpr e
                 }
 
                 break;
+            }
             case SizeofExpr sizeOfExpr:
                 WriteExpr(context, output, sizeOfExpr.Expr);
                 context.Write(output, ".size()");

Src/PRuntimes/PExRuntime/src/main/java/pex/RuntimeExecutor.java

@@ -12,6 +12,7 @@
 import pex.runtime.scheduler.replay.ReplayScheduler;
 import pex.utils.exceptions.BugFoundException;
 import pex.utils.exceptions.MemoutException;
+import pex.utils.exceptions.TooManyChoicesException;
 import pex.utils.monitor.MemoryMonitor;
 import pex.utils.monitor.TimeMonitor;
 import pex.utils.monitor.TimedCall;
@@ -158,6 +159,9 @@ private static void process(boolean resume) throws Exception {
         } catch (BugFoundException e) {
             PExGlobal.setStatus(STATUS.BUG_FOUND);
             PExGlobal.setResult(String.format("found cex of length %d", e.getScheduler().getStepNumber()));
+            if (e instanceof TooManyChoicesException) {
+                PExGlobal.setResult(PExGlobal.getResult() + " (too many choices)");
+            }
             e.getScheduler().getLogger().logStackTrace(e);
 
             String schFile = PExGlobal.getConfig().getOutputFolder() + "/" + PExGlobal.getConfig().getProjectName() + "_0_0.schedule";
@@ -226,6 +230,9 @@ private static void replaySchedule(String fileName) throws Exception {
         } catch (BugFoundException replayException) {
             PExGlobal.setStatus(STATUS.BUG_FOUND);
             PExGlobal.setResult(String.format("found cex of length %d", replayer.getStepNumber()));
+            if (replayException instanceof TooManyChoicesException) {
+                PExGlobal.setResult(PExGlobal.getResult() + " (too many choices)");
+            }
             PExLogger.logStackTrace(replayException);
             throw replayException;
         } catch (Exception replayException) {

Src/PRuntimes/PExRuntime/src/main/java/pex/commandline/PExConfig.java

@@ -75,4 +75,10 @@ public class PExConfig {
     //max number of children search tasks
     @Setter
     int maxChildrenPerTask = 2;
+    //max number of choices per choose(.) operation per call
+    @Setter
+    int maxChoiceBoundPerCall = 10000;
+    //max number of choices per choose(.) operation in total
+    @Setter
+    int maxChoiceBoundTotal = 0;
 }

Src/PRuntimes/PExRuntime/src/main/java/pex/commandline/PExOptions.java

@@ -237,6 +237,28 @@ public class PExOptions {
                         .build();
         addHiddenOption(choiceSelect);
 
+        // max number of choices per choose(.) call
+        Option maxChoicesPerCall =
+                Option.builder()
+                        .longOpt("max-choices-per-call")
+                        .desc("Max number of choices allowed per choose statement per call (default: 10000)")
+                        .numberOfArgs(1)
+                        .hasArg()
+                        .argName("(integer)")
+                        .build();
+        addHiddenOption(maxChoicesPerCall);
+
+        // max number of choices in total
+        Option maxChoicesTotal =
+                Option.builder()
+                        .longOpt("max-choices-total")
+                        .desc("Max number of choices allowed per choose statement in total (default: no bound)")
+                        .numberOfArgs(1)
+                        .hasArg()
+                        .argName("(integer)")
+                        .build();
+        addHiddenOption(maxChoicesTotal);
+
         /*
          * Help menu options
          */
@@ -470,6 +492,21 @@ public static PExConfig ParseCommandlineArgs(String[] args) {
                                     option,
                                     String.format("Unrecognized choice selection mode, got %s", option.getValue()));
                     }
+                case "max-choices-per-call":
+                    try {
+                        config.setMaxChoiceBoundPerCall(Integer.parseInt(option.getValue()));
+                    } catch (NumberFormatException ex) {
+                        optionError(
+                                option, String.format("Expected an integer value, got %s", option.getValue()));
+                    }
+                    break;
+                case "max-choices-total":
+                    try {
+                        config.setMaxChoiceBoundTotal(Integer.parseInt(option.getValue()));
+                    } catch (NumberFormatException ex) {
+                        optionError(
+                                option, String.format("Expected an integer value, got %s", option.getValue()));
+                    }
                     break;
                 case "h":
                 case "help":

Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/Scheduler.java

@@ -8,7 +8,6 @@
 import pex.runtime.machine.PMachineId;
 import pex.runtime.machine.PMonitor;
 import pex.runtime.scheduler.explicit.StepState;
-import pex.utils.exceptions.BugFoundException;
 import pex.utils.exceptions.NotImplementedException;
 import pex.utils.misc.Assert;
 import pex.values.*;
@@ -145,8 +144,10 @@ public void updateLogNumber() {
      *
      * @return boolean data choice
      */
-    public PBool getRandomBool() {
+    public PBool getRandomBool(String loc) {
         List<PValue<?>> choices = new ArrayList<>();
+        stepState.updateChoiceStats(loc, 2);
+
         choices.add(PBool.PTRUE);
         choices.add(PBool.PFALSE);
         return (PBool) getNextDataChoice(choices);
@@ -158,15 +159,14 @@ public PBool getRandomBool() {
      * @param bound upper bound (exclusive) on the integer.
      * @return integer data choice
      */
-    public PInt getRandomInt(PInt bound) {
+    public PInt getRandomInt(String loc, PInt bound) {
         List<PValue<?>> choices = new ArrayList<>();
         int boundInt = bound.getValue();
-        if (boundInt > 10000) {
-            throw new BugFoundException(String.format("choose expects a parameter with at most 10,000 choices, got %d choices instead.", boundInt));
-        }
         if (boundInt == 0) {
             boundInt = 1;
         }
+        stepState.updateChoiceStats(loc, boundInt);
+
         for (int i = 0; i < boundInt; i++) {
             choices.add(new PInt(i));
         }
@@ -179,8 +179,8 @@ public PInt getRandomInt(PInt bound) {
      * @param choices List of data choices
      * @return data choice
      */
-    protected PValue<?> getRandomEntry(List<PValue<?>> choices) {
-        PInt randomEntryIdx = getRandomInt(new PInt(choices.size()));
+    protected PValue<?> getRandomEntry(String loc, List<PValue<?>> choices) {
+        PInt randomEntryIdx = getRandomInt(loc, new PInt(choices.size()));
         return choices.get(randomEntryIdx.getValue());
     }
 
@@ -190,8 +190,8 @@ protected PValue<?> getRandomEntry(List<PValue<?>> choices) {
      * @param seq PSeq object
      * @return data choice
      */
-    public PValue<?> getRandomEntry(PSeq seq) {
-        return getRandomEntry(seq.toList());
+    public PValue<?> getRandomEntry(String loc, PSeq seq) {
+        return getRandomEntry(loc, seq.toList());
     }
 
     /**
@@ -200,8 +200,8 @@ public PValue<?> getRandomEntry(PSeq seq) {
      * @param set PSet object
      * @return data choice
      */
-    public PValue<?> getRandomEntry(PSet set) {
-        return getRandomEntry(set.toList());
+    public PValue<?> getRandomEntry(String loc, PSet set) {
+        return getRandomEntry(loc, set.toList());
     }
 
     /**
@@ -210,8 +210,8 @@ public PValue<?> getRandomEntry(PSet set) {
      * @param map PMap object
      * @return data choice
      */
-    public PValue<?> getRandomEntry(PMap map) {
-        return getRandomEntry(map.toList());
+    public PValue<?> getRandomEntry(String loc, PMap map) {
+        return getRandomEntry(loc, map.toList());
     }
 
     /**

Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/SchedulerInterface.java

@@ -18,40 +18,45 @@ public interface SchedulerInterface extends Serializable {
     /**
      * Return a random PBool based on the search and strategy.
      *
+     * @param loc location in P model
      * @return a boolean choice.
      */
-    PBool getRandomBool();
+    PBool getRandomBool(String loc);
 
     /**
      * Return a random PInt (within a bound) based on the search and strategy.
      *
+     * @param loc   location in P model
      * @param bound upper bound (exclusive) on the integer.
      * @return a integer
      */
-    PInt getRandomInt(PInt bound);
+    PInt getRandomInt(String loc, PInt bound);
 
     /**
      * Return a random element of a PSeq based on the search and strategy.
      *
+     * @param loc      location in P model
      * @param elements list to choose from
      * @return a integer
      */
-    PValue<?> getRandomEntry(PSeq elements);
+    PValue<?> getRandomEntry(String loc, PSeq elements);
 
     /**
      * Return a random element of a PSet based on the search and strategy.
      *
+     * @param loc      location in P model
      * @param elements set to choose from
      * @return a integer
      */
-    PValue<?> getRandomEntry(PSet elements);
+    PValue<?> getRandomEntry(String loc, PSet elements);
 
     /**
      * Return a random key of a PMap based on the search and strategy.
      *
+     * @param loc      location in P model
      * @param elements map to choose from
      * @return a integer
      */
-    PValue<?> getRandomEntry(PMap elements);
+    PValue<?> getRandomEntry(String loc, PMap elements);
 
 }

Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/StepState.java

@@ -1,8 +1,10 @@
 package pex.runtime.scheduler.explicit;
 
 import lombok.Getter;
+import pex.runtime.PExGlobal;
 import pex.runtime.machine.MachineLocalState;
 import pex.runtime.machine.PMachine;
+import pex.utils.exceptions.TooManyChoicesException;
 
 import java.io.Serializable;
 import java.util.*;
@@ -22,6 +24,16 @@ public class StepState implements Serializable {
      */
     private Map<PMachine, MachineLocalState> machineLocalStates = new HashMap<>();
 
+    /**
+     * Map from choose(.) location to total number of calls
+     */
+    private Map<String, Integer> choicesNumCalls = new HashMap<>();
+
+    /**
+     * Map from choose(.) location to total number of choices
+     */
+    private Map<String, Integer> choicesNumChoices = new HashMap<>();
+
     public StepState copyState() {
         StepState stepState = new StepState();
 
@@ -33,12 +45,11 @@ public StepState copyState() {
         }
 
         assert (stepState.machines.size() == stepState.machineLocalStates.size());
-        return stepState;
-    }
 
-    public void clear() {
-        machines.clear();
-        machineLocalStates.clear();
+        stepState.choicesNumCalls = new HashMap<>(this.choicesNumCalls);
+        stepState.choicesNumChoices = new HashMap<>(this.choicesNumChoices);
+
+        return stepState;
     }
 
 
@@ -47,6 +58,8 @@ public void resetToZero(SortedSet<PMachine> allMachines) {
             machine.reset();
         }
         machines.clear();
+        choicesNumCalls.clear();
+        choicesNumChoices.clear();
     }
 
     public void setTo(SortedSet<PMachine> allMachines, StepState input) {
@@ -62,6 +75,9 @@ public void setTo(SortedSet<PMachine> allMachines, StepState input) {
                 machine.setMachineState(ms);
             }
         }
+
+        choicesNumCalls = new HashMap<>(input.choicesNumCalls);
+        choicesNumChoices = new HashMap<>(input.choicesNumChoices);
     }
 
     /**
@@ -105,6 +121,22 @@ public String getTimelineString() {
         return s.toString();
     }
 
+    public void updateChoiceStats(String loc, int num) {
+        if (!choicesNumCalls.containsKey(loc)) {
+            choicesNumCalls.put(loc, 1);
+            choicesNumChoices.put(loc, num);
+        } else {
+            choicesNumCalls.put(loc, choicesNumCalls.get(loc) + 1);
+            choicesNumChoices.put(loc, choicesNumChoices.get(loc) + num);
+        }
+        if (PExGlobal.getConfig().getMaxChoiceBoundPerCall() > 0 && num > PExGlobal.getConfig().getMaxChoiceBoundPerCall()) {
+            throw new TooManyChoicesException(loc, num);
+        }
+        if (PExGlobal.getConfig().getMaxChoiceBoundTotal() > 0 && choicesNumChoices.get(loc) > PExGlobal.getConfig().getMaxChoiceBoundTotal()) {
+            throw new TooManyChoicesException(loc, choicesNumChoices.get(loc), choicesNumCalls.get(loc));
+        }
+    }
+
     @Override
     public String toString() {
         if (this == null) {