From 2aa8b5fef93d42341e800c8ba8ac718b1c69e180 Mon Sep 17 00:00:00 2001 From: Aman Goel Date: Mon, 9 Sep 2024 23:12:58 +0000 Subject: [PATCH] [PEx] Several updates to logging, PEx config Changes default max choices limit to 20 per call and 250 per schedule (to account for open-source protocols with monolithic transition relation modeled as single action) Adds logging support to print choose(.) location info for easy debugging TooManyChoicesException via replayer log Minor correction --- .../src/main/java/pex/RuntimeExecutor.java | 26 ++++++++++------ .../main/java/pex/commandline/PExConfig.java | 4 +-- .../java/pex/runtime/logger/PExLogger.java | 25 +++++++++++----- .../pex/runtime/logger/SchedulerLogger.java | 30 +++++++++++++++---- .../java/pex/runtime/scheduler/Scheduler.java | 10 +++---- .../explicit/ExplicitSearchScheduler.java | 8 ++--- .../explicit/SchedulerStatistics.java | 4 +-- .../runtime/scheduler/explicit/StepState.java | 4 ++- .../scheduler/replay/ReplayScheduler.java | 20 +++++++++++-- .../exceptions/TooManyChoicesException.java | 5 ++++ 10 files changed, 96 insertions(+), 40 deletions(-) diff --git a/Src/PRuntimes/PExRuntime/src/main/java/pex/RuntimeExecutor.java b/Src/PRuntimes/PExRuntime/src/main/java/pex/RuntimeExecutor.java index a7225e4e86..236c76aa5c 100644 --- a/Src/PRuntimes/PExRuntime/src/main/java/pex/RuntimeExecutor.java +++ b/Src/PRuntimes/PExRuntime/src/main/java/pex/RuntimeExecutor.java @@ -165,21 +165,25 @@ private static void process() throws Exception { PExLogger.logBugFoundInfo(e.getScheduler()); String schFile = PExGlobal.getConfig().getOutputFolder() + "/" + PExGlobal.getConfig().getProjectName() + "_0_0.schedule"; - PExLogger.logInfo(String.format("Writing buggy trace in %s", schFile)); + PExLogger.logInfo(String.format("... Writing buggy trace in %s", schFile)); e.getScheduler().getSchedule().writeToFile(schFile); - ReplayScheduler replayer = new ReplayScheduler(e.getScheduler().getSchedule()); + ReplayScheduler replayer = new ReplayScheduler(e.getScheduler().getSchedule(), e); PExGlobal.setReplayScheduler(replayer); + PExLogger.logReplayerInfo(replayer); try { replayer.run(); } catch (NullPointerException | StackOverflowError | ClassCastException replayException) { - PExLogger.logStackTrace((Exception) replayException); + replayer.getLogger().logStackTrace((Exception) replayException); + PExLogger.logTrace((Exception) replayException); throw new BugFoundException(replayException.getMessage(), replayException); } catch (BugFoundException replayException) { - PExLogger.logStackTrace(replayException); + replayer.getLogger().logStackTrace(replayException); + PExLogger.logTrace(replayException); throw replayException; } catch (Exception replayException) { - PExLogger.logStackTrace(replayException); + replayer.getLogger().logStackTrace(replayException); + PExLogger.logTrace(replayException); throw new Exception("Error when replaying the bug", replayException); } throw new Exception("Failed to replay bug", e); @@ -218,14 +222,16 @@ public static void runSearch() throws Exception { private static void replaySchedule(String fileName) throws Exception { PExLogger.logInfo(String.format("... Reading buggy trace from %s", fileName)); - ReplayScheduler replayer = new ReplayScheduler(Schedule.readFromFile(fileName)); + ReplayScheduler replayer = new ReplayScheduler(Schedule.readFromFile(fileName), null); PExGlobal.setReplayScheduler(replayer); + PExLogger.logReplayerInfo(replayer); try { replayer.run(); } catch (NullPointerException | StackOverflowError | ClassCastException replayException) { PExGlobal.setStatus(STATUS.BUG_FOUND); PExGlobal.setResult(String.format("found cex of length %d", replayer.getStepNumber())); - PExLogger.logStackTrace((Exception) replayException); + replayer.getLogger().logStackTrace((Exception) replayException); + PExLogger.logTrace((Exception) replayException); throw new BugFoundException(replayException.getMessage(), replayException); } catch (BugFoundException replayException) { PExGlobal.setStatus(STATUS.BUG_FOUND); @@ -233,10 +239,12 @@ private static void replaySchedule(String fileName) throws Exception { if (replayException instanceof TooManyChoicesException) { PExGlobal.setResult(PExGlobal.getResult() + " (too many choices)"); } - PExLogger.logStackTrace(replayException); + replayer.getLogger().logStackTrace(replayException); + PExLogger.logTrace(replayException); throw replayException; } catch (Exception replayException) { - PExLogger.logStackTrace(replayException); + replayer.getLogger().logStackTrace(replayException); + PExLogger.logTrace(replayException); throw new Exception("Error when replaying the bug", replayException); } finally { printStats(); diff --git a/Src/PRuntimes/PExRuntime/src/main/java/pex/commandline/PExConfig.java b/Src/PRuntimes/PExRuntime/src/main/java/pex/commandline/PExConfig.java index c8d8417f7d..6f2e47ed2d 100644 --- a/Src/PRuntimes/PExRuntime/src/main/java/pex/commandline/PExConfig.java +++ b/Src/PRuntimes/PExRuntime/src/main/java/pex/commandline/PExConfig.java @@ -77,8 +77,8 @@ public class PExConfig { int maxChildrenPerTask = 2; //max number of choices per choose(.) operation per call @Setter - int maxChoicesPerStmtPerCall = 10; + int maxChoicesPerStmtPerCall = 20; //max number of choices per choose(.) operation in total @Setter - int maxChoicesPerStmtPerSchedule = 100; + int maxChoicesPerStmtPerSchedule = 250; } diff --git a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/logger/PExLogger.java b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/logger/PExLogger.java index fcaae1813f..a351137461 100644 --- a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/logger/PExLogger.java +++ b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/logger/PExLogger.java @@ -65,7 +65,7 @@ public static void logVerbose(String message) { * @param timeSpent Time spent in seconds */ public static void logEndOfRun(long timeSpent) { - if (verbosity == 0) { + if (verbosity == 0 && PExGlobal.getStatus() != STATUS.BUG_FOUND) { log.info(""); } log.info("--------------------"); @@ -97,12 +97,12 @@ public static void logEndOfRun(long timeSpent) { * * @param e Exception object */ - public static void logStackTrace(Exception e) { - StringWriter sw = new StringWriter(); - PrintWriter pw = new PrintWriter(sw); - e.printStackTrace(pw); - log.info("--------------------"); - log.info(sw.toString()); + public static void logTrace(Exception e) { +// StringWriter sw = new StringWriter(); +// PrintWriter pw = new PrintWriter(sw); +// e.printStackTrace(pw); +// log.info("--------------------"); + log.info(String.format(".... \033[31m %s \033[0m", e)); } /** @@ -112,6 +112,15 @@ public static void logStackTrace(Exception e) { */ public static void logBugFoundInfo(Scheduler sch) { log.info("--------------------"); - log.info(String.format("Thread %d found a bug. Details in %s", sch.getSchedulerId(), sch.getLogger().getFileName())); + log.info(String.format("... Thread %d found a bug. Details in %s", sch.getSchedulerId(), sch.getLogger().getFileName())); + } + + /** + * Prints replayer info + * + * @param sch Replay scheduler + */ + public static void logReplayerInfo(Scheduler sch) { + log.info(String.format("... Replaying bug. Details in %s", sch.getLogger().getFileName())); } } diff --git a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/logger/SchedulerLogger.java b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/logger/SchedulerLogger.java index 0e24b8b0bc..37d86f0a03 100644 --- a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/logger/SchedulerLogger.java +++ b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/logger/SchedulerLogger.java @@ -44,6 +44,10 @@ public class SchedulerLogger { */ public SchedulerLogger(int schId) { verbosity = PExGlobal.getConfig().getVerbosity(); + if (schId == 0 && verbosity == 0) { + // set minimum verbosity to 1 for replay scheduler + verbosity = 1; + } log = Log4JConfig.getContext().getLogger(SchedulerLogger.class.getName() + schId); org.apache.logging.log4j.core.Logger coreLogger = (org.apache.logging.log4j.core.Logger) LogManager.getLogger(SchedulerLogger.class.getName() + schId); @@ -207,9 +211,9 @@ public void logNewScheduleChoice(List choices, int step, int idx) { } } - public void logNewDataChoice(List> choices, int step, int idx) { + public void logNewDataChoice(String loc, List> choices, int step, int idx) { if (verbosity > 1) { - log.info(String.format(" @%d::%d new data choice: %s", step, idx, choices)); + log.info(String.format(" @%d::%d %d new data choices from %s - %s", step, idx, choices.size(), loc, choices)); } } @@ -225,15 +229,15 @@ public void logCurrentScheduleChoice(PMachine choice, int step, int idx) { } } - public void logRepeatDataChoice(PValue choice, int step, int idx) { + public void logRepeatDataChoice(String loc, PValue choice, int step, int idx) { if (verbosity > 2) { - log.info(String.format(" @%d::%d %s (repeat)", step, idx, choice)); + log.info(String.format(" @%d::%d %s (repeat) from %s", step, idx, choice, loc)); } } - public void logCurrentDataChoice(PValue choice, int step, int idx) { + public void logCurrentDataChoice(String loc, PValue choice, int step, int idx) { if (verbosity > 2) { - log.info(String.format(" @%d::%d %s", step, idx, choice)); + log.info(String.format(" @%d::%d %s from %s", step, idx, choice, loc)); } } @@ -411,4 +415,18 @@ public void logStackTrace(Exception e) { log.info("--------------------"); log.info(sw.toString()); } + + /** + * Print choice loc + * + * @param step Step number + * @param idx Choice number + * @param loc choose(.) location + * @param choices Data choices + */ + public void logDataChoiceLoc(int step, int idx, String loc, List> choices) { + if (verbosity > 0) { + log.info(String.format(" @%d::%d %d new data choices from %s - %s", step, idx, choices.size(), loc, choices)); + } + } } diff --git a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/Scheduler.java b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/Scheduler.java index 956a438326..e986a2cf39 100644 --- a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/Scheduler.java +++ b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/Scheduler.java @@ -130,7 +130,7 @@ protected void reset() { * * @return PValue as data choice */ - protected abstract PValue getNextDataChoice(List> input_choices); + protected abstract PValue getNextDataChoice(String loc, List> input_choices); public void updateLogNumber() { stepNumLogs += 1; @@ -146,11 +146,11 @@ public void updateLogNumber() { */ public PBool getRandomBool(String loc) { List> choices = new ArrayList<>(); - stepState.updateChoiceStats(loc, 2); + stepState.updateChoiceStats(this, loc, 2); choices.add(PBool.PTRUE); choices.add(PBool.PFALSE); - return (PBool) getNextDataChoice(choices); + return (PBool) getNextDataChoice(loc, choices); } /** @@ -165,12 +165,12 @@ public PInt getRandomInt(String loc, PInt bound) { if (boundInt == 0) { boundInt = 1; } - stepState.updateChoiceStats(loc, boundInt); + stepState.updateChoiceStats(this, loc, boundInt); for (int i = 0; i < boundInt; i++) { choices.add(new PInt(i)); } - return (PInt) getNextDataChoice(choices); + return (PInt) getNextDataChoice(loc, choices); } /** diff --git a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/ExplicitSearchScheduler.java b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/ExplicitSearchScheduler.java index b7f6e2bb45..c852fda456 100644 --- a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/ExplicitSearchScheduler.java +++ b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/ExplicitSearchScheduler.java @@ -387,14 +387,14 @@ public PMachine getNextScheduleChoice() { * @return PValue as data choice */ @Override - public PValue getNextDataChoice(List> input_choices) { + public PValue getNextDataChoice(String loc, List> input_choices) { PValue result; if (choiceNumber < backtrackChoiceNumber) { // pick the current data choice result = schedule.getCurrentDataChoice(choiceNumber); assert (input_choices.contains(result)); - logger.logRepeatDataChoice(result, stepNumber, choiceNumber); + logger.logRepeatDataChoice(loc, result, stepNumber, choiceNumber); // increment choice number choiceNumber++; @@ -410,7 +410,7 @@ public PValue getNextDataChoice(List> input_choices) { choices = input_choices; if (choices.size() > 1) { // log new choice - logger.logNewDataChoice(choices, stepNumber, choiceNumber); + logger.logNewDataChoice(loc, choices, stepNumber, choiceNumber); } if (choices.isEmpty()) { @@ -425,7 +425,7 @@ public PValue getNextDataChoice(List> input_choices) { // pick a choice int selected = PExGlobal.getChoiceSelector().selectChoice(this, choices); result = choices.get(selected); - logger.logCurrentDataChoice(result, stepNumber, choiceNumber); + logger.logCurrentDataChoice(loc, result, stepNumber, choiceNumber); // remove the selected choice from unexplored choices choices.remove(selected); diff --git a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/SchedulerStatistics.java b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/SchedulerStatistics.java index 658ca3768c..85e26a4c03 100644 --- a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/SchedulerStatistics.java +++ b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/SchedulerStatistics.java @@ -9,12 +9,12 @@ public class SchedulerStatistics { /** * Min steps */ - public int minSteps = 0; + public int minSteps = -1; /** * Max steps */ - public int maxSteps = 0; + public int maxSteps = -1; /** * Total steps diff --git a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/StepState.java b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/StepState.java index e37cf2570b..e2a8b7810d 100644 --- a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/StepState.java +++ b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/explicit/StepState.java @@ -4,6 +4,8 @@ import pex.runtime.PExGlobal; import pex.runtime.machine.MachineLocalState; import pex.runtime.machine.PMachine; +import pex.runtime.scheduler.Scheduler; +import pex.runtime.scheduler.replay.ReplayScheduler; import pex.utils.exceptions.TooManyChoicesException; import java.io.Serializable; @@ -121,7 +123,7 @@ public String getTimelineString() { return s.toString(); } - public void updateChoiceStats(String loc, int num) { + public void updateChoiceStats(Scheduler sch, String loc, int num) { if (!choicesNumCalls.containsKey(loc)) { choicesNumCalls.put(loc, 1); choicesNumChoices.put(loc, num); diff --git a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/replay/ReplayScheduler.java b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/replay/ReplayScheduler.java index 4ac7a13d6d..6feda3a536 100644 --- a/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/replay/ReplayScheduler.java +++ b/Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/replay/ReplayScheduler.java @@ -1,5 +1,6 @@ package pex.runtime.scheduler.replay; +import lombok.Getter; import pex.runtime.PExGlobal; import pex.runtime.logger.ScheduleWriter; import pex.runtime.logger.TextWriter; @@ -7,6 +8,8 @@ import pex.runtime.machine.PMachineId; import pex.runtime.scheduler.Schedule; import pex.runtime.scheduler.Scheduler; +import pex.utils.exceptions.BugFoundException; +import pex.utils.exceptions.TooManyChoicesException; import pex.utils.misc.Assert; import pex.values.PValue; @@ -14,8 +17,11 @@ import java.util.concurrent.TimeoutException; public class ReplayScheduler extends Scheduler { - public ReplayScheduler(Schedule sch) { + @Getter + BugFoundException bugFoundException = null; + public ReplayScheduler(Schedule sch, BugFoundException e) { super(0, sch); + bugFoundException = e; } @Override @@ -105,7 +111,7 @@ protected PMachine getNextScheduleChoice() { } @Override - protected PValue getNextDataChoice(List> input_choices) { + protected PValue getNextDataChoice(String loc, List> input_choices) { if (choiceNumber >= schedule.size()) { return null; } @@ -113,8 +119,16 @@ protected PValue getNextDataChoice(List> input_choices) { // pick the current data choice PValue result = schedule.getCurrentDataChoice(choiceNumber); assert (input_choices.contains(result)); + ScheduleWriter.logDataChoice(result); - logger.logRepeatDataChoice(result, stepNumber, choiceNumber); + logger.logRepeatDataChoice(loc, result, stepNumber, choiceNumber); + if (bugFoundException != null) { + if (bugFoundException instanceof TooManyChoicesException e) { + if (e.getLoc().equals(loc)) { + logger.logDataChoiceLoc(stepNumber, choiceNumber, loc, input_choices); + } + } + } choiceNumber++; return result; diff --git a/Src/PRuntimes/PExRuntime/src/main/java/pex/utils/exceptions/TooManyChoicesException.java b/Src/PRuntimes/PExRuntime/src/main/java/pex/utils/exceptions/TooManyChoicesException.java index e739e67a15..22f7cd9d80 100644 --- a/Src/PRuntimes/PExRuntime/src/main/java/pex/utils/exceptions/TooManyChoicesException.java +++ b/Src/PRuntimes/PExRuntime/src/main/java/pex/utils/exceptions/TooManyChoicesException.java @@ -1,8 +1,11 @@ package pex.utils.exceptions; +import lombok.Getter; import pex.runtime.PExGlobal; public class TooManyChoicesException extends BugFoundException { + @Getter + String loc = ""; /** * Constructs a new TooManyChoicesException for choose(.) with too choices in a single call. * @@ -12,6 +15,7 @@ public class TooManyChoicesException extends BugFoundException { public TooManyChoicesException(String loc, int numChoices) { super(String.format("%s: choose expects a parameter with at most %d choices, got %d choices instead.", loc, PExGlobal.getConfig().getMaxChoicesPerStmtPerCall(), numChoices)); + this.loc = loc; } /** @@ -26,5 +30,6 @@ public TooManyChoicesException(String loc, int numChoices, int numCalls) { %s: too many choices generated from this statement - total %d choices after %d choose calls. Reduce the total number of choices generated here to at most %d, by reducing the number of times this choose statement is called.""", loc, numChoices, numCalls, PExGlobal.getConfig().getMaxChoicesPerStmtPerSchedule())); + this.loc = loc; } }