Skip to content

Commit

Permalink
[PEx] Minor updates and cleanup (#775)
Browse files Browse the repository at this point in the history 
* [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

* [PEx] Refactoring and formatting changes

* [PEx] Update cli default

Change each task to 2K schedules by default
  • Loading branch information
@aman-goel
aman-goel authored Sep 25, 2024
1 parent 5c8abf0 commit ad66ede
Show file tree
Hide file tree
Showing 12 changed files with 118 additions and 198 deletions.
32 changes: 20 additions & 12 deletions Src/PRuntimes/PExRuntime/src/main/java/pex/RuntimeExecutor.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -157,29 +157,33 @@ private static void process() throws Exception {
throw new Exception("MEMOUT", e);
} catch (BugFoundException e) {
PExGlobal.setStatus(STATUS.BUG_FOUND);
PExGlobal.setResult(String.format("found cex of length %d", e.getScheduler().getStepNumber()));
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);
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);
Expand Down Expand Up @@ -218,25 +222,29 @@ 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);
PExGlobal.setResult(String.format("found cex of length %,d", replayer.getStepNumber()));
replayer.getLogger().logStackTrace((Exception) replayException);
PExLogger.logTrace((Exception) replayException);
throw new BugFoundException(replayException.getMessage(), replayException);
} catch (BugFoundException replayException) {
PExGlobal.setStatus(STATUS.BUG_FOUND);
PExGlobal.setResult(String.format("found cex of length %d", replayer.getStepNumber()));
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);
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();
Expand Down
6 changes: 3 additions & 3 deletions Src/PRuntimes/PExRuntime/src/main/java/pex/commandline/PExConfig.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -71,14 +71,14 @@ public class PExConfig {
ChoiceSelectorMode choiceSelectorMode = ChoiceSelectorMode.Random;
// max number of schedules per search task
@Setter
int maxSchedulesPerTask = 500;
int maxSchedulesPerTask = 2000;
//max number of children search tasks
@Setter
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;
}
18 changes: 9 additions & 9 deletions Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/PExGlobal.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -245,13 +245,13 @@ public static void updateResult() {
if (numUnexplored == 0) {
resultString += "correct for any depth";
} else {
resultString += String.format("partially correct with %d choices remaining", numUnexplored);
resultString += String.format("partially correct with %,d choices remaining", numUnexplored);
}
} else {
if (numUnexplored == 0) {
resultString += String.format("correct up to step %d", getMaxSteps());
resultString += String.format("correct up to step %,d", getMaxSteps());
} else {
resultString += String.format("partially correct up to step %d with %d choices remaining", getMaxSteps(), numUnexplored);
resultString += String.format("partially correct up to step %,d with %,d choices remaining", getMaxSteps(), numUnexplored);
}
}
result = resultString;
Expand Down Expand Up @@ -332,20 +332,20 @@ public static void printProgress(boolean forcePrint) {
s.append(StringUtils.center(String.format("%s", runtimeHms), 11));
s.append(
StringUtils.center(String.format("%.1f GB", MemoryMonitor.getMemSpent() / 1024), 9));
s.append(StringUtils.center(String.format("%d / %d / %d",
s.append(StringUtils.center(String.format("%,d / %,d / %,d",
runningTasks.size(), finishedTasks.size(), pendingTasks.size()),
24));

s.append(StringUtils.center(String.format("%d", getTotalSchedules()), 12));
s.append(StringUtils.center(String.format("%d", timelines.size()), 12));
s.append(StringUtils.center(String.format("%,d", getTotalSchedules()), 12));
s.append(StringUtils.center(String.format("%,d", timelines.size()), 12));
// s.append(
// StringUtils.center(
// String.format(
// "%d (%.0f %% data)", getNumUnexploredChoices(), getUnexploredDataChoicesPercent()),
// 24));

if (config.getStateCachingMode() != StateCachingMode.None) {
s.append(StringUtils.center(String.format("%d", stateCache.size()), 12));
s.append(StringUtils.center(String.format("%,d", stateCache.size()), 12));
}

System.out.print(s);
Expand Down Expand Up @@ -380,8 +380,8 @@ public static int getMaxSteps() {
return result;
}

public static int getTotalSteps() {
int result = 0;
public static long getTotalSteps() {
long result = 0;
for (ExplicitSearchScheduler sch : searchSchedulers.values()) {
result += sch.getStats().totalSteps;
}
Expand Down
38 changes: 22 additions & 16 deletions Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/logger/PExLogger.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,9 +13,6 @@
import pex.runtime.scheduler.explicit.strategy.SearchStrategyMode;
import pex.utils.monitor.MemoryMonitor;

import java.io.PrintWriter;
import java.io.StringWriter;

/**
* Represents the main PEx logger
*/
Expand Down Expand Up @@ -65,7 +62,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("--------------------");
Expand All @@ -78,16 +75,16 @@ public static void logEndOfRun(long timeSpent) {
if (PExGlobal.getConfig().getSearchStrategyMode() != SearchStrategyMode.Replay) {
log.info("... Search statistics:");
if (PExGlobal.getConfig().getStateCachingMode() != StateCachingMode.None) {
log.info(String.format("..... Explored %d distinct states over %d timelines",
log.info(String.format("..... Explored %,d distinct states over %,d timelines",
PExGlobal.getStateCache().size(), PExGlobal.getTimelines().size()));
}
log.info(String.format("..... Explored %d distinct schedules", PExGlobal.getTotalSchedules()));
log.info(String.format("..... Finished %d search tasks (%d pending)",
log.info(String.format("..... Explored %,d distinct schedules", PExGlobal.getTotalSchedules()));
log.info(String.format("..... Finished %,d search tasks (%,d pending)",
PExGlobal.getFinishedTasks().size(), PExGlobal.getPendingTasks().size()));
log.info(String.format("..... Number of steps explored: %d (min), %d (avg), %d (max).",
log.info(String.format("..... Number of steps explored: %,d (min), %,d (avg), %,d (max).",
PExGlobal.getMinSteps(), (PExGlobal.getTotalSteps() / PExGlobal.getTotalSchedules()), PExGlobal.getMaxSteps()));
}
log.info(String.format("... Elapsed %d seconds and used %.1f GB", timeSpent, MemoryMonitor.getMaxMemSpent() / 1000.0));
log.info(String.format("... Elapsed %,d seconds and used %.1f GB", timeSpent, MemoryMonitor.getMaxMemSpent() / 1000.0));
log.info(String.format(".. \033[0;30;47m Result: %s \033[m", PExGlobal.getResult()));
log.info(". Done");
}
Expand All @@ -97,12 +94,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));
}

/**
Expand All @@ -112,6 +109,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()));
}
}
34 changes: 26 additions & 8 deletions Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/logger/SchedulerLogger.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down Expand Up @@ -100,7 +104,7 @@ public void logStartTask(SearchTask task) {
*/
public void logEndTask(SearchTask task, int numSchedules) {
if (verbosity > 0) {
log.info(String.format(" Finished %s after exploring %d schedules", task, numSchedules));
log.info(String.format(" Finished %s after exploring %,d schedules", task, numSchedules));
}
}

Expand All @@ -117,7 +121,7 @@ public void logNextTask(SearchTask task) {

public void logNewTasks(List<SearchTask> tasks) {
if (verbosity > 0) {
log.info(String.format(" Added %d new tasks", tasks.size()));
log.info(String.format(" Added %,d new tasks", tasks.size()));
}
if (verbosity > 1) {
for (SearchTask task : tasks) {
Expand Down Expand Up @@ -207,9 +211,9 @@ public void logNewScheduleChoice(List<PMachineId> choices, int step, int idx) {
}
}

public void logNewDataChoice(List<PValue<?>> choices, int step, int idx) {
public void logNewDataChoice(String loc, List<PValue<?>> 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));
}
}

Expand All @@ -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));
}
}

Expand Down Expand Up @@ -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<PValue<?>> choices) {
if (verbosity > 0) {
log.info(String.format(" @%d::%d %d new data choices from %s - %s", step, idx, choices.size(), loc, choices));
}
}
}
Loading

0 comments on commit ad66ede

Please sign in to comment.